diff --git a/source/pervasive/seq.rs b/source/pervasive/seq.rs index 5ec08a3372..1745363fd5 100644 --- a/source/pervasive/seq.rs +++ b/source/pervasive/seq.rs @@ -28,37 +28,60 @@ verus! { /// To prove that two sequences are equal, it is usually easiest to use the /// extensional equality operator `=~=`. -#[verifier::external_body] -#[verifier::ext_equal] #[verifier::accept_recursive_types(A)] -pub struct Seq { - dummy: marker::PhantomData, +#[verifier::ext_equal] +pub enum Seq { + Nil, + Cons(A, Box>), } impl Seq { /// An empty sequence (i.e., a sequence of length 0). #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::empty"] - pub spec fn empty() -> Seq; + pub closed spec fn empty() -> Seq { + Seq::Nil + } /// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`. #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::new"] - pub spec fn new(len: nat, f: impl Fn(int) -> A) -> Seq; + pub closed spec fn new(len: nat, f: spec_fn(int) -> A) -> Seq + decreases len + { + if len == 0 { Seq::Nil } + else { + Self::new((len-1) as nat, f).push(f(len-1)) + } + } /// The length of a sequence. #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::len"] - pub spec fn len(self) -> nat; + pub closed spec fn len(self) -> nat + decreases self + { + match self { + Seq::Nil => 0, + Seq::Cons(_, l) => 1 + l.len(), + } + } /// Gets the value at the given index `i`. /// /// If `i` is not in the range `[0, self.len())`, then the resulting value - /// is meaningless and arbitrary. + /// is arbitrary(). #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::index"] - pub spec fn index(self, i: int) -> A - recommends 0 <= i < self.len(); + pub closed spec fn index(self, i: int) -> A + recommends 0 <= i < self.len() + decreases self + { + match self { + Seq::Nil => arbitrary(), + Seq::Cons(a, l) => if i == 0 { a } else { l.index(i-1) } + } + } /// `[]` operator, synonymous with `index` @@ -81,7 +104,14 @@ impl Seq { /// ``` #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::push"] - pub spec fn push(self, a: A) -> Seq; + pub closed spec fn push(self, a: A) -> Seq + decreases self + { + match self { + Seq::Nil => Seq::Cons(a, Box::new(Seq::Nil)), + Seq::Cons(x, l) => Seq::Cons(x, Box::new(l.push(a))), + } + } /// Updates the sequence at the given index, replacing the element with the given /// value, and leaves all other entries unchanged. @@ -97,8 +127,25 @@ impl Seq { /// ``` #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::update"] - pub spec fn update(self, i: int, a: A) -> Seq - recommends 0 <= i < self.len(); + pub closed spec fn update(self, i: int, a: A) -> Seq + recommends 0 <= i < self.len() + decreases self + { + if !(0 <= i < self.len()) { + // makes some additional lemmas hold for out-of-bounds updates + self + } else { + match self { + Seq::Nil => Seq::Nil, + Seq::Cons(x, l) => + if i == 0 { + Seq::Cons(a, l) + } else { + Seq::Cons(x, Box::new(l.update(i-1, a))) + } + } + } + } /// DEPRECATED: use =~= or =~~= instead. /// Returns `true` if the two sequences are pointwise equal, i.e., @@ -132,8 +179,25 @@ impl Seq { /// ``` #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::subrange"] - pub spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq - recommends 0 <= start_inclusive <= end_exclusive <= self.len(); + pub closed spec fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq + recommends 0 <= start_inclusive <= end_exclusive <= self.len() + decreases start_inclusive, end_exclusive-start_inclusive + { + match self { + Seq::Nil => Seq::Nil, + Seq::Cons(a, l) => + // skip elements until start_inclusive becomes 0 + if start_inclusive > 0 { + l.subrange(start_inclusive-1, end_exclusive-1) + } else { + if end_exclusive <= 0 { + Seq::Nil + } else { + Seq::Cons(a, Box::new(l.subrange(start_inclusive, end_exclusive-1))) + } + } + } + } /// Returns a sequence containing only the first n elements of the original sequence @@ -161,7 +225,14 @@ impl Seq { /// ``` #[rustc_diagnostic_item = "verus::pervasive::seq::Seq::add"] - pub spec fn add(self, rhs: Seq) -> Seq; + pub closed spec fn add(self, rhs: Seq) -> Seq + decreases self + { + match self { + Seq::Nil => rhs, + Seq::Cons(a, l) => Seq::Cons(a, Box::new(l.add(rhs))), + } + } /// `+` operator, synonymous with `add` @@ -189,8 +260,52 @@ impl Seq { } } +proof fn seq_len_0_empty(s: Seq) + requires s.len() == 0 + ensures s == Seq::::empty() +{ + match s { + Seq::Nil => {} + Seq::Cons(_, l) => { + assert(s.len() == 1 + l.len()); + assert(s.len() > 0); + } + } +} + // Trusted axioms +proof fn lemma_seq_index_decreases(s: Seq, i: int) + requires + 0 <= i < s.len(), + ensures + #[trigger](decreases_to!(s => s[i])), + decreases i +{ + match s { + Seq::Nil => { assert(false); } + Seq::Cons(a, l) => { + if i == 0 {} + else { + lemma_seq_index_decreases(*l, i-1); + } + } + } +} + +proof fn seq_index_out_of_bounds(s: Seq, i: int) + requires !(0 <= i < s.len()) + ensures s[i] == arbitrary::() + decreases s +{ + match s { + Seq::Nil => {} + Seq::Cons(_, l) => { + seq_index_out_of_bounds(*l, i-1); + } + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_index_decreases(s: Seq, i: int) @@ -201,6 +316,12 @@ pub proof fn axiom_seq_index_decreases(s: Seq, i: int) { } +proof fn lemma_seq_empty() + ensures + #[trigger] Seq::::empty().len() == 0, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_empty() @@ -209,6 +330,12 @@ pub proof fn axiom_seq_empty() { } +proof fn lemma_seq_new_len(len: nat, f: spec_fn(int) -> A) + ensures + #[trigger] Seq::new(len, f).len() == len, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_new_len(len: nat, f: spec_fn(int) -> A) @@ -217,6 +344,14 @@ pub proof fn axiom_seq_new_len(len: nat, f: spec_fn(int) -> A) { } +proof fn lemma_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) + requires + 0 <= i < len, + ensures + Seq::new(len, f)[i] == f(i), +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) @@ -227,6 +362,12 @@ pub proof fn axiom_seq_new_index(len: nat, f: spec_fn(int) -> A, i: int) { } +proof fn lemma_seq_push_len(s: Seq, a: A) + ensures + #[trigger] s.push(a).len() == s.len() + 1, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_push_len(s: Seq, a: A) @@ -235,6 +376,14 @@ pub proof fn axiom_seq_push_len(s: Seq, a: A) { } +proof fn lemma_seq_push_index_same(s: Seq, a: A, i: int) + requires + i == s.len(), + ensures + #[trigger] s.push(a)[i] == a, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_push_index_same(s: Seq, a: A, i: int) @@ -245,6 +394,24 @@ pub proof fn axiom_seq_push_index_same(s: Seq, a: A, i: int) { } +proof fn lemma_seq_push_index_different(s: Seq, a: A, i: int) + // 0 <= i not required + requires + i < s.len(), + ensures + s.push(a)[i] == s[i], + decreases s +{ + match s { + Seq::Nil => { + seq_index_out_of_bounds(s.push(a), i); + } + Seq::Cons(x, l) => { + lemma_seq_push_index_different(*l, a, i-1); + } + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_push_index_different(s: Seq, a: A, i: int) @@ -255,6 +422,15 @@ pub proof fn axiom_seq_push_index_different(s: Seq, a: A, i: int) { } +proof fn lemma_seq_update_len(s: Seq, i: int, a: A) + // precondition is not required + // requires + // 0 <= i < s.len(), + ensures + #[trigger] s.update(i, a).len() == s.len(), +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_update_len(s: Seq, i: int, a: A) @@ -265,6 +441,14 @@ pub proof fn axiom_seq_update_len(s: Seq, i: int, a: A) { } +proof fn lemma_seq_update_same(s: Seq, i: int, a: A) + requires + 0 <= i < s.len(), + ensures + #[trigger] s.update(i, a)[i] == a, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_update_same(s: Seq, i: int, a: A) @@ -275,6 +459,28 @@ pub proof fn axiom_seq_update_same(s: Seq, i: int, a: A) { } +proof fn lemma_seq_update_different(s: Seq, i1: int, i2: int, a: A) + requires + // these conditions are not required + // 0 <= i1 < s.len(), + // 0 <= i2 < s.len(), + i1 != i2, + ensures + s.update(i2, a)[i1] == s[i1], + decreases s +{ + match s { + Seq::Nil => { + } + Seq::Cons(x, l) => { + if i2 == 0 { + } else { + lemma_seq_update_different(*l, i1-1, i2-1, a); + } + } + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_update_different(s: Seq, i1: int, i2: int, a: A) @@ -287,6 +493,48 @@ pub proof fn axiom_seq_update_different(s: Seq, i1: int, i2: int, a: A) { } +proof fn seq_extensional_equality_index(s1: Seq, s2: Seq) + requires s1.len() == s2.len(), + forall |i: int| 0 <= i < s1.len() ==> s1[i] == s2[i], + ensures s1 == s2 + decreases s1 +{ + match s1 { + Seq::Nil => { + seq_len_0_empty(s2); + } + Seq::Cons(a, l1) => { + assert(s1.len() == 1 + l1.len()); + match s2 { + Seq::Nil => {}, + Seq::Cons(b, l2) => { + assert(s2.len() == 1 + l2.len()); + assert(s1[0] == a); + assert(s2[0] == b); + assert forall |i: int| 0 <= i < l1.len() implies l1[i] == l2[i] by { + assert(l1[i] == s1[i+1]); + assert(l2[i] == s2[i+1]); + } + seq_extensional_equality_index(*l1, *l2); + } + } + } + } +} + +proof fn lemma_seq_ext_equal(s1: Seq, s2: Seq) + ensures + #[trigger] (s1 =~= s2) <==> { + &&& s1.len() == s2.len() + &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i] + }, +{ + if s1.len() =~= s2.len() + && forall|i: int| 0 <= i < s1.len() ==> s1[i] == s2[i] { + seq_extensional_equality_index(s1, s2); + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_ext_equal(s1: Seq, s2: Seq) @@ -298,6 +546,19 @@ pub proof fn axiom_seq_ext_equal(s1: Seq, s2: Seq) { } +proof fn lemma_seq_ext_equal_deep(s1: Seq, s2: Seq) + ensures + #[trigger] (s1 =~~= s2) <==> { + &&& s1.len() == s2.len() + &&& forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i] + }, +{ + if s1.len() =~~= s2.len() + && forall|i: int| 0 <= i < s1.len() ==> s1[i] =~~= s2[i] { + seq_extensional_equality_index(s1, s2); + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_ext_equal_deep(s1: Seq, s2: Seq) @@ -309,6 +570,14 @@ pub proof fn axiom_seq_ext_equal_deep(s1: Seq, s2: Seq) { } +proof fn lemma_seq_subrange_len(s: Seq, j: int, k: int) + requires + 0 <= j <= k <= s.len(), + ensures + #[trigger] s.subrange(j, k).len() == k - j, +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_subrange_len(s: Seq, j: int, k: int) @@ -319,6 +588,15 @@ pub proof fn axiom_seq_subrange_len(s: Seq, j: int, k: int) { } +proof fn lemma_seq_subrange_index(s: Seq, j: int, k: int, i: int) + requires + 0 <= j <= k <= s.len(), + 0 <= i < k - j, + ensures + s.subrange(j, k)[i] == s[i + j], +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_subrange_index(s: Seq, j: int, k: int, i: int) @@ -330,6 +608,11 @@ pub proof fn axiom_seq_subrange_index(s: Seq, j: int, k: int, i: int) { } +proof fn lemma_seq_add_len(s1: Seq, s2: Seq) + ensures #[trigger] s1.add(s2).len() == s1.len() + s2.len() +{ +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_add_len(s1: Seq, s2: Seq) @@ -337,6 +620,19 @@ pub proof fn axiom_seq_add_len(s1: Seq, s2: Seq) { } +proof fn lemma_seq_add_index1(s1: Seq, s2: Seq, i: int) + // 0 <= i not required + requires + i < s1.len(), + ensures + s1.add(s2)[i] == s1[i], +{ + if !(0 <= i) { + seq_index_out_of_bounds(s1.add(s2), i); + seq_index_out_of_bounds(s1, i); + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_add_index1(s1: Seq, s2: Seq, i: int) @@ -347,6 +643,20 @@ pub proof fn axiom_seq_add_index1(s1: Seq, s2: Seq, i: int) { } +proof fn lemma_seq_add_index2(s1: Seq, s2: Seq, i: int) + requires + 0 <= s1.len(), + // precondition not required + // i < s1.len() as int + s2.len(), + ensures + s1.add(s2)[i] == s2[i - s1.len()], +{ + if !(i < s1.len() as int + s2.len()) { + seq_index_out_of_bounds(s1.add(s2), i); + seq_index_out_of_bounds(s2, i - s1.len()); + } +} + #[verifier(external_body)] #[verifier(broadcast_forall)] pub proof fn axiom_seq_add_index2(s1: Seq, s2: Seq, i: int)