nethermindeth / horus-checker Goto Github PK

Bug description
Horus mishandles functions in namespaces under unknown circumstances, which breaks correctness of judgements of seemingly unrelated functions.

Expected behavior
Horus should conceptually not distinguish between functions within or outside-of namespaces.

To Reproduce
The _stack.lit function gives a wrong judgement in the following example:

%lang starknet

struct Stack {
    value: felt,
    next: Stack*,
}

namespace _Stack {
    func empty() -> (stack: Stack*) {
        return (cast(0, Stack*),);
    }

    // @post $Return.stack.value == stack.value + stack.next.value
    // @post $Return.stack.next == stack.next.next
    func add(stack: Stack*) -> (stack: Stack*) {
        let x = stack.value;
        let y = stack.next.value;
        return (new Stack(value=x + y, next=stack.next.next),);
    }

    // @post $Return.stack.value == i
    // @post $Return.stack.next == stack
    func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
        return (new Stack(value=i, next=stack),);
    }

    // @post $Return.res == stack.value
    func top(stack: Stack*) -> (res: felt) {
        return (stack.value,);
    }
}

// @post [ap - 1] == x
func main_(x: felt) -> (res: felt) {
    let (stack) = _Stack.empty();
    let (stack) = _Stack.lit(stack, x);
    let (top) = _Stack.top(stack);
    return (top,);
}

But gives a correct judgement if we change main_ to:

// @post [ap - 1] == 11
func main_() -> (res: felt) {
    let (stack) = _Stack.empty();
    let (stack) = _Stack.lit(stack, 5);
    let (stack) = _Stack.lit(stack, 6);
    let (stack) = _Stack.add(stack);
    let (top) = _Stack.top(stack);
    return (top,);
}

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

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

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...

Consider the following Cairo files:

The snippets above are the entire files. When we run horus-compile on x.cairo, we get the following output:

(horus37) user@computer:~/pkgs/horus-checker/demos$ ./display.sh x.cairo
~~~~~~~~~~~~~~~{SOURCE}~~~~~~~~~~~~~~
from y import f

~~~~~~~~~~~~~~{RESULT}~~~~~~~~~~~~~~~
/home/user/pkgs/horus-checker/demos/y.cairo:1:1: CheckKind.PRE_COND annotation is not allowed here
@pre True
^*******^

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

horus-check: user error (Malformed contract *.json. Cause: Error in $: not enough input)

real    0m0.005s
user    0m0.000s
sys     0m0.004s

Some interesting things about this bug:

• The line number and character number are wrong in the error message
• If we remove f and instead import g, the bug does not appear
• If you leave f and import both f and g, the bug does not appear

Describe the bug
Horus can't seem to check a storage update of an external function call. In my example Contract B calls the function 'initialize' in Contract A, which updates a storage variable (in contract A). If i write the horus condition in Contract B checking that a storage update was indeed made, then i get error:

ContractB.cairo:1:1: Unknown identifier '_storvar'.
@storage_update _storvar() := 1
^*****************************^ 

I was wondering if this behaviour is normal / would it be possible to add this feature, as I am testing mutliple contract interactions for a project!

Contract A:

%lang starknet


from starkware.cairo.common.cairo_builtins import HashBuiltin, SignatureBuiltin, EcOpBuiltin


@storage_var
func _storvar() -> (res: felt) {
}


namespace LibraryContract {


    func initialize{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}(
        x: felt
    ) {
        // initialize the contract
        _storvar.write(x);
        return ();
    }

}

Contract B:

%lang starknet


from starkware.cairo.common.cairo_builtins import HashBuiltin, SignatureBuiltin, EcOpBuiltin
from ContractA import (
LibraryContract
)


//@storage_update _storvar() := 1
@external
func main{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}() {
    LibraryContract.initialize(1);
    return ();
}

• Versions of SMT solvers used (z3 --version, mathsat -version, cvc5 --version).
• Z3 version 4.12.1 - 64 bit
• Horus version: 0.1.0.1
• Horus-compile (required): >=0.0.6.8, <0.0.7
• This is cvc5 version 1.0.3 [git tag 1.0.3 branch HEAD]
  compiled with GCC version 11.3.0

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

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

After running the command: sudo docker build . -t horus

I got this:

=> ERROR [ 6/14] RUN sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && 0.3s

[ 6/14] RUN sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && if [ $(arch) = "aarch64" ]; then sh scripts/ci/install-z3-from-source.sh; else sh scripts/ci/install-z3-linux-amd64.sh; fi && rm -rf scripts/:
#10 0.243 sh: 0: cannot open scripts/ci/install-mathsat-linux.sh: No such file

executor failed running [/bin/sh -c sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && if [ $(arch) = "aarch64" ]; then sh scripts/ci/install-z3-from-source.sh; else sh scripts/ci/install-z3-linux-amd64.sh; fi && rm -rf scripts/]: exit code: 2

I have a function that can revert for some inputs. I would like to know how to use horus (@pre/@post or other feature) in such a situation. For example:

func assertValid{range_check_ptr}(n) {
with_attr error_message("Number out of bound") {
assert_le(n, SomeBound);
assert_le(-SomeBound, n);
}
return ();
}

Thanks!

See below.

(horus39) mal@computer:~/pkgs/horus-checker$ horus-compile annotated.cairo --output compiled.json --spec_output spec.json
Traceback (most recent call last):
  File "/home/mal/conda/envs/horus39/bin/horus-compile", line 8, in <module>
    sys.exit(run())
  File "/home/mal/pkgs/horus-checker/horus-compile/src/horus/compiler/horus_compile.py", line 412, in run
    main(sys.argv[1:])
  File "/home/mal/pkgs/horus-checker/horus-compile/src/horus/compiler/horus_compile.py", line 396, in main
    preprocessed = horus_compile_common(
  File "/home/mal/pkgs/horus-checker/horus-compile/src/horus/compiler/horus_compile.py", line 225, in horus_compile_common
    pass_manager = pass_manager_factory(args, module_reader)
  File "/home/mal/pkgs/horus-checker/horus-compile/src/horus/compiler/horus_compile.py", line 375, in pass_manager_factory
    return horus_pass_manager(
  File "/home/mal/pkgs/horus-checker/horus-compile/src/horus/compiler/horus_compile.py", line 115, in horus_pass_manager
    manager = starknet_pass_manager(
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/compiler/starknet_pass_manager.py", line 33, in starknet_pass_manager
    hint_whitelist = None if disable_hint_validation else get_hints_whitelist()
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/hints_whitelist.py", line 9, in get_hints_whitelist
    return HintsWhitelist.from_dir(dirname=WHILTELIST_DIR)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/secure_hints.py", line 110, in from_dir
    whitelists = [
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/secure_hints.py", line 111, in <listcomp>
    cls.from_file(filename=os.path.join(dirname, x))
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/secure_hints.py", line 103, in from_file
    return cls.loads(data=fp.read())
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starkware_utils/serializable_dataclass.py", line 32, in loads
    return cls.Schema().loads(json_data=data)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 756, in loads
    return self.load(data, many=many, partial=partial, unknown=unknown)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow_dataclass/__init__.py", line 639, in load
    all_loaded = super().load(data, many=many, **kwargs)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 722, in load
    return self._do_load(
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 861, in _do_load
    result = self._deserialize(
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 664, in _deserialize
    value = self._call_and_store(
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 500, in _call_and_store
    value = getter_func(data)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/schema.py", line 661, in <lambda>
    getter = lambda val: field_obj.deserialize(
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow/fields.py", line 370, in deserialize
    output = self._deserialize(value, attr, data, **kwargs)
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/secure_hints.py", line 77, in _deserialize
    entries = [HintsWhitelistEntry.Schema().load(entry) for entry in value]
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starknet/security/secure_hints.py", line 77, in <listcomp>
    entries = [HintsWhitelistEntry.Schema().load(entry) for entry in value]
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/marshmallow_dataclass/__init__.py", line 644, in load
    return clazz(**all_loaded)
  File "<string>", line 5, in __init__
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starkware_utils/validated_dataclass.py", line 24, in __post_init__
    self.validate_dataclass()
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starkware_utils/validated_dataclass.py", line 27, in validate_dataclass
    self.validate_types()
  File "/home/mal/conda/envs/horus39/lib/python3.9/site-packages/starkware/starkware_utils/validated_dataclass.py", line 123, in validate_types
    typeguard.check_type(
TypeError: check_type() got an unexpected keyword argument 'argname'

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": {}
}

I think that it would be interesting to see the counter-example generated by the SMT solver. The "False" is already helpful but a counter-example can help the specifier to improve the annotations. Thanks!

Expected behavior
In this example:

%lang starknet


from starkware.cairo.common.cairo_builtins import HashBuiltin, SignatureBuiltin, EcOpBuiltin


@storage_var
func _storvar() -> (res: felt) {
}


namespace TestContract {

    //@storage_update _storvar() := x
    func initialize{syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr}(
        x: felt
    ) {
        // initialize the contract
        _storvar.write(x);
        return ();
    }

}

compiling / checking doesnt produce an output as the condition is written inside the namespace 'TestContract'. As of now it works if you remove the namespace or add an external function i.e. main, that calls the function TestContract.initialize. Would it be possible for horus to check functions inside a namespace without calling the function externally ?

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

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

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?

The CLI and JSON output of horus-compile was altered to spit out the specs separately. Now horus-check takes an additional argument --spec_output. However, the docs display the old way of doing things in several places, for example:

I was wondering what invariant condition (and where) I need to add to a recursive function

func compute_sum(n: felt) -> (sum: felt) {

    if (n == 0) {
        // When 0 is reached, return 0.
        return (sum=0);
    }

    // @invariant n >= 0
    loop:
    let (sum) = compute_sum(n=n - 1);
    let new_sum = sum + n;
    
    return (sum=new_sum);
}

func main() {
    let (res) = compute_sum(n=10);
    return();
}

General comments on the docs.

you will also need to use the -s flag to specify which SMT solvers you would like to use for the testing

UX wise, maybe this could be transparent? As in, we set a default to -s z3 or some such and then -s will be an 'advanced' setting?

The following flags are able to added with

Typo.

Specifies conditions that must be true if the function returns.

For future reference: what if the function does not return 🤔 (rollbacks?). Nevertheless, would probably sound better 'when the function returns' to both implicitly assume it returns and make it clearer that it's at the point when the function does return, not 'if it returns anything', which fails to refer to said specific point in time.... or maybe I'm overthinking this and it's fine! :)

Restricts the initial state, value of logical variables, or set of possible inputs for which the postcondition must hold.

Maybe this shouldn't mention postcondition at all 🤔 .

Allows the introduction of logical variables.

Worth explaining they're variables to conveniently refer to (sub)expressions?

Allows claims to be made about the state of a storage variable before and after the function. ...

The entire section on logical variables is rough, but I think this simply stems from the confusing nature of the machinery we have implemented... this might warrant a rethink as to how we express these updates 🤔.

Bug description
Horus incorrectly claims that programs manipulating builtin-pointers that use @assertions or @invariants are incorrect (False).

Expected behavior
Horus should be able to give a 'Verified' result for programs that manipulate builtin pointers in a manner that is consistent with the expected semantics even if one uses either of the pertinent constructs.

To Reproduce

%builtins range_check

// @post a < 2**128
func apply_range_check{range_check_ptr}(a) -> () {
    [range_check_ptr] = a;
    let range_check_ptr = range_check_ptr + 1;
    // Alternatively, @assert a < 2**128
    // @invariant a < 2**128
    hrafn:
    return ();
}

If we remove the @invariant, Horus correctly claims the specification is correct.
Adding an @invariant exactly at the place of a return should be equivalent to specifying a postcondition,
yet these behaviours differ and Horus falsely reports that there is a mistake within the program.

Horus-compile version:
horus-compile 0.0.6.9; cairo-compile 0.10.1

Horus-check version:
Horus version: 0.1.0.1
Horus-compile (required): >=0.0.6.8, <0.0.7

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

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

Additional context
By a remarkable coincidence, I am one of the authors of Horus.

This error is a side-effect of how the behaviour of @assert (and @invariant) is implemented. More specifically, they split the reasoning about a function into two parts, one of which reasons 'until the assert' and the other 'since the assert'.

As of the moment of writing, it is unclear how difficult it would be for Horus to figure out automatically in what state the builtin pointers should be as the split occurs. Note that if a function is allowed to reach its postcondition in the sense that there is no split in reasoning in the middle, we do know what needs to hold about builtin pointers and can instruct Horus to check it.

There is a potential 'simple' solution to this, which would involve providing the ability to have users specify invariants that should hold with regards to builtin pointers, thus overriding the default expected behaviour; it's important to note however, that Cairo 1.0. will remove this problem altogether and as such, time has not been allocated to prioritise the feature, considering it cannot lead to an issue where a program that is incorrect gets reported as Verified.