Skip to content

TRUST_ASSUMPTIONS.md

Latest commit

 

History

History
114 lines (85 loc) · 8.47 KB

TRUST_ASSUMPTIONS.md

File metadata and controls

114 lines (85 loc) · 8.47 KB

Trust Assumptions and Verification Boundaries

This document states what Verity proves and what it still trusts.

Compilation Pipeline

EDSL (Lean)
  ↓ [Layer 1: PROVEN FOR CURRENT CONTRACTS, generic core, contract bridges]
CompilationModel
  ↓ [Layer 2: SUPPORTED-FRAGMENT GENERIC THEOREM -- CompilationModel → IR]
IR
  ↓ [Layer 3: GENERIC SURFACE, explicit bridge hypothesis, IR → Yul]
Yul
  ↓ [trusted: solc]
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 for details.

What's Verified

  • Layer 1: A generic typed-IR compilation-correctness core exists, but the active contract-level bridges are still instantiated per contract and internal-helper proof reuse is not yet a first-class generic interface. This names the frontend EDSL-to-CompilationModel bridge only; the contract-specific specification theorems in Contracts/<Name>/Proofs/ are a separate proof layer about human-readable contract behavior.
  • Layer 2: A generic whole-contract theorem is proved for the current supported CompilationModel fragment. supported_function_correct is now a real theorem, the initial-state normalization step is proved, the former generic body-simulation axiom has been eliminated, and the theorem surface makes explicit that the observed transaction-context fields must already be normalized to the bounded source-side Address/Uint256 domains. Remaining Layer 2 work is now about widening the supported fragment and helper-aware completeness, not repairing sorry placeholders.
  • Layer 3: IR → Yul preservation is generic at the proof surface, and the remaining dispatch bridge now lives as an explicit theorem hypothesis rather than a Lean axiom. The checked contract-level theorem surface makes the dispatch-guard safety preconditions explicit: non-payable cases must see word-level zero msg.value, and each selected function case must have a non-wrapping calldata-width guard.

Current theorem totals, property-test coverage, and proof status live in docs/VERIFICATION_STATUS.md.

Trusted Components

1. Solidity Compiler (solc)

  • Role: Compiles Yul → EVM bytecode.
  • Version: 0.8.33+commit.64118f21 (pinned).
  • Mitigation: CI enforces pin and Yul compileability checks.

2. Lean Axioms

  • Role: Bridge remaining proof obligations not yet fully discharged.
  • Status: 0 documented axioms in 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.
  • Mitigation: CI axiom reporting and location checks enforce explicit tracking.

3. Keccak-based Selector Computation

  • Role: Function selector derivation (bytes4(keccak256(signature))).
  • Status: kernel-computable in Compiler/Selectors.lean via the vendored unrolled Keccak engine in Compiler/Keccak/.
  • Mitigation: CI cross-checks against solc --hashes, selector fixtures, and fixed selector examples.

4. Linked Yul Libraries

  • Role: External functions injected at compile time (e.g., Poseidon hash).
  • Trust: Semantic correctness of linked code. Compiler validates names, arities, collisions.

5. Mapping Slot Derivation

  • Role: keccak256(abi.encode(key, baseSlot)) for Solidity-compatible storage (activeMappingSlotBackend = .keccak).
  • Trust: external keccak implementation (ffi.KEC via EVMYul FFI) + standard collision-resistance assumptions (same trust class as Solidity/EVM).
  • Mitigation: Abstraction-boundary CI, selector/hash cross-checks.
  • Audit surface: machine-readable trust reports now emit the explicit primitive assumption keccak256_memory_slice_matches_evm whenever a contract uses Expr.keccak256.

6. EVM/Yul Semantics and Gas

  • Role: Runtime execution model.
  • Status: 15 pure builtins bridged to EVMYulLean UInt256 operations; 15 universal pure bridge theorems are now proven in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean. All pure bridge cases are now covered by universal symbolic lemmas. Gas is not modeled.
  • Implication: Semantic correctness does not imply gas-safety.
  • Proxy note: delegatecall-based proxy / upgradeability flows still sit outside the current proof-interpreter model. Archive --trust-report and use --deny-proxy-upgradeability when proxy semantics must remain outside the selected verified subset (issue #1420).

7. External Call Modules (ECMs)

  • Role: Reusable typed external call patterns (ERC-20 writes/reads including totalSupply, ERC-4626 preview/conversion helpers plus totalAssets, asset, max* limit reads, and deposit, oracle reads, precompiles, callbacks).
  • Trust: Each module's compile produces correct Yul. Bug in one module doesn't affect others.
  • Mitigation: Axiom aggregation at compile time (--verbose), machine-readable trust-surface emission via --trust-report <path>, and a fail-closed verification gate via --deny-unchecked-dependencies when unchecked foreign surfaces must be excluded. See docs/EXTERNAL_CALL_MODULES.md.

8. Lean Kernel

  • Role: Proof checker soundness. Foundational assumption for all Lean-based verification.

9. Macro Elaborator (verity_contract)

  • Role: Generates both EDSL Contract monad value and CompilationModel from one syntax tree.
  • Status: Trusted unverified metaprogram (Verity/Macro/Translate.lean).
  • Risk: A translation bug would silently cause EDSL and CompilationModel to diverge.
  • Mitigation: The generic Layer 2 whole-contract theorem, macro-generated _semantic_preservation body-alignment checks, and differential tests catch divergence on the current contract set.

10. Local Unsafe / Refinement Obligations

  • Role: Let a function or constructor declare a localized proof obligation for an unsafe/assembly-shaped boundary without marking the whole contract as opaque.
  • Status: Surfaced explicitly in --trust-report, --verbose, and proofStatus.*.localObligations.
  • Mitigation: verity-compiler --deny-local-obligations fails closed on any obligation that remains assumed or unchecked.

Semantic Caveats

Wrapping Arithmetic

Uint256 arithmetic is wrapping modulo 2^256, matching the EVM. This is proven, not assumed (see Compiler/Proofs/ArithmeticProfile.lean). Checked operations (safeAdd, safeSub, safeMul) are available for overflow protection. See docs/ARITHMETIC_PROFILE.md.

Revert-State Modeling

High-level semantics can expose intermediate state in reverted computations. EVM reverts discard state. Contracts should use checks-before-effects. See docs/REVERT_STATE_MODEL.md.

Security Audit Checklist

  1. Confirm deployment uses the supported EDSL CLI path.
  2. Review AXIOMS.md; ensure the axiom list is unchanged and justified.
  3. If linked libraries are used, audit each linked Yul file as trusted code.
  4. Validate selector, Yul compile, and storage-layout CI checks.
  5. Confirm arithmetic and revert assumptions are acceptable for the target contract.
  6. Review the low-level mechanics / external assumption report (--verbose) and archive --trust-report <path> for audit evidence when external calls or linked externals are used. For verification-oriented builds, also pass --deny-unchecked-dependencies so any remaining unchecked foreign surface fails closed.

Planned Hardening

  • Issue #967: Proof-carrying Yul rewrite rules, versioned parity packs, AST identity gates.
  • Issue #998: Per-function machine-checked EDSL execution ≡ EVMYulLean(compile(CompilationModel)) theorems.

Related Documents

Last Updated: 2026-04-09 Maintainer Rule: Update on every trust-boundary-relevant code change.