Phase B - montgomery_reduce (Proofs/ScalarMontSpec.lean + Proofs/ScalarReduceSpec.lean):
- mont_key: LFACTOR*L0 + 1 = 214835089243030*2^52 (the -1 inverse identity, norm_num)
- mont_cancel: (s + ((s*LFACTOR) % 2^52)*L0) % 2^52 = 0 via Nat.ModEq - every
part1 shift is an EXACT division, nothing discarded
- part1_spec / part2_spec: per-round helpers (carry*2^52 = sum + p*L0; exact split)
- mont_head_telescope (E0-E4) and mont_tail_telescope (E5-E8): linear_combination
certificates with weights 2^52k; mont_bound: X' < 2*ell from Z < 2^260*ell
- montgomery_reduce_spec: post `scDenote r * 2^260 = Z` in ZMod ell + 52-bit bounds.
METHOD-4 split at the round-4/5 boundary: the 74-step monolith is
elaboration-pathological; each half compiles in ~25s/3GB.
- The single death-spiral line: an omega for the nonce-sum bound with ~110
hypotheses in context never returns; extracted to nonce_sum_bound (5 hypotheses,
instant). Bisected with fail-probes; documented in control-repo FAILURES.md.
Phase C - mul (Proofs/ScalarFullMulSpec.lean):
- RR_limbs/RR_scVal/RR_lt; RR_denote: RR = 2^520 - K*ell kernel-checked, so
⟦RR⟧ = R^2; R_isUnit: 2^260 unit of ZMod ell (coprime oddness witness)
- mul_spec: mul_internal -> montgomery_reduce -> mul_internal(*, RR) ->
montgomery_reduce composed; column values folded by `ring`; R cancelled via
IsUnit.mul_right_cancel. Hypothesis scVal a * scVal b < 2^260*ell (honest
Montgomery bound; canonical inputs satisfy it).
Aggregate (Proofs/ScalarMain.lean): scalar_add/sub/mul_correct on ScBnd
interfaces + canonical_mul_bound + scalarImplementation bundling all three.
sub_val_spec/add_val_spec posts strengthened with result-limb 52-bit bounds
(the montgomery tail feeds sub's output back into mul_internal).
check-scalar.sh: 9 proof files, 10 kernel audits (was 6), all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
Proofs/ScalarAddSpec.lean, axiom-clean, no sorry:
- add_loop_spec: the 5-limb carry loop unrolled (same skeleton as the
proven conditional-add-L chain, with b's limbs in place of L's
constants); per-limb equations r_i + 2^52*g_(i+1) = a_i + b_i + g_i.
- add_val_spec: denote(add a b) = denote a + denote b in ZMod l for
limb-bounded canonical inputs. Composition: add_telescope lifts the
carry equations to scLimbs sum + 2^260*g5 = scVal a + scVal b;
canonicity (a,b < l < 2^253) forces g5 = 0; the trailing sub(sum, L)
goes through sub_val_spec with subtrahend L — enabled by weakening
sub_val_spec's hypothesis from scVal b < l to scVal b <= l (the
gamma5=1 forcing argument only needs <=), since scVal L = l exactly.
denote L = 0 in ZMod l closes it.
check-scalar.sh: ScalarAddSpec in manifest + audit (5/5 clean), button
green at the re-budgeted 300s/4096MB caps.
With sub (previous commit): the scalar layer's + and - are both fully
verified against dalek's own extraction. Remaining: x3 fork port,
Montgomery mul/reduce (kernel frontier).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
sub_val_spec closes the top-level two-clause value spec:
denote(Scalar52.sub a b) = denote(a) - denote(b) in ZMod l
for limb-bounded inputs with canonical subtrahend (scVal b < l).
Axiom-clean [propext, Classical.choice, Quot.sound]; no sorry.
The assembly documented-as-remaining last session is now done. Key resolutions:
- Applied the WP "spec_bind" rule manually instead of "step", and reduced the
resulting "let (difference,borrow) := (dw,w)" Prod-let with an explicit
"show" — this was the destructuring friction that blocked the earlier
attempt (step's arity heuristics mis-typed the pair result).
- Inlined the subtle "Choice::from" identity (no step-spec, like csel_step).
- PERFORMANCE: kept "scLimbs" as opaque atoms in the gamma5=1 derivation
instead of "unfold ... at *" — the unfold exploded omega with 2^52..2^260
coefficients and blew past 600s; atomic form proves in ~1 min (METHOD 4,
same kernel-cost discipline as the field layer).
- The 2^260 borrow-wrap and the +l conditional-add cancel in ZMod l:
beta5=0 direct; beta5=1 forces top carry gamma5=1 from scVal b < l, closed
by linear_combination over the two telescopes (sub_telescope, add_telescope).
check-scalar.sh: sub_val_spec in the manifest + Phase-3 audit (4/4 clean);
proof-phase caps raised to 600s/8192MB for the assembly; full button green.
exponentiation.threshold raised to 300 for the 2^260 literal.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
New in Proofs/ScalarSubSpec.lean (all axiom-clean [propext, Classical.choice,
Quot.sound], no sorry, no native_decide):
- nat_and_mask52 / nat_shift52 / nat_shift63 : 52/63-bit ops -> %,/
- sub_step_arith : isolated per-limb borrow accounting (tiny ℕ context,
correction-on-the-left so no truncated subtraction) — the METHOD-4
discipline that keeps 2^260-scale coefficients out of any one certificate
- sub_loop_spec : the FULL 5-limb borrow chain of Scalar52::sub, unrolled
via loop_step/range_next_*; wrapping_sub, 52-bit mask store, borrow-out
bit. This is the loop unroll that blocked the earlier attempt.
- csel_step : step-spec for the subtle conditional_select (faithful model)
- cond_add_l_zero_spec / cond_add_l_one_spec : BOTH cases of conditional
add-of-L, full carry chains; the condition-1 case steps the addend as a
clean value so the index_mut write-back matches sub_loop's pattern
- sub_telescope / add_telescope : the 2^52i-weighted value telescopes to
2^260, discharged by omega (no kernel-capacity blowup)
check-scalar.sh: ScalarSubSpec added to the compile manifest; Phase-3 axiom
audit extended to sub_loop_spec + cond_add_l_one_spec (3/3 clean). Full
button green.
Honest boundary: top-level sub_val_spec (⟦sub a b⟧ = ⟦a⟧-⟦b⟧ in ZMod ℓ)
is documented as remaining — every lemma it needs is proven; what's left is
the Aeneas binding-arity for destructuring sub_loop_spec's pair-valued
multi-existential postcondition inside the do-block, a mechanical not a
mathematical gap. No sorry shipped (Invariants H1/H4).
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>
extract-scalar.sh: function-level roots (add/sub/mul/square/montgomery_*)
yield a 28-def Scalar52 limb-arithmetic gen with ZERO iterator/byte/wrapper
entanglement — the byte-serialization and high-level Scalar wrapper (which
pull untranslatable chunks/zip iterators) are excluded by scoping, not faked.
Proofs/ScalarDenote.lean (compiles, axiom-clean): Ell = ℓ = 2^252+..., the
Scalar52 denotation ⟦·⟧ : Scalar52 → ZMod ℓ, the ScBnd 52-bit limb invariant,
and L_val — the transpiled constants::L denotes EXACTLY the group order ℓ
(kernel-checked, no native_decide).
add/sub (Range-loop conditional reductions, tractable — field-layer pattern)
and the Montgomery mul path (shares pasta's big-coefficient kernel limit) are
in progress. check-scalar.sh is green for the foundation.
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. check.sh gates: source integrity, stub audit, zero axiom
declarations under Proofs/, per-certificate axiom audit.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
