Add model for vstd Set and prove its axioms

[matthias-brun]

This PR proves the set axioms and adds a fold function for finite sets (which is used to define cardinality) with associated lemmas.

The way things are bootstrapped is as follows:

• Sets are defined as functions from key to boolean
• A set is finite if there exists a surjective mapping into the natural numbers up to some upper bound
• This allows us to define most set operations except for cardinality
• We then define fold on finite sets by porting Isabelle/HOL's definitions and lemmas for it
  • Because of the inductive predicate-style encoding, we don't need a decreasing measure for induction proofs (We could use e.g. the finiteness upper bound but it's very annoying to do)
• Finally, we define set cardinality as self.fold(|a, b: nat| b + 1, 0)

I'm not sure about where the fold module should go. The current place (inline in set.rs) probably isn't it. But it needs to be a submodule of set to see the bodies of closed functions and the non-public items. We could move set.rs to set/mod.rs and then have set/fold.rs, which wouldn't break any imports of vstd::set. But arguably set_lib.rs should then also live in the set directory, which would be a breaking change. How should I best handle this?

Some miscellaneous notes:

• Isabelle uses a 3-clause BSD license, which is compatible with Verus' MIT license
• Isabelle's fold lemmas only require the function to be commutative on the set to be folded. I decided to require fully commutative functions
  • Triggering is tricky enough with these higher-order predicates, adding another set into the mix that might be defined with a closure doesn't help.
• There was an existing definition of fold for sets, which I replaced with the new one
  • It was based on the recursive encoding with self.choose() which makes reasoning about it very hard
  • That's presumably the reason why there weren't any associated lemmas for it
  • Maybe some of the admitted proofs in tokens.rs can now be proved (I didn't try)
• Aside: The obvious recursive fold (if s == set![] { z } else { f(s.choose(), fold(s.remove(s.choose())), f, z) }) is hard to reason about because the induction hypothesis is useless. The elements of s.remove(s.choose()) might be folded in a completely different order than those of s.

@tjhance I added you as a reviewer since tokens.rs seems to be the only current user of fold (within Verus/vstd)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

having fold as a submodule seems fine to me.

[utaal]

Veritas before:

veritas report for verus main (65f122f2ba42939cd5065a6e398c088067ee33c7) with features: singular

project	revspec	outcome	total verus time (ms)	smt run time (ms)
verus-vstd	main (65f122f2ba42939cd5065a6e398c088067ee33c7)	success (837 verified, 0 errors)	26070	10173
memory-allocator	main (bc2ba93dc916aef3afa347b92c5c8d66cb23fee7)	success (730 verified, 0 errors)	69692	159591
verified-storage	main (7b35ddb12fd505e16a58d9462f15aed559570267)	success (272 verified, 0 errors)	9808	10616
node-replication	main (b3ca921103220b20c6cc144bd2f7d4f259b7c8be)	success (254 verified, 0 errors)	8831	2700

Veritas after:

veritas report for verus verified-set-axioms (db4a7a860f483ff990165c3816ce2d962049481e) with features: singular

project	revspec	outcome	total verus time (ms)	smt run time (ms)
verus-vstd	verified-set-axioms (db4a7a860f483ff990165c3816ce2d962049481e)	success (841 verified, 0 errors)	26729	9286
memory-allocator	main (bc2ba93dc916aef3afa347b92c5c8d66cb23fee7)	success (730 verified, 0 errors)	64478	46088
verified-storage	main (7b35ddb12fd505e16a58d9462f15aed559570267)	success (272 verified, 0 errors)	10307	10694
node-replication	main (b3ca921103220b20c6cc144bd2f7d4f259b7c8be)	success (254 verified, 0 errors)	9413	2895

Memory allocator seems to get a significant smt time speedup, which is strange.
@matthias-brun can you please rebase this branch on main to see if we've had a regression on main since you forked?

(Oh, this may be due to the bug in reporting smt times that @Chris-Hawblitzel spotted a couple of weeks ago.)

[utaal]

After the rebase:

veritas report for verus verified-set-axioms (76eb59694f4497d04d98e3cdfa8c338c059b3714) with features: singular

project	revspec	outcome	total verus time (ms)	smt run time (ms)
verus-vstd	verified-set-axioms (76eb59694f4497d04d98e3cdfa8c338c059b3714)	success (851 verified, 0 errors)	25745	10075
memory-allocator	main (bc2ba93dc916aef3afa347b92c5c8d66cb23fee7)	success (730 verified, 0 errors)	66756	146411
verified-storage	main (7b35ddb12fd505e16a58d9462f15aed559570267)	success (272 verified, 0 errors)	9665	10523
node-replication	main (b3ca921103220b20c6cc144bd2f7d4f259b7c8be)	success (254 verified, 0 errors)	8693	2683

No significant deviations, as expected.