Add the Solana Prover preflight step by ericeil · Pull Request #248 · Certora/AutoProver

ericeil · 2026-09-22T16:46:58Z

The preflight step for the Solana Prover backend. The backend itself is not here: these functions are what its preflight will call. Preflight is a backend's own setup. The pipeline runs it at the same time as system analysis, and a failure cancels that analysis, so the run stops before any rules are written. What it returns is handed to prepare_system.

On a Cargo project this step:

Names the package under verification. A given name wins; otherwise the library crate that owns the main source file. With neither, several library crates is a refusal.
Writes the src/certora/ harness: the module root, an empty specs module where rules will go, and the inlining and summaries files, composed from AutoProver's starting configuration and spelled for the Solana version the project builds. These files are AutoProver's, and they are rewritten whenever they differ from what the scaffold would write, as CVL AutoSetup does with the files it writes under certora/.
Adds the certora cargo feature, the CVLR dependencies and [package.metadata.certora] to the package's manifest, and declares the harness module in lib.rs. Each local path dependency gets a certora feature of its own, which the program's forwards to, so a verification-only edit inside it can be gated. The Prover's build output is added to .gitignore. The project's own files are only added to, and only with what is missing, so a second run changes nothing.
Points Anchor, and the fixed crate, at Certora's verification forks when the project depends on them and the fork covers that version. An uncovered version stops the run. Against crates.io Anchor, a handler cannot be analyzed.
Checks that the scaffolded project compiles, with cargo check on the host target.

Three cases are refused. A package that builds no cdylib, so cargo produces no loadable object. A project on a different Solana platform generation from the CVLR versions the scaffold pins, since the generations have different AccountInfo types and that pairing would not compile. And a project already on a different CVLR release from the one this build supports.

That last one is a narrowing, and worth saying plainly: one CVLR line is supported at a time, the way a Prover release ships one CVL. Everything the scaffold writes belongs to the line composer/spec/cvlr_reference.py names — the pins, the specializations added beside them, and the env files — so a project already on another line cannot be given those without putting two CVLR generations in one graph. An earlier version of this step deferred to such a project instead: it kept the project's pins, withheld the specializations that would have collided, and reported the disagreement for someone to read later. That leaves the run on a configuration nothing else is built for, so it now stops before anything is written. Moving to another line is an edit to the reference set, not a per-project decision.

The pin is read from the resolved graph, which is exact for a crate some member already depends on, and from the manifests, which are the only place a crate pinned in [workspace.dependencies] and depended on by nobody yet can be seen. A reference-set crate the project does not name at all is not a disagreement — that is the ordinary state of a specialization it has no use for — so the two cases are separate types (Mismatched and Absent) rather than one nullable field. Preflight resolves again after the scaffold and fails on a Mismatched, which the gate cannot produce and a [patch] table can.

Every Solana conf is built in composer/spec/cvlr/conf.py, never read from the project: fixed settings (BASE_CONF), the two the author may change (loop_iter and optimistic_loop), and one submission's build script, message, summaries and rule selection.

composer/prover/conf.py is new, and holds what both sides use: dump_conf for writing a conf, and a typed rule selection for scoping one. The settings a CVL conf carries are unchanged. Every CVL conf is now written through dump_conf, and WrappedProverRunner rejects rules and exclude_rules together, as the ProverRunner protocol already required. ConfigurationBuilder's unused with_* methods are removed.

To see the whole step run against real cargo:

uv run --no-sync pytest tests/test_cvlr_preflight.py -m expensive

That test is expensive because it resolves dependencies off the network, and it skips when cargo is not installed. The other tests here build a workspace by hand and run in the normal suite.

Point this at a Cargo workspace and it names the package under verification, resolves which CVLR crates the build will get, scaffolds a verification harness into a project that has none, and proves the result compiles. That is the whole of it: no agent, no prover, no network beyond cargo's own. `tests/test_cvlr_preflight.py` is that sentence as a test, against real cargo: a bare two-member workspace goes in, and what comes out compiles with a harness module in it. It is `expensive` — it resolves a dependency graph off the network — and it skips, naming cargo, when there is no toolchain. Everything else here is tested against a hand-built graph, which is the right way to pin what the planner decides and cannot pin the three things most likely to be wrong: which member cargo says owns a file, that the CVLR crates are only visible after the scaffold is applied and the graph re-read under the verification feature, and that the result builds. The pieces, and why each is here rather than in a later change: * `composer/cargo/{metadata,session}` read `cargo metadata` and run cargo under the command sandbox. Shared with the Rust wheel backends — reading a manifest is the same work whoever wants the answer — but the callers here are the first. * `composer/spec/cvlr_reference` and `cvlr/crates` are the pinned crate set and the resolution of a project's graph against it, including where the two disagree. A gap is reported, never corrected: the project's own pin wins, and what has to be qualified is recall from the knowledge corpus. * `cvlr/conf` is the prover's configuration vocabulary — what a project's own conf means, which keys a run owns, and which two settings may be moved. It was built once and then not wired, so a project that had tuned its solver flags was verified without them; the layering is tested at both ends now. * `cvlr/env_paths` rewrites the canonical directive files for the path spelling a given project's dependency graph actually uses. Solana split one crate into many and both spellings are live. * `cvlr/scaffold` plans and applies the whole shape, never overwriting, so pointing it at a project that is already set up is a read. * `cvlr/munge` carries one subject: replacing a dependency with the verification-oriented fork of it. Upstream's error type boxes its payload and the prover rejects that, so on an Anchor project this is the difference between a rule that can be analyzed and one that cannot. The rest of that module — the source-edit vocabulary — has no caller here and lands with the code that applies it. * `cvlr/preflight` composes all of the above into the two calls a run makes. The canonical directive files under `cvlr/envs/` started as a copy of the Solana spec template's and are maintained here now; they are edited in place, and `DEVIATIONS` records the lines this backend deliberately does not ship as the template wrote them. Nothing outside `composer/spec/cvlr/` imports from it. No existing behaviour changes: the only edit to a file that was already here is five lines of `pyproject.toml`, shipping the directive files with the wheel. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The new modules under composer/spec/cvlr/ spelled the decorator @dataclasses.dataclass; every other module here imports the names it uses from the module. Also covers the two other module-qualified calls, field and replace, since keeping `import dataclasses` for those would defeat the point. No behaviour change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Keep the constraints. Drop change history, restatements, and pointers at docs and modules this branch does not have.

- Type `cargo metadata` output with TypedDicts instead of bare dicts. - Parse `CratePackage.source` into RegistrySource | GitSource | OtherSource at the metadata boundary, so munge dispatches on the type rather than a string prefix. `points_at_fork` now only matches a git source. - Add a `Conf` alias (dict[str, object]) for prover confs. - `RunOverlay.build_script` and `summaries` are Paths, stringified when the conf is written. - `ForkOverride.branches` is a version -> branch mapping, not a tuple of pairs. - `_metadata_section` takes the two tuning-file paths as arguments instead of a dict keyed by family stem. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Reading, writing, and layering a prover conf move to composer.prover.conf: parse_conf/read_conf/dump_conf, merge_prover_args, the loop_iter and optimistic_loop helpers, safe_msg, a RuleSelection sum type (with a new ExcludeRules variant), and overlay(). Each ecosystem keeps its own policy on top: prover_config_overlay for CVL, solana_conf for Solana. CVL conf settings are unchanged. The overlay still forces verify, parametric_contracts, optimistic_loop and rule_sanity; extras are still a plain update; the base's rule entry is still inherited when no rules are given. setup_prover_config_in now takes a RuleSelection, built by rule_selection() from the tool's rules/exclude_rules pair. The run-history TypedDict is renamed RuleSelectionRecord to free the name. WrappedProverRunner now rejects rules and exclude_rules together, which the ProverRunner protocol already disallowed, with verify_spec's message. All conf writers go through dump_conf (indent 2 plus a trailing newline). Solana confs change from indent 4, which changes conf_history digests. ConfigurationBuilder drops its eight unused with_* setters. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The module only redirects dependencies at Certora's verification forks via [patch.crates-io]; "munge" elsewhere in the repo means source editing (composer/spec/source/munge). Rename the module, its test, and the Munge-prefixed names (MungePlan -> ForkPlan, MungeBlocked -> ForkBlocked, plan_munge -> plan_overrides) to match. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Drop nondet.rs, log.rs and mocks/mod.rs from the scaffolded harness. The CVLR backend never writes or reads them: Nondet/CvlrLog impls go in the unit's own specs module, mock_fn stand-ins are named under crate::certora::specs, and module redirects reach certora/mocks/ through #[path], which needs no mocks module. The harness root now declares only `pub mod specs;`. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The inlining and summaries code moves out of scaffold.py into composer/spec/cvlr/tuning.py: EnvFamily, INLINING/SUMMARIES, ENV_DIR, compose_env, and the file headers. The module docstring describes what each file tells the Prover and which layer a change belongs in. The files under envs/ are now AutoProver's own starting configuration rather than a vendored copy of solana-spec-template, and the references to the template are gone. canonical_env/CANONICAL_ENVS become starting_env/STARTING_ENVS. EnvFamily gains a `kind` field and initial_package_layer(), replacing a `family is INLINING` check and the TEMPLATE_REPO constant. Deviation/DEVIATIONS are removed. They existed to keep envs/ byte-identical to upstream, and without an upstream they only patched our own file. The one deviation is now an edit to cvlr_inlining_core.txt: #[inline] ^<solana_program::program_error::ProgramError as core::convert::From<u64>>::from$ in place of #[inline(never)]. ProgramError is returned through an sret out-pointer. Left opaque with no summary, the constructor havocs that write, including the Result discriminant, so an error built with `SomeError.into()` has a nondeterministic is_err(), and a rule that a handler rejects bad input cannot be proved. The unsound directive only started to matter with path rewriting. It names solana_program::program_error::, and on a post-split target (solana-program 2.2+) the symbol is solana_program_error::ProgramError, so the original line matched nothing and was harmless. env_paths rewrites old paths so directives apply again, and for this line that switched on the unsound inline(never). Measured: with the path left unrewritten, or rewritten with #[inline], the rules verify. Rewritten with #[inline(never)], they are violated. The scaffold no longer copies the _core/_anchor layers into a target. Nothing read those copies: composites were built from ENV_DIR, so editing them did nothing. Only _package.txt (written once) and the two composites land in envs/. A new Regenerate change rewrites a composite whenever it differs from what the starting configuration and the package layer compose to. An edit to _package.txt, or a newer starting configuration, now reaches the build on the next preflight. Before, both were frozen at first scaffold (U15 in docs/cvlr-todo.md on eric/solanaProver). A composite that is already current is reported as satisfied, so a second run still changes nothing. Existing projects keep their old _core/_anchor copies, which are now inert. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The scaffold now treats everything it writes under src/certora/ as AutoProver's, as CVL AutoSetup does with the files it writes under certora/. mod.rs, specs/mod.rs and the two tuning composites are rewritten whenever the file on disk differs from what the scaffold would write, so a harness left by an earlier run or by hand is replaced. The project's own files (manifests, lib.rs, .gitignore) are still only added to, and a second run still changes nothing. With the harness overwritten, cvlr_*_package.txt would always be empty, so the package layer is removed: the composites are the starting layers plus the per-unit layer, and a project's own directives belong in the unit layer. NewFile and Regenerate become one Write change. The harness files and the composites are planned by one loop over _harness_files(), replacing _HARNESS_FILES, _HARNESS_WHY and _plan_envs. A missing .gitignore is an AppendSection that creates it. apply() loses the "appeared since planning" branch and the module its logger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The Solana backend no longer takes a project's hand-tuned conf as its base. Every conf is now built from fixed settings (BASE_CONF, BASE_PROVER_ARGS) plus a typed ProverSettings holding the three values the author may change: loop_iter, optimistic_loop and solver_portfolio. settings_conf renders the settings; solana_conf adds one submission's build script, message, summaries and rule selection; conf_history hashes the rendered conf. With no person-written conf to honor, the machinery for one goes: project_conf/PROJECT_CONF_NAMES/load_base and the scaffold's CONFS_DIR; the JSON5 reader (parse_conf, read_conf, MalformedConf); the tolerant readers (str_list, string-valued optimistic_loop); prover_args merging and the -solvers special case; OVERLAY_OWNED_KEYS dropping, the rule_sanity floor, and merging the base's own summaries; RunOverlay.extra; and AllRules, which existed only to override a project conf's rule list. The build settings read from the conf go too. The platform-tools release is the PLATFORM_TOOLS_VERSION constant, since the reference set pins one platform generation, and cargo_tools_version leaves the conf, which the prover never applied. The feature is always DEFAULT_FEATURE. overlay() had one remaining caller, CVL's prover_config_overlay, and its drop parameter was Solana's alone, so it is inlined there. CVL confs are unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…nto BASE_CONF NONLINEAR_SOLVER_PORTFOLIO and ProverSettings.solver_portfolio are removed. The portfolio was the only thing that ever added to prover_args, so the flags are now a fixed prover_args key of BASE_CONF and BASE_PROVER_ARGS goes. The key keeps its position in the rendered conf, so conf_history is unchanged for every remaining setting and no existing stamp goes stale. The note that -solanaTACSoundSignedMath must not be combined with -solanaTACMathInt moves from the portfolio's comment to BASE_CONF's, since it is a constraint on the base flags. The Prover's timeout cracker is the candidate replacement; it is tracked as U16 in docs/cvlr-todo.md on eric/solanaProver. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…ht back-port Backend plan: the scaffold's ownership rule (the harness under src/certora/ is AutoProver's and is rewritten when it differs; the project's files are only added to), the starting tuning layers maintained here rather than vendored, no package layer, starting_env, and forks.py in place of the fork half of munge.py. Landing plan: P1 is #248, and carries forks.py, the env half of tuning.py and composer/prover/conf.py with its CVL callers; the refresh script is gone. munge.py lands whole in P3a, tuning.py is the file split between P1 and P3b, and #243 was closed rather than grown into P1. #248 does not yet carry the cvlr-preflight script or the entry.py hunks. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The scaffold used to defer to a project that already pinned CVLR: it kept those pins, withheld the specializations that would have collided with them, and reported the disagreement as a version gap for someone to read later. That leaves the run on a configuration nothing else here is built for. Everything this scaffold writes belongs to the line the reference set names — the pins, the specializations added beside them, and the env files `tuning.py` composes — so a project already on another line cannot be given those without putting two CVLR generations in one graph, which is the non-compile the withholding existed to avoid. One line is supported at a time, the way a Prover release ships one CVL. So the pin becomes a precondition. `_check_pins` refuses a project on any other CVLR release, beside the platform-generation gate and in the same shape, before anything is written. It reads both the resolved graph, which is exact for a crate some member already depends on, and the manifests, which are the only place a crate pinned in `[workspace.dependencies]` and depended on by nobody yet can be seen. A crate the project does not name is not checked: that is the ordinary state of a specialization it has no use for. `VersionGap` carried those two cases behind one `resolved: str | None` and they now ask for opposite handling, so it splits into `Mismatched` and `Absent`. Preflight resolves again after the scaffold and fails on a `Mismatched`, which the gate cannot produce and a `[patch]` table can. Both gates now run unconditionally. `_scaffold_pins`, `_introduced` and `_declared` existed only to express the deference and are gone. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Four docstrings in the reference set explained themselves by naming a knowledge corpus: `label` was "for corpus provenance", `UnpublishedCapability` was "recorded so the corpus can say it is uncovered", and `crates` / `scaffold_crates` were distinguished by "what the corpus was compiled against". No such corpus exists here, so each of those was a forward reference a reader cannot check. Each has a reason that stands on its own. `label` is what the platform refusal and the tuning-path log line name. `UnpublishedCapability` records a capability with no published release, which is why it cannot be a `Mismatched` — that is a disagreement about which release, and this is the absence of one. `crates` and `scaffold_crates` are two questions asked in two places: `_check_pins` gates on the releases this build supports, and the manifest planning writes the ones a project is given. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The plan for replacing the CVLR source mount with a documentation corpus and a research sub-agent. Three pieces: `cvlr_api_kb` extracted from rustdoc and compile-gated, `cvlr_kb` re-scoped to the manual and practice it already holds, and a `cvlr_research` agent that answers out of both. Two corpora rather than one because what the source mount really provided was an authority ordering — a channel derived from the code, outranking one written by hand — and a retrieval hit carries no provenance, so a merged corpus cannot express it. Their regeneration lifecycles differ too: ingest is a plain INSERT under a unique constraint, so a rebuild means dropping a schema, and a CVLR bump should not take the hand-curated entries with it. The version question is settled by pinning: one CVLR line at a time, the way a Prover release ships one CVL, with a project on another line refused rather than accommodated. §2.6 records that half as landed — it was the first step, it went into #248 where those files are still under review, and it is what makes a single-version corpus a guarantee rather than an assumption. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

jtoman · 2026-09-24T03:32:48Z

@@ -0,0 +1,282 @@
+"""Which published CVLR releases count as current, for each chain.


kinda surprised this isn't in the, y'know, cvlr submodule?

Yeah, I think there was some reason for this in an earlier version, but it clearly should be in the cvlr module.

jtoman · 2026-09-24T03:33:32Z

-    def with_compilation_steps_only(self) -> Self:
-        return self._replace(compilation_steps_only=True)
-
-    def with_loop_iter(self, n: int) -> Self:
-        return self._replace(loop_iter=str(n))
-
-    def with_optimistic_loop(self) -> Self:
-        return self._replace(optimistic_loop=True)
-
-    def with_optimistic_hashing(self) -> Self:
-        return self._replace(optimistic_hashing=True)
-
-    def with_solc_via_ir(self) -> Self:
-        return self._replace(solc_via_ir=True)
-
-    def with_strict_solc_optimizer(self) -> Self:
-        return self._replace(strict_solc_optimizer=True)
-
-    def with_prover_args(self, args: list[str]) -> Self:
-        return self._replace(prover_args=list(args))
-
-    def with_rule(self, rule: str) -> Self:
-        return self._replace(rule=[rule])


....? why would you do this? they're not used now but this is an API type.

Overzealous cleanup while generating some shared conf infrastructure. I'll put this back.

jtoman · 2026-09-24T03:36:10Z

+type RuleSelection = InheritRules | SelectRules | ExcludeRules
+
+
+def with_rules(conf: Conf, rules: RuleSelection) -> Conf:


tioli, but you can define this as a common function across all the types in RuleSelection. pyright is smart enough to understand that if every type in RuleSelection declares a with_rules(self, conf: Conf) -> Conf that calling with_rules(...) on a value of type RuleSelection is safe. (don't call it with_rules, call it apply_to or whatever, but you get the idea).

jtoman · 2026-09-24T03:40:38Z

+#[inline] ^<anchor_lang::accounts::program::Program<T> as core::convert::TryFrom<&solana_program::account_info::AccountInfo>>::try_from$
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+#[inline] ^<anchor_lang::accounts::unchecked_account::UncheckedAccount as core::convert::AsRef<solana_program::account_info::AccountInfo>>::as_ref$


you misspelled something here

haha just kidding, but like, are these autogenerated? If so, there is a way for uv to be convinced to generate them at build/sync/install time.

These are taken from a repo we use as a starting point for hand-written specs; I originally had a whole system for automatically pulling those over here and then editing them (we need some small changes vs. the files in that repo) but it got really messy and I finally settled on just keeping separate copies in this repo.

jtoman · 2026-09-24T03:41:24Z

@@ -0,0 +1 @@
+;; Summaries for anchor functions


This was here for symmetry, and I thought it would simplify the code elsewhere. Not sure about that any more.

jtoman · 2026-09-28T17:56:36Z

+    if blocked or not plan.overrides:
+        return [], [] if blocked else plan.notes(), blocked
+    return (
+        [
+            AppendSection(
+                path=Path("Cargo.toml"),
+                contents=forks.manifest_additions(plan),
+                why=(
+                    "verify against the forks that can be analyzed: "
+                    + ", ".join(f"{o.crate} {o.version} -> {o.branch}" for o in plan.overrides)
+                ),
+            )
+        ],
+        plan.notes(),
+        [],
+    )


there seems to be an implicit invariant here about the list[Change] component being non-empty iff blocked is empty. I'd prefer you make this explicit.

jtoman · 2026-09-28T17:57:27Z

+    manifest_changes, manifest_notes, blocked = _plan_package_manifest(
+        workspace, package, relative, reference, inherit=inherit
+    )
+    # Unconditional, both of them: the scaffold always writes the reference-set pin now, so the
+    # reference set's platform generation always describes what will be built.
+    blocked += _check_pins(workspace, package, reference)
+    blocked += _check_platform(workspace, reference)
+    blocked += fork_blocked


oh, seeing how these result values are used, nevermind. Worth a comment about the invariant at least.

jtoman · 2026-09-28T18:01:46Z

+from composer.spec.cvlr.env_paths import PathDialect
+
+#: The starting layers, shipped in the wheel. Every composite is built from these.
+ENV_DIR = Path(__file__).parent / "envs"


importlib.resources please and thank you

jtoman · 2026-09-28T18:06:00Z

+        # were rewritten.
+        parts.append(
+            f";;; Platform paths rewritten for this target's generation "
+            f"({len(dialect.aliases)} aliases) — see composer/spec/cvlr/env_paths.py\n"


sorry, this is part of the deliverable? please don't leave a reference to some random source file, a reader has no idea what to do with that...

Oh, good point; thanks for spotting that!

jtoman · 2026-09-28T18:06:50Z

+
+
+def compose_env(
+    family: EnvFamily, *, unit_layer: str = "", dialect: PathDialect = PathDialect()


unit_layer: str = "",

Have you heard of our lord and savior the None type?

please use unless it makes the code annoying.

with_rules(conf, rules) matched on the three RuleSelection variants to decide which key to write. Each variant now carries that as apply_to(conf), so the knowledge of which key a selection writes lives on the selection, and the free function goes. Both callers, solana_conf and prover_config_overlay, call rules.apply_to(conf). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

cvlr_summaries_anchor.txt held only its header comment: Anchor adds inlining directives but no points-to summaries. Every family was still made to carry a core and an anchor layer, so the file existed only to fill that slot. EnvFamily now names its starting layers, in composition order, and the composite header and composition iterate them. INLINING keeps core and anchor; SUMMARIES has core alone, and the empty file goes. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

ProverSettings read too close to composer.prover.core.ProverOptions, which is about invoking the prover rather than the conf the author may tune. settings_conf and the settings parameters follow as tunable_conf and tunable. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

plan_overrides' docstring promised four outcomes and listed five, with blocked twice, and said skipping an uncovered fork leaves the boxed error in the build. That is Anchor's failure; fixed has no boxing. The uncovered-version refusal said the same thing to a project on an unlisted fixed release. Blocked is now one outcome with its two causes. ForkOverride carries upstream_failure, and the refusal quotes the fork's own. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The resolution said "do not verify against the unforked crate", and each fork's upstream_failure opened with "it"/"its", leaning on that phrase for its subject. An uncovered fixed release now reads "do not verify against fixed <version> from crates.io: upstream fixed lacks the conversions ...", and each failure names its own library. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

plan_overrides defaulted to SOLANA_OVERRIDES, and _plan_forks never received the ChainReference, so a Soroban scaffold still planned Anchor and fixed. That is the same forgettable Solana default as prepare_workspace's old chain="solana". ChainReference gains a required forks field: SOLANA has Anchor and fixed, SOROBAN has none. plan_overrides takes the forks with no default, and _plan_forks passes the reference's own. SOLANA_OVERRIDES is gone; SOLANA.forks is the list. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The platform, pin, and unpinned-checkout refusals told the reader to edit composer/spec/cvlr/reference.py. The reader owns the project, not AutoProver's source: the same objection as the tuning-file pointer removed in fd4ba89. Each resolution now names the release this build supports and the change to make in the project, and says that staying on another line needs an AutoProver build pinned to it. The platform problem names the line by its crates (ChainReference.line) instead of "the reference set". Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The problem said how the mismatch fails (a compile error, not a warning; the scaffold still builds; the first rule that hands over an account fails), which is maintainer background. The resolution added that staying put needs another AutoProver build. A project author needs the version they are on, the one this build requires, and the one to move to. The mechanism is still in _check_platform's docstring. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Following f588f87's platform refusal, the other Blocked texts drop what a project author cannot act on: how a mismatch fails (two generations in one graph, the build still linking the other copy, the gate not passing what it cannot see), which member has not resolved a crate yet, that staying put needs another AutoProver build, "not a scaffold's call" asides, and "ask for a branch and add it here", which meant editing AutoProver. The uncovered-fork refusal now names the releases the fork covers instead of what upstream fails on, so ForkOverride.upstream_failure has no reader and is removed. The Solana platform label is "solana-program 2.x"; the monolithic-line note is a comment. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

PackageTable.metadata was a dict[str, object], an untyped bag that named a value type it did not check, and Manifest.package_metadata handed the bag out. The one reader, the scaffold, asked only whether "certora" was a key. [package.metadata] is now a model declaring the one tool table consulted, certora: CertoraMetadata | None, and Manifest.certora_metadata replaces package_metadata. Other tools' tables are still ignored. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The note is scaffold output for the project author; a private function name is not theirs to follow. It now says the release is checked on its own. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The default became None in fd4ba89, but the check still read a blank string as absent too. None is now the only absence. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

CvlrSources.of sorted by (name, version), so two copies of one version, say a registry release and a git checkout of it, stayed in cargo's unstable order, and that order is written into run metadata. The manifest path breaks the tie. It is used rather than the source because a path dependency has no source, so two local copies would still tie. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

ericeil

Addressed John's feedback

ericeil · 2026-09-28T18:27:29Z

-    def with_compilation_steps_only(self) -> Self:
-        return self._replace(compilation_steps_only=True)
-
-    def with_loop_iter(self, n: int) -> Self:
-        return self._replace(loop_iter=str(n))
-
-    def with_optimistic_loop(self) -> Self:
-        return self._replace(optimistic_loop=True)
-
-    def with_optimistic_hashing(self) -> Self:
-        return self._replace(optimistic_hashing=True)
-
-    def with_solc_via_ir(self) -> Self:
-        return self._replace(solc_via_ir=True)
-
-    def with_strict_solc_optimizer(self) -> Self:
-        return self._replace(strict_solc_optimizer=True)
-
-    def with_prover_args(self, args: list[str]) -> Self:
-        return self._replace(prover_args=list(args))
-
-    def with_rule(self, rule: str) -> Self:
-        return self._replace(rule=[rule])


Overzealous cleanup while generating some shared conf infrastructure. I'll put this back.

ericeil · 2026-09-28T18:30:57Z

+type RuleSelection = InheritRules | SelectRules | ExcludeRules
+
+
+def with_rules(conf: Conf, rules: RuleSelection) -> Conf:


ericeil · 2026-09-28T18:36:21Z

+#[inline] ^<anchor_lang::accounts::program::Program<T> as core::convert::TryFrom<&solana_program::account_info::AccountInfo>>::try_from$
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+#[inline] ^<anchor_lang::accounts::unchecked_account::UncheckedAccount as core::convert::AsRef<solana_program::account_info::AccountInfo>>::as_ref$


These are taken from a repo we use as a starting point for hand-written specs; I originally had a whole system for automatically pulling those over here and then editing them (we need some small changes vs. the files in that repo) but it got really messy and I finally settled on just keeping separate copies in this repo.

ericeil · 2026-09-28T18:51:07Z

@@ -0,0 +1 @@
+;; Summaries for anchor functions


This was here for symmetry, and I thought it would simplify the code elsewhere. Not sure about that any more.

ericeil · 2026-09-28T18:58:44Z

+
+
+@dataclass(frozen=True)
+class ProverSettings:


TunableConf? Not sure it's better, but at least it's obviously different :)

ericeil · 2026-09-29T01:42:19Z

+    A verification-only edit inside a dependency has to be gated on a feature that dependency
+    declares. Forwarding per-unit features (``unit_x = ["library/unit_x"]``) would give every
+    dependency a different feature set per unit. Those features are empty so they do not do that
+    (:func:`declare_unit_features`). Forwarding the one shared ``certora`` feature keeps a single
+    resolved feature set. An edit gated that way is then on for every unit, not only the one that
+    needed it.


Rewrote this

ericeil · 2026-09-29T01:52:50Z

+    if package.lib is not None:
+        lib_rel = _project_relative(package.lib.src_path, package.root)
+        source = package.lib.src_path.read_text() if package.lib.src_path.is_file() else ""
+        if _MOD_CERTORA.search(source):


yeah, this was wrong

ericeil · 2026-09-29T02:03:14Z

+        # were rewritten.
+        parts.append(
+            f";;; Platform paths rewritten for this target's generation "
+            f"({len(dialect.aliases)} aliases) — see composer/spec/cvlr/env_paths.py\n"


Oh, good point; thanks for spotting that!

ericeil · 2026-09-29T02:12:09Z

+
+    core: CrateRelease
+    #: The chain crate every project on this chain declares.
+    chain: CrateRelease


It's the CVLR "chain crate".

ericeil · 2026-09-29T02:14:58Z

@@ -0,0 +1,282 @@
+"""Which published CVLR releases count as current, for each chain.


Yeah, I think there was some reason for this in an earlier version, but it clearly should be in the cvlr module.

jtoman

looks good. I admit I lost track of what you're actually trying to accomplish; but I believe this code probably does that. I simply lack the cargo background to critically evaluate whether what you're doing is a good idea. Like I said; if what you mean to do is right, this code does it.

jtoman · 2026-09-29T22:20:50Z

+        """``origin`` names the file in a :class:`MalformedManifest`."""
+        try:
+            self._document, self.manifest = _parsed(text)
+        except _UNPARSEABLE as exc:


this works????? Holy heck! Wow TIL.

jtoman · 2026-09-29T22:32:11Z

+    ``tunable``, so a change to the fixed part invalidates a stamp too.
    """
-    digest = hashlib.sha256(dump_conf(settings_conf(settings)).encode()).hexdigest()[:16]
+    digest = hashlib.sha256(dump_conf(tunable_conf(tunable)).encode()).hexdigest()[:16]


there is a string_hash utility function kicking around somewhere. it basically does this, but why invent the wheel right?

jtoman · 2026-10-01T02:12:15Z

@@ -641,122 +671,126 @@ def _plan_package_manifest(
        enables += [
            f"{dep.name}/{DEFAULT_FEATURE}" for dep in local_dependencies(workspace, package)
        ]


this isn't a complaint, but this looks very similar to what's above in feature forwarding. I think I don't know enough about cargo to understand why you're doing it in two places

…ng_hash The program's and each local library's `certora` feature turn on the same crate-local things (the CVLR crates, plus no-entrypoint when declared). _certora_feature now builds that list for both; the program adds its `lib/certora` forwards on top. The comment there now says why both exist: cargo features don't cross crate boundaries. conf_history used an inline sha256-truncated-to-16 that is exactly composer.spec.util.string_hash, so it calls that instead. The token is unchanged, so existing stamps stay valid. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Conflicts in composer/spec/source/{prover,author,artifacts}.py, all from #215 (multi-spec buffers) meeting this branch's typed rule selection: - master's RuleSelection TypedDict is the persisted ProverRunLog.rules record and submit_buffer's job key; it keeps that role under this branch's name, RuleSelectionRecord. RuleSelection is the typed conf scope from composer.prover.conf. - _apply_selection is replaced by _scope_of, which turns a record into a RuleSelection; buffer_conf passes it and its msg through prover_config_overlay. - setup_prover_config_in keeps this branch's `rules: RuleSelection`; WrappedProverRunner validates with rule_selection as before. - master's new conf writers (buffer_conf, the per-entrypoint conf dump) use dump_conf. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Nothing in this change reads them. They reach a build only through the scaffold, and nothing here scaffolds. The directives found since #248 are held on the development branch and will be submitted together, with the measurement that justifies them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…ht back-port Backend plan: the scaffold's ownership rule (the harness under src/certora/ is AutoProver's and is rewritten when it differs; the project's files are only added to), the starting tuning layers maintained here rather than vendored, no package layer, starting_env, and forks.py in place of the fork half of munge.py. Landing plan: P1 is #248, and carries forks.py, the env half of tuning.py and composer/prover/conf.py with its CVL callers; the refresh script is gone. munge.py lands whole in P3a, tuning.py is the file split between P1 and P3b, and #243 was closed rather than grown into P1. #248 does not yet carry the cvlr-preflight script or the entry.py hunks. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The plan for replacing the CVLR source mount with a documentation corpus and a research sub-agent. Three pieces: `cvlr_api_kb` extracted from rustdoc and compile-gated, `cvlr_kb` re-scoped to the manual and practice it already holds, and a `cvlr_research` agent that answers out of both. Two corpora rather than one because what the source mount really provided was an authority ordering — a channel derived from the code, outranking one written by hand — and a retrieval hit carries no provenance, so a merged corpus cannot express it. Their regeneration lifecycles differ too: ingest is a plain INSERT under a unique constraint, so a rebuild means dropping a schema, and a CVLR bump should not take the hand-curated entries with it. The version question is settled by pinning: one CVLR line at a time, the way a Prover release ships one CVL, with a project on another line refused rather than accommodated. §2.6 records that half as landed — it was the first step, it went into #248 where those files are still under review, and it is what makes a single-version corpus a guarantee rather than an assumption. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… work #239, #240, #244 and #248 were pulled out of this branch and changed in review before merging. Replaying the branch's own history of those files onto master conflicts on every commit and means nothing, so the rebase replayed every commit without its changes to the files both sides touch, and this commit brings those files to their merged state in one step: a three-way merge of master and the branch tip, based on the last state the two shared (the PR commit or master commit closest to the branch's copy). Master's version stands wherever the branch carried only a mirror or an intermediate state of the review: the prover options (app/server/ global_timeout rather than LocalRun | CloudRun), `cargo.metadata`'s pydantic models and `Workspace.read`, `TunableConf`, `chain_crate`, `RuleSelection.apply_to`, the CVL author and prover modules, and ragbuild. The branch's own later work is carried onto those versions: * cvlr/reference: `ProgramModel`, `models` / `companions`, and `withholding`, under master's `chain_crate` name. * cvlr/conf: `OptimisticLoop` with its reason, and the `CollectUnsatCore` purpose, on `TunableConf`. * cvlr/crates: `roots()` goes, as it did with the CVLR source mount. * prover/core and cloud: the alert report fetch and `external_functions`, `UnanalyzedCexHandler`, and the job link in a cloud failure, beside master's retried fetch. * report_prover: master's multi-run CVL fetcher (#232) is kept; `make_run_link_fetcher` is the single-run fetcher S4 (#241) made of `make_prover_fetcher`, for CVLR. `job_input` stays for the unsat-core fetch; the verdict fetch already rewrites `/jobStatus/` to `/output/`. * pipeline/core: pinned runs alongside #228's extraction failures. * the inlining env additions, the C7b manifest ingestion in populate_cvlr_rag.sh (ingesting the manual with `--corpus cvlr`), and the P2/P3b halves of test_cvlr_plumbing.py ported onto master's P1 half. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

#248 landed the preflight layer under the names its review settled on, and the rest of the backend still called it by the old ones: * `composer.spec.cvlr_reference` is `composer.spec.cvlr.reference`. * `ProverSettings` / `settings_conf` are `TunableConf` / `tunable_conf`. * `read_workspace(...)` is `Workspace.read(...)`; the test fake patches the classmethod, as test_cvlr_scaffold does. * A cargo feature is a `CargoFeature`, so `HarnessModule.feature` and `UnitTarget.features` say so. * `CvlrSources` has no `core`; the family test checks names and versions. * `declare_unit_features` edits the manifest as TOML and annotates the table it adds, so the tree test reads the result as TOML. And two that came with the merge rather than with #248: the CVLR backend reads verdicts through `make_run_link_fetcher`, and `cloud.results_api` is public again because `verify`'s vacuity analysis fetches through it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

P1 merged as #248 after 61 review commits, and the branch is rebased onto it. The plan now says what landed and how it differs from the description (the reference set's new home and vocabulary, `cargo.manifest`, the harness templates, the symbols fixture), and that the console script and the `entry.py` parser go to P7. It also lists the branch's later work on files P1 now owns and assigns each change to the PR it rides. The manifest-path fix and the dead `CvlrSources.roots()` are for master now. Two other merges change the plan. #232 rewrote the CVL verdict fetch, so #241 conflicts, `job_input` is needed only by P3b's unsat-core fetch, and the single-run fetcher moves to P7. #244 landed the corpus with its template, which empties P6's corpus hunks. The build-environment drop was described as smaller than it is: `CvlrFormalizer` overrides the hook, and the tape test reads the field. Rule 4 gains the replay-and-reconcile method this rebase used, and its one trap: a merge base taken from an unmerged PR silently drops that PR's work. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…rdicts (#258) * cvlr: build a hand-written CVLR harness for SBF, submit it, and read the verdicts back The second slice of the Solana backend. #248 resolves a Cargo project and scaffolds a verification harness into it. This change builds that harness for the Solana VM, submits it to the Solana Prover, and reads the per-rule verdicts back. It is the deterministic half of the backend, with no agent anywhere in the path: a rule someone wrote by hand goes in, and verdicts come out. `tests/test_cvlr_end_to_end.py` is that sentence as a test. It clones Certora/SolanaExamples, builds the two minimal CVLR projects, submits them, and compares the verdicts against the expected-verdict files those projects' own CI uses. That includes the rule meant to fail and the rule meant to fail sanity. `tests/test_cvlr_loop_bound.py` submits a probe and measures what raising the loop bound does. Both are `expensive` and skip, naming what is missing, when there is no SBF toolchain. * `composer/cargo/sbf.py` runs `cargo certora-sbf` under the command sandbox, warms the platform-tools cargo it will actually use, parses the build manifest the prover needs, and writes the build script the prover re-runs. * `composer/spec/cvlr/prover.py` writes a submission's conf and build script beside each other, and runs it through the shared `run_prover`. * `composer/spec/cvlr/rules.py` reads the rule names a harness declares, so a submission can select rules. * `composer/prover/core.py` gains `UnanalyzedCexHandler`, which renders verdicts without asking an LLM to analyze them. A gate that compares against an expected file has nothing for an LLM to do. * The starting tuning files gain the directives found since #248. These inline Anchor's account validation, `system_program::transfer` and `AccountInfo::try_borrow_lamports`, and inline `AccountInfo::realloc` instead of summarizing it. This change submits the first builds, which is where a directive changes a verdict. `test_cvlr_env_paths.py`'s directive counts follow. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: address the PR 258 review * Name each submission's build script and command file by its stem. Two submissions in one tree used to share `confined_build.py`/`.json`, so the second overwrote the first's command. The two-units test now gives each unit different features and checks that each script carries its own. * Grant the platform-tools root the build argv names. `rust_build_policy` granted only the default locations, so a root set by `CERTORA_PLATFORM_TOOLS_ROOT` passed the host check but was unreadable in the confined child. `CargoSession.run_confined` and the new `CargoSession.backend_spec` take `extra_ro` for this. * Parse the build manifest with a strict pydantic model that matches `certoraParseBuildScript`, including "string or list of strings" for the Solana file keys. A field of the wrong type is now rejected at parse time, not later as an unhandled error or a string split into characters. * Move the build script into `composer/cargo/sbf_build_script.py`, copied with `importlib.resources`. It reads the command file beside itself. * Default `Submission.features` to `(DEFAULT_FEATURE,)` and drop `resolved_features`. * Fix the `realloc` directive's comment. It now names `realloc` and says that `realloc(n, true)` reaches the CERT-10184 crash. * Define the `cvlr_confinement` fixture the end-to-end test uses: the production launcher, skipped when it cannot confine. * Drop comments that cite docs not in this tree. * Remove `tests/test_cvlr_loop_bound.py` and its probe. Its scenario is not in this tree, and what it checks belongs to the authoring loop. Remove `composer/spec/cvlr/rules.py` and its tests too: the loop-bound test was its only caller, and it should return with the publish gate that uses it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: make a submission's cex handler the caller's choice run_submission and submit no longer fall back to a no-analysis handler when given none. A caller now says whether a violated rule is explained. Every CVL call site of run_prover already does, and a default that skips analysis is easy to inherit by accident in a production path. That leaves UnanalyzedCexHandler with no caller in this change, so it moves to the change that brings its first production caller: the unsat-core diagnostic run. The end-to-end test, which reads only verdicts, passes a local stub. composer/prover/ is now unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: leave the starting tuning files as #248 landed them Nothing in this change reads them. They reach a build only through the scaffold, and nothing here scaffolds. The directives found since #248 are held on the development branch and will be submitted together, with the measurement that justifies them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: give each submission its own target directory, and name the build script relatively * Build each submission into `<workspace target>/certora/<stem>`. The prover reruns the build script during its local phase, so `run_submission` builds too. Submissions of one crate with different features shared one target directory, so each rerun rebuilt the artifact over the other's, and a prover could upload the `.so` another submission had just built. The directory is set by running the build as `env CARGO_TARGET_DIR=... cargo certora-sbf`: the tool has no flag for it and reads the artifact path from its own `cargo metadata` call, and the launcher scrubs the child's environment. `Submission` gains `target_directory` for this. * Require that target directory to be absolute. `cargo certora-sbf` resolves a relative one against the working directory for `cargo metadata` and against the package directory for the build, so the manifest named an artifact that was never built. The live end-to-end run found this. * Fold the gate's and the build script's shared arguments into one `SbfBuild` value with `argv()`, so both runs take the same build by construction. * Name the build script in the conf relative to the workdir, as `RunOverlay` documents and as CVL confs name their specs. * Make the build script refuse to run outside the tree it was written in. Its command names that tree, the target directory and the confinement grants by absolute path, so a copy would build the original tree. * Correct `prepare_submission`'s account of which half touches the tree: the sources must stay put until `on_prover_link` fires. * Spell `CONF_DIR` with `composer.layout.CERTORA_DIR`, as the CVL backend does. * Test the build script by running it: its working directory, its handling of `--cargo_features`, and its refusal to run from a copy. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * comments: rewrite the CVLR submission comments in plain English Keep the constraints. Drop the asides. * cvlr: build every submission in the workspace's target directory f963172 gave each submission a target directory of its own, so that two submissions of one crate with different features could not replace each other's .so between the gate build and the prover's rerun. That costs a cold dependency build per submission, and a target directory's worth of disk for each one (about 1 GB for an Anchor program). Builds share the workspace's target directory again. The ordering constraint moves to the caller, and prepare_submission's docstring states it: from the start of the local half until on_prover_link fires (or run_submission returns without a link), nothing else may build the crate or change the tree. A single submission, which is all this change makes, meets that trivially. The concurrent authoring loop will hold its build permit over that span. With no target directory set, SbfBuild drops target_dir and the env CARGO_TARGET_DIR prefix, and Submission drops target_directory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: say which files a submission needs left alone prepare_submission's contract forbade changing the tree. What the prover's rerun depends on is narrower: the files the build compiles, and the target directory it writes. The conf is not among them, and the end-to-end test rewrites it between the two halves. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * Cleanup dataclasses * cvlr: simplify build configuration and user-facing messages * Drop the CERTORA_PLATFORM_TOOLS_ROOT override. Nothing sets it, and supporting it needed the --platform-tools-root argv, the extra read-only grants, and CargoSession's extra_ro parameters. The root is now one constant, recipes.PLATFORM_TOOLS_ROOT (~/.cache/solana), which rust_build_policy already granted. * Make the SBF build timeout configurable with AUTOPROVER_SBF_BUILD_TIMEOUT, following AUTOPROVER_GLOBAL_PROVER_TIMEOUT. It is resolved when the build runs; the timeout_s parameters, which no caller set, are gone. * Give the prover's rerun of the build the same timeout. The command file now carries timeout_s, and the build script kills the build's whole process group when it expires, exiting 124. * Shorten the error messages that can reach users: no directories, confinement details, or raw tool output. The detail is logged, and kept as the exception's cause where there is one. * Make Submission.stem and Submission.msg required. A shared default stem let two submissions overwrite each other's conf and build script, and the EVM path already requires a message. * Give the two Solana read-only grants accurate comments. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: parse the build script's prover flags with argparse The script scanned sys.argv for --cargo_features and ignored every other flag. It now declares the flags certoraRun passes (--json, -l, --cargo_features) and rejects any other: an undeclared flag such as --arch may change what the prover expects to get built, so silently dropping it could build the wrong artifact. No branch sets solana_sbf_arch, so --arch is not expected today. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: raise on a malformed build manifest instead of reporting a compile failure The manifest comes from cargo certora-sbf and the crate's [package.metadata.certora], neither of which the authoring agent edits. Reporting it as CompileFailed handed the agent an error it cannot fix, with exit_code 0 standing in for "the compile did not fail". It now propagates like PlatformToolsMissing, as an operator-facing failure. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * cvlr: keep the build script, its command file and the conf out of the build's reach The prover runs the build script unconfined, and the script takes its confinement (`argv_prefix`) from the command file beside it. Both lived in `.certora_build/` under the workdir, and the conf in `certora/confs/`, all of which the confined build can write. A hostile `build.rs` from the gate build, or from another submission sharing the tree, could drop the prefix so the prover's rerun ran unconfined, or plant a symlink so the trusted write landed outside the tree. * `write_build_script`, `write_submission`, `prepare_submission` and `submit` take `into`, a directory the caller owns. `write_build_script` refuses one a confined build can write, checked with the new `CargoSession.build_can_write` against the policy's rw grants after resolving symlinks. * The conf is written beside the script and names it by absolute path. `BUILD_DIR` and `CONF_DIR` are gone. This reverses f963172's relative naming: the script no longer lives in the tree the prover runs in. * Drop the build script's "different working tree" check. It assumed the script sat inside the workdir, and it never guarded against tampering. * command-sandbox.md says a stored `argv_prefix` is only as trusted as its file. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

…ht back-port Backend plan: the scaffold's ownership rule (the harness under src/certora/ is AutoProver's and is rewritten when it differs; the project's files are only added to), the starting tuning layers maintained here rather than vendored, no package layer, starting_env, and forks.py in place of the fork half of munge.py. Landing plan: P1 is #248, and carries forks.py, the env half of tuning.py and composer/prover/conf.py with its CVL callers; the refresh script is gone. munge.py lands whole in P3a, tuning.py is the file split between P1 and P3b, and #243 was closed rather than grown into P1. #248 does not yet carry the cvlr-preflight script or the entry.py hunks. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The plan for replacing the CVLR source mount with a documentation corpus and a research sub-agent. Three pieces: `cvlr_api_kb` extracted from rustdoc and compile-gated, `cvlr_kb` re-scoped to the manual and practice it already holds, and a `cvlr_research` agent that answers out of both. Two corpora rather than one because what the source mount really provided was an authority ordering — a channel derived from the code, outranking one written by hand — and a retrieval hit carries no provenance, so a merged corpus cannot express it. Their regeneration lifecycles differ too: ingest is a plain INSERT under a unique constraint, so a rebuild means dropping a schema, and a CVLR bump should not take the hand-curated entries with it. The version question is settled by pinning: one CVLR line at a time, the way a Prover release ships one CVL, with a project on another line refused rather than accommodated. §2.6 records that half as landed — it was the first step, it went into #248 where those files are still under review, and it is what makes a single-version corpus a guarantee rather than an assumption. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… work #239, #240, #244 and #248 were pulled out of this branch and changed in review before merging. Replaying the branch's own history of those files onto master conflicts on every commit and means nothing, so the rebase replayed every commit without its changes to the files both sides touch, and this commit brings those files to their merged state in one step: a three-way merge of master and the branch tip, based on the last state the two shared (the PR commit or master commit closest to the branch's copy). Master's version stands wherever the branch carried only a mirror or an intermediate state of the review: the prover options (app/server/ global_timeout rather than LocalRun | CloudRun), `cargo.metadata`'s pydantic models and `Workspace.read`, `TunableConf`, `chain_crate`, `RuleSelection.apply_to`, the CVL author and prover modules, and ragbuild. The branch's own later work is carried onto those versions: * cvlr/reference: `ProgramModel`, `models` / `companions`, and `withholding`, under master's `chain_crate` name. * cvlr/conf: `OptimisticLoop` with its reason, and the `CollectUnsatCore` purpose, on `TunableConf`. * cvlr/crates: `roots()` goes, as it did with the CVLR source mount. * prover/core and cloud: the alert report fetch and `external_functions`, `UnanalyzedCexHandler`, and the job link in a cloud failure, beside master's retried fetch. * report_prover: master's multi-run CVL fetcher (#232) is kept; `make_run_link_fetcher` is the single-run fetcher S4 (#241) made of `make_prover_fetcher`, for CVLR. `job_input` stays for the unsat-core fetch; the verdict fetch already rewrites `/jobStatus/` to `/output/`. * pipeline/core: pinned runs alongside #228's extraction failures. * the inlining env additions, the C7b manifest ingestion in populate_cvlr_rag.sh (ingesting the manual with `--corpus cvlr`), and the P2/P3b halves of test_cvlr_plumbing.py ported onto master's P1 half. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

#248 landed the preflight layer under the names its review settled on, and the rest of the backend still called it by the old ones: * `composer.spec.cvlr_reference` is `composer.spec.cvlr.reference`. * `ProverSettings` / `settings_conf` are `TunableConf` / `tunable_conf`. * `read_workspace(...)` is `Workspace.read(...)`; the test fake patches the classmethod, as test_cvlr_scaffold does. * A cargo feature is a `CargoFeature`, so `HarnessModule.feature` and `UnitTarget.features` say so. * `CvlrSources` has no `core`; the family test checks names and versions. * `declare_unit_features` edits the manifest as TOML and annotates the table it adds, so the tree test reads the result as TOML. And two that came with the merge rather than with #248: the CVLR backend reads verdicts through `make_run_link_fetcher`, and `cloud.results_api` is public again because `verify`'s vacuity analysis fetches through it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

P1 merged as #248 after 61 review commits, and the branch is rebased onto it. The plan now says what landed and how it differs from the description (the reference set's new home and vocabulary, `cargo.manifest`, the harness templates, the symbols fixture), and that the console script and the `entry.py` parser go to P7. It also lists the branch's later work on files P1 now owns and assigns each change to the PR it rides. The manifest-path fix and the dead `CvlrSources.roots()` are for master now. Two other merges change the plan. #232 rewrote the CVL verdict fetch, so #241 conflicts, `job_input` is needed only by P3b's unsat-core fetch, and the single-run fetcher moves to P7. #244 landed the corpus with its template, which empties P6's corpus hunks. The build-environment drop was described as smaller than it is: `CvlrFormalizer` overrides the hook, and the tape test reads the field. Rule 4 gains the replay-and-reconcile method this rebase used, and its one trap: a merge base taken from an unmerged PR silently drops that PR's work. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil and others added 3 commits September 22, 2026 09:45

comments: describe the CVLR preflight code as it is

e323b0e

Keep the constraints. Drop change history, restatements, and pointers at docs and modules this branch does not have.

ericeil changed the title ~~CVLR: resolve a Cargo project for verification~~ Add the Solana Prover preflight step Sep 22, 2026

ericeil and others added 14 commits September 22, 2026 10:31

Simplify comment

76ebc6a

Update comment

c6116d3

Update comments

420d2eb

Comment

e3c02d5

Comments

cab3b22

cvlr: explain the Anchor and fixed forks for a reader new to Anchor

ec36b5a

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

ericeil marked this pull request as ready for review September 23, 2026 18:19

ericeil requested review from chandrakananandi and jtoman September 23, 2026 18:19

ericeil and others added 2 commits September 24, 2026 14:59

jtoman requested changes Sep 28, 2026

View reviewed changes

ericeil and others added 4 commits September 28, 2026 11:43

Revert accidental removal

50bd97b

ericeil and others added 10 commits September 28, 2026 20:03

cvlr: the workspace-pin note does not name _check_pins

99ca3da

The note is scaffold output for the project author; a private function name is not theirs to follow. It now says the release is checked on its own. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

cvlr: a unit layer passed to compose_env is appended as given

7394d61

The default became None in fd4ba89, but the check still read a blank string as absent too. None is now the only absence. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

ericeil commented Sep 29, 2026

View reviewed changes

ericeil requested a review from jtoman September 29, 2026 16:51

jtoman approved these changes Oct 1, 2026

View reviewed changes

ericeil and others added 2 commits October 1, 2026 09:38

ericeil merged commit 2eb4a39 into master Oct 1, 2026
4 checks passed

ericeil mentioned this pull request Oct 1, 2026

Build a CVLR program, submit it to the Solana Prover, and read the verdicts #258

Merged

ericeil mentioned this pull request Oct 2, 2026

Use one rule-selection type for conf scoping and run history #259

Merged

		@@ -0,0 +1,282 @@
		"""Which published CVLR releases count as current, for each chain.

		type RuleSelection = InheritRules \| SelectRules \| ExcludeRules


		def with_rules(conf: Conf, rules: RuleSelection) -> Conf:



		def compose_env(
		family: EnvFamily, *, unit_layer: str = "", dialect: PathDialect = PathDialect()



		@dataclass(frozen=True)
		class ProverSettings:

Conversation

ericeil commented Sep 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ericeil left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ericeil commented Sep 22, 2026 •

edited

Loading