Conversation
A plugin that edits one of the author's spec buffers and asks the prover runner to verify it got the text staged alone, as a free-standing spec. With named buffers, that text imports siblings and the shared summaries a directory up, and none of them were on disk where the staged spec looked. The prover runner now takes the name of the buffer the text belongs to. It stages the author's whole buffer set under the component's spec directory, with that buffer replaced by the text under test, and writes the conf the author's own buffer runs use. Without a name it stages the text alone, as before. The component slug rule has one definition, and buffer_conf takes per-run conf overrides the way setup_prover_config_in does. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
jtoman
approved these changes
Oct 1, 2026
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A plugin that edits one of the author's spec buffers and asks the prover runner to verify it got the text staged alone, as a free-standing spec under
certora/specs/adhoc_run.spec. With named buffers, that text imports siblings (import "shared.spec") and the shared summaries a directory up (import "../summaries/X.spec"), and none of them were on disk where the staged spec looked, so every such run failed to compile.The change:
ProverRunner.__call__takesbuffer: str | None = None, the name of the author's buffer the text belongs to.Nonekeeps today's behavior.WrappedProverRunnercarries the author's buffers and the component slug. A run on a named buffer stages the whole set undercertora/specs/<slug>/with that buffer replaced by the text under test, through the samematerialize_buffersandbuffer_confthe author's ownsubmit_bufferruns use, so the imports resolve to the same files. An unknown buffer name or a missing slug is aValueErrorbefore anything is staged.component_slug()is the one definition of the slug rule; the prover tool's closure calls it.buffer_conf()takes per-run conf overrides (msg,compilation_steps_only) the waysetup_prover_config_indoes.Tests: a two-buffer author whose target imports a sibling and the summaries. The run sees the sibling and the edited text on disk under the component dir, the conf verifies
certora/specs/<slug>/target.specwith the rule, the message and the override, and nothing stays behind. Plus the no-name path, the two refusals, and the slug rule. Full suite: 1519 passed. Pyright: 0 errors.🤖 Generated with Claude Code