Incompleteness due to multiple different representation of state snapshots

[aterga]

Hi,

We've been experimenting with using Viper for verifying smart contracts in the Motoko language. I've stumbled upon a strange incompleteness: After a method call, I cannot assert a property that follows from the callee's postcondition. However, if I assert this (quantified) postcondition right after the call, both it and the assertion in question can be verified.

method callee(y: Ref, k: Int)
    ensures forall kk: Int ::
        { prop(y, kk) }
            kk != k ==> prop(y, kk) == old(prop(y, kk))

method client_fails(x: Ref, t: Int) {
    var b: Bool
    if (b) {
        label aux
        callee(x, t)
        assert GOAL  // this assertion fails
    }
}

method client_verifies(x: Ref) {
    var b: Bool
    if (b) {
        label aux
        callee(x, t)
        assert forall kk: Int ::
            { prop(y, kk) }
                kk != t ==> prop(x, kk) == old[aux](prop(x, kk))
        assert GOAL  // this assertion verifies
    }
}

After looking into the SMT query that Silicon produces for the client method, I see that the callee's postcondition is added with the following pattern:

        :pattern (
            (HashMap_Pair_Principal_Principal_get%limited 
                ($Snap.first 
                    ($Snap.second 
                        ($Snap.second 
                            ($Snap.second 
                                ($Snap.second $t@50@10)
                            )
                        )
                    )
                ) 
                ($SortWrappers.$SnapTo$Ref 
                    ($Snap.first 
                        ($Snap.second 
                            ($Snap.second 
                                ($Snap.second $t@50@10)
                            )
                        )
                    )
                ) 
                kk@95@10)
            )

while the client-side (manual) assertion of the same formula has a pattern that differs in the first argument:

                    :pattern (
                        (HashMap_Pair_Principal_Principal_get%limited 
                            ($Snap.first $t@94@10) 
                            ($SortWrappers.$SnapTo$Ref 
                                ($Snap.first 
                                    ($Snap.second 
                                        ($Snap.second 
                                            ($Snap.second $t@50@10)
                                        )
                                    )
                                )
                            ) 
                            kk@97@10
                        )
                    )

Question: Why is it that Silicon creates two different syntactic terms for the same state snapshot in this case?

[mschwerhoff]

Each assertion is symbolically evaluated independently, which can give rise to semantically equivalent but syntactically different snapshots. This can result in incompletenesses, and you unfortunately hit on such incompleteness (triggering). Silicon implements simple heuristics to reduce the chance that these happen, but the heuristics must be cheap (to not affect performance), and are thus brittle.

I unfortunately don't have a good workaround to suggest right now.

[aterga]

Thanks for looking into this. Feel free to decide what to do with the ticket (I just wanted to somehow keep track of the incompletenesses we stumble upon to make sure we're not running in circles).