From e03456cee84f238b42cacbf6930104f105fcd1b0 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Fri, 28 Aug 2026 16:40:26 -0700 Subject: [PATCH 01/15] fix: model JavaScript strings as UTF-16 in Dafny --- SPEC.md | 15 ++- SPEC_DAFNY.md | 11 ++- examples/arrayFind.dfy | 1 + examples/arrayFind.dfy.gen | 1 + examples/arrayIsArrayChain.dfy | 1 + examples/arrayIsArrayChain.dfy.gen | 1 + examples/assume.dfy | 1 + examples/assume.dfy.gen | 1 + examples/auction.dfy | 1 + examples/auction.dfy.gen | 1 + examples/autohavoc.dfy | 1 + examples/autohavoc.dfy.gen | 1 + examples/contentDispatch.dfy | 1 + examples/contentDispatch.dfy.gen | 1 + examples/declareTypeEnum.dfy | 1 + examples/declareTypeEnum.dfy.gen | 1 + examples/declareTypeShadow.dfy | 1 + examples/declareTypeShadow.dfy.gen | 1 + examples/discriminantTrailing.dfy | 1 + examples/discriminantTrailing.dfy.gen | 1 + examples/enumLiteralPositions.dfy | 1 + examples/enumLiteralPositions.dfy.gen | 1 + examples/havoc.dfy | 1 + examples/havoc.dfy.gen | 1 + examples/hof.dfy | 22 ++++- examples/hof.dfy.gen | 22 ++++- examples/inlineHandler.dfy | 1 + examples/inlineHandler.dfy.gen | 1 + examples/lambdaFlatten.dfy | 12 ++- examples/lambdaFlatten.dfy.gen | 12 ++- examples/leftPad.dfy | 1 + examples/leftPad.dfy.gen | 1 + examples/mapRecord.dfy | 1 + examples/mapRecord.dfy.gen | 1 + examples/nameClash.dfy | 1 + examples/nameClash.dfy.gen | 1 + examples/nullableArray.dfy | 12 ++- examples/nullableArray.dfy.gen | 12 ++- examples/opaqueUnion.dfy | 1 + examples/opaqueUnion.dfy.gen | 1 + examples/postTags.dfy | 1 + examples/postTags.dfy.gen | 1 + examples/pureGuard.dfy | 1 + examples/pureGuard.dfy.gen | 1 + examples/recordIndexByEnum.dfy | 1 + examples/recordIndexByEnum.dfy.gen | 1 + examples/sharedDestructorCollision.dfy | 1 + examples/sharedDestructorCollision.dfy.gen | 1 + examples/spec.dfy | 20 +++- examples/spec.dfy.gen | 20 +++- examples/switchEnumField.dfy | 1 + examples/switchEnumField.dfy.gen | 1 + examples/switchLambda.dfy | 1 + examples/switchLambda.dfy.gen | 1 + examples/templateConcat.dfy | 1 + examples/templateConcat.dfy.gen | 1 + examples/todo-domain.dfy | 16 ++- examples/todo-domain.dfy.gen | 16 ++- examples/toposort.dfy | 1 + examples/toposort.dfy.gen | 1 + examples/trim.dfy | 15 +-- examples/trim.dfy.gen | 15 +-- examples/truthiness.dfy | 1 + examples/truthiness.dfy.gen | 1 + examples/tuples.dfy | 1 + examples/tuples.dfy.gen | 1 + tools/fixtures/javascript-utf16-strings.ts | 37 +++++++ .../fixtures/string-with-standard-library.dfy | 4 + tools/src/dafny-commands.ts | 18 +++- tools/src/dafny-emit.ts | 99 +++++++++++++++---- tools/test-fixtures.sh | 13 +++ 71 files changed, 385 insertions(+), 58 deletions(-) create mode 100644 tools/fixtures/javascript-utf16-strings.ts create mode 100644 tools/fixtures/string-with-standard-library.dfy diff --git a/SPEC.md b/SPEC.md index 8da6d3f7..5baf759c 100644 --- a/SPEC.md +++ b/SPEC.md @@ -485,8 +485,8 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions: | `Math.max(...s)` / `Math.min(...s)` | — | `MaxOfSeq(s)` / `MinOfSeq(s)` (requires `\|s\| > 0`) | | `perm(a, b)` (spec-only) | — | `Perm(a, b)` (preamble: `predicate Perm(a, b) { multiset(a) == multiset(b) }`) | | `arr.map((x) => e)` | `arr.map (fun x => e)` | `seq(\|arr\|, i requires 0 <= i < \|arr\| => var x := arr[i]; e)` (§3.7) | -| `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `Std.Collections.Seq.Filter((x) => e, arr)` | -| `arr.every((x) => e)` | `arr.all (fun x => e)` | `Std.Collections.Seq.All(arr, (x) => e)` | +| `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `SeqFilter((x) => e, arr)` | +| `arr.every((x) => e)` | `arr.all (fun x => e)` | `SeqAll(arr, (x) => e)` | | `arr.some((x) => e)` | `arr.any (fun x => e)` | `exists x :: x in arr && e` | | `arr.includes(x)` | `arr.contains x` | `(x in arr)` | | `arr.indexOf(x)` | — | `SeqIndexOf(arr, x)` (preamble) | @@ -667,8 +667,8 @@ The transform uses two strategies for translating `receiver.method(args)`: | `[...arr, e]` | `arrayPush` | `Array.push arr e` | `(arr + [e])` | | `arr.with(i, v)` | `arraySet` | `arr.set! i v` | `arr[i := v]` | | `arr.map(f)` | `map` | `arr.map f` | seq comprehension (§3.7) | -| `arr.filter(f)` | `filter` | `arr.filter f` | `Std.Collections.Seq.Filter(f, arr)` | -| `arr.every(f)` | `every` | `arr.all f` | `Std.Collections.Seq.All(arr, f)` | +| `arr.filter(f)` | `filter` | `arr.filter f` | `SeqFilter(f, arr)` | +| `arr.every(f)` | `every` | `arr.all f` | `SeqAll(arr, f)` | | `arr.some(f)` | `some` | `arr.any f` | `exists x :: x in arr && ...` | | `arr.includes(x)` | `includes` | `arr.contains x` | `(x in arr)` | | `arr.indexOf(x)` | `indexOf` | — | `SeqIndexOf(arr, x)` | @@ -1020,6 +1020,13 @@ The spec body is purely additive — `regen` three-way-merges and preserves user | `A \| B` (union param) | field intersection type | field intersection type | | Anything else | Pass through | Pass through | +For the Dafny backend, `string` is verified in Dafny's UTF-16 code-unit +character mode (`--unicode-char:false`). This matches JavaScript's observable +`.length`, indexing, slicing, `charCodeAt`, and equality semantics, including +astral characters occupying two positions and unpaired surrogate code units. +Non-ASCII source literals are emitted as `\\uXXXX` code-unit escapes so the +generated UTF-8 file preserves the exact JavaScript value. + `lsc` reads parameter and variable types from ts-morph. Primitive types are mapped per the table. User-defined types (like `State`, `Event`) are passed through by name — the corresponding backend type is generated from the TS type declaration. **Tuples.** A tuple type lowers to a native backend tuple (`(A, B)` in Dafny, `A × B` in Lean) only when its element types differ; a *homogeneous* tuple (`[number, number]`) lowers to `seq`/`Array` instead, since a sequence is a superset of what a same-typed tuple offers (dynamic index, `.length`, `.map`). The same homogeneity rule applies to an unannotated array literal: `[1, "a"]` is a tuple, `[1, 2, 3]` a sequence; an explicit expected type wins. Tuple element access **requires a compile-time integer-literal index** — `t[0]`, `t[1]` — because a tuple has a distinct type per slot, so a runtime index has neither a single result type nor a backend projection (`t.0`/`t.1`). A non-literal index into a tuple is a `lsc` error. `const [a, b] = t` destructuring works (it desugars to per-slot access). See [`examples/tuples.ts`](examples/tuples.ts). diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index ce956a2a..4c4dec6d 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -88,6 +88,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at | Helper | When | Purpose | |--------|------|---------| | `SeqIndexOf` | `arr.indexOf(x)` | First-index search (`-1` if absent) | +| `SeqFilter` / `SeqAll` / `SeqFoldLeft` | `filter` / `every` / `reduce` | Local recursive collection helpers (no Dafny standard-library dependency) | | `SeqFindIndex` | `arr.findIndex(f)` | Predicate first-index search | | `SeqFind` | `arr.find(f)` | Predicate first-match search | | `SeqFindLast` | `arr.findLast(f)` | Predicate last-match search | @@ -118,6 +119,14 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the `--standard-libraries` flag is added. -The shared `--time-limit=` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=` is forwarded verbatim to `dafny verify`. +JavaScript strings are sequences of UTF-16 code units, so `lsc check` pins +Dafny to `--unicode-char:false`. Generated files that use source strings carry +the marker `LemmaScript string model: javascript-utf16-code-units`. Dafny 4.11's +precompiled standard library was built for Unicode-scalar chars and cannot be +loaded in this mode. LemmaScript therefore uses local helpers for generated +`filter`, `every`, and `reduce` operations, and fails closed with an actionable +error if a string-bearing proof addition still imports `Std.*`. A string-free +proof may continue to use the standard library. +The shared `--time-limit=` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=` is forwarded verbatim to `dafny verify`. diff --git a/examples/arrayFind.dfy b/examples/arrayFind.dfy index 8fa05f5a..c75aad73 100644 --- a/examples/arrayFind.dfy +++ b/examples/arrayFind.dfy @@ -1,4 +1,5 @@ // Generated by lsc from arrayFind.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/arrayFind.dfy.gen b/examples/arrayFind.dfy.gen index 8fa05f5a..c75aad73 100644 --- a/examples/arrayFind.dfy.gen +++ b/examples/arrayFind.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from arrayFind.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/arrayIsArrayChain.dfy b/examples/arrayIsArrayChain.dfy index ce958b93..54eaec6f 100644 --- a/examples/arrayIsArrayChain.dfy +++ b/examples/arrayIsArrayChain.dfy @@ -1,4 +1,5 @@ // Generated by lsc from arrayIsArrayChain.ts +// LemmaScript string model: javascript-utf16-code-units datatype Part = Part(type_: string) diff --git a/examples/arrayIsArrayChain.dfy.gen b/examples/arrayIsArrayChain.dfy.gen index ce958b93..54eaec6f 100644 --- a/examples/arrayIsArrayChain.dfy.gen +++ b/examples/arrayIsArrayChain.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from arrayIsArrayChain.ts +// LemmaScript string model: javascript-utf16-code-units datatype Part = Part(type_: string) diff --git a/examples/assume.dfy b/examples/assume.dfy index c1f00ffb..7530251d 100644 --- a/examples/assume.dfy +++ b/examples/assume.dfy @@ -1,4 +1,5 @@ // Generated by lsc from assume.ts +// LemmaScript string model: javascript-utf16-code-units method shortenString(text: string) returns (res: int) ensures (res >= 0) diff --git a/examples/assume.dfy.gen b/examples/assume.dfy.gen index c1f00ffb..7530251d 100644 --- a/examples/assume.dfy.gen +++ b/examples/assume.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from assume.ts +// LemmaScript string model: javascript-utf16-code-units method shortenString(text: string) returns (res: int) ensures (res >= 0) diff --git a/examples/auction.dfy b/examples/auction.dfy index 372bfff6..856ee40a 100644 --- a/examples/auction.dfy +++ b/examples/auction.dfy @@ -1,4 +1,5 @@ // Generated by lsc from auction.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/auction.dfy.gen b/examples/auction.dfy.gen index 372bfff6..856ee40a 100644 --- a/examples/auction.dfy.gen +++ b/examples/auction.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from auction.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/autohavoc.dfy b/examples/autohavoc.dfy index 59965685..e83217d8 100644 --- a/examples/autohavoc.dfy +++ b/examples/autohavoc.dfy @@ -1,4 +1,5 @@ // Generated by lsc from autohavoc.ts +// LemmaScript string model: javascript-utf16-code-units type Unknown(==, 0) diff --git a/examples/autohavoc.dfy.gen b/examples/autohavoc.dfy.gen index 59965685..e83217d8 100644 --- a/examples/autohavoc.dfy.gen +++ b/examples/autohavoc.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from autohavoc.ts +// LemmaScript string model: javascript-utf16-code-units type Unknown(==, 0) diff --git a/examples/contentDispatch.dfy b/examples/contentDispatch.dfy index e296c6f1..f519257e 100644 --- a/examples/contentDispatch.dfy +++ b/examples/contentDispatch.dfy @@ -1,4 +1,5 @@ // Generated by lsc from contentDispatch.ts +// LemmaScript string model: javascript-utf16-code-units datatype Part = Part(type_: string, toolCallId: string) diff --git a/examples/contentDispatch.dfy.gen b/examples/contentDispatch.dfy.gen index e296c6f1..f519257e 100644 --- a/examples/contentDispatch.dfy.gen +++ b/examples/contentDispatch.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from contentDispatch.ts +// LemmaScript string model: javascript-utf16-code-units datatype Part = Part(type_: string, toolCallId: string) diff --git a/examples/declareTypeEnum.dfy b/examples/declareTypeEnum.dfy index e540597c..0c814fe2 100644 --- a/examples/declareTypeEnum.dfy +++ b/examples/declareTypeEnum.dfy @@ -1,4 +1,5 @@ // Generated by lsc from declareTypeEnum.ts +// LemmaScript string model: javascript-utf16-code-units datatype Role = user | assistant | toolResult diff --git a/examples/declareTypeEnum.dfy.gen b/examples/declareTypeEnum.dfy.gen index e540597c..0c814fe2 100644 --- a/examples/declareTypeEnum.dfy.gen +++ b/examples/declareTypeEnum.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from declareTypeEnum.ts +// LemmaScript string model: javascript-utf16-code-units datatype Role = user | assistant | toolResult diff --git a/examples/declareTypeShadow.dfy b/examples/declareTypeShadow.dfy index 95c2d4cb..c7d7e050 100644 --- a/examples/declareTypeShadow.dfy +++ b/examples/declareTypeShadow.dfy @@ -1,4 +1,5 @@ // Generated by lsc from declareTypeShadow.ts +// LemmaScript string model: javascript-utf16-code-units datatype RawMsg = RawMsg(kind: string) diff --git a/examples/declareTypeShadow.dfy.gen b/examples/declareTypeShadow.dfy.gen index 95c2d4cb..c7d7e050 100644 --- a/examples/declareTypeShadow.dfy.gen +++ b/examples/declareTypeShadow.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from declareTypeShadow.ts +// LemmaScript string model: javascript-utf16-code-units datatype RawMsg = RawMsg(kind: string) diff --git a/examples/discriminantTrailing.dfy b/examples/discriminantTrailing.dfy index f42991d1..92679138 100644 --- a/examples/discriminantTrailing.dfy +++ b/examples/discriminantTrailing.dfy @@ -1,4 +1,5 @@ // Generated by lsc from discriminantTrailing.ts +// LemmaScript string model: javascript-utf16-code-units datatype Shape = circle | square | triangle diff --git a/examples/discriminantTrailing.dfy.gen b/examples/discriminantTrailing.dfy.gen index f42991d1..92679138 100644 --- a/examples/discriminantTrailing.dfy.gen +++ b/examples/discriminantTrailing.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from discriminantTrailing.ts +// LemmaScript string model: javascript-utf16-code-units datatype Shape = circle | square | triangle diff --git a/examples/enumLiteralPositions.dfy b/examples/enumLiteralPositions.dfy index 3de24754..dcd9c5b1 100644 --- a/examples/enumLiteralPositions.dfy +++ b/examples/enumLiteralPositions.dfy @@ -1,4 +1,5 @@ // Generated by lsc from enumLiteralPositions.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/enumLiteralPositions.dfy.gen b/examples/enumLiteralPositions.dfy.gen index 3de24754..dcd9c5b1 100644 --- a/examples/enumLiteralPositions.dfy.gen +++ b/examples/enumLiteralPositions.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from enumLiteralPositions.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/havoc.dfy b/examples/havoc.dfy index 713bcd6c..a03527d7 100644 --- a/examples/havoc.dfy +++ b/examples/havoc.dfy @@ -1,4 +1,5 @@ // Generated by lsc from havoc.ts +// LemmaScript string model: javascript-utf16-code-units method countMatches(items: seq, validKeys: set) returns (res: int) ensures (res >= 0) diff --git a/examples/havoc.dfy.gen b/examples/havoc.dfy.gen index 713bcd6c..a03527d7 100644 --- a/examples/havoc.dfy.gen +++ b/examples/havoc.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from havoc.ts +// LemmaScript string model: javascript-utf16-code-units method countMatches(items: seq, validKeys: set) returns (res: int) ensures (res >= 0) diff --git a/examples/hof.dfy b/examples/hof.dfy index 95b44efe..a0b64bfc 100644 --- a/examples/hof.dfy +++ b/examples/hof.dfy @@ -1,7 +1,23 @@ // Generated by lsc from hof.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + datatype QuoteElement = QuoteElement(QuoteId: string, ConditionallyHidden: Option) datatype QuoteElements = QuoteElements(Elements: seq) @@ -18,12 +34,12 @@ lemma doubleAll_ensures(arr: seq) function positives(arr: seq): seq { - Std.Collections.Seq.Filter((x: int) => (x > 0), arr) + SeqFilter((x: int) => (x > 0), arr) } function allPositive(arr: seq): bool { - Std.Collections.Seq.All(arr, (x: int) => (x > 0)) + SeqAll(arr, (x: int) => (x > 0)) } function hasNegative(arr: seq): bool @@ -33,7 +49,7 @@ function hasNegative(arr: seq): bool function visibleElementsForQuote(comparisonElements: QuoteElements, quoteId: string): seq { - Std.Collections.Seq.Filter((i_lambdaParam0: QuoteElement) => (var QuoteId := i_lambdaParam0.QuoteId; (var ConditionallyHidden := i_lambdaParam0.ConditionallyHidden; ((QuoteId == quoteId) && (match ConditionallyHidden { case Some(i_value) => !(i_value) case None => true })))), comparisonElements.Elements) + SeqFilter((i_lambdaParam0: QuoteElement) => (var QuoteId := i_lambdaParam0.QuoteId; (var ConditionallyHidden := i_lambdaParam0.ConditionallyHidden; ((QuoteId == quoteId) && (match ConditionallyHidden { case Some(i_value) => !(i_value) case None => true })))), comparisonElements.Elements) } lemma visibleElementsForQuote_ensures(comparisonElements: QuoteElements, quoteId: string) diff --git a/examples/hof.dfy.gen b/examples/hof.dfy.gen index 95b44efe..a0b64bfc 100644 --- a/examples/hof.dfy.gen +++ b/examples/hof.dfy.gen @@ -1,7 +1,23 @@ // Generated by lsc from hof.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + datatype QuoteElement = QuoteElement(QuoteId: string, ConditionallyHidden: Option) datatype QuoteElements = QuoteElements(Elements: seq) @@ -18,12 +34,12 @@ lemma doubleAll_ensures(arr: seq) function positives(arr: seq): seq { - Std.Collections.Seq.Filter((x: int) => (x > 0), arr) + SeqFilter((x: int) => (x > 0), arr) } function allPositive(arr: seq): bool { - Std.Collections.Seq.All(arr, (x: int) => (x > 0)) + SeqAll(arr, (x: int) => (x > 0)) } function hasNegative(arr: seq): bool @@ -33,7 +49,7 @@ function hasNegative(arr: seq): bool function visibleElementsForQuote(comparisonElements: QuoteElements, quoteId: string): seq { - Std.Collections.Seq.Filter((i_lambdaParam0: QuoteElement) => (var QuoteId := i_lambdaParam0.QuoteId; (var ConditionallyHidden := i_lambdaParam0.ConditionallyHidden; ((QuoteId == quoteId) && (match ConditionallyHidden { case Some(i_value) => !(i_value) case None => true })))), comparisonElements.Elements) + SeqFilter((i_lambdaParam0: QuoteElement) => (var QuoteId := i_lambdaParam0.QuoteId; (var ConditionallyHidden := i_lambdaParam0.ConditionallyHidden; ((QuoteId == quoteId) && (match ConditionallyHidden { case Some(i_value) => !(i_value) case None => true })))), comparisonElements.Elements) } lemma visibleElementsForQuote_ensures(comparisonElements: QuoteElements, quoteId: string) diff --git a/examples/inlineHandler.dfy b/examples/inlineHandler.dfy index 639fff73..bd0136b5 100644 --- a/examples/inlineHandler.dfy +++ b/examples/inlineHandler.dfy @@ -1,4 +1,5 @@ // Generated by lsc from inlineHandler.ts +// LemmaScript string model: javascript-utf16-code-units type Unknown(==, 0) diff --git a/examples/inlineHandler.dfy.gen b/examples/inlineHandler.dfy.gen index 639fff73..bd0136b5 100644 --- a/examples/inlineHandler.dfy.gen +++ b/examples/inlineHandler.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from inlineHandler.ts +// LemmaScript string model: javascript-utf16-code-units type Unknown(==, 0) diff --git a/examples/lambdaFlatten.dfy b/examples/lambdaFlatten.dfy index 6e62dabb..18e31490 100644 --- a/examples/lambdaFlatten.dfy +++ b/examples/lambdaFlatten.dfy @@ -1,12 +1,22 @@ // Generated by lsc from lambdaFlatten.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + datatype Part = Part(type_: string, providerExecuted: Option, toolCallId: string) function keepParts(parts: seq, valid: set): seq { - Std.Collections.Seq.Filter((p: Part) => ((p.type_ != "tool-call") || (var tc := p; ((match tc.providerExecuted { case Some(i_value) => (i_value == true) case None => false }) || (tc.toolCallId in valid)))), parts) + SeqFilter((p: Part) => ((p.type_ != "tool-call") || (var tc := p; ((match tc.providerExecuted { case Some(i_value) => (i_value == true) case None => false }) || (tc.toolCallId in valid)))), parts) } lemma keepParts_ensures(parts: seq, valid: set) diff --git a/examples/lambdaFlatten.dfy.gen b/examples/lambdaFlatten.dfy.gen index 6e62dabb..18e31490 100644 --- a/examples/lambdaFlatten.dfy.gen +++ b/examples/lambdaFlatten.dfy.gen @@ -1,12 +1,22 @@ // Generated by lsc from lambdaFlatten.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + datatype Part = Part(type_: string, providerExecuted: Option, toolCallId: string) function keepParts(parts: seq, valid: set): seq { - Std.Collections.Seq.Filter((p: Part) => ((p.type_ != "tool-call") || (var tc := p; ((match tc.providerExecuted { case Some(i_value) => (i_value == true) case None => false }) || (tc.toolCallId in valid)))), parts) + SeqFilter((p: Part) => ((p.type_ != "tool-call") || (var tc := p; ((match tc.providerExecuted { case Some(i_value) => (i_value == true) case None => false }) || (tc.toolCallId in valid)))), parts) } lemma keepParts_ensures(parts: seq, valid: set) diff --git a/examples/leftPad.dfy b/examples/leftPad.dfy index 1f522f5c..3205811d 100644 --- a/examples/leftPad.dfy +++ b/examples/leftPad.dfy @@ -1,4 +1,5 @@ // Generated by lsc from leftPad.ts +// LemmaScript string model: javascript-utf16-code-units method leftPad(str: string, len: nat, ch: string) returns (res: string) requires (|ch| == 1) diff --git a/examples/leftPad.dfy.gen b/examples/leftPad.dfy.gen index 1f522f5c..3205811d 100644 --- a/examples/leftPad.dfy.gen +++ b/examples/leftPad.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from leftPad.ts +// LemmaScript string model: javascript-utf16-code-units method leftPad(str: string, len: nat, ch: string) returns (res: string) requires (|ch| == 1) diff --git a/examples/mapRecord.dfy b/examples/mapRecord.dfy index 342035a6..d6826b4d 100644 --- a/examples/mapRecord.dfy +++ b/examples/mapRecord.dfy @@ -1,4 +1,5 @@ // Generated by lsc from mapRecord.ts +// LemmaScript string model: javascript-utf16-code-units datatype In = In(tag: string, n: int) diff --git a/examples/mapRecord.dfy.gen b/examples/mapRecord.dfy.gen index 342035a6..d6826b4d 100644 --- a/examples/mapRecord.dfy.gen +++ b/examples/mapRecord.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from mapRecord.ts +// LemmaScript string model: javascript-utf16-code-units datatype In = In(tag: string, n: int) diff --git a/examples/nameClash.dfy b/examples/nameClash.dfy index 270b7393..be0d1275 100644 --- a/examples/nameClash.dfy +++ b/examples/nameClash.dfy @@ -1,4 +1,5 @@ // Generated by lsc from nameClash.ts +// LemmaScript string model: javascript-utf16-code-units function JSRem(a: int, b: int): int requires b != 0 diff --git a/examples/nameClash.dfy.gen b/examples/nameClash.dfy.gen index 270b7393..be0d1275 100644 --- a/examples/nameClash.dfy.gen +++ b/examples/nameClash.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from nameClash.ts +// LemmaScript string model: javascript-utf16-code-units function JSRem(a: int, b: int): int requires b != 0 diff --git a/examples/nullableArray.dfy b/examples/nullableArray.dfy index 004b62f4..5c739048 100644 --- a/examples/nullableArray.dfy +++ b/examples/nullableArray.dfy @@ -1,7 +1,17 @@ // Generated by lsc from nullableArray.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + datatype Part = Part(type_: string, toolCallId: string) datatype ArrayOf_Part_Or_string = ArrayBranch(arr: seq) | NonArrayBranch(val: string) @@ -25,7 +35,7 @@ method dropOrphans(messages: seq) returns (res: seq) var cur := filteredContents[i]; match cur { case Some(i_cur_val) => - filteredContents := filteredContents[i := Some(Std.Collections.Seq.Filter(keep, i_cur_val))]; + filteredContents := filteredContents[i := Some(SeqFilter(keep, i_cur_val))]; case None => } diff --git a/examples/nullableArray.dfy.gen b/examples/nullableArray.dfy.gen index 004b62f4..5c739048 100644 --- a/examples/nullableArray.dfy.gen +++ b/examples/nullableArray.dfy.gen @@ -1,7 +1,17 @@ // Generated by lsc from nullableArray.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + datatype Part = Part(type_: string, toolCallId: string) datatype ArrayOf_Part_Or_string = ArrayBranch(arr: seq) | NonArrayBranch(val: string) @@ -25,7 +35,7 @@ method dropOrphans(messages: seq) returns (res: seq) var cur := filteredContents[i]; match cur { case Some(i_cur_val) => - filteredContents := filteredContents[i := Some(Std.Collections.Seq.Filter(keep, i_cur_val))]; + filteredContents := filteredContents[i := Some(SeqFilter(keep, i_cur_val))]; case None => } diff --git a/examples/opaqueUnion.dfy b/examples/opaqueUnion.dfy index dd6e0c11..533c83e9 100644 --- a/examples/opaqueUnion.dfy +++ b/examples/opaqueUnion.dfy @@ -1,4 +1,5 @@ // Generated by lsc from opaqueUnion.ts +// LemmaScript string model: javascript-utf16-code-units type Opaque_TextContent_or_ImageContent(==) diff --git a/examples/opaqueUnion.dfy.gen b/examples/opaqueUnion.dfy.gen index dd6e0c11..533c83e9 100644 --- a/examples/opaqueUnion.dfy.gen +++ b/examples/opaqueUnion.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from opaqueUnion.ts +// LemmaScript string model: javascript-utf16-code-units type Opaque_TextContent_or_ImageContent(==) diff --git a/examples/postTags.dfy b/examples/postTags.dfy index bf6f6e50..40c44ddd 100644 --- a/examples/postTags.dfy +++ b/examples/postTags.dfy @@ -1,4 +1,5 @@ // Generated by lsc from postTags.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/postTags.dfy.gen b/examples/postTags.dfy.gen index bf6f6e50..40c44ddd 100644 --- a/examples/postTags.dfy.gen +++ b/examples/postTags.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from postTags.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/pureGuard.dfy b/examples/pureGuard.dfy index 6f67f789..1c9ca333 100644 --- a/examples/pureGuard.dfy +++ b/examples/pureGuard.dfy @@ -1,4 +1,5 @@ // Generated by lsc from pureGuard.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/pureGuard.dfy.gen b/examples/pureGuard.dfy.gen index 6f67f789..1c9ca333 100644 --- a/examples/pureGuard.dfy.gen +++ b/examples/pureGuard.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from pureGuard.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/recordIndexByEnum.dfy b/examples/recordIndexByEnum.dfy index be57dda4..4c9848a0 100644 --- a/examples/recordIndexByEnum.dfy +++ b/examples/recordIndexByEnum.dfy @@ -1,4 +1,5 @@ // Generated by lsc from recordIndexByEnum.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/recordIndexByEnum.dfy.gen b/examples/recordIndexByEnum.dfy.gen index be57dda4..4c9848a0 100644 --- a/examples/recordIndexByEnum.dfy.gen +++ b/examples/recordIndexByEnum.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from recordIndexByEnum.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/sharedDestructorCollision.dfy b/examples/sharedDestructorCollision.dfy index d8840e4d..42e6a45e 100644 --- a/examples/sharedDestructorCollision.dfy +++ b/examples/sharedDestructorCollision.dfy @@ -1,4 +1,5 @@ // Generated by lsc from sharedDestructorCollision.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/sharedDestructorCollision.dfy.gen b/examples/sharedDestructorCollision.dfy.gen index d8840e4d..42e6a45e 100644 --- a/examples/sharedDestructorCollision.dfy.gen +++ b/examples/sharedDestructorCollision.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from sharedDestructorCollision.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/spec.dfy b/examples/spec.dfy index 52ee530c..a7f3901f 100644 --- a/examples/spec.dfy +++ b/examples/spec.dfy @@ -1,4 +1,5 @@ // Generated by lsc from spec.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) @@ -13,6 +14,21 @@ function JSFloorDiv(a: int, b: int): int else -((a - 1) / (-b)) - 1 } +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + function StringIndexOf(s: string, sub: string): int ensures StringIndexOf(s, sub) == -1 || (0 <= StringIndexOf(s, sub) <= |s| - |sub| && s[StringIndexOf(s, sub)..StringIndexOf(s, sub) + |sub|] == sub) @@ -236,12 +252,12 @@ lemma doubleAll_ensures(arr: seq) function keepPositive(arr: seq): seq { - Std.Collections.Seq.Filter((x: int) => (x > 0), arr) + SeqFilter((x: int) => (x > 0), arr) } function allBelow(arr: seq, cap: int): bool { - Std.Collections.Seq.All(arr, (x: int) => (x < cap)) + SeqAll(arr, (x: int) => (x < cap)) } function anyNegative(arr: seq): bool diff --git a/examples/spec.dfy.gen b/examples/spec.dfy.gen index 52ee530c..a7f3901f 100644 --- a/examples/spec.dfy.gen +++ b/examples/spec.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from spec.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) @@ -13,6 +14,21 @@ function JSFloorDiv(a: int, b: int): int else -((a - 1) / (-b)) - 1 } +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + function StringIndexOf(s: string, sub: string): int ensures StringIndexOf(s, sub) == -1 || (0 <= StringIndexOf(s, sub) <= |s| - |sub| && s[StringIndexOf(s, sub)..StringIndexOf(s, sub) + |sub|] == sub) @@ -236,12 +252,12 @@ lemma doubleAll_ensures(arr: seq) function keepPositive(arr: seq): seq { - Std.Collections.Seq.Filter((x: int) => (x > 0), arr) + SeqFilter((x: int) => (x > 0), arr) } function allBelow(arr: seq, cap: int): bool { - Std.Collections.Seq.All(arr, (x: int) => (x < cap)) + SeqAll(arr, (x: int) => (x < cap)) } function anyNegative(arr: seq): bool diff --git a/examples/switchEnumField.dfy b/examples/switchEnumField.dfy index 71aa6d42..edef011e 100644 --- a/examples/switchEnumField.dfy +++ b/examples/switchEnumField.dfy @@ -1,4 +1,5 @@ // Generated by lsc from switchEnumField.ts +// LemmaScript string model: javascript-utf16-code-units datatype Tag = read | write | exec diff --git a/examples/switchEnumField.dfy.gen b/examples/switchEnumField.dfy.gen index 71aa6d42..edef011e 100644 --- a/examples/switchEnumField.dfy.gen +++ b/examples/switchEnumField.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from switchEnumField.ts +// LemmaScript string model: javascript-utf16-code-units datatype Tag = read | write | exec diff --git a/examples/switchLambda.dfy b/examples/switchLambda.dfy index 83d1c74a..228c6341 100644 --- a/examples/switchLambda.dfy +++ b/examples/switchLambda.dfy @@ -1,4 +1,5 @@ // Generated by lsc from switchLambda.ts +// LemmaScript string model: javascript-utf16-code-units datatype Msg = user(text: string) | system(code: int) diff --git a/examples/switchLambda.dfy.gen b/examples/switchLambda.dfy.gen index 83d1c74a..228c6341 100644 --- a/examples/switchLambda.dfy.gen +++ b/examples/switchLambda.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from switchLambda.ts +// LemmaScript string model: javascript-utf16-code-units datatype Msg = user(text: string) | system(code: int) diff --git a/examples/templateConcat.dfy b/examples/templateConcat.dfy index 8f5715ae..30685e06 100644 --- a/examples/templateConcat.dfy +++ b/examples/templateConcat.dfy @@ -1,4 +1,5 @@ // Generated by lsc from templateConcat.ts +// LemmaScript string model: javascript-utf16-code-units function NatToString(n: nat): string decreases n diff --git a/examples/templateConcat.dfy.gen b/examples/templateConcat.dfy.gen index 8f5715ae..30685e06 100644 --- a/examples/templateConcat.dfy.gen +++ b/examples/templateConcat.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from templateConcat.ts +// LemmaScript string model: javascript-utf16-code-units function NatToString(n: nat): string decreases n diff --git a/examples/todo-domain.dfy b/examples/todo-domain.dfy index 02d43c4a..ee0a0321 100644 --- a/examples/todo-domain.dfy +++ b/examples/todo-domain.dfy @@ -1,4 +1,5 @@ // Generated by lsc from todo-domain.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) @@ -31,6 +32,15 @@ function JSRem(a: int, b: int): int if a < 0 then -r else r } +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + function StringToLower(s: string): string ensures |StringToLower(s)| == |s| decreases |s| @@ -537,7 +547,7 @@ method removeTaskFromAllLists(tasks: map>, taskId: TaskId) r { var lid := i_lid_keys[i_lid_idx]; var lane := tasks[lid]; - result := result[lid := Std.Collections.Seq.Filter((id: TaskId) => (id != taskId), lane)]; + result := result[lid := SeqFilter((id: TaskId) => (id != taskId), lane)]; i_lid_idx := i_lid_idx + 1; } return result; @@ -630,7 +640,7 @@ method apply(m: Model, a: Action) returns (res: Result) newTaskData := (map k | k in newTaskData && k != tid :: newTaskData[k]); i_tid_idx := i_tid_idx + 1; } - var newLists := Std.Collections.Seq.Filter((l: int) => (l != a.listId), m.lists); + var newLists := SeqFilter((l: int) => (l != a.listId), m.lists); var newListNames := m.listNames; newListNames := (map k | k in newListNames && k != i_a_listId :: newListNames[k]); var newTasks := m.tasks; @@ -649,7 +659,7 @@ method apply(m: Model, a: Action) returns (res: Result) var i_t23 := err(Err.BadAnchor); return i_t23; } - var without := Std.Collections.Seq.Filter((l: int) => (l != a.listId), m.lists); + var without := SeqFilter((l: int) => (l != a.listId), m.lists); var clamped := MathMin(pos, |without|); var i_t24 := insertAt(without, clamped, i_a_listId); var newLists := i_t24; diff --git a/examples/todo-domain.dfy.gen b/examples/todo-domain.dfy.gen index 02d43c4a..ee0a0321 100644 --- a/examples/todo-domain.dfy.gen +++ b/examples/todo-domain.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from todo-domain.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) @@ -31,6 +32,15 @@ function JSRem(a: int, b: int): int if a < 0 then -r else r } +function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +} + function StringToLower(s: string): string ensures |StringToLower(s)| == |s| decreases |s| @@ -537,7 +547,7 @@ method removeTaskFromAllLists(tasks: map>, taskId: TaskId) r { var lid := i_lid_keys[i_lid_idx]; var lane := tasks[lid]; - result := result[lid := Std.Collections.Seq.Filter((id: TaskId) => (id != taskId), lane)]; + result := result[lid := SeqFilter((id: TaskId) => (id != taskId), lane)]; i_lid_idx := i_lid_idx + 1; } return result; @@ -630,7 +640,7 @@ method apply(m: Model, a: Action) returns (res: Result) newTaskData := (map k | k in newTaskData && k != tid :: newTaskData[k]); i_tid_idx := i_tid_idx + 1; } - var newLists := Std.Collections.Seq.Filter((l: int) => (l != a.listId), m.lists); + var newLists := SeqFilter((l: int) => (l != a.listId), m.lists); var newListNames := m.listNames; newListNames := (map k | k in newListNames && k != i_a_listId :: newListNames[k]); var newTasks := m.tasks; @@ -649,7 +659,7 @@ method apply(m: Model, a: Action) returns (res: Result) var i_t23 := err(Err.BadAnchor); return i_t23; } - var without := Std.Collections.Seq.Filter((l: int) => (l != a.listId), m.lists); + var without := SeqFilter((l: int) => (l != a.listId), m.lists); var clamped := MathMin(pos, |without|); var i_t24 := insertAt(without, clamped, i_a_listId); var newLists := i_t24; diff --git a/examples/toposort.dfy b/examples/toposort.dfy index 5fb35c9c..9e475297 100644 --- a/examples/toposort.dfy +++ b/examples/toposort.dfy @@ -1,4 +1,5 @@ // Generated by lsc from toposort.ts +// LemmaScript string model: javascript-utf16-code-units method SetToSeq(s: set) returns (res: seq) ensures forall x :: x in s <==> x in res diff --git a/examples/toposort.dfy.gen b/examples/toposort.dfy.gen index 8c841825..38eed715 100644 --- a/examples/toposort.dfy.gen +++ b/examples/toposort.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from toposort.ts +// LemmaScript string model: javascript-utf16-code-units method SetToSeq(s: set) returns (res: seq) ensures forall x :: x in s <==> x in res diff --git a/examples/trim.dfy b/examples/trim.dfy index d732952a..69f2af29 100644 --- a/examples/trim.dfy +++ b/examples/trim.dfy @@ -1,12 +1,13 @@ // Generated by lsc from trim.ts +// LemmaScript string model: javascript-utf16-code-units predicate IsJSWhitespace(c: char) { - c == '\U{0009}' || c == '\U{000A}' || c == '\U{000B}' || c == '\U{000C}' || c == '\U{000D}' || - c == '\U{0020}' || c == '\U{00A0}' || c == '\U{1680}' || - ('\U{2000}' <= c <= '\U{200A}') || - c == '\U{2028}' || c == '\U{2029}' || c == '\U{202F}' || c == '\U{205F}' || - c == '\U{3000}' || c == '\U{FEFF}' + c == '\u0009' || c == '\u000A' || c == '\u000B' || c == '\u000C' || c == '\u000D' || + c == '\u0020' || c == '\u00A0' || c == '\u1680' || + ('\u2000' <= c <= '\u200A') || + c == '\u2028' || c == '\u2029' || c == '\u202F' || c == '\u205F' || + c == '\u3000' || c == '\uFEFF' } function StringTrimLeft(s: string): string @@ -35,7 +36,7 @@ function StringTrim(s: string): string } function StringFromCharCode(n: int): string - requires 0 <= n < 0xD800 || 0xE000 <= n < 0x110000 + requires 0 <= n < 0x10000 ensures |StringFromCharCode(n)| == 1 ensures (StringFromCharCode(n)[0] as int) == n { @@ -54,7 +55,7 @@ lemma trimmed_ensures(s: string) function trimAsciiWs(): string { - StringTrim(" x\n") + StringTrim("\u0009x\u000A") } lemma trimAsciiWs_ensures() diff --git a/examples/trim.dfy.gen b/examples/trim.dfy.gen index d732952a..69f2af29 100644 --- a/examples/trim.dfy.gen +++ b/examples/trim.dfy.gen @@ -1,12 +1,13 @@ // Generated by lsc from trim.ts +// LemmaScript string model: javascript-utf16-code-units predicate IsJSWhitespace(c: char) { - c == '\U{0009}' || c == '\U{000A}' || c == '\U{000B}' || c == '\U{000C}' || c == '\U{000D}' || - c == '\U{0020}' || c == '\U{00A0}' || c == '\U{1680}' || - ('\U{2000}' <= c <= '\U{200A}') || - c == '\U{2028}' || c == '\U{2029}' || c == '\U{202F}' || c == '\U{205F}' || - c == '\U{3000}' || c == '\U{FEFF}' + c == '\u0009' || c == '\u000A' || c == '\u000B' || c == '\u000C' || c == '\u000D' || + c == '\u0020' || c == '\u00A0' || c == '\u1680' || + ('\u2000' <= c <= '\u200A') || + c == '\u2028' || c == '\u2029' || c == '\u202F' || c == '\u205F' || + c == '\u3000' || c == '\uFEFF' } function StringTrimLeft(s: string): string @@ -35,7 +36,7 @@ function StringTrim(s: string): string } function StringFromCharCode(n: int): string - requires 0 <= n < 0xD800 || 0xE000 <= n < 0x110000 + requires 0 <= n < 0x10000 ensures |StringFromCharCode(n)| == 1 ensures (StringFromCharCode(n)[0] as int) == n { @@ -54,7 +55,7 @@ lemma trimmed_ensures(s: string) function trimAsciiWs(): string { - StringTrim(" x\n") + StringTrim("\u0009x\u000A") } lemma trimAsciiWs_ensures() diff --git a/examples/truthiness.dfy b/examples/truthiness.dfy index 597b6daf..a6d8af9c 100644 --- a/examples/truthiness.dfy +++ b/examples/truthiness.dfy @@ -1,4 +1,5 @@ // Generated by lsc from truthiness.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/truthiness.dfy.gen b/examples/truthiness.dfy.gen index 597b6daf..a6d8af9c 100644 --- a/examples/truthiness.dfy.gen +++ b/examples/truthiness.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from truthiness.ts +// LemmaScript string model: javascript-utf16-code-units datatype Option = None | Some(value: T) diff --git a/examples/tuples.dfy b/examples/tuples.dfy index 80f0a331..303e6288 100644 --- a/examples/tuples.dfy +++ b/examples/tuples.dfy @@ -1,4 +1,5 @@ // Generated by lsc from tuples.ts +// LemmaScript string model: javascript-utf16-code-units function swap(p: (int, string)): (string, int) { diff --git a/examples/tuples.dfy.gen b/examples/tuples.dfy.gen index 80f0a331..303e6288 100644 --- a/examples/tuples.dfy.gen +++ b/examples/tuples.dfy.gen @@ -1,4 +1,5 @@ // Generated by lsc from tuples.ts +// LemmaScript string model: javascript-utf16-code-units function swap(p: (int, string)): (string, int) { diff --git a/tools/fixtures/javascript-utf16-strings.ts b/tools/fixtures/javascript-utf16-strings.ts new file mode 100644 index 00000000..efdc6efe --- /dev/null +++ b/tools/fixtures/javascript-utf16-strings.ts @@ -0,0 +1,37 @@ +//@ backend dafny + +export function emojiLength(): number { + //@ verify + //@ ensures \result === 2 + return "😀".length; +} + +export function emojiHighSurrogate(): number { + //@ verify + //@ ensures \result === 0xD83D + return "😀".charCodeAt(0); +} + +export function emojiLowSurrogate(): number { + //@ verify + //@ ensures \result === 0xDE00 + return "😀".charCodeAt(1); +} + +export function unpairedSurrogateLength(): number { + //@ verify + //@ ensures \result === 1 + return "\uD83D".length; +} + +export function slicedHighSurrogate(): number { + //@ verify + //@ ensures \result === 0xD83D + return "😀".slice(0, 1).charCodeAt(0); +} + +export function constructedSurrogate(): number { + //@ verify + //@ ensures \result === 0xD83D + return String.fromCharCode(0xD83D).charCodeAt(0); +} diff --git a/tools/fixtures/string-with-standard-library.dfy b/tools/fixtures/string-with-standard-library.dfy new file mode 100644 index 00000000..e5f87264 --- /dev/null +++ b/tools/fixtures/string-with-standard-library.dfy @@ -0,0 +1,4 @@ +// LemmaScript string model: javascript-utf16-code-units +import opened Std.Arithmetic.Mul + +lemma StringAndStandardLibraryAreIncompatible() {} diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index c670f624..9e07ad50 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -47,12 +47,28 @@ export function dafnyVerify(dfyPath: string, dir: string, timeLimit?: number, ex console.log("Running dafny verify..."); try { const content = readFileSync(dfyPath, "utf-8"); + const usesJavaScriptStrings = content.includes("// LemmaScript string model: javascript-utf16-code-units"); + const usesStandardLibrary = content.includes("Std."); + if (usesJavaScriptStrings && usesStandardLibrary) { + console.error( + "ERROR: this proof combines JavaScript strings with Dafny's standard library. " + + "Dafny 4.11 cannot load its Unicode-scalar standard library while LemmaScript " + + "uses UTF-16 code units. Remove the Std.* dependency or move it to a string-free module." + ); + return false; + } const args: string[] = ["verify"]; - if (content.includes("Std.")) args.push("--standard-libraries"); + if (usesStandardLibrary) args.push("--standard-libraries"); if (timeLimit) args.push("--verification-time-limit", String(timeLimit)); if (extraFlags) { for (const tok of extraFlags.split(/\s+/)) if (tok) args.push(tok); } + // JavaScript strings are UTF-16 code-unit sequences. Dafny 4 defaults to + // Unicode scalar chars, so pin the legacy char mode for string-bearing + // generated programs. + // Dafny 4.11 warns that the option is deprecated; allow that CLI warning, + // while verification errors still fail normally. + if (usesJavaScriptStrings) args.push("--unicode-char:false", "--allow-warnings"); args.push(dfyPath); execFileSync("dafny", args, { cwd: dir, stdio: "inherit" }); return true; diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 234fb4c1..491b47eb 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -38,7 +38,7 @@ function tyToDafny(ty: Ty): string { case "int": return "int"; case "real": return "real"; case "bool": return "bool"; - case "string": return "string"; + case "string": _usesJavaScriptStrings = true; return "string"; case "void": return "()"; case "array": return `seq<${tyToDafny(ty.elem)}>`; case "tuple": return `(${ty.elems.map(tyToDafny).join(", ")})`; @@ -218,6 +218,26 @@ const OP_MAP: Record = { "arrayConcat": "+", }; +/** Render a JavaScript string without losing its UTF-16 representation. + * + * JavaScript iteration by index exposes UTF-16 code units, including unpaired + * surrogates. Node's UTF-8 file writer would replace an unpaired surrogate if + * we emitted it literally, so every non-printable/non-ASCII unit is written as + * a Dafny `\\uXXXX` escape. Under `--unicode-char:false`, each escape denotes + * exactly one Dafny char and therefore exactly one JavaScript code unit. + */ +function escapeDafnyUTF16String(value: string): string { + let out = ""; + for (let i = 0; i < value.length; i++) { + const unit = value.charCodeAt(i); + if (unit === 0x22) out += '\\"'; + else if (unit === 0x5c) out += "\\\\"; + else if (0x20 <= unit && unit <= 0x7e) out += String.fromCharCode(unit); + else out += `\\u${unit.toString(16).toUpperCase().padStart(4, "0")}`; + } + return out; +} + function mapOp(op: string): string { return OP_MAP[op] ?? op; } // ── Expression emission ───────────────────────────────────── @@ -256,7 +276,9 @@ function emitExpr(e: Expr): string { // Already canonical decimal; Dafny's `int` is mathematical, so no `n` suffix. case "bigint": return e.value; case "bool": return e.value ? "true" : "false"; - case "str": return `"${e.value.replace(/\\/g, '\\\\').replace(/"/g, '\\"').replace(/\n/g, '\\n')}"`; + case "str": + _usesJavaScriptStrings = true; + return `"${escapeDafnyUTF16String(e.value)}"`; case "constructor": { // Option constructors (Some/None) may appear in inferred positions @@ -349,10 +371,16 @@ function emitExpr(e: Expr): string { const comp = `seq(|${s}|, ${idx} requires 0 <= ${idx} < |${s}| => ${core})`; return bind ? `(var ${s} := ${obj}; ${comp})` : comp; } - if (e.method === "filter") return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`; + if (e.method === "filter") { + needPreamble("SeqFilter"); + return `SeqFilter(${args[0]}, ${obj})`; + } // filterMap (synthesized in resolve): drop Nones and unwrap to seq. if (e.method === "filterSome") { needPreamble("SeqFilterSome"); needPreamble("OptionType"); return `SeqFilterSome(${obj})`; } - if (e.method === "every") return `Std.Collections.Seq.All(${obj}, ${args[0]})`; + if (e.method === "every") { + needPreamble("SeqAll"); + return `SeqAll(${obj}, ${args[0]})`; + } if (e.method === "find") { needPreamble("OptionType"); needPreamble("SeqFind"); @@ -394,9 +422,10 @@ function emitExpr(e: Expr): string { } return `(exists ${p} :: ${p} in ${obj} && ${body})`; } - // `.reduce(f, init)` → Std's FoldLeft(f, init, xs) (same arg order). + // `.reduce(f, init)` → the local FoldLeft helper (same arg order). if (e.method === "reduce" && args.length === 2) { - return `Std.Collections.Seq.FoldLeft(${args[0]}, ${args[1]}, ${obj})`; + needPreamble("SeqFoldLeft"); + return `SeqFoldLeft(${args[0]}, ${args[1]}, ${obj})`; } } // String methods @@ -959,6 +988,13 @@ function needPreamble(key: string) { _neededPreambles.add(key); } * calls with provable bounds get direct `s[lo..hi]` emission. */ let _useSafeSlice = false; +// Set while emitting a file whenever its generated declarations use the +// JavaScript string model. The verifier reads the resulting marker so it can +// select Dafny's UTF-16-code-unit character mode. Keep this tied to emission, +// rather than a textual scan of the finished Dafny, so comments and proof +// additions cannot accidentally select the source-language model. +let _usesJavaScriptStrings = false; + const POW2 = `function Pow2(n: int): int requires n >= 0 decreases n @@ -1035,6 +1071,28 @@ const SEQ_FILTER_SOME = `function SeqFilterSome(xs: seq>): seq else (if xs[0].Some? then [xs[0].value] else []) + SeqFilterSome(xs[1..]) }`; +const SEQ_FILTER = `function SeqFilter(p: T -> bool, xs: seq): seq + ensures |SeqFilter(p, xs)| <= |xs| + ensures forall x :: x in SeqFilter(p, xs) <==> x in xs && p(x) + decreases |xs| +{ + if |xs| == 0 then [] + else (if p(xs[0]) then [xs[0]] else []) + SeqFilter(p, xs[1..]) +}`; + +const SEQ_ALL = `predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +}`; + +const SEQ_FOLD_LEFT = `function SeqFoldLeft(f: (A, T) -> A, init: A, xs: seq): A + decreases |xs| +{ + if |xs| == 0 then init + else SeqFoldLeft(f, f(init, xs[0]), xs[1..]) +}`; + const SEQ_FIND_INDEX = `function SeqFindIndex(s: seq, p: T -> bool): int ensures -1 <= SeqFindIndex(s, p) < |s| ensures SeqFindIndex(s, p) >= 0 ==> p(s[SeqFindIndex(s, p)]) @@ -1214,15 +1272,15 @@ const SEQ_SORT_BY = `function {:axiom} SeqSortBy(s: seq, cmp: (T, // U+0020, and NOT U+0085 (NEL, which is Cc). See // https://tc39.es/ecma262/#sec-white-space and // https://tc39.es/ecma262/#sec-line-terminators. -// `\\U{..}` are Dafny char escapes (not JS: the string -// is emitted verbatim), so the enumeration below is Dafny source, not decoded. +// `\\uXXXX` is Dafny's code-unit escape form when Unicode chars are disabled; +// the enumeration below is emitted Dafny source, not a decoded JS string. const STRING_TRIM = `predicate IsJSWhitespace(c: char) { - c == '\\U{0009}' || c == '\\U{000A}' || c == '\\U{000B}' || c == '\\U{000C}' || c == '\\U{000D}' || - c == '\\U{0020}' || c == '\\U{00A0}' || c == '\\U{1680}' || - ('\\U{2000}' <= c <= '\\U{200A}') || - c == '\\U{2028}' || c == '\\U{2029}' || c == '\\U{202F}' || c == '\\U{205F}' || - c == '\\U{3000}' || c == '\\U{FEFF}' + c == '\\u0009' || c == '\\u000A' || c == '\\u000B' || c == '\\u000C' || c == '\\u000D' || + c == '\\u0020' || c == '\\u00A0' || c == '\\u1680' || + ('\\u2000' <= c <= '\\u200A') || + c == '\\u2028' || c == '\\u2029' || c == '\\u202F' || c == '\\u205F' || + c == '\\u3000' || c == '\\uFEFF' } function StringTrimLeft(s: string): string @@ -1272,12 +1330,12 @@ const STRING_TO_UPPER = `function StringToUpper(s: string): string [upper] + StringToUpper(s[1..]) }`; -// `String.fromCharCode(n)` — the inverse of `s.charCodeAt(i)`'s `(s[i] as int)`. -// Dafny's `char` is a Unicode scalar value, so the argument must miss the -// surrogate range; that is the `requires`, discharged at each call site. The two -// `ensures` give callers the round-trip law without unfolding the body. +// `String.fromCharCode(n)` — the inverse of `s.charCodeAt(i)`'s `(s[i] as int)` +// in the UTF-16 code-unit model selected by dafny-commands.ts. LemmaScript +// currently admits the direct 16-bit range; JavaScript's wider ToUint16 coercion +// remains outside the verified subset. const STRING_FROM_CHAR_CODE = `function StringFromCharCode(n: int): string - requires 0 <= n < 0xD800 || 0xE000 <= n < 0x110000 + requires 0 <= n < 0x10000 ensures |StringFromCharCode(n)| == 1 ensures (StringFromCharCode(n)[0] as int) == n { @@ -1408,6 +1466,9 @@ const PREAMBLE_CODE: [string, string][] = [ ["SeqIndexOf", SEQ_INDEX_OF], ["SeqFindIndex", SEQ_FIND_INDEX], ["SeqFindLastIndex", SEQ_FIND_LAST_INDEX], + ["SeqFilter", SEQ_FILTER], + ["SeqAll", SEQ_ALL], + ["SeqFoldLeft", SEQ_FOLD_LEFT], ["SeqFilterSome", SEQ_FILTER_SOME], ["SeqFind", SEQ_FIND], ["SeqFindLast", SEQ_FIND_LAST], @@ -1539,6 +1600,7 @@ function translatePattern(p: MatchPattern): string { export function emitDafnyFile(file: Module, tsFileName?: string, opts?: { safeSlice?: boolean }): string { _useSafeSlice = !!opts?.safeSlice; + _usesJavaScriptStrings = false; resetDafnyNameCache(); buildRecordCtorMap(file.decls); _neededPreambles.clear(); @@ -1599,6 +1661,7 @@ export function emitDafnyFile(file: Module, tsFileName?: string, opts?: { safeSl // Build output with needed preambles const lines: string[] = []; if (tsFileName) lines.push(`// Generated by lsc from ${tsFileName}`); + if (_usesJavaScriptStrings) lines.push("// LemmaScript string model: javascript-utf16-code-units"); for (const [key, code] of PREAMBLE_CODE) { if (_neededPreambles.has(key)) { lines.push(""); lines.push(code); } } diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index d72b1a0f..78ed0a56 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -38,6 +38,7 @@ fixture_dir=$(mktemp -d) trap 'rm -rf "$fixture_dir"' EXIT cp tools/fixtures/deterministic-extern-equality.ts "$fixture_dir/deterministic.ts" cp tools/fixtures/impure-extern-equality.ts "$fixture_dir/impure.ts" +cp tools/fixtures/javascript-utf16-strings.ts "$fixture_dir/utf16.ts" npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/impure.ts" if ! grep -Fq 'method {:axiom} rollDie' "$fixture_dir/impure.dfy.gen"; then @@ -49,3 +50,15 @@ npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/det expect_failure \ "Dafny equated two calls to an impure extern" \ npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/impure.ts" + +# JavaScript string length/indexing are UTF-16-code-unit operations. Astral +# characters therefore occupy two Dafny chars, and lone surrogates remain +# representable instead of being replaced while writing the generated file. +npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/utf16.ts" +grep -Fq '// LemmaScript string model: javascript-utf16-code-units' "$fixture_dir/utf16.dfy.gen" +grep -Fq '"\uD83D\uDE00"' "$fixture_dir/utf16.dfy.gen" +grep -Fq '"\uD83D"' "$fixture_dir/utf16.dfy.gen" + +expect_failure \ + "Dafny standard library was combined with JavaScript UTF-16 strings" \ + npx tsx -e 'import { dafnyVerify } from "./tools/src/dafny-commands.ts"; process.exit(dafnyVerify("tools/fixtures/string-with-standard-library.dfy", process.cwd()) ? 0 : 1)' From 4b5ed704d66a9ddb142d2dd69ce0ef81e1c58f56 Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 15:34:24 -0700 Subject: [PATCH 02/15] docs: remove design reference from string option description --- tools/src/config.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/src/config.ts b/tools/src/config.ts index cb3d0160..2a202b61 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -36,7 +36,7 @@ export const OPTION_SPECS = { values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: false, - description: "Which model of JavaScript strings a Dafny proof is made under (DESIGN_STRINGS.md).", + description: "Which model of JavaScript strings a Dafny proof is made under.", }, } as const; From 8a5384a1cd9d8901329884aabc5f3abd14e6af0b Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 15:39:10 -0700 Subject: [PATCH 03/15] docs: make configuration and verifier comments self-contained --- tools/src/config.ts | 8 +++----- tools/src/dafny-commands.ts | 15 +++++++-------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/tools/src/config.ts b/tools/src/config.ts index 2a202b61..3bb4158d 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -213,12 +213,10 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp return out as ExplicitOptions; } -/** Apply defaults and all cross-option rules after explicit layers are merged. */ +/** Fill missing options with defaults and freeze the resolved configuration. */ export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions { - // There are no cross-option constraints in the registry: `string-semantics` - // selects the Dafny helper source by itself (DESIGN_STRINGS.md §4). Keep this - // as the single resolution gate for future dependent defaults and - // incompatibilities, before any consumer runs. + // Each option is independent: selecting a value for one option does not + // change another option's default or make its value invalid. void source; return Object.freeze({ ...DEFAULT_OPTIONS, ...explicit }); } diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index d9a8f053..421cf83f 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -72,13 +72,12 @@ const OPTIONS_HEADER = /^\/\/ lsc options:(.*)$/m; const STRING_SEMANTICS = ["unicode-scalar", "javascript-utf16"]; /** - * Verifier arguments implied by a generated file's `// lsc options:` header - * (DESIGN_STRINGS.md §5–6). Read from the artifact rather than the config, so a - * standalone `.dfy` verifies under the model it was generated for. The char - * mode is always pinned — a default is not a pin. Only `--unicode-char:false` - * is deprecated in Dafny 4.11, and `--allow-deprecation` waives exactly that - * warning; the blanket warning waiver would also un-fatal vacuity and - * missing-{:axiom} warnings, which a verifier must keep fatal. + * Build verifier arguments from the generated file's `// lsc options:` header. + * Reading the saved string model instead of the current project config keeps + * verification consistent with generation, even if the config later changes. + * Always pass `--unicode-char` explicitly. UTF-16 mode also needs + * `--allow-deprecation` because Dafny 4.11 deprecates `--unicode-char:false`. + * Other warning categories remain fatal. */ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?: string): { args: string[]; error?: string } { let stringSemantics = "unicode-scalar"; @@ -89,7 +88,7 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? const value = eq < 0 ? "" : token.slice(eq + 1); if (key !== "string-semantics") continue; if (!STRING_SEMANTICS.includes(value)) { - return { args: [], error: `ERROR: unknown string-semantics '${value}' in the generated header; this lsc knows ${STRING_SEMANTICS.join(", ")} (DESIGN_STRINGS.md).` }; + return { args: [], error: `ERROR: unknown string-semantics '${value}' in the generated header; this lsc knows ${STRING_SEMANTICS.join(", ")}.` }; } stringSemantics = value; } From 5e47d66136716c78aa07e07eda8d78c171ae442a Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 15:54:18 -0700 Subject: [PATCH 04/15] fix: reuse config validation for Dafny string semantics --- tools/src/config.ts | 15 +++++---- tools/src/dafny-commands.ts | 11 +++--- tools/tests/dafny-commands.test.ts | 54 +++++++++++++++++++++++++++--- 3 files changed, 63 insertions(+), 17 deletions(-) diff --git a/tools/src/config.ts b/tools/src/config.ts index 3bb4158d..52d6d6cd 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -68,23 +68,24 @@ function isKnownKey(key: string): key is keyof OptionSpecs { return Object.hasOwn(OPTION_SPECS, key); } -function parseValue(key: keyof OptionSpecs, raw: unknown, source: string): LscOptions[typeof key] { +/** Validate one option against the registry and return its typed value. */ +export function parseOptionValue(key: K, raw: unknown, source: string): LscOptions[K] { const spec = OPTION_SPECS[key] as AnyOptionSpec; if (spec.type === "boolean") { if (typeof raw !== "boolean") fail(source, `option '${key}' must be true or false`); - return raw as LscOptions[typeof key]; + return raw as LscOptions[K]; } if (spec.type === "enum") { if (typeof raw !== "string" || !(spec.values as readonly string[]).includes(raw)) { fail(source, `option '${key}' must be one of: ${spec.values.join(", ")}`); } - return raw as LscOptions[typeof key]; + return raw as LscOptions[K]; } if (typeof raw !== "string" || raw.trim().length === 0) { fail(source, `option '${key}' must be a non-empty relative path`); } if (path.isAbsolute(raw)) fail(source, `option '${key}' must be relative to lemmascript.json`); - return raw as LscOptions[typeof key]; + return raw as LscOptions[K]; } /** Validate a parsed lemmascript.json object, returning only explicitly set keys. */ @@ -98,7 +99,7 @@ export function validateOptions(raw: unknown, source: string): ExplicitOptions { if (!isKnownKey(key)) { fail(source, `unknown option '${key}' (known options: ${KNOWN_KEYS.join(", ")})`); } - out[key] = parseValue(key, value, source); + out[key] = parseOptionValue(key, value, source); } return out as ExplicitOptions; } @@ -109,10 +110,10 @@ function parseDirectiveValue(key: keyof OptionSpecs, text: string, source: strin if (text !== "true" && text !== "false") fail(source, `option '${key}' must be true or false`); return (text === "true") as LscOptions[typeof key]; } - if (spec.type === "enum") return parseValue(key, text, source); + if (spec.type === "enum") return parseOptionValue(key, text, source); // Config-only today, but keep the diagnostic precise if a future path is // made file-overridable. - return parseValue(key, text, source); + return parseOptionValue(key, text, source); } /** diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 421cf83f..cf868855 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -5,6 +5,7 @@ import { existsSync, readFileSync, writeFileSync, copyFileSync, unlinkSync } from "fs"; import { execFileSync } from "child_process"; import path from "path"; +import { DEFAULT_OPTIONS, parseOptionValue, type LscOptions } from "./config.js"; function writeGen(genPath: string, text: string) { writeFileSync(genPath, text); @@ -69,7 +70,6 @@ export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean { } const OPTIONS_HEADER = /^\/\/ lsc options:(.*)$/m; -const STRING_SEMANTICS = ["unicode-scalar", "javascript-utf16"]; /** * Build verifier arguments from the generated file's `// lsc options:` header. @@ -80,17 +80,18 @@ const STRING_SEMANTICS = ["unicode-scalar", "javascript-utf16"]; * Other warning categories remain fatal. */ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?: string): { args: string[]; error?: string } { - let stringSemantics = "unicode-scalar"; + let stringSemantics: LscOptions["string-semantics"] = DEFAULT_OPTIONS["string-semantics"]; const header = content.match(OPTIONS_HEADER); for (const token of (header?.[1] ?? "").trim().split(/\s+/).filter(Boolean)) { const eq = token.indexOf("="); const key = eq < 0 ? token : token.slice(0, eq); const value = eq < 0 ? "" : token.slice(eq + 1); if (key !== "string-semantics") continue; - if (!STRING_SEMANTICS.includes(value)) { - return { args: [], error: `ERROR: unknown string-semantics '${value}' in the generated header; this lsc knows ${STRING_SEMANTICS.join(", ")}.` }; + try { + stringSemantics = parseOptionValue(key, value, "generated header"); + } catch (error) { + return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` }; } - stringSemantics = value; } const utf16 = stringSemantics === "javascript-utf16"; const usesStandardLibrary = content.includes("Std."); diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts index faa9244a..f0a1ca47 100644 --- a/tools/tests/dafny-commands.test.ts +++ b/tools/tests/dafny-commands.test.ts @@ -3,6 +3,7 @@ import assert from "node:assert/strict"; import { chmodSync, mkdtempSync, rmSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; import { join } from "node:path"; +import { DEFAULT_OPTIONS, OPTION_SPECS, validateOptions } from "../src/config.ts"; import { dafnyCheckDiff, dafnyVerifyArgs } from "../src/dafny-commands.ts"; function fixture(gen: string, proof: string, check: (g: string, p: string, dir: string) => void): void { @@ -80,9 +81,19 @@ test("missing Git executable is not success", () => { fixture("x\n", "y\n", (g, p, dir) => env({ PATH: dir }, () => assert.equal(dafnyCheckDiff(g, p), false))); }); -test("no header token pins Dafny's default char mode explicitly", () => { - assert.deepEqual(dafnyVerifyArgs("// Generated by lsc from a.ts\nmethod M() {}\n").args, ["verify", "--unicode-char:true"]); - assert.deepEqual(dafnyVerifyArgs("method M() {}\n").args, ["verify", "--unicode-char:true"]); +test("no header token uses the configuration default", () => { + const explicit = dafnyVerifyArgs(`// lsc options: string-semantics=${DEFAULT_OPTIONS["string-semantics"]}\n`); + assert.equal(explicit.error, undefined); + assert.deepEqual(dafnyVerifyArgs("// Generated by lsc from a.ts\nmethod M() {}\n"), explicit); + assert.deepEqual(dafnyVerifyArgs("method M() {}\n"), explicit); +}); + +test("every registered string model is accepted in the proof header", () => { + for (const value of OPTION_SPECS["string-semantics"].values) { + const result = dafnyVerifyArgs(`// lsc options: string-semantics=${value}\n`); + assert.equal(result.error, undefined); + assert.ok(result.args.includes(value === "javascript-utf16" ? "--unicode-char:false" : "--unicode-char:true")); + } }); test("javascript-utf16 selects code-unit chars and only the deprecation waiver", () => { @@ -96,8 +107,41 @@ test("javascript-utf16 refuses the Unicode-scalar standard library", () => { assert.match(error ?? "", /string-semantics/); }); -test("an unknown string-semantics token is an error, not a silent default", () => { - assert.match(dafnyVerifyArgs("// lsc options: string-semantics=utf8\n").error ?? "", /unknown string-semantics 'utf8'/); +for (const token of ["string-semantics=utf8", "string-semantics=", "string-semantics"]) { + test(`proof header uses config validation for invalid token: ${token}`, () => { + const value = token.includes("=") ? token.slice(token.indexOf("=") + 1) : ""; + let message = ""; + assert.throws(() => validateOptions({ "string-semantics": value }, "generated header"), (error: Error) => { + message = error.message; + return true; + }); + const result = dafnyVerifyArgs(`// lsc options: ${token}\n`); + assert.deepEqual(result, { args: [], error: `ERROR: ${message}` }); + assert.match(result.error ?? "", /generated header: option 'string-semantics' must be one of:/); + }); +} + +test("a later valid token does not hide an invalid string model", () => { + assert.deepEqual( + dafnyVerifyArgs("// lsc options: string-semantics=utf8 string-semantics=javascript-utf16\n"), + dafnyVerifyArgs("// lsc options: string-semantics=utf8\n"), + ); +}); + +test("proof header settings are independent of the current project config", () => { + fixture("", "", (_gen, _proof, dir) => { + const previousDirectory = process.cwd(); + try { + process.chdir(dir); + for (const value of OPTION_SPECS["string-semantics"].values) { + writeFileSync(join(dir, "lemmascript.json"), JSON.stringify({ "string-semantics": value })); + assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n").args, + ["verify", "--unicode-char:false", "--allow-deprecation"]); + assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=unicode-scalar\n").args, + ["verify", "--unicode-char:true"]); + } + } finally { process.chdir(previousDirectory); } + }); }); test("time limit and extra flags keep their positions before the char-mode pin", () => { From d911efea8c909566052d760ee2a8426ef18388dc Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 15:59:51 -0700 Subject: [PATCH 05/15] test: cover per-file Dafny string state reset --- tools/src/dafny-emit.ts | 1 + tools/tests/dafny-emit.test.ts | 78 ++++++++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 tools/tests/dafny-emit.test.ts diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 2e1f04b2..25b472ab 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -1623,6 +1623,7 @@ function translatePattern(p: MatchPattern): string { export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOptions = DEFAULT_OPTIONS): string { _useSafeSlice = options["safe-slice"]; _stringSemantics = options["string-semantics"]; + // Reset before scanning types, including when the previous file failed to emit. _usesStrings = false; resetDafnyNameCache(); buildRecordCtorMap(file.decls); diff --git a/tools/tests/dafny-emit.test.ts b/tools/tests/dafny-emit.test.ts new file mode 100644 index 00000000..f227e3a7 --- /dev/null +++ b/tools/tests/dafny-emit.test.ts @@ -0,0 +1,78 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { DEFAULT_OPTIONS, type LscOptions } from "../src/config.ts"; +import { emitDafnyFile } from "../src/dafny-emit.ts"; +import type { Decl, Module } from "../src/ir.ts"; + +const utf16: LscOptions = { ...DEFAULT_OPTIONS, "string-semantics": "javascript-utf16" }; +const optionsHeader = /^\/\/ lsc options: string-semantics=javascript-utf16$/m; + +function moduleWith(...decls: Decl[]): Module { + return { comment: "", imports: [], options: [], decls }; +} + +const numbers = moduleWith({ kind: "const", name: "answer", type: { kind: "int" }, value: { kind: "num", value: 42 } }); +const stringType: Decl = { kind: "type-alias", name: "Text", target: { kind: "string" } }; + +for (const [name, declaration] of [ + ["string type without literals", stringType], + ["nested string type", { kind: "type-alias", name: "Texts", target: { + kind: "optional", inner: { kind: "array", elem: { kind: "string" } }, + } }], + ["string literals without string annotations", { kind: "const", name: "same", type: { kind: "bool" }, value: { + kind: "binop", op: "==", left: { kind: "str", value: "hello" }, right: { kind: "str", value: "hello" }, + } }], +] satisfies [string, Decl][]) { + test(`string usage resets between files after ${name}`, () => { + const baseline = emitDafnyFile(numbers, "numbers.ts", utf16); + assert.doesNotMatch(baseline, optionsHeader); + assert.match(emitDafnyFile(moduleWith(declaration), "strings.ts", utf16), optionsHeader); + assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline); + }); +} + +test("string usage remains set across declarations within one file", () => { + assert.match(emitDafnyFile(moduleWith(stringType, ...numbers.decls), "mixed.ts", utf16), optionsHeader); +}); + +test("string profile and literal encoding reset between files", () => { + const literal = moduleWith({ kind: "const", name: "emoji", type: { kind: "string" }, value: { kind: "str", value: "😀" } }); + const encoded = emitDafnyFile(literal, "literal.ts", utf16); + assert.match(encoded, optionsHeader); + assert.ok(encoded.includes('"\\uD83D\\uDE00"')); + + // Omit the options argument so the default must replace the previous profile. + const scalar = emitDafnyFile(literal, "literal.ts"); + assert.doesNotMatch(scalar, optionsHeader); + assert.ok(scalar.includes('"😀"')); + assert.equal(emitDafnyFile(literal, "literal.ts", utf16), encoded); +}); + +test("string helper preambles do not leak into the next file", () => { + const baseline = emitDafnyFile(numbers, "numbers.ts", utf16); + const search = moduleWith({ kind: "const", name: "position", type: { kind: "int" }, value: { + kind: "methodCall", obj: { kind: "str", value: "hello" }, objTy: { kind: "string" }, + method: "indexOf", args: [{ kind: "str", value: "e" }], monadic: false, + } }); + const output = emitDafnyFile(search, "search.ts", utf16); + assert.match(output, optionsHeader); + assert.match(output, /function StringIndexOf\(/); + assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline); +}); + +for (const inNamespace of [false, true]) { + test(`string usage resets after failed emission${inNamespace ? " inside a namespace" : ""}`, () => { + const baseline = emitDafnyFile(numbers, "numbers.ts", utf16); + const declarations: Decl[] = [stringType, { + kind: "const", name: "unsupported", type: { kind: "int" }, value: { + kind: "methodCall", obj: { kind: "str", value: "hello" }, objTy: { kind: "string" }, + method: "unsupported", args: [], monadic: false, + }, + }]; + const failing = inNamespace + ? moduleWith({ kind: "namespace", name: "Example", decls: declarations }) + : moduleWith(...declarations); + assert.throws(() => emitDafnyFile(failing, "unsupported.ts", utf16), /Unsupported Dafny method call/); + assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline); + }); +} From 3199c140ac771cb8f8bdbff3ee9878c4e868b39a Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 17:06:12 -0700 Subject: [PATCH 06/15] feat: separate Dafny collection library configuration Default dafny-library to stdlib independently of the string model. Require an explicit local selection for javascript-utf16 and reject incompatible settings through the shared config resolver. Route filter, every, and reduce through the library option; cover configuration errors, per-file state reset, and real Dafny proofs across the three valid combinations. Update fixtures and documentation. --- DESIGN_CONFIG.md | 59 ++++++++++--------- DESIGN_STRINGS.md | 53 ++++++++++------- SPEC.md | 6 +- SPEC_DAFNY.md | 12 +++- TOOLS.md | 7 ++- site/src/content/docs/reference/cli.md | 5 ++ .../collection-library-project/collections.ts | 37 ++++++++++++ .../lemmascript.json | 3 + .../lemmascript.json | 3 + .../config-incompatible-strings/source.ts | 7 +++ .../config-incompatible-strings/stdlib.json | 4 ++ tools/fixtures/utf16-project/lemmascript.json | 3 +- tools/src/config.ts | 19 ++++-- tools/src/dafny-emit.ts | 18 +++--- tools/src/extract.ts | 2 +- tools/test-fixtures.sh | 59 ++++++++++++++++++- tools/tests/config.test.ts | 32 +++++++++- tools/tests/dafny-emit.test.ts | 35 ++++++++++- 18 files changed, 291 insertions(+), 73 deletions(-) create mode 100644 tools/fixtures/collection-library-project/collections.ts create mode 100644 tools/fixtures/collection-library-project/lemmascript.json create mode 100644 tools/fixtures/config-incompatible-strings/lemmascript.json create mode 100644 tools/fixtures/config-incompatible-strings/source.ts create mode 100644 tools/fixtures/config-incompatible-strings/stdlib.json diff --git a/DESIGN_CONFIG.md b/DESIGN_CONFIG.md index 810af9a6..20aaff38 100644 --- a/DESIGN_CONFIG.md +++ b/DESIGN_CONFIG.md @@ -1,6 +1,6 @@ # DESIGN_CONFIG — Project options via `lemmascript.json` -**Status:** initial implementation complete. The registry, `extern-default`, `safe-slice`, `proof-dir`, file overrides, and `lsc config` are implemented. #211 (Dafny strings as JavaScript UTF-16 code units) and #205 (JavaScript number semantics) remain future users of the mechanism and are not implemented here. +**Status:** implemented. The registry supports `extern-default`, `safe-slice`, `proof-dir`, file overrides, and `lsc config`. PR #211 adds `string-semantics` and `dafny-library`, including their compatibility check. #205 (JavaScript number semantics) remains a future user of the mechanism. **Date:** August 2026 ## Requirements @@ -50,6 +50,8 @@ export const OPTION_SPECS = { "extern-default": { type: "enum", values: ["pure", "impure"], default: "pure", fileOverride: true, description: "…" }, "safe-slice": { type: "boolean", default: false, fileOverride: true, directiveAliases: ["safe-slice"], description: "…" }, "proof-dir": { type: "path", default: null, fileOverride: false, description: "…" }, + "string-semantics": { type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: false, description: "…" }, + "dafny-library": { type: "enum", values: ["stdlib", "local"], default: "stdlib", fileOverride: false, description: "…" }, } as const; export type LscOptions = { readonly [K in keyof typeof OPTION_SPECS]: /* boolean | enum union | string | null */ }; @@ -58,12 +60,12 @@ export const DEFAULT_OPTIONS: LscOptions; export function validateOptions(raw: unknown, source: string): ExplicitOptions; // per-key checks; returns only explicit keys export function parseFileOptions(sourceText: string, source: string): ExplicitOptions; -export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions; // defaults + dependent defaults + cross-key checks +export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions; // defaults + cross-key checks export function loadConfigOptions(sourcePath: string, configPath?: string): { explicit: ExplicitOptions; configFile: string | null }; export function resolveDafnyArtifactDir(sourcePath: string, configFile: string | null, options: LscOptions): string; ``` -`validateOptions` and `parseFileOptions` return only the keys that were present. `lsc.ts` merges those two partial objects, file over config, and calls `resolveOptions` once, so future dependent defaults can distinguish an explicit setting from a default. `resolveOptions` applies dependent defaults and then rejects cross-key contradictions; the message names the conflicting explicit settings and the fix. The file parser uses the registry's types, enum values, and `fileOverride` field rather than maintaining a second switch; its only special cases come from declared `directiveAliases`. The `path` type accepts a non-empty relative string; the artifact helper anchors it at the selected config file and performs the containment check from §3.3. +`validateOptions` and `parseFileOptions` return only the keys that were present. `lsc.ts` merges those two partial objects, file over config, and calls `resolveOptions`. It fills registry defaults and then rejects cross-key contradictions; the message names the conflicting settings and the fix. The file parser uses the registry's types, enum values, and `fileOverride` field rather than maintaining a second switch; its only special cases come from declared `directiveAliases`. The `path` type accepts a non-empty relative string; the artifact helper anchors it at the selected config file and performs the containment check from §3.3. Adding an independent option is: one registry entry, then `options[""]` in the consuming phase, then a row in SPEC.md §7 and a fixture. An interacting option also adds its dependent-default or incompatibility rule to `resolveOptions` and a negative fixture; consumers still receive only a valid, fully resolved set. @@ -102,21 +104,24 @@ The source must be inside the config directory when `proof-dir` is set (includin Enabling the option must not silently strand proof additions. If the mapped `.dfy` is absent but a sibling `.dfy`, `.dfy.base`, or `.dfy.merged` exists beside the TS, `lsc` fails with paths and tells the user to move the hand-written `.dfy`, discard or inspect merge-state files, and rerun; `.dfy.gen` is regeneratable. Changing from one non-default proof directory to another likewise requires moving the proof first and is documented as a migration, because the new config cannot discover an arbitrary old root. -## Future options (not part of the initial implementation) +## String and collection options (PR #211, issue #210) -The registry and resolution path are intended to accept the following options later, but this proposal does not add their keys, change their emitters, add verifier flags, or add their fixtures. +`string-semantics: "unicode-scalar" | "javascript-utf16"` chooses the string model, +defaulting to `unicode-scalar`. `dafny-library: "stdlib" | "local"` independently chooses +the generated collection helpers, defaulting to `stdlib`. Both are config-only. -### `javascript-utf16` and `dafny-lib` (PR #211, issue #210) +`stdlib` emits `Std.Collections.Seq.Filter/All/FoldLeft` for `filter`/`every`/`reduce`; +`local` emits `SeqFilter`/`SeqAll`/`SeqFoldLeft` definitions on demand. Unicode-scalar +projects may select either. UTF-16 requires an explicit `local` choice: `resolveOptions` +rejects both an omitted and an explicit `stdlib`, without silently changing the default. -A later `javascript-utf16: true` option would gate PR #211's Dafny emitter behavior: +UTF-16 string-bearing artifacts record their model in the header; verification uses +`--unicode-char:false --allow-deprecation`. The precompiled Dafny standard library uses +Unicode-scalar characters and cannot load in that mode. The artifact-level check still +rejects `Std.*` in UTF-16 proof additions; config validation cannot inspect handwritten +proof text. The library choice itself requires no additional verifier flag. -- `string` types and `str` literals set a per-emission flag; literals are written as `\uXXXX` code-unit escapes for everything outside printable ASCII, so astral pairs and lone surrogates survive the UTF-8 file. -- Preambles that mention chars vary with the mode. This is forced, not stylistic: Dafny 4.11 rejects `\U{…}` escapes under `--unicode-char:false` and `\u…` escapes under the default, so `IsJSWhitespace` (StringTrim) must be emitted with `\u0009…` in UTF-16 mode and `\U{0009}…` otherwise, and `StringFromCharCode`'s `requires` is `0 <= n < 0x10000` vs the surrogate-free scalar range. `PREAMBLE_CODE` entries become `string | (options) => string`. -- The file header records the model (§5), and `dafnyVerify` passes `--unicode-char:false --allow-warnings` when it sees it. `--allow-warnings` is required: 4.11 prints a deprecation warning for the flag and, by default, a warning fails the run. - -A future `dafny-lib` option would select where `filter`/`every`/`reduce` come from: `Std.Collections.Seq.Filter/All/FoldLeft` (today; `dafnyVerify` already auto-adds `--standard-libraries` on a `Std.` substring) or the local `SeqFilter`/`SeqAll`/`SeqFoldLeft` recursive helpers from PR #211, emitted into the preamble on demand like `SeqFind`. - -The two would interact: Dafny's precompiled standard library is built for Unicode-scalar chars and cannot load under `--unicode-char:false`. After config and file layers are merged, `resolveOptions` must implement exactly this rule: if `javascript-utf16` is true and `dafny-lib` is absent, supply the dependent default `local-lib`; if `dafny-lib` is explicitly `std-lib`, reject the combination and name both keys. An explicit incompatible choice is never silently replaced. PR #211's per-file fail-closed check would stay as the last line of defense (a UTF-16 file whose *proof additions* import `Std.*`), because the config can't see hand-written proof text; its message should name the config key. A string-free file could keep importing `Std.*` in its proofs: the header marker would only be emitted when strings actually appear. +## Future options ### `number-semantics` (issue #205) @@ -130,25 +135,25 @@ JavaScript numbers need an enum-shaped semantic choice, not a `javascript-number | `extract.ts` | `extractModule(sourceFile, options = DEFAULT_OPTIONS)`; module-level `_options` set on entry, following the existing `_externs` reset pattern; `externIsImpure` reads it. | | `resolve`, `narrow`, `autohavoc`, `peephole` | Unchanged initially. Add an `options` parameter only when a future option needs one. | | `transform.ts` | Unchanged. `TransformOptions { backend, monadic }` is backend-intrinsic pipeline configuration; keep it separate rather than merging `LscOptions` into it. | -| `dafny-emit.ts` | `emitDafnyFile(file, tsFileName, options = DEFAULT_OPTIONS)` replaces the `{ safeSlice }` bag; `_useSafeSlice` becomes `_options["safe-slice"]`. No other emission changes are part of this proposal. | -| `dafny-commands.ts` | Algorithms are unchanged; `lsc.ts` passes mapped artifact paths and uses the mapped directory as the verifier/regen working directory. Artifact-derived verifier flags belong to the future options in §5. | -| `lean-emit.ts` | Error text only. Dafny-only options are ignored under Lean without a warning — a per-file warning would be noise in batch mode, and the docs table carries the backend column. | +| `dafny-emit.ts` | `emitDafnyFile(file, tsFileName, options = DEFAULT_OPTIONS)` receives resolved settings and applies the shared compatibility check for programmatic callers. Each emission resets its safe-slice, string, and collection-library state from those settings. | +| `dafny-commands.ts` | `lsc.ts` passes mapped artifact paths and uses the mapped directory as the verifier/regen working directory. The generated artifact's options header determines verifier flags (§5). | +| `lean-emit.ts` | The CLI rejects UTF-16 because Lean has no matching string model. Other Dafny-only settings do not affect Lean emission. | | `info-command.ts` | `lsc info --typed` gains a top-level `options` field (the effective set). Additive, so `schema` stays `1`. | Optional-with-default parameters keep any external programmatic caller of `extractModule`/`emitDafnyFile` working; the CLI always passes explicitly. -## 5. Future artifact headers +## 5. Artifact headers -The initial options do not require non-default verifier flags, so this proposal does not change generated headers or `dafnyVerify`. When a future option does require flags, preserve PR #211's idea — the artifact, not the config, is what a human hands to `dafny verify` — but generalize the form so each option does not invent another sentence: +Options requiring non-default verifier flags are recorded in the artifact, so a standalone proof keeps its interpretation without reading the project config: ``` // Generated by lsc from foo.ts -// lsc options: javascript-utf16 +// lsc options: string-semantics=javascript-utf16 ``` -The future line is space-separated `key` (boolean) or `key=value` tokens, listing only non-default options that *materially affected this file* (UTF-16 would appear only when the file has strings; `dafny-lib` would never appear because it changes emitted helpers, not verifier flags). `dafnyVerify` would parse the line and map tokens to flags: `javascript-utf16` → `--unicode-char:false --allow-warnings`; a future `number-semantics=javascript` marker would select the version/capability checks and any flags established by the number-backend spike. The additions-only check already guarantees `.dfy` and `.dfy.gen` share the header, so flipping an option in `lemmascript.json` would surface as an ordinary generator change: `regen` three-way-merges the new header line in, then verifies under the new flags. +The line contains space-separated option tokens. UTF-16 appears only when the file has strings and selects `--unicode-char:false --allow-deprecation`. `dafny-library` does not need a token because it changes emitted helpers, not verifier flags. A future number-model marker can use the same mechanism. The additions-only check guarantees `.dfy` and `.dfy.gen` share the header, so changing a model surfaces as a generator change: `regen` merges the new header before verification. -Reading future flags from the artifact rather than from the config is deliberate: the two could not drift within one `lsc check`, while a standalone `.dfy` (a fixture, a file someone pulled out of a repo) would still verify correctly and a reader would see the model on line 2. +Without a string-model token, verification explicitly uses `--unicode-char:true`. Existing scalar artifacts therefore need no header change. ## 6. CLI surface @@ -167,7 +172,7 @@ Reading future flags from the artifact rather than from the config is deliberate - **`extern-default`** generalizes the existing explicit `//@ impure` path and adds config/directive fixtures and conditional docs. No default-flipping PR or regenerated examples are needed; existing examples keep their explicit `//@ impure`, and unmarked externs remain pure. - **Existing `safe-slice`** moves from an emitter-specific boolean into the registry without changing generated output. Its old directive remains an alias. - **`proof-dir`** adds path routing only; it does not change emitter text or the additions-only/regen algorithms. Existing projects stay beside-source until they opt in and move their hand-written proofs. -- **#211 and #205** do not land as part of this proposal. When their encodings are ready, they add registry entries and the explicitly future emitter/header work above, with their own fixtures and docs. +- **#211** adds string models and collection-library selection through the same registry and artifact mechanism. **#205** remains a future number-model extension. - **Flipping a default later:** change the registry line, run `./regen-dafny.sh`, and note it in the release. Projects that want the old model add one key. The registry's `default` field is where that decision lives, visibly, rather than being implicit in emitter code. ## Non-goals @@ -175,7 +180,7 @@ Reading future flags from the artifact rather than from the config is deliberate - Per-function option overrides. `//@ option` is file-level; function facts keep their specific annotations. - A `backend` config option. `--backend=` selects the command target and `//@ backend` declares file membership; neither is a semantic model option. - Relocating Lean artifacts with `proof-dir`. Lean paths participate in module names and Lake roots, unlike standalone Dafny files, so that needs its own design. -- Implementing `javascript-utf16`, `dafny-lib`, or `number-semantics`; they are future applications documented above, not initial registry entries. +- Implementing `number-semantics`; it remains a future application documented above. - Nested/namespaced config (`{"dafny": {…}}`). Flat kebab-case keys with a backend column in the docs are enough for the initial options; revisit past ~15. - `time-limit` / `extra-flags` as project defaults. `LemmaScript-files.txt` already carries them per file; adding a project-wide default is a registry entry away if a case study asks. - JSON Schema generation (`lsc config --schema`). Cheap follow-up from the registry; not needed to land. @@ -183,6 +188,6 @@ Reading future flags from the artifact rather than from the config is deliberate ## Open questions -1. **Future string option shape.** Should `javascript-utf16` be a boolean or should a later proposal use `strings: "unicode-scalar" | "javascript-utf16"`? This does not block the initial config implementation. -2. **Future `--allow-warnings` scope.** UTF-16 mode would need it for Dafny's `--unicode-char` deprecation warning, but it also un-fatals every other warning in the file. Resolve this with the UTF-16 implementation, not here. -3. **Future header parsing.** When artifact-derived flags exist, should `dafnyVerify` warn when a `.dfy` lacks the `// Generated by lsc` line entirely? Resolve this with the first option that needs such a header. +1. **Resolved string option shape.** `string-semantics: "unicode-scalar" | "javascript-utf16"` selects the string model. The independent `dafny-library` option selects collection helpers. +2. **Resolved warning scope.** UTF-16 uses `--allow-deprecation` for Dafny's character-mode flag. Other warnings remain fatal. +3. **Header parsing.** Should `dafnyVerify` warn when a `.dfy` lacks the `// Generated by lsc` line entirely? It currently accepts such files and uses the default string model when no options header is present. diff --git a/DESIGN_STRINGS.md b/DESIGN_STRINGS.md index 8d92af8e..ad6795db 100644 --- a/DESIGN_STRINGS.md +++ b/DESIGN_STRINGS.md @@ -1,6 +1,6 @@ # DESIGN_STRINGS — JavaScript string semantics as a versioned profile -**Status:** rung 0 and rung 1 implemented in PR #211; later rungs unscheduled. Takes up the `javascript-utf16` sketch in [DESIGN_CONFIG.md](DESIGN_CONFIG.md) §"Future options" and answers its open question 1 with the enum shape it asked about. Rung 1 is PR #211 rebased onto the option registry that shipped in 0.6.4 — #211's merge-base is 0.6.1 (`bcaf168`), before `tools/src/config.ts` existed. +**Status:** rung 0 and rung 1 implemented in PR #211; later rungs unscheduled. The project selects its string model and collection library through the option registry described in [DESIGN_CONFIG.md](DESIGN_CONFIG.md). **Date:** September 2026 **Issue:** [#210](https://github.com/midspiral/LemmaScript/issues/210) · **PR:** [#211](https://github.com/midspiral/LemmaScript/pull/211) @@ -25,7 +25,8 @@ shape [DESIGN_NUMBERS.md](DESIGN_NUMBERS.md) chose for `number-semantics`: `unicode-scalar` stays the default so no `lemmascript.json` means today's behaviour ([DESIGN_CONFIG.md](DESIGN_CONFIG.md) requirement 3). A project opts into `javascript-utf16` -with one key. A `javascript-utf16` proof carries `// lsc options: string-semantics=javascript-utf16` +by setting `"string-semantics": "javascript-utf16"` and `"dafny-library": "local"` explicitly. +A `javascript-utf16` proof carries `// lsc options: string-semantics=javascript-utf16` in its header ([DESIGN_CONFIG.md](DESIGN_CONFIG.md) §5 form); the default's header is unchanged, so no existing artifact changes. Each identity's claim sentence lives in SPEC_DAFNY.md §4. `dafnyVerify` pins `--unicode-char:true` whenever the token is absent — @@ -141,7 +142,7 @@ for the domain and states the operations that differ instead. ## 4. Configuration -One registry entry in [`tools/src/config.ts`](tools/src/config.ts), following the shape +Two registry entries in [`tools/src/config.ts`](tools/src/config.ts), following the shape `OPTION_SPECS` already has: ```ts @@ -150,7 +151,14 @@ One registry entry in [`tools/src/config.ts`](tools/src/config.ts), following th values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: false, - description: "Which model of JavaScript strings a proof is made under (DESIGN_STRINGS.md).", + description: "Which model of JavaScript strings a Dafny proof is made under.", +}, +"dafny-library": { + type: "enum", + values: ["stdlib", "local"], + default: "stdlib", + fileOverride: false, + description: "Use Dafny's standard library or generated local helpers for collection operations.", }, ``` @@ -161,13 +169,17 @@ under its own model. Profiles must agree across a checked dependency closure, in across nested `lemmascript.json` files; a mismatch is an error naming both files, and auto-extern must not invent a bridge. -`resolveOptions` gains no rule: with one key there is no cross-option constraint (the -`config.ts` comment reserving "UTF-16 → local Dafny library" is retired). The emitter derives -the helper source from the profile — `Std.Collections.Seq` under `unicode-scalar`, the local -`SeqFilter`/`SeqAll`/`SeqFoldLeft` under `javascript-utf16` — because the user never chooses -the library. `dafnyVerify`'s text detection of `Std.` is unchanged; a `javascript-utf16` +`dafny-library` independently selects `Std.Collections.Seq` helpers (`stdlib`, the default) +or generated `SeqFilter`/`SeqAll`/`SeqFoldLeft` helpers (`local`). Unicode-scalar strings +support either choice. `resolveOptions` rejects UTF-16 with an omitted or explicit `stdlib` +choice and asks for `"dafny-library": "local"`; it never changes the library silently. +Both options are project settings, with no file override. +`dafnyVerify`'s text detection of `Std.` is unchanged; a `javascript-utf16` artifact whose proof additions import `Std.*` is refused by #211's fail-closed check with a -message naming `string-semantics`. `lsc config` reports the resolved value. +message naming `string-semantics`. `lsc config` reports both resolved values. +The library choice is embodied in the generated helper definitions/calls, so it needs no +extra verifier flag or artifact token. Handwritten imports remain subject to the artifact's +character mode, independently of which collection helpers were generated. Selecting `javascript-utf16` with `--backend=lean` is an error. Lean's `String` is a sequence of `Char` (Unicode scalars) and [`LemmaScript/JSString.lean`](LemmaScript/JSString.lean) @@ -255,8 +267,8 @@ One PR per rung, stacked, each landing only with its evidence. **Rung 0 — name the profile, make it configuration, pin the default.** No semantic change, no artifact change. -- `string-semantics` registry entry; `lsc config` row. No `dafny-lib` key (open decision 3): - the emitter derives helper source from the profile. +- `string-semantics` and `dafny-library` registry entries; `lsc config` reports both. + The emitter selects collection helpers from the library choice, not the string profile. - `dafnyVerify` parses the `lsc options:` line; pins `--unicode-char:true` whenever no `string-semantics=` token is present (a header-less `.dfy` gets the pin and no warning — DESIGN_CONFIG.md open question 3); rejects a token naming an unknown or unimplemented value. @@ -293,7 +305,8 @@ in every `dafnyVerify` invocation that lacks the token; a `.dfy` carrying - Preambles that mention chars vary with the mode (`IsJSWhitespace` must use `\u` escapes under `unicode-char:false` and `\U{}` otherwise; Dafny rejects the other form). `PREAMBLE_CODE` entries become `string | (options) => string`. -- `SeqFilter` / `SeqAll` / `SeqFoldLeft` local helpers emitted whenever the profile is `javascript-utf16`. +- `SeqFilter` / `SeqAll` / `SeqFoldLeft` helpers emitted under `dafny-library: "local"`, + which UTF-16 requires explicitly and Unicode-scalar projects may also select. - `--unicode-char:false --allow-deprecation`; never `--allow-warnings`. - Lean: hard error. @@ -335,20 +348,18 @@ Differential tests support the model; they do not replace the Dafny proofs. ## 9. Open decisions 1. *Resolved.* The `lsc options:` line appears only when the file uses `string` and the - profile is non-default — DESIGN_CONFIG.md §"Future options" decided this ("the header - marker would only be emitted when strings actually appear"), #211's emission-tied flag is - the mechanism, and the always-on cost is measured in §7. There is no separate + profile is non-default. The emitter tracks string usage while generating declarations; + the always-on cost is measured in §7. There is no separate `String model:` line. 2. Should `unicode-scalar` refuse `.length`, indexing, and `charCodeAt` on literals that contain astral text (where the answer is knowably wrong), rather than stating the difference in the profile's claim sentence (SPEC_DAFNY.md §4)? Refusal is safer; the documented claim is what today's proofs already rely on. Rung 0 keeps the claim; rung 1 may add the refusal as a warning. -3. *Resolved.* `dafny-lib` is not a user-facing key: the profile determines helper source - (§4), `Std.` detection stays text-based, and nobody asked for `local-lib` under - `unicode-scalar`. Byte-for-byte default output is preserved. If the local helpers ever - become the only library under both profiles, that is an emitter change plus a regen, with - no registry entry to remove. +3. *Resolved.* `dafny-library: "stdlib" | "local"` is an independent project setting, + defaulting to `stdlib`. UTF-16 requires an explicit `local` choice; Unicode-scalar + projects can use either. Default output is preserved, and `Std.` detection stays + artifact-based (§4). 4. Should the identity suffix be part of the public value (`javascript-utf16-1` in `lemmascript.json`) or internal, as DESIGN_NUMBERS proposes? This design keeps it internal. diff --git a/SPEC.md b/SPEC.md index 8fa50166..d069a048 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1386,13 +1386,17 @@ it; absent means current behavior. Unknown keys and bad values are errors. | `safe-slice` | boolean | `false` | yes | | `proof-dir` | relative path | source directory | no (Dafny only) | | `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | no (Dafny only) | +| `dafny-library` | `stdlib` \| `local` | `stdlib` | no (Dafny only) | Eligible settings use `//@ option ` before the first source statement. File values override project values; duplicates are errors. `proof-dir` mirrors the source's config-relative path under its configured root (see SPEC_DAFNY.md §1). `string-semantics` selects which model of JavaScript strings a Dafny proof is made under (SPEC_DAFNY.md §4); it is config-only because the model changes -every string signature across the dependency closure. `lsc config foo.ts` prints the config path, effective +every string signature across the dependency closure. `dafny-library` selects standard-library +or generated local helpers for `filter`, `every`, and `reduce`. UTF-16 requires an explicit +`"dafny-library": "local"`; omitting it keeps the `stdlib` default and reports an incompatibility. +Unicode-scalar strings support either library choice. `lsc config foo.ts` prints the config path, effective options, and resolved Dafny artifact directory; `lsc config` reports defaults from the current directory. `backend` is deliberately not a config option. diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index 89f9349a..50f77a43 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -117,12 +117,19 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at | `StringTrim` | `s.trim()` / `s.trimEnd()` / `s.trimStart()` | Trim (also provides `StringTrimRight` / `StringTrimLeft`); strips the full ECMAScript whitespace set via `IsJSWhitespace`, not just `' '` | | `StringToLower` / `StringToUpper` | `s.toLowerCase()` / `s.toUpperCase()` | Case folding | -**String profile.** `string-semantics` in `lemmascript.json` (SPEC.md §7.6) selects which model of JavaScript strings a proof is made under; each is a named identity the proof's claims are relative to (DESIGN_STRINGS.md): +**String profile.** `string-semantics` in `lemmascript.json` (SPEC.md §7.6) selects which model of JavaScript strings a proof is made under; each is a named identity the proof's claims are relative to: | Identity | `lemmascript.json` | Claim | |---|---|---| | `unicode-scalar-1` | `"unicode-scalar"` (default) | Dafny `string` under `--unicode-char:true`: strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` are over scalars and differ from JavaScript for astral text; unpaired surrogates are outside the domain (refused in literals; `String.fromCharCode` requires a scalar); case mapping is ASCII-only. No header token. | -| `javascript-utf16-1` | `"javascript-utf16"` | Dafny `string` under `--unicode-char:false`: strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, `charCodeAt`, and `String.fromCharCode` (`0 <= n < 0x10000`) are exact; `filter`/`every`/`reduce` use local `SeqFilter`/`SeqAll`/`SeqFoldLeft` helpers because the Dafny standard library cannot load in this mode; case mapping is ASCII-only. Generated files carry `// lsc options: string-semantics=javascript-utf16`. | +| `javascript-utf16-1` | `"javascript-utf16"` | Dafny `string` under `--unicode-char:false`: strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, `charCodeAt`, and `String.fromCharCode` (`0 <= n < 0x10000`) are exact; requires `"dafny-library": "local"` because the Dafny standard library cannot load in this mode; case mapping is ASCII-only. Generated string-bearing files carry `// lsc options: string-semantics=javascript-utf16`. | + +**Collection helpers.** `dafny-library` independently selects `stdlib` (default) or `local` +for `filter`, `every`, and `reduce`: `Std.Collections.Seq.Filter/All/FoldLeft` or generated +`SeqFilter`/`SeqAll`/`SeqFoldLeft`. Unicode-scalar strings support both choices. UTF-16 with +an omitted or explicit `stdlib` choice is a configuration error; select `local` explicitly. +This option controls generated helpers, not handwritten proof imports; those remain subject +to the character-mode compatibility check below. Selecting `local` does not change string semantics. --- @@ -148,4 +155,3 @@ a `javascript-utf16` proof whose additions import `Std.*` fails closed with an error naming `string-semantics`; a `unicode-scalar` proof may use it freely. The shared `--time-limit=` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=` is forwarded verbatim to `dafny verify`. - diff --git a/TOOLS.md b/TOOLS.md index c6049ee1..683cd08f 100644 --- a/TOOLS.md +++ b/TOOLS.md @@ -63,9 +63,12 @@ cross-option checks. `lsc.ts` merges explicit project values with eligible top-of-file overrides and resolves once per source file. It passes the result to extraction/emission; those phases never read config files. `string-semantics` is consumed by the Dafny emitter (literal escaping, char-sensitive -preambles, helper source, and the `// lsc options:` header token) and by extraction +preambles, and the `// lsc options:` header token) and by extraction (surrogate literals under the default); `dafnyVerify` derives the char-mode flags from -that token, never from the config. `proof-dir` is +that token, never from the config. `dafny-library` selects standard-library or local +collection helpers. `resolveOptions` rejects UTF-16 with the default or explicit `stdlib` +choice; callers must select `local`. `emitDafnyFile` also applies this shared check to +programmatically supplied options. `proof-dir` is consumed only by `lsc.ts`, which maps the complete Dafny companion set before calling the unchanged Dafny command helpers. `TransformOptions` remains backend-intrinsic pipeline configuration and is deliberately separate. diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md index 3b7df589..1971dbd7 100644 --- a/site/src/content/docs/reference/cli.md +++ b/site/src/content/docs/reference/cli.md @@ -95,11 +95,16 @@ at the current directory. Use `--config=` to pin a particular file. { "extern-default": "impure", "string-semantics": "unicode-scalar", + "dafny-library": "stdlib", "safe-slice": true, "proof-dir": "proofs" } ``` +`dafny-library` selects `stdlib` (default) or generated `local` helpers for collection +operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitly setting +`"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error. + ### `lsc claimcheck` Forwards to the bundled `lemmascript-claimcheck` CLI, which cross-examines the diff --git a/tools/fixtures/collection-library-project/collections.ts b/tools/fixtures/collection-library-project/collections.ts new file mode 100644 index 00000000..2a5cd409 --- /dev/null +++ b/tools/fixtures/collection-library-project/collections.ts @@ -0,0 +1,37 @@ +//@ backend dafny + +export function positiveNumbers(): number[] { + //@ verify + //@ ensures \result.length === 2 && \result[0] === 1 && \result[1] === 2 + return [-1, 1, 2].filter(value => value > 0); +} + +export function everyNumberIsPositive(): boolean { + //@ verify + //@ ensures \result === true + return [1, 2, 3].every(value => value > 0); +} + +export function sumNumbers(): number { + //@ verify + //@ ensures \result === 6 + return [1, 2, 3].reduce((total, value) => total + value, 0); +} + +export function nonemptyStrings(): string[] { + //@ verify + //@ ensures \result.length === 2 && \result[0] === "a" && \result[1] === "bc" + return ["a", "", "bc"].filter(value => value.length > 0); +} + +export function everyStringIsNonempty(): boolean { + //@ verify + //@ ensures \result === true + return ["a", "bc"].every(value => value.length > 0); +} + +export function sumStringLengths(): number { + //@ verify + //@ ensures \result === 3 + return ["a", "bc"].reduce((total, value) => total + value.length, 0); +} diff --git a/tools/fixtures/collection-library-project/lemmascript.json b/tools/fixtures/collection-library-project/lemmascript.json new file mode 100644 index 00000000..7ec71b58 --- /dev/null +++ b/tools/fixtures/collection-library-project/lemmascript.json @@ -0,0 +1,3 @@ +{ + "dafny-library": "local" +} diff --git a/tools/fixtures/config-incompatible-strings/lemmascript.json b/tools/fixtures/config-incompatible-strings/lemmascript.json new file mode 100644 index 00000000..6211b2ae --- /dev/null +++ b/tools/fixtures/config-incompatible-strings/lemmascript.json @@ -0,0 +1,3 @@ +{ + "string-semantics": "javascript-utf16" +} diff --git a/tools/fixtures/config-incompatible-strings/source.ts b/tools/fixtures/config-incompatible-strings/source.ts new file mode 100644 index 00000000..c7fa5836 --- /dev/null +++ b/tools/fixtures/config-incompatible-strings/source.ts @@ -0,0 +1,7 @@ +//@ backend dafny + +export function answer(): number { + //@ verify + //@ ensures \result === 42 + return 42; +} diff --git a/tools/fixtures/config-incompatible-strings/stdlib.json b/tools/fixtures/config-incompatible-strings/stdlib.json new file mode 100644 index 00000000..04218445 --- /dev/null +++ b/tools/fixtures/config-incompatible-strings/stdlib.json @@ -0,0 +1,4 @@ +{ + "string-semantics": "javascript-utf16", + "dafny-library": "stdlib" +} diff --git a/tools/fixtures/utf16-project/lemmascript.json b/tools/fixtures/utf16-project/lemmascript.json index 6211b2ae..5fde7fcc 100644 --- a/tools/fixtures/utf16-project/lemmascript.json +++ b/tools/fixtures/utf16-project/lemmascript.json @@ -1,3 +1,4 @@ { - "string-semantics": "javascript-utf16" + "string-semantics": "javascript-utf16", + "dafny-library": "local" } diff --git a/tools/src/config.ts b/tools/src/config.ts index 52d6d6cd..b2955be1 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -38,6 +38,13 @@ export const OPTION_SPECS = { fileOverride: false, description: "Which model of JavaScript strings a Dafny proof is made under.", }, + "dafny-library": { + type: "enum", + values: ["stdlib", "local"], + default: "stdlib", + fileOverride: false, + description: "Use Dafny's standard library or generated local helpers for collection operations.", + }, } as const; type OptionSpecs = typeof OPTION_SPECS; @@ -214,12 +221,14 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp return out as ExplicitOptions; } -/** Fill missing options with defaults and freeze the resolved configuration. */ +/** Apply defaults, check option compatibility, and freeze the resolved configuration. */ export function resolveOptions(explicit: ExplicitOptions, source: string): LscOptions { - // Each option is independent: selecting a value for one option does not - // change another option's default or make its value invalid. - void source; - return Object.freeze({ ...DEFAULT_OPTIONS, ...explicit }); + const options = { ...DEFAULT_OPTIONS, ...explicit }; + // Dafny's precompiled standard library uses Unicode-scalar characters. + if (options["string-semantics"] === "javascript-utf16" && options["dafny-library"] === "stdlib") { + fail(source, '"string-semantics": "javascript-utf16" is incompatible with "dafny-library": "stdlib"; set "dafny-library": "local" explicitly'); + } + return Object.freeze(options); } /** Find `fileName` at or above `fromPath`. */ diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 25b472ab..d1756864 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -7,7 +7,7 @@ import { exactIntegerLiteral, usesName, usesNameInDecl, usesNameInStmts } from " import type { Ty } from "./typedir.js"; import { freshName, freshNameWhere, userNames } from "./names.js"; import { renameFreeVar } from "./transform.js"; -import { DEFAULT_OPTIONS, type LscOptions } from "./config.js"; +import { DEFAULT_OPTIONS, resolveOptions, type LscOptions } from "./config.js"; /** Fresh binder for a comprehension wrapping the given subexpressions: `base` * verbatim unless one of them references it, then primed until free. A *local* @@ -377,14 +377,14 @@ function emitExpr(e: Expr): string { return bind ? `(var ${s} := ${obj}; ${comp})` : comp; } if (e.method === "filter") { - if (!isUtf16()) return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`; + if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`; needPreamble("SeqFilter"); return `SeqFilter(${args[0]}, ${obj})`; } // filterMap (synthesized in resolve): drop Nones and unwrap to seq. if (e.method === "filterSome") { needPreamble("SeqFilterSome"); needPreamble("OptionType"); return `SeqFilterSome(${obj})`; } if (e.method === "every") { - if (!isUtf16()) return `Std.Collections.Seq.All(${obj}, ${args[0]})`; + if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.All(${obj}, ${args[0]})`; needPreamble("SeqAll"); return `SeqAll(${obj}, ${args[0]})`; } @@ -429,11 +429,9 @@ function emitExpr(e: Expr): string { } return `(exists ${p} :: ${p} in ${obj} && ${body})`; } - // `.reduce(f, init)` → FoldLeft(f, init, xs) (same arg order): Std's under - // unicode-scalar, the local helper under javascript-utf16, whose char mode - // cannot load the precompiled standard library. + // `.reduce(f, init)` → FoldLeft(f, init, xs), using the selected library. if (e.method === "reduce" && args.length === 2) { - if (!isUtf16()) return `Std.Collections.Seq.FoldLeft(${args[0]}, ${args[1]}, ${obj})`; + if (_dafnyLibrary === "stdlib") return `Std.Collections.Seq.FoldLeft(${args[0]}, ${args[1]}, ${obj})`; needPreamble("SeqFoldLeft"); return `SeqFoldLeft(${args[0]}, ${args[1]}, ${obj})`; } @@ -996,6 +994,9 @@ function needPreamble(key: string) { _neededPreambles.add(key); } * config plus file directives before emission. */ let _useSafeSlice = false; +// Source of generated collection helpers, selected independently of string semantics. +let _dafnyLibrary: LscOptions["dafny-library"] = DEFAULT_OPTIONS["dafny-library"]; + // The string profile this file is emitted under (DESIGN_STRINGS.md) and whether // any generated declaration used `string`. Together they decide the // `// lsc options:` header token that `dafnyVerify` maps to Dafny's char mode. @@ -1621,8 +1622,11 @@ function translatePattern(p: MatchPattern): string { export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOptions = DEFAULT_OPTIONS): string { + // Programmatic callers share the CLI's compatibility checks. + options = resolveOptions(options, tsFileName ?? "Dafny emission"); _useSafeSlice = options["safe-slice"]; _stringSemantics = options["string-semantics"]; + _dafnyLibrary = options["dafny-library"]; // Reset before scanning types, including when the previous file failed to emit. _usesStrings = false; resetDafnyNameCache(); diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 0de80f53..a35130dc 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -850,7 +850,7 @@ function stringLiteral(value: string, node: Node): RawExpr { throw new Error( `${file.getFilePath()}:${line}: string literal contains an unpaired surrogate ` + `U+${lone.toString(16).toUpperCase()}, which "string-semantics": "unicode-scalar" cannot ` + - `represent; set "javascript-utf16" in lemmascript.json (DESIGN_STRINGS.md §3)`, + `represent; set "string-semantics": "javascript-utf16" and "dafny-library": "local" in lemmascript.json`, ); } } diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index b3801d52..9fe99fc5 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -175,7 +175,7 @@ expect_failure \ npx tsx tools/src/lsc.ts gen --backend=dafny "$config_fixture/src/legacy.ts" expect_absent "$config_fixture/proofs/src/legacy.dfy" -# ── String profile (DESIGN_STRINGS.md) ────────────────────────────────────── +# ── String profile and collection library ───────────────────────────────── # Under "string-semantics": "javascript-utf16" a JavaScript string is a UTF-16 # code-unit sequence: astral characters occupy two Dafny chars and lone # surrogates stay representable. The header token is what dafnyVerify maps to @@ -186,6 +186,10 @@ if ! npx tsx tools/src/lsc.ts config "$utf16" | grep -Fq '"string-semantics": "j echo "ERROR: lsc config did not report string-semantics=javascript-utf16" exit 1 fi +if ! npx tsx tools/src/lsc.ts config "$utf16" | grep -Fq '"dafny-library": "local"'; then + echo "ERROR: lsc config did not report the explicit local library choice" + exit 1 +fi npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$utf16" grep -Fq '// lsc options: string-semantics=javascript-utf16' "$utf16_gen" grep -Fq '"\uD83D\uDE00"' "$utf16_gen" @@ -195,6 +199,59 @@ if grep -Fq 'Std.Collections' "$utf16_gen"; then exit 1 fi +# The library has a fixed stdlib default; UTF-16 never silently changes it. +cp -R tools/fixtures/config-incompatible-strings "$fixture_dir/incompatible-strings" +incompatible="$fixture_dir/incompatible-strings/source.ts" +expect_failure "UTF-16 silently changed the default library" \ + npx tsx tools/src/lsc.ts gen --backend=dafny "$incompatible" +expect_failure "UTF-16 accepted an explicit stdlib choice" \ + npx tsx tools/src/lsc.ts gen --backend=dafny \ + --config="$fixture_dir/incompatible-strings/stdlib.json" "$incompatible" +expect_absent "$fixture_dir/incompatible-strings/source.dfy.gen" +expect_absent "$fixture_dir/incompatible-strings/source.dfy" + +# Prove the same collection contracts with default stdlib, scalar/local, and +# UTF-16/local. All generated artifacts stay in the temporary fixture directory. +cp -R tools/fixtures/collection-library-project "$fixture_dir/local-collections" +cp tools/fixtures/collection-library-project/collections.ts "$fixture_dir/standard-collections.ts" +cp tools/fixtures/collection-library-project/collections.ts "$fixture_dir/utf16-project/collections.ts" +npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/standard-collections.ts" +# Standard Filter is opaque. Add proof steps that expose its definition and +# unfold the three input elements plus the empty tail; check enforces additions-only. +node --input-type=module - "$fixture_dir/standard-collections.dfy" <<'JS' +import { readFileSync, writeFileSync } from "node:fs"; +const path = process.argv[2]; +let proof = readFileSync(path, "utf8"); +for (const [name, type, expected] of [ + ["positiveNumbers", "int", "[1, 2]"], + ["nonemptyStrings", "string", '["a", "bc"]'], +]) { + const start = new RegExp(`lemma ${name}_ensures\\(\\)[\\s\\S]*?\\{\\n`); + if (!start.test(proof)) throw new Error(`Missing proof body for ${name}`); + proof = proof.replace(start, "$& reveal Std.Collections.Seq.Filter();\n" + + ` assert {:fuel Std.Collections.Seq.Filter<${type}>, 4, 5} ${name}() == ${expected};\n`); +} +writeFileSync(path, proof); +JS +npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/standard-collections.ts" +for helper in Filter All FoldLeft; do + grep -Fq "Std.Collections.Seq.$helper(" "$fixture_dir/standard-collections.dfy.gen" +done +for source in "$fixture_dir/local-collections/collections.ts" "$fixture_dir/utf16-project/collections.ts"; do + npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$source" + generated="${source%.ts}.dfy.gen" + if grep -Fq 'Std.' "$generated"; then + echo "ERROR: dafny-library=local emitted a standard-library reference" + exit 1 + fi + for helper in SeqFilter SeqAll SeqFoldLeft; do grep -Fq "$helper<" "$generated"; done +done +if grep -Fq '// lsc options:' "$fixture_dir/local-collections/collections.dfy.gen"; then + echo "ERROR: selecting local helpers changed scalar string semantics" + exit 1 +fi +grep -Fq '// lsc options: string-semantics=javascript-utf16' "$fixture_dir/utf16-project/collections.dfy.gen" + expect_failure \ "Dafny standard library was combined with javascript-utf16 strings" \ npx tsx -e 'import { dafnyVerify } from "./tools/src/dafny-commands.ts"; process.exit(dafnyVerify("tools/fixtures/string-with-standard-library.dfy", ".") ? 0 : 1)' diff --git a/tools/tests/config.test.ts b/tools/tests/config.test.ts index cc6a5643..daef150a 100644 --- a/tools/tests/config.test.ts +++ b/tools/tests/config.test.ts @@ -145,7 +145,7 @@ for (const [directive, message] of [ ["option", "expected //@ option "], ["option safe-slice", "expected //@ option "], ["option safe-slice true extra", "expected //@ option "], - ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir, string-semantics)"], + ["option missing true", "unknown option 'missing' (known options: extern-default, safe-slice, proof-dir, string-semantics, dafny-library)"], ["option safe-slice yes", "option 'safe-slice' must be true or false"], ["option extern-default invalid", "option 'extern-default' must be one of: pure, impure"], ["option proof-dir proofs", "option 'proof-dir' is config-only"], @@ -189,3 +189,33 @@ test("string-semantics is config-only: a file cannot reinterpret a callee's stri /config-only/, ); }); + +test("Dafny library defaults to stdlib and local works with scalar strings", () => { + assert.equal(resolveOptions({}, "lemmascript.json")["dafny-library"], "stdlib"); + const options = resolveOptions(validateOptions({ "dafny-library": "local" }, "lemmascript.json"), "lemmascript.json"); + assert.equal(options["dafny-library"], "local"); + assert.equal(options["string-semantics"], "unicode-scalar"); + assert.ok(Object.isFrozen(options)); +}); + +for (const library of [undefined, "stdlib"] as const) { + test(`UTF-16 rejects ${library === undefined ? "the default" : "explicit"} stdlib choice`, () => { + const explicit = library === undefined + ? { "string-semantics": "javascript-utf16" } + : { "string-semantics": "javascript-utf16", "dafny-library": library }; + assert.throws(() => resolveOptions(validateOptions(explicit, "lemmascript.json"), "lemmascript.json"), + /lemmascript\.json:.*"string-semantics": "javascript-utf16".*"dafny-library": "stdlib".*"local" explicitly/); + }); +} + +test("UTF-16 requires an explicit local library choice", () => { + const explicit = validateOptions({ "string-semantics": "javascript-utf16", "dafny-library": "local" }, "lemmascript.json"); + assert.equal(resolveOptions(explicit, "lemmascript.json")["dafny-library"], "local"); +}); + +test("Dafny library accepts only registered values and is config-only", () => { + for (const value of [true, "standard", null]) { + assert.throws(() => validateOptions({ "dafny-library": value }, "lemmascript.json"), /must be one of: stdlib, local/); + } + assert.throws(() => parseFileOptions("//@ option dafny-library local\n", "example.ts"), /config-only/); +}); diff --git a/tools/tests/dafny-emit.test.ts b/tools/tests/dafny-emit.test.ts index f227e3a7..b75ef143 100644 --- a/tools/tests/dafny-emit.test.ts +++ b/tools/tests/dafny-emit.test.ts @@ -1,10 +1,10 @@ import { test } from "node:test"; import assert from "node:assert/strict"; -import { DEFAULT_OPTIONS, type LscOptions } from "../src/config.ts"; +import { DEFAULT_OPTIONS, resolveOptions } from "../src/config.ts"; import { emitDafnyFile } from "../src/dafny-emit.ts"; -import type { Decl, Module } from "../src/ir.ts"; +import type { Decl, Expr, Module } from "../src/ir.ts"; -const utf16: LscOptions = { ...DEFAULT_OPTIONS, "string-semantics": "javascript-utf16" }; +const utf16 = resolveOptions({ "string-semantics": "javascript-utf16", "dafny-library": "local" }, "test"); const optionsHeader = /^\/\/ lsc options: string-semantics=javascript-utf16$/m; function moduleWith(...decls: Decl[]): Module { @@ -14,6 +14,35 @@ function moduleWith(...decls: Decl[]): Module { const numbers = moduleWith({ kind: "const", name: "answer", type: { kind: "int" }, value: { kind: "num", value: 42 } }); const stringType: Decl = { kind: "type-alias", name: "Text", target: { kind: "string" } }; +test("programmatic emission rejects UTF-16 with the default standard library", () => { + assert.throws(() => emitDafnyFile(numbers, "numbers.ts", { ...DEFAULT_OPTIONS, "string-semantics": "javascript-utf16" }), + /numbers\.ts:.*javascript-utf16.*dafny-library.*stdlib.*local/); +}); + +for (const [method, helper, resultType] of [ + ["filter", "Filter", { kind: "array", elem: { kind: "int" } }], + ["every", "All", { kind: "bool" }], + ["reduce", "FoldLeft", { kind: "int" }], +] as const) { + test(`${method} follows the library option independently of string semantics`, () => { + const callback: Expr = { kind: "var", name: "callback" }; + const file = moduleWith({ kind: "const", name: "value", type: resultType, value: { + kind: "methodCall", obj: { kind: "var", name: "values" }, objTy: { kind: "array", elem: { kind: "int" } }, + method, args: method === "reduce" ? [callback, { kind: "num", value: 0 }] : [callback], monadic: false, + } }); + const standard = emitDafnyFile(file, "collections.ts"); + assert.ok(standard.includes(`Std.Collections.Seq.${helper}(`)); + for (const options of [resolveOptions({ "dafny-library": "local" }, "test"), utf16]) { + const local = emitDafnyFile(file, "collections.ts", options); + assert.doesNotMatch(local, /Std\./); + assert.match(local, new RegExp(`(?:function|predicate) Seq${helper}<`)); + } + // A local emission must not change the next file's default library. + assert.equal(emitDafnyFile(file, "collections.ts"), standard); + assert.equal(emitDafnyFile(file, "collections.ts", resolveOptions({ "dafny-library": "stdlib" }, "test")), standard); + }); +} + for (const [name, declaration] of [ ["string type without literals", stringType], ["nested string type", { kind: "type-alias", name: "Texts", target: { From f5cff1efba54530b3f86426d714e2e6aa43bfe1a Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Sun, 27 Sep 2026 19:45:58 -0700 Subject: [PATCH 07/15] feat: support per-file string model options with a verified example Allow string-semantics and dafny-library directives before source statements. Validate merged settings and require matching string models across TypeScript-resolved source dependencies and compiler-selected cross-file callees. Add examples/utf16.ts and its Dafny proof, cover option precedence and dependency boundaries, and update docs and diagnostics. Existing generated example artifacts remain unchanged. --- DESIGN_CONFIG.md | 18 ++- DESIGN_STRINGS.md | 23 ++-- SPEC.md | 21 +++- SPEC_DAFNY.md | 5 +- TOOLS.md | 9 +- examples/utf16.dfy | 38 ++++++ examples/utf16.dfy.gen | 38 ++++++ examples/utf16.ts | 24 ++++ site/src/content/docs/reference/cli.md | 11 ++ tools/src/config.ts | 4 +- tools/src/dafny-commands.ts | 2 +- tools/src/extract.ts | 10 +- tools/src/lsc.ts | 34 +++++- tools/test-fixtures.sh | 5 + tools/tests/config.test.ts | 25 ++-- tools/tests/file-options.test.ts | 162 +++++++++++++++++++++++++ 16 files changed, 391 insertions(+), 38 deletions(-) create mode 100644 examples/utf16.dfy create mode 100644 examples/utf16.dfy.gen create mode 100644 examples/utf16.ts create mode 100644 tools/tests/file-options.test.ts diff --git a/DESIGN_CONFIG.md b/DESIGN_CONFIG.md index 20aaff38..65704ae8 100644 --- a/DESIGN_CONFIG.md +++ b/DESIGN_CONFIG.md @@ -50,8 +50,8 @@ export const OPTION_SPECS = { "extern-default": { type: "enum", values: ["pure", "impure"], default: "pure", fileOverride: true, description: "…" }, "safe-slice": { type: "boolean", default: false, fileOverride: true, directiveAliases: ["safe-slice"], description: "…" }, "proof-dir": { type: "path", default: null, fileOverride: false, description: "…" }, - "string-semantics": { type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: false, description: "…" }, - "dafny-library": { type: "enum", values: ["stdlib", "local"], default: "stdlib", fileOverride: false, description: "…" }, + "string-semantics": { type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", fileOverride: true, description: "…" }, + "dafny-library": { type: "enum", values: ["stdlib", "local"], default: "stdlib", fileOverride: true, description: "…" }, } as const; export type LscOptions = { readonly [K in keyof typeof OPTION_SPECS]: /* boolean | enum union | string | null */ }; @@ -108,7 +108,17 @@ Enabling the option must not silently strand proof additions. If the mapped `.df `string-semantics: "unicode-scalar" | "javascript-utf16"` chooses the string model, defaulting to `unicode-scalar`. `dafny-library: "stdlib" | "local"` independently chooses -the generated collection helpers, defaulting to `stdlib`. Both are config-only. +the generated collection helpers, defaulting to `stdlib`. Both accept top-of-file +`//@ option` directives, which override project settings before compatibility is checked. +The ordinary [UTF-16 example](examples/utf16.ts) needs no JSON config. + +The CLI follows TypeScript-resolved source dependencies and checks their effective string +models against the root file before emission. It also checks compiler-selected cross-file +callees before extraction copies their contracts, including global declarations without +an import edge. Cycles are visited once; unrelated tsconfig files are not dependencies. +Declaration files carry no model, but their re-exports are followed. `--config` pins the +project settings for dependencies too; file directives still apply separately. Different +collection-library choices are allowed because they do not reinterpret contracts. `stdlib` emits `Std.Collections.Seq.Filter/All/FoldLeft` for `filter`/`every`/`reduce`; `local` emits `SeqFilter`/`SeqAll`/`SeqFoldLeft` definitions on demand. Unicode-scalar @@ -164,7 +174,7 @@ Without a string-model token, verification explicitly uses `--unicode-char:true` ## 7. Docs and tests - **SPEC.md §2 and §7**: add `option` to the file-level directive table; add `config` to the command list, `--config=` to flags, and new §7.6 "Project configuration: `lemmascript.json`" with the table from §3 (~15 lines, per AGENTS.md style). §2.7 describes `safe-slice` as both an option and a legacy directive; §2.9/§2.11 extern prose becomes conditional on `extern-default`. **SPEC_DAFNY.md**: document `proof-dir`, its mirrored layout, and proof migration. **SPEC_LEAN.md**: one line on impure externs. **TOOLS.md**: `config.ts` in the file table plus a short "Options" section on the flow in §4. **AGENTS.md**: one line under Toolchain commands pointing at `lsc config`; its regen rules apply to mapped paths unchanged. **site `reference/cli.md`**: directive, flag, and command rows plus a "Project configuration" section (hand-written page; `DESIGN_CONFIG.md` itself joins `sync-docs.mjs` like the other design docs). -- **`tools/test-fixtures.sh`** keeps a small fixture directory with `lemmascript.json` and a nested source file to exercise nearest-ancestor discovery, plus invalid config fixtures for an unknown key and a bad value. It verifies that `proof-dir` mirrors the nested path, creates `.dfy.gen` and `.dfy` there rather than beside the TS, and refuses to bypass a pre-existing sibling proof. Self-contained source fixtures use `//@ option` to exercise `extern-default`, `safe-slice: false`, a config-only `proof-dir` directive error, bad and duplicate directives, and precedence over the project config. A `lsc config` invocation is grepped for the effective post-directive values and resolved artifact directory. Existing fixtures run without a config and pin the defaults. UTF-16 and JavaScript-number fixtures are deferred with those options. +- **`tools/test-fixtures.sh`** keeps a small fixture directory with `lemmascript.json` and a nested source file to exercise nearest-ancestor discovery, plus invalid config fixtures for an unknown key and a bad value. It verifies that `proof-dir` mirrors the nested path, creates `.dfy.gen` and `.dfy` there rather than beside the TS, and refuses to bypass a pre-existing sibling proof. Self-contained source fixtures use `//@ option` to exercise `extern-default`, `safe-slice: false`, a config-only `proof-dir` directive error, bad and duplicate directives, and precedence over the project config. A `lsc config` invocation is grepped for the effective post-directive values and resolved artifact directory. Existing fixtures run without a config and pin the defaults. UTF-16 is exercised through both project config and the ordinary file-directive example; unit tests cover dependency compatibility. JavaScript-number fixtures remain deferred. - **CI** is otherwise untouched: examples and case studies verify under today's pure-extern default; #211 and #205 are outside the initial scope. ## 8. Initial scope and future PRs diff --git a/DESIGN_STRINGS.md b/DESIGN_STRINGS.md index ad6795db..941efe88 100644 --- a/DESIGN_STRINGS.md +++ b/DESIGN_STRINGS.md @@ -25,7 +25,8 @@ shape [DESIGN_NUMBERS.md](DESIGN_NUMBERS.md) chose for `number-semantics`: `unicode-scalar` stays the default so no `lemmascript.json` means today's behaviour ([DESIGN_CONFIG.md](DESIGN_CONFIG.md) requirement 3). A project opts into `javascript-utf16` -by setting `"string-semantics": "javascript-utf16"` and `"dafny-library": "local"` explicitly. +by setting `"string-semantics": "javascript-utf16"` and `"dafny-library": "local"` explicitly, +either in project config or through file-level `//@ option` directives. A `javascript-utf16` proof carries `// lsc options: string-semantics=javascript-utf16` in its header ([DESIGN_CONFIG.md](DESIGN_CONFIG.md) §5 form); the default's header is unchanged, so no existing artifact changes. Each identity's claim sentence lives in @@ -150,30 +151,30 @@ Two registry entries in [`tools/src/config.ts`](tools/src/config.ts), following type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", - fileOverride: false, + fileOverride: true, description: "Which model of JavaScript strings a Dafny proof is made under.", }, "dafny-library": { type: "enum", values: ["stdlib", "local"], default: "stdlib", - fileOverride: false, + fileOverride: true, description: "Use Dafny's standard library or generated local helpers for collection operations.", }, ``` -`fileOverride: false` for the same reason `number-semantics` is config-only -([DESIGN_NUMBERS.md](DESIGN_NUMBERS.md) §6): the model changes every string signature, so -a per-file `//@ option` would let a caller reinterpret an auto-externed callee's `string` -under its own model. Profiles must agree across a checked dependency closure, including -across nested `lemmascript.json` files; a mismatch is an error naming both files, and -auto-extern must not invent a bridge. +Both settings accept `//@ option` before the first source statement. File values override +project values, and compatibility is checked after merging. The CLI checks the effective +string model across source dependencies, including re-exports, nested config files, and +compiler-selected cross-file callees. A mismatch names both files and stops translation +before contracts can be interpreted under the wrong model. Declaration files carry no +model; their re-exports are followed. Unrelated tsconfig files can use other profiles. `dafny-library` independently selects `Std.Collections.Seq` helpers (`stdlib`, the default) or generated `SeqFilter`/`SeqAll`/`SeqFoldLeft` helpers (`local`). Unicode-scalar strings support either choice. `resolveOptions` rejects UTF-16 with an omitted or explicit `stdlib` choice and asks for `"dafny-library": "local"`; it never changes the library silently. -Both options are project settings, with no file override. +Library choices may differ between dependencies; their string profiles must agree. `dafnyVerify`'s text detection of `Std.` is unchanged; a `javascript-utf16` artifact whose proof additions import `Std.*` is refused by #211's fail-closed check with a message naming `string-semantics`. `lsc config` reports both resolved values. @@ -356,7 +357,7 @@ Differential tests support the model; they do not replace the Dafny proofs. difference in the profile's claim sentence (SPEC_DAFNY.md §4)? Refusal is safer; the documented claim is what today's proofs already rely on. Rung 0 keeps the claim; rung 1 may add the refusal as a warning. -3. *Resolved.* `dafny-library: "stdlib" | "local"` is an independent project setting, +3. *Resolved.* `dafny-library: "stdlib" | "local"` is an independent setting with project defaults and file overrides, defaulting to `stdlib`. UTF-16 requires an explicit `local` choice; Unicode-scalar projects can use either. Default output is preserved, and `Std.` detection stays artifact-based (§4). diff --git a/SPEC.md b/SPEC.md index d069a048..f2898c6b 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1385,21 +1385,34 @@ it; absent means current behavior. Unknown keys and bad values are errors. | `extern-default` | `pure` \| `impure` | `pure` | yes | | `safe-slice` | boolean | `false` | yes | | `proof-dir` | relative path | source directory | no (Dafny only) | -| `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | no (Dafny only) | -| `dafny-library` | `stdlib` \| `local` | `stdlib` | no (Dafny only) | +| `string-semantics` | `unicode-scalar` \| `javascript-utf16` | `unicode-scalar` | yes (Dafny only) | +| `dafny-library` | `stdlib` \| `local` | `stdlib` | yes (Dafny only) | Eligible settings use `//@ option ` before the first source statement. File values override project values; duplicates are errors. `proof-dir` mirrors the source's config-relative path under its configured root (see SPEC_DAFNY.md §1). `string-semantics` selects which model of JavaScript strings a -Dafny proof is made under (SPEC_DAFNY.md §4); it is config-only because the model changes -every string signature across the dependency closure. `dafny-library` selects standard-library +Dafny proof is made under (SPEC_DAFNY.md §4). Source dependencies must use the same +effective string model; mismatches name both files and are rejected before emission. +`dafny-library` selects standard-library or generated local helpers for `filter`, `every`, and `reduce`. UTF-16 requires an explicit `"dafny-library": "local"`; omitting it keeps the `stdlib` default and reports an incompatibility. Unicode-scalar strings support either library choice. `lsc config foo.ts` prints the config path, effective options, and resolved Dafny artifact directory; `lsc config` reports defaults from the current directory. `backend` is deliberately not a config option. +For a standalone file, put both settings before its first statement: + +```typescript +//@ backend dafny +//@ option string-semantics javascript-utf16 +//@ option dafny-library local +``` + +See [examples/utf16.ts](examples/utf16.ts) and its Dafny proof. Compatibility is checked +after project values and file directives are merged. Collection libraries may differ +between files; unlike the string model, they do not change the meaning of contracts. + --- ## 8. Pipeline diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index 50f77a43..5a4ac61f 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -117,9 +117,9 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at | `StringTrim` | `s.trim()` / `s.trimEnd()` / `s.trimStart()` | Trim (also provides `StringTrimRight` / `StringTrimLeft`); strips the full ECMAScript whitespace set via `IsJSWhitespace`, not just `' '` | | `StringToLower` / `StringToUpper` | `s.toLowerCase()` / `s.toUpperCase()` | Case folding | -**String profile.** `string-semantics` in `lemmascript.json` (SPEC.md §7.6) selects which model of JavaScript strings a proof is made under; each is a named identity the proof's claims are relative to: +**String profile.** `string-semantics` in `lemmascript.json` or a file's `//@ option` directive (SPEC.md §7.6) selects which model of JavaScript strings a proof is made under; each is a named identity the proof's claims are relative to: -| Identity | `lemmascript.json` | Claim | +| Identity | Option value | Claim | |---|---|---| | `unicode-scalar-1` | `"unicode-scalar"` (default) | Dafny `string` under `--unicode-char:true`: strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` are over scalars and differ from JavaScript for astral text; unpaired surrogates are outside the domain (refused in literals; `String.fromCharCode` requires a scalar); case mapping is ASCII-only. No header token. | | `javascript-utf16-1` | `"javascript-utf16"` | Dafny `string` under `--unicode-char:false`: strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, `charCodeAt`, and `String.fromCharCode` (`0 <= n < 0x10000`) are exact; requires `"dafny-library": "local"` because the Dafny standard library cannot load in this mode; case mapping is ASCII-only. Generated string-bearing files carry `// lsc options: string-semantics=javascript-utf16`. | @@ -128,6 +128,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at for `filter`, `every`, and `reduce`: `Std.Collections.Seq.Filter/All/FoldLeft` or generated `SeqFilter`/`SeqAll`/`SeqFoldLeft`. Unicode-scalar strings support both choices. UTF-16 with an omitted or explicit `stdlib` choice is a configuration error; select `local` explicitly. +Both settings accept file directives; [examples/utf16.ts](examples/utf16.ts) demonstrates them. This option controls generated helpers, not handwritten proof imports; those remain subject to the character-mode compatibility check below. Selecting `local` does not change string semantics. diff --git a/TOOLS.md b/TOOLS.md index 683cd08f..079bc25e 100644 --- a/TOOLS.md +++ b/TOOLS.md @@ -60,14 +60,19 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = ` `config.ts` owns the `OPTION_SPECS` registry, nearest-ancestor `lemmascript.json` discovery, JSON and `//@ option` validation, defaults, and cross-option checks. `lsc.ts` merges explicit project values with eligible -top-of-file overrides and resolves once per source file. It passes the result +top-of-file overrides and resolves once per source file. It checks that source dependencies +share the root file's string model, following TypeScript-resolved imports/re-exports and +compiler-selected cross-file callees before their contracts are copied. Unrelated files +in the tsconfig are not checked. An explicit `--config` applies to dependencies too; +each file still applies its own directives. It passes the result to extraction/emission; those phases never read config files. `string-semantics` is consumed by the Dafny emitter (literal escaping, char-sensitive preambles, and the `// lsc options:` header token) and by extraction (surrogate literals under the default); `dafnyVerify` derives the char-mode flags from that token, never from the config. `dafny-library` selects standard-library or local collection helpers. `resolveOptions` rejects UTF-16 with the default or explicit `stdlib` -choice; callers must select `local`. `emitDafnyFile` also applies this shared check to +choice; callers must select `local` through config or file directives. Collection-library +choices may differ across dependencies. `emitDafnyFile` also applies this shared check to programmatically supplied options. `proof-dir` is consumed only by `lsc.ts`, which maps the complete Dafny companion set before calling the unchanged Dafny command helpers. `TransformOptions` remains diff --git a/examples/utf16.dfy b/examples/utf16.dfy new file mode 100644 index 00000000..68081a4d --- /dev/null +++ b/examples/utf16.dfy @@ -0,0 +1,38 @@ +// Generated by lsc from utf16.ts +// lsc options: string-semantics=javascript-utf16 + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + +function emojiLength(): int +{ + |"\uD83D\uDE00"| +} + +lemma emojiLength_ensures() + ensures (emojiLength() == 2) +{ +} + +function emojiFirstCodeUnit(): int +{ + ("\uD83D\uDE00"[0..1][0] as int) +} + +lemma emojiFirstCodeUnit_ensures() + ensures (emojiFirstCodeUnit() == 55357) +{ +} + +function allTextIsNonempty(): bool +{ + SeqAll(["\uD83D\uDE00", "text"], (value: string) => (|value| > 0)) +} + +lemma allTextIsNonempty_ensures() + ensures (allTextIsNonempty() == true) +{ +} diff --git a/examples/utf16.dfy.gen b/examples/utf16.dfy.gen new file mode 100644 index 00000000..68081a4d --- /dev/null +++ b/examples/utf16.dfy.gen @@ -0,0 +1,38 @@ +// Generated by lsc from utf16.ts +// lsc options: string-semantics=javascript-utf16 + +predicate SeqAll(xs: seq, p: T -> bool) + decreases |xs| +{ + |xs| == 0 || (p(xs[0]) && SeqAll(xs[1..], p)) +} + +function emojiLength(): int +{ + |"\uD83D\uDE00"| +} + +lemma emojiLength_ensures() + ensures (emojiLength() == 2) +{ +} + +function emojiFirstCodeUnit(): int +{ + ("\uD83D\uDE00"[0..1][0] as int) +} + +lemma emojiFirstCodeUnit_ensures() + ensures (emojiFirstCodeUnit() == 55357) +{ +} + +function allTextIsNonempty(): bool +{ + SeqAll(["\uD83D\uDE00", "text"], (value: string) => (|value| > 0)) +} + +lemma allTextIsNonempty_ensures() + ensures (allTextIsNonempty() == true) +{ +} diff --git a/examples/utf16.ts b/examples/utf16.ts new file mode 100644 index 00000000..85ce0e96 --- /dev/null +++ b/examples/utf16.ts @@ -0,0 +1,24 @@ +//@ backend dafny +//@ option string-semantics javascript-utf16 +//@ option dafny-library local + +// JavaScript counts UTF-16 code units: this emoji occupies two. +export function emojiLength(): number { + //@ verify + //@ ensures \result === 2 + return "😀".length; +} + +// Slicing one code unit may produce an unpaired surrogate. +export function emojiFirstCodeUnit(): number { + //@ verify + //@ ensures \result === 0xD83D + return "😀".slice(0, 1).charCodeAt(0); +} + +// UTF-16 uses local collection helpers rather than Dafny's standard library. +export function allTextIsNonempty(): boolean { + //@ verify + //@ ensures \result === true + return ["😀", "text"].every(value => value.length > 0); +} diff --git a/site/src/content/docs/reference/cli.md b/site/src/content/docs/reference/cli.md index 1971dbd7..a06329d4 100644 --- a/site/src/content/docs/reference/cli.md +++ b/site/src/content/docs/reference/cli.md @@ -105,6 +105,17 @@ at the current directory. Use `--config=` to pin a particular file. operations. Enabling `"string-semantics": "javascript-utf16"` requires explicitly setting `"dafny-library": "local"`; an omitted or explicit `stdlib` choice is an error. +A file can override both project settings before its first statement: + +```typescript +//@ backend dafny +//@ option string-semantics javascript-utf16 +//@ option dafny-library local +``` + +Source dependencies must use the same effective string model. `lsc config file.ts` +shows the settings after file overrides; `lsc check file.ts` also checks dependencies. + ### `lsc claimcheck` Forwards to the bundled `lemmascript-claimcheck` CLI, which cross-examines the diff --git a/tools/src/config.ts b/tools/src/config.ts index b2955be1..0b8b402a 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -35,14 +35,14 @@ export const OPTION_SPECS = { type: "enum", values: ["unicode-scalar", "javascript-utf16"], default: "unicode-scalar", - fileOverride: false, + fileOverride: true, description: "Which model of JavaScript strings a Dafny proof is made under.", }, "dafny-library": { type: "enum", values: ["stdlib", "local"], default: "stdlib", - fileOverride: false, + fileOverride: true, description: "Use Dafny's standard library or generated local helpers for collection operations.", }, } as const; diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index cf868855..177cbe71 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -99,7 +99,7 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? return { args: [], error: "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " + "Dafny 4.11 cannot load its Unicode-scalar standard library under --unicode-char:false. " + - "Remove the Std.* import from the proof additions, or set \"unicode-scalar\" in lemmascript.json." }; + "Remove the Std.* import from the proof additions, or select unicode-scalar in lemmascript.json or a //@ option directive and regenerate." }; } const args: string[] = ["verify"]; if (usesStandardLibrary) args.push("--standard-libraries"); diff --git a/tools/src/extract.ts b/tools/src/extract.ts index a35130dc..bd9e7dc5 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -57,6 +57,8 @@ let _currentSourceFile: SourceFile | null = null; let _inFunctionExtraction = false; /** Effective options for the current extraction. Reset at extractModule entry. */ let _extractOptions: LscOptions = DEFAULT_OPTIONS; +/** The CLI validates source options before copying a cross-file contract. */ +let _validateDependency: (source: SourceFile) => void = () => {}; /** Counter for synthetic names used by let-statement array destructuring * when the initializer isn't a bare variable (single-eval temp). */ let _destrCounter = 0; @@ -122,6 +124,8 @@ function detectCrossFileExtern( if (externalDecl.getSourceFile().getFilePath().endsWith(".d.ts")) return null; const sig = callee.getType().getCallSignatures()[0]; if (!sig) return null; + // Includes global declarations selected by TypeScript without an import edge. + _validateDependency(externalDecl.getSourceFile()); // Generic type parameters (e.g. `step`). ts-morph reports param/return // types in the callee's own type-parameter namespace, so these names match // what `params`/`returnType` reference — declare them on the emitted axiom. @@ -850,7 +854,7 @@ function stringLiteral(value: string, node: Node): RawExpr { throw new Error( `${file.getFilePath()}:${line}: string literal contains an unpaired surrogate ` + `U+${lone.toString(16).toUpperCase()}, which "string-semantics": "unicode-scalar" cannot ` + - `represent; set "string-semantics": "javascript-utf16" and "dafny-library": "local" in lemmascript.json`, + `represent; select string-semantics=javascript-utf16 and dafny-library=local in lemmascript.json or //@ option directives`, ); } } @@ -2075,8 +2079,10 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot // ── Module extraction ──────────────────────────────────────── -export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFAULT_OPTIONS): RawModule { +export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFAULT_OPTIONS, + validateDependency: (source: SourceFile) => void = () => {}): RawModule { _extractOptions = options; + _validateDependency = validateDependency; // Seed the fresh-name check (names.ts) before anything mints: every // Identifier token in the module, a deliberate over-approximation. setUserNames(new Set(sourceFile.getDescendantsOfKind(SyntaxKind.Identifier).map(i => i.getText()))); diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index 83c89abb..1be98245 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -5,7 +5,7 @@ * Pipeline: extract → resolve → narrow → transform → peephole → emit */ -import { Project, ScriptTarget } from "ts-morph"; +import { Project, ScriptTarget, type SourceFile } from "ts-morph"; import { existsSync, mkdirSync, readFileSync } from "fs"; import { execFileSync } from "child_process"; import { createRequire } from "module"; @@ -219,6 +219,29 @@ function effectiveOptions( return { options, configFile: loaded.configFile }; } +/** Imported contracts must retain the string model used by their source files. */ +function stringModelValidator(source: SourceFile, options: LscOptions, configPath?: string): (source: SourceFile) => void { + const seen = new Set(); + return start => { + const pending = [start]; + while (pending.length > 0) { + const dependency = pending.pop()!; + if (seen.has(dependency)) continue; + seen.add(dependency); + pending.push(...dependency.getReferencedSourceFiles()); + // Declaration files describe host APIs; follow re-exports through them, + // but compare models only for source files that can carry verified code. + if (dependency === source || dependency.isDeclarationFile()) continue; + const { options: imported } = effectiveOptions(dependency.getFilePath(), dependency.getFullText(), configPath); + if (imported["string-semantics"] !== options["string-semantics"]) { + throw new Error(`${source.getFilePath()}: string-semantics=${options["string-semantics"]} differs from ` + + `${dependency.getFilePath()} (string-semantics=${imported["string-semantics"]}); ` + + "use the same string model across source dependencies"); + } + } + }; +} + /** `lsc config [file.ts]` — report discovery, effective values, and routing. */ function runConfig(filePath: string | undefined, configPath?: string): void { if (!filePath) { @@ -331,8 +354,13 @@ function runFile( const leanModuleDirective = fullText.match(/\/\/@ lean-module ([A-Za-z0-9_.\-]+)/); const leanModuleOverride = leanModuleDirective ? leanModuleDirective[1] : undefined; + // Validate the actual dependency graph, not unrelated files in the tsconfig. + // Library selection may differ; only the string model changes contract meaning. + const validateDependency = stringModelValidator(sourceFile, options, configPath); + validateDependency(sourceFile); + // Extract: ts-morph → Raw IR - const raw = extractModule(sourceFile, options); + const raw = extractModule(sourceFile, options, validateDependency); if (cmd === "extract") { console.log(JSON.stringify(raw, null, 2)); @@ -414,7 +442,7 @@ function runFile( // LemmaScript has no UTF-16 encoding for it (DESIGN_STRINGS.md §4). Refuse // rather than emit scalar Lean for a code-unit claim. if (options["string-semantics"] === "javascript-utf16") { - console.error('ERROR: "string-semantics": "javascript-utf16" is not available for --backend=lean; use --backend=dafny or set "unicode-scalar" in lemmascript.json.'); + console.error('ERROR: "string-semantics": "javascript-utf16" is not available for --backend=lean; use --backend=dafny or select "unicode-scalar" in lemmascript.json or a //@ option directive.'); process.exit(1); } const leanBase = leanModuleOverride ?? base; diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index 9fe99fc5..81903d4f 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -176,6 +176,11 @@ expect_failure \ expect_absent "$config_fixture/proofs/src/legacy.dfy" # ── String profile and collection library ───────────────────────────────── +# The ordinary example selects both options in source, without a JSON config. +cp examples/utf16.ts "$fixture_dir/utf16-example.ts" +npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/utf16-example.ts" +grep -Fq '// lsc options: string-semantics=javascript-utf16' "$fixture_dir/utf16-example.dfy.gen" + # Under "string-semantics": "javascript-utf16" a JavaScript string is a UTF-16 # code-unit sequence: astral characters occupy two Dafny chars and lone # surrogates stay representable. The header token is what dafnyVerify maps to diff --git a/tools/tests/config.test.ts b/tools/tests/config.test.ts index daef150a..58714e7a 100644 --- a/tools/tests/config.test.ts +++ b/tools/tests/config.test.ts @@ -183,11 +183,13 @@ test("string-semantics is an enum whose default is today's Unicode-scalar model" ); }); -test("string-semantics is config-only: a file cannot reinterpret a callee's strings", () => { - assert.throws( - () => parseFileOptions("//@ option string-semantics javascript-utf16\n", "example.ts"), - /config-only/, - ); +test("string and library directives override project defaults before compatibility checks", () => { + const file = parseFileOptions("//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n", "example.ts"); + const options = resolveOptions({ "string-semantics": "unicode-scalar", "dafny-library": "stdlib", ...file }, "example.ts"); + assert.equal(options["string-semantics"], "javascript-utf16"); + assert.equal(options["dafny-library"], "local"); + assert.throws(() => resolveOptions(parseFileOptions("//@ option string-semantics javascript-utf16\n", "example.ts"), "example.ts"), + /incompatible/); }); test("Dafny library defaults to stdlib and local works with scalar strings", () => { @@ -213,9 +215,18 @@ test("UTF-16 requires an explicit local library choice", () => { assert.equal(resolveOptions(explicit, "lemmascript.json")["dafny-library"], "local"); }); -test("Dafny library accepts only registered values and is config-only", () => { +test("Dafny library accepts only registered values in config and file directives", () => { for (const value of [true, "standard", null]) { assert.throws(() => validateOptions({ "dafny-library": value }, "lemmascript.json"), /must be one of: stdlib, local/); } - assert.throws(() => parseFileOptions("//@ option dafny-library local\n", "example.ts"), /config-only/); + assert.deepEqual(parseFileOptions("//@ option dafny-library local\n", "example.ts"), { "dafny-library": "local" }); + assert.throws(() => parseFileOptions("//@ option dafny-library standard\n", "example.ts"), /must be one of: stdlib, local/); }); + +for (const [key, value] of [["string-semantics", "javascript-utf16"], ["dafny-library", "local"]]) { + test(`${key} retains duplicate and placement checks`, () => { + const directive = `//@ option ${key} ${value}\n`; + assert.throws(() => parseFileOptions(directive + directive, "example.ts"), /duplicate option/); + assert.throws(() => parseFileOptions("const value = 1;\n" + directive, "example.ts"), /before the first source statement/); + }); +} diff --git a/tools/tests/file-options.test.ts b/tools/tests/file-options.test.ts new file mode 100644 index 00000000..55880336 --- /dev/null +++ b/tools/tests/file-options.test.ts @@ -0,0 +1,162 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { spawnSync } from "node:child_process"; +import { existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { createRequire } from "node:module"; +import { tmpdir } from "node:os"; +import { dirname, join } from "node:path"; +import { fileURLToPath } from "node:url"; + +const cli = fileURLToPath(new URL("../src/lsc.ts", import.meta.url)); +const loader = createRequire(import.meta.url).resolve("tsx"); +const utf16 = "//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n"; +const scalar = "//@ option string-semantics unicode-scalar\n//@ option dafny-library stdlib\n"; +const library = "export function size(value: string): number { return value.length; }\n"; +const caller = 'import { size } from "./library";\nexport function read(): number { return size("😀"); }\n'; + +function runCli(files: Record, args: string[] = ["gen", "source.ts"]) { + const dir = realpathSync(mkdtempSync(join(tmpdir(), "lsc-file-options-"))); + try { + for (const [name, source] of Object.entries(files)) { + const target = join(dir, name); + mkdirSync(dirname(target), { recursive: true }); + writeFileSync(target, source); + } + const result = spawnSync(process.execPath, ["--import", loader, cli, ...args], { + cwd: dir, encoding: "utf8", timeout: 30_000, + }); + assert.ifError(result.error); + const gen = join(dir, "source.dfy.gen"); + return { ...result, generated: existsSync(gen) ? readFileSync(gen, "utf8") : null, + proofExists: existsSync(join(dir, "source.dfy")) }; + } finally { + rmSync(dir, { recursive: true, force: true }); + } +} + +test("lsc config reports file-level options without a project config", () => { + const result = runCli({ "source.ts": utf16 + library }, ["config", "source.ts"]); + assert.equal(result.status, 0, result.stderr); + const report = JSON.parse(result.stdout); + assert.equal(report.configFile, null); + assert.equal(report.options["string-semantics"], "javascript-utf16"); + assert.equal(report.options["dafny-library"], "local"); +}); + +test("file directives can select scalar/stdlib over project UTF-16/local", () => { + const result = runCli({ + "lemmascript.json": JSON.stringify({ "string-semantics": "javascript-utf16", "dafny-library": "local" }), + "source.ts": scalar + library, + }, ["config", "source.ts"]); + assert.equal(result.status, 0, result.stderr); + const report = JSON.parse(result.stdout); + assert.equal(report.options["string-semantics"], "unicode-scalar"); + assert.equal(report.options["dafny-library"], "stdlib"); +}); + +test("a local-library directive completes a UTF-16 project setting before validation", () => { + const result = runCli({ + "lemmascript.json": '{"string-semantics":"javascript-utf16"}', + "source.ts": "//@ option dafny-library local\n" + library, + }); + assert.equal(result.status, 0, result.stderr); + assert.match(result.generated!, /string-semantics=javascript-utf16/); +}); + +for (const [name, project, directive] of [ + ["default stdlib", "{}", "//@ option string-semantics javascript-utf16\n"], + ["inherited stdlib", '{"dafny-library":"stdlib"}', "//@ option string-semantics javascript-utf16\n"], + ["file stdlib", '{"string-semantics":"javascript-utf16","dafny-library":"local"}', "//@ option dafny-library stdlib\n"], +]) { + test(`UTF-16 rejects ${name} before writing artifacts`, () => { + const result = runCli({ "lemmascript.json": project, "source.ts": directive + library }); + assert.notEqual(result.status, 0); + assert.match(result.stderr, /incompatible.*dafny-library.*stdlib/); + assert.equal(result.generated, null); + assert.equal(result.proofExists, false); + }); +} + +for (const [name, rootOptions, dependencyOptions] of [ + ["UTF-16 calling scalar", utf16, ""], + ["scalar calling UTF-16", "", utf16], +]) { + test(`rejects ${name} with both source paths and models`, () => { + const result = runCli({ "source.ts": rootOptions + caller, "library.ts": dependencyOptions + library }); + assert.notEqual(result.status, 0); + assert.match(result.stderr, /source\.ts: string-semantics=.*differs from .*library\.ts/); + assert.match(result.stderr, /unicode-scalar/); + assert.match(result.stderr, /javascript-utf16/); + assert.equal(result.generated, null); + assert.equal(result.proofExists, false); + }); +} + +test("matching UTF-16 dependencies work without reinterpreting unrelated tsconfig files", () => { + const result = runCli({ + "tsconfig.json": '{"compilerOptions":{"strict":true},"include":["*.ts"]}', + "source.ts": utf16 + caller, "library.ts": utf16 + library, + "unrelated.ts": library, + }); + assert.equal(result.status, 0, result.stderr); + assert.match(result.generated!, /string-semantics=javascript-utf16/); +}); + +test("scalar dependencies may choose different collection libraries", () => { + const result = runCli({ "source.ts": caller, "library.ts": "//@ option dafny-library local\n" + library }); + assert.equal(result.status, 0, result.stderr); +}); + +test("checks compiler-selected global callees without an import edge", () => { + const result = runCli({ + "tsconfig.json": '{"compilerOptions":{"strict":true},"include":["*.ts"]}', + "source.ts": utf16 + 'export function read(): number { return size("😀"); }\n', + "library.ts": library.replace("export ", ""), + }); + assert.notEqual(result.status, 0); + assert.match(result.stderr, /differs from .*library\.ts/); + assert.equal(result.generated, null); +}); + +for (const barrel of ["barrel.ts", "barrel.d.ts"]) { + test(`checks transitive model mismatches through ${barrel}`, () => { + const result = runCli({ + "source.ts": caller.replace("./library", "./barrel"), + [barrel]: 'export { size } from "./library";\n', + "library.ts": utf16 + library, + }); + assert.notEqual(result.status, 0); + assert.match(result.stderr, /differs from .*library\.ts/); + assert.equal(result.generated, null); + }); +} + +test("cycles terminate when all dependency models match", () => { + const result = runCli({ + "source.ts": caller, + "library.ts": 'export { read } from "./source";\n' + library, + }); + assert.equal(result.status, 0, result.stderr); +}); + +test("nested project configs are checked instead of inheriting the caller's model", () => { + const result = runCli({ + "source.ts": caller.replace("./library", "./nested/library"), + "nested/lemmascript.json": '{"string-semantics":"javascript-utf16","dafny-library":"local"}', + "nested/library.ts": library, + }); + assert.notEqual(result.status, 0); + assert.match(result.stderr, /differs from .*nested\/library\.ts/); + assert.equal(result.generated, null); +}); + +test("--config pins the shared project settings for dependencies too", () => { + const result = runCli({ + "source.ts": caller.replace("./library", "./nested/library"), + "shared.json": '{"string-semantics":"javascript-utf16","dafny-library":"local"}', + "nested/lemmascript.json": '{"string-semantics":"unicode-scalar"}', + "nested/library.ts": library, + }, ["gen", "--config=shared.json", "source.ts"]); + assert.equal(result.status, 0, result.stderr); + assert.match(result.generated!, /string-semantics=javascript-utf16/); +}); From 7fcf97496a1fef1136ca1ba6f78456126f46e5a0 Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Mon, 28 Sep 2026 12:27:24 -0700 Subject: [PATCH 08/15] fix: explain local library option in UTF-16 diagnostic --- tools/src/dafny-commands.ts | 4 +++- tools/tests/dafny-commands.test.ts | 22 +++++++++++++++++++--- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 177cbe71..518ee4c4 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -99,7 +99,9 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? return { args: [], error: "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " + "Dafny 4.11 cannot load its Unicode-scalar standard library under --unicode-char:false. " + - "Remove the Std.* import from the proof additions, or select unicode-scalar in lemmascript.json or a //@ option directive and regenerate." }; + "Set \"dafny-library\": \"local\" in lemmascript.json or add //@ option dafny-library local, " + + "then run lsc regen to regenerate collection helpers. " + + "This does not rewrite handwritten Std.* imports or calls; replace those with local proofs or helpers separately." }; } const args: string[] = ["verify"]; if (usesStandardLibrary) args.push("--standard-libraries"); diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts index f0a1ca47..48847363 100644 --- a/tools/tests/dafny-commands.test.ts +++ b/tools/tests/dafny-commands.test.ts @@ -102,9 +102,25 @@ test("javascript-utf16 selects code-unit chars and only the deprecation waiver", assert.deepEqual(args, ["verify", "--unicode-char:false", "--allow-deprecation"]); }); -test("javascript-utf16 refuses the Unicode-scalar standard library", () => { - const { error } = dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\nimport opened Std.Arithmetic.Mul\n"); - assert.match(error ?? "", /string-semantics/); +for (const reference of [ + "import opened Std.Arithmetic.Mul", + "function all(xs: seq): bool { Std.Collections.Seq.All(xs, x => x > 0) }", +]) { + test(`UTF-16 library diagnostic explains local helpers and proof additions: ${reference}`, () => { + const { args, error } = dafnyVerifyArgs(`// lsc options: string-semantics=javascript-utf16\n${reference}\n`); + assert.deepEqual(args, []); + assert.match(error ?? "", /string-semantics/); + assert.match(error ?? "", /Set "dafny-library": "local" in lemmascript\.json/); + assert.match(error ?? "", /\/\/@ option dafny-library local/); + assert.match(error ?? "", /lsc regen/); + assert.match(error ?? "", /does not rewrite handwritten Std\.\* imports or calls/); + }); +} + +test("Unicode-scalar proofs can still use the standard library", () => { + const { args, error } = dafnyVerifyArgs("import opened Std.Arithmetic.Mul\n"); + assert.equal(error, undefined); + assert.deepEqual(args, ["verify", "--standard-libraries", "--unicode-char:true"]); }); for (const token of ["string-semantics=utf8", "string-semantics=", "string-semantics"]) { From 09d0240a9e1517a0d2688feab34e3040b80983b6 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Tue, 29 Sep 2026 20:28:56 -0700 Subject: [PATCH 09/15] Clarify string verification documentation --- DESIGN_STRINGS.md | 29 ++++++++++++++--------------- SPEC_DAFNY.md | 17 +++++++---------- 2 files changed, 21 insertions(+), 25 deletions(-) diff --git a/DESIGN_STRINGS.md b/DESIGN_STRINGS.md index 941efe88..b9305787 100644 --- a/DESIGN_STRINGS.md +++ b/DESIGN_STRINGS.md @@ -237,21 +237,20 @@ or case-study file regenerates. | `unicode-scalar` | `--unicode-char:true` — an explicit pin of today's default. A default is not a pin; verifying under a changed setting would silently reinterpret every string obligation. | | `javascript-utf16` | `--unicode-char:false --allow-deprecation` | -#211 passes `--allow-warnings`, because Dafny 4.11 prints -`CLI: Warning: the option unicode-char has been deprecated.` and, by default, any warning -fails the run (`--allow-warnings` still prints it and only un-fatals it; `--allow-deprecation` -removes it). But `--allow-warnings` un-fatals *every* warning in the file — including -`warn-contradictory-assumptions` (a `requires` proved vacuous) and the missing-`{:axiom}` -warning, which are exactly the guards a verifier most needs. Dafny 4.11 has the narrow -alternative, `--allow-deprecation`: "Do not warn about the use of deprecated features." -Measured on 4.11.0: with `unicode-char = false`, `allow-deprecation = true`, and -`allow-warnings = false`, a surrogate literal verifies with no warning, and a method with -`requires false` under `warn-contradictory-assumptions` still fails the run. That resolves -[DESIGN_CONFIG.md](DESIGN_CONFIG.md) open question 2: the `unicode-char` deprecation — and, -by the flag's definition, every other *deprecated-feature* warning, which are style warnings — -is suppressed; `warn-contradictory-assumptions`, missing-`{:axiom}` (bodiless `ensures`, -`assume`), `{:verify false}`, and missing-trigger warnings all remain fatal (measured on -4.11.0). +`dafnyVerifyArgs` reads the generated header and supplies the flags above. Dafny +4.11 deprecates `--unicode-char:false`, so UTF-16 verification adds +`--allow-deprecation`. This suppresses deprecated-feature warnings, including the +character-mode warning; other warning categories remain fatal under the default +verification policy. + +Using `--allow-warnings` would also allow verification to succeed despite warnings +about contradictory assumptions or missing `{:axiom}` declarations. The narrower +flag preserves those checks. Measured on Dafny 4.11.0 with `unicode-char = false`, +`allow-deprecation = true`, and `allow-warnings = false`: a surrogate literal +verifies with no warning, while `requires false` under +`warn-contradictory-assumptions` still fails the run. Missing-`{:axiom}` (bodiless +`ensures`, `assume`), `{:verify false}`, and missing-trigger warnings also remain +fatal. This resolves [DESIGN_CONFIG.md](DESIGN_CONFIG.md) open question 2. Two facts that make this safe, both measured on Dafny 4.11.0. `--unicode-char:true` is silent — only the `:false` value is warned as deprecated — so pinning the default costs diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index 5a4ac61f..e2847b17 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -144,15 +144,12 @@ to the character-mode compatibility check below. Selecting `local` does not chan Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the `--standard-libraries` flag is added. -The char mode is read from the artifact, not the config, so a standalone `.dfy` -verifies under the model it was generated for: `dafnyVerify` pins -`--unicode-char:true` unless the header carries -`// lsc options: string-semantics=javascript-utf16`, in which case it passes -`--unicode-char:false --allow-deprecation` (only the `:false` value is deprecated -in Dafny 4.11; `--allow-deprecation` waives exactly that warning, whereas -`--allow-warnings` would also un-fatal vacuity and missing-`{:axiom}` warnings). -Dafny's precompiled standard library cannot load under `--unicode-char:false`, so -a `javascript-utf16` proof whose additions import `Std.*` fails closed with an -error naming `string-semantics`; a `unicode-scalar` proof may use it freely. +`lsc` verifies each `.dfy` using the string semantics recorded in its generated +header, even if the project configuration has changed. A file without a +`string-semantics` header uses `unicode-scalar`. + +Proofs using `javascript-utf16` cannot import Dafny's precompiled standard library +(`Std.*`); verification reports an error if they do. Proofs using `unicode-scalar` +can use that library. The shared `--time-limit=` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=` is forwarded verbatim to `dafny verify`. From cb1d9c96bfbd1630c8add6b3044af3bf4dfc4e74 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Tue, 29 Sep 2026 20:41:40 -0700 Subject: [PATCH 10/15] Clarify UTF-16 configuration scope --- SPEC.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/SPEC.md b/SPEC.md index f2898c6b..a8af06f9 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1392,8 +1392,11 @@ Eligible settings use `//@ option ` before the first source statement. File values override project values; duplicates are errors. `proof-dir` mirrors the source's config-relative path under its configured root (see SPEC_DAFNY.md §1). `string-semantics` selects which model of JavaScript strings a -Dafny proof is made under (SPEC_DAFNY.md §4). Source dependencies must use the same -effective string model; mismatches name both files and are rejected before emission. +Dafny proof is made under (SPEC_DAFNY.md §4). A source file and the source files it +imports, directly or indirectly, must use the same `string-semantics` value after +project settings and file overrides are combined. Declaration files (`.d.ts`) +are excluded from this comparison. If values differ, `lsc` reports both files +and stops before generating Dafny. `dafny-library` selects standard-library or generated local helpers for `filter`, `every`, and `reduce`. UTF-16 requires an explicit `"dafny-library": "local"`; omitting it keeps the `stdlib` default and reports an incompatibility. @@ -1401,7 +1404,9 @@ Unicode-scalar strings support either library choice. `lsc config foo.ts` prints options, and resolved Dafny artifact directory; `lsc config` reports defaults from the current directory. `backend` is deliberately not a config option. -For a standalone file, put both settings before its first statement: +To use JavaScript UTF-16 string semantics in a standalone file, add these +directives before its first statement. These overrides are not needed for the +default `unicode-scalar` mode: ```typescript //@ backend dafny From 74b8e349acc14de15fa7873773999df8c338c7e6 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Tue, 29 Sep 2026 20:51:01 -0700 Subject: [PATCH 11/15] Simplify string profile documentation --- SPEC_DAFNY.md | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index e2847b17..76d6e2db 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -117,20 +117,26 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at | `StringTrim` | `s.trim()` / `s.trimEnd()` / `s.trimStart()` | Trim (also provides `StringTrimRight` / `StringTrimLeft`); strips the full ECMAScript whitespace set via `IsJSWhitespace`, not just `' '` | | `StringToLower` / `StringToUpper` | `s.toLowerCase()` / `s.toUpperCase()` | Case folding | -**String profile.** `string-semantics` in `lemmascript.json` or a file's `//@ option` directive (SPEC.md §7.6) selects which model of JavaScript strings a proof is made under; each is a named identity the proof's claims are relative to: +**String semantics.** Set `string-semantics` in `lemmascript.json` or a file's +`//@ option` directive (SPEC.md §7.6). Proofs depend on the selected model: -| Identity | Option value | Claim | +| Profile | Setting | Meaning | |---|---|---| -| `unicode-scalar-1` | `"unicode-scalar"` (default) | Dafny `string` under `--unicode-char:true`: strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` are over scalars and differ from JavaScript for astral text; unpaired surrogates are outside the domain (refused in literals; `String.fromCharCode` requires a scalar); case mapping is ASCII-only. No header token. | -| `javascript-utf16-1` | `"javascript-utf16"` | Dafny `string` under `--unicode-char:false`: strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, `charCodeAt`, and `String.fromCharCode` (`0 <= n < 0x10000`) are exact; requires `"dafny-library": "local"` because the Dafny standard library cannot load in this mode; case mapping is ASCII-only. Generated string-bearing files carry `// lsc options: string-semantics=javascript-utf16`. | - -**Collection helpers.** `dafny-library` independently selects `stdlib` (default) or `local` -for `filter`, `every`, and `reduce`: `Std.Collections.Seq.Filter/All/FoldLeft` or generated -`SeqFilter`/`SeqAll`/`SeqFoldLeft`. Unicode-scalar strings support both choices. UTF-16 with -an omitted or explicit `stdlib` choice is a configuration error; select `local` explicitly. -Both settings accept file directives; [examples/utf16.ts](examples/utf16.ts) demonstrates them. -This option controls generated helpers, not handwritten proof imports; those remain subject -to the character-mode compatibility check below. Selecting `local` does not change string semantics. +| `unicode-scalar-1` | `"unicode-scalar"` (default) | Strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` can differ from JavaScript for characters such as emoji. Unpaired surrogates are unsupported. | +| `javascript-utf16-1` | `"javascript-utf16"` | Strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, and `charCodeAt` match JavaScript. Requires `"dafny-library": "local"`. | + +Both profiles support ASCII-only case conversion. `String.fromCharCode` requires +a Unicode scalar in the default profile, or `0 <= n < 0x10000` in UTF-16 mode. +Generated string-bearing files record the UTF-16 setting in their header; +the default profile adds no `string-semantics` setting. + +**Collection helpers.** `dafny-library` selects standard-library helpers (`stdlib`, +the default) or generated helpers (`local`) for `filter`, `every`, and `reduce`. +Unicode-scalar mode supports either; UTF-16 mode requires an explicit `local` setting. + +This choice does not change string semantics or control handwritten proof imports. +Those imports must still be compatible with the selected string model (see §5). +Both settings support file directives; see [examples/utf16.ts](examples/utf16.ts). --- From 4ec57ea716b7cf9f531f7d5c0741008e9c2f45b7 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Tue, 29 Sep 2026 21:18:10 -0700 Subject: [PATCH 12/15] Correct default string semantics documentation --- SPEC.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/SPEC.md b/SPEC.md index a8af06f9..8acd4d20 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1021,12 +1021,10 @@ The spec body is purely additive — `regen` three-way-merges and preserves user | `A \| B` (union param) | field intersection type | field intersection type | | Anything else | Pass through | Pass through | -For the Dafny backend, `string` is verified in Dafny's UTF-16 code-unit -character mode (`--unicode-char:false`). This matches JavaScript's observable -`.length`, indexing, slicing, `charCodeAt`, and equality semantics, including -astral characters occupying two positions and unpaired surrogate code units. -Non-ASCII source literals are emitted as `\\uXXXX` code-unit escapes so the -generated UTF-8 file preserves the exact JavaScript value. +For the Dafny backend, `string` uses Unicode-scalar semantics by default. +To use JavaScript's UTF-16 code-unit model, select +`"string-semantics": "javascript-utf16"` and `"dafny-library": "local"` +(§7.6). See SPEC_DAFNY.md §4 for the behavior and limitations of each model. `lsc` reads parameter and variable types from ts-morph. Primitive types are mapped per the table. User-defined types (like `State`, `Event`) are passed through by name — the corresponding backend type is generated from the TS type declaration. From 656533fc1c9e213e9db3fcf7cc879945b1c8bfcf Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Wed, 30 Sep 2026 13:35:38 -0700 Subject: [PATCH 13/15] Simplify string model handling and protect proof headers --- DESIGN_CONFIG.md | 58 ++- DESIGN_STRINGS.md | 437 +++++------------------ SPEC.md | 15 +- SPEC_DAFNY.md | 15 +- TOOLS.md | 33 +- tools/src/dafny-commands.ts | 46 ++- tools/src/dafny-emit.ts | 18 +- tools/tests/dafny-commands.test.ts | 30 ++ tools/tests/dafny-emit.test.ts | 25 +- tools/tests/dafny-string-profile.test.ts | 99 +++++ 10 files changed, 311 insertions(+), 465 deletions(-) create mode 100644 tools/tests/dafny-string-profile.test.ts diff --git a/DESIGN_CONFIG.md b/DESIGN_CONFIG.md index 65704ae8..f07db4f8 100644 --- a/DESIGN_CONFIG.md +++ b/DESIGN_CONFIG.md @@ -104,32 +104,22 @@ The source must be inside the config directory when `proof-dir` is set (includin Enabling the option must not silently strand proof additions. If the mapped `.dfy` is absent but a sibling `.dfy`, `.dfy.base`, or `.dfy.merged` exists beside the TS, `lsc` fails with paths and tells the user to move the hand-written `.dfy`, discard or inspect merge-state files, and rerun; `.dfy.gen` is regeneratable. Changing from one non-default proof directory to another likewise requires moving the proof first and is documented as a migration, because the new config cannot discover an arbitrary old root. -## String and collection options (PR #211, issue #210) - -`string-semantics: "unicode-scalar" | "javascript-utf16"` chooses the string model, -defaulting to `unicode-scalar`. `dafny-library: "stdlib" | "local"` independently chooses -the generated collection helpers, defaulting to `stdlib`. Both accept top-of-file -`//@ option` directives, which override project settings before compatibility is checked. -The ordinary [UTF-16 example](examples/utf16.ts) needs no JSON config. - -The CLI follows TypeScript-resolved source dependencies and checks their effective string -models against the root file before emission. It also checks compiler-selected cross-file -callees before extraction copies their contracts, including global declarations without -an import edge. Cycles are visited once; unrelated tsconfig files are not dependencies. -Declaration files carry no model, but their re-exports are followed. `--config` pins the -project settings for dependencies too; file directives still apply separately. Different -collection-library choices are allowed because they do not reinterpret contracts. - -`stdlib` emits `Std.Collections.Seq.Filter/All/FoldLeft` for `filter`/`every`/`reduce`; -`local` emits `SeqFilter`/`SeqAll`/`SeqFoldLeft` definitions on demand. Unicode-scalar -projects may select either. UTF-16 requires an explicit `local` choice: `resolveOptions` -rejects both an omitted and an explicit `stdlib`, without silently changing the default. - -UTF-16 string-bearing artifacts record their model in the header; verification uses -`--unicode-char:false --allow-deprecation`. The precompiled Dafny standard library uses -Unicode-scalar characters and cannot load in that mode. The artifact-level check still -rejects `Std.*` in UTF-16 proof additions; config validation cannot inspect handwritten -proof text. The library choice itself requires no additional verifier flag. +### 3.4 String and collection options + +`string-semantics` selects `unicode-scalar` (default) or `javascript-utf16`. +The independent `dafny-library` option selects `stdlib` (default) or `local` +collection helpers. Both accept file overrides. UTF-16 requires an explicit +`local` choice; `resolveOptions` rejects incompatible effective settings after +project values and file directives are merged. Lean rejects UTF-16. + +Source dependencies must use the same effective string model before their +contracts are copied. The check follows imports, re-exports, and compiler-selected +cross-file callees; unrelated files are excluded. An explicit `--config` applies +to dependencies too, while each file retains its directives. Collection-library +choices may differ because they do not reinterpret contracts. + +See [DESIGN_STRINGS.md](DESIGN_STRINGS.md) for emission and verification behavior, +and [SPEC.md §7.6](SPEC.md#76-project-configuration-lemmascriptjson) for setup. ## Future options @@ -161,9 +151,15 @@ Options requiring non-default verifier flags are recorded in the artifact, so a // lsc options: string-semantics=javascript-utf16 ``` -The line contains space-separated option tokens. UTF-16 appears only when the file has strings and selects `--unicode-char:false --allow-deprecation`. `dafny-library` does not need a token because it changes emitted helpers, not verifier flags. A future number-model marker can use the same mechanism. The additions-only check guarantees `.dfy` and `.dfy.gen` share the header, so changing a model surfaces as a generator change: `regen` merges the new header before verification. +Every UTF-16-selected file receives the token, including files whose declarations +have no string types. `dafny-library` needs no token because it changes generated +helpers rather than verifier flags. The verifier reads the saved model; +without a token it uses Unicode-scalar mode. Existing scalar headers are unchanged. -Without a string-model token, verification explicitly uses `--unicode-char:true`. Existing scalar artifacts therefore need no header change. +Parsing rejects unknown models, duplicate options headers, and duplicate string-model tokens. +The additions-only gate compares the proof's model with its generated companion, +so an inserted header cannot override it. A model change requires `regen` to +merge the new generated header before verification. ## 6. CLI surface @@ -195,9 +191,3 @@ Without a string-model token, verification explicitly uses `--unicode-char:true` - `time-limit` / `extra-flags` as project defaults. `LemmaScript-files.txt` already carries them per file; adding a project-wide default is a registry entry away if a case study asks. - JSON Schema generation (`lsc config --schema`). Cheap follow-up from the registry; not needed to land. - Options in the Raw IR JSON (`lsc extract`). The IR already reflects their effect (`RawExtern.impure`). - -## Open questions - -1. **Resolved string option shape.** `string-semantics: "unicode-scalar" | "javascript-utf16"` selects the string model. The independent `dafny-library` option selects collection helpers. -2. **Resolved warning scope.** UTF-16 uses `--allow-deprecation` for Dafny's character-mode flag. Other warnings remain fatal. -3. **Header parsing.** Should `dafnyVerify` warn when a `.dfy` lacks the `// Generated by lsc` line entirely? It currently accepts such files and uses the default string model when no options header is present. diff --git a/DESIGN_STRINGS.md b/DESIGN_STRINGS.md index b9305787..b60d3df8 100644 --- a/DESIGN_STRINGS.md +++ b/DESIGN_STRINGS.md @@ -1,373 +1,98 @@ -# DESIGN_STRINGS — JavaScript string semantics as a versioned profile +# DESIGN_STRINGS — Selectable Dafny string semantics -**Status:** rung 0 and rung 1 implemented in PR #211; later rungs unscheduled. The project selects its string model and collection library through the option registry described in [DESIGN_CONFIG.md](DESIGN_CONFIG.md). -**Date:** September 2026 +**Status:** implemented in PR #211. **Issue:** [#210](https://github.com/midspiral/LemmaScript/issues/210) · **PR:** [#211](https://github.com/midspiral/LemmaScript/pull/211) -## Decision summary +JavaScript strings are UTF-16 code-unit sequences, while Dafny's default strings +are Unicode scalar sequences. For example, JavaScript gives `"😀".length === 2`; +the default Dafny model gives 1. LemmaScript keeps that existing model as the +default and offers an explicit UTF-16 choice for code that depends on code units. -A kind of string is a **named, versioned profile**: a domain of admitted values, a -length/index/equality semantics proved to agree with JavaScript on that domain, a closed -set of operations each with a stated meaning, and an **identity stamped into every proof**. -LemmaScript should expose it as an enum-shaped project option, not a boolean — the same -shape [DESIGN_NUMBERS.md](DESIGN_NUMBERS.md) chose for `number-semantics`: +## Models and configuration -```json -{ - "string-semantics": "unicode-scalar" -} -``` - -| Value | Artifact identity | Meaning | Intended use | -|---|---|---|---| -| `unicode-scalar` | `unicode-scalar-1` | Today's model, byte for byte: Dafny `string` under `unicode-char:true`, one `char` per Unicode scalar. `.length`, indexing, `slice`, and `charCodeAt` are over scalars and differ from JavaScript for astral characters; unpaired surrogates are outside the domain. | Existing proofs. Strings that are ASCII, or where only emptiness, equality of well-formed text, and search matter. | -| `javascript-utf16` | `javascript-utf16-1` | PR #211's model: `unicode-char:false`, one `char` per UTF-16 code unit. `.length`, indexing, `slice`, and `charCodeAt` are exact; `String.fromCharCode` is exact for `0 <= n < 0x10000` (JavaScript's ToUint16 wrap is refused by precondition). The Dafny standard library is unavailable. | Code whose behaviour depends on code-unit counts, surrogates, or `charCodeAt` of non-BMP text. | - -`unicode-scalar` stays the default so no `lemmascript.json` means today's behaviour -([DESIGN_CONFIG.md](DESIGN_CONFIG.md) requirement 3). A project opts into `javascript-utf16` -by setting `"string-semantics": "javascript-utf16"` and `"dafny-library": "local"` explicitly, -either in project config or through file-level `//@ option` directives. -A `javascript-utf16` proof carries `// lsc options: string-semantics=javascript-utf16` -in its header ([DESIGN_CONFIG.md](DESIGN_CONFIG.md) §5 form); the default's header is -unchanged, so no existing artifact changes. Each identity's claim sentence lives in -SPEC_DAFNY.md §4. `dafnyVerify` pins `--unicode-char:true` whenever the token is absent — -today the default is Dafny's *unstated* setting rather than a pin. - -The immediate deliverable is rung 0 (§7): name the profile, make it configuration, and pin the -default in the verifier. It changes no semantics and no checked-in file, and is worth landing -whether or not #211 merges. Rung 1 is #211's emitter work on the option registry, gated on the -option. - -## 1. What "faithful" means for strings - -For each supported string construct, translation must commute with ECMAScript evaluation on -the profile's domain: - -```text -decode(evalBackend(translate(e))) = evalECMAScript(e) for every string value in Domain(profile) -``` - -The observable results are: a Number for `.length`, `indexOf`, and `charCodeAt`; a string -for `slice`, `substring`, `trim`, case mapping, `repeat`, concatenation, and template -literals; a Boolean for `includes`, `startsWith`, `endsWith`, and `===`; and a string array -for `split`. A JavaScript string is a sequence of UTF-16 code units -([ECMAScript §6.1.4](https://tc39.es/ecma262/multipage/ecmascript-data-types-and-values.html#sec-ecmascript-language-types-string-type)); -`.length` counts code units, indexing yields code units, and unpaired surrogates are legal -values. Nothing in the language distinguishes a code point from its surrogate pair except by -value. - -This is scoped to the LemmaScript fragment. Constructs outside it — regular expressions, -`normalize`, `localeCompare`, `Intl.*`, iteration by code point — do not become supported -because the string model is faithful. Every accepted construct must be faithful on the -selected profile's domain, or refused with a diagnostic. An unmodelled construct is never an -opportunity to emit a scalar operation and call it a code-unit one. - -Where the two languages disagree, the difference becomes an obligation, a refusal, or a -stated claim in the artifact. It never becomes an approximation that looks right. - -## 2. The mismatch, and why a boolean is the wrong shape - -Dafny defines `string` as `seq`, and `char` depends on `--unicode-char` -([Dafny 4.11 reference](https://dafny.org/v4.11.0/Compilation/StringsAndChars)): - -| Concern | JavaScript | Dafny, `unicode-char:true` (4.x default) | Dafny, `unicode-char:false` | -|---|---|---|---| -| Element | UTF-16 code unit | Unicode scalar value | UTF-16 code unit | -| `"😀".length` / `\|"😀"\|` | 2 | 1 | 2 | -| `"\uD83D"` (lone surrogate) | length 1 | not representable | length 1 | -| Standard library | — | available | **incompatible** (`--standard-libraries` help: "Not compatible with the --unicode-char:false option") | -| Status of the option | — | silent (not listed by `dafny verify --help`) | deprecated in the CLI: `:false` prints `CLI: Warning: the option unicode-char has been deprecated.`; `:true` prints nothing | - -`main` passes no `--unicode-char` at all -([`tools/src/dafny-commands.ts` `dafnyVerify`](tools/src/dafny-commands.ts)), so the scalar -model is Dafny's default, not a LemmaScript decision, and the one-line header -`// Generated by lsc from foo.ts` does not mention it. A reader of a standalone `.dfy` cannot -tell that `|s|` in the proof is not JavaScript's `s.length`. #211 flips the model whenever a -file contains a string, marks the artifact, and text-scans the mark in the verifier. That -makes the model observable, but it is presence-selected *semantics*: every string-bearing -case study's obligations are reinterpreted and its `.dfy.gen` changes, so `lsc check` fails -until a `regen` — that is the "breaking" in #210. A presence-emitted *annotation* is harmless -to proofs and is what DESIGN_CONFIG.md §5 already specifies; the fix is to declare the model -in configuration and let the header record a non-default choice. - -A boolean fixes the declaration and stops there. A profile family is what the next rung -needs: JavaScript also offers `normalize()` (canonical equivalence) and `Intl.Segmenter` -(grapheme clusters), each a different domain and equality with its own trusted, versioned -tables. LemmaSwift's `textProfile` went from one rung to four on one key; each rung landed as -its own PR with its own evidence, and asking for an unimplemented rung is a configuration -error naming today's values, never a silent reinterpretation. Those rungs exist because -Swift's `.count` is grapheme-based; JavaScript's `.length` is code units and no issue asks for -`normalize()` or `Intl.Segmenter`, so the same *shape* applies here — the enum costs nothing -now and avoids a second key later — not the same schedule. - -## 3. The two rungs, operation by operation - -The string surface is the twelve `string.*` entries in -[`tools/src/builtins.ts`](tools/src/builtins.ts) (typed by the resolver), plus `s.indexOf` -and `s.charCodeAt` — which the resolver types `unknown` and the Dafny emitter lowers by -method name (`dafny-emit.ts`) — plus `.length` (typed `nat` in resolve), indexing (typed -`unknown`), `String.fromCharCode` (typed `string`), `+`, template literals, and `===`. -Registering `string.indexOf`/`string.charCodeAt` there is deferred (§7): they type `unknown` -today, and a registered return type would change emitted text. Each row states what a proof -under each rung claims. "Exact" -means the emitted Dafny equals the JavaScript result for every value in the rung's domain. - -| Operation | Emitted Dafny (today) | `unicode-scalar-1` | `javascript-utf16-1` | -|---|---|---|---| -| `s.length` | `\|s\|` | scalar count — **differs from JS for astral text** | exact | -| `s[i]`, `s.charCodeAt(i)` | `s[i]`, `(s[i] as int)` | scalar at scalar index — **differs** | exact | -| `s.slice(a, b)`, `s.substring(a, b)` | `s[a..b]` | scalar indices — **differs** | exact | -| `String.fromCharCode(n)` | `StringFromCharCode(n)`, `requires 0 <= n < 0xD800 \|\| 0xE000 <= n < 0x110000` | surrogates refused by precondition (today's behaviour, now stated) | `requires 0 <= n < 0x10000`; exact | -| `a + b`, template literals | `+` | exact on the domain | exact | -| `===`, `!==` | `==` | exact on the domain (no two distinct scalar sequences are equal) | exact | -| `s.indexOf(t)`, `.includes` | `StringIndexOf` | scalar offsets — **differs** | exact | -| `s.startsWith(t)`, `.endsWith(t)` | prefix/suffix `==` | exact on the domain | exact | -| `s.split(d)` | `StringSplit` (axiomatic; `requires \|d\| > 0`, `1 <= \|res\| <= \|s\| + 1`) | trusted axiom, as today; `split("")` refused by precondition | same | -| `s.trim*()` | `StringTrim` via `IsJSWhitespace` | exact — whitespace set is BMP-only in both encodings | exact; escape form changes (`\u` vs `\U{}`) | -| `s.toLowerCase()`, `.toUpperCase()` | `StringToLower`/`Upper`, ASCII letters only (`A–Z` → `a–z`, `a–z` → `A–Z`), `ensures \|res\| == \|s\|` | **ASCII case mapping only**; non-ASCII letters unchanged — differs from JS, which is full Unicode and not length-preserving (`"ß".toUpperCase() === "SS"`) | same restriction, same claim | -| `s.repeat(n)` | `StringRepeat` | exact | exact | -| Literal | written raw; only `\`, `"`, `\n` escaped | literal must be in the domain: a source literal containing an unpaired surrogate is **refused at extraction** (today Node's UTF-8 writer would silently replace it — a current defect this rung closes) | every literal admitted; non-printable-ASCII units written as `\uXXXX` | - -Two rows deserve a sentence each. The `fromCharCode` precondition on `main` is the scalar -profile being honest at exactly one point — it refuses `String.fromCharCode(0xD83D)` by an -obligation the caller cannot discharge — while `.length` two lines away is silently scalar. -Rung 0 makes SPEC_DAFNY.md §4 say what that precondition already knows. And case mapping is -ASCII-only under *both* rungs; each profile's claim sentence names it, because `toLowerCase` -is the -kind of operation that looks identical in both languages and is not. - -Under `unicode-scalar` the domain is "strings with no unpaired surrogate", which Dafny -enforces structurally: the type cannot hold one. That is a fact of both type systems, not a -premise a caller must discharge, so the profile's claim sentence says *no caller premise* -for the domain and states the operations that differ instead. - -## 4. Configuration - -Two registry entries in [`tools/src/config.ts`](tools/src/config.ts), following the shape -`OPTION_SPECS` already has: - -```ts -"string-semantics": { - type: "enum", - values: ["unicode-scalar", "javascript-utf16"], - default: "unicode-scalar", - fileOverride: true, - description: "Which model of JavaScript strings a Dafny proof is made under.", -}, -"dafny-library": { - type: "enum", - values: ["stdlib", "local"], - default: "stdlib", - fileOverride: true, - description: "Use Dafny's standard library or generated local helpers for collection operations.", -}, -``` - -Both settings accept `//@ option` before the first source statement. File values override -project values, and compatibility is checked after merging. The CLI checks the effective -string model across source dependencies, including re-exports, nested config files, and -compiler-selected cross-file callees. A mismatch names both files and stops translation -before contracts can be interpreted under the wrong model. Declaration files carry no -model; their re-exports are followed. Unrelated tsconfig files can use other profiles. - -`dafny-library` independently selects `Std.Collections.Seq` helpers (`stdlib`, the default) -or generated `SeqFilter`/`SeqAll`/`SeqFoldLeft` helpers (`local`). Unicode-scalar strings -support either choice. `resolveOptions` rejects UTF-16 with an omitted or explicit `stdlib` -choice and asks for `"dafny-library": "local"`; it never changes the library silently. -Library choices may differ between dependencies; their string profiles must agree. -`dafnyVerify`'s text detection of `Std.` is unchanged; a `javascript-utf16` -artifact whose proof additions import `Std.*` is refused by #211's fail-closed check with a -message naming `string-semantics`. `lsc config` reports both resolved values. -The library choice is embodied in the generated helper definitions/calls, so it needs no -extra verifier flag or artifact token. Handwritten imports remain subject to the artifact's -character mode, independently of which collection helpers were generated. - -Selecting `javascript-utf16` with `--backend=lean` is an error. Lean's `String` is a sequence -of `Char` (Unicode scalars) and [`LemmaScript/JSString.lean`](LemmaScript/JSString.lean) -defines `indexOf`/`slice` over `List Char`; it has a scalar model and no UTF-16 encoding. -The error must say so rather than emit scalar Lean for a UTF-16 claim. A value not on the -knob is an error listing today's values. - -## 5. The artifact - -Generated files carry the model in [DESIGN_CONFIG.md](DESIGN_CONFIG.md) §5's `lsc options` -form, and only when it is non-default: +| Setting | Meaning | +|---|---| +| `unicode-scalar` (default) | One element per Unicode scalar. Length, indexing, slicing, character codes, and search offsets can differ from JavaScript for astral text. Unpaired surrogates are outside the domain. | +| `javascript-utf16` | One element per UTF-16 code unit. Supported operations use JavaScript's code-unit representation, including astral pairs and unpaired surrogates. | + +`string-semantics` selects the model. The independent `dafny-library` option +selects `stdlib` (default) or generated `local` helpers for `filter`, `every`, +and `reduce`. Unicode-scalar mode supports either library. UTF-16 requires an +explicit `local` choice because Dafny's precompiled standard library cannot load +in that character mode; incompatible combinations are errors. + +Both options accept project settings and file directives, with file values +taking precedence. Configuration syntax lives in [SPEC.md §7.6](SPEC.md#76-project-configuration-lemmascriptjson). +Before copying contracts or emitting a proof, the CLI checks that source +dependencies use the same effective string model. Re-exports and compiler-selected +cross-file callees are included; unrelated files are not. Library choices may +differ between dependencies because they do not reinterpret contracts. +The Lean backend rejects UTF-16 because it has no corresponding string model. + +## Emission and operation boundaries + +UTF-16 literals are emitted as `\uXXXX` code-unit escapes outside printable ASCII, +so astral pairs and lone surrogates survive writing the UTF-8 artifact. +Unicode-scalar extraction rejects literals containing unpaired surrogates. +Character-sensitive helpers use the selected Dafny character representation. + +| Operation | Unicode-scalar | UTF-16 | +|---|---|---| +| Length, indexing, slicing, `charCodeAt`, search offsets | Scalar positions and values | Code-unit positions and values | +| Concatenation, equality, prefixes/suffixes, `repeat`, `trim*` | Preserves the operation's meaning on well-formed scalar strings | Preserves the operation's meaning on code-unit strings | +| `String.fromCharCode(n)` | Requires a Unicode scalar value | Requires `0 <= n < 0x10000`; wrapping is not modeled | +| `toLowerCase`, `toUpperCase` | ASCII letter conversion; non-ASCII letters unchanged | Same restriction | +| `split(d)` | Existing axiomatic helper; requires a nonempty delimiter | Same helper and restriction | + +These claims are limited to the supported fragment and its preconditions. Selecting +UTF-16 does not add regular expressions, normalization, locale-aware operations, +or unrestricted JavaScript argument coercions. `split` remains a trusted axiom. + +Case conversion handles ASCII letters only, leaves non-ASCII letters unchanged, +and preserves length. It can differ from JavaScript: `"ß".toUpperCase()` is +`"SS"` in JavaScript. + +`stdlib` emits `Std.Collections.Seq.Filter/All/FoldLeft`; `local` emits the +recursive `SeqFilter/SeqAll/SeqFoldLeft` helpers on demand. The choice is visible +in generated definitions and calls, so it needs no separate artifact marker. + +## Proof interpretation and verification + +Every file selecting UTF-16 receives this generated header, even if its +declarations contain no string types: ```dafny // Generated by lsc from foo.ts // lsc options: string-semantics=javascript-utf16 ``` -Under the default the header is `// Generated by lsc from foo.ts`, unchanged, and no example -or case-study file regenerates. - -- The `lsc options:` line lists only non-default options that materially affected the file, - exactly as §5 specifies. `string-semantics=javascript-utf16` appears only when the file uses - `string` — DESIGN_CONFIG.md already decided this ("the header marker would only be emitted - when strings actually appear") — and is tied to emission the way #211's flag is - (`dafny-emit.ts`: "Keep this tied to emission, rather than a textual scan"). -- There is no second prose line. §5 asks that each option not invent another sentence, so the - claim sentences of §3 live in SPEC_DAFNY.md §4 keyed by identity (`unicode-scalar-1`, - `javascript-utf16-1`); that is where a reader of a standalone `.dfy` is sent. The default's - identity is documented, not stamped. Stamping every artifact would touch 64 files today and - fail the case-study CI (§7), so if it is ever wanted it is a separate PR paired with a - regen sweep of every case study. -- The public value is `javascript-utf16`; the artifact identity is `javascript-utf16-1` - (DESIGN_NUMBERS's `javascript` / `ecma262-2026-v1` split). The suffix is internal (open - decision 4) and moves when the domain or an operation's meaning changes, so a later helper - change cannot silently alter what a standalone proof claims. -- `dafnyVerify` maps the token to flags (§6) and pins `--unicode-char:true` whenever no - `string-semantics=` token is present — including a `.dfy` with no `// Generated by lsc` - line at all. That resolves DESIGN_CONFIG.md open question 3: no warning, because such a - file was already verifying under that setting and the pin only makes it explicit. The - additions-only check already guarantees `.dfy` and `.dfy.gen` share the header, so flipping - the key in `lemmascript.json` surfaces as a generator change: `regen` three-way-merges the - new line 2 in, then verifies under the new flags. Measured with `dafnyRegen`: the merge is - clean when the proof's line 2 is unchanged generated text (`examples/toposort.dfy`, - collab-todo `domain.dfy`), and conflicts — reported, `.dfy` restored — when the proof - inserted its own line 2 (an `import opened Std.*` block as AGENTS.md prescribes, or a comment block as - `examples/countBadPairs.dfy` and `preorder.dfy` have). Opting in is a one-time manual merge - for such files. Reading flags from the artifact rather than the config is deliberate — a - fixture or a file pulled out of a repo still verifies correctly. - -## 6. Verifier flags — and why not `--allow-warnings` - -| Profile | Flags added by `dafnyVerify` | -|---|---| -| `unicode-scalar` | `--unicode-char:true` — an explicit pin of today's default. A default is not a pin; verifying under a changed setting would silently reinterpret every string obligation. | -| `javascript-utf16` | `--unicode-char:false --allow-deprecation` | - -`dafnyVerifyArgs` reads the generated header and supplies the flags above. Dafny -4.11 deprecates `--unicode-char:false`, so UTF-16 verification adds -`--allow-deprecation`. This suppresses deprecated-feature warnings, including the -character-mode warning; other warning categories remain fatal under the default -verification policy. - -Using `--allow-warnings` would also allow verification to succeed despite warnings -about contradictory assumptions or missing `{:axiom}` declarations. The narrower -flag preserves those checks. Measured on Dafny 4.11.0 with `unicode-char = false`, -`allow-deprecation = true`, and `allow-warnings = false`: a surrogate literal -verifies with no warning, while `requires false` under -`warn-contradictory-assumptions` still fails the run. Missing-`{:axiom}` (bodiless -`ensures`, `assume`), `{:verify false}`, and missing-trigger warnings also remain -fatal. This resolves [DESIGN_CONFIG.md](DESIGN_CONFIG.md) open question 2. - -Two facts that make this safe, both measured on Dafny 4.11.0. `--unicode-char:true` is -silent — only the `:false` value is warned as deprecated — so pinning the default costs -nothing. And `--standard-libraries` under `--unicode-char:false` is a hard CLI error -(`CLI: Error: cannot load /DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True`; -a second line names `/DafnyStandardLibraries-notarget.doo`; exit code 1, unaffected by -`--allow-warnings`), not a warning: Dafny itself refuses the misload, so #211's per-file fail-closed check (a UTF-16 file -whose *proof additions* import `Std.*`) is about giving a good message, not about soundness. - -## 7. The ladder - -One PR per rung, stacked, each landing only with its evidence. - -**Rung 0 — name the profile, make it configuration, pin the default.** No semantic change, -no artifact change. - -- `string-semantics` and `dafny-library` registry entries; `lsc config` reports both. - The emitter selects collection helpers from the library choice, not the string profile. -- `dafnyVerify` parses the `lsc options:` line; pins `--unicode-char:true` whenever no - `string-semantics=` token is present (a header-less `.dfy` gets the pin and no warning — - DESIGN_CONFIG.md open question 3); rejects a token naming an unknown or unimplemented value. -- Registering `string.indexOf` and `string.charCodeAt` in `builtins.ts` (§3) is deferred: - they type `unknown` today, and a registered return type changes emitted text. The profile - gate keys on the emitter's method-name dispatch, where both already live. -- A source literal containing an unpaired surrogate is refused at extraction under - `unicode-scalar`, with the source line. -- `javascript-utf16` is accepted by the parser and **rejected by every emitter** with a - message naming this document and rung 1 — a staged answer, not a silent no-op. -- No regeneration. The always-stamp variant would have meant: regenerate the examples, where - 32 of 70 `.dfy.gen` mention `string` and gain one header line, and their 32 checked-in - `.dfy` files gain the same line via regen — 64 files, the same 32 #211 stamps — and - `dafnyCheckDiff` reports the missing line as a modified generated line, so `lsc check` on - collab-todo's `domain.dfy.gen` (42 `string` occurrences, no `lemmascript.json`) fails this repo's - `case-studies-dafny` CI job (`.github/workflows/ci.yml`) until that repo regenerates. Rung 0 - does none of it. -- Docs: SPEC.md §7.6 table (one row, "File override: no"), SPEC_DAFNY.md §4 String helpers - (the two identity claim sentences from §3, keyed `unicode-scalar-1` / `javascript-utf16-1`) - and §5 flags, SUBSET.md's `string` row, TOOLS.md §Options, site `reference/cli.md`, - AGENTS.md's `Std.` auto-detect sentence (DESIGN_CONFIG.md §7 lists it; it gains the - `javascript-utf16` caveat with rung 1). - -Gate: existing examples and case studies verify byte-for-byte with no file changes; -`lsc config` shows the resolved profile; the verifier-flag test (§8) shows `--unicode-char:true` -in every `dafnyVerify` invocation that lacks the token; a `.dfy` carrying -`string-semantics=javascript-utf16` fails with the rung-1 message. - -**Rung 1 — `javascript-utf16`.** #211's emitter work, gated on the option: - -- `\uXXXX` escaping of every unit outside printable ASCII - (`escapeDafnyUTF16String`), so astral pairs and lone surrogates survive the UTF-8 file. -- `StringFromCharCode` precondition `0 <= n < 0x10000`. -- Preambles that mention chars vary with the mode (`IsJSWhitespace` must use `\u` escapes - under `unicode-char:false` and `\U{}` otherwise; Dafny rejects the other form). - `PREAMBLE_CODE` entries become `string | (options) => string`. -- `SeqFilter` / `SeqAll` / `SeqFoldLeft` helpers emitted under `dafny-library: "local"`, - which UTF-16 requires explicitly and Unicode-scalar projects may also select. -- `--unicode-char:false --allow-deprecation`; never `--allow-warnings`. -- Lean: hard error. - -Gate: #211's fixture verifies under the option — `"😀".length === 2`, -`charCodeAt(0) === 0xD83D`, `charCodeAt(1) === 0xDE00`, a lone surrogate has length 1, -slicing preserves the high surrogate, `String.fromCharCode(0xD83D)` round-trips — plus a -Node oracle agreeing on each; the `Std.*`-in-proof-additions negative fixture fails with a message naming -`string-semantics`; `unicode-scalar` output is byte-identical to rung 0; no case study -changes; flipping the key in a project regenerates every string-bearing artifact through -`regen`, with proofs that inserted their own line 2 reporting a conflict rather than a silent -merge (§5). - -**Later rungs** are new values on the same key, each with its own design and evidence: -`unicode-nfc` (equality as canonical equivalence through a versioned normalization summary, -for code using `normalize()`) and `grapheme` (`Intl.Segmenter` semantics through a versioned -segmentation summary). Their identities must carry the Unicode table version *range* they -hold on — segmentation moves between Unicode releases and runtimes mix them — never a single -engine pin. Casing beyond ASCII is a third summary with the non-length-preserving cases named. -None of these are scoped here. - -## 8. Test plan +Default artifacts retain their existing header. Without a string-model token, +verification explicitly uses Unicode-scalar mode. The verifier reads the saved +artifact, so its interpretation does not depend on later project-config changes. -- `tools/test-fixtures.sh`: a config fixture directory selecting each value; `lsc config` - grepped for the resolved profile; #211's positive fixture under `javascript-utf16`; the - negative Std fixture; an - unpaired-surrogate literal refused under `unicode-scalar`; a Lean rejection. -- A JavaScript runtime oracle for every operation in §3 on a boundary corpus — ASCII, BMP - non-ASCII, astral pairs, lone high and low surrogates, empty string, CR-LF — asserting the - `javascript-utf16` proof result equals Node's, and recording where `unicode-scalar` differs - so the documented claim is tested, not asserted. -- Golden header: #211's fixture's `lsc options:` line is pinned and diffed; `unicode-scalar` - example output is asserted header-identical to `main`. -- Verifier-flag test: `dafnyVerify` maps each token to exactly the flags in §6, pins - `--unicode-char:true` for a header without the token and for no header at all, and rejects - a `.dfy` whose token names an unknown value. +Header parsing rejects unknown models, duplicate options-header lines, and +duplicate string-model tokens. The additions-only check also compares the proof's +model with its generated companion. Proof additions cannot select a different +model, including during `regen --no-verify`. Changing the source setting requires +`regen` to merge the generated header into the proof before verification. -Differential tests support the model; they do not replace the Dafny proofs. +Unicode-scalar verification adds `--unicode-char:true`; UTF-16 adds +`--unicode-char:false --allow-deprecation`. Dafny 4.11 deprecates the latter +character mode, so deprecated-feature warnings are allowed while other warning +categories retain the default fatal policy. `--allow-warnings` is not needed. +UTF-16 proof additions importing `Std.*` are rejected with a compatibility error; +the collection-library setting does not control handwritten imports. -## 9. Open decisions +## Validation -1. *Resolved.* The `lsc options:` line appears only when the file uses `string` and the - profile is non-default. The emitter tracks string usage while generating declarations; - the always-on cost is measured in §7. There is no separate - `String model:` line. -2. Should `unicode-scalar` refuse `.length`, indexing, and `charCodeAt` on literals that - contain astral text (where the answer is knowably wrong), rather than stating the - difference in the profile's claim sentence (SPEC_DAFNY.md §4)? Refusal is safer; the - documented claim is what today's proofs already rely on. Rung 0 keeps the claim; rung 1 - may add the refusal as a warning. -3. *Resolved.* `dafny-library: "stdlib" | "local"` is an independent setting with project defaults and file overrides, - defaulting to `stdlib`. UTF-16 requires an explicit `local` choice; Unicode-scalar - projects can use either. Default output is preserved, and `Std.` detection stays - artifact-based (§4). -4. Should the identity suffix be part of the public value (`javascript-utf16-1` in - `lemmascript.json`) or internal, as DESIGN_NUMBERS proposes? This design keeps it internal. +Tests cover option defaults and overrides, dependency compatibility, literal +escaping and surrogate handling, helper selection, verifier flags, and header +validation. Frontend fixtures prove representative UTF-16 results for astral pairs +and lone surrogates. The helper-only regression also checks the JavaScript result. +Regression cases cover added model headers and strings introduced only by helpers. +Existing scalar examples retain their generated output. -## Primary references +## References -- [ECMAScript 2026 §6.1.4, The String Type](https://tc39.es/ecma262/multipage/ecmascript-data-types-and-values.html#sec-ecmascript-language-types-string-type) -- [ECMAScript 2026 §22.1, String Objects](https://tc39.es/ecma262/multipage/text-processing.html#sec-string-objects) -- [Dafny 4.11 — Strings and characters](https://dafny.org/v4.11.0/Compilation/StringsAndChars) -- [Dafny reference manual — escaped characters per `--unicode-char` mode](https://dafny.org/v4.11.0/DafnyRef/DafnyRef#sec-escaped-characters) and [§5.2.5 Characters](https://dafny.org/v4.11.0/DafnyRef/DafnyRef#sec-characters) -- [PRECIS framework (RFC 8264)](https://www.rfc-editor.org/rfc/rfc8264) — the named-string-profile pattern -- LemmaSwift `DESIGN_SWIFT_STRINGS.md` — the versioned-profile shape this design borrows (its four rungs are Swift-driven; none is scheduled here) +- [ECMAScript: The String Type](https://tc39.es/ecma262/multipage/ecmascript-data-types-and-values.html#sec-ecmascript-language-types-string-type) +- [Dafny 4.11: Strings and characters](https://dafny.org/v4.11.0/Compilation/StringsAndChars) diff --git a/SPEC.md b/SPEC.md index 8acd4d20..dcca3688 100644 --- a/SPEC.md +++ b/SPEC.md @@ -452,6 +452,10 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions: ### 3.2 Special Forms +The collection rows show the default `dafny-library: stdlib` setting. +With `local`, `SeqFilter` and `SeqAll` replace the corresponding +`Std.Collections.Seq` helpers (§7.6). + | Spec / TS | Lean | Dafny | |-----------|------|-------| | `arr.length` | `arr.size` | `\|arr\|` | @@ -486,8 +490,8 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions: | `Math.max(...s)` / `Math.min(...s)` | — | `MaxOfSeq(s)` / `MinOfSeq(s)` (requires `\|s\| > 0`) | | `perm(a, b)` (spec-only) | — | `Perm(a, b)` (preamble: `predicate Perm(a, b) { multiset(a) == multiset(b) }`) | | `arr.map((x) => e)` | `arr.map (fun x => e)` | `seq(\|arr\|, i requires 0 <= i < \|arr\| => var x := arr[i]; e)` (§3.7) | -| `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `SeqFilter((x) => e, arr)` | -| `arr.every((x) => e)` | `arr.all (fun x => e)` | `SeqAll(arr, (x) => e)` | +| `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `Std.Collections.Seq.Filter((x) => e, arr)` | +| `arr.every((x) => e)` | `arr.all (fun x => e)` | `Std.Collections.Seq.All(arr, (x) => e)` | | `arr.some((x) => e)` | `arr.any (fun x => e)` | `exists x :: x in arr && e` | | `arr.includes(x)` | `arr.contains x` | `(x in arr)` | | `arr.indexOf(x)` | — | `SeqIndexOf(arr, x)` (preamble) | @@ -668,8 +672,8 @@ The transform uses two strategies for translating `receiver.method(args)`: | `[...arr, e]` | `arrayPush` | `Array.push arr e` | `(arr + [e])` | | `arr.with(i, v)` | `arraySet` | `arr.set! i v` | `arr[i := v]` | | `arr.map(f)` | `map` | `arr.map f` | seq comprehension (§3.7) | -| `arr.filter(f)` | `filter` | `arr.filter f` | `SeqFilter(f, arr)` | -| `arr.every(f)` | `every` | `arr.all f` | `SeqAll(arr, f)` | +| `arr.filter(f)` | `filter` | `arr.filter f` | `Std.Collections.Seq.Filter(f, arr)` | +| `arr.every(f)` | `every` | `arr.all f` | `Std.Collections.Seq.All(arr, f)` | | `arr.some(f)` | `some` | `arr.any f` | `exists x :: x in arr && ...` | | `arr.includes(x)` | `includes` | `arr.contains x` | `(x in arr)` | | `arr.indexOf(x)` | `indexOf` | — | `SeqIndexOf(arr, x)` | @@ -682,6 +686,9 @@ The transform uses two strategies for translating `receiver.method(args)`: | `s.add(x)` | `setAdd` | `s.insert x` | `(s + {x})` | | `s.delete(x)` | `setDelete` | `s.erase x` | `(s - {x})` | +Dafny collection entries use the default `stdlib` setting; `local` uses +`SeqFilter` and `SeqAll` instead (§7.6). + The transform checks helper-function methods first, then dot-notation methods. If neither matches, it errors. ### 3.9 Map, Set, and Optional Narrowing diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index 76d6e2db..c98c5ad0 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -98,7 +98,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at | Helper | When | Purpose | |--------|------|---------| | `SeqIndexOf` | `arr.indexOf(x)` | First-index search (`-1` if absent) | -| `SeqFilter` / `SeqAll` / `SeqFoldLeft` | `filter` / `every` / `reduce` | Local recursive collection helpers (no Dafny standard-library dependency) | +| `SeqFilter` / `SeqAll` / `SeqFoldLeft` | `filter` / `every` / `reduce` with `dafny-library: local` | Local recursive collection helpers (no Dafny standard-library dependency) | | `SeqFindIndex` | `arr.findIndex(f)` | Predicate first-index search | | `SeqFind` | `arr.find(f)` | Predicate first-match search | | `SeqFindLast` | `arr.findLast(f)` | Predicate last-match search | @@ -120,14 +120,14 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at **String semantics.** Set `string-semantics` in `lemmascript.json` or a file's `//@ option` directive (SPEC.md §7.6). Proofs depend on the selected model: -| Profile | Setting | Meaning | -|---|---|---| -| `unicode-scalar-1` | `"unicode-scalar"` (default) | Strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` can differ from JavaScript for characters such as emoji. Unpaired surrogates are unsupported. | -| `javascript-utf16-1` | `"javascript-utf16"` | Strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, and `charCodeAt` match JavaScript. Requires `"dafny-library": "local"`. | +| Setting | Meaning | +|---|---| +| `"unicode-scalar"` (default) | Strings are Unicode scalar sequences. `.length`, indexing, `slice`, `charCodeAt`, and `indexOf` can differ from JavaScript for characters such as emoji. Unpaired surrogates are unsupported. | +| `"javascript-utf16"` | Strings are UTF-16 code-unit sequences. `.length`, indexing, `slice`, and `charCodeAt` use JavaScript code-unit positions and values; indexing and slicing retain the fragment's bounds obligations. Requires `"dafny-library": "local"`. | Both profiles support ASCII-only case conversion. `String.fromCharCode` requires a Unicode scalar in the default profile, or `0 <= n < 0x10000` in UTF-16 mode. -Generated string-bearing files record the UTF-16 setting in their header; +Generated files record every UTF-16 selection in their header; the default profile adds no `string-semantics` setting. **Collection helpers.** `dafny-library` selects standard-library helpers (`stdlib`, @@ -154,6 +154,9 @@ Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the ` header, even if the project configuration has changed. A file without a `string-semantics` header uses `unicode-scalar`. +Proof additions must preserve the generated file's string model. Conflicting or +duplicate model settings are errors, including when verification is skipped. + Proofs using `javascript-utf16` cannot import Dafny's precompiled standard library (`Std.*`); verification reports an error if they do. Proofs using `unicode-scalar` can use that library. diff --git a/TOOLS.md b/TOOLS.md index 079bc25e..331ac8ae 100644 --- a/TOOLS.md +++ b/TOOLS.md @@ -60,29 +60,26 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = ` `config.ts` owns the `OPTION_SPECS` registry, nearest-ancestor `lemmascript.json` discovery, JSON and `//@ option` validation, defaults, and cross-option checks. `lsc.ts` merges explicit project values with eligible -top-of-file overrides and resolves once per source file. It checks that source dependencies -share the root file's string model, following TypeScript-resolved imports/re-exports and -compiler-selected cross-file callees before their contracts are copied. Unrelated files -in the tsconfig are not checked. An explicit `--config` applies to dependencies too; -each file still applies its own directives. It passes the result -to extraction/emission; those phases never read config files. -`string-semantics` is consumed by the Dafny emitter (literal escaping, char-sensitive -preambles, and the `// lsc options:` header token) and by extraction -(surrogate literals under the default); `dafnyVerify` derives the char-mode flags from -that token, never from the config. `dafny-library` selects standard-library or local -collection helpers. `resolveOptions` rejects UTF-16 with the default or explicit `stdlib` -choice; callers must select `local` through config or file directives. Collection-library -choices may differ across dependencies. `emitDafnyFile` also applies this shared check to -programmatically supplied options. `proof-dir` is -consumed only by `lsc.ts`, which maps the complete Dafny companion set before -calling the unchanged Dafny command helpers. `TransformOptions` remains -backend-intrinsic pipeline configuration and is deliberately separate. +top-of-file overrides and resolves once per source file, then passes options to +extraction and emission. Those phases do not read config files. + +Before copying cross-file contracts, the CLI checks that dependencies share the +root's string model, following imports, re-exports, and selected callees. +`string-semantics` controls literal validation, Dafny character helpers, and the +saved model header. Verification reads that header and the additions-only gate +checks it against the generated companion. `dafny-library` independently selects +collection helpers; the shared compatibility check requires `local` for UTF-16. +See [DESIGN_STRINGS.md](DESIGN_STRINGS.md) for the model boundaries. + +`proof-dir` is consumed only by `lsc.ts`, which maps the complete Dafny companion +set before calling the command helpers. `TransformOptions` remains separate +backend-intrinsic pipeline configuration. ## 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, "filter")` → Lean: `arr.filter f`, Dafny: `Seq.Filter(f, arr)`. Unsupported `(type, method)` pairs error at emit time. +Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "filter")` → Lean: `arr.filter f`, Dafny: `Std.Collections.Seq.Filter(f, arr)` by default (`SeqFilter(f, arr)` with `dafny-library: local`). 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)`. diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 518ee4c4..9559e305 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -28,6 +28,18 @@ export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean { } } + // Proof additions must retain the model chosen by the generated companion. + try { + const generated = readStringSemantics(readFileSync(genPath, "utf-8")); + const proof = readStringSemantics(readFileSync(dfyPath, "utf-8")); + if (proof !== generated) { + throw new Error(`proof string-semantics=${proof} differs from generated string-semantics=${generated}`); + } + } catch (error) { + console.error(`ERROR: ${path.basename(dfyPath)}: ${error instanceof Error ? error.message : String(error)}`); + return false; + } + let diff = ""; try { diff = execFileSync( @@ -69,7 +81,22 @@ export function dafnyCheckDiff(genPath: string, dfyPath: string): boolean { return true; } -const OPTIONS_HEADER = /^\/\/ lsc options:(.*)$/m; +/** Read the saved model, rejecting ambiguous headers before verification. */ +function readStringSemantics(content: string): LscOptions["string-semantics"] { + const headers = [...content.matchAll(/^\/\/ lsc options:(.*)$/gm)]; + if (headers.length > 1) throw new Error("generated header: duplicate lsc options header (string-semantics must be unambiguous)"); + let model = DEFAULT_OPTIONS["string-semantics"]; + let seen = false; + for (const token of (headers[0]?.[1] ?? "").trim().split(/\s+/).filter(Boolean)) { + const eq = token.indexOf("="); + const key = eq < 0 ? token : token.slice(0, eq); + if (key !== "string-semantics") continue; + if (seen) throw new Error("generated header: duplicate string-semantics option"); + seen = true; + model = parseOptionValue(key, eq < 0 ? "" : token.slice(eq + 1), "generated header"); + } + return model; +} /** * Build verifier arguments from the generated file's `// lsc options:` header. @@ -80,18 +107,11 @@ const OPTIONS_HEADER = /^\/\/ lsc options:(.*)$/m; * Other warning categories remain fatal. */ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?: string): { args: string[]; error?: string } { - let stringSemantics: LscOptions["string-semantics"] = DEFAULT_OPTIONS["string-semantics"]; - const header = content.match(OPTIONS_HEADER); - for (const token of (header?.[1] ?? "").trim().split(/\s+/).filter(Boolean)) { - const eq = token.indexOf("="); - const key = eq < 0 ? token : token.slice(0, eq); - const value = eq < 0 ? "" : token.slice(eq + 1); - if (key !== "string-semantics") continue; - try { - stringSemantics = parseOptionValue(key, value, "generated header"); - } catch (error) { - return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` }; - } + let stringSemantics: LscOptions["string-semantics"]; + try { + stringSemantics = readStringSemantics(content); + } catch (error) { + return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` }; } const utf16 = stringSemantics === "javascript-utf16"; const usesStandardLibrary = content.includes("Std."); diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index d1756864..f738d339 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -39,7 +39,7 @@ function tyToDafny(ty: Ty): string { case "int": return "int"; case "real": return "real"; case "bool": return "bool"; - case "string": _usesStrings = true; return "string"; + case "string": return "string"; case "void": return "()"; case "array": return `seq<${tyToDafny(ty.elem)}>`; case "tuple": return `(${ty.elems.map(tyToDafny).join(", ")})`; @@ -278,7 +278,6 @@ function emitExpr(e: Expr): string { case "bigint": return e.value; case "bool": return e.value ? "true" : "false"; case "str": - _usesStrings = true; // Under the default profile the literal is written exactly as before; // only the UTF-16 profile needs code-unit escapes (DESIGN_STRINGS.md §3). return isUtf16() @@ -997,13 +996,8 @@ let _useSafeSlice = false; // Source of generated collection helpers, selected independently of string semantics. let _dafnyLibrary: LscOptions["dafny-library"] = DEFAULT_OPTIONS["dafny-library"]; -// The string profile this file is emitted under (DESIGN_STRINGS.md) and whether -// any generated declaration used `string`. Together they decide the -// `// lsc options:` header token that `dafnyVerify` maps to Dafny's char mode. -// Kept tied to emission, rather than a textual scan of the finished Dafny, so -// comments and proof additions cannot select the source-language model. +// The selected model controls literals, character helpers, and verifier flags. let _stringSemantics: LscOptions["string-semantics"] = DEFAULT_OPTIONS["string-semantics"]; -let _usesStrings = false; function isUtf16(): boolean { return _stringSemantics === "javascript-utf16"; } const POW2 = `function Pow2(n: int): int @@ -1627,8 +1621,6 @@ export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOpt _useSafeSlice = options["safe-slice"]; _stringSemantics = options["string-semantics"]; _dafnyLibrary = options["dafny-library"]; - // Reset before scanning types, including when the previous file failed to emit. - _usesStrings = false; resetDafnyNameCache(); buildRecordCtorMap(file.decls); _neededPreambles.clear(); @@ -1689,10 +1681,8 @@ export function emitDafnyFile(file: Module, tsFileName?: string, options: LscOpt // Build output with needed preambles const lines: string[] = []; if (tsFileName) lines.push(`// Generated by lsc from ${tsFileName}`); - // Non-default options that materially affected this file (DESIGN_CONFIG.md §5). - // `dafnyVerify` maps the token to Dafny's char mode; the default is documented - // in SPEC_DAFNY.md §4 rather than stamped, so existing artifacts do not change. - if (_usesStrings && isUtf16()) lines.push("// lsc options: string-semantics=javascript-utf16"); + // Record every UTF-16 selection, including strings introduced by helpers. + if (isUtf16()) lines.push("// lsc options: string-semantics=javascript-utf16"); for (const [key, code] of PREAMBLE_CODE) { if (_neededPreambles.has(key)) { lines.push(""); lines.push(typeof code === "function" ? code() : code); } } diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts index 48847363..9ae3ac59 100644 --- a/tools/tests/dafny-commands.test.ts +++ b/tools/tests/dafny-commands.test.ts @@ -102,6 +102,36 @@ test("javascript-utf16 selects code-unit chars and only the deprecation waiver", assert.deepEqual(args, ["verify", "--unicode-char:false", "--allow-deprecation"]); }); +for (const secondModel of ["unicode-scalar", "javascript-utf16"]) { + test(`duplicate proof options headers are rejected even when the second model is ${secondModel}`, () => { + const result = dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n" + + `// lsc options: string-semantics=${secondModel}\n`); + assert.deepEqual(result.args, []); + assert.match(result.error ?? "", /duplicate lsc options header/); + }); + test(`duplicate string model tokens are rejected even when the second model is ${secondModel}`, () => { + const result = dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16 " + + `string-semantics=${secondModel}\n`); + assert.deepEqual(result.args, []); + assert.match(result.error ?? "", /duplicate string-semantics option/); + }); +} + +test("proof additions cannot introduce UTF-16 over the generated scalar default", () => { + const generated = "// Generated by lsc from a.ts\nmethod M() {}\n"; + fixture(generated, "// lsc options: string-semantics=javascript-utf16\n" + generated, + (g, p) => assert.equal(dafnyCheckDiff(g, p), false)); +}); + +test("proof additions cannot override a generated UTF-16 header", () => { + const generated = "// Generated by lsc from a.ts\n" + + "// lsc options: string-semantics=javascript-utf16\nmethod M() {}\n"; + fixture(generated, "// lsc options: string-semantics=unicode-scalar\n" + generated, + (g, p) => assert.equal(dafnyCheckDiff(g, p), false)); + fixture(generated, generated + "\nlemma Proof() {}\n", + (g, p) => assert.equal(dafnyCheckDiff(g, p), true)); +}); + for (const reference of [ "import opened Std.Arithmetic.Mul", "function all(xs: seq): bool { Std.Collections.Seq.All(xs, x => x > 0) }", diff --git a/tools/tests/dafny-emit.test.ts b/tools/tests/dafny-emit.test.ts index b75ef143..d47ae07f 100644 --- a/tools/tests/dafny-emit.test.ts +++ b/tools/tests/dafny-emit.test.ts @@ -43,25 +43,10 @@ for (const [method, helper, resultType] of [ }); } -for (const [name, declaration] of [ - ["string type without literals", stringType], - ["nested string type", { kind: "type-alias", name: "Texts", target: { - kind: "optional", inner: { kind: "array", elem: { kind: "string" } }, - } }], - ["string literals without string annotations", { kind: "const", name: "same", type: { kind: "bool" }, value: { - kind: "binop", op: "==", left: { kind: "str", value: "hello" }, right: { kind: "str", value: "hello" }, - } }], -] satisfies [string, Decl][]) { - test(`string usage resets between files after ${name}`, () => { - const baseline = emitDafnyFile(numbers, "numbers.ts", utf16); - assert.doesNotMatch(baseline, optionsHeader); - assert.match(emitDafnyFile(moduleWith(declaration), "strings.ts", utf16), optionsHeader); - assert.equal(emitDafnyFile(numbers, "numbers.ts", utf16), baseline); - }); -} - -test("string usage remains set across declarations within one file", () => { - assert.match(emitDafnyFile(moduleWith(stringType, ...numbers.decls), "mixed.ts", utf16), optionsHeader); +test("UTF-16 stamps numeric-only modules so proof additions use the selected model", () => { + assert.match(emitDafnyFile(numbers, "numbers.ts", utf16), optionsHeader); + assert.doesNotMatch(emitDafnyFile(numbers, "numbers.ts"), optionsHeader); + assert.match(emitDafnyFile(numbers, "numbers.ts", utf16), optionsHeader); }); test("string profile and literal encoding reset between files", () => { @@ -90,7 +75,7 @@ test("string helper preambles do not leak into the next file", () => { }); for (const inNamespace of [false, true]) { - test(`string usage resets after failed emission${inNamespace ? " inside a namespace" : ""}`, () => { + test(`string profile resets after failed emission${inNamespace ? " inside a namespace" : ""}`, () => { const baseline = emitDafnyFile(numbers, "numbers.ts", utf16); const declarations: Decl[] = [stringType, { kind: "const", name: "unsupported", type: { kind: "int" }, value: { diff --git a/tools/tests/dafny-string-profile.test.ts b/tools/tests/dafny-string-profile.test.ts new file mode 100644 index 00000000..3d3eb2a8 --- /dev/null +++ b/tools/tests/dafny-string-profile.test.ts @@ -0,0 +1,99 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { spawnSync } from "node:child_process"; +import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { createRequire } from "node:module"; +import { tmpdir } from "node:os"; +import { delimiter, join } from "node:path"; +import { fileURLToPath } from "node:url"; + +const cli = fileURLToPath(new URL("../src/lsc.ts", import.meta.url)); +const loader = createRequire(import.meta.url).resolve("tsx"); +const utf16 = "//@ option string-semantics javascript-utf16\n//@ option dafny-library local\n"; +const header = "// lsc options: string-semantics=javascript-utf16\n"; +const posixOnly = { skip: process.platform === "win32" }; + +function fixture(source: string, useFakeVerifier: boolean, run: (f: { + dir: string; proof: string; gen: string; marker: string; + cli: (args: string[]) => { status: number | null; output: string }; +}) => void): void { + const dir = realpathSync(mkdtempSync(join(tmpdir(), "lsc-string-profile-"))); + try { + writeFileSync(join(dir, "source.ts"), source); + const marker = join(dir, "verifier-called"); + const env = { ...process.env, LSC_TEST_VERIFIER_MARKER: marker }; + if (useFakeVerifier) { + const bin = join(dir, "bin"); + mkdirSync(bin); + const verifier = join(bin, "dafny"); + writeFileSync(verifier, '#!/bin/sh\nprintf "called\\n" > "$LSC_TEST_VERIFIER_MARKER"\nexit 0\n'); + chmodSync(verifier, 0o755); + env.PATH = `${bin}${delimiter}${env.PATH ?? ""}`; + } + run({ dir, proof: join(dir, "source.dfy"), gen: join(dir, "source.dfy.gen"), marker, + cli(args) { + const result = spawnSync(process.execPath, ["--import", loader, cli, + ...args, "--backend=dafny", "--time-limit=10", "source.ts"], { + cwd: dir, env, encoding: "utf8", timeout: 60_000, + }); + assert.ifError(result.error); + return { status: result.status, output: result.stdout + result.stderr }; + }, + }); + } finally { + rmSync(dir, { recursive: true, force: true }); + } +} + +const lengthSource = "export function codeUnitLength(value: string): number { return value.length; }\n"; +for (const command of [["check"], ["gen-check"], ["regen"], ["regen", "--no-verify"]]) { + for (const profile of ["javascript-utf16", "unicode-scalar"]) { + test(`${command.join(" ")}: proof additions cannot change the generated ${profile} model`, posixOnly, () => { + fixture("//@ backend dafny\n" + (profile === "javascript-utf16" ? utf16 : "") + lengthSource, true, f => { + const generated = f.cli(["gen"]); + assert.equal(generated.status, 0, generated.output); + const original = readFileSync(f.proof, "utf8"); + const override = profile === "javascript-utf16" + ? "// lsc options: string-semantics=unicode-scalar\n" + : header; + const claim = profile === "javascript-utf16" + ? 'lemma WrongLength() ensures codeUnitLength("😀") == 1 {}\n' + : 'lemma ChangedModel() ensures codeUnitLength("\\uD83D\\uDE00") == 2 {}\n'; + writeFileSync(f.proof, override + original + "\n" + claim); + const result = f.cli(command); + assert.equal(result.status, 1, result.output); + assert.match(result.output, /string-semantics|duplicate lsc options header/); + assert.equal(existsSync(f.marker), false, "the model guard must reject the proof before invoking Dafny"); + assert.equal(readFileSync(f.gen, "utf8"), original); + }); + }); + } +} + +test("ordinary UTF-16 proof additions still reach the verifier", posixOnly, () => { + fixture("//@ backend dafny\n" + utf16 + lengthSource, true, f => { + const generated = f.cli(["gen"]); + assert.equal(generated.status, 0, generated.output); + writeFileSync(f.proof, readFileSync(f.proof, "utf8") + + '\nlemma CorrectLength() ensures codeUnitLength("😀") == 2 {}\n'); + const result = f.cli(["check"]); + assert.equal(result.status, 0, result.output); + assert.equal(existsSync(f.marker), true); + }); +}); + +test("numeric-returning surrogate operations verify through the frontend in UTF-16 mode", () => { + const source = "//@ backend dafny\n" + utf16 + `export function surrogateCode(): number { + //@ verify + //@ ensures \\result === 0xD800 + return String.fromCharCode(0xD800).charCodeAt(0); +} +`; + assert.equal(String.fromCharCode(0xD800).charCodeAt(0), 0xD800); + fixture(source, false, f => { + const result = f.cli(["check"]); + assert.equal(result.status, 0, result.output); + assert.match(result.output, /0 errors/); + assert.ok(readFileSync(f.gen, "utf8").includes(header)); + }); +}); From 0c78eab030bc3ce4bb27187f902f1a2b32958be9 Mon Sep 17 00:00:00 2001 From: stevenguyen-hiya Date: Wed, 30 Sep 2026 13:50:52 -0700 Subject: [PATCH 14/15] Ignore literals and comments in Dafny library detection --- AGENTS.md | 2 +- SPEC_DAFNY.md | 2 +- tools/src/dafny-commands.ts | 58 +++++++++++++++++++++++- tools/tests/dafny-commands.test.ts | 39 ++++++++++++++++ tools/tests/dafny-string-profile.test.ts | 23 ++++++++++ 5 files changed, 121 insertions(+), 3 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 52738d7c..4f42da34 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -103,7 +103,7 @@ import opened Std.Arithmetic.DivMod // LemmaMulStrictInequality(x,y,z): x=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. (Exception: a project with `"string-semantics": "javascript-utf16"` cannot use `Std.*` — Dafny's standard library does not load under `--unicode-char:false`; `lsc check` refuses the combination with a message naming the key.) 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. +`lsc`'s `dafnyVerify` (`tools/dist/dafny-commands.js`) **auto-adds `--standard-libraries` for `Std`-qualified code references, ignoring literals and comments** — so an `import opened` is all you need; no CLI flag or config change, and `lsc check` picks it up. (Exception: a project with `"string-semantics": "javascript-utf16"` cannot use `Std.*` — Dafny's standard library does not load under `--unicode-char:false`; `lsc check` refuses the combination with a message naming the key.) 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 diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index c98c5ad0..f9f4c173 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -148,7 +148,7 @@ Both settings support file directives; see [examples/utf16.ts](examples/utf16.ts 2. Check additions-only invariant 3. Run `dafny verify foo.dfy` -Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the `--standard-libraries` flag is added. +Standard libraries are auto-detected from `Std`-qualified code references, including imports and calls; string/character literals and comments are ignored. The `--standard-libraries` flag is added when a reference is found. `lsc` verifies each `.dfy` using the string semantics recorded in its generated header, even if the project configuration has changed. A file without a diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 9559e305..73d4aa7c 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -98,6 +98,62 @@ function readStringSemantics(content: string): LscOptions["string-semantics"] { return model; } +/** Detect Std-qualified code references, not text inside literals or comments. */ +function usesDafnyStandardLibrary(content: string): boolean { + const identifier = /[A-Za-z0-9_'?]+/y; + const character = /'(?:[^\uD800-\uDFFF'\\\r\n]|\\(?:['"\\0nrt]|u[\da-fA-F]{4}|U\{[\da-fA-F](?:_?[\da-fA-F])*\}))'/uy; + let i = 0; + let std = false; + while (i < content.length) { + if (/\s/.test(content[i])) { i++; continue; } + if (content.startsWith("//", i)) { + const newline = content.indexOf("\n", i + 2); + i = newline < 0 ? content.length : newline + 1; + continue; + } + if (content.startsWith("/*", i)) { + let depth = 1; + i += 2; + while (i < content.length && depth > 0) { + if (content.startsWith("/*", i)) { depth++; i += 2; } + else if (content.startsWith("*/", i)) { depth--; i += 2; } + else i++; + } + continue; + } + const verbatim = content.startsWith('@"', i); + if (verbatim || content[i] === '"') { + std = false; + i += verbatim ? 2 : 1; + while (i < content.length) { + if (verbatim && content.startsWith('""', i)) { i += 2; } + else if (content[i] === '"') { i++; break; } + else if (!verbatim && content[i] === "\\") i += 2; + else i++; + } + continue; + } + // Apostrophes also occur in identifiers; use the longest token match. + identifier.lastIndex = character.lastIndex = i; + const word = identifier.exec(content); + const char = content[i] === "'" ? character.exec(content) : null; + if (char && (!word || char[0].length >= word[0].length)) { + std = false; + i = character.lastIndex; + continue; + } + if (word) { + std = word[0] === "Std"; + i = identifier.lastIndex; + continue; + } + if (std && content[i] === "." && !content.startsWith("..", i)) return true; + std = false; + i++; + } + return false; +} + /** * Build verifier arguments from the generated file's `// lsc options:` header. * Reading the saved string model instead of the current project config keeps @@ -114,7 +170,7 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` }; } const utf16 = stringSemantics === "javascript-utf16"; - const usesStandardLibrary = content.includes("Std."); + const usesStandardLibrary = usesDafnyStandardLibrary(content); if (utf16 && usesStandardLibrary) { return { args: [], error: "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " + diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts index 9ae3ac59..384d5380 100644 --- a/tools/tests/dafny-commands.test.ts +++ b/tools/tests/dafny-commands.test.ts @@ -135,6 +135,16 @@ test("proof additions cannot override a generated UTF-16 header", () => { for (const reference of [ "import opened Std.Arithmetic.Mul", "function all(xs: seq): bool { Std.Collections.Seq.All(xs, x => x > 0) }", + "import opened Std \n . Arithmetic.Mul", + "import opened Std /* proof comment */ .Arithmetic.Mul", + "import opened Std // proof comment\n .Arithmetic.Mul", + "import opened Std /* outer /* nested */ comment */ .Arithmetic.Mul", + "function value'(): int { Std.Arithmetic.Mul.Value() }", + String.raw`const quote: char := '"'; function value(): int { Std.Arithmetic.Mul.Value() }`, + String.raw`const quote: char := '\''; function value(): int { Std.Arithmetic.Mul.Value() }`, + String.raw`const character: char := '\u0053'; function value(): int { Std.Arithmetic.Mul.Value() }`, + String.raw`const character: char := '\U{1_F600}'; function value(): int { Std.Arithmetic.Mul.Value() }`, + "function value<'T>(): int { Std.Arithmetic.Mul.Value() }", ]) { test(`UTF-16 library diagnostic explains local helpers and proof additions: ${reference}`, () => { const { args, error } = dafnyVerifyArgs(`// lsc options: string-semantics=javascript-utf16\n${reference}\n`); @@ -144,6 +154,35 @@ for (const reference of [ assert.match(error ?? "", /\/\/@ option dafny-library local/); assert.match(error ?? "", /lsc regen/); assert.match(error ?? "", /does not rewrite handwritten Std\.\* imports or calls/); + assert.deepEqual(dafnyVerifyArgs(reference).args, + ["verify", "--standard-libraries", "--unicode-char:true"]); + }); +} + +for (const [description, content] of [ + ["ordinary string", 'const text: string := "Std.";'], + ["escaped quotes", String.raw`const text: string := "quoted \"Std.\" text";`], + ["escaped backslash before a quote", String.raw`const text: string := "backslash \\"; // Std.`], + ["verbatim string", 'const text: string := @"quoted ""Std."" text";'], + ["multiline verbatim string", 'const text: string := @"first line\nStd. on second line";'], + ["line comment", "// Std.Arithmetic.Mul\nmethod M() {}"], + ["block comment", "/* import opened Std.Arithmetic.Mul */\nmethod M() {}"], + ["nested block comment", "/* outer /* Std.Arithmetic.Mul */ still a comment */\nmethod M() {}"], + ["escaped character literal", String.raw`const quote: char := '\''; // Std.`], + ["identifier suffix", "function f(): bool { NotStd.Collections.Seq.All([]) }"], + ["identifier prefix", "function f(): bool { _Std.Collections.Seq.All([]) }"], + ["digit suffix", "function f(): bool { Std2.Collections.Seq.All([]) }"], + ["prime identifier", "function f(): bool { Std'.Collections.Seq.All([]) }"], + ["question-mark identifier", "function f(): bool { Std?.Collections.Seq.All([]) }"], + ["leading-apostrophe identifier", "function f(): bool { 'Std.Collections.Seq.All([]) }"], + ["longest-match apostrophe identifier", "function f(): bool { 'x'Std.Collections.Seq.All([]) }"], + ["sequence slice bound", "function slice(s: seq, Std: int): seq requires 0 <= Std <= |s| { s[Std..] }"], +]) { + test(`Std. in ${description} does not select the standard library`, () => { + assert.deepEqual(dafnyVerifyArgs(content), + { args: ["verify", "--unicode-char:true"] }); + assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n" + content), + { args: ["verify", "--unicode-char:false", "--allow-deprecation"] }); }); } diff --git a/tools/tests/dafny-string-profile.test.ts b/tools/tests/dafny-string-profile.test.ts index 3d3eb2a8..0b15d9c5 100644 --- a/tools/tests/dafny-string-profile.test.ts +++ b/tools/tests/dafny-string-profile.test.ts @@ -97,3 +97,26 @@ test("numeric-returning surrogate operations verify through the frontend in UTF- assert.ok(readFileSync(f.gen, "utf8").includes(header)); }); }); + +test("Std. text and proof comments verify through the frontend in UTF-16 mode", () => { + const source = "//@ backend dafny\n" + utf16 + `export function literalLength(): number { + //@ verify + //@ ensures \\result === 4 + return "Std.".length; +} +`; + assert.equal("Std.".length, 4); + fixture(source, false, f => { + const generated = f.cli(["gen"]); + assert.equal(generated.status, 0, generated.output); + const original = readFileSync(f.proof, "utf8"); + assert.ok(original.includes(header)); + assert.ok(original.includes('"Std."')); + writeFileSync(f.proof, original + '\n// Std.Arithmetic.Mul is only text, not an import.\n' + + '/* A nested /* Std.Collections.Seq.All */ proof comment. */\n'); + const result = f.cli(["check"]); + assert.equal(result.status, 0, result.output); + assert.match(result.output, /0 errors/); + assert.equal(readFileSync(f.gen, "utf8"), original); + }); +}); From 258973e96e0a7e04db99edbcde1fe93739493b6b Mon Sep 17 00:00:00 2001 From: Steve Nguyen <129918147+quangng2000@users.noreply.github.com> Date: Wed, 30 Sep 2026 17:47:38 -0700 Subject: [PATCH 15/15] Revert "Ignore literals and comments in Dafny library detection" This reverts commit 0c78eab030bc3ce4bb27187f902f1a2b32958be9. --- AGENTS.md | 2 +- SPEC_DAFNY.md | 2 +- tools/src/dafny-commands.ts | 58 +----------------------- tools/tests/dafny-commands.test.ts | 39 ---------------- tools/tests/dafny-string-profile.test.ts | 23 ---------- 5 files changed, 3 insertions(+), 121 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 4f42da34..52738d7c 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -103,7 +103,7 @@ import opened Std.Arithmetic.DivMod // LemmaMulStrictInequality(x,y,z): x=0 && p>0 ==> (m*p)%p == 0 ``` -`lsc`'s `dafnyVerify` (`tools/dist/dafny-commands.js`) **auto-adds `--standard-libraries` for `Std`-qualified code references, ignoring literals and comments** — so an `import opened` is all you need; no CLI flag or config change, and `lsc check` picks it up. (Exception: a project with `"string-semantics": "javascript-utf16"` cannot use `Std.*` — Dafny's standard library does not load under `--unicode-char:false`; `lsc check` refuses the combination with a message naming the key.) 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. +`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. (Exception: a project with `"string-semantics": "javascript-utf16"` cannot use `Std.*` — Dafny's standard library does not load under `--unicode-char:false`; `lsc check` refuses the combination with a message naming the key.) 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 diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md index f9f4c173..c98c5ad0 100644 --- a/SPEC_DAFNY.md +++ b/SPEC_DAFNY.md @@ -148,7 +148,7 @@ Both settings support file directives; see [examples/utf16.ts](examples/utf16.ts 2. Check additions-only invariant 3. Run `dafny verify foo.dfy` -Standard libraries are auto-detected from `Std`-qualified code references, including imports and calls; string/character literals and comments are ignored. The `--standard-libraries` flag is added when a reference is found. +Standard libraries are auto-detected: if `foo.dfy` contains `import Std.`, the `--standard-libraries` flag is added. `lsc` verifies each `.dfy` using the string semantics recorded in its generated header, even if the project configuration has changed. A file without a diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts index 73d4aa7c..9559e305 100644 --- a/tools/src/dafny-commands.ts +++ b/tools/src/dafny-commands.ts @@ -98,62 +98,6 @@ function readStringSemantics(content: string): LscOptions["string-semantics"] { return model; } -/** Detect Std-qualified code references, not text inside literals or comments. */ -function usesDafnyStandardLibrary(content: string): boolean { - const identifier = /[A-Za-z0-9_'?]+/y; - const character = /'(?:[^\uD800-\uDFFF'\\\r\n]|\\(?:['"\\0nrt]|u[\da-fA-F]{4}|U\{[\da-fA-F](?:_?[\da-fA-F])*\}))'/uy; - let i = 0; - let std = false; - while (i < content.length) { - if (/\s/.test(content[i])) { i++; continue; } - if (content.startsWith("//", i)) { - const newline = content.indexOf("\n", i + 2); - i = newline < 0 ? content.length : newline + 1; - continue; - } - if (content.startsWith("/*", i)) { - let depth = 1; - i += 2; - while (i < content.length && depth > 0) { - if (content.startsWith("/*", i)) { depth++; i += 2; } - else if (content.startsWith("*/", i)) { depth--; i += 2; } - else i++; - } - continue; - } - const verbatim = content.startsWith('@"', i); - if (verbatim || content[i] === '"') { - std = false; - i += verbatim ? 2 : 1; - while (i < content.length) { - if (verbatim && content.startsWith('""', i)) { i += 2; } - else if (content[i] === '"') { i++; break; } - else if (!verbatim && content[i] === "\\") i += 2; - else i++; - } - continue; - } - // Apostrophes also occur in identifiers; use the longest token match. - identifier.lastIndex = character.lastIndex = i; - const word = identifier.exec(content); - const char = content[i] === "'" ? character.exec(content) : null; - if (char && (!word || char[0].length >= word[0].length)) { - std = false; - i = character.lastIndex; - continue; - } - if (word) { - std = word[0] === "Std"; - i = identifier.lastIndex; - continue; - } - if (std && content[i] === "." && !content.startsWith("..", i)) return true; - std = false; - i++; - } - return false; -} - /** * Build verifier arguments from the generated file's `// lsc options:` header. * Reading the saved string model instead of the current project config keeps @@ -170,7 +114,7 @@ export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags? return { args: [], error: `ERROR: ${error instanceof Error ? error.message : String(error)}` }; } const utf16 = stringSemantics === "javascript-utf16"; - const usesStandardLibrary = usesDafnyStandardLibrary(content); + const usesStandardLibrary = content.includes("Std."); if (utf16 && usesStandardLibrary) { return { args: [], error: "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " + diff --git a/tools/tests/dafny-commands.test.ts b/tools/tests/dafny-commands.test.ts index 384d5380..9ae3ac59 100644 --- a/tools/tests/dafny-commands.test.ts +++ b/tools/tests/dafny-commands.test.ts @@ -135,16 +135,6 @@ test("proof additions cannot override a generated UTF-16 header", () => { for (const reference of [ "import opened Std.Arithmetic.Mul", "function all(xs: seq): bool { Std.Collections.Seq.All(xs, x => x > 0) }", - "import opened Std \n . Arithmetic.Mul", - "import opened Std /* proof comment */ .Arithmetic.Mul", - "import opened Std // proof comment\n .Arithmetic.Mul", - "import opened Std /* outer /* nested */ comment */ .Arithmetic.Mul", - "function value'(): int { Std.Arithmetic.Mul.Value() }", - String.raw`const quote: char := '"'; function value(): int { Std.Arithmetic.Mul.Value() }`, - String.raw`const quote: char := '\''; function value(): int { Std.Arithmetic.Mul.Value() }`, - String.raw`const character: char := '\u0053'; function value(): int { Std.Arithmetic.Mul.Value() }`, - String.raw`const character: char := '\U{1_F600}'; function value(): int { Std.Arithmetic.Mul.Value() }`, - "function value<'T>(): int { Std.Arithmetic.Mul.Value() }", ]) { test(`UTF-16 library diagnostic explains local helpers and proof additions: ${reference}`, () => { const { args, error } = dafnyVerifyArgs(`// lsc options: string-semantics=javascript-utf16\n${reference}\n`); @@ -154,35 +144,6 @@ for (const reference of [ assert.match(error ?? "", /\/\/@ option dafny-library local/); assert.match(error ?? "", /lsc regen/); assert.match(error ?? "", /does not rewrite handwritten Std\.\* imports or calls/); - assert.deepEqual(dafnyVerifyArgs(reference).args, - ["verify", "--standard-libraries", "--unicode-char:true"]); - }); -} - -for (const [description, content] of [ - ["ordinary string", 'const text: string := "Std.";'], - ["escaped quotes", String.raw`const text: string := "quoted \"Std.\" text";`], - ["escaped backslash before a quote", String.raw`const text: string := "backslash \\"; // Std.`], - ["verbatim string", 'const text: string := @"quoted ""Std."" text";'], - ["multiline verbatim string", 'const text: string := @"first line\nStd. on second line";'], - ["line comment", "// Std.Arithmetic.Mul\nmethod M() {}"], - ["block comment", "/* import opened Std.Arithmetic.Mul */\nmethod M() {}"], - ["nested block comment", "/* outer /* Std.Arithmetic.Mul */ still a comment */\nmethod M() {}"], - ["escaped character literal", String.raw`const quote: char := '\''; // Std.`], - ["identifier suffix", "function f(): bool { NotStd.Collections.Seq.All([]) }"], - ["identifier prefix", "function f(): bool { _Std.Collections.Seq.All([]) }"], - ["digit suffix", "function f(): bool { Std2.Collections.Seq.All([]) }"], - ["prime identifier", "function f(): bool { Std'.Collections.Seq.All([]) }"], - ["question-mark identifier", "function f(): bool { Std?.Collections.Seq.All([]) }"], - ["leading-apostrophe identifier", "function f(): bool { 'Std.Collections.Seq.All([]) }"], - ["longest-match apostrophe identifier", "function f(): bool { 'x'Std.Collections.Seq.All([]) }"], - ["sequence slice bound", "function slice(s: seq, Std: int): seq requires 0 <= Std <= |s| { s[Std..] }"], -]) { - test(`Std. in ${description} does not select the standard library`, () => { - assert.deepEqual(dafnyVerifyArgs(content), - { args: ["verify", "--unicode-char:true"] }); - assert.deepEqual(dafnyVerifyArgs("// lsc options: string-semantics=javascript-utf16\n" + content), - { args: ["verify", "--unicode-char:false", "--allow-deprecation"] }); }); } diff --git a/tools/tests/dafny-string-profile.test.ts b/tools/tests/dafny-string-profile.test.ts index 0b15d9c5..3d3eb2a8 100644 --- a/tools/tests/dafny-string-profile.test.ts +++ b/tools/tests/dafny-string-profile.test.ts @@ -97,26 +97,3 @@ test("numeric-returning surrogate operations verify through the frontend in UTF- assert.ok(readFileSync(f.gen, "utf8").includes(header)); }); }); - -test("Std. text and proof comments verify through the frontend in UTF-16 mode", () => { - const source = "//@ backend dafny\n" + utf16 + `export function literalLength(): number { - //@ verify - //@ ensures \\result === 4 - return "Std.".length; -} -`; - assert.equal("Std.".length, 4); - fixture(source, false, f => { - const generated = f.cli(["gen"]); - assert.equal(generated.status, 0, generated.output); - const original = readFileSync(f.proof, "utf8"); - assert.ok(original.includes(header)); - assert.ok(original.includes('"Std."')); - writeFileSync(f.proof, original + '\n// Std.Arithmetic.Mul is only text, not an import.\n' - + '/* A nested /* Std.Collections.Seq.All */ proof comment. */\n'); - const result = f.cli(["check"]); - assert.equal(result.status, 0, result.output); - assert.match(result.output, /0 errors/); - assert.equal(readFileSync(f.gen, "utf8"), original); - }); -});