Change Seq to an enum and verify its axioms

[tchajed]

Instead of making Seq an axiomatic type (with verifier::external_body), make it an enum that implements the usual inductive definition of a list:

pub enum Seq {
Nil,
Cons(A, Box<Seq>),
}

This PR verifies as lemmas everything that was previously an axiom about Seq. Due to current limitations of Verus, if these lemmas are annotated with verifier::broadcast_forall, they do not have the exact same behavior as the current axioms in that they must be reveal'd explicitly rather than being ambiently available, which would affect many downstream proofs. To maintain compatibility I've added the lemmas alongside the axioms, but the ultimate goal would be to remove this duplication.

Now that we have a model it's possible to remove some preconditions and show that this is sound (since the new lemmas are verified rather than assumed). I've done this where I saw opportunities, but didn't propagate the changes to the axioms for now.

This is an attempt to fix #986.

[tchajed]

My first attempt didn't work because as @tjhance points out the proofs are just using the broadcast_forall axioms. I've started to prove the axioms and found an unsoundness in axiom_seq_add_index2:

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() {}
}

[tchajed]

The issue is that this:

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()],

should have a precondition 0 <= s1.len() <= i.

[parno]

This is very cool! In theory, we could also use this to simplify the interpreter, which currently has a bunch of special logic for simulating sequences. It's missing that logic for maps and sets, since no one has asked for it yet, but that could be avoided as well. However, the interpreter's current policy is not to open closed function definitions, so that would be an issue here. Would it be worth considering using opaque instead of closed?

[Chris-Hawblitzel]

In theory, we could also use this to simplify the interpreter

I think the plan is to hide the entire datatype definition as a private field of a struct, so the functions would have to be marked closed (opaque open pub functions aren't allowed to access private fields). We don't have any equivalent of opaque datatypes or opaque public fields.

Also, right now the interpreter uses an "Optimized representation of intermediate sequence results": Seq(Vector<Exp>). We'd lose this if we interpreted the underlying model directly. I'm pretty nervous about making the model available directly, even if it's marked opaque. This depends on pruning to keep the model out of the client SMT context, whereas with closed we could erase the model entirely from the vstd library file and be sure it didn't show up in the SMT context.

[parno]

I'm pretty nervous about making the model available directly, even if it's marked opaque.

That's fair and a more compelling argument. I'm nervous about adding more complexity to the interpreter to add special cases for maps, sets, and other future axiomatized types, but at least that doesn't directly affect the SMT encoding.

[parno]

FWIW, it looks like Dafny is starting to take some similar steps (although via a more complicated mechanism).