chore(verification): scaffold OpenSpec change for Tier 2 OoxmlDoc model + inv_field_001 closure#202
Merged
Merged
Conversation
…el + inv_field_001 closure Authors the OpenSpec change `add-ooxml-doc-subset-and-inv-field-001-proof` to kick off Tier 2 of the Lean 4 verification roadmap. Two rounds of gemini + codex CLI peer review have been incorporated. The proposal does NOT implement Tier 2; it scopes the work and decomposes it into eight single-`/codex-implement`-run-sized tasks (T1, T2, T3a, T3b, T4a, T4b, T5a, T5b/T6) that successor PRs against this change will land. Key decisions captured: - Model boundary: small tree-structured syntactic OOXML subset (paragraphs → blocks with `Ins`/`Del`/`MoveFrom`/`MoveTo` wrappers → runs → atoms including `DelInstrText`). Mirrors `trackChangesAcceptorAst.ts:368-659` structurally; deliberately narrower than full `ComparisonUnitAtom`. - Closure strategy: introduce a recursive well-formedness predicate `recursivelyWellformed` (whole-doc `validateFieldStructure` plus every wrapper subtree `fieldSelfContained`) and prove a preservation lemma over the Lean model. The `Spec.lean:71` sorry closes by composing the lemma with a single new named axiom `compareDocumentXml_output_recursivelyWellformed`, which becomes the load-bearing residual obligation Tier 3 will discharge. - `fieldSelfContained` strengthening (round-2 peer review fix): the counterexample `Begin, Separate, Ins(Del(End, Begin), InstrText), End` showed that per-subtree `validateFieldStructure` is too weak, so wrapper subtrees must enter and exit the depth/seenSeparator walk at `(0, false)`. - `inv_rt_001` (Spec.lean:95 sorry), Tier 2.5 (Lean↔TS equivalence, broader projection), and Tier 3 (definitional `compareDocumentXml`) are explicitly out of scope for this change. Also updates `verification/ROADMAP.md` line 3 to reflect PR #164 merged and this change in progress (the line was stale, calling PR #164 a draft when it merged 2026-05-11). `openspec validate add-ooxml-doc-subset-and-inv-field-001-proof --strict` passes. The proposal is opened as a draft PR so the model-boundary and predicate-strengthening decisions can take further peer-review iteration in PR comments before any implementation work begins. Ref: #201 (tracking issue), #164 (Tier 1 spike).
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…eld context, T0 generic-lemma split) Round 3 peer review (codex + gemini CLI, 2026-05-13) caught three further counterexample families that defeat any "standalone walk from (0, false) ends at (0, false)" predicate: - DelInstrText is unchecked: Del(DelInstrText) breaks reject after rewrite - subtree consumes outer field state via leading End/Separate: Begin, Ins(End) breaks reject; Begin, Del(End) breaks accept - single-boolean seenSeparator reset: [Begin, Separate, Del(Begin, End), InstrText, End] slips through The fix tracks seenSeparator as a depth-indexed stack (FieldCtx := List Bool), exactly mirroring the TS engine's pastSeparatorAtDepth at pipeline.ts:374-389, and strengthens the per-subtree predicate to fieldContextNeutral: the subtree is invariant under any outer field-stack context. Other revisions in this commit: - Pull shared walk-over-append + context-extension + DelInstrText rewrite lemmas out into a new T0 task (Tier2/WalkLemmas.lean) so accept and reject halves consume identical generic results. - Fix DelInstrText locality claim: rewrite is global at the operation level (after both Del and MoveFrom unwraps complete, per TS lines 602-616); locality is enforced by recursivelyWellformed on the input. - Tone down empirical wording in the new axiom's docstring; scope it to this repo's inplace atomizer rather than to OOXML comparison engines in general. - Add scenario [LEAN-T2-04](f) covering the DelInstrText locality and reject ordering documentation.
Member
Author
Round 3 peer review incorporated (commit 9beb692)Ran
Both reviewers landed independently on the same root cause: the per-subtree predicate must operate over a stack-valued field context, exactly mirroring what Changes in this commit
Validation
Round 4 review is welcomed if a third-party Lean-fluent reviewer wants to attack the |
Member
Author
✅ Post-merge smoke passedMerged: Steps
Why no CI rerun outcome: failed jobs were rerun and presumably passed (PR merged successfully via automerge). Log: Successor work: file individual issues for T0..T6 from |
9 tasks
stevenobiajulu
added a commit
that referenced
this pull request
May 22, 2026
…208) * feat(verification): close inv_field_001 with Tier 2 OoxmlDoc subset Implements OpenSpec change `add-ooxml-doc-subset-and-inv-field-001-proof` (merged 2026-05-14 via PR #202). Replaces the uninterpreted document-level axioms in `LeanSpike/Spec.lean` with a definitional Lean OOXML subset under `verification/lean/Tier2/` and proves the field-structure preservation lemma machine-checked. `inv_field_001` is closed by composing that lemma with a single named residual axiom `compareDocumentXml_output_recursivelyWellformed`, which captures the only remaining assumption (discharging it by modeling `compareDocumentXml` definitionally is Tier 3 work). `inv_rt_001` remains `sorry`'d (deferred to `add-inv-rt-001-proof`). Why: PR #164 shipped `Spec.lean` over fully uninterpreted axioms, leaving both invariants as `sorry`. Closing `inv_field_001` requires either a definitional comparison model (Tier 3) or carrying an explicit, named residual obligation. Three peer-review rounds (codex + gemini CLI) drove the design to a stack-valued field context exactly mirroring the TS engine's `pastSeparatorAtDepth: number[]` and the strictly stronger `fieldContextNeutral` per-subtree predicate. What's delivered: - `Tier2/OoxmlModel.lean` — tree-structured OOXML subset. - `Tier2/FieldStructure.lean` — stack-valued walk, `validateFieldStructure`, `fieldContextNeutral`, `recursivelyWellformed`. - `Tier2/WalkLemmas.lean` — `walkBlocks_append`, neutrality no-op, `neutral_balanced` (via a tall-stack length-tracking argument so no `end` underflows), `delInstrText_rewrite_safe`. - `Tier2/AcceptReject.lean` — definitional `accept` / `reject`. - `Tier2/InvFieldOne.lean` — closed `field_structure_preserved` (zero `sorry`). - `LeanSpike/Spec.lean` — `OoxmlDoc` / `acceptAllChanges` / `rejectAllChanges` / `validateFieldStructure` rewired from `axiom` to Tier 2 definitions; new named residual axiom; `inv_field_001` proof. - `lean-build.yml` — non-Spec zero-sorry audit extended to `Tier2/`; Spec.lean audit updated from 2 sorries to 1. - `lean-spec-bridge.test.ts` — one field-bearing fixture case exercising a TS analogue of `recursivelyWellformed` as a falsifiability layer for the new axiom. - `Tier2/README.md`, `verification/lean/README.md`, `verification/ROADMAP.md` — scope, residual obligations, status. Verification: `lake build` clean with one expected `sorry` warning (`inv_rt_001`). `#print axioms inv_field_001` depends only on `propext`, `Quot.sound`, `compareDocumentXml`, and the one residual axiom — no `sorryAx`. Full `lean-spec-bridge.test.ts` suite (5 tests) passes. `tsc --noEmit` and ESLint clean on the test file. `openspec validate --strict` passes; all 10 tasks checked off. Ref: #201 * feat(verification): extend Tier2 Block with transparent .other container; add delInstrText falsifiability fixtures Closes peer-review gap B (subset coverage) and tightens gap C (axiom evidence) on PR #208. Both surfaced by Codex + Gemini peer review (commit-comment thread) and an ECMA-376 Part 4 deep-research report. ## Lean changes Adds a 6th `Block` constructor `Block.other (tag : String) (children : List Block)` to model OOXML structural containers that the field-context walk MUST descend through transparently but that are NOT track-change wrappers: `w:tbl`, `w:tr`, `w:tc`, `w:sdt`, `w:sdtContent`, `w:hyperlink`, bookmark elements, etc. Before this change the Lean model implicitly assumed inplace output contained no such containers — `compareDocumentXml : OoxmlDoc → OoxmlDoc → Option OoxmlDoc` was side-stepping a lossy projection. - `Tier2/OoxmlModel.lean`: add `.other` constructor with docstring explaining the modeling intent. - `Tier2/FieldStructure.lean`: `walkBlocks`, `countBlocks` descend through `.other` transparently. `wrapperSubtreesBlocks` does NOT emit the children as a wrapper subtree (only wrappers nested inside `.other` are emitted) — `.other` is structural, not a track-change wrapper. - `Tier2/AcceptReject.lean`: `acceptBlocks`, `rejectBlocks`, `renameBlocks` preserve the `.other` container with its tag while recursively processing children. Accept/reject don't unwrap or drop the container itself. - `Tier2/WalkLemmas.lean`: add `case7` to `walkBlocks_invalid`, `walkBlocks_append`, `countBlocks_append`, and the inductive `walkBlocks_tall` key block. - `Tier2/InvFieldOne.lean`: add `case7` to every `induction ... using *.induct` (walkBlocks_renameBlocks, countBlocks_renameBlocks, walkBlocks_acceptBlocks, walkBlocks_rejectBlocks, both countBlocks_*_balance). Introduce `allNeutral_other` helper that does NOT extract a `fieldContextNeutral` obligation on the container's children (since `.other` is not in `wrapperSubtreesBlocks`). `acceptBlocks_append` / `rejectBlocks_append` / `renameBlocks_append` and `accept_blocks` / `reject_blocks` use `cases b <;> simp [...]` patterns and require no edit — Lean enumerates all 6 constructors. ## Spec.lean axiom docstring rewrite Honestly states the engine-specific justification for the `∀ ctx` neutrality strength: safe-docx's current inplace atomizer emits whole field sequences as single track-change wrappers (verified at `inPlaceModifier.ts:717, 938, 1505, 1671, 1957, 2300` and `collapsed-field-inplace.test.ts:211`). The axiom is NOT spec-conformant: under ECMA-376 Part 4 a conformant emitter must fragment fields across wrapper boundaries when modifying them, and fragmented wrappers are not `fieldContextNeutral` under `∀ ctx`. When the engine becomes ECMA-376-conformant, this axiom and the per-subtree neutrality predicate will need replacement with a document-level form (follow-up PR-B tracked in plan). ## TS bridge fixtures (gap C) Adds three new tests to `lean-spec-bridge.test.ts`: 1. **NUMPAGES deletion fixture** — original has the complete field; revised deletes it. Exercises the `w:delInstrText` atom case in `isFieldContextNeutral`, which the existing NUMPAGES insertion fixture never reaches. 2. **Regression guard — `isFieldContextNeutral` rejects non-neutral shapes**: standalone `w:fldChar separate`, standalone `w:fldChar end`, and a `[begin, separate]` fragment. Crafted DOM-level XML, not full DOCX. 3. **Regression guard — `isFieldContextNeutral` accepts a complete self-contained field wrapper**: the canonical NUMPAGES-in-w:ins shape the engine actually emits. All 8 bridge tests pass locally; typecheck and lint clean. ## Out of scope (deferred to PR-B) The `∀ ctx` → document-level predicate weakening. Codex's review concluded that the current engine satisfies the existing `∀ ctx` predicate, so the weakening is not required for shipping PR #208. PR-B will land after the engine fragmentation conformance work (new GH issue to be filed) is scoped. Ref: #208 * docs(verification): reference issue #217 in inv_field_001 residual axiom docstring Replaces the placeholder "see follow-up issue" with the concrete cross-reference to the engine fragmentation conformance work tracked in #217. No behavior change. Ref: #208, #217 --------- Co-authored-by: Steven Obiajulu <stevenobiajulu@Stevens-MacBook-Pro.local>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Authors the OpenSpec change
add-ooxml-doc-subset-and-inv-field-001-proofto kick off Tier 2 of the Lean 4 verification roadmap defined inverification/ROADMAP.md. This PR is the proposal only — it does NOT implement Tier 2. Implementation lands in successor PRs (one pertasks.mditem, each via/codex-implementagainst its own GitHub issue).Tracking issue: #201.
Prerequisite: #164 (Tier 1 spike, merged 2026-05-11).
What's in this PR
openspec/changes/add-ooxml-doc-subset-and-inv-field-001-proof/proposal.md— the change overview.openspec/changes/add-ooxml-doc-subset-and-inv-field-001-proof/design.md— model boundary, predicate strengthening, axiom rewiring, proof sketches, stop conditions.openspec/changes/add-ooxml-doc-subset-and-inv-field-001-proof/tasks.md— eight tasks (T1..T6), each sized for one/codex-implementrun.openspec/changes/add-ooxml-doc-subset-and-inv-field-001-proof/specs/docx-comparison/spec.md—## ADDED Requirementsdelta with five scenarios.verification/ROADMAP.md:3— flip stale "draft PR chore(verification): atom-level Lean 4 spike with proofs + bridge + CI #164" → "merged PR chore(verification): atom-level Lean 4 spike with proofs + bridge + CI #164" and note this proposal in progress.openspec validate add-ooxml-doc-subset-and-inv-field-001-proof --strictpasses.Key design decisions
Ins/Del/MoveFrom/MoveTowrappers → runs → atoms includingDelInstrText). MirrorstrackChangesAcceptorAst.ts:368-659structurally; narrower than fullComparisonUnitAtom(intentional and documented).recursivelyWellformed(whole-docvalidateFieldStructureplus every wrapper subtreefieldSelfContained) and prove a preservation lemma over the Lean model. Compose it with a single new named axiomcompareDocumentXml_output_recursivelyWellformedto close theSpec.lean:71sorry. The new axiom is the load-bearing residual obligation Tier 3 will discharge.fieldSelfContainedstrengthening (round-2 peer review fix): the counterexampleBegin, Separate, Ins(Del(End, Begin), InstrText), Endshowed that per-subtreevalidateFieldStructureis too weak, so wrapper subtrees must enter and exit the depth/seenSeparator walk at(0, false).Out of scope (separate future changes)
inv_rt_001closure (Spec.lean:95sorry remains untouched)compareDocumentXml_output_recursivelyWellformed(Tier 3, by modelingcompareDocumentXmldefinitionally)accept/reject(Tier 2.5)Peer review
Two rounds of
gemini+codexCLI peer review have been incorporated:Spec.lean:66has novalidateFieldStructure combinedprecondition. Fix: introduce the named axiomcompareDocumentXml_output_recursivelyWellformedand compose. Also: original tape-shaped model retracted in favor of a tree.validateFieldStructuretofieldSelfContained.Further iteration on the model boundary, predicate shape, and named-axiom phrasing is welcomed in PR comments before any implementation work begins.
Test plan
openspec validate add-ooxml-doc-subset-and-inv-field-001-proof --strictpasses locallyfieldSelfContainedstrengthening actually closes the counterexample family/codex-implementper task