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.
|
2026-07-06 02:01:15 +00:00
|
|
|
|
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:
|
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:17 +00:00
|
|
|
|
`ed25519.Signature` (wire-format type), the three SHA-512 wrapper
|
|
|
|
|
|
oracles `verifying.sha512_new/update/finalize_bytes` (+ the opaque
|
|
|
|
|
|
`sha2.Sha512` state type), `ed25519.Signature.to_bytes`, and
|
|
|
|
|
|
`signature.error.Error`/`Error.new` (opaque error type). The hash is an
|
2026-07-06 02:01:15 +00:00
|
|
|
|
oracle with no algebraic properties assumed — the theorems hold for
|
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:17 +00:00
|
|
|
|
whatever bytes it produces; the SHA-512 implementation itself is NOT
|
2026-07-06 02:01:15 +00:00
|
|
|
|
verified. Zero curve, scalar, or backend axioms are in any of the four
|
|
|
|
|
|
cones. The constructive decompress theorem underneath the full lift
|
|
|
|
|
|
(`decompress_of_canonical`) carries the standard three axioms ONLY.
|
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.
|