From 35414e3eff694268c0c20b0317d653e7ff2acc99 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 18:03:15 -0700 Subject: [PATCH 1/3] feat(formal): add where.mjs, the contract lookup command `node formal/tools/where.mjs C45` prints where one contract is stated (its CONTRACTS row and every Quint comment that cites it, with file:line), tested (the semantic cases that carry it with their scenarios, scoped Quint checks, witnesses, replays and vectors, the documentation sections and tests disposed to it, the feature families), challenged (the model-fault challenges that name it, with their invariant, native mutant, reproducer and profile partition counts) and mapped (the native mutants whose case carries it, with the ports they edit, and the Go parity rows). A semantic case ID narrows the view to that case. `--json` prints the same structure for an agent. It reads only the catalogs the audit already parses and adds no data and no gate: it is the navigation a reviewer or an agent otherwise assembles by hand, and the contract-level navigation test of lan17/DialCache#220 as a command. The README task table, the tools index and AUTHORING's reviewer-context section point at it. --- formal/README.md | 1 + formal/catalogs/source-audit.json | 4 +- formal/guides/AUTHORING.md | 4 +- formal/tools/README.md | 1 + formal/tools/where.mjs | 107 +++++++++++++++++++++++++++ typescript/test/formal-where.test.ts | 47 ++++++++++++ 6 files changed, 161 insertions(+), 3 deletions(-) create mode 100644 formal/tools/where.mjs create mode 100644 typescript/test/formal-where.test.ts diff --git a/formal/README.md b/formal/README.md index ff3100fa..3000eb8d 100644 --- a/formal/README.md +++ b/formal/README.md @@ -16,6 +16,7 @@ the test [coordinator](./guides/GLOSSARY.md#coordinator). | Change a behavior or extend coverage | [AUTHORING.md](./guides/AUTHORING.md) | | Implement another language | [PORTING.md](./guides/PORTING.md) and [PROTOCOL.md](./guides/PROTOCOL.md) | | Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and the commands below | +| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` (or a case, `C45.recheck-after-decode`) | | Interpret validation results | [VALIDATION.md](./guides/VALIDATION.md) | | Look up a term | [GLOSSARY.md](./guides/GLOSSARY.md) | diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index b4a7585b..b496f5b2 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -1084,7 +1084,7 @@ "reviewedGuides": [ { "path": "formal/README.md", - "sha256": "bc318ab21ccd8d5589584f280ef09fdd49404596c8ce0dfedd147aa41b0f2d6e", + "sha256": "8fa28f2e7a726708a486b837756dcbf69d6073534e510fa652b20d64c89c6d33", "entries": [ {"title":"Executable DialCache specification"}, {"title":"Start with your task"}, @@ -1102,7 +1102,7 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "7f3aee31a1f311f27420550960f1ceed757ecae1f1616bea01436a9635cd12f6", + "sha256": "7ca3b3b7502feaadcda03586b604b60df64bfec9e9e1ed68bffd3d118de50a59", "entries": [ {"title":"Reading and extending the DialCache models"}, {"title":"Reading a model"}, diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index c8a4221a..b041f1bc 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -259,7 +259,9 @@ work in issue #165 does not need to precede unrelated feature or port developmen ## Give reviewers focused context For a human or LLM review, search the stable contract and case IDs first, then -extract the matching catalog entries. Provide a small context packet: +extract the matching catalog entries; `node formal/tools/where.mjs C45` (or a +case ID) prints them in one place, with `--json` for an agent. Provide a small +context packet: - Contract/case IDs, the observable rule or change, and its documentation link. - Model file, exact regression/property symbols, and their execution-manifest entries. diff --git a/formal/tools/README.md b/formal/tools/README.md index fc8a6365..fce2174f 100644 --- a/formal/tools/README.md +++ b/formal/tools/README.md @@ -12,6 +12,7 @@ which scripts a target runs. - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites. - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory. +- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract or semantic case is stated, tested, challenged and mapped, from the catalogs; `--json` for agents. ## Checks diff --git a/formal/tools/where.mjs b/formal/tools/where.mjs new file mode 100644 index 00000000..430b9f13 --- /dev/null +++ b/formal/tools/where.mjs @@ -0,0 +1,107 @@ +// Where a contract lives, from the catalogs the audit already parses. For one +// contract ID (C45) or one semantic case (C45.recheck-after-decode) it prints +// where the obligation is stated (its CONTRACTS row and every Quint comment +// that cites it), tested (the semantic cases that carry it with their +// scenarios, scoped Quint checks, witnesses, replays and vectors, and the +// documentation sections and tests disposed to it), challenged (the model +// fault challenges that name it) and mapped (the native mutants whose case +// carries it and the Go parity rows). No new data and no gate: this is the +// navigation a reviewer or an agent otherwise assembles by hand. +// +// node formal/tools/where.mjs C45 [--json] +import { readFileSync, readdirSync } from 'node:fs'; +import { resolve } from 'node:path'; +import { fileURLToPath } from 'node:url'; + +export const root = fileURLToPath(new URL('../../', import.meta.url)); +const read = (path, directory) => readFileSync(resolve(directory, path), 'utf8'); +const json = (path, directory) => JSON.parse(read(path, directory)); + +function quintFiles(directory) { + const walk = relative => readdirSync(resolve(directory, relative), { withFileTypes: true }).flatMap(entry => + entry.isDirectory() ? walk(`${relative}/${entry.name}`) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []); + return walk('formal/models').sort(); +} + +export function lookup(query, { directory = root } = {}) { + const match = /^([CWEBX]\d{2})(?:\.([\w-]+))?$/.exec(query ?? ''); + if (!match) throw new Error(`${query}: expected a contract ID such as C45 or a semantic case such as C45.recheck-after-decode`); + const [, id, caseName] = match; + const caseId = caseName ? `${id}.${caseName}` : undefined; + const row = read('formal/guides/CONTRACTS.md', directory).split('\n').map((line, index) => [line, index + 1]).find(([line]) => line.startsWith(`| ${id} |`)); + if (!row) throw new Error(`${id}: not a contract in formal/guides/CONTRACTS.md`); + const [, obligation, evidence] = row[0].trim().replace(/^\|\s*|\s*\|$/g, '').split(/\s*\|\s*/); + const cites = new RegExp(`\\b${id}\\b`); + const quint = quintFiles(directory).flatMap(path => read(path, directory).split('\n').flatMap((line, index) => + line.trim().startsWith('//') && cites.test(line) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : [])); + const semantic = json('formal/catalogs/semantic-cases.json', directory).cases + .filter(entry => caseId ? entry.id === caseId : (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`)) + .map(entry => ({ id: entry.id, rule: entry.rule, scenarios: entry.scenarios ?? [], models: (entry.models ?? []).map(model => model.ref), + witnesses: (entry.generated ?? []).map(item => `${item.profile}/${item.witness}`), replays: entry.quintReplays ?? [], vectors: entry.vectors ?? [], + generatedVectors: (entry.generatedVectors ?? []).map(item => `${item.artifact}#${item.group ?? 'vectors'}/${item.name}`) })); + if (caseId && semantic.length === 0) throw new Error(`${caseId}: not a semantic case in formal/catalogs/semantic-cases.json`); + const caseIds = new Set(semantic.map(entry => entry.id)); + const audit = json('formal/catalogs/source-audit.json', directory); + const disposed = (audit.sources ?? []).flatMap(source => (source.entries ?? []).filter(entry => (entry.contracts ?? []).includes(id)).map(entry => ({ path: source.path, title: entry.title }))); + const guides = (audit.reviewedGuides ?? []).filter(guide => (guide.review?.contracts ?? []).includes(id)).map(guide => guide.path); + const challenges = (json('formal/catalogs/execution.json', directory).challenges ?? []).filter(challenge => challenge.contract === id) + .filter(challenge => !caseId || (challenge.nativeMutants?.mutant && mutantCase(challenge.nativeMutants.mutant, directory) === caseId)) + .map(challenge => ({ id: challenge.id, source: challenge.source, model: challenge.model, invariant: challenge.invariant, + native: challenge.nativeMutants?.kind, mutant: challenge.nativeMutants?.mutant, run: challenge.reproducer?.run, + detecting: (challenge.reproducer?.profiles ?? []).length, excluded: Object.keys(challenge.reproducer?.exclusions ?? {}).length })); + const rust = new Map((json('formal/catalogs/rust-mutations.json', directory).mutations ?? []).map(mutant => [mutant.typescriptMutation ?? mutant.id, mutant])); + const mutants = (json('formal/catalogs/mutations.json', directory).mutations ?? []).filter(mutant => caseId ? mutant.case === caseId : String(mutant.case).startsWith(`${id}.`)) + .map(mutant => ({ id: mutant.id, case: mutant.case, description: mutant.description, + ports: [mutant.typescript?.edits?.length ? 'typescript' : null, mutant.go?.edits?.length ? 'go' : null, rust.get(mutant.id)?.edits?.length ? 'rust' : null].filter(Boolean) })); + const parity = (json('formal/catalogs/go-parity.json', directory).cases ?? []).filter(entry => caseIds.has(entry.id)) + .map(entry => ({ id: entry.id, group: entry.group, gaps: entry.gaps ?? [], nativeGo: entry.evidence?.nativeGo ?? [] })); + const features = (json('formal/catalogs/feature-coverage.json', directory).features ?? []).filter(feature => (feature.contracts ?? []).includes(id) || (feature.cases ?? []).some(entry => caseIds.has(entry))) + .map(feature => ({ id: feature.id, title: feature.title })); + return { id, case: caseId, obligation, evidence, contractsLine: row[1], quint, cases: semantic, disposed, guides, challenges, mutants, parity, features }; +} + +function mutantCase(mutantId, directory) { + return (json('formal/catalogs/mutations.json', directory).mutations ?? []).find(mutant => mutant.id === mutantId)?.case; +} + +export function render(result) { + const lines = [`${result.case ?? result.id}: ${result.obligation}`, '']; + lines.push('Stated', ` formal/guides/CONTRACTS.md:${result.contractsLine} (evidence column: ${result.evidence})`); + for (const cite of result.quint) lines.push(` ${cite.path}:${cite.line} ${cite.text}`); + if (result.guides.length) lines.push(` reviewed guides naming it: ${result.guides.join(', ')}`); + lines.push('', `Tested (${result.cases.length} semantic case${result.cases.length === 1 ? '' : 's'})`); + for (const entry of result.cases) { + lines.push(` ${entry.id}: ${entry.rule}`); + if (entry.scenarios.length) lines.push(` scenarios: ${entry.scenarios.map(s => `"${s}"`).join(', ')}`); + if (entry.models.length) lines.push(` quint: ${entry.models.join(', ')}`); + if (entry.witnesses.length) lines.push(` witnesses: ${entry.witnesses.join(', ')}`); + if (entry.replays.length) lines.push(` replays: ${entry.replays.join(', ')}`); + if (entry.vectors.length) lines.push(` vectors: ${entry.vectors.join(', ')}`); + if (entry.generatedVectors.length) lines.push(` generated vectors: ${entry.generatedVectors.join(', ')}`); + } + if (result.disposed.length) { lines.push(' disposed sections and tests (source-audit.json):'); for (const item of result.disposed) lines.push(` ${item.path} "${item.title}"`); } + if (result.features.length) lines.push(` feature families: ${result.features.map(f => `${f.id} (${f.title})`).join('; ')}`); + lines.push('', `Challenged (${result.challenges.length} challenge${result.challenges.length === 1 ? '' : 's'})`); + for (const challenge of result.challenges) { + lines.push(` ${challenge.id}: ${challenge.source.split('/').pop()} under ${challenge.model.split('/').pop()}:${challenge.invariant}; native ${challenge.native}${challenge.mutant ? ` ${challenge.mutant}` : ''}${challenge.run ? `; reproducer ${challenge.run}` : ''}; detected by ${challenge.detecting} profiles, ${challenge.excluded} excluded`); + } + lines.push('', `Mapped (${result.mutants.length} native mutant${result.mutants.length === 1 ? '' : 's'})`); + for (const mutant of result.mutants) lines.push(` ${mutant.id} (${mutant.case}): ${mutant.description}; edits in ${mutant.ports.join(', ') || 'no port'}`); + for (const row of result.parity) lines.push(` go-parity ${row.id}: group ${row.group}${row.gaps.length ? `; gaps ${row.gaps.length}` : ''}${row.nativeGo.length ? `; native Go ${row.nativeGo.join(', ')}` : ''}`); + return lines.join('\n') + '\n'; +} + +if (process.argv[1] === fileURLToPath(import.meta.url)) { + const args = process.argv.slice(2); + const wantJson = args.includes('--json'); + const query = args.find(arg => !arg.startsWith('--')); + if (!query || args.length > 2) { + console.error('Usage: node formal/tools/where.mjs [--json]'); + process.exitCode = 2; + } else { + try { + const result = lookup(query); + process.stdout.write(wantJson ? `${JSON.stringify(result, null, 2)}\n` : render(result)); + } catch (error) { console.error(error.message); process.exitCode = 1; } + } +} diff --git a/typescript/test/formal-where.test.ts b/typescript/test/formal-where.test.ts new file mode 100644 index 00000000..10a76462 --- /dev/null +++ b/typescript/test/formal-where.test.ts @@ -0,0 +1,47 @@ +import { describe, expect, it } from "vitest"; + +const { lookup, render } = await import(new URL("../../formal/tools/where.mjs", import.meta.url).href) as { + lookup(query: string): { + id: string; case?: string; obligation: string; contractsLine: number; + quint: Array<{ path: string; line: number; text: string }>; + cases: Array<{ id: string; scenarios: string[]; models: string[]; witnesses: string[] }>; + disposed: Array<{ path: string; title: string }>; challenges: Array<{ id: string; mutant?: string }>; + mutants: Array<{ id: string; ports: string[] }>; parity: Array<{ id: string }>; + }; + render(result: unknown): string; +}; + +describe("contract lookup", () => { + it("finds where C45 is stated, tested, challenged and mapped from the catalogs", () => { + const result = lookup("C45"); + expect(result.obligation).toMatch(/^Recheck age before\/after asynchronous decode/); + expect(result.quint.map(cite => cite.path)).toContain("formal/models/kernel/recovery.qnt"); + expect(result.cases.map(entry => entry.id)).toContain("C45.recheck-after-decode"); + expect(result.cases.every(entry => entry.scenarios.length + entry.models.length + entry.witnesses.length > 0)).toBe(true); + expect(result.challenges.map(challenge => challenge.id)).toContain("recovery-inclusive-maximum"); + expect(result.mutants.find(mutant => mutant.id === "M01")?.ports).toEqual(["typescript", "go", "rust"]); + expect(result.parity.map(row => row.id)).toEqual(result.cases.map(entry => entry.id)); + expect(result.disposed.length).toBeGreaterThan(0); + }); + + it("narrows to one semantic case and keeps the challenges mapped through its mutant", () => { + const result = lookup("C45.maximum-age-exclusive"); + expect(result.case).toBe("C45.maximum-age-exclusive"); + expect(result.cases.map(entry => entry.id)).toEqual(["C45.maximum-age-exclusive"]); + expect(result.mutants.map(mutant => mutant.id)).toEqual(["M01"]); + expect(result.challenges.map(challenge => challenge.mutant)).toEqual(result.challenges.map(() => "M01")); + }); + + it("renders the four sections with clickable locations", () => { + const text = render(lookup("C45")); + for (const heading of ["Stated", "Tested (", "Challenged (", "Mapped ("]) expect(text).toContain(`\n${heading}`); + expect(text).toMatch(/formal\/guides\/CONTRACTS\.md:\d+/); + expect(text).toMatch(/formal\/models\/kernel\/recovery\.qnt:\d+/); + }); + + it("rejects an unknown contract, a malformed query and an unknown case", () => { + expect(() => lookup("C99")).toThrow(/not a contract in formal\/guides\/CONTRACTS.md/); + expect(() => lookup("recovery")).toThrow(/expected a contract ID/); + expect(() => lookup("C45.not-a-case")).toThrow(/not a semantic case/); + }); +}); From 4927fcba2d1ffc7f9aa0d6aa46089269c3caaa1d Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 18:05:45 -0700 Subject: [PATCH 2/3] fix(formal): match contract citations without building a regex from the argument CodeQL flagged the regular expression where.mjs built from the validated command-line ID. The scan now tests whole-token occurrences of the ID directly, which also makes the intent (an ID is a letter and two digits, not a prefix of a longer one) explicit. --- formal/tools/where.mjs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/formal/tools/where.mjs b/formal/tools/where.mjs index 430b9f13..41ad7b0b 100644 --- a/formal/tools/where.mjs +++ b/formal/tools/where.mjs @@ -31,9 +31,11 @@ export function lookup(query, { directory = root } = {}) { const row = read('formal/guides/CONTRACTS.md', directory).split('\n').map((line, index) => [line, index + 1]).find(([line]) => line.startsWith(`| ${id} |`)); if (!row) throw new Error(`${id}: not a contract in formal/guides/CONTRACTS.md`); const [, obligation, evidence] = row[0].trim().replace(/^\|\s*|\s*\|$/g, '').split(/\s*\|\s*/); - const cites = new RegExp(`\\b${id}\\b`); + // A comment cites the ID when it appears as a whole token: the ID is a letter + // and two digits, so a neighbouring word character means another ID (C450). + const cites = line => { let at = line.indexOf(id); while (at >= 0) { const before = line[at - 1], after = line[at + id.length]; if (!/\w/.test(before ?? ' ') && !/\w/.test(after ?? ' ')) return true; at = line.indexOf(id, at + 1); } return false; }; const quint = quintFiles(directory).flatMap(path => read(path, directory).split('\n').flatMap((line, index) => - line.trim().startsWith('//') && cites.test(line) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : [])); + line.trim().startsWith('//') && cites(line) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : [])); const semantic = json('formal/catalogs/semantic-cases.json', directory).cases .filter(entry => caseId ? entry.id === caseId : (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`)) .map(entry => ({ id: entry.id, rule: entry.rule, scenarios: entry.scenarios ?? [], models: (entry.models ?? []).map(model => model.ref), From d8b4d38f28f96ca7d43d3e04f9385ffb3773bab0 Mon Sep 17 00:00:00 2001 From: Lev Neiman Date: Wed, 14 Oct 2026 18:21:54 -0700 Subject: [PATCH 3/3] fix(formal): make where.mjs select by contract and narrow honestly Review follow-up. Mapped selected mutants by case-ID prefix while Tested selected cases by contract, so a cross-listed case lost its mutant: C33 printed four challenges "mapped M06" above "Mapped (0 native mutants)". Mutants are now the ones whose case the contract's cases include. A case query dropped every challenge whose mutant sits on another case, including the eight cross-contract mappings and the eight challenges without a port line. Those stay with a tag ("cross-contract via M40 on C40.future-rejected", "model-only, not narrowed to a case") and the cross-contract note that execution.mjs requires is printed at both levels. Citations now include ranges ("C40 to C46", "C40-C45"), the house style of the rewritten kernel headers; C42 showed no model citation although six headers state it. The kernel fixtures are no longer scanned as statements. The B-series contracts list their native cases from feature-coverage.json with the port tests, and a native case ID is an accepted query. Each semantic case shows its defining transitions and source pointers. Challenge rows carry full paths and count profiles and models separately; the CONTRACTS row must split into three cells; the CLI rejects unknown flags and extra arguments; a case query's header is the case rule. The near-constant "reviewed guides naming it" line is gone. --- formal/README.md | 2 +- formal/catalogs/source-audit.json | 4 +- formal/guides/AUTHORING.md | 5 +- formal/tools/README.md | 7 +- formal/tools/where.mjs | 161 ++++++++++++++++++--------- typescript/test/formal-where.test.ts | 71 +++++++++--- 6 files changed, 174 insertions(+), 76 deletions(-) diff --git a/formal/README.md b/formal/README.md index 3000eb8d..7627bced 100644 --- a/formal/README.md +++ b/formal/README.md @@ -16,7 +16,7 @@ the test [coordinator](./guides/GLOSSARY.md#coordinator). | Change a behavior or extend coverage | [AUTHORING.md](./guides/AUTHORING.md) | | Implement another language | [PORTING.md](./guides/PORTING.md) and [PROTOCOL.md](./guides/PROTOCOL.md) | | Locate or reproduce a failing check | [TEST-MAP.md](./guides/TEST-MAP.md) and the commands below | -| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` (or a case, `C45.recheck-after-decode`) | +| See where one contract is stated, tested, challenged and mapped | `node formal/tools/where.mjs C45` (or a case, `C45.recheck-after-decode` or `B01.registration-and-policy-snapshot`) | | Interpret validation results | [VALIDATION.md](./guides/VALIDATION.md) | | Look up a term | [GLOSSARY.md](./guides/GLOSSARY.md) | diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json index b496f5b2..1b2ac7ee 100644 --- a/formal/catalogs/source-audit.json +++ b/formal/catalogs/source-audit.json @@ -1084,7 +1084,7 @@ "reviewedGuides": [ { "path": "formal/README.md", - "sha256": "8fa28f2e7a726708a486b837756dcbf69d6073534e510fa652b20d64c89c6d33", + "sha256": "cb6204391896e6c69ac5ab5e6195bc1c5f07261358220bb156433b9f5599b14a", "entries": [ {"title":"Executable DialCache specification"}, {"title":"Start with your task"}, @@ -1102,7 +1102,7 @@ }, { "path": "formal/guides/AUTHORING.md", - "sha256": "7ca3b3b7502feaadcda03586b604b60df64bfec9e9e1ed68bffd3d118de50a59", + "sha256": "728051bdcc8e1a7df19052aaa259ccdf8d7375647255325e514beafb9e22933b", "entries": [ {"title":"Reading and extending the DialCache models"}, {"title":"Reading a model"}, diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md index b041f1bc..9f44293e 100644 --- a/formal/guides/AUTHORING.md +++ b/formal/guides/AUTHORING.md @@ -260,8 +260,9 @@ work in issue #165 does not need to precede unrelated feature or port developmen For a human or LLM review, search the stable contract and case IDs first, then extract the matching catalog entries; `node formal/tools/where.mjs C45` (or a -case ID) prints them in one place, with `--json` for an agent. Provide a small -context packet: +case ID) prints the catalog entries and model citations in one place, with +`--json` for an agent; the validation evidence and port mappings below come +from the reports and the replay descriptors. Provide a small context packet: - Contract/case IDs, the observable rule or change, and its documentation link. - Model file, exact regression/property symbols, and their execution-manifest entries. diff --git a/formal/tools/README.md b/formal/tools/README.md index fce2174f..c7b90787 100644 --- a/formal/tools/README.md +++ b/formal/tools/README.md @@ -2,8 +2,9 @@ The Node scripts behind the `make` targets. `make ` is `node formal/tools/validation.mjs `; `make help` lists the targets and -their prerequisites. Every script reads its inputs from -[../catalogs/](../catalogs/README.md) and writes generated output only under +their prerequisites. The scripts read their inputs from +[../catalogs/](../catalogs/README.md) (and, for the checks and lookups over the +text, from the models and guides) and write generated output only under [../generated/](../generated/README.md) and, for the witness fixtures, `typescript/test/fixtures/`. Start with `validation.mjs` to see which scripts a target runs. @@ -12,7 +13,7 @@ which scripts a target runs. - [validation.mjs](./validation.mjs): the target dispatcher; composes every `make` target from the scripts below and checks prerequisites. - [execution.mjs](./execution.mjs): reads and validates the execution manifest; `node formal/tools/execution.mjs` prints the inventory. -- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract or semantic case is stated, tested, challenged and mapped, from the catalogs; `--json` for agents. +- [where.mjs](./where.mjs): `node formal/tools/where.mjs C45` prints where one contract, semantic case or native case is stated, tested, challenged and mapped, from the catalogs and the model comments; `--json` for agents. ## Checks diff --git a/formal/tools/where.mjs b/formal/tools/where.mjs index 41ad7b0b..4aa98d93 100644 --- a/formal/tools/where.mjs +++ b/formal/tools/where.mjs @@ -1,12 +1,15 @@ // Where a contract lives, from the catalogs the audit already parses. For one -// contract ID (C45) or one semantic case (C45.recheck-after-decode) it prints -// where the obligation is stated (its CONTRACTS row and every Quint comment -// that cites it), tested (the semantic cases that carry it with their -// scenarios, scoped Quint checks, witnesses, replays and vectors, and the -// documentation sections and tests disposed to it), challenged (the model -// fault challenges that name it) and mapped (the native mutants whose case -// carries it and the Go parity rows). No new data and no gate: this is the -// navigation a reviewer or an agent otherwise assembles by hand. +// contract ID (C45), one semantic case (C45.recheck-after-decode) or one native +// case (B01.registration-and-policy-snapshot) it prints where the obligation is +// stated (its CONTRACTS row and every model comment that cites it, ranges such +// as "C40 to C46" included), tested (the semantic cases that carry it with +// their scenarios, scoped Quint checks, witnesses, replays, vectors, defining +// transitions and source pointers; the native cases that carry it with their +// port tests; the documentation sections and tests disposed to it; the feature +// families), challenged (the model-fault challenges that name it) and mapped +// (the native mutants whose case carries it and the Go parity rows). No new +// data and no gate: this is the navigation a reviewer or an agent otherwise +// assembles by hand. // // node formal/tools/where.mjs C45 [--json] import { readFileSync, readdirSync } from 'node:fs'; @@ -17,93 +20,141 @@ export const root = fileURLToPath(new URL('../../', import.meta.url)); const read = (path, directory) => readFileSync(resolve(directory, path), 'utf8'); const json = (path, directory) => JSON.parse(read(path, directory)); -function quintFiles(directory) { +// The scheduled models and the kernel: the sources whose comments state +// rules. The kernel fixtures exercise seams and are not scanned. +function modelFiles(directory) { const walk = relative => readdirSync(resolve(directory, relative), { withFileTypes: true }).flatMap(entry => - entry.isDirectory() ? walk(`${relative}/${entry.name}`) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []); + entry.isDirectory() ? (entry.name === 'fixtures' ? [] : walk(`${relative}/${entry.name}`)) : entry.name.endsWith('.qnt') ? [`${relative}/${entry.name}`] : []); return walk('formal/models').sort(); } +// Does a comment line cite the ID? A citation is the ID as a whole token, or a +// range of the same letter that contains it: "C40-C46", "C40 to C46". +export function cites(line, id) { + const letter = id[0], number = Number(id.slice(1)); + for (const match of line.matchAll(/\b([CWEBX])(\d{2})(?:\s*(?:-|to)\s*([CWEBX])(\d{2}))?\b/g)) { + const [, fromLetter, from, toLetter, to] = match; + if (fromLetter !== letter) continue; + if (to === undefined) { if (Number(from) === number) return true; continue; } + if (toLetter === letter && Number(from) <= number && number <= Number(to)) return true; + } + return false; +} + +function contractRow(id, directory) { + const rows = read('formal/guides/CONTRACTS.md', directory).split('\n'); + const index = rows.findIndex(line => line.startsWith(`| ${id} |`)); + if (index < 0) throw new Error(`${id}: not a contract in formal/guides/CONTRACTS.md`); + const cells = rows[index].trim().replace(/^\|\s*|\s*\|$/g, '').split(/\s*\|\s*/); + if (cells.length !== 3) throw new Error(`formal/guides/CONTRACTS.md:${index + 1}: expected three cells (ID, obligation, evidence), found ${cells.length}`); + return { line: index + 1, obligation: cells[1], evidence: cells[2] }; +} + export function lookup(query, { directory = root } = {}) { const match = /^([CWEBX]\d{2})(?:\.([\w-]+))?$/.exec(query ?? ''); - if (!match) throw new Error(`${query}: expected a contract ID such as C45 or a semantic case such as C45.recheck-after-decode`); + if (!match) throw new Error(`${query}: expected a contract ID such as C45, a semantic case such as C45.recheck-after-decode or a native case such as B01.registration-and-policy-snapshot`); const [, id, caseName] = match; const caseId = caseName ? `${id}.${caseName}` : undefined; - const row = read('formal/guides/CONTRACTS.md', directory).split('\n').map((line, index) => [line, index + 1]).find(([line]) => line.startsWith(`| ${id} |`)); - if (!row) throw new Error(`${id}: not a contract in formal/guides/CONTRACTS.md`); - const [, obligation, evidence] = row[0].trim().replace(/^\|\s*|\s*\|$/g, '').split(/\s*\|\s*/); - // A comment cites the ID when it appears as a whole token: the ID is a letter - // and two digits, so a neighbouring word character means another ID (C450). - const cites = line => { let at = line.indexOf(id); while (at >= 0) { const before = line[at - 1], after = line[at + id.length]; if (!/\w/.test(before ?? ' ') && !/\w/.test(after ?? ' ')) return true; at = line.indexOf(id, at + 1); } return false; }; - const quint = quintFiles(directory).flatMap(path => read(path, directory).split('\n').flatMap((line, index) => - line.trim().startsWith('//') && cites(line) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : [])); - const semantic = json('formal/catalogs/semantic-cases.json', directory).cases - .filter(entry => caseId ? entry.id === caseId : (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`)) - .map(entry => ({ id: entry.id, rule: entry.rule, scenarios: entry.scenarios ?? [], models: (entry.models ?? []).map(model => model.ref), - witnesses: (entry.generated ?? []).map(item => `${item.profile}/${item.witness}`), replays: entry.quintReplays ?? [], vectors: entry.vectors ?? [], - generatedVectors: (entry.generatedVectors ?? []).map(item => `${item.artifact}#${item.group ?? 'vectors'}/${item.name}`) })); - if (caseId && semantic.length === 0) throw new Error(`${caseId}: not a semantic case in formal/catalogs/semantic-cases.json`); + const row = contractRow(id, directory); + const quint = modelFiles(directory).flatMap(path => read(path, directory).split('\n').flatMap((line, index) => + line.trim().startsWith('//') && cites(line, id) ? [{ path, line: index + 1, text: line.trim().replace(/^\/\/\s?/, '') }] : [])); + const coverage = json('formal/catalogs/feature-coverage.json', directory); + const semanticAll = json('formal/catalogs/semantic-cases.json', directory).cases.filter(entry => (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`)); + const nativeAll = (coverage.nativeCases ?? []).filter(entry => (entry.contracts ?? []).includes(id) || entry.id.startsWith(`${id}.`)); + if (caseId && !semanticAll.some(entry => entry.id === caseId) && !nativeAll.some(entry => entry.id === caseId)) { + throw new Error(`${caseId}: not a semantic case in formal/catalogs/semantic-cases.json nor a native case in formal/catalogs/feature-coverage.json`); + } + const semantic = semanticAll.filter(entry => !caseId || entry.id === caseId).map(entry => ({ id: entry.id, rule: entry.rule, scenarios: entry.scenarios ?? [], + models: (entry.models ?? []).map(model => model.ref), definitions: (entry.definitions ?? []).map(definition => definition.ref), provenance: entry.provenance ?? [], + witnesses: (entry.generated ?? []).map(item => `${item.profile}/${item.witness}`), replays: entry.quintReplays ?? [], vectors: entry.vectors ?? [], + generatedVectors: (entry.generatedVectors ?? []).map(item => `${item.artifact}#${item.group ?? 'vectors'}/${item.name}`) })); + const native = nativeAll.filter(entry => !caseId || entry.id === caseId).map(entry => ({ id: entry.id, rule: entry.rule, related: entry.relatedContracts ?? [], + tests: ['typescript', 'go'].flatMap(port => (entry[port] ?? []).map(test => `${test.path} "${test.test}"`)), adaptation: entry.adaptation, gaps: entry.gaps ?? [], notApplicable: entry.notApplicable })); const caseIds = new Set(semantic.map(entry => entry.id)); const audit = json('formal/catalogs/source-audit.json', directory); const disposed = (audit.sources ?? []).flatMap(source => (source.entries ?? []).filter(entry => (entry.contracts ?? []).includes(id)).map(entry => ({ path: source.path, title: entry.title }))); - const guides = (audit.reviewedGuides ?? []).filter(guide => (guide.review?.contracts ?? []).includes(id)).map(guide => guide.path); - const challenges = (json('formal/catalogs/execution.json', directory).challenges ?? []).filter(challenge => challenge.contract === id) - .filter(challenge => !caseId || (challenge.nativeMutants?.mutant && mutantCase(challenge.nativeMutants.mutant, directory) === caseId)) - .map(challenge => ({ id: challenge.id, source: challenge.source, model: challenge.model, invariant: challenge.invariant, - native: challenge.nativeMutants?.kind, mutant: challenge.nativeMutants?.mutant, run: challenge.reproducer?.run, - detecting: (challenge.reproducer?.profiles ?? []).length, excluded: Object.keys(challenge.reproducer?.exclusions ?? {}).length })); + const mutantsAll = json('formal/catalogs/mutations.json', directory).mutations ?? []; + const caseOf = new Map(mutantsAll.map(mutant => [mutant.id, mutant.case])); const rust = new Map((json('formal/catalogs/rust-mutations.json', directory).mutations ?? []).map(mutant => [mutant.typescriptMutation ?? mutant.id, mutant])); - const mutants = (json('formal/catalogs/mutations.json', directory).mutations ?? []).filter(mutant => caseId ? mutant.case === caseId : String(mutant.case).startsWith(`${id}.`)) - .map(mutant => ({ id: mutant.id, case: mutant.case, description: mutant.description, - ports: [mutant.typescript?.edits?.length ? 'typescript' : null, mutant.go?.edits?.length ? 'go' : null, rust.get(mutant.id)?.edits?.length ? 'rust' : null].filter(Boolean) })); + // Under a case query a challenge stays when its mutant sits on that case; a + // challenge without a port line, or one mapped across contracts, cannot be + // narrowed and stays with a tag saying so. + const challenges = (json('formal/catalogs/execution.json', directory).challenges ?? []).filter(challenge => challenge.contract === id).flatMap(challenge => { + const mutant = challenge.nativeMutants?.mutant, kind = challenge.nativeMutants?.kind, mutantCase = mutant ? caseOf.get(mutant) : undefined; + let tag; + if (caseId) { + if (!mutant) tag = `${kind}, not narrowed to a case`; + else if (mutantCase !== caseId) { if (!challenge.nativeMutants?.crossContract) return []; tag = `cross-contract via ${mutant} on ${mutantCase}`; } + } else if (challenge.nativeMutants?.crossContract) tag = `cross-contract via ${mutant} on ${mutantCase}`; + const profiles = challenge.reproducer?.profiles ?? []; + return [{ id: challenge.id, source: challenge.source, model: challenge.model, invariant: challenge.invariant, native: kind, mutant, mutantCase, tag, + crossContract: challenge.nativeMutants?.crossContract, run: challenge.reproducer?.run, + detectingProfiles: profiles.filter(profile => !profile.includes('/')).length, detectingModels: profiles.filter(profile => profile.includes('/')).length, + excluded: Object.keys(challenge.reproducer?.exclusions ?? {}).length }]; + }); + const mutants = mutantsAll.filter(mutant => caseIds.has(mutant.case)).map(mutant => ({ id: mutant.id, case: mutant.case, description: mutant.description, + ports: [mutant.typescript?.edits?.length ? 'typescript' : null, mutant.go?.edits?.length ? 'go' : null, rust.get(mutant.id)?.edits?.length ? 'rust' : null].filter(Boolean) })); const parity = (json('formal/catalogs/go-parity.json', directory).cases ?? []).filter(entry => caseIds.has(entry.id)) .map(entry => ({ id: entry.id, group: entry.group, gaps: entry.gaps ?? [], nativeGo: entry.evidence?.nativeGo ?? [] })); - const features = (json('formal/catalogs/feature-coverage.json', directory).features ?? []).filter(feature => (feature.contracts ?? []).includes(id) || (feature.cases ?? []).some(entry => caseIds.has(entry))) + const features = (coverage.features ?? []).filter(feature => (feature.contracts ?? []).includes(id) || (feature.cases ?? []).some(entry => caseIds.has(entry)) || (feature.nativeCases ?? []).some(entry => native.some(item => item.id === entry))) .map(feature => ({ id: feature.id, title: feature.title })); - return { id, case: caseId, obligation, evidence, contractsLine: row[1], quint, cases: semantic, disposed, guides, challenges, mutants, parity, features }; + const rule = semantic.find(entry => entry.id === caseId)?.rule ?? native.find(entry => entry.id === caseId)?.rule ?? null; + return { id, case: caseId ?? null, caseRule: rule, obligation: row.obligation, evidence: row.evidence, contractsLine: row.line, quint, cases: semantic, nativeCases: native, disposed, challenges, mutants, parity, features }; } -function mutantCase(mutantId, directory) { - return (json('formal/catalogs/mutations.json', directory).mutations ?? []).find(mutant => mutant.id === mutantId)?.case; -} +const plural = (count, word) => `${count} ${word}${count === 1 ? '' : 's'}`; export function render(result) { - const lines = [`${result.case ?? result.id}: ${result.obligation}`, '']; + const lines = [result.case ? `${result.case}: ${result.caseRule}` : `${result.id}: ${result.obligation}`, '']; + if (result.case) lines.push(`Contract ${result.id}: ${result.obligation}`, ''); lines.push('Stated', ` formal/guides/CONTRACTS.md:${result.contractsLine} (evidence column: ${result.evidence})`); for (const cite of result.quint) lines.push(` ${cite.path}:${cite.line} ${cite.text}`); - if (result.guides.length) lines.push(` reviewed guides naming it: ${result.guides.join(', ')}`); - lines.push('', `Tested (${result.cases.length} semantic case${result.cases.length === 1 ? '' : 's'})`); + lines.push('', `Tested (${plural(result.cases.length, 'semantic case')}${result.nativeCases.length ? `, ${plural(result.nativeCases.length, 'native case')}` : ''})`); for (const entry of result.cases) { lines.push(` ${entry.id}: ${entry.rule}`); if (entry.scenarios.length) lines.push(` scenarios: ${entry.scenarios.map(s => `"${s}"`).join(', ')}`); - if (entry.models.length) lines.push(` quint: ${entry.models.join(', ')}`); + if (entry.models.length) lines.push(` quint checks: ${entry.models.join(', ')}`); + if (entry.definitions.length) lines.push(` defining transitions: ${entry.definitions.join(', ')}`); if (entry.witnesses.length) lines.push(` witnesses: ${entry.witnesses.join(', ')}`); if (entry.replays.length) lines.push(` replays: ${entry.replays.join(', ')}`); if (entry.vectors.length) lines.push(` vectors: ${entry.vectors.join(', ')}`); if (entry.generatedVectors.length) lines.push(` generated vectors: ${entry.generatedVectors.join(', ')}`); + if (entry.provenance.length) lines.push(` source: ${entry.provenance.join(', ')}`); + } + for (const entry of result.nativeCases) { + lines.push(` ${entry.id}: ${entry.rule}${entry.related.length ? ` (related ${entry.related.join(', ')})` : ''}`); + if (entry.tests.length) lines.push(` tests: ${entry.tests.join('; ')}`); + if (entry.adaptation) lines.push(` adaptation: ${entry.adaptation}`); + if (entry.notApplicable) lines.push(` not applicable: ${typeof entry.notApplicable === 'string' ? entry.notApplicable : JSON.stringify(entry.notApplicable)}`); + if (entry.gaps.length) lines.push(` gaps: ${entry.gaps.map(gap => typeof gap === 'string' ? gap : JSON.stringify(gap)).join('; ')}`); } if (result.disposed.length) { lines.push(' disposed sections and tests (source-audit.json):'); for (const item of result.disposed) lines.push(` ${item.path} "${item.title}"`); } if (result.features.length) lines.push(` feature families: ${result.features.map(f => `${f.id} (${f.title})`).join('; ')}`); - lines.push('', `Challenged (${result.challenges.length} challenge${result.challenges.length === 1 ? '' : 's'})`); + lines.push('', `Challenged (${plural(result.challenges.length, 'challenge')})`); for (const challenge of result.challenges) { - lines.push(` ${challenge.id}: ${challenge.source.split('/').pop()} under ${challenge.model.split('/').pop()}:${challenge.invariant}; native ${challenge.native}${challenge.mutant ? ` ${challenge.mutant}` : ''}${challenge.run ? `; reproducer ${challenge.run}` : ''}; detected by ${challenge.detecting} profiles, ${challenge.excluded} excluded`); + lines.push(` ${challenge.id}: ${challenge.source ?? '?'} under ${challenge.model ?? '?'}:${challenge.invariant}; native ${challenge.native}${challenge.mutant ? ` ${challenge.mutant}` : ''}${challenge.run ? `; reproducer ${challenge.run}` : ''}; detected by ${plural(challenge.detectingProfiles, 'profile')}${challenge.detectingModels ? ` and ${plural(challenge.detectingModels, 'model')}` : ''}, ${challenge.excluded} excluded${challenge.tag ? ` [${challenge.tag}]` : ''}`); + if (challenge.crossContract) lines.push(` cross-contract: ${challenge.crossContract}`); } - lines.push('', `Mapped (${result.mutants.length} native mutant${result.mutants.length === 1 ? '' : 's'})`); + lines.push('', `Mapped (${plural(result.mutants.length, 'native mutant')})`); for (const mutant of result.mutants) lines.push(` ${mutant.id} (${mutant.case}): ${mutant.description}; edits in ${mutant.ports.join(', ') || 'no port'}`); for (const row of result.parity) lines.push(` go-parity ${row.id}: group ${row.group}${row.gaps.length ? `; gaps ${row.gaps.length}` : ''}${row.nativeGo.length ? `; native Go ${row.nativeGo.join(', ')}` : ''}`); return lines.join('\n') + '\n'; } +export function parseArguments(args) { + const flags = args.filter(arg => arg.startsWith('--')), positional = args.filter(arg => !arg.startsWith('--')); + const unknown = flags.filter(flag => flag !== '--json'); + if (positional.length !== 1 || unknown.length) throw new Error('Usage: node formal/tools/where.mjs [--json]'); + return { query: positional[0], json: flags.includes('--json') }; +} + if (process.argv[1] === fileURLToPath(import.meta.url)) { - const args = process.argv.slice(2); - const wantJson = args.includes('--json'); - const query = args.find(arg => !arg.startsWith('--')); - if (!query || args.length > 2) { - console.error('Usage: node formal/tools/where.mjs [--json]'); - process.exitCode = 2; - } else { + let parsed; + try { parsed = parseArguments(process.argv.slice(2)); } catch (error) { console.error(error.message); process.exitCode = 2; } + if (parsed) { try { - const result = lookup(query); - process.stdout.write(wantJson ? `${JSON.stringify(result, null, 2)}\n` : render(result)); + const result = lookup(parsed.query); + process.stdout.write(parsed.json ? `${JSON.stringify(result, null, 2)}\n` : render(result)); } catch (error) { console.error(error.message); process.exitCode = 1; } } } diff --git a/typescript/test/formal-where.test.ts b/typescript/test/formal-where.test.ts index 10a76462..e83c3bbd 100644 --- a/typescript/test/formal-where.test.ts +++ b/typescript/test/formal-where.test.ts @@ -1,35 +1,76 @@ import { describe, expect, it } from "vitest"; -const { lookup, render } = await import(new URL("../../formal/tools/where.mjs", import.meta.url).href) as { +const { lookup, render, cites, parseArguments } = await import(new URL("../../formal/tools/where.mjs", import.meta.url).href) as { lookup(query: string): { - id: string; case?: string; obligation: string; contractsLine: number; + id: string; case: string | null; caseRule: string | null; obligation: string; contractsLine: number; quint: Array<{ path: string; line: number; text: string }>; - cases: Array<{ id: string; scenarios: string[]; models: string[]; witnesses: string[] }>; - disposed: Array<{ path: string; title: string }>; challenges: Array<{ id: string; mutant?: string }>; - mutants: Array<{ id: string; ports: string[] }>; parity: Array<{ id: string }>; + cases: Array<{ id: string; scenarios: string[]; models: string[]; witnesses: string[]; provenance: string[] }>; + nativeCases: Array<{ id: string; tests: string[] }>; + disposed: Array<{ path: string; title: string }>; + challenges: Array<{ id: string; mutant?: string; mutantCase?: string; tag?: string; crossContract?: string; native?: string }>; + mutants: Array<{ id: string; case: string; ports: string[] }>; parity: Array<{ id: string }>; }; render(result: unknown): string; + cites(line: string, id: string): boolean; + parseArguments(args: string[]): { query: string; json: boolean }; }; describe("contract lookup", () => { it("finds where C45 is stated, tested, challenged and mapped from the catalogs", () => { const result = lookup("C45"); + expect(result.case).toBeNull(); expect(result.obligation).toMatch(/^Recheck age before\/after asynchronous decode/); expect(result.quint.map(cite => cite.path)).toContain("formal/models/kernel/recovery.qnt"); + expect(result.quint.every(cite => !cite.path.includes("/fixtures/"))).toBe(true); expect(result.cases.map(entry => entry.id)).toContain("C45.recheck-after-decode"); expect(result.cases.every(entry => entry.scenarios.length + entry.models.length + entry.witnesses.length > 0)).toBe(true); + expect(result.cases.some(entry => entry.provenance.length > 0)).toBe(true); expect(result.challenges.map(challenge => challenge.id)).toContain("recovery-inclusive-maximum"); + expect(result.challenges.find(challenge => challenge.id === "recovery-future-candidate")).toMatchObject({ mutant: "M40", mutantCase: "C40.future-rejected", tag: "cross-contract via M40 on C40.future-rejected" }); expect(result.mutants.find(mutant => mutant.id === "M01")?.ports).toEqual(["typescript", "go", "rust"]); expect(result.parity.map(row => row.id)).toEqual(result.cases.map(entry => entry.id)); expect(result.disposed.length).toBeGreaterThan(0); }); - it("narrows to one semantic case and keeps the challenges mapped through its mutant", () => { - const result = lookup("C45.maximum-age-exclusive"); - expect(result.case).toBe("C45.maximum-age-exclusive"); - expect(result.cases.map(entry => entry.id)).toEqual(["C45.maximum-age-exclusive"]); - expect(result.mutants.map(mutant => mutant.id)).toEqual(["M01"]); - expect(result.challenges.map(challenge => challenge.mutant)).toEqual(result.challenges.map(() => "M01")); + it("selects mutants by the cases that carry the contract, so a cross-listed case keeps its mutant", () => { + const result = lookup("C33"); + expect(result.cases.map(entry => entry.id)).toContain("W04.strict-fence"); + expect(result.mutants.map(mutant => mutant.id)).toContain("M06"); + for (const challenge of result.challenges) if (challenge.mutant && !challenge.tag) expect(result.mutants.map(mutant => mutant.id), challenge.id).toContain(challenge.mutant); + }); + + it("narrows to one semantic case and keeps unlinkable challenges with a tag", () => { + const narrowed = lookup("C45.maximum-age-exclusive"); + expect(narrowed.case).toBe("C45.maximum-age-exclusive"); + expect(narrowed.caseRule).toMatch(/exactly M preserves the source error/); + expect(narrowed.cases.map(entry => entry.id)).toEqual(["C45.maximum-age-exclusive"]); + expect(narrowed.mutants.map(mutant => mutant.id)).toEqual(["M01"]); + const linked = narrowed.challenges.filter(challenge => !challenge.tag); + expect(linked).toHaveLength(4); + expect(linked.every(challenge => challenge.mutant === "M01")).toBe(true); + expect(lookup("C45.rollback-future").challenges.map(challenge => [challenge.id, challenge.tag])).toContainEqual(["recovery-future-candidate", "cross-contract via M40 on C40.future-rejected"]); + const modelOnly = lookup("C24").challenges.filter(challenge => !challenge.mutant); + expect(modelOnly.length).toBeGreaterThan(0); + const firstCase = lookup("C24").cases[0]!.id; + expect(lookup(firstCase).challenges.filter(challenge => !challenge.mutant).map(challenge => challenge.tag)).toEqual(modelOnly.map(challenge => `${challenge.native}, not narrowed to a case`)); + }); + + it("cites ranges and whole tokens, not prefixes", () => { + expect(cites("// Stale-on-error recovery (C40 to C46, C57)", "C42")).toBe(true); + expect(cites("// Selected rules from C40-C45.", "C43")).toBe(true); + expect(cites("// Selected rules from C40-C45.", "C46")).toBe(false); + expect(cites("// judged once (C43/C45)", "C45")).toBe(true); + expect(cites("// C450 and C4 and C455 only", "C45")).toBe(false); + expect(cites("// W01 to W03", "C02")).toBe(false); + expect(lookup("C42").quint.map(cite => cite.path)).toContain("formal/models/kernel/recovery.qnt"); + }); + + it("lists native cases and their port tests for a binding contract", () => { + const result = lookup("B01"); + expect(result.cases).toEqual([]); + expect(result.nativeCases.map(entry => entry.id)).toContain("B01.registration-and-policy-snapshot"); + expect(result.nativeCases.every(entry => entry.tests.length > 0)).toBe(true); + expect(lookup("B01.registration-and-policy-snapshot").nativeCases.map(entry => entry.id)).toEqual(["B01.registration-and-policy-snapshot"]); }); it("renders the four sections with clickable locations", () => { @@ -37,11 +78,15 @@ describe("contract lookup", () => { for (const heading of ["Stated", "Tested (", "Challenged (", "Mapped ("]) expect(text).toContain(`\n${heading}`); expect(text).toMatch(/formal\/guides\/CONTRACTS\.md:\d+/); expect(text).toMatch(/formal\/models\/kernel\/recovery\.qnt:\d+/); + expect(text).toContain("cross-contract: "); + expect(render(lookup("C45.maximum-age-exclusive"))).toMatch(/^C45\.maximum-age-exclusive: After asynchronous decoding/); }); - it("rejects an unknown contract, a malformed query and an unknown case", () => { + it("rejects an unknown contract, a malformed query, an unknown case and bad arguments", () => { expect(() => lookup("C99")).toThrow(/not a contract in formal\/guides\/CONTRACTS.md/); expect(() => lookup("recovery")).toThrow(/expected a contract ID/); - expect(() => lookup("C45.not-a-case")).toThrow(/not a semantic case/); + expect(() => lookup("C45.not-a-case")).toThrow(/not a semantic case .* nor a native case/); + expect(parseArguments(["C45", "--json"])).toEqual({ query: "C45", json: true }); + for (const args of [[], ["C45", "C46"], ["C45", "--jsonx"], ["--json"]]) expect(() => parseArguments(args)).toThrow(/Usage/); }); });