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

# Portable Contract IR

> Status: Draft spec (Phase 1)

Status: **Draft spec (Phase 1)**

The portable contract IR sits between the chain-neutral Contract Intent API and
target backends. It expresses chain-independent business logic plus the
target-resolved capability effects that the selected target adapter will lower.

Related: [RFC 0001](/rfcs/0001-multichain-platform),
[RFC 0002](/rfcs/0002-target-implementation-design),
[RFC 0003](/rfcs/0003-portable-ir-and-runtime) (detailed draft),
[Capability registry](/concepts/capability-registry),
[Shared scenario](/concepts/shared-scenario).

## Goals

* Preserve the user-facing model where contract source declares portable
  intents and `--target` chooses the concrete chain route at compile time.
* Represent exported entrypoints, state, and transitions without EVM/Solana/Move
  ABI details.
* Record target-resolved capability calls as typed effects so targets can
  reject unsupported operations before lowering.
* Carry enough metadata for artifact emission and cross-target scenario tests.

## Non-goals (v0)

* Full Lean/LCNF preservation — only the contract-relevant subset.
* Automatic account/object inference for Solana or Move.
* Implicitly emulating target-specific semantics when a target cannot route an
  intent safely.
* Runtime proof transport to target chains — proofs are checked in Lean before
  codegen.

## Layering

```text theme={null}
Lean contract source
  -> Contract Intent API
  -> target intent resolution (`--target`)
  -> CapabilityPlan
  -> Portable Contract IR + target metadata
  -> Target AST / assembler / package printer
```

The default SDK surface is the Contract Intent API. It should not expose EVM
storage slots, Solana account metas, Move resources, or Wasm host ABIs. The
selected target adapter resolves those intents into a `CapabilityPlan` before
lowering. Target Extension SDKs may expose chain-specific operations such as
Solana PDA/CPI or Move resource primitives, but those extensions still lower
through capability ids and target metadata rather than adding chain-only
constructors to the portable IR.

## IR Units (v0 sketch)

### Module

* `name`: package/module identifier
* `entrypoints`: exported handlers
* `state`: declared persistent state slots
* `types`: portable structs/enums used by the module

### Entrypoint

* `name`: logical method name (e.g. `increment`, `get`)
* `tag`: optional dispatch tag for non-EVM targets
* `params`: portable values plus target-resolved account/resource bindings when
  the selected adapter requires explicit metadata
* `effects`: ordered target-resolved capability calls
* `returns`: portable return type or unit

### State

* `id`: stable state variable name
* `kind`: `scalar` | `map` | `account_owned` | `object` (target lowering hints)
* `type`: portable type reference

### Effect (target-resolved capability call)

* `capability`: id from [capability-registry.md](/concepts/capability-registry)
* `args`: portable operands
* `source`: optional Lean source span for diagnostics

### Expression Surface

The current executable IR in `ProofForge/IR/Contract.lean` includes a compact
expression set for target-source backends:

* literals: `U32`, `U64`/Felt, Bool, and fixed four-limb Hash literals
* local variables, fixed-array literals/indexing, struct literals, and field
  access
* numeric operations: `+`, `-`, `*`, `/`, `%`, `**`
* bitwise operations and shifts: `&`, `|`, `^`, `<<`, `>>`
* casts between supported scalar value types
* comparisons and boolean composition
* dynamic Hash value construction from four Felt limbs
* hash intrinsics: one-to-one and two-to-one hash operations
* effect expressions for storage reads, map reads, array reads, storage-path
  reads, and context reads

The statement set includes immutable and mutable local bindings, plain
assignment, first-class compound assignment (`+=`, `-=`, `*=`, `/=`, `%=`,
`|=`, `&=`, `^=`, `<<=`, `>>=`), statement effects, assertions, `if/else`,
bounded `for`, and explicit `return`. Statement effects include storage writes
and storage-reference compound assignment effects for scalar storage and
generic storage paths.

Each target backend is responsible for either lowering each node it accepts or
rejecting it before source generation with an explicit diagnostic.

## Relationship to LCNF

```text theme={null}
Lean contract source
  -> Lean frontend / LCNF (today)
  -> Portable Contract IR (Phase 1)
  -> Target lowering
```

**Phase 1 transition:** EVM may temporarily lower from LCNF while the IR extractor
is built, but the Counter shared scenario must compile through IR before Phase 2
spikes are considered complete.

## Target IR Subsets

Each target accepts a subset of IR. Unsupported constructs fail at capability
check time with target id and capability id.

| Restriction               | Solana                           | Move (Aptos/Sui)                 | Psy DPN                                                     |
| ------------------------- | -------------------------------- | -------------------------------- | ----------------------------------------------------------- |
| Implicit contract storage | Rejected — use explicit accounts | Rejected — use resources/objects | Allowed only through explicit Psy storage/sourcegen mapping |
| Higher-order functions    | Restricted runtime subset TBD    | Rejected in v0                   | Rejected in v0                                              |
| Arbitrary heap objects    | Runtime size TBD                 | Rejected                         | Rejected                                                    |
| Closures                  | TBD with sBPF spike              | Rejected                         | Rejected                                                    |
| Unbounded loops           | TBD with sBPF spike              | Rejected in v0                   | Rejected; require circuit-friendly bounded shape            |

See [targets/solana-sbf.md](/targets/solana-sbf),
[targets/move-family.md](/targets/move-family), and
[targets/psy-dpn.md](/targets/psy-dpn) for family-specific limits.

## Counter IR Example (v0)

Logical module for the [shared scenario](/concepts/shared-scenario):

```text theme={null}
module Counter {
  state count: scalar U64

  entrypoint initialize() {
    effect storage.scalar.write("count", 0)
  }

  entrypoint increment() {
    let n = effect storage.scalar.read("count")
    effect storage.scalar.write("count", n + 1)
  }

  entrypoint get() -> U64 {
    return effect storage.scalar.read("count")
  }
}
```

EVM lowering maps `storage.scalar` to slot storage; Solana maps to account data;
CosmWasm maps to string-keyed KV; Aptos maps to an account resource field.

## Phase 1 Acceptance Criteria

* [ ] IR node types documented in Lean (`ProofForge/IR/` or equivalent).
* [ ] Counter module expressible in IR without EVM-specific opcodes.
* [ ] EVM backend can lower Counter IR to Yul (directly or via existing EmitYul
  path with a thin adapter).
* [ ] Capability checker rejects at least one unsupported capability per
  non-EVM target with a clear diagnostic.
* [x] EVM portable IR bytecode metadata records `irVersion:
      portable-ir-v0` in `proof-forge-artifact.json`.

## Open Questions

* How much of LCNF to reuse vs. a fresh contract IR AST?
* Should account schemas live in IR or in target sidecar manifests?
* IR versioning strategy when capabilities expand.