LemmaScript

Imported from midspiral/LemmaScript (AGENTS.md). Install upstream with npx skills add midspiral/LemmaScript. Copyright stays with the author.

AGENTS.md

Guidance for AI coding agents working on LemmaScript itself or on projects that use it. Human-oriented docs live in README.md, SPEC.md, SPEC_DAFNY.md, SPEC_LEAN.md, DESIGN.md, TOOLS.md. This file collects the things that are easy to get wrong if you only read those.

What LemmaScript is

A verification toolchain for TypeScript. The user writes ordinary TS with //@ annotations. lsc generates either:

• Dafny — one .dfy.gen (always regeneratable) + one .dfy (the source of truth where proof additions accumulate). Diff must be additions-only.
• Lean 4 / Velvet / Loom — four files: .types.lean + .def.lean are generated; .spec.lean + .proof.lean are hand-written.

Whatever you do, the TS file is the source of truth for the program. The hand-written verification files are the source of truth for the proof. Don't conflate them.

Toolchain commands

npx lsc gen   --backend=<dafny|lean> path/to/foo.ts   # generate artifacts
npx lsc check --backend=<dafny|lean> path/to/foo.ts   # gen + verify
npx lsc regen --backend=dafny        path/to/foo.ts   # three-way merge after TS changes
npx lsc config                       path/to/foo.ts   # show effective options and Dafny artifact directory

Default backend is Dafny. Pass --backend=... explicitly anyway — case-study CIs and helper scripts all do, and the default has been flipped before.

If lemmascript.json sets proof-dir, all Dafny companions (.dfy.gen, .dfy, .dfy.base, .dfy.merged) live in the mirrored directory reported by lsc config, not beside the TS file. The edit boundaries and regen rules below apply at that mapped location unchanged.

After editing lsc itself (anything under tools/), run npm run build before re-invoking npx lsc — the CLI runs the compiled tools/dist/lsc.js, not the TS source.

File-edit boundaries

Never edit these — they are regenerated from .ts:

• foo.dfy.gen (Dafny)
• foo.types.lean, foo.def.lean (Lean)

If a generated file is wrong, the fix is in foo.ts (or in the emitter under tools/), not in the generated file. The .gen extension on the Dafny file is a deliberate signal — it keeps Dafny tooling from auto-verifying it and reminds you it is not the source of truth.

Edit these freely — they hold proofs:

• foo.dfy (Dafny) — copy of .dfy.gen plus additions
• foo.spec.lean (Lean) — ghost definitions and helper lemmas
• foo.proof.lean (Lean) — prove_correct plus tactics

For Dafny, the diff between foo.dfy.gen and foo.dfy must be additions-only. You may insert helper lemmas, ghost predicates, asserts, and loop invariants, but you may not modify or delete generated lines. lsc check enforces this. (A subtle trap: don't append a trailing comment to a generated line like { or decreases fuel — that counts as a modified generated line. Put your comment on its own new line.)

Function-level ensures for caller composition

A TS //@ ensures always emits a separate <fn>_ensures lemma; the generated Dafny function carries only requires/decreases. Since a Dafny function can't invoke a lemma, a function caller can't see a callee's postcondition — e.g. g() calling h(f(x)) where h requires arg >= 0 and f's >= 0 lives only in f_ensures will not verify.

Fix: hand-add the ensures to the generated Dafny function as an addition. Dafny discharges it inline against the body — even recursively (the function's own postcondition serves as the IH, e.g. ensures scan(...) >= startDay on a recursive scan). Callers then compose it with no lemma call. Keep it additions-only: put the ensures (and any comment) on their own new lines, above the {.

Regen, don't rm

When the TS changes and the existing foo.dfy needs to absorb the new generated code:

npx lsc regen --backend=dafny foo.ts

Do not rm foo.dfy foo.dfy.gen && npx lsc gen ... — that drops every proof addition you (or the previous agent) made in foo.dfy. regen does a three-way merge against the old .dfy.gen and preserves additions. On conflict it restores the original foo.dfy and writes the merged result to foo.dfy.merged for manual inspection.

When regen needs merge-state recovery

regen anchors its three-way merge on foo.dfy.base if that file exists, otherwise on the previous .dfy.gen. When a merge is clean but verification fails, regen advances foo.dfy.base to the newly generated .dfy.gen before reporting failure. That anchor is intentional: the proof file already contains the new generated content, so the next regen can preserve proof additions while merging from the generation it actually contains.

A merge conflict keeps the old anchor and restores the original proof; inspect foo.dfy.merged before retrying. An additions-only failure also keeps the old anchor; repair the generated-line changes in the proof. Do not delete either anchor merely to make the next command run.

A successful regen removes .dfy.base, including under --no-verify after a clean additions-only merge. To clear recovery state manually, first confirm that the proof matches the current generated file and verifies:

npx lsc check --backend=dafny foo.ts && rm -f foo.dfy.base

Only after that successful check is the current .dfy.gen an established replacement anchor. On older checkouts, back up the proof and recovery files before investigating a suspected stale anchor; a failed command alone is not evidence that deleting it is safe. Keep *.dfy.base out of version control.

Annotation pitfalls

These are the ones that bite repeatedly:

• //@ assume is not a proof shortcut. It emits assume P; in Dafny, telling the verifier to trust P unconditionally. It is appropriate to constrain a //@ havoc'd value (whose true behavior is outside the LS fragment) — and that's about it. Don't reach for it to paper over a proof obligation you don't feel like discharging. If you find yourself adding //@ assume to make verification pass on code you wrote, restructure the algorithm or prove the lemma. (Same goes for //@ assume false to silence a throw new Error(...) path — instead, characterize the valid-input domain in //@ requires.)
• //@ havoc is Dafny-only. It marks the RHS of a declaration or assignment as nondeterministic. The Lean backend will reject files that use it. Pair it with //@ assume immediately after if you need to constrain the resulting value (|cleaned| <= |text|, for example).
• //@ extern is the deterministic cousin of //@ havoc. Use it when callers should reason parametric over a function whose body is out of model (regex, IO, parser). The axiom is deterministic and extensional — proofs that depend on f(x) == f(x) go through. Add //@ impure to an extern (or to a cross-file source declaration) when each call needs an independent result; this emits a body-less Dafny method and does not model shared heap effects.
• //@ annotations don't support \old(...). For mutating methods, this.field in ensures is the post-state; pre-state references must be added as old(this.field) in .dfy proof additions (see SPEC.md §2.8).
• Empty Dafny lemma body means proven. lemma foo() ensures P {} is auto-discharged by Z3 — it is not "skipped" or "unproven." Only assume / havoc / weak specs side-step the verifier.
• Regex isn't in the model. Code that uses RegExp, String.prototype.match, String.prototype.replace(regex, ...), etc. cannot be verified inside the LS fragment. Either rewrite to non-regex string operations, or wrap the regex behind //@ havoc / //@ extern and verify the surrounding logic.

Dafny verification workflow

Single-lemma iteration is far faster than re-verifying the whole file:

dafny verify --filter-symbol=lemma_name foo.dfy

For a final whole-file pass, run once and inspect with tail -50 rather than narrowing with grep — the verifier's summary line lives at the end, and a partial grep can hide errors that don't match your filter pattern. Add --isolate-assertions when one lemma has many conjuncts and you want a clean breakdown of which conjunct is failing; add --verification-time-limit=<sec> when the default 30s isn't enough.

Nonlinear arithmetic: reach for the standard library, don't hand-roll

Goals involving multiplication/division of variables — (m*p)/p == m, (m*p)%p == 0, x <= y ==> x*p <= y*p — are nondeterministic in Z3: they verify on one run and time out the next, even as isolated lemma goals. Hand-rolled inductive helpers don't rescue you, because the inductive step needs an equally-flaky div/mod-add fact ((q+p)%p == q%p).

The robust fix is Dafny's standard arithmetic library, whose Mul/DivMod lemmas are proven once, robustly:

import opened Std.Arithmetic.Mul       // LemmaMulInequality(x,y,z): x<=y && z>=0 ==> x*z<=y*z
import opened Std.Arithmetic.DivMod     // LemmaMulStrictInequality(x,y,z): x<y && z>0 ==> x*z<y*z
                                        // LemmaModMultiplesBasic(m,p): m>=0 && p>0 ==> (m*p)%p == 0

lsc's dafnyVerify (tools/dist/dafny-commands.js) auto-adds --standard-libraries whenever the .dfy text contains the substring Std. — so an import opened is all you need; no CLI flag or config change, and lsc check picks it up. The imports go in as an inserted block (additions-only — don't touch the generated header). Euclidean identities (x == x/p*p + x%p, 0 <= x%p < p) and small distributivity ((k+1)*p == k*p + p) are reliable inline; reserve the library for the cancellation and monotonicity goals.

Lean verification workflow

lake build runs the full chain. loom_solve is the default tactic for discharging Velvet VCs, but it does not automatically apply step lemmas to recursive helpers — for those, you need an explicit chain (e.g., loomAbstractionSimp + the step lemma name) rather than a bare loom_solve.

.spec.lean is for ghost definitions and helper lemmas; .proof.lean is for prove_correct plus the tactic script. Keep them separate; don't push everything into .proof.lean.

Brownfield (existing TS codebases)

When verifying a small slice of a larger TS project:

• Add //@ verify to the function bodies you want verified. As soon as any function in the file has it, lsc switches to opt-in mode and silently skips the rest. Type and const declarations are always extracted.
• For functions outside the LS fragment that you still want callers to reason about, use //@ extern (deterministic axiom) or //@ havoc (nondeterministic).
• In-place means in-place. When the user asks for in-place verification of an existing function, add annotations only. Don't refactor the production code, don't restructure control flow, don't rename things. The point is that the verified function and the shipping function are byte-for-byte the same.

Case studies and external repos

If you are working in a <name>-lemmascript/ clone of an upstream library:

• Clone with full history. git clone --depth=1 will break case-study work that needs to compare against upstream commits.
• Confirm the upstream is TS-native before proposing it. Check repository, language, and the source tree on GitHub. A package with shipped @types/... and types-at-API but a JS source tree (e.g., semver) is not a LemmaScript brownfield candidate.
• Pick algorithms where the proof difficulty is the cleverness. A case study lands well when the interesting part of the proof is the algorithmic insight (an invariant, a witness construction, a partition argument), not data-structure plumbing.
• Don't reference other case studies or working design docs from production source comments. // see DESIGN_X.md for context and // like the foo-lemmascript pattern rot fast and are noise in the verified TS.

Style for repo edits

• README case-study entries: ~2–3 sentences, headline technique only. Lead with what makes the case study compelling (the WHY — what was proven and why it matters), not a function-by-function enumeration. Don't overclaim ("verified end-to-end") and don't apologize ("just a demo") — name the trust assumption inline.
• SPEC.md / SPEC_DAFNY.md / SPEC_LEAN.md subsections: match the existing peers in length (~15 lines per subsection). Don't expand a section into multiple subheadings to fit a new feature; usually a sentence and a code block is enough.
• No customer or partner names in persisted docs. Use generic terms ("a pilot," "a brownfield user") instead.
• Light edits stay light. When the user says "lightly edit" or "one-paragraph edit," that's a single paragraph with no new sub-headings.

When in doubt

• Re-read the relevant SPEC.md section before adding an annotation you haven't used before.
• lsc extract foo.ts prints the Raw IR JSON — useful when the toolchain is doing something you don't expect and you need to see what extract produced.
• If a generated file looks wrong, the bug is in tools/ (most likely transform.ts, peephole.ts, or one of the emitters), not in the generated text.