feat(verification): close inv_field_001 with Tier 2 OoxmlDoc subset

[stevenobiajulu]

Summary

Implements OpenSpec change add-ooxml-doc-subset-and-inv-field-001-proof (merged 2026-05-14 via #202). Closes the inv_field_001 sorry in verification/lean/LeanSpike/Spec.lean with a machine-checked preservation lemma over a definitional Lean OOXML subset, composed with a single named residual axiom.

• New verification/lean/Tier2/ module: OoxmlModel, FieldStructure, WalkLemmas, AcceptReject, InvFieldOne. All zero-sorry. The preservation lemma field_structure_preserved is proven against a stack-valued field-context walk (FieldCtx := List Bool) exactly mirroring the TS engine's pastSeparatorAtDepth: number[] at pipeline.ts:374-389, with the strictly stronger fieldContextNeutral per-subtree predicate that survives the round-3 counterexample families.
• Spec.lean rewires OoxmlDoc / acceptAllChanges / rejectAllChanges / validateFieldStructure from axiom to Tier 2 definitions, adds the single residual axiom compareDocumentXml_output_recursivelyWellformed, and closes the inv_field_001 sorry with a two-line proof. #print axioms inv_field_001 confirms zero sorryAx — depends only on propext, Quot.sound, compareDocumentXml, and the named residual axiom.
• inv_rt_001 remains sorry'd (explicitly deferred to add-inv-rt-001-proof).
• lean-build.yml audit extended to cover Tier2/; Spec.lean expected-sorry count drops from 2 to 1.
• lean-spec-bridge.test.ts gets one field-bearing fixture case (NUMPAGES insert) that runs a TS analogue of recursivelyWellformed against the live engine as a falsifiability layer for the new axiom.
• Tier2/README.md, verification/lean/README.md, and verification/ROADMAP.md document scope, residual obligations, and Tier 2 status.

Ref: #201. See change at openspec/changes/add-ooxml-doc-subset-and-inv-field-001-proof/.

Test plan

• cd verification/lean && lake build — clean build, single expected sorry warning (Spec.lean:126 = inv_rt_001).
• Non-Spec zero-sorry audit (workflow logic): find LeanSpike.lean LeanSpike Tier2.lean Tier2 -name '*.lean' ! -name 'Spec.lean' -print0 | xargs -0 grep -nwH sorry → empty.
• grep -cw sorry LeanSpike/Spec.lean → 1.
• #print axioms LeanSpike.inv_field_001 → [propext, compareDocumentXml, compareDocumentXml_output_recursivelyWellformed, Quot.sound] (no sorryAx).
• npx vitest run packages/docx-core/src/integration/lean-spec-bridge.test.ts — all 5 tests pass, including the new field-bearing fixture case.
• npx tsc --noEmit -p packages/docx-core/tsconfig.json — clean.
• npx eslint packages/docx-core/src/integration/lean-spec-bridge.test.ts — clean.
• npx openspec validate add-ooxml-doc-subset-and-inv-field-001-proof --strict — valid; all 10 tasks checked off.
• CI green (lean-build workflow + workspace-test matrix).

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
site	Ready	Preview, Comment	May 22, 2026 6:29am

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[stevenobiajulu]

Peer-review synthesis (Codex + Gemini + ECMA-376 deep research)

Captured here so the patterns are durable for future Lean/TS-fidelity work.

Blocking findings (both reviewers converged)

1. w:delInstrText TS↔Lean divergence — TS under-validates the spec.
TS validateFieldStructure (pipeline.ts:357, :391-393) checks only w:instrText; Lean Tier2/FieldStructure.lean:64-71 checks both. ECMA-376 (DeletedFieldCode) mandates w:delInstrText placement inside <w:del> — Word, LibreOffice, and docx4j all enforce or split to maintain this. Lean is right; TS is the gap. Tracked in #209.

2. OoxmlModel subset coverage gap — projection is doing silent load-bearing work.
Lean Block := run|ins|del|moveFrom|moveTo (OoxmlModel.lean:54-63) omits w:tbl, w:sdt, w:hyperlink, bookmarks. The residual axiom is over compareDocumentXml : OoxmlDoc → OoxmlDoc → Option OoxmlDoc, which side-steps the projection. Adding a second projection axiom would grow the trusted base without fixing the underlying issue. Preferred fix: extend Lean Block with a transparent other tag children constructor and let walkBlocks descend through it — keeps the trusted base at one axiom, mirrors TS's recursive-scan behavior.

3. fieldContextNeutral ∀ ctx is incompatible with ECMA-376 field fragmentation. ⚠️ Foundational
ECMA-376 explicitly requires conformant emitters to fragment fields across wrapper boundaries when a field is modified under track changes. Canonical fixture (FORMCHECKBOX→FORMFIELDTEXT):

<w:fldChar w:fldCharType=\"begin\"/>
<w:ins><w:r><w:instrText>FORMCHECKBOX</w:instrText></w:r></w:ins>
<w:del><w:r><w:delInstrText>FORMFIELDTEXT</w:delInstrText></w:r></w:del>
<w:fldChar w:fldCharType=\"separate\"/>

The <w:ins> wrapper contains only [w:instrText] and is not fieldContextNeutral under empty ctx (instrText on empty stack → invalid). The current NUMPAGES test fixture passes only because it's a whole-field insertion (entire field in one <w:ins>). For any inplace output that modifies an existing field, the residual axiom is demonstrably false, not just thinly evidenced. The Lean predicate needs path-conditional neutrality ("neutral under the contexts the walk actually reaches it with"), not universal ∀ ctx.

4. Falsifiability layer is too thin.
One NUMPAGES insertion fixture exercises zero w:delInstrText atoms and zero fragmented-field topologies. Minimum additions before merge: deleted-field fixture, complete-field-in-<w:del> fixture, complete-field-in-<w:ins> fixture, negative neutrality unit cases (standalone separate, standalone end, [begin, separate]).

5. #print axioms LeanSpike.inv_field_001 is unverified.
Both reviewers ran static-only (no lake in their sandboxes). Static grep confirms no sorry/unsafe/classical/decide in Tier2/, but the exact claimed axiom list must be confirmed in CI or local Lean before merge.

Not blockers

• Stale pastSeparatorAtDepth[depth+1] vs Lean pop — observationally equivalent (TS only reads at current depth; next begin overwrites). No change needed; optional comment in pipeline.ts documenting why the stale entry is unreachable would harden against future refactors.
• Doc.blocks paragraph flattening — aligned with TS recursive scan and with ECMA-376's "fields can cross paragraph boundaries within a story" rule. No change.
• Lean proof tactics — no suspicious usage. omega is bounded to count arithmetic backed by explicit count lemmas. The weak point is the axiom + model fidelity, not the proof.

Cross-cutting TS engine recommendations from this Lean work

1. Add w:fldChar-inside-<w:del> rejection. ECMA-376 strictly forbids this; Word discards the field state machine on violation. Currently unchecked. → Folded into validateFieldStructure: add w:delInstrText placement check + reject w:fldChar inside <w:del> #209.
2. Cross-story field-closure check. Per ECMA-376 an unclosed field at end-of-story invalidates the field. The current global balance check is whole-document, not per-story; footnote/header expansions may miss this.
3. Per-wrapper neutrality as a runtime safety gate. Bring the bridge test's isFieldContextNeutral (in the now path-conditional form) into the engine itself so the residual axiom becomes a checked invariant, not just an asserted one.

Pattern for future Lean↔TS fidelity work

The recurring failure mode in this review: Lean models that over-strengthen a predicate beyond what production XML actually satisfies, with a single thin fixture as falsifiability evidence. When the next OpenSpec change touches a validate* function or another invariant proof, check:

• Does the Lean predicate match the spec, the engine, or some intersection? If the engine under-validates the spec, fix the engine first.
• Is the predicate's quantifier (∀ over contexts, ∀ over inputs) tighter than what the engine can plausibly produce? Look for fragmentation/split behaviors in the engine that violate the universal.
• Is the falsifiability layer exercising the adverse shapes of every atom case (esp. delText/delInstrText/wrapper-fragmented fields), or just the happy path?

Sources

• Codex review log: /tmp/peer-review-pr208-codex-output.txt (final verdict at ~line 5906)
• Gemini review log: /tmp/peer-review-pr208-gemini-output.txt
• ECMA-376 research: notes thread (DeletedFieldCode placement, fldChar/del nesting prohibition, fragmentation requirement, sibling rule for fldChar runs)