From d4a0532090aeb1b9c350494651b9113a8988793f Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 16 Jul 2026 19:02:40 +0100 Subject: [PATCH 1/5] tweaks for Lean: order of decls need toposort, plus minor parentheses --- tools/src/lean-emit.ts | 53 +++++++++++++++++++++++++++++++++++++++--- tools/src/transform.ts | 16 +++++++++++++ 2 files changed, 66 insertions(+), 3 deletions(-) diff --git a/tools/src/lean-emit.ts b/tools/src/lean-emit.ts index dbdc4b9..c58b386 100644 --- a/tools/src/lean-emit.ts +++ b/tools/src/lean-emit.ts @@ -464,8 +464,13 @@ function emitExpr(e: Expr, parentPrec?: number): string { // Same unsupported-real story as the `real` type case in tyToLean. throw new Error("real arithmetic is not supported by the Lean backend (needs noncomputable ℝ / Mathlib)."); - case "index": - return `${emitExpr(e.arr)}[${emitExpr(e.idx)}]!`; + case "index": { + const arr = emitExpr(e.arr); + // Parenthesize a low-precedence array expr (e.g. a function application) + // so the index binds to the whole thing, not its last token. + const wrap = e.arr.kind === "app" || e.arr.kind === "binop" || e.arr.kind === "methodCall" || e.arr.kind === "if" || e.arr.kind === "let" || e.arr.kind === "unop"; + return `${wrap ? `(${arr})` : arr}[${emitExpr(e.idx)}]!`; + } case "record": { const fields = e.fields.map(f => `${escapeName(f.name)} := ${emitExpr(f.value)}`); @@ -644,6 +649,48 @@ function emitStmt(s: Stmt, indent: number): string { // ── Declaration emission ───────────────────────────────────── +/** Collect every function/variable name an IR tree references (stripping any + * `Pure.` qualifier), via a generic walk over `app`/`var` nodes. */ +function collectRefNames(node: unknown, into: Set): void { + if (node === null || typeof node !== "object") return; + if (Array.isArray(node)) { for (const x of node) collectRefNames(x, into); return; } + const n = node as { kind?: string; fn?: unknown; name?: unknown }; + if (n.kind === "app" && typeof n.fn === "string") into.add(n.fn.replace(/^Pure\./, "")); + if (n.kind === "var" && typeof n.name === "string") into.add(n.name.replace(/^Pure\./, "")); + for (const k of Object.keys(node)) collectRefNames((node as Record)[k], into); +} + +/** Lean requires definition-before-use: order sibling decls so one that + * references another is emitted after it. Cycles are left in place (they would + * need a `mutual` block). Bails to the original order if any decl is unnamed. */ +function orderDeclsByDeps(decls: Decl[]): Decl[] { + const named = decls.filter((d): d is Decl & { name: string } => typeof (d as { name?: unknown }).name === "string"); + if (named.length !== decls.length) return decls; + const names = new Set(named.map(d => d.name)); + const byName = new Map(named.map(d => [d.name, d])); + const deps = new Map(); + for (const d of named) { + const refs = new Set(); + collectRefNames(d, refs); + refs.delete(d.name); + deps.set(d.name, [...refs].filter(r => names.has(r))); + } + const sorted: Decl[] = []; + const done = new Set(); + const onStack = new Set(); + const visit = (name: string) => { + if (done.has(name) || onStack.has(name)) return; + onStack.add(name); + for (const dep of deps.get(name) ?? []) visit(dep); + onStack.delete(name); + done.add(name); + const def = byName.get(name); + if (def) sorted.push(def); + }; + for (const d of named) visit(d.name); + return sorted; +} + function emitDecl(d: Decl): string { switch (d.kind) { case "inductive": { @@ -725,7 +772,7 @@ function emitDecl(d: Decl): string { case "namespace": { const lines = [`namespace ${d.name}`]; - for (const inner of d.decls) lines.push("", emitDecl(inner)); + for (const inner of orderDeclsByDeps(d.decls)) lines.push("", emitDecl(inner)); lines.push("", `end ${d.name}`); return lines.join("\n"); } diff --git a/tools/src/transform.ts b/tools/src/transform.ts index 097dbcf..60837b0 100644 --- a/tools/src/transform.ts +++ b/tools/src/transform.ts @@ -192,6 +192,14 @@ let _opts: TransformOptions = DAFNY_OPTIONS; /** Type declarations — set once per module transform for discriminated union handling. */ let _typeDecls: TypeDeclInfo[] = []; +/** Names of functions that get a `Pure.` mirror (Lean). A bare reference to one + * in a higher-order position resolves to the monadic method, so it must be + * redirected to the pure mirror. Set once per module transform. */ +let _pureDefNames: Set = new Set(); + +/** Array methods that take a function argument. */ +const HOF_METHODS = new Set(["map", "filter", "every", "some", "find", "findLast", "findIndex", "findLastIndex", "reduce"]); + /** Prefix match-bound field names to avoid capturing user variables. * When prefix is given (the scrutinee name), include it to avoid * collisions in nested matches on different variables. `freshName` closes @@ -774,8 +782,15 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr { if (e.fn.kind === "field") { const recv = lowerExpr(e.fn.obj, binds); let method = e.fn.field; + const isHOF = e.fn.obj.ty.kind === "array" && HOF_METHODS.has(method); const args = e.args.map((a, i) => { const lowered = lowerExpr(a, binds); + // Lean: a pure fn passed to a HOF by name resolves to the monadic + // method; redirect to its pure `Pure.` mirror. + if (_opts.backend === "lean" && isHOF && + lowered.kind === "var" && _pureDefNames.has(lowered.name)) { + return { kind: "var" as const, name: `Pure.${lowered.name}` }; + } // Array index args must be nat in Lean: `with`'s index (0), includes/indexOf `from` (1). const isArrIdxArg = e.fn.kind === "field" && e.fn.obj.ty.kind === "array" && ((e.fn.field === "with" && i === 0) || ((e.fn.field === "includes" || e.fn.field === "indexOf") && i === 1)); @@ -2191,6 +2206,7 @@ export function transformModule(mod: TModule, specImport?: string, moduleBaseOve _forofCounters.clear(); _liftCounter = 0; _typeDecls = mod.typeDecls; + _pureDefNames = new Set(mod.functions.filter(f => f.isPure).map(f => f.name)); const typeDecls = mod.typeDecls.map(transformTypeDecl); // Module-level constants From 440f6f217aae3236105c19e56e8b1bf584ff7611 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 16 Jul 2026 19:04:35 +0100 Subject: [PATCH 2/5] another parenthesis fix --- tools/src/lean-emit.ts | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tools/src/lean-emit.ts b/tools/src/lean-emit.ts index c58b386..2c4bff2 100644 --- a/tools/src/lean-emit.ts +++ b/tools/src/lean-emit.ts @@ -795,8 +795,10 @@ function emitDecl(d: Decl): string { if (d.requires.length === 0 && d.ensures.length === 0) return sig; // Spec axiom: ∀ params, req1 → … → (ens1 ∧ … ∧ ensN). Tagged `@[grind]` so // the proof automation can use it, matching the ghost-function convention. - const hyps = d.requires.map(emitExpr); - const concl = d.ensures.map(emitExpr).join(" ∧ "); + // Parenthesize each clause: an unwrapped `∀ k, P` would otherwise swallow + // the following ` ∧ …` conjuncts into its body. + const hyps = d.requires.map(e => `(${emitExpr(e)})`); + const concl = d.ensures.map(e => `(${emitExpr(e)})`).join(" ∧ "); const axBody = [...hyps, concl].join(" → "); const axiom = `@[grind] axiom ${escapeName(d.name)}_spec${params ? ` ${params}` : ""} : ${axBody}`; return `${sig}\n${axiom}`; From 5d4d800b4ed26155d6a5fe60a96a1f32f710f085 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 16 Jul 2026 19:25:54 +0100 Subject: [PATCH 3/5] retrigger CI after updates of case study From 75704e9887d3a2f4564c888370bb3f5d36f483b4 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 16 Jul 2026 19:28:56 +0100 Subject: [PATCH 4/5] retrigger CI after full updates of case study From 2f10bf94d097738152c1c9f1d9629cf943ea6960 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 16 Jul 2026 19:37:34 +0100 Subject: [PATCH 5/5] retrigger CI after updates of case study