Unsoundness with Datatype Axioms

[yizhou7]

I think I found an unsoundness issue using empty structs. I have reduced the example to the following:

use vstd::prelude::*;

verus! {
    pub struct Empty {}

    spec fn foo() -> Option<(Empty, Empty)> {
        Some((Empty {}, Empty {}))
    }
} // verus!

fn main() {
}

Since it doesn't really prove anything, the SMT file contains axioms only, which is not expected to create any conflicts.
I initially fond a conflict using vampire (version 4.8):

2. ! [X1 : 'Height()',X0 : 'Height()'] : (height_lt(X0,X1) <=> ('partial-order'(X0,X1) & ~X0 = X1)) [input]
3. ! [X0 : 'Dcr()',X1 : 'Type()'] : has_type('Poly%core!option.Option.'('core!option.Option./None'),'TYPE%core!option.Option.'(X0,X1)) [input]
4. ! [X0 : 'Dcr()',X2 : 'Poly()',X1 : 'Type()'] : (has_type(X2,'TYPE%core!option.Option.'(X0,X1)) => has_type('core!option.Option./Some/0'('%Poly%core!option.Option.'(X2)),X1)) [input]
5. ! [X0 : 'Poly()'] : (has_type(X0,'TYPE%sample!Empty.') => 'Poly%sample!Empty.'('%Poly%sample!Empty.'(X0)) = X0) [input]
7. ! [X0 : 'Dcr()',X1 : 'Type()',X3 : 'Type()',X2 : 'Dcr()',X4 : 'Poly()'] : (has_type(X4,'TYPE%tuple%2.'(X0,X1,X2,X3)) => 'Poly%tuple%2.'('%Poly%tuple%2.'(X4)) = X4) [input]
8. ! [X0 : 'Dcr()',X1 : 'Type()',X3 : 'Type()',X2 : 'Dcr()',X4 : 'Poly()'] : (has_type(X4,'TYPE%tuple%2.'(X0,X1,X2,X3)) => has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'(X4)),X1)) [input]
9. ! [X0 : 'tuple%2.()'] : ('$istuple%2./tuple%20'(X0) => height_lt(height('tuple%2./tuple%2/0'(X0)),height('Poly%tuple%2.'(X0)))) [input]
13. 'tuple%2./tuple%2'('tuple%2./tuple%2/?0'(X0),'tuple%2./tuple%2/?1'(X0)) = X0 [term algebras exhaustiveness]
16. '$istuple%2./tuple%20'('tuple%2./tuple%2'(X0,X1)) [term algebras discriminators]
17. 'sample!Empty./Empty' = X0 [term algebras exhaustiveness]
18. ! [X0 : 'Dcr()',X1 : 'Type()',X2 : 'Type()',X3 : 'Dcr()',X4 : 'Poly()'] : (has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2)) => has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'(X4)),X1)) [rectify 8]
19. ! [X0 : 'Dcr()',X1 : 'Type()',X2 : 'Type()',X3 : 'Dcr()',X4 : 'Poly()'] : (has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2)) => 'Poly%tuple%2.'('%Poly%tuple%2.'(X4)) = X4) [rectify 7]
20. ! [X0 : 'Dcr()',X1 : 'Poly()',X2 : 'Type()'] : (has_type(X1,'TYPE%core!option.Option.'(X0,X2)) => has_type('core!option.Option./Some/0'('%Poly%core!option.Option.'(X1)),X2)) [rectify 4]
21. ! [X0 : 'Height()',X1 : 'Height()'] : (height_lt(X1,X0) <=> ('partial-order'(X1,X0) & ~X0 = X1)) [rectify 2]
22. ! [X0 : 'Height()',X1 : 'Height()'] : (height_lt(X1,X0) <=> ('partial-order'(X1,X0) & X0 != X1)) [flattening 21]
23. ! [X0 : 'Height()',X1 : 'Height()'] : (height_lt(X1,X0) => ('partial-order'(X1,X0) & X0 != X1)) [unused predicate definition removal 22]
24. ! [X0 : 'Height()',X1 : 'Height()'] : (height_lt(X1,X0) => X0 != X1) [pure predicate removal 23]
25. ! [X0 : 'tuple%2.()'] : (height_lt(height('tuple%2./tuple%2/0'(X0)),height('Poly%tuple%2.'(X0))) | ~'$istuple%2./tuple%20'(X0)) [ennf transformation 9]
26. ! [X0 : 'Dcr()',X1 : 'Type()',X2 : 'Type()',X3 : 'Dcr()',X4 : 'Poly()'] : (has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'(X4)),X1) | ~has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2))) [ennf transformation 18]
27. ! [X0 : 'Dcr()',X1 : 'Type()',X2 : 'Type()',X3 : 'Dcr()',X4 : 'Poly()'] : ('Poly%tuple%2.'('%Poly%tuple%2.'(X4)) = X4 | ~has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2))) [ennf transformation 19]
28. ! [X0 : 'Poly()'] : ('Poly%sample!Empty.'('%Poly%sample!Empty.'(X0)) = X0 | ~has_type(X0,'TYPE%sample!Empty.')) [ennf transformation 5]
29. ! [X0 : 'Dcr()',X1 : 'Poly()',X2 : 'Type()'] : (has_type('core!option.Option./Some/0'('%Poly%core!option.Option.'(X1)),X2) | ~has_type(X1,'TYPE%core!option.Option.'(X0,X2))) [ennf transformation 20]
30. ! [X0 : 'Height()',X1 : 'Height()'] : (X0 != X1 | ~height_lt(X1,X0)) [ennf transformation 24]
32. height_lt(height('tuple%2./tuple%2/0'(X0)),height('Poly%tuple%2.'(X0))) | ~'$istuple%2./tuple%20'(X0) [cnf transformation 25]
33. ~has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2)) | has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'(X4)),X1) [cnf transformation 26]
34. ~has_type(X4,'TYPE%tuple%2.'(X0,X1,X3,X2)) | 'Poly%tuple%2.'('%Poly%tuple%2.'(X4)) = X4 [cnf transformation 27]
36. 'Poly%sample!Empty.'('%Poly%sample!Empty.'(X0)) = X0 | ~has_type(X0,'TYPE%sample!Empty.') [cnf transformation 28]
37. ~has_type(X1,'TYPE%core!option.Option.'(X0,X2)) | has_type('core!option.Option./Some/0'('%Poly%core!option.Option.'(X1)),X2) [cnf transformation 29]
38. has_type('Poly%core!option.Option.'('core!option.Option./None'),'TYPE%core!option.Option.'(X0,X1)) [cnf transformation 3]
39. X0 != X1 | ~height_lt(X1,X0) [cnf transformation 30]
42. ~height_lt(X1,X1) [equality resolution 39]
43. ~has_type(X0,'TYPE%sample!Empty.') | 'Poly%sample!Empty.'('sample!Empty./Empty') = X0 [forward demodulation 36,17]
48. '$istuple%2./tuple%20'(X0) [superposition 16,13]
71. has_type('core!option.Option./Some/0'('%Poly%core!option.Option.'('Poly%core!option.Option.'('core!option.Option./None'))),X3) [resolution 37,38]
91. 'Poly%sample!Empty.'('sample!Empty./Empty') = 'core!option.Option./Some/0'('%Poly%core!option.Option.'('Poly%core!option.Option.'('core!option.Option./None'))) [resolution 71,43]
94. has_type('Poly%sample!Empty.'('sample!Empty./Empty'),X3) [backward demodulation 71,91]
110. has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty'))),X5) [resolution 33,94]
120. 'Poly%sample!Empty.'('sample!Empty./Empty') = 'Poly%tuple%2.'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty'))) [resolution 34,94]
145. 'Poly%sample!Empty.'('sample!Empty./Empty') = 'tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty'))) [resolution 110,43]
245. height_lt(height('tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty')))),height('Poly%sample!Empty.'('sample!Empty./Empty'))) | ~'$istuple%2./tuple%20'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty'))) [superposition 32,120]
246. height_lt(height('tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty')))),height('Poly%sample!Empty.'('sample!Empty./Empty'))) [subsumption resolution 245,48]
247. height_lt(height('Poly%sample!Empty.'('sample!Empty./Empty')),height('Poly%sample!Empty.'('sample!Empty./Empty'))) [forward demodulation 246,145]
248. $false [subsumption resolution 247,42]

Then I manually reduced the SMT file (by removing certain axioms and all the options),
I was able to get Z3 (version 4.13.0) to reach unsat as well.

(declare-sort Poly 0)
(declare-sort Height 0)
(declare-fun I (Int) Poly)
(declare-sort Type 0)
(declare-const BOOL Type)
(declare-sort Dcr 0)
(declare-const $ Dcr)
(declare-fun has_type (Poly Type) Bool)
(declare-fun as_type (Poly Type) Poly)
(assert (forall ((x Poly) (t Type)) (! (and (has_type (as_type x t) t) (=> (has_type x t) (= x (as_type x t)))) :pattern ((as_type x t)) :qid prelude_as_type :skolemid skolem_prelude_as_type)))
(declare-fun height (Poly) Height)
(declare-fun height_lt (Height Height) Bool)
(declare-fun partial-order (Height Height) Bool)
; (assert (forall ((x Height) (y Height)) (! (= (height_lt x y) (and (partial-order x y) (not (= x y)))) :pattern ((height_lt x y)) :qid prelude_height_lt :skolemid skolem_prelude_height_lt)))
(assert (forall ((x Height) (y Height)) (! (= (height_lt x y) (and ((_ partial-order 0) x y) (not (= x y)))) :pattern ((height_lt x y)) :qid prelude_height_lt :skolemid skolem_prelude_height_lt)))
(declare-datatypes (
    (core!option.Option. 0) (sample!Empty. 0) (tuple%2. 0))
    (
        ((core!option.Option./None ) (core!option.Option./Some (core!option.Option./Some/?0 Poly)))
        ((sample!Empty./Empty ))
        ((tuple%2./tuple%2 (tuple%2./tuple%2/?0 Poly) (tuple%2./tuple%2/?1 Poly)))
    )
)
(declare-fun core!option.Option./Some/0 (core!option.Option.) Poly)
(declare-fun tuple%2./tuple%2/0 (tuple%2.) Poly)
(declare-fun tuple%2./tuple%2/1 (tuple%2.) Poly)
(declare-fun TYPE%core!option.Option. (Dcr Type) Type)
(declare-const TYPE%sample!Empty. Type)
(declare-fun TYPE%tuple%2. (Dcr Type Dcr Type) Type)
(declare-fun Poly%core!option.Option. (core!option.Option.) Poly)
(declare-fun %Poly%core!option.Option. (Poly) core!option.Option.)
(declare-fun Poly%sample!Empty. (sample!Empty.) Poly)
(declare-fun %Poly%sample!Empty. (Poly) sample!Empty.)
(declare-fun Poly%tuple%2. (tuple%2.) Poly)
(declare-fun %Poly%tuple%2. (Poly) tuple%2.)
(assert (forall ((V&. Dcr) (V& Type)) (! (has_type (Poly%core!option.Option. core!option.Option./None) (TYPE%core!option.Option. V&. V&)) :pattern ((has_type (Poly%core!option.Option. core!option.Option./None) (TYPE%core!option.Option. V&. V&))) :qid internal_core!option.Option./None_constructor_definition :skolemid skolem_internal_core!option.Option./None_constructor_definition)))
(assert (forall ((V&. Dcr) (V& Type) (x Poly)) (! (=> (has_type x (TYPE%core!option.Option. V&. V&)) (has_type (core!option.Option./Some/0 (%Poly%core!option.Option. x)) V&)) :pattern ((core!option.Option./Some/0 (%Poly%core!option.Option. x)) (has_type x (TYPE%core!option.Option. V&. V&))) :qid internal_core!option.Option./Some/0_invariant_definition :skolemid skolem_internal_core!option.Option./Some/0_invariant_definition)))
(assert (forall ((x Poly)) (! (=> (has_type x TYPE%sample!Empty.) (= x (Poly%sample!Empty. (%Poly%sample!Empty. x)))) :pattern ((has_type x TYPE%sample!Empty.)) :qid internal_sample__Empty_unbox_axiom_definition :skolemid skolem_internal_sample__Empty_unbox_axiom_definition)))
(assert (forall ((x tuple%2.)) (! (= x (%Poly%tuple%2. (Poly%tuple%2. x))) :pattern ((Poly%tuple%2. x)) :qid internal_crate__tuple__2_box_axiom_definition :skolemid skolem_internal_crate__tuple__2_box_axiom_definition)))
(assert (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (! (=> (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&)) (= x (Poly%tuple%2. (%Poly%tuple%2. x)))) :pattern ((has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))) :qid internal_crate__tuple__2_unbox_axiom_definition :skolemid skolem_internal_crate__tuple__2_unbox_axiom_definition)))
(assert (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (! (=> (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&)) (has_type (tuple%2./tuple%2/0 (%Poly%tuple%2. x)) T%0&)) :pattern ((tuple%2./tuple%2/0 (%Poly%tuple%2. x)) (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))) :qid internal_tuple__2./tuple__2/0_invariant_definition :skolemid skolem_internal_tuple__2./tuple__2/0_invariant_definition)))
(assert (forall ((x tuple%2.)) (! (=> ((_ is tuple%2./tuple%2) x) (height_lt (height (tuple%2./tuple%2/0 x)) (height (Poly%tuple%2. x)))) :pattern ((height (tuple%2./tuple%2/0 x))) :qid prelude_datatype_height_tuple%2./tuple%2/0 :skolemid skolem_prelude_datatype_height_tuple%2./tuple%2/0)))
(check-sat)

However, it is worth noting that Z3 does not reach unsat under the default options Verus uses, which means that the unsoundess is not easily reachable using pattern-based QI only.

2024-12-18-11-49-35.zip

[tjhance]

I'm guessing this has to do with the way Height interacts with Poly. We have an axiom that says height(a) < height((a, b)) but this isn't guarded by any HasTypes. So, using a tuple that is equal to its own 'fst' element, we can get a contradiction. (edit: I'm not really sure if this is right, I don't see why the existence of such a tuple would be implied by the given axioms)

[yizhou7]

I think you might be onto something, one of the intermediary steps in Vampire is

'Poly%sample!Empty.'('sample!Empty./Empty') = 
'tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty')))

If we consider the sub-terms an their SMT Sorts:

	Term	Sort
t0	sample!Empty./Empty	sample!Empty.
t1	(Poly%sample!Empty t0)	Poly
t2	(%Poly%tuple%2. t1)	tuple%2.
t3	(tuple%2./tuple%2/0 t2)	Poly

So Vampire is somehow able to derive t1 = t3, and then create a conflict using that.

[tjhance]

It seems that one follows from:

110. has_type('tuple%2./tuple%2/0'('%Poly%tuple%2.'('Poly%sample!Empty.'('sample!Empty./Empty'))),X5) [resolution 33,94]

this is clearly nonsense, it's taking an 'Empty', making it into Poly, and then un-polying it but reinterpreting that as a Tuple. However I can't quite make sense of how 110 comes about.

[tjhance]

I think it might come down to this axiom:

(assert (forall ((V&. Dcr) (V& Type) (x Poly)) (!
  (=>
    (has_type x (TYPE%core!option.Option. V&. V&))
    (has_type (core!option.Option./Some/0 (%Poly%core!option.Option. x)) V&))

This axiom should have a hypothesis that (%Poly%core!option.Option. x) is in the Some state (edit: nevermind)

[tjhance]

Note that in line 91 from the proof trace:

91. 'Poly%sample!Empty.'('sample!Empty./Empty') = 'core!option.Option./Some/0'('%Poly%core!option.Option.'('Poly%core!option.Option.'('core!option.Option./None')))

It's calling 'Some/0' on a 'None' value.

[tjhance]

Yeah something is borked about the way we handle None here. The encoding has 1 Option datatype to cover every type, so only one 'None' value. Thus 'Poly(None)' needs to have every type (forall t, has_type(Poly(None), t)).

But we also have a function get_Some_0<A> : forall A. Option<A> -> A. Which again, in this encoding, is the same for every type ...

I think the fundamental problem is that these SMT datatype constructors don't have type parameters.

[yizhou7]

Very interesting. Technically, SMT datatypes can be polymorphic with respect to Sort. I wonder if anyone has looked into using a more native encoding of polymorphism using polymorphic datatypes? Of course that would require a pretty major overhaul of the box/unbox type system.

On the other hand, I wonder what is the current benefit of using solver's builtin theory for datatypes? I have been diagnosing various performance issues, and the theory instantiations (datatypes, ariths) have been difficult to deal with.

[tjhance]

The encoding of datatypes was recently changed to use SMT-native types. However, I think the soundness issue was probably present in the original encoding as well. Unfortunately, it probably would have much easier to fix the issue using the old encoding ...

I don't know if SMT-sort polymorphism would help here. That wouldn't help with the way we do polymorphism via our Poly/Type/has_type system.

[tjhance]

I think the following would work:

• replace the "field-getters" like core!option.Option./Some/0 with uninterpreted functions that take the necessary type arguments.
• add axioms that these uninterpreted functions agree with the field-getters, but only on the correct variants.

[utaal]

Just a quick note that this is in flight, and may interact with fixes to this issue: #1359

[Chris-Hawblitzel]

@yizhou7 Thanks for finding this and generating a minimized example! I've been on vacation, so it took me a while to take a look at this. I just went through a quick attempt to prove all the axioms in the SMT file you posted. Indeed, one of the axioms is missing a precondition. Specifically, for the following:

// (axiom (forall ((V&. Dcr) (V& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%core!option.Option. V&. V&))
//     (has_type (core!option.Option./Some/0 (%Poly%core!option.Option. x)) V&)
//    )
//    :qid internal_core!option.Option./Some/0_invariant_definition
// )))
proof fn some_invariant_definition_good(v: Type, x: Poly)
    requires
        unbox_opt(x) is Some,
        has_type(x, Type::Opt(Box::new(v))),
    ensures
        has_type((unbox_opt(x))->0, v),
{
}

the unbox_opt(x) is Some precondition is missing from the axiom. With this precondition, I can prove the axiom from more fundamental definitions. Without this precondition, the axiom is simply false.

Below are some definitions and proofs to justify the corrected axiom, along with the other axioms, and to demonstrate that the uncorrected axiom is false. (Of course, we might want to check these in an independent tool, like F* or Dafny or Coq.)

enum Type {
    Empty,
    Tuple(Box<Type>, Box<Type>),
    Opt(Box<Type>),
}

enum Poly {
    Empty,
    Tuple(Box<Poly>, Box<Poly>),
    None,
    Some(Box<Poly>),
}

struct Empty;
struct Tuple(Poly, Poly);
enum Opt { None, Some(Poly) }

spec fn has_type(p: Poly, t: Type) -> bool
    decreases p
{
    match (p, t) {
        (Poly::Empty, Type::Empty) => true,
        (Poly::Tuple(p0, p1), Type::Tuple(t0, t1)) => has_type(*p0, *t0) && has_type(*p1, *t1),
        (Poly::None, Type::Opt(_)) => true,
        (Poly::Some(p0), Type::Opt(t0)) => has_type(*p0, *t0),
        _ => false,
    }
}

spec fn height(p: Poly) -> nat
    decreases p
{
    match p {
        Poly::Empty => 0,
        Poly::Tuple(p0, p1) => 1 + height(*p0) + height(*p1),
        Poly::None => 0,
        Poly::Some(p0) => 1 + height(*p0),
    }
}

spec fn height_lt(x: nat, y: nat) -> bool {
    x < y
}

spec fn box_empty(e: Empty) -> Poly {
    Poly::Empty
}

spec fn box_tuple(e: Tuple) -> Poly {
    Poly::Tuple(Box::new(e.0), Box::new(e.1))
}

spec fn box_opt(e: Opt) -> Poly {
    match e {
        Opt::None => Poly::None,
        Opt::Some(p) => Poly::Some(Box::new(p)),
    }
}

spec fn unbox_empty(p: Poly) -> Empty {
    Empty
}

spec fn unbox_tuple(p: Poly) -> Tuple {
    match p {
        Poly::Tuple(p0, p1) => Tuple(*p0, *p1),
        _ => Tuple(Poly::Empty, Poly::Empty) // dummy value
    }
}

spec fn unbox_opt(p: Poly) -> Opt {
    match p {
        Poly::None => Opt::None,
        Poly::Some(p0) => Opt::Some(*p0),
        _ => Opt::None, // dummy value
    }
}

// (axiom (forall ((x tuple%2.)) (!
//    (=>
//     (is-tuple%2./tuple%2 x)
//     (height_lt (height (tuple%2./tuple%2/0 x)) (height (Poly%tuple%2. x)))
//    )
//    :qid prelude_datatype_height_tuple%2./tuple%2/0
// )))
proof fn prelude_datatype_height_tuple(x: Tuple)
    ensures
        height_lt(height(x.0), height(box_tuple(x))),
{
    reveal_with_fuel(height, 2);
}

// (axiom (forall ((V&. Dcr) (V& Type)) (!
//    (has_type (Poly%core!option.Option. (core!option.Option./None)) (TYPE%core!option.Option.
//      V&. V&
//    ))
//    :qid internal_core!option.Option./None_constructor_definition
// )))
proof fn none_constructor_definition(v: Type)
    ensures
        has_type(box_opt(Opt::None), Type::Opt(Box::new(v))),
{
}

// (axiom (forall ((V&. Dcr) (V& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%core!option.Option. V&. V&))
//     (has_type (core!option.Option./Some/0 (%Poly%core!option.Option. x)) V&)
//    )
//    :qid internal_core!option.Option./Some/0_invariant_definition
// )))
proof fn some_invariant_definition_bad(v: Type, x: Poly)
    requires
        has_type(x, Type::Opt(Box::new(v))),
    ensures
        has_type((unbox_opt(x))->0, v),
{
    assume(false);
}
proof fn some_invariant_definition_good(v: Type, x: Poly)
    requires
        unbox_opt(x) is Some,
        has_type(x, Type::Opt(Box::new(v))),
    ensures
        has_type((unbox_opt(x))->0, v),
{
}

// (axiom (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))
//     (= x (Poly%tuple%2. (%Poly%tuple%2. x)))
//    )
//    :qid internal_crate__tuple__2_unbox_axiom_definition
// )))
proof fn tuple_unbox_axiom_definition(t0: Type, t1: Type, x: Poly)
    requires
        has_type(x, Type::Tuple(Box::new(t0), Box::new(t1))),
    ensures
        x == box_tuple(unbox_tuple(x)),
{
}

// (axiom (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))
//     (has_type (tuple%2./tuple%2/0 (%Poly%tuple%2. x)) T%0&)
//    )
//    :qid internal_tuple__2./tuple__2/0_invariant_definition
// )))
proof fn tuple_invariant_definition(t0: Type, t1: Type, x: Poly)
    requires
        has_type(x, Type::Tuple(Box::new(t0), Box::new(t1))),
    ensures
        has_type(unbox_tuple(x).0, t0),
{
}

// (assert (forall ((x Poly)) (!
//    (=>
//     (has_type x TYPE%sample!Empty.)
//     (= x (Poly%sample!Empty. (%Poly%sample!Empty. x)))
//    )
//    :qid internal_sample__Empty_unbox_axiom_definition
// )))
proof fn empty_unbox_axiom_definition(x: Poly)
    requires
        has_type(x, Type::Empty),
    ensures
        x == box_empty(unbox_empty(x)),
{
}

proof fn demonstrate_some_invariant_definition_bad()
    ensures
        false,
{
    some_invariant_definition_bad(Type::Empty, Poly::None);
    some_invariant_definition_bad(Type::Tuple(Box::new(Type::Empty), Box::new(Type::Empty)), Poly::None);
}

[tjhance]

I came to a similar conclusion earlier, but then I wasn't so sure.

If we add the hypothesis "unbox_opt(x) is Some" to this axiom, won't it violate Verus's maxim that all functions be total?

i.e., this would no longer be total:

fn unwrap(x: Option<T>) -> T { x-> 0 }

This is why I suggested the other change about the type parameters. (Though I haven't formally validated that it's correct.)

[Chris-Hawblitzel]

@tjhance Ah, I see what you mean. My quick attempt above was too quick and wouldn't cover the unwrap function well enough. I should have used something closer to the OOPSLA paper definitions. That has a defaults_to definition that can make the total version of ->0 explicit. Here's a revised version with the explicit ->0 definition, as you suggest, and the proof that the original axiom works with this without the added precondition. I also proved the unwrap axioms.

// struct Empty {}
// struct Tuple<A.B>(A, B);
// enum Option<A> { None, Some(A) }

enum Type {
    Empty,
    Tuple(Box<Type>, Box<Type>),
    Opt(Box<Type>),
}

enum Poly {
    Empty,
    Tuple(Box<Poly>, Box<Poly>),
    None,
    Some(Box<Poly>),
}

struct Empty;
struct Tuple(Poly, Poly);
enum Opt { None, Some(Poly) }

spec fn default(t: Type) -> Poly
    decreases t
{
    match t {
        Type::Empty => Poly::Empty,
        Type::Tuple(t0, t1) => Poly::Tuple(Box::new(default(*t0)), Box::new(default(*t1))),
        Type::Opt(t0) => Poly::None,
    }
}

spec fn get0(t: Type, o: Opt) -> Poly {
    match o {
        Opt::None => default(t),
        Opt::Some(s) => s,
    }
}

spec fn has_type(p: Poly, t: Type) -> bool
    decreases p
{
    match (p, t) {
        (Poly::Empty, Type::Empty) => true,
        (Poly::Tuple(p0, p1), Type::Tuple(t0, t1)) => has_type(*p0, *t0) && has_type(*p1, *t1),
        (Poly::None, Type::Opt(_)) => true,
        (Poly::Some(p0), Type::Opt(t0)) => has_type(*p0, *t0),
        _ => false,
    }
}

spec fn height(p: Poly) -> nat
    decreases p
{
    match p {
        Poly::Empty => 0,
        Poly::Tuple(p0, p1) => 1 + height(*p0) + height(*p1),
        Poly::None => 0,
        Poly::Some(p0) => 1 + height(*p0),
    }
}

spec fn height_lt(x: nat, y: nat) -> bool {
    x < y
}

spec fn box_empty(e: Empty) -> Poly {
    Poly::Empty
}

spec fn box_tuple(e: Tuple) -> Poly {
    Poly::Tuple(Box::new(e.0), Box::new(e.1))
}

spec fn box_opt(e: Opt) -> Poly {
    match e {
        Opt::None => Poly::None,
        Opt::Some(p) => Poly::Some(Box::new(p)),
    }
}

spec fn unbox_empty(p: Poly) -> Empty {
    Empty
}

spec fn unbox_tuple(p: Poly) -> Tuple {
    match p {
        Poly::Tuple(p0, p1) => Tuple(*p0, *p1),
        _ => Tuple(Poly::Empty, Poly::Empty) // dummy value
    }
}

spec fn unbox_opt(p: Poly) -> Opt {
    match p {
        Poly::None => Opt::None,
        Poly::Some(p0) => Opt::Some(*p0),
        _ => Opt::None, // dummy value
    }
}

proof fn default_has_type(t: Type)
    ensures
        has_type(default(t), t),
    decreases t
{
    match t {
        Type::Empty => {}
        Type::Tuple(t0, t1) => {
            default_has_type(*t0);
            default_has_type(*t1);
        }
        Type::Opt(t0) =>  {
            default_has_type(*t0);
        }
    }
}

// (axiom (forall ((x tuple%2.)) (!
//    (=>
//     (is-tuple%2./tuple%2 x)
//     (height_lt (height (tuple%2./tuple%2/0 x)) (height (Poly%tuple%2. x)))
//    )
//    :qid prelude_datatype_height_tuple%2./tuple%2/0
// )))
proof fn prelude_datatype_height_tuple(x: Tuple)
    ensures
        height_lt(height(x.0), height(box_tuple(x))),
{
    reveal_with_fuel(height, 2);
}

// (axiom (forall ((V&. Dcr) (V& Type)) (!
//    (has_type (Poly%core!option.Option. (core!option.Option./None)) (TYPE%core!option.Option.
//      V&. V&
//    ))
//    :qid internal_core!option.Option./None_constructor_definition
// )))
proof fn none_constructor_definition(v: Type)
    ensures
        has_type(box_opt(Opt::None), Type::Opt(Box::new(v))),
{
}

// (axiom (forall ((V&. Dcr) (V& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%core!option.Option. V&. V&))
//     (has_type (core!option.Option./Some/0 (%Poly%core!option.Option. x)) V&)
//    )
//    :qid internal_core!option.Option./Some/0_invariant_definition
// )))
proof fn some_invariant_definition_not_so_bad(v: Type, x: Poly)
    requires
        has_type(x, Type::Opt(Box::new(v))),
    ensures
        has_type(get0(v, unbox_opt(x)), v),
{
    default_has_type(v);
}
proof fn some_invariant_definition_good(v: Type, x: Poly)
    requires
        unbox_opt(x) is Some,
        has_type(x, Type::Opt(Box::new(v))),
    ensures
        has_type(get0(v, unbox_opt(x)), v),
{
}

// (axiom (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))
//     (= x (Poly%tuple%2. (%Poly%tuple%2. x)))
//    )
//    :qid internal_crate__tuple__2_unbox_axiom_definition
// )))
proof fn tuple_unbox_axiom_definition(t0: Type, t1: Type, x: Poly)
    requires
        has_type(x, Type::Tuple(Box::new(t0), Box::new(t1))),
    ensures
        x == box_tuple(unbox_tuple(x)),
{
}

// (axiom (forall ((T%0&. Dcr) (T%0& Type) (T%1&. Dcr) (T%1& Type) (x Poly)) (!
//    (=>
//     (has_type x (TYPE%tuple%2. T%0&. T%0& T%1&. T%1&))
//     (has_type (tuple%2./tuple%2/0 (%Poly%tuple%2. x)) T%0&)
//    )
//    :qid internal_tuple__2./tuple__2/0_invariant_definition
// )))
proof fn tuple_invariant_definition(t0: Type, t1: Type, x: Poly)
    requires
        has_type(x, Type::Tuple(Box::new(t0), Box::new(t1))),
    ensures
        has_type(unbox_tuple(x).0, t0),
{
}

// (assert (forall ((x Poly)) (!
//    (=>
//     (has_type x TYPE%sample!Empty.)
//     (= x (Poly%sample!Empty. (%Poly%sample!Empty. x)))
//    )
//    :qid internal_sample__Empty_unbox_axiom_definition
// )))
proof fn empty_unbox_axiom_definition(x: Poly)
    requires
        has_type(x, Type::Empty),
    ensures
        x == box_empty(unbox_empty(x)),
{
}

proof fn demonstrate_some_invariant_definition_not_so_bad()
//    ensures
//        false,
{
    some_invariant_definition_not_so_bad(Type::Empty, Poly::None);
    some_invariant_definition_not_so_bad(Type::Tuple(Box::new(Type::Empty), Box::new(Type::Empty)), Poly::None);
}

// (declare-fun get.? (Dcr Type Poly) Poly)
spec fn unwrap(t: Type, p: Poly) -> Poly {
    get0(t, unbox_opt(p))
}

// (assert
//   (forall ((A&. Dcr) (A& Type) (o! Poly)) (!
//     (= (unwrap.? A&. A& o!) (core!option.Option./Some/0 (%Poly%core!option.Option.
//        o!
//     )))
//     :pattern ((unwrap.? A&. A& o!))
//     :qid internal!unwrap.?_definition
//     :skolemid skolem_internal!unwrap.?_definition
// )))
proof fn unwrap_definition(a: Type, o: Poly)
    ensures
        unwrap(a, o) == get0(a, unbox_opt(o))
{
}

// (assert (forall ((A&. Dcr) (A& Type) (o! Poly)) (!
//    (=>
//     (has_type o! (TYPE%core!option.Option. A&. A&))
//     (has_type (unwrap.? A&. A& o!) A&)
//    )
//    :pattern ((unwrap.? A&. A& o!))
//    :qid internal!unwrap.?_pre_post_definition
//    :skolemid skolem_internal!unwrap.?_pre_post_definition
// )))
proof fn unwrap_pre_post_definition(a: Type, o: Poly)
    requires
        has_type(o, Type::Opt(Box::new(a))),
    ensures
        has_type(unwrap(a, o), a),
{
    default_has_type(a);
}

proof fn demonstrate_get_pre_post_definition_not_so_bad()
//    ensures
//        false,
{
    unwrap_pre_post_definition(Type::Empty, Poly::None);
    unwrap_pre_post_definition(Type::Tuple(Box::new(Type::Empty), Box::new(Type::Empty)), Poly::None);
}

[Chris-Hawblitzel]

I think the following would work:

• replace the "field-getters" like core!option.Option./Some/0 with uninterpreted functions that take the necessary type arguments.
• add axioms that these uninterpreted functions agree with the field-getters, but only on the correct variants.

One thing that may help with this is that, to avoid matching loops, field getters are already uninterpreted functions that wrap the raw SMT datatype getters:

(declare-datatypes ((core!option.Option. 0)) (((core!option.Option./None) (core!option.Option./Some
    (core!option.Option./Some/?0 Poly)
))))
(declare-fun core!option.Option./Some/0 (core!option.Option.) Poly)
(axiom (forall ((x core!option.Option.)) (!
   (= (core!option.Option./Some/0 x) (core!option.Option./Some/?0 x))
   :pattern ((core!option.Option./Some/0 x))
   :qid internal_core!option.Option./Some/0_accessor_definition
   :skolemid skolem_internal_core!option.Option./Some/0_accessor_definition
)))

So implementing this plan could be as simple as adding the type arguments to the existing field getter wrappers and updating the existing _accessor_definition axioms. As an optimization, only transparent datatypes with at least 2 variants need this change (non-transparent datatypes have no variants and no getters so there's nothing to change, and single-variant datatype getter wrappers wouldn't use the type arguments anyway).