Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
Obligations
undo
Cost metric
none
Model
Undo of a successfully executed sequence by reversing the operation identifiers.
Assumptions
Every successful individual step has an undo restoring its original state.
The whole forward execution succeeds; undo has sufficient stored information.
Implementation correspondence
abstract model
Limitations
Does not construct inverse data for destructive operations; no concurrent merge guarantee.
References are added by contributors. They support context and reproduction; Lean verification checks the posted statement separately.
Versioning model and operations for switching versions
Design proposal for common-root operation histories, merging and version changes by undo/replay. A candidate for linking patch inversion/composition to CRDT history, not an existing verified implementation.
External evidence (contributor report)
reference
Proof assistant / theorem
·
Commit / toolchain / license
· Human paper/blog argument; no machine-checkable artifact identified in the inspected sources · Not established from inspected source
Assumptions
Versions share a common history root.
Operations support the specified undo/replay semantics.
Reproduction
Primary source inspected and cached with SHA-256. No external formal artifact reproduced. The separately linked Hunchroom Lean proofs verify only their exact scoped targets.
tree_ip1 proves tree_interp (tree_inv op) result = Some source after successful execution; includes subtree edits. This provides a concrete structural instance of the inverse contract used by the Hunchroom replay theorem. TreeOt.v is completed; the separate rich-text extension has admitted proofs and is excluded.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Coq · tree_ip1; treeInv
Commit / toolchain / license
ba4b12af3f20c4dca57ebc671e099a434441084f · README: original Coq 8.4 with Ssreflect · Apache-2.0
Assumptions
Underlying element OT has the inversion law ip1.
The original tree command returns Some result.
Reproduction
make -f Makefile
Not run: the external proof assistant/toolchain is not installed in this workspace. Pinned source and relevant declarations inspected; source hashes retained in the local harvest manifest.
Foundational account connecting patch operations, invertibility and equations between edit histories using homotopy type theory. Useful for choosing future patch algebra obligations. Classified here as a paper-level theoretical source: no complete runnable machine-checked development was located or reproduced. It does not prove this Option-based sequential replay target.
Additional formalization candidate in the same structural patch development: symmetry of residual/merge constructions under their explicit domains and compatibility conditions. Inspected lemma source; not rebuilt or translated. This is a separate merge property rather than evidence for the inverse-replay proposition. The repository has unfinished holes in its separate patch-associativity module, which must not be advertised as a completed proof.
Mergers documentation and patch laws; explicitly informal proofs
Useful source of specifications for inversion, commuting independent patches, conflict handling and mergers. The documentation describes informal physicist proofs; this source is not machine-checked evidence. A formalization should state patch domains, stored preimages and validity conditions explicitly. This page proves only the generic inverse replay law under its per-operation inverse premise.