Supported Lean Input For Code Generation

Full step-by-step tutorial:

• https://www.agentpmt.com/docs/tutorials/write-lean-input-for-code-generation

Download the working example zip:

• https://www.agentpmt.com/downloads/lean-proof-code-generation-example.zip

This service does not accept arbitrary Lean programs and "turn them into C". It accepts Lean source that builds a value of:

• HeytingLean.LeanCP.CProgramDecl

The selected entry_symbol must elaborate to that type. The generated c, rust, and wasm artifacts are emitted from that LeanCP intermediate representation.

Async Workflow

1. Call generate or verify.
2. Poll get_task with the returned task_id until status is completed or failed.
3. Read artifacts from the completed task result.

What To Put In The Archive

Upload a .zip file whose top-level entries are Lean source files under UserProofs/.

Required:

• UserProofs/Main.lean or another module referenced by entry_module
• only .lean files under UserProofs/

Do not include:

• lakefile.lean
• lean-toolchain
• lake-manifest.json
• .lake/
• external package checkouts or generated build artifacts

The platform supplies the pinned Lean toolchain and the pinned LeanCP runtime.

Authoring Model

You can use ordinary Lean definitions to build your program value. For example, it is fine to use:

• namespace, open, def, let
• helper functions and helper constants
• lists, tuples, and other normal Lean data needed to assemble the IR
• small amounts of proof-oriented helper code if it stays within the pinned runtime surface

What actually gets exported is only the final CProgramDecl value. General Lean code is authoring support, not emitted output by itself.

Required Export Shape

Import the LeanCP declaration and syntax modules:

import HeytingLean.LeanCP.Lang.CDecl
import HeytingLean.LeanCP.Lang.CSyntax
import HeytingLean.LeanCP.Core.HProp

open HeytingLean.LeanCP

Your exported symbol must be a CProgramDecl:

def exportProgram : CProgramDecl := {
  defs := []
  main := {
    name := "add_one"
    params := [("x", .int)]
    retType := .int
    body := .ret (.binop .add (.var "x") (.intLit 1))
  }
}

CProgramDecl contains:

• defs : List CFunDecl
• main : CFunDecl

Each CFunDecl contains:

• name : String
• params : List (String × CType)
• retType : CType
• body : CStmt

Supported Type Surface

The exported IR currently supports these CType constructors:

• .int
• .intSized signedness intSize
• .float
• .double
• .ptr ty
• .array ty n
• .funcPtr ret args
• .struct name
• .union name
• .enum name
• .typedef name
• .void

In practice, the most stable surface today is:

• integers
• pointers
• fixed-size arrays
• the built-in struct layouts the runtime already knows about

Supported Expression Surface

CExpr currently supports:

• .var name
• .intLit n
• .floatLit v
• .null
• .sizeOf ty
• .cast ty expr
• .binop op lhs rhs
• .deref ptrExpr
• .arrayAccess arr idx
• .addrOf varName
• .fieldAccess base field
• .call functionName args

Supported binary operators (BinOp):

• arithmetic: .add, .sub, .mul, .div, .mod
• comparisons: .eq, .ne, .lt, .le, .gt, .ge
• boolean/logical: .and, .or, .lAnd, .lOr
• bitwise: .bitAnd, .bitOr, .bitXor, .shl, .shr

Supported Statement Surface

CStmt currently supports:

• .skip
• .assign lhs rhs
• .seq s1 s2
• .ite cond thenStmt elseStmt
• .whileInv cond invariant body
• .block locals body
• .switch expr tag caseBody defaultBody
• .forLoop init cond step body
• .break
• .continue
• .ret expr
• .alloc varName cellCount
• .free expr cellCount
• .decl varName ty

Useful helper:

• switchMany expr cases defaultStmt

Notes:

• whileInv takes a loop invariant of type HProp. Use HProp.htrue when you need a permissive invariant.
• block takes a list of local declarations as (String × CType).
• alloc and free work at the LeanCP memory-model level with explicit cell counts.

Practical Examples

Simple arithmetic function:

def applyTax : CFunDecl := {
  name := "apply_tax"
  params := [("subtotal", .int), ("tax_rate", .int)]
  retType := .int
  body := .ret
    (.binop .add
      (.var "subtotal")
      (.binop .div
        (.binop .mul (.var "subtotal") (.var "tax_rate"))
        (.intLit 100)))
}

Conditional return:

def shippingProgram : CProgramDecl := {
  defs := []
  main := {
    name := "shipping_quote"
    params := [("weight_kg", .int)]
    retType := .int
    body := .ite (.binop .le (.var "weight_kg") (.intLit 5))
      (.ret (.intLit 8))
      (.ret (.intLit 15))
  }
}

Loop with invariant:

def loyaltyProgram : CProgramDecl := {
  defs := []
  main := {
    name := "loyalty_points"
    params := [("orders", .int), ("points_each", .int)]
    retType := .int
    body := .block [("total", .int), ("i", .int)] (
      .seq (.assign (.var "total") (.intLit 0)) (
      .seq (.assign (.var "i") (.intLit 0)) (
      .seq (.whileInv (.binop .lt (.var "i") (.var "orders")) HProp.htrue (
          .seq (.assign (.var "total") (.binop .add (.var "total") (.var "points_each")))
               (.assign (.var "i") (.binop .add (.var "i") (.intLit 1)))))
          (.ret (.var "total")))))
  }
}

Pointer and array access:

def basketProgram : CProgramDecl := {
  defs := []
  main := {
    name := "basket_head_total"
    params := [("prices", .ptr .int)]
    retType := .int
    body := .ret (.binop .add
      (.arrayAccess (.var "prices") (.intLit 0))
      (.arrayAccess (.var "prices") (.intLit 1)))
  }
}

What Will Not Work

These inputs are outside the supported contract:

• an entry_symbol whose type is not CProgramDecl
• a custom Lean package graph that depends on your own lakefile.lean
• imports that require packages not already present in the pinned runtime
• raw theorem statements with no executable CProgramDecl
• arbitrary Lean runtime code that is not expressed through the LeanCP IR

Target Honesty

All targets start from the same CProgramDecl.

• c is the baseline and most direct emission path
• rust is a deterministic translation of the same C IR and uses unsafe for pointer semantics
• wasm is the most restrictive path and should be treated as preview-grade compared with c