Type safety violation and soundness bug with parameterized domain

[DebraChait]

The following domain definition is from the 2vyper project here. $Struct defines a domain giving a unique identifier to every element of a struct, and $StructOps defines a domain for struct operations, parameterized by the type of struct element you are getting or setting. (Struct is defined in this way to avoid axioms that need to quantify over types.)

domain $Struct { function $struct_loc($s: $Struct, $m: Int): Int }
domain $StructOps[$T] {
    function $struct_get($l: Int): $T
    function $struct_set($s: $Struct, $m: Int, $t: $T): $Struct
    axiom $get_set_0_ax {
        forall $s: $Struct, $m: Int, $t: $T ::
            { $struct_loc($struct_set($s, $m, $t), $m) }
                $struct_get($struct_loc($struct_set($s, $m, $t), $m)) == $t
    }
    axiom $get_set_1_ax {
        forall $s: $Struct, $m: Int, $n: Int, $t: $T ::
            { $struct_loc($struct_set($s, $n, $t), $m) }
                $m != $n ==> $struct_loc($s, $m) == $struct_loc($struct_set($s, $n, $t), $m)
    }
}

The following does not raise a type error, allowing us to set a Bool variable to an Int value. Furthermore, it exposes a soundness bug, since the assertion (y == true) || (y == false) passes, despite the actual value of y being 10.

method test_struct() {
    var s: $Struct 
    s := $struct_set(s,0,10)
    var y: Bool 
    y := $struct_get($struct_loc(s,0))
    assert (y == true) || (y == false)
}

It seems that the SMT solver assumes that the type checker is catching all type errors, and so relies on the original type of y as a Bool to vacuously verify assert (y == true) || (y == false). However, the type checker does not catch the type safety violation of setting y to 10, leading the solver to verify the false statement (y == true) || (y == false).

(Credit to my advisor Thomas Wies on realizing that the type safety violation can lead to a soundness bug!)

[marcoeilers]

Thanks for filing this issue! However, I don't think I agree that this qualifies as a type safety violation or a soundness issue; IMO it's simply the case that 2vyper's struct encoding has some potentially unexpected properties.

Viper monomorphizes generic domains. I.e., from Viper's point of view, the program you and 2vyper wrote is essentially equivalent to:

domain $Struct { function $struct_loc($s: $Struct, $m: Int): Int }
domain $StructOps_Int {
    function $struct_get_Int($l: Int): Int
    function $struct_set_Int($s: $Struct, $m: Int, $t: Int): $Struct
    axiom $get_set_0_ax_Int {
        forall $s: $Struct, $m: Int, $t: Int ::
            { $struct_loc($struct_set_Int($s, $m, $t), $m) }
                $struct_get_Int($struct_loc($struct_set_Int($s, $m, $t), $m)) == $t
    }
    axiom $get_set_1_ax_Int {
        forall $s: $Struct, $m: Int, $n: Int, $t: Int ::
            { $struct_loc($struct_set_Int($s, $n, $t), $m) }
                $m != $n ==> $struct_loc($s, $m) == $struct_loc($struct_set_Int($s, $n, $t), $m)
    }
}
domain $StructOps_Bool {
    function $struct_get_Bool($l: Int): Bool
    function $struct_set_Bool($s: $Struct, $m: Int, $t: Bool): $Struct
    axiom $get_set_0_ax_Bool {
        forall $s: $Struct, $m: Int, $t: Bool ::
            { $struct_loc($struct_set_Bool($s, $m, $t), $m) }
                $struct_get_Bool($struct_loc($struct_set_Bool($s, $m, $t), $m)) == $t
    }
    axiom $get_set_1_ax_Bool {
        forall $s: $Struct, $m: Int, $n: Int, $t: Bool ::
            { $struct_loc($struct_set_Bool($s, $n, $t), $m) }
                $m != $n ==> $struct_loc($s, $m) == $struct_loc($struct_set_Bool($s, $n, $t), $m)
    }
}

method test_struct() {
    var s: $Struct 
    s := $struct_set_Int(s,0,10)
    var y: Bool 
    y := $struct_get_Bool($struct_loc(s,0))  // the type of y forces the use of $struct_get_Bool over $struct_get_Int
    assert (y == true) || (y == false)
}

So, conceptually, the encoding defines different get and set functions for every type. The effect of setting the value of a struct member of a given type constrains the value of the getter for the same type, but says nothing about the getters of other types. So in the example, the Int value of member 0 of the struct is set to 10, but its Bool (and Ref, and Seq, etc) values are unconstrained, so it makes sense that you can prove that its Bool value is either true or false.

I agree that this is probably unexpected when using 2vyper's struct encoding as a general struct encoding, and that it is not so obvious that domains with type parameters conceptually declare functions with type parameters s.t. two versions of the same function with different type arguments are essentially independent. But knowing that, I think Viper's behavior makes sense. 2vyper itself will only ever generate Viper code that always accesses a member of a given struct with the same getter, so the surprising effect should never be visible on the Vyper level.

[DebraChait]

Thanks for the explanation! The resulting behavior is certainly a bit strange, but the explanation makes sense. (This might be a nice example to add to the Viper tutorial to demonstrate the way Viper handles parameterized domains.)