Skip to content
LogoLogo

Installation and first contract

Build the compiler

Lithe is written in Rust. Build it from the repository root with a recent stable toolchain:

cargo build --release

The compiler is now at target/release/lithe. Put it on your PATH, or call it by path:

export PATH="$PWD/target/release:$PATH"
lithe

Run with no arguments, lithe prints its commands. See Command line for the full list.

To prove contracts' specs with lithe prove, also install the Z3 solver, which it runs:

brew install z3        # macOS
sudo apt install z3    # Debian and Ubuntu

Or download a release from github.com/Z3Prover/z3/releases and put z3 on your PATH, or set LITHE_Z3 to its path. Nothing else needs Z3.

Write a contract

A Lithe file is a contract. Create counter.lithe:

counter.lithe
(* Comments are written like this, and they nest. *)
 
storage is record {
  count : uint;
}
 
external view function get() : uint is
  storage.count
 
external function inc() is {
  storage.count := storage.count + 1;
}
 
external function dec() is {
  storage.count := storage.count - 1;
}

A few things to notice:

  • storage is record declares the contract's persistent state. Every contract has one, and every access is qualified as storage.count.
  • uint is an unsigned 256-bit integer. 1 is a uint literal. Arithmetic is checked, so dec on zero reverts with Panic(0x11), the same panic Solidity uses.
  • external puts a function in the ABI. external view promises the function never writes, and the compiler checks the promise.
  • := assigns. = compares.
  • A function body is a block { ... } or a single expression.

Compile

lithe compile counter.lithe

This prints the contract's creation bytecode as hex. Generate its ABI with:

lithe abi counter.lithe

To build every .lithe file in a directory into Foundry-style artifacts under ./out, pass the directory:

lithe compile src

Deploy and call

The output of lithe compile is creation code, so any deployment tool can use it. With Foundry and a local anvil:

anvil &
 
KEY=0xac0974bec39a17e36ba4a6b4d238ff944bacb478cbed5efcae784d7bf4f2ff80
cast send --private-key $KEY --create $(lithe compile counter.lithe)
# contractAddress 0x5FbDB2315678afecb367f032d93F642f64180aa3
 
cast send --private-key $KEY 0x5FbDB2315678afecb367f032d93F642f64180aa3 "inc()"
cast call 0x5FbDB2315678afecb367f032d93F642f64180aa3 "get()(uint256)"
# 1

Calling dec() twice from here reverts with panic: arithmetic underflow or overflow (0x11).

See what the compiler knows

Because effects are explicit, the compiler can summarize each entrypoint:

lithe footprint counter.lithe
inc   writes: count            during defers: callable
dec   writes: count            during defers: callable
get   reads: count             during defers: callable

Inspecting contracts covers footprint, abi-tree, analysis, errors, and storage.

Next steps