fix(docx-core): corrected reject/accept round-trip oracle — projection-to-projection (#347)#361
Conversation
…to-projection (#347) The inplace reconstruction safety check compared the candidate's accept/reject PROJECTIONS against the RAW extracted text of the inputs (pipeline.ts originalTextForRoundTrip / revisedTextForRoundTrip). extractTextWithParagraphs counts both w:t and w:delText, so on an input that already carries its own tracked changes the raw baseline is neither the accept- nor the reject-projection — the check was falsified by construction on legitimate pre-tracked inputs and forced spurious inplace→rebuild fallbacks (the INV-RT-001 CI flake, #339, and the PR #344 seed-1586860402 family). The corrected law is apples-to-apples projection equality: accept-all(combined) == accept-all(revised input) reject-all(combined) == reject-all(original input) For clean inputs the projections equal the raw extraction, so the common case is unchanged. Accept/reject are global across all authors; the law constrains text projections only, not the raw mixed-revision markup or author provenance (a deliberate scope choice, documented in the Lean and bridge prose). The soft bookmark baselines (never fallback-triggering) keep the raw shape and are out of scope. Three layers encode the corrected law in lockstep: - engine: project each input through the same accept/reject operation the candidate is checked under (pipeline.ts baselines feeding evaluateRoundTripSafety); - Lean: compareDocumentXml_output_text_roundtrip restated over the inputs' revisedText/originalText projections; inv_rt_001 restated as projection equality, closed by applying the EXISTING machine-checked lemmas (extractText_accept_normalized, extractText_reject) on both combined and the inputs — zero sorry, no new residual axiom (#print axioms inv_rt_001: propext, Classical.choice, Quot.sound, compareDocumentXml, compareDocumentXml_output_text_roundtrip); - bridge test: assertRoundTripInvariant now asserts the projection surface (the former theorem-domain triage category collapsed into the law) and trackedPairArb spans paragraph-insert originals. Discovery payoff (aggressive discovery, bounded remediation): relaxing the arbitrary surfaced two genuine engine bug classes, adjudicated by XML, pinned with narrow issue-linked exclusions plus a characterization test asserting today's divergences verbatim, and filed: - #358 inline run-level pre-tracked w:ins ORIGINALS: insertion provenance flattened unconditionally; reject(combined) keeps text reject(original) drops, on both reconstruction paths. - #359 pre-tracked insertion text colliding with the other side's plain text: one lineage's provenance wins; the inline shape (the exact #339 counterexample) is rescued by the rebuild fallback, the paragraph-insert shapes ship law-violating output. A dedicated two-author stacked-insertion test locks in the committed global accept/reject semantics (stays inplace, both authors' revisions present, projections round-trip). Verification: lean-spec-bridge 14/14 across 6 fresh-seed runs; fixture round-trip suites 34/34; helper differential 11/11 (accept/reject helpers untouched); full docx-core 1357/1357; lake build green, zero-sorry; PR#344 comment-anchor+paragraph-insert family and the paragraph-insert-original peer-review family now stay inplace with empty fallbackDiagnostics. Fixes: #347 Fixes: #339 Ref: #358, #359, #344, #226
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
LLM-Based Quality GateOverall: ✅ PASS (5 pass · 0 warn · 9 skipped · 14 total)
Full checklist questions
Estimated cost (this run): $0.0136 — 41,803 input + 377 output tokens (≈4 chars/token) on |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
✅ Post-merge smoke passedMerged: Steps
Real-world fixtures
Visual evidence: rendered + opened locally — Cleanup
|
First minor since v0.9.1 — headline: OpenDocument (.odt) support is now installable. Covers everything accumulated on main: - ODF lane end-to-end: odf-core library (#328), provider wiring (#335), grep + insert_paragraph (#336), comments (#341), compare_documents two-file (#348), session mode (#366), intra-paragraph (run-level) tracked changes (#370) - odf-core folded into the suite release train + published as a real dependency of docx-mcp (#373); first publish bootstrapped manually at 0.9.1 with the trusted publisher configured, so this tag publishes odf-core@0.10.0 via OIDC like the rest - docx-core: formatting-fidelity comparison check (#365), reject/accept round-trip oracle stated projection-to-projection (#361), LibreOffice oracle trust-boundary characterization (#364) Also in this commit: add odf-core to scripts/bump_version.mjs (PACKAGE_JSONS + WORKSPACE_DEPS — it predated the package), and refresh the README granularity wording (#370 upgraded ODF compare from whole-paragraph to inline run-level tracked changes). Generated via scripts/bump_version.mjs. Ref: #372
…#379) * chore(release): bump workspace versions to 0.10.0 First minor since v0.9.1 — headline: OpenDocument (.odt) support is now installable. Covers everything accumulated on main: - ODF lane end-to-end: odf-core library (#328), provider wiring (#335), grep + insert_paragraph (#336), comments (#341), compare_documents two-file (#348), session mode (#366), intra-paragraph (run-level) tracked changes (#370) - odf-core folded into the suite release train + published as a real dependency of docx-mcp (#373); first publish bootstrapped manually at 0.9.1 with the trusted publisher configured, so this tag publishes odf-core@0.10.0 via OIDC like the rest - docx-core: formatting-fidelity comparison check (#365), reject/accept round-trip oracle stated projection-to-projection (#361), LibreOffice oracle trust-boundary characterization (#364) Also in this commit: add odf-core to scripts/bump_version.mjs (PACKAGE_JSONS + WORKSPACE_DEPS — it predated the package), and refresh the README granularity wording (#370 upgraded ODF compare from whole-paragraph to inline run-level tracked changes). Generated via scripts/bump_version.mjs. Ref: #372 * fix(odf-core): group adjacent word replacements in ODF inline compare (#378) Comparing "… by and among Zephyr BioSystems, Inc., …" against "… by and among Acme Manufacturing, Inc., …" produced an interleaved per-word redline (Acme ~~Zephyr~~ Manufacturing, ~~BioSystems,~~) instead of one grouped deletion + one grouped insertion. The token-level LCS in diffInline matches the space between the two replaced words as `equal`, which splits a single logical replacement into two delete/insert pairs; unlike the DOCX pipeline (reorderChangeBlocks / coalesceDelInsPairChains), the ODF inline diff had no whitespace-bridging pass to put them back together. Grouped redlines are what Word, Word compare, and LibreOffice all produce for multi-word replacements, so the interleaved shape reads as broken to reviewers even though it round-trips correctly. The fix is a post-pass in diffInline: a maximal window of change spans may absorb an equal span only when it is whitespace-only AND has change spans on both sides, and a window containing at least one delete and one insert is rewritten as a single delete+insert pair (the delete covers every original char in the window, bridge whitespace included; the insert every revised char). Delete-only and insert-only windows keep their bridges as `equal` — striking a kept space just to reinsert it would be noise, not grouping. The pass preserves the delete-before-insert / shared-revStart convention the emitter relies on and the lockstep-offset reconstruction invariant the property sweep pins. Verified the DOCX path does NOT have this bug on main (both rebuild and inplace group correctly over the same NVCA preamble), so the fix is scoped to odf-core. Spec scenario [OCMPI-14] added to the active add-odf-intra-paragraph-compare change. Fixes: #378
1 participant
Fixes #347. Fixes #339 (the INV-RT-001 CI flake — root cause, not a rerun band-aid).
What
The inplace reconstruction safety check compared the candidate's accept/reject projections against the raw extracted text of the inputs.
extractTextWithParagraphscounts bothw:tandw:delText, so on a pre-tracked input the raw baseline is neither projection — the check was falsified by construction on legitimate inputs and forced spurious inplace→rebuild fallbacks. The corrected law is apples-to-apples projection equality:accept-all(combined) == accept-all(revised input)reject-all(combined) == reject-all(original input)For clean inputs the projections equal the raw extraction, so the common case is a no-op. Three layers encode the corrected law in lockstep:
pipeline.tsround-trip baselines project each input through the same accept/reject operation the candidate is checked under (evaluateRoundTripSafetyonly; the soft bookmark baselines never trigger fallback and deliberately keep their raw shape).compareDocumentXml_output_text_roundtriprestated over the inputs'revisedText/originalTextprojections;inv_rt_001restated as projection equality and closed by applying the existing machine-checked lemmas on bothcombinedand the inputs. Zerosorry;#print axioms inv_rt_001listspropext, Classical.choice, Quot.sound, compareDocumentXml, compareDocumentXml_output_text_roundtrip— the only text residual axiom is unchanged in name and count; no new residual was introduced.assertRoundTripInvariantasserts the projection surface (the oldtheorem-domaintriage category collapsed into the law), andtrackedPairArbwas relaxed to the corrected oracle's scope, paragraph-insert originals included.Scope of the guarantee (deliberate)
Projection-to-projection guarantees global accept/reject text round-trip safety. It does not validate the raw mixed-revision markup surface or author provenance — a candidate whose projections are correct but whose intermediate markup is ugly or whose attribution is wrong can pass. That is the intended contract of this text oracle; the Lean axiom doc, theorem doc, and bridge prose now say so explicitly.
Discovery payoff — two engine bug classes pinned and filed
Relaxing the arbitrary did its job (aggressive discovery, bounded remediation). Every surfaced failure was adjudicated by XML before labeling:
w:insoriginals: the engine flattens the original's insertion provenance unconditionally (probed against matched / deleted / identical / unrelated revised counterparts), soreject(combined)keeps textreject(original)drops — on both reconstruction paths (the rebuild fallback output violates the law too, unchecked per DirectreconstructionMode: 'rebuild'bypasses evaluateRoundTripSafety entirely #226). Pinned by excluding the family fromtrackedOriginalScenarioArb.w:insof'I'matching a plain original word) is rescued by the rebuild fallback; the paragraph-insert shapes (either side) ship law-violating output. Pinned byhasInsProvenanceCollisionon the pair arbitrary.Both pins carry a characterization test asserting today's behavior verbatim (mode=rebuild,
failedChecks=["rejectText"], the exact reject divergences), so the eventual fixes flip it deliberately — the[LEAN-HELP-08]/G5 cadence. By contrast, paragraph-MARK provenance already threads correctly (stackedPPR-DEL(Comparison)+PPR-INS(input-author)), which the included two-author stacked-insertion test locks in: it stays inplace, carries both authors' revisions, and round-trips projection-to-projection.Plan deviation worth knowing: the plan predicted the exact #339 shape would stop falling back. It doesn't — that shape is a genuine #359 provenance conflict, and under the corrected oracle its fallback is a true positive (the rebuild output satisfies the law). What the oracle fix does eliminate is the spurious-fallback families: the PR #344 seed-1586860402 family (comment-anchor original + paragraph-insert revised) and the peer-review paragraph-insert-original families now stay inplace with empty
fallbackDiagnostics.Verification
lean-spec-bridge.test.ts: 14/14, six consecutive fresh-seed runsround-trip,round-trip-inplace,nvca-coi-regression,roundtrip-structural-invariants): 34/34lean-differential-helpers(accept/reject helpers untouched): 11/11docx-core: 1357/1357lake buildgreen; zero-sorrygrep overLeanSpike*+Tier2*verification/lean/print_axioms.leanreview scratch (untracked)Ref #344, #226.