Initial work toward PieceInclusionProof (merkle inclusion proof spec).

filecoin-project · May 2, 2019 · f9c97f7 · f9c97f7
1 parent e0d15dd
commit f9c97f7
Show file tree

Hide file tree

Showing 5 changed files with 484 additions and 0 deletions.
diff --git a/tla+/piece-inclusion-proof/.gitignore b/tla+/piece-inclusion-proof/.gitignore
@@ -0,0 +1,10 @@
+!/PieceInclusoinProof.toolbox/Model_*/*
+PieceInclusionProof.toolbox/Model_*/*.tla
+!PieceInclusionProof.toolbox/Model_*/MC.tla
+PieceInclusionProof.toolbox/Model_*/*.out
+PieceInclusionProof.toolbox/Model_*_SnapShot*/
+PieceInclusionProof.toolbox/PieceInclusionProof.*
+PieceInclusionProof.toolbox/*.launch
+PieceInclusionProof.toolbox/.*
+
+
diff --git a/tla+/piece-inclusion-proof/PieceInclusionProof.pdf b/tla+/piece-inclusion-proof/PieceInclusionProof.pdf