From 9da09026407cd394d00a1650c032dafecaf949c4 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 2 Jul 2026 17:23:44 +0200 Subject: [PATCH] pasta field WIP: add/const/reduce/mul spec drafts + memory-lean discharge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit AddSpec: sub_spec preconditions discharged by exact matches (the blanket simp[*] discharge here is what OOM-crashed the session — see formal-verification-control/POSTMORTEM-2026-07-02.md). ConstSpecs: R/R2/INV/ zero/one literal specs. ReduceSpec: full HAC 14.32 Montgomery accounting — per-round dropped-limb-is-zero facts from k = r·INV, exact t'·2^256 = t + m·p identity, composition with the general sub_spec reduction. MulSpec: 16-mac schoolbook accounting via zify + linear_combination (nonlinear cross-products are atoms), composed with montgomery_reduce_spec. DRAFTS: written against the generated code but not yet compiled; README carries an explicit construction note until check.sh goes green. Co-Authored-By: Claude Fable 5 --- README.md | 7 +++++++ verification/lean-guard | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 29de976..e2d43ca 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,13 @@ statements; this repository exists to do it properly.) ## Layer status +> **Construction note (2026-07-02):** the field layer is mid-build. PROVEN and +> compiled: PPallas (primality), Denote (Montgomery denotation), HelperSpecs +> (adc/sbb/mac), SubNegSpec (sub/neg). DRAFTED, awaiting compilation: +> AddSpec, ConstSpecs, ReduceSpec (Montgomery reduction), MulSpec. Not yet +> written: SquareSpec, InvertSpec, FieldMain (the certificate), check.sh. +> This note is removed when `verification/check.sh` goes green end-to-end. + | Layer | Certificate | Status | Axioms of certificate | |-------|-------------|--------|-----------------------| | Field 𝔽_p (Montgomery) | `fieldImplementation` | ⏳ in progress | — | diff --git a/verification/lean-guard b/verification/lean-guard index 256ef42..10a0af3 100755 --- a/verification/lean-guard +++ b/verification/lean-guard @@ -106,7 +106,7 @@ if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; # --scope runs the command as a child of THIS shell (env inherited), # merely placing it in a fresh cgroup with the hard caps below. systemd-run --user --scope --quiet \ - -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \ + -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \ -- taskset -c "$CORES" \ timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"