diff --git a/AXIOMS.md b/AXIOMS.md index 39346e36b..04db8d072 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -41,6 +41,63 @@ Instead, Verity treats it as a black box and validates its outputs in CI. **Risk**: Low. +### 2. `solidityMappingSlot_lt_evmModulus` + +**Location**: `Compiler/Proofs/MappingSlot.lean:125` + +**Statement**: +```lean +axiom solidityMappingSlot_lt_evmModulus (baseSlot key : Nat) : + solidityMappingSlot baseSlot key < Compiler.Constants.evmModulus +``` + +**Purpose**: +Asserts that the keccak256 hash used to compute a Solidity mapping slot fits +in 256 bits (i.e. is less than 2^256). This is mathematically true because +keccak256 produces exactly 32 bytes, but unprovable in Lean because `ffi.KEC` +is an opaque FFI call that does not expose the output length. + +**Why this is currently an axiom**: +The FFI boundary hides the byte-length guarantee. Proving it would require +internalising the keccak256 spec or exposing output-length metadata from the +FFI layer. + +**Soundness controls**: +- End-to-end regression suites exercise mapping reads/writes. +- Mapping-slot abstraction boundary checks in CI. + +**Risk**: Low. + +### 3. `solidityMappingSlot_add_wordOffset_lt_evmModulus` + +**Location**: `Compiler/Proofs/MappingSlot.lean:140` + +**Statement**: +```lean +axiom solidityMappingSlot_add_wordOffset_lt_evmModulus + (baseSlot key wordOffset : Nat) : + solidityMappingSlot baseSlot key + wordOffset < Compiler.Constants.evmModulus +``` + +**Purpose**: +Asserts that adding a word offset to a mapping slot still fits in 256 bits. +This is used when accessing struct fields stored at consecutive slots after +a mapping base slot. In practice, word offsets are tiny (typically < 32) +while keccak256 outputs are uniformly distributed over a 256-bit range, so +overflow is astronomically unlikely. + +**Why this is currently an axiom**: +Same FFI opacity as axiom 2, plus the additional assumption that the offset +does not cause overflow. A tighter formulation could bound `wordOffset` +explicitly, but the current version is simpler and sufficient for struct +layout proofs. + +**Soundness controls**: +- End-to-end regression suites exercise struct-in-mapping access patterns. +- Mapping-slot abstraction boundary checks in CI. + +**Risk**: Low. + ## Trusted Cryptographic Primitive (Non-Axiom) ### `ffi.KEC` (keccak256 via FFI) @@ -134,7 +191,7 @@ specification. ## Trust Summary -- Active axioms: 1 +- Active axioms: 3 - Production blockers from axioms: 0 - Enforcement: `scripts/check_axioms.py` ensures this file tracks exact source locations. - All internal compiler functions are proven to terminate (no axioms involved). @@ -147,4 +204,4 @@ Any commit that adds, removes, renames, or moves an axiom must update this file If this file is stale, trust analysis is stale. -**Last Updated**: 2026-03-11 +**Last Updated**: 2026-03-27 diff --git a/README.md b/README.md index 05b17f97a..f13e1fd4c 100644 --- a/README.md +++ b/README.md @@ -119,7 +119,7 @@ EVM Bytecode | 2 | A generic whole-contract theorem exists for the current explicit supported fragment, and its function-level closure now runs by theorem rather than axiom. The theorem statements are in place but the Layer 2 proof scripts are currently being repaired after a definition refactor (PR #1639) and contain `sorry` placeholders; see [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md). The theorem surface explicitly assumes normalized transaction-context fields. Follow-on work in [#1510](https://github.com/Th0rgal/verity/issues/1510) focuses on widening the fragment. | [Contract.lean](Compiler/Proofs/IRGeneration/Contract.lean) | | 3 | IR → Yul codegen is proved generically at the statement/function level, but the current full dispatch-preservation path still uses 1 documented bridge hypothesis; the checked contract-level theorem surface now makes dispatch-guard safety explicit for each selected function case | [Preservation.lean](Compiler/Proofs/YulGeneration/Preservation.lean) | -There is currently 1 documented Lean axiom in total: the selector axiom. Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom. See [AXIOMS.md](AXIOMS.md). +There are currently 3 documented Lean axioms in total: the selector axiom and 2 mapping-slot range axioms. Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom. See [AXIOMS.md](AXIOMS.md). Layer 1 is the frontend EDSL-to-`CompilationModel` bridge. The per-contract files in `Contracts//Proofs/` prove human-readable contract specifications; they are not what "Layer 1" means in the compiler stack. Layer 2 now has a generic whole-contract theorem for the explicit supported fragment. The compiler proves Layer 2 preservation automatically — no manual per-contract bridge proofs are needed. Layers 2 and 3 (`CompilationModel → IR → Yul`) are verified with the current documented axioms and bridge boundaries; see [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md), [docs/GENERIC_LAYER2_PLAN.md](docs/GENERIC_LAYER2_PLAN.md), and [AXIOMS.md](AXIOMS.md). diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 363cb49d9..130ffb407 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -16,7 +16,7 @@ Yul EVM Bytecode ``` -The repository currently has `sorry` placeholders in the Layer 2 proof scripts (Source → IR), which are being repaired after a definition refactor (PR #1639 added `transientStorage` to `WorldState` and expanded interpreter definitions); the theorem statements are unchanged but their tactic proofs need updating. Layer 3 (IR → Yul) proofs remain fully discharged, and it now has 1 documented Lean axiom. See [AXIOMS.md](AXIOMS.md) for the exact list and current elimination plan. +The repository currently has `sorry` placeholders in the Layer 2 proof scripts (Source → IR), which are being repaired after a definition refactor (PR #1639 added `transientStorage` to `WorldState` and expanded interpreter definitions); the theorem statements are unchanged but their tactic proofs need updating. Layer 3 (IR → Yul) proofs remain fully discharged, and it now has 3 documented Lean axioms. See [AXIOMS.md](AXIOMS.md) for the exact list and current elimination plan. ## What's Verified @@ -38,7 +38,7 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V ### 2. Lean Axioms - **Role**: Bridge remaining proof obligations not yet fully discharged. -- **Status**: 1 documented axiom in [AXIOMS.md](AXIOMS.md): the selector axiom. The Layer 2 generic body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge remains an explicit theorem hypothesis rather than a Lean axiom. +- **Status**: 3 documented axioms in [AXIOMS.md](AXIOMS.md): the selector axiom and 2 mapping-slot range axioms. The Layer 2 generic body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge remains an explicit theorem hypothesis rather than a Lean axiom. - **Mitigation**: CI axiom reporting and location checks enforce explicit tracking. ### 3. Keccak-based Selector Computation diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index 83dc00a8b..12449c2bf 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -18,7 +18,7 @@ Lean 4 EDSL for writing smart contracts with machine-checked proofs. Three-layer - **Core Size**: 400 lines - **Verified Contracts**: SimpleStorage, Counter, Owned, SimpleToken, OwnedCounter, Ledger, SafeCounter, ReentrancyExample (+ CryptoHash as unverified linker demo) - **Theorems**: 273 across 10 categories, 273 fully proven; Layer 2 proof scripts contain `sorry` placeholders (being repaired after definition refactor) -- **Axioms**: 1 documented Lean axiom (see AXIOMS.md) — the selector axiom. Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps an explicit dispatch bridge hypothesis rather than a Lean axiom. +- **Axioms**: 3 documented Lean axioms (see AXIOMS.md) — the selector axiom and 2 mapping-slot range axioms. Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps an explicit dispatch bridge hypothesis rather than a Lean axiom. - **Tests**: 478 Foundry tests, multi-seed differential testing (7 seeds), 8-shard parallel CI - **Build**: `lake build` verifies all proofs - **Repository**: https://github.com/Th0rgal/verity @@ -126,7 +126,7 @@ Add `.md` to any URL for raw markdown (saves tokens). See TRUST_ASSUMPTIONS.md for full analysis. Key trust boundaries: - **Verified**: EDSL -> CompilationModel -> IR -> Yul - **Trusted**: Yul -> Bytecode (via solc, validated by 90,000+ differential tests) -- **Axioms**: 1 documented Lean axiom, with soundness justification in AXIOMS.md +- **Axioms**: 3 documented Lean axioms, with soundness justification in AXIOMS.md - **External**: Lean 4 kernel, EVM specification alignment ## Known Limitations diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md index ff74b6b19..6a0a4558c 100644 --- a/docs/VERIFICATION_STATUS.md +++ b/docs/VERIFICATION_STATUS.md @@ -161,7 +161,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co 4 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules. These are concentrated in the Layer 2 proof modules (`Compiler/Proofs/IRGeneration/`) due to a definition refactor (PR #1639) that added helper-aware interpreter targets. The theorem statements are structurally sound; the tactic proofs are being repaired. Layer 3 proofs and all contract-level specification proofs are fully discharged. -1 documented Lean axiom remains. The Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom. +3 documented Lean axioms remain (1 selector axiom, 2 mapping-slot range axioms). The Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom. ## Differential Testing diff --git a/scripts/check_axioms.py b/scripts/check_axioms.py index 79c6d9858..0e76b55d0 100644 --- a/scripts/check_axioms.py +++ b/scripts/check_axioms.py @@ -27,6 +27,8 @@ DOCUMENTED_AXIOMS = frozenset([ "keccak256_first_4_bytes", + "solidityMappingSlot_lt_evmModulus", + "solidityMappingSlot_add_wordOffset_lt_evmModulus", ]) FORBIDDEN_AXIOMS = frozenset([ diff --git a/scripts/check_layer2_boundary_sync.py b/scripts/check_layer2_boundary_sync.py index ab2e16d4e..71f4dd586 100644 --- a/scripts/check_layer2_boundary_sync.py +++ b/scripts/check_layer2_boundary_sync.py @@ -33,7 +33,7 @@ def expected_snippets() -> dict[str, list[str]]: return { "AXIOMS": [ "### 1. `keccak256_first_4_bytes`", - "- Active axioms: 1", + "- Active axioms: 3", ], "COMPILER_PROOFS_README": [ "`Compiler.Proofs.IRGeneration.Contract.compile_preserves_semantics`", @@ -57,14 +57,14 @@ def expected_snippets() -> dict[str, list[str]]: "Layer 2: CompilationModel → IR [GENERIC WHOLE-CONTRACT THEOREM]", "Layer 2 now has a generic whole-contract theorem for the explicit supported fragment.", "its function-level closure now runs by theorem rather than axiom", - "There is currently 1 documented Lean axiom in total: the selector axiom.", + "There are currently 3 documented Lean axioms in total: the selector axiom and 2 mapping-slot range axioms.", "Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom.", ], "TRUST_ASSUMPTIONS": [ "Layer 2: SUPPORTED-FRAGMENT GENERIC THEOREM — CompilationModel → IR", "A generic whole-contract theorem is proved for the current supported `CompilationModel` fragment.", "former generic body-simulation axiom has been eliminated", - "it now has 1 documented Lean axiom", + "it now has 3 documented Lean axioms", "explicit theorem hypothesis rather than a Lean axiom", ], "DOCS_SITE_COMPILER": [ @@ -91,7 +91,7 @@ def expected_snippets() -> dict[str, list[str]]: ], "LLMS": [ "generic whole-contract CompilationModel -> IR theorem for the supported fragment", - "1 documented Lean axiom", + "3 documented Lean axioms", ], } @@ -127,14 +127,12 @@ def forbidden_snippets() -> dict[str, list[str]]: "depends on 2 documented axioms", "documented bridge axiom", "1 generic non-core Layer 2 axiom", - "There are currently 3 documented Lean axioms in total", "There are currently 4 documented Lean axioms in total", ], "TRUST_ASSUMPTIONS": [ "FULLY VERIFIED — CompilationModel → IR", "All three layers are proven in Lean", "2 documented sub-axioms for generic body simulation and the `execIRFunctionFuel`/`execIRFunction` bridge", - "3 documented Lean axioms", "4 documented Lean axioms", "1 documented bridge axiom", "2 documented axioms in [AXIOMS.md](AXIOMS.md): 1 selector axiom and 1 generic non-core Layer 2 axiom", diff --git a/scripts/check_proof_length.py b/scripts/check_proof_length.py index b1ce1e156..c61aba66d 100644 --- a/scripts/check_proof_length.py +++ b/scripts/check_proof_length.py @@ -547,6 +547,10 @@ # long due to explicit scope-discipline threading through the full # compiled statement list; decomposition is follow-up cleanup. "compileStmt_ok_any_scope_aux", + # PR #1670 — GenericInduction setStorage bridge: long because it threads + # identifier-shape and function-reference validation through the full + # compiled storage-write step; mechanical plumbing, not proof complexity. + "compiledStmtStep_setStorage_of_validateIdentifierShapes_of_validateFunctionIdentifierReferences", } # Directories containing proof files to scan. diff --git a/scripts/test_check_layer2_boundary_sync.py b/scripts/test_check_layer2_boundary_sync.py index b2cad4131..43f5ab695 100644 --- a/scripts/test_check_layer2_boundary_sync.py +++ b/scripts/test_check_layer2_boundary_sync.py @@ -74,8 +74,8 @@ def test_detects_stale_axiom_count_language(self) -> None: target = root / check.TARGETS["ROOT_README"].relative_to(check.ROOT) target.write_text( target.read_text(encoding="utf-8").replace( + "There are currently 3 documented Lean axioms in total: the selector axiom and 2 mapping-slot range axioms.", "There is currently 1 documented Lean axiom in total: the selector axiom.", - "There are currently 3 documented Lean axioms in total: 1 selector axiom, 1 generic non-core Layer 2 axiom, and 1 Layer 3 dispatch bridge axiom.", ), encoding="utf-8", ) @@ -98,7 +98,7 @@ def test_detects_stale_axiom_count_language(self) -> None: check.TARGETS = old_targets self.assertEqual(rc, 1) - self.assertIn("There are currently 3 documented Lean axioms in total", output) + self.assertIn("missing `There are currently 3 documented Lean axioms in total", output) def test_compiler_proofs_readme_stale_axiom_wording_is_forbidden(self) -> None: forbidden = check.forbidden_snippets()