Multi-spec buffers: parallel, per-precision CVL verification - #215

Open

jar-ben wants to merge 34 commits into

jaroslav/multi-spec-buffers-v2

Commits on Sep 8, 2026

multi-spec-buffers: pure substrate on top of the buffer abstraction
jar-ben
committed
a965548
multi-spec-buffers: buffer authoring tools (put/get/edit/list/delete)
jar-ben
committed
37a6e07
multi-spec-buffers: per-buffer materialization + run planning (pure)
jar-ben
committed
236e5ed
multi-spec-buffers: per-buffer completion tracking
jar-ben
committed
a6dd34b
multi-spec-buffers: per-buffer verify orchestration (run_buffers)
jar-ben
committed
413049f
multi-spec-buffers: activation wiring (opt-in tools + state)
jar-ben
committed
99989f2
multi-spec-buffers: per-buffer property ownership on put_buffer
jar-ben
committed
971e3ad
multi-spec-buffers: prompt guidance + judge/report over buffers
jar-ben
committed
69ec04e
multi-spec-buffers: per-buffer review + per-buffer completion (supersede combined view)
jar-ben
committed
463b184
multi-spec-buffers: AUTOPROVER_SPEC_BUFFERS takes true/false only
jar-ben
committed
5465182
multi-spec-buffers: review fixes (dead code, dedup, per-buffer nag)
jar-ben
committed
31f0eb1
autoprover: async per-buffer prover — submit_buffer / collect_results
jar-ben
committed
ca7e98c
autoprover: default spec buffers on (AUTOPROVER_SPEC_BUFFERS=false to disable)
jar-ben
committed
2c4e507
autoprover: make async-buffer prover test jar-free
jar-ben
committed
9dfd2ec
autoprover: multi-buffer is the only CVL-gen mode; cap at 6
jar-ben
committed
5d6a272
autoprover: fix non-editing buffer feedback; selective shared imports; dup linter
jar-ben
committed
8eb8eaf
autosetup: make the sanity-phase timeout configurable (AUTOPROVER_SANITY_TIMEOUT)
jar-ben
committed
5b2dae9
autoprover: re-fetch a completed cloud job on transport failure
jar-ben
committed
c051a20
autoprover: strongly recommend splitting + preemptive summaries (drop forced split)
jar-ben
committed
3e311c4
autoprover: spec buffers TODO note - don't rerun prover just because of a comment change
jar-ben
committed
1caafbb
autoprover: remove single-spec dead code left by the buffer-only switch
jar-ben
committed
0a7659a
autoprover: drop the --certora-run-command / AUTOPROVER_CERTORA_HOME override
jar-ben
committed
244d9e9
autosetup: robust CVL import parsing (fixes prover-cache invalidation)
jar-ben
committed
12f21f8
autoprover: derive buffer imports from CVL (drop the manual imports field)
jar-ben
committed
50e7732
autoprover: resolve buffer imports by path, not string ops
jar-ben
committed
f95ab1a