How to use loop invariants

[Leonard-Pat]

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();
}

[langfield]

I'm unsure if we can write a better invariant than this. @Ferinko would know best. It seems the example is not very interesting without a postcondition describing what the compute_sum() function should do. It isn't necessary, but without it, Horus is not really doing much.

Moreover, according to @Ferinko, the invariant annotation and label don't do anything because there's no jumping. Take a look at this, which only works for small n:

// @pre n >= 0
// @pre n <= 15
// @post 2 * $Return.sum == n * (n + 1)
func compute_sum(n: felt) -> (sum: felt) {
    if (n == 0) {
        // When 0 is reached, return 0.
        return (sum=0);
    }

    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();
}

(horus37) mal@computer:~/pkgs/horus-checker/demos$ ./display.sh invariant.cairo
~~~~~~~~~~~~~~~{SOURCE}~~~~~~~~~~~~~~
// @pre n >= 0
// @pre n <= 15
// @post 2 * $Return.sum == n * (n + 1)
func compute_sum(n: felt) -> (sum: felt) {
    if (n == 0) {
        // When 0 is reached, return 0.
        return (sum=0);
    }

    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();
}

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

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

compute_sum
Verified

main [inlined]
Verified


real    0m1.640s
user    0m1.618s
sys     0m0.024s
~~~~~~~~~~~~~~{REVISION}~~~~~~~~~~~~~
3f2e0db (HEAD -> langfield/makerdao-frob, origin/langfield/makerdao-frob) dirty: Bump `horus-compile` version exclusive upper bound to 0.0.8

~~~~~~~~~~~~~~{FILENAME}~~~~~~~~~~~~~
invariant.cairo

This at least works, although from the timeout behavior, I'm fairly sure it's checking via bit-blasting. Any thoughts on how to make this work for larger n @Ferinko?

Edit: Okay it works the same even without the label and invariant. I had assumed this example complained about a loop without invariant before it was added.

[langfield]

It should be noted that our upper bound needs to be sufficiently small so that the product does not wrap around, since we are working in a finite field.

[Ferinko]

I am very confused by this example - what are we trying to show? There's no looping behaviour here, the loop: label is never jumped to and its annotation is a normal Cairo comment, not a Horus thing ::thinking::. (And the sum is computed recursively.)

And if we look at the original example by @Leonard-Pat that does use a Horus annotation of invariant, then Horus will split the reasoning into:

Pre(compute_sum) -> Invariant(loop) and Invariant(loop -> Post(compute_sum); unfortunately, n > 0 is too weak to compute Post(compute_sum) from unless n is severerly bounded and Horus can bruteforce it.

[langfield]

There's no looping behaviour here, the loop: label is never jumped to and its annotation is a normal Cairo comment, not a Horus thing 🤔. (And the sum is computed recursively.)

Okay that's a typo. I guess I didn't understand what is and is not considered a loop.

[langfield]

@Leonard-Pat Can you show us the code example you were running where you did get the "loop with no invariant" error?

[Leonard-Pat]

The function i'm trying to test is as follows:

%lang starknet

from starkware.cairo.common.cairo_builtins import HashBuiltin, SignatureBuiltin
from starkware.cairo.common.alloc import alloc
from starkware.cairo.common.memcpy import memcpy
from starkware.cairo.common.math import assert_not_zero, assert_le, assert_nn
from starkware.starknet.common.syscalls import call_contract
from starkware.cairo.common.bool import TRUE, FALSE


struct CallArray {
    to: felt,
    selector: felt,
    data_offset: felt,
    data_len: felt,
}

// @pre call_array_len >= 0
// @post call_array_len == 0
func execute_multicall{syscall_ptr: felt*}(
    call_array_len: felt, call_array: CallArray*, calldata: felt*
) -> (response_len: felt, response: felt*) {
    alloc_locals;
    if (call_array_len == 0) {
        let (response) = alloc();
        return (0, response);
    }

    // call recursively all previous calls
    let (response_len, response: felt*) = execute_multicall(call_array_len - 1, call_array, calldata);
    let last_call = call_array[call_array_len - 1];

    // call the last call
    with_attr error_message("multicall {call_array_len} failed") {
        let res = call_contract(
            contract_address=last_call.to,
            function_selector=last_call.selector,
            calldata_size=last_call.data_len,
            calldata=calldata + last_call.data_offset,
        );
    }

    // store response data
    assert [response + response_len] = res.retdata_size;
    memcpy(response + response_len + 1, res.retdata, res.retdata_size);
    return (response_len + res.retdata_size + 1, response);
}

I can't seem to add an invariant check, or run horus-checker on it without it throwing an error

[langfield]

Okay this was addressed on Discord: basically, the loopy behavior that requires an @invariant is in a library function that we don't have a pre-written spec for yet. We're working on supporting it but it may take a while as it's nontrivial.