Toolchain architecture

The lsc toolchain translates annotated TypeScript to formal verification artifacts (Lean or Dafny), using ts-morph.

Pipeline

TS source (.ts)
  → extract    (ts-morph → Raw IR)
  → resolve    (Raw IR → Typed IR; types and type-narrowing only)
  → narrow     (Typed IR → Typed IR; structural narrowing — `someMatch` rewrites)
  → transform  (Typed IR → IR, configured per backend)
  → peephole   (IR → IR, local rewrites that eliminate Some/None ceremony)
  → emit       (IR → Lean text or Dafny text)

Three IRs

Raw IR (rawir.ts)

Structured AST from ts-morph. Expressions are nodes, not strings. Has declared type references (tsType: "Packet") but no resolved types. Close to TS syntax.

• RawExpr: var, num, str, bool, binop, unop, call, index, field, record, arrayLiteral, lambda, conditional, optChain (obj?.…), nullish (a ?? b), emptyCollection (new Map/new Set), nonNull (e!); spec-only: result (\result), forall, exists, havoc
• RawStmt: let, assign, return, break, continue, expr, if, while, switch, forof, throw; spec-only: ghostLet, ghostAssign, assert
• //@ annotations remain as strings (parsed by specparser in the resolve pass)

Typed IR (typedir.ts)

Raw IR annotated with resolved types and classifications. Produced by a resolve pass that runs once. Still TS-shaped, not backend-shaped.

Each expression carries:

• ty: Ty — resolved LemmaScript type (nat, int, bool, array, user, etc.)
• Calls carry callKind (pure, method, spec-pure, unknown)
• Discriminant fields identified

Each statement carries type information for variables. Unsupported patterns (data-carrying variant equality, return in loop) are rejected here with source locations.

IR (ir.ts)

Backend-neutral intermediate representation. Produced by the transform from Typed IR. Consumed by either emitter. Types are preserved as Ty objects (not converted to strings) — each emitter converts to its own type syntax.

Type names: Expr, Stmt, Module, MatchArm, StmtMatchArm, and Decl = Inductive | Structure | FnDef | FnDefByMethod | FnMethod | Namespace | ClassDecl | ConstDecl | TypeAlias | ExternDecl. (FnDefByMethod is a //@ pure function whose body can’t be a pure expression — emitted as a Dafny function-by-method.)

Phases

Extract (extract.ts): ts-morph → Raw IR. Walks the TS AST, produces structured expression nodes. Only string outputs are //@ annotation text. Two backend-neutral CLI commands stop here. lsc extract foo.ts dumps the Raw IR as JSON — external tools can consume it instead of re-parsing TS, e.g. lemmascript-claimcheck reads each function’s //@ contract, requires, and ensures to check the prose against the spec. lsc info foo.ts writes foo.ts.json, a per-function spec summary ({ name: { sig, requires, ensures, decreases } }, class methods keyed Class.method) — see info-command.ts.

Resolve (resolve.ts): Raw IR → Typed IR. Resolves types from ts-morph type info and //@ type annotations. Classifies calls. Identifies discriminants. Rejects unsupported patterns. Parses //@ annotations with the specparser. Carries narrowing context (env, narrowedPaths) so that the then-branch of if (e !== undefined) resolves with e’s unwrapped type — TS-faithful: simple vars and pure access paths (a.b.c, any depth) narrow. && chains accumulate narrowings (each premise in scope for later ones); ==> propagates premise narrowings into the conclusion. Type narrowing only — no structural rewriting.

Narrow (narrow.ts): Typed IR → Typed IR. Owns all structural narrowing — both for optional checks and for discriminated unions. Optional patterns rewrite to someMatch; discriminant patterns (x.kind === "v", 'k' in x, Array.isArray(x) for synthesized array-unions, x.kind !== "v") return; ...) rewrite to tagMatch. Also handles ==> premise narrowing in specs, left ?? right (nullish coalescing), k in m ? m[k] : default for map-typed m, and obj?.<chain> for any combination of ?.field, ?.foo(), ?.[i], and continuations (via the optChain IR node). Rules fire for pure access paths (var(x), field(purePath, name)); optChain and nullish are the sole paths for complex scrutinees. See Narrow rules below.

Transform (transform.ts): Typed IR → IR. Consumes resolved types and classifications. Pattern-matches on ty to decide: constructor vs string, .toNat vs direct, if vs match, pure def vs method. Configured with TransformOptions for backend-specific behavior (backend, monadic). Lowers someMatch to IR match Some/None — substituting the binder for any pure access path scrutinee, or lowering naively when the scrutinee is complex (narrow pre-bound the someBody). No optional-narrowing logic of its own.

Peephole (peephole.ts): IR → IR. Local rewrite rules applied bottom-up to fixed point. Eliminates wrap-then-unwrap ceremony around partial-access expressions like m.get(k) (which is internally lowered to methodCall(map, "get", [k]) and emits as (if k in m then Some(m[k]) else None)). See Peephole rules below.

Emit (lean-emit.ts / dafny-emit.ts): IR → text. Each emitter maps Ty objects to backend type syntax and method calls to backend-specific syntax.

Method Calls

All TS receiver.method(args) calls produce methodCall IR nodes carrying the receiver, its type, the TS method name, the args, and a monadic flag. No renaming — the IR stores the TS name ("map", "indexOf", "with", "get", etc.) and the receiver type disambiguates.

Each emitter dispatches on (receiverTy, method) to decide syntax. For example, (array, "map") → Lean: arr.map f, Dafny: Seq.Map(f, arr). Unsupported (type, method) pairs error at emit time.

app is reserved for receiver-less calls: user-defined functions, Pure.fnName(...), JSFloorDiv(a, b), SetToSeq(s).

Externs

When a call resolves to a pure function declared in a different .ts file, extract records it as a RawExtern (resolved to TExtern, lowered to ExternDecl). The Dafny emitter renders these as top-of-file function {:axiom} Name(...): R with the source declaration’s requires/ensures lifted along, so callers reason against the same contract the source verified. Externs are emitted before all other declarations so they’re in scope everywhere.

Spec Expression Parser

The specparser (specparser.ts) parses //@ annotation expressions into RawExpr nodes. Called by the resolve pass, not by extract or transform.

Adding a New Feature

1. Extract: add the TS construct to Raw IR.
2. Resolve: add type resolution and classification for the new construct.
3. Narrow (only if it introduces a narrowing pattern): add a rule that detects the pattern and rewrites to someMatch.
4. Transform: add an IR lowering rule that pattern-matches on the typed node.
5. Emit: add backend-specific rendering in each emitter if the new IR node needs special syntax.

Scoping

The resolve pass uses linked environments (Scheme-style). Each binding is a frame with one name, one type, and a pointer to the parent:

interface Env { name: string; ty: Ty; parent: Env | null }

let extends the chain. Lookup walks it. No mutation, no maps, no copying. resolveStmt returns [TStmt, Env] so bindings thread through a block. Block-creating constructs (if, while, forof, switch) call resolveBlock; inner bindings don’t leak out. let x = init resolves init before adding x to the env.

Known Limitations

• Data-carrying variant equality: //@ requires m.tag === "b" where b carries data throws an error. Use switch to destructure instead.
• For-of desugaring leaks index variable: _x_idx is visible in //@ invariant and //@ done_with annotations.
• Spec annotations are strings: //@ expressions are parsed by the specparser, not extracted from ts-morph. They don’t benefit from the structured raw IR.

Lean Backend

Pipeline

TS source (.ts)
  → extract    (ts-morph → Raw IR)
  → resolve    (Raw IR → Typed IR)
  → narrow     (Typed IR → Typed IR)
  → transform  (Typed IR → IR, with LEAN_OPTIONS)
  → peephole   (IR → IR)
  → emit       (IR → Lean text)

Commands (lean-commands.ts)

• lsc gen foo.ts — generate .types.lean + .def.lean
• lsc check foo.ts — gen + lake build

Dafny Backend

Pipeline

TS source (.ts)
  → extract    (ts-morph → Raw IR)
  → resolve    (Raw IR → Typed IR)
  → narrow     (Typed IR → Typed IR)
  → transform  (Typed IR → IR, with DAFNY_OPTIONS)
  → peephole   (IR → IR)
  → dafny-emit (IR → Dafny text)

Two-File System

Each TS source produces two Dafny files:

• foo.dfy.gen — always regeneratable from TS. The merge base.
• foo.dfy — source of truth. Starts as a copy of .dfy.gen, then accumulates user/LLM proof additions. The diff between .dfy.gen and .dfy must be additions-only.
• foo.dfy.base — transient three-way-merge anchor written by regen when a regenerated .dfy.gen diverges from a dirty .dfy; deleted on a clean, verified merge.

Commands (dafny-commands.ts)

• lsc gen --backend=dafny foo.ts — generate .dfy.gen + seed .dfy
• lsc gen-check --backend=dafny foo.ts — gen + additions-only check (no dafny verify)
• lsc regen --backend=dafny foo.ts — regenerate .dfy.gen, three-way merge, verify
• lsc check --backend=dafny foo.ts — gen + additions-only check + dafny verify

Narrow Rules

narrow.ts (structural-narrowing rewrite pass) takes typed IR and rewrites narrowing patterns into IR nodes that transform lowers uniformly: someMatch (binary, for optional checks) or tagMatch (multi-case, for discriminated unions). Each carries the scrutinee, the matched cases, and the fallthrough.

The walker is bottom-up over TExpr/TStmt. At each node, recurse into children, then try the rules in order.

Throughout, e !== undefined includes equivalent forms: undefined !== e, bare truthiness e where e is optional-typed, and (for the negative direction) e === undefined, undefined === e, !e.

Statement-level rules — optional narrowing

Pattern	Rewrites to
if (e !== undefined) S (some-branch non-empty)	someMatch e { Some(_e_val) => S, None => {} }
if (e === undefined) terminate; rest (some-branch empty + rest)	someMatch e { Some(_e_val) => rest, None => terminate }
if (e !== undefined && rest) S (no else)	someMatch e { Some(_e_val) => if rest S, None => {} }
e !== undefined && rest (bare expression statement — the if-less guard idiom)	someMatch e { Some(_e_val) => rest;, None => {} }
if (a === undefined || b === undefined || ...) terminate; rest	nested someMatch for each var, deepest body is rest
let x = (e_opt && rest) ? a : b (statement, impure-OK guard)	var x := b; someMatch e_opt { Some(_v) => { if rest { x := a } } }

Statement-level rules — discriminated-union narrowing (emit tagMatch IR)

Pattern	Rewrites to
if (x.kind === "v1") S1 [else if (x.kind === "v2") S2 ...] (also 'k' in x and Array.isArray(x) forms)	tagMatch x { v1 => S1, v2 => S2, ..., _ => fallthrough }
if (x.kind !== "v") terminate; rest (also !Array.isArray(x) form)	tagMatch x { v => rest, _ => terminate }
if (<rest> && Array.isArray(path) && <more>) S [else]	tagMatch path { ArrayBranch => if (<rest && more>) S [else] }

For the chain and neg-early-return rules, the Array.isArray(x) / !Array.isArray(x) discriminant forms require a bare-var scrutinee (the var-name-keyed replacement in transform only handles that shape); path scrutinees like m.content go through the expression-form rules below.

Expression-level rules

Pattern	Rewrites to
e !== undefined ? a : b	someMatch e { Some(_e_val) => a, None => b }
e !== undefined && rest ? a : b (pure rest)	someMatch e { Some(_e_val) => if rest then a else b, None => b }
opt ? a : b (truthiness; cond is optional-typed)	someMatch opt { Some(_opt_val) => a, None => b }
left ?? right (nullish coalescing)	someMatch left { Some(_v) => _v, None => right }
path !== undefined [&& rest] ==> B (spec implication)	someMatch path { Some(_p_val) => (rest ==> B), None => true }
optChain(obj, chain) (from extract’s obj?.<chain> — chain may be field/call/index steps)	someMatch obj { Some(_oc{N}_val) => apply(chain, _oc{N}_val), None => undefined }
k in m ? m[k] : default (m map-typed; then-branch is exactly m[k], default non-optional)	someMatch m[k] { Some(_m_k_val) => _m_k_val, None => default }

The &&-ternary rule skips when rest contains impure method calls (those would be lifted out of the match arm by transform, breaking binder scope) — the let-cond statement-level rule handles those. Both &&-ternary and ==> rules walk their inner expression recursively so chained checks (a !== undefined && a.b !== undefined ? ... : ..., ... ==> ...) become nested someMatches. The bare-statement && rule (above) has no such restriction: its arm is a statement-level someMatch, which keeps a guarded call in statement position, so transform never ANF-lifts it out. It likewise walks rest as a statement, so chained checks nest.

The k in m map rule mirrors the discriminant-in path but is gated on map; the existing Dafny Map.get peephole then collapses the result back to if k in m then m[k] else default.

Expression-level rules — Array.isArray narrowing (synthesized array-unions, discriminant "__isArray__"; emit tagMatch IR). The matched arm rewrites bare x references to the variant’s payload field (e.g. x.arr) at transform time; scrutinee may be any narrowable path (var or field chain).

Pattern	Rewrites to
Array.isArray(x) ? a : b (or !Array.isArray(x) ? a : b)	tagMatch x { ArrayBranch => a } fallthrough b (NonArrayBranch when negated)
(<rest> && Array.isArray(path)) ? a : b	tagMatch path { ArrayBranch => (<rest>) ? a : b } fallthrough b
Array.isArray(x) ==> B (or !Array.isArray(x) ==> B)	tagMatch x { ArrayBranch => B, _ => true } (NonArrayBranch when negated)

The ==> form mirrors ruleImplOptional: the unmatched variant becomes a vacuous-true fallthrough, since the implication is trivially satisfied when the premise is false.

Scrutinee handling

All optional-narrowing rules above (except optChain and nullish) accept any pure access path (var(x), field(var(o), f), or any depth of field(field(...), name)) — matching TS, which narrows access paths but not method-call results. The rules build someMatch with the body still referencing the scrutinee; transform substitutes via replacePathInTExpr / replacePathInTStmts at lowering time. Binder name joins the path: _root_val for a bare var, _root_f1_f2_val for root.f1.f2.

The optChain and nullish rules are exceptions: their scrutinee can be any expression (call result, deep chain, etc.), and narrow constructs the someBody to reference the binder directly — so transform’s lowering skips substitution for complex scrutinees.

The statement-level discriminant rules require the scrutinee to be a simple var (x.kind === "v" requires x to be a var; likewise the Array.isArray(x) statement forms). Transform’s emitMatchStmt does the variant destructuring (replaces x.field with the variant binder). Discriminator must be the named discriminant field of a user discriminated-union type. The expression-form Array.isArray rules relax this to any narrowable path (var or field chain).

Peephole Rules

Local IR-to-IR rewrites applied bottom-up to fixed point at each node, in peephole.ts. They eliminate Some/None ceremony that comes from Map.get(k) and Record<K,V> index access (both lowered to methodCall(map, "get", [k]), which dafny-emit renders as (if k in m then Some(m[k]) else None)).

Each rule is local and semantics-preserving. The pass takes a backend parameter — some rules are Dafny-only (see below).

Map.get rules (both backends)

Expression rules

Pattern	Rewrites to
match m.get(k) { Some(v) => sb, None => nb }	if k in m then (let v = m[k] in sb) else nb
let x = m.get(k) in match x { Some(v) => sb, None => nb } (when x not used in arms)	if k in m then (let v = m[k] in sb) else nb

Statement rules

Pattern	Rewrites to
match m.get(k) { Some(v) => sb, None => nb } (statement-level)	if k in m { var v := m[k]; sb } else { nb }
let x = m.get(k); match x { Some(v) => sb, None => nb } (when x not used after)	if k in m { var v := m[k]; sb } else { nb }

The let-collapse rules require the bound variable to not be referenced after the match (conservative use-count check, no shadowing analysis). When the variable is referenced elsewhere, the let is preserved and only the inline match rule fires.

The bound value m[k] is captured once via let (expression form) or var (statement form). Substitution would re-evaluate m[k] at every use, which changes semantics if the body mutates m.

Boolean simplification rules (Dafny only)

Pattern	Rewrites to
if c then false else true	¬c
if c then true else false	c
if c then b else false	c && b
if c then true else b	c || b

These apply only for the Dafny backend. They emit ∧/∨ in the IR, which:

• Dafny renders as &&/|| — short-circuit Bool, sound for termination analysis when the right operand contains a recursive call.
• Lean renders as ∧/∨ — Prop conjunction/disjunction, which evaluate both arguments. For recursive functions like if n = 0 then true else f(n - 1) ∧ ..., the recursive call appears unconditionally in the term and Lean’s structural-termination check fails.

For Lean we keep the original if-then-else form, which preserves the conditional structure and lets Lean see that the recursive branch is reachable only when the guard holds.

Emitter precedence

The Dafny emitter wraps if-then-else and let (var-binding) expressions in parentheses (alongside match). Without the parens, an outer arr[idx] post-fix would parse into the else branch — e.g., if c then a else [] followed by [i] becomes ... else [][i] which type-checks against the [] rather than the whole if. Always wrapping is verbose but safe.

Current State

File	Phase	Role
rawir.ts	Types	Raw IR type definitions
extract.ts	Extract	ts-morph → Raw IR
specparser.ts	(parser)	Parses //@ annotations → RawExpr
resolve.ts	Resolve	Raw IR → Typed IR (types and type-narrowing)
typedir.ts	Types	Typed IR type definitions (incl. someMatch/tagMatch)
narrow.ts	Narrow	Typed IR → Typed IR (structural narrowing → someMatch / tagMatch)
ir.ts	Types	Backend-neutral IR type definitions
transform.ts	Transform	Typed IR → IR
peephole.ts	Peephole	IR → IR (Some/None ceremony elimination)
types.ts	(shared)	TypeDeclInfo, parseTsType
names.ts	(shared)	Fresh-name minting — collision-safe internal identifiers
lean-emit.ts	Emit	IR → Lean text
dafny-emit.ts	Emit	IR → Dafny text
lean-commands.ts	CLI	Lean gen/check commands
dafny-commands.ts	CLI	Dafny gen/gen-check/regen/check commands
info-command.ts	CLI	lsc info — per-function spec summary JSON
lsc.ts	CLI	Wires the pipeline, dispatches to backend