The semantics of operator `/` in assertions is not the proper `felt` semantics

[aemartinez]

Describe the bug For field elements, the operation a / b results in an x such that b * x = a. (Because this is an operation in the field, when a is not a multiple of b, x is not the integral part of the quotient as if operating with Ints).

Horus-compile transforms the / operator in assertions to the div operator in SMTLIB. The assertion @post $Return.res == a / b will be translated to (= (memory (+ ap (- 1))) (div (memory (+ fp (- 4))) (memory (+ fp (- 3))))) (where a and b are the arguments of the function).

This leads to unexpected behavior, even if horus-check encodes operations using modulo P.

Expected behavior

// @pre 0 < a and a < 100 and 0 < b and b < 100
// @post $Return.res == a / b
func division(a, b) -> (res: felt) {
    return (res=a/b);
}

I expect

division
Verified

I get

division
False

To Reproduce horus-compile==0.0.6.11 horus-check latest version in master Solver: default (cvc5)

Operating system [x] Linux [ ] MacOS [ ] Windows [ ] Other (please write)

CPU architecture [ ] x86-64 [x] AArch64 [ ] Other (please write)

Additional context

Unoptimized smt query obtained from the example (simplified, showing only the relevant assertions)

(declare-fun MEM!1 () Int)
(declare-fun MEM!2 () Int)
(declare-fun MEM!3 () Int)
(declare-fun prime () Int)
(assert (and (<= 0 MEM!1) (< MEM!1 prime)))
(assert (and (<= 0 MEM!2) (< MEM!2 prime)))
(assert (and (<= 0 MEM!3) (< MEM!3 prime)))
(assert (= prime 3618502788666131213697322783095070105623107215331596699973092056135872020481))
(assert (and (< 0 MEM!1) (> 100 MEM!1) (< 0 MEM!2) (> 100 MEM!2)))
(assert (= (mod (* MEM!3 MEM!2) prime) MEM!1))
(assert (not (= MEM!3 (mod (div MEM!1 MEM!2) prime))))

(check-sat)
(get-model)

z3 output

sat
(
  (define-fun MEM!2 () Int
    98)
  (define-fun MEM!1 () Int
    99)
  (define-fun MEM!3 () Int
    480005471965915365082297920206488891562248916319497521425002007446595268024)
  (define-fun prime () Int
    3618502788666131213697322783095070105623107215331596699973092056135872020481)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    1)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    1)
)

spec.json:

{

    "horus_version": "0.0.6.11",
    "invariants": {},
    "specifications": {
        "__main__.division": {
            "decls": {},
            "logical_variables": {},
            "post": {
                "sexpr": [
                    "(= (memory (+ ap (- 1))) (div (memory (+ fp (- 4))) (memory (+ fp (- 3)))))"
                ],
                "source": [
                    "$Return.res == a / b"
                ]
            },
            "pre": {
                "sexpr": [
                    "(and (< 0 (memory (+ fp (- 4))))",
                    "     (> 100 (memory (+ fp (- 4))))",
                    "     (< 0 (memory (+ fp (- 3))))",
                    "     (> 100 (memory (+ fp (- 3)))))"
                ],
                "source": [
                    "0 < a and a < 100 and 0 < b and b < 100"
                ]
            },
            "storage_update": {}
        }
    },
    "storage_vars": {}
}

[langfield]

In other words:

• a / b in annotations tells you the biggest $x$ such that $bx \leq a$,
• a / b in Cairo gives you the only $x$ with $0 \leq x < p$ such that $bx \equiv a \mod p$.

For example, in $\mathbb{F}_5$:

• 4 / 3 in annotations is $1$.
• 4 / 3 in Cairo is $3$.

Intuitively, we perform the following:

• Annotations: do decimal division, and round down.
• Cairo: Arrange numbers $0$ through $p$ on a clock. To divide $a$ by $b$, we start at $0$ and jump by steps of size $b$ around the clock until we hit $a$. The number of jumps is the quotient.

[langfield]

Fixed by https://github.com/NethermindEth/horus-compile/pull/62.