2026-07-02 11:10:26 +00:00
|
|
|
|
# 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.
|
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 09:48:18 +00:00
|
|
|
|
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` (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 theorem holds 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()`.
|
2026-07-02 11:10:26 +00:00
|
|
|
|
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.
|