Inspecting contracts

Lithe makes every effect explicit, so the compiler knows what each entrypoint can do, and it will tell you. Use these summaries in code review, in audits, in CI checks that an entrypoint's effects have not changed, and as structured input for AI review tools.

The examples on this page use this contract:

bank.lithe

import "std/evm";
 
error NotOwner;
error Paused;
 
error InsufficientBalance of record {
  available : uint;
  required : uint;
}
 
error InvalidAmount of uint;
 
errors withdrawalErrors is
  | Paused
  | InvalidAmount
  | InsufficientBalance
 
storage is record {
  owner : address;
  paused : bool;
  balance : uint;
}
 
event Withdrawal of record {
  account : address;
  amount : uint;
}
 
view function requireOwner()
  raises NotOwner
is {
  assert(Evm.sender() = storage.owner, NotOwner);
}
 
view function requireAmount(const amount : uint) : uint
  raises InvalidAmount
is {
  assert(amount <> 0, InvalidAmount(amount));
} with amount
 
external function withdraw(const amount : uint)
  raises withdrawalErrors
is {
  assert(not storage.paused, Paused);
 
  const taken : uint := requireAmount(amount);
 
  assert(
    storage.balance >= taken,
    InsufficientBalance {
      available = storage.balance;
      required = taken;
    }
  );
 
  storage.balance := storage.balance - taken;
 
  emit Withdrawal {
    account = Evm.sender();
    amount = taken;
  };
}
 
external function setPause(const value : bool)
  raises NotOwner
is {
  requireOwner();
  storage.paused := value;
}

`footprint`

One line per entrypoint:

lithe footprint bank.lithe

withdraw    writes: balance   emits: Withdrawal      raises: Paused, InvalidAmount, InsufficientBalance   during defers: callable
setPause   writes: paused                           raises: NotOwner                                     during defers: callable

during defers says whether the entrypoint can run while another transition's deferred calls are running: callable, or rejected for a nonreentrant function. See Reentrancy.

An entrypoint of a guarded module external shows its guard, such as guard: Prices.pricer, which abi-tree lists under guards, and errors lists each guard with the errors it raises.

When the contract has facets, each line ends with where the entrypoint runs: the facet of a module, such as runs in: ERC20, or runs in: router. abi-tree shows the same as a runs in: section.

`abi-tree`

The full picture of each entrypoint, including functions it calls, and guards inherited through dispatch:

lithe abi-tree counter.lithe

reset
  path:
    main -> ownerMain -> reset

  calls:
    none

  guards:
    - Evm.sender() = storage.owner

  storage reads:
    - storage.owner
    - storage.count

  storage writes:
    - storage.count

  queries:
    none

  events:
    - CountChanged

  operations:
    none

  raises:
    - InvalidOwnerAccess()

`analysis`

The same facts as JSON:

lithe analysis bank.lithe

[
  {
    "name": "withdraw",
    "effect": "stateful",
    "payable": false,
    "nonreentrant": false,
    "reads": [{ "space": "storage", "path": "paused" }, { "space": "storage", "path": "balance" }],
    "writes": [{ "space": "storage", "path": "balance" }],
    "emits": ["Withdrawal"],
    "defers": [],
    "raises": ["Paused", "InvalidAmount", "InsufficientBalance"]
  },
  ...
]

space is storage or transient. path names the domain for named storage (config.fee, Ownable.ownable.owner), and goes down through map entries to record fields (orders.status).

`errors`

Every entrypoint's errors, then every error's selector, fields, and raisers:

lithe errors bank.lithe

withdraw(uint256)

  Paused()
  InvalidAmount(uint256)
  InsufficientBalance(uint256,uint256)

setPause(bool)

  NotOwner()

...

InsufficientBalance(uint256,uint256)

selector:
  0xcf479181

fields:
  available : uint256
  required : uint256

raised by:
  withdraw(uint256)

`storage`

Slot-by-slot layout, including named-domain roots and transient slots:

lithe storage bank.lithe

storage
  root: 0x0000000000000000000000000000000000000000000000000000000000000000
  owner: address    slot 0, offset 0, 20 bytes
  paused: bool      slot 0, offset 20, 1 byte
  balance: uint256  slot 1

The layout matches the equivalent Solidity contract, so cast storage and other slot-level tools work unchanged.