Improper interaction of @invariant/@assert with manipulation of builtin pointers.

[Ferinko]

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.