diff --git a/AUDIT.md b/AUDIT.md index 88f8aece3c..6da11278ef 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -363,7 +363,10 @@ sibling entrypoint. listed-vs-written slot inequality. A lone `writeTransient` preserves the same lists by constructor injectivity (`StorageKey.transient` vs persistent `.slot` / `.map` / `.mapUint` / `.map2`); no slot - inequality. Global (all-keys) preservation remains open. + inequality. Global aligned `writeMap`+`writeSlot` preservation of + `MappingCoherent` uses `solidityMappingSlot_injective`. Lone + `writeSlot` all-keys remains open. C5 step 4 is not axiom-free + complete. `FieldEncode` derives `findResolvedFieldAtSlot` from `findFieldWithResolvedSlot` plus no write-slot conflict, persistent, and unpacked, then identifies that slot with `encodeStorageAt`. diff --git a/AXIOMS.md b/AXIOMS.md index 42cd93b8fe..cb60a99dee 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -13,24 +13,17 @@ Axioms are exceptional. When an axiom exists, it must have: ## Current Axioms -**None.** Verity has zero project-level Lean axioms. - -- Active axioms: 0 - -The last remaining axiom (`solidityMappingSlot_lt_evmModulus`) was eliminated -by replacing the opaque FFI-based keccak256 call with the kernel-computable -Keccak engine (`Compiler/Keccak/Sponge.lean`), which exposes the 32-byte -output-length guarantee to Lean's proof system. +- Active axioms: 1 C5 step 3 (`ContractState.storageWords` over injective `StorageKey`) does not add a keccak-injectivity axiom. Source lens laws use constructor injectivity; Solidity slot derivation remains compiler-side. -C5 step 4's mapping-coherence, field-list, and finite-set slices -likewise add no axiom: other-pair and finite-list preservation -(address / uint / map2, including cross-channel lists) is -hypothesized by an explicit derived-slot inequality, not by keccak -injectivity. `FieldStorageKey` is a +C5 step 4's finite-set slices still use explicit derived-slot +inequalities. Global aligned-write `MappingCoherent` preservation +depends on `solidityMappingSlot_injective` below — collision-resistance +of the 64-byte ABI mapping preimage, **not** injectivity of keccak256 +on arbitrary byte strings. `FieldStorageKey` is a constructor match on `FieldType` / `isTransient`; struct-member slots add `wordOffset` via `mappingSlotLocation`. Compatibility `aliasSlots` are extra compiler slots, not extra source keys. @@ -54,6 +47,40 @@ FunctionSpec call denotation (`DenoteFunctionCalls`), ETH-valued is an explicit `AdversaryModel` / `calleeStep` parameter, not an assumed transition. +### 1. `solidityMappingSlot_injective` + +**Location**: `Compiler/Proofs/MappingSlot.lean:65` + +**Statement**: +```lean +axiom solidityMappingSlot_injective + (base₁ key₁ base₂ key₂ : Nat) : + solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ → + base₁ = base₂ ∧ key₁ = key₂ +``` + +**Justification**: +`solidityMappingSlot base key` is `keccak256(abi.encode(key, base))` — +a 64-byte ABI preimage. Distinct `(base, key)` pairs colliding would +alias two Solidity mapping entries onto one EVM word. Solidity's +layout makes the same collision-resistance assumption. This is **not** +a claim that keccak256 is injective on all `ByteArray`s (256-bit +output, infinite domain). + +**Risk**: Medium. A keccak collision on this preimage family would +make the global `MappingCoherent` preservation theorem false. Finite +listed-pair certificates remain valid without the axiom. + +**CI validation**: +- `scripts/check_axioms.py` location + count check +- `DOCUMENTED_AXIOMS` in that script +- Kernel Keccak output is already cross-checked against FFI/EVM keccak + +**Elimination path**: +Replace with a theorem if a restricted-domain injectivity proof +becomes available, or keep as an explicit cryptographic assumption +and stop calling C5 step 4 axiom-free. + ## Eliminated Axioms ### 1. `solidityMappingSlot_lt_evmModulus` (eliminated) @@ -357,7 +384,7 @@ proof exists. ## Trust Summary -- Active project-level axioms: 0 +- Active project-level axioms: 1 - Production blockers from project-level axioms: 0 - Consumer intrinsic obligations: owned and documented by consumer packages - Enforcement: `scripts/check_axioms.py` ensures this file tracks exact source locations. diff --git a/Compiler/Proofs/MappingSlot.lean b/Compiler/Proofs/MappingSlot.lean index d37529060d..935f3a3c55 100644 --- a/Compiler/Proofs/MappingSlot.lean +++ b/Compiler/Proofs/MappingSlot.lean @@ -13,7 +13,7 @@ Mapping slot abstraction used by proof interpreters. The active backend is keccak-faithful (`solidityMappingSlot`). -## Axiom elimination (zero-axiom target) +## Range axiom eliminated; slot collision-resistance is axiomatic The mapping-slot definition now uses the kernel-computable `KeccakEngine.keccak256` so that the output-length bound is structurally provable. The FFI version (`ffi.KEC`) @@ -57,6 +57,25 @@ private def solidityMappingSlot_ffi (baseSlot key : Nat) : Nat := def solidityMappingSlot (baseSlot key : Nat) : Nat := EvmYul.fromByteArrayBigEndian (KeccakEngine.keccak256 (abiEncodeMappingSlot baseSlot key)) +/-- Collision-resistance of Solidity mapping-slot derivation + `keccak256(abi.encode(key, baseSlot))`. + + **Not** injectivity of keccak256 on arbitrary `ByteArray`s (256-bit + output, infinite domain). See `AXIOMS.md`. -/ +axiom solidityMappingSlot_injective + (base₁ key₁ base₂ key₂ : Nat) : + solidityMappingSlot base₁ key₁ = solidityMappingSlot base₂ key₂ → + base₁ = base₂ ∧ key₁ = key₂ + +theorem solidityMappingSlot_ne {base₁ key₁ base₂ key₂ : Nat} + (h : base₁ ≠ base₂ ∨ key₁ ≠ key₂) : + solidityMappingSlot base₁ key₁ ≠ solidityMappingSlot base₂ key₂ := by + intro heq + rcases solidityMappingSlot_injective base₁ key₁ base₂ key₂ heq with ⟨hb, hk⟩ + cases h with + | inl hbase => exact hbase hb + | inr hkey => exact hkey hk + /-- Active proof-model mapping slot encoding backend. -/ def abstractMappingSlot (baseSlot key : Nat) : Nat := solidityMappingSlot baseSlot key @@ -250,6 +269,33 @@ theorem abstractMappingSlot_lt_evmModulus (baseSlot key : Nat) : abstractMappingSlot baseSlot key < Compiler.Constants.evmModulus := solidityMappingSlot_lt_evmModulus baseSlot key +theorem abstractNestedMappingSlot_injective + (base₁ key₁ key₂ base₂ key₁' key₂' : Nat) + (h : abstractNestedMappingSlot base₁ key₁ key₂ = + abstractNestedMappingSlot base₂ key₁' key₂') : + base₁ = base₂ ∧ key₁ = key₁' ∧ key₂ = key₂' := by + have hinj := + solidityMappingSlot_injective + (solidityMappingSlot base₁ key₁) key₂ + (solidityMappingSlot base₂ key₁') key₂' (by + simpa [abstractNestedMappingSlot, abstractMappingSlot] using h) + rcases hinj with ⟨hinner, hkey2⟩ + rcases solidityMappingSlot_injective base₁ key₁ base₂ key₁' hinner with ⟨hbase, hkey1⟩ + exact ⟨hbase, hkey1, hkey2⟩ + +theorem abstractNestedMappingSlot_ne + {base₁ key₁ key₂ base₂ key₁' key₂' : Nat} + (h : base₁ ≠ base₂ ∨ key₁ ≠ key₁' ∨ key₂ ≠ key₂') : + abstractNestedMappingSlot base₁ key₁ key₂ ≠ + abstractNestedMappingSlot base₂ key₁' key₂' := by + intro heq + rcases abstractNestedMappingSlot_injective base₁ key₁ key₂ base₂ key₁' key₂' heq + with ⟨hb, hk1, hk2⟩ + rcases h with h | h | h + · exact h hb + · exact h hk1 + · exact h hk2 + theorem solidityMappingSlot_add_lt_evmModulus (baseSlot key wordOffset : Nat) (h : wordOffset < Compiler.Constants.evmModulus - solidityMappingSlot baseSlot key) : solidityMappingSlot baseSlot key + wordOffset < Compiler.Constants.evmModulus := by diff --git a/Compiler/Proofs/Storage/MappingCoherence.lean b/Compiler/Proofs/Storage/MappingCoherence.lean index f179ccfce6..5ae87d095b 100644 --- a/Compiler/Proofs/Storage/MappingCoherence.lean +++ b/Compiler/Proofs/Storage/MappingCoherence.lean @@ -4,8 +4,8 @@ Source `StorageKey` constructors stay injective. Keccak layout lives only here, on the compiler side. Global preservation of `MappingCoherent` is - not claimed: that needs finite non-alias certificates, because keccak - injectivity is not assumed. + not claimed without `solidityMappingSlot_injective`. That axiom is + ABI mapping-preimage collision-resistance, not keccak-on-all-bytes. -/ import Verity.Core @@ -194,4 +194,71 @@ theorem storageKeySlot_map2 (slot : Nat) (k1 k2 : Address) : some (abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val) := rfl +theorem addressToWord_injective {a b : Address} + (h : addressToWord a = addressToWord b) : a = b := by + apply Core.Address.ext + have hval : + a.toNat % Core.Uint256.modulus = b.toNat % Core.Uint256.modulus := by + simpa [addressToWord, Core.Uint256.val_ofNat] using + congrArg Core.Uint256.val h + have ha : a.toNat < Core.Uint256.modulus := + Nat.lt_trans a.isLt (by decide : Core.ADDRESS_MODULUS < Core.Uint256.modulus) + have hb : b.toNat < Core.Uint256.modulus := + Nat.lt_trans b.isLt (by decide : Core.ADDRESS_MODULUS < Core.Uint256.modulus) + rw [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb] at hval + simpa [Core.Address.toNat] using hval + +theorem mappingAddrSlot_ne_of_map_ne {slot slot' : Nat} {key key' : Address} + (h : StorageKey.map slot' key' ≠ StorageKey.map slot key) : + solidityMappingSlot slot' (addressToWord key').val ≠ + solidityMappingSlot slot (addressToWord key).val := by + intro heq + rcases solidityMappingSlot_injective slot' (addressToWord key').val + slot (addressToWord key).val heq with ⟨hs, hk⟩ + apply h + rw [hs, addressToWord_injective (Core.Uint256.ext hk)] + +theorem mappingUintSlot_ne_of_mapUint_ne {slot slot' : Nat} {key key' : Uint256} + (h : StorageKey.mapUint slot' key' ≠ StorageKey.mapUint slot key) : + solidityMappingSlot slot' key'.val ≠ solidityMappingSlot slot key.val := by + intro heq + rcases solidityMappingSlot_injective slot' key'.val slot key.val heq with ⟨hs, hk⟩ + apply h + rw [hs, Core.Uint256.ext hk] + +theorem mappingMap2Slot_ne_of_map2_ne + {slot slot' : Nat} {k1 k1' k2 k2' : Address} + (h : StorageKey.map2 slot' k1' k2' ≠ StorageKey.map2 slot k1 k2) : + abstractNestedMappingSlot slot' (addressToWord k1').val (addressToWord k2').val ≠ + abstractNestedMappingSlot slot (addressToWord k1).val (addressToWord k2).val := by + intro heq + rcases abstractNestedMappingSlot_injective slot' (addressToWord k1').val + (addressToWord k2').val slot (addressToWord k1).val (addressToWord k2).val heq + with ⟨hs, hk1, hk2⟩ + apply h + rw [hs, addressToWord_injective (Core.Uint256.ext hk1), + addressToWord_injective (Core.Uint256.ext hk2)] + +/-- Global aligned-write preservation. Other-pair slot inequality comes + from `solidityMappingSlot_injective`, not from a listed certificate. + Not injectivity of keccak on all ByteArrays. -/ +theorem writeMap_aligned_preserves_mappingCoherent + (s : ContractState) (slot : Nat) (key : Address) (v : Uint256) + (hcoh : MappingCoherent s) : + MappingCoherent + ((s.writeMap slot key v).writeSlot + (solidityMappingSlot slot (addressToWord key).val) v) := by + intro slot' key' + by_cases hs : slot' = slot + · by_cases hk : key' = key + · simpa [hs, hk] using writeMap_aligned_same s slot key v + · have hkey : StorageKey.map slot' key' ≠ StorageKey.map slot key := by + intro heq; injection heq with _ hk'; exact hk hk' + exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key') + hkey (mappingAddrSlot_ne_of_map_ne hkey) + · have hkey : StorageKey.map slot' key' ≠ StorageKey.map slot key := by + intro heq; injection heq with hs' _; exact hs hs' + exact writeMap_aligned_other s slot key v slot' key' (hcoh slot' key') + hkey (mappingAddrSlot_ne_of_map_ne hkey) + end Compiler.Proofs.Storage.MappingCoherence diff --git a/Compiler/Proofs/Storage/MappingCoherenceOn.lean b/Compiler/Proofs/Storage/MappingCoherenceOn.lean index 9e5212d64f..46320023e0 100644 --- a/Compiler/Proofs/Storage/MappingCoherenceOn.lean +++ b/Compiler/Proofs/Storage/MappingCoherenceOn.lean @@ -12,8 +12,9 @@ constructor injectivity (`StorageKey.transient` vs persistent `.slot` / `.map` / `.mapUint` / `.map2`). No slot inequality. - This is not global preservation. A certificate for every pair would - be keccak injectivity on an unbounded preimage set. + Global `MappingCoherent` aligned-write preservation lives in + `MappingCoherence.writeMap_aligned_preserves_mappingCoherent` and + depends on `solidityMappingSlot_injective`. This file stays finite-set. -/ import Compiler.Proofs.Storage.MappingCoherence diff --git a/PrintAxioms.lean b/PrintAxioms.lean index e2c2f69c6e..df4c726014 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -4637,6 +4637,7 @@ end Verity.AxiomAudit Compiler.Proofs.LoopSimulation.forEach_sum_over_array -- Compiler/Proofs/MappingSlot.lean + Compiler.Proofs.solidityMappingSlot_ne Compiler.Proofs.abstractMappingSlot_eq_solidity Compiler.Proofs.abstractMappingTag_eq_zero Compiler.Proofs.abstractDecodeMappingSlot_eq_none @@ -4655,6 +4656,8 @@ end Verity.AxiomAudit Compiler.Proofs.solidityMappingSlot_lt_evmModulus Compiler.Proofs.mappingSlotLocation_zero Compiler.Proofs.abstractMappingSlot_lt_evmModulus + Compiler.Proofs.abstractNestedMappingSlot_injective + Compiler.Proofs.abstractNestedMappingSlot_ne Compiler.Proofs.solidityMappingSlot_add_lt_evmModulus Compiler.Proofs.solidityMappingSlot_add_wordOffset_lt_evmModulus @@ -4738,6 +4741,11 @@ end Verity.AxiomAudit Compiler.Proofs.Storage.MappingCoherence.writeMap2_aligned_other Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_mapUint Compiler.Proofs.Storage.MappingCoherence.storageKeySlot_map2 + Compiler.Proofs.Storage.MappingCoherence.addressToWord_injective + Compiler.Proofs.Storage.MappingCoherence.mappingAddrSlot_ne_of_map_ne + Compiler.Proofs.Storage.MappingCoherence.mappingUintSlot_ne_of_mapUint_ne + Compiler.Proofs.Storage.MappingCoherence.mappingMap2Slot_ne_of_map2_ne + Compiler.Proofs.Storage.MappingCoherence.writeMap_aligned_preserves_mappingCoherent -- Compiler/Proofs/Storage/MappingCoherenceOn.lean Compiler.Proofs.Storage.MappingCoherenceOn.mappingCoherentOn_of_mappingCoherent @@ -6966,4 +6974,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 6458 theorems/lemmas (4588 public, 1870 private, 0 sorry'd) +-- Total: 6466 theorems/lemmas (4596 public, 1870 private, 0 sorry'd) diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 4357d14ec4..091bca6f66 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -16,7 +16,7 @@ Yul EVM Bytecode ``` -The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 0 documented Lean axioms. See [AXIOMS.md](AXIOMS.md) for details. Audit evidence and generated trust-boundary artifacts are indexed in [AUDIT.md](AUDIT.md). +The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 1 documented Lean axiom (`solidityMappingSlot_injective`). See [AXIOMS.md](AXIOMS.md) for details. Audit evidence and generated trust-boundary artifacts are indexed in [AUDIT.md](AUDIT.md). ## 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**: 0 documented axioms in [AXIOMS.md](AXIOMS.md). The mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, 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**: 1 documented axiom in [AXIOMS.md](AXIOMS.md): `solidityMappingSlot_injective` (collision-resistance of `keccak256(abi.encode(key, base))`, not keccak injectivity on all inputs). The mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, 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 @@ -224,8 +224,11 @@ stays coherent under an aligned write when the list carries an explicit pairwise derived-slot certificate (`MappingCoherentOn` / `MappingCoherentUintOn` / `MappingCoherentMap2On`); that is not a global (all-keys) claim. Cross-channel preservation of another -list likewise takes an explicit derived-slot inequality. Keccak -injectivity is **not** assumed. +list likewise takes an explicit derived-slot inequality. Global +aligned `writeMap`+`writeSlot` preservation of `MappingCoherent` +uses `solidityMappingSlot_injective` (64-byte ABI preimage +collision-resistance). Keccak injectivity on arbitrary byte +strings is **not** assumed. `storageArray` and `knownAddresses` are still separate fields. ### External-Call Journal (`ContractState.calls`) diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json index a7d33677b9..134482b006 100644 --- a/artifacts/verification_status.json +++ b/artifacts/verification_status.json @@ -4,7 +4,7 @@ "example_contracts": 18 }, "proofs": { - "axioms": 0, + "axioms": 1, "sorry": 0 }, "schema_version": 1, diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index c7f625dc6f..bc9c2a0f87 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -25,7 +25,7 @@ EDSL --> CompilationModel --> IR --> Yul --> EVM bytecode 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). Internal helper calls exist at the source level, and helper-summary proof reuse is available in source-semantics lemmas, but that reuse is not yet fully consumed through the generic body/IR theorem path. ECMs, typed interface calls, external calls, and low-level call/returndata mechanics are trust-reported or compiler-supported rather than fully proof-modeled. Constructors, fallback/receive, events/logs, typed errors, proxy/delegatecall, local obligations, and richer storage-layout features remain outside the generic proof fragment or partial. `forEach` proof support is partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved; positive non-empty loop bodies and nonliteral bounds are not yet proved. +**Layer 2**: Generic whole-contract theorem for the supported fragment. 0 axioms. 1 documented Lean axiom remains project-wide (`solidityMappingSlot_injective`; Layer 2 still 0). Internal helper calls exist at the source level, and helper-summary proof reuse is available in source-semantics lemmas, but that reuse is not yet fully consumed through the generic body/IR theorem path. ECMs, typed interface calls, external calls, and low-level call/returndata mechanics are trust-reported or compiler-supported rather than fully proof-modeled. Constructors, fallback/receive, events/logs, typed errors, proxy/delegatecall, local obligations, and richer storage-layout features remain outside the generic proof fragment or partial. `forEach` proof support is partial: zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops are proved; positive non-empty loop bodies and nonliteral bounds are not yet proved. ## Quick facts @@ -34,7 +34,7 @@ Every transition inside the proof envelope is either fully verified or recorded - **Core Size**: 1098 lines - **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault) - **Theorems**: 314 across 15 categories, 314 fully proven -- **Axioms**: 0 documented Lean axioms (see AXIOMS.md) +- **Axioms**: 1 documented Lean axiom (`solidityMappingSlot_injective`; see AXIOMS.md) - **Tests**: 528 Foundry tests, 239 property tests - **Build**: `lake build` verifies all proofs - **Repository**: https://github.com/lfglabs-dev/verity diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 04ea755682..026f867711 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -42,7 +42,9 @@ Next: derive the executable shallow program from the deep model per-function `_bridge` theorems into one AST-induction theorem (`GenericInduction/LegacyCompatibility` and the compile-derived legacy-compatibility witness chain are already retired), then finish C5 -step 4 — remaining global (all-keys) `MappingCoherent` preservation. +step 4 — global aligned `MappingCoherent` preservation now depends on +`solidityMappingSlot_injective`; lone-`writeSlot` all-keys remains +open and is not claimed. Implemented: address/uint/map2 coherence laws, `FieldStorageKey` (including address-keyed mappingStruct member slots, bytes32-keyed compiler slots, all `MappingType.nested` key-type @@ -55,7 +57,10 @@ as extra compiler write targets), and finite-set `MappingCoherentOn` / `MappingCoherentUintOn` / `MappingCoherentMap2On` under explicit pairwise derived-slot certificates, including cross-channel aligned-write, lone -`writeSlot`, and lone `writeTransient` preservation. FunctionSpec +`writeSlot`, and lone `writeTransient` preservation. Global +aligned `writeMap`+`writeSlot` preservation of `MappingCoherent` +is `writeMap_aligned_preserves_mappingCoherent`, under +`solidityMappingSlot_injective`. FunctionSpec raw/linked calls with target, value and ETH debit are denoted in `DenoteFunctionCalls` (base `evalExpr`/`execStmt` stay `none`/`.revert` so `DenoteAgreement` holds). Payable calls credit diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md index 1bb0bc117a..aebb3ef2a3 100644 --- a/docs/VERIFICATION_STATUS.md +++ b/docs/VERIFICATION_STATUS.md @@ -217,7 +217,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co 0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules. 5266 theorems/lemmas (3645 public, 1621 private) verified by `lake build PrintAxioms`. -0 documented Lean axioms remain. The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, 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. +1 documented Lean axiom remains: `solidityMappingSlot_injective` (mapping-slot ABI preimage collision-resistance). The former mapping-slot *range* axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, 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. Layer 2 itself still has 0 axioms. ## Differential Testing diff --git a/scripts/check_axioms.py b/scripts/check_axioms.py index ca6c90baa8..09a34a5cdc 100644 --- a/scripts/check_axioms.py +++ b/scripts/check_axioms.py @@ -31,7 +31,7 @@ ]) DOCUMENTED_AXIOMS = frozenset([ - # Zero project axioms — solidityMappingSlot_lt_evmModulus eliminated via kernel Keccak + "Compiler.Proofs.solidityMappingSlot_injective", ]) FORBIDDEN_AXIOMS = frozenset([ diff --git a/scripts/docsync.py b/scripts/docsync.py index c43d14a4d9..8454c7c952 100644 --- a/scripts/docsync.py +++ b/scripts/docsync.py @@ -588,7 +588,8 @@ def check(self, root: Path) -> int: required={ "AXIOMS": [ "### 1. `solidityMappingSlot_lt_evmModulus` (eliminated)", - "- Active axioms: 0", + "- Active axioms: 1", + "`solidityMappingSlot_injective`", ], "COMPILER_PROOFS_README": [ "Generic whole-contract theorem", @@ -613,7 +614,7 @@ def check(self, root: Path) -> int: "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 0 documented Lean axioms", + "it now has 1 documented Lean axiom", "explicit theorem hypothesis rather than a Lean axiom", ], "DOCS_SITE_COMPILER": [ @@ -636,7 +637,7 @@ def check(self, root: Path) -> int: ], "LLMS": [ "Generic whole-contract theorem for the supported fragment. 0 axioms.", - "0 documented Lean axioms", + "1 documented Lean axiom", ], }, forbidden={ @@ -648,7 +649,7 @@ def check(self, root: Path) -> int: "### 2. `supported_function_body_correct_from_exact_state`", "supported_function_body_correct_from_exact_state", "- Active axioms: 3", - "- Active axioms: 1", + "- Active axioms: 0", ], "VERIFICATION_STATUS": [ "## Layer 2: CompilationModel → IR — COMPLETE", @@ -679,7 +680,6 @@ def check(self, root: Path) -> int: "2 documented axioms in [AXIOMS.md](AXIOMS.md): 1 selector axiom and 1 generic non-core Layer 2 axiom", "Layer 3: GENERIC SURFACE, 1 axiom — IR → Yul", "1 Layer 3 dispatch bridge axiom", - "it now has 1 documented Lean axiom", ], "DOCS_SITE_COMPILER": [ "**Layer 2 framework proof**: `CompilationModel -> IR` preserves semantics.", @@ -696,7 +696,6 @@ def check(self, root: Path) -> int: "3 documented axioms", "4 documented axioms", "partial generic CompilationModel -> IR boundary", - "1 documented Lean axiom", ], }, missing_message=(