This repository contains a port of various CRDTs and MRDTs from the Neem framework to Lean. It also comes equipped with a custom tactic called sal and a counterexample generation and visualization framework.
Clone this repository, and run lake update followed by lake build. Ensure that the Lean version in lean-toolchain stays at v4.26.0. The various proofs are in the Neem directory. Click on each Lean file in VS code to run all the verification conditions.
| RDT | dsimp + grind | Lean Blaster | Fallback to ITP |
|---|---|---|---|
| Increment-only counter MRDT | 24 | 0 | 0 |
| PN-counter MRDT | 24 | 0 | 0 |
| OR-set MRDT | 3 | 21 | 0 |
| Enable-Wins Flag MRDT | 9 | 14 | 0 |
| Efficient OR-Set MRDT | 2 | 22 | 0 |
| Grows-only set MRDT | 24 | 0 | 0 |
| Grows-only map MRDT | 22 | 0 | 2 |
| Replicated Growable Array MRDT | 15 | 9 | 0 |
| Multi-valued Register MRDT | 24 | 0 | 0 |
| Increment-only counter CRDT | 24 | 0 | 0 |
| PN-counter CRDT | 16 | 2 | 6 |
| Multi-Valued Register CRDT | 24 | 0 | 0 |
| OR-set CRDT | 4 | 19 | 1 |
Our implementation of the en-wins flag was erroneous, and it did not pass the inter_right_1op VC. Earlier, the counterexample needed to be worked out manually, but we can now automatically generate small counter-examples. The Plausible generator was used to generate minimal examples. The section of code can be checked out here. We prove that both the pre and post conditions are decidable under a suitable upper bound, and generate counter examples. Subsequently, we use Logging-style monads to derive the computation tree for the left and right hand sides of the ensures equality. This file shows the computation path logged as a list and the subsequent visualization in HTML.