From eb927ae83c744547c46f1fbc51b1e178038dafe6 Mon Sep 17 00:00:00 2001 From: Rootul P Date: Wed, 17 Apr 2024 19:01:07 -0400 Subject: [PATCH] chore: rename master to main (#249) Closes https://github.com/celestiaorg/nmt/issues/171 --- .github/workflows/go.yml | 2 +- .github/workflows/lint.yml | 4 +- README.md | 4 +- docs/nmt-lib.md | 6 +- nmt.go | 4 +- nmt_quint_model/README.md | 8 +- nmt_quint_model/nmt.qnt | 370 ++++++++++++++++++------------------- proof.go | 2 +- 8 files changed, 200 insertions(+), 200 deletions(-) diff --git a/.github/workflows/go.yml b/.github/workflows/go.yml index 1c56fef..5e94c02 100644 --- a/.github/workflows/go.yml +++ b/.github/workflows/go.yml @@ -2,7 +2,7 @@ name: Go on: push: - branches: [ master ] + branches: [ main ] pull_request: jobs: diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index bfb51f9..d6668cd 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -3,10 +3,10 @@ on: pull_request: push: branches: - - master + - main jobs: # Runs golangci-lint over the nmt repository - # This workflow is run on every pull request and push to master + # This workflow is run on every pull request and push to main # The `golangci` job will pass without running if no *.{go, mod, sum} files have been modified. golangci: name: golangci-lint diff --git a/README.md b/README.md index 3691a31..7398395 100644 --- a/README.md +++ b/README.md @@ -2,9 +2,9 @@ ![Go version](https://img.shields.io/badge/go-1.21-blue.svg) [![Go Reference](https://pkg.go.dev/badge/github.com/celestiaorg/nmt.svg)](https://pkg.go.dev/github.com/celestiaorg/nmt) -![golangci-lint](https://github.com/celestiaorg/nmt/workflows/golangci-lint/badge.svg?branch=master) +![golangci-lint](https://github.com/celestiaorg/nmt/workflows/golangci-lint/badge.svg?branch=main) ![Go](https://github.com/celestiaorg/nmt/workflows/Go/badge.svg) -![codecov.io](https://codecov.io/github/celestiaorg/nmt/coverage.svg?branch=master) +![codecov.io](https://codecov.io/github/celestiaorg/nmt/coverage.svg?branch=main) A Namespaced Merkle Tree is > [...] an ordered Merkle tree that uses a modified hash function diff --git a/docs/nmt-lib.md b/docs/nmt-lib.md index 557ef6f..44a1cd3 100644 --- a/docs/nmt-lib.md +++ b/docs/nmt-lib.md @@ -47,7 +47,7 @@ idSize := tree.NamespaceSize() // outputs 1 If the NMT is configured with `IgnoreMaxNamespace` set to true (the flag is explained [here](#nmt-initialization-and-configuration)), then the calculation of the namespace ID range of non-leaf nodes in the [namespace hash function](./spec/nmt.md#namespaced-hash) will change slightly. That is, if the right child of a node is entirely filled with leaves with the maximum possible namespace `maxPossibleNamespace`, i.e., its minimum and maximum namespace are equal to the `maxPossibleNamespace`, then the right child is excluded from the calculation of the namespace ID range of the parent node, and the parent node inherits the namespace range of the left child. In the preceding code example with the ID size of `1` byte, the value of `maxPossibleNamespace` is $2^8-1 = 0xFF$. -Concretely, consider a node `n` with children `l` and `r`. If `r.minNs` and `r.maxNs` are both equal to `maxPossibleNamespace` (indicating that it represents the root of a subtree whose leaves all have the namespace ID of `maxPossibleNamespace`), then the namespace ID range of `n` is set to the namespace range of `l`, i.e., `n.MinNs = l.MinNs` and `n.MaxNs = l.MaxNs`. +Concretely, consider a node `n` with children `l` and `r`. If `r.minNs` and `r.maxNs` are both equal to `maxPossibleNamespace` (indicating that it represents the root of a subtree whose leaves all have the namespace ID of `maxPossibleNamespace`), then the namespace ID range of `n` is set to the namespace range of `l`, i.e., `n.MinNs = l.MinNs` and `n.MaxNs = l.MaxNs`. Otherwise, the namespace ID range of `n` is set as normal i.e., `n.minNs = min(l.minNs, r.minNs)` and `n.maxNs = max(l.maxNs, r.maxNs)`. Note that the `IgnoreMaxNamespace` flag is Celestia-specific and is motivated by the fact that half of the data items in the NMT are associated with reserved namespace IDs (i.e., the highest possible value within the ID size) and do not need to be queried using their namespace IDs. @@ -80,7 +80,7 @@ d2 := namespace.PrefixedData(append(namespace.ID{1}, []byte("leaf_2")...)) if err := tree.Push(d2); err != nil { // something went wrong } -d3 := namespace.PrefixedData(append(namespace.ID{3}, []byte("leaf_3")...)) +d3 := namespace.PrefixedData(append(namespace.ID{3}, []byte("leaf_3")...)) if err := tree.Push(d3); err != nil { // something went wrong } @@ -186,7 +186,7 @@ In the example given earlier, each node is `34` bytes in length and takes the fo ## Verify Namespace Proof -The correctness of a namespace `Proof` for a specific namespace ID `nID` can be verified using the [`VerifyNamespace`](https://github.com/celestiaorg/nmt/blob/master/proof.go) method. +The correctness of a namespace `Proof` for a specific namespace ID `nID` can be verified using the [`VerifyNamespace`](https://github.com/celestiaorg/nmt/blob/main/proof.go) method. ```go func (proof Proof) VerifyNamespace(h hash.Hash, nID namespace.ID, leaves [][]byte, root []byte) bool diff --git a/nmt.go b/nmt.go index 869f081..e9c318a 100644 --- a/nmt.go +++ b/nmt.go @@ -1,5 +1,5 @@ // Package nmt contains an NMT implementation. -// The specifications can be found in https://github.com/celestiaorg/nmt/blob/master/docs/spec/nmt.md. +// The specifications can be found in https://github.com/celestiaorg/nmt/blob/main/docs/spec/nmt.md. package nmt import ( @@ -69,7 +69,7 @@ func NamespaceIDSize(size int) Option { // IgnoreMaxNamespace sets whether the largest possible namespace.ID MAX_NID // should be 'ignored'. If set to true, this allows for shorter proofs in // particular use-cases. E.g., see: -// https://github.com/celestiaorg/celestiaorg-specs/blob/master/specs/data_structures.md#namespace-merkle-tree +// https://github.com/celestiaorg/celestiaorg-specs/blob/main/specs/data_structures.md#namespace-merkle-tree // Defaults to true. func IgnoreMaxNamespace(ignore bool) Option { return func(opts *Options) { diff --git a/nmt_quint_model/README.md b/nmt_quint_model/README.md index aa820e8..cdb83f5 100644 --- a/nmt_quint_model/README.md +++ b/nmt_quint_model/README.md @@ -33,7 +33,7 @@ is necessary. translates them to function calls.) The generation of the tests happens through simulation. In that sense, it is similar to the existing tests -[fuzz_test.go](https://github.com/celestiaorg/nmt/blob/master/fuzz_test.go), +[fuzz_test.go](https://github.com/celestiaorg/nmt/blob/main/fuzz_test.go), except that it also adds corruption of the data. - Having specifications written in Quint makes it possible to change tests/specs quickly: @@ -110,13 +110,13 @@ verifyInclusionProof(proofZero, c_root, 0, [{ value: ("data", 0), namespaceId: 2 import nmtProofVerification.* // runs the initialization action -init +init // runs one step of the model -step +step // runs another step of the model -step +step ``` After getting acquainted with all the operators, diff --git a/nmt_quint_model/nmt.qnt b/nmt_quint_model/nmt.qnt index be96ef0..40d8acf 100644 --- a/nmt_quint_model/nmt.qnt +++ b/nmt_quint_model/nmt.qnt @@ -1,19 +1,19 @@ // -*- mode: Bluespec; -*- // This file contains a Quint specification of the (part of the) Namespaced Merkle Tree -// library. +// library. // The specification is written in Quint (https://github.com/informalsystems/quint), a modern specification // language based on TLA. -// +// // The file is split into five modules: // - basics: some basic functions and types // - nmt_helpers: helper function (e.g., generation of trees, pairwise hashing etc.) // - nmt: creation of NMT proof and their verification -// - nmtProofVerification: actions that generate proofs and verify them, thereby checking if +// - nmtProofVerification: actions that generate proofs and verify them, thereby checking if // the logic of the spec is sound // - nmtTest: actions that generate proof and non-deterministically corrupt them afterwards, // whose output can be used in test generation -// +// // The specification models Inclusion proofs, but does not model Absence proofs. module basics{ @@ -34,48 +34,48 @@ module basics{ acc } ) - - // this function gets the first power of + + // this function gets the first power of // 2 which is greater than `lastNode` def getFullTreeSize(lastNode : int) : int = if (lastNode == 0) 1 else 2^length(binary(lastNode)) - + def sum(list: List[int]) : int = list.foldl(0, (acc, i) => acc + i) - - def min(S: Set[int]) : int = + + def min(S: Set[int]) : int = // val tentativeMin = chooseSome(S) ---> chooseSome is not supported yet val tentativeMin = -1 S.fold( - tentativeMin, + tentativeMin, (acc, i) => if ((acc == tentativeMin) or (i < acc)) i else acc ) - def listToSet(S: List[int]) : Set[int] = + def listToSet(S: List[int]) : Set[int] = S.foldl(Set(), (acc, i) => acc.union(Set(i))) - def setToSortedList(S: Set[int]) : List[int] = + def setToSortedList(S: Set[int]) : List[int] = S.fold( - [], + [], (acc, i) => acc.concat( [min(S.exclude(listToSet(acc)))] ) ) - def max(S: Set[int]) : int = + def max(S: Set[int]) : int = // val tentativeMax = chooseSome(S) --> chooseSome not supported yet val tentativeMax = -1 S.fold( - tentativeMax, + tentativeMax, (acc, i) => if ((acc == -1) or (i > acc)) i else acc ) - - - + + + def reverse(L: List[x]) : List[x] = L.foldl([], (acc, i) => [i].concat(acc)) @@ -84,7 +84,7 @@ module basics{ if (mapX.keys().contains(key)) mapX.get(key) else - default + default } @@ -101,14 +101,14 @@ module nmt_helpers{ // corresponding data at leaf nodes and hashes of all nodes. // the root of the tree has index 1, its child 2 and 3 etc. (as captured in functions // `getParentIdx`, `getLeftChildidx` and `getRightChildIdx`) - // + // type TREE = { - leaves: NODE_IDX -> DATA_ITEM, - hashes: NODE_IDX -> NAMESPACE_HASH + leaves: NODE_IDX -> DATA_ITEM, + hashes: NODE_IDX -> NAMESPACE_HASH } type NAMESPACE_HASH = {minNS: int, maxNS: int, hash: WORD} - + type PROOF = {start: int, end: int, supporting_hashes: List[NAMESPACE_HASH]} type DATA = (str, int) @@ -141,10 +141,10 @@ module nmt_helpers{ concat(concat(left, middle), right) - // takes a list and maps it to a new list which contains hashes + // takes a list and maps it to a new list which contains hashes // of consecutive pairs of elements from the original list def pairwiseHash(dataList: WORD) : WORD = - + if (length(dataList) == 1) dataList else @@ -156,29 +156,29 @@ module nmt_helpers{ else acc.concat(Hash(concat([dataList[i-1]],[dataList[i]]))) } - ) + ) // This function takes as parameters: // - `namespaceBordersSet`: a sorted list of integers which defines borders between different namespaces. - // For instance, [3, 5] would indicate that leaves 0,1,2, belong to a same namespace; leaves 3 and 4 to another namespace; + // For instance, [3, 5] would indicate that leaves 0,1,2, belong to a same namespace; leaves 3 and 4 to another namespace; // leaf 5 and all leaves after 5 to a third namespace. // - `power`: an integer defining the height of the tree. The tree will have 2^(power-1) leaves - // + // // The function returns a list of data items. In this model, we don't care about the data itself, so we just use dummy data. - // Our format for dummy ddata is a pair (str, int), where the first element is always "data" and the second element is the index of the leaf. + // Our format for dummy ddata is a pair (str, int), where the first element is always "data" and the second element is the index of the leaf. def GenerateLeavesCorrectly(power: int, namespaceBordersSet : Set[int]) : List[DATA_ITEM] = - + // add left-most and right-most borders to namespaces val namespaceBorders = concat( concat([0], setToSortedList(namespaceBordersSet)), [2^(power-1)] - ) - - val generated_leaves_dummy_hash : List[DATA_ITEM] = + ) + + val generated_leaves_dummy_hash : List[DATA_ITEM] = // for each namespace range(0, length(namespaceBorders)-1).foldl( [], - (acc, i) => + (acc, i) => acc.concat( // and for each leaf between two namespaces range(namespaceBorders[i], namespaceBorders[i+1]).foldl( @@ -191,10 +191,10 @@ module nmt_helpers{ // this is mostly for debugging purposes: have data value correspond exactly to the index // of the leaf. (This enables easier reasoning about the generated proofs later) - val generated_leaves : List[DATA_ITEM] = + val generated_leaves : List[DATA_ITEM] = range(0, length(generated_leaves_dummy_hash)).foldl( [], - (acc, i) => acc.concat( + (acc, i) => acc.concat( [{value: ("data", i), namespaceId: generated_leaves_dummy_hash[i].namespaceId}] ) ) @@ -204,30 +204,30 @@ module nmt_helpers{ - def BuildTree(leaves: List[DATA_ITEM]) : TREE = + def BuildTree(leaves: List[DATA_ITEM]) : TREE = // because of the way trees are represented (nodes enumerated from 1 to 2^n - 1), // and the assumption of full and complete trees, we know that leaves // are occupying the half of the tree. Thus, their starting index equals their length val leaf_idx_start = length(leaves) - val tree_leaves : NODE_IDX -> DATA_ITEM = + val tree_leaves : NODE_IDX -> DATA_ITEM = range(0, length(leaves)).foldl( Map(), (acc, i) => acc.put(leaf_idx_start + i, leaves[i]) ) - val tree_leaves_hashes : NODE_IDX -> NAMESPACE_HASH = + val tree_leaves_hashes : NODE_IDX -> NAMESPACE_HASH = range(0, length(leaves)).foldl( Map(), - (acc, i) => + (acc, i) => acc.put( - leaf_idx_start + i, + leaf_idx_start + i, {minNS: leaves[i].namespaceId, maxNS: leaves[i].namespaceId, hash: Hash([leaves[i].value])}) ) - // starting from leaves, calculating the hashes for all other nodes + // starting from leaves, calculating the hashes for all other nodes // of the tree - val tree_hashes : NODE_IDX -> NAMESPACE_HASH = + val tree_hashes : NODE_IDX -> NAMESPACE_HASH = reverse(range(1, leaf_idx_start)).foldl( tree_leaves_hashes, (acc, i) => @@ -245,70 +245,70 @@ module nmt_helpers{ ) ) } - ) + ) ) {leaves: tree_leaves, hashes: tree_hashes} - - - + + + } -module nmt { - // ASSUMPTIONS/LIMITATIONS: +module nmt { + // ASSUMPTIONS/LIMITATIONS: // - each tree is full and complete (2^n leaves at the bottom level) // - not modelling ignoring max namespace import basics.* import nmt_helpers.* - - - - + + + + pure val MAX_POWER = 5 pure val MAX_NAMESPACE_ID = 100 pure val EMPTY_PROOF = {start: -1, end: -1, supporting_hashes: []} pure val EMPTY_TREE = {leaves: Map(), hashes: Map()} pure val EMPTY_LEAVES = [] - - - + + + // This function creates a proof for a given `namespaceId` and a given `tree`. - // Following the NMT documentation (https://github.com/celestiaorg/nmt/blob/master/docs/spec/nmt.md#namespace-proof), + // Following the NMT documentation (https://github.com/celestiaorg/nmt/blob/main/docs/spec/nmt.md#namespace-proof), // the proof consists of `start` and `end` indices and the hashes of the nodes (`supporting_hashes`) that are left siblings - // in the regular Merkle proof of `start` and those that are right hashes in the regular proof of `end-1` + // in the regular Merkle proof of `start` and those that are right hashes in the regular proof of `end-1` def CreateProofNamespace(namespaceId: int, tree: TREE): PROOF = - val leavesStart = min(tree.leaves.keys()) + val leavesStart = min(tree.leaves.keys()) // take only those keys that are of the desired namespace val relevantLeavesKeys = tree.leaves.keys().fold( Set(), - (acc, i) => + (acc, i) => if (tree.leaves.get(i).namespaceId == namespaceId) union(acc, Set(i)) else - acc + acc ) - val start = min(relevantLeavesKeys) + val start = min(relevantLeavesKeys) - // we want to get the binary representation of the number leaves from the `start` (first node of the - // leaves that go to the proof) and the very beginning of leaves because this encodes left siblings, - // uncles, etc., which are needed for the merkle proof. The fact that we use it reversed is because the + // we want to get the binary representation of the number leaves from the `start` (first node of the + // leaves that go to the proof) and the very beginning of leaves because this encodes left siblings, + // uncles, etc., which are needed for the merkle proof. The fact that we use it reversed is because the // proof defines the nodes to be in-order, thus, older ancestors come first (bcs they are more left) val binaryLeftLimitDistanceReversed = reverse(binary(start - leavesStart)) - - val left_hashes : List[NAMESPACE_HASH] = + + val left_hashes : List[NAMESPACE_HASH] = range(0, length(binaryLeftLimitDistanceReversed)).foldl( [], (acc, i) => - if (binaryLeftLimitDistanceReversed[i] == 1) + if (binaryLeftLimitDistanceReversed[i] == 1) concat([tree.hashes.get(getLeftUncleIdx(start, i))], acc) else acc @@ -317,42 +317,42 @@ module nmt { val end = max(relevantLeavesKeys) val binaryRightLimitDistanceReversed = reverse(binary(2*leavesStart-1 - end)) - val right_hashes : List[NAMESPACE_HASH] = + val right_hashes : List[NAMESPACE_HASH] = range(0, length(binaryRightLimitDistanceReversed)).foldl( [], (acc, i) => - if (binaryRightLimitDistanceReversed[i] == 1) + if (binaryRightLimitDistanceReversed[i] == 1) acc.concat([tree.hashes.get(getRightUncleIdx(end, i))]) else acc - ) + ) - // start needs to be expressed relative to leaves start and so does end. + // start needs to be expressed relative to leaves start and so does end. { - start: start - leavesStart, + start: start - leavesStart, // the +1 is because the range has to be non-inclusive at the right side - end: end - leavesStart +1, + end: end - leavesStart +1, supporting_hashes: concat(left_hashes, right_hashes) } - - - + + + def SensibleStartEnd(start: int, end: int) : bool = and { - start >= 0, + start >= 0, start < end } // all leaf nodes in the proof should have the same namespace def CorrectNamespaceValue(proof: PROOF, namespaceId: int, leaves: List[DATA_ITEM]) : bool = - val elementsWithWrongId = leaves.select(x => x.namespaceId != namespaceId) + val elementsWithWrongId = leaves.select(x => x.namespaceId != namespaceId) length(elementsWithWrongId) == 0 - - + + // Given `proof` and `leaves`, this function calculates the Merkle root (which is hash) for that range. def MerkleRangeHash(proof: PROOF, leaves: List[DATA_ITEM]) : WORD = - + // the number of leaves in a complete subtree that covers the last leaf // in the proof val fullTreeSize = getFullTreeSize(proof.end - 1) @@ -365,78 +365,78 @@ module nmt { // create a mapping levelOfTheTree -> hash. This enables knowing which of the supporting_hashes // is used on which level of the tree (from the left side) - val leftMap : int -> WORD = + val leftMap : int -> WORD = range(0, length(binaryLeftLimitDistance)).foldl( Map(), - (accMap, i) => + (accMap, i) => // if the bit is 1, then the left uncle from the tree level i is necessary in the Merkle proof - if (binaryLeftLimitDistance[i] == 1) + if (binaryLeftLimitDistance[i] == 1) accMap.put( // reversing: because the supporting nodes are given in-order, closer relatives of // the leaf node will come the last - length(binaryLeftLimitDistance) - 1 - i, + length(binaryLeftLimitDistance) - 1 - i, // adding the first unused of the supporting hashes (hence, key equals to the size of the growing map) proof.supporting_hashes[size(accMap.keys())].hash - ) - else + ) + else accMap ) // similarly to leftMap, the rightMap holds the mapping of the supporting leaves from the right side of the // range - val rightMap : int -> WORD = + val rightMap : int -> WORD = range(0, length(binaryRightLimitDistance)).foldl( Map(), - (accMap, i) - => - if (binaryRightLimitDistance[i] == 1) + (accMap, i) + => + if (binaryRightLimitDistance[i] == 1) accMap.put( - i, + i, proof.supporting_hashes[sum(binaryLeftLimitDistance) + size(accMap.keys())].hash - ) - else + ) + else accMap ) val numLeavesUsed = sum(binaryLeftLimitDistance)+sum(binaryRightLimitDistance) - - // after the left and right maps are created, the remaining supporting hashes + + // after the left and right maps are created, the remaining supporting hashes // are the ones that are not used. They are necessarily on the right side of the leaf range // and can be treated as a proof path in a regular (not the range-based) Merkle tree - val remainingSupportNodes : List[NAMESPACE_HASH] = - if (numLeavesUsed == length(proof.supporting_hashes)) - [] - else + val remainingSupportNodes : List[NAMESPACE_HASH] = + if (numLeavesUsed == length(proof.supporting_hashes)) + [] + else proof.supporting_hashes.slice(numLeavesUsed,length(proof.supporting_hashes)) - + // height of the smallest tree which starts at the leaf index 0 and encompasses the whole range - val treeHeight : int = + val treeHeight : int = if (proof.end == 1) 1 else length(binary(proof.end-1)) + 1 - + // a list of hashes of the leaves in the [start, end) range - val leafHashes: WORD = + val leafHashes: WORD = leaves.foldl( [], (acc, leaf) => acc.concat(Hash([leaf.value])) ) - - val partialTreeRootHash : WORD = + + val partialTreeRootHash : WORD = // Fold over the levels of the tree, starting from the leaf level. // Progress to the next level by hashing pairs of hashes from the previous level. - // Each level is half the size of the previous one until finally a list containing a single hash is returned. + // Each level is half the size of the previous one until finally a list containing a single hash is returned. range(0,treeHeight).foldl( leafHashes, // pairwiseHash will map a list to a new list by taking a hash of every two consecutive values - (acc, i) => pairwiseHash( + (acc, i) => pairwiseHash( mergeWithLeftAndRight( getWithDefault(leftMap, i, []), acc, getWithDefault(rightMap, i, []) ) ) - ) + ) // having computed the partialTreeRootHash, we can now treat the rest of the supporting hashes // as a regular Merkle inclusion proof and starting from the `partialTreeRootHash` chain the hashes @@ -445,32 +445,32 @@ module nmt { partialTreeRootHash, (acc, levelHashes) => Hash(acc.concat(levelHashes.hash)) ) - + // a hash value that is returned calculatedRootHash // none of the proof nodes should have an overlap with the `namespaceId` - def Completeness(proof: PROOF, namespaceId: int) : bool = - val allSupportingNamespaceIds = + def Completeness(proof: PROOF, namespaceId: int) : bool = + val allSupportingNamespaceIds = proof.supporting_hashes.foldl( Set(), (acc, el) => union(acc, el.minNS.to(el.maxNS)) ) - + not(allSupportingNamespaceIds.contains(namespaceId)) def verifyInclusionProof(proof: PROOF, rootHash: NAMESPACE_HASH, namespaceId: int, leaves: List[DATA_ITEM]) : bool = { - - and { - SensibleStartEnd(proof.start, proof.end), - CorrectNamespaceValue(proof, namespaceId, leaves), + + and { + SensibleStartEnd(proof.start, proof.end), + CorrectNamespaceValue(proof, namespaceId, leaves), Completeness(proof, namespaceId), rootHash.hash == MerkleRangeHash(proof, leaves) } } - + } @@ -487,32 +487,32 @@ module nmtProofVerification { import nmt.* var proof_v : PROOF - var tree_v : TREE + var tree_v : TREE var namespace_v : int var verification_success_v : bool var state_v : string - action init = { - all{ + action init = { + all{ tree_v' = EMPTY_TREE, proof_v' = EMPTY_PROOF, verification_success_v' = false, state_v' = "requirements", namespace_v' = -1 - } + } } - // step is modelled as a loop of the four always repeating states: + // step is modelled as a loop of the four always repeating states: // 1) requirements, 2) generation, 3) verification, and 4) final state. - // - // 1) when in the "requirements" state, a random size of the tree and the namespaces + // + // 1) when in the "requirements" state, a random size of the tree and the namespaces // corresponding to leaves, // are generated and one of the namespaces is chosen to generate a proof for // 2) when in the "generation" state, a proof is generated for the generated tree and the chosen namespace // 3) when in the "verification" state, that proof is verified // 4) final step collects all the results - // + // // The three steps happen one after another (no non-determinism involved) action step = { any{ @@ -524,23 +524,23 @@ module nmtProofVerification { // update state for the next step state_v' = "generation", - nondet power = oneOf(3.to(MAX_POWER)) + nondet power = oneOf(3.to(MAX_POWER)) //TODO: there must be a better way to generate this set nondet namespaceBordersSet = 1.to(2^(power-1) - 2).powerset().filter(x => size(x) > 1).oneOf() val leaves = GenerateLeavesCorrectly(power, namespaceBordersSet) - all{ + all{ val tree = BuildTree(leaves) all{ tree_v' = tree, nondet namespaceId = tree.leaves.keys().fold( Set(), - (acc, leaf_key) => - union(acc, Set(tree.leaves.get(leaf_key).namespaceId)) - ).oneOf() + (acc, leaf_key) => + union(acc, Set(tree.leaves.get(leaf_key).namespaceId)) + ).oneOf() namespace_v' = namespaceId, } }, - proof_v' = proof_v, + proof_v' = proof_v, verification_success_v' = verification_success_v, }, @@ -553,7 +553,7 @@ module nmtProofVerification { proof_v' = CreateProofNamespace(namespace_v, tree_v), namespace_v' = namespace_v, verification_success_v' = verification_success_v, - tree_v' = tree_v + tree_v' = tree_v }, // 3): verification @@ -566,11 +566,11 @@ module nmtProofVerification { val min_leaf_key = min(tree_v.leaves.keys()) val max_leaf_key = max(tree_v.leaves.keys()) - val leaves : List[DATA_ITEM] = + val leaves : List[DATA_ITEM] = range(min_leaf_key, max_leaf_key+1) .foldl( [], - (acc, leaf_key) => + (acc, leaf_key) => if ((proof_v.start <= leaf_key - min_leaf_key) and (leaf_key - min_leaf_key < proof_v.end)) acc.append( tree_v.leaves.get(leaf_key) @@ -578,10 +578,10 @@ module nmtProofVerification { else acc ) - + verification_success_v' = verifyInclusionProof(proof_v, tree_v.hashes.get(1), namespace_v, leaves), tree_v' = tree_v, - proof_v' = proof_v, + proof_v' = proof_v, }, // 4): collecting all results @@ -601,7 +601,7 @@ module nmtProofVerification { // this invariant states that after the full loop of states, // verification will be successful - val verificationAlwaysCorrect = + val verificationAlwaysCorrect = (state_v == "final") implies (verification_success_v == true) } @@ -611,24 +611,24 @@ module nmtTest { // this module iteratively generates a proof and then non-deterministically corrupts it. // run by: // quint run --main=nmtTest --max-samples=1 --max-steps=100 nmt.qnt --out-itf=ITF_files/out.itf.json - // to simulate 100 steps and save output into `out.itf.json`. This output can be used to generate + // to simulate 100 steps and save output into `out.itf.json`. This output can be used to generate // test cases (eg., in `simulation_test.go`) import basics.* import nmt_helpers.* - import nmt.* + import nmt.* var proof_v : PROOF - var tree_v : TREE - var namespace_v : int + var tree_v : TREE + var namespace_v : int var state_v : string var leaves_v : List[DATA_ITEM] var corrupted : bool var corruption_type : string var corruption_diff : {changed_start: int, changed_end: int, changed_namespace: int, changed_indices: List[int]} - action init = { - all{ + action init = { + all{ tree_v' = EMPTY_TREE, proof_v' = EMPTY_PROOF, corrupted' = false, @@ -636,7 +636,7 @@ module nmtTest { namespace_v' = -1, leaves_v' = EMPTY_LEAVES, corruption_type' = "", - corruption_diff' = + corruption_diff' = { changed_start: -1, changed_end: -1, @@ -644,7 +644,7 @@ module nmtTest { changed_indices: [] } - } + } } action requirements = { @@ -654,25 +654,25 @@ module nmtTest { // update state for the next step state_v' = "generation", - nondet power = oneOf(3.to(MAX_POWER)) + nondet power = oneOf(3.to(MAX_POWER)) //TODO: there must be a better way to generate this set nondet namespaceBordersSet = 1.to(2^(power-1) - 2).powerset().filter(x => size(x) > 1).oneOf() val leaves = GenerateLeavesCorrectly(power, namespaceBordersSet) - all{ + all{ val tree = BuildTree(leaves) all{ leaves_v' = leaves, tree_v' = tree, nondet namespaceId = tree.leaves.keys().fold( Set(), - (acc, leaf_key) => - union(acc, Set(tree.leaves.get(leaf_key).namespaceId)) - ).oneOf() + (acc, leaf_key) => + union(acc, Set(tree.leaves.get(leaf_key).namespaceId)) + ).oneOf() namespace_v' = namespaceId, } }, // unchanged variables - proof_v' = proof_v, + proof_v' = proof_v, corrupted' = corrupted, corruption_type' = corruption_type, corruption_diff' = corruption_diff @@ -692,12 +692,12 @@ module nmtTest { tree_v' = tree_v, leaves_v' = leaves_v, corruption_type' = corruption_type, - corruption_diff' = corruption_diff + corruption_diff' = corruption_diff } } - + @@ -714,7 +714,7 @@ module nmtTest { corrupted' = false, leaves_v' = EMPTY_LEAVES, corruption_type' = "", - corruption_diff' = + corruption_diff' = { changed_start: -1, changed_end: -1, @@ -742,14 +742,14 @@ module nmtTest { 0.to(proof_v.end - 1).exclude(Set(proof_v.start)) ) all{ - - proof_v' = {start: new_start, end: proof_v.end, supporting_hashes: proof_v.supporting_hashes}, - corruption_type' = "start", + + proof_v' = {start: new_start, end: proof_v.end, supporting_hashes: proof_v.supporting_hashes}, + corruption_type' = "start", corruption_diff' = corruption_diff.with("changed_start", new_start), } }, - // corrupting the end value: we will change its value, while maintaining the property that it must + // corrupting the end value: we will change its value, while maintaining the property that it must // be greater than start by at least 1 (we get that by requiring `new_end` to be from the set {proof_v.start, ..., proof_v.end - 1}) all{ proof_v.start < proof_v.end - 1, @@ -760,22 +760,22 @@ module nmtTest { corruption_type' = "end", corruption_diff' = corruption_diff.with("changed_end", new_end), } - + }, - + // corrupting the supporting hashes in a controlled way: we will take a subset of existing supporting hashes all{ proof_v.supporting_hashes.length() > 1, namespace_v' = namespace_v, // We use the original set of indices and then take a subset of it as a corrupted one. - // We do so by selecting `oneOf` from the set of all subsets of existing indices (`powerset`), + // We do so by selecting `oneOf` from the set of all subsets of existing indices (`powerset`), // provided that it is not the empty set and not the full set of indices. (`filter`). // Note that this is non-deterministic value (`nondet`) because of the function `oneOf`. nondet new_supporting_hashes_indices = oneOf( 0.to(proof_v.supporting_hashes.length()-1) .powerset() .filter( - x => + x => and{ size(x) < proof_v.supporting_hashes.length(), size(x) > 0 @@ -784,25 +784,25 @@ module nmtTest { ) // Now we use the calculated subset of indices to extract the corresponding subset of supporting hashes. - // We do so by iterating over the set of indices. Iteration over lists in Quint is done by using the concept of - // the left fold (`foldl`). For more info on `foldl`, check + // We do so by iterating over the set of indices. Iteration over lists in Quint is done by using the concept of + // the left fold (`foldl`). For more info on `foldl`, check // https://github.com/informalsystems/quint/blob/main/doc/builtin.md#pure-def-foldl-lista-b-b-a--b--b val new_supporting_hashes = range(0, proof_v.supporting_hashes.length()) .foldl( [], - (acc, i) => + (acc, i) => if (new_supporting_hashes_indices.contains(i)) acc.append(proof_v.supporting_hashes[i]) else acc - ) - all{ + ) + all{ proof_v' = {start: proof_v.start, end: proof_v.end, supporting_hashes: new_supporting_hashes}, corruption_type' = "supporting_hashes", val new_indices = range(0, proof_v.supporting_hashes.length()) .foldl( [], - (acc, i) => + (acc, i) => if (new_supporting_hashes_indices.contains(i)) acc.append(i) else @@ -810,13 +810,13 @@ module nmtTest { ) corruption_diff' = corruption_diff.with("changed_indices", new_indices), } - + }, - + // corrupting the namespace value: we will change the value of the namespace for which the proof is written. - // We do so by selecting `newNamespace` from the set {1,...,MAX_NAMESPACE_ID}, while requiring that it is + // We do so by selecting `newNamespace` from the set {1,...,MAX_NAMESPACE_ID}, while requiring that it is // indeed different from `namespace_v`. - all{ + all{ proof_v' = proof_v, nondet newNamespace = 1.to(MAX_NAMESPACE_ID).exclude(Set(namespace_v)).oneOf() all{ @@ -825,23 +825,23 @@ module nmtTest { corruption_diff' = corruption_diff.with("changed_namespace", newNamespace), } } - }, + }, corrupted' = true, // unchanged variables state_v' = state_v, - tree_v' = tree_v, + tree_v' = tree_v, leaves_v' = leaves_v } - + } // step is modelled by 4 states: // 1) requirements, 2) generation, 2a) corruptProof, and 3) final state. - // + // // The state `corruptProof` is marked by 2a because it may be skipped (leaving the proof uncorrupted) - // 1) when in the "requirements" state, a random size of the tree and the namespaces + // 1) when in the "requirements" state, a random size of the tree and the namespaces // corresponding to leaves, // are generated and one of the namespaces is chosen to generate a proof for // 2) when in the "generation" state, a proof is generated for the generated tree and the chosen namespace @@ -849,7 +849,7 @@ module nmtTest { // and not transitioning to the next state, but remaining in `final`. (There will be no two corruptions because // the variable `corrupted` is set to true after the first corruption.) // 3) when in the `final` state, the state is reset to the initial values - // + // // The three steps happen one after another (no non-determinism involved) action step = { any{ @@ -857,17 +857,17 @@ module nmtTest { // 1): requirements: defining the tree and the namespace to generate a proof for requirements, - // 2): generation of the proof + // 2): generation of the proof generation, - + // 2b): corrupting the proof - corruptProof, + corruptProof, // 3): collecting all results final - + } } - + } diff --git a/proof.go b/proof.go index 6bf877e..083370e 100644 --- a/proof.go +++ b/proof.go @@ -133,7 +133,7 @@ func NewAbsenceProof(proofStart, proofEnd int, proofNodes [][]byte, leafHash []b return Proof{proofStart, proofEnd, proofNodes, leafHash, ignoreMaxNamespace} } -// IsEmptyProof checks whether the proof corresponds to an empty proof as defined in NMT specifications https://github.com/celestiaorg/nmt/blob/master/docs/spec/nmt.md. +// IsEmptyProof checks whether the proof corresponds to an empty proof as defined in NMT specifications https://github.com/celestiaorg/nmt/blob/main/docs/spec/nmt.md. func (proof Proof) IsEmptyProof() bool { return proof.start == proof.end && len(proof.nodes) == 0 && len(proof.leafHash) == 0 }