updated README

Author: pranavramesh2003

CaseStudies/Neem/Tactics/SalExample.lean

@@ -27,3 +27,6 @@ example (a b c : Nat) (h : a = b) : a + c = b + c := by
   sal
 
 
+
+
+

CaseStudies/Neem/WriterMonad_ENflag.lean

@@ -204,8 +204,12 @@ def splitAtMerge (lst : List ((concrete_st) × String × concrete_st)) (mergeLab
 open ProofWidgets Jsx in
 def renderBranchingTreeFromList (lst : List ((concrete_st) × String × concrete_st)) : Html :=
   let (rootPath, afterLMerge) := splitAtMerge lst "LMerge"
-  let (leftBranch, afterAMerge) := splitAtMerge afterLMerge "AMerge"
-  let (rightBranch, afterBMerge) := splitAtMerge afterAMerge "BMerge"
+  let (leftBranchFull, afterAMerge) := splitAtMerge afterLMerge "AMerge"
+  let (rightBranchFull, afterBMerge) := splitAtMerge afterAMerge "BMerge"
+
+  -- Drop the shared LCA operations from branches
+  let leftBranch := leftBranchFull.drop rootPath.length
+  let rightBranch := rightBranchFull.drop rootPath.length
 
   let finalNode := match rightBranch.getLast? with
     | some ((_, _), _, n1, n2) => (n1, n2)

CaseStudies/Neem/WriterMonad_Set.lean

@@ -173,10 +173,14 @@ def splitAtMerge' {α : Type} [ToString α] [DecidableEq α] [Hashable α]  (lst
 open ProofWidgets Jsx in
 def renderBranchingTreeFromList {α : Type} [ToString α] [DecidableEq α] [Hashable α]  (lst : List ((concrete_st_viz α) × String × concrete_st_viz α)) : Html :=
   let (rootPath, afterLMerge) := splitAtMerge lst "LMerge"
-  let (leftBranch, afterAMerge) := splitAtMerge afterLMerge "AMerge"
-  let (rightBranch, afterBMerge) := splitAtMerge afterAMerge "BMerge"
+  let (leftBranchFull, afterAMerge) := splitAtMerge afterLMerge "AMerge"
+  let (rightBranchFull, afterBMerge) := splitAtMerge afterAMerge "BMerge"
   let (mergePath,_) := splitAtMerge' lst "LMerge"
 
+  let leftBranch := leftBranchFull.drop rootPath.length
+  let rightBranch := rightBranchFull.drop rootPath.length
+
+
   let finalNode := match mergePath.getLast? with
     | some (_, _, y) => y
     | none => {_set := empty, _universe:={}}

README.md

@@ -1,15 +1,30 @@
 # Port of the Neem MRDT and CRDT Framework to Lean
 
-The code is built on top of the [Loom](https://github.com/verse-lab/loom/tree/master) repository. Initially, Loom was used to prove the correctness directly, but eventually pure Lean was used since the structures being verified did not have mutability. Therefore, some proofs use Loom and some do not. 
+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. 
 
 ## Steps to run
 
 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](CaseStudies/Neem) directory. Click on each Lean file in VS code to run all the verification conditions. 
 
 # Data structures implemented and description
 
-TODO
+| **RDT**                          | **dsimp + grind** | **Lean Blaster** | **Fallback to ITP** |
+|----------------------------------|:------:|:------:|:-------------------:|
+| Increment-only counter MRDT      | 24     | 0      | 0                   |
+| PN-counter MRDT                  | 24     | 0      | 0                   |
+| OR-set MRDT                      | 21     | 3      | 0                   |
+| Enable-Wins Flag MRDT            | 9      | 14     | 0                   |
+| Efficient OR-Set MRDT            | 22     | 2      | 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                   |
+
 
 # Counterexample generation using Plausible
 
-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](https://github.com/leanprover-community/plausible) generator was used to generate minimal examples. The section of code can be checked out [here](https://github.com/pranavramesh2003/Neem_Loom/blob/master/CaseStudies/Neem/en_wins_flag.lean#L312). We prove that both the pre and post conditions are decidable under a suitable upper bound, and generate counter examples. Subsequently, we use [Logging](https://leanprover.github.io/functional_programming_in_lean/monads.html#logging)-style monads to derive the computation tree for the left and right hand sides of the `ensures` equality. [This file](CaseStudies/Neem/WriterMonad_ENflag.lean) shows the computation path logged as a list. 
+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](https://github.com/leanprover-community/plausible) generator was used to generate minimal examples. The section of code can be checked out [here](https://github.com/pranavramesh2003/Neem_Loom/blob/master/CaseStudies/Neem/en_wins_flag.lean#L312). We prove that both the pre and post conditions are decidable under a suitable upper bound, and generate counter examples. Subsequently, we use [Logging](https://leanprover.github.io/functional_programming_in_lean/monads.html#logging)-style monads to derive the computation tree for the left and right hand sides of the `ensures` equality. [This file](CaseStudies/Neem/WriterMonad_ENflag.lean) shows the computation path logged as a list and the subsequent visualization in HTML.