# Compiler & CLI How verified EDSL contracts become deployable EVM bytecode, plus the CLI reference. For the trust boundary, see [Trust Model](/trust-model). ## Pipeline ``` EDSL Contract → CompilationModel → IR → Yul → EVM Bytecode ``` `CompilationModel` is the declarative surface: storage fields, function bodies, constructor params, events. The compiler infers slots, looks up selectors, lowers expressions/statements to IR, generates Yul, and hands off to `solc` for the final bytecode step. > Verity has two **distinct** "spec" concepts: > 1. **Logical specs** in `Contracts//Spec.lean`, `Prop` statements used for proofs. > 2. **Compiler specs** in `Compiler/Specs.lean`, `CompilationModel` values used for code generation. ### Modules | Module | Role | |--------|------| | `Compiler/CompilationModel.lean` | Declarative DSL: expressions, statements, constructors, storage inference. | | `Compiler/Specs.lean` | The validated contract specs, registered via `allSpecs`. | | `Compiler/Selector.lean` | Canonical selector computation; kernel-checkable `keccak256_first_4_bytes`; CI cross-check against `solc --hashes`. | | `Compiler/Codegen.lean` | IR → Yul: dispatcher, mapping-slot helper, deploy/runtime split. | | `Compiler/Linker.lean` | External Yul library linking with reference validation. | | `Compiler/Yul/*` | Yul AST and pretty printer. | ## Compile all contracts ```bash cd /path/to/verity export PATH="$HOME/.elan/bin:$PATH" lake build verity-compiler lake exe verity-compiler # writes artifacts/yul/*.yul ``` For contracts that use external libraries (e.g. Poseidon): ```bash lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yul/ ``` See the [Linking External Libraries](/guides/linking-libraries) guide. ## Audit artifacts The CLI emits machine-readable audit artifacts alongside Yul/ABI: - `--trust-report `, proof-boundary and assumption data. - `--assumption-report `, flattened assumption inventory grouped by contract and usage site. Direct assembly-shaped primitives without any `local_obligations [...]` fail closed. - `--layout-report `, resolved storage-slot metadata, alias writes, reserved-slot policy. - `--layout-compat-report `, baseline vs candidate layout compatibility for upgrade reviews. Pair with `--deny-layout-incompatibility` to fail closed on incompatible upgrades. For proof-strict builds, deny flags lock down the trust surface. Each one fails the build closed when the corresponding category of assumption appears: | Flag | Fails closed on | |------|-----------------| | `--deny-unchecked-dependencies` | Module dependencies that haven't been checked | | `--deny-assumed-dependencies` | Dependencies marked as assumed rather than verified | | `--deny-axiomatized-primitives` | Primitives still treated as axioms (e.g., raw `keccak256`) | | `--deny-local-obligations` | Any undischarged `local_obligations [...]` | | `--deny-linear-memory-mechanics` | `mload` / `mstore` / `calldatacopy` / `returndatacopy` use | | `--deny-event-emission` | `rawLog` and not-yet-modeled event emission | | `--deny-low-level-mechanics` | Raw `call` / `staticcall` / `delegatecall` constructs | | `--deny-runtime-introspection` | Runtime calldata/returndata size and memory introspection | | `--deny-proxy-upgradeability` | `delegatecall` and proxy upgrade patterns | | `--deny-layout-incompatibility` | Candidate storage layout breaks baseline (paired with `--layout-compat-report`) | | `--deny-unsafe` | Catch-all: any of the above categories trips the build | See [Glossary](/glossary) for one-line definitions of each report. ## Example: SimpleStorage **EDSL** (`Contracts/SimpleStorage/SimpleStorage.lean`): ```verity def storedData : StorageSlot Uint256 := ⟨0⟩ def store (value : Uint256) : Contract Unit := do setStorage storedData value def retrieve : Contract Uint256 := do getStorage storedData ``` **CompilationModel** (`Compiler/Specs.lean`): ```verity def simpleStorageSpec : CompilationModel := { name := "SimpleStorage" fields := [{ name := "storedData", ty := FieldType.uint256 }] functions := [ { name := "store" params := [{ name := "value", ty := ParamType.uint256 }] returnType := none body := [ Stmt.setStorage "storedData" (Expr.param "value"), Stmt.stop ] }, { name := "retrieve" params := [] returnType := some FieldType.uint256 body := [Stmt.return (Expr.storage "storedData")] } ] } ``` **Generated Yul** (`artifacts/yul/SimpleStorage.yul`): ```yul object "SimpleStorage" { code { datacopy(0, dataoffset("runtime"), datasize("runtime")) return(0, datasize("runtime")) } object "runtime" { code { switch shr(224, calldataload(0)) case 0x6057361d { let value := calldataload(4); sstore(0, value); stop() } case 0x2e64cec1 { mstore(0, sload(0)); return(0, 32) } default { revert(0, 0) } } } } ``` ## CompilationModel surface **Storage inference**: slots assigned in field order; no manual slot management. ```verity fields := [ { name := "owner", ty := FieldType.address }, -- slot 0 { name := "balances", ty := FieldType.mappingTyped (.simple .address) }, -- slot 1 { name := "totalSupply", ty := FieldType.uint256 } -- slot 2 ] ``` **Constructor parameters**: loaded from end of deployment bytecode (Solidity convention). ```verity constructor := some { params := [{ name := "initialOwner", ty := ParamType.address }] body := [Stmt.setStorage "owner" (Expr.constructorArg 0)] } ``` **Expressions** cover literals, parameters, storage and mapping reads, EVM context (`caller`, `chainid`, `msgValue`, `blockTimestamp`, `blockNumber`, `blobbasefee`), memory primitives (`mload`, `keccak256`), low-level calls (`call`, `staticcall`, `delegatecall`), arithmetic, bitwise, comparisons, logical operators. > **Low-level call boundary**: the three call forms compile, but their runtime semantics are still outside the current proof-interpreter model. The call success / returndata mechanics remain validated by differential testing and tracked under issue `#1332`. `delegatecall` also remains a separate proxy / upgradeability trust boundary; archive `--trust-report` and add `--deny-proxy-upgradeability` if those semantics must stay outside the selected verification envelope (see issue `#1420`). > > **Linear-memory boundary**: Memory-oriented intrinsics (`mload`, `mstore`, `calldatacopy`, `returndataCopy`, `returndataOptionalBoolAt`) compile, but the current proof interpreters still model them only partially. When they appear, surface that boundary with `--trust-report` / `--deny-linear-memory-mechanics`; the remaining gap is tracked under issue `#1411`. > > **Axiomatized-primitive boundary**: The `keccak256` intrinsic also compiles, but it remains axiomatized in the current proof stack rather than fully modeled end to end. When it appears, archive `--trust-report` and add `--deny-axiomatized-primitives` if the selected contracts must stay inside the proved subset (see issue `#1411`). **Statements** cover local variables, storage and mapping writes, `require`, `return`, memory writes, returndata copy and revert bubbling, `stop`, `ite` branching, bounded `forEach` loops, event emission, and internal calls. Low-level calls, linear-memory primitives, `rawLog`, and `keccak256` compile but remain partially modeled in the proof interpreter. Functions or constructors that use direct assembly-shaped primitives without `localObligations [...]` fail closed under `--deny-axiomatized-primitives`. **Internal functions** via `isInternal := true` and `Stmt.internalCall`; **events** via the `events` block and `Stmt.emit` (topic0 computed from the event signature); **double mappings** via `mapping2`/`setMapping2`; **uint256-keyed mappings**; **dynamic, fixed-size, and bytes array parameters** with ABI offset-based decoding. For Morpho-style `mapping(K => Struct)` / `mapping(K1 => mapping(K2 => Struct))` layouts, declare `FieldType.mappingStruct` / `FieldType.mappingStruct2` and access members with `structMember "f" key "member"`, `structMember2 "f" k1 k2 "member"`, `setStructMember "f" key "member" val`, `setStructMember2 "f" k1 k2 "member" val`. Member offsets and packed sub-word widths are part of the declaration, so the generated Yul keeps Solidity's storage layout reviewable. ## Add a new contract 1. Declare it with `verity_contract` in `Contracts//.lean`: ```verity verity_contract MyContract where storage value : Uint256 := slot 0 function setValue (x : Uint256) : Unit := do setStorage value x function getValue () : Uint256 := do return (← getStorage value) ``` Stateless contracts may leave the `storage` block empty. 2. Register it in `Compiler/Specs.lean` under `allSpecs`: ```lean Contracts.MyContract.spec ``` 3. Recompile: ```bash lake build verity-compiler lake exe verity-compiler ``` Handwritten `Compiler.Specs.*Spec` definitions are retained for migration only; they are not the canonical compile path. For the full authoring checklist (specs, invariants, proofs, tests), see [First Contract](/first-contract). ## Test compiled contracts ```bash FOUNDRY_PROFILE=difftest forge test # FFI enables Yul compilation lake build # verifies all Lean proofs ``` ## Validated contracts | Contract | What it shows | |----------|---------------| | SimpleStorage | Basic storage operations | | Counter | Arithmetic | | Owned | Access control with constructor args | | OwnedCounter | Pattern composition | | Ledger | Mapping balances | | SimpleToken | ERC20-like token with constructor | | SafeCounter | Checked arithmetic with underflow protection | Not compiled: `ReentrancyExample` (inline proofs only). `CryptoHash` compiles via `--link` with external Poseidon and is validated in CI. ## Trust boundary Three verified layers, EDSL ↔ CompilationModel, CompilationModel ↔ IR, IR ↔ Yul. The `solc` Yul-to-bytecode step and the EVM execution model itself are trusted, not verified. See [Trust Model](/trust-model). **Layer 2 boundary today**: the generic whole-contract `CompilationModel -> IR` theorem is proved for the current explicit supported fragment. The former exact-state body-simulation axiom has been eliminated; the remaining dispatcher bridge is an explicit theorem hypothesis rather than a Lean axiom, so legacy contract-specific bridge theorems are wrappers above the generic theorem rather than independent assumptions. ## See also - [Trust Model](/trust-model), what the audit artifacts bound. - [Verification Status](/verification), theorem inventory. - [Examples](/examples), the validated contract set with code excerpts. - [Linking External Libraries](/guides/linking-libraries).