From 697dd6430dbfed1c485e836e3d47262b92c61331 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Tue, 30 Jun 2026 23:01:30 -0400 Subject: [PATCH 1/4] emit unknown as opaque type in dafny --- tools/src/dafny-emit.ts | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index d71adb6..f176c9d 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -21,7 +21,9 @@ function tyToDafny(ty: Ty): string { case "optional": { needPreamble("OptionType"); return `Option<${tyToDafny(ty.inner)}>`; } case "user": return ty.name; case "fn": return `(${ty.params.map(tyToDafny).join(", ")}) -> ${tyToDafny(ty.result)}`; - case "unknown": return "int"; + // Out-of-subset (`any`/`unknown`); opaque so real ops on it fail loudly + // rather than silently verify as `int`. Mirrors the Lean backend's `_`. + case "unknown": needPreamble("UnknownType"); return "Unknown"; } } @@ -1079,6 +1081,9 @@ const SET_TO_SEQ = `method SetToSeq(s: set) returns (res: seq) /** Preamble code keyed by name. Emitted in this order when needed. */ const PREAMBLE_CODE: [string, string][] = [ ["OptionType", "datatype Option = None | Some(value: T)"], + // Opaque carrier for `unknown`-typed values. `(==)` for compare/map-key/match; + // `(0)` (auto-init ⇒ nonempty) so `havoc` (`:= *`) is well-formed. + ["UnknownType", "type Unknown(==, 0)"], ["SetToSeq", SET_TO_SEQ], ["Pow2", POW2], ["BitAnd", BIT_AND], From eb2248266ea34494e6b53961319e3e00e3d181d4 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Tue, 30 Jun 2026 23:37:16 -0400 Subject: [PATCH 2/4] tweak about finding declared types --- tools/src/extract.ts | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 46f832a..98dd0de 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -1780,10 +1780,19 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot const nameNode = p.getNameNode(); if (Node.isObjectBindingPattern(nameNode)) { const type = p.getType(); + // `//@ declare-type` types are invisible to the TS checker, so + // `type.getProperty` finds nothing for them and the bindings would + // collapse to `unknown`. Fall back to the declared record's field types. + const declTypeName = p.getTypeNode()?.getText(); + const declFields = declTypeName + ? _synthArrayUnions?.find(d => d.name === declTypeName && d.kind === "record")?.fields + : undefined; return nameNode.getElements().map(el => { const name = el.getName(); const propType = type.getProperty(name)?.getTypeAtLocation(p); - return { name, tsType: propType ? typeToString(propType) : "unknown" }; + if (propType) return { name, tsType: typeToString(propType) }; + const declTy = declFields?.find(f => f.name === name)?.tsType; + return { name, tsType: declTy ?? "unknown" }; }); } // Syntactic union nodes go through _tsTypeFromUnionNode so synth fires From a2ce78948f63a480d433dc7292ea80b82072e6c0 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Tue, 30 Jun 2026 23:43:09 -0400 Subject: [PATCH 3/4] avoid preambules collected for unemitted declaration --- tools/src/dafny-emit.ts | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index f176c9d..d800042 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -1187,6 +1187,22 @@ export function emitDafnyFile(file: Module, tsFileName?: string, opts?: { safeSl // skipped when the corresponding pure def was actually emitted. const emittedPureDefs = new Set(); + // Emit a decl, rolling back any preamble requirements it registered if it + // throws. A skipped decl must contribute neither text nor preambles — else a + // side-effecting `needPreamble` from a half-emitted decl leaves an unused + // preamble (e.g. `type Unknown` from a skipped const whose head is + // `unknown`-typed but whose value expr is unsupported). + const emitDeclTx = (d: Decl): string => { + const saved = new Set(_neededPreambles); + try { + return emitDecl(d); + } catch (e) { + _neededPreambles.clear(); + for (const k of saved) _neededPreambles.add(k); + throw e; + } + }; + // Emit declarations const declLines: string[] = []; const skipped: string[] = []; @@ -1198,7 +1214,7 @@ export function emitDafnyFile(file: Module, tsFileName?: string, opts?: { safeSl for (const inner of decl.decls) { try { declLines.push(""); - declLines.push(emitDecl(inner)); + declLines.push(emitDeclTx(inner)); if (inner.kind === "def") emittedPureDefs.add(inner.name); } catch (e) { const name = "name" in inner ? inner.name : "unknown"; @@ -1212,7 +1228,7 @@ export function emitDafnyFile(file: Module, tsFileName?: string, opts?: { safeSl } try { declLines.push(""); - declLines.push(emitDecl(decl)); + declLines.push(emitDeclTx(decl)); if (decl.kind === "def-by-method") emittedPureDefs.add(decl.name); } catch (e) { const name = "name" in decl ? decl.name : "unknown"; From 9742a16f0014a6ca8c11978d78b2e74ab1926b36 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Wed, 1 Jul 2026 00:00:14 -0400 Subject: [PATCH 4/4] update examples --- examples/autohavoc.dfy | 6 ++++-- examples/autohavoc.dfy.gen | 6 ++++-- examples/inlineHandler.dfy | 8 +++++--- examples/inlineHandler.dfy.gen | 8 +++++--- examples/todo-domain.dfy | 4 +++- examples/todo-domain.dfy.gen | 4 +++- 6 files changed, 24 insertions(+), 12 deletions(-) diff --git a/examples/autohavoc.dfy b/examples/autohavoc.dfy index 388e605..5996568 100644 --- a/examples/autohavoc.dfy +++ b/examples/autohavoc.dfy @@ -1,5 +1,7 @@ // Generated by lsc from autohavoc.ts +type Unknown(==, 0) + 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) @@ -37,7 +39,7 @@ function validPath(path: string): bool !((StringIndexOf(path, "..") >= 0)) } -method loadEntry(req: int) returns (res: string) +method loadEntry(req: Unknown) returns (res: string) { var id: string := *; var filePath := (("./data/" + id) + ".json"); @@ -50,7 +52,7 @@ method loadEntry(req: int) returns (res: string) return entry.name; } -method mergeEntries(req: int) returns (res: string) +method mergeEntries(req: Unknown) returns (res: string) { var a: string := *; var b: string := *; diff --git a/examples/autohavoc.dfy.gen b/examples/autohavoc.dfy.gen index 388e605..5996568 100644 --- a/examples/autohavoc.dfy.gen +++ b/examples/autohavoc.dfy.gen @@ -1,5 +1,7 @@ // Generated by lsc from autohavoc.ts +type Unknown(==, 0) + 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) @@ -37,7 +39,7 @@ function validPath(path: string): bool !((StringIndexOf(path, "..") >= 0)) } -method loadEntry(req: int) returns (res: string) +method loadEntry(req: Unknown) returns (res: string) { var id: string := *; var filePath := (("./data/" + id) + ".json"); @@ -50,7 +52,7 @@ method loadEntry(req: int) returns (res: string) return entry.name; } -method mergeEntries(req: int) returns (res: string) +method mergeEntries(req: Unknown) returns (res: string) { var a: string := *; var b: string := *; diff --git a/examples/inlineHandler.dfy b/examples/inlineHandler.dfy index e3484d2..b039dad 100644 --- a/examples/inlineHandler.dfy +++ b/examples/inlineHandler.dfy @@ -1,5 +1,7 @@ // Generated by lsc from inlineHandler.ts +type Unknown(==, 0) + 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) @@ -35,16 +37,16 @@ function safePath(path: string): bool !((StringIndexOf(path, "..") >= 0)) } -method get_entries(req: int, res: int) returns (res_: int) +method get_entries(req: Unknown, res: Unknown) returns (res_: Unknown) { var id: string := *; var filePath := (("./entries/" + id) + ".json"); var i_t0 := safePath(filePath); if !(i_t0) { - var i_t1: int := *; + var i_t1: Unknown := *; return i_t1; } var contents := readSafe(filePath); - var i_t2: int := *; + var i_t2: Unknown := *; return i_t2; } diff --git a/examples/inlineHandler.dfy.gen b/examples/inlineHandler.dfy.gen index e3484d2..b039dad 100644 --- a/examples/inlineHandler.dfy.gen +++ b/examples/inlineHandler.dfy.gen @@ -1,5 +1,7 @@ // Generated by lsc from inlineHandler.ts +type Unknown(==, 0) + 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) @@ -35,16 +37,16 @@ function safePath(path: string): bool !((StringIndexOf(path, "..") >= 0)) } -method get_entries(req: int, res: int) returns (res_: int) +method get_entries(req: Unknown, res: Unknown) returns (res_: Unknown) { var id: string := *; var filePath := (("./entries/" + id) + ".json"); var i_t0 := safePath(filePath); if !(i_t0) { - var i_t1: int := *; + var i_t1: Unknown := *; return i_t1; } var contents := readSafe(filePath); - var i_t2: int := *; + var i_t2: Unknown := *; return i_t2; } diff --git a/examples/todo-domain.dfy b/examples/todo-domain.dfy index 0b63cf0..02d43c4 100644 --- a/examples/todo-domain.dfy +++ b/examples/todo-domain.dfy @@ -2,6 +2,8 @@ datatype Option = None | Some(value: T) +type Unknown(==, 0) + method SetToSeq(s: set) returns (res: seq) ensures forall x :: x in s <==> x in res ensures |res| == |s| @@ -308,7 +310,7 @@ function rebase(remote: Action, local: Action): Action } } -function candidates(m: int, a: Action): seq +function candidates(m: Unknown, a: Action): seq { if (a.MoveTask? && (!a.taskPlace.AtEnd?)) then [a, a.(taskPlace := Place.AtEnd)] diff --git a/examples/todo-domain.dfy.gen b/examples/todo-domain.dfy.gen index 0b63cf0..02d43c4 100644 --- a/examples/todo-domain.dfy.gen +++ b/examples/todo-domain.dfy.gen @@ -2,6 +2,8 @@ datatype Option = None | Some(value: T) +type Unknown(==, 0) + method SetToSeq(s: set) returns (res: seq) ensures forall x :: x in s <==> x in res ensures |res| == |s| @@ -308,7 +310,7 @@ function rebase(remote: Action, local: Action): Action } } -function candidates(m: int, a: Action): seq +function candidates(m: Unknown, a: Action): seq { if (a.MoveTask? && (!a.taskPlace.AtEnd?)) then [a, a.(taskPlace := Place.AtEnd)]