2026-07-02 19:13:43 +00:00
|
|
|
|
#!/usr/bin/env bash
|
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
|
|
|
|
# Scalar-layer check (Scalar52 arithmetic mod ℓ) — the layer is COMPLETE:
|
|
|
|
|
|
# add, sub, Montgomery mul, and the byte-parsing chain, all kernel-audited.
|
|
|
|
|
|
# Runs against the merged gen/CurveField universe (the scalar module lives
|
|
|
|
|
|
# there since the merge; see extract.sh). Guarded compiles throughout.
|
2026-07-02 19:13:43 +00:00
|
|
|
|
set -uo pipefail
|
|
|
|
|
|
source ~/aeneas-toolchain/env.sh
|
|
|
|
|
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
|
|
|
|
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
Merge scalar into CurveField; integrate the verify glue against the model
Gen merge: extract.sh now co-extracts the Scalar52 backend and the public
scalar::from_bytes_mod_order[_wide] conversions into the SAME CurveField
model, so the whole library — field, curve_models, edwards, scalar — shares
one type universe (Scalar is a single structure, not two). The scalar proof
chain repoints by one import line (ScalarDenote: CurveScalar.Funs ->
CurveField.Funs); check-scalar.sh's gen list follows. Both buttons — the
scalar certificates and the field/group/dsm certificates — pass fresh over
the merged gen, so the merge is proven-safe, not merely hoped-safe.
Verify glue (gen/CurveSig): the extracted ed25519-dalek verify_sha512 path,
integrated against the proven model:
- TypesExternal.lean imports CurveField.Types, so CompressedEdwardsY /
EdwardsPoint / Scalar in the glue ARE the proven model's types. Only the
genuinely foreign types stay opaque: sha2.Sha512, ed25519.Signature,
signature.error.Error.
- FunsExternal.lean imports CurveField.Funs, so every curve/scalar call
(compress, vartime_double_scalar_mul_basepoint, as_bytes, neg,
from_bytes_mod_order[_wide]) resolves to a proven definition — no axioms.
The `?`-operator plumbing (Try::branch, FromResidual::from_residual) and
compressed_from_bytes get real definitions. Only the SHA-512 hasher
(sha512_new/update/finalize_bytes) and two opaque wire accessors
(Signature.to_bytes, Error.new) remain axiomatized — the deliberate,
documented hash-oracle boundary.
Audited: `verify_sha512`'s entire axiom cone is
[propext, Classical.choice, Quot.sound,
sha2.Sha512, sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error.new]
— zero curve axioms, zero scalar axioms. The verify path is definitionally
grounded in the certified model; the only trust boundary is SHA-512.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 16:13:58 +00:00
|
|
|
|
GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs) # MERGED GEN: scalar module now lives in CurveField
|
2026-07-04 08:31:32 +00:00
|
|
|
|
PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec)
|
2026-07-02 19:13:43 +00:00
|
|
|
|
|
|
|
|
|
|
echo "=== stub/axiom audit ==="
|
|
|
|
|
|
grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }
|
|
|
|
|
|
echo " clean"
|
|
|
|
|
|
echo "=== compile (guarded) ==="
|
|
|
|
|
|
cd "$AENEAS_LEAN"
|
|
|
|
|
|
lake env bash -c "
|
|
|
|
|
|
set -uo pipefail
|
|
|
|
|
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
|
|
|
|
|
for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
|
|
|
|
|
|
cd '$HERE'
|
2026-07-03 15:51:14 +00:00
|
|
|
|
for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
|
2026-07-02 19:13:43 +00:00
|
|
|
|
" || { echo FAIL; exit 1; }
|
2026-07-03 10:54:26 +00:00
|
|
|
|
echo "=== Phase 3: axiom audit (kernel-level) ==="
|
|
|
|
|
|
cd "$AENEAS_LEAN"
|
|
|
|
|
|
lake env bash -c "
|
|
|
|
|
|
set -uo pipefail
|
|
|
|
|
|
export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
|
|
|
|
|
|
cd '$HERE'
|
|
|
|
|
|
AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
|
2026-07-04 08:31:32 +00:00
|
|
|
|
{ echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarWideSpec'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarFromBytesSpec'; echo '#print axioms ScalarProofs.L_val'
|
scalar layer: prove Scalar52::sub borrow + conditional-add-L carry chains
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>
2026-07-03 14:26:24 +00:00
|
|
|
|
echo '#print axioms ScalarProofs.sub_loop_spec'
|
Scalar layer complete: Montgomery reduction + full mul proven, scalarImplementation aggregate
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.
2026-07-03 19:06:15 +00:00
|
|
|
|
echo '#print axioms ScalarProofs.cond_add_l_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_spec'
|
2026-07-04 08:31:32 +00:00
|
|
|
|
echo '#print axioms ScalarProofs.part1_spec'; echo '#print axioms ScalarProofs.montgomery_reduce_spec'; echo '#print axioms ScalarProofs.mul_spec'; echo '#print axioms ScalarProofs.scalarImplementation'; echo '#print axioms ScalarProofs.montgomery_mul_spec'; echo '#print axioms ScalarProofs.bytes_unpack_spec'; echo '#print axioms ScalarProofs.from_bytes_wide_spec'; } > \"\$AUD\"
|
2026-07-03 10:54:26 +00:00
|
|
|
|
OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
|
|
|
|
|
|
echo \"\$OUT\"
|
|
|
|
|
|
rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
|
scalar layer: prove Scalar52::sub borrow + conditional-add-L carry chains
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>
2026-07-03 14:26:24 +00:00
|
|
|
|
N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true)
|
2026-07-04 08:31:32 +00:00
|
|
|
|
[ \"\$N\" -eq 13 ] || { echo \"AXIOM AUDIT FAILED: \$N/13 clean\"; exit 1; }
|
2026-07-03 10:54:26 +00:00
|
|
|
|
" || { echo FAIL; exit 1; }
|
|
|
|
|
|
echo " L_val axiom-clean"
|
|
|
|
|
|
|
2026-07-02 19:13:43 +00:00
|
|
|
|
echo ""
|
Scalar layer complete: Montgomery reduction + full mul proven, scalarImplementation aggregate
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.
2026-07-03 19:06:15 +00:00
|
|
|
|
echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round through RR) proven mod ℓ; aggregate certificate scalarImplementation kernel-audited."
|