test(docx-comparison): field-bearing fast-check arbitrary for the Lean spec bridge#294
Conversation
…ange Approved OpenSpec proposal for a field-bearing fast-check arbitrary in the Lean spec bridge test. Generalizes the three single NUMPAGES field fixtures into a property over field type (NUMPAGES/PAGE/PAGEREF) x operation (insert/delete/stable/text-only) x placement, falsifying both residual axioms (compareDocumentXml_output_preservation_friendly and compareDocumentXml_output_text_roundtrip) over generated field documents. Test-layer only: no Lean changes, no production-engine changes. Two load-bearing design decisions recorded in design.md: (1) per-operation assertion strength (field-delete drops to document-level assertFieldInvariant because post-#217 fragmentation makes <w:del> subtrees non-context-neutral); (2) fallback treated as falsification + coverage floor rather than silent fc.pre filtering. openspec validate add-field-bearing-bridge-arbitrary --strict passes.
…Lean spec bridge Generalizes the three single NUMPAGES field fixtures in lean-spec-bridge.test.ts into a property over field type (NUMPAGES/PAGE/PAGEREF) x operation (field-insert / field-delete / field-stable / text-only) x placement, driving randomly-generated clean field-bearing document pairs through the live inplace comparison engine to falsify both residual axioms (compareDocumentXml_output_preservation_friendly, INV-FIELD-001; and compareDocumentXml_output_text_roundtrip, INV-RT-001) over a far wider surface than three fixed XML strings. Why this matters: the field-bearing surface (w:fldChar / w:instrText / w:delInstrText atoms exercising the field-walk and the delInstrText->instrText rename) is the riskiest part of the axioms' domain and previously had only single-fixture empirical grounding. The two field-free arbitraries (pairArb, trackedPairArb) never touch it. Two load-bearing design decisions (see design.md): - Per-operation assertion strength: field-insert/stable/text-only runs assert the stronger assertRecursivelyWellformed (per-subtree fieldContextNeutral forall ctx) in addition to the document-level assertFieldInvariant; field-delete runs assert only assertFieldInvariant, because post-#217 the inplace atomizer fragments deleted fields so the <w:del> subtrees are not context-neutral. The generator's operation tag is the honest discriminator (not output-XML inspection). - Fallback = falsification + coverage floor, not silent fc.pre filtering: the arbitrary is constrained to whole-complete-field-at-run-boundary shapes the existing fixtures prove are inplace-safe; assertInplaceResult keeps throwing on fallback, and the operation x type coverage assertion is the floor against a degenerate all-fallback run. The 12 operation x type combos are also seeded via fast-check `examples` so the floor is deterministic on top of 100 random runs. Field XML sourced from the shared COMPLETE_* constants via new paragraphWithField / paragraphWithText helpers in ooxml-fixtures.ts (issue #221 drift rule). Header comment blocks updated so the file no longer oversells field-free-ness now that a field-bearing generator exists (asymmetry-of-rot). ROADMAP follow-up flipped to delivered. Traceability via .openspec([LEAN-FBA-NN]) tags (matrix auto-generates on archive). Test-layer only: no Lean changes, no production-engine changes. Verified locally: docx-core build + lint (tsc --noEmit) + full suite (1290 passed) + check:spec-coverage + conformance checks all green. Peer review (Gemini + Codex) pending before merge. Implements openspec/changes/add-field-bearing-bridge-arbitrary.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
LLM-Based Quality GateOverall: ✅ PASS (14 pass · 0 warn · 14 total)
Full checklist questions
Estimated cost (this run): $0.0616 — 198,610 input + 756 output tokens (≈4 chars/token) on |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…examples
Peer review (Codex, dynamic) found that fast-check consumes `examples` from
WITHIN the `numRuns` budget, not in addition to it — so `{ numRuns: 100,
examples: <12> }` ran 12 examples + 88 random = 100 total, not 112. The claim
of "100 random runs plus 12 deterministic examples" in the test/tasks was
therefore overstated (asymmetry-of-rot).
Fix: set the budget to `NUM_RUNS + fieldBearingExampleArgs.length` on both
field-bearing properties so all 12 deterministic operation×type combos run AND
a full NUM_RUNS (100) random cases run. Documents the fast-check budget
semantics at the examples definition and both call sites; aligns tasks.md.
Codex evidence: numRuns:10 + 3 examples yielded exactly 10 executions
(3 examples, 7 random). Re-verified: lint (tsc --noEmit) clean; both
properties green at 112 runs each.
No behavior change to the assertions; coverage floor unchanged.
Peer review (Gemini + Codex) — 2026-06-02Codex (dynamic, executed): Ran the bridge tests package-scoped and stressed at
One Medium finding (resolved): fast-check consumes Gemini (static only): Execution was unavailable in its sandbox ( Resolution: the single finding is fixed and re-verified; both load-bearing design decisions are empirically validated by Codex's execution. |
|
Re-review note: the focused re-review CLI crashed (tooling, not a finding), so I verified the fix directly with the same method Codex used — |
CI `allure-labels` failed: once this file carries `.openspec([LEAN-FBA-*])`
traceability tags, validate_allure_test_labels.mjs requires a named
`const TEST_FEATURE = ...` for deterministic Allure feature mapping (matching
openspec.traceability.test.ts / openspec.priority-scenarios.test.ts).
Hoist the existing friendly feature label 'Lean Spec Bridge (fast-check)' into
a TEST_FEATURE const and reference it via .withLabels({ feature: TEST_FEATURE }).
No label-value change (Allure grouping unchanged); using a const reference also
keeps it clear of the slug-literal Title-Case check.
Re-verified: check:allure-labels / -quality / -filenames pass; lint clean;
bridge properties green.
✅ Post-merge smoke passedMerged: Steps
Test-layer change (no production-engine code), so no real-document fixture run applies; the smoke exercises the new arbitrary against the live inplace engine plus the full regression suite. LLM gate ( Log: |
✅ Post-merge smoke passed (real-document, document-shaped)Merged: This PR touches Steps
Real-world fixture
Cleanup (already completed in the merge turn)
Log: |
…d-bearing arbitrary (#295) Both changes are merged on main but were left unarchived: - add-inv-rt-001-proof (PR #293) — closes inv_rt_001, zero-sorry spike - add-field-bearing-bridge-arbitrary (PR #294) — field-bearing fast-check arbitrary `openspec archive` moves each change into changes/archive/ and applies its delta to the canonical docx-comparison spec (two new requirements + their [LEAN-RT-*] / [LEAN-FBA-*] scenarios). The traceability matrix is regenerated to reflect the now- canonical scenarios; the Lean-build-verified (LEAN-RT-01/02/03), doc-verified (LEAN-RT-04) and falsifiability-bridge (LEAN-RT-05) scenarios show as unmapped in the vitest matrix by design, and check:spec-coverage stays green (PASS: canonical scenarios covered). Docs/spec only — no production-engine or test code changed.
…Lean spec bridge (#296) * test(docx-comparison): fragmented-field fast-check arbitrary for the Lean spec bridge Widens the field-bearing falsifiability layer for the two residual axioms (INV-FIELD-001 / INV-RT-001) to the fragmented-field surface the predecessor (add-field-bearing-bridge-arbitrary, #294) explicitly deferred: a field whose result run changes under track changes, and/or a pre-tracked field whose instruction code is already split into <w:ins>/<w:del>. Empirically grounded: probing the live engine showed it CORRECTLY falls back from inplace to rebuild on the clean->pretracked-fragmented + result-change operation (its inplace candidate fails ONLY the fieldStructure safety check — the #217 fldChar-in-del class — while acceptText/rejectText pass). So the predecessor's "fallback = falsification" rule does not hold here. The new `fragmentedFieldPairArb` property asserts the axioms MODE-INDEPENDENTLY (on the resolved accept/reject projections, never the raw combined output) and a mode-distribution coverage floor requires BOTH inplace and fallback outcomes to be observed, so a silent all-inplace/all-fallback regression fails loudly. Test-layer only: no Lean changes, no production-engine changes. The fallback is the engine's correct defensive behavior, not a bug to fix. - ooxml-fixtures.ts: add completeField / fragmentedFieldModification / FIELD_INSTRUCTIONS; refactor COMPLETE_* and FRAGMENTED_NUMPAGES_MODIFICATION onto them (byte-identical values). - lean-spec-bridge.test.ts: fragmentedFieldPairArb + mode-independent property + mode-distribution coverage floor; header Coverage/Fallback blocks updated. - OpenSpec change add-fragmented-field-bridge-arbitrary (ADD-only delta, [LEAN-FRAG-01..04]); nested + paragraph-spanning fields deferred to successor. Peer review (Gemini + Codex) pending. * test(docx-comparison): single-line LEAN-FRAG openspec tags for clean coverage mapping Codex peer review: the multiline .openspec(...) calls with trailing commas defeated the check:spec-coverage parser (regex expects .openspec('...') on one line), so the FRAG block was reported as one Extra-scenario blob instead of mapping [LEAN-FRAG-01..04] individually. Reformat to single-line, matching the existing [LEAN-FBA-02..05] style. No behavior change.
1 participant
Summary
Generalizes the three single NUMPAGES field fixtures in
lean-spec-bridge.test.tsinto a fast-check arbitrary that drives randomly-generated clean field-bearing document pairs through the live inplace comparison engine, falsifying both residual axioms over field type × operation × placement instead of three fixed XML strings.Implements the approved OpenSpec change
add-field-bearing-bridge-arbitrary— the follow-up deferred by name from Tier 2 (add-ooxml-doc-subset-and-inv-field-001-proof) and fromadd-inv-rt-001-proof.Test-layer only: no Lean changes, no production-engine changes.
Why
The field-bearing surface —
w:fldChar/w:instrText/w:delInstrTextatoms exercising the field-walk and thedelInstrText → instrTextrename — is the riskiest part of the two axioms' domain (compareDocumentXml_output_preservation_friendly/compareDocumentXml_output_text_roundtrip), and previously had only single-fixture empirical grounding. The two field-free arbitraries (pairArb,trackedPairArb) never touch it.Implementation
fieldBearingPairArbover{field-insert, field-delete, field-stable, text-only}×{NUMPAGES, PAGE, PAGEREF}, clean inputs (engine generates all tracking — the analogue ofpairArb, nottrackedPairArb).numRuns: 100, plus all 12 operation×type combos seeded via fast-checkexamplesso the coverage floor is deterministic.COMPLETE_*constants via newparagraphWithField/paragraphWithTexthelpers inooxml-fixtures.ts(issue Extract shared XML test fixtures (NUMPAGES field, DOCX skeleton, fldChar primitives) into a single fixtures module #221 drift rule)..openspec([LEAN-FBA-NN])tags.Two load-bearing design decisions (design.md)
field-insert/stable/text-onlyruns assert the strongerassertRecursivelyWellformedandassertFieldInvariant;field-deleteruns assertassertFieldInvariantonly — post-inplace atomizer: emit fragmented fields per ECMA-376 Part 4 (split <w:ins>/<w:del> at field-character boundaries) #217 fragmentation makes deleted<w:del>subtrees non-context-neutral. The generator's operation tag is the discriminator (not output-XML inspection).fc.pre. The arbitrary is constrained to whole-field-at-run-boundary shapes the existing fixtures prove are inplace-safe;assertInplaceResultkeeps throwing on fallback; the operation×type coverage assertion is the floor against a degenerate all-fallback run.Verification (local)
npm run build -w @usejunior/docx-core— cleannpm run lint -w @usejunior/docx-core(tsc --noEmit, typechecks tests) — cleannpm run check:spec-coverage— PASS (both workspaces)npm run check:conformance-citations && check:conformance-doc— OKOpenSpec
openspec/changes/add-field-bearing-bridge-arbitrary/(proposal, design, tasks,docx-comparisondelta with[LEAN-FBA-01..05])openspec validate add-field-bearing-bridge-arbitrary --strictpasses