Expand Solana CVLR documentation with practical-guide pages by johspaeth · Pull Request #471 · Certora/Documentation

johspaeth · 2026-05-05T09:17:30Z

Summary

Substantial expansion of the Solana CVLR documentation. New dedicated
pages for the day-to-day topics readers actually hit (accounts, mocks,
nondet, parametric rules, methodology, anchor) and a rework of the
existing pages (speclanguage.md, usage.md) so they stay narrow.

New pages under "Writing specifications":
- nondet.md — the Nondet trait, enums, Pubkey helpers,
  alloc_*_havoced, bounded vectors.
- mocks.md — four mocking patterns (full swap, cvlr::mock_fn,
  trait indirection, cvlr_hook_on_exit) plus the msg! stub.
- accounts.md — cvlr_deserialize_nondet_accounts, POD reads,
  sysvar / clock helpers, the pre/post snapshot pattern.
- anchor.md — Anchor-specific harness helpers (split out of
  accounts.md).
- parametric-rules.md — trait-parameterised harnesses and
  macro_rules!-driven setup; hook-based invariant tracking.
- methodology.md — practical guidelines (sanity, vacuity, conf
  hygiene, antipatterns).
Reworked existing pages:
- usage.md — folded the originally separate project-setup.md
  into the master usage.md (project setup + run-time configuration
  in one page); added the source-code-leakage warning for sources
  uploads.
- speclanguage.md — focused on the language reference; deduped
  against the new pages (multi-assert moved to methodology, NativeInt
  examples consolidated).
- index.rst — toctree split into "Setup and tooling" and
  "Writing specifications".
Polish pass — grammar / spelling cleanup across the new pages.

🤖 Generated with Claude Code

Enriches the existing Solana docs with deeper coverage of CVLR/cvlr-solana patterns drawn from real specifications. The high-level reference (speclanguage.md) gains the prelude table, all assert variants, expanded satisfy/assume guidance, clog!/CvlrLog, and mathint::NativeInt. Six new pages cover project setup (Cargo features, layout), nondet beyond primitives, mock patterns (full swap, cvlr::mock_fn, trait indirection, cvlr_hook_on_exit), Solana accounts (cvlr_deserialize_nondet_accounts, Anchor harnesses, clock helpers, pre/post snapshots), parametric rules (CvlrProp trait, macro_rules! patterns, hook-based invariant tracking), and methodology (15 practical guidelines on property IDs, sanity rules, scope, conf hygiene, antipatterns). The TOC is split into "Setup and tooling" and "Writing specifications" sections. Co-Authored-By: Claude <noreply@anthropic.com>

The Cargo.toml feature-gate setup, the recommended source-tree layout, and the bounded-vectors primer each had two or three near-identical copies across mocks.md, methodology.md, and parametric-rules.md. Replace the duplicates with one- or two-sentence pointers to the canonical location (project-setup.md and nondet.md). Net diff removes ~88 lines without losing any unique content. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Anchor wrappers (cvlr_anchor_account / cvlr_anchor_account_try_from / into_signer! / into_program! / cvlr_anchor_new_context!) and the Anchor end-to-end harness example are not part of cvlr-solana's account primitives — they are project-local helpers on top of those primitives. Move them to a dedicated solana/anchor.md page so accounts.md stays focused on the underlying AccountInfo machinery, and add the new page to the "Writing specifications" toctree. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

The earlier docs invented their own prover-args set, paths, and loop_iter default. Realign to what https://github.com/Certora/solana-spec-template ships in confs/run.conf and the package.metadata.certora block its setup script writes: - prover_args: -unsatCoresForAllAsserts true / -solanaSkipCallRegInst true / -solanaTACOptimize 2 / -solanaStackSize 8192 / -solanaTACMathInt true (replacing the -solanaOptimistic* set, TACOptimize 3, and the random-seed example that were in the old defaults). - loop_iter: 1 (was 3); reframe the "Pin loop_iter" advice accordingly. - solanaStackSize: note the template ships with 8192, so the "bump only when you hit stack errors" advice now starts from that baseline. - Random-seed -s flag: reframe as opt-in, not in the default conf. - package.metadata.certora paths: src/certora/envs/cvlr_inlining.txt (singular) instead of certora/summaries/cvlr_inlining_core.txt. - Reframe inlining/summaries: not optional fine-tuning to "start without" but required scaffolding to start from the template's set. - Directory layout: confs/ + envs/ under src/certora/, matching the template; note the older crate-root layout is still supported. Also surface the spec template at the index level and in methodology.md §15, so users see it as the recommended starting scaffold. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Files listed in [package.metadata.certora].sources are uploaded to the Certora cloud to power Jump to Source in the rule report and persist there. A publicly shared report URL exposes every uploaded source file, which is a leakage risk for closed-source programs. Add a prominent warning in project-setup.md (the canonical place where sources is introduced) explaining the trade-off, why JTS needs the upload, and the two practical consequences (trim aggressively; audit report URLs before sharing publicly). Link back from the brief methodology.md mention. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Both files duplicated the [package.metadata.certora] block, the cargo certora-sbf description, and example .conf files. Merge the project-setup content as a "Project Setup" section inside usage.md (anchored solana_project_setup so existing cross-references keep resolving) and drop the standalone file. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Three overlap fixes: - Remove speclanguage.md "Multi-assert mode" section. Strict subset of methodology.md §9 (which has the conf example) and options.md --multi_assert_check (the canonical flag reference). - Trim speclanguage.md "Putting it together" — drop the repeated CvlrLog impl that was just shown 50 lines above in the CvlrLog section. - Trim methodology.md §7 NativeInt — drop the duplicated lift/assume/ assert example, keep the when/when-not guidance, cross-ref speclanguage for the API and worked example. Net: -38 / +10 lines. Speclanguage owns the API; methodology owns the guidelines. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Mix of editorial cleanup on the new CVLR pages and grammar/spelling fixes: - methodology.md: rename §2 to "Don't disable the default sanity check"; rebuild §4 (process_instruction handler scoping) sentence flow; tighten §9, §10, §13, §14; replace `I.e.` with `That is,`; drop trailing comma + whitespace in conf JSON. - usage.md: split run-on inlining/summaries paragraph; fix subject-verb agreement; tidy lib.rs bullet. - mocks.md: rebuild broken intro sentence; fix `when="..."` paragraph (drop incorrect comma before restrictive `that`, `when enable` → `when enabled`); add missing article in "swap in an implementation". - nondet.md: fix `symbolic/("havoced")` → `symbolic ("havoced")`; fix `cannot precise reason` → `cannot precisely reason`; number agreement and missing article in bounded-vectors paragraph. - parametric-rules.md: replace `cvt_hook_end` alias with `cvlr_hook_on_exit` to match mocks.md; small re-phrasing of intro. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Bring the Solana docs in line with the cvlr-spec layer introduced in cvlr 0.6 (CvlrFormula, predicates, lemmas, cvlr_spec!, cvlr_rules!). Add a new spec.md covering the spec primitives end-to-end, prune 0.4-era residue (CvlrProp parenthetical, cvt_assert! rename note, acc_infos_with_mem_layout!), and revise informal phrasings to a reference-doc register. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

- Tighten informal phrasings to a reference-doc register (drop "copy-paste piling up", "fight the Prover", "rope to hang itself", "Prover is happier", "shines when", etc.) - Convert British spellings to US English (specialised, generalised, organised, behaviour, modelled, parameterised, stabilises, etc.) - Wrap free-text impl/impls in backticks for code formatting - Spell out a few prose abbreviations (two-arg -> two-argument, prose confs -> configs) - Fix four MyST cross-reference warnings in spec.md by adding explicit (solana_spec_*)= anchors and switching the TOC to {ref} syntax with custom display text - Extend spelling_wordlist.txt with domain terms (Pubkey, multisig, syscall, sysvars, deserializer, antipatterns, etc.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

johspaeth

Round of reviews.

johspaeth · 2026-05-08T09:03:28Z

@@ -0,0 +1,165 @@
+(solana_anchor)=


@1arie1 Has there been any major update in API for cvlr for Anchor, that you see missing here?

I.e. after the project that used these helpers, we said we would move them. Has this happened?

no. after I reviewed the changes, the only changes that had to happen were in anchor itself. I've created custom versions of anchor with the needed patches.

there was nothing that could be reused at cvlr level.

johspaeth · 2026-05-08T09:04:07Z

+| A loop bounded by a configurable constant                  | Inline if small (≤ 4); else mock     |
+| A CPI                                                      | Mock (Pattern D — track the call)    |
+| Heavy table-driven math                                    | Mock (Pattern A or B with `nondet`)  |
+| A function whose result the rule does not use              | Mock with `Ok(())`                   |


This table should be removed. It rather confuses than adding value.

johspaeth · 2026-05-08T09:05:06Z

+        "-solanaSkipCallRegInst true",
+        "-solanaTACOptimize 2",
+        "-solanaTACMathInt true"
+    ]


We should better remove invalid / old flags here. We should keep it to a minimal sensible ones for demonstrating the example.

johspaeth · 2026-05-08T09:05:16Z

+
+The `[package.metadata.certora]` block in your `Cargo.toml` controls what
+`cargo certora-sbf` ships to verification. Every extra entry in `sources`
+adds compile time, so list only the crates this verification job actually


This is not true. It doesn't add compile time, but we want to keep that sources is a sensitive field to use with extra care.

johspaeth · 2026-05-08T09:06:00Z

+
+Most real Solana handlers take `&[AccountInfo]` and read/write account data.
+To verify them you need a way to produce nondeterministic accounts, read
+typed state out of them, and snapshot before/after. This page covers the


Suggested change

typed state out of them, and snapshot before/after. This page covers the

typed state out of them, and snapshot the accounts before/after of the execution of a protocol handler. This page covers the

johspaeth · 2026-05-08T09:07:40Z

+### Account-loader-flavored helpers
+
+Some projects use a trait-bound deserializer (often called something like
+`FatAccountLoader`). Where it exists, the verification harness mirrors the


Is it called Fat...? I haven't seen this / heard this.

johspaeth · 2026-05-08T09:09:34Z

+- **Forgetting to `.unwrap()` on the handler call.** Without `.unwrap()`,
+  the rule trivially succeeds even when the handler errors out — a common
+  source of vacuous "passing" rules. Always either `.unwrap()` or
+  `cvlr_assume!(result.is_ok())` and assert on the post-state.


@1arie1 Does our vacuity check discover this? Then we should mention this here.

how can I read this in a readable format? I am getting lost between comments and diffs

@1arie1 here you go https://certora-certora-prover-documentation--471.com.readthedocs.build/en/471/docs/solana/index.html

johspaeth · 2026-05-08T09:11:32Z

+The recommended starting scaffold for new projects is the
+`Certora Solana spec template <https://github.com/Certora/solana-spec-template>`_


@1arie1 is this still the case? If not, what's the state of the art way of getting started on a Solana project?

johspaeth · 2026-05-08T09:14:58Z

@@ -0,0 +1,513 @@
+(solana_spec)=


This section should reference https://github.com/Certora/SolanaExamples after we've updated it with better examples - this will be done in a separate PR.

johspaeth and others added 8 commits May 4, 2026 14:45

johspaeth requested a review from 1arie1 May 5, 2026 09:18

johspaeth and others added 2 commits May 6, 2026 11:52

johspaeth commented May 8, 2026

View reviewed changes

johspaeth requested a review from srunquist-certora May 13, 2026 08:20

	typed state out of them, and snapshot before/after. This page covers the
	typed state out of them, and snapshot the accounts before/after of the execution of a protocol handler. This page covers the

		The recommended starting scaffold for new projects is the
		`Certora Solana spec template <https://github.com/Certora/solana-spec-template>`_

Conversation

johspaeth commented May 5, 2026

Summary

Uh oh!

johspaeth 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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants