Skip to content

AUDIT.md

Latest commit

 

History

History
88 lines (73 loc) · 5.01 KB

AUDIT.md

File metadata and controls

88 lines (73 loc) · 5.01 KB

Audit Registry

This file records trust-boundary changes and the evidence that keeps them reviewable. Keep it synchronized with TRUST_ASSUMPTIONS.md and AXIOMS.md whenever semantics, trusted components, generated audit artifacts, or CI boundary checks change.

Current Audit State

  • Lean proof placeholders: 0 sorry in compiler/proof modules.
  • Project-level Lean axioms: 0. See AXIOMS.md.
  • Authoritative safe-body Yul runtime target: pinned lfglabs-dev/EVMYulLean.
  • The previous reference-comparison modules have been removed from the live proof tree; native EVMYulLean is the checked runtime boundary.
  • Yul-to-bytecode compilation remains trusted through pinned solc 0.8.33.
  • Consumer-declared intrinsics are consumer-owned trust boundaries. The CLZ prototype keeps Verity at 0 project-level axioms and requires downstream packages to document any assumed intrinsic obligation they declare.
  • Gas safety is not modeled by the semantic preservation theorems.

Issue #1722: EVMYulLean Semantic Target

Status: full semantic integration for safe compiler-produced bodies.

The EVMYulLean transition moved the safe-body EndToEnd runtime target from Verity-owned Yul builtin scaffolding to native EVMYulLean runtime execution. The current proof surface has:

  • 36 of 36 builtin bridge theorems proven.
  • 0 admitted bridge lemmas.
  • smod and sar bridge equivalences fully discharged.
  • compileStmtList_always_bridged proven for BridgedSafeStmts.
  • Public native EndToEnd wrappers whose runtime target is EvmYul.Yul.callDispatcher.

The external-call/function-table family (internalCall, internalCallAssign, externalCallBind, and ecm) now has function-table-aware closure scaffolding in Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean. The public surface — BridgedSourceInternalCallStmt, BridgedSourceExternalCallBindStmt, BridgedSourceEcmStmt (with the per-module ECMBridgeable obligation), and the corresponding compileStmt_*_bridged / compileStmtList_*_bridged closure theorems — discharges BridgedStmts against a BridgedFunctionTable. The composition lemma BridgedStmts_of_compileStmtList_append lets concrete contracts chain these closures with compileStmtList_always_bridged across an arbitrary pfx ++ sfx split. End-to-end smoke proof in the same file. Wiring of SupportedFragment / SupportedSpec for contracts that actually use this family is the next milestone.

Audit Artifacts

Artifact Purpose Check
artifacts/evmyullean_adapter_report.json Adapter coverage, admitted bridge lemmas, safe-body integration status python3 scripts/generate_evmyullean_adapter_report.py --check
artifacts/evmyullean_fork_audit.json Pinned fork divergence and non-semantic fork delta python3 scripts/generate_evmyullean_fork_audit.py --check
artifacts/evmyullean_capability_report.json EVMYulLean capability surface and reference-oracle paths python3 scripts/generate_evmyullean_capability_report.py --check
PrintAxioms.lean / generated axiom report Axiom dependency visibility python3 scripts/generate_print_axioms.py --check and lake build PrintAxioms
Compiler.Proofs.IRGeneration.IntrinsicProofs Proven Verity-owned intrinsic plumbing: scope accounting, generic lowering shape, fork-order facts, and arity rejection lake build Compiler.Proofs.IRGeneration.IntrinsicProofs
Intrinsic fork gate Fail-closed min_fork enforcement against --target-fork / YulEmitOptions.targetFork lake build Compiler.CompileDriverTest
trust_report.intrinsics[*] Planned consumer-declared intrinsic trust surface: name, emission mode, opcode/builtin target, obligation, min_fork, and source location Follow-up hardening; until then, grep consumer trees for verity_intrinsic

CI Guards

  • make check validates generated reports, bridge coverage synchronization, builtin bridge matrix synchronization, Lean hygiene, proof length, and documentation counters.
  • make test-evmyullean-fork validates the pinned fork audit, checks the adapter report, rebuilds the public EndToEnd EVMYulLean target, and runs the concrete bridge-equivalence tests.
  • .github/workflows/evmyullean-fork-conformance.yml runs the EVMYulLean fork conformance probe weekly. Scheduled or manual failures fail the workflow and open or update a GitHub issue for drift triage.
  • Intrinsic fork enforcement is fail-closed: builds using an intrinsic whose min_fork exceeds the contract target fail unless the caller passes --allow-future-fork-intrinsics.

Update Checklist

  1. Update TRUST_ASSUMPTIONS.md for the human-readable trust boundary.
  2. Update AXIOMS.md if axioms, non-axiom trusted primitives, or soundness controls changed.
  3. Update this file with the changed audit state, artifacts, and CI guards.
  4. Regenerate deterministic artifacts with the relevant scripts/generate_*.py command.
  5. Run make check; run targeted Lean builds for changed proof modules.

Last Updated: 2026-05 (intrinsics addition)