Soundness issue in sequence axioms (axiom_seq_add_index2)

[tchajed]

The axiom axiom_seq_add_index2 is unsound:

verus/source/pervasive/seq.rs

Lines 352 to 357 in 214c3d8

	pub proof fn axiom_seq_add_index2<A>(s1: Seq<A>, s2: Seq<A>, i: int)
	requires
	0 <= s1.len(),
	i < s1.len() as int + s2.len(),
	ensures
	s1.add(s2)[i] == s2[i - s1.len()],

Here's a proof of false:

use vstd::prelude::*;

verus! {
    proof fn seq_bad()
        ensures false
    {
        let s1: Seq<int> = seq![1];
        let s1_2: Seq<int> = seq![1, 2];
        let s2: Seq<int> = seq![];
        assert(s1.add(s2)[0] == s2[-1]);
        assert(s1_2.add(s2)[1] == s2[-1]);
    }

    fn main() {}
}

The lemma becomes true if the precondition is changed to 0 <= s1.len() <= i.

[Chris-Hawblitzel]

Oops. That's a good motivation for #988 .

[Chris-Hawblitzel]

Fixed by bf057b6