# Trust Model What you trust when you trust a Verity contract: the Lean kernel, the Yul compiler, the deployment toolchain, the EVM specification itself, and the short list of axioms documented in `AXIOMS.md`. Everything else, the EDSL semantics, the `CompilationModel → IR` transformation, the `IR → Yul` preservation, and the per-contract specifications, is machine-checked. ## The three layers Correctness is organized into three nested boundaries. Each layer states what is verified and what is explicitly *not* yet. ### Layer 1, spec ↔ EDSL The frontend bridge. An EDSL implementation written in `Contracts//` is proven equivalent to its `CompilationModel`, and per-contract proofs in `Contracts//Proofs/` show that the EDSL satisfies a human-readable `Spec.lean`. **What's verified:** functional behavior of every supported primitive, success/revert paths via `ContractResult`, storage isolation and context preservation. **What's not:** the spec itself is a human artifact , Layer 1 cannot tell you that the spec is the *right* specification for your business problem. ### Layer 2, EDSL ↔ IR / CompilationModel The compiler middle. The generic whole-contract theorem in `Compiler/Proofs/IRGeneration/Contract.lean` proves that `CompilationModel.compile` produces IR with matching semantics for the current supported fragment. The former exact-state body-simulation axiom has been eliminated; legacy contract-specific bridge theorems now sit above the generic compiler theorem as wrappers. **What's verified:** every statement and expression constructor in the supported fragment lowers to semantically equivalent IR. **What's not:** features marked as "not modeled" in the trust report, including parts of low-level call mechanics, linear-memory primitives (`mload`/`mstore`/`calldatacopy`/`returndatacopy`), raw `rawLog` event emission, and `keccak256` (still axiomatized end-to-end). Each carries a `--deny-*` flag for proof-strict builds. ### Layer 3, IR ↔ Yul / EVM The backend. `IR → Yul` preservation is proved in `Compiler/Proofs/YulGeneration/`, with the remaining dispatcher bridge exposed as an explicit theorem hypothesis rather than a Lean axiom. **What's verified:** the Yul AST emitted for each IR program has matching semantics under the in-Lean Yul interpreter. **What's not:** the final `Yul → bytecode` step performed by `solc`, and the EVM's own runtime semantics, which sit outside the proof envelope. ## Axioms and assumptions [`AXIOMS.md`](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md) is the authoritative registry of Lean axioms in the proof tree. Today it lists **zero active project-level axioms**: the last residual axiom (`solidityMappingSlot_lt_evmModulus`) was eliminated when the FFI-based `keccak256` call was replaced by the kernel-computable `KeccakEngine.keccak256` whose output length is proved by `squeeze256_size`. What remains outside the proof envelope is **assumptions**, not axioms: - **Externally Callable Modules (ECMs)** in `Compiler/Modules/*.lean` carry named assumptions like `erc20_balanceOf_interface`, `evm_ecrecover_precompile`, `keccak256_memory_slice_matches_evm`. These are trust-report metadata, not Lean axioms, they document that the call mechanics depend on the EVM behaving as specified. - **`local_obligations`** declared on a constructor or function carry a named refinement obligation at that exact usage site. - **Not-modeled features** (parts of low-level call mechanics, linear-memory primitives, raw `rawLog`, dynamic `keccak256` over memory) compile but the proof interpreter does not yet model their full semantics. The compiler exports the per-build view of all of this: `--assumption-report ` writes the flat inventory of every assumption that any selected contract depends on, grouped by contract and usage site. Pair it with `--trust-report` for the structured proof-boundary view, and add the matching `--deny-*` flag (`--deny-axiomatized-primitives`, `--deny-event-emission`, `--deny-linear-memory-mechanics`, `--deny-proxy-upgradeability`, `--deny-local-obligations`, `--deny-layout-incompatibility`) when a build must fail closed. ## What is trusted - **The Lean 4 kernel.** Every proof in Verity is reduced to kernel-checked terms. - **The Yul compiler (`solc`).** Verity proves correctness down to Yul; the Yul-to-bytecode step is delegated to `solc --strict-assembly`. - **The EVM specification.** The Yul and IR interpreters in Lean model the EVM as defined by the Yellow Paper and the post-merge spec. - **The deployment toolchain.** `forge`, `cast`, RPC providers, and any other artifact handling sit outside the proof boundary. - **Pre-computed function selectors.** Selectors are derived from `keccak256` of canonical signatures; CI cross-checks against `solc --hashes`. - **The ECM and `local_obligation` assumptions surfaced in `--trust-report`.** Not Lean axioms, but trust-report metadata that documents where the proof depends on external EVM behavior (e.g., `erc20_balanceOf_interface`, `evm_ecrecover_precompile`, `keccak256_memory_slice_matches_evm`). ## What is verified - **EDSL semantics.** `Verity/Core.lean` primitives have full-result `@[simp]` lemmas and complete coverage in proofs. - **The `CompilationModel → IR` transformation.** Proved generically for the supported fragment. - **The `IR → Yul` preservation.** Proved with the dispatcher bridge stated as an explicit hypothesis rather than an axiom. - **Contract-specific specifications.** Each `Contracts//Proofs/` tree proves the implementation satisfies its `Spec.lean`. - **Contract-specific invariants.** Conservation, isolation, and well-formedness lemmas for the contracts that need them (Ledger, SimpleToken, OwnedCounter). ## See also - [Verification](/verification), live theorem and proof-status inventory. - [Proof Techniques](/proof-techniques), how proofs are structured, and what is currently out of scope.