emit unknown as opaque type in dafny

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 := *;

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 := *;

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;
 }

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;
 }

examples/todo-domain.dfy

@@ -2,6 +2,8 @@
 
 datatype Option<T> = None | Some(value: T)
 
+type Unknown(==, 0)
+
 method SetToSeq<T>(s: set<T>) returns (res: seq<T>)
   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<Action>
+function candidates(m: Unknown, a: Action): seq<Action>
 {
   if (a.MoveTask? && (!a.taskPlace.AtEnd?)) then
     [a, a.(taskPlace := Place.AtEnd)]

examples/todo-domain.dfy.gen

@@ -2,6 +2,8 @@
 
 datatype Option<T> = None | Some(value: T)
 
+type Unknown(==, 0)
+
 method SetToSeq<T>(s: set<T>) returns (res: seq<T>)
   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<Action>
+function candidates(m: Unknown, a: Action): seq<Action>
 {
   if (a.MoveTask? && (!a.taskPlace.AtEnd?)) then
     [a, a.(taskPlace := Place.AtEnd)]

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<T>(s: set<T>) returns (res: seq<T>)
 /** Preamble code keyed by name. Emitted in this order when needed. */
 const PREAMBLE_CODE: [string, string][] = [
   ["OptionType", "datatype Option<T> = 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],
@@ -1182,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<string>();
 
+  // 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[] = [];
@@ -1193,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";
@@ -1207,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";

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