Codegen Mapping
How Cambrian constructs lower on the public targets.
Solidity-EVM (--target evm)
| Cambrian | Solidity |
|---|---|
entity E | Contract E (flat file, pragma solidity ^0.8.24) |
| members | Storage variables (+ transforms inlined into route bodies) |
| routes | External / public functions |
private routes / call r(...) | internal function _r, called directly (msg.sender stays the original caller) |
view routes | view functions |
msg::sender / msg::value | msg.sender / msg.value (payable when value is read) |
~> dest typed send | External call |
deploy E(...) / E.address(...) | CREATE2 through the generated CambrianFactory (deployE / predictE) |
init route | Deploy-time constructor stub + factory-only initialize(...) |
event / emit | Solidity event / emit |
error / throw Name | Custom errors / revert |
test / property / invariant | Foundry tests / fuzz / invariant handlers |
On EVM every entity is deployed via CREATE2 by the generated
CambrianFactory; there is no plain new E(...) path.
An identifier that collides with a Solidity keyword or built-in (now,
bytes, type, mapping, …) gets a leading underscore in the generated
Solidity (now → _now); the Cambrian source keeps the natural name.
Types
| Cambrian | Solidity |
|---|---|
u8 … u128, U256 | uint8 … uint128, uint256 |
i8 … i128 | int8 … int128 |
bool, address | bool, address |
Address<E> | address |
String, bytes | string, bytes |
bytes32, pubkey | bytes32 |
Vec<T> | T[] |
HashMap<K, V> | mapping(K => V) |
Option<T> | Generated struct Option_<T> (tag + value) |
record R | struct R |
enum E | enum E; a payload-bearing enum becomes a tagged-union struct (E08) |
Output layout
<out>/
src/<E>.sol # one per entity
src/_<name>_project.sol # combined file (entities + CambrianFactory)
test/<E>.t.sol # tests and property test/fuzz instances
test/Invariant_<E>_<name>.t.sol # one per invariant
foundry.toml
setup.sh # installs forge-std
.cambrian-manifest.json # hashes of the generated files
In project mode <name> is the project name and each src/<E>.sol is a
stub that imports the combined file. In single-file mode the combined file
is src/_Harness_project.sol. A single-file build without tests,
properties or invariants writes only src/<E>.sol (with all entities and
the factory) and the manifest — no Foundry harness. A multi-entity
invariant is written to test/Invariant_<name>.t.sol.
Build and test with bash setup.sh && forge test.
Lean-EVM (--target lean)
| Cambrian | Lean |
|---|---|
| entity state | structure State (plus ghost key lists for iterated maps when needed) and structure Identity |
| numeric types | BitVec n under the default lean.numerics: overflow-wrap (Nat under nat) |
| routes | E.Routes.<route> (w : World) (inst : E.Identity) (ctx : MsgCtx) … returning World, or World × T with -> T |
failing routes (where / throw / failing calls) | Result wrapped in Cambrian.RouteResult α := Except ThrowCode α |
| sends / deploys | World updates (call, occupancy, balances) |
property / test | Theorems in <E>Spec.lean |
invariant | Action / step / runTrace definitions + checks |
Output layout
<out>/
lakefile.toml
lean-toolchain # lean.lean_toolchain (default leanprover/lean4:v4.29.1)
Cambrian.lean # library root, imports everything
Cambrian/{Core,Evm,Prelude,SimpAttrs}.lean # vendored runtime
Cambrian/Generated/<E>.lean # State, Identity, member transforms
Cambrian/Generated/<E>Routes.lean # route functions over World
Cambrian/Generated/World.lean # shared world / storage
Cambrian/Generated/<E>Spec.lean # only when there are tests / properties / invariants
Cambrian/Generated/Pure.lean # only with top-level pure fns / records / enums
Cambrian/Generated/Extern.lean # only with extern entities (opaque route axioms)
Cambrian/Generated/Dispatch.lean # only with sends to address-typed destinations
Build with lake build (or pass --check-lean).