OT.vfx defines application-order equality C1 and transformation-path equality C2. ResselTest.scala and ImineTest.scala expect C1 cases to prove but C2 to be rejected. This is valuable negative evidence: pairwise transformation correctness does not establish three-operation consistency. Tests inspected, not executed here.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Other · OT.C1; OT.C2; Ressel.C1_inserts/C1_deletes/C1_mix1/C1_mix2; Ressel.C2 (expected refutation)
Commit / toolchain / license
06eae81c20d9efac6c18bc5c9b67584386faa893 · VeriFx 1.0.1; Scala 2.13.1; sbt 1.4.7; Z3 backend version not independently pinned · MIT
Assumptions
Operations are enabled on the common source and mutually compatible.
Ressel priority/site identifiers distinguish concurrent operations.
SMT translation and Z3 are trusted; no kernel proof certificate inspected.
Reproduction
cd "examples/OT Verification" && sbt test
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.
tree_c1 is completed with Qed and proves equal successful results of the two transformed execution orders. TreeOt.v dependencies inspected without admitted proofs found. RichText.v contains active admit/Admitted occurrences, so the rich-text extension and whole repository must not be called fully verified. C1 alone is not a C2 or network SEC proof.
External evidence (contributor report)
source inspected
Proof assistant / theorem
Coq · tree_c1; treeOT
Commit / toolchain / license
ba4b12af3f20c4dca57ebc671e099a434441084f · README: original Coq 8.4 with Ssreflect; separate 8.8/8.13 versions mentioned · Apache-2.0
Assumptions
Underlying element OT satisfies its C1 law.
Both commands are successfully applicable to the common source tree; tie-breaking boolean is reversed between the two orders.
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.
This proof connects executable Isabelle definitions to abstract operations. Its commutation theorem gives equal logs and equal lookups, not identical concrete memory layouts. The README explicitly says the separate hand-optimized evaluation implementation is not verified; only the Isabelle-generated implementation has this correspondence.
6c23447c12a7862ff31b7fc2205f6c90fbdb9dc0 · README demonstrates Isabelle2019; AFP Collections and CRDT dependencies · MIT
Assumptions
Equal operation sets and distinct move timestamps.
Concrete hash-map equality is extensional lookup equality, not equality of memory representation.
Reproduction
cd proof && isabelle build -D .
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.