saymrwulf/risc0-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/risc0-ed25519-verified.git synced 2026-09-03 19:53:45 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
risc0-ed25519-verified/TRUSTED-BASE.md
mrwulf a6e32a41a6 Coherence pass 3: post-apex accuracy sweep, hygiene, guard ladder 
- README: the pyramid diagram claimed the cofactored ZIP-215 equation,
  which is NOT the proven statement - corrected to the actual theorem
  (accepted IFF compress([s]B-[k]A) = R, byte-for-byte) and the signature
  row now names verify_accepts_iff; new "The signature apex (phase 1)"
  section states the theorem, this repo's glue architecture, the exact
  button-enforced axiom cone, and the phase-2 deferral.
- TRUSTED-BASE: item 5 rewritten from an aspirational hash paragraph to
  the structural boundary - certificate name, exact allowed cone, and the
  Phase 3b enforcement that fails the build on any deviation.
- Dead pre-merge artifacts removed: gen/CurveScalar, CurveScalar.llbc,
  extract-scalar.sh (the merged gen/CurveField universe is the single
  model; check-scalar.sh remains the scalar button, header updated).
- lean-guard: Guard 3a retry ladder (LEAN_MEM_WAIT_SEC) - a clamped run
  that dies on memory retries as headroom improves, converting ambient
  memory pressure from a deterministic abort into a delayed pass.

Fresh green buttons after these changes: check.sh (incl. Phase 3b apex
audit) + check-scalar.sh, both at shipped defaults, coherence pass 3
sweep 2026-07-05.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-05 11:48:19 +02:00

2.4 KiB
Raw Blame History

Trusted base

What you must believe for the theorems in this repository to transfer to the running Rust code. Everything else is machine-checked.

  1. Lean 4 kernel (v4.30.0-rc2) and its three foundational axioms [propext, Classical.choice, Quot.sound]. Every certificate is #print axioms-audited against exactly this list.
  2. mathlib (prebuilt oleans fetched by lake exe cache get).
  3. Charon + Aeneas (pinned 9dd7f23c / bf13c42e): the translation from Rust MIR to the Lean model is assumed faithful. The generated gen/ files are never edited (comments only); proofs are stated ABOUT them.
  4. External-function models (gen/*/FunsExternal.lean): Rust items that Aeneas cannot translate (constant-time subtle primitives, iterator plumbing, formatting) are axiomatized as opaque symbols. The axiom audit proves none of these axioms enters the dependency cone of any certificate, except where a model is explicitly listed below.
  5. The signature-apex boundary (signature layer only): the apex certificate CurveFieldProofs.verify_accepts_iff ("the verifier accepts iff compress([s]·B − [k]·A) = R byte-for-byte") is #print axioms-audited by check.sh Phase 3b against EXACTLY the standard three plus this documented set, and the build fails on any deviation: ed25519.Signature (wire-format type), the single SHA-512 oracle verifying.sha512_hash3 (semantically Sha512(R ‖ A ‖ msg)), ed25519.Signature.to_bytes, and signature.error.Error/Error.new (opaque error type). The hash is an oracle with no algebraic properties assumed — the theorem holds for whatever bytes it produces; the SHA-512 implementation itself is NOT verified. Zero curve, scalar, or backend axioms are in the cone.
  6. Scalar52::sub::black_box (scalar layer): this fork's v4.1.3 code implements the constant-time conditional via a local black_box = unsafe { core::ptr::read_volatile(&value) }. The volatile read is an optimization fence whose VALUE semantics is the identity; it is modeled as id in gen/CurveField/FunsExternal.lean (merged gen). (Upstream v5 uses subtle here; betrusted v4.1.2 uses a pure arithmetic mask — each fork is verified against its own strategy.)
  7. Compilation of Rust to machine code (rustc backend) is out of scope, as is side-channel behaviour (timing, speculation). The proofs are about functional correctness at the MIR/LLBC level.