saymrwulf/anza-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/anza-ed25519-verified.git synced 2026-09-04 20:24:06 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
anza-ed25519-verified/TRUSTED-BASE.md
mrwulf 25b73f1778 Coherence pass 4 (the closing pass): 4-tier apex documentation + hygiene 
- README: pyramid-diagram apex row upgraded to the proven full lift
  (accepted <=> decompress(R) = [k](-A)+[s]B), status table names all
  four button-enforced tiers, apex section gains the phase-2 tier table
  (half-lift / point equation / full lift) + the decompress-chain
  summary; source pin updated to the pushed patch commit.
- TRUSTED-BASE item 5: rewritten from the single byte-apex certificate
  to the FOUR enforced tiers (decompress_of_canonical noted as
  standard-three-only).
- gen/CurveField/FunsExternal.lean: stale root-namespace
  edwards.decompress.step_1/step_2 axioms removed (dead weight left
  behind by un-opaquing; outside every cone, but they forced
  fully-qualified unfolds - see control FAILURES.md).
- check.sh Phase 3b success echo aligned to "apex + full-lift" (echo
  only; the enforcing greps covered all four tiers already).

Validated by the pass-4 sweep: 9/9 buttons green (this repo's check.sh
+ check-scalar.sh among them), logs retained in the pass workspace.
Full record: formal-verification-control/COHERENCE-PASS-4.md.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-06 04:01:17 +02:00

2.6 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): FOUR apex-tier certificates — CurveFieldProofs.verify_accepts_iff (byte apex: accepted iff compress([s]·B − [k]·A) = R byte-for-byte), verify_accepts_iff_point (half-lift: R is the canonical encoding of the recomputed point), verify_accepts_iff_point_eq (point equation: canonically-encoded Q accepted iff Q equals the recomputed point), and verify_accepts_iff_decompress (full lift: R decompresses to a valid on-curve point that equals the recomputed point) — are each #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 (the foreign wire-format type), the single SHA-512 oracle ed_sigs.sha512_hash3 (semantically Sha512(R ‖ A ‖ msg)), and the two byte accessors ed25519.Signature.r_bytes/s_bytes. The Error enum, the parse/filter helpers, and backend selection are real extracted code (no axioms). The hash is an oracle with no algebraic properties assumed — the theorems hold for whatever bytes it produces; the SHA-512 implementation itself is NOT verified. The verified entry point is verify_sha512 ≡ verify_dalek (canonical-R path), not the crate's default HEEA/Zebra verify(). The constructive decompress theorem underneath the full lift (decompress_of_canonical) carries the standard three axioms ONLY.
  6. 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.