Contradictory premises

[acmLL]

When I write a precondition like this

// @pre b >= 0 and b <= BOUND

where b is felt and BOUND is a positive number, horus gives the expected answer. But if we consider a negative number like this

// @pre b >= -1 and b <= BOUND

we get:

main_
Contradictory premises

Why?

[langfield]

This is because arithmetic in StarkNet takes place over a finite field. In particular, -1 is just another name for the equivalence class of p - 1 in the finite field, where $p$ is the order (in StarkNet, always some prime).

Note that in a finite field, we have:

• $0 &lt; -1$

And Horus agrees:

(horus37) user@computer:~/pkgs/horus-checker/demos$ ./display.sh premises.cairo
~~~~~~~~~~~~~~~{SOURCE}~~~~~~~~~~~~~~
// @post -1 <= 0
func f(b: felt) -> felt {
    return b;
}

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

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

f
False


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

~~~~~~~~~~~~~~{FILENAME}~~~~~~~~~~~~~
premises.cairo

In other words, $-1$ is the "largest" element of the field. If we choose const BOUND = 2 and say we're working over $\mathbb{F}_5$, then $-1 = 4$, and so your precondition is:

// @pre b >= 4 and b <= 2

The only field element >= 4 is 4, and so it reduces to // @pre b == 4 and b <= 2, which reduces to // @pre 4 <= 2.
It is indeed a contradictory premise.

[acmLL]

Thanks, @langfield !