Something is wrong with the implications in queries

[langfield]

Consider the following example:

// @pre token == 0 or token == 1
// @post (token == 0 and $Return.t == 1) or (token == 1 and $Return.t == 0)
func get_opposite_token(token: felt) -> (t: felt) {
    if (token == 0) {
        return (t=1);
    } else {
        return (t=0);
    }
}

// @post $Return.res == 42
func foo() -> (res: felt) {
	let (t) = get_opposite_token(2);
	return (res=42);
}

Note that we pass token=2 to our call to get_opposite_token(). This violates the precondition. However, this program results in the following output:

(horus37) user@computer:~/pkgs/horus-checker/demos$ ./display.sh agustin.cairo
~~~~~~~~~~~~~~~{SOURCE}~~~~~~~~~~~~~~
// @pre (token == 0) or (token == 1)
// @post (token == 0 and $Return.t == 1) or (token == 1 and $Return.t == 0)
func get_opposite_token(token: felt) -> (t: felt) {
    if (token == 0) {
        return (t=1);
    } else {
        return (t=0);
    }
}

// @post $Return.res == 42
func foo() -> (res: felt) {
        let (t) = get_opposite_token(2);
        return (res=42);
}

~~~~~~~~~~~~~~{RESULT}~~~~~~~~~~~~~~~

real    0m1.254s
user    0m1.199s
sys     0m0.056s
Warning: Horus is currently in the *alpha* stage. Please be aware of the
Warning: known issues: https://github.com/NethermindEth/horus-checker/issues

foo
Verified

get_opposite_token
Verified


real    0m0.072s
user    0m0.053s
sys     0m0.020s
~~~~~~~~~~~~~~{REVISION}~~~~~~~~~~~~~
82d626a (HEAD -> master, origin/master, origin/HEAD) Merge pull request #162 from NethermindEth/julek/MathSAT_fix

~~~~~~~~~~~~~~{FILENAME}~~~~~~~~~~~~~
agustin.cairo

The function foo() is Verified, which is wrong. If we comment-out the postcondition for get_opposite_token(), we get False as we expect. The following is the pretty-printed SMT query:

0 ≤ AP!@1 ∧ AP!@1 < prime
0 ≤ fp!10:get_opposite_token ∧ fp!10:get_opposite_token < prime
0 ≤ fp! ∧ fp! < prime
prime == 3618502788666131213697322783095070105623107215331596699973092056135872020481
addr1 == AP!@1                                      # Address of argument in call to `get_opposite_token()`
addr2 == (AP!@1 + 1) % prime
addr3 == (AP!@1 + 2) % prime
addr4 == (fp!10:get_opposite_token + -3) % prime    # Address of `token`        (parameter of `get_opposite_token()`)
addr5 == (AP!@1 + 3) % prime                        # Address of `$Return.t`    (return value of `get_opposite_token()`)
addr6 == (AP!@1 + 4) % prime                        # Address of `$Return.res`  (return value of `foo()`)
fp! ≤ AP!@1
AP!@1 == fp!
2 == mem1
fp!10:get_opposite_token == (AP!@1 + 3) % prime
  ∧ mem2 == fp!
  ∧ mem3 == 12
0 == token ∨ 1 == token ∨ ¬(42 == $Return.res ∧ (0 == token ∧ 1 == $Return.t ∨ 1 == token ∧ 0 == $Return.t))
⇒
42 == $Return.res
  ∧ (0 == token ∨ 1 == token)
  ∧ (0 == token ∧ 1 == $Return.t ∨ 1 == token ∧ 0 == $Return.t)
  ∧ ¬(42 == $Return.res)

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 to get_opposite_token(). The equalities concerning the addrs and the precondition together imply that addr1 == addr4, and thus token == 2 when we call get_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):

0 == 2 ∨ 1 == 2 ∨ ¬(42 == $Return.res ∧ (0 == 2 ∧ 1 == $Return.t ∨ 1 == 2 ∧ 0 == $Return.t))
False ∨ False ∨ ¬(42 == $Return.res ∧ (False ∧ 1 == $Return.t ∨ False ∧ 0 == $Return.t))
False ∨ False ∨ ¬(42 == $Return.res ∧ (False ∨ False))
False ∨ False ∨ ¬(42 == $Return.res ∧ False)
False ∨ False ∨ ¬(False)
False ∨ False ∨ True
True
⇒
42 == $Return.res
  ∧ (0 == 2 ∨ 1 == 2)
  ∧ (0 == 2 ∧ 1 == $Return.t ∨ 1 == 2 ∧ 0 == $Return.t)
  ∧ ¬(42 == $Return.res)
42 == $Return.res
  ∧ (False ∨ False)
  ∧ (False ∧ 1 == $Return.t ∨ False ∧ 0 == $Return.t)
  ∧ ¬(42 == $Return.res)
42 == $Return.res
  ∧ False
  ∧ False
  ∧ ¬(42 == $Return.res)
False

Clearly this is Unsat, and thus we get Verified.

Julian has the following to add:

The implication with the extra (un-negated) post is generated on line 141 in the snippet below:

horus-checker/src/Horus/CairoSemantics/Runner.hs

Lines 135 to 142 in 82d626a

	.= ( ( ExistentialAss
	( \mv ->
	let restAss' = map (builderToAss mv . fst) restAss
	asAtoms = concatMap (\x -> fromMaybe [x] (unAnd x)) restAss'
	restExp' = map fst restExp
	in (a mv .|| Expr.not (Expr.and (filter (/= a mv) asAtoms)))
	.=> Expr.and (restAss' ++ [Expr.not (Expr.and restExp') | not (null restExp')])
	)

So we think somehow the post is ending up in restAss':

horus-checker/src/Horus/CairoSemantics.hs

Line 425 in 82d626a

assert pre *> expect post

Which is surprising, as the only place where the post is manipulated in query generation is here, which quite clearly adds it into the set of expects, not assertions...

[langfield]

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:

horus-checker/src/Horus/CairoSemantics.hs

Lines 342 to 348 in 82d626a

	mkInstructionConstraints :: LabeledInst -> Label -> Map (NonEmpty Label, Label) Bool -> CairoSemanticsL ()
	mkInstructionConstraints lInst@(pc, Instruction{..}) nextPc jnzOracle = do
	fp <- getFp
	dst <- prepare pc fp (memory (regToVar i_dstRegister + fromInteger i_dstOffset))
	case i_opCode of
	Call -> mkCallConstraints pc nextPc fp =<< getCallee lInst
	AssertEqual -> getRes fp lInst >>= \res -> assert (res .== dst)

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.

[langfield]

This may have been fixed by #187.