From ef885dc422788ea886c93aa635cc01d75bd856b9 Mon Sep 17 00:00:00 2001 From: Matthias Date: Sat, 1 Feb 2025 11:20:58 +0100 Subject: [PATCH 1/2] Add model for vstd Set and prove its axioms --- source/vstd/map.rs | 4 +- source/vstd/set.rs | 631 ++++++++++++++++++++++++++++++++++++++--- source/vstd/set_lib.rs | 20 -- source/vstd/tokens.rs | 3 +- 4 files changed, 593 insertions(+), 65 deletions(-) diff --git a/source/vstd/map.rs b/source/vstd/map.rs index 1ce1f0c8f..8dbae7460 100644 --- a/source/vstd/map.rs +++ b/source/vstd/map.rs @@ -41,13 +41,13 @@ impl Map { /// Gives a `Map` whose domain contains every key, and maps each key /// to the value given by `fv`. - pub open spec fn total(fv: impl Fn(K) -> V) -> Map { + pub open spec fn total(fv: spec_fn(K) -> V) -> Map { Set::full().mk_map(fv) } /// Gives a `Map` whose domain is given by the boolean predicate on keys `fk`, /// and maps each key to the value given by `fv`. - pub open spec fn new(fk: impl Fn(K) -> bool, fv: impl Fn(K) -> V) -> Map { + pub open spec fn new(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V) -> Map { Set::new(fk).mk_map(fv) } diff --git a/source/vstd/set.rs b/source/vstd/set.rs index 2dec920ed..238e5c4b1 100644 --- a/source/vstd/set.rs +++ b/source/vstd/set.rs @@ -1,5 +1,3 @@ -use core::marker; - #[allow(unused_imports)] use super::map::*; #[allow(unused_imports)] @@ -28,19 +26,29 @@ verus! { /// /// To prove that two sequences are equal, it is usually easiest to use the extensionality /// operator `=~=`. -#[verifier::external_body] #[verifier::ext_equal] #[verifier::reject_recursive_types(A)] pub struct Set { - dummy: marker::PhantomData, + set: spec_fn(A) -> bool, } impl Set { /// The "empty" set. - pub spec fn empty() -> Set; + pub closed spec fn empty() -> Set { + Set { set: |a| false } + } /// Set whose membership is determined by the given boolean predicate. - pub spec fn new bool>(f: F) -> Set; + pub closed spec fn new(f: spec_fn(A) -> bool) -> Set { + Set { + set: |a| + if f(a) { + true + } else { + false + }, + } + } /// The "full" set, i.e., set containing every element of type `A`. pub open spec fn full() -> Set { @@ -48,7 +56,9 @@ impl Set { } /// Predicate indicating if the set contains the given element. - pub spec fn contains(self, a: A) -> bool; + pub closed spec fn contains(self, a: A) -> bool { + (self.set)(a) + } /// Predicate indicating if the set contains the given element: supports `self has a` syntax. #[verifier::inline] @@ -68,14 +78,34 @@ impl Set { /// Returns a new set with the given element inserted. /// If that element is already in the set, then an identical set is returned. - pub spec fn insert(self, a: A) -> Set; + pub closed spec fn insert(self, a: A) -> Set { + Set { + set: |a2| + if a2 == a { + true + } else { + (self.set)(a2) + }, + } + } /// Returns a new set with the given element removed. /// If that element is already absent from the set, then an identical set is returned. - pub spec fn remove(self, a: A) -> Set; + pub closed spec fn remove(self, a: A) -> Set { + Set { + set: |a2| + if a2 == a { + false + } else { + (self.set)(a2) + }, + } + } /// Union of two sets. - pub spec fn union(self, s2: Set) -> Set; + pub closed spec fn union(self, s2: Set) -> Set { + Set { set: |a| (self.set)(a) || (s2.set)(a) } + } /// `+` operator, synonymous with `union` #[verifier::inline] @@ -84,7 +114,9 @@ impl Set { } /// Intersection of two sets. - pub spec fn intersect(self, s2: Set) -> Set; + pub closed spec fn intersect(self, s2: Set) -> Set { + Set { set: |a| (self.set)(a) && (s2.set)(a) } + } /// `*` operator, synonymous with `intersect` #[verifier::inline] @@ -93,7 +125,9 @@ impl Set { } /// Set difference, i.e., the set of all elements in the first one but not in the second. - pub spec fn difference(self, s2: Set) -> Set; + pub closed spec fn difference(self, s2: Set) -> Set { + Set { set: |a| (self.set)(a) && !(s2.set)(a) } + } /// Set complement (within the space of all possible elements in `A`). /// `-` operator, synonymous with `difference` @@ -102,18 +136,29 @@ impl Set { self.difference(s2) } - pub spec fn complement(self) -> Set; + pub closed spec fn complement(self) -> Set { + Set { set: |a| !(self.set)(a) } + } /// Set of all elements in the given set which satisfy the predicate `f`. - pub open spec fn filter bool>(self, f: F) -> Set { + pub open spec fn filter(self, f: spec_fn(A) -> bool) -> Set { self.intersect(Self::new(f)) } /// Returns `true` if the set is finite. - pub spec fn finite(self) -> bool; + pub closed spec fn finite(self) -> bool { + exists|f: spec_fn(A) -> nat, ub: nat| + { + &&& #[trigger] trigger_finite(f, ub) + &&& surj_on(f, self) + &&& forall|a| self.contains(a) ==> f(a) < ub + } + } /// Cardinality of the set. (Only meaningful if a set is finite.) - pub spec fn len(self) -> nat; + pub closed spec fn len(self) -> nat { + self.fold(|a, b: nat| b + 1, 0) + } /// Chooses an arbitrary element of the set. /// @@ -127,7 +172,7 @@ impl Set { /// Creates a [`Map`] whose domain is the given set. /// The values of the map are given by `f`, a function of the keys. - pub spec fn mk_map V>(self, f: F) -> Map; + pub closed spec fn mk_map(self, f: spec_fn(A) -> V) -> Map; /// Returns `true` if the sets are disjoint, i.e., if their interesection is /// the empty set. @@ -136,13 +181,426 @@ impl Set { } } -// Trusted axioms +// Closures make triggering finicky but using this to trigger explicitly works well. +spec fn trigger_finite(f: spec_fn(A) -> nat, ub: nat) -> bool { + true +} + +spec fn surj_on(f: spec_fn(A) -> B, s: Set) -> bool { + forall|a1, a2| #![all_triggers] s.contains(a1) && s.contains(a2) && a1 != a2 ==> f(a1) != f(a2) +} + +pub mod fold { + //! This module defines a fold function for finite sets and proves a number of associated + //! lemmas. + //! + //! The module was ported (with some modifications) from Isabelle/HOL's finite set theory in: + //! `HOL/Finite_Set.thy` + //! That file contains the following author list: + //! + //! + //! (* Title: HOL/Finite_Set.thy + //! Author: Tobias Nipkow + //! Author: Lawrence C Paulson + //! Author: Markus Wenzel + //! Author: Jeremy Avigad + //! Author: Andrei Popescu + //! *) + //! + //! + //! The file is distributed under a 3-clause BSD license as indicated in the file `COPYRIGHT` + //! in Isabelle's root directory, which also carries the following copyright notice: + //! + //! Copyright (c) 1986-2024, + //! University of Cambridge, + //! Technische Universitaet Muenchen, + //! and contributors. + use super::*; + + broadcast group group_set_axioms_early { + axiom_set_empty, + axiom_set_new, + axiom_set_insert_same, + axiom_set_insert_different, + axiom_set_remove_same, + axiom_set_remove_insert, + axiom_set_remove_different, + axiom_set_union, + axiom_set_intersect, + axiom_set_difference, + axiom_set_complement, + axiom_set_ext_equal, + axiom_set_ext_equal_deep, + axiom_set_empty_finite, + axiom_set_insert_finite, + axiom_set_remove_finite, + } + + pub open spec fn is_fun_commutative(f: spec_fn(A, B) -> B) -> bool { + forall|a1, a2, b| #[trigger] f(a1, f(a2, b)) == f(a2, f(a1, b)) + } + + // This predicate is intended to be used like an inductive predicate, with the corresponding + // introduction, elimination and induction rules proved below. + #[verifier(opaque)] + spec fn fold_graph(f: spec_fn(A, B) -> B, z: B, s: Set, y: B, d: nat) -> bool + decreases d, + { + if s === Set::empty() { + &&& z == y + &&& d == 0 + } else { + exists|yr, a| + { + &&& #[trigger] trigger_fold_graph(yr, a) + &&& d > 0 + &&& s.remove(a).finite() + &&& s.contains(a) + &&& fold_graph(f, z, s.remove(a), yr, sub(d, 1)) + &&& y == f(a, yr) + } + } + } + + spec fn trigger_fold_graph(yr: B, a: A) -> bool { + true + } + + // Introduction rules + proof fn lemma_fold_graph_empty_intro(f: spec_fn(A, B) -> B, z: B) + ensures + fold_graph(f, z, Set::empty(), z, 0), + { + reveal(fold_graph); + } + + proof fn lemma_fold_graph_insert_intro( + f: spec_fn(A, B) -> B, + z: B, + s: Set, + y: B, + d: nat, + a: A, + ) + requires + fold_graph(f, z, s, y, d), + !s.contains(a), + ensures + fold_graph(f, z, s.insert(a), f(a, y), d + 1), + { + broadcast use group_set_axioms_early; + + reveal(fold_graph); + let _ = trigger_fold_graph(y, a); + assert(s == s.insert(a).remove(a)); + } + + // Elimination rules + proof fn lemma_fold_graph_empty_elim(f: spec_fn(A, B) -> B, z: B, y: B, d: nat) + requires + fold_graph(f, z, Set::empty(), y, d), + ensures + z == y, + d == 0, + { + reveal(fold_graph); + } + + proof fn lemma_fold_graph_insert_elim( + f: spec_fn(A, B) -> B, + z: B, + s: Set, + y: B, + d: nat, + a: A, + ) + requires + is_fun_commutative(f), + fold_graph(f, z, s.insert(a), y, d), + !s.contains(a), + ensures + d > 0, + exists|yp| y == f(a, yp) && #[trigger] fold_graph(f, z, s, yp, sub(d, 1)), + { + reveal(fold_graph); + lemma_fold_graph_insert_elim_aux(f, z, s.insert(a), y, d, a); + assert(s.insert(a).remove(a) =~= s); + let yp = choose|yp| y == f(a, yp) && #[trigger] fold_graph(f, z, s, yp, sub(d, 1)); + } + + proof fn lemma_fold_graph_insert_elim_aux( + f: spec_fn(A, B) -> B, + z: B, + s: Set, + y: B, + d: nat, + a: A, + ) + requires + is_fun_commutative(f), + fold_graph(f, z, s, y, d), + s.contains(a), + ensures + exists|yp| y == f(a, yp) && #[trigger] fold_graph(f, z, s.remove(a), yp, sub(d, 1)), + decreases d, + { + broadcast use group_set_axioms_early; + + reveal(fold_graph); + let (yr, aa): (B, A) = choose|yr, aa| + #![all_triggers] + { + &&& trigger_fold_graph(yr, a) + &&& d > 0 + &&& s.remove(aa).finite() + &&& s.contains(aa) + &&& fold_graph(f, z, s.remove(aa), yr, sub(d, 1)) + &&& y == f(aa, yr) + }; + assert(trigger_fold_graph(yr, a)); + if s.remove(aa) === Set::empty() { + } else { + if a == aa { + } else { + lemma_fold_graph_insert_elim_aux(f, z, s.remove(aa), yr, sub(d, 1), a); + let yrp = choose|yrp| + yr == f(a, yrp) && #[trigger] fold_graph( + f, + z, + s.remove(aa).remove(a), + yrp, + sub(d, 2), + ); + assert(fold_graph(f, z, s.remove(aa).insert(aa).remove(a), f(aa, yrp), sub(d, 1))) + by { + assert(s.remove(aa).remove(a) == s.remove(aa).insert(aa).remove(a).remove(aa)); + assert(trigger_fold_graph(yrp, aa)); + }; + } + } + } + + // Induction rule + proof fn lemma_fold_graph_induct( + f: spec_fn(A, B) -> B, + z: B, + s: Set, + y: B, + d: nat, + pred: spec_fn(Set, B, nat) -> bool, + ) + requires + is_fun_commutative(f), + fold_graph(f, z, s, y, d), + pred(Set::empty(), z, 0), + forall|a, s, y, d| + pred(s, y, d) && !s.contains(a) && #[trigger] fold_graph(f, z, s, y, d) ==> pred( + #[trigger] s.insert(a), + f(a, y), + d + 1, + ), + ensures + pred(s, y, d), + decreases d, + { + broadcast use group_set_axioms_early; + + reveal(fold_graph); + if s === Set::empty() { + lemma_fold_graph_empty_elim(f, z, y, d); + } else { + let a = s.choose(); + lemma_fold_graph_insert_elim(f, z, s.remove(a), y, d, a); + let yp = choose|yp| + y == f(a, yp) && #[trigger] fold_graph(f, z, s.remove(a), yp, sub(d, 1)); + lemma_fold_graph_induct(f, z, s.remove(a), yp, sub(d, 1), pred); + } + } + + impl Set { + pub closed spec fn fold(self, f: spec_fn(A, B) -> B, z: B) -> B + recommends + self.finite(), + is_fun_commutative(f), + { + let (y, d): (B, nat) = choose|y, d| fold_graph(f, z, self, y, d); + y + } + } + + proof fn lemma_fold_graph_finite(f: spec_fn(A, B) -> B, z: B, s: Set, y: B, d: nat) + requires + is_fun_commutative(f), + fold_graph(f, z, s, y, d), + ensures + s.finite(), + { + broadcast use group_set_axioms_early; + + let pred = |s: Set, y, d| s.finite(); + lemma_fold_graph_induct(f, z, s, y, d, pred); + } + + proof fn lemma_fold_graph_deterministic( + f: spec_fn(A, B) -> B, + z: B, + s: Set, + y1: B, + y2: B, + d1: nat, + d2: nat, + ) + requires + is_fun_commutative(f), + fold_graph(f, z, s, y1, d1), + fold_graph(f, z, s, y2, d2), + ensures + y1 == y2, + d1 == d2, + { + let pred = |s: Set, y1: B, d1: nat| + forall|y2, d2| fold_graph(f, z, s, y2, d2) ==> y1 == y2 && d2 == d1; + // Base case + assert(pred(Set::empty(), z, 0)) by { + assert forall|y2, d2| fold_graph(f, z, Set::empty(), y2, d2) implies z == y2 && d2 + == 0 by { + lemma_fold_graph_empty_elim(f, z, y2, d2); + }; + }; + // Step case + assert forall|a, s, y1, d1| + pred(s, y1, d1) && !s.contains(a) && #[trigger] fold_graph( + f, + z, + s, + y1, + d1, + ) implies pred(#[trigger] s.insert(a), f(a, y1), d1 + 1) by { + assert forall|y2, d2| fold_graph(f, z, s.insert(a), y2, d2) implies f(a, y1) == y2 && d2 + == d1 + 1 by { + lemma_fold_graph_insert_elim(f, z, s, y2, d2, a); + }; + }; + lemma_fold_graph_induct(f, z, s, y2, d2, pred); + } + + proof fn lemma_fold_is_fold_graph(f: spec_fn(A, B) -> B, z: B, s: Set, y: B, d: nat) + requires + is_fun_commutative(f), + fold_graph(f, z, s, y, d), + ensures + s.fold(f, z) == y, + { + lemma_fold_graph_finite(f, z, s, y, d); + if s.fold(f, z) != y { + let (y2, d2) = choose|y2, d2| fold_graph(f, z, s, y2, d2) && y2 != y; + lemma_fold_graph_deterministic(f, z, s, y2, y, d2, d); + assert(false); + } + } + + // At this point set cardinality is not yet defined, so we can't easily give a decreasing + // measure to prove the subsequent lemma `lemma_fold_graph_exists`. Instead, we first prove + // this lemma, for which we use the upper bound of a finiteness witness as the decreasing + // measure. + pub proof fn lemma_finite_set_induct(s: Set, pred: spec_fn(Set) -> bool) + requires + s.finite(), + pred(Set::empty()), + forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)), + ensures + pred(s), + { + let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger] + trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub); + lemma_finite_set_induct_aux(s, f, ub, pred); + } + + proof fn lemma_finite_set_induct_aux( + s: Set, + f: spec_fn(A) -> nat, + ub: nat, + pred: spec_fn(Set) -> bool, + ) + requires + surj_on(f, s), + s.finite(), + forall|a| s.contains(a) ==> f(a) < ub, + pred(Set::empty()), + forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)), + ensures + pred(s), + decreases ub, + { + broadcast use group_set_axioms_early; + + if s =~= Set::empty() { + } else { + let a = s.choose(); + // If `f` maps something to `ub - 1`, remap it to `f(a)` so we can decrease ub + let fp = |aa| + if f(aa) == ub - 1 { + f(a) + } else { + f(aa) + }; + lemma_finite_set_induct_aux(s.remove(a), fp, sub(ub, 1), pred); + } + } + + proof fn lemma_fold_graph_exists(f: spec_fn(A, B) -> B, z: B, s: Set) + requires + s.finite(), + is_fun_commutative(f), + ensures + exists|y, d| fold_graph(f, z, s, y, d), + { + let pred = |s| exists|y, d| fold_graph(f, z, s, y, d); + // Base case + assert(fold_graph(f, z, Set::empty(), z, 0)) by { + lemma_fold_graph_empty_intro(f, z); + }; + // Step case + assert forall|s, a| pred(s) && s.finite() && !s.contains(a) implies #[trigger] pred( + s.insert(a), + ) by { + let (y, d): (B, nat) = choose|y, d| fold_graph(f, z, s, y, d); + lemma_fold_graph_insert_intro(f, z, s, y, d, a); + }; + lemma_finite_set_induct(s, pred); + } + + pub broadcast proof fn lemma_fold_insert(s: Set, f: spec_fn(A, B) -> B, z: B, a: A) + requires + s.finite(), + !s.contains(a), + is_fun_commutative(f), + ensures + #[trigger] s.insert(a).fold(f, z) == f(a, s.fold(f, z)), + { + lemma_fold_graph_exists(f, z, s); + let (y, d): (B, nat) = choose|y, d| fold_graph(f, z, s, y, d); + lemma_fold_graph_insert_intro(f, z, s, s.fold(f, z), d, a); + lemma_fold_is_fold_graph(f, z, s.insert(a), f(a, s.fold(f, z)), d + 1); + } + + pub broadcast proof fn lemma_fold_empty(f: spec_fn(A, B) -> B, z: B) + ensures + #[trigger] Set::empty().fold(f, z) == z, + { + let (y, d): (B, nat) = choose|y, d| fold_graph(f, z, Set::empty(), y, d); + lemma_fold_graph_empty_intro(f, z); + lemma_fold_graph_empty_elim(f, z, y, d); + } + +} + +// Axioms /// The empty set contains no elements pub broadcast proof fn axiom_set_empty(a: A) ensures !(#[trigger] Set::empty().contains(a)), { - admit(); } /// A call to `Set::new` with the predicate `f` contains `a` if and only if `f(a)` is true. @@ -150,7 +608,6 @@ pub broadcast proof fn axiom_set_new(f: spec_fn(A) -> bool, a: A) ensures #[trigger] Set::new(f).contains(a) == f(a), { - admit(); } /// The result of inserting element `a` into set `s` must contains `a`. @@ -158,7 +615,6 @@ pub broadcast proof fn axiom_set_insert_same(s: Set, a: A) ensures #[trigger] s.insert(a).contains(a), { - admit(); } /// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s` @@ -169,7 +625,6 @@ pub broadcast proof fn axiom_set_insert_different(s: Set, a1: A, a2: A) ensures #[trigger] s.insert(a2).contains(a1) == s.contains(a1), { - admit(); } /// The result of removing element `a` from set `s` must not contain `a`. @@ -177,7 +632,6 @@ pub broadcast proof fn axiom_set_remove_same(s: Set, a: A) ensures !(#[trigger] s.remove(a).contains(a)), { - admit(); } /// Removing an element `a` from a set `s` and then inserting `a` back into the set` @@ -218,7 +672,6 @@ pub broadcast proof fn axiom_set_remove_different(s: Set, a1: A, a2: A) ensures #[trigger] s.remove(a2).contains(a1) == s.contains(a1), { - admit(); } /// The union of sets `s1` and `s2` contains element `a` if and only if @@ -227,7 +680,6 @@ pub broadcast proof fn axiom_set_union(s1: Set, s2: Set, a: A) ensures #[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)), { - admit(); } /// The intersection of sets `s1` and `s2` contains element `a` if and only if @@ -236,7 +688,6 @@ pub broadcast proof fn axiom_set_intersect(s1: Set, s2: Set, a: A) ensures #[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)), { - admit(); } /// The set difference between `s1` and `s2` contains element `a` if and only if @@ -245,7 +696,6 @@ pub broadcast proof fn axiom_set_difference(s1: Set, s2: Set, a: A) ensures #[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)), { - admit(); } /// The complement of set `s` contains element `a` if and only if `s` does not contain `a`. @@ -253,7 +703,6 @@ pub broadcast proof fn axiom_set_complement(s: Set, a: A) ensures #[trigger] s.complement().contains(a) == !s.contains(a), { - admit(); } /// Sets `s1` and `s2` are equal if and only if they contain all of the same elements. @@ -261,14 +710,24 @@ pub broadcast proof fn axiom_set_ext_equal(s1: Set, s2: Set) ensures #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)), { - admit(); + if s1 =~= s2 { + assert(forall|a: A| s1.contains(a) == s2.contains(a)); + } + if forall|a: A| s1.contains(a) == s2.contains(a) { + if !(forall|a: A| #[trigger] (s1.set)(a) <==> (s2.set)(a)) { + assert(exists|a: A| #[trigger] (s1.set)(a) != (s2.set)(a)); + let a = choose|a: A| #[trigger] (s1.set)(a) != (s2.set)(a); + assert(s1.contains(a)); + assert(false); + } + assert(s1 =~= s2); + } } pub broadcast proof fn axiom_set_ext_equal_deep(s1: Set, s2: Set) ensures #[trigger] (s1 =~~= s2) <==> s1 =~= s2, { - admit(); } pub broadcast proof fn axiom_mk_map_domain(s: Set, f: spec_fn(K) -> V) @@ -293,7 +752,9 @@ pub broadcast proof fn axiom_set_empty_finite() ensures #[trigger] Set::::empty().finite(), { - admit(); + let f = |a: A| 0; + let ub = 0; + let _ = trigger_finite(f, ub); } /// The result of inserting an element `a` into a finite set `s` is also finite. @@ -303,7 +764,34 @@ pub broadcast proof fn axiom_set_insert_finite(s: Set, a: A) ensures #[trigger] s.insert(a).finite(), { - admit(); + let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger] + trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub); + let f2 = |a2: A| + if a2 == a { + ub + } else { + f(a2) + }; + let ub2 = ub + 1; + let _ = trigger_finite(f2, ub2); + assert forall|a1, a2| + #![all_triggers] + s.insert(a).contains(a1) && s.insert(a).contains(a2) && a1 != a2 implies f2(a1) != f2( + a2, + ) by { + if a != a1 { + assert(s.contains(a1)); + } + if a != a2 { + assert(s.contains(a2)); + } + }; + assert forall|a2| s.insert(a).contains(a2) implies #[trigger] f2(a2) < ub2 by { + if a == a2 { + } else { + assert(s.contains(a2)); + } + }; } /// The result of removing an element `a` from a finite set `s` is also finite. @@ -313,7 +801,25 @@ pub broadcast proof fn axiom_set_remove_finite(s: Set, a: A) ensures #[trigger] s.remove(a).finite(), { - admit(); + let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger] + trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub); + assert forall|a1, a2| + #![all_triggers] + s.remove(a).contains(a1) && s.remove(a).contains(a2) && a1 != a2 implies f(a1) != f(a2) by { + if a != a1 { + assert(s.contains(a1)); + } + if a != a2 { + assert(s.contains(a2)); + } + }; + assert(surj_on(f, s.remove(a))); + assert forall|a2| s.remove(a).contains(a2) implies #[trigger] f(a2) < ub by { + if a == a2 { + } else { + assert(s.contains(a2)); + } + }; } /// The union of two finite sets is finite. @@ -324,7 +830,21 @@ pub broadcast proof fn axiom_set_union_finite(s1: Set, s2: Set) ensures #[trigger] s1.union(s2).finite(), { - admit(); + let (f1, ub1) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger] + trigger_finite(f, ub) && surj_on(f, s1) && (forall|a| s1.contains(a) ==> f(a) < ub); + let (f2, ub2) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger] + trigger_finite(f, ub) && surj_on(f, s2) && (forall|a| s2.contains(a) ==> f(a) < ub); + let f3 = |a| + if s1.contains(a) { + f1(a) + } else { + ub1 + f2(a) + }; + let ub3 = ub1 + ub2; + assert(trigger_finite(f3, ub3)); + assert(forall|a| + #![all_triggers] + s1.union(s2).contains(a) ==> s1.contains(a) || s2.contains(a)); } /// The intersection of two finite sets is finite. @@ -334,7 +854,9 @@ pub broadcast proof fn axiom_set_intersect_finite(s1: Set, s2: Set) ensures #[trigger] s1.intersect(s2).finite(), { - admit(); + assert(forall|a| + #![all_triggers] + s1.intersect(s2).contains(a) ==> s1.contains(a) && s2.contains(a)); } /// The set difference between two finite sets is finite. @@ -344,7 +866,9 @@ pub broadcast proof fn axiom_set_difference_finite(s1: Set, s2: Set) ensures #[trigger] s1.difference(s2).finite(), { - admit(); + assert(forall|a| + #![all_triggers] + s1.difference(s2).contains(a) ==> s1.contains(a) && !s2.contains(a)); } /// An infinite set `s` contains the element `s.choose()`. @@ -354,7 +878,9 @@ pub broadcast proof fn axiom_set_choose_finite(s: Set) ensures #[trigger] s.contains(s.choose()), { - admit(); + let f = |a: A| 0; + let ub = 0; + let _ = trigger_finite(f, ub); } // Trusted axioms about len @@ -365,7 +891,7 @@ pub broadcast proof fn axiom_set_empty_len() ensures #[trigger] Set::::empty().len() == 0, { - admit(); + fold::lemma_fold_empty(|a: A, b: nat| b + 1, 0); } /// The result of inserting an element `a` into a finite set `s` has length @@ -380,7 +906,11 @@ pub broadcast proof fn axiom_set_insert_len(s: Set, a: A) 1 }), { - admit(); + if s.contains(a) { + assert(s =~= s.insert(a)); + } else { + fold::lemma_fold_insert(s, |a: A, b: nat| b + 1, 0, a); + } } /// The result of removing an element `a` from a finite set `s` has length @@ -395,7 +925,13 @@ pub broadcast proof fn axiom_set_remove_len(s: Set, a: A) 0 }), { - admit(); + axiom_set_remove_finite(s, a); + axiom_set_insert_len(s.remove(a), a); + if s.contains(a) { + assert(s =~= s.remove(a).insert(a)); + } else { + assert(s =~= s.remove(a)); + } } /// If a finite set `s` contains any element, it has length greater than 0. @@ -406,7 +942,11 @@ pub broadcast proof fn axiom_set_contains_len(s: Set, a: A) ensures #[trigger] s.len() != 0, { - admit(); + let a = s.choose(); + assert(s.remove(a).insert(a) =~= s); + axiom_set_remove_finite(s, a); + axiom_set_insert_finite(s.remove(a), a); + axiom_set_insert_len(s.remove(a), a); } /// A finite set `s` contains the element `s.choose()` if it has length greater than 0. @@ -417,7 +957,14 @@ pub broadcast proof fn axiom_set_choose_len(s: Set) ensures #[trigger] s.contains(s.choose()), { - admit(); + // Separate statements to work around https://github.com/verus-lang/verusfmt/issues/86 + broadcast use axiom_set_contains_len; + broadcast use axiom_set_empty_len; + broadcast use axiom_set_ext_equal; + broadcast use axiom_set_insert_finite; + + let pred = |s: Set| s.finite() ==> s.len() == 0 <==> s =~= Set::empty(); + fold::lemma_finite_set_induct(s, pred); } pub broadcast group group_set_axioms { diff --git a/source/vstd/set_lib.rs b/source/vstd/set_lib.rs index b8a6dbfe3..9966a0279 100644 --- a/source/vstd/set_lib.rs +++ b/source/vstd/set_lib.rs @@ -30,26 +30,6 @@ impl Set { Set::new(|a: B| exists|x: A| self.contains(x) && a == f(x)) } - /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by - /// the choose operator. - /// - /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)` - /// returns `f(...f(f(init, x0), x1), ..., xn)`. - pub open spec fn fold(self, init: E, f: spec_fn(E, A) -> E) -> E - decreases self.len(), - { - if self.finite() { - if self.len() == 0 { - init - } else { - let a = self.choose(); - self.remove(a).fold(f(init, a), f) - } - } else { - arbitrary() - } - } - /// Converts a set into a sequence with an arbitrary ordering. pub open spec fn to_seq(self) -> Seq recommends diff --git a/source/vstd/tokens.rs b/source/vstd/tokens.rs index 55ab4ad73..79c810000 100644 --- a/source/vstd/tokens.rs +++ b/source/vstd/tokens.rs @@ -465,7 +465,7 @@ pub tracked struct MultisetToken } spec fn map_values(m: Map) -> Multiset { - m.dom().fold(Multiset::empty(), |multiset: Multiset, k: K| multiset.insert(m[k])) + m.dom().fold(|k: K, multiset: Multiset| multiset.insert(m[k]), Multiset::empty()) } proof fn map_values_insert_not_in(m: Map, k: K, v: V) @@ -536,6 +536,7 @@ impl MultisetToken s.multiset() === Multiset::empty(), { let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData, }; + broadcast use super::set::fold::lemma_fold_empty; assert(Self::map_elems(Map::empty()) =~= Map::empty()); return s; } From db4a7a860f483ff990165c3816ce2d962049481e Mon Sep 17 00:00:00 2001 From: Matthias Date: Mon, 3 Feb 2025 13:11:54 +0100 Subject: [PATCH 2/2] Fix set fold test --- source/rust_verify_test/tests/sets.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/source/rust_verify_test/tests/sets.rs b/source/rust_verify_test/tests/sets.rs index 03d19b67a..6058b143c 100644 --- a/source/rust_verify_test/tests/sets.rs +++ b/source/rust_verify_test/tests/sets.rs @@ -111,12 +111,12 @@ test_verify_one_file! { proof fn test() { let s: Set = set![9]; - reveal_with_fuel(Set::fold, 10); + broadcast use fold::lemma_fold_insert, fold::lemma_fold_empty; assert(s.finite()); assert(s.len() > 0); - assert(s.fold(0, |p: nat, a: nat| p + a) == 9); + assert(s.fold(|p: nat, a: nat| p + a, 0) == 9); - assert(set![].fold(0, |p: nat, a: nat| p + a) == 0); + assert(set![].fold(|p: nat, a: nat| p + a, 0) == 0); } } => Ok(()) }