mirror of
https://github.com/saymrwulf/anza-ed25519-verified.git
synced 2026-09-03 20:13:46 +00:00
mrwulf
673c15e10a
- 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>
41 lines
2.6 KiB
Markdown
41 lines
2.6 KiB
Markdown
# 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.
|