Multi-spec buffers: parallel, per-precision CVL verification - #215
Multi-spec buffers: parallel, per-precision CVL verification#215jar-ben wants to merge 33 commits into
Conversation
jar-ben
changed the title
…ede combined view)
…of a comment change
e917f8e to
1caafbb
Compare
| """One named CVL spec buffer the agent authors. Frozen and pydantic so it is both the substrate's | ||
| algorithm type and the shape stored (serializably) in graph state.""" |
| name: str | ||
| #: The buffer's own CVL text — its rules, its ``methods{}`` block, and its ``import`` statements. |
There was a problem hiding this comment.
I assume it is an invariant that buffers[nm].name == nm for all nm?
| returned sorted by name. A run-target buffer imports a shared (``is_run_target=false``) buffer only | ||
| when it does, so a shared buffer belongs to the closure (and invalidation set) of exactly the |
There was a problem hiding this comment.
"a run target buffer imports a shared buffer only when it does"
????? what?
| return tuple(out) | ||
|
|
||
|
|
||
| def import_closure(buffers: Mapping[str, NamedBuffer], name: str) -> list[NamedBuffer]: |
There was a problem hiding this comment.
is there a reason we don't have the prover create this inventory for us? The answer might be "because it doesn't produce the output we want, and this needs to land independently of that". I buy that answer, to be clear, but I want to make sure I understand the reason.
| (e.g. skipped-property or conf-flag markers). Editing the buffer OR any buffer it imports changes | ||
| the digest, so it keys the buffer's cached verify/review. Mirrors | ||
| :meth:`ContentCache.compute_cache_key` (content-keyed, order-independent).""" | ||
| # TODO: a pure-comment edit (e.g. reframing a property's justification docstring) changes this |
There was a problem hiding this comment.
WHAT IF WE USED THE CANONICAL TAC
| Verifying — submit / collect (buffers prove in parallel; never wait on a slow buffer to work on a fast | ||
| one): | ||
| - **Settle the shared base before submitting anything that imports it.** Submit a run-target buffer only | ||
| once BOTH (i) that buffer is finished AND (ii) every shared buffer it imports is finished — you do not |
There was a problem hiding this comment.
what does it mean for a run-target buffer to be "finished"? Like, finished editing?
| under-approximation), edit the shared buffer; that invalidates every buffer importing it — the | ||
| board lists them under `needs (re)submission` (including ones already verified) — so re-submit | ||
| each of them. |
There was a problem hiding this comment.
er, no it doesn't. This makes it sound like the board tells the agent what jobs need to be resubmitted based on the fix required for a shared spec fix. But it has no way of knowing a CEX remediation requires a shared spec fix?
| working_dir=pathlib.Path(run_root), | ||
| curr_spec=st["curr_spec"], | ||
| curr_spec=None, | ||
| prover_runner=WrappedProverRunner( |
There was a problem hiding this comment.
UH. Wait, hang on. This breaks the plugin API in a BIG way that will break some other code. let's discuss
| class _PutBufferTemplate(BaseModel): | ||
| name: str = Field(description="Unique buffer name (also its on-disk spec stem).") | ||
| cvl: str = Field(description="The buffer's full CVL text (rules, methods{}, imports).") | ||
| property_rules: dict[str, list[str]] = Field( | ||
| default_factory=dict, | ||
| description="The properties this buffer verifies and, for each (by its snake_case title), the " | ||
| "rule/invariant names in this buffer's CVL that verify it. Across all run-target buffers every " | ||
| "non-skipped property must appear in exactly one buffer. Omit for a shared buffer.", | ||
| ) | ||
| is_run_target: bool = Field( | ||
| default=True, description="False for a shared, imported-only buffer that runs no rules." | ||
| ) | ||
|
|
||
|
|
||
| def put_buffer[S: WithBuffers](ty: type[S]) -> BaseTool: | ||
| schema = create_model( | ||
| "PutBuffer", __base__=_PutBufferTemplate, __doc__=put_buffer_description, | ||
| state=(Annotated[ty, InjectedState], ...), | ||
| tool_call_id=(Annotated[str, InjectedToolCallId], ...), | ||
| ) | ||
|
|
There was a problem hiding this comment.
turns out you can subscript generic pydantic models with concrete types just fine, so this create model template dance is totally unnecessary.
| def put_buffer(**args) -> str | Command: | ||
| if (err := cvl_syntax_error(args["cvl"])) is not None: | ||
| return err | ||
| buffers_now = args["state"].get("buffers") or {} |
There was a problem hiding this comment.
I guess ... what's the point of the argument schema if you're gonna throw it all away at the argument typing level? But with the above understanding, just use the "WithImplementation" and what not to avoid all this boilerplate.
2 participants
Summary
Today the CVL-generation agent authors one spec with one global
methods{}block, soevery rule is verified under the intersection of what all rules need precise — one property
that needs an expensive function (nonlinear math, hashing, a heavy external) kept exact forces
every rule to pay that cost. That coupling is a common source of timeouts, and a single
combined run cannot escape it.
This PR replaces the single-spec model with named spec buffers: the agent partitions its
properties into several self-contained CVL buffers, each with its own
methods{}(so afunction summarized in one buffer can stay exact in another), and each verified and reviewed
independently and in parallel. A function's precision cost is now paid only by the buffer that
needs it.
It also converts the prover interaction from a blocking, one-spec-at-a-time call into an
async submit/collect model, so buffers prove concurrently and the agent keeps working
(authoring the next buffer, or processing a finished result) instead of blocking on the slowest
job.
Validated end-to-end on a real project (see Validation).
The buffer model
put_buffer/edit_buffer/get_buffer/list_buffers/delete_bufferauthor CVL buffers;submit_buffer/collect_resultsverify them (replacingverify_spec).property_rules(the properties itverifies + their rule names) and is run by the prover. A shared buffer (
is_run_target=false)carries infrastructure (ghosts, common invariants, helper CVL, token/oracle models, summaries)
and is never run itself.
a subset of run-targets can share one base while another subset shares a different one, and
editing a shared buffer re-verifies only its importers.
and each rule lives in exactly one buffer (
validate_coverage/validate_disjoint_rules).feedback stamp keyed to a content digest over the buffer's import closure — so editing a
buffer (or a shared buffer it imports) invalidates exactly the buffers affected, and nothing
else is re-run.
The async prover model
submit_buffer(name)launches a prover job in the background and returns immediately(concurrency-throttled; idempotent; supersedes a stale in-flight job for the same buffer).
collect_results()drains finished jobs without blocking and returns a status board(
complete/running/needs (re)submission); it blocks only when there is nothing else todo. The agent works a strict priority order — process a finished result, else author/submit the
next buffer, else block on the next completion.
{name}__{digest}.specfiles with sibling imports retargeted, so concurrent jobs never read each other's in-flight
edits.
already-verified ones); the board lists them under
needs (re)submissionso the agent re-runsexactly those.
Guidance & advisories
splitting by precision need + adding over-approximating performance summaries preemptively
(before a monolithic run), including the
assert-only vssatisfysoundness split. It is arecommendation, not a mandate.
methods{}/ghost declarations duplicatedverbatim across run-targets and suggests hoisting them into a shared buffer. It only tells —
it never blocks.
Reliability fixes (independent; bundled here — can be split if preferred)
composer/llm/anthropic.py): a mid-stream connection dropsurfaces as a raw
httpx.RemoteProtocolError; treat it as retryable.composer/prover/cloud.py): a transient failure whiledownloading a completed job's results used to bubble up and re-run the whole (often
hours-long) proof. Now the fetch itself is retried with capped exponential backoff against the
already-
SUCCEEDEDjob.certora_autosetup/setup/sanity.py):AUTOPROVER_SANITY_TIMEOUT(default 1200s) caps the sanity phase's per-job timeout.
Config knobs
AUTOPROVER_MAX_SPEC_BUFFERS— max run-target buffers (default 6).AUTOPROVER_SANITY_TIMEOUT— sanity-phase per-job timeout in seconds (default 1200).Files
New substrate & tools:
composer/spec/source/spec_buffers.py— pure buffer substrate (model, import closure, digests,coverage/disjointness validation, completion stamps, dup detection).
composer/spec/source/buffer_tools.py— the authoring tools (put/get/edit/list/delete_buffer,cap enforcement).
Wiring & orchestration:
composer/spec/source/prover.py— asyncsubmit_buffer/collect_results, materialization,job supersession, dup-linter surfacing.
composer/spec/source/author.py— buffer-only authoring mode, per-buffer review/feedback,buffer guidance.
composer/spec/source/pipeline.py,autoprove_common.py,composer/spec/cvl_generation.py,composer/certora_env.py,certora_autosetup/cache/content_cache.py— supporting wiring.composer/templates/property_generation_system_prompt.j2— prompt updates.Testing
51 new unit tests across 7 files, all pure (no live prover / no jar):
test_spec_buffers.py(26) — substrate: ownership, import closure, digests, coverage,disjoint rules, completion stamps, dup detection, buffer-map reducer.
test_buffer_completion.py(6),test_spec_buffer_prover.py(5),test_buffer_tools.py(5) —completion tracking, async submit/collect + per-buffer feedback, cap enforcement.
test_cloud_fetch_retry.py(2),test_sanity_timeout.py(4),test_anthropic_retry.py(3) —the reliability fixes.
Full non-expensive suite green (1219 passed; the only errors are pre-existing
test_rag_db.py [postgres]env cases that need the local RAG container).pyrightclean.Validation (live cloud run)
Run on a testing real project:
init/ownership, impl/upgrade-auth, attack-vectors; combinatorial-collateral: core, operations,
attack) — i.e. multiple buffers within a property class, not merely one per class.
buffers were refined.
expected-failure attack vectors + refinement CEXes).
owner()across the 3 buffers) and the agentcorrectly treated it as a non-blocking suggestion.
same volume that previously surfaced transient stalls).
Follow-ups (out of scope)
spec_buffers.py): a pure-comment edit changes thebuffer digest and re-runs an identical proof. The fix is a separate comment-stripped prover
digest distinct from the raw feedback digest — noted, not done here.
custom_summaries.spec(SafeTransferLib path not covered) and the summarizer↔CVL-agentone-way handoff — a pre-existing, unrelated issue, not introduced by this PR; handed off
separately.