Repository navigation
Parallelize EasyCrypt split replay with isolated caches and exact coverage #768
Description
The full EasyCrypt split gate currently runs 438 direct targets, 438 CLI targets and 411 controls serially. A clean local replay on 2026-09-29 took 11,843.585 active seconds (3 h 17 min 24 s), source d03db3d, published in PR #757. The session exceeded six hours because upstream pinned Rust source changes required a second replay.
The owner requested throughput optimization before continuing EasyCrypt research. Current scope is bounded profiling and an isolated-worker comparison on master 10dfb47. This is exploratory timing evidence, not a replacement gate.
Implementation acceptance criteria:
- Preserve all direct and CLI targets, every declared control and all existing static/identity/requirability checks.
- Use bounded concurrency with separate writable caches; no shared-tree parallel EasyCrypt processes or stale/prebuilt-only acceptance.
- Preserve the existing per-driver solver options and exact expected control rejection reasons.
- Reject missing/duplicate jobs, worker errors/timeouts, CLI diagnostics and inventory drift; retain per-task timing/log receipts.
- Measure a complete replay on the selected worker configuration before claiming an end-to-end speedup.
- Batch proof work and integrate relevant upstream changes before freezing; reuse evidence only where the covered input identities are unchanged.
Review at the combined implementation boundary under the project workflow; broader assurance sweep remains deferred under #509. Research tasks #100 and #295 remain separate from this execution optimization.
Activity
Nicola-Ceornea commentedon Sep 29, 2026
Bounded Phase-A measurement completed on master
10dfb47c75252cc5a95fa1b9619fcd05d7763d88with the pinned EasyCrypt image and unchanged solver arguments:Measured sample speedup: 3.04x, about 67.1% less elapsed time. Command arguments, exit codes, CLI diagnostics and prompt counts agreed across arms; no task timed out. Every worker started in a separate disposable tree without project
.ecofiles. The sample covers four proof files under both drivers and eight positive/negative controls. Negative outcomes matched their declared reasons.This is one paired feasibility sample, not a full-suite performance or verification receipt. The large FORS_ES/WOTS_TW_ES tasks were not sampled; OS-cache/thermal effects were not controlled. The authoritative gate has not been changed. Full equivalent replay and fail-closed scheduler controls remain prerequisites for adopting parallel execution.
Local reproducible artifacts:
/home/nicola/.local/state/pqsigner-research/easycrypt-performance-20260929/(README, script, source identity, commands, raw logs and individual results). All 1466 snapshot Git blobs were checked unchanged. Canonical working-tree status was preserved.Recommended next slice: bounded four-worker scheduling with isolated caches, exact task coverage/failure aggregation and per-task timings, followed by one complete replay and the combined bounded merge review.
Nicola-Ceornea commentedon Sep 29, 2026
Owner requested more aggressive scaling and one Opus 5.5 consultation. Phase A continues at clean snapshot
10dfb47c75252cc5a95fa1b9619fcd05d7763d88.Artifacts and detached final-report writer:
/home/nicola/.local/state/pqsigner-research/easycrypt-performance-20260929/scale-01/.receipt-design.mddefines the proposed invalidation and composition rules;opus-reconciliation.mddistinguishes confirmed facts from speculative claims.comparison.jsonandREADME.mdwill be produced automatically when the remaining arms finish. Laptop power settings and authoritative proof/gate sources remain unchanged.Nicola-Ceornea commentedon Sep 30, 2026
The owner requested higher measurement limits and further throughput investigation. New detached run:
scale-02, same clean source10dfb47c75252cc5a95fa1b9619fcd05d7763d88, same pinned EasyCrypt image and same 40-task set, configuration order 4/8/12.compile -tstats stats/<job>.txtinstrumentation across all arms. The completion writer aggregates exact outcome comparisons and top commands. EasyCrypt itself uses wall time for command statistics, so an arm containing suspension is explicitly marked unsuitable for hotspot selection; proof task/arm deadlines remain active-time based.cli -iterate -pragmas silent) reduced WOTS_C_Interactive from a mean 40.132s to 35.023s (12.7% less time). Two successful runs per setting, all with 744 commands and no diagnostics. A deliberately invalid proof preserved the exact rejection diagnostics and command count in both settings. The pinned tool source shows this pragma changes only goal display, not proof-checking mode. This is a limited experiment, not a full-gate equivalence claim.Other selected opportunities remain measured longest-first scheduling and separating proof replay evidence from fresh Rust correspondence checks. No proof weakening or solver-budget reduction is proposed.
Artifacts:
/home/nicola/.local/state/pqsigner-research/easycrypt-performance-20260929/scale-02/. Liveprogress.json; finalcomparison.json,hotspots.jsonandREADME.md; CLI A/B evidence inquiet-probe/result.json. Raw logs and launch/source identities are retained. The observer never stops or restarts proof processes.Nicola-Ceornea commentedon Sep 30, 2026
The expanded 40-task benchmark is complete: 4 workers matched 40/40 in 24m24s; 8 matched 40/40 in 22m19s; 12 matched 39/40 in 26m32s. No outer benchmark timeouts occurred. This remains a partial experiment, not a full-gate receipt.
The 12-worker failure starts at
cdrafts-split/GprocT1Opre.ec:1630,by apply htwsc; smt(ge2_t).; the other 426 CLI diagnostics cascade from that unfinished proof. An unchanged, cold, isolated full-file CLI replay passed in 118.207 s with 880 prompts and a log hash identical to the successful 4/8-worker runs.Diagnostic SMT capture isolates the flattened-index range bound. The default three-second CLI solver budget first fails on a small task, then expands to a ~1.52 MB Why3 task. Replaying its identical native query with the pinned solvers gave Alt-Ergo
Validat 1.0877 s before load, timeouts in 8/12 simultaneous copies at the unchanged three-second limit, andValidat 1.2058 s after load. Z3/CVC4 did not supply an alternative successful result. Five direct CVC4 calls required the diagnostic outer bound; direct replay omits the normal Why3 watchdog, so that does not establish original gate termination behavior.This reproduces a load-sensitive SMT timeout mechanism, the supported explanation of the observed failure. The original run lacks individual prover answers, so its exact scheduling/iteration history remains unreconstructed. Affinity-only contention in the EasyCrypt state did not fail. No theorem refutation or cache corruption was observed.
An extra arithmetic SMT hint still enters the expensive fallback, so it is not a demonstrated robustness fix. Next: explicitly prove the flattened-index bounds, then validate it together with the parallel runner. Keep 12 workers unvalidated; do not raise global solver budgets or relax CLI diagnostics.
No authoritative source/gate changes. Source remains
10dfb47c75252cc5a95fa1b9619fcd05d7763d88. Local complete evidence:/home/nicola/.local/state/pqsigner-research/easycrypt-performance-20260929/failure-diagnosis-01/diagnosis.txtanddiagnosis.json; raw receipts, excluded setup attempts and inputs are retained alongside them. No diagnosis jobs remain running.Nicola-Ceornea commentedon Sep 30, 2026
The observed load-sensitive proof corrections are now published in draft PR #769, commit
6dfa891e98961d24744fbbd7c23c3c6062a9981a(tree871cedd5f52aff16252fa071ccf919345cda2bda). Opus 5.5 was consulted before implementation. The patch replaces SMT search with explicit existing arithmetic lemmas in two proof bodies:flat_decompandt1_win. Statements, assumptions, toolchain, solver budgets and gate inventories are unchanged.The first repair exposed earlier unchanged quotient-bound failures under twelve-worker load. Those related steps were included in the same implementation batch before freezing. On the final candidate, two cold isolated twelve-worker partial CLI rounds through
t1_winpassed 24/24 with zero diagnostics (29.56 and 47.79 seconds). Cold whole-file compile and CLI also passed (165.09 and 111.25 seconds). The replacement blocks make zero SMT calls in focused traces; five targeted negative variants fail at the intended proof steps. These are focused measurements, not an end-to-end gate speedup.Astra and Opus 5.5 both returned GO in one simultaneous bounded review, with no findings. The unchanged full serial gate is running on the frozen candidate; PR #769 stays draft and master is unchanged until it passes. Its required inventory remains 438 direct targets, 438 CLI targets and 411 controls, plus the existing static/toolchain/source/canary checks.
This issue stays open for the isolated parallel runner and full mixed-workload/full-gate measurements. The later same-shaped
htwscproof and adjacenthxsautomation are profiling candidates, not confirmed defects or extra work in this merge batch. Proof/Rust evidence separation is also still future work. The combined owner-triggered assurance sweep remains deferred under #509.Nicola-Ceornea commentedon Sep 30, 2026
Research update, 2026-09-30: the proof reliability prerequisite is landed in #769 at
7bacd8dd46405462d13ed8160a77def98b6d77d1. All 15 CI checks passed, resolving the final review’s sole pending-CI gap. Its full split replay passed 438 direct / 438 CLI / 411 controls in 3h19m49s active time. That replay was still serial; the production parallel runner remains unimplemented and this issue stays open.The larger 40-task benchmark predates the proof repairs:
Four to eight workers saved only 8.6% elapsed time while using about 40% more CPU. Twelve was slower. The repaired-prefix stress test later passed 24/24 at twelve workers, but does not establish complete-suite reliability there.
Concrete bottlenecks and opportunities:
XmssmtCC_All.eccompile took 18m09s / 22m19s / 26m32s at 4/8/12 workers. At four workers its compile and CLI jobs started 5m52s and 7m18s into the run. A longest-job-first simulation using fixed observed durations gives 19m55s for the four-worker sample instead of 24m24s. This is a scheduling model, not a measured speedup; changed concurrency/cache behavior and production phase barriers matter.WOTS_C_Interactive; output shrank 2,036,107 -> 11,742 bytes, with the same 744 prompts. The small rejecting fixture retained its diagnostics. Pinned source confirmssilentchanges goal printing independently of proof-check mode. Whole-gate benefit remains unmeasured.GprocT1Opre.ec:3788takes 74.65s of its 165.09s compile. The twoXmssmtCC_All.eccommands at 6777/8014 took 78.49s/77.97s in the four-worker profile. These are specific targets for simpler proof steps or smaller SMT contexts, preserving statements and assumptions.New source-verified toolchain finding: our pinned EasyCrypt r2026.02 declares
-serverbut reads the different option keywhy3server. A tiny local proof with-serverpointing to a unique nonexistent socket still succeeded, confirming the option is ignored. The mismatch also appears in upstream main fetched today. A shared Why3 solver scheduler is therefore not a usable one-flag optimization on this image; it needs a deliberate toolchain correction and validation. Why3 1.8.2 itself supports a shared queue and global process cap, with process CPU limits applied when the solver starts. Keep this as a later candidate.Also reproduced the
.ecocaveat:compile -no-ecostill reads a matching existing cache and exits before producing command timings. It prevents writing in that code path, not reading. Native cache artifacts are insufficient as our authoritative evidence receipts. Cold comparisons need explicit private-cache handling.Recommended bounded next batch:
Fast runner/evidence acceptance tests first, a bounded slow-file comparison next, then one complete cold replay of the selected implementation and the combined owner-configured review boundary. Missing/duplicate tasks, worker failure, truncated/empty CLI output, unexpected control reasons and identity drift must all reject. A sub-hour cold replay is an engineering target, not measured performance. No production gate or solver options were changed for this research.
Primary sources:
src/server/README.serverandserver-unix.c.Local full research report and reproducible evidence:
/home/nicola/.local/state/pqsigner-research/easycrypt-performance-20260929/research-20260930/research.txt,performance-analysis.json,server-option-smoke.json,eco-smoke.json, andmanifest.json. Upstream pinned source files were fetched via GitHub API and matched the installed container source byte-for-byte. Prior timing receipts remain underscale-02/andrange-fix-01/. This is Phase A/B throughput work; the broader #509 assurance sweep remains deferred.feat(easycrypt): run the split gate's proof jobs in parallel (#768)
Nicola-Ceornea commentedon Oct 6, 2026
Reviewed the EasyCrypt changes landed September 30–October 6. Private parallel workers, exact coverage, serial rechecks, isolated budget-sensitive controls and deterministic replacements for the slow/load-sensitive SMT steps are already on master. The October 2/3 complete receipt is approximately one hour; the later
752436f6bb497485fe11226b2fd47aebreceipt matches current master proof inputs and has all 438 compile checks, 438 CLI checks and 411 controls green with no serial retries. Its long wall interval is not treated as active runtime.Follow-up draft PR #782 (
ced1ba009fc61ce3c9390e8a3825d5804cdb9b43) enables quiet goal rendering for both CLI paths. All 37 contract/runner regressions and source/statement pins pass. Pinned-image input probes preserve diagnostics, exit status and prompt counts. A one-file ABBA comparison averages 41.60 s default versus 36.21 s quiet (about 13% faster), preserving 744 prompts and reducing output from 2,036,107 to 11,742 bytes. Full-gate benefit remains unmeasured.One complete fresh replay is running on the frozen candidate with eight workers. Opus 5.5 reported no blocker; Astra's source reads failed before execution on its initial attempt and permitted mechanical retry, so the Astra review remains unavailable. The draft cannot land yet: complete replay and the missing mandatory review remain open. Kimi remains omitted per owner instruction. No further reviewer calls are part of this wave.
Local receipts:
/home/nicola/.local/state/pqsigner-research/easycrypt-resume-20261006/. After this bounded batch, proof/Rust evidence separation remains a distinct possible speed improvement. Mathematical exposure charges and the composed adaptive bound remain open; this throughput work changes no theorem claim.Nicola-Ceornea commentedon Oct 6, 2026
Throughput implementation is complete in PR #782 (final source c6f9d42; implementation reviewed at 58205b7). The existing isolated eight-worker runner is retained; CLI jobs now suppress goal rendering while keeping prompts, diagnostics and judging.
A complete pinned-image replay passed in 3115.13 active seconds (51m55s): 438 compile targets, 438 CLI targets and 411 controls; 1,287 judged; zero retries, timeouts, signals, errors or missing jobs. The parallel phase ran 1,274 jobs, followed by 13 isolated controls. This is a measured full replay, not an extrapolated benchmark. The parent-replay input identity is
4067452c5514aac56662fa5c70272072; the final candidate preserves every proof/toolchain file and all 402 bound inputs.The combined firmware CI correction releases the 18 KiB calldata frame before batch keygen/signing, preserves all tuple/completion/signature checks, and updates the stale board-SPI test. Host tests: 2,695 passed, one ignored. Standard and pixel QEMU plus invariant/pin gates pass. Astra/ultra and Opus 5.5/xhigh independently returned GO with no blocking findings in 249/210 seconds; Kimi is omitted by the owner. The follow-on commit only refreshes one generated source-excerpt line; its freshness gate passes.
Raw local receipts:
/home/nicola/.local/state/pqsigner-research/easycrypt-resume-20261006/(full-gate-result.json,combined-evidence.json,review-combined-wave/manifest.json,review-combined-reconciliation.json, final landing receipt). Broader assurance remains deferred in #509; mathematical research remains open in #100/#295. This work does not establish an end-to-end C10 forgery bound or a hardware stack bound.Landed on master at
2a98af050b70054a794629666ea5d99e910a9b80(treefbad5c6dac81397ef1a7eeba5fca1190b952758e), identical to the final candidate tree. All 15/15 GitHub checks passed before merge.The next independent engineering slice, separating proof-replay evidence from Rust correspondence receipts, is tracked in #789.