Start with the ready-to-upload example archive:
This tool does not accept arbitrary Lean packages for whole-program compilation. It accepts Lean source that builds a value of:
HeytingLean.LeanCP.CProgramDeclThe selected entry_symbol must elaborate to that type. The generated c,
rust, and wasm artifacts are emitted from that LeanCP intermediate
representation.
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.lean files under UserProofs/Do not include:
lakefile.leanlean-toolchainlake-manifest.json.lake/The platform supplies the pinned Lean toolchain and the pinned LeanCP runtime.
Your archive should only contain your own UserProofs/ Lean source.
Import the LeanCP declaration and syntax modules:
import HeytingLean.LeanCP.Lang.CDecl
import HeytingLean.LeanCP.Lang.CSyntax
import HeytingLean.LeanCP.Core.HProp
open HeytingLean.LeanCPYour 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 CFunDeclmain : CFunDeclEach CFunDecl contains:
name : Stringparams : List (String × CType)retType : CTypebody : CStmtYou can use ordinary Lean definitions to build your program value. It is fine to use:
namespace, open, def, and letWhat actually gets exported is only the final CProgramDecl value. General Lean
code is authoring support, not emitted output by itself.
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.voidIn practice, the most stable surface today is:
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 argsSupported binary operators (BinOp):
.add, .sub, .mul, .div, .mod.eq, .ne, .lt, .le, .gt, .ge.and, .or, .lAnd, .lOr.bitAnd, .bitOr, .bitXor, .shl, .shrCStmt 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 tyUseful helper:
switchMany expr cases defaultStmtNotes:
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.def exportProgram : CProgramDecl := {
defs := []
main := {
name := "add_one"
params := [("x", .int)]
retType := .int
body := .ret (.binop .add (.var "x") (.intLit 1))
}
}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)))
}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))
}
}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")))))
}
}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)))
}
}Download lean-proof-code-generation-example.zip.
Use the file manager flow for the proof compiler tool so you get a source_archive_file_id.
Use entry_module set to UserProofs.Main and entry_symbol set to exportProgram.
{
"action": "generate",
"source_archive_file_id": "your_uploaded_file_id",
"entry_module": "UserProofs.Main",
"entry_symbol": "exportProgram",
"target_language": "c"
}Use get_task until the task reaches completed, then read the output artifact and bundle metadata from the result.
These inputs are outside the supported contract:
entry_symbol whose type is not CProgramDecllakefile.leanCProgramDeclAll targets start from the same CProgramDecl.
c is the baseline and most direct emission pathrust is a deterministic translation of the same C IR and uses unsafe for pointer semanticswasm is the most restrictive path and should be treated as preview-grade compared with c