Phase 3 and 3b mktemp an audit file, compile it, then removed only the .lean —
leaving the .olean behind on every run. check-scalar.sh:38 has always done this
correctly (`rm -f "$AUD" "${AUD%.lean}.olean"`); the main script was the odd one
out. Estate-wide that had accumulated 101 orphan compiled modules with no
sibling source (dalek 44, anza/risc0/betrusted 19 each), invisible to git
because *.olean is gitignored. All swept.
The litter was inert — the names are not valid Lean identifiers, so nothing
could import them. It matters as a pattern: an audit whose verdict can depend on
untracked build state is the class of defect that took eight review rounds to
close in the sibling SLH-DSA repository (there: an orphan .olean with its source
deleted satisfied an import and the button went green). A build-hygiene phase
that purges compiled artifacts and bans stray files is the proper fix and is
queued as part of the protocol port; this commit stops the bleeding.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
(verify_accepts_iff_decompress, button-enforced)
Port of the dalek decompress chain to the risc0 fork (v4 gen):
- source patch 8b69091: decompress step_2 negate-then-conditional-assign
(the documented sqrt_ratio_i rewrite; sqrt_ratio_i itself was already
in the compatible shape); extract.sh: decompress un-opaqued,
re-extracted - the step_1/step_2 external axioms vanish from the
template, decompress is transparent.
- Proofs/DecompressSpec.lean: dalek port, instance rename
Shared0FieldElement51 -> SharedAFieldElement51.
- Proofs/FromBytesSpec.lean: PORT DELTA - this gen's from_bytes takes
RangeFrom subslices (bytes[k..]) into a local load8 CLOSURE with
literal indices instead of dalek's named load8_at: new
range_from_index_spec (over the step_simps-reduced slice index) +
closure_call_spec (same disjoint-OR loader math); window/telescope
arithmetic identical.
- Proofs/DecompressMain.lean: decompress_of_canonical (standard three)
+ verify_accepts_iff_decompress (corollary verbatim - this fork's
point-equation signature is byte-identical to dalek's):
accept <=> decompress(R) = [k]*(-A) + [s]*B (as points).
check.sh: 4-tier Phase 3b; full-lift cone exactly [3 standard +
Signature + sha512_hash3 + to_bytes + Error + Error.new]. Full button
green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
verify_accepts_iff_point_eq, button-enforced
Port of dalek's PointEqSpec (the encoding-injectivity mathematics is
fork-independent; compiled first try): for any valid on-curve point Q
whose canonical encoding is the signature's R bytes, the verifier
accepts IFF Q equals the recomputed point as denoted affine points -
the literal point-level EdDSA verification equation, no decompress
needed. enc_point_inj carries the standard three axioms; the equation
itself carries exactly this fork's enforced apex boundary, and Phase 3b
now audits all three tiers (byte apex, half-lift, point equation).
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full replication of dalek's phase 2 in one increment - the five files
ported with only the v4 deltas (to_bytes -> as_bytes on both serializers,
byte-identical bodies verified; compress inlines the affine conversion;
recompute has ONE sha512_hash3 oracle bind instead of five, so the
inversion is a single bind_ok_inv before the proven tail). Every proof
compiled FIRST TRY after the mechanical renames.
- Proofs/ToBytesMath + ToBytesSpec: field as_bytes canonicity.
- Proofs/ScalarPackSpec: scalar pack + canonical hash-to-scalar entry.
- Proofs/CompressSpec: ed_compress_spec - compress emits the canonical
encoding of the denoted affine point.
- Proofs/PointLiftSpec: dsm dispatch transfer, byte-comparison bridge,
recompute inversion, and THE HALF-LIFT verify_accepts_iff_point:
accept IFF the signature's R bytes are the canonical encoding of the
recomputed [k](-A) + [s]B (valid, on-curve, certified model).
check.sh: five new certificates (exact standard three) and Phase 3b now
enforces the hash3 + wire-format boundary on BOTH apex and half-lift.
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replicates dalek's apex with this fork's sha2-0.10 adaptation: the hash
oracle is the single monomorphic sha512_hash3(R, A, m) call (no foreign
types in its signature — the 0.10 Sha512 alias cannot be declared opaque),
and extraction runs --no-default-features so the error path avoids boxed
dyn-Error.
- gen/CurveSig: the extracted verify glue, definitionally welded to the
proven model (TypesExternal/FunsExternal import CurveField; every curve
and scalar call is a certified definition).
- Proofs/SigApexSpec.lean (unchanged from dalek): verify_loop_full (the
32-byte comparison = array equality; axiom cone exactly the standard
three) and verify_accepts_iff — accept IFF compress([s]B - [k]A) = R
byte-for-byte, SHA-512 opaque.
- check.sh Phase 3b: the apex axiom cone is enforced to be EXACTLY
[propext, Classical.choice, Quot.sound, ed25519.Signature,
verifying.sha512_hash3, ed25519.Signature.to_bytes,
signature.error.Error, signature.error.Error.new]
- zero curve, scalar, or backend axioms.
Full check.sh green: 17 standard certificates + the apex audit.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
remaining-bits measure: per-step 64-bit window read (4-way word split),
digit write via hcast/wrapping_sub (exact value window - 32*carry',
oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
DISCHARGED; the digits satisfy the NAF conditions and
sum naf[k]*2^k = V EXACTLY (integers, no modular slack)
for any scalar whose LE byte value V is below 2^253.
And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
kernel-checked via denominator-free 121666-scaled witnesses. Includes the
generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
vartime_double_base::mul: for canonical scalars and a valid on-curve A,
the result is valid, on-curve, and denotes
dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
with both digit arrays proven exact NAF encodings. Phase 2 (group
semantics [a]A + [b]B) requires Edwards associativity — deferred and
documented; nothing assumes it.
Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.
CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three new proof files over the CurveField extraction, composing the proven
group-law layer (no new axioms, no associativity assumed — computational
layering over the abstract `edAdd`):
- `Proofs/DsmTableSpec.lean` — `NafLookupTable5::from(&A)`: the 8 entries
are valid `ProjectiveNielsPoint` caches of valid on-curve points denoting
the odd multiples A, 3A, ..., 15A as the `edOdd` double-and-add recursion.
7 explicit loop peels over edwards_as_projective_niels_spec /
add_projniels_law / compl_as_extended_law, seeded by edwards_double_law.
`select`: both masserts (x odd, x < 16) DISCHARGED — panic-freedom is
proven, not assumed; post enumerates all 8 digit cases.
- `Proofs/DsmStepSpec.lean` — `proj_double_law` (the projective doubling
denotes `edAdd P P`; same Z^2-scaled linear_combination discipline as the
extended-coordinate law), `compl_as_projective_law` ((X:Z),(Y:T) to
(XT:YZ:ZT) preserves the point), `naf_select_entry` (digit-indexed lookup
returns THE entry: NafEntryOf r A ((x-1)/2)), and `dsm_step_p_law` /
`dsm_step_b_law`: the three-way NAF digit step denotes `edDigit` — add
the d-th odd multiple, add its negation, or pass through.
- `Proofs/DsmLoopSpec.lean` — the 256-iteration Straus loop by GENUINE
induction on the counter (one symbolic body walk, no unrolling):
`dsm_loop_spec` — from the identity, the loop returns a valid on-curve
point denoting `dsmFold ... edId 256`, the abstract double-and-add fold
of both digit arrays over the table points. Digit and table hypotheses
are exactly what the NAF spec and naf_table_spec provide (layering).
check.sh wired: PROOFS + AUDIT_IMPORTS + 7 new CERTS (naf_table_spec,
naf_select_spec, proj_double_law, compl_as_projective_law, dsm_step_p_law,
dsm_step_b_law, dsm_loop_spec), each `#print axioms`-audited to exactly
[propext, Classical.choice, Quot.sound]. Full check.sh green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- check.sh: proofs memory default 6144 -> 8192 (ReduceSpec's norm_num
step peaks above 6144; guard aborted gracefully — R3 was broken, S1
held). Matches pasta's calibration.
- check.sh: dead-file gate now exempts Scalar* (delegated to
check-scalar.sh); the gate had been un-passable since the scalar layer
landed, masked by the memory failure.
- check.sh: axiom-audit phase routed through lean-guard (cgroup + flock;
was raw lean -M), audit temp file moved into the workspace (lake env
rejects /tmp inputs — the /tmp phase had never run green).
- check-scalar.sh: NEW Phase 3 kernel axiom audit — ScalarProofs.L_val
must report exactly [propext, Classical.choice, Quot.sound].
- README: signature layer '⏳ planned' (was 'in progress' with nothing
started); planned certificate names marked as such.
Validated: full check.sh + check-scalar.sh green end-to-end in the pass-2
sweep (see formal-verification-control/COHERENCE-PASS-2.md).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Ported from the locally verified Hermes working copy; FeQ and Square2Spec
(dead files in the published replica) now compile and are in the check
manifest. Basic.lean (never compiled under v4 Aeneas) removed rather than
shipped dead.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
