Formal verification of StarkNet smart contracts with language annotations
Report bug · Request feature

Horus is a command-line formal verification tool for StarkNet contracts.

- **Note.** Horus is currently in alpha, and thus should not be fully trusted yet! -

• Installation - Get the horus-compile and horus-check executables setup for your development environment.
• Tutorial: Your first verified StarkNet contract - Try this if you're new to Horus or formal verification in general. This will walk you through an example step-by-step.
• FAQ - What is Cairo? What is Horus? When should I use Horus? Why should I use Horus? All these answered and more!
• Usage - Exhaustive reference information on the CLI options, among other things.
• Internals - In which we explain why things are implemented the way they are, and discuss details relevant to the development of Horus. This is prose to aid contributors and onboard new team members.

Horus is supported on Linux and MacOS (including AArch64 Macs)!

We also have instructions for installing with Docker if you want to run Horus in a container.

• Python 3.9
• Stack (Haskell build tool)
• Poetry (Python package and dependency manager)
• Z3 (version 4.10.2)
• CVC5 (version 1.0.3)

Check your python version:

python3 --version

_{Expected output:}

Python 3.9.13

If you see 3.9 as in above (any variant of 3.9 should be okay), you can skip ahead to installing stack.

Otherwise, you may have a different version, or you may not have python installed at all. Follow the instructions below to install the needed version.

1. Download and install miniconda on your system:

• Linux 64-bit
• macOS Intel x86 64-bit
• macOS Apple M1 64-bit

In each case, run the downloaded script/executable, and follow the instructions.

2. Create a conda environment with python 3.9:

conda create -n horus-py39 python=3.9

In the above, horus-py39 is just a name we've chosen for this environment.

3. Activate the created environment:

conda activate horus-py39

4. Verify that you're running 3.9:

python3 --version

_{Expected output:}

Python 3.9.13

curl -sSL https://get.haskellstack.org/ | sh

brew install stack

These setup instructions assume that you have Homebrew installed on your Mac.

Check that the install was successful:

stack --version

_{Expected output (something like this):}

Version 2.7.5, Git revision ba147e6f59b2da75b1beb98b1888cce97f7032b1 x86_64 hpack-0.34.4

pip3 install poetry

Clone the horus-compile and horus-checker repositories to your machine.

git clone git@github.com:NethermindEth/horus-compile.git
git clone git@github.com:NethermindEth/horus-checker.git

Navigate to the horus-checker/ repository root.

cd horus-checker/

# Inside the `horus-checker/` repository root.
sh ./scripts/ci/install-z3-linux-amd64.sh
sh ./scripts/ci/install-cvc5-linux.sh

# Inside the `horus-checker/` repository root.
sh ./scripts/ci/install-z3-macos.sh
sh ./scripts/ci/install-cvc5-macos.sh

# Inside the `horus-checker/` repository root.
sh ./scripts/ci/install-z3-macos.sh
sh ./scripts/ci/install-cvc5-macos-aarch64.sh

If you're using conda, you can skip to install horus-compile.

Otherwise, navigate to the horus-compile/ repository root and run the following commands:

python -m venv .venv/horus
source .venv/horus/bin/activate

In the above, horus is just the name we chose for our virtual environment.

Make sure you're inside the horus-compile repository root.

On Linux:

pip install .

On macOS:

CFLAGS=-I`brew --prefix gmp`/include LDFLAGS=-L`brew --prefix gmp`/lib pip install .

Navigate to the horus-checker repository root and run:

On Linux:

stack install

On macOS:

C_INCLUDE_PATH="`xcrun --show-sdk-path`/usr/include/ffi" stack --extra-include-dirs=/opt/homebrew/opt/z3@4.10.2/include --extra-lib-dirs=/opt/homebrew/opt/z3@4.10.2/lib install

Note. Stack installs executables to ~/.local/bin by default. Make sure this directory is on your PATH or pass a different install directory with stack install --local-bin-path <dir>.

You can check that the install was successful with:

horus-check --help

If the above command executed without error, you are ready to use Horus!

Follow these instructions if you prefer to install Horus in a docker container. Refer to the Docker documentation for more information on working with containers.

Clone the horus-compile and horus-checker repositories to your machine.

git clone git@github.com:NethermindEth/horus-checker.git
cd horus-checker
git clone git@github.com:NethermindEth/horus-compile.git

sudo docker build . -t horus

This process might take several minutes.

Note. If your local platform is an AArch64 Mac, this process will take even longer because some dependencies will be compiled from source. For us, it took 38min in a MacBook Pro M1.

At the end you should see a message like this:

Successfully built e48336cb10ae
Successfully tagged horus:latest

To access files on the host (your machine) from inside a docker container, you must mount some extant directory. This makes the directory readable and writable from both the host and the container.

Here, we'll create an example project directory named my-cairo-project for this purpose.

mkdir my-cairo-project/

See the docker documentation section on bind mounts for more information.

The following command will:

1. Run the container
2. Mount the directory my-cairo-project/ on your filesystem to the location /home/ on the container's filesystem
3. Drop you into a root shell inside the container

sudo docker run -v $(pwd)/my-cairo-project/:/home/ -it horus:latest /bin/bash

Inside the docker container, run the following commands:

horus-compile --help

horus-check --help

If these commands execute without error, you're ready to use Horus!

Let's verify a StarkNet contract! First, we'll write a simple program that implements a stack data structure in Cairo. If you're unfamiliar with Cairo, or you need a refresher, check out the documentation.

To follow along, the full example program without annotations is provided in example.cairo.

Let's define a struct called Stack with two members:

• one called value which has type felt,
• one called next of type Stack*, which means it's a pointer to an instance of the struct Stack that we're currently defining.

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

Intuitively, we are representing our stack as a linked list. The value is the head of the list, i.e. the top of the stack, and the next member is a pointer to the next node in the list.

Now we've got a bare data structure. Let's define some functions that operate on it.

First, we'll define a function called empty() that takes no arguments and returns a pointer to a new, empty Stack.

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

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

The use of cast() above is a typed reference.

We'll also define a function called add(). It will take one argument, which will be a pointer to a stack, and it will have one return value, also a pointer to a stack.

We can use member accessor notation to access the appropriate data from our parameter stack.

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

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

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

We use the new operator which creates a specified object, in this case a Stack, in the execution segment of our program. It then returns a pointer to the newly created object. In this case, it returns a pointer to a Stack, and that makes sense, since our return value is stack: Stack*!

Next, we'll define a function called lit() for pushing values onto the stack.

By convention, lit stands for "literal", since we're pushing "literal" values. This is a naming tradition that originates from implementations of stack machines and stack-based languages:

LIT is the primitive word for pushing a "literal" number onto the data stack. -Wikipedia page for Forth

Our function will take two arguments, a pointer to a stack, and a literal value i, which has type felt. It will return a pointer to a stack to which the literal i has been pushed, and is now the top element. Our function will leave the rest of the stack unmodified.

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

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

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

func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
  return (new Stack(value=i, next=stack),);
}

And finally, we'll define a function top() which simply returns the top value on the stack without modifying the stack.

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

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

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

func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
  return (new Stack(value=i, next=stack),);
}

func top(stack: Stack*) -> (res: felt) {
  return (stack.value,);
}

We can wrap all these functions up in a namespace called _Stack to clarify usage:

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

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

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

  func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
      return (new Stack(value=i, next=stack),);
  }

  func top(stack: Stack*) -> (res: felt) {
      return (stack.value,);
  }
}

This means when we call them we must write, for example, _Stack.add instead of just add, which makes it slightly clearer what sort of objects we're operating on, and where to find the implementation of that operation.

Great! Now we'll just add a short main() function to test that our stack functions as we expect.

// Declare this program as a starknet contract.
%lang starknet

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

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

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

  func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
      return (new Stack(value=i, next=stack),);
  }

  func top(stack: Stack*) -> (res: felt) {
      return (stack.value,);
  }
}

// Perform some example operations on a stack to sum two integers.
@external
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 (res=top);
}

Our example main() function pushes two literals to an empty stack, adds them, and then returns the result.

See the Hello, StarkNet tutorial if you'd like to try running this contract on a testnet. You should get the answer 11.

Now, let's add some annotations that describe how we expect our _Stack functions to behave, and then we'll prove that the implementations we wrote always do what the annotations say.

Here's our program with the annotations:

%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,);
  }
}

// Perform some example operations on a stack.
// @post $Return.res == 11
@external
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 (res=top);
}

The annotations are the comments directly above each of the functions add(), lit(), and top(), along with the assert comment in main(). They all begin with // @. The @post keyword indicates that an annotation is specifying a condition that must hold at the end of the function call, when the function returns. It is called @post because it is a "postcondition".

Briefly, with the annotations we've added, we are checking that:

• The add() function returns a pointer to a stack with the sum of the first two elements on top, and the remainder of the original stack (the third element and so on) after that.
• The lit function puts i on the top of the stack, and preserves the old stack underneath it.
• The top function actually returns the top of the stack we pass as an argument.
• The top value on the stack in main() is actually 11 (the sum of pushed values 5 and 6).

As an example, let's examine the annotations for the _Stack.add() function:

// @post $Return.stack.value == stack.value + stack.next.value
// @post $Return.stack.next == stack.next.next

Here's what's going on:

• The // is just the syntax for comments.
• The @post declares a Horus postcondition annotation. This condition must hold at the end of each function call.
• The $Return syntax is a way of referring to the return values of the function. So $Return.stack is the return value named stack of the add() function. In general, the $ syntax is how we reference logical variables.
• Both annotations are boolean expressions asserting equality of a pair of values, and we can use arithmetic operators like + in annotations for supported datatypes. See the section on spec syntax for more info on what operators and symbols are supported.
• It is notable that we cannot reference locals within preconditions or postconditions. So if we tried to say @pre x == 0 for the add function, the compiler would print an error message telling us it cannot find the identifier x.

Let's compile this annotated program with Horus and then check these properties:

horus-compile annotated.cairo --output compiled.json --spec_output spec.json

This should create two files called compiled.json and spec.json. Now let's verify the compiled binary:

horus-check --solver z3 compiled.json spec.json

The --solver z3 flag tells Horus which SMT solver to use (Z3, in this case). See also the available solvers.

_{Expected output:}

Warning: Horus is currently in the *alpha* stage. Please be aware of the
Warning: known issues: https://github.com/NethermindEth/horus-checker/issues

_Stack.add
Verified

_Stack.lit
Verified

_Stack.top
Verified

main
Verified

_Stack.empty [inlined]
Verified

The four functions _Stack.add, _Stack.lit, _Stack.top, and main that we annotated all say Verified, which means our implementations are correct with respect to the specifications we wrote in our annotations.

Note: _Stack.empty appears here since Horus implicitly gives all unannotated functions a trivial (always true) specification.

Note: The [inlined] marker just tells us that a given function was inline expanded, which happens whenever a function has no explicit @pre or @post annotations, and but needs to be checked for the purposes of checking something else.

Congrats! You've just formally verified your first StarkNet contract!

Horus is a command-line tool for the StarkNet ecosystem. It helps you formally verify StarkNet smart contracts.

The way it works is like this:

1. You write a StarkNet smart contract.
2. You add annotations that describe how the program should operate.
3. You run Horus on your program, and Horus tells you one of the following:
   • The program obeys the annotations.
   • The program does not obey the annotations (found a counterexample).
   • Ran out of time (Unknown).

“Program testing can be used to show the presence of bugs, but never to show their absence!” ― Edsger W. Dijkstra

Horus can be used to show the absence of bugs.

Note. Horus is currently in alpha, and thus should not be fully trusted yet. Both Horus and SMT solvers may have bugs themselves, and so a given judgement is never a "certainty".

Horus consists of two command-line tools, called horus-compile and horus-check. The first, horus-compile, is a modified version of the Cairo compiler that you can use to compile a program with Horus annotations. You can then run horus-check on the compiled program to formally verify the program's behavior.

StarkNet is a Layer 2 network over Ethereum. Specifically, it is a ZK-Rollup (zero-knowledge rollup), which is basically a way of scaling up the number of transactions that a blockchain can process by bundling (rolling-up) many transactions into one.

Cairo is a Turing-complete language for writing dApps using STARKs. STARK stands for Scalable Transparent Argument of Knowledge.

Basically, it's a programming language for verifiable computing that runs on StarkNet. It lets you write programs where one party can prove to another that a certain computation was executed correctly. The syntax is a bit like Rust.

You can write StarkNet smart contracts in the Cairo language.

Use Horus when you need to be absolutely sure that a function in a StarkNet contract executes correctly according to some specification. Horus is good for when you know what your program should do, but you aren't sure that the implementation actually does that thing, in all cases, no matter what. Horus will not help you if you don't know exactly what your program should do.

You could also use Horus for lightweight things like a sanity check on the bounds of the output of some function, for instance.

Horus has been designed to be easy to use without an extensive background in formal verification. You can start simple and iteratively refine your specifications as you learn how to use the tool better.

Horus, and formal verification in general, proves that the implementation of a program matches the expected behavior, as expressed in some formal specification.

You get the most mileage out of this when the expected behavior is simple, but the implementation is very complex.

Because you love formal verification and care about writing provably correct programs!

Really stupid “smart contract” bug let hackers steal $31 million in digital coin

Alternatively, because you don't want your firm to be in the news.

It uses a modified version of the StarkNet compiler to translate your function specification annotations into SMT solver queries. These are mathematical assertions that the desired properties of the function in question are true for all inputs. Then these queries are run, and the SMT solver magically tells us whether or not it was able to prove that the program is sound!

You can assert things about function parameters, function return values, arbitrary labels/variables in a function body, and storage variables. Here are examples of things you can check about these values:

• Two values are equal (==)
• One value is less/greater than (or equal) to another (e.g. <, <=)
• A storage variable is updated with a particular value
• An invariant holds, e.g. in a loop

Note that arithmetic operations are defined over finite field elements (felts).

You can check these conditions hold at the start and end of a function call with @pre and @post, respectively, and also in the middle of a function body with @invariant and @assert.

The -s/--solver flag is used to tell Horus which SMT solver to use.

Example

horus-check -s cvc5 program.json spec.json

In the above example, we use the solver named cvc5.

Example

horus-check -s mathsat program.json spec.json

In the above example, we use the solver named mathsat.

Horus supports the following solvers:

• cvc5
• mathsat
• z3

MathSAT5 must be installed separately.

You can use the $Return syntax to refer to elements of the return tuple by name. This can only be done in a postcondition, i.e. a @post annotation. The names must be declared in the type signature of the function, after the -> notation. Example:

// @post $Return.a == 1
// @post $Return.b == 2
func f() -> (a: felt, b: felt) {
    return (a=1, b=2);
}

You can use get_caller_address(). Here's an example:

%lang starknet
from starkware.starknet.common.syscalls import get_caller_address

// @post $Return.res == get_caller_address()
func f{syscall_ptr: felt*}() -> (res: felt) {
    let (res) = get_caller_address();
    return (res=res);
}

You can use get_contract_address(). Here's an example:

%lang starknet
from starkware.starknet.common.syscalls import get_contract_address

// @post $Return.res == get_contract_address()
func f{syscall_ptr: felt*}() -> (res: felt) {
    let (res) = get_contract_address();
    return (res=res);
}

You can use get_block_timestamp(). Here's an example:

%lang starknet
from starkware.starknet.common.syscalls import get_block_timestamp

// @post $Return.res == get_block_timestamp()
func f{syscall_ptr: felt*}() -> (res: felt) {
    let (res) = get_block_timestamp();
    return (res=res);
}

Horus prints a judgement for every function it uses to verify your annotations. If an annotated function f calls an unannotated function g (perhaps a library function), the judgement for g may also be printed.

Horus also adds a trivial annotation (equivalent to @pre True and @post True) which is always verifiable to all unannotated functions, and so judgements for these will also be printed.

One common reason this happens is contradictions in the @pre condition. If you have constraints that cannot ever be true, i.e. are impossible, and you ask Horus, "if you assume my @pre conditions, are my @post conditions always true?", what you are asking is really, "if you assume an impossible situation, are my @post conditions always true?"

In first-order logic, anything can be proved, i.e. anything is possible, if you start from an impossible state.

As an example:

// @pre 9 == 10
// @post $Return.a == 1
func f() -> (a: felt) {
  return (a=0);
}

The above program has a postcondition which is obviously False, since we return a literal a=0, and we assert that $Return.a == 1. However, since the @pre condition assumes 9 == 10, which is impossible, we will get Verified, because we are asking Horus to prove that "if 9 == 10, does f return a=1?", and this is indeed true in a vacuous sort of way, because it will never be the case that 9 == 10.

More generally, you may also expect False when you use a @pre condition which is obviously not always satisfied. For example:

// @pre x == 2
// @post $Return.a == 1
func f(x: felt) -> (a: felt) {
  return (a=1);
}

We may expect to get False for the above, since, obviously, x is not always going to be 2, in general. However, Horus will tell us that f has judgement Verified. This is because what Horus checks is that if x == 2, then the function returns a=1. It never checks whether x == 2. It only assumes x == 2 to then check other things.

Instead, we only get a failure when we call f from some other place where Horus is unable to prove that x is always 2. For example:

// @pre x == 2
// @post $Return.a == 1
func f(x: felt) -> (a: felt) {
  return (a=1);
}

// @pre x > 0
func g(x: felt) -> (b: felt) {
  let (b,) = f(x);
  return (b=b);
}

When we run Horus on the above program, we get:

user@computer:~/pkgs/horus-checker$ horus-check -s cvc5 a.json spec.json
f
Verified

g
False

So we see that the False is given for the caller g, and not f, since in order for the call to f to satisfy f's precondition, we must have that x == 2, but all we know is that x > 0, from the precondition of g. So it is easy for Horus to find a counterexample that breaks our specification. In particular, we could pick x == 1.

You may see this error message when you try to reference a variable that is out-of-scope in an annotation.

Consider the following program:

// @pre y == 3
// @post $Return.a == 1
func f(x: felt) -> (a: felt) {
    let y = 4;
    return (a=x + 2);
}

When we compile this, we see:

(horus39) user@computer:~/pkgs/horus-checker$ horus-compile contra.cairo --output a.json --spec_output spec.json
contra.cairo:1:6: Cannot obtain identifier "y". Expected a reference but got "future"
@pre y == 3
     ^

This is because y is a local variable. It is not present in the function's type signature, it is defined within the function body. We see this error because local variables cannot be referenced in preconditions or postconditions.

There are many reasons why an SMT solver may timeout on a query. Unfortunately, satisfiability is a very difficult problem (undecidable in general), and it is nigh impossible to accurately predict how long an arbitrary query will take to solve.

However, besides increasing the timeout passed to the solver with the -t flag, it may also be helpful to try using a different solver backend to resolve Unknown results. It is notable that cvc5 (the default solver) does not perform well with nonlinear arithmetic, and thus it is better to use z3 or mathsat for these cases.

It is also sometimes helpful to rewrite your annotations in a different, but logically equivalent form, as this sometimes has the effect of making the query easier for solver.

Unfortunately, we currently don’t support @assert annotations inside functions that read/write storage variables, so this is one possible reason why you may be having trouble with @assert annotations. If you're still stuck, please open an issue!

Horus does not yet fully support account contracts compiled with the --account_contract CLI flag.

This can sometimes happen when you comment-out a function, but not its annotations (which are themselves already comments). It can also happen when you comment out a decorator, like @external (because then it looks like a Horus annotation: // @external).

Make sure to add another set of /// characters in front of any annotations that were associated with your commented-out function. Suppose we want to comment out an annotated function like this:

// @pre x == 0
// @post 0 == 1
@external
func f(x : felt) -> felt {
    return 0;
}

Instead of:

// @pre x == 0
// @post 0 == 1
// @external
// func f(x : felt) -> felt {
//     return 0;
// }

Try:

/// // @pre x == 0
/// // @post 0 == 1
/// @external
/// func f(x : felt) -> felt {
///     return 0;
}

Horus consists of two command-line tools, horus-compile and horus-check.

horus-compile [-h] [--abi ABI] [--disable_hint_validation]
              [--account_contract] [--spec_output SPEC_OUTPUT]
              [--prime PRIME] [--cairo_path CAIRO_PATH]
              [--preprocess] [--output OUTPUT] [--no_debug_info]
              [--debug_info_with_source]
              [--cairo_dependencies CAIRO_DEPENDENCIES]
              [--no_opt_unused_functions] [-v]
              file [file ...]

A tool to compile checked StarkNet contracts.

Emits a compiled StarkNet contract in the form of JSON, printed to stdout by default.

horus-compile a.cairo --output b.json --spec_output spec.json

Compiles the annotated StarkNet contract a.cairo, and dumps the output into b.json and spec.json for the specifications.

file

One or more StarkNet contracts to compile.

-h, --help

Show a help message and exit

--abi ABI

Dump the contract's ABI (application binary interface) to a file. This is a JSON list containing metadata (like type signatures and members) on functions, structs, and other things within the program.

--disable-hint-validation

Disable the hint validation, which ordinarily checks program hints against a whitelist.

--account-contract

Compile as account contract, which means the ABI will be checked for expected builtin entry points.

--spec_output SPEC_OUTPUT

The specification output file name (default: stdout).

--prime PRIME

The positive integer size of the finite field. This is a (usually large) prime power over which basic arithmetic within the program is carried out.

--cairo_path CAIRO_PATH

A list of directories, separated by ":" to resolve import paths. The full list will consist of directories defined by this argument, followed by the environment variable CAIRO_PATH, the working directory and the standard library path.

--preprocess

Stop after the preprocessor step and output the preprocessed program, which consists only of low-level Cairo (e.g. frame pointer and allocation pointer manipulations) along with annotations indicating relevant source code locations.

--output OUTPUT

The output file name (default: stdout).

--no_debug_info

Don't include debug information in the compiled file. Removes the 'debug_info' field from the JSON output, which by default contains an 'instruction_locations' map with information on flow tracking data, hints, accessible scopes, and source code location.

--cairo_dependencies CAIRO_DEPENDENCIES

Path to dump a list of the Cairo source files used during the compilation as a CMake file.

--no_opt_unused_functions

Disable unused function optimization, which ordinarily only compiles functions reachable from the main scope in the dependency graph, i.e. functions that are actually called.

-v, --version

Show program's version number and exit

horus-check [COMPILED_FILE] [SPECIFICATION] [-v|--verbose] 
            [--output-queries DIR] [--output-optimized-queries DIR] 
            [--version] [(-s|--solver SOLVER)] [-t|--timeout TIMEOUT]

horus-check b.json spec.json

Attempts to verify the compiled StarkNet contract b.json and its specification spec.json with the default SMT solver cvc5, and prints the output to stdout.

COMPILED_FILE

A JSON contract compiled with 'horus-compile'. This can be generated from a '.cairo' file as follows (for an example contract called program.cairo):

horus-compile --output program.json --spec_output spec.json program.cairo

SPECIFICATION A JSON file containing additional information about annotations. This is produced by horus-compile as well.

-v,--verbose

Print all intermediate steps (control flow graph, SMT2 queries, metadata for each module).

--output-queries DIR

Stores the (unoptimized) SMT queries for each module in .smt2 files inside DIR.

--output-optimized-queries DIR

Stores the (optimized) SMT queries for each module in .smt2 files inside DIR.

-s,--solver SOLVER

Solver to check the resulting SMT queries (options: z3, cvc5, mathsat).

Note: If verifying a function f() that calls a function g() whose Horus annotations contain logical variables, the mathsat and cvc5 solvers will fail, and thus z3 must be used.

You can also pass multiple solvers, which will be tried in the order they are passed as flags. In the example below, we run z3 followed by mathsat:

horus-check example.json spec.json -s z3 mathsat cvc5

The timeout will apply to each solver individually, meaning that running two solvers doubles the maximum time the horus-check command will run before terminating.

-t,--timeout TIMEOUT

Time limit (ms) per-SMT query, per-SMT solver.

Horus makes at least one SMT query per function in the program. It may make multiple SMT queries for a single function. And it does this when there are multiple control flow branches in that function.

For example, if you have 2 functions in a contract/program, and both have an if-then-else clause, then we will have 4 branches, and thus 4 SMT queries made. If we run Horus with two separate solvers (say Z3 and cvc5), then we will make a total of 8 queries.

Thus if we set a timeout of 1000ms, the maximum running time of the horus-check invocation is 8000ms or 8s.

-h,--help

Show this help text

To formally verify a program, we must prove that it behaves as expected. In order to do this, we must tell Horus what the expected behavior of the program is. The way that we do this is with the annotation language. Annotations are comments that contain special syntax that Horus can understand. The set of all of a function's annotations is sometimes referred to as its specification or spec. Here's an example:

// @post $Return.res == 3
func example() -> (res: felt) {
	return (3,);
}

The annotation in the example above is the line:

// @post $Return.res == 3

It asserts that the res return value must always be 3.

In order to describe the expected behavior of a function, we need to be able to talk about the function's inputs, outputs, and effects. This means, we need to be able to reference the function's parameters and return values in annotations. Below, we describe the syntax for references, logical variables, boolean expressions, and implications:

• a, $a cairo references and logical variables can be used by name
• $Return.a the special logical variable $Return is defined to contain the values returned from the function
• a+b, a==b, arithmetic operations and comparisons are supported for felts as in Cairo
• a==b or c==d, a==b and c==d, not a==b, a==b -> c==d (disjunctions, conjunctions, negations, and implications)
• True, False are defined as keywords

Specifies conditions that must be true when the function returns. The name post is short for "postcondition".

No claim is made about whether the function completes or reverts. We only assert that if it completes, then the postcondition holds.

Example

// @post $Return.res < 100 && $Return.res >= 50

The annotation above asserts that the return value with name res of the function (not pictured here) is less than 100 and greater than or equal to 50.

Local variables cannot be referenced in postconditions.

Specifies conditions that must be true immediately before a function is called. The name pre is short for "precondition". This annotation type allows us to:

• Place constraints on the values of function parameters
• Assign values to logical variables

Example

// @pre flag * (flag - 1) == 0

The annotation above asserts that the function parameter with name flag satisfies the equation $x(x - 1) = 0$, which implies that $x = 0$ or $x = 1$.

Local variables cannot be referenced in preconditions.

Allows the introduction of logical variables.

A logical variable is a variable defined and used within a function specification (i.e. a set of annotations for a function, i.e. a set of lines starting with // @) for conveniently referring to subexpressions. They play the same role that ordinary variables do in any programming language, but they can only be used within horus annotations.

Logical variable names must begin with a $. Note that if a logical variable is not mentioned in the precondition, then the specification must hold for all possible values of that variable.

Example

// @declare $x : felt
// @pre $x == 5

In the above example, $x is the logical variable being declared, and we assign it a value using a precondition.

Allows claims to be made about the state of a storage variable before and after the function. A storage update must be included for all storage variables modified by a function, or verification will fail.

The first new primitive that we see in the code is @storage_var. Unlike a Cairo program, which is stateless, StarkNet contracts have a state, called “the contract’s storage”. Transactions invoked on such contracts may modify this state, in a way defined by the contract.

The @storage_var decorator declares a variable which will be kept as part of this storage. In our case, this variable consists of a single felt, called balance. To use this variable, we will use the balance.read() and balance.write() functions which are automatically created by the @storage_var decorator. When a contract is deployed, all its storage cells are initialized to zero. In particular, all storage variables are initially zero.

From the Cairo documentation on writing Starknet contracts

Example

// @storage_update x() := x() + 1

In the above example, only the top-level storage variable reference on the left hand side refers to the state after the function. As such, if x took one input and we specified the update as such x(y()) := x(y()) + 1, both instances of y() refer to the state before the function was called.

Note: If you would like to make claims about the relationship between multiple storage variables after the function is complete, this can be achieved via the use of logical variables. To do so, equate your 'before' logical variable to the storage variable in the precondition. Then, also in the precondition, relate the 'after' and 'before' logical variables. Finally assign the 'after' logical variable to the storage variable in a storage update annotation.

Introduces a constraint attached to a label, typically used for loop invariants.

The invariant annotation is only required in the case of low level loops implemented with jump instructions, however it can also be used to make claims that must hold at any specific point in a function by adding an appropriately named label and attaching the annotation to it. Note that this effectively splits the function in two, and that anything from before the invariant that is not mentioned within it cannot be used after.

Example

// @invariant i <= 10
label1:

In the above example, we assert that a local variable i (perhaps a loop variable) is always less than or equal to 10. This invariant assertion is attached to the label named label1.

Introduces a boolean constraint at an arbitrary point in a function body.

You write a boolean expression after @assert, and Horus will try to prove that the expression will always evaluate to True.

Example

// @assert j >= 10

In the above example, we assert that a local variable j is at least 10.

Warning: Assertions constitute a full-stop in the continuity of Horus's reasoning and should be thought of exactly as though a function with unknown allocation pointer change was invoked and its postcondition is the annotation present at @assert. Horus can no longer reason about anything that 'happened' prior to said assertion, whether it is contents of memory or preceding annotations such as the precondition.

It is therefore recommended to avoid @assert, or alternatively, to make sure to propagate all information that one wants to remember for further reasoning.

In other words, use at your own peril, the semantics are complicated. It is not like a typical assert statement in an ordinary programming language.

See also: this relevant bug report.

In a function that updates a storage variable x, it is ambiguous what the name x refers to in an annotation. It could be the initial value, before the update, or the final value, after the update.

Here are the rules for figuring out which value is being referenced:

• If a storage variable is referenced in a precondition (@pre), it is the initial value.
• If a storage variable is referenced in a postcondition (@post), it is the final value.
• Storage variables cannot be referenced in @assert annotations within function bodies.

The purpose of this section is to give a brief high-level overview of the architecture of Horus. Hopefully this can serve as a minimal guide to understanding the source code and contributing to the project.

The entrypoint source file is app/Main.hs. When we run horus-check on a compiled JSON file:

horus-check -s z3 a.json spec.json

the first thing that happens is that we deserialize the JSONs into a value of type ContractDefinition, which is defined in ContractDefinition.hs. This contract is then preprocessed into a richer value of type called ContractInfo, which contains information on the instructions, storage variables, identifiers, etc.

A mutable configuration record and the immutable ContractInfo data are carried around in an Env throughout the program, accessible from within a ReaderT stack.

The implementation makes use of several eDSLs (embedded domain-specific languages), the most important of which is GlobalL, defined in Global.hs. Each DSL is separated into two source files: one containing functions written in the DSL, like Global.hs, and one containing the implementation of the interpreter for the DSL, as well as a runner, like Global/Runner.hs. Each DSL contains a record type defining the 'instructions' that constitute the language, which is named something like GlobalL, where the L suffix stands for "Language".

There is an Impl type defined in the Runner.hs file for each DSL, which is the monad stack in which the interpreter is run. For example, the Impl type for GlobalL looks like this:

type Impl = ReaderT Env (ExceptT Text IO)

The DSLs are written in a continuation-passing style. For example, the constructor GetConfig within the GlobalL DSL looks like this:

data GlobalF a
  ...
  | GetConfig (Config -> a)
  ...

This constructor can be thought of as an "instruction" within the DSL, which, when run by the interpreter, returns a value of type Config. The reason why we see (Config -> a) is because a is the continuation of the "program" within the DSL, i.e. more instructions for the interpreter to process.

The Global DSL, and in particular the solveContract routine within Global.hs, serves as the entrypoint to the rest of the program, and its runner is called from within Main.hs.

Apart from GlobalL, there are several other sub-DSLs, which include:

• CFGBuildL -- builds the control flow graph.
• ModuleL -- constructs a list of Modules from the control flow graph.
• CairoSemanticsL -- constructs the set of memory variables, assertions, etc. for a given module.
• PreprocessorL -- preprocesses and runs SMT queries.

As mentioned above, the purpose of the CairoSemanticsL eDSL is to construct the set of constraints which we will eventually transform into a solver query.

At the time of writing, this is represented in a record type called ConstraintsState, which looks like this:

data ConstraintsState = ConstraintsState
  { cs_memoryVariables :: [MemoryVariable]
  , cs_asserts :: [(AssertionBuilder, AssertionType)]
  , cs_expects :: [(Expr TBool, AssertionType)]
  , cs_nameCounter :: Int
  , cs_callStack :: CallStack
  }

So the asserts and expects are basically boolean expressions, and the preconditions and postconditions are encoded here. We have a list of memory variables as well. A memory variable is defined as follows:

data MemoryVariable = MemoryVariable
  { mv_varName :: Text
  , mv_addrName :: Text
  , mv_addrExpr :: Expr TFelt
  }
  deriving (Show)

We have a variable name, an address name, and an address expression, which is a felt. This is just an association between some variable name and an address in memory, along with its contents.

When we print a memory variable, we see something like this:

MEM!27 : (ap!<112=addr/root>@5 + 35)

The 27 in MEM!27 is just a way to identify distinct memory variables. The ap stands for allocation pointer, and this indicates that this is the address in memory of some felt pushed on to the stack within a function body. The @5 indicates the AP tracking group of this memory variable. The + 35 is the offset, specifically the offset from the beginning of the function context. Thus, an offset of + 0 indicates the first thing pushed onto the memory stack within that context.

Here's an example:

func foo:
  [ap] = 0, ap++;  // <- this will be <foo/root>@x + 0
  [ap] = 42, ap++; // <- this will be <foo/root>@x + 1
  call bar;        // <- ^ now we're fp<bar/foo/root> + 0 and e.g. fp<bar/foo/root< - 3 = <foo/root>@x + 1 (remember call pushes 2 things on the stack)

The stuff in angle brackets, <112=addr/root>, is the current execution context, i.e. the stack frame. Each function call gets its own stack frame. The addr/root part is a representation of the call stack itself, where root is the execution context of top-level functions and subsequent stack frames are prepended, delimited with a /. The 112 is the program counter value, which tells us the instruction at which the current function was invoked.

For example, consider:

func foo [inlinable]             		root
func bar [inlinable]

func baz:
  call bar -- inlining, push bar -> bar/root
    ... (body of bar)
    ret                 pop      -> root
  ...
  call foo -- inlining, push foo -> foo/root
    ... (body of foo)
    ret                 pop      -> root
  ...

The stuff in the right-hand column is the context we're executing within. So when you refer to memory cells that have <foo/root>, you're referring to them from within the inlined function foo.

• contract - a Starknet smart contract.
• control flow - refers to things like if-else blocks, loops, function calls, etc.
• control flow graph - consists of a list of labels, which are our vertices, along with the code between these labels, which is represented as edges between those vertices.
• label - a construct within the Cairo language implementation that identifies instructions which may be jumped-to.
• module - a set of contiguous Cairo instructions between control flow primitives. A function may contain multiple modules. For example, a function with if branching will include a module for when the branching condition is True, and another module for when it is False.
• SMT query - a symbolic proposition which may be passed to an SMT solver, which will attempt to prove it or give a counterexample.

Kindly note, Horus is a tool consisting of two separate components: Horus-Checker, released under the AGPLv3 license, and Horus-Compile, released under the Cairo Toolkit License. When "Horus" is referenced, the reference is to the two components jointly.

Horus is currently in the alpha stage and no guarantee is being given as to the accuracy and/or completeness of any of the outputs the tool may generate. The tool is provided on an 'as is' basis, without warranties or conditions of any kind, either express or implied, including without limitation as to the outputs of the verification process and the security of any system verified using Horus. As per the relevant licenses, to the fullest extent permitted by the law, Nethermind disclaims any liability in connection with your use of Horus and/or any of its outputs.

Please also note that the terminology used by Horus, including but not limited to words such as 'guarantee', should be interpreted strictly within the remit of formal verification terminology. These words are not intended to, and shall not be construed as having legal significance of any kind.

For the avoidance of doubt, the outputs generated by Horus and/or your usage thereof shall not be considered or relied upon as any form of financial, investment, tax, legal, regulatory, or other advice.

Horus-Checker is licensed under AGPLv3 (Copyright (C) 2023 Nethermind). For more information on the dependencies, please see here.

Horus-Compile is licensed under the Cairo Toolkit License (Copyright (C) 2023 Nethermind), pursuant to an exception granted to Nethermind by Starkware Industries Ltd. For more information on the dependencies please see here.