mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
e4b73a555d
- 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>
32 lines
2 KiB
Markdown
32 lines
2 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)**: 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. **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.
|