fix top constraint

[andreistefanescu]

patch for transferFrom-failure-1-spec. The specific issue here is that chop(BAL_TO_1347:Int +Int VALUE_1344:Int) >Int BAL_TO_1347:Int)) is being evaluated to BAL_TO_1347:Int +Int VALUE_1344:Int >Int BAL_TO_1347:Int when that exact inequality is in the topConstraint. This is sound, and makes a call to z3, but results in information loss. I don't have a simple solution, but this patch should unblock @daejunpark

more generally, this would require better control over how constraints are evaluated

[daejunpark]

@andreistefanescu could you explain a bit more about the information loss and how this resetting the topconstraint solves the problem?

[andreistefanescu]

Currently, we use the existing constraint ("top constraint") when we apply functions inside terms and formulae. If we set it before trying to take a rewrite step, and don't unset it, it will be used to simplify anything, including itself. In particular, when the constraint has the chop(BAL_TO_1347:Int +Int VALUE_1344:Int) >Int BAL_TO_1347:Int inequality (and also that both BAL_TO_1347 and VALUE_1344:Int are between 0 and 2^256), it will attempt to apply the chop function rule chop(I) => I if 0 <= I <2^256, and it will succeed, because chop(BAL_TO_1347:Int +Int VALUE_1344:Int) >Int BAL_TO_1347:Int ==> 0 <= BAL_TO_1347:Int +Int VALUE_1344:Int < 2^256. But then, the resulting constraint only has BAL_TO_1347:Int +Int VALUE_1344:Int >Int BAL_TO_1347:Int, which is only implied by the initial constraint, but not equivalent, hence the information loss. Because of this, the constraint for the execution path without exceptions becomes satisfiable, and the proof fails. This is sound but incomplete, so my fix is to avoid simplifying a constraint using itself.

[daejunpark]

@andreistefanescu this change also improves the prover performance for the hkg proofs as well, which is great! But, unfortunately, it introduces an exiting proof failure: viper/transferFrom-failure-2-spec.k. Could you take a look?