From 28d1deb6ff4a412e473fa4215f174fd2b1fac184 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Fri, 13 Nov 2026 00:59:32 -0500 Subject: [PATCH 1/4] fun spec for function by method stub so that it parses --- SPEC.md | 13 +++++++------ examples/countBadPairs.dfy | 29 ++++++++++++++++++++++++----- examples/countBadPairs.dfy.gen | 12 ++++++++++++ tools/src/dafny-emit.ts | 18 ++++++++++++++++-- 4 files changed, 59 insertions(+), 13 deletions(-) diff --git a/SPEC.md b/SPEC.md index 84d8559..9c7d586 100644 --- a/SPEC.md +++ b/SPEC.md @@ -993,8 +993,12 @@ function tagNameExists(m: Model, name: string, excludeTag?: TagId): boolean { If `transformPureBody` can auto-convert the body to a pure expression, the function emits as a normal Dafny `function`. If it cannot (e.g., the body has loops), it emits as `function by method`: ```dafny +// Specification of tagNameExists: add its body in the .dfy. +function tagNameExists_spec(m: Model, name: string, excludeTag: Option): bool + function tagNameExists(m: Model, name: string, excludeTag: Option): bool { + tagNameExists_spec(m, name, excludeTag) } by method { var i_tid_keys := SetToSeq(m.tags.Keys); @@ -1002,21 +1006,18 @@ by method { } ``` -The empty `{ }` block is the spec body placeholder — **Dafny will reject the file as a parse error until it is filled in**. Complete it in the `.dfy` file *before* running verify: +The functional body delegates to a bodyless `tagNameExists_spec` stub, so the generated file parses and resolves on its own. Give the stub a body in the `.dfy` by adding lines after its signature: ```dafny -function tagNameExists(m: Model, name: string, excludeTag: Option): bool +function tagNameExists_spec(m: Model, name: string, excludeTag: Option): bool { exists tid :: tid in m.tags && (match excludeTag { case None => true case Some(v) => v != tid }) && eqIgnoreCase(m.tags[tid].name, name) } -by method { - // ... auto-generated, preserved by regen -} ``` -The spec body is purely additive — `regen` three-way-merges and preserves user additions while updating the `by method` block when the TypeScript changes. +Dafny then verifies that the `by method` block computes `tagNameExists_spec`; left bodyless, the stub is uninterpreted and that proof fails. `regen` three-way-merges the `by method` block when the TypeScript changes without touching the added body. **Effect on callers:** Since `//@ pure` functions are `function`s in Dafny, callers that only invoke pure functions become pure automatically. For example, a large `switch`-based `apply` function becomes a `function` if all the map-iterating helpers it calls are marked `//@ pure`. diff --git a/examples/countBadPairs.dfy b/examples/countBadPairs.dfy index 2cee796..86bb5dc 100644 --- a/examples/countBadPairs.dfy +++ b/examples/countBadPairs.dfy @@ -26,13 +26,20 @@ function JSFloorDiv(a: int, b: int): int datatype Pair = Pair(i: nat, j: nat) // ═════════════════════ Iterative impls (function by method) ═════════════════════ -// Spec body delegates to the matching hand-written predicate, so the -// `by method` block verifies the imperative impl returns that set. +// Each generated `_spec` stub gets its body here: the matching +// hand-written predicate, so the `by method` block verifies the imperative +// impl returns that set. -function allPairsImpl(nums: seq): set +// Specification of allPairsImpl: add its body in the .dfy. +function allPairsImpl_spec(nums: seq): set { AllPairs(nums) } + +function allPairsImpl(nums: seq): set +{ + allPairsImpl_spec(nums) +} by method { var result: set := {}; var i := 0; @@ -60,10 +67,16 @@ by method { return result; } -function goodPairsImpl(nums: seq): set +// Specification of goodPairsImpl: add its body in the .dfy. +function goodPairsImpl_spec(nums: seq): set { GoodPairs(nums) } + +function goodPairsImpl(nums: seq): set +{ + goodPairsImpl_spec(nums) +} by method { var result: set := {}; var i := 0; @@ -93,10 +106,16 @@ by method { return result; } -function badPairsImpl(nums: seq): set +// Specification of badPairsImpl: add its body in the .dfy. +function badPairsImpl_spec(nums: seq): set { BadPairs(nums) } + +function badPairsImpl(nums: seq): set +{ + badPairsImpl_spec(nums) +} by method { var result: set := {}; var i := 0; diff --git a/examples/countBadPairs.dfy.gen b/examples/countBadPairs.dfy.gen index 92e5abd..8c046ec 100644 --- a/examples/countBadPairs.dfy.gen +++ b/examples/countBadPairs.dfy.gen @@ -13,8 +13,12 @@ function JSFloorDiv(a: int, b: int): int datatype Pair = Pair(i: nat, j: nat) +// Specification of allPairsImpl: add its body in the .dfy. +function allPairsImpl_spec(nums: seq): set + function allPairsImpl(nums: seq): set { + allPairsImpl_spec(nums) } by method { var result: set := {}; @@ -43,8 +47,12 @@ by method { return result; } +// Specification of goodPairsImpl: add its body in the .dfy. +function goodPairsImpl_spec(nums: seq): set + function goodPairsImpl(nums: seq): set { + goodPairsImpl_spec(nums) } by method { var result: set := {}; @@ -75,8 +83,12 @@ by method { return result; } +// Specification of badPairsImpl: add its body in the .dfy. +function badPairsImpl_spec(nums: seq): set + function badPairsImpl(nums: seq): set { + badPairsImpl_spec(nums) } by method { var result: set := {}; diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 6273ec5..04549f6 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -11,6 +11,8 @@ import { DEFAULT_OPTIONS, resolveOptions, type LscOptions } from "./config.js"; /** Appended to a function's name for the lemma that carries its `//@ ensures`. */ export const ENSURES_LEMMA_SUFFIX = "_ensures"; +/** `function by method` bodies delegate to a proof-defined `_spec`. */ +export const SPEC_FUNCTION_SUFFIX = "_spec"; /** Fresh binder for a comprehension wrapping the given subexpressions: `base` * verbatim unless one of them references it, then primed until free. A *local* @@ -973,10 +975,22 @@ function emitDecl(d: Decl): string { case "def-by-method": { const tp = d.typeParams.length > 0 ? `<${d.typeParams.join(", ")}>` : ""; - const lines = [`function ${escapeName(d.name)}${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`]; - for (const r of d.requires) lines.push(` requires ${emitExpr(r)}`); + const signature = `${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`; + const requires = d.requires.map(r => ` requires ${emitExpr(r)}`); + // The functional specification is the proof author's to write: a bodyless + // `_spec` stub, which the .dfy completes by adding a body after its + // signature. The generated file parses and resolves on its own (an empty + // function body would not), and the proof adds lines instead of editing + // between generated braces. + const spec = escapeGeneratedName(`${d.name}${SPEC_FUNCTION_SUFFIX}`); + const lines = [ + `// Specification of ${escapeName(d.name)}: add its body in the .dfy.`, + `function ${spec}${signature}`, ...requires, "", + `function ${escapeName(d.name)}${signature}`, ...requires, + ]; if (d.decreases) lines.push(` decreases ${emitExpr(d.decreases)}`); lines.push(`{`); + lines.push(` ${spec}(${d.params.map(p => escapeName(p.name)).join(", ")})`); lines.push(`}`); lines.push(`by method {`); lines.push(emitStmts(d.methodBody, 1)); From cdeb8ab8e3190eb5894c6efa1a55e39432322960 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Fri, 13 Nov 2026 01:08:17 -0500 Subject: [PATCH 2/4] do not include comments --- SPEC.md | 1 - examples/countBadPairs.dfy | 3 --- examples/countBadPairs.dfy.gen | 3 --- tools/src/dafny-emit.ts | 1 - 4 files changed, 8 deletions(-) diff --git a/SPEC.md b/SPEC.md index 9c7d586..d249bfa 100644 --- a/SPEC.md +++ b/SPEC.md @@ -993,7 +993,6 @@ function tagNameExists(m: Model, name: string, excludeTag?: TagId): boolean { If `transformPureBody` can auto-convert the body to a pure expression, the function emits as a normal Dafny `function`. If it cannot (e.g., the body has loops), it emits as `function by method`: ```dafny -// Specification of tagNameExists: add its body in the .dfy. function tagNameExists_spec(m: Model, name: string, excludeTag: Option): bool function tagNameExists(m: Model, name: string, excludeTag: Option): bool diff --git a/examples/countBadPairs.dfy b/examples/countBadPairs.dfy index 86bb5dc..b29871b 100644 --- a/examples/countBadPairs.dfy +++ b/examples/countBadPairs.dfy @@ -30,7 +30,6 @@ datatype Pair = Pair(i: nat, j: nat) // hand-written predicate, so the `by method` block verifies the imperative // impl returns that set. -// Specification of allPairsImpl: add its body in the .dfy. function allPairsImpl_spec(nums: seq): set { AllPairs(nums) @@ -67,7 +66,6 @@ by method { return result; } -// Specification of goodPairsImpl: add its body in the .dfy. function goodPairsImpl_spec(nums: seq): set { GoodPairs(nums) @@ -106,7 +104,6 @@ by method { return result; } -// Specification of badPairsImpl: add its body in the .dfy. function badPairsImpl_spec(nums: seq): set { BadPairs(nums) diff --git a/examples/countBadPairs.dfy.gen b/examples/countBadPairs.dfy.gen index 8c046ec..2073caa 100644 --- a/examples/countBadPairs.dfy.gen +++ b/examples/countBadPairs.dfy.gen @@ -13,7 +13,6 @@ function JSFloorDiv(a: int, b: int): int datatype Pair = Pair(i: nat, j: nat) -// Specification of allPairsImpl: add its body in the .dfy. function allPairsImpl_spec(nums: seq): set function allPairsImpl(nums: seq): set @@ -47,7 +46,6 @@ by method { return result; } -// Specification of goodPairsImpl: add its body in the .dfy. function goodPairsImpl_spec(nums: seq): set function goodPairsImpl(nums: seq): set @@ -83,7 +81,6 @@ by method { return result; } -// Specification of badPairsImpl: add its body in the .dfy. function badPairsImpl_spec(nums: seq): set function badPairsImpl(nums: seq): set diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 04549f6..8a0498b 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -984,7 +984,6 @@ function emitDecl(d: Decl): string { // between generated braces. const spec = escapeGeneratedName(`${d.name}${SPEC_FUNCTION_SUFFIX}`); const lines = [ - `// Specification of ${escapeName(d.name)}: add its body in the .dfy.`, `function ${spec}${signature}`, ...requires, "", `function ${escapeName(d.name)}${signature}`, ...requires, ]; From 1b00c4b3efa4a3f7300ff1ed4d01fd05a6875915 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Fri, 13 Nov 2026 01:20:51 -0500 Subject: [PATCH 3/4] rename to fun_spec suffix --- SPEC.md | 10 +++++----- examples/countBadPairs.dfy | 12 ++++++------ examples/countBadPairs.dfy.gen | 12 ++++++------ tools/src/dafny-emit.ts | 6 +++--- 4 files changed, 20 insertions(+), 20 deletions(-) diff --git a/SPEC.md b/SPEC.md index d249bfa..3834412 100644 --- a/SPEC.md +++ b/SPEC.md @@ -993,11 +993,11 @@ function tagNameExists(m: Model, name: string, excludeTag?: TagId): boolean { If `transformPureBody` can auto-convert the body to a pure expression, the function emits as a normal Dafny `function`. If it cannot (e.g., the body has loops), it emits as `function by method`: ```dafny -function tagNameExists_spec(m: Model, name: string, excludeTag: Option): bool +function tagNameExists_fun_spec(m: Model, name: string, excludeTag: Option): bool function tagNameExists(m: Model, name: string, excludeTag: Option): bool { - tagNameExists_spec(m, name, excludeTag) + tagNameExists_fun_spec(m, name, excludeTag) } by method { var i_tid_keys := SetToSeq(m.tags.Keys); @@ -1005,10 +1005,10 @@ by method { } ``` -The functional body delegates to a bodyless `tagNameExists_spec` stub, so the generated file parses and resolves on its own. Give the stub a body in the `.dfy` by adding lines after its signature: +The functional body delegates to a bodyless `tagNameExists_fun_spec` stub, so the generated file parses and resolves on its own. Give the stub a body in the `.dfy` by adding lines after its signature: ```dafny -function tagNameExists_spec(m: Model, name: string, excludeTag: Option): bool +function tagNameExists_fun_spec(m: Model, name: string, excludeTag: Option): bool { exists tid :: tid in m.tags && (match excludeTag { case None => true case Some(v) => v != tid }) && @@ -1016,7 +1016,7 @@ function tagNameExists_spec(m: Model, name: string, excludeTag: Option): } ``` -Dafny then verifies that the `by method` block computes `tagNameExists_spec`; left bodyless, the stub is uninterpreted and that proof fails. `regen` three-way-merges the `by method` block when the TypeScript changes without touching the added body. +Dafny then verifies that the `by method` block computes `tagNameExists_fun_spec`; left bodyless, the stub is uninterpreted and that proof fails. `regen` three-way-merges the `by method` block when the TypeScript changes without touching the added body. **Effect on callers:** Since `//@ pure` functions are `function`s in Dafny, callers that only invoke pure functions become pure automatically. For example, a large `switch`-based `apply` function becomes a `function` if all the map-iterating helpers it calls are marked `//@ pure`. diff --git a/examples/countBadPairs.dfy b/examples/countBadPairs.dfy index b29871b..4ae5ca9 100644 --- a/examples/countBadPairs.dfy +++ b/examples/countBadPairs.dfy @@ -30,14 +30,14 @@ datatype Pair = Pair(i: nat, j: nat) // hand-written predicate, so the `by method` block verifies the imperative // impl returns that set. -function allPairsImpl_spec(nums: seq): set +function allPairsImpl_fun_spec(nums: seq): set { AllPairs(nums) } function allPairsImpl(nums: seq): set { - allPairsImpl_spec(nums) + allPairsImpl_fun_spec(nums) } by method { var result: set := {}; @@ -66,14 +66,14 @@ by method { return result; } -function goodPairsImpl_spec(nums: seq): set +function goodPairsImpl_fun_spec(nums: seq): set { GoodPairs(nums) } function goodPairsImpl(nums: seq): set { - goodPairsImpl_spec(nums) + goodPairsImpl_fun_spec(nums) } by method { var result: set := {}; @@ -104,14 +104,14 @@ by method { return result; } -function badPairsImpl_spec(nums: seq): set +function badPairsImpl_fun_spec(nums: seq): set { BadPairs(nums) } function badPairsImpl(nums: seq): set { - badPairsImpl_spec(nums) + badPairsImpl_fun_spec(nums) } by method { var result: set := {}; diff --git a/examples/countBadPairs.dfy.gen b/examples/countBadPairs.dfy.gen index 2073caa..1c66832 100644 --- a/examples/countBadPairs.dfy.gen +++ b/examples/countBadPairs.dfy.gen @@ -13,11 +13,11 @@ function JSFloorDiv(a: int, b: int): int datatype Pair = Pair(i: nat, j: nat) -function allPairsImpl_spec(nums: seq): set +function allPairsImpl_fun_spec(nums: seq): set function allPairsImpl(nums: seq): set { - allPairsImpl_spec(nums) + allPairsImpl_fun_spec(nums) } by method { var result: set := {}; @@ -46,11 +46,11 @@ by method { return result; } -function goodPairsImpl_spec(nums: seq): set +function goodPairsImpl_fun_spec(nums: seq): set function goodPairsImpl(nums: seq): set { - goodPairsImpl_spec(nums) + goodPairsImpl_fun_spec(nums) } by method { var result: set := {}; @@ -81,11 +81,11 @@ by method { return result; } -function badPairsImpl_spec(nums: seq): set +function badPairsImpl_fun_spec(nums: seq): set function badPairsImpl(nums: seq): set { - badPairsImpl_spec(nums) + badPairsImpl_fun_spec(nums) } by method { var result: set := {}; diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 8a0498b..58915a6 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -11,8 +11,8 @@ import { DEFAULT_OPTIONS, resolveOptions, type LscOptions } from "./config.js"; /** Appended to a function's name for the lemma that carries its `//@ ensures`. */ export const ENSURES_LEMMA_SUFFIX = "_ensures"; -/** `function by method` bodies delegate to a proof-defined `_spec`. */ -export const SPEC_FUNCTION_SUFFIX = "_spec"; +/** `function by method` bodies delegate to a proof-defined `_fun_spec`. */ +export const SPEC_FUNCTION_SUFFIX = "_fun_spec"; /** Fresh binder for a comprehension wrapping the given subexpressions: `base` * verbatim unless one of them references it, then primed until free. A *local* @@ -978,7 +978,7 @@ function emitDecl(d: Decl): string { const signature = `${tp}(${paramList(d.params)}): ${tyToDafny(d.returnType)}`; const requires = d.requires.map(r => ` requires ${emitExpr(r)}`); // The functional specification is the proof author's to write: a bodyless - // `_spec` stub, which the .dfy completes by adding a body after its + // `_fun_spec` stub, which the .dfy completes by adding a body after its // signature. The generated file parses and resolves on its own (an empty // function body would not), and the proof adds lines instead of editing // between generated braces. From e4b2b37beb05c81f86e0635e583bfb2a0c81fe05 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Fri, 13 Nov 2026 01:26:38 -0500 Subject: [PATCH 4/4] trigger CI after case study updates