Standard collections should use type information to identify finiteness

[jonhnet]

Where Dafny has separate types for set/iset and map/imap, Verus chose a single type for each that supports infinites, and then adds broadcast rules that say ∀m.m_is_finite() ⇒ m.some_good_thing().

The unfortunate consequence is that, when you're expecting your maps to be finite, and they're not, you end up chasing down wild goose assertion failures, since the broadcast rules can't tell you that they're failing to trigger.

This reminds me of one of the main motivations for creating Verus in the first place: ownership types moved a bunch of confusing SMT errors into crystal clear type errors. I propose that we should separate infinite maps (sets, seqs) from finite maps (sets, seqs) using types.

Having to split into a separate Map:IMap type would suck. How about a Finite trait, and define type Map = IMap + Finite? In common usage, we'd always type Map, as usual, and get finiteness, but most of the map properties would actually derive from IMap, so they'd be available there, too. And impl IMap could offer as_finite() -> Map that requires is_finite(): that is, you can use an SMT obligation to upgrade the type.

[jaybosamiya-ms]

My 2 cents: I'm not fully sure if we can define a Finite trait of that kind, but a couple of alternatives:

• Alternative 1 (newtype pattern): Define pub struct FiniteMap { map: Map } (note the private field) that simply re-exposes everything from Map except it enforces is_finite(). This does need either adding wrapper functions to forward Map functions over, or would need a Deref(Mut) implementation or such. Existing users of Map are left unaffected, since this is just a wrapper.

• Alternative 2 (const-generic arg): Update the current pub struct Map<K, V> to pub struct Map<K, V, const POSSIBLY_INFINITE: bool=true>. One could add a convenience alias of FiniteMap<K, V> = Map<K, V, false> and not even need to add the wrapper functions for each existing function, unlike in alternative 1. Also, any existing user of Map is left unaffected, since POSSIBLY_INFINITE has the default of true.

Personally, I think alternative 2 is more elegant and would likely be easier to maintain in the long run.

[tjhance]

I would love to have a FiniteMap type. One advantage that hasn't been mentioned yet is that FiniteMap<K, V> can have K be marked accept_recursive_types

[jonhnet]

I'm glad it's getting traction! As a second order suggestion, if we pull this off, I think it make senses to have Map be the finite version. Experience suggests finite maps appear much more frequently than infinite. (I'm not super concerned about "existing users of Map". The language is young; better to make good choices now than start the ossification process early.)

[jaybosamiya-ms]

I agree Map being finite by default is the better move overall. My mention if "existing users" was mostly to provide a smoother migration path for folks without suddenly having a breakage. Specifically, changing it to suddenly mean "finite" is placing an (implicit) assumption, which could be harder to diagnose in a proof failure. With that in mind, here's a possible migration path:

• Step 1: Add POSSIBLY_INFINITE but do not add a default to it. This will cause breakages, but purely at type checking level, which is easier to diagnose (people will see the type, put a true/false there based on what they are using the map as, and move on)
• Step 2: Wait till we're confident everyone has picked true/false.
• Step 3: Make POSSIBLY_INFINITE default to false. This will help get the better default. Folks who picked true/false are just being more explicit with their intention, but do not need to debug a proof failure.
• Step 4: World domination

It is possible I am overthinking this though, and maybe a single-step change would be ok

[jonhnet]

Wait, why not step 4?

[jaybosamiya-ms]

Knowledge about step 4 possibly breaching containment. Applying evasive countermeasures.

Step 4? What step 4?

[utaal]

I'm going to add that, pedagogically, the nuance of finite() as a predicate has caused some confusion. I had to specifically introduce students in the UdS course to the idea that the same type can represent both finite and infinite maps, and I don't think that I was fully successful in conveying how knowledge of finiteness made certain reasoning available (while the knowledge of !finite() did not). I'm in favor of some form of type-based information carrying the finiteness of a Map: I'm not yet sure what's the exact right thing to do which will minimize confusion.

[tjhance]

There's one important technical thing to consider, which is that commonly used functions like Map::new don't work with finite maps, not without some way to check that the domain is finite. I believe dafny has heuristics for this (which usually worked well IIRC), but it's more awkward for us since we don't have set comprehension or map comprehensions as primitive constructs. We should think about how we want to handle this.

[jonhnet]

Well, we could have a Map::new variant where the domain argument is a Set, in particular a Set that has the corresponding finite-type property annotation.

That means that common patterns like this still don't work:
Map::new(|i| 0<=i<foo.len(), foo[i])

Dafny solves this with a shallow syntax analysis that recognizes the finiteness of that set expression. We could instead ask users to use standard library functions, such as Set::range(0, foo.len()), which would return a Set+Finite (or however it gets expressed).

I guess the idea is this: By hypothesis there are only a few common patterns that people use to generate most finite sets (map domains); that's why Dafny can get away with syntax regexes. If that's so, we'd encode those same patterns with a few std library functions (like Set::range above). The only downside is that we're asking users to discover the existence of such functions they need to call. But maybe we can do a clever shallow syntax analysis in the help diagnostic to nudge users in the right direction for common cases.

[parno]

More supporting evidence for making finite/infinite more obvious in the type system:
#1525

[Chris-Hawblitzel]

Alternative 2 (const-generic arg): Update the current pub struct Map<K, V> to pub struct Map<K, V, const POSSIBLY_INFINITE: bool=true>. One could add a convenience alias of FiniteMap<K, V> = Map<K, V, false> and not even need to add the wrapper functions for each existing function, unlike in alternative 1. Also, any existing user of Map is left unaffected, since POSSIBLY_INFINITE has the default of true. Personally, I think alternative 2 is more elegant and would likely be easier to maintain in the long run

I would love to have a FiniteMap type. One advantage that hasn't been mentioned yet is that FiniteMap<K, V> can have K be marked accept_recursive_types

I like both of these ideas, but we'll need a way to allow them to work together. Right now, you can only put one accept/reject-recursive types declaration on any given struct, so I think we'll need a more flexible declaration of accept/reject.

[jonhnet]

Okay, I have a draft of these changes here:
https://github.com/verus-lang/verus/tree/jonh/sets-typed-finite

Current status:
I have three of the four veritas projects updated to work with the new syntax. I've done most of verified-memory-allocator, but have run into some trouble; I'm hoping @tjhance can check in and help me over the finish line.

Observations to discuss:

Error messages: The error messages for using the wrong type of set aren't very good. I'd want "expected ISet, found Set," but instead we have "expected false, found true".

Ergonomics for finite constructions: Code that uses finite Set has some trouble producing witnesses for the map in Set::int_range().map() constructors. Moreso with whichever library it was that wanted nat ranges; had to build up a library. Not sure there's anything more elegant we can do. I think we need to see code written from scratch in finite style to see how well it's working out.

VerusSync isn't generic: In my changes, verussync macros use IMaps. This is opinionated, it sort of forces applications (verified-memory-allocator, verified-node-replication) to stay in IMap land. Conceivably, we could make verussync generic over finiteness, but I'm out of bandwidth for trying that experiment.

I think these issues might be tolerable in exchange for finally landing this first version of the feature, but maybe I'm saying that just because I've been staring at it for too long.

[parno]

Error messages: The error messages for using the wrong type of set aren't very good. I'd want "expected ISet, found Set," but instead we have "expected false, found true".

Since one of the motivations for this change was to make it easier to discover when you've mixed up your set types, this drawback is a bit worrisome. Ignoring costs, what would it take to provide an improved error message here? I.e., what mechanism would we want to add?

[tjhance]

This might be a viable alternative:

struct Finite;
struct Infinite;

trait Finiteness { }

impl Finiteness for Finite { }

impl Finiteness for Infinite { }

struct Map<FINITE: Finiteness> {
    _finite: FINITE,
}

type FiniteMap = Map<Finite>;
type InfiniteMap = Map<Infinite>;

It gives a much nicer error message:

fn test(m: InfiniteMap) {
}

fn test2(m: FiniteMap) {
    test(m);
}

error[E0308]: mismatched types
  --> test.rs:21:10
   |
21 |     test(m);
   |     ---- ^ expected `Map<Infinite>`, found `Map<Finite>`
   |     |
   |     arguments to this function are incorrect
   |
   = note: expected struct `Map<Infinite>`
              found struct `Map<Finite>`

[jonhnet]

Travis, your solution works. Thanks!

[jonhnet]

Veritas project links and status:

verified-memory-allocator
https://github.com/jonhnet/verified-memory-allocator/tree/jonh/sets-typed-finite
status: some assume(false) statements remain where I couldn't debug due to challenges with VerusSync macro opacity.

page-table
https://github.com/jonhnet/verified-nrkernel/tree/jonh/sets-typed-finite
status: Fails with one rlimit exceeded, but the main veritas fails with two. This code base seems to have some timeout hygiene challenges.

verified-storage
https://github.com/jonhnet/verified-storage/tree/jonh/sets-typed-finite
status: works locally, but in veritas, I get:

            crate `deps_hack` compiled by rustc 1.82.0 ...
    = help: please recompile that crate using this compiler (rustc 1.85.1 (4eb161250 2025-03-15)) (consider running `cargo clean` first)

node-replication
https://github.com/jonhnet/verified-node-replication/tree/jonh/sets-typed-finite
Passes in veritas.