Skip to main content

​
Layers

ProofForge is structured as five layers:

​
Authoring surface

  • Contract Intent API — the default SDK surface: state, entrypoints, events, caller/value access, checked arithmetic, assertions, and proofs, without importing a destination-chain module.
  • Target Extension SDKs — explicit chain-native semantics when a contract needs them (Solana accounts/PDA/CPI, allocator selection, …). Extensions lower through capability ids and target metadata, never by adding chain-only constructors to the portable IR (D-027).
  • Target adapters — ABI, packaging, test-runner, and deployment logic per chain family; --target selects the adapter, and unsupported intents are rejected before artifact generation (D-028).

​
Module naming

  • Lake module: ProofForge.Evm (import in contract files).
  • Lean namespace: Lean.Evm (use via open Lean.Evm in examples).
This split comes from the Lean fork migration. The rename to a uniform ProofForge.* namespace is tracked in the backlog (Workstream 24), because Lean.Evm shadows the Lean compiler’s own Lean namespace.

​
Deeper reading

Authoring model

Learn source, contract_source, and internal ContractSpec boundaries.

Portable IR

The IR spec and Phase 1 acceptance criteria.

Capability registry

Canonical capability ids and the per-target support matrix.

RFC 0002

The target implementation design RFC.