refactor(verification): weaken inv_field_001 axiom to document-level preservationFriendly (PR-B follow-up to #208)#219
Merged
stevenobiajulu merged 1 commit intoMay 22, 2026
Conversation
…nt-level preservation friendliness Closes peer-review concern D (predicate strength) from PR #208. Codex review confirmed the current engine satisfies the stronger `∀ ctx` predicate, but the ECMA-376 Part 4 deep-research report showed that a conformant emitter MUST fragment fields across wrapper boundaries when modifying a field — fragmented `<w:ins>`/`<w:del>` wrappers containing only `w:instrText`/`w:delInstrText` are NOT `fieldContextNeutral` under `∀ ctx`. When safe-docx becomes ECMA-376-conformant (tracked in #217), the stronger predicate will break. This commit weakens the residual axiom to be future-compatible without touching the engine. ## Predicate weakening Adds `Tier2.AcceptReject.preservationFriendly` — a document-level property asserting only that accept and reject preserve the *composed* field walk and begin/end balance. Strictly weaker than the previous per-subtree `Tier2.FieldStructure.recursivelyWellformed`: * Old: `validateFieldStructure d ∧ ∀ wrapper-subtree, fieldContextNeutral subtree` where `fieldContextNeutral bs := ∀ ctx, walkBlocks (.ok ctx) bs = .ok ctx`. * New: `validateFieldStructure d ∧ walkBlocks (.ok []) (acceptBlocks d.blocks) = walkBlocks (.ok []) d.blocks ∧ ...` (analogous for reject + balance). The old predicate is retained in `Tier2.FieldStructure` and the legacy `field_structure_preserved` lemma still compiles — they remain available for audit traceability. Only `inv_field_001` is rewired to consume the new predicate via the new `Tier2.InvFieldOne.field_structure_preserved_doc` lemma. ## Axiom replacement `Spec.lean` replaces `compareDocumentXml_output_recursivelyWellformed` with `compareDocumentXml_output_preservation_friendly`. The `inv_field_001` proof body changes to compose the new axiom with `field_structure_preserved_doc`. `#print axioms LeanSpike.inv_field_001` becomes: [propext, compareDocumentXml, compareDocumentXml_output_preservation_friendly, Quot.sound] ## TS bridge — explanatory comment The existing `isFieldContextNeutral` / `assertRecursivelyWellformed` checks in `lean-spec-bridge.test.ts` enforce the OLD stricter property. With the axiom now weaker, these become an audit OVER-check: the engine currently satisfies them (whole-field wrapping), but when #217 lands and the engine starts fragmenting, these checks will need to be removed or relaxed. The comment block above the field-bearing fixtures is updated to reflect this layering. Ref: #208, #217
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Open
4 tasks
4 tasks
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
Stacked on top of #208. Replaces the load-bearing residual axiom in
Spec.leanfrom the per-subtreeTier2.FieldStructure.recursivelyWellformed(which requires∀ ctxneutrality of every track-change wrapper subtree) to the new document-levelTier2.AcceptReject.preservationFriendly(which only asserts that accept and reject preserve the composed walk and begin/end balance).The new predicate is strictly weaker than the old one and is future-compatible with ECMA-376 field fragmentation (#217). The old predicate happens to hold for the current safe-docx engine — Codex's review of #208 confirmed via
inPlaceModifier.ts:717, 938, 1505, 1671, 1957, 2300that the engine emits whole field sequences as single track-change wrappers. But when #217 lands and the engine starts fragmenting per ECMA-376 Part 4, the old∀ ctxpredicate breaks whilepreservationFriendlystill holds.This PR lands the predicate weakening before the engine refactor so the Lean side never has to live with a known-broken axiom.
Strength comparison (constructed by Codex during review)
Both predicates hold for a complete-field-in-
<w:ins>(the engine's current shape). OnlypreservationFriendlyholds for the ECMA-376 fragmented shape[fldChar begin, ins[instrText], fldChar separate, text, fldChar end]— the inner<w:ins>is not∀ ctx-neutral but the document as a whole is preservation-friendly.What changed
verification/lean/Tier2/AcceptReject.lean— addspreservationFriendlydefinition. OpensTier2.FieldStructureto reuse the walk and count utilities.verification/lean/Tier2/InvFieldOne.lean— adds new theoremfield_structure_preserved_doc(the doc-level variant). ~25 lines. The legacyfield_structure_preservedis retained for audit traceability.verification/lean/LeanSpike/Spec.lean— replaces the axiom withcompareDocumentXml_output_preservation_friendly. Rewires theinv_field_001proof body. Updates the axiom docstring to explain the layering.packages/docx-core/src/integration/lean-spec-bridge.test.ts— updates the comment block above the field-bearing fixtures to document that the existingassertRecursivelyWellformedover-check is now stricter than what the axiom requires; will need adjustment when inplace atomizer: emit fragmented fields per ECMA-376 Part 4 (split <w:ins>/<w:del> at field-character boundaries) #217 lands.Out of scope
walkBlocks_acceptBlocks,walkBlocks_rejectBlocks,countBlocks_*_balance, tall-stack lemmas,neutral_balanced, etc. all remain. Per Codex's review they have standalone value (e.g.,neutral_balancedis an elegant tall-stack proof). A future cleanup PR can move them to aLegacyNeutralLemmas.leanafter inplace atomizer: emit fragmented fields per ECMA-376 Part 4 (split <w:ins>/<w:del> at field-character boundaries) #217 lands.Test plan
lake buildon the existing PR feat(verification): close inv_field_001 with Tier 2 OoxmlDoc subset #208 branch is green (validated by upstream CI — see feat(verification): close inv_field_001 with Tier 2 OoxmlDoc subset #208 status).lean-buildruns against this branch and passes.workspace-testmatrix passes (no TS changes beyond a comment block).#print axioms LeanSpike.inv_field_001returns[propext, compareDocumentXml, compareDocumentXml_output_preservation_friendly, Quot.sound](audit pending CI).Sequencing
This PR's base is
worktree-inv-field-001-proof(i.e., it stacks on #208). After #208 merges, this PR can be retargeted tomain.🤖 Generated with Claude Code