diff --git a/SPEC.md b/SPEC.md index a9a7c23..ba6cfc8 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1256,7 +1256,9 @@ lsc check [--backend=lean|dafny] — gen + verify lsc regen --backend=dafny — regenerate with three-way merge (Dafny only) lsc extract — print Raw IR JSON (debugging) lsc info — write a JSON summary of verified functions (backend-neutral) +lsc info --typed — print the machine-readable Typed IR contract (stdout) lsc claimcheck [] — 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 ``, `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 diff --git a/TOOLS.md b/TOOLS.md index 2bc2ee8..09aad34 100644 --- a/TOOLS.md +++ b/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 | diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 5ec8d98..b73b18d 100644 --- a/tools/src/dafny-emit.ts +++ b/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 { + 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). diff --git a/tools/src/info-command.ts b/tools/src/info-command.ts index c67c356..68040e0 100644 --- a/tools/src/info-command.ts +++ b/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; + /** 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(); + const walk = (node: unknown): void => { + if (Array.isArray(node)) { node.forEach(walk); return; } + if (node && typeof node === "object") { + const o = node as Record; + 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 and Record 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)); +} diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index 293c3a4..9bdc162 100755 --- a/tools/src/lsc.ts +++ b/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 …` forwards verbatim to the lemmascript-claimcheck // CLI (a dependency; its cli reads the rewritten process.argv). With no // leading , 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 [--backend=lean|dafny] "); + console.error(" lsc info --typed (machine-readable Typed IR contract to stdout)"); console.error(" lsc [--backend=…] [--slow] (no file: batch over LemmaScript-files.txt)"); console.error(" lsc claimcheck [] [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");