- 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 <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>
- 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>
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>
Replicates dalek's gen merge: extract.sh co-extracts the Scalar52 backend
and scalar::from_bytes_mod_order[_wide] into the CurveField model (with this
fork's sub::black_box opaqued, its identity model ported to the merged
FunsExternal), pins RUSTFLAGS --cfg curve25519_dalek_backend="serial" so
the SIMD dispatch arm compiles out (get_selected_backend becomes a real
definition), and upgrades unwrap_u8 to the documented Choice-model
definition. ScalarDenote repoints by one import line; both buttons green
over the merged gen (scalar chain + field/group/dsm chain, all certificates
axiom-clean).
Prepares the verify-glue integration (CurveSig) on this fork.
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>
extract.sh now opens crate::backend::serial::scalar_mul::vartime_double_base
(the other scalar_mul strategies stay opaque): non_adjacent_form (with its
loops), NafLookupTable5 (from/select), the curve-model helpers and
vartime_double_base::mul itself land in gen/CurveField - the same
namespace as the proven edwards operations, so the coming double-and-add
induction can consume EdDouble/EdAddProjNiels/EdConvert directly.
Zero sorries, zero external axioms (the pinned sources carry documented
compat refactors: single-assignment loop helpers, param-rooted while,
always-256-iterations, index-based LE load).
Full check.sh pressed fresh over the regenerated model: every existing
field and group-law certificate still green and axiom-clean - the scope
extension is purely additive.
The apex brick of the scalar layer: for any 64 bytes (the opaque SHA-512
digest), [from_bytes_wide bytes] = (LE 512-bit value) mod l, with
canonical 52-bit-bounded output. Composition: bytes_unpack_spec (8x8
loops) -> split_words_lo/hi_spec (exact div/mod per limb, disjoint ORs
as additions) -> wide_split_telescope (isolated omega) -> montgomery_mul
by R and RR (R cancels as a unit, RR restores it) -> the canonical add.
The two kernel-capacity walls found and crossed en route (control repo
FAILURES.md updated):
- a montgomery_mul inside any walk motive replays its 400-line body at
every kernel step (fix: named prefix functions in the pinned source);
- straight-line IndexMut closure chains make kernel defeq exponential in
depth (fix: struct-literal construction - the split halves now build
Scalar52([...]) directly). Full certificate: 77 s kernel-inclusive.
Regenerated gen (sources factor from_bytes_wide -> from_bytes_wide_parts
-> split_words_lo/hi; documented pure refactors, cargo-checked).
check-scalar.sh: 13 proof files, 13 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
Canonicity pass (the layer is now closed under its own preconditions):
- sub_val_spec post carries the exact value equation
(exists beta <= 1, scVal r + scVal b = scVal a + ell*beta, with the
underflow guard beta = 1 -> scVal a < scVal b)
- add/montgomery_reduce/mul/aggregate posts all carry scVal r < ell:
canonical inputs give canonical outputs everywhere. Needed because
from_bytes_wide (hash-to-scalar) feeds Montgomery outputs into add.
Hash-to-scalar foundation (toward Scalar::from_hash / EdDSA verify):
- extraction scope + from_bytes_wide (brings constants::R); regenerated gen
- source repos carry a documented Aeneas-compat patch: the bare
`hi[4] = words[7] >> 20` extracts ill-typed at pin bf13c42e; masked
(semantic no-op, words[7] >> 20 < 2^44)
- Proofs/ScalarWideSpec.lean: R constant lemmas (R = 2^260 mod ell,
witness 2^260 = R + 255*ell) and montgomery_mul_spec, the single
Montgomery round: [r]*2^260 = [a]*[b], canonical bounded output
check-scalar.sh: 10 proof files, 11 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.
- verification/extract-scalar.sh: function-level Charon/Aeneas extraction.
This fork (v4.1.3) inlines a local `black_box` (a volatile read used as an
optimization barrier) inside Scalar52::sub; charon cannot translate the
`&raw const` it lowers to, so it is marked --opaque and modeled below.
- verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (27 defs)
- verification/gen/CurveScalar/FunsExternal.lean: hand-written model of
Scalar52::sub::black_box as the identity on u64 (a volatile read returns
the value written; the qualifier is only an optimization barrier).
TypesExternal.lean is decl-free — this fork pulls in no external types
(unlike v5 dalek, which routes sub through subtle::Choice).
- verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
constants::L denotes exactly the group order ℓ, kernel-checked).
- verification/check-scalar.sh: guarded compile of the gen modules plus the
denotation foundation.
check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.
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>
