Added Quint specification

formal_spec/ITF_files/scenario.json

@@ -0,0 +1,98 @@
+{
+    "#meta": {
+        "source": "tests.qnt",
+        "status": "violation",
+        "generatedBy": "Quint",
+        "timestamp": 1681461155649
+    },
+    "vars": [
+        "leaves_namespace_idx_v",
+        "namespace_v",
+        "namespaceIdFound_v"
+    ],
+    "testCases": [
+        {
+            "name": "5 leaves and not found but within range",
+            "states": [
+            {
+                "leaves_namespace_idx_v": [
+                    39
+                ],
+                "namespace_v": 56,
+                "namespaceIdFound_v": false
+            },
+            {
+                "leaves_namespace_idx_v": [
+                    39,
+                    71
+                ],
+                "namespace_v": 56,
+                "namespaceIdFound_v": false
+            },
+            {
+                "leaves_namespace_idx_v": [
+                    39,
+                    71,
+                    92
+                ],
+                "namespace_v": 56,
+                "namespaceIdFound_v": false
+            },
+            {
+                "leaves_namespace_idx_v": [
+                    39,
+                    71,
+                    92,
+                    92
+                ],
+                "namespace_v": 56,
+                "namespaceIdFound_v": false
+            },
+            {
+                "leaves_namespace_idx_v": [
+                    39,
+                    71,
+                    92,
+                    92,
+                    100
+                ],
+                "namespace_v": 56,
+                "namespaceIdFound_v": false
+            }
+            ]
+        },
+        {
+            "name": "two leaves and found",
+            "states": [
+                {
+                    "leaves_namespace_idx_v": [
+                        42
+                    ],
+                    "namespace_v": 56,
+                    "namespaceIdFound_v": false
+                },
+                {
+                    "leaves_namespace_idx_v": [
+                        42,
+                        56
+                    ],
+                    "namespace_v": 56,
+                    "namespaceIdFound_v": true
+                }
+            ]
+        },
+        {
+            "name": "not found",
+            "states": [
+                {
+                    "leaves_namespace_idx_v": [
+                        39
+                    ],
+                    "namespace_v": 94,
+                    "namespaceIdFound_v": false
+                }
+            ]
+        }
+    ]
+
+}

formal_spec/tests.qnt

@@ -0,0 +1,114 @@
+module basics {
+
+    def listToSet(l: List[a]) : Set[a] = 
+        l.foldl(Set(), (acc, x) => union(acc, Set(x)))
+
+    def min(S: Set[int]) : int = 
+        // val tentativeMin = chooseSome(S) ---> chooseSome is not supported yet
+        val tentativeMin = -1
+        S.fold(
+            tentativeMin, 
+            (acc, i) => if ((acc == tentativeMin) or (i < acc)) i else acc
+            )
+
+
+    def max(S: Set[int]) : int = 
+        // val tentativeMax = chooseSome(S) --> chooseSome not supported yet
+        val tentativeMax = -1
+        S.fold(
+            tentativeMax, 
+            (acc, i) => if ((acc == -1) or (i > acc)) i else acc
+            )
+
+
+}
+
+// This module creates leaves with namespaces and a namespace id to search for.
+// Its purpose is to create data for tests similar to those from 
+// nmt_test.go::TestNamespacedMerkleTree_ProveNamespace_Ranges_And_Verify
+// 
+// The approach taken here is different from the one in nmt.qnt: here,
+// in every step, one leaf is generated. Thus, the final test data is available in the 
+// last step
+
+module tests {     
+
+    import basics.*
+    pure val MAX_NAMESPACE_ID = 100
+
+    var leaves_namespace_idx_v : List[int]
+    var namespace_v : int  
+    var namespaceIdFound_v : bool
+
+    // syntactic sugar, for better readability
+    def require(pred: bool) : bool = pred
+
+    action init = {
+        nondet first_element = oneOf(0.to(MAX_NAMESPACE_ID))
+        nondet namespace = oneOf(0.to(MAX_NAMESPACE_ID))
+        all {                        
+            leaves_namespace_idx_v' = [first_element],                        
+            namespace_v' = namespace,  
+            namespaceIdFound_v' = first_element == namespace
+        }
+    }
+
+    action step = {
+        val l = length(leaves_namespace_idx_v)
+        val lastElement = leaves_namespace_idx_v[l-1]
+        nondet new_index = oneOf(
+                lastElement.to(MAX_NAMESPACE_ID)                    
+            )            
+        all{   
+            require(lastElement < MAX_NAMESPACE_ID),                                             
+            leaves_namespace_idx_v' = append(leaves_namespace_idx_v, new_index),
+            namespace_v' = namespace_v,
+            namespaceIdFound_v' = (namespaceIdFound_v or (new_index == namespace_v))
+        }
+    }
+
+    // 
+    // test scenarios, as originally described in nmt_test.go
+    //     
+
+    // original test comment (from nmt_test.go): "not found",
+    val namespaceIdNotFound =               
+        val leavesSet = listToSet(leaves_namespace_idx_v)
+        not(leavesSet.contains(namespace_v))
+
+    val namespaceIdNotFoundTest =                 
+            not(namespaceIdNotFound)
+
+
+
+    // original test comment (from nmt_test.go): "two leaves and found"
+    val twoLeavesAndFound = 
+        and{
+            length(leaves_namespace_idx_v) == 2,
+            val leavesSet = listToSet(leaves_namespace_idx_v)
+            leavesSet.contains(namespace_v)
+        }
+
+    val twoLeavesAndFoundTest = 
+        not(twoLeavesAndFound)
+
+
+    // original test comment (from nmt_test.go): "5 leaves and not found but within range"
+    val fiveLeavesAndNotFoundButWithinRange = 
+        val leavesSet = listToSet(leaves_namespace_idx_v)
+        and{
+            length(leaves_namespace_idx_v) == 5,            
+            not(leavesSet.contains(namespace_v)),
+            min(leavesSet) < namespace_v,
+            max(leavesSet) > namespace_v
+        }
+
+    val fiveLeavesAndNotFoundButWithinRangeTest = 
+        not(fiveLeavesAndNotFoundButWithinRange)
+
+
+
+
+
+
+}

simulation_test.go

@@ -12,8 +12,8 @@ import (
 
 const nidSize = 2
 
-func getLeavesFromState(state gjson.Result, nidSize int) [][]byte {
-	itf_leaves := state.Get("leaves_v").Array()
+func getLeavesFromState(state gjson.Result, nidSize int, key string) [][]byte {
+	itf_leaves := state.Get(key).Array()
 	var leaves [][]byte
 
 	for _, itf_leaf := range itf_leaves {
@@ -97,7 +97,7 @@ func TestFromITF(t *testing.T) {
 		// only the states marked "final"
 		if state.Get("state_v").String() == "final" {
 			modelNamespace := int(state.Get("namespace_v").Int())
-			modelLeaves := getLeavesFromState(state, nidSize)
+			modelLeaves := getLeavesFromState(state, nidSize, "leaves_v")
 			modelProof := state.Get("proof_v")
 			corrupted := state.Get("corrupted").Bool()
 			t.Logf("Obtained state data:\n\tState namespace: %v\n\tleaves: %v\n\tcorrupted: %v\n",
@@ -167,3 +167,55 @@ func TestFromITF(t *testing.T) {
 
 	}
 }
+
+func TestFromScenario(t *testing.T) {
+	itfFileName := "formal_spec/ITF_files/scenario.json"
+	data, err := ioutil.ReadFile(itfFileName)
+	if err != nil {
+		t.Errorf("Error opening file: %v", err)
+	}
+	tests := gjson.GetBytes(data, "testCases").Array()
+
+	for _, tt := range tests {
+		states := tt.Get("states").Array()
+		lastState := states[len(states)-1]
+		namespaceId := int(lastState.Get("namespace_v").Int())
+
+		itf_leaves := lastState.Get("leaves_namespace_idx_v").Array()
+
+		tree := nmt.New(sha256.New(), nmt.NamespaceIDSize(nidSize))
+		for _, itf_leaf := range itf_leaves {
+			leaf_id := int(itf_leaf.Int())
+			pushData := namespace.PrefixedData(append(
+				intToBytes(leaf_id, nidSize),
+				[]byte("dummy_data")...))
+			err := tree.Push(pushData)
+			if err != nil {
+				t.Fatalf("invalid test case: %v, error on Push(): %v", tt.Get("name").String(), err)
+			}
+		}
+		proveNID := intToBytes(namespaceId, nidSize)
+		gotProof, err := tree.ProveNamespace(proveNID)
+		if err != nil {
+			t.Fatalf("ProveNamespace() unexpected error: %v", err)
+		}
+
+		gotFound := gotProof.IsNonEmptyRange() && len(gotProof.LeafHash()) == 0
+		wantFound := lastState.Get("namespaceIdFound_v").Bool()
+
+		if gotFound != wantFound {
+			t.Errorf("Proof.ProveNamespace() gotFound = %v, wantFound = %v ", gotFound, wantFound)
+		}
+
+		// Verification round-trip should always pass:
+		gotGetLeaves := tree.Get(proveNID)
+		r, err := tree.Root()
+		if err != nil {
+			t.Fatalf("Root() unexpected error: %v", err)
+		}
+		gotChecksOut := gotProof.VerifyNamespace(sha256.New(), proveNID, gotGetLeaves, r)
+		if !gotChecksOut {
+			t.Errorf("Proof.VerifyNamespace() gotChecksOut: %v, want: true", gotChecksOut)
+		}
+	}
+}