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! -
horus-compile
and
horus-check
executables setup for your development environment.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.
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.
Download and install
miniconda
on your
system:
In each case, run the downloaded script/executable, and follow the instructions.
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.
Activate the created environment:
conda activate horus-py39
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
aarch64
):# 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.
horus-compile
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 .
horus-checker
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 yourPATH
or pass a different install directory withstack 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:
my-cairo-project/
on your filesystem to the location
/home/
on the container's filesystemsudo docker run -v $(pwd)/my-cairo-project/:/home/ -it horus:latest /bin/bash
horus-compile
and horus-check
installation.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
.
Stack
Let's define a struct
called Stack
with two members:
value
which has type felt
,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.
Stack
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,);
}
Stack
-related functionsWe 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.
main()
functionGreat! 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:
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.lit
function puts i
on the top of the stack, and preserves the old
stack underneath it.top
function actually returns the top of the stack we pass as an
argument.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:
//
is just the syntax for comments.@post
declares a Horus postcondition annotation. This condition must
hold at the end of each function call.$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.+
in annotations for
supported datatypes. See the section on spec syntax for more
info on what operators and symbols are supported.@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:
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:
==
)<
, <=
)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.
Verified
when I expect False
?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
.
Cannot obtain identifier "y". Expected a reference but got "future"
?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.
Unknown
?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.
@assert
annotations work in my function?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.
Unexpected annotation type
or annotation is not allowed here
in my commented-out code?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
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
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 functiong()
whose Horus annotations contain logical variables, themathsat
andcvc5
solvers will fail, and thusz3
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 functiona+b
, a==b
, arithmetic operations and comparisons are supported for felts as in Cairoa==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@post
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.
@pre
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:
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.
@declare
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.
@storage_update
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 thebalance.read()
andbalance.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 suchx(y()) := x(y()) + 1
, both instances ofy()
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.
@invariant
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 namedlabel1
.
@assert
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:
@pre
), it is the initial value.@post
), it is the final value.@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 Module
s from the control flow graph.CairoSemanticsL
-- constructs the set of memory variables, assertions, etc.
for a given module.PreprocessorL
-- preprocesses and runs SMT queries.CairoSemanticsL
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
.
if-else
blocks, loops, function
calls, etc.if
branching will include a module for when the branching condition is
True
, and another module for when it is False
.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.