Make `Set` and `Map` finite, add `ISet` and `IMap`.#2486

Draft

jaylorch wants to merge 167 commits into

verus-lang:mainfrom

jaylorch:sets-typed-finite

Commits on Oct 16, 2025

supersquash
Jon Howell
committed
slogging away on rotted lemma_to_seq_to_set_id
Jon Howell
committed
set_lib sorted
Jon Howell
committed
lemma_set_filter_finite
Jon Howell
committed
semantic fixups
Jon Howell
committed
restore run_configuration_all.toml
Jon Howell
committed
vargo fmt
Jon Howell
committed
correct builtin reference
Jon Howell
committed
replace an admit with a proof
Jon Howell
committed
fix standalone vstd build
Jon Howell
committed
vargo fmt
Jon Howell
committed
fix refs that break in test
Jon Howell
committed
verusfmt
Jon Howell
committed
deprecate set_int_range for Set::int_range
Jon Howell
committed
better error messages with structs instead of const bool
Jon Howell
committed
fmt
Jon Howell
committed
Set::nat_range
Jon Howell
committed
end mk_map. fix a bunch of tests
Jon Howell
committed
fmt, clean up mk_map leftovers
Jon Howell
committed
update decreases tests to check both names for finite, infinite maps
Jon Howell
committed
expose rustc_diagnostic_items
Jon Howell
committed
fix invariants, multiset tests
Jon Howell
committed
fix tests/sets
Jon Howell
committed
fix summer_school tests; add automation for to_infinite ensures
Jon Howell
committed
fmt
Jon Howell
committed
draft of doc fixes
Jon Howell
committed
doc suggestions from bryan; fix assumes in set.rs
Jon Howell
committed
minimize lemma_fold_graph_insert_elim_aux
Jon Howell
committed
correct typos in lib_exmaples
Jon Howell
committed
fmt
Jon Howell
committed
correct vstd.rs merge
Jon Howell
committed
apply some comments from parno
Jon Howell
committed
apply parno comments
Jon Howell
committed
fmt
Jon Howell
committed
grammar
Jon Howell
committed
rename lemmas that aren't axioms anymore
Jon Howell
committed
correct comments
Jon Howell
committed
generic flatten
Jon Howell
committed
progress on flatten
Jon Howell
committed
progress on flatten proofs
Jon Howell
committed
tighten up filter_map_congruence
Jon Howell
committed
fix last assume in flatten proof
Jon Howell
committed
kill a couple no-op lemmas
Jon Howell
committed
kill another couple no-op lemma
Jon Howell
committed
sort out some TODOs in set.rs
Jon Howell
committed
kill no-op lemma in set_lib
Jon Howell
committed
kill no-op lemma in set_lib
Jon Howell
committed
fmt
Jon Howell
committed
delete dead comment
Jon Howell
committed
fix Set ctor in tests/raw_ptrs/allocate_in_bounds
Jon Howell
committed
incorporate Chris' generalized Set::range
Jon Howell
committed
fmt
Jon Howell
committed
shift tests and examples to Set::range
Jon Howell
committed
remove extn tilde -- why did this break in CI?
Jon Howell
committed
update token stufen changes
Jon Howell
committed
fmt
Jon Howell
committed
update token stufen changes
Jon Howell
committed
Fix old references to Set to point to GSet
Jon Howell
committed
add lemmas to ease porting to ISet
Jon Howell
committed
fmt
Jon Howell
committed
add lemma_set_disjoint_lens_finite
Jon Howell
committed
fmt
Jon Howell
committed
duplicate ensures trigger to attempt to address test flake
Jon Howell
committed
Chris' set and set_lib additions
Jon Howell
committed
add a broadcast
Jon Howell
committed
fmt
Jon Howell
committed
sharded state machines support iset,imap,set,map separately
Jon Howell
committed
add infinite/finite variants of PersistentMap, PersistentSet, StorageMap
Jon Howell
committed
fmt
Jon Howell
committed
missing imap/iset variant code
Jon Howell
committed
missing pieces for ISet, PersistentISet and friends
Jon Howell
committed
fmt
Jon Howell
committed
fix more infinite/finite discrepancies in state machines
Jon Howell
committed
fmt
Jon Howell
committed

Commits on Feb 21, 2026

work-in-progress snapshot of GSet refactor

jonhnet
and
claude
committed

Commits on Feb 22, 2026

Commits on Feb 23, 2026

Commits on Feb 25, 2026

hide GSet type
jonhnet
committed

Commits on Feb 26, 2026

hide GSet surface
jonhnet
committed

Commits on Feb 28, 2026

Commits on Mar 2, 2026

Fix std/alloc vstd proof regressions in hash and pptr
jonhnet
committed

Commits on May 6, 2026

last work unit
jonhnet
committed

Commits on May 13, 2026

Commits on May 14, 2026

Add reach_type
jaylorch
committed

Commits on May 15, 2026

Partial progress
jaylorch
committed

Commits on May 16, 2026

More progress
jaylorch
committed

Commits on May 18, 2026

Commits on May 19, 2026

Commits on May 20, 2026

Commits on May 21, 2026

Commits on May 26, 2026

Fix failing tests
jaylorch
committed