Revertable function

[acmLL]

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!

[langfield]

Hi! I'll need a bit more information on how you expect this function to behave. It appears that it will simply raise an error if n is out-of-bounds. When you specify the behavior of a function with a @pre/@post pair, you are asserting that if the preconditions are satisfied, and if the function returns, then the postcondition(s) are satisfied at that point.

If the function raises an error, then the function never returns, and thus the conditions specified in the @post annotation(s) are not applicable.

Does this make any sense?

[acmLL]

Thanks, @langfield ! But looking into the cairo documentation, when the function cannot complete, (in this case) it sends an error message that can be checked outside this function. The Certora prover uses an annotation @withRevert (associated with a function to signal that the function can revert) and a boolean variable "lastReverted", which reveals if this function worked as expected or reverted... What can we do with horus about this? I know that such a situation is not usual in the formal methods community but it is practical...in the present context...

[Ferinko]

@acmLL The best we can currently do about this is to mark this as a feature request (smh took me a while to realize we have this as an 'enhancement tag'!) and add it to our internal pile of features to work on :).

Thank you kindly for sketching the way Certora does it, one can certainly take some inspiration from their approach. I do think Horus does indeed need some way to reason about this and I suspect this will be a common request, so I'll make sure to assign appropriate priority.

[acmLL]

Thank you very much, @Ferinko ! Another point I would like to ask is: can we use horus with "tests" without concrete values? Something like a \forall x... instead of a x = 2... Best!

[Ferinko]

@acmLL Of course you can; as a matter of fact, \forall is in some sense 'implicit' unless you go out of your way to assign concrete numbers - admittedly the 'main' stack example in the readme does not convey this particularly well :-/.

As a simple example, this test proves for the function comp_id that the composition of succ and pred is the identity. The spec for said function can be read as: forall x, comp_id x = x. And indeed, the spec for said succ function states: forall x, succ x = x + 1, etc.

There are many more examples in the tests/resources/golden folder, do feel encouraged to take a look at said *.cairo files (the corresponding *.gold files are there for automated testing).

[Ferinko]

I have also made a small change to the original example:

%lang starknet

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

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

// @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) = empty();
    let (stack) = lit(stack, x + 1);
    let (tawp) = top(stack);
    return (tawp,);
}

Which outputs:

lit
Verified

main_
False

top
Verified

empty [inlined]
Verified

Note that I made a deliberate mistake and pushed x+1, one can get a correct result with x. I also removed the namespace because we've just run into a bug where things break subtly when namespaces are used (oops), which explains the delay in my writing up this example! :)

Note that this (dis)proves that forall inputs, the function returns x, which is taken from the top of the stack.

[acmLL]

Wonderful, @Ferinko ! I was expecting something like this because solvers did not to work only with concrete values! Thank you very much, @acmLL