LemmaScript

Version: 0.5.19 Date: July 2026

This document covers what is unique to the Lean backend. See SPEC.md for the shared annotation language, translation rules, type mapping, and pipeline.

---

1. Project Structure

LemmaScript is a Lean library. Each user project depends on it.

my-app/
  src/
    binarySearch.ts              ← TypeScript source
    binarySearch.types.lean      ← Lean types from TS (generated)
    binarySearch.spec.lean       ← ghost definitions, lemmas (user-written)
    binarySearch.def.lean        ← method definition (generated)
    binarySearch.proof.lean      ← prove_correct + tactics (user/LLM-written)
  lakefile.lean                  ← requires LemmaScript
  lean-toolchain
  package.json                   ← depends on @lemmascript/tools

1.1 The Four Lean Files

For each verified TS function foo.ts, there are up to four Lean files:

File	Who writes it	Purpose
foo.types.lean	lsc gen	Lean type definitions derived from TS types
foo.spec.lean	User	Ghost definitions, helper lemmas
foo.def.lean	lsc gen	Velvet method definition (generated from TS)
foo.proof.lean	User / LLM	prove_correct with proof tactics

Key property: foo.types.lean and foo.def.lean are always regeneratable from foo.ts. The user only writes .spec.lean and .proof.lean.

1.2 Import Chain

foo.types.lean         ← generated: Lean inductives/structures from TS types
foo.spec.lean          ← imports foo.types.lean, user-written ghost definitions
foo.def.lean           ← imports foo.spec.lean, generated method definition
foo.proof.lean         ← imports foo.def.lean, user-written proof

Each file imports the previous. Lean checks the full chain.

foo.def.lean imports foo.spec.lean, which imports foo.types.lean (if it exists). If there is no .spec.lean, foo.def.lean imports foo.types.lean directly (or LemmaScript if there are no types either).

1.3 File Naming and Lake Modules

Files use dotted names: binarySearch.spec.lean. In Lean imports, dots in filenames are escaped:

import «binarySearch.spec»
import «binarySearch.def»

All files live in src/, which Lake is configured to scan. No nested lean/ directory.

To set up a new project, copy lakefile.lean, lean-toolchain, and dependencies.toml from an existing case study.

1.4 Overriding the Module Base — //@ lean-module

By default the Lean module base is the file's basename, so foo.ts emits foo.types.lean / foo.def.lean and a lakefile.lean root of «foo.types». Lean module names are flat and global: two .ts files with the same basename in different directories (e.g. an in-place fork that annotates two copies of compaction.ts) would emit colliding modules and cannot both be Lean libraries. Dafny is unaffected — each .dfy is verified as a standalone unit.

A file-level directive overrides the base for the Lean backend only:

//@ lean-module compaction-cli

lsc gen --backend=lean then emits compaction-cli.types.lean / compaction-cli.def.lean (with import «compaction-cli.types»), and looks for compaction-cli.spec.lean / compaction-cli.proof.lean. Wire it into lakefile.lean with matching roots (`«compaction-cli.types», `«compaction-cli.def», `«compaction-cli.proof»). The Dafny artifacts (foo.dfy, foo.dfy.gen) keep the file basename.

---

2. Monadic Lifting

The shared method-call lifting (SPEC.md §3.6) has specific Lean semantics. Lifted method calls use Lean's monadic ← bind in do-notation:

x ← f a b          -- mutation: rebinds existing variable
let x ← f a b      -- new binding

This follows Lean's do-notation desugaring rules (Ullrich & de Moura, "'do' Unchained", 2022). The ← is not just syntax — it carries monadic semantics that Velvet's WPGen reasons about.

Monadic HOF variants: When a lambda callback passed to a HOF calls a method, the transform selects the monadic variant of the HOF (e.g., arr.mapM f instead of arr.map f). The monadic HOF call is itself monadic — it gets ← at the call site. The transform checks the transformed lambda body for ← binds and selects the variant automatically.

Short-circuit note: As in Lean's ←, lifting from &&/|| loses short-circuit semantics (both sides execute). This matches Lean's behavior.

Proof note: Velvet's WPGen does not currently have rules for mapM/filterM/etc. Proofs involving monadic HOFs require manual tactics.

---

3. Generated Lean files

For src/foo.ts, lsc gen produces src/foo.types.lean and src/foo.def.lean.

foo.types.lean contains Lean type definitions derived from TS type declarations (string literal unions, discriminated unions, records). If the TS file has no user-defined types, this file is not generated.

foo.def.lean contains the Velvet method definition:

/-
  Generated by lsc from foo.ts
  Do not edit — re-run `lsc gen` to regenerate.
-/
import «foo.spec»

set_option loom.semantics.termination "total"
set_option loom.semantics.choice "demonic"

method foo (params...) return (res : RetType)
  require ...
  ensures ...
  do
    ...

The generated file contains only the method definition, no prove_correct. The proof lives in foo.proof.lean.

3.1 Pure Function Mirrors

For functions that are pure (see SPEC.md §5), lsc also generates a plain Lean def in foo.types.lean, inside a namespace Pure:

namespace Pure

def foo (params...) : RetType :=
  -- same logic as the Velvet method, as a plain function

end Pure

This enables proofs by standard Lean induction over sequences of calls. The Velvet method is also generated, but as a thin wrapper: return Pure.foo params. This avoids termination issues (the pure def handles termination natively) while keeping the method callable from other Velvet methods via ←.

Spec references: In //@ ensures, //@ requires, and //@ invariant annotations, calls to pure functions are resolved as Pure.fnName. The resolve phase classifies these as spec-pure call kind, and the transform emits the qualified name. Calls to external Lean-defined spec helpers (e.g., sumTo in a hand-written .spec.lean) pass through unqualified.

Proof note: Since the method body is return Pure.foo ..., proofs need unfold Pure.foo before loom_solve to expose the logic.

---

4. User-Written .proof.lean File

import «binarySearch.def»

set_option loom.semantics.termination "total"
set_option loom.semantics.choice "demonic"

prove_correct binarySearch by
  loom_solve

This is the simplest proof — delegate everything to loom_solve. When loom_solve fails:

1. lsc check reports unsolved goals.
2. The user (or LLM) edits .proof.lean to add fallback tactics:

prove_correct binarySearch by
  loom_solve!
  · -- handle remaining goal
    grind

3. Or the user adds helper lemmas to .spec.lean that loom_solve can use.

Invariants are part of the method definition (in the //@ annotations), not the proof. If an invariant is missing, the user adds //@ invariant to the TS file and regenerates .def.lean.

4.1 Standalone Lemmas

Properties about functions can be proved as standalone Hoare triples in .proof.lean, separately from the function's requires/ensures. This is useful when:

• The function has no natural precondition but interesting properties hold under specific conditions
• Multiple properties should be proved about the same function
• The property involves multiple functions

-- The function has no ensures — just loop invariants
prove_correct runSession by
  loom_solve

-- Property proved separately as a Hoare triple
open TotalCorrectness DemonicChoice in
theorem runSession_timeout_resets (events : Array Event)
    (h1 : events.size > 0) (h2 : lastEvent events = .timeout) :
    triple (events.size > 0 ∧ lastEvent events = .timeout)
           (runSession events)
           (fun res => res = State.idle) := by
  unfold runSession
  loom_solve

The pattern: unfold the method to expose the body, then loom_solve to discharge the VCs.

---

5. LemmaScript Lean Library

The LemmaScript Lean library provides:

1. Re-exports of Velvet (forked) and Loom. Users import LemmaScript and get everything.
2. Velvet fork: One change from upstream — obligations are persisted across files so prove_correct works in a separate file from method.
3. WPGen rules and simp lemmas for Option (WPGenOption.lean: dependent if-then-else / dite) and HashSet (WPGenHashSet.lean: insert size bounds, strip_withname tactic).

The library depends on:

• Velvet (forked, which depends on Loom, which depends on mathlib)
• Z3 and cvc5 (downloaded by the lakefile)

Pre-built oleans are distributed so user projects skip compilation.

Future: replacing Velvet with LemmaScript-native macros. The Velvet fork is pragmatic for Phase 1. Long term, building our own Lean macros on Loom directly would give us: exact control over the generated proof state (no WithName surprises), TS-specific constructs without waiting on Velvet, error messages that reference TS source instead of Velvet internals, and independent evolution from Velvet's Dafny-oriented design.

---

6. Findings from Phase 0

Empirical constraints discovered during prototyping. They inform the design but should be re-validated.

6.1 Int vs Nat

• All TS number variables default to Int in Lean.
• Variables annotated //@ type v nat become Nat.
• Mixing Int and Nat in comparisons is fine — Lean coerces Nat to Int.
• Quantifier types must be consistent within a property: don't use k : Int in an invariant and k : Nat in the ensures for the same property.
• arr.size is Nat. No explicit ↑ coercion needed.
• Array indexing: arr[i]! for Nat, arr[i.toNat]! for Int.
• Recursive ghost functions on array indices should take Nat. Calling code should use //@ type for the index variable.
• Bridge lemmas (e.g., (i + 1).toNat = i.toNat + 1) may be needed in .spec.lean when mixing Int and Nat.

6.2 loom_solve Capabilities

• Discharges most VCs for array algorithms automatically.
• Handles all comparison directions (≥, >, ≤, <).
• Needs ghost functions tagged @[grind, loomAbstractionSimp].
• Recursive ghost functions may need explicit step lemmas with the same attributes.
• Cannot invent loop invariants. Missing or weak invariants produce unsolved goals.
• Cannot bridge (i + 1).toNat to i.toNat + 1 without a lemma.

6.3 Velvet Specifics

• method syntax handles require, ensures, invariant, done_with, decreasing, break, mutable variables.
• return not supported inside loops — users restructure to break + result variable.
• done_with captures what is true when the loop exits (by condition or by break).
• prove_correct works across files (with our fork's persistence fix).
• loom_solve! shows unsolved goals for debugging.

6.4 Decreasing Clauses

• Lean accepts any well-founded relation: Nat, tuples (lexicographic), etc.
• Nat expressions work directly (e.g., arr.size - i where i : Nat).
• Int expressions need .toNat (e.g., (hi - lo + 1).toNat).
• Avoid mixing Nat and Int in subtraction: (arr.size - i).toNat where i : Int causes issues. Either make i : Nat or use arr.size - i.toNat.