diff --git a/docs-site/README.md b/docs-site/README.md index c854db24a..f2b813903 100644 --- a/docs-site/README.md +++ b/docs-site/README.md @@ -37,22 +37,23 @@ npm start ``` docs-site/ -├── app/ -│ └── api/ -│ └── docs/[...slug]/route.ts # API for serving markdown -├── content/ # Documentation pages (MDX) +├── app/api/docs/[...slug]/route.ts # API for serving markdown +├── content/ # Documentation pages (MDX) │ ├── index.mdx # Homepage -│ ├── research.mdx # Research log -│ ├── iterations.mdx # Iteration summaries │ ├── examples.mdx # Example contracts │ ├── core.mdx # Core architecture │ └── _meta.js # Navigation config -├── public/ -│ └── llms.txt # AI agent index +├── public/llms.txt # AI agent index ├── proxy.ts # Middleware for AI agent detection └── next.config.mjs # Next.js config with Nextra ``` +## Verity syntax highlighting + +`verity` code fences use a Verity-specific TextMate grammar and the LFGLabs Cream theme. Contract structure is visually explicit (`verity_contract`, section headers, `linked_externals`, typed `external` declarations, `modifier`, `function`), Solidity-like control surfaces are highlighted by semantic role (`with onlyRelayer`, `nonreentrant(...)`, `forEach`, `requireError`, `tryExternalCall`, `abiEncode`, `emit`), and domain-level signals (field access, typed external returns, event names, custom errors) receive dedicated scopes. + +The scope contract is checked by `npm run check:highlighting`. Snippets that show contract DSL code must use the `verity` fence, not generic `lean`. + ## AI Agent Support The site automatically serves markdown to AI agents through: diff --git a/docs-site/app/api/docs/[...slug]/route.ts b/docs-site/app/api/docs/[...slug]/route.ts index fbd9881d2..e21f0460a 100644 --- a/docs-site/app/api/docs/[...slug]/route.ts +++ b/docs-site/app/api/docs/[...slug]/route.ts @@ -69,7 +69,7 @@ async function listDocs(dir: string = CONTENT_DIR, prefix: string = ""): Promise * * Examples: * - /api/docs/index.md → Raw markdown for homepage - * - /api/docs/research → Raw markdown (extension optional) + * - /api/docs/compiler → Raw markdown (extension optional) */ export async function GET( request: NextRequest, diff --git a/docs-site/app/sitemap.ts b/docs-site/app/sitemap.ts index 9e0c37bb8..59c0289c7 100644 --- a/docs-site/app/sitemap.ts +++ b/docs-site/app/sitemap.ts @@ -2,21 +2,28 @@ import type { MetadataRoute } from 'next' const ROUTES = [ '', + // Introduction + '/architecture', + '/trust-model', + // Tutorials '/getting-started', + '/first-contract', + // How-To Guides + '/guides/add-contract', + '/guides/solidity-to-verity', + '/guides/production-solidity-patterns', + '/guides/linking-libraries', + '/guides/debugging-proofs', + // Reference '/examples', '/core', - '/add-contract', + '/edsl-api-reference', '/compiler', '/verification', - '/edsl-api-reference', - '/research', - '/research/iterations', - '/guides/first-contract', - '/guides/solidity-to-verity', - '/guides/production-solidity-patterns', - '/guides/debugging-proofs', - '/guides/linking-libraries', - '/guides/verity-syntax-highlighting', + '/glossary', + // Explanation + '/proof-techniques', + '/faq', ] export default function sitemap(): MetadataRoute.Sitemap { diff --git a/docs-site/components/VerityHero.tsx b/docs-site/components/VerityHero.tsx index fa34ef8f4..bbb440944 100644 --- a/docs-site/components/VerityHero.tsx +++ b/docs-site/components/VerityHero.tsx @@ -1,4 +1,4 @@ -const primaryLink = { href: '/guides/first-contract', label: 'Start with a contract' } +const primaryLink = { href: '/first-contract', label: 'Start with a contract' } const paperLink = { href: 'https://lfglabs.dev/papers/verity.pdf', @@ -8,7 +8,7 @@ const paperLink = { const secondaryLinks = [ { href: '/compiler', label: 'Compiler model' }, { href: '/verification', label: 'Verification status' }, - { href: '/research', label: 'Research notes' }, + { href: '/faq', label: 'FAQ' }, ] const facts = [ diff --git a/docs-site/content/_meta.js b/docs-site/content/_meta.js index d00ef5eb5..fbbefaca8 100644 --- a/docs-site/content/_meta.js +++ b/docs-site/content/_meta.js @@ -1,12 +1,26 @@ export default { index: 'Home', + + '-- introduction': { type: 'separator', title: 'Introduction' }, + architecture: 'Architecture Overview', + 'trust-model': 'Trust Model', + + '-- tutorials': { type: 'separator', title: 'Tutorials' }, 'getting-started': 'Getting Started', - examples: 'Example Contracts', - core: 'Core Architecture', - 'edsl-api-reference': 'EDSL API Reference', + 'first-contract': 'Your First Contract', + + '-- howto': { type: 'separator', title: 'How-To Guides' }, guides: 'Guides', - 'add-contract': 'Add a Contract', - compiler: 'Compiler', - verification: 'Formal Verification', - research: 'Research', + + '-- reference': { type: 'separator', title: 'Reference' }, + examples: 'Examples Gallery', + core: 'Core', + 'edsl-api-reference': 'EDSL API', + compiler: 'Compiler & CLI', + verification: 'Verification Status', + glossary: 'Glossary', + + '-- explanation': { type: 'separator', title: 'Explanation' }, + 'proof-techniques': 'Proof Techniques', + faq: 'FAQ', }; diff --git a/docs-site/content/architecture.mdx b/docs-site/content/architecture.mdx new file mode 100644 index 000000000..701ff9e8b --- /dev/null +++ b/docs-site/content/architecture.mdx @@ -0,0 +1,90 @@ +--- +title: Architecture Overview +description: A single-page map of the Verity system, from EDSL source down to EVM bytecode. +--- + +# Architecture Overview + +Verity is a Lean-4 embedded DSL for writing smart contracts that compile to EVM +bytecode and come with machine-checked correctness proofs. Each layer of the +system has a specific responsibility: the **EDSL** is where humans write +contracts and theorems; the **CompilationModel** is the declarative typed +specification the compiler consumes; the **IR** is the intermediate form the +proofs target; **Yul** is the textual EVM dialect emitted to disk; and the +deployable **EVM** bytecode is produced by `solc` from Yul. Every transition is +either proved in Lean or recorded as an explicit assumption in the trust report. + +## Pipeline + +``` +EDSL --> CompilationModel --> IR --> Yul --> EVM +``` + +**EDSL.** The source layer. Contracts are written using `verity_contract` (or +the lower-level `Contract` monad) against `Verity/Core.lean`. Specs, invariants, +and proofs live next to the implementation in `Contracts//`. Read by the +human author; consumed by the elaborator to build a `CompilationModel`. Layer 1 +proves the EDSL implementation refines its `CompilationModel`. + +**CompilationModel.** The declarative typed-IR layer (`Compiler/CompilationModel.lean`). +A `CompilationModel` carries fields, events, errors, the constructor, function +bodies as `Expr`/`Stmt`, externals, and local obligations. Written by the +compiler (or by hand for legacy specs); read by the IR generator. Layer 2 +proves that the IR generated from any `CompilationModel` in the supported +fragment preserves its semantics. + +**IR.** The typed intermediate representation that sits between +`CompilationModel` and Yul (`Compiler/Proofs/IRGeneration/`). Generated +automatically; read by the Yul code generator and by the Layer 2 / Layer 3 +proofs. The end-to-end correctness theorem is stated at this level. + +**Yul.** The textual EVM dialect emitted by `Compiler/Codegen.lean` and the Yul +pretty-printer in `Compiler/Yul/*.lean`. Written to `artifacts/yul/*.yul`; read +by `solc --strict-assembly`. Layer 3 proves IR-to-Yul preservation. + +**EVM.** The final deployable bytecode. Produced by `solc` from Yul; deployed by +`forge create` or any standard toolchain. Not in the proof envelope: `solc`, +the EVM spec, and the deployment pipeline are explicit trust assumptions. + +## Source layer (EDSL) + +The EDSL is intentionally small. `Verity/Core.lean` provides `ContractState`, +`ContractResult` (the success/revert algebra), the `Contract` monad with +short-circuiting `bind`, six persistent storage spaces (uint256, address, +address-keyed mapping, uint256-keyed mapping, double mapping, dynamic arrays) +plus EIP-1153 transient storage, `require`, and a curated set of `@[simp]` +lemmas for proof automation. The `verity_contract` macro lowers +human-friendly syntax to both an executable Lean definition and a +`CompilationModel`, keeping the two in sync. See [`/edsl-api-reference`](/edsl-api-reference) +for the full surface and [`/first-contract`](/first-contract) for a guided walkthrough. + +## Pipeline (CompilationModel → Yul) + +The compiler runs a fixed sequence per contract: storage-slot inference, +selector lookup, IR generation, Yul AST construction, and pretty-printing. The +same binary emits machine-readable audit artifacts: `--trust-report`, +`--assumption-report`, `--layout-report`, and `--layout-compat-report`. The +linker (`Compiler/Linker.lean`) splices external Yul libraries (`--link`) into +the runtime section after validating that every non-builtin call site is +satisfied. See [`/compiler`](/compiler) for the pipeline narrative and CLI reference. + +## Verification layers (1 / 2 / 3) + +Verity organizes its correctness story in three layers. **Layer 1** is the +frontend bridge: an EDSL implementation is proven equivalent to its +`CompilationModel`. **Layer 2** is the compiler middle: a generic +whole-contract theorem in `Compiler/Proofs/IRGeneration/Contract.lean` proves +that `CompilationModel.compile` produces IR with matching semantics for the +current supported fragment. **Layer 3** is the backend: `IR → Yul` preserves +semantics, with the dispatcher bridge exposed as an explicit hypothesis rather +than a Lean axiom. See [`/trust-model`](/trust-model) for what is verified and +what is trusted at each layer, and [`/verification`](/verification) for the +live theorem inventory. + +## Where to next + +- [Getting Started](/getting-started) — local setup and your first verification run. +- [First Contract](/first-contract) — guided spec-to-proof walkthrough. +- [Compiler & CLI](/compiler) — the pipeline in detail, plus CLI flags. +- [Trust Model](/trust-model) — what you trust when you trust a Verity contract. +- [EDSL API Reference](/edsl-api-reference) — canonical primitive reference. diff --git a/docs-site/content/compiler.mdx b/docs-site/content/compiler.mdx index e5ef4d2f4..b586819d4 100644 --- a/docs-site/content/compiler.mdx +++ b/docs-site/content/compiler.mdx @@ -1,62 +1,85 @@ --- -title: Compiler -description: EDSL to EVM compilation with automatic IR generation +title: Compiler & CLI +description: The Verity compiler — pipeline, CLI usage, and the CompilationModel surface. --- -# Compiler +# Compiler & CLI -**Automatic compilation from verified EDSL to EVM bytecode.** +How verified EDSL contracts become deployable EVM bytecode, plus the CLI reference. For the trust boundary, see [Trust Model](/trust-model). -## Overview +## Pipeline -The Verity compiler transforms `CompilationModel` models into deployable EVM bytecode. No manual IR writing is required. +``` +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. | -**Pipeline**: EDSL Contract → CompilationModel → IR → Yul → EVM Bytecode +## Compile all contracts -The CLI can also emit machine-readable audit artifacts alongside Yul/ABI output: -- `--trust-report ` writes proof-boundary and assumption data. -- `--assumption-report ` writes a flattened assumption inventory grouped by contract and usage site. -- `--layout-report ` writes resolved storage-slot metadata, including effective alias writes and reserved-slot policies for upgrade/layout reviews. -- `--layout-compat-report ` compares the first selected contract as the baseline layout and the second as the candidate upgrade layout, then writes a machine-readable compatibility summary. +```bash +cd /path/to/verity +export PATH="$HOME/.elan/bin:$PATH" -Important: Verity has two different "spec" concepts. +lake build verity-compiler +lake exe verity-compiler # writes artifacts/yul/*.yul +``` -1. Logical specs in `Verity/Specs//Spec.lean` are `Prop` statements used for proofs. -2. Compiler specs in `Compiler/Specs.lean` are `CompilationModel` values used for code generation. +For contracts that use external libraries (e.g. Poseidon): -`CompilationModel` is not only an ABI. It also contains storage fields and function bodies (`Expr`/`Stmt`). +```bash +lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yul/ +``` -## Trust Model +See the [Linking External Libraries](/guides/linking-libraries) guide. -### What's Verified (Zero Trust Required) -- **Layer 1 frontend bridge**: EDSL behavior is proven equivalent to its `CompilationModel`. -- **Layer 2 boundary today**: the generic whole-contract `CompilationModel -> IR` theorem is proved for the current explicit supported fragment. -- **Layer 2 framework proof**: the former exact-state body-simulation axiom has been eliminated, and legacy contract-specific bridge theorems now sit above the generic compiler theorem as example wrappers. -- **Layer 3 framework proof**: `IR -> Yul` preserves semantics, with the remaining dispatch bridge exposed as an explicit theorem hypothesis rather than a Lean axiom. -- **Machine-checked proofs**: see [VERIFICATION_STATUS.md](https://github.com/Th0rgal/verity/blob/main/docs/VERIFICATION_STATUS.md) for the current proof-status snapshot and [AXIOMS.md](https://github.com/Th0rgal/verity/blob/main/AXIOMS.md) for documented axioms. -- **Interpreter semantics**: Spec, IR, and Yul semantics defined and linked in Lean +## Audit artifacts -The per-contract files in `Contracts//Proofs/` are separate contract-specification proofs. They show that a given contract satisfies its human-readable spec; they are not the definition of Layer 1 in the compiler stack. +The CLI emits machine-readable audit artifacts alongside Yul/ABI: -### What's Tested (High Confidence) -- **Compilation correctness**: Foundry unit and differential tests cover compiled contracts -- **Output validation**: Generated Yul is exercised against expected runtime behavior -- **Constructor handling**: Bytecode argument loading is covered in tests -- **Storage layout**: Automatic slot inference validated by examples +- `--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. -### What's Assumed (Trust Required) -- **Yul compiler**: Solidity's `solc` compiles Yul to bytecode correctly -- **EVM semantics**: Ethereum's execution model matches the spec used in proofs -- **Function selectors**: Pre-computed `keccak256` hashes are correct +For proof-strict builds, deny flags lock down the trust surface. Each one fails the build closed when the corresponding category of assumption appears: -### Roadmap -Roadmap, milestones, and progress updates live in `docs-site/content/research.mdx` and `docs-site/content/research/iterations.mdx`. +| 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 Implementation +**EDSL** (`Contracts/SimpleStorage/SimpleStorage.lean`): + ```verity --- Verity/Examples/SimpleStorage.lean def storedData : StorageSlot Uint256 := ⟨0⟩ def store (value : Uint256) : Contract Unit := do @@ -66,15 +89,12 @@ def retrieve : Contract Uint256 := do getStorage storedData ``` -### Declarative Specification +**CompilationModel** (`Compiler/Specs.lean`): + ```verity --- Compiler/Specs.lean def simpleStorageSpec : CompilationModel := { name := "SimpleStorage" - fields := [ - { name := "storedData", ty := FieldType.uint256 } - ] - constructor := none + fields := [{ name := "storedData", ty := FieldType.uint256 }] functions := [ { name := "store" params := [{ name := "value", ty := ParamType.uint256 }] @@ -87,751 +107,129 @@ def simpleStorageSpec : CompilationModel := { { name := "retrieve" params := [] returnType := some FieldType.uint256 - body := [ - Stmt.return (Expr.storage "storedData") - ] + body := [Stmt.return (Expr.storage "storedData")] } ] } ``` -### Generated IR -```lean --- Automatically generated (no manual writing) -{ name := "SimpleStorage" - deploy := [] - functions := [ - { name := "store" - selector := 0x6057361d - params := [{ name := "value", ty := IRType.uint256 }] - ret := IRType.unit - body := [ - YulStmt.let_ "value" (YulExpr.call "calldataload" [YulExpr.lit 4]), - YulStmt.expr (YulExpr.call "sstore" [YulExpr.lit 0, YulExpr.ident "value"]), - YulStmt.expr (YulExpr.call "stop" []) - ] - }, - { name := "retrieve" - selector := 0x2e64cec1 - params := [] - ret := IRType.uint256 - body := [ - YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 0, YulExpr.call "sload" [YulExpr.lit 0]]), - YulStmt.expr (YulExpr.call "return" [YulExpr.lit 0, YulExpr.lit 32]) - ] - } - ] - usesMapping := false -} -``` +**Generated Yul** (`artifacts/yul/SimpleStorage.yul`): -### Generated Yul ```yul -// artifacts/yul/SimpleStorage.yul object "SimpleStorage" { + code { datacopy(0, dataoffset("runtime"), datasize("runtime")) + return(0, datasize("runtime")) } + object "runtime" { code { - datacopy(0, dataoffset("runtime"), datasize("runtime")) - return(0, datasize("runtime")) - } - object "runtime" { - code { - switch shr(224, calldataload(0)) - case 0x6057361d { - /* store() */ - let value := calldataload(4) - sstore(0, value) - stop() - } - case 0x2e64cec1 { - /* retrieve() */ - mstore(0, sload(0)) - return(0, 32) - } - default { - revert(0, 0) - } - } + 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) } } + } } ``` -### Deployed Bytecode -```bash -# Compile Yul to bytecode -solc --strict-assembly SimpleStorage.yul - -# Deploy to Ethereum (local, testnet, or mainnet) -forge create SimpleStorage --from 0x... --private-key ... -``` - -## Compiler Architecture +## CompilationModel surface -### Modules +**Storage inference**: slots assigned in field order; no manual slot management. -**`Compiler/CompilationModel.lean`** -- Declarative contract DSL -- Expression language: `literal`, `param`, `storage`, `mapping`, `mappingWord`, `mappingPackedWord`, `structMember`, `structMember2`, `mapping2`, `mappingUint`, `caller`, `msgValue`, `blockTimestamp`, `blockNumber`, `blobbasefee`, `localVar`, `externalCall`, `internalCall`, `arrayLength`, `arrayElement`, arithmetic, bitwise, comparisons, logical operators -- Statement language: `letVar`, `assignVar`, `setStorage`, `setMapping`, `setMappingWord`, `setMappingPackedWord`, `setStructMember`, `setStructMember2`, `setMapping2`, `setMappingUint`, `require`, `return`, `stop`, `ite`, `forEach`, `emit`, `internalCall` -- Automatic IR generation from specs -- Constructor parameter handling (bytecode argument loading) -- Storage slot inference (field order → slots 0, 1, 2, ...) - -**`Compiler/Specs.lean`** -- Specifications for the example contracts -- Concise, type-safe, maintainable - -**`Compiler/Selector.lean`** -- Canonical function selector computation from `FunctionSpec` -- Type-safe Solidity signature generation from `FunctionSpec` - -**`Compiler/Selectors.lean`** -- Kernel-computable `keccak256_first_4_bytes` definition via the vendored unrolled Keccak engine -- Fixed selector regressions plus CI cross-checks against `solc --hashes` - -**`Compiler/Codegen.lean`** -- IR → Yul code generation -- Dispatcher generation (function selector switch) -- Mapping slot computation helper -- Deploy code + runtime code separation - -**`Compiler/Linker.lean`** -- External Yul library linking -- Line-based parser for extracting function definitions from `.yul` files -- Injection of library functions into runtime code section -- Validation of external references (`validateExternalReferences`) - -**`Compiler/Yul/*.lean`** (Yul AST + pretty printer) -- Yul abstract syntax tree -- Pretty printer (Yul → text) - -### Compilation Process - -1. **Specification**: Write declarative `CompilationModel` -2. **Storage Inference**: Assign slots 0, 1, 2, ... based on field order -3. **Selector Lookup**: Retrieve pre-computed function selectors -4. **IR Generation**: Compile expressions/statements to IR -5. **Code Generation**: Transform IR to Yul AST -6. **Pretty Print**: Render Yul AST as text -7. **Yul Compilation**: Use Solidity compiler (solc) to generate bytecode - -## Features - -### Automatic Storage Slot Inference ✅ ```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 + { name := "owner", ty := FieldType.address }, -- slot 0 + { name := "balances", ty := FieldType.mappingTyped (.simple .address) }, -- slot 1 + { name := "totalSupply", ty := FieldType.uint256 } -- slot 2 ] ``` -No manual slot management needed. Compiler assigns slots based on field order. +**Constructor parameters**: loaded from end of deployment bytecode (Solidity convention). -### Constructor Parameters ✅ ```verity constructor := some { params := [{ name := "initialOwner", ty := ParamType.address }] - body := [ - Stmt.setStorage "owner" (Expr.constructorArg 0) - ] -} -``` - -Arguments loaded from end of deployment bytecode (Solidity convention). - -### Function Selectors ✅ -```lean -"store(uint256)" → 0x6057361d -"retrieve()" → 0x2e64cec1 -``` - -Pre-computed from Solidity keccak256. Extensible for new functions. - -### Type-Safe DSL ✅ - -The CompilationModel DSL provides a complete expression and statement language for specifying contract behavior. - -**Expressions** (`Expr`): key constructors: - -| Constructor | Description | Yul Output | -|-------------|-------------|------------| -| `literal n` | Integer constant (mod 2^256) | `n` | -| `param "x"` | Function parameter | `x` (from calldata) | -| `constructorArg i` | Deploy-time argument | `argN` (from bytecode) | -| `storage "f"` | Read storage field | `sload(slot)` | -| `mapping "f" key` | Read mapping entry | `sload(mappingSlot(slot, key))` | -| `mappingWord "f" key offset` | Read mapping member word | `sload(add(mappingSlot(slot, key), offset))` | -| `mappingPackedWord "f" key offset {offset=o,width=w}` | Read packed bits from mapping member word | `and(shr(o, sload(add(mappingSlot(slot, key), offset))), mask)` | -| `structMember "f" key "member"` | Read named member of `mapping(K => Struct)` | same lowering as `mappingWord` / `mappingPackedWord` after member lookup | -| `structMember2 "f" k1 k2 "member"` | Read named member of `mapping(K1 => mapping(K2 => Struct))` | same lowering as nested mapping word/payload access after member lookup | -| `mapping2 "f" k1 k2` | Read nested mapping (e.g., allowances) | `sload(mappingSlot(mappingSlot(slot, k1), k2))` | -| `mappingUint "f" key` | Read uint256-keyed mapping | `sload(mappingSlot(slot, key))` | -| `caller` | Transaction sender | `caller()` | -| `contractAddress` | Current contract address | `address()` | -| `chainid` | Current chain ID | `chainid()` | -| `msgValue` | Sent ETH value | `callvalue()` | -| `blockTimestamp` | Current block timestamp | `timestamp()` | -| `blockNumber` | Current block number | `number()` | -| `blobbasefee` | Current blob base fee (EIP-7516) | `blobbasefee()` | -| `mload offset` | Read word from memory | `mload(offset)` | -| `keccak256 offset size` | Hash memory slice | `keccak256(offset, size)` | -| `call ...` | Low-level call primitive | `call(...)` | -| `staticcall ...` | Low-level static call primitive | `staticcall(...)` | -| `delegatecall ...` | Low-level delegate call primitive | `delegatecall(...)` | -| `returndataSize` | Bytes in returndata buffer | `returndatasize()` | -| `returndataOptionalBoolAt offset` | ERC20 optional-bool helper | `returndatasize()/mload` pattern | -| `localVar "x"` | Reference local variable | `x` | -| `externalCall "f" args` | Call linked library function | `f(args...)` | -| `internalCall "f" args` | Call internal contract function | `internal_f(args...)` | -| `arrayLength "arr"` | Length of dynamic array parameter | `arr_length` | -| `arrayElement "arr" idx` | Checked element of dynamic array parameter (reverts if `idx >= arr_length`) | `__verity_array_element_*_checked(arr_data_offset, arr_length, idx)` | -| `add a b` | Addition | `add(a, b)` | -| `sub a b` | Subtraction | `sub(a, b)` | -| `mul a b` | Multiplication | `mul(a, b)` | -| `div a b` | Division | `div(a, b)` | -| `mod a b` | Modulo | `mod(a, b)` | -| `bitAnd a b` | Bitwise AND | `and(a, b)` | -| `bitOr a b` | Bitwise OR | `or(a, b)` | -| `bitXor a b` | Bitwise XOR | `xor(a, b)` | -| `bitNot a` | Bitwise NOT | `not(a)` | -| `shl s v` | Shift left | `shl(s, v)` | -| `shr s v` | Shift right | `shr(s, v)` | -| `eq a b` | Equal | `eq(a, b)` | -| `gt a b` | Greater than | `gt(a, b)` | -| `lt a b` | Less than | `lt(a, b)` | -| `ge a b` | Greater or equal | `iszero(lt(a, b))` | -| `le a b` | Less or equal | `iszero(gt(a, b))` | - -Low-level call expressions compile to the expected Yul builtins, but their runtime semantics are still outside the current proof-interpreter model. Today they are a partial feature: codegen exists, while 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`). -| `logicalAnd a b` | Short-circuit logical AND | `and(iszero(iszero(a)), iszero(iszero(b)))` | -| `logicalOr a b` | Short-circuit logical OR | `or(iszero(iszero(a)), iszero(iszero(b)))` | -| `logicalNot a` | Logical NOT | `iszero(a)` | - -Use typed intrinsics (`Expr.mload`, `Expr.keccak256`, `Expr.contractAddress`, `Expr.chainid`, `Stmt.mstore`) instead of `Expr.externalCall` for these opcodes. Builtin names routed through `externalCall` remain rejected by interop validation. - -Memory-oriented intrinsics (`mload`, `mstore`, `calldatacopy`, `returndataCopy`, `returndataOptionalBoolAt`) compile, but the current proof interpreters still model them only partially. For audit-oriented or proof-strict builds, surface that boundary with `--trust-report` / `--deny-linear-memory-mechanics`; the remaining gap is tracked under issue `#1411`. - -Raw `rawLog` event emission also compiles, but the current proof interpreters still treat it as a not-modeled feature rather than a proved event semantics layer. For audit-oriented or proof-strict builds, archive `--trust-report` and add `--deny-event-emission` if the selected contracts must stay inside the proved subset. - -The `keccak256` intrinsic also compiles, but it remains axiomatized in the current proof stack rather than fully modeled end to end. For audit-oriented or proof-strict builds, archive `--trust-report` and add `--deny-axiomatized-primitives` if the selected contracts must stay inside the proved subset (see issue `#1411`). - -The trust-report surface also supports localized `localObligations` on a function or constructor. Use these when a small unsafe/assembly-shaped boundary still needs a user-supplied refinement contract without turning the whole compilation unit into an opaque trust blob. Direct raw low-level calls, returndata choreography, and manual memory/calldata primitives are expected to carry at least one such obligation on the enclosing constructor or function. For proof-strict builds, add `--deny-local-obligations` so any undischarged local obligation fails closed. When audit tooling needs a flat machine-readable list instead of the full nested trust report, archive `--assumption-report` alongside `--trust-report`. - -For upgradeability reviews, pair `--layout-compat-report` with `--deny-layout-incompatibility`. That path compares the first selected contract against the second, preserves all baseline field slots/types/alias writes, and fails closed if the candidate moves or mutates persisted storage fields while still writing the JSON compatibility report for audit trails. - -For Morpho-style `mapping(K => Struct)` / `mapping(K1 => mapping(K2 => Struct))` layouts, declare `FieldType.mappingStruct` / `FieldType.mappingStruct2` and access named members through `Expr.structMember` / `Expr.structMember2`. The `verity_contract` surface now exposes matching storage forms: - -```lean -positions : MappingStruct(Address,[ - supplyShares @word 0 packed(0,128), - borrowShares @word 0 packed(128,128), - delegate @word 1 -]) := slot 0 -approvals : MappingStruct2(Address,Address,[ - allowance @word 0 packed(0,128), - nonce @word 1 -]) := slot 1 -``` - -Members can carry packed bit metadata, so common `uint128`-style packed subfields stay declarative instead of becoming hand-written masking arithmetic in user code. - -For ERC-7201 and other namespaced layouts, `verity_contract` can switch the -active storage root inside the `storage` block. Use one namespace item per -source root, then declare fields below it: - -```lean -storage - storage_namespace erc7201 "unlink.storage.State" - state : StorageStruct [ - nextLeafIndex : Uint256 @word 0, - merkleTree : StorageStruct [ - root : Uint256 @word 0, - depth : Uint256 @word 1 - ] @word 1, - verifierRouter : Address @word 10 - ] := slot 0 - - storage_namespace erc7201 "unlink.storage.UnlinkPoolRelayers" - relayersSlot : Address -> Uint256 := slot 0 -``` - -`StorageStruct` is for explicit storage layout trees. Named `struct` -declarations remain the ABI/source type surface for parameters and local values. -Use `MappingStruct(...)` / `MappingStruct2(...)` when the source has -`mapping(K => Struct)` rather than a top-level storage struct root. - -**Statements** (`Stmt`): key constructors: - -| Constructor | Description | Yul Output | -|-------------|-------------|------------| -| `letVar "x" expr` | Declare local variable | `let x := expr` | -| `assignVar "x" expr` | Reassign existing variable | `x := expr` | -| `setStorage "f" expr` | Write storage field | `sstore(slot, expr)` | -| `setMapping "f" key val` | Write mapping entry | `sstore(mappingSlot(slot, key), val)` | -| `setMappingWord "f" key offset val` | Write mapping member word | `sstore(add(mappingSlot(slot, key), offset), val)` | -| `setMappingPackedWord "f" key offset {offset=o,width=w} val` | Packed mapping member write (RMW) | `slotWord := sload(...); sstore(..., or(and(slotWord, not(mask< Struct)` | same lowering as mapping word / packed-word writes after member lookup | -| `setStructMember2 "f" k1 k2 "member" val` | Write named member of nested struct mapping | same lowering as nested mapping word / packed-word writes after member lookup | -| `setMapping2 "f" k1 k2 val` | Write nested mapping entry | `sstore(mappingSlot(mappingSlot(slot, k1), k2), val)` | -| `setMappingUint "f" key val` | Write uint256-keyed mapping | `sstore(mappingSlot(slot, key), val)` | -| `require cond "msg"` | Guard with revert message | `if iszero(cond) { revert(...) }` | -| `mstore offset value` | Write memory word | `mstore(offset, value)` | -| `return expr` | Return value | `mstore(0, expr) return(0, 32)` | -| `returndataCopy d s n` | Copy returndata bytes | `returndatacopy(d, s, n)` | -| `revertReturndata` | Bubble revert payload | `returndatacopy(0,0,n); revert(0,n)` | -| `stop` | End execution | `stop()` | -| `ite cond then else` | If/else branching | `if cond { then } if iszero(cond) { else }` | -| `forEach "i" count body` | Bounded loop | `for { let i := 0 } lt(i, count) { i := add(i,1) } { body }` | -| `emit "Event" args` | Emit event | `log1(ptr, size, topic0)` | -| `internalCall "f" args` | Call internal function (statement) | `internal_f(args...)` | - -**Example**, combining multiple features: -```verity --- Balance check with require -Stmt.require (Expr.ge (Expr.mapping "balances" Expr.caller) (Expr.param "amount")) "Insufficient", -Stmt.setMapping "balances" Expr.caller - (Expr.sub (Expr.mapping "balances" Expr.caller) (Expr.param "amount")), -Stmt.stop -``` - -```verity --- If/else branching -Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner")) - [Stmt.setStorage "paused" (Expr.literal 1), Stmt.stop] - [Stmt.stop] -- non-owner: no-op -``` - -```verity --- Bounded loop over array -Stmt.forEach "i" (Expr.arrayLength "recipients") - [Stmt.setMapping "balances" (Expr.arrayElement "recipients" (Expr.localVar "i")) - (Expr.param "amount")] -``` - -### Code Optimization ✅ -```yul -// Before (manual): Unnecessary variable -let current := sload(0) -sstore(0, add(current, 1)) - -// After (automatic): Inlined expression -sstore(0, add(sload(0), 1)) -``` - -Automatic expression inlining reduces bytecode size and gas costs. - -### External Library Linking ✅ - -Link production cryptographic libraries (or any external Yul functions) into compiled contracts using the `--link` flag: - -```bash -lake exe verity-compiler \ - --link examples/external-libs/PoseidonT3.yul \ - --link examples/external-libs/PoseidonT4.yul \ - -o artifacts/yul -``` - -**How it works**: The linker parses `.yul` files, extracts function definitions, and injects them into the runtime `code {}` section of each compiled contract. This lets you prove properties about contract logic using simple placeholder functions in Lean, then swap in production-grade implementations at compile time. - -**Library file format**: External libraries should contain plain Yul function definitions (no `object` wrapper): -```yul -function PoseidonT3_hash(a, b) -> result { - // Production implementation here - result := /* ... */ -} -``` - -**Validation**: The `validateExternalReferences` function checks that all non-builtin function calls in the contract are satisfied by linked libraries, catching missing dependencies at compile time. - -See [`examples/external-libs/`](https://github.com/Th0rgal/verity/tree/main/examples/external-libs) for example library files. - -### Backend Profiles - -The compiler supports an opt-in backend profile for deterministic output-shape normalization: - -```bash -# Default semantic profile -lake exe verity-compiler --backend-profile semantic - -# Sort dispatch `case` blocks by selector -lake exe verity-compiler --backend-profile solidity-parity-ordering - -# Sort selector cases + enable deterministic patch pass -lake exe verity-compiler-patched --backend-profile solidity-parity -``` - -### If/Else Branching - -Conditional logic for contract functions: - -```verity --- Simple if (no else) -Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner")) - [Stmt.setStorage "paused" (Expr.literal 1)] - [] - --- If/else with both branches -Stmt.ite (Expr.gt (Expr.param "amount") (Expr.literal 0)) - [Stmt.setMapping "balances" Expr.caller - (Expr.add (Expr.mapping "balances" Expr.caller) (Expr.param "amount"))] - [-- else: revert on zero amount - Stmt.require (Expr.literal 0) "Amount must be positive"] -``` - -Compiles to a block-scoped condition variable to avoid re-evaluation after state mutation: -```yul -{ - let __ite_cond := eq(caller(), sload(0)) - if __ite_cond { sstore(1, 1) } - if iszero(__ite_cond) { /* else branch */ } -} -``` - -### Bounded Loops - -Iterate over array parameters or fixed counts: - -```verity --- Iterate over a dynamic array -Stmt.forEach "i" (Expr.arrayLength "recipients") - [Stmt.setMapping "balances" - (Expr.arrayElement "recipients" (Expr.localVar "i")) - (Expr.add - (Expr.mapping "balances" (Expr.arrayElement "recipients" (Expr.localVar "i"))) - (Expr.param "amount"))] -``` - -Compiles to a Yul `for` loop: -```yul -for { let i := 0 } lt(i, recipients_length) { i := add(i, 1) } { - sstore(mappingSlot(0, calldataload(add(recipients_data_offset, mul(i, 32)))), - add(sload(mappingSlot(0, calldataload(add(recipients_data_offset, mul(i, 32))))), amount)) -} -``` - -### Internal Functions - -Define reusable logic shared across multiple external functions. Internal functions compile to Yul `function` definitions and are **not** exposed via selector dispatch: - -The examples in this section use the lower-level `CompilationModel` API directly. In `verity_contract` source, call same-contract helpers with ordinary function-call syntax instead: - -```lean -helper arg -let result ← helper arg -let (lhs, rhs) ← helperPair arg -``` - -Those source forms lower to `Stmt.internalCall`, `Stmt.internalCallAssign`, or `Expr.internalCall` in the compilation model. - -```verity -def mySpec : CompilationModel := { - name := "MyContract" - fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }] - functions := [ - -- Internal helper (not exposed) - { name := "addBalance" - params := [{ name := "addr", ty := ParamType.address }, - { name := "amt", ty := ParamType.uint256 }] - returnType := none - body := [ - Stmt.setMapping "balances" (Expr.param "addr") - (Expr.add (Expr.mapping "balances" (Expr.param "addr")) - (Expr.param "amt")) - ] - isInternal := true -- Not dispatched externally - }, - -- External function that calls the helper - { name := "deposit" - params := [] - returnType := none - body := [ - Stmt.internalCall "addBalance" [Expr.caller, Expr.msgValue], - Stmt.stop - ] - } - ] + body := [Stmt.setStorage "owner" (Expr.constructorArg 0)] } ``` -Internal functions that return values use `__ret` assignment instead of EVM `RETURN`: -```verity --- Internal function returning a value -{ name := "getBalance" - params := [{ name := "addr", ty := ParamType.address }] - returnType := some FieldType.uint256 - body := [Stmt.return (Expr.mapping "balances" (Expr.param "addr"))] - isInternal := true -} - --- Call it from an expression context -Stmt.letVar "bal" (Expr.internalCall "getBalance" [Expr.caller]) -``` - -### Event Emission - -Emit EVM events for standards compliance (ERC20 Transfer/Approval, etc.): - -```verity -def tokenSpec : CompilationModel := { - name := "Token" - fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }] - events := [ - { name := "Transfer" - params := [ - { name := "from", ty := ParamType.address, kind := EventParamKind.indexed }, - { name := "to", ty := ParamType.address, kind := EventParamKind.indexed }, - { name := "amount", ty := ParamType.uint256, kind := EventParamKind.unindexed } - ] - } - ] - functions := [ - { name := "transfer" - params := [{ name := "to", ty := ParamType.address }, - { name := "amount", ty := ParamType.uint256 }] - returnType := none - body := [ - -- ... transfer logic ... - Stmt.emit "Transfer" [Expr.caller, Expr.param "to", Expr.param "amount"], - Stmt.stop - ] - } - ] -} -``` - -Event topic0 is computed from the event signature (e.g., `keccak256("Transfer(address,address,uint256)")`). The compiler generates `log1` opcodes for events. - -### Nested Mappings (Double Mappings) - -For ERC20 allowances and similar patterns requiring `mapping(address => mapping(address => uint256))`: - -```verity -fields := [ - { name := "allowances", ty := FieldType.mappingTyped (MappingType.nested .address .address) } -] - --- Read: allowances[owner][spender] -Expr.mapping2 "allowances" (Expr.param "owner") (Expr.param "spender") - --- Write: allowances[owner][spender] = amount -Stmt.setMapping2 "allowances" (Expr.param "owner") (Expr.param "spender") (Expr.param "amount") -``` - -Storage layout: `keccak256(spender . keccak256(owner . slot))`; matches Solidity nested mapping layout. - -### Uint256-Keyed Mappings - -For mappings keyed by numeric values instead of addresses: - -```verity -fields := [ - { name := "data", ty := FieldType.mappingTyped (MappingType.simple .uint256) } -] - --- Read: data[tokenId] -Expr.mappingUint "data" (Expr.param "tokenId") - --- Write: data[tokenId] = value -Stmt.setMappingUint "data" (Expr.param "tokenId") (Expr.param "value") -``` - -### Array and Bytes Parameters +**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. -Dynamic arrays, fixed arrays, and bytes parameters for batch operations: +> **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`). -```verity --- Dynamic array parameter -{ name := "recipients", ty := ParamType.array ParamType.address } +**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. --- Fixed-size array parameter -{ name := "values", ty := ParamType.fixedArray ParamType.uint256 3 } +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`. --- Dynamic bytes parameter -{ name := "data", ty := ParamType.bytes } +**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. --- Access array elements in function body -Expr.arrayLength "recipients" -- number of elements -Expr.arrayElement "recipients" (Expr.localVar "i") -- element at index i -``` +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. -Dynamic arrays use ABI offset-based decoding. The compiler generates `_length` and `_data_offset` local variables automatically. +## Add a new contract -## Usage +1. Declare it with `verity_contract` in `Contracts//.lean`: -### Compile All Contracts -```bash -cd /path/to/verity -export PATH="$HOME/.elan/bin:$PATH" + ```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) + ``` -# Build compiler -lake build verity-compiler + Stateless contracts may leave the `storage` block empty. -# Generate Yul for all contracts -lake exe verity-compiler +2. Register it in `Compiler/Specs.lean` under `allSpecs`: -# Output: artifacts/yul/*.yul -``` + ```lean + Contracts.MyContract.spec + ``` -### Test Compiled Contracts -```bash -# Run all Foundry tests (difftest profile enables FFI for Yul compilation) -FOUNDRY_PROFILE=difftest forge test +3. Recompile: -# Expected: all current difftest suites pass -``` + ```bash + lake build verity-compiler + lake exe verity-compiler + ``` -### Add New Contract +Handwritten `Compiler.Specs.*Spec` definitions are retained for migration only; they are not the canonical compile path. -1. **Add a macro contract declaration** 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) -``` +For the full authoring checklist (specs, invariants, proofs, tests), see [First Contract](/first-contract). -If a contract is stateless, the `storage` block may be left empty instead of inventing a dummy slot. +## Test compiled contracts -2. **Register it in** `Compiler/Specs.lean` **under** `allSpecs`: -```lean -Contracts.MyContract.spec -``` - -3. **Recompile**: ```bash -lake build verity-compiler -lake exe verity-compiler +FOUNDRY_PROFILE=difftest forge test # FFI enables Yul compilation +lake build # verifies all Lean proofs ``` -4. **Done!** Contract generated in `artifacts/yul/MyContract.yul` - -Legacy note: handwritten `Compiler.Specs.*Spec` definitions are retained only for -migration/special workflows and are not the canonical CLI compile path. - -Time: **~5 minutes** (vs ~30 minutes manual IR) - -## Test Results - -### All Tests Pass ✅ - -**Lean Proofs**: `lake build` verifies the current proof set. See [VERIFICATION_STATUS.md](https://github.com/Th0rgal/verity/blob/main/docs/VERIFICATION_STATUS.md) for the live totals. -```bash -$ lake build -Build completed successfully. -``` - -**Foundry Tests**: `FOUNDRY_PROFILE=difftest forge test` exercises the current test suite. -```bash -$ FOUNDRY_PROFILE=difftest forge test -... -``` +## Validated contracts -**Coverage**: Unit, property, and differential tests across EDSL and compiled Yul. See `test/` for suites. +| 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 | -### Validated Contracts +Not compiled: `ReentrancyExample` (inline proofs only). `CryptoHash` compiles via `--link` with external Poseidon and is validated in CI. -All current example contracts compile and pass tests: -- ✅ **SimpleStorage**: Basic storage operations -- ✅ **Counter**: Arithmetic operations -- ✅ **Owned**: Access control with constructor args -- ✅ **OwnedCounter**: Pattern composition with constructor -- ✅ **Ledger**: Mapping-based balances -- ✅ **SimpleToken**: ERC20-like token with constructor -- ✅ **SafeCounter**: Checked arithmetic with underflow protection +## Trust boundary -**Not compiled**: ReentrancyExample (proofs are embedded inline, no compiler spec). CryptoHash compiles via `--link` with external Poseidon libraries and is validated in CI. - -## Comparison: Manual vs Automatic - -### Lines of Code -- **Before**: Manual IR for all contracts (brittle to maintain) -- **After**: Declarative specs for all contracts (stable, reusable) -- **Reduction**: Manual IR eliminated - -### Time to Add Contract -- **Before**: Manual IR requires more steps (write IR, test, debug) -- **After**: Declarative specs reduce the setup and iteration work -- **Improvement**: Faster authoring and less surface for mistakes - -### Code Quality -- **Before**: Manual Yul construction, error-prone -- **After**: Type-safe DSL, compile-time validation -- **Result**: More optimized, safer, maintainable - -### Example: Owned Contract - -**Before** (manual IR): -```lean -private def ownedContract : IRContract := - let deployBody := [ - stmtLet "argsOffset" (call "sub" [call "codesize" [], lit 32]), - stmtExpr (call "codecopy" [lit 0, ident "argsOffset", lit 32]), - stmtLet "initialOwner" (call "and" [call "mload" [lit 0], hex addressMask]), - sstoreSlot 0 (ident "initialOwner") - ] - let transferBody := onlyOwnerCheck 0 ++ [ - stmtLet "newOwner" (calldataAddress 4), - sstoreSlot 0 (ident "newOwner"), - stop - ] - let getOwnerBody := returnUint (sloadSlot 0) - { name := "Owned" - deploy := deployBody - functions := [ - fn "transferOwnership" 0xf2fde38b [addrParam "newOwner"] IRType.unit transferBody, - fn "getOwner" 0x893d20e8 [] IRType.address getOwnerBody - ] - usesMapping := false } -``` - -**After** (declarative spec): -```verity -def ownedSpec : CompilationModel := { - name := "Owned" - fields := [ - { name := "owner", ty := FieldType.address } - ] - constructor := some { - params := [{ name := "initialOwner", ty := ParamType.address }] - body := [ - Stmt.setStorage "owner" (Expr.constructorArg 0) - ] - } - functions := [ - { name := "transferOwnership" - params := [{ name := "newOwner", ty := ParamType.address }] - returnType := none - body := [ - Stmt.require (Expr.eq Expr.caller (Expr.storage "owner")) "Not owner", - Stmt.setStorage "owner" (Expr.param "newOwner"), - Stmt.stop - ] - }, - { name := "getOwner" - params := [] - returnType := some FieldType.address - body := [ - Stmt.return (Expr.storage "owner") - ] - } - ] -} -``` +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). -**Improvements**: -- 33% shorter -- Type-safe expressions -- No manual Yul construction -- Automatic slot/selector management +**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. -## Links +## See also -- [Research & Development](/research): Design decisions and proof techniques -- [Examples](/examples): current example contracts and walkthroughs -- [Verification](/verification): live proof/test status and verification structure -- [GitHub Repository](https://github.com/Th0rgal/verity): Source code +- [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). diff --git a/docs-site/content/core.mdx b/docs-site/content/core.mdx index 96b5979e6..a3903437c 100644 --- a/docs-site/content/core.mdx +++ b/docs-site/content/core.mdx @@ -21,28 +21,37 @@ structure StorageSlot (α : Type) where `Uint256` is a dedicated 256-bit modular integer type, so `+`, `-`, `*`, `/`, and `%` wrap exactly like the EVM. -> **Note**: This matches EVM wrapping semantics, not Solidity's default checked arithmetic (^0.8). Use `require` guards to match Solidity behavior. See [TRUST_ASSUMPTIONS.md](https://github.com/Th0rgal/verity/blob/main/TRUST_ASSUMPTIONS.md#8-arithmetic-semantics-wrapping-vs-checked) for details. +> **Note**: This matches EVM wrapping semantics, not Solidity's default checked arithmetic (^0.8). Use `require` guards to match Solidity behavior. See [TRUST_ASSUMPTIONS.md](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md#8-arithmetic-semantics-wrapping-vs-checked) for details. ## ContractState ```verity structure ContractState where - storage : Nat → Uint256 -- Uint256 storage - storageAddr : Nat → Address -- Address storage - storageMap : Nat → Address → Uint256 -- Mapping storage (address-keyed) - storageMapUint : Nat → Uint256 → Uint256 -- Mapping storage (uint256-keyed) - storageMap2 : Nat → Address → Address → Uint256 -- Double mapping storage - sender : Address - thisAddress : Address - msgValue : Uint256 - blockTimestamp : Uint256 - knownAddresses : Nat → FiniteAddressSet -- Tracked addresses per slot - events : List Event := [] -- Emitted events (append-only) + -- Persistent storage spaces, indexed by slot + storage : Nat → Uint256 -- uint256 slots + storageAddr : Nat → Address -- address slots + storageMap : Nat → Address → Uint256 -- address-keyed mapping + storageMapUint : Nat → Uint256 → Uint256 -- uint-keyed mapping + storageMap2 : Nat → Address → Address → Uint256 -- double mapping + storageArray : Nat → List Uint256 -- dynamic in-storage arrays + -- EIP-1153 transient storage + transientStorage : Nat → Uint256 + -- EVM context + sender, thisAddress : Address + msgValue, selfBalance : Uint256 + blockTimestamp, blockNumber, chainId, blobBaseFee : Uint256 + -- Calldata and memory + calldataSize : Uint256 + calldata : List Nat + memory : Nat → Uint256 + -- Bookkeeping + knownAddresses : Nat → FiniteAddressSet -- tracked per slot, for conservation + events : List Event -- append-only log ``` -Five independent storage spaces: `storage` for Uint256 values, `storageAddr` for addresses, `storageMap` for address-keyed mappings (e.g., `balances[owner]`), `storageMapUint` for uint256-keyed mappings, and `storageMap2` for double mappings (e.g., `allowances[owner][spender]`). Each is indexed by a natural number (the slot). +Six persistent storage spaces plus transient storage. `storage` for Uint256 values, `storageAddr` for addresses, `storageMap` / `storageMapUint` / `storageMap2` for the three mapping shapes, `storageArray` for dynamic arrays. Each is indexed by a natural number (the slot). -The state also carries: the `sender` address, the contract's own `thisAddress`, EVM context fields (`msgValue`, `blockTimestamp`), `knownAddresses` for tracking which addresses have been seen per slot (used in conservation proofs), and an append-only `events` log. +`knownAddresses` tracks which addresses have been seen per slot and is used by conservation proofs. EVM context fields (`msgValue`, `blockTimestamp`, `blockNumber`, `chainId`, `blobBaseFee`, `selfBalance`) and calldata/memory are modeled so EDSL proofs can reason about them; the `verity_contract` macro routes context accessors and `tstore`/`tload` through these fields. ## ContractResult @@ -54,7 +63,7 @@ inductive ContractResult (α : Type) where Every contract operation returns either `success` with a value and updated state, or `revert` with an error message and the state at the point of failure. -> **Important**: On revert, the returned state may include mutations from operations that executed *before* the revert. This differs from EVM semantics where REVERT discards all state changes. Contracts must follow the **checks-before-effects pattern** — all `require` guards before any `setStorage`/`setMapping` calls — to ensure the revert state equals the original input state. See [TRUST_ASSUMPTIONS.md](https://github.com/Th0rgal/verity/blob/main/TRUST_ASSUMPTIONS.md) and [#254](https://github.com/Th0rgal/verity/issues/254) for details. +> **Important**: On revert, the returned state may include mutations from operations that executed *before* the revert. This differs from EVM semantics where REVERT discards all state changes. Contracts must follow the **checks-before-effects pattern** — all `require` guards before any `setStorage`/`setMapping` calls — to ensure the revert state equals the original input state. See [TRUST_ASSUMPTIONS.md](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md) and [#254](https://github.com/lfglabs-dev/verity/issues/254) for details. ## Contract monad @@ -73,79 +82,13 @@ def bind (ma : Contract α) (f : α → Contract β) : Contract β := This gives do-notation with automatic failure propagation. A failed `require` stops the whole chain. -## Storage operations +## Primitives -Five pairs of get/set functions, one per storage type: +The core types above are operated on by a small surface of EDSL primitives — storage get/set, mapping get/set, context accessors (`msgSender`, `msgValue`, `blockTimestamp`, `contractAddress`), event emission, and the `require` guard. Those are documented in the [EDSL API Reference](/edsl-api-reference); the prose here only covers the *type layer* and the monad, not the operation catalogue. -| Storage type | Get | Set | Slot type | -|---|---|---|---| -| Uint256 | `getStorage` | `setStorage` | `StorageSlot Uint256` | -| Address | `getStorageAddr` | `setStorageAddr` | `StorageSlot Address` | -| Mapping (address-keyed) | `getMapping` | `setMapping` | `StorageSlot (Address → Uint256)` | -| Mapping (uint256-keyed) | `getMappingUint` | `setMappingUint` | `StorageSlot (Uint256 → Uint256)` | -| Double mapping | `getMapping2` | `setMapping2` | `StorageSlot (Address → Address → Uint256)` | +The shape of every primitive is the same: it's a `Contract α` value, which is `ContractState → ContractResult α`. Read-only primitives like `msgSender` and `getStorage` always emit `ContractResult.success`; write primitives like `setStorage` return `success ()` with a modified `ContractState`. `require` is the one operation that may emit `ContractResult.revert`, preserving the original state. -All follow the same pattern — read from or write to the corresponding `ContractState` field: - -```verity -def getStorage (s : StorageSlot Uint256) : Contract Uint256 := - fun state => ContractResult.success (state.storage s.slot) state - -def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit := - fun state => ContractResult.success () - { state with storage := fun slot => - if slot == s.slot then value else state.storage slot } -``` - -Mapping operations take key arguments: - -```verity --- Address-keyed mapping (e.g., balances[owner]) -let bal ← getMapping balances owner -setMapping balances owner newBal - --- Uint256-keyed mapping -let val ← getMappingUint prices tokenId -setMappingUint prices tokenId newPrice - --- Double mapping (e.g., allowances[owner][spender]) -let allow ← getMapping2 allowances owner spender -setMapping2 allowances owner spender newAllow -``` - -> `setMapping` also inserts the key into `knownAddresses` for that slot, enabling conservation proofs that sum over all balances. - -## Context accessors - -Read-only functions for accessing transaction context: - -```verity -let sender ← msgSender -- Transaction sender address -let self ← contractAddress -- This contract's address -let value ← msgValue -- ETH value sent with call -let time ← blockTimestamp -- Current block timestamp -``` - -These return values from `ContractState` without modifying state. - -## Event emission - -```verity -emitEvent "Transfer" [amount] [senderBal, recipientBal] -``` - -`emitEvent name args indexedArgs` appends to the `events` log. The `indexedArgs` parameter is optional (defaults to `[]`). - -## Require guard - -```verity -def require (condition : Bool) (message : String) : Contract Unit := - fun s => if condition - then ContractResult.success () s - else ContractResult.revert message s -``` - -Returns `success` when the condition holds, `revert` with the message when it doesn't. +> `setMapping` (and its keyed variants) also inserts the key into `knownAddresses` for that slot, enabling conservation proofs that sum over all balances. ## Simp lemmas @@ -191,75 +134,22 @@ let allow ← getMapping2 allowances owner spender -- Uint256 let wrong ← getStorage owner -- Type error: owner is Address, not Uint256 ``` -## Spec helpers (`Verity/Specs/Common.lean`) - -Specs express what a function **did not change**. `Common.lean` provides named predicates so specs don't repeat field-by-field equality. - -Import with `import Verity.Specs.Common` and `open Verity.Specs`. - -### Atomic helpers (single field) - -| Helper | Asserts | -|--------|---------| -| `sameStorage s s'` | `s'.storage = s.storage` | -| `sameStorageAddr s s'` | `s'.storageAddr = s.storageAddr` | -| `sameStorageMap s s'` | `s'.storageMap = s.storageMap` | -| `sameStorageMapUint s s'` | `s'.storageMapUint = s.storageMapUint` | -| `sameStorageMap2 s s'` | `s'.storageMap2 = s.storageMap2` | -| `sameContext s s'` | sender, thisAddress, msgValue, blockTimestamp unchanged | - -### Composite helpers - -Use these instead of conjunctions of atomics: - -| Helper | Meaning | Use when operation only writes... | -|--------|---------|-----------------------------------| -| `sameAllStorage s s'` | All 5 storage types unchanged | Context fields only | -| `sameExceptStorage s s'` | Everything except `storage` unchanged | `setStorage` | -| `sameExceptStorageAddr s s'` | Everything except `storageAddr` unchanged | `setStorageAddr` | -| `sameExceptStorageMap s s'` | Everything except `storageMap` unchanged | `setMapping` | -| `sameExceptStorageMapUint s s'` | Everything except `storageMapUint` unchanged | `setMappingUint` | -| `sameExceptStorageMap2 s s'` | Everything except `storageMap2` unchanged | `setMapping2` | - -All composites include `sameContext`. - -### Mixed storage+context helpers - -These combine two atomic storage checks with `sameContext`. They are the most commonly used helpers in practice — appearing in nearly every spec: - -| Helper | Meaning | Use when operation only writes... | -|--------|---------|-----------------------------------| -| `sameAddrMapContext s s'` | `sameStorageAddr ∧ sameStorageMap ∧ sameContext` | `setStorage` (uint256 slot only) | -| `sameStorageMapContext s s'` | `sameStorage ∧ sameStorageMap ∧ sameContext` | `setStorageAddr` (address slot only) | -| `sameStorageAddrContext s s'` | `sameStorage ∧ sameStorageAddr ∧ sameContext` | `setMapping` (mapping only) | - -**Example**: A counter's `increment` spec modifies a uint256 storage slot, so the unchanged-state predicate is `sameAddrMapContext` (address storage, mapping storage, and context are all unchanged). - -### Fine-grained helpers (specific slot or key) +## Spec helpers -For operations that modify a single entry in a mapping: +Specs express what a function **did not change**. `Verity/Specs/Common.lean` provides named predicates so specs don't repeat field-by-field equality. Import with `import Verity.Specs.Common` and `open Verity.Specs`. -| Helper | Asserts | -|--------|---------| -| `storageUnchangedExcept slot s s'` | All uint256 slots except `slot` unchanged | -| `storageAddrUnchangedExcept slot s s'` | All address slots except `slot` unchanged | -| `storageMapUnchangedExceptKeyAtSlot slot addr s s'` | Mapping unchanged except `slot`/`addr` | -| `storageMapUnchangedExceptKeysAtSlot slot a1 a2 s s'` | Mapping unchanged except `slot`/`a1`/`a2` (transfers) | -| `storageMapUintUnchangedExceptSlot slot s s'` | Uint256-keyed mapping unchanged except `slot` | -| `storageMapUintUnchangedExceptKey slot key s s'` | Uint256-keyed mapping at `slot` unchanged except `key` | -| `storageMap2UnchangedExceptSlot slot s s'` | Double mapping unchanged except `slot` | +Three layers, narrowest first: -### Choosing the right helper +- **Atomic** — one field at a time: `sameStorage`, `sameStorageAddr`, `sameStorageMap`, `sameStorageMapUint`, `sameStorageMap2`, `sameContext`. +- **Mixed** (most common in practice) — two storage checks + `sameContext`: + - `sameAddrMapContext` — use when only `setStorage` (uint256 slot) writes. + - `sameStorageMapContext` — use when only `setStorageAddr` writes. + - `sameStorageAddrContext` — use when only `setMapping` writes. +- **Composite** (strictest) — everything except one storage type: `sameExceptStorage`, `sameExceptStorageAddr`, `sameExceptStorageMap`, `sameExceptStorageMapUint`, `sameExceptStorageMap2`. `sameAllStorage` covers context-only writes. All composites include `sameContext`. +- **Fine-grained** — for single-entry mapping updates: `storageUnchangedExcept slot`, `storageAddrUnchangedExcept slot`, `storageMapUnchangedExceptKeyAtSlot slot addr`, `storageMapUnchangedExceptKeysAtSlot slot a1 a2` (transfers), `storageMapUintUnchangedExceptSlot`, `storageMapUintUnchangedExceptKey`, `storageMap2UnchangedExceptSlot`. -| Operation | Mixed (most common) | Composite (strictest) | Fine-grained | -|-----------|---------------------|----------------------|--------------| -| `setStorage count v` | `sameAddrMapContext` | `sameExceptStorage` | `storageUnchangedExcept count.slot` | -| `setStorageAddr owner v` | `sameStorageMapContext` | `sameExceptStorageAddr` | `storageAddrUnchangedExcept owner.slot` | -| `setMapping balances addr v` | `sameStorageAddrContext` | `sameExceptStorageMap` | `storageMapUnchangedExceptKeyAtSlot balances.slot addr` | -| ERC20 transfer (two keys) | `sameStorageAddrContext` | `sameExceptStorageMap` | `storageMapUnchangedExceptKeysAtSlot balances.slot from to` | -| `setMappingUint prices id v` | — | `sameExceptStorageMapUint` | `storageMapUintUnchangedExceptKey prices.slot id` | -| Read-only (`getStorage`, etc.) | — | `sameAllStorage ∧ sameContext` | — | +A counter's `increment` writes only the uint256 count slot, so the unchanged-state predicate is `sameAddrMapContext`. An ERC20 `transfer` (two mapping keys) uses `storageMapUnchangedExceptKeysAtSlot balances.slot from to`. ## Source -[`Verity/Core.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Core.lean) · [`Verity/Specs/Common.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Specs/Common.lean) +[`Verity/Core.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Core.lean) · [`Verity/Specs/Common.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Specs/Common.lean) diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx index 9ddf77c21..6a6eb6421 100644 --- a/docs-site/content/edsl-api-reference.mdx +++ b/docs-site/content/edsl-api-reference.mdx @@ -5,9 +5,7 @@ description: Canonical reference for Verity contract-building primitives # EDSL API Reference -This page is the canonical API reference for primitives used to write Verity contracts. - -## Imports +Canonical reference for primitives used to write Verity contracts. ```lean import Verity @@ -16,206 +14,59 @@ open Verity.EVM.Uint256 open Verity.Stdlib.Math ``` -## `verity_contract` Local Obligations - -Use `local_obligations [...]` on constructors or functions when a small unsafe or refinement-shaped boundary must stay explicit in the generated trust report. Direct assembly-shaped primitives such as raw low-level calls, returndata forwarding, and manual memory/calldata operations are expected to carry at least one local obligation at that exact usage site. - -```verity -function unsafeEdge () - local_obligations [manual_delegatecall_refinement := assumed "Caller must separately prove the handwritten assembly path."] - : Unit := do - pure () -``` - -Each entry lowers into `spec.constructor.localObligations` or `FunctionSpec.localObligations`, shows up in `--trust-report`, and participates in `--deny-local-obligations`. If a constructor or function uses direct assembly-shaped primitives without any `local_obligations [...]`, compilation now fails closed. - -## Storage Operations - -### `getStorage` / `setStorage` - -**Signature** - -```verity -def getStorage (s : StorageSlot Uint256) : Contract Uint256 -def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit -``` - -**Description** - -Read/write a `Uint256` storage slot. - -**Example** - -```verity -let x <- getStorage counterSlot -setStorage counterSlot (x + 1) -``` - -**Proof lemmas** - -- `getStorage_run`, `setStorage_run` (`Verity/Core.lean`) -- `getStorage_runState`, `getStorage_runValue`, `setStorage_getStorage` (`Verity/Proofs/Stdlib/Automation.lean`) - -### `getStorageAddr` / `setStorageAddr` - -**Signature** - -```verity -def getStorageAddr (s : StorageSlot Address) : Contract Address -def setStorageAddr (s : StorageSlot Address) (value : Address) : Contract Unit -``` - -**Description** - -Read/write an `Address` storage slot. - -**Example** - -```verity -let owner <- getStorageAddr ownerSlot -setStorageAddr ownerSlot newOwner -``` - -**Proof lemmas** - -- `getStorageAddr_run`, `setStorageAddr_run` (`Verity/Core.lean`) -- Address-storage automation lemmas in `Verity/Proofs/Stdlib/Automation.lean` - -### `getMapping` / `setMapping` - -**Signature** - -```verity -def getMapping (s : StorageSlot (Address -> Uint256)) (key : Address) : Contract Uint256 -def setMapping (s : StorageSlot (Address -> Uint256)) (key : Address) (value : Uint256) : Contract Unit -``` - -**Description** +Every primitive is a `Contract α = ContractState → ContractResult α`. Read-only primitives never revert; write primitives return `success ()`; only `require` and `requireSomeUint` (and `revertError`) may emit `ContractResult.revert`. Proof lemmas for every primitive live in `Verity/Core.lean` (one `_run` lemma per primitive) and `Verity/Proofs/Stdlib/Automation.lean` / `Verity/Proofs/Stdlib/MappingAutomation.lean` (`_runState` / `_runValue` mirrors). See [Core Architecture](/core) for the model. -Read/write address-keyed mappings. +## Storage -**Example** +| Function | Type | +|----------|------| +| `getStorage` / `setStorage` | `StorageSlot Uint256 → …` | +| `getStorageAddr` / `setStorageAddr` | `StorageSlot Address → …` | +| `getMapping` / `setMapping` | `StorageSlot (Address → Uint256) → Address → …` | +| `getMappingAddr` / `setMappingAddr` | Address-keyed mapping with address values (`wordToAddress` under the hood) | +| `getMappingUint` / `setMappingUint` | `StorageSlot (Uint256 → Uint256) → Uint256 → …` | +| `getMappingUintAddr` / `setMappingUintAddr` | Uint-keyed mapping with address values | +| `getMapping2` / `setMapping2` | `StorageSlot (Address → Address → Uint256) → Address → Address → …` | +| `getStorageArrayLength` / `getStorageArrayElement` / `setStorageArrayElement` | Dynamic in-storage arrays with `[StorageArrayElem α]` typeclass | +| `pushStorageArray` / `popStorageArray` | Append / remove tail element of an in-storage array | ```verity -let bal <- getMapping balances msgSenderAddr +let bal <- getMapping balances msgSenderAddr +let owner <- getMappingUintAddr tokenOwners tokenId setMapping balances msgSenderAddr (bal - amount) -``` - -**Proof lemmas** - -- `getMapping_run`, `setMapping_run` (`Verity/Core.lean`) -- `getMapping_runState`, `getMapping_runValue`, `setMapping_runState` (`Verity/Proofs/Stdlib/MappingAutomation.lean`) - -### `getMappingUint` / `setMappingUint` -**Signature** - -```verity -def getMappingUint (s : StorageSlot (Uint256 -> Uint256)) (key : Uint256) : Contract Uint256 -def setMappingUint (s : StorageSlot (Uint256 -> Uint256)) (key : Uint256) (value : Uint256) : Contract Unit -``` - -**Description** - -Read/write uint256-keyed mappings. - -**Example** - -```verity -let price <- getMappingUint oraclePrices tokenId -setMappingUint oraclePrices tokenId newPrice -``` - -**Proof lemmas** - -- `getMappingUint_run`, `setMappingUint_run` (`Verity/Core.lean`) -- `getMappingUint_runState`, `getMappingUint_runValue`, `setMappingUint_runState` (`Verity/Proofs/Stdlib/MappingAutomation.lean`) - -### `getMapping2` / `setMapping2` - -**Signature** - -```verity -def getMapping2 (s : StorageSlot (Address -> Address -> Uint256)) (key1 key2 : Address) : Contract Uint256 -def setMapping2 (s : StorageSlot (Address -> Address -> Uint256)) (key1 key2 : Address) (value : Uint256) : Contract Unit -``` - -**Description** - -Read/write double mappings (for example, allowances). - -**Example** - -```verity let allow <- getMapping2 allowances owner spender setMapping2 allowances owner spender (allow - amount) ``` -**Proof lemmas** - -- `getMapping2_run`, `setMapping2_run` (`Verity/Core.lean`) -- `getMapping2_runState`, `getMapping2_runValue`, `setMapping2_runState` (`Verity/Proofs/Stdlib/MappingAutomation.lean`) - -## Control Flow - -### `require` +The `addressToWord` / `wordToAddress` helpers convert between the two representations; the `*Addr` mapping variants apply them automatically. -**Signature** +## Control flow ```verity def require (condition : Bool) (message : String) : Contract Unit +def bind {α β : Type} (ma : Contract α) (f : α → Contract β) : Contract β ``` -**Description** +`require false msg` is the only revert primitive. Use it in place of an explicit `revert`. `bind` short-circuits on revert and powers do-notation. -Guard that reverts when `condition = false`. - -**Example** - -```lean +```verity require (amount > 0) "amount must be nonzero" +let x <- getStorage counterSlot +setStorage counterSlot (x + 1) ``` -**Proof lemmas** - -- `require_true`, `require_false` (`Verity/Core.lean`) -- `require_true_isSuccess`, `require_false_isSuccess` (`Verity/Proofs/Stdlib/Automation.lean`) - -### Revert behavior - -There is no separate `revert` primitive in the core API. Use: - -```lean -require false "error message" -``` - -### `bind` / do-notation - -**Signature** - -```lean -def bind {α β : Type} (ma : Contract α) (f : α -> Contract β) : Contract β -``` - -**Description** - -Monadic sequencing with short-circuit on revert. - -**Example** +### `Contract.tryCatch` ```verity -let x <- getStorage counterSlot -setStorage counterSlot (x + 1) +def Contract.tryCatch {α : Type} (attempt : Contract α) (handler : String → Contract Unit) : Contract α ``` -**Proof lemmas** - -- `Contract.bind_pure_left`, `Contract.bind_pure_right`, `Contract.bind_assoc` (`Verity/Core.lean`) -- `bind_pure_left`, `bind_pure_right`, `bind_assoc` (`Verity/Proofs/Stdlib/Automation.lean`) +If `attempt` reverts with message `msg`, `tryCatch` runs `handler msg` on the state *before* the revert and returns whatever `handler` returns (or the original revert if `handler` itself reverts). Useful for fallback paths inside a contract. See `Verity/Core.lean` for the exact semantics. ### `forEach` -Bounded iteration is available as a language form in the macro/compilation model (`Stmt.forEach`). +Bounded iteration in the compilation-model surface (`Stmt.forEach`). Accumulator-style loops use `Stmt.assignVar` inside `Stmt.forEach`; the macro path currently rejects mutating `let mut` locals from nested `forEach` bodies, so macro-authored contracts should use explicit memory scratch space for accumulators. ```lean forEach "i" count (do @@ -223,74 +74,26 @@ forEach "i" count (do ) ``` -The compilation model supports accumulator-style loops by placing `Stmt.assignVar` -inside `Stmt.forEach`; generated Yul preserves assignment to the outer local. -The `verity_contract` source fallback currently rejects mutating a Lean -`let mut` local from inside the nested `forEach` body term, so macro-authored -contracts should use explicit memory scratch space for loop accumulators until -that executable-path limitation is removed. - -Reference points: - -- `Stmt.forEach` in `Compiler/CompilationModel.lean` -- Macro translation in `Verity/Macro/Translate.lean` - ## Events -### `emitEvent` - -**Signature** - ```verity def emitEvent (name : String) (args : List Uint256) (indexedArgs : List Uint256 := []) : Contract Unit -``` - -**Description** - -Append an event entry to the execution state's event log. - -**Example** -```verity emitEvent "Transfer" [amount] [fromAddr, toAddr] ``` -**Proof lemmas** - -- `emitEvent_run` (`Verity/Core.lean`) -- `emitEvent_runState`, `emitEvent_runValue` (`Verity/Proofs/Stdlib/Automation.lean`) - ## Arithmetic -### Wrapping arithmetic (`Uint256`) - -**Signatures** - -```lean -Verity.EVM.Uint256.add : Uint256 -> Uint256 -> Uint256 -Verity.EVM.Uint256.sub : Uint256 -> Uint256 -> Uint256 -Verity.EVM.Uint256.mul : Uint256 -> Uint256 -> Uint256 -Verity.EVM.Uint256.pow : Uint256 -> Uint256 -> Uint256 -Verity.EVM.Uint256.div : Uint256 -> Uint256 -> Uint256 -Verity.EVM.Uint256.mod : Uint256 -> Uint256 -> Uint256 -``` - -These model EVM modular arithmetic. `pow a b` and `a ^ b` compile to Yul/EVM `exp(a, b)`. +### Wrapping (`Uint256`) -**Example** +`add`, `sub`, `mul`, `pow`, `div`, `mod` — EVM modular arithmetic. `pow a b` / `a ^ b` compiles to Yul `exp(a, b)`. ```lean let z : Uint256 := add x y let scale : Uint256 := pow 10 decimals ``` -**Proof lemmas** - -- `add_eq_of_lt`, `sub_eq_of_le`, `sub_add_cancel` (`Verity/EVM/Uint256.lean`) - -### Checked arithmetic (`Stdlib.Math`) - -**Signatures** +### Checked (`Stdlib.Math`) ```verity def safeAdd (a b : Uint256) : Option Uint256 @@ -299,310 +102,142 @@ def safeMul (a b : Uint256) : Option Uint256 def safeDiv (a b : Uint256) : Option Uint256 def requireSomeUint (opt : Option Uint256) (message : String) : Contract Uint256 -``` -**Example** - -```verity -let sum <- requireSomeUint (safeAdd a b) "overflow" +let sum <- requireSomeUint (safeAdd a b) "overflow" let product <- requireSomeUint (safeMul a b) "overflow" -let quotient <- requireSomeUint (safeDiv a b) "division by zero" +let quot <- requireSomeUint (safeDiv a b) "division by zero" ``` -`verity_contract` lowers `requireSomeUint` over `safeAdd`, `safeSub`, `safeMul`, and `safeDiv` to explicit compiled `require` guards before binding the arithmetic result. Bare `add`, `sub`, `mul`, and `div` remain wrapping EVM arithmetic. +`verity_contract` lowers `requireSomeUint` over `safeAdd`/`Sub`/`Mul`/`Div` to explicit compiled `require` guards. Bare `add`/`sub`/`mul`/`div` stay wrapping. -**Proof lemmas** +### Fixed-point helpers -- `safeAdd_some`, `safeAdd_none`, `safeSub_some`, `safeSub_none`, `safeMul_some`, `safeMul_none`, `safeDiv_some`, `safeDiv_none` (`Verity/Proofs/Stdlib/Math.lean`) -- `requireSomeUint_some`, `requireSomeUint_none` (`Verity/Stdlib/Math.lean`) +In `Stdlib.Math`: `mulDivDown`, `mulDivUp`, `wMulDown`, `wDivUp`, `SNARK_SCALAR_FIELD`, `modField`. Full-precision proof helpers: `mulDiv512Down?`, `mulDiv512Up?` (return `Option Uint256`; `none` on zero divisor or quotient overflow). First-class compiler lowering for a 512-bit division primitive is tracked separately. -### `mulDivDown` / `mulDivUp` / `wMulDown` / `wDivUp` +## Context accessors -Fixed-point helpers live in `Stdlib.Math`: - -```lean -def mulDivDown (a b c : Uint256) : Uint256 - -def mulDivUp (a b c : Uint256) : Uint256 - -def wMulDown (a b : Uint256) : Uint256 - -def wDivUp (a b : Uint256) : Uint256 - -def SNARK_SCALAR_FIELD : Uint256 - -def modField (x : Uint256) : Uint256 +```verity +def msgSender : Contract Address +def contractAddress : Contract Address +def msgValue : Contract Uint256 +def blockTimestamp : Contract Uint256 +def blockNumber : Contract Uint256 +def blobbasefee : Contract Uint256 ``` -**Proof lemmas** +## `verity_contract` authoring surface -- `mulDivDown_nat_eq`, `mulDivUp_nat_eq`, `mulDivDown_le_mulDivUp`, `mulDivDown_antitone_divisor`, `mulDivUp_antitone_divisor`, `mulDivDown_comm`, `mulDivUp_comm`, `wMulDown_comm` (`Verity/Proofs/Stdlib/Math.lean`) -- `SNARK_SCALAR_FIELD_val`, `modField_def` (`Verity/Stdlib/Math.lean`) -- BN254 field lemmas: `SNARK_SCALAR_FIELD_ne_zero`, `SNARK_SCALAR_FIELD_lt_modulus`, `modField_nat_eq`, `modField_lt`, `modField_zero`, `modField_SNARK_SCALAR_FIELD`, `modField_eq_zero_iff`, `modField_eq_of_nat_mod_eq`, `modField_eq_iff_nat_mod_eq`, `modField_eq_self_of_lt`, `modField_nat_mod_eq`, `modField_idempotent` (`Verity/Proofs/Stdlib/Math.lean`) -- Rounding-gap lemmas: `mulDivUp_le_mulDivDown_add_one`, `mulDivUp_eq_mulDivDown_or_succ`, `mulDivUp_eq_mulDivDown_of_dvd`, `mulDivUp_eq_mulDivDown_add_one_of_not_dvd` (`Verity/Proofs/Stdlib/Math.lean`) -- Positivity lemmas: `mulDivDown_pos`, `mulDivUp_pos`, `wMulDown_pos`, `wDivUp_pos` (`Verity/Proofs/Stdlib/Math.lean`) -- Zero-case lemmas: `mulDivDown_zero_left/right`, `mulDivUp_zero_left/right`, `wMulDown_zero_left/right`, `wDivUp_zero` (`Verity/Proofs/Stdlib/Math.lean`) -- Exact cancellation and wad identity lemmas: `mulDivDown_cancel_right/left`, `mulDivUp_cancel_right/left`, `wMulDown_one_left/right`, `wDivUp_by_wad` (`Verity/Proofs/Stdlib/Math.lean`) -- Wad-specialized helper lemmas: `wMulDown_nat_eq`, `wDivUp_nat_eq`, `wDivUp_antitone_right` (`Verity/Proofs/Stdlib/Math.lean`) +### Local obligations -### Full-precision `mulDiv512` - -Proof/modeling helpers for Solidity `Math.mulDiv` / `FullMath.mulDiv` -semantics live in `Stdlib.Math`: - -```lean -def mulDiv512Down? (a b c : Uint256) : Option Uint256 - -def mulDiv512Up? (a b c : Uint256) : Option Uint256 +```verity +function unsafeEdge () + local_obligations [manual_delegatecall_refinement := assumed "Caller proves the handwritten assembly path."] + : Unit := do + pure () ``` -These compute `a * b` in unbounded natural-number precision and return `none` -only when the divisor is zero or the final floor/ceil quotient does not fit in -`uint256`. They are EDSL proof helpers; first-class compiler lowering for a -512-bit division primitive remains tracked separately. +Each entry lowers into `localObligations`, surfaces in `--trust-report`, and participates in `--deny-local-obligations`. Direct assembly-shaped primitives (raw low-level calls, returndata forwarding, manual memory/calldata) without a local obligation fail closed. -**Proof lemmas** +### Same-contract helpers -- Fit/rejection lemmas: `mulDiv512Down?_some`, `mulDiv512Down?_none_of_zero_divisor`, `mulDiv512Down?_none_of_overflow`, `mulDiv512Down?_isSome_iff`, `mulDiv512Down?_isNone_iff`, `mulDiv512Up?_some`, `mulDiv512Up?_none_of_zero_divisor`, `mulDiv512Up?_none_of_overflow`, `mulDiv512Up?_isSome_iff`, `mulDiv512Up?_isNone_iff` (`Verity/Proofs/Stdlib/Math.lean`) -- Result-characterization lemmas: `mulDiv512Down?_eq_some_iff`, `mulDiv512Up?_eq_some_iff` (`Verity/Proofs/Stdlib/Math.lean`) -- Sandwich lemmas: `mulDiv512Down?_mul_le`, `mulDiv512Down?_lt_succ_mul`, `mulDiv512Down?_mul_lt_add`, `mulDiv512Up?_mul_ge`, `mulDiv512Up?_mul_le_add_pred`, `mulDiv512Up?_mul_lt_add` (`Verity/Proofs/Stdlib/Math.lean`) -- Compatibility lemmas: `mulDiv512Down?_eq_mulDivDown_of_no_overflow`, `mulDiv512Up?_eq_mulDivUp_of_no_overflow` (`Verity/Proofs/Stdlib/Math.lean`) -- Rounding and shape lemmas: `mulDiv512Down?_comm`, `mulDiv512Up?_comm`, `mulDiv512Down?_monotone_left/right`, `mulDiv512Up?_monotone_left/right`, `mulDiv512Down?_antitone_divisor`, `mulDiv512Up?_antitone_divisor`, `mulDiv512Down?_isSome_of_up_isSome`, `mulDiv512Up?_isNone_of_down_isNone`, `mulDiv512Down?_le_up`, `mulDiv512Up?_le_down_add_one`, `mulDiv512Up?_eq_down_or_succ`, `mulDiv512Up?_eq_down_of_dvd`, `mulDiv512Up?_some_succ_of_not_dvd`, `mulDiv512Down?_pos`, `mulDiv512Up?_pos`, `mulDiv512Down?_zero_left/right`, `mulDiv512Up?_zero_left/right`, `mulDiv512Down?_cancel_right/left`, `mulDiv512Up?_cancel_right/left` (`Verity/Proofs/Stdlib/Math.lean`) -- Automation mirrors: `mulDiv512Down?_some_iff`, `mulDiv512Down?_none_iff`, `mulDiv512Up?_some_iff`, `mulDiv512Up?_none_iff` (`Verity/Proofs/Stdlib/Automation.lean`) - -## Same-Contract Helper Calls - -Inside `verity_contract`, call reusable same-contract helpers with ordinary function-call syntax. Do not write `internalCall` or `internalCallAssign` in source contracts; those names are compilation-model IR constructors used after macro lowering. +Call helpers with ordinary function-call syntax — do not write `internalCall` directly (those are post-lowering IR nodes). ```verity -verity_contract HelperExample where - storage - total : Uint256 := slot 0 - - function bump (x : Uint256) : Uint256 := do - return add x 1 - - function storeBump (x : Uint256) : Unit := do - let y ← bump x - setStorage total y - - function applyBump (x : Uint256) : Unit := do - storeBump x -``` - -Use the same direct-call form for helpers that return no value, one value, or a static tuple: - -```lean storeBump x let y ← bump x let (assets, shares) ← preview seed ``` -The macro lowers effect-only helper calls such as `storeBump x` to `Stmt.internalCall`, helper result bindings such as `let y ← bump x` to `Stmt.internalCallAssign`, and expression-position helper calls to `Expr.internalCall`. Those IR nodes are useful when writing `CompilationModel` values by hand, but direct helper-call syntax is the supported `verity_contract` authoring surface. - -Direct helper lowering supports the source shapes used by ordinary same-contract -helpers, including scalar parameters, static tuple/struct payloads, and direct -`Bytes` / dynamic-array parameter forwarding when those values come from the -caller ABI. Dynamic returns still use the explicit supported return surfaces: -single static values, static tuples via `return (..)`, and byte payloads through -the dedicated bytes return path. - -For Solidity helper boundaries that include calldata-shaped dynamic payloads, -preserve the helper when possible: - -```verity -function transferWithBalanceCheck - (permit : PermitTransferFrom, depositor : Address, signature : Bytes, - totalAmount : Uint256, witness : Bytes32) : Unit := do - ... -``` - -## Tuple Surface +The macro lowers effect-only calls to `Stmt.internalCall`, result bindings to `Stmt.internalCallAssign`, expression-position calls to `Expr.internalCall`. Supports scalar parameters, static tuples/structs, direct `Bytes`/dynamic-array forwarding from caller ABI. Dynamic returns use explicit return surfaces only. -`verity_contract` now accepts tuple-shaped local sugar for the static tuple cases already supported by the compilation model: +### Tuple sugar ```lean let (first, second) := pair let (_, second) := pair -let (lhs, rhs) := (seed, add seed 1) -let (assets, shares) := preview seed let (assets, shares) ← preview seed let (supply, borrow, delegate_) := structMembers positions user [supplyShares, borrowShares, delegate] return (first, second) -return structMembers2 approvals owner spender [allowance, nonce] ``` -Today this elaborates cleanly for tuple literals, tuple-typed parameters, internal helper multi-returns via either `let (...) := helper ...` or `let (...) ← helper ...`, and storage-backed mapping-struct reads via `structMembers` / `structMembers2`. `_` binders are accepted inside tuple destructuring and are discarded hygienically instead of entering scope. `return (..)` lowers to `Stmt.returnValues [...]`, tuple-parameter destructuring maps onto the ABI-flattened component names (`pair_0`, `pair_1`, ...), helper-call destructuring lowers to `Stmt.internalCallAssign [...]`, and struct-backed destructuring lowers to explicit `Expr.structMember` / `Expr.structMember2` reads, so the generated model stays explicit for debugging and proofs. - -For executable Lean definitions generated by `verity_contract`, tuple-typed parameters now stay tuple-shaped as right-nested Lean products instead of being erased to `Unit`. The same ABI-flattened component aliases are also injected into the executable body, so a parameter such as `pair : Tuple [Uint256, Uint256]` can be referenced directly as `pair_0` / `pair_1` inside the contract body without dropping back to manual destructuring. +Tuple-typed parameters stay shape-preserved as right-nested Lean products; ABI-flattened aliases (`pair_0`, `pair_1`, …) are injected so you can use them directly. `_` binders are accepted and discarded hygienically. -## Stateless Contracts - -`verity_contract` now accepts an empty `storage` block when a contract is purely functional or only depends on ambient values such as `msg.sender`: +### Stateless contracts and payable / initializer constructors ```verity verity_contract Stateless where - storage - - function echoWord (value : Uint256) : Uint256 := do - return value + storage -- empty block is allowed function whoAmI () : Address := do let sender ← msgSender return sender ``` -This keeps the macro surface usable for helper-style and interface-shaped contracts without forcing a dummy storage slot. The generated `CompilationModel.fields` list is empty, ABI generation still works normally, and selectors remain computed from the external functions exactly as before. - -Constructors can also be marked payable directly in the macro surface: - ```verity -verity_contract PayableInit where - storage - owner : Address := slot 0 - - constructor (seedOwner : Address) payable := do - setStorageAddr owner seedOwner - - function getOwner () : Address := do - let currentOwner ← getStorageAddr owner - return currentOwner +constructor (seedOwner : Address) payable := do + setStorageAddr owner seedOwner ``` -This sets `spec.constructor.isPayable := true`, emits constructor ABI `stateMutability: "payable"`, and removes the deploy-time `callvalue` guard from generated Yul. - -Upgradeable-style initialization can also be guarded directly from the macro surface using an explicit version slot: +`payable` removes the `callvalue` guard and emits `stateMutability: "payable"` in the ABI. ```verity -verity_contract UpgradeableConfig where - storage - initializedVersion : Uint256 := slot 0 - owner : Address := slot 1 - paused : Uint256 := slot 2 - - function initOwner (seedOwner : Address) initializer(initializedVersion) : Unit := do - setStorageAddr owner seedOwner - - function upgradeToV2 () reinitializer(initializedVersion, 2) : Unit := do - setStorage paused 1 +function initOwner (seedOwner : Address) initializer(initializedVersion) : Unit := ... +function upgradeToV2 () reinitializer(initializedVersion, 2) : Unit := ... ``` -`initializer(versionSlot)` prepends `require(versionSlot == 0, "initializer already run")` and then stores `1` into that slot before the user body runs. `reinitializer(versionSlot, n)` similarly requires the tracked version to be strictly less than `n`, then stores `n` before running the body. The guard slot must be a user-declared `Uint256` storage field, which keeps layout and proof state explicit instead of hiding upgrade metadata in an implicit slot. - -## Contract Constants +`initializer(slot)` prepends `require(slot == 0, ...)` then stores `1`. `reinitializer(slot, n)` requires the tracked version `< n`, then stores `n`. Guard slots must be user-declared `Uint256` fields. -`verity_contract` also supports contract-scoped compile-time constants that are shared between the executable fallback and the generated compilation model: +### Constants and immutables ```verity -verity_contract FeeConfig where - storage - - constants - basisPoints : Uint256 := 10000 - mintFeeBps : Uint256 := 30 - treasury : Address := (wordToAddress 42) - - function feeOn (amount : Uint256) : Uint256 := do - let fee := div (mul amount mintFeeBps) basisPoints - return fee +constants + basisPoints : Uint256 := 10000 + mintFeeBps : Uint256 := 30 + treasury : Address := (wordToAddress 42) - function treasuryAddr () : Address := do - return treasury +immutables + seededSupply : Uint256 := add seed offset + treasury : Address := ownerSeed + paused : Bool := true + feeBps : Uint8 := 7 + domainTag : Bytes32 := 42 ``` -These declarations elaborate to ordinary Lean `def`s inside the generated contract namespace, so the executable path can reference them directly. On the compilation-model side, constant identifiers are inlined into `Expr` trees transitively, while ordinary parameter/local shadowing still wins if a function binds the same name later. +Constants inline into `Expr` trees at compile time; constant bodies cannot reference runtime builtins (`blockTimestamp`, calldata reads, low-level opcodes, etc.) — those are rejected at elaboration. Immutables lower to read-only `__immutable_` slots seeded in the constructor. Supported immutable types: `Uint256`, `Uint8`, `Address`, `Bytes32`, `Bool`. -Constant bodies must stay compile-time-only. Runtime-dependent builtins such as `blockTimestamp`, `blockNumber`, `blobbasefee`, `contractAddress`, `chainid`, calldata/returndata size reads, and low-level memory/call opcodes are rejected in `constants` declarations so the executable and compilation-model paths cannot diverge. +Storage, constants, immutables, and functions share one namespace; duplicate or cross-kind reuse is rejected with explicit diagnostics. Generated names (`spec`, `_modelBody`, `_model`, `_bridge`, `_semantic_preservation`) are reserved. -Storage fields, constants, and functions also share the generated Lean namespace for a `verity_contract`. Duplicate declarations or cross-kind name reuse such as `owner` as both a storage field and a constant are rejected during macro elaboration with explicit diagnostics instead of falling through to raw duplicate-definition errors from Lean. Generated declarations are reserved too: `spec` and the per-function helpers `_modelBody`, `_model`, `_bridge`, and `_semantic_preservation` cannot be reused by contract declarations. - -## Contract Immutables - -`verity_contract` also supports contract-scoped immutables for deployment-time values that should become read-only at runtime: +### Linked externals ```verity -verity_contract ImmutableConfig where - storage - owner : Address := slot 0 - - constants - offset : Uint256 := 2 - - immutables - seededSupply : Uint256 := add seed offset - treasury : Address := ownerSeed - paused : Bool := true - feeBps : Uint8 := 7 - domainTag : Bytes32 := 42 +linked_externals + external echo(Uint256) -> (Uint256) - constructor (seed : Uint256, ownerSeed : Address) := do - setStorageAddr owner ownerSeed - - function supplyCap () : Uint256 := do - return seededSupply - - function treasuryAddr () : Address := do - return treasury - - function isPaused () : Bool := do - return paused +function storeQuote (value : Uint256) : Unit := do + let quoted := externalCall "echo" [value] + setStorage lastQuote quoted ``` -In this parity slice, immutables are lowered to internal read-only slots named `__immutable_`. `Uint256`, `Uint8`, `Bytes32`, and `Bool` immutables use word-backed hidden storage slots, while `Address` immutables keep the address-typed executable accessor. Constructor initialization is prepended automatically in the generated compilation-model constructor, and runtime functions load those slots into local bindings before the user body runs. Function parameters still shadow immutable names normally, and contracts with `immutables` but no explicit `constructor` receive a synthetic zero-argument constructor that seeds the immutable slots. - -Immutable names must be unique within the `immutables` block and must not reuse a storage-field or contract-constant name. That keeps runtime name resolution unambiguous across the executable fallback and the generated compilation model. +Populates `spec.externals` with assumed foreign signatures. Single-word argument/return types only (`Uint256`, `Uint8`, `Address`, `Bytes32`, `Bool`); at most one return. Dynamic and tuple-shaped linked externals are rejected at elaboration. -Immutable initializer bodies are also elaborated against the declared executable-facing type before translation. That means obviously ill-typed declarations such as `Uint256 := true` or `Address := true` are rejected up front instead of silently compiling into a mismatched spec. - -The current surface supports `Uint256`, `Uint8`, `Address`, `Bytes32`, and `Bool` immutables. Dynamic types still stay out of scope so the executable fallback and the compilation model remain aligned without pretending the repository already has native bytecode-embedded immutable lowering. - -## Linked Externals - -`verity_contract` can now declare linked external functions directly and use them from `externalCall` expressions: - -```verity -verity_contract LinkedOracle where - storage - lastQuote : Uint256 := slot 0 - - linked_externals - external echo(Uint256) -> (Uint256) - - function storeQuote (value : Uint256) : Unit := do - let quoted := externalCall "echo" [value] - setStorage lastQuote quoted -``` - -These declarations populate `spec.externals` with assumed foreign signatures so the existing compilation-model validation for `Expr.externalCall` works from the macro surface too. This first slice is intentionally narrow: it covers linked external declarations plus `externalCall` expression lowering, while richer statement-style bindings and ECM module declarations still remain separate follow-up work. - -On the executable Lean path, this surface is currently limited to single-word argument and return types: `Uint256`, `Uint8`, `Address`, `Bytes32`, and `Bool`, with at most one return value. Dynamic values (`String`, `Bytes`, arrays) and tuple-shaped linked externals are still rejected at macro elaboration time instead of falling through to opaque instance-resolution failures from the runtime stub, and multi-return linked externals remain deferred until statement-style external bindings are exposed from `verity_contract`. - -## Low-Level Log Surface - -`verity_contract` bodies can emit low-level runtime-dependent logs directly: +### Raw log surface ```lean rawLog [topic0, add topic1 1] dataOffset dataSize ``` -`rawLog topics dataOffset dataSize` lowers to `Stmt.rawLog topics dataOffset dataSize`. Both the compiler and the executable fallback currently support 0 to 4 topics only (`log0` to `log4`); larger topic lists are rejected. On the executable path, successful calls append a low-level trace entry shaped like `{ name := "logN", args := [dataOffset, dataSize], indexedArgs := topics }`, so macro-authored contracts can round-trip observable log behavior instead of only compiling it. +Lowers to `Stmt.rawLog`. Supports 0–4 topics (`log0`–`log4`). Classified as not-modeled event emission in the trust report — use `--deny-event-emission` for proof-strict runs. -`rawLog` also remains outside the current proved interpreter semantics: the compiler lowers it directly, but the trust report still classifies it as not-modeled event emission rather than a fully proved event primitive. When it appears, archive `--trust-report` and use `--deny-event-emission` for proof-strict runs. - -## Transient Storage Surface - -`verity_contract` now exposes the EIP-1153 transient storage builtins directly: +### Transient storage (EIP-1153) ```lean tstore slot value let warmed := tload slot ``` -`tstore slot value` lowers to `Stmt.tstore slot value`, and `tload slot` lowers to `Expr.tload slot`. The generated Yul uses the native `tstore(...)` / `tload(...)` builtins, and the trust report classifies them under `lowLevelMechanics` instead of hiding them behind ordinary storage reads/writes. On the executable path, `Contracts/Common.lean` keeps a separate `ContractState.transientStorage` map so transient reads do not alias persistent storage slots. +Lowers to `Stmt.tstore` / `Expr.tload`. The executable path keeps a separate `ContractState.transientStorage` map. Classified under `lowLevelMechanics` in the trust report. -## Dynamic Array Surface - -Dynamic array parameters can be consumed directly from `verity_contract` bodies using the same helper names that lower into the compilation model: +### Dynamic arrays ```lean let count := arrayLength recipients @@ -610,13 +245,15 @@ let first := arrayElement recipients 0 returnArray amounts ``` -`arrayLength arr` lowers to `Expr.arrayLength "arr"`, `arrayElement arr idx` lowers to `Expr.arrayElement "arr" idx`, and `returnArray arr` lowers to `Stmt.returnArray "arr"`. `arrayElement` supports word-sized scalar arrays and the ABI-decodable static/nested struct-array shapes used by Solidity calldata structs. Dynamic members inside a struct element should be accessed through field projection plus `arrayLength` / `arrayElement` on that member rather than treating the member as a scalar word. Dynamic-element arrays such as `Array Bytes` and `Array String` still support `arrayLength`, but indexed element reads and direct `returnArray` lowering are rejected until the compiler grows offset-aware element lowering for those payloads. `arrayElement` remains bounds-checked on the compiled path, and the executable fallback in `Contracts/Common.lean` now mirrors that by reverting on out-of-range indices instead of silently defaulting. +`arrayElement` is bounds-checked (compiled path reverts on out-of-range; executable fallback mirrors). Supports scalar arrays and ABI-decodable static/nested struct arrays. Dynamic-element arrays (`Array Bytes`, `Array String`) support `arrayLength` only; indexed reads and `returnArray` are rejected for those until offset-aware lowering lands. + +`String`/`Bytes` support ABI transport (`returnBytes`, custom-error/event payloads, parameter flow) and direct `==`/`!=` checks. Other word-level operators (`<`, `add`, `logicalAnd`) on `String`/`Bytes` are rejected — applies to function bodies, constructor bodies, constants, and immutable initializers. -String and bytes values remain intentionally bounded. ABI transport is supported (`returnBytes`, custom-error payloads, event payloads, parameter flow), and direct parameter `==` / `!=` checks lower through the dynamic-bytes equality helper. Other word-level operators such as `<`, `add`, or the numeric `logicalAnd` helpers still remain restricted to Bool or word-backed scalar values, and dynamic local aliases are still rejected on the compilation-model path, so unsupported `String` / `Bytes` expressions fail fast at macro elaboration time instead of silently lowering to bogus word comparisons. That validation applies uniformly to function bodies, constructor bodies, contract constants, and immutable initializers. +### Modifiers, structs, ADTs, and namespaced storage -## Custom Errors +`verity_contract` also supports Solidity-style **modifiers** (`modifier onlyRelayer := do ...` then `with onlyRelayer`), **struct declarations** (including packed storage structs via `@word N packed(byteOffset, byteWidth)`), **algebraic data types**, **newtype wrappers**, **storage namespaces** (`storage_namespace erc7201 "myapp.storage.X"`), and **mapping-of-struct** sugar (`MappingStruct`, `MappingStruct2`). The full grammar lives in [`Verity/Macro/Syntax.lean`](https://github.com/lfglabs-dev/verity/blob/main/Verity/Macro/Syntax.lean); concrete usage shapes are in the [production Solidity patterns guide](/guides/production-solidity-patterns). -`verity_contract` now accepts custom error declarations and threads them into the generated `CompilationModel`/ABI surface: +### Custom errors ```verity errors @@ -631,77 +268,15 @@ function rejectLarge (amount : Uint256) : Unit := do revert AmountTooLarge(amount, 100) ``` -These declarations populate `CompilationModel.errors`, and the macro now lowers guarded and unconditional custom-error exits to `Stmt.requireError` / `Stmt.revertError`. That keeps `#check_contract`, ABI generation, and the Yul compiler on the same custom-error surface authored in the macro contract. +Populates `CompilationModel.errors`; guarded and unconditional custom-error exits lower to `Stmt.requireError` / `Stmt.revertError`. ## External Calls (ECM) -### ERC-20 safe wrappers - -`ecmTransfer`/`ecmTransferFrom` naming is superseded by standard modules: - -```lean -def Compiler.Modules.ERC20.safeTransfer (token to amount : Expr) : Stmt -def Compiler.Modules.ERC20.safeTransferFrom (token fromAddr to amount : Expr) : Stmt -def Compiler.Modules.ERC20.balanceOf - (resultVar : String) (token owner : Expr) : Stmt -def Compiler.Modules.ERC20.allowance - (resultVar : String) (token owner spender : Expr) : Stmt -def Compiler.Modules.ERC20.totalSupply - (resultVar : String) (token : Expr) : Stmt -def Compiler.Modules.ERC4626.previewDeposit - (resultVar : String) (vault assets : Expr) : Stmt -def Compiler.Modules.ERC4626.previewMint - (resultVar : String) (vault shares : Expr) : Stmt -def Compiler.Modules.ERC4626.previewWithdraw - (resultVar : String) (vault assets : Expr) : Stmt -def Compiler.Modules.ERC4626.previewRedeem - (resultVar : String) (vault shares : Expr) : Stmt -def Compiler.Modules.ERC4626.convertToAssets - (resultVar : String) (vault shares : Expr) : Stmt -def Compiler.Modules.ERC4626.convertToShares - (resultVar : String) (vault assets : Expr) : Stmt -def Compiler.Modules.ERC4626.totalAssets - (resultVar : String) (vault : Expr) : Stmt -def Compiler.Modules.ERC4626.asset - (resultVar : String) (vault : Expr) : Stmt -def Compiler.Modules.ERC4626.maxDeposit - (resultVar : String) (vault receiver : Expr) : Stmt -def Compiler.Modules.ERC4626.maxMint - (resultVar : String) (vault receiver : Expr) : Stmt -def Compiler.Modules.ERC4626.maxWithdraw - (resultVar : String) (vault owner : Expr) : Stmt -def Compiler.Modules.ERC4626.maxRedeem - (resultVar : String) (vault owner : Expr) : Stmt -def Compiler.Modules.ERC4626.deposit - (resultVar : String) (vault assets receiver : Expr) : Stmt -def Compiler.Modules.Oracle.oracleReadUint256 - (resultVar : String) (target : Expr) (selector : Nat) - (staticArgs : List Expr) : Stmt -def Compiler.Modules.Precompiles.sha256Memory - (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt -def Compiler.Modules.Precompiles.sha256 - (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt -def Compiler.Modules.Calls.bubblingValueCall - (target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt -def Compiler.Modules.Calls.bubblingValueCallNoOutput - (target value inputOffset inputSize : Expr) : Stmt -def Compiler.Modules.Hashing.abiEncodePackedWords - (resultVar : String) (words : List Expr) : Stmt -def Compiler.Modules.Hashing.abiEncodePacked - (resultVar : String) (words : List Expr) : Stmt -def Compiler.Modules.Hashing.sha256PackedWords - (resultVar : String) (words : List Expr) : Stmt -def Compiler.Modules.Hashing.sha256Packed - (resultVar : String) (words : List Expr) : Stmt -def Compiler.Modules.Hashing.abiEncodePackedStaticSegments - (resultVar : String) (segments : List (Expr × Nat)) : Stmt -def Compiler.Modules.Hashing.sha256PackedStaticSegments - (resultVar : String) (segments : List (Expr × Nat)) : Stmt -``` +External calls are modeled as **Externally Callable Modules** (ECMs) — statement constructors that ABI-encode arguments, perform a `call` / `staticcall`, validate the return shape, and bind the result word. They carry explicit trust-report metadata; module-level `axioms` apply rather than pure `simp`-style contract lemmas. -These are emitted as `Stmt.ecm ...` with explicit module metadata and trust assumptions. +### ERC-20 helpers -Inside `verity_contract` bodies, the standard ERC-20 helper names lower directly too: +Inside `verity_contract` bodies, the standard names lower directly: ```lean safeTransfer token to amount @@ -710,173 +285,91 @@ safeApprove token spender amount let balance <- balanceOf token owner let current <- allowance token owner spender -let supply <- totalSupply token +let supply <- totalSupply token ``` -Those forms compile to the corresponding `Compiler.Modules.ERC20.*Module` ECMs, so macro-only contracts can use the common token wrapper surface without dropping back to handwritten `CompilationModel` specs. - -If the contract already defines a same-named function with the matching arity, the macro now rejects the direct ERC-20 helper form instead of silently reinterpreting it. That keeps `balanceOf` / `safeTransfer` helper syntax reserved for ECM lowering and avoids ambiguous model generation. - -### Low-level `tryCatch` - -`verity_contract` also accepts a low-level `tryCatch` do-element for call-style expressions that return a success word: - -```verity -tryCatch (call gas target value inOffset inSize outOffset outSize) (do - setStorage lastFailure 1) -``` +These compile to `Compiler.Modules.ERC20.*Module` ECMs. If the contract defines a same-named function with matching arity, the helper form is rejected to avoid ambiguity. -On the compilation-model path, this lowers to a synthetic `letVar` followed by an `ite` that enters the catch block when the result word is `0`. This currently covers low-level call-like expressions only. Higher-level external-call helpers / ECMs are still outside this surface, and catch-payload decoding is not modeled yet, so any named handler argument must currently be ignored. +### ERC-4626 vault helpers -### Generic external call with return value +Twelve ECMs share one template: ABI-encode the selector + static args, `staticcall` (or `call` for state-changing), expect one 32-byte return word, bind it. ```lean -def Compiler.Modules.Calls.withReturn - (resultVar : String) (target : Expr) (selector : Nat) - (args : List Expr) (isStatic : Bool := false) : Stmt +Compiler.Modules.ERC4626.previewDeposit (resultVar : String) (vault assets : Expr) : Stmt +Compiler.Modules.ERC4626.previewMint (resultVar : String) (vault shares : Expr) : Stmt +Compiler.Modules.ERC4626.previewWithdraw (resultVar : String) (vault assets : Expr) : Stmt +Compiler.Modules.ERC4626.previewRedeem (resultVar : String) (vault shares : Expr) : Stmt +Compiler.Modules.ERC4626.convertToAssets (resultVar : String) (vault shares : Expr) : Stmt +Compiler.Modules.ERC4626.convertToShares (resultVar : String) (vault assets : Expr) : Stmt +Compiler.Modules.ERC4626.totalAssets (resultVar : String) (vault : Expr) : Stmt +Compiler.Modules.ERC4626.asset (resultVar : String) (vault : Expr) : Stmt +Compiler.Modules.ERC4626.maxDeposit (resultVar : String) (vault receiver : Expr) : Stmt +Compiler.Modules.ERC4626.maxMint (resultVar : String) (vault receiver : Expr) : Stmt +Compiler.Modules.ERC4626.maxWithdraw (resultVar : String) (vault owner : Expr) : Stmt +Compiler.Modules.ERC4626.maxRedeem (resultVar : String) (vault owner : Expr) : Stmt +Compiler.Modules.ERC4626.deposit (resultVar : String) (vault assets receiver : Expr) : Stmt ``` -### `keccak256` primitive +`asset` masks the returned word to 160 bits. `deposit` uses `call` (state-changing). Each module records a corresponding `erc4626__interface` assumption in the trust report. -`verity_contract` can hash a memory slice directly: +### Precompiles and hashing ```lean -let digest := keccak256 offset size +Compiler.Modules.Precompiles.ecrecover -- `let signer <- ecrecover digest v r s` in macro surface +Compiler.Modules.Precompiles.sha256Memory -- aliased as `sha256` +Compiler.Modules.Hashing.abiEncodePackedWords -- contiguous-word keccak256 +Compiler.Modules.Hashing.sha256PackedWords -- contiguous-word SHA-256 via 0x02 +Compiler.Modules.Hashing.abiEncodePackedStaticSegments -- mixed widths, 1–32 bytes each +Compiler.Modules.Hashing.sha256PackedStaticSegments ``` -This elaborates to `Compiler.CompilationModel.Expr.keccak256` and lowers to the Yul `keccak256(offset, size)` builtin. The machine-readable trust report records the explicit primitive assumption `keccak256_memory_slice_matches_evm`. - -`Expr.keccak256` also remains an explicit proof boundary today: the compiler supports it directly, but the current proof stack still treats it as an axiomatized primitive instead of a fully modeled operation. When it appears, archive `--trust-report` and use `--deny-axiomatized-primitives` for proof-strict runs (see issue `#1411`). - -### Static-word packed hashing - -For packed preimages where each item is already a full 32-byte word, use the -standard hashing ECMs instead of open-coded offset arithmetic: - ```verity -Compiler.Modules.Hashing.abiEncodePackedWords - "digest" +Compiler.Modules.Hashing.abiEncodePackedWords "digest" [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"] - -Compiler.Modules.Hashing.sha256PackedWords - "publicSignalDigest" - [Expr.param "root", Expr.param "contextHash"] ``` -These helpers lower to contiguous `mstore` calls starting at scratch memory -offset zero. The shorter `abiEncodePacked` and `sha256Packed` names are aliases -for the same static-word semantics. `abiEncodePackedWords` binds -`keccak256(0, wordCount * 32)`; `sha256PackedWords` calls precompile `0x02`, -reverts on precompile failure, and binds the digest word. +Segment widths in 1–32 bytes; sub-word values are left-aligned. Dynamic `bytes`/`string` packed encoding stays outside this core surface. Trust report records `evm_ecrecover_precompile`, `evm_sha256_precompile`, etc. -For static mixed-width preimages, use explicit byte-width segment helpers: +### Oracle and generic calls -```verity -Compiler.Modules.Hashing.abiEncodePackedStaticSegments - "digest" - [(Expr.param "who", 20), (Expr.param "amount", 32)] +```lean +Compiler.Modules.Oracle.oracleReadUint256 + (resultVar : String) (target : Expr) (selector : Nat) (staticArgs : List Expr) : Stmt -Compiler.Modules.Hashing.sha256PackedStaticSegments - "publicSignalDigest" - [(Expr.param "who", 20), (Expr.param "contextHash", 32)] -``` +Compiler.Modules.Calls.withReturn + (resultVar : String) (target : Expr) (selector : Nat) (args : List Expr) (isStatic : Bool := false) : Stmt -Segment widths must be between 1 and 32 bytes. Sub-word values are left-aligned -before `mstore`, and later segments are placed at byte-precise offsets. Dynamic -`bytes` and `string` packed encoding remains outside this core helper surface. +Compiler.Modules.Calls.bubblingValueCall + (target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt +``` -### `ecrecover` precompile +`Oracle.oracleReadUint256` is the standard read-only oracle case; trust-report assumption `oracle_read_uint256_interface`. -`verity_contract` can bind the standard `ecrecover` precompile directly: +### `keccak256` primitive ```lean -let signer <- ecrecover digest v r s +let digest := keccak256 offset size ``` -This elaborates to `Compiler.Modules.Precompiles.ecrecoverModule` and the trust report records the explicit assumption `evm_ecrecover_precompile`. - -`Compiler.Modules.Precompiles.sha256Memory` covers SHA-256 over an existing -memory slice. The shorter `Compiler.Modules.Precompiles.sha256` name is an -alias for the same ECM. It emits precompile `0x02`, reverts on precompile -failure, binds `mload(outputOffset)`, and records the explicit assumption -`evm_sha256_precompile`. - -`Compiler.Modules.Oracle.oracleReadUint256` covers the common read-only oracle case: it ABI-encodes the selector plus static arguments, performs a `staticcall`, requires exactly one 32-byte return word, and binds that word to a local result variable. The trust report records the explicit ECM assumption `oracle_read_uint256_interface`. - -`Compiler.Modules.ERC20.balanceOf` covers the common token-balance read case: it ABI-encodes `balanceOf(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned balance word to a local result variable. The trust report records the explicit ECM assumption `erc20_balanceOf_interface`. - -`Compiler.Modules.ERC20.allowance` covers the common ERC-20 allowance read case: it ABI-encodes `allowance(address,address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned allowance word to a local result variable. The trust report records the explicit ECM assumption `erc20_allowance_interface`. - -`Compiler.Modules.ERC20.totalSupply` covers the common ERC-20 aggregate-supply read case: it ABI-encodes `totalSupply()`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned supply word to a local result variable. The trust report records the explicit ECM assumption `erc20_totalSupply_interface`. +Elaborates to `Expr.keccak256`; lowers to Yul `keccak256(offset, size)`. The machine-readable trust report records the explicit primitive assumption `keccak256_memory_slice_matches_evm`. -`Compiler.Modules.ERC4626.previewDeposit` covers the common vault preview case: it ABI-encodes `previewDeposit(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned share quote to a local result variable. The trust report records the explicit ECM assumption `erc4626_previewDeposit_interface`. - -`Compiler.Modules.ERC4626.previewMint` covers the complementary mint-quote case: it ABI-encodes `previewMint(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset quote to a local result variable. The trust report records the explicit ECM assumption `erc4626_previewMint_interface`. - -`Compiler.Modules.ERC4626.previewWithdraw` covers the asset-withdrawal quote case: it ABI-encodes `previewWithdraw(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned share quote to a local result variable. The trust report records the explicit ECM assumption `erc4626_previewWithdraw_interface`. - -`Compiler.Modules.ERC4626.previewRedeem` covers the complementary redeem-quote case: it ABI-encodes `previewRedeem(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset quote to a local result variable. The trust report records the explicit ECM assumption `erc4626_previewRedeem_interface`. - -`Compiler.Modules.ERC4626.convertToAssets` covers the canonical share-to-asset conversion case: it ABI-encodes `convertToAssets(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset amount to a local result variable. The trust report records the explicit ECM assumption `erc4626_convertToAssets_interface`. - -`Compiler.Modules.ERC4626.convertToShares` covers the canonical asset-to-share conversion case: it ABI-encodes `convertToShares(uint256)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned share amount to a local result variable. The trust report records the explicit ECM assumption `erc4626_convertToShares_interface`. - -`Compiler.Modules.ERC4626.totalAssets` covers the canonical vault-assets aggregate case: it ABI-encodes `totalAssets()`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset total to a local result variable. The trust report records the explicit ECM assumption `erc4626_totalAssets_interface`. - -`Compiler.Modules.ERC4626.asset` covers the canonical underlying-asset getter case: it ABI-encodes `asset()`, performs a `staticcall`, requires exactly one 32-byte return word, masks the returned word to 160 bits, and binds the resulting asset address to a local result variable. The trust report records the explicit ECM assumption `erc4626_asset_interface`. - -`Compiler.Modules.ERC4626.maxDeposit` covers the canonical receiver-scoped deposit ceiling case: it ABI-encodes `maxDeposit(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset limit to a local result variable. The trust report records the explicit ECM assumption `erc4626_maxDeposit_interface`. - -`Compiler.Modules.ERC4626.maxMint` covers the canonical receiver-scoped mint ceiling case: it ABI-encodes `maxMint(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned share limit to a local result variable. The trust report records the explicit ECM assumption `erc4626_maxMint_interface`. - -`Compiler.Modules.ERC4626.maxWithdraw` covers the canonical owner-scoped withdrawal ceiling case: it ABI-encodes `maxWithdraw(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned asset limit to a local result variable. The trust report records the explicit ECM assumption `erc4626_maxWithdraw_interface`. - -`Compiler.Modules.ERC4626.maxRedeem` covers the canonical owner-scoped redeem ceiling case: it ABI-encodes `maxRedeem(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned share limit to a local result variable. The trust report records the explicit ECM assumption `erc4626_maxRedeem_interface`. - -`Compiler.Modules.ERC4626.deposit` covers the canonical vault deposit path: it ABI-encodes `deposit(uint256,address)`, performs a `call`, requires exactly one 32-byte return word, and binds the returned share amount to a local result variable. The trust report records the explicit ECM assumption `erc4626_deposit_interface`. - -### Low-level `call` / `staticcall` / `delegatecall` - -First-class low-level forms exist in the compilation model (`Expr.call`, `Expr.staticcall`, `Expr.delegatecall`). - -They are not yet modeled by the current proof interpreters. In the machine-readable interpreter feature matrix, the spec interpreters still treat these forms as fallback-zero / not-modeled constructs, so low-level call plumbing and returndata behavior remain a compiler-and-testing trust boundary rather than a proved semantic feature today. - -When the low-level form is `delegatecall`, the trust report now also isolates it as a dedicated proxy / upgradeability boundary; archive `--trust-report` and use `--deny-proxy-upgradeability` for proof-strict runs (see issue `#1420`). - -Prefer ECM wrappers when they fit the use case, and see issue `#1332` plus [`docs/INTERPRETER_FEATURE_MATRIX.md`](../../docs/INTERPRETER_FEATURE_MATRIX.md) for the current proof boundary. - -Reference: `Compiler/CompilationModel.lean`. - -For the remaining migration cases where a tiny unsafe/assembly-shaped escape hatch is unavoidable, `FunctionSpec.localObligations` / `ConstructorSpec.localObligations` let the contract author attach a named local refinement obligation to that exact usage site. The trust report records these under `localObligations` and `proofStatus.*.localObligations`, and `--deny-local-obligations` fails closed unless every such obligation has been discharged to `proved`. - -First-class linear-memory forms (`Expr.mload`, `Stmt.mstore`, `Stmt.calldatacopy`, `Stmt.returndataCopy`, `Expr.returndataOptionalBoolAt`) also compile today, but they are still only partially modeled by the current proof interpreters. When these forms appear, treat them as an explicit memory/ABI trust boundary, archive `--trust-report`, and use `--deny-linear-memory-mechanics` for proof-strict runs (see issue `#1411`). - -## Context Accessors +`Expr.keccak256` also remains an explicit proof boundary today: the compiler supports it directly, but the current proof stack still treats it as an axiomatized primitive instead of a fully modeled operation. When it appears, archive `--trust-report` and use `--deny-axiomatized-primitives` for proof-strict runs (see issue `#1411`). -**Signatures** +### `tryCatch` ```verity -def msgSender : Contract Address -def contractAddress : Contract Address -def msgValue : Contract Uint256 -def blockTimestamp : Contract Uint256 -def blockNumber : Contract Uint256 -def blobbasefee : Contract Uint256 +tryCatch (call gas target value inOffset inSize outOffset outSize) (do + setStorage lastFailure 1) ``` -**Example** +Lowers to a synthetic `letVar` + `ite` entering the catch block when the result word is `0`. Low-level call-like expressions only; catch-payload decoding is not modeled yet. -```verity -let from <- msgSender -let value <- msgValue -``` +### Low-level `call` / `staticcall` / `delegatecall` -**Proof lemmas** +First-class forms exist in the compilation model (`Expr.call`, `Expr.staticcall`, `Expr.delegatecall`). They are not yet modeled by the current proof interpreters. In the machine-readable interpreter feature matrix, low-level call plumbing and returndata behavior remain a compiler-and-testing trust boundary rather than a proved semantic feature today. -- `msgSender_run`, `contractAddress_run`, `msgValue_run`, `blockTimestamp_run` (`Verity/Core.lean`) -- `msgSender_runState`, `msgSender_runValue` (`Verity/Proofs/Stdlib/Automation.lean`) +When the low-level form is `delegatecall`, the trust report now also isolates it as a dedicated proxy / upgradeability boundary; archive `--trust-report` and use `--deny-proxy-upgradeability` for proof-strict runs (see issue `#1420`). -## Notes +First-class linear-memory forms (`Expr.mload`, `Stmt.mstore`, `Stmt.calldatacopy`, `Stmt.returndataCopy`, `Expr.returndataOptionalBoolAt`) also compile today, but they are still only partially modeled by the current proof interpreters. When they appear, treat them as an explicit memory/ABI trust boundary, archive `--trust-report`, and use `--deny-linear-memory-mechanics` for proof-strict runs (see issue `#1411`). -- For proofs, prefer full-result `.run` lemmas in `Verity/Core.lean`, then use automation lemmas from `Verity/Proofs/Stdlib/Automation.lean` and `Verity/Proofs/Stdlib/MappingAutomation.lean`. -- ECM calls intentionally carry module-level `axioms` metadata (see `Compiler/Modules/*.lean`) rather than pure `simp`-style contract lemmas. +Prefer ECM wrappers when they fit. For the remaining unavoidable cases, attach a `localObligations` entry at the usage site and discharge it before shipping. diff --git a/docs-site/content/examples.mdx b/docs-site/content/examples.mdx index 826109f8d..005de2dfd 100644 --- a/docs-site/content/examples.mdx +++ b/docs-site/content/examples.mdx @@ -1,47 +1,30 @@ --- -title: Example Contracts -description: 12 contracts covering storage, arithmetic, access control, mappings, composition, and security +title: Examples Gallery +description: Sample contracts, ordered by the pattern each introduces — single-slot storage through full token composition. --- -# Example Contracts +# Examples Gallery -A small set of contracts, each introducing a new pattern. They build on each other: SimpleStorage uses one slot, Counter adds arithmetic, Owned adds access control, and SimpleToken combines all three. +A small set of contracts, each introducing a new pattern. They build on each other: SimpleStorage uses one slot, Counter adds arithmetic, Owned adds access control, SimpleToken combines all three. -## How to organize a contract +Each contract is verified end-to-end against the generic whole-contract Layer 2 theorem in `Compiler/Proofs/IRGeneration/Contract.lean` for the current supported fragment — there are no per-contract bridge axioms. -- **Spec**: `Verity/Specs//Spec.lean` -- **Invariants**: `Verity/Specs//Invariants.lean` -- **Implementation**: `Verity/Examples/.lean` -- **Basic proofs**: `Verity/Proofs//Basic.lean` -- **Advanced proofs**: `Verity/Proofs//Correctness.lean` -- **Compilation correctness**: `Compiler/TypedIRCompilerCorrectness.lean` + `Compiler/Proofs/IRGeneration/Contract.lean` for the current supported fragment. -- **Reusable proof infra**: `Verity/Proofs/Stdlib/` - -Example (SimpleStorage): -- Spec: `Contracts/SimpleStorage/Spec.lean` -- Implementation: `Contracts/SimpleStorage/SimpleStorage.lean` -- Basic proofs: `Contracts/SimpleStorage/Proofs/Basic.lean` -- Correctness proofs: `Contracts/SimpleStorage/Proofs/Correctness.lean` - -## Authoring checklist - -1. Define behavior in `Contracts//Spec.lean`. -2. Add invariants in `Contracts//Invariants.lean` if needed. -3. Implement the EDSL contract in `Contracts//.lean`. -4. Prove spec adherence in `Contracts//Proofs/Basic.lean` using `Verity/Proofs/Stdlib/` helpers. +For the *file layout* and authoring steps these examples follow, see [Add a Contract](/guides/add-contract). For a guided walkthrough that builds one from scratch, see [Your First Contract](/first-contract). ## SimpleStorage Single storage slot with get/set. ```verity -def storedData : StorageSlot Uint256 := ⟨0⟩ +verity_contract SimpleStorage where + storage + storedData : Uint256 := slot 0 -def store (value : Uint256) : Contract Unit := do - setStorage storedData value + function store (value : Uint256) : Unit := do + setStorage storedData value -def retrieve : Contract Uint256 := do - getStorage storedData + function retrieve () : Uint256 := do + return (← getStorage storedData) ``` Proofs cover store/retrieve roundtrip and state isolation. @@ -51,63 +34,76 @@ Proofs cover store/retrieve roundtrip and state isolation. Read-modify-write with increment and decrement. ```verity -def count : StorageSlot Uint256 := ⟨0⟩ +verity_contract Counter where + storage + count : Uint256 := slot 0 -def increment : Contract Unit := do - let current ← getStorage count - setStorage count (add current 1) + function increment () : Unit := do + let current ← getStorage count + setStorage count (add current 1) -def decrement : Contract Unit := do - let current ← getStorage count - setStorage count (sub current 1) + function decrement () : Unit := do + let current ← getStorage count + setStorage count (sub current 1) ``` -Proofs cover arithmetic, composition (two increments add 2), and decrement-at-zero behavior. +Proofs cover arithmetic, composition (two increments add 2), and decrement-at-zero wraparound behavior. ## SafeCounter -Same as Counter but uses checked arithmetic from `Stdlib/Math`. +Same as Counter but uses checked arithmetic from `Stdlib.Math`. ```verity -def increment : Contract Unit := do - let current ← getStorage count - let newCount ← requireSomeUint (safeAdd current 1) "Overflow" - setStorage count newCount +verity_contract SafeCounter where + storage + count : Uint256 := slot 0 + + function increment () : Unit := do + let current ← getStorage count + let newCount ← requireSomeUint (safeAdd current 1) "Overflow" + setStorage count newCount ``` Proofs cover overflow/underflow revert and bounds preservation. ## Owned -Access control with an owner address and a `require` guard. +Access control with an owner address and a `require` guard. `onlyOwner` is a same-contract helper that any function can call directly. ```verity -def owner : StorageSlot Address := ⟨0⟩ +verity_contract Owned where + storage + owner : Address := slot 0 + + constructor (initialOwner : Address) := do + setStorageAddr owner initialOwner -def isOwner : Contract Bool := do - let sender ← msgSender - let currentOwner ← getStorageAddr owner - return sender == currentOwner + function onlyOwner () : Unit := do + let sender ← msgSender + let currentOwner ← getStorageAddr owner + require (sender == currentOwner) "Caller is not the owner" -def onlyOwner : Contract Unit := do - let ownerCheck ← isOwner - require ownerCheck "Caller is not the owner" + function transferOwnership (newOwner : Address) : Unit := do + onlyOwner + setStorageAddr owner newOwner ``` -Proofs cover access control enforcement and ownership transfer. +Proofs cover access-control enforcement and the full lifecycle (create, transfer, locked-out old owner). ## OwnedCounter Composes Owned and Counter. Increment/decrement require ownership. ```verity -def owner : StorageSlot Address := ⟨0⟩ -def count : StorageSlot Uint256 := ⟨1⟩ - -def increment : Contract Unit := do - onlyOwner - let current ← getStorage count - setStorage count (add current 1) +verity_contract OwnedCounter where + storage + owner : Address := slot 0 + count : Uint256 := slot 1 + + function increment () : Unit := do + onlyOwner + let current ← getStorage count + setStorage count (add current 1) ``` Proofs cover cross-pattern composition, ownership transfer locking out old owner, and counter value surviving ownership transfer. @@ -117,24 +113,26 @@ Proofs cover cross-pattern composition, ownership transfer locking out old owner Mapping storage for per-address balances with deposit, withdraw, and transfer. ```verity -def balances : StorageSlot (Address → Uint256) := ⟨0⟩ - -def deposit (amount : Uint256) : Contract Unit := do - let sender ← msgSender - let currentBalance ← getMapping balances sender - setMapping balances sender (add currentBalance amount) -- modular arithmetic (EVM) - -def transfer (to : Address) (amount : Uint256) : Contract Unit := do - let sender ← msgSender - let senderBalance ← getMapping balances sender - require (senderBalance >= amount) "Insufficient balance" - if sender == to then - pure () - else - let recipientBalance ← getMapping balances to - let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow" - setMapping balances sender (sub senderBalance amount) - setMapping balances to newRecipientBalance +verity_contract Ledger where + storage + balances : Address → Uint256 := slot 0 + + function deposit (amount : Uint256) : Unit := do + let sender ← msgSender + let currentBalance ← getMapping balances sender + setMapping balances sender (add currentBalance amount) -- EVM modular arithmetic + + function transfer (to : Address) (amount : Uint256) : Unit := do + let sender ← msgSender + let senderBalance ← getMapping balances sender + require (senderBalance >= amount) "Insufficient balance" + if sender == to then + pure () + else + let recipientBalance ← getMapping balances to + let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow" + setMapping balances sender (sub senderBalance amount) + setMapping balances to newRecipientBalance ``` Proofs cover balance guards, deposit/withdraw/transfer sum equations, and deposit-withdraw cancellation. @@ -144,34 +142,70 @@ Proofs cover balance guards, deposit/withdraw/transfer sum equations, and deposi Composes Owned and Ledger. Adds owner-controlled minting and supply tracking. ```verity -def owner : StorageSlot Address := ⟨0⟩ -def balances : StorageSlot (Address → Uint256) := ⟨1⟩ -def totalSupply : StorageSlot Uint256 := ⟨2⟩ - -def mint (to : Address) (amount : Uint256) : Contract Unit := do - onlyOwner - let currentBalance ← getMapping balances to - let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow" - let currentSupply ← getStorage totalSupply - let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow" - setMapping balances to newBalance - setStorage totalSupply newSupply - -def transfer (to : Address) (amount : Uint256) : Contract Unit := do - let sender ← msgSender - let senderBalance ← getMapping balances sender - require (senderBalance >= amount) "Insufficient balance" - if sender == to then - pure () - else - let recipientBalance ← getMapping balances to - let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow" - setMapping balances sender (sub senderBalance amount) - setMapping balances to newRecipientBalance +verity_contract SimpleToken where + storage + owner : Address := slot 0 + balances : Address → Uint256 := slot 1 + totalSupply : Uint256 := slot 2 + + constructor (initialOwner : Address) := do + setStorageAddr owner initialOwner + setStorage totalSupply 0 + + function mint (to : Address) (amount : Uint256) : Unit := do + onlyOwner + let currentBalance ← getMapping balances to + let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow" + let currentSupply ← getStorage totalSupply + let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow" + setMapping balances to newBalance + setStorage totalSupply newSupply + + function transfer (to : Address) (amount : Uint256) : Unit := do + let sender ← msgSender + let senderBalance ← getMapping balances sender + require (senderBalance >= amount) "Insufficient balance" + if sender == to then + pure () + else + let recipientBalance ← getMapping balances to + let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow" + setMapping balances sender (sub senderBalance amount) + setMapping balances to newRecipientBalance ``` Proofs cover mint/transfer correctness, supply conservation equations, and storage isolation across all three slot types. +## Vault (minimal ERC-4626) + +A conservative ERC-4626-style vault with 1:1 asset/share accounting. Deposits mint shares equal to assets; withdrawals burn 1:1. The shape exercises the canonical vault surface without complicating the share-price math. + +```verity +verity_contract Vault where + storage + totalAssetsSlot : Uint256 := slot 0 + totalSupplySlot : Uint256 := slot 1 + shareBalancesSlot : Address → Uint256 := slot 2 + + constructor () := do + setStorage totalAssetsSlot 0 + setStorage totalSupplySlot 0 + + function deposit (assets : Uint256) : Unit := do + let sender ← msgSender + let currentShares ← getMapping shareBalancesSlot sender + let newShares ← requireSomeUint (safeAdd currentShares assets) "Share balance overflow" + let currentAssets ← getStorage totalAssetsSlot + let newAssets ← requireSomeUint (safeAdd currentAssets assets) "Total assets overflow" + let currentSupply ← getStorage totalSupplySlot + let newSupply ← requireSomeUint (safeAdd currentSupply assets) "Total supply overflow" + setMapping shareBalancesSlot sender newShares + setStorage totalAssetsSlot newAssets + setStorage totalSupplySlot newSupply +``` + +The spec layer (`deposit_spec`, `withdraw_spec`, isolation predicates) lives in `Contracts/Vault/Spec.lean`. Native IR-lowering proofs are checked in [`Contracts/Vault/Proofs/Native.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/Vault/Proofs/Native.lean); deeper Basic/Correctness/Conservation coverage is tracked under issue [#1163](https://github.com/lfglabs-dev/verity/issues/1163). + ## ReentrancyExample Two parallel bank contracts, one vulnerable, one safe, demonstrating that reentrancy is a *provable* property, not just a testing concern. @@ -200,7 +234,7 @@ Proofs cover: existential attack witness (vulnerability is provably exploitable) ## CryptoHash -Unverified example demonstrating external library linking via the [Linker](/compiler#linker). Has no specs or proofs; it exists to show how external Yul helper functions integrate with compiled output. See the [Linking Libraries](/guides/linking-libraries) guide for a walkthrough. +Unverified example demonstrating external library linking via the [Linker](/compiler#linker). Has no specs or proofs; it exists to show how external Yul helper functions integrate with compiled output. See the [Linking External Libraries](/guides/linking-libraries) guide for a walkthrough. ```verity -- Placeholder hash for proofs (replaced with real Poseidon at compile time) @@ -215,30 +249,30 @@ def storeHashTwo (a b : Uint256) : Contract Unit := do The EDSL uses a placeholder function (`add`) for the hash. At compile time, the [Linker](/guides/linking-libraries) replaces the compiled output with a call to the real Poseidon library via `Expr.externalCall` in the CompilationModel layer. -Source: [`Contracts/CryptoHash/Contract.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/CryptoHash/Contract.lean) +Source: [`Contracts/CryptoHash/Contract.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/CryptoHash/Contract.lean) -## ERC20 (Foundation Scaffold) +## ERC20 -Baseline-verified ERC20 foundation scaffold with executable logic (`mint`, `transfer`, `approve`, `transferFrom`) and formal spec/invariant modules. +Baseline-verified ERC20 with `mint`, `transfer`, `approve`, `transferFrom` and formal spec/invariant modules. Source: [`Contracts/ERC20/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts/ERC20). -Source: -- Implementation: [`Contracts/ERC20/ERC20.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/ERC20.lean) -- Spec: [`Contracts/ERC20/Spec.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/Spec.lean) -- Invariants: [`Contracts/ERC20/Invariants.lean`](https://github.com/Th0rgal/verity/blob/main/Contracts/ERC20/Invariants.lean) +## ERC721 -## Pattern progression +Standards-shaped NFT contract demonstrating multi-mapping storage: uint-keyed `owners` and `tokenApprovals`, address-keyed `balances`, and double-mapping `operatorApprovals`. Exercises `getMappingUint`, `getMapping2`, `addressToWord`/`wordToAddress`, and constructor parameters. + +```verity +verity_contract ERC721 where + storage + owner : Address := slot 0 + totalSupply : Uint256 := slot 1 + nextTokenId : Uint256 := slot 2 + balances : Address → Uint256 := slot 3 + owners : Uint256 → Uint256 := slot 4 + tokenApprovals : Uint256 → Uint256 := slot 5 + operatorApprovals : Address → Address → Uint256 := slot 6 +``` -1. **SimpleStorage**: single slot -2. **Counter**: arithmetic -3. **SafeCounter**: stdlib integration -4. **Owned**: access control -5. **OwnedCounter**: composition (Owned + Counter) -6. **Ledger**: mapping storage -7. **SimpleToken**: full composition (Owned + Ledger + supply tracking) -8. **ReentrancyExample**: vulnerability modeling and safety proofs -9. **CryptoHash**: external library linking (unverified) -10. **ERC20**: standards-oriented token scaffold with baseline proofs and specs/invariants +Source: [`Contracts/ERC721/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts/ERC721). ## Source -All contracts are in [`Contracts/`](https://github.com/Th0rgal/verity/tree/main/Contracts). +All contracts: [`Contracts/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts). diff --git a/docs-site/content/faq.mdx b/docs-site/content/faq.mdx new file mode 100644 index 000000000..c652d4104 --- /dev/null +++ b/docs-site/content/faq.mdx @@ -0,0 +1,97 @@ +--- +title: FAQ +description: Why Lean, why an EDSL, how Verity compares to other formal-methods tools, and what's actually verified. +--- + +# FAQ + +## Why Lean 4, not Coq, Dafny, or Isabelle? + +Lean 4 combines a dependently-typed core, a fast elaborator, and a macro system +expressive enough to embed a domain-specific surface syntax (`verity_contract`) +without leaving the host language. That last property is what makes the EDSL +approach work: specifications, implementations, and proofs all share one type +system and one kernel. + +Coq and Isabelle have older ecosystems and more developed libraries, but their +metaprogramming stories make embedding a usable contract DSL substantially +harder. Dafny is a verification-oriented language rather than a proof +assistant — it relies on SMT for automation, which is fast for shallow +properties but opaque when proofs require nonlinear arithmetic, induction +over storage state, or precise EVM-shaped reasoning. Lean's tradeoff is more +manual proof, but the proofs are kernel-checked and the trust base is smaller. + +## Why an EDSL, not a new language? + +Building a new language means building a new parser, a new type checker, a +new elaborator, a new editor integration, and a new proof checker — and then +re-justifying that all of those are correct. Embedding the language inside +Lean 4 inherits all of that for free: the same toolchain that elaborates +contracts also checks the proofs about them. + +The core is intentionally small (`Verity/Core.lean`): six storage spaces plus transient, a +`Contract` monad, a `require` guard, and a curated set of `@[simp]` lemmas. +Every primitive is shallow enough that the standard unfolding-then-`simp` +recipe works for most properties. New surface syntax — `verity_contract`, +`local_obligations`, `linked_externals`, ECM helpers — is added via macros +that lower to the same core. + +## What's verified vs what's trusted? + +Verified: the EDSL semantics, the `CompilationModel → IR` transformation for +the supported fragment, the `IR → Yul` preservation, and per-contract specs +and invariants. Trusted: the Lean kernel, the Yul compiler (`solc`), the EVM +specification, the deployment toolchain, and the named external assumptions +listed in `--trust-report` (ECM interface signatures, precompile semantics, +any `local_obligations`). [`AXIOMS.md`](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md) +itself lists **zero active project-level Lean axioms** today — the residual +ones have been eliminated. The full breakdown lives at [`/trust-model`](/trust-model). + +## How is Verity different from Certora, Halmos, or K? + +Certora, Halmos, K, and similar tools verify *already-compiled* bytecode (or a +near-bytecode representation) against a user-supplied specification. They take +the compiler as given and use symbolic execution, SMT, or rewriting to check +that the deployed contract refines the spec. Their strength is that they work +on existing Solidity code with minimal changes. + +Verity verifies the *compilation* itself and the *spec ↔ implementation* +relationship. The compiler from EDSL to Yul is part of the proof tree: +`Compiler/Proofs/IRGeneration/Contract.lean` proves +`CompilationModel.compile` is correct for the supported fragment, and +`Compiler/Proofs/YulGeneration/` proves IR-to-Yul preservation. That means a +verified Verity contract carries a guarantee about the artifact you deploy, +not just about a separately-modelled source. The tradeoff: you write contracts +in the Verity EDSL, not in Solidity. + +## Can I use existing Solidity? + +Not directly — Verity contracts are written in the Lean-embedded EDSL. There +are translation guides that walk through common Solidity patterns and how to +express them in Verity: see [`/guides/solidity-to-verity`](/guides/solidity-to-verity) +and [`/guides/production-solidity-patterns`](/guides/production-solidity-patterns) +for modifiers, externals, ABI, events, and oracle patterns. + +## What's the EVM compatibility story? + +Verity compiles to Yul, the standard EVM intermediate dialect. Yul is then +compiled to EVM bytecode by `solc --strict-assembly`. The generated contracts +use the Solidity ABI for calldata encoding, standard Solidity selector +computation (`keccak256` of the canonical signature, first 4 bytes), the +canonical mapping-slot layout (`keccak256(key . slot)` and the nested +equivalent), and the standard constructor-argument convention of loading from +the tail of deployment bytecode. Deployment uses any standard tool: `forge +create`, `cast`, raw RPC, etc. + +## Is this production-ready? + +Verity verifies a precisely-scoped class of contracts today — not a drop-in replacement for general Solidity. Inside the supported fragment, you get strong machine-checked guarantees; outside it, the trust report tells you exactly which assumptions are doing the work. Several features compile but are not yet end-to-end modeled (low-level call mechanics, linear-memory primitives, `rawLog`, `keccak256`); each has a `--deny-*` flag for proof-strict builds. There is no multi-contract interaction model, no reentrancy semantics, and no gas modeling. + +## Where can I see verified contracts? + +Browse [`/examples`](/examples) for walkthroughs and [`/verification`](/verification) +for the live theorem inventory by contract. + +## Can AI agents write Verity proofs? + +That question is the explicit purpose of [`verity-benchmark`](https://github.com/lfglabs-dev/verity-benchmark) — a fixed set of 30 proof tasks across six real-world protocols (Ethereum deposit contract, Lido VaultHub, Nexus Mutual RAMM, Kleros sortition, Paladin Votes, Damn Vulnerable DeFi). Each task hands an agent a contract, a spec, and a single theorem to prove, with no placeholders allowed (`sorry`, `admit`, `axiom`). The shallow EDSL surface and the `_meets_spec` proof pattern make this a tractable benchmark for measuring agent capability, not a vibe-check. diff --git a/docs-site/content/first-contract.mdx b/docs-site/content/first-contract.mdx new file mode 100644 index 000000000..49b057134 --- /dev/null +++ b/docs-site/content/first-contract.mdx @@ -0,0 +1,214 @@ +--- +title: Adding Your First Contract +description: Step-by-step tutorial for creating a verified smart contract in Verity +--- + +# Adding Your First Contract to Verity + +**Time Required**: 2-3 hours for first contract +**Prerequisites**: Basic familiarity with Lean 4 syntax and smart contract concepts + +> **New to Lean 4?** You'll need `do` notation, `def`/`theorem`, and basic tactics (`simp`, `intro`, `constructor`). Start with [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) (chapters 1–5) and [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) (chapter 4 on `do` and monads). + +This tutorial walks you through creating a complete verified smart contract from scratch. We build a **TipJar**, a simple balance ledger where users deposit tips and check balances. It uses the core EDSL features (mappings, `msgSender`, `require`, arithmetic) while staying small enough to prove fully on the first attempt. + +## Overview + +Every contract follows this path: + +``` +Specification → Implementation → Proofs → Compilation → Testing + (30m) (45m) (1-2h) (auto) (30m) +``` + +## Phase 1: Setup + +```bash +python3 scripts/generate_contract.py TipJar \ + --fields "tips:mapping" \ + --functions "tip(uint256),getBalance(address)" +``` + +This creates all required files: +- `Contracts/TipJar/Spec.lean` — formal specification +- `Contracts/TipJar/Invariants.lean` — state invariants +- `Contracts/TipJar/SpecProofs.lean` — compilation correctness re-export +- `Contracts/TipJar/TipJar.lean` — EDSL implementation +- `Contracts/TipJar/Proofs/Basic.lean` — basic correctness proofs +- `Contracts/TipJar/Proofs/Correctness.lean` — advanced correctness proofs +- `test/PropertyTipJar.t.sol` — Foundry tests + +Our goal: users deposit a tip (adding to their balance) via `tip(uint256)`, anyone reads a balance via `getBalance(address)`. Balances use EVM modular arithmetic; for Solidity ^0.8 checked behavior, add `require` guards (see `SafeCounter`). + +## Phase 2: Specification + +Specifications describe **what** the contract should do, not **how**. + +Open `Contracts/TipJar/Spec.lean`: + +```verity +import Verity.Specs.Common +import Verity.Macro +import Verity.EVM.Uint256 + +namespace Contracts.TipJar.Spec + +open Verity +open Verity.EVM.Uint256 + +/-- tip: increases sender's balance by amount -/ +def tip_spec (amount : Uint256) (s s' : ContractState) : Prop := + s'.storageMap 0 s.sender = add (s.storageMap 0 s.sender) amount ∧ + storageMapUnchangedExceptKeyAtSlot 0 s.sender s s' ∧ + sameStorageAddrContext s s' + +/-- getBalance: returns balance at given address, no state change -/ +def getBalance_spec (addr : Address) (result : Uint256) (s : ContractState) : Prop := + result = s.storageMap 0 addr + +end Contracts.TipJar.Spec +``` + +`s` is initial state, `s'` final. `storageMap 0` is the mapping at slot 0. `storageMapUnchangedExceptKeyAtSlot` and `sameStorageAddrContext` come from [`Verity/Specs/Common.lean`](/core#spec-helpers); see the spec-helper reference for picking the right predicate for what your function actually writes. + +## Phase 3: Implementation + +Open `Contracts/TipJar/TipJar.lean`: + +```verity +import Contracts.Common + +namespace Contracts.TipJar + +open Verity hiding pure bind +open Verity.EVM.Uint256 + +def tips : StorageSlot (Address → Uint256) := ⟨0⟩ + +def tip (amount : Uint256) : Contract Unit := do + let sender ← msgSender + let currentBalance ← getMapping tips sender + setMapping tips sender (add currentBalance amount) + +def getBalance (addr : Address) : Contract Uint256 := do + getMapping tips addr + +end Contracts.TipJar +``` + +Full primitive catalogue: [EDSL API Reference](/edsl-api-reference). + +```bash +lake build Contracts.TipJar +``` + +## Phase 4: Prove Correctness + +Open `Contracts/TipJar/Proofs/Basic.lean`: + +```verity +import Contracts.TipJar.Spec +import Contracts.TipJar.Invariants +import Verity.Proofs.Stdlib.Automation + +namespace Contracts.TipJar.Proofs + +open Verity +open Verity.EVM.Uint256 +open Contracts.TipJar +open Contracts.TipJar.Spec + +theorem tip_meets_spec (s : ContractState) (amount : Uint256) : + tip_spec amount s (((tip amount).run s).snd) := by + simp [tip, tip_spec, tips, msgSender, getMapping, setMapping, bind, + Specs.storageMapUnchangedExceptKeyAtSlot, + Specs.sameStorageAddrContext, Specs.sameStorage, Specs.sameStorageAddr, + Specs.sameContext] + refine ⟨?_, ?_, ?_⟩ <;> simp [Contract.run] + +theorem getBalance_correct (s : ContractState) (addr : Address) : + getBalance_spec addr (((getBalance addr).run s).fst) s := by + simp [getBalance, getBalance_spec, tips, getMapping] + +theorem getBalance_preserves_state (s : ContractState) (addr : Address) : + ((getBalance addr).run s).snd = s := by + simp [getBalance, tips, getMapping] + +end Contracts.TipJar.Proofs +``` + +```bash +lake build +grep -r "sorry" Contracts/TipJar/ # should be empty +``` + +Stuck on a proof? See the [Proof Debugging Handbook](/guides/debugging-proofs). + +## Phase 5: Add to Compiler + +Define the contract with `verity_contract` in `Contracts//.lean`, then register `Contracts..spec` in `Compiler/Specs.lean` under `allSpecs`: + +```verity +verity_contract TipJar where + storage + tips : Address -> Uint256 := slot 0 + + function tip (amount : Uint256) : Unit := do + let sender <- msgSender + let current ← getMapping tips sender + setMapping tips sender (add current amount) + + function getBalance (addr : Address) : Uint256 := do + return (← getMapping tips addr) +``` + +Function selectors are computed automatically. Verify them against `solc --hashes` with `python3 scripts/check_selectors.py`. + +```bash +lake build verity-compiler +lake exe verity-compiler # writes artifacts/yul/TipJar.yul +python3 scripts/check_yul.py +``` + +Compilation correctness is generic: the framework's `Compiler/TypedIRCompilerCorrectness.lean` covers the supported fragment with no per-contract bridge proofs needed, and the compiler-level `CompilationModel -> IR` result now lives in `Compiler/Proofs/IRGeneration/Contract.lean`. See [Verification Status](/verification). + +## Phase 6: Testing + +The scaffold generator writes `test/PropertyTipJar.t.sol` with property tests that exercise the deployed Yul against the proven theorems. Run: + +```bash +FOUNDRY_PROFILE=difftest forge test --match-contract TipJar -vv +python3 scripts/report_property_coverage.py --format=markdown +``` + +Tests use `deployYul("TipJar")` to deploy from `artifacts/yul/TipJar.yul` (via `solc` through `vm.ffi`), `vm.prank` to set `msg.sender`, and `vm.load`/`vm.store` for direct storage access. Mapping slots follow Solidity's `keccak256(abi.encode(key, baseSlot))` layout. + +## Phase 7: Validation + +```bash +lake build # all proofs check +grep -r "sorry" Contracts/TipJar/ # empty +FOUNDRY_PROFILE=difftest forge test --match-contract TipJar +python3 scripts/check_selectors.py +python3 scripts/check_property_manifest.py +python3 scripts/check_storage_layout.py +``` + +Add imports to your `All.lean`: + +```lean +import Contracts.TipJar.Spec +import Contracts.TipJar.Invariants +import Contracts.TipJar.TipJar +import Contracts.TipJar.Proofs.Basic +import Contracts.TipJar.Proofs.Correctness +``` + +The scaffold generator prints these exact lines — copy them directly. + +## Next steps + +- Add access control with `require` + owner pattern — see `Contracts/OwnedCounter/`. +- Add a `withdraw` with balance checks — see `Contracts/Ledger/`. +- Study `SimpleStorage`, `Counter`, `Ledger`, `OwnedCounter` for progressive patterns. +- [Core Architecture](/core) and [EDSL API Reference](/edsl-api-reference) for the full surface. diff --git a/docs-site/content/getting-started.mdx b/docs-site/content/getting-started.mdx index 1a358b283..7a81b2109 100644 --- a/docs-site/content/getting-started.mdx +++ b/docs-site/content/getting-started.mdx @@ -50,42 +50,27 @@ forge --version ## 3. Clone and build ```bash -git clone https://github.com/Th0rgal/verity.git +git clone https://github.com/lfglabs-dev/verity.git cd verity lake build # Downloads dependencies and verifies the current proof set ``` The first build downloads Mathlib and compiles everything — expect **20–45 minutes** on first run (Mathlib is large). Subsequent builds are incremental and much faster (seconds to minutes). -## Explore a proof (5 minutes) +## Explore a proof -While the first build runs (or after it completes), get a feel for what Verity does: +Once the build completes, the core loop is **write a contract in Lean → prove it correct → compile it to EVM bytecode**: -Before reading files, keep this map: - -1. `Verity/Examples/*`: EDSL implementation, executable Lean code. -2. `Verity/Specs/*`: logical behavior specs (`Prop`) and invariants. -3. `Compiler/Specs.lean`: `CompilationModel` compiler models that generate IR/Yul. - -**1. Open an example contract** — [`Verity/Examples/SimpleStorage.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Examples/SimpleStorage.lean): -```verity --- A contract with a single uint256 storage slot -def store (value : Uint256) : Contract Unit := setStorage storedData value -def retrieve : Contract Uint256 := getStorage storedData -``` - -**2. See its proven theorems** — [`Verity/Proofs/SimpleStorage/Basic.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Proofs/SimpleStorage/Basic.lean) contains theorems like `store_meets_spec` and `retrieve_preserves_state`, each machine-checked by Lean with zero `sorry`. Build just that file to confirm: ```bash -lake build Verity.Proofs.SimpleStorage.Basic # Verifies in seconds +lake build Contracts.SimpleStorage.Proofs.Basic # verifies theorems in seconds +lake exe verity-compiler # writes artifacts/yul/SimpleStorage.yul ``` -**3. See it compile to EVM bytecode** — after `lake build` completes: -```bash -lake exe verity-compiler # Outputs Yul to artifacts/yul/ -cat artifacts/yul/SimpleStorage.yul -``` +Three directories to keep in mind: -This is the core loop: **write a contract in Lean → prove it correct → compile it to EVM bytecode**. +1. `Contracts//.lean` — EDSL implementation, executable Lean code. +2. `Contracts//Spec.lean`, `Invariants.lean`, `Proofs/` — logical specs (`Prop`) and proofs. +3. `Compiler/Specs.lean` — `CompilationModel` values that generate IR/Yul. ## 4. Run the test suite @@ -107,19 +92,7 @@ python3 scripts/generate_contract.py TipJar \ --functions "tip(uint256),getBalance(address)" ``` -This creates all the scaffold files you need: - -| File | Purpose | -|------|---------| -| `Verity/Examples/TipJar.lean` | EDSL implementation | -| `Verity/Specs/TipJar/Spec.lean` | Formal specification | -| `Verity/Specs/TipJar/Invariants.lean` | State invariants | -| `Verity/Specs/TipJar/Proofs.lean` | Layer 2 proof re-export | -| `Verity/Proofs/TipJar/Basic.lean` | Basic correctness proofs | -| `Verity/Proofs/TipJar/Correctness.lean` | Advanced proofs | -| `test/PropertyTipJar.t.sol` | Solidity property tests | - -Follow the printed instructions to register the contract in `Verity/All.lean` and `Compiler/Specs.lean`, then see the [First Contract tutorial](/guides/first-contract) for a full walkthrough. +This writes EDSL implementation, specs, invariants, proofs, and a Foundry property test under `Contracts/TipJar/` and `test/`. Follow the printed instructions to register the contract in `Compiler/Specs.lean`, then see the [First Contract tutorial](/first-contract) for the full walkthrough. ## 6. Compile to Yul/EVM @@ -140,5 +113,5 @@ See the [Linking Libraries guide](/guides/linking-libraries) for details. 1. **[Example Contracts](/examples)** — Progressive examples from single-slot storage to token transfers 2. **[Core Architecture](/core)** — The Contract monad, state model, and design decisions -3. **[First Contract tutorial](/guides/first-contract)** — Hands-on guide building a TipJar from scratch +3. **[First Contract tutorial](/first-contract)** — Hands-on guide building a TipJar from scratch 4. **[Compiler reference](/compiler)** — Full CompilationModel DSL documentation diff --git a/docs-site/content/glossary.mdx b/docs-site/content/glossary.mdx new file mode 100644 index 000000000..f45eeda4c --- /dev/null +++ b/docs-site/content/glossary.mdx @@ -0,0 +1,152 @@ +--- +title: Glossary +description: Canonical one-paragraph definitions of Verity's load-bearing terminology. +--- + +# Glossary + +### Assumption inventory + +The `--assumption-report ` CLI output. A flat, machine-readable list of +every assumption used by proofs in the selected contracts, grouped by +contract and usage site. Use it alongside `--trust-report` when audit tooling +needs a flattened view rather than the structured proof-boundary report. + +### CompilationModel + +The typed-IR layer between the EDSL and Yul, defined in +`Compiler/CompilationModel.lean`. A `CompilationModel` value carries fields, +events, errors, the constructor, function bodies as `Expr`/`Stmt`, externals, +and local obligations. It is the declarative input the Verity compiler +consumes to produce IR, Yul, ABI, and trust artifacts. + +### ContractResult + +The success/revert algebra used by all EDSL guards. `ContractResult α` is +either `success a s` or `revert msg s`. Modeling `require` as `revert` +explicitly (rather than as a `StateM` axiom) lets proofs reason about both the +success path and the failure path without introducing axioms. + +### ContractState + +The EVM-shaped state model used by EDSL contracts. Carries six persistent +storage spaces (uint256, address, address-keyed mapping, uint256-keyed +mapping, double mapping, dynamic arrays), EIP-1153 transient storage, the +transaction context (`sender`, `thisAddress`, `msgValue`, `selfBalance`, +`blockTimestamp`, `blockNumber`, `chainId`, `blobBaseFee`), calldata, +memory, tracked `knownAddresses` per slot for conservation proofs, and +an append-only `events` log. + +### Differential test + +A CI tier that runs random transaction sequences against both the EDSL +interpreter and the compiled contract (Yul → EVM via `solc` and Foundry), +then diffs the resulting states. Enabled by `FOUNDRY_PROFILE=difftest`. +Catches compilation regressions outside the proved fragment. + +### ECM (External Call Module) + +A packaged reusable external-call pattern. ECMs live in `Compiler/Modules/*.lean` +(for example `Compiler.Modules.ERC20.safeTransfer`, +`Compiler.Modules.Oracle.oracleReadUint256`, `Compiler.Modules.Precompiles.sha256`). +Each module bundles ABI encoding, call mechanics, mutability metadata, and an +explicit assumption that surfaces in the trust report (for example +`erc20_balanceOf_interface`, `oracle_read_uint256_interface`). + +### EDSL + +The Lean-4 embedded domain-specific language used to write Verity contracts. +Provided by `Verity/Core.lean` and the `verity_contract` macro; consumed by +the elaborator to build both an executable Lean definition and a +`CompilationModel`. + +### Implementation + +The executable EDSL body of a contract function, lowered from +`verity_contract`. One of the four files in the standard contract shape (see +*Spec / Invariant / Implementation / Proof*). + +### Invariant + +A property that should hold of `ContractState` at every reachable point — +typically conservation, isolation, or well-formedness. Lives in +`Contracts//Invariants.lean` and is proved over the implementation. + +### Layer 1 / Layer 2 / Layer 3 + +The three trust boundaries. **Layer 1** verifies the EDSL implementation +matches its `CompilationModel`. **Layer 2** verifies that +`CompilationModel.compile` produces IR with matching semantics for the +supported fragment (generic whole-contract theorem in +`Compiler/Proofs/IRGeneration/Contract.lean`). **Layer 3** verifies the +`IR → Yul` step preserves semantics. See [`/trust-model`](/trust-model) for +the full breakdown. + +### Layout report + +The `--layout-report ` CLI output. A JSON dump of resolved storage-slot +metadata for each compiled contract, including effective alias writes and +reserved-slot policies. Used by upgrade and layout audits. Pair with +`--layout-compat-report` and `--deny-layout-incompatibility` for upgrade +compatibility checks. + +### linked_externals + +A `verity_contract` block declaring external Yul helpers the EDSL can call +via `externalCall`. Declarations populate `spec.externals` with assumed +foreign signatures so the compiler's `Expr.externalCall` validation works +from the macro surface. The bodies are spliced in at compile time via +`--link`. Currently restricted to single-word arguments and at most one +return. + +### local_obligations + +Per-function (or per-constructor) trust receipts attached to a small +unsafe or refinement-shaped boundary inside a `verity_contract`. Each entry +lowers into `FunctionSpec.localObligations` or `ConstructorSpec.localObligations`, +shows up in the `--trust-report`, and participates in +`--deny-local-obligations`. Functions that use direct assembly-shaped +primitives without any `local_obligations [...]` fail closed. See +[`/edsl-api-reference`](/edsl-api-reference) for syntax. + +### Property test + +A CI tier between unit tests and differential tests: randomized inputs +exercised against expected algebraic properties (commutativity, idempotence, +conservation). Lives in the Foundry test suite. + +### Proof + +The Lean term that establishes the contract's `Spec`. Lives under +`Contracts//Proofs/` (typically split across `Basic.lean`, +`Correctness.lean`, `Conservation.lean`, `Supply.lean`, `Isolation.lean`). +Checked by `lake build`; a broken proof is a broken build. + +### Spec + +The human-readable `Prop` statement of what each function should do. Lives in +`Contracts//Spec.lean` and uses the helpers from +`Verity/Specs/Common.lean` (`sameStorage`, `sameContext`, +`storageMapUnchangedExceptKeyAtSlot`, etc.) to avoid field-by-field +conjunctions. Distinct from the *compiler* spec (a `CompilationModel`). + +### Spec / Invariant / Implementation / Proof + +The four-file shape of a Verity contract: + +- **Spec** — `Spec.lean`, the `Prop` statement of intended behavior. +- **Invariant** — `Invariants.lean`, properties that should always hold. +- **Implementation** — the executable EDSL in `.lean`. +- **Proof** — the Lean term in `Proofs/` that ties the implementation to the + spec. + +### Trust report + +The `--trust-report ` CLI output. A structured JSON artifact recording +the proof boundary for the selected contracts: which constructors and +functions are proved, which carry `local_obligations`, which use +not-modeled features (low-level memory, raw `rawLog`, axiomatized `keccak256`, +delegatecall, etc.), and which ECM assumptions are active. Generate at audit +time; pair with `--deny-*` flags for proof-strict builds. + +See also: [Architecture Overview](/architecture), [Trust Model](/trust-model). diff --git a/docs-site/content/guides/_meta.js b/docs-site/content/guides/_meta.js index b1f50b3d3..66d730836 100644 --- a/docs-site/content/guides/_meta.js +++ b/docs-site/content/guides/_meta.js @@ -1,8 +1,7 @@ export default { - 'first-contract': 'Adding Your First Contract', - 'solidity-to-verity': 'Solidity to Verity Translation', + 'add-contract': 'Add a Contract', + 'solidity-to-verity': 'Port from Solidity', 'production-solidity-patterns': 'Production Solidity Patterns', - 'verity-syntax-highlighting': 'Verity Syntax Highlighting', - 'linking-libraries': 'Linking External Libraries', - 'debugging-proofs': 'Proof Debugging Handbook', + 'linking-libraries': 'Link External Libraries', + 'debugging-proofs': 'Debug Failing Proofs', }; diff --git a/docs-site/content/add-contract.mdx b/docs-site/content/guides/add-contract.mdx similarity index 94% rename from docs-site/content/add-contract.mdx rename to docs-site/content/guides/add-contract.mdx index 9a339007c..c169ede3c 100644 --- a/docs-site/content/add-contract.mdx +++ b/docs-site/content/guides/add-contract.mdx @@ -1,10 +1,11 @@ --- title: Add a Contract +description: Shortest reliable spec → proof → compiler → tests workflow for a new contract, anchored to SimpleStorage. --- # Add a Contract (Spec → Proof → Compiler → Tests) -> **New to Verity?** Follow the [step-by-step First Contract tutorial](/guides/first-contract) instead. It walks through building a TipJar contract from scratch with explanations at every step (2–3 hours). +> **New to Verity?** Follow the [step-by-step First Contract tutorial](/first-contract) instead. It walks through building a TipJar contract from scratch with explanations at every step (2–3 hours). This is the shortest reliable path to add a new contract end-to-end, anchored to SimpleStorage. It assumes familiarity with the Verity EDSL and proof patterns. @@ -124,7 +125,7 @@ python3 scripts/check_lean_hygiene.py ## See also -- [Adding Your First Contract](/guides/first-contract), step-by-step tutorial with TipJar +- [Adding Your First Contract](/first-contract), step-by-step tutorial with TipJar - [Solidity to Verity Translation](/guides/solidity-to-verity), direct mappings and translation workflow - [Production Solidity Patterns](/guides/production-solidity-patterns), reusable surfaces and oracle/spec-boundary guidance - [Linking External Libraries](/guides/linking-libraries), if your contract uses Yul library functions diff --git a/docs-site/content/guides/debugging-proofs.mdx b/docs-site/content/guides/debugging-proofs.mdx index a96905bed..44c7e50e9 100644 --- a/docs-site/content/guides/debugging-proofs.mdx +++ b/docs-site/content/guides/debugging-proofs.mdx @@ -1,326 +1,105 @@ --- title: Proof Debugging Handbook -description: Practical guide for debugging common proof failures, errors, and roadblocks in Verity development +description: Practical guide for debugging common proof failures in Verity development --- # Proof Debugging Handbook -**Purpose**: Get unstuck when proofs fail with practical solutions, not theory. +When proofs fail. Patterns and fixes, no theory. -**Who this is for**: Developers writing proofs in Verity, from beginners to experts encountering unfamiliar errors. +## Quick reference ---- - -## Quick Reference - -### Most Common Issues - -| Symptom | Quick Fix | Section | -|---------|-----------|---------| -| "simp made no progress" | Pass definitions to `simp`: `simp [myDef]` | [Tactic Failures](#common-tactic-failures) | -| "omega failed" | Use `by_cases` to split constraints | [Tactic Failures](#common-tactic-failures) | -| "unknown identifier" | Check imports, spelling | [Import Errors](#import-errors) | -| "type mismatch" | Use `#check` to compare types | [Type Errors](#type-errors) | -| Proof too slow | Cache intermediate lemmas with `have` | [Performance](#proof-performance) | -| "motive is not type correct" | Use `generalize` before `induction` | [Induction Errors](#induction-errors) | - ---- - -## Diagnostic Tools - -Before debugging, know your tools: - -### Type Inspection - -```lean --- Show the type of an expression -#check myTerm -- Output: myTerm : Type - --- Show all implicit arguments -#check @myFunction -- Shows hidden type parameters - --- Print full definition -#print MyTheorem -- Shows complete proof/definition - --- Show type and value -#reduce myComplexExpression -- Normalizes and evaluates -``` +| Symptom | Fix | +|---------|-----| +| "simp made no progress" | Pass definitions to `simp`: `simp [myDef]`, or `unfold` first | +| "omega failed" | Split with `by_cases`; omega is linear-only | +| "unknown identifier" | Check imports and `open` | +| "type mismatch" | Use `#check` on both sides; add `.val` or `ofNat` | +| "motive is not type correct" | `generalize` before `induction` | +| "failed to synthesize OfNat" | Add `import Verity.EVM.Uint256` | +| Proof too slow | Cache with `have h := ...`; prefer `rfl` over `simp` | -### Goal Inspection +## Diagnostic tools ```lean --- In a proof, inspect current state -theorem my_theorem : ... := by - trace "{goal}" -- Print current goal - trace "Variable x: {x}" -- Print specific variable - sorry -- Skip temporarily to see what's needed -``` +#check myTerm -- show type +#check @myFunction -- show implicit args +#print MyTheorem -- show full definition +#reduce expr -- normalize and evaluate +#eval myFunction arg1 arg2 -- run it -### Evaluation - -```lean --- Test functions -#eval myFunction arg1 arg2 -- Runs the function - --- Check equivalence -example : expr1 = expr2 := rfl -- Definitional equality +-- In a proof +theorem t : ... := by + trace "goal: {goal}" + sorry -- skip to see remaining goals ``` ---- - -## Common Tactic Failures +## Tactic failures -### "simp made no progress" +### `simp made no progress` -**Diagnosis**: `simp` doesn't know how to simplify your goal. +`simp` doesn't know how to simplify your goal. Either unfold first or pass the right lemmas: -**Cause**: Definition not unfolded, or no simp lemmas apply. - -**Solution 1**: Unfold before simping ```verity --- ❌ DOESN'T WORK +-- Doesn't work theorem getValue_correct : ... := by - simp [getStorage] -- Error: simp made no progress + simp [getStorage] --- ✅ WORKS +-- Works theorem getValue_correct : ... := by - unfold getValue -- First unfold the definition - simp [getStorage] -- Now simp can make progress + unfold getValue + simp [getStorage] ``` -**Solution 2**: Add simp attribute -```lean --- Mark lemma for automatic simplification -@[simp] theorem my_helper_lemma : a + 0 = a := ... - --- Now simp will use it automatically -theorem uses_helper : ... := by - simp -- Automatically applies my_helper_lemma -``` - -**Solution 3**: Add specific lemmas to simp -```lean --- Be explicit about what to simplify -simp [myDefinition, myLemma1, myLemma2] -``` +If a helper applies often, mark it `@[simp]` once so you don't have to thread it everywhere. -### "omega failed to solve goal" +### `omega failed` -**Diagnosis**: Constraint is not linear arithmetic, or omega needs help. +`omega` solves *linear* integer arithmetic. Non-linear terms (`a * b`), dependent types, or quantifiers will defeat it. Split into linear cases: -**Cause**: Non-linear terms, dependent types, or complex constraints. - -**Solution 1**: Split into linear cases ```lean --- ❌ DOESN'T WORK (non-linear) -theorem complex_bound : a * b ≤ MAX := by - omega -- Error: not linear arithmetic - --- ✅ WORKS (split cases) theorem complex_bound : a * b ≤ MAX := by by_cases ha : a = 0 - · simp [ha] -- a = 0 case is trivial + · simp [ha] · by_cases hb : b = 0 - · simp [hb] -- b = 0 case is trivial - · omega -- Now linear constraints only -``` - -**Solution 2**: Add intermediate lemmas -```lean --- Help omega with explicit steps -theorem with_helper : a + b < MAX := by - have h1 : a < MAX / 2 := by assumption - have h2 : b < MAX / 2 := by assumption - omega -- Now has enough context -``` - -**Solution 3**: Convert inequalities -```lean --- omega prefers ≤ over < -have h : a + b ≤ MAX := by omega -have h' : a + b < MAX + 1 := by omega + · simp [hb] + · omega ``` -### "failed to synthesize instance" +Or stage with `have` so omega has concrete bounds in context. -**Diagnosis**: Lean can't find required typeclass instance. +### `motive is not type correct` -**Cause**: Missing import, or instance doesn't exist. +The goal depends on the term you're inducting on. Generalize the dependency first: -**Solution 1**: Add missing import ```lean --- ❌ DOESN'T WORK -#check (5 : Uint256) -- Error: failed to synthesize OfNat - --- ✅ WORKS -import Verity.EVM.Uint256 -#check (5 : Uint256) -- Now works -``` - -**Solution 2**: Provide instance explicitly -```lean --- If instance exists but isn't found automatically -example : MyClass MyType := inferInstance -- Try to find it -example : MyClass MyType := by assumption -- Use from context -``` - -### "motive is not type correct" - -**Diagnosis**: Dependent type mismatch during induction. - -**Cause**: Goal depends on the term being inducted on. - -**Solution**: Generalize the motive -```lean --- ❌ DOESN'T WORK -theorem bad_induction (xs : List α) : xs.length = n := by - induction xs -- Error: motive not type correct - --- ✅ WORKS theorem good_induction (xs : List α) : xs.length = n := by - generalize hlen : xs.length = m -- Generalize first + generalize hlen : xs.length = m rw [hlen] in * - induction xs - · simp -- Base case - · simp [*] -- Inductive case + induction xs <;> simp [*] ``` ---- +## Type errors -## Type Errors +`#check` is the fastest debugger. The error message usually shows expected vs got — read both sides carefully. For `Uint256`/`Nat` mismatches, extract `.val` or coerce with `ofNat`. -### "type mismatch" +## `.run`, `.fst`, `.snd` -**Diagnosis**: Expression has wrong type for context. +Verity contracts are `ContractState → ContractResult α`. Three projection patterns dominate: -**Cause**: Incorrect type annotation, coercion needed, or logic error. +| Expression | Returns | Use for | +|------------|---------|---------| +| `(op).run s` | Full `ContractResult α` | Match on success/revert | +| `((op).run s).fst` | Return value `α` | Prove what a getter returns | +| `((op).run s).snd` | Output state | Prove how state changes | -**Solution 1**: Check types -```lean --- Use #check to debug -#check myValue -- Expected: Uint256, Got: Nat - --- Add explicit coercion -example : Uint256 := ofNat myNatValue -- ✅ -``` +`.fst` returns `default` on revert — if the operation might revert, add a guard hypothesis or match the full result. Avoid `Contract.runState`/`Contract.runValue` in new proofs. -**Solution 2**: Check expected vs actual -```lean --- Error message shows: --- Expected: a.val + b.val ≤ MAX_UINT256 --- Got: a + b ≤ MAX_UINT256 +## Storage reasoning --- Fix: Extract .val explicitly -have h : a.val + b.val ≤ MAX_UINT256 := by assumption -``` +**Function extensionality.** Two storage functions equal? Use `ext slot` and split: -**Solution 3**: Rewrite to match types -```lean --- Use rw to convert types -rw [theorem_that_converts_type] -exact my_proof -``` - ---- - -## Arithmetic & Overflow Proofs - -### SafeAdd/SafeSub Failures - -**Pattern 1**: Proving safeAdd returns Some -```verity --- Goal: safeAdd a b = some c -theorem safeAdd_proof (h : a.val + b.val ≤ MAX_UINT256) : - safeAdd a b = some ⟨a.val + b.val, by omega⟩ := by - unfold safeAdd - simp [willAddOverflow_eq_false h] - -- Now prove the value is correct - rfl -``` - -**Pattern 2**: Proving addition doesn't overflow -```lean --- Common pattern for increment proofs -theorem increment_no_overflow (h : count.val < MAX_UINT256) : - willAddOverflow count 1 = false := by - unfold willAddOverflow - simp - omega -- Uses h to show count.val + 1 ≤ MAX_UINT256 -``` - -**Pattern 3**: Bounded arithmetic -```verity --- Prove result stays in bounds -theorem bounded_add (h1 : a.val ≤ bound) (h2 : b.val ≤ bound) : - (safeAdd a b).isSome → (safeAdd a b).get!.val ≤ 2 * bound := by - intro hsome - have hval : (safeAdd a b).get! = ⟨a.val + b.val, _⟩ := by - simp [safeAdd] at hsome ⊢ - omega - simp [hval] - omega -- Uses h1, h2 -``` - ---- - -## Contract Execution: `.run`, `.fst`, `.snd` - -Verity contracts are functions `ContractState → ContractResult α`. Use these to extract results: - -| Expression | Returns | Type | When to use | -|------------|---------|------|-------------| -| `(op).run s` | Full result | `ContractResult α` | Matching on success/revert | -| `((op).run s).fst` | Return value | `α` | Proving what a getter returns | -| `((op).run s).snd` | Output state | `ContractState` | Proving how state changes | - -**Common patterns in actual proofs:** - -```lean --- Proving a getter returns the right value -theorem retrieve_meets_spec (s : ContractState) : - let result := ((retrieve).run s).fst -- extract return value - retrieve_spec result s := by ... - --- Proving a setter modifies state correctly -theorem store_meets_spec (s : ContractState) (value : Uint256) : - let s' := ((store value).run s).snd -- extract output state - store_spec value s s' := by ... - --- Proving a guarded operation succeeds -theorem increment_unfold (s : ContractState) (h : ...) : - (increment).run s = ContractResult.success () -- match full result - { storage := ..., ... } := by ... -``` - -**Important caveat**: `.fst` returns `default` on revert. If the operation might revert, either: -- Add a guard hypothesis (e.g., `h_no_overflow : ...`) to ensure success -- Match on the full `ContractResult` instead - -Avoid `Contract.runState` and `Contract.runValue` in new proofs — use `((op).run s).snd` and `((op).run s).fst` directly. The `run` + projection pattern is used by all existing proofs and works better with `simp`. - ---- - -## Storage State Reasoning - -### Function Extensionality - -**Problem**: Prove two storage functions are equal. - -**Pattern**: Use `ext` tactic -```verity --- Goal: state1.storage = state2.storage -theorem storage_equal : state1.storage = state2.storage := by - ext slot -- For all slots - by_cases h : slot = targetSlot - · simp [h] -- Show target slot is equal - · simp [h] -- Show other slots unchanged -``` - -### Storage Unchanged Except - -**Pattern**: Common in contract proofs ```verity --- Goal: Only slot k changed theorem only_slot_k_changed : ∀ slot, slot ≠ k → state'.storage slot = state.storage slot := by intro slot hneq @@ -328,24 +107,8 @@ theorem only_slot_k_changed : simp [setStorage, hneq] ``` -### Sequential Operations - -**Problem**: Multiple storage updates in sequence. - -**Pattern**: Use `have` to chain `_meets_spec` lemmas (see Counter proofs) -```lean --- Actual pattern from Counter/Basic.lean -theorem increment_twice_adds_two (s : ContractState) : - let s' := ((increment).run s).snd - let s'' := ((increment).run s').snd - s''.storage 0 = EVM.Uint256.add (EVM.Uint256.add (s.storage 0) 1) 1 := by - have h1 := increment_adds_one s -- First op - have h2 := increment_adds_one (((increment).run s).snd) -- Second op - calc ... = ... := h2 - _ = ... := by rw [h1] -``` +**Sequential operations.** Chain `_meets_spec` lemmas with `have`, or unfold `bind` for low-level reasoning: -For low-level multi-update proofs, unfold bind directly: ```verity theorem two_updates (s : ContractState) : let s' := ((do setStorage slot1 val1; setStorage slot2 val2).run s).snd @@ -353,435 +116,88 @@ theorem two_updates (s : ContractState) : simp [bind, Bind.bind, setStorage, Contract.run, ContractResult.snd] ``` ---- - -## Proof Pattern Library - -### Authorization Checks - -```lean --- Pattern: Operation succeeds when authorized -theorem authorized_succeeds (state : ContractState) (sender : Address) - (h : state.storageAddr owner.slot = sender) : - ((operation sender).run state).isSuccess = true := by - unfold operation onlyOwner require - simp [h] -- Simplifies sender = owner check - -- Prove rest of operation -``` - -### Induction on Nat - -```lean --- Pattern: Structural induction -theorem by_nat_induction : ∀ n : Nat, P n := by - intro n - induction n with - | zero => - -- Base case: P 0 - constructor - simp - | succ k ih => - -- Inductive case: P k → P (k+1) - constructor - simp [ih] -- Use inductive hypothesis -``` - -### Induction on Lists - -```lean --- Pattern: List induction -theorem by_list_induction (xs : List α) : Q xs := by - induction xs with - | nil => - -- Base case: Q [] - simp [Q] - | cons head tail ih => - -- Inductive case: Q tail → Q (head :: tail) - simp [Q, ih] -``` - -### Case Analysis - -```lean --- Pattern: Boolean case split -theorem by_bool_cases (b : Bool) : R b := by - cases b - · -- Case: b = false - simp [R] - · -- Case: b = true - simp [R] -``` - -### Option Handling - -```lean --- Pattern: Option.isSome vs Option.get? -theorem option_proof (opt : Option α) (h : opt.isSome) : - opt.get! = value := by - cases opt - · contradiction -- opt = none contradicts h - · simp -- opt = some x, prove x = value -``` +## Real examples ---- +Verity proofs follow the **`_meets_spec` pattern**: each EDSL operation has a `_spec` predicate, and the proof shows the operation satisfies it. -## Tactic Ordering +### Read-only (SimpleStorage) -**Preferred (Verity standard)**: ```lean --- ✅ BEST: Pass all definitions to simp in one call -theorem retrieve_meets_spec (s : ContractState) : - let result := ((retrieve).run s).fst - retrieve_spec result s := by - simp [retrieve, storedData, retrieve_spec] -- One shot -``` - -**Alternative when simp can't unfold**: -```verity --- ✅ OK: unfold first, then simp -theorem good_order : getValue state = value := by - unfold getValue -- Expose the definition - simp [getStorage] -- Now simp can work with it -``` - -**General rule**: Pass definitions directly to `simp` (e.g. `simp [myDef, mySlot]`). Use `unfold` only when `simp` can't unfold a definition on its own (e.g., mutually recursive definitions). - ---- - -## Common Error Messages - -### Import Errors - -| Error | Cause | Fix | -|-------|-------|-----| -| "unknown identifier 'Uint256'" | Missing import | `import Verity.EVM.Uint256` | -| "unknown identifier 'Contract'" | Missing import | `import Verity.Core` and `open Verity` | -| "unknown identifier 'ContractState'" | Missing import | `import Verity.Core` and `open Verity` | -| "ambiguous identifier" | Multiple imports | Use fully qualified name | - -### Type Class Errors - -| Error | Cause | Fix | -|-------|-------|-----| -| "failed to synthesize OfNat" | Missing numeric instance | Check type has OfNat instance | -| "failed to synthesize Inhabited" | No default value | Provide explicit value | -| "failed to synthesize DecidableEq" | Can't decide equality | Use `= true` or `= false` explicitly | - -### Proof Errors - -| Error | Cause | Fix | -|-------|-------|-----| -| "unsolved goals" | Proof incomplete | Add sorry to see remaining goals | -| "maximum recursion depth" | Infinite tactic loop | Add fuel or use different tactic | -| "kernel type mismatch" | Proof term invalid | Check proof type matches theorem | -| "deterministic timeout" | Proof too expensive | Simplify or add intermediate lemmas | - ---- - -## Proof Performance - -### Slow Proofs (>10 seconds) - -**Problem**: Proof takes too long. - -**Diagnosis**: Expensive tactics on large terms. - -**Solution 1**: Cache intermediate results -```lean --- ❌ SLOW: Recomputes expensive_lemma multiple times -theorem slow_proof : ... := by - simp [expensive_lemma args] - rw [expensive_lemma args] - exact expensive_lemma args - --- ✅ FAST: Compute once, reuse -theorem fast_proof : ... := by - have h := expensive_lemma args -- Compute once - simp [h] - rw [h] - exact h -``` - -**Solution 2**: Split into smaller lemmas -```lean --- Instead of one giant proof -theorem giant_proof : A ∧ B ∧ C ∧ D := by - constructor; [proof of A] - constructor; [proof of B] - constructor; [proof of C] - [proof of D] - --- Split into pieces -theorem prove_A : A := by [proof] -theorem prove_B : B := by [proof] -theorem prove_C : C := by [proof] -theorem prove_D : D := by [proof] - --- Combine quickly -theorem fast_proof : A ∧ B ∧ C ∧ D := ⟨prove_A, prove_B, prove_C, prove_D⟩ -``` - -**Solution 3**: Use rfl instead of simp -```lean --- ❌ SLOW: simp does lots of work -example : (a + 0) = a := by simp - --- ✅ FAST: rfl is instant for definitional equality -example : (a + 0) = a := rfl -- Works if definitionally equal -``` - ---- - -## Debugging Workflows - -### Workflow 1: Unknown Error - -1. **Read error message carefully** - Often points to exact issue -2. **Use #check** on terms mentioned in error -3. **Simplify** - Remove parts of proof until it works -4. **Add sorry** - See remaining goals after partial proof -5. **Search codebase** - Find similar proofs that worked - -### Workflow 2: Stuck on Goal - -1. **Inspect goal** - `trace "{goal}"` to see full state -2. **Try tactics** systematically: - - `simp` (simplify) - - `unfold` (expand definitions) - - `rw` (rewrite with lemma) - - `omega` (arithmetic) -3. **Split cases** - `by_cases` or `cases` to reduce complexity -4. **Add assumptions** - Use `have` for intermediate steps - -### Workflow 3: Type Mismatch - -1. **Check both types** - `#check expected` and `#check actual` -2. **Look for coercions** - May need `ofNat`, `.val`, etc. -3. **Rewrite** - Use `rw [lemma]` to transform type -4. **Convert** - Add explicit conversion functions - ---- - -## Real Examples from Verity - -Verity proofs follow the **`_meets_spec` pattern**: each EDSL operation has a corresponding `_spec` predicate, and the proof shows the operation satisfies it. This is the dominant pattern across all verified contracts. - -### Example 1: SimpleStorage retrieve (spec-based proof) - -**Goal**: Prove `retrieve` returns the stored value. - -```lean --- The spec predicate (defined in Specs/SimpleStorage/Spec.lean) -def retrieve_spec (result : Uint256) (s : ContractState) : Prop := - result = s.storage storedData.slot - --- The proof (from Proofs/SimpleStorage/Basic.lean) theorem retrieve_meets_spec (s : ContractState) : let result := ((retrieve).run s).fst retrieve_spec result s := by simp [retrieve, storedData, retrieve_spec] ``` -**Key insights**: -- Theorem states the operation's result satisfies a named `_spec` predicate -- Single `simp` with the operation, slot name, and spec definition — no `unfold` needed -- `((op).run s).fst` extracts the return value; `.snd` extracts the output state - -### Example 2: Counter increment (multi-conjunct spec) +Single `simp` with operation + slot + spec — no `unfold` needed. -**Goal**: Prove `increment` updates count and preserves everything else. +### Multi-conjunct spec (Counter) ```verity --- The spec is a conjunction: correct value ∧ other slots preserved ∧ context preserved theorem increment_meets_spec (s : ContractState) : let s' := ((increment).run s).snd increment_spec s s' := by - refine ⟨?_, ?_, ?_⟩ -- Split the conjunction into 3 goals - · rfl -- Goal 1: s'.storage 0 = add (s.storage 0) 1 - · intro slot h_neq -- Goal 2: other slots unchanged + refine ⟨?_, ?_, ?_⟩ + · rfl + · intro slot h_neq simp only [increment, count, getStorage, setStorage, bind, Contract.run, Bind.bind, ContractResult.snd] split · next h => exact absurd (by simp [beq_iff_eq] at h; exact h) h_neq · rfl - · simp [Specs.sameAddrMapContext, ...] -- Goal 3: context preserved + · simp [Specs.sameAddrMapContext] ``` -**Key insights**: -- `refine ⟨?_, ?_, ?_⟩` splits a conjunction into separate goals -- Each conjunct is proved independently (value correctness, isolation, context preservation) -- When `simp` alone doesn't close a goal, use `split` for `if`-expressions and `exact absurd` for contradictions +`refine ⟨?_, ?_, ?_⟩` splits a conjunction; prove each conjunct independently. -### Example 3: Owned transferOwnership (require-guarded proof) - -**Goal**: Prove ownership transfer works when the caller is the current owner. +### `require`-guarded (Owned) ```verity theorem transferOwnership_meets_spec_when_owner (s : ContractState) (newOwner : Address) (h_is_owner : s.sender = s.storageAddr 0) : let s' := ((transferOwnership newOwner).run s).snd transferOwnership_spec newOwner s s' := by - -- Unfold the full chain: transferOwnership → onlyOwner → isOwner → require → setStorageAddr simp only [transferOwnership, onlyOwner, isOwner, owner, msgSender, getStorageAddr, setStorageAddr, Verity.require, Verity.pure, Verity.bind, Bind.bind, Pure.pure, - Contract.run, ContractResult.snd, ContractResult.fst, - transferOwnership_spec] - -- After unfolding, the guard is (s.sender == s.storageAddr 0) - -- h_is_owner resolves it, so execution proceeds to setStorageAddr - simp [h_is_owner, Specs.sameStorageMapContext, ...] + Contract.run, ContractResult.snd, transferOwnership_spec] + simp [h_is_owner, Specs.sameStorageMapContext] intro slot h_neq simp [beq_iff_eq, h_neq] ``` -**Key insights**: -- `require`/`onlyOwner` guards add a hypothesis like `h_is_owner : s.sender = s.storageAddr 0` -- Pass the guard hypothesis to `simp` so it can resolve the boolean check -- After the guard resolves, the proof proceeds like an unguarded operation - -### Example 4: Ledger sum preservation (conservation proof) +Pass the guard hypothesis to `simp` so it can resolve the boolean check. -**Goal**: Total balance unchanged by transfer (accounts for duplicate addresses). +### Conservation (Ledger) ```lean --- Uses countOcc to handle addresses appearing multiple times in the list theorem transfer_sum_preservation (s : ContractState) (to : Address) (amount : Uint256) (addrs : List Address) (h_guard : ...) : let s' := ((transfer to amount).run s).snd balanceSum s' addrs + countOccU s.sender addrs * amount = balanceSum s addrs + countOccU to addrs * amount := by - -- Strategy: use point_update_sum_eq for sender (subtract) and recipient (add) have h_sender := point_update_sum_eq ... have h_recipient := point_update_sum_eq ... - -- Combine with omega for final arithmetic omega ``` -**Key insights**: -- Conservation proofs use `countOcc` to account for duplicate addresses in the sum -- Helper lemma `point_update_sum_eq` relates storage point-updates to sum changes -- `omega` handles the final linear arithmetic after `have` statements set up equations +Conservation uses `countOcc` for duplicate-safe sums; helper lemmas stage the equation, omega finishes. ### Pattern summary -| Pattern | When to use | Example | -|---------|-------------|---------| -| `simp [op, slot, spec]` | Simple read-only operations | `retrieve_meets_spec` | -| `refine ⟨?_, ?_, ?_⟩` | Multi-conjunct specs | `increment_meets_spec` | -| `simp only [... chain ...]` + `simp [h_guard]` | Guarded operations with `require` | `transferOwnership_meets_spec_when_owner` | -| `have h := helper ...` + `omega` | Conservation / arithmetic properties | `transfer_sum_preservation` | - ---- - -## Getting Help - -### When to Ask for Help - -Try these first: -1. ✅ Read this guide -2. ✅ Search codebase for similar proofs -3. ✅ Use diagnostic tools (#check, trace) -4. ✅ Simplify to minimal failing example - -If still stuck: -- **GitHub Discussions**: Post minimal example -- **Issues**: If you found a bug or missing documentation -- **Lean Zulip**: For general Lean questions - -### Minimal Example Template - -```lean --- Minimal failing example for help requests -import Verity.Core - --- Context -def myDefinition : Type := ... - --- What I'm trying to prove -theorem my_theorem : myProperty := by - unfold myDefinition - simp - -- ERROR: simp made no progress - sorry - --- What I expected: ... --- What I got: ... -``` - ---- - -## Advanced Debugging - -### Proof Term Inspection - -```lean --- See the proof term Lean generates -#print my_theorem -- Shows proof term - --- Check if proof is what you expect -example : ... := proof_term -- Manually write proof term -``` - -### Tactic Tracing - -```lean --- Enable tactic tracing -set_option trace.Meta.Tactic.simp true - -theorem my_theorem : ... := by - simp -- Will show all simplification steps -``` - -### Goal State Logging +| Pattern | When | +|---------|------| +| `simp [op, slot, spec]` | Simple read-only | +| `refine ⟨?_, ?_, ?_⟩` | Multi-conjunct specs | +| `simp only [...]` then `simp [h_guard]` | Guarded operations | +| `have h := helper ...` then `omega` | Conservation / arithmetic | -```lean --- Log intermediate states -theorem complex_proof : ... := by - trace "Initial goal: {goal}" - unfold definition1 - trace "After unfold: {goal}" - simp - trace "After simp: {goal}" - omega -``` - ---- +## Tactic ordering -## Summary: Quick Decision Tree - -**Proof fails?** -→ Read error message - -**"unknown identifier"?** -→ Check imports, spelling - -**"type mismatch"?** -→ Use #check, add coercion - -**"simp made no progress"?** -→ Add unfold first - -**"omega failed"?** -→ Split cases with by_cases - -**Proof too slow?** -→ Cache intermediate results with have - -**Still stuck?** -→ Search for similar proofs, ask for help - ---- - -## Additional Resources - -- **First Contract Tutorial**: [/guides/first-contract](/guides/first-contract) - Start here if new -- **Code Comment Conventions**: [CONTRIBUTING.md](https://github.com/Th0rgal/verity/blob/main/CONTRIBUTING.md) - Style guide -- **Proof Structure**: [Compiler/Proofs/README.md](https://github.com/Th0rgal/verity/blob/main/Compiler/Proofs/README.md) - Architecture -- **Lean 4 Manual**: [https://lean-lang.org/lean4/doc/](https://lean-lang.org/lean4/doc/) - Language reference -- **Lean Zulip**: [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/) - Community chat - ---- +Prefer one-shot `simp [def, slot, spec]`. Use `unfold` only when `simp` can't expose a definition on its own (e.g., mutually recursive). Don't sprinkle `unfold`s when one `simp` would do. -**Happy Proving! 🎉** +## See also -Remember: Every expert was once stuck on "simp made no progress". You've got this! +- [First Contract](/first-contract) — the full workflow this guide drops into. +- [Core Architecture](/core) — types and the `Contract` monad. +- [EDSL API Reference](/edsl-api-reference) — every primitive with its simp lemma. diff --git a/docs-site/content/guides/first-contract.mdx b/docs-site/content/guides/first-contract.mdx deleted file mode 100644 index a5a010d28..000000000 --- a/docs-site/content/guides/first-contract.mdx +++ /dev/null @@ -1,698 +0,0 @@ ---- -title: Adding Your First Contract -description: Step-by-step tutorial for creating a verified smart contract in Verity ---- - -# Adding Your First Contract to Verity - -**Time Required**: 2-3 hours for first contract -**Prerequisites**: Basic familiarity with Lean 4 syntax and smart contract concepts - -> **New to Lean 4?** You'll need to understand `do` notation, `def`/`theorem`, and basic tactic proofs (`simp`, `intro`, `constructor`). Start with: -> - [Lean 4 Manual: Basics](https://lean-lang.org/lean4/doc/): language overview -> - [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/): chapters 1–5 cover everything needed here -> - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/): `do` notation and monads (chapter 4) - -This tutorial walks you through creating a complete verified smart contract from scratch. We'll build a **TipJar** contract, a simple balance ledger where users can deposit tips and check balances. - -> **Why TipJar?** It uses the core EDSL features (mappings, `msgSender`, `require`, arithmetic) while staying simple enough to prove fully on your first attempt. - ---- - -## Overview: The Verity Workflow - -Every contract follows this path: - -``` -Specification → Implementation → Proofs → Compilation → Testing - (30m) (45m) (1-2h) (auto) (30m) -``` - -**What you'll learn**: -- How to write formal specifications -- How to implement contracts in the EDSL -- How to prove correctness properties -- How to compile and test against deployed bytecode - ---- - -## Phase 1: Setup (15 minutes) - -### 1.1 Use the Scaffold Generator - -The easiest way to start is with the scaffold generator: - -```bash -python3 scripts/generate_contract.py TipJar \ - --fields "tips:mapping" \ - --functions "tip(uint256),getBalance(address)" -``` - -This creates all required files: -- `Contracts/TipJar/Spec.lean`: formal specification -- `Contracts/TipJar/Invariants.lean`: state invariants -- `Contracts/TipJar/SpecProofs.lean`: compilation correctness proof re-export -- `Contracts/TipJar/TipJar.lean`: EDSL implementation -- `Contracts/TipJar/Proofs/Basic.lean`: basic correctness proofs (EDSL matches spec) -- `Contracts/TipJar/Proofs/Correctness.lean`: advanced correctness proofs -- `test/PropertyTipJar.t.sol`: Foundry tests - -### 1.2 Or Create Files Manually - -```bash -mkdir -p Contracts/TipJar/Proofs -touch Contracts/TipJar/Spec.lean -touch Contracts/TipJar/Invariants.lean -touch Contracts/TipJar/SpecProofs.lean -touch Contracts/TipJar/TipJar.lean -touch Contracts/TipJar/Proofs/Basic.lean -touch Contracts/TipJar/Proofs/Correctness.lean -touch test/PropertyTipJar.t.sol -``` - -### 1.3 Our Contract Goal - -We want to build a contract where: -- Users can deposit a tip (adding to their balance) via `tip(uint256)` -- Anyone can check a balance via `getBalance(address) → uint256` -- Each address has an independent balance -- Balances use EVM modular arithmetic (wrapping on overflow). This matches EVM opcodes, not Solidity's default checked arithmetic - -> **Tip**: For contracts that should match Solidity ^0.8 behavior, add `require` guards (see `SafeCounter` example). - ---- - -## Phase 2: Write Specification (30 minutes) - -Specifications describe **what** the contract should do, not **how** it does it. - -### 2.1 Create the Spec File - -Open `Contracts/TipJar/Spec.lean`: - -```verity -/- - TipJar: Formal Specification - - Specifies deposit and balance-check behavior for a simple tip ledger. --/ - -import Verity.Specs.Common -import Verity.Macro -import Verity.EVM.Uint256 - -namespace Contracts.TipJar.Spec - -open Verity -open Verity.EVM.Uint256 - -/-- tip: increases sender's balance by amount -/ -def tip_spec (amount : Uint256) (s s' : ContractState) : Prop := - -- Sender's balance increases by amount (modular arithmetic) - s'.storageMap 0 s.sender = add (s.storageMap 0 s.sender) amount ∧ - -- No other mapping entries change - storageMapUnchangedExceptKeyAtSlot 0 s.sender s s' ∧ - -- Non-mapping storage and context are preserved - sameStorageAddrContext s s' - -/-- getBalance: returns balance at given address, no state change -/ -def getBalance_spec (addr : Address) (result : Uint256) (s : ContractState) : Prop := - result = s.storageMap 0 addr - -end Contracts.TipJar.Spec -``` - -**Key Concepts**: -- `s` is the initial state, `s'` is the final state after the operation -- `storageMap 0` refers to the mapping at storage slot 0 -- `storageMapUnchangedExceptKeyAtSlot` says only one key changed at one slot -- `sameStorageAddrContext` says uint256 storage, address storage, and context are preserved -- `add` is EVM modular addition (wraps at 2^256) - -### 2.2 Create Invariants File - -Open `Contracts/TipJar/Invariants.lean`: - -```verity -/- - TipJar: State Invariants - - Properties that hold across all operations. --/ - -import Verity.Specs.Common - -namespace Contracts.TipJar.Invariants - -open Verity - --- Tip operations don't affect regular storage slots -def uint_storage_unchanged (s s' : ContractState) : Prop := - s'.storage = s.storage - --- Tip operations don't affect address storage -def addr_storage_unchanged (s s' : ContractState) : Prop := - s'.storageAddr = s.storageAddr - -end Contracts.TipJar.Invariants -``` - ---- - -## Phase 3: Implement in EDSL (45 minutes) - -Now we implement the contract using the EDSL. Every function in the EDSL is a `Contract`, a state-transforming computation that can succeed or revert. - -### 3.1 Create EDSL Implementation - -Open `Contracts/TipJar/TipJar.lean`: - -```verity -/- - TipJar: Deposit tips and check balances - - Demonstrates: - - Mapping storage (Address → Uint256) - - Sender identification via msgSender - - EVM modular arithmetic - - Pattern: Simple balance ledger --/ - -import Contracts.Common - -namespace Contracts.TipJar - -open Verity hiding pure bind -open Verity.EVM.Uint256 - --- Storage layout: tips mapping at slot 0 -def tips : StorageSlot (Address → Uint256) := ⟨0⟩ - --- Deposit a tip: add amount to sender's balance -def tip (amount : Uint256) : Contract Unit := do - let sender ← msgSender - let currentBalance ← getMapping tips sender - setMapping tips sender (add currentBalance amount) - --- Look up balance for any address -def getBalance (addr : Address) : Contract Uint256 := do - getMapping tips addr - --- Example: Alice tips 100, then we check her balance -def exampleUsage : Contract Uint256 := do - tip 100 - getBalance "0xAlice" - -#eval (exampleUsage.run { defaultState with - sender := "0xAlice", - thisAddress := "0xTipJar" -}).getValue? --- Expected output: some 100 - -end Contracts.TipJar -``` - -**EDSL API reference** (from `Verity/Core.lean`): - -| Function | Type | Description | -|----------|------|-------------| -| `msgSender` | `Contract Address` | Get transaction sender | -| `msgValue` | `Contract Uint256` | Get ETH value sent with call | -| `blockTimestamp` | `Contract Uint256` | Get current block timestamp | -| `getStorage s` | `Contract Uint256` | Read uint256 slot | -| `setStorage s val` | `Contract Unit` | Write uint256 slot | -| `getMapping s key` | `Contract Uint256` | Read mapping entry | -| `setMapping s key val` | `Contract Unit` | Write mapping entry | -| `getStorageAddr s` | `Contract Address` | Read address slot | -| `setStorageAddr s val` | `Contract Unit` | Write address slot | -| `require cond msg` | `Contract Unit` | Revert if condition is false | - -> **Tip**: Use `defaultState` to create a zero-initialized state for testing: -> ```lean -> #eval (myContract.run { defaultState with sender := "0xAlice" }).getValue? -> ``` -> This avoids spelling out every field and stays valid when new fields are added. - -### 3.2 Test the EDSL Implementation - -```bash -lake build Contracts.TipJar -``` - -If successful, the `#eval` block evaluates and prints `some 100`. - ---- - -## Phase 4: Prove Correctness (1-2 hours) - -This is where formal verification happens. We prove that our implementation matches our specification. - -### 4.1 Write Contract Specification Proofs - -Open `Contracts/TipJar/Proofs/Basic.lean`: - -```verity -/- - TipJar: Basic Correctness Proofs - - Prove that the EDSL implementation matches the formal specification. --/ - -import Contracts.TipJar.Spec -import Contracts.TipJar.Invariants -import Verity.Proofs.Stdlib.Automation - -namespace Contracts.TipJar.Proofs - -open Verity -open Verity.EVM.Uint256 -open Contracts.TipJar -open Contracts.TipJar.Spec - --- tip: implementation matches spec -theorem tip_meets_spec (s : ContractState) (amount : Uint256) : - tip_spec amount s (((tip amount).run s).snd) := by - simp [tip, tip_spec, tips, msgSender, getMapping, setMapping, bind, - Specs.storageMapUnchangedExceptKeyAtSlot, - Specs.storageMapUnchangedExceptKey, Specs.storageMapUnchangedExceptSlot, - Specs.sameStorageAddrContext, Specs.sameStorage, Specs.sameStorageAddr, - Specs.sameContext] - constructor - · simp [Contract.run] - · constructor - · constructor - · intro other hne; simp [*] - · intro other hne addr; simp [*] - · simp - --- getBalance: returns the correct value -theorem getBalance_correct (s : ContractState) (addr : Address) : - getBalance_spec addr (((getBalance addr).run s).fst) s := by - simp [getBalance, getBalance_spec, tips, getMapping] - --- getBalance doesn't modify state -theorem getBalance_preserves_state (s : ContractState) (addr : Address) : - ((getBalance addr).run s).snd = s := by - simp [getBalance, tips, getMapping] - --- Roundtrip: tip then getBalance returns updated balance -theorem tip_getBalance_roundtrip (amount : Uint256) (s : ContractState) : - let s' := ((tip amount).run s).snd - ((getBalance s.sender).run s').fst = add (s.storageMap 0 s.sender) amount := by - simp [tip, getBalance, tips, msgSender, getMapping, setMapping, bind] - -end Contracts.TipJar.Proofs -``` - -### 4.2 Common Proof Patterns - -Here are the tactics you'll use most often: - -**Pattern 1: Simple proofs with simp** -```lean -theorem simple_property : ... := by - simp [functionName, helperFunctions] -``` - -**Pattern 2: Proofs with case splits** -```lean -theorem conditional_property : ... := by - unfold functionName - split - · -- Case 1: condition true - simp [...] - · -- Case 2: condition false - simp [...] -``` - -**Pattern 3: Proofs requiring intermediate lemmas** -```lean -theorem main_property : ... := by - have h1 := helper_lemma_1 - have h2 := helper_lemma_2 - simp [h1, h2, ...] -``` - -See [Proof Debugging Handbook](/guides/debugging-proofs) for common errors and fixes. - -### 4.3 Build and Check Proofs - -```bash -# Build all proofs -lake build - -# Check for incomplete proofs -grep -r "sorry" Contracts/TipJar/ -``` - -**Goal**: Zero `sorry` statements before moving to testing. - ---- - -## Phase 5: Add to Compiler (15 minutes) - -### 5.1 Add Canonical Compiler Declaration - -Add your contract in `Contracts//.lean` with `verity_contract`. -Then register `Contracts..spec` in `Compiler/Specs.lean` under `allSpecs`: - -```verity -verity_contract TipJar where - storage - tips : Address -> Uint256 := slot 0 - - function tip (amount : Uint256) : Unit := do - let sender <- msgSender - let current ← getMapping tips sender - setMapping tips sender (add current amount) - - function getBalance (addr : Address) : Uint256 := do - return (← getMapping tips addr) -``` - -### 5.2 Legacy Note - -Handwritten `Compiler.Specs.*Spec` definitions are retained for proof-migration and -special workflows only; they are not the canonical CLI compile path. - -Function selectors (the first 4 bytes of `keccak256("functionName(paramTypes)")`) are computed automatically by `computeSelectors` during compilation. - -> **Tip**: Run `python3 scripts/check_selectors.py` to verify that the auto-computed selectors match `solc --hashes` output. You can also compute selectors manually with `python3 scripts/keccak256.py "tip(uint256)" "getBalance(address)"`. - -### 5.3 Compilation Correctness - -When you define a contract using the `verity_contract` macro in `Contracts//.lean`, the framework provides the frontend typed-IR correctness path in `Compiler/TypedIRCompilerCorrectness.lean`. For the current explicit supported fragment, the compiler-level `CompilationModel -> IR` result now lives in `Compiler/Proofs/IRGeneration/Contract.lean` as a generic whole-contract theorem rooted at successful `CompilationModel.compile`. - -The compiler proves Layer 2 preservation automatically for the supported fragment, with no manual per-contract bridge proofs needed. All three compiler layers are fully proved with 0 sorry and 0 axioms. The remaining trusted boundary is `solc` (Yul to bytecode). See `AXIOMS.md` for details. - -> **Tip**: Study `Compiler/TypedIRCompilerCorrectness.lean` to see the supported statement fragment grammar and bridge theorem examples for Counter, SimpleStorage, ERC20, and ERC721. - -### 5.4 Generate Yul Code - -```bash -lake build verity-compiler -lake exe verity-compiler - -# Check output -ls artifacts/yul/TipJar.yul -``` - -### 5.5 Verify Compilation - -```bash -python3 scripts/check_yul.py -``` - ---- - -## Phase 6: Testing (30 minutes) - -### 6.1 Create Property Tests - -Open `test/PropertyTipJar.t.sol`. This is a complete, working test file you can copy-paste: - -```solidity -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.33; - -import "./yul/YulTestBase.sol"; - -/** - * @title PropertyTipJarTest - * @notice Property tests matching Lean theorems from Contracts/TipJar/Proofs/Basic.lean - * - * Tests 4 proven theorems: - * 1. tip_meets_spec - Tip increases sender balance by amount - * 2. getBalance_correct - getBalance returns correct value - * 3. getBalance_preserves_state - getBalance is read-only - * 4. tip_getBalance_roundtrip - Tip then getBalance returns updated balance - */ -contract PropertyTipJarTest is YulTestBase { - address tipjar; - address alice = address(0x1111); - address bob = address(0x2222); - - function setUp() public { - tipjar = deployYul("TipJar"); - require(tipjar != address(0), "Deploy failed"); - } - - //═══════════════════════════════════════════════════════════════════════ - // Property 1: tip_meets_spec (fuzz test) - // Theorem: Tip increases sender's balance by the given amount - //═══════════════════════════════════════════════════════════════════════ - - /// Property: tip_meets_spec - function testProperty_Tip_MeetsSpec(address sender, uint256 amount) public { - // Constrain to avoid overflow in our assertion - vm.assume(amount > 0 && amount <= type(uint256).max / 2); - uint256 before = getBalanceFromStorage(sender); - vm.assume(before + amount <= type(uint256).max); - - // Call tip(uint256) as sender - vm.prank(sender); - (bool success,) = tipjar.call(abi.encodeWithSignature("tip(uint256)", amount)); - require(success, "tip failed"); - - // Assert: sender's balance increased by exactly `amount` - assertEq( - getBalanceFromStorage(sender), - before + amount, - "tip_meets_spec: balance should increase by amount" - ); - } - - //═══════════════════════════════════════════════════════════════════════ - // Property 2: getBalance_correct (fuzz test) - // Theorem: getBalance returns the stored value - //═══════════════════════════════════════════════════════════════════════ - - /// Property: getBalance_correct - function testProperty_GetBalance_Correct(address addr, uint256 amount) public { - // Set a known balance directly in storage - setBalance(addr, amount); - - // Call getBalance(address) - (bool success, bytes memory data) = tipjar.call( - abi.encodeWithSignature("getBalance(address)", addr) - ); - require(success, "getBalance failed"); - uint256 result = abi.decode(data, (uint256)); - - // Assert: returned value matches storage - assertEq(result, amount, "getBalance_correct: should return stored balance"); - } - - //═══════════════════════════════════════════════════════════════════════ - // Property 3: getBalance_preserves_state - // Theorem: getBalance doesn't modify storage - //═══════════════════════════════════════════════════════════════════════ - - /// Property: getBalance_preserves_state - function testProperty_GetBalance_PreservesState(address addr) public { - // Set up some state - setBalance(addr, 42); - uint256 balanceBefore = getBalanceFromStorage(addr); - - // Call getBalance, should be read-only - (bool success,) = tipjar.call( - abi.encodeWithSignature("getBalance(address)", addr) - ); - require(success, "getBalance failed"); - - // Assert: storage unchanged - assertEq( - getBalanceFromStorage(addr), - balanceBefore, - "getBalance_preserves_state: storage should not change" - ); - } - - //═══════════════════════════════════════════════════════════════════════ - // Property 4: tip_getBalance_roundtrip (fuzz test) - // Theorem: Tip then getBalance returns the updated balance - //═══════════════════════════════════════════════════════════════════════ - - /// Property: tip_getBalance_roundtrip - function testProperty_Tip_GetBalance_Roundtrip(uint256 amount) public { - vm.assume(amount <= type(uint256).max / 2); - - uint256 before = getBalanceFromStorage(alice); - - // Tip as alice - vm.prank(alice); - (bool success1,) = tipjar.call(abi.encodeWithSignature("tip(uint256)", amount)); - require(success1, "tip failed"); - - // Read back via getBalance - (bool success2, bytes memory data) = tipjar.call( - abi.encodeWithSignature("getBalance(address)", alice) - ); - require(success2, "getBalance failed"); - uint256 result = abi.decode(data, (uint256)); - - // Assert: roundtrip gives before + amount - assertEq( - result, - before + amount, - "tip_getBalance_roundtrip: should return before + amount" - ); - } - - //═══════════════════════════════════════════════════════════════════════ - // Utility functions (reusable pattern for mapping-based contracts) - //═══════════════════════════════════════════════════════════════════════ - - /// @notice Read a mapping(address => uint256) entry directly from storage - /// @dev TipJar uses slot 0 for the tips mapping. - /// Solidity/Yul mapping layout: keccak256(abi.encode(key, baseSlot)) - function getBalanceFromStorage(address addr) internal view returns (uint256) { - bytes32 slot = keccak256(abi.encode(addr, uint256(0))); - return uint256(vm.load(tipjar, slot)); - } - - /// @notice Write a mapping entry directly (for test setup) - function setBalance(address addr, uint256 amount) internal { - bytes32 slot = keccak256(abi.encode(addr, uint256(0))); - vm.store(tipjar, slot, bytes32(amount)); - } -} -``` - -**Key patterns to understand**: -- `deployYul("TipJar")` deploys your pre-generated `artifacts/yul/TipJar.yul` contract (via `solc` assembly through `vm.ffi`) -- `vm.prank(sender)` sets `msg.sender` for the next call (Foundry cheatcode) -- `vm.load`/`vm.store` read/write raw storage slots (for assertions and test setup) -- Mapping slot formula: `keccak256(abi.encode(key, baseSlot))` (the standard Solidity storage layout) -- `vm.assume(...)` constrains fuzz inputs to avoid false failures (e.g., overflow) - -### 6.2 Run Tests - -```bash -FOUNDRY_PROFILE=difftest forge test --match-contract TipJar -vv -``` - -### 6.3 Verify Property Coverage - -```bash -python3 scripts/extract_property_manifest.py # regenerate manifest with new theorems -python3 scripts/check_property_manifest.py -python3 scripts/report_property_coverage.py --format=markdown -``` - ---- - -## Phase 7: Integration & Validation (15 minutes) - -### 7.1 Final Checklist - -```bash -# 1. All Lean code compiles (including proofs) -lake build - -# 2. No incomplete proofs -grep -r "sorry" Contracts/TipJar/ - -# 3. Yul generates and compiles -lake build verity-compiler -lake exe verity-compiler -python3 scripts/check_yul.py - -# 4. Tests pass -FOUNDRY_PROFILE=difftest forge test --match-contract TipJar - -# 5. All CI checks pass -python3 scripts/check_selectors.py -python3 scripts/extract_property_manifest.py -python3 scripts/check_property_manifest.py -python3 scripts/check_property_manifest_sync.py -python3 scripts/check_property_coverage.py -python3 scripts/check_contract_structure.py -python3 scripts/check_storage_layout.py -python3 scripts/generate_verification_status.py --check -``` - -### 7.2 Add to Module Exports - -Register your contract in the build by adding imports to the appropriate `All.lean` or lakefile target: -```lean -import Contracts.TipJar.Spec -import Contracts.TipJar.Invariants -import Contracts.TipJar.TipJar -import Contracts.TipJar.Proofs.Basic -import Contracts.TipJar.Proofs.Correctness -``` - -> **Tip**: The scaffold generator prints these exact lines when you run it. Copy them directly. - -> **Tip**: Focus on the supported `CompilationModel` (`CompilationModel`) path for compiler-facing work. The scaffold and CI checks in this repository are aligned to that single path. - ---- - -## Common Troubleshooting - -### "Unknown identifier" in proofs - -**Problem**: Lean can't find a function or type. - -**Solution**: Check your imports and `open` statements: -```lean -import Contracts.TipJar.Spec -import Contracts.TipJar.TipJar - -open Verity -open Verity.EVM.Uint256 -``` - -### "Type mismatch" errors - -**Problem**: Wrong return type. - -**Solution**: Check the function signature matches what you return: -```verity -def tip (amount : Uint256) : Contract Unit := do -- Returns nothing - ... - -def getBalance (addr : Address) : Contract Uint256 := do -- Returns Uint256 - ... -``` - -### Proofs don't close with `simp` - -**Problem**: `simp` can't solve the goal. - -**Solution**: Try `unfold` first to expose definitions, then `simp`: -```verity -theorem my_thm : ... := by - unfold myFunction bind - simp [getMapping, setMapping, msgSender, tips] -``` - -See [Proof Debugging Handbook](/guides/debugging-proofs) for more patterns. - -### Tests fail with "selector not found" - -**Problem**: Function selector mismatch between Lean and Solidity. - -**Solution**: -```bash -python3 scripts/check_selectors.py -``` - ---- - -## Next Steps - -1. **Add more properties**: Think of edge cases (zero amount, same sender/receiver) -2. **Add access control**: Look at `Contracts/OwnedCounter/OwnedCounter.lean` for the `require` + owner pattern -3. **Add more functions**: Try adding a `withdraw` with balance checks (see `Contracts/Ledger/Ledger.lean`) -4. **Study existing contracts**: `SimpleStorage` (simplest), `Counter` (arithmetic), `Ledger` (mappings), `OwnedCounter` (composition) - -### Learning Resources - -- [Core Architecture](/core): the full EDSL API reference -- [Compiler](/compiler): how the compilation pipeline works -- [Proof Debugging Handbook](/guides/debugging-proofs): common tactic failures and fixes -- [Lean 4 Manual](https://lean-lang.org/lean4/doc/): language reference -- [Foundry Book](https://book.getfoundry.sh/): testing framework diff --git a/docs-site/content/guides/linking-libraries.mdx b/docs-site/content/guides/linking-libraries.mdx index 3915d4e33..88e96ecfc 100644 --- a/docs-site/content/guides/linking-libraries.mdx +++ b/docs-site/content/guides/linking-libraries.mdx @@ -5,99 +5,49 @@ description: How to use external Yul libraries (Poseidon, Groth16, etc.) with ve # Linking External Libraries -**Time Required**: 30 minutes -**Prerequisites**: Verity project builds (`lake build` passes) +For cryptographic primitives (Poseidon, Groth16, etc.) that are impractical to implement in Lean, or for reusing audited Yul libraries. Your proofs verify contract logic against a placeholder; the real implementation is injected at compile time. -## TL;DR +## How it works -**Step 1** — Write your Yul library (plain functions, no `object` wrapper): -```bash -mkdir -p examples/external-libs -echo 'function myHash(a, b) -> result { result := add(xor(a, b), 0x42) }' > examples/external-libs/MyHash.yul -``` - -**Step 2** — Use a placeholder in your Lean EDSL (for proofs): -```verity -def myHash (a b : Uint256) : Contract Uint256 := return add a b -``` - -**Step 3** — Declare the external function and reference it in your CompilationModel: -```verity --- In your CompilationModel definition: -externals := [ - { name := "myHash" - params := [ParamType.uint256, ParamType.uint256] - returnType := some ParamType.uint256 - proofStatus := .assumed - axiomNames := [] } -] --- In a function body: -Stmt.letVar "h" (Expr.externalCall "myHash" [Expr.param "a", Expr.param "b"]) -``` - -**Step 4** — Compile with linking: -```bash -lake exe verity-compiler --link examples/external-libs/MyHash.yul -o artifacts/yul -``` +1. **Yul library** — plain function definitions, no `object` wrapper. +2. **Lean placeholder** — used only by proofs; never appears in compiled Yul. +3. **`externals` declaration on the `CompilationModel`** — the linker only injects into contracts that declare what they need. +4. **`--link` flag** — pass `.yul` library files at compile time. -Your proofs verify the contract logic (using placeholders). Real implementations are injected at compile time. +## Walkthrough ---- - -## When to Use This - -- You need **cryptographic primitives** (Poseidon hash, Groth16 verification, etc.) that are impractical to implement in Lean -- You want to **reuse audited Yul libraries** without re-implementing them -- You want to **prove contract logic** independently of complex library internals - -## Quick Start - -### 1. Write your library as a `.yul` file - -Create a file with plain Yul function definitions (no `object` wrapper): +**Yul library** (`examples/external-libs/MyHash.yul`): ```yul -// examples/external-libs/MyHash.yul function myHash(a, b) -> result { - // Your implementation here result := add(xor(a, b), 0x42) } ``` -### 2. Write a placeholder in your Lean contract - -In your EDSL contract, define a placeholder that models the same interface: +**Lean placeholder** (used for proofs, ignored at compile time): ```verity --- Placeholder for proofs: models the hash as addition --- At compile time, replaced by the real myHash from MyHash.yul -def myHash (a b : Uint256) : Contract Uint256 := do - return add a b +def myHash (a b : Uint256) : Contract Uint256 := return add a b ``` -### 3. Declare externals and add the call to your CompilationModel - -In `Compiler/Specs.lean`, first declare the external function in the `externals` field of your CompilationModel, then use `Expr.externalCall` in the function body: +**`CompilationModel`** (`Compiler/Specs.lean`): ```verity def myCompilationModel : CompilationModel := { name := "MyContract" fields := [...] - constructor := none - -- Declare external functions used by this contract externals := [ { name := "myHash" params := [ParamType.uint256, ParamType.uint256] returnType := some ParamType.uint256 proofStatus := .assumed - axiomNames := [] } -- Add axiom names if modeling trust assumptions + axiomNames := [] } ] functions := [ { name := "storeHash" params := [...] returnType := none body := [ - -- Call the external function Stmt.letVar "h" (Expr.externalCall "myHash" [Expr.param "a", Expr.param "b"]), ... ] @@ -106,241 +56,55 @@ def myCompilationModel : CompilationModel := { } ``` -> **Important**: The `externals` field is required. Without it, the linker will not inject library functions into this contract's Yul output, even if `--link` is passed. See `cryptoHashSpec` in `Compiler/Specs.lean` for a complete example. - -> **Tip**: `Expr.param` takes the parameter **name** as a string — it must match the `name` field in your function's `params` list. For example, if your function declares `{ name := "a", ty := ParamType.uint256 }`, use `Expr.param "a"`. +> **The `externals` field is required.** Without it, the linker silently skips this contract even if `--link` is passed. `Expr.param "a"` must match the parameter `name` declared in `params`. -### 4. Compile with `--link` +**Compile**: ```bash lake exe verity-compiler --link examples/external-libs/MyHash.yul -o artifacts/yul ``` -The compiler validates that: -- No duplicate function names across libraries -- Library functions don't shadow generated code or Yul builtins -- All external calls in contracts are satisfied by linked libraries - -If validation fails, you get a clear error message: +The linker parses each `.yul`, validates (no duplicate names, no shadowing of Yul builtins or `mappingSlot`, all references resolved, correct arity), and injects functions into the runtime `code {}` block. Unresolved references fail closed: ``` Unresolved external references: myHash ``` -This means you forgot to pass `--link examples/external-libs/MyHash.yul`. - ---- - -## Complete Example: CryptoHash Contract - -Verity includes a working example in [`Verity/Examples/CryptoHash.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Examples/CryptoHash.lean) with libraries in [`examples/external-libs/`](https://github.com/Th0rgal/verity/tree/main/examples/external-libs). - -**EDSL placeholder** (`Verity/Examples/CryptoHash.lean`): -```verity --- Placeholder: just adds the inputs (for proving logic) -def hashTwo (a b : Uint256) : Contract Uint256 := do - return add a b - -def hashThree (a b c : Uint256) : Contract Uint256 := do - return add (add a b) c - -def storeHashTwo (a b : Uint256) : Contract Unit := do - let h ← hashTwo a b - setStorage lastHash h - -def storeHashThree (a b c : Uint256) : Contract Unit := do - let h ← hashThree a b c - setStorage lastHash h -``` - -**External library** (`examples/external-libs/PoseidonT3.yul`): -```yul -function PoseidonT3_hash(a, b) -> result { - // Placeholder — real Poseidon uses field arithmetic and S-boxes - result := add(xor(a, b), 0x1234567890abcdef) -} -``` - -> The EDSL function (`hashTwo`) is a placeholder used only in formal proofs — it never appears in the compiled Yul. The CompilationModel's `Expr.externalCall "PoseidonT3_hash"` is what the compiler actually emits, and the linker resolves it to the library function above. - -**Compile with linking**: -```bash -lake exe verity-compiler \ - --link examples/external-libs/PoseidonT3.yul \ - --link examples/external-libs/PoseidonT4.yul \ - -o artifacts/yul -``` - ---- - -## How the Linker Works - -The linking process has three stages: - -### Stage 1: Parse libraries - -The linker reads each `.yul` file and extracts function definitions using a line-based parser. It tracks brace depth to capture complete function bodies: - -``` -Input file: Parsed output: -function foo() { -> LibraryFunction { name: "foo", body: [...] } - sstore(0, 1) -} -``` - -### Stage 2: Validate - -Four safety checks run before any code is injected: - -| Check | What it catches | -|-------|-----------------| -| `validateNoDuplicateNames` | Two libraries defining the same function | -| `validateNoNameCollisions` | Library function shadowing `mappingSlot` or Yul builtins like `add`, `sstore` | -| `validateExternalReferences` | Contract calling a function not provided by any library | -| `validateCallArity` | Library function called with wrong number of arguments | +## Reference example: CryptoHash -### Stage 3: Inject - -Library functions are injected into the runtime `code {}` section of each compiled Yul contract, with proper indentation: - -```yul -object "MyContract" { - code { /* deploy */ } - object "runtime" { - code { - // ... generated contract code ... - - // Injected from MyHash.yul: - function myHash(a, b) -> result { - result := add(xor(a, b), 0x42) - } - } - } -} -``` - ---- +The repo includes a working setup in [`Contracts/CryptoHash/Contract.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/CryptoHash/Contract.lean) with libraries in [`examples/external-libs/`](https://github.com/lfglabs-dev/verity/tree/main/examples/external-libs). Look at `cryptoHashSpec` in `Compiler/Specs.lean` for a complete `externals` declaration. -## Library File Format +## Trust model -External library files must contain **plain Yul function definitions**: +External libraries are **outside the formal verification boundary**. The linker validates *structure* (no shadowing, resolved references, correct arity); it does not verify *behavior*. Your proofs establish: *if the library functions behave like the placeholders, then the contract is correct*. -```yul -// Good: plain function definitions -function foo(x) -> y { - y := add(x, 1) -} +In practice: a contract using `PoseidonT3_hash` via the linker has formally verified logic (storage, access control, arithmetic) but an *unverified* cryptographic core. The proof guarantees the contract correctly *uses* the hash; it does not guarantee the hash *is* Poseidon. Auditing the `.yul` library is the developer's responsibility. -function bar(a, b) -> c { - c := mul(a, b) -} -``` +To increase confidence: use audited implementations, add Foundry tests that exercise the linked contract end-to-end, compare library output against a reference, and document the assumption in [`TRUST_ASSUMPTIONS.md`](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md). -Do **not** wrap them in an `object` block: +## CLI -```yul -// Bad: object wrapper not supported -object "MyLib" { - code { - function foo(x) -> y { y := add(x, 1) } - } -} ``` - ---- - -## Trust Model - -External libraries are **outside the formal verification boundary**. The Linker validates structural properties (no shadowing, all references resolved, correct arity) but does not verify the library's correctness. - -Your proofs establish: *"If the library functions behave like the placeholders, then the contract is correct."* - -**What this means in practice**: A contract using `PoseidonT3_hash` via the linker has formally verified *logic* (storage updates, access control, arithmetic) but an *unverified* cryptographic core. The Lean proof guarantees that IF `PoseidonT3_hash(a, b)` returns a consistent value, THEN the contract correctly stores and retrieves it. The proof does NOT guarantee the Poseidon implementation computes the correct hash — auditing the `.yul` library file is the developer's responsibility. - -> Without the `externals` field on a `CompilationModel`, the linker will skip that contract even if `--link` is passed. No injection occurs and no error is raised. - -To increase confidence in linked libraries: -- Use audited, battle-tested implementations -- Add Foundry fuzz tests that exercise the linked contract end-to-end -- Compare library output against a known reference implementation -- Document the trust assumption explicitly (see [`TRUST_ASSUMPTIONS.md`](https://github.com/Th0rgal/verity/blob/main/TRUST_ASSUMPTIONS.md)) - ---- - -## Common Issues and Debugging - -### Function name mismatch - -If you see `Unresolved external references: myFunc`, check that: -- The function name in your CompilationModel matches the Yul library exactly (case-sensitive) -- The library file is properly formatted with plain function definitions - -### Arity mismatch - -If you see `Arity mismatch: myFunc: called with N args but library defines M params`: -- The number of parameters in your `Expr.externalCall` must match the library function -- Remember: return values don't count as parameters - -### Runtime errors with linked contracts - -If your verified contract works with placeholders but fails with linked libraries: -1. **Check gas requirements**: Linked functions may use more gas than placeholders -2. **Verify return types**: Ensure the library returns the expected type -3. **Test with Foundry**: Add property tests that run against the linked contract - -### Debugging tips - -```bash -# Generate Yul output to see how external calls are rendered -lake exe verity-compiler --link examples/external-libs/MyLib.yul -o artifacts/yul -v - -# Check the generated Yul in artifacts/yul/ -cat artifacts/yul/*.yul -``` - ---- - -## CLI Reference - -```bash lake exe verity-compiler [options] -lake exe verity-compiler-patched [patch-options] -Options: - --link Link external Yul library (can be used multiple times) - --output Output directory (default: artifacts/yul) - -o Short form of --output - --abi-output Output ABI JSON artifacts (.abi.json) - --backend-profile - --mapping-slot-scratch-base Scratch memory base for mappingSlot helper (default: 0) - --verbose Enable verbose output - -v Short form of --verbose - --help Show help message +--link Link external Yul library (repeatable) +-o, --output Output directory (default: artifacts/yul) +--abi-output Output ABI JSON artifacts +--backend-profile

semantic (default) | solidity-parity-ordering +--mapping-slot-scratch-base Scratch memory base for mappingSlot +-v, --verbose +--help ``` -`--backend-profile` controls deterministic output-shape normalization: -- `semantic`: default behavior. -- `solidity-parity-ordering`: sort dispatch `case` blocks by selector. - -Patch-enabled generation moved to `verity-compiler-patched`: +Patch-enabled generation lives in `verity-compiler-patched`: ```bash lake exe verity-compiler-patched --backend-profile solidity-parity lake exe verity-compiler-patched --enable-patches --patch-report artifacts/patch-report.tsv ``` -**Examples**: -```bash -# Compile without libraries -lake exe verity-compiler - -# Compile with one library -lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul +## Common errors -# Compile with multiple libraries, verbose output -lake exe verity-compiler \ - --link examples/external-libs/PoseidonT3.yul \ - --link examples/external-libs/PoseidonT4.yul \ - --link examples/external-libs/Groth16.yul \ - -v -o output/ -``` +- `Unresolved external references: ` — missing `--link`, or the name doesn't match between `CompilationModel` and the `.yul` file (case-sensitive). +- `Arity mismatch: : called with N args but library defines M params` — return values don't count as parameters. +- Contract works with the placeholder but reverts at runtime — usually gas, or the library returns an unexpected shape. Run Foundry tests against the linked Yul. diff --git a/docs-site/content/guides/production-solidity-patterns.mdx b/docs-site/content/guides/production-solidity-patterns.mdx index b8fdee9fe..d133ecdc7 100644 --- a/docs-site/content/guides/production-solidity-patterns.mdx +++ b/docs-site/content/guides/production-solidity-patterns.mdx @@ -1,3 +1,8 @@ +--- +title: Production Solidity Patterns +description: Agent-facing checklist for porting non-trivial Solidity contracts — reusable surfaces, oracle/spec boundaries, and ECM usage. +--- + # Production Solidity Translation Patterns This guide is for agents porting non-trivial Solidity contracts into Verity. Use diff --git a/docs-site/content/guides/solidity-to-verity.mdx b/docs-site/content/guides/solidity-to-verity.mdx index 8fb368d4a..b25800189 100644 --- a/docs-site/content/guides/solidity-to-verity.mdx +++ b/docs-site/content/guides/solidity-to-verity.mdx @@ -1,3 +1,8 @@ +--- +title: Solidity to Verity +description: Practical mappings for porting a Solidity contract into the verity_contract surface — first-pass syntax, restructuring patterns, and a worked walkthrough. +--- + # Solidity-to-Verity Translation Guide This guide is the practical path for converting a Solidity contract into the @@ -37,10 +42,12 @@ Use this table as your first-pass conversion checklist. | `x = y - z` (checked) | `let d <- requireSomeUint (safeSub y z) "underflow"` then `setStorage xSlot d` | | `x = y * z` (checked) | `let p <- requireSomeUint (safeMul y z) "overflow"` then `setStorage xSlot p` | | `x = y / z` (checked) | `let q <- requireSomeUint (safeDiv y z) "division by zero"` then `setStorage xSlot q` | -| `balances[a]` | `let m <- getStorage balances; pure (m a)` | -| `balances[a] = v` | `let m <- getStorage balances; setStorage balances (fun k => if k == a then v else m k)` | -| `emit Transfer(from, to, amount)` | `emit "Transfer" [from, to, amount]` | -| `return v;` | `pure v` | +| `balances[a]` | `let v ← getMapping balances a` | +| `balances[a] = v` | `setMapping balances a v` | +| `allowances[a][b]` | `let v ← getMapping2 allowances a b` | +| `tokenOwners[id]` (address-valued uint-keyed) | `let owner ← getMappingUintAddr tokenOwners id` | +| `emit Transfer(from, to, amount)` | `emitEvent "Transfer" [amount] [addressToWord from, addressToWord to]` | +| `return v;` | `pure v` (or `return v` inside `verity_contract`) | ## 2. Patterns That Need Restructuring @@ -206,26 +213,20 @@ def totalSupply : StorageSlot Uint256 := ⟨1⟩ ### Step B: Translate the function body ```verity -def transfer (to : Address) (amount : Uint256) : Contract Bool := do - let sender <- msgSender - let current <- getStorage balances - - let senderBal := current sender +def transfer (to : Address) (amount : Uint256) : Contract Unit := do + let sender ← msgSender + let senderBal ← getMapping balances sender require (senderBal >= amount) "insufficient" - - let newSender <- requireSomeUint (safeSub senderBal amount) "underflow" - let toBal := current to - let newTo <- requireSomeUint (safeAdd toBal amount) "overflow" - - setStorage balances (fun a => - if a == sender then newSender - else if a == to then newTo - else current a) - - emit [sender.toNat, to.toNat, amount.toNat] - pure true + let newSender ← requireSomeUint (safeSub senderBal amount) "underflow" + let toBal ← getMapping balances to + let newTo ← requireSomeUint (safeAdd toBal amount) "overflow" + setMapping balances sender newSender + setMapping balances to newTo + emitEvent "Transfer" [amount] [addressToWord sender, addressToWord to] ``` +Use `getMapping` / `setMapping` for individual entries — there is no whole-mapping read or function-shaped write in the EDSL. Keep `require` guards before any `setMapping` mutation so the revert state equals the input state. + ### Step C: Write the spec shape For this transfer path, typical specs include: @@ -235,30 +236,36 @@ For this transfer path, typical specs include: 3. Total supply is unchanged. 4. If guard fails, result is `revert` and state is preserved. -Example spec skeleton: +Specs are `Prop`-valued predicates over the pre/post `ContractState`, not records. The canonical shape (used across `Contracts//Spec.lean`) is `_spec args s s' : Prop`: ```lean -def transferSpec (to : Address) (amount : Uint256) : ContractSpec := - { pre := fun s => (s.storageMap balances s.sender) >= amount - post := fun s r s' => - r = true /\ - s'.storageMap balances s.sender = (s.storageMap balances s.sender) - amount /\ - s'.storageMap balances to = (s.storageMap balances to) + amount } +def transfer_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop := + s'.storageMap balances.slot s.sender = + sub (s.storageMap balances.slot s.sender) amount ∧ + s'.storageMap balances.slot to = + add (s.storageMap balances.slot to) amount ∧ + storageMapUnchangedExceptKeysAtSlot balances.slot s.sender to s s' ∧ + sameStorageAddrContext s s' ``` -### Step D: Prove with existing automation +Pick the right "unchanged" helper from [`Verity.Specs.Common`](/core#spec-helpers) for the actual write set. Conservation specs (`balanceSum` equations) go here too when the contract needs them. -Typical proof shape: +### Step D: Prove with existing automation -1. `unfold transfer` -2. `simp` through `require`, `bind`, `getStorage`, `setStorage` -3. discharge arithmetic/branch conditions -4. finish with storage equality goals +Use the `_meets_spec` convention — single `simp` with the operation, slot names, spec definition, and any guard hypothesis: -Use examples in: +```lean +theorem transfer_meets_spec (s : ContractState) (to : Address) (amount : Uint256) + (h_funds : s.storageMap balances.slot s.sender >= amount) : + let s' := ((transfer to amount).run s).snd + transfer_spec to amount s s' := by + simp [transfer, transfer_spec, balances, msgSender, getMapping, setMapping, + bind, h_funds, + Specs.storageMapUnchangedExceptKeysAtSlot, + Specs.sameStorageAddrContext] +``` -- `Verity/Proofs/SimpleToken/Basic.lean` -- `Verity/Proofs/ERC20/Basic.lean` +Real-world references: [`Contracts/SimpleToken/Proofs/Basic.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/SimpleToken/Proofs/Basic.lean) and [`Contracts/ERC20/Proofs/Basic.lean`](https://github.com/lfglabs-dev/verity/blob/main/Contracts/ERC20/Proofs/Basic.lean). ## 4. Common Pitfalls @@ -302,7 +309,7 @@ A selector mismatch can make proofs pass while runtime dispatch is wrong. If you are starting from zero, pair this with: -- [Adding Your First Contract](/guides/first-contract) +- [Adding Your First Contract](/first-contract) - [Production Solidity Patterns](/guides/production-solidity-patterns) -- [Compiler](/compiler) -- [Formal Verification](/verification) +- [Compiler & CLI](/compiler) +- [Verification Status](/verification) diff --git a/docs-site/content/guides/verity-syntax-highlighting.mdx b/docs-site/content/guides/verity-syntax-highlighting.mdx deleted file mode 100644 index e0de5f546..000000000 --- a/docs-site/content/guides/verity-syntax-highlighting.mdx +++ /dev/null @@ -1,48 +0,0 @@ -# Verity Syntax Highlighting - -The docs site uses a Verity-specific TextMate grammar and the LFGLabs Cream theme for `verity` code fences. - -## Definition of Done - -- Verity snippets are rendered with `verity`, not generic `lean`, when they show contract DSL code. -- Contract structure is visually explicit: `verity_contract`, section headers, `linked_externals`, typed `external` declarations, `modifier`, and `function` headers each receive distinct scopes. -- Solidity-like control surfaces are easy to scan: `with onlyRelayer`, `nonreentrant(...)`, `forEach`, `requireError`, `tryExternalCall`, `abiEncode`, and `emit` are all highlighted by semantic role. -- Domain-level signals stand out without changing source text: field access such as `txn.proof`, typed external returns such as `Circuit`, event names, and custom errors such as `PoolCircuitNotRegistered()` receive dedicated scopes. -- Code blocks use a warm light theme with subtle scope bands for guards, external calls, events, and declaration lines. -- The scope contract is checked by `npm run check:highlighting`. - -## Unlink-Style Example - -```verity -linked_externals - external getCircuit(Address, Uint256) -> (Circuit) - external getCircuit_try(Address, Uint256) -> (Bool, Circuit) - -modifier onlyRelayer := do - let sender ← msgSender - let isR ← getMapping relayersSlot sender - requireError (isR != 0) PoolUnauthorizedRelayer() - -function nonreentrant(reentrancyLockSlot) transfer - (transactions : Array Transaction) with onlyRelayer : Unit := do - let txLen := arrayLength transactions - requireError (txLen != 0) PoolEmptyTransactions() - forEach "i" txLen (do - let txn := arrayElement transactions i - let verifierRouter ← getStorageAddr stateVerifierRouter - let (success, circuit) ← tryExternalCall "getCircuit" - [verifierRouter, txn.circuitId] - requireError success PoolCircuitNotRegistered() - requireError (circuit.verifier != 0) PoolCircuitNotRegistered() - let (proofOk, ok) ← tryExternalCall "verifySpend" - [circuit.verifier, abiEncode txn.proof, txn.merkleRoot, - txn.contextHash, txn.nullifierHashes, txn.newCommitments] - requireError proofOk PoolProofVerificationFailed() - requireError ok PoolProofVerificationFailed() - let leaves ← realCommitments txn.newCommitments maxUint - let startIndex ← nextLeafIndex - let newRoot ← insertLeaves leaves - emit "Transferred" - [newRoot, startIndex, leaves, - realNullifiers txn.nullifierHashes, txn.ciphertexts]) -``` diff --git a/docs-site/content/index.mdx b/docs-site/content/index.mdx index 292a2195d..30b0dfbda 100644 --- a/docs-site/content/index.mdx +++ b/docs-site/content/index.mdx @@ -14,11 +14,12 @@ import { ReportCallout } from '../components/ReportCallout' A small, audited Lean EDSL with example contracts that compile to EVM artifacts. -Every claim is machine-checked and every assumption is documented. Read the docs -as a short manual: start with a contract, inspect the compiler, then check the -theorem and assumption inventory. Layer 2 proof status is tracked in -`Compiler/Proofs/IRGeneration/Contract.lean` (generic whole-contract -`CompilationModel -> IR` theorem for the current supported fragment). +Every claim is machine-checked and every assumption is documented. Compilation +correctness rides on `Compiler/Proofs/IRGeneration/Contract.lean` (generic +whole-contract `CompilationModel -> IR` theorem for the current supported +fragment) — no per-contract bridge axioms. The full three-layer breakdown lives +on the [Trust Model](/trust-model) page; the live theorem inventory is on +[Verification Status](/verification). ## The Three-Layer Structure @@ -67,12 +68,12 @@ Lean checks every proof at compile time. A broken proof is a broken build. import { ReadingList } from '../components/ReadingList' diff --git a/docs-site/content/proof-techniques.mdx b/docs-site/content/proof-techniques.mdx new file mode 100644 index 000000000..e0614a025 --- /dev/null +++ b/docs-site/content/proof-techniques.mdx @@ -0,0 +1,101 @@ +--- +title: Proof Techniques +description: How Verity contracts are proved correct, and what's currently out of scope. +--- + +# Proof Techniques + +This page collects the proof patterns used throughout `Contracts//Proofs/` +and the `Verity/Proofs/Stdlib/` automation modules, plus the current set of +known limitations. The companion live status page is [`/verification`](/verification). + +## Guard modeling + +The `ContractResult` type models Solidity's `require` explicitly: + +```verity +inductive ContractResult (α : Type) where + | success : α → ContractState → ContractResult α + | revert : String → ContractState → ContractResult α + +def require (condition : Bool) (message : String) : Contract Unit := + fun s => if condition + then ContractResult.success () s + else ContractResult.revert message s +``` + +This lets proofs reason about both the success path and the revert path of +guard-protected operations. + +## Proof techniques + +**Full unfolding** is the main approach. For guarded operations, unfold the +entire do-notation chain through `bind`/`pure`/`Contract.run`/`ContractResult.snd`, +then `simp [h_guard]` to resolve the guard condition. + +```verity +simp only [operation, onlyOwner, isOwner, owner, + msgSender, getStorageAddr, setStorage, + Verity.bind, Bind.bind, Pure.pure, + Contract.run, ContractResult.snd] +simp [h_owner] +``` + +It works because the EDSL is shallow: every contract function is a composition +of core primitives. + +**Private unfold helpers**: for complex operations, a private theorem +pre-computes the exact result state when guards pass. Main proofs then +`rw [op_unfold]` to get the concrete state. + +```lean +private theorem increment_unfold (s : ContractState) + (h_owner : s.sender = s.storageAddr 0) : + (increment.run s) = ContractResult.success () { ... } := by + simp only [increment, ...]; simp [h_owner] +``` + +`private theorem` isn't accessible from other files, so isolation proofs in +separate files must repeat the full unfolding. + +**Boolean equality conversion**: `beq_iff_eq` converts between `(x == y) = true` +and `x = y`. + +**Slot preservation**: `intro slot h_neq h_eq; exact absurd h_eq h_neq` is the +standard pattern for "this operation doesn't touch slot `n`" lemmas. + +**List sum reasoning**: `omega` cannot handle `List.sum` or nonlinear +multiplication, so conservation proofs use explicit +`Nat.add_assoc`/`Nat.add_comm`/`Nat.add_left_comm` rewrite chains. + +**countOcc helpers**: `simp [countOcc, if_pos rfl]` produces `if True then 1 else 0` +which doesn't reduce. Pre-proven `countOcc_cons_eq` / `countOcc_cons_ne` helpers +avoid this. + +**No Mathlib**: tactics such as `push_neg`, `set`, `ring`, and `linarith` are +unavailable. Use `by_cases`, explicit witnesses, and manual `Nat.*` lemma +chains. + +## Arithmetic semantics + +All core arithmetic is EVM-compatible. `Uint256` wraps at `2^256`, so `+`, +`-`, `*`, `/`, and `%` match EVM behavior by default. + +Two approaches coexist for overflow safety: + +- **Counter**: bare `add`/`sub` (modular arithmetic, EVM-accurate). +- **SafeCounter / Ledger / SimpleToken**: `safeAdd` / `safeSub` from + `Stdlib/Math.lean` return `Option`, reverting on overflow/underflow. + +`MAX_UINT256 := 2^256 - 1`. Safe arithmetic checks this bound before returning +`some`. + +## Known limitations + +No multi-contract interaction, no reentrancy modeling, no gas modeling. The CompilationModel supports events and double mappings, but EDSL-level proofs for those are still limited. Conservation is proven as exact `countOcc`-based sum equations, not as a global invariant over all addresses; transfer theorems treat self-transfer as a no-op. `ContractResult.fst` returns `default` on revert (requires `[Inhabited α]`), so proofs using `.fst` show `success` first. Mathlib tactics (`set`, `ring`, `linarith`) are unavailable. + +## See also + +- [Verification](/verification) — live theorem inventory and proof-status snapshot. +- [Glossary](/glossary) — definitions of `ContractResult`, `local_obligations`, and other load-bearing terms. +- [Trust Model](/trust-model) — what the proof techniques here actually buy you. diff --git a/docs-site/content/research.mdx b/docs-site/content/research.mdx deleted file mode 100644 index 1c30bd8c3..000000000 --- a/docs-site/content/research.mdx +++ /dev/null @@ -1,108 +0,0 @@ ---- -title: Research & Development -description: Design decisions, iterations, and proof techniques ---- - -# Research & Development - -**Compact core, built across 7 iterations.** See [/verification](/verification) for current theorem totals and proof status. [AXIOMS.md](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md) remains the source of truth for documented axioms. - -## Evolution - -The project evolved in two phases: - -**Phase 1 (Iterations 1-7)**: Built 7 contracts on `StateM ContractState`. The core stayed intentionally small while storage types were added incrementally: `Nat -> Uint256` (iteration 1), `Nat -> Address` (iteration 3), `Nat -> Address -> Uint256` for mappings (iteration 6). Each addition was driven by a concrete example that needed it. - -**Phase 2 (Verification)**: Replaced `StateM` with custom `ContractResult` type (`success | revert`) to model `require` guards explicitly. This enabled proving properties like "mint reverts when caller is not owner." The core expanded to include proof automation lemmas and EVM context fields. - -## Iterations - -| Iteration | Contract | Core Change | Key Feature | -|-----------|----------|-------------|-------------| -| 1 | SimpleStorage | Bootstrap | `ContractState`, storage ops, `require` | -| 2 | Counter | Reuse | Read-modify-write pattern | -| 3 | Owned | Extend | Address storage, access control | -| 4 | OwnedCounter | Compose | Pattern composition | -| 5 | SafeCounter | Extend | Math stdlib with checked arithmetic | -| 6 | Ledger | Extend | Mapping support (`Address -> Uint256`) | -| 7 | SimpleToken | Compose | Combined patterns: owned + ledger + supply | - -## Design Decisions - -**What worked:** -- `Address := String`, `Uint256` is a dedicated 256-bit modular type. -- Storage as functions (`Nat -> Uint256`), not finite maps. Uninitialized slots return 0. -- `require` returns `ContractResult.revert msg s`, preserving original state. -- Manual storage slot allocation (slot 0, 1, 2...). No automatic allocation needed. -- Selectors are auto-computed from function signatures via `computeSelectors`; no manual selector maps needed. -- `onlyOwner` is a regular function, not special syntax. - -**What didn't work:** -- `StateM.get` doesn't exist in Lean 4. Use plain `get` in do-notation. -- `Repr` can't derive for function types. Added manual instance. -- Generic `requireSome` needs `[Inhabited a]`. Made Uint256-specific version instead. -- Marking `.fst`/`.snd` as `@[simp]` caused over-simplification. Added operation-specific simp lemmas. - -## Arithmetic Semantics - -All core arithmetic is EVM-compatible. `Uint256` wraps at `2^256`, so `+`, `-`, `*`, `/`, and `%` match EVM behavior by default. - -Two approaches coexist for overflow safety: -- **Counter**: Bare `add`/`sub` (modular arithmetic, EVM-accurate) -- **SafeCounter / Ledger / SimpleToken**: `safeAdd`/`safeSub` from `Stdlib/Math.lean` return `Option`, reverting on overflow/underflow - -`MAX_UINT256 := 2^256 - 1`. Safe arithmetic checks this bound before returning `some`. - -## Proof Techniques - -**Full unfolding** is the main approach: -```verity -simp only [operation, onlyOwner, isOwner, owner, - msgSender, getStorageAddr, setStorage, - Verity.bind, Bind.bind, Pure.pure, - Contract.run, ContractResult.snd] -simp [h_owner] -``` - -Works because the EDSL is shallow: every contract function is a composition of core primitives. - -**Private unfold helpers** pre-compute exact result states when guards pass: -```lean -private theorem increment_unfold (s : ContractState) - (h_owner : s.sender = s.storageAddr 0) : - (increment.run s) = ContractResult.success () { ... } := by - simp only [increment, ...]; simp [h_owner] -``` - -But `private theorem` isn't accessible from other files. Isolation proofs in separate files must repeat the full unfolding. - -**Other techniques:** -- **Boolean equality**: Use `beq_iff_eq` to convert `(x == y) = true` to `x = y` -- **Slot preservation**: `intro slot h_neq h_eq; exact absurd h_eq h_neq` -- **List sum reasoning**: `omega` can't handle `List.sum` or `var * var`. Use explicit `Nat.add_assoc`/`add_comm`/`add_left_comm` chains -- **No Mathlib**: `push_neg`, `set`, `ring`, `linarith` unavailable. Use `by_cases`, explicit witnesses, manual `Nat.*` lemma chains - -## Known Limitations - -- **Self-transfer**: Modeled as a no-op; transfer theorems no longer require `sender != to`. -- **Supply = sum of balances**: Requires finite address model. Proven as exact sum equations with `countOcc`, not as global invariant over all addresses. -- **`ContractResult.fst`**: Returns `default` on revert, requiring `[Inhabited a]`. Proofs using `.fst` always show result is `success` first. -- **No gas modeling**: EDSL models storage and control flow only; verification assumes infinite gas. -- **Events**: The CompilationModel DSL supports event emission (`Stmt.emit`), but the EDSL core does not yet model events in proofs. -- **Nested mappings**: The CompilationModel DSL supports double mappings (`mapping2`/`setMapping2`), but EDSL-level proofs for nested mapping semantics are still limited. - -## Compiler Development - -The compiler pipeline compiles declarative `CompilationModel` specs to Yul/EVM bytecode automatically, replacing the earlier manual IR approach. - -Key milestones: -- **Generic compilation** (2026-02-10): All contracts compile from declarative specs. Zero manual IR. -- **Differential testing** (2026-02-10): Random transaction generation + parallel execution on EDSL interpreter vs compiled EVM. Zero mismatches. -- **CompilationModel expansion**: Loops, branching, arrays, events, multi-mappings, internal calls, verified extern linking. -- **Layer 2**: Supported-fragment generic theorem in place. The compiler-level theorem lives in `Compiler/Proofs/IRGeneration/Contract.lean`. The compiler proves Layer 2 preservation automatically for supported contracts. - -See [`docs/ROADMAP.md`](https://github.com/lfglabs-dev/verity/blob/main/docs/ROADMAP.md) for active workstreams and the full roadmap. - -## Detailed Logs - -For iteration-by-iteration development notes, see [/research/iterations](/research/iterations). diff --git a/docs-site/content/research/_meta.js b/docs-site/content/research/_meta.js deleted file mode 100644 index ae4d09d62..000000000 --- a/docs-site/content/research/_meta.js +++ /dev/null @@ -1,3 +0,0 @@ -export default { - iterations: 'Detailed Iterations', -}; diff --git a/docs-site/content/research/iterations.mdx b/docs-site/content/research/iterations.mdx deleted file mode 100644 index 2fafeeb8f..000000000 --- a/docs-site/content/research/iterations.mdx +++ /dev/null @@ -1,72 +0,0 @@ ---- -title: Iteration Summaries -description: Development history across 8 iterations ---- - -# Iteration Summaries - -The project was built in 8 iterations. The first 7 added contracts and, when needed, extended the core. The 8th focused on verification infrastructure. - -This page is the detailed iteration log and the only place for milestone-style progress notes. - -## Iteration 7: SimpleToken - -Combined Owned and Ledger patterns into a token contract with owner-controlled minting, public transfers, and supply tracking. No core changes needed. - -- Core: unchanged - -## Iteration 6: Mapping Support - -Added `storageMap` field to `ContractState` for key-value storage (`Address -> Uint256`). Ledger example demonstrates deposit, withdraw, and transfer with balance guards. - -- Core: mapping support added - -## Iteration 5: Math Safety Stdlib - -Added `Stdlib/Math.lean` with `safeAdd`, `safeSub`, `safeMul`, `safeDiv`. SafeCounter example uses checked arithmetic instead of bare `+`/`-`. Core unchanged. - -- Core: unchanged -- Stdlib/Math: added safe arithmetic helpers - -## Iteration 4: OwnedCounter - -Combined Owned and Counter patterns. Increment/decrement require ownership. No core changes needed. - -- Core: unchanged - -## Iteration 3: Owned - -Added `storageAddr` field to `ContractState` for Address storage. Owned example implements `onlyOwner` guard and `transferOwnership`. - -- Core: address storage added - -## Iteration 2: Counter - -Increment/decrement with read-modify-write pattern. No core changes needed. Raised the question of arithmetic safety (Lean `Nat` subtraction saturates at 0, Solidity 0.8+ reverts). - -- Core: unchanged - -## Iteration 1: Bootstrap - -Initial core with `ContractState`, `StorageSlot`, `getStorage`/`setStorage`, `msgSender`, `require`. SimpleStorage example. - -- Core: initial core - -## Core growth - -| Iteration | Change summary | What was added | -|-----------|----------------|----------------| -| 1 (Bootstrap) | New core | ContractState, storage access, msgSender, require | -| 2 (Counter) | No change | Nothing needed | -| 3 (Owned) | Extended core | Address storage | -| 4 (OwnedCounter) | No change | Nothing needed | -| 5 (SafeCounter) | Cleanup | Safer arithmetic helpers in stdlib | -| 6 (Ledger) | Extended core | Mapping storage | -| 7 (SimpleToken) | No change | Nothing needed | -| 8 (Verification) | Extended core | ContractResult, bind, simp lemmas, EVM context | - -4 out of the 7 implementation iterations needed no core changes. The verification iteration added infrastructure for proofs, not new contract primitives. - -## Source - -See the [Research Log](/research) for detailed notes on each iteration, including failed approaches and design decisions. diff --git a/docs-site/content/trust-model.mdx b/docs-site/content/trust-model.mdx new file mode 100644 index 000000000..12284e3a7 --- /dev/null +++ b/docs-site/content/trust-model.mdx @@ -0,0 +1,102 @@ +--- +title: Trust Model +description: The canonical home for the Layer 1/2/3 framing, the trust boundary, and the assumption model. +--- + +# 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. diff --git a/docs-site/content/verification.mdx b/docs-site/content/verification.mdx index f41753eef..5773f996d 100644 --- a/docs-site/content/verification.mdx +++ b/docs-site/content/verification.mdx @@ -1,456 +1,54 @@ --- -title: Formal Verification -description: EDSL proofs plus compiler correctness proofs (IR + Yul) +title: Verification Status +description: Theorem inventory by contract, plus the compiler-proof structure. --- -# Formal Verification +# Verification Status -The compiler is verified with IR preservation proofs and Yul equivalence proofs in `Compiler/Proofs/`. All three layers are complete and checked by `lake build`. +All three pipeline layers (EDSL → CompilationModel → IR → Yul) are complete and machine-checked by `lake build`. Zero `sorry`. For *how* these proofs are built, see [Proof Techniques](/proof-techniques); for *what is trusted vs verified*, see [Trust Model](/trust-model). The authoritative axiom list lives in [AXIOMS.md](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md). -**Status**: See [docs/VERIFICATION_STATUS.md](https://github.com/Th0rgal/verity/blob/main/docs/VERIFICATION_STATUS.md) for the current theorem totals, test counts, exclusions, and proof-status snapshot. [AXIOMS.md](https://github.com/Th0rgal/verity/blob/main/AXIOMS.md) remains the source of truth for documented axioms. +## Per-contract proof coverage -- ERC721: 11 total (Basic 6, Correctness 5). -- ReentrancyExample: 5 total (inline proofs: vulnerability existence, supply invariant). -- Stdlib: 0 theorems (Math 25, Automation 56, MappingAutomation 37, ListSum 7, AddressAutomation 24; 2 shared between Automation and MappingAutomation). +Counts are theorems in each module. Read the actual statements in [`Contracts//Proofs/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts) — Lean is the source of truth. -## Compiler Proofs (IR + Yul) +| Contract | Basic | Correctness | Conservation / Supply | Isolation | Native | Total | +|----------|-------|-------------|----------------------|-----------|--------|-------| +| SimpleStorage | 13 | 7 | — | — | — | 20 | +| Counter | 19 | 9 | — | — | — | 28 | +| SafeCounter | 20 | 8 | — | — | — | 28 | +| Owned | 19 | 4 | — | — | — | 23 | +| OwnedCounter | 33 | 6 | — | 14 | — | 53 | +| Ledger | 24 | 6 | 7 (conservation) | — | — | 37 | +| SimpleToken | 40 | 10 | 6 (supply) | 12 | — | 68 | +| ERC20 | 15 | 7 | — | — | 3 | 25 | +| ERC721 | 6 | 5 | — | — | — | 11 | +| Vault (ERC-4626) | scaffold | scaffold | scaffold | — | 3 | 3 | +| ReentrancyExample | 5 inline (vulnerability witness + safety proofs) | | | | | 5 | -- **Generic whole-contract Layer 2 theorem**: `Compiler/Proofs/IRGeneration/Contract.lean` (`CompilationModel.compile` correctness for the current supported fragment) -- **End-to-end proofs**: `Compiler/Proofs/EndToEnd.lean` (full pipeline correctness) -- **Typed IR correctness**: `Compiler/TypedIRCompilerCorrectness.lean` (generic compilation-correctness theorem with 36 supported statement fragments, including ABI-head tuple/bytes/fixed-array/dynamic-array/string params as word-typed inputs) -- **IR generation**: `Compiler/Proofs/IRGeneration/` (infrastructure + concrete IR proofs in `Expr.lean`) -- **Yul semantics + preservation**: `Compiler/Proofs/YulGeneration/` (complete, PR #42) +The **Native** column counts theorems that pin the IR / Yul lowering to the EVMYulLean-bridged backend (`Contracts//Proofs/Native.lean`). -## Structure +Vault carries a verified surface spec and full IR-lowering coverage; the spec-level Basic/Correctness/Conservation proofs are intentionally scaffold (issue [#1163](https://github.com/lfglabs-dev/verity/issues/1163)). -Each contract lives under `Contracts/{Name}/`: +## Stdlib -``` -Contracts/{Name}/ -├── {Name}.lean # Implementation (EDSL via verity_contract) -├── Spec.lean # What each operation should do -├── Invariants.lean # Properties that should always hold -├── SpecProofs.lean # User-facing spec statements and re-exports -└── Proofs/ - ├── Basic.lean # Spec conformance and lemmas - ├── Correctness.lean # Composition and revert behavior - ├── Conservation.lean # Sum conservation (Ledger) - ├── Supply.lean # Supply conservation (SimpleToken) - └── Isolation.lean # Storage isolation (SimpleToken) +Reusable proof infrastructure in `Verity/Proofs/Stdlib/`: -Verity/Proofs/Stdlib/ # Reusable proof infrastructure (Math, Automation, etc.) -``` +| Module | Theorems | What it covers | +|--------|----------|----------------| +| `Math` | ~148 | `safeAdd/Sub/Mul/Div`, `mulDivDown/Up`, `wMulDown/wDivUp`, full-precision `mulDiv512Down?/Up?`, `SNARK_SCALAR_FIELD` / `modField` | +| `Automation` | ~108 | Full-result and `runState`/`runValue` lemmas for storage, address storage, context, events, require | +| `MappingAutomation` | ~48 | Mapping, uint-keyed mapping, double-mapping automation | +| `ListSum` | ~8 | Sum reasoning for conservation proofs (`countOcc`, `balanceSum`) | -## Guard modeling +## Compiler proofs -The `ContractResult` type models Solidity's `require` explicitly: +- **Generic whole-contract Layer 2 theorem**: `Compiler/Proofs/IRGeneration/Contract.lean` — `CompilationModel.compile` correctness for the supported fragment. +- **End-to-end**: `Compiler/Proofs/EndToEnd.lean`. +- **Typed IR**: `Compiler/TypedIRCompilerCorrectness.lean` — 36 supported statement fragments including ABI-head tuples, bytes, fixed/dynamic arrays, and strings as word-typed inputs. +- **Yul semantics + preservation**: `Compiler/Proofs/YulGeneration/`, with an EVMYulLean-bridged native backend in `Compiler/Proofs/YulGeneration/Backends/`. -```verity -inductive ContractResult (α : Type) where - | success : α → ContractState → ContractResult α - | revert : String → ContractState → ContractResult α +## See also -def require (condition : Bool) (message : String) : Contract Unit := - fun s => if condition - then ContractResult.success () s - else ContractResult.revert message s -``` - -This lets proofs reason about both the success path and the revert path of guard-protected operations. - -## Theorems by contract - -### SimpleStorage - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `setStorage_updates_slot` | Updates the correct storage slot | -| 2 | `getStorage_reads_slot` | Reads the correct storage slot | -| 3 | `setStorage_preserves_other_slots` | Other slots unchanged | -| 4 | `setStorage_preserves_sender` | msg.sender preserved | -| 5 | `setStorage_preserves_address` | Contract address preserved | -| 6 | `setStorage_preserves_addr_storage` | Address storage unaffected | -| 7 | `setStorage_preserves_map_storage` | Mapping storage unaffected | -| 8 | `store_meets_spec` | Store satisfies formal specification | -| 9 | `retrieve_meets_spec` | Retrieve satisfies formal specification | -| 10 | `store_retrieve_correct` | After storing v, retrieve returns v | -| 11 | `store_preserves_wellformedness` | Well-formed state maintained | -| 12 | `retrieve_preserves_state` | Read doesn't modify state | -| 13 | `retrieve_twice_idempotent` | Two consecutive retrieves are idempotent | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `store_retrieve_roundtrip_holds` | Roundtrip specification | -| 2 | `store_preserves_storage_isolated` | Storage isolation | -| 3 | `store_preserves_addr_storage` | Address storage preservation | -| 4 | `store_preserves_map_storage` | Mapping storage preservation | -| 5 | `store_preserves_context` | Context (sender, thisAddress) preservation | -| 6 | `retrieve_preserves_context` | Read-only preserves context | -| 7 | `retrieve_preserves_wellformedness` | Well-formedness preservation | - -### Counter - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `setStorage_updates_count` | Updates the count storage slot | -| 2 | `getStorage_reads_count` | Reads the count storage slot | -| 3 | `setStorage_preserves_other_slots` | Other slots unchanged | -| 4 | `setStorage_preserves_context` | Sender and contract address preserved | -| 5 | `setStorage_preserves_addr_storage` | Address storage unaffected | -| 6 | `setStorage_preserves_map_storage` | Mapping storage unaffected | -| 7 | `increment_meets_spec` | Increment satisfies formal specification | -| 8 | `increment_adds_one` | Count increases by exactly 1 | -| 9 | `decrement_meets_spec` | Decrement satisfies formal specification | -| 10 | `decrement_subtracts_one` | Count decreases by exactly 1 | -| 11 | `getCount_meets_spec` | getCount satisfies formal specification | -| 12 | `getCount_reads_count_value` | Returns stored count value | -| 13 | `increment_getCount_correct` | Increment then getCount returns count + 1 | -| 14 | `decrement_getCount_correct` | Decrement then getCount returns count - 1 | -| 15 | `increment_twice_adds_two` | Two increments add 2 | -| 16 | `increment_decrement_cancel` | Increment then decrement equals identity | -| 17 | `increment_preserves_wellformedness` | Well-formedness maintained | -| 18 | `decrement_preserves_wellformedness` | Well-formedness maintained | -| 19 | `getCount_preserves_state` | Read doesn't modify state | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `increment_state_preserved_except_count` | Only count slot changes | -| 2 | `decrement_state_preserved_except_count` | Only count slot changes | -| 3 | `getCount_state_preserved` | Read-only preserves state | -| 4 | `increment_getCount_meets_spec` | Increment then getCount | -| 5 | `decrement_getCount_meets_spec` | Decrement then getCount | -| 6 | `two_increments_meets_spec` | Two increments composition | -| 7 | `increment_decrement_meets_cancel` | Cancellation property | -| 8 | `getCount_preserves_wellformedness` | Read-only well-formedness | -| 9 | `decrement_getCount_correct` | Decrement then getCount equals count - 1 | -| 10 | `decrement_at_zero_wraps_max` | Decrementing at zero wraps to MAX_UINT256 | - -### Owned - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `setStorageAddr_updates_owner` | setStorageAddr writes owner slot | -| 2 | `getStorageAddr_reads_owner` | getStorageAddr reads owner slot | -| 3 | `setStorageAddr_preserves_other_slots` | Other address slots unchanged | -| 4 | `setStorageAddr_preserves_uint_storage` | Uint256 storage unchanged | -| 5 | `setStorageAddr_preserves_map_storage` | Mapping storage unchanged | -| 6 | `setStorageAddr_preserves_context` | Context unchanged | -| 7 | `constructor_meets_spec` | Constructor sets owner to sender | -| 8 | `constructor_sets_owner` | Owner equals deployer | -| 9 | `getOwner_meets_spec` | getOwner reads correct slot | -| 10 | `getOwner_returns_owner` | Returns stored owner | -| 11 | `getOwner_preserves_state` | getOwner is read-only | -| 12 | `isOwner_meets_spec` | isOwner meets specification | -| 13 | `isOwner_returns_correct_value` | isOwner returns correct boolean | -| 14 | `transferOwnership_meets_spec_when_owner` | Owner transfer satisfies spec | -| 15 | `transferOwnership_changes_owner_when_allowed` | Owner successfully changed | -| 16 | `transferOwnership_unfold` | Unfold lemma for transferOwnership when owner | -| 17 | `constructor_getOwner_correct` | Constructor then getOwner equals sender | -| 18 | `constructor_preserves_wellformedness` | Well-formedness maintained | -| 19 | `getOwner_preserves_wellformedness` | getOwner preserves well-formedness | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `transferOwnership_reverts_when_not_owner` | Access control enforced | -| 2 | `transferOwnership_preserves_wellformedness` | Well-formedness with non-empty owner | -| 3 | `constructor_transferOwnership_getOwner` | Full lifecycle: create, transfer, read | -| 4 | `transferred_owner_cannot_act` | Old owner is actually locked out | - -### SimpleToken - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `setStorageAddr_updates_owner` | setStorageAddr writes owner slot | -| 2 | `setStorage_updates_supply` | setStorage writes supply slot | -| 3 | `setMapping_updates_balance` | setMapping writes balance entry | -| 4 | `getMapping_reads_balance` | getMapping reads balance entry | -| 5 | `getStorage_reads_supply` | getStorage reads supply slot | -| 6 | `getStorageAddr_reads_owner` | getStorageAddr reads owner slot | -| 7 | `setMapping_preserves_other_addresses` | setMapping doesn't change other keys | -| 8 | `constructor_meets_spec` | Constructor meets full specification | -| 9 | `constructor_sets_owner` | Owner equals deployer | -| 10 | `constructor_sets_supply_zero` | Initial supply is zero | -| 11 | `isOwner_true_when_owner` | isOwner returns true for owner | -| 12 | `mint_meets_spec_when_owner` | Owner mint satisfies full spec | -| 13 | `mint_increases_balance` | Recipient balance increases by amount | -| 14 | `mint_increases_supply` | Total supply increases by amount | -| 15 | `mint_reverts_balance_overflow` | Mint reverts on balance overflow | -| 16 | `mint_reverts_supply_overflow` | Mint reverts on supply overflow | -| 17 | `transfer_meets_spec_when_sufficient` | Transfer satisfies spec | -| 18 | `transfer_preserves_supply_when_sufficient` | Transfer doesn't change supply | -| 19 | `transfer_decreases_sender_balance` | Sender balance decreases | -| 20 | `transfer_increases_recipient_balance` | Recipient balance increases | -| 21 | `transfer_self_preserves_balance` | Self-transfer is a no-op | -| 22 | `transfer_reverts_recipient_overflow` | Transfer reverts on recipient overflow | -| 23 | `balanceOf_meets_spec` | balanceOf meets specification | -| 24 | `balanceOf_returns_balance` | balanceOf returns stored value | -| 25 | `balanceOf_preserves_state` | balanceOf is read-only | -| 26 | `getTotalSupply_meets_spec` | getTotalSupply meets specification | -| 27 | `getTotalSupply_returns_supply` | getTotalSupply returns stored value | -| 28 | `getTotalSupply_preserves_state` | getTotalSupply is read-only | -| 29 | `getOwner_meets_spec` | getOwner meets specification | -| 30 | `getOwner_returns_owner` | getOwner returns stored value | -| 31 | `getOwner_preserves_state` | getOwner is read-only | -| 32 | `constructor_getTotalSupply_correct` | Constructor then getTotalSupply correct | -| 33 | `constructor_getOwner_correct` | Constructor then getOwner correct | -| 34 | `constructor_preserves_wellformedness` | Constructor preserves well-formedness | -| 35 | `balanceOf_preserves_wellformedness` | balanceOf preserves well-formedness | -| 36 | `getTotalSupply_preserves_wellformedness` | getTotalSupply preserves well-formedness | -| 37 | `getOwner_preserves_wellformedness` | getOwner preserves well-formedness | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `mint_reverts_when_not_owner` | Non-owners cannot mint | -| 2 | `transfer_reverts_insufficient_balance` | No overdrafts | -| 3 | `mint_preserves_wellformedness` | WellFormedState survives mint | -| 4 | `transfer_preserves_wellformedness` | WellFormedState survives transfer | -| 5 | `mint_preserves_owner` | Mint doesn't change owner | -| 6 | `transfer_preserves_owner` | Transfer doesn't change owner | -| 7 | `mint_then_balanceOf_correct` | After mint, balanceOf returns updated balance | -| 8 | `mint_then_getTotalSupply_correct` | After mint, getTotalSupply returns updated supply | -| 9 | `transfer_then_balanceOf_sender_correct` | After transfer, sender balance decreased | -| 10 | `transfer_then_balanceOf_recipient_correct` | After transfer, recipient balance increased | - -**Supply Conservation:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `constructor_establishes_supply_bounds` | Constructor establishes supply invariant | -| 2 | `mint_sum_equation` | `new_sum = old_sum + count(to) * amount` | -| 3 | `transfer_sum_equation` | `new_sum + count(sender)*amt = old_sum + count(to)*amt` | -| 4 | `mint_sum_singleton_to` | Mint sum equation for singleton recipient list | -| 5 | `transfer_sum_preserved_unique` | For unique sender & to: `new_sum = old_sum` | - -Transfer proofs handle self-transfer by modeling it as a no-op (preloading balances and applying a zero delta), so `sender != to` is not required. Supply conservation uses exact sum equations rather than the `supply_bounds_balances` invariant, which cannot be preserved for lists with duplicate addresses. - -**Isolation:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `constructor_supply_storage_isolated` | Constructor only writes Uint256 slot 2 | -| 2 | `constructor_balance_mapping_isolated` | Constructor doesn't write any mapping slot | -| 3 | `constructor_owner_addr_isolated` | Constructor only writes Address slot 0 | -| 4 | `mint_supply_storage_isolated` | Mint only writes Uint256 slot 2 | -| 5 | `mint_balance_mapping_isolated` | Mint only writes Mapping slot 1 | -| 6 | `mint_owner_addr_isolated` | Mint doesn't write any Address slot | -| 7 | `transfer_supply_storage_isolated` | Transfer doesn't write any Uint256 slot | -| 8 | `transfer_balance_mapping_isolated` | Transfer only writes Mapping slot 1 | -| 9 | `transfer_owner_addr_isolated` | Transfer doesn't write any Address slot | - -### OwnedCounter - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `constructor_meets_spec` | Constructor meets specification | -| 2 | `constructor_sets_owner` | Constructor sets owner correctly | -| 3 | `constructor_preserves_count` | Constructor preserves count slot | -| 4 | `getCount_meets_spec` | getCount meets specification | -| 5 | `getCount_returns_count` | getCount returns stored count | -| 6 | `getCount_preserves_state` | getCount is read-only | -| 7 | `getOwner_meets_spec` | getOwner meets specification | -| 8 | `getOwner_returns_owner` | getOwner returns stored owner | -| 9 | `getOwner_preserves_state` | getOwner is read-only | -| 10 | `isOwner_correct` | isOwner returns correct boolean | -| 11 | `increment_meets_spec_when_owner` | Owner increment meets specification | -| 12 | `increment_adds_one_when_owner` | Owner increment adds exactly 1 | -| 13 | `increment_reverts_when_not_owner` | Non-owner increment reverts | -| 14 | `decrement_meets_spec_when_owner` | Owner decrement meets specification | -| 15 | `decrement_subtracts_one_when_owner` | Owner decrement subtracts exactly 1 | -| 16 | `decrement_reverts_when_not_owner` | Non-owner decrement reverts | -| 17 | `transferOwnership_meets_spec_when_owner` | Owner transfer meets specification | -| 18 | `transferOwnership_changes_owner` | Owner successfully changed | -| 19 | `transferOwnership_reverts_when_not_owner` | Non-owner transfer reverts | -| 20 | `increment_preserves_owner` | Increment preserves owner | -| 21 | `decrement_preserves_owner` | Decrement preserves owner | -| 22 | `transferOwnership_preserves_count` | Transfer preserves count | -| 23 | `constructor_preserves_wellformedness` | Constructor preserves well-formedness | -| 24 | `increment_preserves_wellformedness` | Increment preserves well-formedness | -| 25 | `decrement_preserves_wellformedness` | Decrement preserves well-formedness | -| 26 | `constructor_increment_getCount` | Constructor then increment then getCount | -| 27 | `increment_unfold` | Unfold increment under owner guard | -| 28 | `decrement_unfold` | Unfold decrement under owner guard | -| 29 | `transferOwnership_unfold` | Unfold transferOwnership under owner guard | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `transfer_then_increment_reverts` | Old owner locked out of increment | -| 2 | `transfer_then_decrement_reverts` | Old owner locked out of decrement | -| 3 | `transfer_then_transfer_reverts` | Old owner locked out of re-transfer | -| 4 | `transferOwnership_preserves_wellformedness` | Well-formedness preservation | -| 5 | `increment_survives_transfer` | Counter value survives ownership transfer | - -**Isolation:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `increment_count_preserves_owner` | Increment preserves owner address storage | -| 2 | `decrement_count_preserves_owner` | Decrement preserves owner address storage | -| 3 | `constructor_owner_preserves_count` | Constructor preserves counter storage | -| 4 | `transferOwnership_owner_preserves_count` | Transfer preserves counter storage | -| 5 | `constructor_context_preserved` | Constructor preserves sender/thisAddress | -| 6 | `increment_context_preserved` | Increment preserves sender/thisAddress | -| 7 | `decrement_context_preserved` | Decrement preserves sender/thisAddress | -| 8 | `transferOwnership_context_preserved` | Transfer preserves sender/thisAddress | -| 9 | `getCount_context_preserved` | getCount preserves sender/thisAddress | -| 10 | `getOwner_context_preserved` | getOwner preserves sender/thisAddress | -| 11 | `constructor_preserves_map_storage` | Constructor preserves mapping storage | -| 12 | `increment_preserves_map_storage` | Increment preserves mapping storage | -| 13 | `decrement_preserves_map_storage` | Decrement preserves mapping storage | -| 14 | `transferOwnership_preserves_map_storage` | Transfer preserves mapping storage | - -### Ledger - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `getBalance_meets_spec` | getBalance meets specification | -| 2 | `getBalance_returns_balance` | getBalance returns stored balance | -| 3 | `getBalance_preserves_state` | getBalance is read-only | -| 4 | `deposit_meets_spec` | Deposit meets specification | -| 5 | `deposit_increases_balance` | Deposit increases sender balance | -| 6 | `deposit_preserves_other_balances` | Deposit preserves other balances | -| 7 | `withdraw_meets_spec` | Withdraw meets specification | -| 8 | `withdraw_decreases_balance` | Withdraw decreases sender balance | -| 9 | `withdraw_reverts_insufficient` | Withdraw reverts on insufficient balance | -| 10 | `transfer_meets_spec` | Transfer meets specification | -| 11 | `transfer_self_preserves_balance` | Self-transfer is a no-op | -| 12 | `transfer_decreases_sender` | Transfer decreases sender balance | -| 13 | `transfer_increases_recipient` | Transfer increases recipient balance | -| 14 | `transfer_reverts_insufficient` | Transfer reverts on insufficient balance | -| 15 | `transfer_succeeds_recipient_overflow` | Transfer succeeds on recipient overflow (wrap semantics) | -| 16 | `deposit_preserves_non_mapping` | Deposit preserves non-mapping storage | -| 17 | `withdraw_preserves_non_mapping` | Withdraw preserves non-mapping storage | -| 18 | `deposit_preserves_wellformedness` | Deposit preserves well-formedness | -| 19 | `withdraw_preserves_wellformedness` | Withdraw preserves well-formedness | -| 20 | `deposit_getBalance_correct` | Deposit then getBalance returns updated balance | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `transfer_preserves_wellformedness` | Transfer preserves WellFormedState | -| 2 | `transfer_preserves_non_mapping` | Transfer preserves non-mapping storage | -| 3 | `withdraw_getBalance_correct` | After withdraw, getBalance returns decreased balance | -| 4 | `transfer_getBalance_sender_correct` | After transfer, sender balance decreased | -| 5 | `transfer_getBalance_recipient_correct` | After transfer, recipient balance increased | -| 6 | `deposit_withdraw_cancel` | Deposit then withdraw cancellation | - -**Conservation:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `deposit_sum_equation` | `new_sum = old_sum + count(sender) * amount` | -| 2 | `deposit_sum_singleton_sender` | For unique sender: `new_sum = old_sum + amount` | -| 3 | `withdraw_sum_equation` | `new_sum + count(sender) * amount = old_sum` | -| 4 | `withdraw_sum_singleton_sender` | For unique sender: `new_sum + amount = old_sum` | -| 5 | `transfer_sum_equation` | `new_sum + count(sender)*amt = old_sum + count(to)*amt` | -| 6 | `transfer_sum_preserved_unique` | For unique sender & to: `new_sum = old_sum` | -| 7 | `deposit_withdraw_sum_cancel` | Deposit then withdraw preserves total sum | - -### SafeCounter - -**Basic:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `getCount_meets_spec` | getCount meets its specification | -| 2 | `getCount_returns_count` | getCount returns the stored count | -| 3 | `getCount_preserves_state` | getCount is read-only | -| 4 | `evm_add_eq_of_no_overflow` | EVM addition equals natural addition when no overflow | -| 5 | `increment_meets_spec` | increment meets its specification | -| 6 | `increment_adds_one` | increment adds one to count | -| 7 | `increment_preserves_other_slots` | increment preserves other storage slots | -| 8 | `increment_reverts_overflow` | increment reverts on overflow | -| 9 | `decrement_meets_spec` | decrement meets its specification | -| 10 | `decrement_subtracts_one` | decrement subtracts one from count | -| 11 | `decrement_preserves_other_slots` | decrement preserves other storage slots | -| 12 | `decrement_reverts_underflow` | decrement reverts on underflow | -| 13 | `increment_preserves_wellformedness` | increment preserves well-formedness | -| 14 | `decrement_preserves_wellformedness` | decrement preserves well-formedness | -| 15 | `increment_preserves_bounds` | increment preserves count bounds | -| 16 | `decrement_preserves_bounds` | decrement preserves count bounds | -| 17 | `increment_getCount_correct` | increment then getCount returns count + 1 | - -**Correctness:** - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `increment_preserves_context` | increment preserves context | -| 2 | `decrement_preserves_context` | decrement preserves context | -| 3 | `increment_preserves_storage_isolated` | increment preserves storage isolation | -| 4 | `decrement_preserves_storage_isolated` | decrement preserves storage isolation | -| 5 | `getCount_preserves_context` | getCount preserves context | -| 6 | `getCount_preserves_wellformedness` | getCount preserves well-formedness | -| 7 | `increment_decrement_cancel` | increment then decrement cancellation | -| 8 | `decrement_getCount_correct` | decrement then getCount equals count - 1 | - -### Stdlib/Math - -| # | Theorem | Property | -|---|---------|----------| -| 1 | `safeAdd_some` | Returns sum when no overflow | -| 2 | `safeAdd_none` | Returns none on overflow | -| 3 | `safeAdd_zero_left` | 0 + b equals b when bounded | -| 4 | `safeAdd_zero_right` | a + 0 equals a when bounded | -| 5 | `safeAdd_comm` | Commutativity | -| 6 | `safeAdd_result_bounded` | Successful result less than or equal to MAX_UINT256 | -| 7 | `safeSub_some` | Returns difference when no underflow | -| 8 | `safeSub_none` | Returns none on underflow | -| 9 | `safeSub_zero` | a - 0 equals a | -| 10 | `safeSub_self` | a - a equals 0 | -| 11 | `safeSub_result_le` | Result never exceeds minuend | -| 12 | `safeMul_some` | Returns product when no overflow | -| 13 | `safeMul_none` | Returns none on overflow | -| 14 | `safeMul_zero_left` | 0 * b equals 0, always safe | -| 15 | `safeMul_zero_right` | a * 0 equals 0, always safe | -| 16 | `safeMul_one_left` | 1 * b equals b when bounded | -| 17 | `safeMul_one_right` | a * 1 equals a when bounded | -| 18 | `safeMul_comm` | Commutativity | -| 19 | `safeMul_result_bounded` | Successful result less than or equal to MAX_UINT256 | -| 20 | `safeDiv_some` | Returns quotient when divisor nonzero | -| 21 | `safeDiv_none` | Returns none on division by zero | -| 22 | `safeDiv_zero_numerator` | 0 / b equals 0 | -| 23 | `safeDiv_by_one` | a / 1 equals a | -| 24 | `safeDiv_self` | a / a equals 1 (when a > 0) | -| 25 | `safeDiv_result_le_numerator` | Result never exceeds numerator | - -## Proof techniques - -**Full unfolding**: For guarded operations, unfold the entire do-notation chain through bind/pure/Contract.run/ContractResult.snd, then `simp [h_guard]` to resolve the guard condition. - -**Private unfold helpers**: For complex operations, a private theorem pre-computes the exact result state when guards pass. Main proofs then `rw [op_unfold]` to get the concrete state. - -**Boolean equality conversion**: `beq_iff_eq` converts between `(x == y) = true` and `x = y`. - -**List sum reasoning**: `omega` cannot handle `List.sum` or nonlinear multiplication, so conservation proofs use explicit `Nat.add_assoc`/`Nat.add_comm`/`Nat.add_left_comm` rewrite chains. - -**countOcc helpers**: `simp [countOcc, if_pos rfl]` produces `if True then 1 else 0` which doesn't reduce. Pre-proven `countOcc_cons_eq`/`countOcc_cons_ne` helpers avoid this. - -## Known limitations - -1. Uint256 is a dedicated 256-bit modular type; `+`, `-`, `*`, `/`, and `%` wrap at `2^256` -2. No multi-contract interaction -3. No reentrancy modeling -4. `supply_bounds_balances` not preserved for lists with duplicates; exact sum equations are proven instead -5. No Mathlib: `set`, `ring`, `linarith` unavailable +- [Proof Techniques](/proof-techniques) — guard modeling, unfolding, list-sum reasoning. +- [Trust Model](/trust-model) — what each theorem rules out, what assumptions remain. +- [Examples Gallery](/examples) — sources the theorems apply to. diff --git a/docs-site/next.config.mjs b/docs-site/next.config.mjs index 9cde5af34..839af5cb9 100644 --- a/docs-site/next.config.mjs +++ b/docs-site/next.config.mjs @@ -54,4 +54,20 @@ export default withNextra({ images: { formats: ["image/avif", "image/webp"], }, + // Redirect legacy URLs to the new IA so old bookmarks / external + // links don't 404 after the restructure. + async redirects() { + return [ + { source: "/guides/first-contract", destination: "/first-contract", permanent: true }, + { source: "/add-contract", destination: "/guides/add-contract", permanent: true }, + // Compiler architecture merged into /compiler. + { source: "/compiler-architecture", destination: "/compiler", permanent: true }, + // Syntax highlighting moved to the docs-site README (contributor reference, not user docs). + { source: "/guides/verity-syntax-highlighting", destination: "/", permanent: true }, + { source: "/syntax-highlighting", destination: "/", permanent: true }, + // Research log retired. + { source: "/research", destination: "/", permanent: true }, + { source: "/research/iterations", destination: "/", permanent: true }, + ]; + }, }); diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index fdd702e4f..3182b42c4 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -1,12 +1,22 @@ # Verity -> **For AI agents:** This file provides a complete overview. Add `.md` to any docs page URL to get raw markdown. +> Lean 4 framework for writing smart contracts that compile to EVM bytecode and carry machine-checked correctness proofs. +> Add `.md` to any docs URL on veritylang.com to get raw markdown (saves tokens). Or fetch `/api/docs/_all` for everything concatenated. -## Overview +## What it is -Lean 4 framework for writing smart contracts with machine-checked proofs. Three-layer verified compilation: EDSL -> CompilationModel -> IR -> Yul -> EVM bytecode. Zero axioms, zero sorry. +Three-layer verified compilation: -## Quick Facts +``` +EDSL --> CompilationModel --> IR --> Yul --> EVM bytecode + (Layer 1) (Layer 2) (Layer 3) (solc, trusted) +``` + +Every transition inside the proof envelope is either fully verified or recorded as an explicit assumption in the per-build trust report. The Yul-to-bytecode step is delegated to `solc --strict-assembly`. + +**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 0 documented Lean axioms remain (AXIOMS.md). + +## Quick facts - **Language**: Lean 4.22.0 @@ -19,39 +29,67 @@ Lean 4 framework for writing smart contracts with machine-checked proofs. Three- - **Repository**: https://github.com/lfglabs-dev/verity -## Verification Layers +## Key types -- **Layer 1** (EDSL -> CompilationModel): Per-contract bridge theorems. Generic typed-IR core. -- **Layer 2** (CompilationModel -> IR): Generic whole-contract theorem for the supported fragment. 0 axioms. -- **Layer 3** (IR -> Yul): Generic statement/function equivalence. Dispatch bridge is an explicit hypothesis. -- **External** (Yul -> bytecode): Trusted. Compiled by solc v0.8.33. Validated by differential testing. +```lean +abbrev Contract α := ContractState → ContractResult α -## Trust Boundary +inductive ContractResult (α : Type) where + | success : α → ContractState → ContractResult α + | revert : String → ContractState → ContractResult α +``` -- **Verified**: EDSL -> CompilationModel -> IR -> Yul (3 layers, 0 axioms, 0 sorry) -- **Trusted**: Yul -> bytecode (solc), Lean 4 kernel, EVM specification alignment -- See [TRUST_ASSUMPTIONS.md](https://github.com/lfglabs-dev/verity/blob/main/TRUST_ASSUMPTIONS.md) and [AXIOMS.md](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md) +`ContractState` carries six persistent storage spaces (`storage`, `storageAddr`, `storageMap`, `storageMapUint`, `storageMap2`, `storageArray`), transient storage, EVM context (`sender`, `thisAddress`, `msgValue`, `blockTimestamp`, `blockNumber`, `chainId`, `blobBaseFee`, `selfBalance`), calldata, memory, `knownAddresses` for conservation proofs, and an append-only `events` log. -## Key Types +Every primitive is a `Contract α`. Read-only primitives never revert; write primitives return `success ()`; only `require` (and `requireSomeUint`, `revertError`) may emit `revert`. The custom `bind` short-circuits on revert. -```lean --- Contracts are state-passing functions -abbrev Contract a := ContractState -> ContractResult a +## How proofs are written -inductive ContractResult (a : Type) where - | success : a -> ContractState -> ContractResult a - | revert : String -> ContractState -> ContractResult a -``` +The dominant pattern is `_meets_spec`: each EDSL operation has a `_spec` predicate, and a single `simp` with the operation, slot names, and spec definition closes the goal. For guard-protected operations, unfold the full `bind`/`Contract.run`/`ContractResult.snd` chain then pass the guard hypothesis to `simp`. See `/proof-techniques` and `/guides/debugging-proofs`. + +## Trust boundary + +- **Verified**: EDSL semantics, CompilationModel→IR, IR→Yul (three layers, zero `sorry`, zero active project-level Lean axioms per AXIOMS.md). +- **Trusted**: Lean 4 kernel, solc, EVM spec alignment, deployment toolchain, and the ECM/local-obligation **assumptions** surfaced by `--trust-report` (e.g., `erc20_balanceOf_interface`, `evm_ecrecover_precompile`, `keccak256_memory_slice_matches_evm`). +- Each build emits machine-readable `--trust-report`, `--assumption-report`, `--layout-report`, `--layout-compat-report`. Deny flags fail-closed on a specific assumption category: `--deny-unchecked-dependencies`, `--deny-assumed-dependencies`, `--deny-axiomatized-primitives`, `--deny-local-obligations`, `--deny-linear-memory-mechanics`, `--deny-event-emission`, `--deny-low-level-mechanics`, `--deny-runtime-introspection`, `--deny-proxy-upgradeability`, `--deny-layout-incompatibility`. `--deny-unsafe` is the catch-all that trips on any of those. + +## Agent benchmark + +[lfglabs-dev/verity-benchmark](https://github.com/lfglabs-dev/verity-benchmark) measures AI agent capability at proving contract specs in this framework: 30 tasks across six real-world protocols (Ethereum deposit, Lido VaultHub, Nexus Mutual RAMM, Kleros sortition, Paladin Votes, Damn Vulnerable DeFi). No `sorry`/`admit`/`axiom` placeholders allowed. + +## Documentation index + +Introduction: +- https://veritylang.com/architecture — single-page system map +- https://veritylang.com/trust-model — what is verified vs trusted + +Tutorials: +- https://veritylang.com/getting-started — local setup +- https://veritylang.com/first-contract — guided spec→proof walkthrough (TipJar) + +How-to: +- https://veritylang.com/guides/add-contract +- https://veritylang.com/guides/solidity-to-verity +- https://veritylang.com/guides/production-solidity-patterns — modifiers, ERC-7201 namespaces, ECMs, oracle patterns +- https://veritylang.com/guides/linking-libraries — `--link` for external Yul (Poseidon, etc.) +- https://veritylang.com/guides/debugging-proofs + +Reference: +- https://veritylang.com/examples — SimpleStorage / Counter / SafeCounter / Owned / OwnedCounter / Ledger / SimpleToken / Vault / ERC721 / ReentrancyExample / CryptoHash / ERC20 +- https://veritylang.com/core — ContractState, Contract monad, spec helpers (`sameAddrMapContext` etc.) +- https://veritylang.com/edsl-api-reference — every primitive, plus `verity_contract` macro features +- https://veritylang.com/compiler — pipeline, CLI flags, audit artifacts +- https://veritylang.com/verification — per-contract theorem inventory +- https://veritylang.com/glossary + +Explanation: +- https://veritylang.com/proof-techniques — guard modeling, unfolding, list-sum reasoning +- https://veritylang.com/faq + +## Working effectively in this codebase -## Documentation URLs - -- Main: https://veritylang.com/ -- Verification: https://veritylang.com/verification -- Research: https://veritylang.com/research -- Examples: https://veritylang.com/examples -- Core: https://veritylang.com/core -- Compiler: https://veritylang.com/compiler -- First contract guide: https://veritylang.com/guides/first-contract -- Solidity to Verity translation: https://veritylang.com/guides/solidity-to-verity -- Production Solidity patterns: https://veritylang.com/guides/production-solidity-patterns -- Add `.md` to any URL for raw markdown (saves tokens). +- Lean files in `Contracts//` are the source of truth; docs prose can lag. +- For *what* exists: `lake build` + `grep ^theorem Contracts/.../Proofs/*.lean`. +- For *how* to add a contract: scaffold via `python3 scripts/generate_contract.py --fields ... --functions ...`, then follow `/first-contract`. +- For *trust* questions: read the per-build `--trust-report` JSON, then cross-reference with `AXIOMS.md`. +- The `_meets_spec` pattern is the load-bearing convention; deviate only when you must. diff --git a/scripts/check_layer2_boundary_sync.py b/scripts/check_layer2_boundary_sync.py index 88131c476..b12e2ef7b 100644 --- a/scripts/check_layer2_boundary_sync.py +++ b/scripts/check_layer2_boundary_sync.py @@ -17,9 +17,8 @@ "DOCS_SITE_COMPILER": ROOT / "docs-site" / "content" / "compiler.mdx", "DOCS_SITE_INDEX": ROOT / "docs-site" / "content" / "index.mdx", "DOCS_SITE_EXAMPLES": ROOT / "docs-site" / "content" / "examples.mdx", - "DOCS_SITE_FIRST_CONTRACT": ROOT / "docs-site" / "content" / "guides" / "first-contract.mdx", + "DOCS_SITE_FIRST_CONTRACT": ROOT / "docs-site" / "content" / "first-contract.mdx", "DOCS_SITE_VERIFICATION": ROOT / "docs-site" / "content" / "verification.mdx", - "DOCS_SITE_RESEARCH": ROOT / "docs-site" / "content" / "research.mdx", "LLMS": ROOT / "docs-site" / "public" / "llms.txt", } @@ -78,10 +77,6 @@ def expected_snippets() -> dict[str, list[str]]: "DOCS_SITE_VERIFICATION": [ "**Generic whole-contract Layer 2 theorem**: `Compiler/Proofs/IRGeneration/Contract.lean`", ], - "DOCS_SITE_RESEARCH": [ - "Supported-fragment generic theorem in place.", - "`Compiler/Proofs/IRGeneration/Contract.lean`", - ], "LLMS": [ "Generic whole-contract theorem for the supported fragment. 0 axioms.", "0 documented Lean axioms", @@ -142,12 +137,6 @@ def forbidden_snippets() -> dict[str, list[str]]: "DOCS_SITE_FIRST_CONTRACT": [ "18 proof terms currently use `sorry`", ], - "DOCS_SITE_RESEARCH": [ - "Complete for all 7 contracts", - "`Verity/Examples/X.lean`", - "`Compiler/TypedIRCompilerCorrectness.lean` — Compilation correctness (generic theorem, 36 supported fragments)", - "Partial generic coverage only.", - ], "LLMS": [ "CompilationModel -> IR preservation", "3 documented axioms", diff --git a/scripts/check_struct_mapping_surface_sync.py b/scripts/check_struct_mapping_surface_sync.py index 6856e05b1..bbfb1f814 100644 --- a/scripts/check_struct_mapping_surface_sync.py +++ b/scripts/check_struct_mapping_surface_sync.py @@ -11,7 +11,7 @@ TARGET_FILES = { "ROADMAP": ROOT / "docs" / "ROADMAP.md", "COMPILER_DOC": ROOT / "docs-site" / "content" / "compiler.mdx", - "ADD_CONTRACT": ROOT / "docs-site" / "content" / "add-contract.mdx", + "ADD_CONTRACT": ROOT / "docs-site" / "content" / "guides" / "add-contract.mdx", }