[ericeil]

Point preflight at a Solana program on the split solana-* 3.x crates and today it refuses it: master's reference set has one platform generation, solana-program 2.x, and builds with platform-tools v1.43, whose cargo cannot parse the edition-2024 manifests the SDK 3 crates use. This PR gives each Solana platform generation its own reference set, picks the one the target is on, and builds every generation with platform-tools v1.53 under one host toolchain.

Generation	cvlr-solana	Specializations
solana-* 3.x	0.6.0	cvlr-solana-stake, cvlr-spl-token 0.6.0
solana-program 2.x	0.5.1	cvlr-solana-stake, cvlr-spl-token 0.5.1
solana-program 1.18	0.4.6	none

All three are on the cvlr 0.6.2 core, and all are published on crates.io.

Why is this needed?

A chain crate works only with its own generation's AccountInfo, so one CVLR line can't serve every target. Master refuses anything that isn't on 2.x, including the Solana stake program, which is on SDK 3. Each step below came out of running that program or a large Anchor program through preflight:

• v1.53. v1.43's cargo is 1.79, and SDK 3 lockfiles are full of edition-2024 manifests. v1.53's rustc 1.89 names the allocator shims __rustc::__rust_alloc. So the never-inline directives in cvlr_inlining_core.txt and the frames SOLANA_TRACE drops now accept both spellings.
• One host toolchain. HOST_RUST_TOOLCHAIN replaces the target's rust-toolchain.toml for every cargo command. That pin exists for the project's own builds. Following it fails wherever the runtime user can't write the rustup home, because a toolchain that isn't installed can't be installed. The program itself is compiled by the platform tools' rustc either way.
• An SBF check, not a host check. The preflight gate runs cargo check for the SBF target with the platform tools' cargo, rustc and C tools (sbf_check). The host can't always compile what the chain build does: from rustc 1.77, u128 is 16-byte aligned on x86_64, so a program's own layout assertions can fail there and hold on SBF.
• The never-inline blanket stays on the monolith. Master widened ^solana_program::.*$ to every split crate. A function that isn't inlined is external: it returns an arbitrary value and writes nothing. So Sysvar::from_account_info never returned Ok, and the stake program's interface crate became an oracle. Unwidened, the split crates are analyzed.
• No allocator conflict. The stake program calls entrypoint! unconditionally and has no no-entrypoint feature. Its allocator then writes the heap at a fixed address, and a rule that also allocates fails with Prover error 3309. The scaffold enables custom-heap from certora for such a package.
• Smaller fixes. The manifest editor can now edit a [package] table split by another table, as stake's is. $CERTORA_PLATFORM_TOOLS_ROOT is honoured and passed to cargo certora-sbf explicitly, because the launcher drops it. Preflight's cargo metadata fetches into the confined run's cargo home, so the gate's warm step doesn't fetch it again, with the cold-fetch timeout.

Where to start

1. The reference sets. composer/spec/cvlr/reference.py: SOLANA_V3, SOLANA_V2, SOLANA_V1_18, and generations(), which replaces reference_for(). The SDK 3 path aliases were read off the stake program's symbols, tests/data/stake_sdk3_sbf_symbols.txt. GitCommit and CommitPatch let a release be read from its commit before it is on crates.io. No shipped set uses them today; the scaffold tests do.
2. Picking the generation. select_generation and _read_platform in composer/spec/cvlr/scaffold.py, and select_package in preflight.py. The evidence is the resolved graph's normal dependencies of the target's library (Workspace.linked_into in composer/cargo/metadata.py). A copy only a sibling member or a dev-dependency pulls in is never compiled with the harness. Below 2.0, a generation is keyed on major.minor, because Solana's 1.x minors broke compatibility.
3. The toolchain. PLATFORM_TOOLS_VERSION and HOST_RUST_TOOLCHAIN in composer/spec/cvlr/conf.py. Then CargoSession.toolchain / check_with (HostCheck | CrossCheck) in composer/cargo/session.py, and sbf_check in composer/cargo/sbf.py. The build script carries the toolchain to the Prover, which runs it with its own environment. SandboxConfig.env carries it into a confined child.
4. Tests. tests/test_cvlr_reference.py, test_cvlr_scaffold.py (generation selection, the 1.18 and SDK 3 cases, custom-heap, the commit patches), test_cvlr_env_paths.py (each alias against real symbol tables) and test_cvlr_plumbing.py (the toolchain and the SBF check). None needs a toolchain or the network.

The vault and examples tests that build for SBF (tests/test_cvlr_preflight.py, tests/test_cvlr_end_to_end.py) are expensive and were not run for this PR. They need platform-tools v1.53 installed, and the end-to-end test needs SOLANA_EXAMPLES_REPO. Run them by hand before merging.

🤖 Generated with Claude Code