Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phase 1's anti-smuggling check reads source text. Measured today on Lean
v4.30.0-rc2, four distinct declarations compile cleanly and slip past its
anchored pattern:
` axiom cheat : ...` one leading space
`@[simp] axiom cheat : ...` line starts with the attribute
`unsafe axiom cheat : ...` `unsafe` absent from the modifier list
`axiom` <newline> ` cheat` no space follows the keyword
Any of them yields a repository that proves False while the button prints
ALL GREEN. Only the tab variant is blocked, and by Lean, not by us.
Hardening the pattern would fix the exhibited syntax rather than the class,
which is the mistake this estate has made before. Phase 2b stops parsing text
and asks the kernel instead: it reads every compiled Proofs/*.olean with
readModuleData and rejects any declaration that is an axiom.
Design notes:
- reads compiled artifacts rather than importing the modules, because
Proofs.Basic and Proofs.ConstSpecs deliberately reuse `zero_spec` and a
whole-corpus import is impossible by construction;
- membership is self-deriving from the filesystem, so Scalar* and
AxiomCheck are covered too — both are skipped by the CERTS audit and by
the dead-file gate;
- fails closed on absence: a missing .olean would make the scan vacuous, so
the count of compiled modules must equal the count of shipped sources;
- removes its temp source AND artifact on both paths, since a bare `rm`
after the call never runs under `set -e` when the gate goes red — exactly
how this repo accumulated 101 orphan .olean files;
- ~3 s for the whole corpus, against ~53 s for one module-importing run.
Phase 1's grep stays as a fast first line of defence. Phase 2b is the gate
that is load-bearing.
selftest-axgate.sh attacks the shipping gate, lifted out of check.sh at run
time rather than copied. It asserts the specific diagnostic, so a rejection
for an unrelated reason fails too, and it was itself negative-tested: with
the gate's throwError removed, the self-test goes red on exactly that case.
No proof, statement, specification or certificate is touched. No attested
commit is altered — the log binds specific commit hashes, all of which remain
ancestors of HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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>
- 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)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
kernel-audited)
Proofs/FromBytesSpec.lean: FieldElement51::from_bytes is exact below bit
255 - for any 32 input bytes it succeeds with 51-bit limbs denoting
bytesVal b mod 2^255 (the sign bit is discarded, everything else is the
little-endian value). This is the y-parse of decompression: a canonical
encoding parses to exactly its y-residue.
- load8_at_spec: generic 8-byte little-endian loader (the disjoint-OR
idiom with the product-order-robust or_add_low helper; per-round clear
hygiene cured a fat-context elaboration timeout).
- window_extract / window_shift / digits_tile: the pure window algebra -
five 64-bit windows at byte offsets 0/6/12/19/24, shifted 0/3/6/1/12,
tile bits 0..254 exactly (base-2^51 digit identity).
- from_bytes_spec: the walk composing them; the five window equations
come from ring-verified low/window/high decompositions of the byte sum.
Certificate exact standard three; full button green fresh. Next:
decompress_of_canonical (step 3/5).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(sqrt_ratio_i_sq_spec, kernel-audited)
The largest single proof of the decompress chain: for square u/v
(witness x, v nonzero), the extracted sqrt_ratio_i returns choice 1 and
the even-parity root - Bnd r (2^52), r^2 * v = u, r's canonical residue
even. The walk composes every previously certified piece: the
square/mul/pow_p58 candidate chain, sqrt_m1_spec, fe_ct_eq_spec x3 (the
three constant-time residue checks), neg_spec, the Choice bitor, and
fe_cond_assign_spec twice (root flip by sqrt(-1), then sign
normalization via is_negative).
Case analysis: sqrt_core's disjunction (v*r^2 = +/-u) against the check
flags - u = 0 collapses everything to the zero root; u != 0 with
v*r^2 = u kills both flip flags (u = -u forces u = 0 in odd
characteristic; u = -u*i forces u*(1+i) = 0 with 1+i nonzero); with
v*r^2 = -u the flip fires and (i*r)^2 * v = -(-u) = u. Parity: the odd-
prime negation flip (ZMod.neg_val), zero-root edge included. New
helpers: eq_neg_self_iff_zero, one_add_i_ne_zero.
Certificate exact standard three; full button green fresh. Remaining:
from_bytes walk, decompress_of_canonical, replication, pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(kernel-audited)
- fe_cond_assign_spec: the per-limb constant-time selection on field
elements (real extracted code: five index_mut rounds over the u64
select) keeps self iff the choice is 0 - the operation sqrt_ratio_i
uses for both the root flip and the sign normalization. Walked with
backfun-rewrite hygiene; the u64 model lemma restated locally
(Proofs.Basic is a parallel root that clashes with ConstSpecs).
- sqrt_core: THE ALGEBRAIC HEART - for square u/v (witness x, v nonzero)
the candidate r = (u*v^3)*(u*v^7)^((p-5)/8) satisfies v*r^2 = +/-u.
The v-part of the exponent collapses by Fermat (8*(2^253-5) = 2(p-1));
the residual x^((p-1)/2) is +/-1 by factoring its square. Exponent
bookkeeping: (p-5)/8 = 2^252-3, (p-1)/2 = 2^254-10, all closed by
norm_num after pow_mul merges.
Both certificates exact standard three. Full button green fresh.
Remaining: the sqrt_ratio_i walk composing these, from_bytes,
decompress_of_canonical.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Proofs/DecompressSpec.lean, the arithmetic ingredients of sqrt_ratio_i:
- pow_p58_spec: a^((p-5)/8) = a^(2^252 - 3) via the pow22501 chain (the
invert_spec pattern).
- fe_ct_eq_spec: the constant-time field comparison DECIDES denotational
equality - because to_bytes is canonical (to_bytes_spec), byte equality
is residue equality in both directions. Supporting bridge lemmas:
bytesVal_inj (little-endian digits are unique, so value equality forces
list equality), bytesVal_congr, bytes_eq_iff_denote.
- sqrt(-1) needs no new work: ConstSpecs.sqrt_m1_spec (the constants
campaign) already pins SQRT_M1 to Bnd + denote*denote = -1.
Both new certificates exact standard three; full button green fresh.
Remaining in the chain: the sqrt_ratio_i success-case walk, from_bytes,
decompress_of_canonical.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
button-enforced (phase-2 goal reached on dalek)
CurveFieldProofs.verify_accepts_iff_point_eq: under the half-lift's
hypotheses, for ANY valid on-curve point Q whose canonical encoding is
the signature's R bytes,
verifier accepts <=> Q = [k]*(-A) + [s]*B (as denoted points)
- the literal point-level EdDSA verification equation, no decompress
needed: the canonical encoding is INJECTIVE on curve points.
Proofs/PointEqSpec.lean:
- one_add_d_y_sq_ne_zero: 1 + d*y^2 never vanishes - d nonsquare
(edD_not_square, the completeness ingredient doing its second job)
vs -1 a square (p = 1 mod 4).
- x_sq_of_onCurve + enc_inj_coord: the curve equation determines x^2
from y; +/-x have different parities mod an odd prime unless x = 0,
so y-residue + parity bit determine the point.
- enc_point_inj (standard three axioms): equal canonical encodings of
valid on-curve points force equal denoted points.
- verify_accepts_iff_point_eq: half-lift + injectivity. Axiom cone
EXACTLY the apex boundary; Phase 3b now enforces all THREE tiers
(byte apex, half-lift, point equation).
Remaining phase-2 garnish: the constructive decompress specs (sqrt
chain), giving "the accepted bytes decompress to the recomputed point".
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
extract.sh drops --opaque crate::edwards::decompress: step_1/step_2,
sqrt_ratio_i, pow_p58, and FieldElement51::from_bytes now extract as real
code (source aa0f6ab patches step_2's conditional_negate to the documented
negate-then-conditional-assign - the ConditionallyNegatable blanket impl
is the one thing the toolchain cannot translate). No new axioms: the
slice-level ct_eq the sqrt check needs was already a real def. Full
button green on the regenerated universe.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
THE THEOREM (CurveFieldProofs.verify_accepts_iff_point): for a parsing
signature, a valid on-curve public-key point, a canonical signature
scalar, and a successful recompute, there is a point R' - the certified
[k](-A) + [s]B, ExtValid and on-curve - with
verifier accepts <=> bytesVal R_bytes
= (edY R').val + ((edX R').val % 2) * 2^255
The apex's byte-for-byte comparison IS point-encoding equality: the
signature's R bytes are accepted exactly when they are THE canonical
encoding of the recomputed point. Axiom cone: EXACTLY the apex boundary
(SHA-512 oracle + wire-format opaques; zero curve/scalar/backend axioms),
now enforced for BOTH apex and half-lift by check.sh Phase 3b.
New machinery in Proofs/PointLiftSpec.lean:
- bind_ok_inv: generic ok-inversion of one monadic bind - the clean way
to invert oracle-bearing chains (axioms cannot be walked).
- recompute_inv: names the recompute chain's intermediates (hash, k,
-A, R') with their defining equations, via eight flat bind_ok_inv
steps after the pass-through reductions.
- Bytes64.exists_bytes + List.exists_len32: the 64-byte destructure -
Lean's match refuses list patterns beyond ~32 elements, so the device
is a 32-cons prefix + a list-level 32-destructure on the tail.
- The assembly: recompute_inv + from_bytes_mod_order_wide_spec (k
canonical) + edwards_neg_law (-A) + vartime_dsm_basepoint_spec (R',
valid, on-curve) + ed_compress_spec (er = canonical encoding) +
rangeEq_iff_bytesVal (byte comparison = value equality), threaded
through the ok-injectivity of the inverted equations.
Full button green fresh, incl. the extended Phase 3b.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
bridge (Proofs/PointLiftSpec.lean, kernel-audited)
- vartime_dsm_basepoint_spec: the PUBLIC dsm entry the verifier calls
(EdwardsPoint::vartime_double_scalar_mul_basepoint) satisfies the dsm
certificate - under the serial pin the backend dispatch is the real
constant Serial, so the wrapper reduces definitionally to the certified
serial path. No new axioms; in CERTS.
- rangeEq_iff_bytesVal: the verifier's byte-wise comparison IS value
equality of the encodings - little-endian digits are unique (32-fold
byte peel, one omega over the flat bound set; U8 equality recovered via
UScalar.eq_of_val_eq).
With ed_compress_spec and from_bytes_mod_order_wide_spec already landed,
the half-lift now needs only the recompute bind-chain inversion (the sha
calls are oracles - inverted from the hrec hypothesis the apex carries)
and the assembly theorem. Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
(from_bytes_mod_order_wide_spec, kernel-audited)
Proofs/ScalarPackSpec.lean:
- scalar52_to_bytes_spec: Scalar52::to_bytes (the PACK step - pure
bit-packing at radix 2^52, no reduction) serializes canonical limbs to
exactly their value: bytesVal s = scVal a. Second application of the
ToBytesSpec walk generator; boundary bytes 6 and 19 only (the two
non-byte-aligned 52j offsets), disjoint ORs to additions as before.
- from_bytes_mod_order_wide_spec: the verifier's k = SHA-512-to-scalar
entry composes from_bytes_wide_spec (the proven mod-l reduction) with
the pack: for 64 input bytes of value T, the returned Scalar's 32
bytes denote V with V < l and V = T (mod l) - precisely the scalar
premises vartime_double_base_mul_spec consumes (V < l < 2^253).
- byte_split_52_4: the offset-4 chunk split for 52-bit limbs; the five
ToBytesMath byte_split_* lemmas shed their unused 2^51 premises (pure
telescopes, valid for all f).
Both certificates exact-standard-three. Full button green fresh.
Half-lift remaining (mapped in memory): dsm dispatch wrapper, recompute
bind-chain inversion, bytesVal injectivity, assembly in PointLiftSpec.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
encoding of the denoted affine point (kernel-audited)
CurveFieldProofs.ed_compress_spec: for any valid extended point Pt
(ExtValid - the invariant every certified curve op guarantees),
compress Pt = ok s with
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255
- the 32 wire bytes are the canonical little-endian y-residue with the
x-parity bit at position 255. Compress semantics AND canonicity in one
statement, because to_bytes_spec pins the bytes to the residue itself.
Supporting certificates in Proofs/CompressSpec.lean:
- is_negative_spec: the sign read is the parity of the CANONICAL residue
(bit 0 of to_bytes) - (feVal x mod p) mod 2.
- Bytes32.exists_bytes: the 32-byte destructuring device (the
Fe.exists_limbs idiom, 32-wide).
- to_bytes_spec': premise-free restatement of the canonicity brick.
- xor_top_bit (ToBytesMath): setting a clear top bit by XOR is addition -
proven from xor_div_two_pow + and_xor_distrib_right, no bit-blasting.
The chain is entirely certified code: invert (Fermat), two muls, to_bytes
(canonicity), is_negative, and the sign-bit XOR. Axiom cone of
ed_compress_spec: exactly [propext, Classical.choice, Quot.sound].
check.sh: CompressSpec in PROOFS, ed_compress_spec in CERTS - full button
green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The load-bearing brick of the point-level apex equation:
FieldElement51::to_bytes always succeeds and its 32 output bytes denote
EXACTLY the represented residue - bytesVal s = feVal a mod p. Since the
canonical residue determines the bytes, this is simultaneously
canonicity ("output is the canonical encoding") and the injectivity
compress needs ("equal residues iff equal bytes").
- Proofs/ToBytesMath.lean: the context-free ℕ mathematics (METHOD 4) -
the 5-rung carry telescope (div_rung/q_telescope), the q-trick facts
(q = (h+19)/2^255 is a bit, fires iff h >= p), q_mod_p (adding 19q and
discarding bit 255 subtracts pq exactly), carry_pack (the masked-limb
assembly mod 2^255), five per-limb byte-chunk splits, and bytes_pack
(the 32-byte little-endian reassembly, closed by one zify +
linear_combination over the five splits).
- Proofs/ToBytesSpec.lean: the symbolic execution - at ~150 machine ops
the longest walk in the repo, loop-free: weak reduce (reduce_spec),
the q pass, the fold + carry pass, 32 byte extractions (the four
limb-boundary bytes turn disjoint ORs into additions via
Nat.two_pow_add_eq_or_of_lt), and the trailing top-bit debug-assert
DISCHARGED (b31 = f4/2^44 < 2^7), not assumed.
- check.sh: ToBytesMath/ToBytesSpec in PROOFS, to_bytes_spec in CERTS
(exact standard-three audit) - full button green fresh.
Walk lessons (for the control repo, next push): rw index-equations into
their consumers instead of subst (subst eliminates the wrong side or
dies on dependent do-motives); never rw [Nat.mod_eq_of_lt (by omega)]
(metavariable goal reaches omega) - state the bound with show.
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>
The verify-glue extraction (charon on the vendored ed25519-dalek with the
SHA-512/wire-format opaque boundary) is now stanza [3/4]-[4/4] of the one
extraction script, not an ad-hoc step. Regenerated artifacts identical.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
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>
- `Proofs/DsmNafLoadSpec.lean` (generated) — the byte-to-word LE load of
`non_adjacent_form`: four 8-peel inner walks (t |= bytes[8k+bi] << 8bi)
and the outer 4-peel filling x_u64[0..3]; x_u64[4] stays 0 (the pad word
the cross-word window reads at positions >= 251).
- `Proofs/DsmNafMath.lean` — the pure arithmetic of the w=5 digit loop:
`nafSum`/`nafSum_set`; window-read lemmas `naf_window_single` /
`naf_window_cross` (cross-word disjoint-OR read sees (V >> pos) mod 32);
invariant steps `naf_even_step` / `naf_odd_step` (Nat.mod_mul telescope:
digit + promoted carry reconstruct the consumed bits EXACTLY, in ZZ);
carry-kill `naf_carry_even` / `naf_carry_odd` (V < 2^253 forces the
carry dead before bit 256); `naf_exit` (nafSum naf 256 = V exactly).
The digit-loop walk (stage 3) composes these next; its invariant is
nafSum naf 256 + carry*2^pos = V mod 2^pos
with digits at k >= pos all zero and carry = 1 -> pos <= 254.
CERTS += naf_load_spec, naf_window_cross, naf_exit (axiom-clean).
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>
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.
Toward Scalar::from_hash: bytes_unpack_spec proves the from_bytes_wide
word-unpack loops pack 64 little-endian bytes into 8 words exactly.
- Proofs/ScalarBytesSpec.lean (3308 lines): bytes_word_loop_spec_0..7,
each split head/tail at j=4 (the 8-fold monolith grows exponentially
in elaboration - METHOD 4). Disjoint-bit ORs become additions via
core's Nat.two_pow_add_eq_or_of_lt with explicit calc bridges (the
default simp set literalizes 2^8 -> 256 and breaks pow-form rewrites;
simp only everywhere).
- Proofs/ScalarUnpackSpec.lean: bytes_unpack_spec composes the eight
inner lemmas through the outer loop (iterator start needs a term-level
equality rewrite per peel).
The from_bytes_wide main walk itself is proven at elaboration level
(fail-probe verified end to end) but its single-decl kernel certificate
replays >30min; it ships next as a phase-split (plan in the control
repo's method notes). check-scalar.sh: 12 proof files, 12 kernel audits,
all exactly [propext, Classical.choice, Quot.sound]. Button 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.
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/ScalarMulSpec.lean (axiom-clean, no sorry):
- m_spec: the widening 52x52->104-bit product helper — total, exact
- mul_internal_spec: all NINE schoolbook column sums proven exact
(z_k = sum_{i+j=k} a_i*b_j) and bounded (each product < 2^104, each
column < 2^107) through the 60-step straight-line extraction
This is the half of Scalar52::mul that the kernel-capacity frontier does
NOT touch. Phase B — montgomery_reduce (74 steps, part1/part2, the
Montgomery invariant result = input * R^{-1} mod l with R = 2^260, and
the double-round composition through RR) — remains the open frontier,
now precisely one function wide.
check-scalar.sh: ScalarMulSpec in manifest + audit (6/6 clean), green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
check-scalar.sh proofs phase back to 300s/4096MB: the sub_val_spec
assembly's true peak is 753MB after the atomic-scLimbs fix — the 8192 cap
was inflation left over from the slow draft and caused the 2026-07-03
swap-pressure incident (see control repo FAILURES.md). lean-guard updated
to master with Guard 3b. Button green at the honest budget, 4/4 audits.
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>
Reusable infrastructure for the scalar Range-loop reductions (sub_loop,
add_loop, conditional_add_l). Re-stated standalone so scalar proofs stay
independent of the field gen tree. Compiles axiom-clean.
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>
