Repository navigation
Conversation
The CVL agents' context documents and recipe index were module-level singletons. They become a KnowledgeBundle: context documents for the front of every agent in a family, and optionally a RecipeSet, an index plus bodies fetched by id. KBRecipe and IndexModel are generic over the channel vocabulary, because a channel names a tool the reading agent holds, and the CVL and CVLR agents hold different tools. The loaders are cached per bundle, so a bundle is frozen and carries nothing that varies per run. kb_tools(bundle) returns the bundle's recipe tool, or none for a bundle without recipes. CVL_BUNDLE is the old context, unchanged in content; its callers pass it explicitly. kb_index.j2 replaces cvl_kb_index.j2, names the bundle rather than CVL, and renders the index's channel legend. The second instance is CVLR's: cvlr_baseline_facts.md, the run-invariant facts about CVLR and the Solana Prover, and recipes K1-K3 behind get_cvlr_recipe. CVLR_FACTS_BUNDLE is the same facts without the index, for a reader that cannot retrieve a recipe. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ericeil
added a commit
that referenced
this pull request
Nov 5, 2026
Both were cut from eric/solana-staging onto master on 2026-11-05. Record their sizes and what each cut took or left against the plan. P1b carries the sound signed math flag and its prover_version pin, so the older sections that held them on the branch now say they are superseded; C7b reads generations(), which replaces reference_for. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Review fixes for the CVLR bundle. The facts document is read by the editor and the researcher as well as the author, so it no longer instructs the reader to call the author's tools; those steps are in the author's prompt. It describes the files the scaffold actually writes and states the orphan rule for CvlrLog impls, says what a counterexample carries and where clog! fits in it, states the crate:: path as a fact of the harness's location rather than of a gate, and replaces a citation to a task-prompt section that does not exist with the action itself. K3 scopes "sysvars are analyzed" to solana-program 2.2 and the SDK 3 crates. On 1.18 from_account_info is under the never-inline solana_program blanket, so it is external and the property is a skip. The CVLR channel legend says where a fix lies in the author's tools rather than ordering the reader to use them, since the judge reads it too. IndexModel rejects a recipe channel the legend does not explain, and rejects extra keys, so the preamble the index files carried (dropped on load, and disagreeing with the rendered one) is gone from both. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Drop the checks that restated headings, the K3 paragraph, the loader body, and the current count of CVL documents. Check the cache marker, that a rendered index carries its channel legend and tool name, and that an unknown id or a missing recipe file is a miss.
Comments and docstrings only. The constraints stay: one channel set per family, unknown YAML keys fail to load, and the CVLR channel names map to the author's tools.
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
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.
This PR generalizes the CVL agents' knowledge context into a
KnowledgeBundleand adds its second instance, CVLR's: a document of run-invariant facts about CVLR and the Certora Solana Prover, and three CVLR recipes behind aget_cvlr_recipetool.Why is this needed?
The CVLR agents (the rule author, its judge, the reviewer of program edits, and the research sub-agent) all need the same facts about CVLR and the Prover. The way CVL already delivers such facts is the right one: context documents in front of the agent's initial prompt, behind a cache marker, and a recipe index whose bodies the agent fetches by id when a trigger matches. But that mechanism was CVL's alone: one module-level list of documents, one recipe index file, one tool name, and a channel vocabulary (
CVL | CONF | EDIT) that names CVL agents' actions.Copying it for CVLR would fork it. This PR generalizes it instead, and lands the generalization together with its second user, so the API can be judged against a real one rather than a future one. Neither the CVLR author nor its judge is on master yet;
test_kb_bundle.pyandtest_cvlr_bundle.pyrender and check the CVLR bundle the way they will use it.Where to start
KnowledgeBundleandRecipeSetincomposer/kb/kb_context.py. A bundle is a label, its context documents, and optionally a recipe set. It is frozen, and its loaders are cached per bundle, so nothing that varies per run can go in it.context_documents(bundle)andwith_context(bundle, prompt)replacecvl_context_raw()and the body ofwith_cvl_context, which is kept as a one-line wrapper overCVL_BUNDLE.KBRecipe[C]andIndexModel[C]are generic over the channel vocabulary, because a channel tells a stuck agent whether the fix is in its own action space, and CVL and CVLR agents hold different tools. A CVLR index that named a CVL channel, or the reverse, fails validation. The index'schannels:legend, which the CVL index file already carried but never rendered, is now rendered with the index (composer/templates/kb_index.j2, which replacescvl_kb_index.j2and names the bundle rather than CVL).kb_tools(bundle)incomposer/kb/knowledge_base.pyreturns the bundle's recipe tool, named by its recipe set, or no tool for a bundle without recipes. Its two callers (composer/spec/services.py,composer/workflow/executor.py) passCVL_BUNDLE.CVLR_BUNDLE(facts and recipe index) is for the agents that holdget_cvlr_recipe.CVLR_FACTS_BUNDLEis the same facts document without the index, for readers that cannot retrieve a recipe: the index tells its reader to fetch a file, and its channels name the author's tools. The content iscomposer/kb/resources/cvlr_baseline_facts.md,cvlr_recipes_index.yaml, and recipes K1 (satisfyfor reachability), K2 (clog!before an enum assert) and K3 (read sysvars directly).What changes for CVL agents
The documents are the same. The rendered recipe index gains the channel legend, and its wording refers to "the recipe's id" rather than
Rnn. So the CVL agents' cached prefix changes once.🤖 Generated with Claude Code