diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 87dc8838..08e0c3b8 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -30,7 +30,7 @@ safe-docx/ ├── skills/ Agent instructions for document editing ├── docs/ User and maintainer guides ├── spec-compliance/ ECMA-376 registry, schemas, and reports -├── verification/ Invariants and optional formal verification +├── verification/ Runtime and release-verification evidence ├── openspec/ Requirements and change proposals ├── tests/ Cross-package fixtures and integration tests └── site/ Public documentation site @@ -190,7 +190,7 @@ npm run check:conformance-citations && \ npm run check:conformance-doc ``` -Also run checks specific to the changed surface, including generated tool docs, site links, package manifests, or formal verification where applicable. +Also run checks specific to the changed surface, including generated tool docs, site links, package manifests, or release-verification evidence where applicable. ## Pull Requests diff --git a/openspec/changes/remove-lean-verification/design.md b/openspec/changes/archive/2026-09-03-remove-lean-verification/design.md similarity index 100% rename from openspec/changes/remove-lean-verification/design.md rename to openspec/changes/archive/2026-09-03-remove-lean-verification/design.md diff --git a/openspec/changes/remove-lean-verification/proposal.md b/openspec/changes/archive/2026-09-03-remove-lean-verification/proposal.md similarity index 100% rename from openspec/changes/remove-lean-verification/proposal.md rename to openspec/changes/archive/2026-09-03-remove-lean-verification/proposal.md diff --git a/openspec/changes/remove-lean-verification/specs/docx-comparison/spec.md b/openspec/changes/archive/2026-09-03-remove-lean-verification/specs/docx-comparison/spec.md similarity index 100% rename from openspec/changes/remove-lean-verification/specs/docx-comparison/spec.md rename to openspec/changes/archive/2026-09-03-remove-lean-verification/specs/docx-comparison/spec.md diff --git a/openspec/changes/remove-lean-verification/specs/spec-compliance/spec.md b/openspec/changes/archive/2026-09-03-remove-lean-verification/specs/spec-compliance/spec.md similarity index 100% rename from openspec/changes/remove-lean-verification/specs/spec-compliance/spec.md rename to openspec/changes/archive/2026-09-03-remove-lean-verification/specs/spec-compliance/spec.md diff --git a/openspec/changes/remove-lean-verification/tasks.md b/openspec/changes/archive/2026-09-03-remove-lean-verification/tasks.md similarity index 100% rename from openspec/changes/remove-lean-verification/tasks.md rename to openspec/changes/archive/2026-09-03-remove-lean-verification/tasks.md diff --git a/openspec/changes/remove-lean-verification-subsystem/design.md b/openspec/changes/remove-lean-verification-subsystem/design.md new file mode 100644 index 00000000..9b2ddef9 --- /dev/null +++ b/openspec/changes/remove-lean-verification-subsystem/design.md @@ -0,0 +1,31 @@ +# Design: Complete Lean subsystem retirement + +## Principle + +Retirement is atomic at the architectural boundary: no Lean executable, +supervisor, option, certificate field, workflow, or normative requirement may +remain. Historical archived proposals may retain their record, but current +specification and live guidance must describe the post-retirement system. + +## Coverage migration + +Before deletion, inventory every non-duplicated behavioral invariant exercised +only through Lean. Re-express user-visible invariants—package admission limits, +relationship safety, move/comment/note topology, accept/reject behavior, and +fail-closed parsing—as TypeScript unit, property, or corpus regression tests. +Proof-internal claims with no runtime behavioral counterpart are retired rather +than translated into pretend proofs. + +## API transition + +Remove `leanXmlVerifier` configuration, `LeanXmlVerifierOptions`, +`runLeanXmlTripleVerifier`, and Lean certificate output. Because these are +exported surfaces, release notes must call out the breaking removal. No inert +compatibility flag remains. + +## OpenSpec transition + +Canonical Lean requirements are removed from `docx-comparison`; behavioral +requirements that remain product requirements are rewritten without naming an +implementation language or proof system. Active Lean proposals are marked as +superseded by this change before archival. diff --git a/openspec/changes/remove-lean-verification-subsystem/inventory.md b/openspec/changes/remove-lean-verification-subsystem/inventory.md new file mode 100644 index 00000000..70e66e70 --- /dev/null +++ b/openspec/changes/remove-lean-verification-subsystem/inventory.md @@ -0,0 +1,41 @@ +# Retirement inventory and coverage map + +The complete implementation was already present on `main` in commit `55df2b94` +(`refactor: replace Lean verification with artifact checks`). This audit records +the resulting state and the maintained TypeScript evidence that replaced the +removed subsystem. + +## Removed surfaces + +| Surface | Post-retirement state | +| --- | --- | +| Source and build | `verification/lean`, its toolchain files, build artifacts, and audit scripts are absent. | +| CI | `.github/workflows/lean-build.yml` is absent. | +| Runtime | The comparison pipeline has no checker subprocess branch or executable discovery. | +| Public API | `leanXmlVerifier`, `LeanXmlVerifierOptions`, `runLeanXmlTripleVerifier`, and certificate fields are absent. | +| Integration tests | Differential, specification-bridge, and checker-supervisor suites are absent. | +| Current specification | Canonical comparison and conformance specifications contain no formal-verifier requirement. | +| Current claims | Generated capability and conformance surfaces contain no formal-assurance claim. | + +## Preserved user-visible invariants + +| Invariant | Maintained TypeScript evidence | +| --- | --- | +| Emitted-redline LCS minimality | `packages/docx-release-verifier/src/minimality.ts` and `minimality.test.ts` | +| Accept/reject text projection | `packages/docx-release-verifier/src/verifier.ts` and `verifier.test.ts`; `packages/docx-core/src/integration/accept_reject_invariant_corpus.test.ts` | +| Field structure under comparison and resolution | `packages/docx-compare/src/baselines/atomizer/pipeline.field-validation.test.ts`; complex-field reconstruction tests; docx-core field regressions | +| Package and relationship integrity | release-verifier package gates; docx-compare relationship collision and ancillary-story tests | +| Comment and note topology | docx-compare comment/ancillary-note tests and docx-core acceptance/rejection integration tests | +| Move-range pairing and paragraph-mark resolution | docx-compare move-range and in-place modifier regressions | +| Real implementation cross-check | `packages/docx-core/src/integration/libreoffice-oracle-trust-boundary.test.ts` when LibreOffice is available | + +Proof-internal propositions with no observable product behavior were retired; +they were not relabeled as runtime guarantees. + +## Residual-reference classification + +Current product code, public APIs, workflows, canonical specs, and generated +claims contain no retired-subsystem references. Historical OpenSpec material is +retained only as change history. The retirement proposal itself necessarily +names the removed surface, and negative claim tests continue to reject generic +formal-assurance language. diff --git a/openspec/changes/remove-lean-verification-subsystem/proposal.md b/openspec/changes/remove-lean-verification-subsystem/proposal.md new file mode 100644 index 00000000..2779ce64 --- /dev/null +++ b/openspec/changes/remove-lean-verification-subsystem/proposal.md @@ -0,0 +1,34 @@ +# Change: Retire the Lean verification subsystem + +## Why + +Lean verification was expected to have been removed, but the repository still +contains an active CI workflow, a compiled checker and proof tree, public +TypeScript options, production pipeline integration, differential/bridge tests, +quality-gate rules, and normative OpenSpec requirements. The remaining verifier +also currently fails the ordinary paragraph-mark insertion case, blocking the +otherwise unrelated pre-submit suite. Removing only that test would conceal the +larger architectural inconsistency. + +## What Changes + +- Remove the `verification/lean` project and Lean-specific CI workflow. +- Remove the TypeScript Lean checker supervisor, public configuration/options, + exports, certificates, and atomizer pipeline branch. +- Remove Lean-only bridge, differential, and integration tests and scripts. +- Remove or rewrite quality-gate, traceability, and documentation references. +- Retire active Lean-specific OpenSpec changes and remove Lean-specific + normative requirements from the canonical comparison specification. +- Preserve behaviorally important OOXML invariants as ordinary TypeScript + regression/property tests before deleting any Lean-only coverage. + +## Impact + +- **BREAKING** for callers using `leanXmlVerifier` options or + `runLeanXmlTripleVerifier` directly +- Affected specs: `docx-comparison` +- Affected code: `verification/lean`, `.github/workflows/lean-build.yml`, + `packages/docx-compare`, Lean bridge/differential tests in `docx-core`, and + Lean-specific repository documentation and scripts +- OpenSpec cleanup: active `verify-lean-*` changes must be superseded or closed + explicitly rather than left as impossible work diff --git a/openspec/changes/remove-lean-verification-subsystem/specs/docx-comparison/spec.md b/openspec/changes/remove-lean-verification-subsystem/specs/docx-comparison/spec.md new file mode 100644 index 00000000..7b65ec47 --- /dev/null +++ b/openspec/changes/remove-lean-verification-subsystem/specs/docx-comparison/spec.md @@ -0,0 +1,27 @@ +## ADDED Requirements + +### Requirement: Comparison integrity is enforced without an external Lean verifier + +The comparison pipeline SHALL enforce its supported package, relationship, +story-topology, and accept/reject integrity requirements through maintained +runtime validation and TypeScript regression or property tests, without a Lean +executable or Lean-specific public API. + +#### Scenario: Comparison runs without a Lean toolchain + +- **GIVEN** a supported comparison input on a machine with no Lean installation or compiled checker +- **WHEN** comparison runs +- **THEN** all required runtime integrity checks SHALL execute without invoking Lean +- **AND** the result SHALL contain no Lean-specific certificate or not-run state + +#### Scenario: Former verifier option is absent + +- **GIVEN** the post-retirement public comparison API +- **WHEN** a caller inspects its options and exports +- **THEN** `leanXmlVerifier`, `LeanXmlVerifierOptions`, and `runLeanXmlTripleVerifier` SHALL not be present + +#### Scenario: Behavioral coverage survives retirement + +- **GIVEN** an OOXML case whose user-visible invariant was previously checked only by Lean integration +- **WHEN** the Lean subsystem is removed +- **THEN** an equivalent TypeScript regression, property, or corpus test SHALL protect that invariant before deletion diff --git a/openspec/changes/remove-lean-verification-subsystem/tasks.md b/openspec/changes/remove-lean-verification-subsystem/tasks.md new file mode 100644 index 00000000..6e769f14 --- /dev/null +++ b/openspec/changes/remove-lean-verification-subsystem/tasks.md @@ -0,0 +1,28 @@ +## 1. Inventory and coverage preservation + +- [x] 1.1 Inventory Lean-only runtime, CI, API, documentation, and spec surface +- [x] 1.2 Map each user-visible Lean-checked invariant to existing TypeScript coverage +- [x] 1.3 Add missing TypeScript regression/property coverage before removal + +## 2. Runtime and API removal + +- [x] 2.1 Remove the Lean verifier supervisor and tests +- [x] 2.2 Remove atomizer pipeline integration, options, exports, and certificate fields +- [x] 2.3 Remove Lean-dependent integration and differential tests + +## 3. Build and repository removal + +- [x] 3.1 Remove `verification/lean` and `.github/workflows/lean-build.yml` +- [x] 3.2 Remove Lean-only scripts, caches, quality-gate rules, and traceability entries +- [x] 3.3 Update contributor and release documentation + +## 4. Specification cleanup + +- [x] 4.1 Remove Lean-specific canonical `docx-comparison` requirements +- [x] 4.2 Rewrite retained behavioral requirements without Lean coupling +- [x] 4.3 Supersede and archive active `verify-lean-*` changes + +## 5. Verification + +- [x] 5.1 Confirm no live Lean references remain outside archived history +- [x] 5.2 Run the full repository pre-submit suite diff --git a/scripts/check_advanced_revision_classification.mjs b/scripts/check_advanced_revision_classification.mjs index 3d207ef9..70f61997 100644 --- a/scripts/check_advanced_revision_classification.mjs +++ b/scripts/check_advanced_revision_classification.mjs @@ -153,7 +153,7 @@ async function validateEvidence(record, operationStatuses, executedClaimsByEvide for (const [operation, status] of operationStatuses) { if (!ALLOWED_STATUSES.has(status)) throw new Error(`${record.id}: invalid ${operation} status ${status}`); - if (status === 'non-goal' || operation.startsWith('lean.')) continue; + if (status === 'non-goal') continue; const covered = evidenceByOperation.get(operation) ?? new Set(); const missing = record.elements.filter((element) => !covered.has(element)); if (missing.length > 0) throw new Error(`${record.id}: ${operation} lacks element-specific evidence for ${missing.join(', ')}`); diff --git a/scripts/generate_capability_projection.test.mjs b/scripts/generate_capability_projection.test.mjs index bf160d3c..3406327f 100644 --- a/scripts/generate_capability_projection.test.mjs +++ b/scripts/generate_capability_projection.test.mjs @@ -314,5 +314,5 @@ test('the human report retains the neutral evidence limitations', async () => { const report = await readFile(path.join(root, 'spec-compliance/generated/safe-docx-capability-projection.md'), 'utf8'); assert.match(report, /a positive row applies only to the listed evidence and scope/); assert.match(report, /explicit untested and gap rows/); - assert.doesNotMatch(report, /formal assurance|theorem prover|Lean/i); + assert.doesNotMatch(report, /formal assurance|theorem prover/i); }); diff --git a/verification/ROADMAP.md b/verification/ROADMAP.md index 0d1dd637..a21925af 100644 --- a/verification/ROADMAP.md +++ b/verification/ROADMAP.md @@ -1,14 +1,9 @@ # Verification roadmap -## Lean retirement (2026-08-13) +## Release verification model -Safe DOCX previously maintained a Lean verification program in this location. -That program was removed because its local toolchain and multi-minute build made -the release certificate non-portable and routinely `not_run` in the environment -where documents are actually reviewed. - -This changes the mechanism, not the release standard. The independent -TypeScript release verifier operates on the finished DOCX artifact and requires: +The independent TypeScript release verifier operates on the finished DOCX +artifact and requires: - exact accept-all and reject-all text projections; - emitted-redline LCS minimality; @@ -18,5 +13,3 @@ TypeScript release verifier operates on the finished DOCX artifact and requires: The release verifier remains separate from the redline generator so the implementation producing a document does not certify its own in-memory model. -Historical Lean design work remains available in Git history; it is not a -current product claim, runtime dependency, or release gate.