From 8ded7bcf9a1f0016cee93f371796b935b25b7ff8 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 04:01:15 +0200 Subject: [PATCH] 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 --- README.md | 34 +++++++++++++------ TRUSTED-BASE.md | 22 ++++++++---- verification/check.sh | 2 +- verification/extract.sh | 8 +++-- verification/gen/CurveField/FunsExternal.lean | 17 ---------- 5 files changed, 45 insertions(+), 38 deletions(-) diff --git a/README.md b/README.md index 6ff6e2e..9e7d36b 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline: ``` ┌──────────────────────────────┐ - │ Signature (EdDSA verify) │ accepted ⇔ compress([s]B−[k]A) = R + │ Signature (EdDSA verify) │ accepted ⇔ decompress(R) = [k](−A)+[s]B ├──────────────────────────────┤ │ Scalar arithmetic mod ℓ │ Scalar52 ops correct mod ℓ ├──────────────────────────────┤ @@ -28,15 +28,15 @@ in this repository. | Field 𝔽_p | `fieldImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` | | Group law (Edwards) | `edwardsImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` | | Scalar mod ℓ | `scalarImplementation` (add ✅ sub ✅ mul ✅) | ✅ proven | `[propext, Classical.choice, Quot.sound]` | -| Signature (EdDSA) | `verify_accepts_iff` | ✅ proven (phase 1) | standard three + the button-enforced SHA-512/wire-format boundary — see [The signature apex](#the-signature-apex-phase-1) | +| Signature (EdDSA) | `verify_accepts_iff` … `verify_accepts_iff_decompress` (4 tiers) | ✅ proven (phases 1+2) | standard three + the button-enforced SHA-512/wire-format boundary — see [The signature apex](#the-signature-apex-phases-1-and-2) | Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started. This table is updated only when `verification/check.sh` passes for the layer. -## The signature apex (phase 1) +## The signature apex (phases 1 and 2) -The apex certificate `CurveFieldProofs.verify_accepts_iff` is the literal EdDSA -acceptance criterion, proven about the extracted verifier: +The byte-level apex certificate `CurveFieldProofs.verify_accepts_iff` is the +literal EdDSA acceptance criterion, proven about the extracted verifier: > For a signature that parses, the verifier returns `Ok(())` **iff** the > recomputed compressed point `compress([s]·B − [k]·A)` equals the signature's @@ -58,16 +58,30 @@ boundary. Zero curve, scalar, or backend axioms. The companion certificate `verify_loop_full` (the 32-byte comparison loop computes array equality) carries the standard three axioms only. -**Phase 2 (deferred, documented):** lifting the byte-level equation to the -point level (`[s]B − [k]A = decompress R`) additionally needs `compress` -canonicity and a verified `decompress`; it is deliberately out of scope for -this milestone, mirroring the layer-by-layer phase split used below the apex. +**Phase 2 (complete): the point-level lift.** Phase 3b enforces the SAME +axiom boundary on three further tiers that lift the byte equation to points: + +| Tier | Certificate | Statement | +|------|-------------|-----------| +| half-lift | `verify_accepts_iff_point` | accepted ⇔ R = the **canonical encoding** of `[k]·(−A) + [s]·B` (compress semantics + `to_bytes` canonicity + hash-to-scalar, recompute chain inverted) | +| point equation | `verify_accepts_iff_point_eq` | for any valid on-curve `Q` canonically encoded by R: accepted ⇔ `Q = [k]·(−A) + [s]·B` **as points** (encoding-injectivity: d non-square + parity root-selection) | +| full lift | `verify_accepts_iff_decompress` | R **decompresses** to a valid on-curve `Pt`, and accepted ⇔ `Pt = [k]·(−A) + [s]·B` — the constructive capstone | + +The full lift runs through the extracted `CompressedEdwardsY::decompress` +itself, proven end-to-end: `from_bytes` parses the y-residue exactly below +bit 255 (`from_bytes_spec`), `sqrt_ratio_i` returns the even square root of +`(y²−1)/(dy²+1)` (`sqrt_ratio_i_sq_spec`, Fermat-exponent square root), and +the sign bit selects the x-parity (`decompress_of_canonical`, standard three +axioms). Byte comparison ↔ encoding equality ↔ point equality ↔ +decompressed-point equality: every link is machine-checked over the +extracted code, and `check.sh` fails the build if any of the four tiers' +cones deviates from the boundary above. ## Source - **Upstream**: [dalek-cryptography/curve25519-dalek](https://github.com/dalek-cryptography/curve25519-dalek), commit `4cf8db2` -- **Pinned/patched source**: [saymrwulf/curve25519-dalek-source](https://github.com/saymrwulf/curve25519-dalek-source), commit `135ed70` +- **Pinned/patched source**: [saymrwulf/curve25519-dalek-source](https://github.com/saymrwulf/curve25519-dalek-source), commit `aa0f6ab` (adds the decompress step_2 negate-then-assign patch) - **Patches**: minimal Aeneas-compatibility only (documented in the source repo) - Verified backend: `backend/serial/u64` (`FieldElement51`, `Scalar52`). SIMD/AVX backends are out of scope (marked opaque). diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index b853a77..89bb16a 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -15,18 +15,26 @@ running Rust code. Everything else is machine-checked. 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: +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` (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 - oracle with no algebraic properties assumed — the theorem holds for + oracle with no algebraic properties assumed — the theorems hold for whatever bytes it produces; the SHA-512 implementation itself is NOT - verified. Zero curve, scalar, or backend axioms are in the cone. + 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. 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. diff --git a/verification/check.sh b/verification/check.sh index 0d18970..2ebeaec 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -226,7 +226,7 @@ lake env bash -c " && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\" \ && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point_eq' depends on axioms: \$ALLOWED\" \ && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_decompress' depends on axioms: \$ALLOWED\"; then - echo ' apex + half-lift axiom cones = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)' + echo ' apex + full-lift axiom cones = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)' else echo 'APEX AUDIT FAILED: apex/half-lift cone is not the documented boundary'; exit 1 fi diff --git a/verification/extract.sh b/verification/extract.sh index 0638ab2..6bd1605 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -5,9 +5,11 @@ # roots: crate::field, crate::backend::serial::u64::field, # crate::backend::serial::curve_models, crate::edwards # (same widening the reference solution used for its Tier-1 addition-law -# theorem; scalar-mul backends and decompress internals stay opaque — -# upstream Aeneas cannot translate them; they are modeled/axiomatized in -# gen/CurveField/FunsExternal.lean OUTSIDE every certificate's cone). +# theorem; scalar-mul backends stay opaque — upstream Aeneas cannot +# translate them; they are modeled/axiomatized in +# gen/CurveField/FunsExternal.lean OUTSIDE every certificate's cone. +# decompress IS extracted since the phase-2 full lift — the source's +# step_2 uses the documented negate-then-conditional-assign rewrite). # # Rust --charon--> CurveField.llbc --aeneas--> gen/CurveField/*.lean # diff --git a/verification/gen/CurveField/FunsExternal.lean b/verification/gen/CurveField/FunsExternal.lean index 6cf5c2c..0a1253a 100644 --- a/verification/gen/CurveField/FunsExternal.lean +++ b/verification/gen/CurveField/FunsExternal.lean @@ -397,23 +397,6 @@ axiom edwards.affine.AffinePoint.Insts.CoreCmpEq.assert_fields_are_eq axiom edwards.CompressedEdwardsY.Insts.CoreCmpEq.assert_fields_are_eq : edwards.CompressedEdwardsY → Result Unit -/-- [curve25519_dalek::edwards::decompress::step_2]: - Source: 'curve25519-dalek/src/edwards.rs', lines 240:4-257:5 -/ -axiom edwards.decompress.step_2 - : - edwards.CompressedEdwardsY → backend.serial.u64.field.FieldElement51 → - backend.serial.u64.field.FieldElement51 → - backend.serial.u64.field.FieldElement51 → Result edwards.EdwardsPoint - -/-- [curve25519_dalek::edwards::decompress::step_1]: - Source: 'curve25519-dalek/src/edwards.rs', lines 226:4-237:5 -/ -axiom edwards.decompress.step_1 - : - edwards.CompressedEdwardsY → Result (subtle.Choice × - backend.serial.u64.field.FieldElement51 × - backend.serial.u64.field.FieldElement51 × - backend.serial.u64.field.FieldElement51) - /-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::from_slice]: Source: 'curve25519-dalek/src/edwards.rs', lines 423:4-425:5 Visibility: public -/