> ## Documentation Index > Fetch the complete documentation index at: https://gradiences.mintlify.site/llms.txt > Use this file to discover all available pages before exploring further. # Solana sBPF Assembly Backend (Direct Codegen) > Canonical target id: solana-sbpf-asm Canonical target id: **`solana-sbpf-asm`** This is a new route distinct from the existing `solana-sbpf-linker` (Zig) route. It generates sBPF assembly text (`.s`) directly from the portable contract IR, then delegates to the [blueshift-gg/sbpf](https://github.com/blueshift-gg/sbpf) toolchain for assembly, linking, and packaging into a Solana loader-compatible ELF. ## Route Rationale ``` Lean contract source -> LCNF (Lean compiler frontend) -> Portable Contract IR (ProofForge.IR.Contract) -> sBPF assembly text (.s, generated by ProofForge.Backend.Solana.SbpfAsm) -> sbpf build (blueshift-gg assembler + linker) -> Solana ELF (deploy/.so) ``` ### Why this route over the Zig/sbpf-linker route | Concern | Zig/sbpf-linker route | sBPF assembly route | | -------------------- | ---------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------ | | Lean runtime linking | Must link full Lean Zig runtime under `bpfel-freestanding` — high risk of `.rodata`, `.bss`, panic, allocator failures | No Lean runtime at all. ProofForge owns the codegen end-to-end. | | Stack pressure | Lean runtime stack frames may exceed the 4KB Solana stack limit | Stack usage is tightly controlled: every local is a known offset, every call is accounted. | | Compute units | Lean runtime overhead is unpredictable | Instruction-level control over every load, store, branch, and syscall. | | Toolchain simplicity | Needs Zig, sbpf-linker, possibly a solana-zig fork | Single `cargo install --git https://github.com/blueshift-gg/sbpf.git` | | Observability | Binary-only | sbpf disassembler, debugger, and Mollusk-style test runner come free | | Mirrors EVM pattern | No — EVM goes through Yul + solc | Yes — intermediate text artifact + external packager, the same shape as Yul + solc | Cost: ProofForge must implement a full lowering backend in Lean that emits sBPF assembly. This includes register allocation, stack-frame discipline, Solana account ABI parsing, instruction dispatch, and Borsh-like serialization. ## Target Toolchain: blueshift-gg/sbpf The `sbpf` CLI provides everything needed after `.s` emission: | Command | Role | | ------------------------ | ----------------------------------------------------------------------------------------------- | | `sbpf init <name>` | Scaffold a project: `src/<name>/<name>.s`, `Cargo.toml` (for Rust tests), etc. | | `sbpf build` | Assemble `src/**/*.s` → `deploy/<name>.so` (ELF). Supports `--arch v0` / `v3`, `--debug`. | | `sbpf disassemble` | ELF → sBPF assembly (round-trip verification). | | `sbpf debug --asm/--elf` | Interactive debugger with input JSON (accounts + instruction data). | | `sbpf test` / `e2e` | Mollusk-based tests or build + deploy + test. | ProofForge's role is to produce valid `.s` text files that `sbpf build` accepts. No further toolchain work is needed in this repo. ## SDK Reference Anchors The Solana SDK completion work tracks these upstream surfaces: * Solana CPI: native programs call other programs through `invoke` / `invoke_signed`, which is the high-level Rust API shape ProofForge lowers to `sol_invoke_signed_c`. * SPL Token: `TokenInstruction` defines the account schemas and data payloads for `transfer_checked`, `mint_to`, `burn`, `approve`, `revoke`, and `set_authority`. * Pinocchio: the framework target is a `no_std`, zero-copy, no-copy/no-allocation entrypoint style with optional allocator control; ProofForge mirrors that by keeping Solana account parsing, allocator policy, and CPI packing in target lowering rather than portable IR. * pinocchio-tkn: the longer-term token SDK reference is stack-only, zero-allocation CPI helpers spanning SPL Token and Token-2022. ProofForge's current SPL Token helpers are the first compatible slice of that surface. ### Assembler ISA The sBPF assembly grammar (from the blueshift `sbpf.pest` PEG grammar): **Registers:** `r0`–`r10` (64 bit), `w0`–`w10` (32‑bit alias for lo‑half). **ALU (64‑bit & 32‑bit):** `add64/32`, `sub64/32`, `mul64/32`, `div64/32`, `or64/32`, `and64/32`, `lsh64/32`, `rsh64/32`, `mod64/32`, `xor64/32`, `mov64/32`, `arsh64/32`, `neg64/32` — each with immediate and register variants. **Endian byte-swap:** `le16/32/64`, `be16/32/64`. **Loads/stores:** `lddw rD, imm64`, `ldxb/h/w/dw rD, [rBase ± off]`, `stb/h/w/dw [rBase ± off], imm`, `stxb/h/w/xdw [rBase ± off], rS`. **Control flow:** `ja target`, `jeq/jne/jgt/jge/jlt/jle/jsgt/jsge/jslt/jsle/jset rA, rB/imm, target`, `call `, `callx rA`, `exit`. **Directives:** `.globl`, `.equ`, `.text` / `.data` / `.rodata`, `.ascii` / `.byte` / `.short` / `.word` / `.int` / `.long` / `.quad`. **Identifiers:** labels (alphanumeric + underscore), numeric labels (`0:`, `1:` with `0f`/`0b` references). ### Available syscalls | Syscall | Signature (conceptual) | Used for | | ----------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | `sol_log_` | (r1: ptr, r2: len) | Logging / events | | `sol_log_64_` | (r1: u64, r2: u64, r3: u64, r4: u64, r5: u64) | Logging structured data | | `sol_log_pubkey` | (r1: ptr) | Logging pubkeys | | `sol_log_data` | (r1: slices\_ptr, r2: slice\_count) | Base64 data logs used by Anchor-style event payloads | | `sol_log_compute_units_` | () → r0 | Compute budget tracking | | `sol_memcpy_` / `sol_memmove_` / `sol_memset_` / `sol_memcmp_` | copy/fill/compare pointers and byte lengths | Memory operations | | `sol_create_program_address` | (seeds\_ptr, seeds\_len, program\_id\_ptr, result\_ptr) → r0 | PDA derivation | | `sol_try_find_program_address` | (seeds\_ptr, seeds\_count, program\_id\_ptr, result\_addr, bump\_ptr) → r0 | PDA find | | `sol_invoke_signed_c` | (instruction\_ptr, account\_infos\_ptr, num\_accounts, signer\_seeds\_ptr, num\_seeds) → r0 | CPI with signer seeds | | `sol_invoke_signed_rust` | (instruction\_ptr, infos\_ptr, num\_accounts, seeds\_ptr, num\_seeds) | CPI Rust calling convention | | `sol_get_clock_sysvar` / `sol_get_rent_sysvar` / `sol_get_epoch_schedule_sysvar` / `sol_get_epoch_rewards_sysvar` | (ptr) → r0 | Fixed-layout sysvar reads | | `sol_get_sysvar` | (r1: sysvar id ptr, r2: result ptr, r3: offset, r4: len) → r0 | Generic feature-gated sysvar reads, including `LastRestartSlot` | | `sol_get_last_restart_slot` | (ptr) → r0 | Direct feature-gated LastRestartSlot syscall; kept as the canonical Solana name, but ProofForge currently lowers LastRestartSlot through `sol_get_sysvar` because `sbpf` 0.2.2 still registers the older assembler spelling | | `sol_get_return_data` | (buffer, len, program\_id\_ptr) → r0 | Cross-call return data | | `sol_set_return_data` | (buffer, len) | Return data / results | | `sol_sha256` / `sol_keccak256` / `sol_blake3` | (vals: slice table ptr, val\_len: slice count, hash\_result: ptr) → u64 | Cryptographic hashing | | `sol_panic_` | () → ! | Abort | | `sol_remaining_compute_units` | () → u64 | Compute unit budget query | ### Syscall coverage plan ProofForge treats Solana syscalls as target-extension capabilities, not portable IR primitives. Each syscall family should move through the same evidence ladder: SDK/API shape → capability metadata → sBPF AST helper → assembly smoke → `sbpf build` → Mollusk/runtime test → Surfpool/Web3.js live test when the syscall changes observable chain behavior. | Family | Current status | Next validation | | ------------------------------------------------------------------------------------------------------------------------------------------ | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------- | | Return data (`sol_set_return_data`, `sol_get_return_data`) | Implemented for IR `return`; covered by Mollusk and Surfpool/Web3.js Counter `get`; `runtime.return_data` SDK entrypoint actions now lower state-backed return-data buffers through `sol_set_return_data`, read return-data buffers/program ids through `sol_get_return_data`, and have Surfpool/Web3.js coverage for empty reads, set-return simulation output, and same-instruction set/get roundtrips | Add typed return payload helpers beyond `u64` and CPI return-value handling | | PDA (`sol_create_program_address`, `sol_try_find_program_address`) | SDK metadata and helper emission exist; typed seed descriptors cover literal/UTF-8 bytes, account pubkeys, bump seeds, and scalar instruction-data seeds; Solana `Slice { ptr, len }` tables are packed before `sol_create_program_address`; derived pubkeys can be validated against declared PDA accounts; assembly builds | Add Web3.js PDA fixture against `PublicKey.findProgramAddressSync`, then add `sol_try_find_program_address` support | | CPI (`sol_invoke_signed_c`, `sol_invoke_signed_rust`) | SDK metadata, entry actions, and helper emission exist; System Program transfer/create-account and SPL Token helpers pack C `SolInstruction`, standard instruction data bytes, `SolAccountMeta[]`, bound `SolAccountInfo[]`, signer seed tables, and decoded scalar entrypoint parameters; System transfer/create-account plus SPL Token `transfer_checked`, `mint_to`, `burn`, `approve`, `revoke`, and `set_authority` have Surfpool/Web3.js live behavior gates; System transfer, System `create_account`, SPL Token `transfer_checked`, SPL Token `mint_to`/`burn`/`approve`/`revoke`, and SPL Token `set_authority` now have checked-in Pinocchio reference contract/manifest gates included in `just solana-light`, plus dual-deploy live-equivalence harnesses gated on Solana rustc availability | Make the Pinocchio live gates pass in CI/local toolchains, add Token-2022 reference coverage, and extend remaining SPL helper live-equivalence | | Sysvars (`sol_get_clock_sysvar`, `sol_get_rent_sysvar`, `sol_get_epoch_schedule_sysvar`, `sol_get_epoch_rewards_sysvar`, `sol_get_sysvar`) | Clock.slot, Rent.lamports\_per\_byte\_year, EpochSchedule's five RPC-exposed fields, EpochRewards' scalar/word-view fields, and feature-gated LastRestartSlot.last\_restart\_slot are exposed as Solana-only SDK target-extension helpers, route through capability metadata, render manifest/artifact action metadata, build to ELF, and have Surfpool/Web3.js smoke scripts | Add generic account-passed sysvar reads, plus Rust/Pinocchio reference comparisons | | Account schema | Module-wide multi-account schemas are generated from state/PDA/CPI declarations plus explicit typed account declarations; manifest, artifact JSON (`solanaExtensions.accounts`), fixed `INSTRUCTION_DATA` offsets, and signer/writable/program-owner validation use the same schema | Replace the module-wide fixed schema with dynamic per-entrypoint account parsing before dispatch | | Runtime allocator | SDK metadata, target routing, manifest output, artifact JSON, and assembly metadata comments exist for Solana's default bump allocator and `noAllocator` | Lower actual dynamic allocation / heap-backed data structures through the selected allocator model | | Logs/events (`sol_log_`, `sol_log_64_`, `sol_log_pubkey`, `sol_log_data`) | Phase 1 scalar `events.emit` lowers to `sol_log_64_`; Solana-only `logAccountPubkey` entrypoint actions lower account pubkey pointers to `sol_log_pubkey`; Solana-only `logStateData` actions pack a `SolBytes` slice table and lower state-backed payloads through `sol_log_data`; Surfpool/Web3.js verifies transaction logs contain a stable event tag, scalar field value, base58 account pubkey, and base64 `Program data:` payload | Extend to `sol_log_` string payloads, Anchor-style discriminator/Borsh events, and indexed fields | | Memory (`sol_memcpy_`, `sol_memmove_`, `sol_memset_`, `sol_memcmp_`) | `runtime.memory` target extension lowers entrypoint actions to `sol_memcpy_`, `sol_memmove_`, `sol_memcmp_`, and `sol_memset_`; Surfpool/Web3.js verifies account byte effects | Use memory helpers for broader account/data packing and compare against Rust/Pinocchio fixtures | | Sysvars (`sol_get_clock_sysvar`, rent, epoch schedule, epoch rewards, restart slot) | `contextRead checkpointId` lowers to `sol_get_clock_sysvar` and reads `Clock.slot`; Solana-only `sysvar` target-extension actions lower `Rent.lamports_per_byte_year` to `sol_get_rent_sysvar`, all current RPC-exposed `EpochSchedule` fields to `sol_get_epoch_schedule_sysvar`, all current `EpochRewards` fields through scalar/word-view states to `sol_get_epoch_rewards_sysvar`, and feature-gated `LastRestartSlot.last_restart_slot` to `sol_get_sysvar`; Surfpool/Web3.js verifies recorded values against transaction metadata, sysvar account data, or RPC `getEpochSchedule()` | Expose typed SDK accessors for additional Clock/Rent fields and generic account-passed sysvars | | Crypto (`sol_sha256`, `sol_keccak256`, `sol_blake3`) | SHA-256, Keccak-256, and feature-gated Blake3 target-extension actions lower to `sol_sha256`/`sol_keccak256`/`sol_blake3` and have Surfpool/Web3.js reference hash gates | Add portable `Expr.hash` lowering where target semantics match, plus additional crypto syscall families | | Compute/panic (`sol_log_compute_units_`, `sol_remaining_compute_units`, `sol_panic_`) | `runtime.compute_units` SDK entrypoint actions lower the feature-gated `sol_remaining_compute_units` syscall and store the result in state; profiling actions lower `sol_log_compute_units_`; Surfpool/Web3.js coverage verifies remaining-CU state writes and compute-unit logs | Add explicit panic failure tests and track public-cluster feature variance | Implementation note: `sol_get_epoch_schedule_sysvar` returns the runtime struct layout, not the compact 33-byte sysvar-account serialization. The live Surfpool/Web3.js gate pins the currently used offsets as `slots_per_epoch = 0`, `leader_schedule_slot_offset = 8`, `warmup = 16`, `first_normal_epoch = 24`, and `first_normal_slot = 32`. Implementation note: `sol_get_epoch_rewards_sysvar` writes the runtime `EpochRewards` struct. ProofForge exposes 64-bit state views for every field: `distribution_starting_block_height = 0`, `num_partitions = 8`, `parent_blockhash_word0..3 = 16,24,32,40`, `total_points_low/high = 48,56`, `total_rewards = 64`, `distributed_rewards = 72`, and `active = 80`. ### Runtime allocator Solana's Rust SDK entrypoint installs a default heap allocator. The runtime constants are `HEAP_START_ADDRESS = 0x300000000` and `HEAP_LENGTH = 32 * 1024`, and the allocator is a one-way bump allocator: `alloc` moves the bump pointer downward with alignment and `dealloc` is a no-op. Pinocchio follows the same shape: `entrypoint!` expands to the program entrypoint plus `default_allocator!` and `default_panic_handler!`; lower-level macros also let a program opt out with `no_allocator!`. ProofForge mirrors this at the target-extension layer instead of baking it into portable IR: ```lean theme={null} build "SolanaVault" do scalarState "nonce" .u64 bumpAllocator ``` `bumpAllocator` records `runtime.allocator` with: ```toml theme={null} [[solana.allocator]] name = "runtime" kind = "bump" model = "downward-bump" heap_start = "0x300000000" heap_bytes = 32768 ``` `noAllocator` records `kind = "none"` and `model = "deny-dynamic"`, matching the no-heap pattern useful for Pinocchio-style programs that intentionally avoid dynamic allocation. At this stage the selected allocator is emitted in `manifest.toml`, `proof-forge-artifact.json`, and assembly metadata comments. Future lowering for heap-backed SDK data structures must route through this capability before emitting real allocation code. ## Solana Contract Model Solana programs have a single entrypoint: ```zig theme={null} export fn entrypoint(input: [*]u8) callconv(.c) u64 ``` The input buffer (`r1`) contains a serialized layout: ``` [8] num_accounts (u64 LE) For each non-duplicate account: [1] NON_DUP_MARKER (0xff) [1] is_signer [1] is_writable [1] is_executable [4] padding [32] pubkey [32] owner [8] lamports (u64 LE) [8] data_len (u64 LE) [data_len] data + 10240 padding + align to 8 [8] rent_epoch (u64 LE) For duplicate accounts: [1] first_index (u8) [7] padding [8] instruction_data_len (u64 LE) [...] instruction_data [32] program_id ``` The entrypoint parses this, dispatches on the first byte of instruction data (instruction discriminant), validates accounts, and mutates account data. ## Instruction Manifest Solana requires explicit account schemas — a sidecar manifest describing instruction dispatch and account constraints. Below is the proposed TOML format (should live as target metadata, not embedded into the generic Lean source). ```toml theme={null} # manifest.toml — generated alongside the .s by ProofForge target = "solana-sbpf-asm" [program] id = "BmDHboaj1kBUoinJKKSRqKfMeRKJqQqEbUj1VgzeQe4A" name = "counter" [[instruction]] name = "initialize_counter" tag = 0 handler = "sol_initialize_counter" accounts = [ { name = "authority", index = 0, signer = true, writable = true }, { name = "counter", index = 1, signer = false, writable = true, owner = "program" }, { name = "system_program", index = 2, signer = false, writable = false } ] [[instruction]] name = "increment" tag = 1 handler = "sol_increment" accounts = [ { name = "authority", index = 0, signer = true, writable = false }, { name = "counter", index = 1, signer = false, writable = true, owner = "program" } ] ``` This manifest drives: * Offsets for each account field in the generated `.s` (computed by the codegen from the account count and data lengths). * Validation code emitted in the entrypoint adapter (signer, writable, owner checks). * Instruction dispatch (first‑byte discriminant → handler label). * Test input generation (the `input.json` fed to `sbpf debug` or test runner). ## IR Lowering Design The lowering lives in `ProofForge/Backend/Solana/SbpfAsm.lean` and consumes a `ProofForge.IR.Contract.Module` to produce: 1. An sBPF assembly text file (`.s`) for each contract module. 2. An instruction manifest (`.toml`). 3. A `proof-forge-artifact.json` with artifact metadata. ### Module structure Each Lean contract module compiles to: ```text theme={null} sbpf-contract/ src//.s # generated sBPF assembly src//.ld # optional custom linker script manifest.toml # instruction manifest proof-forge-artifact.json # artifact metadata ``` ### IR to sBPF lowering walkthrough For the `Counter` shared scenario: **IR (IR/Contract.lean level):** ```lean theme={null} def counterModule : Module := { name := "Counter" structs := #[] state := #[{ id := "counter", kind := .scalar, type := .u64, owner := "program" }] entrypoints := #[ { name := "initialize", params := #[], returns := .unit, body := #[ .effect (.storageScalarWrite "counter" (.literal (.u64 0))) ] }, { name := "increment", params := #[], returns := .unit, body := #[ .letBind "n" .u64 (.effect (.storagePathRead "counter" #[])), .effect (.storagePathWrite "counter" #[] (.add (.local "n") (.literal (.u64 1)))) ] }, { name := "get", params := #[], returns := .u64, body := #[ .return (.effect (.storagePathRead "counter" #[])) ] } ] } ``` **Lowered sBPF assembly (simplified — `StorageBackend` = account data at fixed offset):** ```asm theme={null} .globl entrypoint entrypoint: ;; --- parse + dispatch --- ldxdw r2, [r1 + INSTRUCTION_DATA_LEN] jeq r2, 0, zero_instruction ;; ensure at least 1 byte ldxb r2, [r1 + INSTRUCTION_DATA] jeq r2, 0, sol_initialize jeq r2, 1, sol_increment jeq r2, 2, sol_get ;; unknown discriminant lddw r0, 1 exit sol_initialize: ;; validate authority is signer ldxb r2, [r1 + OWNER_HEADER + 1] jeq r2, 0, error_signature ;; write 0 to counter account data at offset COUNTER_DATA lddw r2, 0 stxdw [r1 + COUNTER_DATA], r2 lddw r0, 0 exit sol_increment: ;; validate authority is signer ldxb r2, [r1 + OWNER_HEADER + 1] jeq r2, 0, error_signature ;; read counter ldxdw r2, [r1 + COUNTER_DATA + 0] add64 r2, 1 stxdw [r1 + COUNTER_DATA + 0], r2 lddw r0, 0 exit sol_get: ;; no validation needed (read-only) lddw r0, 0 exit error_signature: lddw r0, 4 ;; custom error exit ``` ### Register discipline sBPF has 11 registers (r0–r10). Convention: | Register | Role | | -------- | ------------------------------------------------------------------------------ | | r0 | Return value (syscall results, entrypoint error code) | | r1 | Syscall arg 1 / entrypoint input pointer (preserved) | | r2–r5 | Syscall args 2–5 / scratch | | r6–r9 | Callee-saved across effects; used for persistent locals, account base pointers | | r10 | Frame pointer (stack discipline — offset downward for locals) | For the initial spike, a simple convention suffices: * r1 = input buffer base (never spilled — needed for all account access). * r6 = instruction\_data base pointer (computed once from r1). * r7–r9 = scratch for intermediate values. * Stack (`r10 - N`) for spilled locals when registers are exhausted. * Every entrypoint handler is at most \~70 instructions; simple register reuse is acceptable before implementing a proper register allocator. ### Expression lowering rules Each IR `Expr` node lowers to sBPF instructions that compute the value into a target register. Example mapping: | IR Expr | sBPF | | ----------------------------------- | ------------------------------------------------------------------- | | `.literal (.u64 n)` | `lddw rD, n` | | `.literal (.u32 n)` | `mov32 rD, n` | | `.add (lhs rhs)` | eval lhs → rD, eval rhs → rT, `add64 rD, rT` | | `.sub (lhs rhs)` | same, `sub64 rD, rT` | | `.eq (lhs rhs)` → bool | eval → rD/rT, `jeq rD, rT, eq_true` → `mov64 rD, 1` / `mov64 rD, 0` | | `.local "x"` | load from stack-frame slot at `r10 - offset(x)` | | `.cast (e) .u64` | 32→64 sign-extend via shifts or explicit load | | `.effect (.storagePathRead "s" [])` | `ldxdw rD, [r1 + STATE_OFFSET(s)]` | | `.hashTwoToOne (a b)` | eval a,b to args, `call sol_sha` on the concatenated input | | `.field (.local "s") "x"` | struct field access at a known offset | All 64‑bit computations should be 32‑bit safe (32‑bit variants for `.u32`, no over-64‑bit intermediate overflows). `sol_log_64_` is available for debugging. ### Statement lowering rules | IR Statement | sBPF | | ------------------------------------ | -------------------------------------------------------------------------------------------------------------- | | `.letBind "x" τ e` | eval e → rD, store rD at `r10 - offset(x)` | | `.letMutBind "x" τ e` | same (no distinction at assembly level) | | `.assign (.local "x") e` | eval e → rD, store rD at `r10 - offset(x)` | | `.assignOp (.local "x") .add e` | load from `r10-offset(x)` → rD, eval e → rT, `add64 rD, rT`, store | | `.ifElse cond then else_` | eval cond, `jeq rD, 0, else_label` / then code / `ja after_label` / `else_label:` / else code / `after_label:` | | `.for "i" (start) (end) (step) body` | **Phase 1**: unroll bounded loops. **Phase 2**: generate counted loop with explicit counter, conditional jump. | | `.return e` | eval e → r0 (or r1/r2 for return data via `sol_set_return_data`), `exit` | | `.effect eff` | delegate to Effect lowering (see below) | | `.assert cond "msg"` | eval cond, if false: `lddw r1, error_code`, `exit` | | `.assertEq a b "msg"` | eval a,b → rD/rT, `jne rD, rT, assert_fail` | ### Effect lowering: storage `storageScalar` / `storageArray` / `storageStructField` all map to **account data offsets** rather than EVM slot storage. The IR state declarations carry the owning account index and field offset, computed by the state-layout compiler pass before codegen. | IR Effect | Solana mapping | | ----------------------------------------- | ------------------------------------------------------------------------------------------- | | `.storageScalarWrite "counter" v` | `stxdw [r1 + ACCOUNT_DATA_BASE(i) + field_offset], rV` | | `.storageScalarAssignOp "counter" .add v` | load from `[r1 + offset]`, add, store back | | `.storageArrayWrite "xs" idx v` | `stxdw [r1 + ACCOUNT_DATA_BASE(i) + elem_offset(idx)], rV` | | `.storageArrayRead "xs" idx` | `ldxdw rD, [r1 + ACCOUNT_DATA_BASE(i) + elem_offset(idx)]` | | `.storageMapInsert "m" k v` | **Phase 2+**: map → Borsh serialization onto the account data with a hash-based key lookup. | | `.storagePathRead` / `.storagePathWrite` | Composite offsets: array index + struct field path → single `[base + sum]` access | | `.storagePathAssignOp` | Load-modify-store at compound offset | Storage layout is deterministic and computed at codegen time: 1. For each account declared in the manifest, assign the data region start offset. 2. For each state variable owned by that account, allocate a fixed offset within the data region, packing fields (u64 aligned). 3. Emit `.equ` constants for every field offset so the assembly is readable. ### Effect lowering: CPI/PDA (Solana-specific SDK extension) CPI and PDA derivation are Solana‑only concepts (D-027). They do **not** enter the portable IR. Instead, Solana-specific SDK calls are routed through `ProofForge.Solana` into target capability calls, gated by the existing `crosscall.cpi` and `storage.pda` capability IDs in `Target/Capability.lean`: ```lean theme={null} entrySelector "touch" "62de7396" do derivePda "vault" #[literalSeed "vault", accountSeed "authority"] (bump? := some "vault_bump") (account? := some "vault_account") (isSigner := true) invokeSplTokenTransferChecked "token_transfer" "source" "mint" "destination" "authority" "amount" 9 (signerSeeds := #["vault", "vault_bump"]) ``` The portable IR never knows about these — it operates at the capability level via `crosscall.cpi` and `storage.pda`. The generic builder records entrypoint scope as `proof_forge.entrypoint`; the Solana backend resolves that metadata into entrypoint actions and injects helper calls after account validation and before the portable IR body. The generated assembly preserves `r1` around helper calls so subsequent storage lowering still sees the original Solana input pointer. Current CPI/PDA lowering pattern: 1. Allocate stack space for `SolInstruction` + `SolAccountInfo[]` + seeds. 2. Emit one helper per declared PDA/CPI intent (`sol_pda_derive_`, `sol_cpi_`). 3. In entrypoint handlers with scoped SDK actions, call the helper and branch to `error_pda` / `error_cpi` when `r0 != 0`. 4. Build a module-wide multi-account instruction schema from state, PDA, CPI accounts, and executable CPI program accounts. This schema is used by `manifest.toml`, `proof-forge-artifact.json`, fixed instruction-data offset computation, and generated signer/writable/program-owner validation. 5. Build `manifest.toml` and artifact metadata with both extension definitions and entrypoint action lists. The SDK layer already exposes protocol-level helpers for System Program transfer/create-account and SPL Token transfer/mint/burn/approve/revoke/ set-authority. These helpers emit `solana.cpi.protocol`, `solana.cpi.data_layout`, account metas, signer seeds, and instruction-data sources into the capability plan, manifest, and artifact metadata. The source-facing layer exposes first-class `contract_source` forms for System Program transfer, System Program `create_account`, and SPL Token `transfer_checked` plus `set_authority`. These forms are still a v1 embedded macro frontend rather than the legacy standalone `.learn` parser, but they prevent new examples from dropping back to raw `ContractSpec`/builder strings for the core CPI paths. System and SPL Token helpers now emit the C ABI packing skeleton for `sol_invoke_signed_c`: program id bytes, C `SolAccountMeta[]`, standard instruction-data bytes, C `SolInstruction`, bound `SolAccountInfo[]`, optional signer seed tables, and the syscall register contract. `system.transfer` uses the bincode-style `u32 discriminator=2 + u64 lamports` layout; `system.create_account` uses `u32 discriminator=0 + u64 lamports + u64 space + owner pubkey`; SPL Token `transfer_checked`, `mint_to`, `burn`, `approve`, and `revoke` use the standard token instruction tags and amount/decimals layouts; SPL Token `set_authority` uses instruction tag `6`, authority type `0` (`MintTokens`), a `Some` option byte, and a new-authority pubkey copied from the generated program's readonly `new_authority` input account. Program ids, account meta pubkeys, and `SolAccountInfo` key/lamports/data/owner/rent/flag fields are sourced from the generated multi-account input layout when the account appears in the module schema. CPI value sources can bind to scalar state offsets, numeric literals, or decoded entrypoint parameters. PDA helper metadata now carries both a compatibility `seeds` list and target-facing typed seed descriptors. Bare strings remain literal seed bytes for backward compatibility; SDK helpers such as `literalSeed`, `utf8Seed`, `accountSeed`, `bumpSeed`, and `paramSeed` make the source explicit for Solana lowering. The Solana target extension consumes those descriptors, appends the declared `bump?` as an effective bump seed, and emits `typed_seeds` in `manifest.toml` plus `typedSeeds` in `proof-forge-artifact.json`. This remains a target-extension concern: portable IR and the chain-neutral SDK surface only see capability intent, while `--target solana-sbpf-asm` decides how those capabilities are packed into the Solana syscall ABI. The current instruction-data ABI reserves byte 0 for the ProofForge entrypoint tag. Packed scalar parameters start at `instruction_data+1`, in entrypoint parameter order, with little-endian `U64`/`U32` loads and one-byte `Bool` loads. The generated dispatcher rejects empty instruction data before reading the tag; each handler also checks the minimum payload length required by its parameter schema before decoding. The backend decodes those parameters into stack locals before SDK helper calls and exposes the same absolute input offsets to CPI value binding, so helpers can pack fields such as SPL Token `amount` directly from user instruction data. `manifest.toml` and `proof-forge-artifact.json` record each instruction's `min_data_len`/`minDataLen` plus parameter name, type, offset, byte size, and encoding. The module-wide helper table only binds a parameter name when all occurrences share the same offset; duplicate names at conflicting offsets are intentionally left unbound until per-entrypoint helper specialization lands. Remaining work: add dynamic per-entrypoint account parsing, richer aggregate/string/bytes instruction ABI decoding, return-data decoding, and runtime tests that exercise live CPI paths. PDA helper lowering: 1. Allocate stack space for seed data + result buffer (32 byte). 2. Pack typed seeds into Solana `Slice { ptr, len }` entries: literal/UTF-8 seeds are copied into stack buffers, account seeds point at input account pubkeys, bump seeds are one byte, and scalar instruction-data seeds are copied from the decoded fixed input offset. 3. `call sol_create_program_address`. 4. Restore the Solana input pointer and, when `account?` is declared, compare the 32-byte derived pubkey with the declared account pubkey before returning. ### Effect lowering: events Solana has no chain-level event log like EVM. Options: 1. `sol_log_` / `sol_log_64_` — simple but unstructured. 2. `sol_log_data` — base64 data logs used as the Anchor-style event payload carrier. 3. `sol_set_return_data` as a quasi-event mechanism. Phase 1 emits scalar `eventEmit` fields through `sol_log_64_` as `[eventTag, fieldIndex, value, 0, 0]`. The event tag is a stable 32-bit compile-time tag derived from the event name so generated Web3.js harnesses can assert the transaction log without baking in Solana-specific syntax at the portable SDK layer. Solana-only `logAccountPubkey` lowers account keys through `sol_log_pubkey`, and `logStateData` lowers fixed state-backed byte payloads through `sol_log_data` as the base layer for future Anchor-compatible discriminator/Borsh event serialization. Future work should add string `sol_log_` payloads, complete Anchor-compatible serialization, and indexed event forms. ### Capability mapping The target profile must accept or reject each IR capability. The proposed `solana-sbpf-asm` profile extends the existing `solanaSbpfLinker` capability set: | Capability | sBPF route support | Notes | | ----------------------- | ------------------ | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | `storage.scalar` | ✓ | Account data at fixed offset | | `storage.array` | ✓ | Account data at computed offset | | `storage.map` | Partial (Phase 2) | Requires Borsh or compact serialization | | `storage.pda` | ✓ | PDA derivation + account checks | | `caller.sender` | ✓ | Check signer flag on authority account | | `value.native` | ✗ (Phase 3) | Read lamports, SOL transfers | | `events.emit` | Partial | `sol_log_` / `sol_log_64_` | | `crosscall.invoke` | ✗ | EVM‑specific; Solana uses CPI | | `crosscall.cpi` | Partial | SDK entry actions emit `sol_invoke_signed_c` helpers; full account/data packing remains | | `env.block` | ✓ | `contextRead checkpointId` lowers to Clock.slot via `sol_get_clock_sysvar` | | `control.conditional` | ✓ | Conditional jumps | | `control.bounded_loop` | Phase 2 | Counted loop or unrolling | | `data.fixed_array` | ✓ | Fixed‑size local arrays, stack‑allocated | | `data.struct` | ✓ | Struct access at known offsets | | `crypto.hash` | Partial | Solana-only SHA-256, Keccak-256, and feature-gated Blake3 entrypoint actions lower to `sol_sha256`/`sol_keccak256`/`sol_blake3`; portable `Expr.hash` lowering remains target-semantics-dependent | | `assertions.check` | ✓ | Assert with error codes | | `account.explicit` | ✓ | The core abstraction | | `runtime.allocator` | ✓ | Bump allocator or no-allocator contract recorded as target-extension metadata | | `runtime.memory` | ✓ | Solana-only entrypoint actions lower to memory syscalls and stay outside portable IR | | `runtime.return_data` | ✓ | Solana-only entrypoint actions lower state-backed buffers to `sol_set_return_data`, read return buffers/program ids through `sol_get_return_data`, and have live `--solana-return-data-compute-elf` coverage | | `runtime.compute_units` | Partial | Feature-gated `sol_remaining_compute_units` helper emission plus `sol_log_compute_units_` profiling logs have live Surfpool coverage; public-cluster availability must be checked before relying on remaining-CU reads | ## CLI and Build Integration ### New CLI flag ```text theme={null} proof-forge --solana-elf [--root DIR] [--manifest manifest.toml] [--solana-sbpf-arch v0|v3] [-o output.so] input.lean ``` Also: * `--emit-sbpf-asm` — emit `.s` without invoking `sbpf build` (development). * `--emit-sbpf-elf` or `--solana-elf` — emit `.s` then invoke `sbpf build`. * `--solana-sbpf-arch v0|v3` — pass the selected sbpf architecture to `sbpf build --arch`; artifacts record the value under `toolchain.sbpf.arch`. ### Build pipeline steps 1. **Lean frontend**: Parse contract, resolve LCNF. 2. **IR extraction**: Map LCNF to `ProofForge.IR.Contract.Module`. 3. **Capability check**: Validate against `solana-sbpf-asm` target profile. 4. **Storage layout**: Compute account data offsets per manifest, assign `.equ` constants. 5. **Codegen** (`ProofForge.Backend.Solana.SbpfAsm`): * Emit instruction dispatch adapter (labeled handlers). * For each entrypoint: lower body statements + expressions → sBPF text. * Emit `.rodata` for string constants, event type tags. 6. **Write `.s`**: Produce `src//.s`. 7. **Write `manifest.toml`**: Record instruction metadata, account offsets. 8. **`sbpf build`**: Invoke external tool with the selected sbpf architecture, produce `deploy/.so`. 9. **Artifact metadata**: Write `proof-forge-artifact.json` recording `irVersion`, target id, tool versions, capability subset. ### Artifact metadata ```json theme={null} { "target": "solana-sbpf-asm", "irVersion": "portable-ir-v0", "artifactKind": "solana-elf", "module": "Counter", "entrypoints": ["initialize", "increment", "get"], "capabilities": ["storage.scalar", "account.explicit", "control.conditional"], "tools": { "sbpf": "0.1.0" } } ``` ## State Layout: From IR StateDecl to sBPF `.equ`s The storage layout compiler (`ProofForge.Backend.Solana.StateLayout`) takes the account manifest + IR state declarations and computes fixed offsets for every state variable per account. Example state declarations: ```lean theme={null} state counter : StateDecl := { id := "counter", kind := .scalar, type := .u64 } state balance : StateDecl := { id := "balance", kind := .scalar, type := .u64 } state owner : StateDecl := { id := "owner", kind := .scalar, type := .hash } -- pubkey ``` If `account_index` maps `"counter"` → 1 (the Counter account) and the Counter account data region starts at byte 0 within that account's data buffer: | Variable | Offset | Size | sBPF `.equ` | | --------------- | ------ | ---- | ---------------------------- | | counter.count | 0 | 8 | `COUNTER_COUNT_OFFSET = 0` | | counter.balance | 8 | 8 | `COUNTER_BALANCE_OFFSET = 8` | | counter.owner | 16 | 32 | `COUNTER_OWNER_OFFSET = 16` | Each `.equ` constant is added to the per-account data base (`COUNTER_DATA` in the dispatch adapter), producing the final memory reference: `[r1 + COUNTER_DATA + COUNTER_COUNT_OFFSET]`. ## Toolchain Dependency | Tool | Version | Role | | ---------------------------------- | ----------------------------- | ------------------------------------------------------ | | `sbpf` | latest from blueshift-gg/sbpf | Assembler, linker, test runner, disassembler, debugger | | `cargo` | (for `cargo install`) | Build sbpf from git | | `surfpool` | 0.10+ | Local simnet for live deploy/invoke smoke | | `solana` CLI | 3.x | Program deploy, airdrop, RPC checks | | `node` / `npm` / `@solana/web3.js` | Node 18+ / Web3.js 1.x | Standard JS client invocation | | `mollusk` | (bundled in sbpf) | Fast local test runner | CI should make Solana tests optional (gated on `sbpf`, Surfpool, Solana CLI, and Node tooling) following the same pattern as others (`solc`, `foundry`, `dargo` per `validation-gates.md`). ## Test Strategy ### Spike 1: Static entrypoint * Generated `entrypoint` returns success (r0 = 0). * No account parsing, no storage. * `sbpf build` succeeds, `sbpf debug` shows the entrypoint executes. * Validate the `.s` round‑trips via `sbpf disassemble`. ### Spike 2: Counter (single scalar u64) * Account manifest with one writable account. * Dispatch adapter: parse accounts, validate signer, dispatch on instruction tag. * `initialize`: write `u64(0)` to account data at fixed offset. * `increment`: read, add 1, write. * `sbpf test` with Mollusk. * Surfpool/Web3.js live deploy/invoke smoke. ### Spike 3: Multiple instruction types, typed returns * Add return data (`sol_set_return_data`). * Multi‑instruction dispatch. * Validation gate against the shared Counter scenario. ### Spike 4: CPI (System Program) * Account creation via System Program CPI with signer seeds. * PDA derivation and validation. * `sol_invoke_signed_c` call pattern. ### Spike 5: Borsh and structured types * Struct state with multiple fields. * Borsh serialization/deserialization primitives (hand‑written sBPF or generated). * Map storage via sorted entries or sparse buckets. ### Spike 6: SPL Token CPI * Token account create, mint, transfer. * Associated Token Program integration. ### Acceptance criteria | Gate | Criterion | | ------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | V-GATE-SOLANA-01 | `--emit-sbpf-asm` produces valid `.s` accepted by `sbpf build` (no assembly errors). | | V-GATE-SOLANA-02 | `sbpf build` produces a valid ELF that `sbpf disassemble` round‑trips. | | V-GATE-SOLANA-03 | Counter scenario (initialize, increment, get) passes `sbpf test` with Mollusk. | | V-GATE-SOLANA-04 | Counter scenario deploys to Surfpool and passes Web3.js initialize/increment/get behavior checks. | | V-GATE-SOLANA-05 | Capability checker rejects IR modules using unsupported capabilities with a clear diagnostic mentioning the target id. | | V-GATE-SOLANA-06 | `proof-forge-artifact.json` includes `target: "solana-sbpf-asm"`, `irVersion`, and entrypoint list. | | V-GATE-SOLANA-07 | `sbpf debug --elf --input` works interactively (developer ergonomics gate — not CI). | | V-GATE-SOLANA-16 | `just solana-memory-web3` deploys a generated memory syscall program on Surfpool and verifies `sol_memcpy_`, `sol_memmove_`, `sol_memcmp_`, and `sol_memset_` effects through Web3.js account reads. | | V-GATE-SOLANA-17 | `just solana-crypto-hash-web3` deploys a generated SHA-256/Keccak-256/Blake3 syscall program on Surfpool and verifies account-stored digests against Node `crypto.createHash("sha256")` plus `@noble/hashes` Keccak-256 and Blake3 references. | | V-GATE-SOLANA-18 | `just solana-rent-sysvar-web3` deploys a generated Rent sysvar program on Surfpool and verifies `sol_get_rent_sysvar` records `Rent.lamports_per_byte_year` matching the Rent sysvar account data. | | V-GATE-SOLANA-19 | `just solana-epoch-schedule-sysvar-web3` deploys a generated EpochSchedule sysvar program on Surfpool and verifies `sol_get_epoch_schedule_sysvar` records all five current RPC-exposed `EpochSchedule` fields matching RPC `getEpochSchedule()` fields. | | V-GATE-SOLANA-20 | `just solana-last-restart-slot-sysvar-web3` deploys a generated LastRestartSlot sysvar program on Surfpool and verifies the feature-gated read lowers through `sol_get_sysvar` with `SysvarLastRestartS1ot1111111111111111111111`. | | V-GATE-SOLANA-21 | `just solana-epoch-rewards-sysvar-web3` deploys a generated EpochRewards sysvar program on Surfpool and verifies `sol_get_epoch_rewards_sysvar` records all scalar/word-view fields matching the EpochRewards sysvar account data. | | V-GATE-SOLANA-22 | `just solana-return-data-compute-web3` deploys a generated ReturnDataCompute program on Surfpool and verifies `sol_set_return_data`, `sol_get_return_data`, `sol_remaining_compute_units`, and `sol_log_compute_units_` through Web3.js. | | V-GATE-SOLANA-10R | `just solana-pinocchio-system-transfer-equivalence` emits the generated System transfer CPI source/artifact metadata and compares its ABI/account/CPI/state-write contract against a checked-in Pinocchio reference manifest/source. Included in `just solana-light` through `just solana-pinocchio-reference-equivalence`. | | V-GATE-SOLANA-10L | `just solana-pinocchio-system-transfer-live-equivalence` builds/deploys the ProofForge and Pinocchio System transfer programs on Surfpool and compares the same Web3.js transfer scenario against both. | | V-GATE-SOLANA-11R | `just solana-pinocchio-system-create-account-equivalence` emits the generated System `create_account` CPI source/artifact metadata and compares its ABI/account/CPI/state-write contract against a checked-in Pinocchio reference manifest/source. Included in `just solana-light` through `just solana-pinocchio-reference-equivalence`. | | V-GATE-SOLANA-11L | `just solana-pinocchio-system-create-account-live-equivalence` builds/deploys the ProofForge and Pinocchio System `create_account` programs on Surfpool and compares the same Web3.js account-creation scenario against both. | | V-GATE-SOLANA-12R | `just solana-pinocchio-spl-token-transfer-equivalence` emits the generated SPL Token `transfer_checked` CPI source/artifact metadata and compares its ABI/account/CPI/state-write contract against a checked-in Pinocchio Token reference manifest/source. Included in `just solana-light` through `just solana-pinocchio-reference-equivalence`. | | V-GATE-SOLANA-12L | `just solana-pinocchio-spl-token-transfer-live-equivalence` builds/deploys the ProofForge and Pinocchio SPL Token `transfer_checked` programs on Surfpool and compares the same Web3.js token-transfer scenario against both. | | V-GATE-SOLANA-13R | `just solana-pinocchio-spl-token-ops-equivalence` emits the generated SPL Token `mint_to`/`burn`/`approve`/`revoke` CPI source/artifact metadata and compares its ABI/account/CPI/state-write contract against a checked-in Pinocchio Token ops reference manifest/source. Included in `just solana-light` through `just solana-pinocchio-reference-equivalence`. | | V-GATE-SOLANA-13L | `just solana-pinocchio-spl-token-ops-live-equivalence` builds/deploys the ProofForge and Pinocchio SPL Token ops programs on Surfpool and compares the same Web3.js mint/burn/approve/revoke scenario against both. | | V-GATE-SOLANA-13A | `just solana-spl-token-authority-cpi-web3` deploys a generated SPL Token `set_authority` CPI program on Surfpool and verifies mint authority plus marker state through Web3.js. | | V-GATE-SOLANA-13AR | `just solana-pinocchio-spl-token-authority-equivalence` emits the generated SPL Token `set_authority` CPI source/artifact metadata and compares its ABI/account/CPI/state-write contract against a checked-in Pinocchio Token authority reference manifest/source. Included in `just solana-light` through `just solana-pinocchio-reference-equivalence`. | | V-GATE-SOLANA-13AL | `just solana-pinocchio-spl-token-authority-live-equivalence` builds/deploys the ProofForge and Pinocchio SPL Token `set_authority` programs on Surfpool and compares the same Web3.js mint-authority transfer scenario against both. | ## Lean Module Layout ``` ProofForge/ Backend/ Solana/ SbpfAsm.lean # IR.Module → sBPF text (the main codegen) StateLayout.lean # account offset computation Register.lean # register allocator (simple v0) Syscalls.lean # syscall name constants, calling convention helpers Manifest.lean # instruction manifest -> TOML AsmPrinter.lean # sBPF text emitter (label, instruction, directive) Target/ Solana.lean # solana-sbpf-asm profile, capability set, tool deps IR/ Contract.lean # extended with Solana-aware effects (cpiInvoke, pdaDerive) ``` ## Input/Abstraction: The Lean SDK Layer Above the sBPF codegen, developers should get convenient Lean abstractions. Proposed API (Phase 3): ```lean theme={null} namespace Solana structure Pubkey extends Hash 32 structure Account where index : UInt8 structure Syscall where name : String opaque input : IO Input opaque account (index : UInt8) : IO Account opaque owner (acct : Account) : IO Pubkey opaque isSigner (acct : Account) : IO Bool -- etc. end Solana ``` The sBPF codegen recognizes these opaque operations and lowers them directly to account offset loads / syscalls — they never exist as Lean runtime code. ## Registration in Target Profile New target profile in `ProofForge/Target/Registry.lean`: ```lean theme={null} def solanaSbpfAsm : TargetProfile := { id := "solana-sbpf-asm" family := .solana artifactKind := .solanaElf capabilities := #[ .storageScalar, .storageArray, .callerSender, .controlConditional, .dataFixedArray, .dataStruct, .cryptoHash, .assertions, .accountExplicit, .runtimeAllocator, .runtimeMemory, .runtimeReturnData, .runtimeComputeUnits, .storagePda, .crosscallCpi ] requiredTools := #["sbpf"] } ``` ## Risks and Mitigations | Risk | Severity | Mitigation | | ------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------- | | sBPF codegen is a full compiler backend — scope may exceed Phase 1 budget | High | Spike 1 validates the toolchain round‑trip in a few hundred LoC. Counter scenario limits scope to scalar storage + dispatch + `sbpf test`. | | Account layout changes across Solana runtime versions break fixed offsets | Medium | Compute offsets from the manifest at codegen time (not hardcoded). Keep both Mollusk and Surfpool/Web3.js gates so harness-only assumptions are caught. | | 10240‑byte MAX\_DATA\_INCREASE padding per account blows up code size | Low | The padding is in the input buffer, not the generated code. Code only references offsets relative to the input base pointer. | | Borsh serialization is complex to implement in sBPF | Medium | Defer to Phase 2+. Use zero‑copy struct layouts (known C‑struct equivalents) for Phase 1; Borsh path is a follow‑on spike. | | Register allocator for nontrivial expressions | Medium | Phase 1 uses a fixed‑scratch‑register convention (no spills). If expressions exceed 5 scratch registers, add a simple stack‑spill pass. | | Blueshift sbpf toolchain changes incompatibly | Low | Pin to a known commit; the assembler grammar is stable (PEG‑based). | ## Phased Implementation Plan ### Phase 0: Toolchain integration (Spike 1) * Add `solana-sbpf-asm` to `Target/Registry.lean`. * Write a fixed sBPF entrypoint `.s` that returns success. * Run `sbpf build` + `sbpf debug` round‑trip. * CLI flag `--emit-sbpf-asm` that writes the canned `.s`. ### Phase 1: Counter (Spike 2–3) * `StateLayout.lean`: account offsets from manifest. * `SbpfAsm.lean`: lowering for Module → `.s` text. * Support: `literal`, `local`, `add`, `effect(storageScalarWrite/Read)`, `letBind`, `assign`, `ifElse`, `return`, `assert`. * Counter scenario passes `sbpf test`. ### Phase 2: Storage mid‑level (Spike 4-5) * Storage arrays, structs, and maps. * CPI (Account creation, SPL Token transfers). * PDA derivation. * Bounded loops. * Instruction manifest TOML generation. ### Phase 3: Developer SDK Phase 3 is split into verifiable SDK completeness levels rather than one large "framework" milestone. Estimates assume one engineer working from the 2026-07-02 baseline, current direct-assembly codegen staying stable, and local `sbpf`/Surfpool/Solana CLI tooling being available. | Level | Estimated effort | Scope | | ------------------------------ | ---------------------------: | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | SDK alpha | 3-5 focused engineering days | Validate PDA/System/SPL behavior live through Surfpool/Web3.js and expose basic logs/return-data helpers. PDA/System/SPL live gates, instruction ABI bounds/schema metadata, typed PDA seed lowering, return-data `get`, scalar `sol_log_64_` event logging, pubkey logging, and state-backed `sol_log_data` payload logging are already in place. | | SDK beta | 2-3 focused weeks | Add syscall families (sysvars, crypto, memory), runtime allocator lowering, dynamic per-entrypoint account schemas, and Rust/Pinocchio equivalence fixtures. Clock.slot, Rent.lamports\_per\_byte\_year, all current RPC-exposed EpochSchedule fields, all current EpochRewards fields through scalar/word-view states, SHA-256, Keccak-256, and feature-gated Blake3 are already covered through their target-extension syscall paths. | | Anchor/Pinocchio-class surface | 4-6 focused weeks after beta | Extend the new typed account/PDA/CPI surface toward richer account/data wrappers, IDL/client generation, richer SPL/Token-2022 helper coverage, and SDK-facing diagnostics. | The alpha line is the point where a developer should be able to write and deploy simple Solana programs without hand-written assembly patches. The beta line is the point where ProofForge output can be compared against reference Rust/Pinocchio programs for the same account schema. The System transfer, System `create_account`, SPL Token `transfer_checked`, and SPL Token `mint_to`/`burn`/`approve`/`revoke` plus SPL Token `set_authority` reference contracts are the first static equivalence anchors for that line, and their live dual-deploy harnesses are already wired to build/deploy both ELFs when Solana rustc is available. The final framework line adds the higher-level ergonomics expected from Anchor-like and Pinocchio-style workflows without moving Solana-specific details into portable IR. ## References * [sbpf toolchain](https://github.com/blueshift-gg/sbpf) — assembler, linker, runtime, debugger. * [sbpf-asm-counter](https://github.com/blueshift-gg/sbpf/tree/master/examples/sbpf-asm-counter) — example assembly‑level Counter. * [Solana native program examples (QuickNode)](https://github.com/quicknode/solana-program-examples) — reference SDK patterns. * Existing [solana-sbf.md](/targets/solana-sbf) — Zig/sbpf-linker route background. * [RFC 0002](/rfcs/0002-target-implementation-design) — target families and build pipeline design. * [Portable IR doc](/concepts/portable-ir) — IR specification.