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 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/<name>.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 <syscall>, 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:

build "SolanaVault" do
  scalarState "nonce" .u64
  bumpAllocator

bumpAllocator records runtime.allocator with:

[[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:

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).

# 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:

sbpf-contract/
  src/<name>/<name>.s          # generated sBPF assembly
  src/<name>/<name>.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):

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):

.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:

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_<name>, sol_cpi_<name>).
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

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/<module>/<module>.s.
7. Write manifest.toml: Record instruction metadata, account offsets.
8. sbpf build: Invoke external tool with the selected sbpf architecture, produce deploy/<module>.so.
9. Artifact metadata: Write proof-forge-artifact.json recording irVersion, target id, tool versions, capability subset.

Artifact metadata

{
  "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 .equs

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:

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):

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:

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 — assembler, linker, runtime, debugger.
• sbpf-asm-counter — example assembly‑level Counter.
• Solana native program examples (QuickNode) — reference SDK patterns.
• Existing solana-sbf.md — Zig/sbpf-linker route background.
• RFC 0002 — target families and build pipeline design.
• Portable IR doc — IR specification.