Add configurable UTF-16 string semantics

AGENTS.md

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

DESIGN_STRINGS.md

@@ -0,0 +1,98 @@
+# DESIGN_STRINGS — Selectable Dafny string semantics
+
+**Status:** implemented in PR #211.
+**Issue:** [#210](https://github.com/midspiral/LemmaScript/issues/210) · **PR:** [#211](https://github.com/midspiral/LemmaScript/pull/211)
+
+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.
+
+## Models and configuration
+
+| 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
+```
+
+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.
+
+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.
+
+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.
+
+## Validation
+
+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.
+
+## References
+
+- [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)

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\|` |
@@ -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
@@ -1021,6 +1028,11 @@ 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` 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.
 
 **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).
@@ -1378,14 +1390,39 @@ 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` | yes (Dafny only) |
+| `dafny-library` | `stdlib` \| `local` | `stdlib` | yes (Dafny only) |
 
 Eligible settings use `//@ option <key> <value>` 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). `lsc config foo.ts` prints the config path, effective
+(see SPEC_DAFNY.md §1). `string-semantics` selects which model of JavaScript strings a
+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.
+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.
 
+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
+//@ 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

SPEC_DAFNY.md

@@ -98,6 +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` 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 |
@@ -116,6 +117,27 @@ 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 semantics.** Set `string-semantics` in `lemmascript.json` or a file's
+`//@ option` directive (SPEC.md §7.6). Proofs depend on the selected model:
+
+| 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 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`,
+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).
+
 ---
 
 ## 5. Verification
@@ -128,5 +150,15 @@ 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=<seconds>` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=<string>` is forwarded verbatim to `dafny verify`.
+`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`.
+
+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.
+
+The shared `--time-limit=<seconds>` flag (SPEC.md §7) maps to Dafny's `--verification-time-limit`; `--extra-flags=<string>` is forwarded verbatim to `dafny verify`.

SUBSET.md

@@ -34,7 +34,7 @@ Two things shape what you can verify:
 | `number` (non-integer literal) | real | `0.8`, `3.14` become reals; mixed int/real arithmetic coerces automatically. |
 | `bigint` | integer | Same as `number`; `32n`, `0xffffn` literals supported, exact past 2^53. |
 | `boolean` | bool | |
-| `string` | string | |
+| `string` | string | Modelled per the project's `string-semantics` (SPEC_DAFNY.md §4): Unicode scalars by default, UTF-16 code units under `"javascript-utf16"`. |
 | `T[]` / `Array<T>` / `readonly T[]` | sequence | |
 | `[A, B, ...]` (heterogeneous tuple) | tuple | Native tuple (`(A, B)` / `A × B`). Access needs a literal index (`t[0]`, `t[1]`); `const [a, b] = t` works. |
 | `[T, T, ...]` (homogeneous tuple) | sequence | Same-typed elements model as a `seq` (more capable than a fixed tuple). |

TOOLS.md

@@ -60,17 +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 passes the result
-to extraction/emission; those phases never read config files. `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)`.
 

examples/utf16.dfy

@@ -0,0 +1,38 @@
+// Generated by lsc from utf16.ts
+// lsc options: string-semantics=javascript-utf16
+
+predicate SeqAll<T>(xs: seq<T>, 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)
+{
+}