Expose the redline reversibility proof on every client surface (#464) - #533
Open
JSv4 wants to merge 2 commits into
Open
Expose the redline reversibility proof on every client surface (#464)#533JSv4 wants to merge 2 commits into
JSv4 wants to merge 2 commits into
Conversation
The proof engine landed with #497 but stopped at the .NET boundary: VerificationOps had no entry point, and nothing under tools/, python/, or npm/src referenced it. Callers on every other surface could generate a redline but not prove it was honest. VerificationOps.ProveRedlineReversibility becomes the single owner of the wire shape, and the canonical redline-reversibility-proof/v1 document now reaches: WASM DocumentConverter.ProveRedlineReversibility npm proveRedlineReversibility, plus a worker path stdio op prove_redline_reversibility Python prove_redline_reversibility, decoded into frozen dataclasses MCP docxodus_track_changes action prove_reversibility Only the proof JSON crosses the facade. RedlineReversibilityProofRun's two rebuilt packages stay in-process: every transport here is a JSON wire, and base64 of two further packages would multiply the payload for evidence the proof already carries as digests and structured divergences. Three packages are inspected and two rebuilt, making this the heaviest verification operation in the library, so the browser surface gets a worker path rather than only a main-thread call. The MCP action proves the session's clean-save checkpoint -- the same bytes docxodus_get_content format 'verification' already gates -- and reads its two comparison packages through the document store, so neither can name a location outside the server's scope. It is resolved before RunTrackChangesAction so read-only evidence stays out of the docxodus_mutations batch set. The WASM budget guard is generalised from two packages to a running subtraction over any number, so a three-package call cannot overflow its way under the 100MB ceiling. Transport-seam tests on all three surfaces assert the same canonical document, determinism, digests bound to the exact inputs, and fail-closed behaviour: when a package cannot be admitted neither path is attempted, so a partial result can never be misread as evidence.
Same one-file fix as #532, carried here because it is what makes a working tree clean on any branch cut from current main: #510 committed the file with CRLF stored in the blob, bypassing the `*.csproj text eol=crlf` rule in .gitattributes, so git reports it as permanently modified. The change is line terminators only, so whichever of the two lands first, the other is a no-op.
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
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.
Track B, step 5. Closes the exposure half of #464; unblocks #465, which embeds the proof.
Problem
The proof engine landed with #497 —
RedlineReversibilityVerifier,RedlineReversibilityProof, receipt embedding viaDeliveryEvidenceKind.RedlineReversibility, ~2,200 lines of tests, and a design doc — and then stopped at the .NET boundary:Docxodus/Internal/VerificationOps.cshad no entry point for it.grep -ri reversib tools/ python/ npm/srcreturned nothing.So every non-.NET caller could generate a redline but not prove it was honest. This PR is the ripple, not new engine work: moves, multi-author preservation, and first-divergent-part/anchor reporting are already covered in core (
RP006,RP015,RP030,RP031, and the anchor assertions inRedlineReversibilityProofTests).Change
VerificationOps.ProveRedlineReversibilitybecomes the single owner of the wire shape, per theCLAUDE.mdsingle-owner rule — facade first, then outward:VerificationOps.ProveRedlineReversibilityDocumentConverter.ProveRedlineReversibilityproveRedlineReversibility(baseline, intendedFinal, redline)worker.proveRedlineReversibility(...)prove_redline_reversibilitydocx_scalpel.prove_redline_reversibility→ typedRedlineReversibilityProofdocxodus_track_changesactionprove_reversibilityThree decisions worth reviewing
Only the proof JSON crosses the facade.
RedlineReversibilityProofRunalso carries the two rebuilt packages; those stay in-process. Every transport here is a JSON wire, and base64 of two further packages would multiply the payload for evidence the proof already carries as digests plus structured divergences. A caller that genuinely needs the bytes uses the verifier directly, in-process. This matches the design doc's existing stance on why package bytes sit outside the JSON.The browser surface gets a worker path, not just a main-thread call. Three packages are inspected and two rebuilt, making this the heaviest verification operation in the library. Shipping it main-thread-only would be a regression against
verifyDeliverable, which already has both.MCP proves the session's clean-save checkpoint. Reversibility needs three packages, but every MCP tool is session-scoped, and weakening
sessionIdondocxodus_track_changesto admit a stateless form would be worse than the alternative: the open session is the redline, andbaselinePath/intendedFinalPathresolve through the document store like any other location, so neither can escape the server's scope. Proving the clean-save checkpoint — rather than the anchor-annotated working copy — matches whatdocxodus_get_content(format: "verification")already gates, so an agent proves what it would ship. This required no new core method, keeps the tool count flat, and is resolved inTrackChangesbeforeRunTrackChangesAction, so read-only evidence stays out of thedocxodus_mutationsbatch set.Incidental
The WASM aggregate byte guard went from a hardcoded two-package check to a running subtraction over any number of packages, so a three-package call cannot overflow its way under the 100MB ceiling.
ArgumentNullException.ThrowIfNull(docxBytes)moved to the two existing call sites so their null contract is unchanged.Tests
Transport-seam tests only — the engine is already covered. Each asserts the same canonical document, determinism (a receipt digest depends on it), digests bound to the exact inputs passed, and fail-closed behaviour: when a package cannot be admitted, neither path is attempted, so a partial result can never be misread as evidence.
Docxodus.Tests/RedlineReversibilityTransportTests.cs— facade byte-identical to the engine's canonical form, lowered limits constraining the proof rather than rejecting it afterwards, the MCP action end-to-end including an out-of-scope path refusal, and thatprove_reversibilityis advertised but not batchable.python/tests/test_redline_reversibility.py— typed decode through the stdio host, enums decoding as enums on nested divergences, each path'sexpectedPackagebeing the document it must reproduce.npm/tests/redline-reversibility.spec.ts— the trimmed WASM export through the browser harness.Verification
npx tsc --noEmitandnpx tsc --noEmit -p tsconfig.tests.jsonboth clean; the Python package imports with no duplicate or dangling__all__entries. The .NET and Playwright suites were not run locally — this container has no .NET SDK (dotnetis absent), so the C# additions and the browser spec are compiled and executed by CI for the first time. Worth a closer read on the C# hunks than usual.Note on the second commit
chore(git): renormalize Docxodus.Tests.csproj line endingsduplicates #532. #510 stored that file's blob with CRLF, bypassing*.csproj text eol=crlfin.gitattributes, so it reports as permanently modified in every working tree cut from current main — including this one. The change is line terminators only; whichever of the two PRs lands first, the other becomes a no-op.Generated by Claude Code