Skip to main content
ProofForge should not ask application developers to author ContractSpec objects directly. ContractSpec is a compiler-owned boundary: source syntax lowers into it, target routing consumes it, and backends print target artifacts from the resulting IR and target-extension metadata.

​
Layers

The current stack has three authoring layers:
LayerStatusPurpose
Lean embedded SDK / contract_sourceImplemented v1 embedded source syntaxCurrent authoring surface. It lets the repo express portable state, entrypoints, events, arithmetic, SDK intents, and Solana account/PDA/CPI declarations in Lean syntax without hand-building ContractSpec strings.
Legacy .learn parserImplemented v0 standalone parser and CLI compatibility entrypointCompatibility/smoke-test input that lowers into the same compiler-owned ContractSpec / TokenSpec boundary. It should not grow into a second product language.
ContractSpec / IRInternal compiler artifactStable bridge into target routing, capability checks, backend lowering, AST/printer stages, manifests, IDL, clients, and deployable packages.
The intended user experience is Lean-first for the current repo: developers use Lean syntax and SDK helpers, and the compiler lowers those values into ContractSpec, TokenSpec, portable IR, and target-extension plans. The standalone .learn parser remains useful as a compatibility harness because it exercises the same lowering boundary from files, but new SDK work should land in the Lean/SDK layer first. proof-forge --learn --target <id> and proof-forge --learn-token --target <id> are therefore legacy CLI paths that reuse the same compiler-owned boundaries instead of defining a separate product language. The string-heavy ContractSpec and Builder examples should therefore be read as compiler fixtures, not as the product surface. They describe the same program shape that the compiler consumes after parsing, capability routing, and target-extension expansion. Application authors should see Lean SDK syntax and typed helpers; tests may keep Builder and .learn fixtures as reviewed equivalence inputs. It is still normal for the compiler-owned source AST and IR boundary to store identifiers as strings after parsing. That representation is not the authoring model. The product direction is that users write Lean SDK syntax, typed helpers check names and references where possible, and only then does the compiler materialize string names inside ContractSpec, manifests, IDL, clients, and backend ASTs.

​
Source Principles

  • Portable contracts should express business logic without target-specific deployment details.
  • Target-specific capabilities should be requested through typed SDK forms, not raw string plumbing.
  • Chain dispatch belongs to build configuration and target routing. Source code should remain reusable when a target can provide equivalent capabilities.
  • Target extensions, such as Solana account/PDA/CPI declarations, may appear in source when the contract intentionally needs chain-native semantics. Those extensions lower to target metadata and helper actions, not to portable IR constructors unless multiple chain families share the same semantic shape.
  • Literal strings are acceptable for real protocol bytes, such as PDA literal seeds. They should not be the primary representation for accounts, owners, capability names, methods, or deployment configuration.

​
Current Syntax Boundary

ProofForge.Contract.Source is the current executable Lean syntax layer and covers:
  • portable scalar state;
  • entrypoints and queries with typed parameters;
  • local bindings, assignment, return, event emission, and checked arithmetic syntax;
  • Solana allocator selection;
  • Solana account constraints, including writable and signer declarations;
  • Solana PDA declarations and derivation statements;
  • Solana System Program transfer and create_account CPI declarations and invocation statements;
  • Solana SPL Token transfer_checked, mint_to, burn, approve, revoke, and set_authority CPI declarations and invocation statements;
  • Solana log, return-data, compute-unit, memory, crypto, and sysvar helper statements.
ProofForge.Contract.Token is the current token SDK planning boundary. Lean-authored TokenSpec values route to ERC-20 on EVM or to structured Solana SPL Token / Token-2022 deployment plans. The Solana plan records mint account creation, associated token accounts, mint_to, transfer_checked, approve, burn, revoke, authority changes, Token-2022 extension initialization, and Token-2022 transfer-fee collection flows such as direct withheld-fee withdraw and harvest-to-mint plus withdraw-from-mint, plus non-transferable token initialization that rejects TransferChecked while still allowing burn. It also records the Solana program ids needed by Web3.js or client generation. ProofForge.Contract.Learn still parses the checked-in .learn examples under Examples/Learn/ into a small source AST and lowers that AST to the same ContractSpec/portable IR boundary used by contract_source. The CLI can route a .learn input through --target evm for EVM bytecode metadata or --target solana-sbpf-asm for Solana sBPF assembly packages. The parser covers the portable scalar/event subset plus the first Solana target-extension forms for accounts, PDA derivation, System Program transfer/create-account CPI, and SPL Token transfer, mint, burn, approve, and revoke CPI. It also accepts selector-bearing entrypoints such as entry mint selector "04"(amount: u64), so Solana instruction tags can be represented in Learn source instead of only in Builder fixtures. Learn statements now also cover the Solana log helpers for pubkey/data logs, return-data set/get helpers, and remaining-compute-unit read or log helpers. The same source layer covers Solana memory helpers, SHA-256, Keccak-256, and BLAKE3 hash helpers, and sysvar/context reads for Clock, Rent, EpochSchedule, EpochRewards, and LastRestartSlot fixture coverage. Learn lowering also validates declared Solana CPI/PDA references, signer seeds, declared CPI account references, CPI writable/signer requirements, and helper state/account references before emitting ContractSpec, so the remaining string-bearing identifiers are checked compiler data instead of unchecked user-facing spec plumbing. ProofForge.Contract.Token.Learn separately parses Learn token intent sources such as Examples/Learn/ProofToken.learn and Examples/Learn/FeeToken.learn. --learn-token --target evm now emits ERC-20 Yul, bytecode, and artifact metadata with standard ERC-20 selectors and Transfer/Approval topics, while --learn-token --target solana-sbpf-asm reuses TokenSpec to emit the same structured SPL Token / Token-2022 plan used by Lean-authored token specs. Examples such as ProofForge.Contract.Examples.ValueVault should be read as v1 Lean source examples, not as a staging area for a second .learn grammar. The matching .learn files are legacy compatibility examples used to prove lowering equivalence.

​
Target Routing

The build target chooses the lowering path: 
Lean SDK syntax / contract_source
  -> source AST
  -> ContractSpec / portable IR
  -> target resolver + capability routing
  -> target semantic AST
  -> printer / assembler / package emitter
For Solana, target extensions attach account schemas, PDA seeds, CPI layouts, IDL, clients, and sBPF assembly helpers. For EVM, routing derives ABI selectors, Yul, bytecode, ABI metadata, and deployment files. The source author should not need to manually switch between these internals when the contract is portable.

​
Next Implementation Steps

  1. Keep new SDK Alpha/Beta work in Lean SDK syntax and compiler-owned planning layers, then let legacy .learn inputs reuse those layers only when useful for compatibility tests.
  2. Gradually replace string-bearing Solana declarations with typed account, owner, program, and capability references in Lean helpers while keeping string names inside compiler artifacts only.
  3. Extend target package emission beyond EVM and Solana sBPF as Wasm, Move, and other target backends grow from routing plans into package emitters.