From 4e67ff6e0d02b37522d3e0d6f282c443b3b2a9b6 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Wed, 30 Oct 2024 10:59:14 -0700 Subject: [PATCH 1/4] prove theorem about fold_right over permutations For a commutative fold_right operator, any folding order (i.e., folding over any permutation of a sequence) produces the same result. --- source/vstd/seq_lib.rs | 84 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 82 insertions(+), 2 deletions(-) diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs index 6bfc05691..f4e4fe695 100644 --- a/source/vstd/seq_lib.rs +++ b/source/vstd/seq_lib.rs @@ -446,6 +446,7 @@ impl Seq { pub proof fn to_multiset_ensures(self) ensures forall|a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a), + forall|i: int| 0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset()) =~= self.to_multiset().remove(self[i]), self.len() == self.to_multiset().len(), forall|a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0, { @@ -453,6 +454,10 @@ impl Seq { (self.push(a).to_multiset()) =~= self.to_multiset().insert(a) by { to_multiset_build(self, a); } + assert forall|i: int| 0 <= i < self.len() implies #[trigger] + (self.remove(i).to_multiset()) =~= self.to_multiset().remove(self[i]) by { + to_multiset_remove(self, i); + } to_multiset_len(self); assert forall|a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0 by { to_multiset_contains(self, a); @@ -649,14 +654,16 @@ impl Seq { /// An auxiliary lemma for proving [`Self::lemma_fold_right_alt`]. proof fn aux_lemma_fold_right_alt(self, f: spec_fn(A, B) -> B, b: B, k: int) requires - 0 <= k < self.len(), + 0 <= k <= self.len(), ensures self.subrange(0, k).fold_right(f, self.subrange(k, self.len() as int).fold_right(f, b)) == self.fold_right(f, b), decreases self.len(), { reveal_with_fuel(Seq::fold_right, 2); - if k == self.len() - 1 { + if k == self.len() { + assert(self.subrange(0, k) == self); + } else if k == self.len() - 1 { // trivial base case } else { self.subrange(0, self.len() - 1).aux_lemma_fold_right_alt(f, f(self.last(), b), k); @@ -1320,6 +1327,23 @@ proof fn to_multiset_build(s: Seq, a: A) } } +proof fn to_multiset_remove(s: Seq, i: int) + requires + 0 <= i < s.len() + ensures + s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]) +{ + broadcast use super::multiset::group_multiset_axioms; + + let s0 = s.subrange(0, i); + let s1 = s.subrange(i, s.len() as int); + let s2 = s.subrange(i+1, s.len() as int); + lemma_seq_union_to_multiset_commutative(s0, s2); + lemma_seq_union_to_multiset_commutative(s0, s1); + assert(s == s0 + s1); + assert(s2+s0 == (s1+s0).drop_first()); +} + /// to_multiset() preserves length proof fn to_multiset_len(s: Seq) ensures @@ -1669,6 +1693,62 @@ pub proof fn lemma_seq_subrange_elements(s: Seq, start: int, stop: int, x: } } +// Definition of a commutative fold_right operator. +pub open spec fn commutative_foldr(f: spec_fn(A, B) -> B) -> bool { + forall |x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) +} + +// Helper lemma that it's possible to commute a commutative operator across fold_right. +proof fn lemma_fold_right_commute_one(l: Seq, a: A, f: spec_fn(A, B) -> B, v: B) + requires + commutative_foldr(f) + ensures + l.fold_right(f, f(a, v)) == f(a, l.fold_right(f, v)) + decreases + l.len() +{ + if l.len() > 0 { + lemma_fold_right_commute_one(l.drop_last(), a, f, f(l.last(), v)); + } +} + +// For a commutative fold_right operator, any folding order +// (i.e., any permutation) produces the same result. +pub proof fn fold_right_permutation(l1: Seq, l2: Seq, f: spec_fn(A, B) -> B, v: B) + requires + commutative_foldr(f), + l1.to_multiset() == l2.to_multiset(), + ensures + l1.fold_right(f, v) == l2.fold_right(f, v) + decreases + l1.len() +{ + l1.to_multiset_ensures(); + l2.to_multiset_ensures(); + + if l1.len() > 0 { + let a = l1.last(); + let i = l2.index_of(a); + let l2r = l2.subrange(i+1, l2.len() as int).fold_right(f, v); + + assert(l1.to_multiset().count(a) > 0); + lemma_fold_right_commute_one(l1.drop_last(), a, f, v); + lemma_fold_right_commute_one(l2.subrange(0, i), a, f, l2r); + + l2.aux_lemma_fold_right_alt(f, v, i+1); + l2.remove(i).aux_lemma_fold_right_alt(f, v, i); + + assert(l2.subrange(0, i+1).drop_last() == l2.subrange(0, i)); + assert(l1.drop_last() == l1.remove(l1.len() - 1)); + + assert(l2.remove(i).subrange(0, i) == l2.subrange(0, i)); + assert(l2.remove(i).subrange(i, l2.remove(i).len() as int) == + l2.subrange(i+1, l2.len() as int)); + + fold_right_permutation(l1.drop_last(), l2.remove(i), f, v); + } +} + /************************** Lemmas about Take/Skip ***************************/ // This verified lemma used to be an axiom in the Dafny prelude From 3d3028e4ea7898730a2c2f0c8a8d8952d6f44801 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Wed, 30 Oct 2024 11:39:53 -0700 Subject: [PATCH 2/4] add the converse of lemma_multiset_has_no_duplicates --- source/vstd/seq_lib.rs | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs index f4e4fe695..384ca3018 100644 --- a/source/vstd/seq_lib.rs +++ b/source/vstd/seq_lib.rs @@ -720,6 +720,34 @@ impl Seq { } } + /// If, in a sequence's conversion to a multiset, each element occurs only once, + /// the sequence has no duplicates. + pub proof fn lemma_multiset_has_no_duplicates_conv(self) + requires + forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1 + ensures + self.no_duplicates() + { + broadcast use super::multiset::group_multiset_axioms; + + assert forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) implies self[i] != self[j] by { + let mut a = if (i < j) { i } else { j }; + let mut b = if (i < j) { j } else { i }; + + if (self[a] == self[b]) { + let s0 = self.subrange(0, b); + let s1 = self.subrange(b, self.len() as int); + assert(self == s0 + s1); + + s0.to_multiset_ensures(); + s1.to_multiset_ensures(); + + lemma_multiset_commutative(s0, s1); + assert(self.to_multiset().count(self[a]) >= 2); + } + } + } + /// The concatenation of two subsequences derived from a non-empty sequence, /// the first obtained from skipping the last element, the second consisting only /// of the last element, is the original sequence. From bb7ec6b50bee22df4bc978bd22440a4e1977d436 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Wed, 30 Oct 2024 12:02:53 -0700 Subject: [PATCH 3/4] make verusfmt happy --- source/vstd/seq_lib.rs | 61 +++++++++++++++++++++++++----------------- 1 file changed, 36 insertions(+), 25 deletions(-) diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs index 384ca3018..24b6c08d7 100644 --- a/source/vstd/seq_lib.rs +++ b/source/vstd/seq_lib.rs @@ -446,7 +446,9 @@ impl Seq { pub proof fn to_multiset_ensures(self) ensures forall|a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a), - forall|i: int| 0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset()) =~= self.to_multiset().remove(self[i]), + forall|i: int| + 0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset()) + =~= self.to_multiset().remove(self[i]), self.len() == self.to_multiset().len(), forall|a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0, { @@ -454,8 +456,8 @@ impl Seq { (self.push(a).to_multiset()) =~= self.to_multiset().insert(a) by { to_multiset_build(self, a); } - assert forall|i: int| 0 <= i < self.len() implies #[trigger] - (self.remove(i).to_multiset()) =~= self.to_multiset().remove(self[i]) by { + assert forall|i: int| 0 <= i < self.len() implies #[trigger] (self.remove(i).to_multiset()) + =~= self.to_multiset().remove(self[i]) by { to_multiset_remove(self, i); } to_multiset_len(self); @@ -724,15 +726,24 @@ impl Seq { /// the sequence has no duplicates. pub proof fn lemma_multiset_has_no_duplicates_conv(self) requires - forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1 + forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1, ensures - self.no_duplicates() + self.no_duplicates(), { broadcast use super::multiset::group_multiset_axioms; - assert forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) implies self[i] != self[j] by { - let mut a = if (i < j) { i } else { j }; - let mut b = if (i < j) { j } else { i }; + assert forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) implies self[i] + != self[j] by { + let mut a = if (i < j) { + i + } else { + j + }; + let mut b = if (i < j) { + j + } else { + i + }; if (self[a] == self[b]) { let s0 = self.subrange(0, b); @@ -1357,19 +1368,19 @@ proof fn to_multiset_build(s: Seq, a: A) proof fn to_multiset_remove(s: Seq, i: int) requires - 0 <= i < s.len() + 0 <= i < s.len(), ensures - s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]) + s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]), { broadcast use super::multiset::group_multiset_axioms; let s0 = s.subrange(0, i); let s1 = s.subrange(i, s.len() as int); - let s2 = s.subrange(i+1, s.len() as int); + let s2 = s.subrange(i + 1, s.len() as int); lemma_seq_union_to_multiset_commutative(s0, s2); lemma_seq_union_to_multiset_commutative(s0, s1); assert(s == s0 + s1); - assert(s2+s0 == (s1+s0).drop_first()); + assert(s2 + s0 == (s1 + s0).drop_first()); } /// to_multiset() preserves length @@ -1723,17 +1734,16 @@ pub proof fn lemma_seq_subrange_elements(s: Seq, start: int, stop: int, x: // Definition of a commutative fold_right operator. pub open spec fn commutative_foldr(f: spec_fn(A, B) -> B) -> bool { - forall |x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) + forall|x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) } // Helper lemma that it's possible to commute a commutative operator across fold_right. proof fn lemma_fold_right_commute_one(l: Seq, a: A, f: spec_fn(A, B) -> B, v: B) requires - commutative_foldr(f) + commutative_foldr(f), ensures - l.fold_right(f, f(a, v)) == f(a, l.fold_right(f, v)) - decreases - l.len() + l.fold_right(f, f(a, v)) == f(a, l.fold_right(f, v)), + decreases l.len(), { if l.len() > 0 { lemma_fold_right_commute_one(l.drop_last(), a, f, f(l.last(), v)); @@ -1747,9 +1757,8 @@ pub proof fn fold_right_permutation(l1: Seq, l2: Seq, f: spec_fn(A, commutative_foldr(f), l1.to_multiset() == l2.to_multiset(), ensures - l1.fold_right(f, v) == l2.fold_right(f, v) - decreases - l1.len() + l1.fold_right(f, v) == l2.fold_right(f, v), + decreases l1.len(), { l1.to_multiset_ensures(); l2.to_multiset_ensures(); @@ -1757,21 +1766,23 @@ pub proof fn fold_right_permutation(l1: Seq, l2: Seq, f: spec_fn(A, if l1.len() > 0 { let a = l1.last(); let i = l2.index_of(a); - let l2r = l2.subrange(i+1, l2.len() as int).fold_right(f, v); + let l2r = l2.subrange(i + 1, l2.len() as int).fold_right(f, v); assert(l1.to_multiset().count(a) > 0); lemma_fold_right_commute_one(l1.drop_last(), a, f, v); lemma_fold_right_commute_one(l2.subrange(0, i), a, f, l2r); - l2.aux_lemma_fold_right_alt(f, v, i+1); + l2.aux_lemma_fold_right_alt(f, v, i + 1); l2.remove(i).aux_lemma_fold_right_alt(f, v, i); - assert(l2.subrange(0, i+1).drop_last() == l2.subrange(0, i)); + assert(l2.subrange(0, i + 1).drop_last() == l2.subrange(0, i)); assert(l1.drop_last() == l1.remove(l1.len() - 1)); assert(l2.remove(i).subrange(0, i) == l2.subrange(0, i)); - assert(l2.remove(i).subrange(i, l2.remove(i).len() as int) == - l2.subrange(i+1, l2.len() as int)); + assert(l2.remove(i).subrange(i, l2.remove(i).len() as int) == l2.subrange( + i + 1, + l2.len() as int, + )); fold_right_permutation(l1.drop_last(), l2.remove(i), f, v); } From 2e7ddb154b7272ca4469b5f13a7903a0b0955002 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Wed, 30 Oct 2024 13:38:34 -0700 Subject: [PATCH 4/4] make some more seq lemmas public lemma_fold_right_split (formerly aux_lemma_fold_right_alt) is a useful lemma in its own right about how fold_right distributes over splitting a sequence into two parts using subrange. lemma_fold_right_commute_one is also useful for proofs that need to commute the order of operations in fold_right, in a way that's not quite about permutations. --- source/vstd/seq_lib.rs | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs index 24b6c08d7..0475d2b53 100644 --- a/source/vstd/seq_lib.rs +++ b/source/vstd/seq_lib.rs @@ -653,8 +653,8 @@ impl Seq { } } - /// An auxiliary lemma for proving [`Self::lemma_fold_right_alt`]. - proof fn aux_lemma_fold_right_alt(self, f: spec_fn(A, B) -> B, b: B, k: int) + /// A lemma that proves how [`Self::fold_right`] distributes over splitting a sequence. + pub proof fn lemma_fold_right_split(self, f: spec_fn(A, B) -> B, b: B, k: int) requires 0 <= k <= self.len(), ensures @@ -668,7 +668,7 @@ impl Seq { } else if k == self.len() - 1 { // trivial base case } else { - self.subrange(0, self.len() - 1).aux_lemma_fold_right_alt(f, f(self.last(), b), k); + self.subrange(0, self.len() - 1).lemma_fold_right_split(f, f(self.last(), b), k); assert_seqs_equal!( self.subrange(0, self.len() - 1).subrange(0, k) == self.subrange(0, k) @@ -684,6 +684,19 @@ impl Seq { } } + // Lemma that proves it's possible to commute a commutative operator across fold_right. + pub proof fn lemma_fold_right_commute_one(self, a: A, f: spec_fn(A, B) -> B, v: B) + requires + commutative_foldr(f), + ensures + self.fold_right(f, f(a, v)) == f(a, self.fold_right(f, v)), + decreases self.len(), + { + if self.len() > 0 { + self.drop_last().lemma_fold_right_commute_one(a, f, f(self.last(), v)); + } + } + /// [`Self::fold_right`] and [`Self::fold_right_alt`] are equivalent. pub proof fn lemma_fold_right_alt(self, f: spec_fn(A, B) -> B, b: B) ensures @@ -696,7 +709,7 @@ impl Seq { // trivial base cases } else { self.subrange(1, self.len() as int).lemma_fold_right_alt(f, b); - self.aux_lemma_fold_right_alt(f, b, 1); + self.lemma_fold_right_split(f, b, 1); } } @@ -1737,19 +1750,6 @@ pub open spec fn commutative_foldr(f: spec_fn(A, B) -> B) -> bool { forall|x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v)) } -// Helper lemma that it's possible to commute a commutative operator across fold_right. -proof fn lemma_fold_right_commute_one(l: Seq, a: A, f: spec_fn(A, B) -> B, v: B) - requires - commutative_foldr(f), - ensures - l.fold_right(f, f(a, v)) == f(a, l.fold_right(f, v)), - decreases l.len(), -{ - if l.len() > 0 { - lemma_fold_right_commute_one(l.drop_last(), a, f, f(l.last(), v)); - } -} - // For a commutative fold_right operator, any folding order // (i.e., any permutation) produces the same result. pub proof fn fold_right_permutation(l1: Seq, l2: Seq, f: spec_fn(A, B) -> B, v: B) @@ -1769,11 +1769,11 @@ pub proof fn fold_right_permutation(l1: Seq, l2: Seq, f: spec_fn(A, let l2r = l2.subrange(i + 1, l2.len() as int).fold_right(f, v); assert(l1.to_multiset().count(a) > 0); - lemma_fold_right_commute_one(l1.drop_last(), a, f, v); - lemma_fold_right_commute_one(l2.subrange(0, i), a, f, l2r); + l1.drop_last().lemma_fold_right_commute_one(a, f, v); + l2.subrange(0, i).lemma_fold_right_commute_one(a, f, l2r); - l2.aux_lemma_fold_right_alt(f, v, i + 1); - l2.remove(i).aux_lemma_fold_right_alt(f, v, i); + l2.lemma_fold_right_split(f, v, i + 1); + l2.remove(i).lemma_fold_right_split(f, v, i); assert(l2.subrange(0, i + 1).drop_last() == l2.subrange(0, i)); assert(l1.drop_last() == l1.remove(l1.len() - 1));