Skip to content

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

Open
ericeil wants to merge 10 commits into
masterfrom
eric/cvlr-submission
Open

Build a CVLR program, submit it to the Solana Prover, and read the verdicts#258
ericeil wants to merge 10 commits into
masterfrom
eric/cvlr-submission

Conversation

@ericeil

@ericeil ericeil commented Oct 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

#248 scaffolds a Cargo project for CVLR and checks that the scaffold compiles. This PR builds the CVLR program in that project, submits it to the Solana Prover, and reads the per-rule verdicts. The CVLR already in the project is the input.

Polling, the treeView parse, and the verdict roll-up use the shared runner from #240. certoraSolanaProver writes the same reports as certoraRun.

  • composer/cargo/sbf.py runs cargo certora-sbf in the command sandbox and writes the build script the prover reruns. That script is composer/cargo/sbf_build_script.py. Every build of a crate uses the workspace target directory, so the dependencies are compiled once. Another build of that crate replaces the .so. Each submission still has its own conf and build script.
  • The conf names the build script. With files, the prover copies the .so and not the Rust sources. The prover's own from-sources build runs unconfined, which the sandbox does not allow.
  • composer/cargo/session.py can add a read-only path. The confined build does not see CERTORA_PLATFORM_TOOLS_ROOT, so the platform-tools root is passed that way.
  • composer/spec/cvlr/prover.py writes the conf and submits it. The caller passes the Solana CLI and the counterexample handler. There is no default handler. From the start of prepare_submission until on_prover_link fires, or until run_submission returns with no link, nothing else may build that crate or change a file the build compiles. The conf is not one of those files: the prover reads it, and the build does not.
  • A failed build here is a compiler error. The same failure on the prover's rerun is a CertoraUserInputError after the upload.

tests/test_cvlr_plumbing.py checks the build arguments, the manifest, the script, and the conf, with no toolchain and no network. tests/test_cvlr_end_to_end.py submits Certora/SolanaExamples under the production sandbox and checks that project's expected verdicts. It is marked expensive. It skips when the platform tools or the sandbox are missing.

The diff is limited to composer/cargo/, composer/spec/cvlr/, and the tests.

ericeil and others added 4 commits October 1, 2026 11:37
@ericeil @claude
cvlr: build a hand-written CVLR harness for SBF, submit it, and read …
9733b85 
…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>
@ericeil @claude
cvlr: address the PR 258 review
0a65ce1 
* 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>
@ericeil @claude
cvlr: make a submission's cex handler the caller's choice
3fa2690 
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>
@ericeil @claude
cvlr: leave the starting tuning files as #248 landed them
d005e76 
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>
ericeil added a commit that referenced this pull request Oct 1, 2026
@ericeil @claude
docs: P2 is open as #258
d56c9ea 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ericeil added a commit that referenced this pull request Oct 1, 2026
@ericeil @claude
docs: P2 after the #258 review
5a0b38e 
rules.py and UnanalyzedCexHandler move to P3b, where their first
production callers are. The loop-bound test and its probe are removed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ericeil and others added 2 commits October 1, 2026 13:47
@ericeil @claude
cvlr: give each submission its own target directory, and name the bui…
f963172 
…ld 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>
@ericeil
comments: rewrite the CVLR submission comments in plain English
43044d1 
Keep the constraints. Drop the asides.
@ericeil ericeil changed the title Build, submit and read back a hand-written Solana Prover rule Plumbing to submit a Solana Prover job Oct 1, 2026
@ericeil ericeil changed the title Plumbing to submit a Solana Prover job Build a CVLR program, submit it to the Solana Prover, and read the verdicts Oct 1, 2026
ericeil and others added 3 commits October 1, 2026 14:30
@ericeil @claude
cvlr: build every submission in the workspace's target directory
a165d75 
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>
@ericeil @claude
cvlr: say which files a submission needs left alone
1821726 
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>
@ericeil
Cleanup dataclasses
e45c9c8
ericeil added a commit that referenced this pull request Oct 1, 2026
@ericeil @claude
docs: P2 is open as #258
69c7159 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ericeil added a commit that referenced this pull request Oct 1, 2026
@ericeil @claude
docs: P2 after the #258 review
1d26ff4 
rules.py and UnanalyzedCexHandler move to P3b, where their first
production callers are. The loop-bound test and its probe are removed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ericeil added a commit that referenced this pull request Oct 1, 2026
@ericeil @claude
Reconcile the branch with #258's version of the submission layer
1297536 
The branch is now stacked on #258 (eric/cvlr-submission at e45c9c8).
Its commits were replayed without their changes to the six files #258
owns, and this commit brings those files to the merged state, three-way
against #258's first commit (9733b85).

#258's versions stand for `composer/cargo/{sbf,sbf_build_script,session}.py`
and the end-to-end test. The branch had not changed those since #258 was
cut. On top of #258, the branch keeps what #258 left for later slices:

* `Submission.purpose` (`CheckVerdicts` / `CollectUnsatCore`), which the
  vacuity diagnostics need.
* The P3b cases of test_cvlr_plumbing.py, and `OptimisticLoop` in the
  tuned-conf test.

Callers move to #258's API. `SolanaToolchain` builds through `SbfBuild`.
The anchor-reach and dropped-writes probes now pass `UnanalyzedCexHandler`
to `run_submission`, which no longer defaults to it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@ericeil @claude
cvlr: simplify build configuration and user-facing messages
1370746 
* 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>
@ericeil
ericeil marked this pull request as ready for review October 2, 2026 00:42

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chandrakananandi chandrakananandi Awaiting requested review from chandrakananandi

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@ericeil