Open langfield opened 1 year ago
I do not believe that it is on line 425 as suggested above. I have traced the contents of restAss'
and found it to be here on line 348:
https://github.com/NethermindEth/horus-checker/blob/82d626a97969610df3abf202952766157923b7de/src/Horus/CairoSemantics.hs#L342-L348
Here is the tracing output:
~~~~~~~~~~~~~~{RESULT}~~~~~~~~~~~~~~~
real 0m1.261s
user 0m1.185s
sys 0m0.077s
Warning: Horus is currently in the *alpha* stage. Please be aware of the
Warning: known issues: https://github.com/NethermindEth/horus-checker/issues
res == dst: 2 == MEM!1
preparedPre and preparedPost: ((0 == MEM!4 ∨ 1 == MEM!4) ∧ ((0 == MEM!4 ∧ 1 == MEM!5) ∨ (1 == MEM!4 ∧ 0 == MEM!5)))
res == dst: 42 == MEM!6
restAss: [(QFAss True,InstructionSemanticsAssertion),(QFAss 42 == MEM!6,InstructionSemanticsAssertion),(QFAss ((0 == MEM!4 ∨ 1 == MEM!4) ∧ ((0 == MEM!4 ∧ 1 == MEM!5) ∨ (1 == MEM!4 ∧ 0 == MEM
!5))),InstructionSemanticsAssertion)]
restAss': [True,42 == MEM!6,((0 == MEM!4 ∨ 1 == MEM!4) ∧ ((0 == MEM!4 ∧ 1 == MEM!5) ∨ (1 == MEM!4 ∧ 0 == MEM!5)))]
restAss': [True,42 == MEM!6,((0 == MEM!4 ∨ 1 == MEM!4) ∧ ((0 == MEM!4 ∧ 1 == MEM!5) ∨ (1 == MEM!4 ∧ 0 == MEM!5)))]
res == dst: 0 == MEM!2
res == dst: 1 == MEM!2
foo
Verified
get_opposite_token
Verified
real 0m0.074s
user 0m0.053s
sys 0m0.022s
Note that 42 == MEM!6
is the offending boolean expression, and it only appears in a res == dst
assert.
This may have been fixed by #187.
Consider the following example:
Note that we pass
token=2
to our call toget_opposite_token()
. This violates the precondition. However, this program results in the following output:The function
foo()
isVerified
, which is wrong. If we comment-out the postcondition forget_opposite_token()
, we getFalse
as we expect. The following is the pretty-printed SMT query:For ease of readability, we have made the following substitutions:
mem4
$\mapsto$token
mem5
$\mapsto$$Return.t
mem6
$\mapsto$$Return.res
Note that
mem1
is the argument passed toget_opposite_token()
. The equalities concerning theaddr
s and the precondition together imply thataddr1 == addr4
, and thustoken == 2
when we callget_opposite_token()
.On the right-hand side, we have both
42 == $Return.res
and¬(42 == $Return.res)
. This does not appear to be correct. In particular, it is possible that the first expression should not be in this conjunction.We can simplify the implication as follows (each unindented line/block is a simplification of the previous line/block):
Clearly this is
Unsat
, and thus we getVerified
.Julian has the following to add: