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

# Architecture

> How ProofForge lowers Lean contract sources to chain-native artifacts through portable IR and capability routing

## Layers

ProofForge is structured as five layers:

```mermaid theme={null}
flowchart TB
  subgraph authoring ["Authoring (user-facing, chain-neutral)"]
    SDK["Lean SDK<br/>contract_source / Contract Intent API"]
    TOK["Token SDK<br/>TokenSpec"]
    LEARN[".learn parser<br/>(frozen compatibility)"]
  end
  subgraph core ["Compiler-owned core"]
    SPEC["ContractSpec"]
    IR["Portable IR<br/>+ AllocatorConfig + ownership rules"]
    SEM["IR semantics + formal anchors<br/>(FV roadmap)"]
  end
  subgraph routing ["Target routing (--target)"]
    REG["Target registry<br/>profiles + allocator bindings"]
    CAP["Capability check<br/>reject unsupported intents"]
    EXT["Target Extension SDKs<br/>Solana accounts/PDA/CPI, ..."]
  end
  subgraph backends ["Backends"]
    EVM["EVM<br/>Plan → Yul → solc"]
    SOL["Solana<br/>sBPF asm → ELF"]
    NEAR["NEAR<br/>EmitWat → WAT → wasm"]
    PSY["Psy/DPN<br/>.psy → Dargo"]
    ALEO["Aleo<br/>Leo package"]
    CFW["CF Workers<br/>TypeScript"]
  end
  subgraph artifacts ["Artifacts + validation"]
    ART["bytecode/ELF/wasm/circuit + ABI/IDL<br/>artifact + deploy manifests + TS clients"]
    GATES["Gates: Lean tests · testkit<br/>Foundry · Mollusk/Surfpool · offline host · dargo/leo"]
  end
  SDK --> SPEC
  TOK --> SPEC
  LEARN --> SPEC
  SPEC --> IR
  IR --- SEM
  IR --> CAP
  REG --> CAP
  EXT --> CAP
  CAP --> EVM & SOL & NEAR & PSY & ALEO & CFW
  EVM & SOL & NEAR & PSY & ALEO & CFW --> ART
  ART --> GATES
```

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

<CardGroup cols={2}>
  <Card title="Authoring model" icon="pen-to-square" href="/concepts/authoring-model">
    Learn source, contract\_source, and internal ContractSpec boundaries.
  </Card>

  <Card title="Portable IR" icon="diagram-project" href="/concepts/portable-ir">
    The IR spec and Phase 1 acceptance criteria.
  </Card>

  <Card title="Capability registry" icon="puzzle-piece" href="/concepts/capability-registry">
    Canonical capability ids and the per-target support matrix.
  </Card>

  <Card title="RFC 0002" icon="file-lines" href="/rfcs/0002-target-implementation-design">
    The target implementation design RFC.
  </Card>
</CardGroup>