info --typed and version

SPEC.md

@@ -1256,7 +1256,9 @@ lsc check [--backend=lean|dafny] <file.ts>    — gen + verify
 lsc regen --backend=dafny <file.ts>           — regenerate with three-way merge (Dafny only)
 lsc extract <file.ts>                          — print Raw IR JSON (debugging)
 lsc info <file.ts>                             — write a JSON summary of verified functions (backend-neutral)
+lsc info --typed <file.ts>                     — print the machine-readable Typed IR contract (stdout)
 lsc claimcheck [<file.ts>]                     — check //@ contract prose vs //@ ensures (forwards to lemmascript-claimcheck)
+lsc version                                    — print the lemmascript package version
 ```
 
 Default backend is Dafny. `extract` and `info` are backend-neutral and always run, regardless of any `//@ backend` directive. With no `<file.ts>`, `gen`, `gen-check`, and `check` batch over the files listed in `LemmaScript-files.txt`.
@@ -1285,6 +1287,28 @@ Three-way merge when generated code changes. See [SPEC_DAFNY.md](SPEC_DAFNY.md).
 
 Extract-only (no resolve/transform/emit). Writes `foo.ts.json` next to the source, mapping each top-level function and class method (`ClassName.method`) to its signature and original `//@ requires` / `//@ ensures` / `//@ decreases` clause text. Backend-neutral.
 
+### 7.5 `info --typed`
+
+The machine-readable contract for satellite tools (e.g. differential/property
+testers): runs the front half of the pipeline (extract → resolve → narrow →
+autohavoc) and prints one JSON document to stdout — no file is written.
+Versioned by a top-level `schema` field (currently `1`) and stamped with the
+`lemmascript` package version for satellite version handshakes.
+
+Per module: resolved `typeDecls` (with field order and pre-computed types),
+`externs`, `constants`, and per function/class-method: parameter and return
+types as structured type trees, `requires`/`ensures` as resolved typed spec
+ASTs, `decreases`, `//@ contract` prose, `exported`, purity/`autohavoc` flags,
+and `bodyKinds` — a census of statement/expression kinds appearing in the body
+(with `assume` reported distinctly from `assert`), so consumers can classify
+functions (havoc/assume usage) without receiving bodies.
+
+The `dafny` section carries `emittedNames`, the source-name → emitted-Dafny-name
+map from an in-memory Dafny emission (so consumers never re-derive mangling
+rules); if that emission fails, it degrades to `{ "error": … }` without failing
+the command. Backend-neutral otherwise; the file's `//@ backend` directive is
+reported as `backendDirective`.
+
 ---
 
 ## 8. Pipeline

TOOLS.md

@@ -43,7 +43,7 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = `
 
 ## Phases
 
-**Extract** (`extract.ts`): ts-morph → Raw IR. Walks the TS AST, produces structured expression nodes. Only string outputs are `//@ ` annotation text. Two backend-neutral CLI commands stop here. `lsc extract foo.ts` dumps the Raw IR as JSON — external tools can consume it instead of re-parsing TS, e.g. [lemmascript-claimcheck](https://github.com/midspiral/lemmascript-claimcheck) reads each function's `//@ contract`, `requires`, and `ensures` to check the prose against the spec. `lsc info foo.ts` writes `foo.ts.json`, a per-function spec summary (`{ name: { sig, requires, ensures, decreases } }`, class methods keyed `Class.method`) — see `info-command.ts`.
+**Extract** (`extract.ts`): ts-morph → Raw IR. Walks the TS AST, produces structured expression nodes. Only string outputs are `//@ ` annotation text. Two backend-neutral CLI commands stop here. `lsc extract foo.ts` dumps the Raw IR as JSON — external tools can consume it instead of re-parsing TS, e.g. [lemmascript-claimcheck](https://github.com/midspiral/lemmascript-claimcheck) reads each function's `//@ contract`, `requires`, and `ensures` to check the prose against the spec. `lsc info foo.ts` writes `foo.ts.json`, a per-function spec summary (`{ name: { sig, requires, ensures, decreases } }`, class methods keyed `Class.method`) — see `info-command.ts`. `lsc info --typed foo.ts` goes further — through resolve/narrow/autohavoc — and prints the machine-readable Typed IR contract (typed signatures, spec ASTs, flags, body-kind census, emitted-Dafny-name map) to stdout for satellites like [lemmascript-crosscheck](https://github.com/midspiral/lemmascript-crosscheck); see SPEC.md §7.5.
 
 **Resolve** (`resolve.ts`): Raw IR → Typed IR. Resolves types from ts-morph type info and `//@ type` annotations. Classifies calls. Identifies discriminants. Rejects unsupported patterns. Parses `//@ ` annotations with the specparser. Carries narrowing context (env, `narrowedPaths`) so that the then-branch of `if (e !== undefined)` resolves with `e`'s unwrapped type — TS-faithful: simple vars and pure access paths (`a.b.c`, any depth) narrow. `&&` chains accumulate narrowings (each premise in scope for later ones); `==>` propagates premise narrowings into the conclusion. **Type narrowing only** — no structural rewriting.
 
@@ -274,5 +274,5 @@ The Dafny emitter wraps `if-then-else` and `let` (var-binding) expressions in pa
 | `dafny-emit.ts` | Emit | IR → Dafny text |
 | `lean-commands.ts` | CLI | Lean gen/check commands |
 | `dafny-commands.ts` | CLI | Dafny gen/gen-check/regen/check commands |
-| `info-command.ts` | CLI | `lsc info` — per-function spec summary JSON |
+| `info-command.ts` | CLI | `lsc info` — per-function spec summary JSON; `--typed` — Typed IR contract for satellites |
 | `lsc.ts` | CLI | Wires the pipeline, dispatches to backend |

tools/src/dafny-emit.ts

@@ -129,6 +129,14 @@ function resetDafnyNameCache(): void {
   }
 }
 
+/** Source-name → emitted-Dafny-name pairs from the most recent emitDafnyFile
+ *  call (identity-mapped names included). Consumed by `lsc info --typed` so
+ *  satellites (e.g. lemmascript-crosscheck) can address emitted declarations
+ *  by their mangled names (`_Box` → `i_Box'`) without re-deriving the rules. */
+export function emittedNameMap(): Map<string, string> {
+  return new Map([..._generatedDafnyNames, ..._userDafnyNames]);
+}
+
 function escapeName(name: string): string {
   // \result is carried through the IR as var "\\result"; render it as the
   // current method's out-parameter name (chosen locally by methodHeader).

tools/src/info-command.ts

@@ -12,6 +12,7 @@
 
 import { writeFileSync } from "fs";
 import type { RawFunction, RawModule } from "./rawir.js";
+import type { TFunction, TModule } from "./typedir.js";
 import { parseTsType, tyToCanonical } from "./types.js";
 
 interface FnInfo {
@@ -48,3 +49,90 @@ export function runInfo(raw: RawModule, outPath: string): void {
   writeFileSync(outPath, JSON.stringify(out, null, 2) + "\n");
   console.log(`Wrote ${outPath}`);
 }
+
+// ── `lsc info --typed` ───────────────────────────────────────
+//
+// Machine-readable contract for satellites (lemmascript-crosscheck): the
+// resolved Typed IR's signatures, spec ASTs, and flags — everything a tool
+// needs to derive generators and classify functions without importing the
+// pipeline. Printed to stdout (like `lsc extract`), versioned by `schema`.
+
+export interface TypedInfoDafny {
+  /** Source name → emitted Dafny name, from an in-memory Dafny emission. */
+  emittedNames?: Record<string, string>;
+  /** Present when the Dafny emission failed (e.g. Lean-only constructs). */
+  error?: string;
+}
+
+/** Statement/expression kinds present anywhere in a function body — a cheap
+ *  structural census so consumers can classify (havoc/assume/throw usage)
+ *  without receiving the whole body. */
+function bodyKinds(fn: TFunction): string[] {
+  // Keys under which a Ty (not a statement/expression) hangs — their `kind`
+  // tags belong to the type grammar and would pollute the census.
+  const TY_KEYS = new Set(["ty", "binderTy", "varTy", "nameTypes"]);
+  const kinds = new Set<string>();
+  const walk = (node: unknown): void => {
+    if (Array.isArray(node)) { node.forEach(walk); return; }
+    if (node && typeof node === "object") {
+      const o = node as Record<string, unknown>;
+      if (typeof o.kind === "string") {
+        kinds.add(o.kind === "assert" && o.assumed === true ? "assume" : o.kind);
+      }
+      for (const [k, v] of Object.entries(o)) if (!TY_KEYS.has(k)) walk(v);
+    }
+  };
+  walk(fn.body);
+  return [...kinds].sort();
+}
+
+function typedFn(fn: TFunction, rawFn: RawFunction | undefined) {
+  // Carry the original TS type string per parameter: Ty conflates types whose
+  // runtime shapes differ (Map<K,V> and Record<K,V> both map to kind "map"),
+  // and satellites that construct runtime values need to tell them apart.
+  const rawTsTypes = new Map((rawFn?.params ?? []).map(p => [p.name, p.tsType]));
+  return {
+    name: fn.name,
+    exported: rawFn?.exported ?? false,
+    typeParams: fn.typeParams,
+    params: fn.params.map(p => ({ ...p, tsType: rawTsTypes.get(p.name) })),
+    returnTy: fn.returnTy,
+    requires: fn.requires,
+    ensures: fn.ensures,
+    decreases: fn.decreases,
+    contract: rawFn?.contract ?? [],
+    isPure: fn.isPure,
+    forcePure: fn.forcePure,
+    autohavoc: fn.autohavoc,
+    bodyKinds: bodyKinds(fn),
+  };
+}
+
+export function runTypedInfo(
+  raw: RawModule,
+  typed: TModule,
+  version: string,
+  backendDirective: string | null,
+  dafny: TypedInfoDafny,
+): void {
+  const rawByName = new Map(raw.functions.map(f => [f.name, f]));
+  const rawMethods = new Map(
+    raw.classes.flatMap(c => c.methods.map(m => [`${c.name}.${m.name}`, m] as const)));
+  const out = {
+    schema: 1,
+    lemmascript: version,
+    file: typed.file,
+    backendDirective,
+    typeDecls: typed.typeDecls,
+    externs: typed.externs,
+    constants: typed.constants,
+    functions: typed.functions.map(f => typedFn(f, rawByName.get(f.name))),
+    classes: typed.classes.map(c => ({
+      name: c.name,
+      fields: c.fields,
+      methods: c.methods.map(m => typedFn(m, rawMethods.get(`${c.name}.${m.name}`))),
+    })),
+    dafny,
+  };
+  console.log(JSON.stringify(out, null, 2));
+}

tools/src/lsc.ts

@@ -17,14 +17,29 @@ import { autoHavocModule } from "./autohavoc.js";
 import { transformModuleLean, transformModuleDafny } from "./transform.js";
 import { peepholeModule } from "./peephole.js";
 import { emitLeanFile, resetLeanModule } from "./lean-emit.js";
-import { emitDafnyFile } from "./dafny-emit.js";
+import { emitDafnyFile, emittedNameMap } from "./dafny-emit.js";
 import { dafnyGen, dafnyCheckDiff, dafnyVerify, dafnyRegen } from "./dafny-commands.js";
 import { leanGen, leanCheck } from "./lean-commands.js";
-import { runInfo } from "./info-command.js";
+import { runInfo, runTypedInfo, type TypedInfoDafny } from "./info-command.js";
+
+/** Version of the lemmascript package — the root package.json sits two levels
+ *  above this module from both tools/src/ (tsx) and tools/dist/ (installed). */
+function lscVersion(): string {
+  const pkg = JSON.parse(readFileSync(new URL("../../package.json", import.meta.url), "utf8"));
+  return pkg.version as string;
+}
 
 function main() {
   const args = process.argv.slice(2);
 
+  // `lsc version` — print the package version. Machine consumers (satellites
+  // like lemmascript-claimcheck/-crosscheck) use this for their version
+  // handshake; keep the output to the bare semver string.
+  if (args[0] === "version") {
+    console.log(lscVersion());
+    return;
+  }
+
   // `lsc claimcheck <file.ts> …` forwards verbatim to the lemmascript-claimcheck
   // CLI (a dependency; its cli reads the rewritten process.argv). With no
   // leading <file.ts>, batch: one satellite run per LemmaScript-files.txt entry,
@@ -114,6 +129,15 @@ function main() {
     args.splice(noVerifyIdx, 1);
   }
 
+  // --typed (info only): print the machine-readable Typed IR contract to
+  // stdout instead of writing the human-oriented foo.ts.json.
+  let typedInfo = false;
+  const typedIdx = args.indexOf("--typed");
+  if (typedIdx >= 0) {
+    typedInfo = true;
+    args.splice(typedIdx, 1);
+  }
+
   // Anything flag-shaped left over is a typo or a space-separated form
   // (`--backend lean`): reject it rather than let it become a positional arg
   // or be silently ignored (which would e.g. verify with the wrong backend).
@@ -126,15 +150,21 @@ function main() {
   const [cmd, filePath] = args;
   if (!cmd) {
     console.error("Usage: lsc <gen|check|regen|extract|info> [--backend=lean|dafny] <file.ts>");
+    console.error("       lsc info --typed <file.ts>   (machine-readable Typed IR contract to stdout)");
     console.error("       lsc <gen|gen-check|check> [--backend=…] [--slow]   (no file: batch over LemmaScript-files.txt)");
     console.error("       lsc claimcheck [<file.ts>] [flags…]   (forwards to lemmascript-claimcheck)");
+    console.error("       lsc version");
+    process.exit(1);
+  }
+  if (typedInfo && cmd !== "info") {
+    console.error(`--typed is only valid with the info command (got: ${cmd})`);
     process.exit(1);
   }
   if (!filePath) {
     runBatch(cmd, backend, slow);
     return;
   }
-  runFile(cmd, filePath, backend, timeLimit, extraFlags, noVerify);
+  runFile(cmd, filePath, backend, timeLimit, extraFlags, noVerify, typedInfo);
 }
 
 // LemmaScript-files.txt, parsed: `filepath [timeout_in_seconds] [extra dafny
@@ -173,7 +203,7 @@ function runBatch(cmd: string, backend: "lean" | "dafny", slow: boolean) {
   }
 }
 
-function runFile(cmd: string, filePath: string, backend: "lean" | "dafny", timeLimit: number | undefined, extraFlags: string | undefined, noVerify = false) {
+function runFile(cmd: string, filePath: string, backend: "lean" | "dafny", timeLimit: number | undefined, extraFlags: string | undefined, noVerify = false, typedInfo = false) {
   const absPath = path.resolve(filePath);
   if (!existsSync(absPath)) {
     console.error(`File not found: ${absPath}`);
@@ -227,7 +257,7 @@ function runFile(cmd: string, filePath: string, backend: "lean" | "dafny", timeL
     return;
   }
 
-  if (cmd === "info") {
+  if (cmd === "info" && !typedInfo) {
     const outPath = path.join(path.dirname(absPath), `${path.basename(filePath, ".ts")}.ts.json`);
     runInfo(raw, outPath);
     return;
@@ -241,6 +271,26 @@ function runFile(cmd: string, filePath: string, backend: "lean" | "dafny", timeL
   // over-approximation). No-op unless a function opts in.
   const typed = autoHavocModule(narrowModule(resolved));
 
+  if (cmd === "info") {
+    // --typed: the satellite contract. Run an in-memory Dafny emission purely
+    // to harvest the emitted-name map; the file is backend-neutral otherwise,
+    // so a failure here (e.g. Lean-only constructs) degrades to an error note
+    // rather than failing the command.
+    let dafnyInfo: TypedInfoDafny;
+    try {
+      let { typesFile, defFile } = transformModuleDafny(typed);
+      if (typesFile) typesFile = peepholeModule(typesFile, "dafny");
+      defFile = peepholeModule(defFile, "dafny");
+      const merged = { ...defFile, decls: [...(typesFile?.decls ?? []), ...defFile.decls] };
+      emitDafnyFile(merged, path.basename(filePath), { safeSlice });
+      dafnyInfo = { emittedNames: Object.fromEntries(emittedNameMap()) };
+    } catch (err) {
+      dafnyInfo = { error: err instanceof Error ? err.message : String(err) };
+    }
+    runTypedInfo(raw, typed, lscVersion(), backendDirective ? backendDirective[1] : null, dafnyInfo);
+    return;
+  }
+
   const dir = path.dirname(absPath);
   const base = path.basename(filePath, ".ts");