Add configurable UTF-16 string semantics by quangng2000 · Pull Request #211 · midspiral/LemmaScript

quangng2000 · 2026-08-28T23:42:46Z

Adds opt-in UTF-16 semantics for supported JavaScript string operations, including astral text and lone surrogates. Unicode-scalar semantics remain the default.

For a standalone file:

//@ backend dafny
//@ option string-semantics javascript-utf16
//@ option dafny-library local

Both options also support project defaults in lemmascript.json. UTF-16 requires local collection helpers because Dafny's precompiled standard library uses Unicode-scalar characters. Imported source files must share the same string model.

Every generated UTF-16 file records its mode in the header. Proof additions cannot override that mode or introduce duplicate headers, including during regen --no-verify. Emitting the header unconditionally removes string-usage tracking and covers strings created only by helpers.

Standard-library detection checks Std-qualified code references, ignoring literals and comments. Ordinary text such as "Std." no longer rejects UTF-16/local proofs; genuine library imports and calls remain incompatible.

The existing fragment limits still apply: indexing and slicing have bounds obligations, case conversion is ASCII-only, split remains axiomatic, and Lean does not support UTF-16 mode.

The design document now describes the implemented behavior without speculative profiles or roadmap sections; collection tables distinguish the default standard library from opt-in local helpers.

Validated: build, example typecheck, all 187 unit tests, the full fixture suite, and real frontend/Dafny regressions for surrogate helpers and "Std." text with JavaScript result checks.

Closes #210.

namin · 2026-08-29T00:02:34Z

This seems like a reasonable change, but it's breaking. Many case studies need to be updated already. Let me ponder whether we need per-project configuration (as another PR).

…pt.json `string-semantics: "unicode-scalar" | "javascript-utf16"` (default `unicode-scalar`, config-only) replaces the presence-triggered marker: the first cut flipped every string-bearing file to UTF-16 and text-scanned the mark in the verifier, which reinterpreted every case study's obligations on merge. No config means today's output byte for byte — the 71 examples are drift-clean and no artifact changes. The artifact declares the model, not the config. A javascript-utf16 file that uses `string` carries `// lsc options: string-semantics=javascript-utf16` (the DESIGN_CONFIG.md §5 form); `dafnyVerify` pins the char mode either way — `--unicode-char:true` when the token is absent, since a default is not a pin, and `--unicode-char:false --allow-deprecation` when present. Only the `:false` value is deprecated in Dafny 4.11, and `--allow-deprecation` waives exactly that warning; the blanket `--allow-warnings` would also have un-fatalled vacuity and missing-{:axiom} warnings. Under javascript-utf16 the emitter writes non-ASCII units as `\uXXXX` escapes, `String.fromCharCode` admits `0 <= n < 0x10000`, `IsJSWhitespace` uses the `\u` escape form that mode requires, and filter/every/reduce use local helpers because the precompiled standard library cannot load under `--unicode-char:false` (a hard Dafny error). Under unicode-scalar each of those emits what it always has, and a source literal containing an unpaired surrogate is refused at extraction with its line rather than silently replaced by the UTF-8 writer. The profile is Dafny-only: Lean's String is scalar-based, so `--backend=lean` refuses it. Merges main (0.6.4) so the option registry is available; the earlier base predated tools/src/config.ts. Design: DESIGN_STRINGS.md.

namin

some minor comments. i find this change a bit invasive. not sure i am ready to merge.

namin · 2026-09-26T19:51:26Z

-  // as the single resolution gate: future dependent defaults (UTF-16 → local
-  // Dafny library) and incompatibilities belong here, before any consumer runs.
+  // There are no cross-option constraints in the registry: `string-semantics`
+  // selects the Dafny helper source by itself (DESIGN_STRINGS.md §4). Keep this


namin · 2026-09-26T19:52:03Z

+    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).",


no neef to ref DESIGN_STRINGS.md?

removed the reference.

namin · 2026-09-26T19:53:17Z

+
+/**
+ * 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


again not sure why we are referencing the doc? should make sense on its own

remove the reference.

namin · 2026-09-26T19:54:18Z

    case "real": return "real";
    case "bool": return "bool";
-    case "string": return "string";
+    case "string": _usesStrings = true; return "string";


need to make sure _usesStrings is reset properly

Reset is at the start of each files
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);

namin · 2026-09-26T19:55:18Z

        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") {
+          if (!isUtf16()) return `Std.Collections.Seq.All(${obj}, ${args[0]})`;


I would rather std-lib vs not for collections was a separate option, and utf16 forces one way

namin · 2026-09-26T20:14:42Z

+ * missing-{:axiom} warnings, which a verifier must keep fatal.
+ */
+export function dafnyVerifyArgs(content: string, timeLimit?: number, extraFlags?: string): { args: string[]; error?: string } {
+  let stringSemantics = "unicode-scalar";


why doesn't this use config.ts?

namin · 2026-09-26T20:33:22Z

 cp tools/fixtures/deterministic-extern-equality.ts "$fixture_dir/deterministic.ts"
 cp tools/fixtures/impure-extern-equality.ts "$fixture_dir/impure.ts"
 cp examples/safeSlice.ts "$fixture_dir/legacy-safe-slice.ts"
+cp -R tools/fixtures/utf16-project "$fixture_dir/utf16-project"


we should also have an ordinary example with the @ option directive

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.

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.

namin · 2026-09-28T18:41:22Z

+  const usesStandardLibrary = content.includes("Std.");
+  if (utf16 && usesStandardLibrary) {
+    return { args: [], error:
+      "ERROR: this proof combines \"string-semantics\": \"javascript-utf16\" with Dafny's standard library. " +


this seems misleading. should mention the local option

namin · 2026-09-29T00:33:35Z

 `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). Source dependencies must use the same


Source dependencies sentence unclear.

namin · 2026-09-29T00:34:06Z

 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:


it's not clear that this recommendation is not blanket

namin · 2026-09-29T00:35:20Z


-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`.
+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


dafnyVerify is an internal detail

namin · 2026-09-29T00:37:10Z

+`--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


this is providing justification for the setup?

namin · 2026-09-29T00:38:13Z

 | `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


this is not the default, right?

namin · 2026-10-01T00:15:58Z

 }

+/** Detect Std-qualified code references, not text inside literals or comments. */
+function usesDafnyStandardLibrary(content: string): boolean {


this change seems excessive for what it precents. let's just revert this commit.

namin · 2026-10-01T00:17:15Z

Hi @quangng2000 -- thanks for all your work here. This is almost ready to merge. Can you just revert the commit I flagged for revert? Then I'll do a final end-to-end review, and it should be ready to merge. Thanks, again!

This reverts commit 0c78eab.

fix: model JavaScript strings as UTF-16 in Dafny

e03456c

quangng2000 changed the title ~~Fix Dafny string semantics to match JavaScript UTF-16~~ Model JavaScript strings as a versioned profile selected in lemmascript.json Sep 22, 2026

quangng2000 force-pushed the codex/issue-210-js-utf16-strings branch from 8c1d8fb to 543c617 Compare September 26, 2026 03:14

namin reviewed Sep 26, 2026

View reviewed changes

quangng2000 added 6 commits September 27, 2026 15:34

docs: remove design reference from string option description

4b5ed70

docs: make configuration and verifier comments self-contained

8a5384a

fix: reuse config validation for Dafny string semantics

5e47d66

test: cover per-file Dafny string state reset

d911efe

namin reviewed Sep 28, 2026

View reviewed changes

fix: explain local library option in UTF-16 diagnostic

7fcf974

namin reviewed Sep 29, 2026

View reviewed changes

stevenguyen-hiya added 5 commits September 29, 2026 20:28

Clarify string verification documentation

09d0240

Clarify UTF-16 configuration scope

cb1d9c9

Simplify string profile documentation

74b8e34

Correct default string semantics documentation

4ec57ea

Simplify string model handling and protect proof headers

656533f

quangng2000 changed the title ~~Model JavaScript strings as a versioned profile selected in lemmascript.json~~ Add configurable UTF-16 string semantics Sep 30, 2026

Ignore literals and comments in Dafny library detection

0c78eab

namin reviewed Oct 1, 2026

View reviewed changes

Revert "Ignore literals and comments in Dafny library detection"

258973e

This reverts commit 0c78eab.

namin approved these changes Oct 1, 2026

View reviewed changes

namin merged commit 37eb3f2 into midspiral:main Oct 1, 2026
40 checks passed

Conversation

quangng2000 commented Aug 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

namin commented Aug 29, 2026

Uh oh!

namin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

namin commented Oct 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

quangng2000 commented Aug 28, 2026 •

edited

Loading