Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
150 changes: 150 additions & 0 deletions docs/specs/code/merkle.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,150 @@
## Code from the spec for operating on MerkleTree datastructures.

import hashlib

def hash(data):
assert isinstance(data, bytes), "data not bytes"
return hashlib.sha256(data).digest()

class MerkleTree:
def __init__(self, n):
self.n = n
self.a = [b''] * (2 * n)

def set_leaf(self, pos, leaf):
"""
Sets a leaf at a specific position.
pos: 0-based index relative to the leaves (0 to n-1)
"""
assert 0 <= pos < self.n, f"{pos} is out of bounds"
self.a[pos + self.n] = leaf

def build_tree(self):
"""
Computes the internal nodes from n-1 down to 1.
Returns the root (M.a[1]).
"""
for i in range(self.n - 1, 0, -1):
left = self.a[2 * i]
right = self.a[2 * i + 1]

self.a[i] = hash(left + right)

return self.a[1]

def mark_tree(self, requested_leaves):
marked = [False] * (2 * self.n)

for i in requested_leaves:
assert 0 <= i < self.n, f"invalid requested index {i}"
marked[i + self.n] = True

for i in range(self.n - 1, 0, -1):
marked[i] = marked[2 * i] or marked[2 * i + 1]

return marked

def compressed_proof(self, requested_leaves):
"""
Generates a compressed proof for the requested leaves.
"""
proof = []

marked = self.mark_tree(requested_leaves)

for i in range(self.n - 1, 0, -1):
if marked[i]:
child = 2 * i

# If the left child is marked, we need the right child (sibling).
if marked[child]:
child += 1

# If the identified child/sibling is NOT marked,
# we must provide its hash in the proof so the verifier can calculate the parent.
if not marked[child]:
proof.append(self.a[child])

return proof

def verify_merkle(self, root, n, k, s, indices, proof):
"""
Verifies that the provided leaves (s) at specific positions (indices)
are part of the Merkle tree defined by 'root'.

:param root: The expected Root Hash
:param n: Total number of leaves in the tree
:param k: Number of leaves being verified
:param s: List of leaf data/hashes to verify
:param indices: List of positions for the leaves in 's'
:param proof: List of proof hashes
"""
tmp = [None] * (2 * n)
defined = [False] * (2 * n)

proof_index = 0

if n != self.n: return False

marked = self.mark_tree(indices)

for i in range(n - 1, 0, -1):
if marked[i]:
child = 2 * i
if marked[child]:
child += 1

if not marked[child]:
if proof_index >= len(proof):
return False

tmp[child] = proof[proof_index]
proof_index += 1
defined[child] = True

for i in range(k):
pos = indices[i] + n
tmp[pos] = s[i]
defined[pos] = True

for i in range(n - 1, 0, -1):
if defined[2 * i] and defined[2 * i + 1]:
left = tmp[2 * i]
right = tmp[2 * i + 1]
tmp[i] = hash(left + right)
defined[i] = True

return defined[1] and (tmp[1] == root)


if __name__ == "__main__":
# Example from the test vector section in the Appendix.
n = 5
mt = MerkleTree(n)

c0 = bytes.fromhex('4bf5122f344554c53bde2ebb8cd2b7e3d1600ad631c385a5d7cce23c7785459a')
c1 = bytes.fromhex('dbc1b4c900ffe48d575b5da5c638040125f65db0fe3e24494b76ea986457d986')
c3 = bytes.fromhex('e52d9c508c502347344d8c07ad91cbd6068afc75ff6292f062a09ca381c89e71')
mt.set_leaf(0, c0)
mt.set_leaf(1, c1)
mt.set_leaf(2,bytes.fromhex('084fed08b978af4d7d196a7446a86b58009e636b611db16211b65a9aadff29c5'))
mt.set_leaf(3, c3)
mt.set_leaf(4,bytes.fromhex('e77b9a9ae9e30b0dbdb6f510a264ef9de781501d7b6b92ae89eb059c5ab743db'))

root_hash = mt.build_tree()

print(f"Merkle Root: {root_hash.hex()}")

print(f"Requesting [0,1]:")
req_leaves = [0, 1]
proof = mt.compressed_proof(req_leaves)
for p in proof:
print(p.hex())
assert mt.verify_merkle(root_hash, n, 2, [c0, c1], [0, 1], proof), "Bad proof"

print(f"Requesting [1,3]:")
req_leaves = [1, 3]
proof = mt.compressed_proof(req_leaves)
for p in proof:
print(p.hex())
assert mt.verify_merkle(root_hash, n, 2, [c1, c3], [1, 3], proof), "Bad proof"
156 changes: 84 additions & 72 deletions docs/specs/ligero.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,20 +24,22 @@ A tree that contains `n` leaves is represented by an array of `2 * n` message di
### Constructing a Merkle tree from `n` digests

```
struct {
Digest a[2 * n]
} MerkleTree

def set_leaf(M, pos, leaf) {
assert(pos < M.n)
M.a[pos + n] = leaf
}

def build_tree(M) {
FOR M.n < i <= 1 DO
M.a[i] = hash(M.a[2 * i] || M.a[2 * i + 1])
return M.a[1]
}
class MerkleTree:
def __init__(self, n):
self.n = n
self.a = [b''] * (2 * n)

def set_leaf(self, pos, leaf):
assert 0 <= pos < self.n, f"{pos} is out of bounds"
self.a[pos + self.n] = leaf

def build_tree(self):
for i in range(self.n - 1, 0, -1):
left = self.a[2 * i]
right = self.a[2 * i + 1]s
self.a[i] = hash(left + right)

return self.a[1]
```

### Constructing a proof of inclusion
Expand All @@ -48,72 +50,77 @@ To address these inefficiencies, this section explains how to produce a batch pr
It is important in this formulation to treat the input digests as a sequence, i.e. with a given order. Both the prover and verifier of this batch proof must use the same order of the `requested_leaves` array.

```
def compressed_proof(M, requested_leaves[], n) {
marked = mark_tree(requested_leaves, n)
FOR n < i <= 1 DO
IF (marked[i]) {
child = 2 * i
IF (marked[child]) {
child += 1
}
IF (!marked[child]) {
proof.append(M.a[child])
}
}
return proof
}
def mark_tree(self, requested_leaves):
marked = [False] * (2 * self.n)

def mark_tree(requested_leaves[], n) {
bool marked[2 * n] // initialized to false
for i in requested_leaves:
assert 0 <= i < self.n, f"invalid requested index {i}"
marked[i + self.n] = True

for(index i : requested_leaves)
marked[i + n] = true
for i in range(self.n - 1, 0, -1):
marked[i] = marked[2 * i] or marked[2 * i + 1]

FOR n < i <= 1 DO
// mark parent if child is marked
marked[i] = marked[2 * i] || marked[2 * i + 1];
return marked

return marked
}
def compressed_proof(self, requested_leaves):
proof = []
marked = self.mark_tree(requested_leaves)
for i in range(self.n - 1, 0, -1):
if marked[i]:
child = 2 * i

# If the left child is marked, we need the right child.
if marked[child]:
child += 1

# If the identified child/sibling is NOT marked,
# add its hash to the proof so the verifier can calculate the parent.
if not marked[child]:
proof.append(self.a[child])

return proof
```

### Verifying a proof of inclusion
This section describes how to verify a compressed Merkle proof. The claim to verify is that "the commitment `root` defines an `n`-leaf Merkle tree that contains `k` digests s[0],..s[k-1] at corresponding indicies i[0],...i[k-1]." The strategy of this verification procedure is to deduce which nodes are needed along the `k` verification paths from index to root, then read these values from the purported proof, and then recompute the Merkle tree and the consistency of the `root` digest. As an optimization, the `defined[]` array avoids recomputing internal portions of the Merkle tree that are not relevant to the verification. By convention, a proof for the degenerate case of `k=0` digests is defined to fail. It is assumed that the `indicies[]` array does not contain duplicates.
Copy link
Contributor

@TallTed TallTed Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I note inconsistent use of .. (not really an ellipsis) and ... (ellipsis) for sequences. I recognize that some programming languages and user interfaces use two dots as a range operator, but I think this causes confusion for readers who are not familiar with those specific programming languages and user interfaces, so I suggest that the two-dots not be used at all. I suggest that ... (three dots, preferred) or (a single-character ellipsis) should be used in such cases.

When an ellipsis (whether or ...) follows a comma, I suggest that there be a space between, i.e., immediately preceding the ellipsis, as blah, ....

When an ellipsis is followed by any character other than a terminating . (single dot a/k/a full stop) or other punctuation mark, I suggest that the ellipsis be immediately followed by a space, as ... blah or ...! or ...? or ... i[k-1].

For most (probably all) of the above cases, &nbsp; should be used instead of wherever a browser-rendered line break might make the punctuation harder for a human reader to parse.

(EDITted to fix autocorrect's miscorrections of ellipsis to ellipse.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apologies that my other changes for the f-s section are also being added to this PR.

-- the e123 commit fixes your issue. I'll also wait for comments on the FS changes on this PR before merging.

Thank you for your careful review.


```
def verify_merkle(root, n, k, s[], indicies[], proof[]) {
tmp = []
defined = []

proof_index = 0
marked = mark_tree(indicies, n)
FOR n < i <= 1 DO
if (marked[i]) {
child = 2 * i
if (marked[child]) {
child += 1
}
if (!marked[child]) {
if proof_index > |proof| {
return false
}
tmp[child] = proof[proof_index++]
defined[child] = true
}
}

FOR 0 <= i < k DO
tmp[indicies[i] + n] = s[i]
defined[indicies[i] + n] = true

FOR n < j <= 1 DO
if defined[2 * i] && defined[2 * i + 1] {
tmp[i] = hash(tmp[2 * i] || tmp[2 * i + 1])
defined[i] = true
}

return defined[1] && tmp[1] = root
}
def verify_merkle(self, root, n, k, s, indices, proof):
tmp = [None] * (2 * n)
defined = [False] * (2 * n)

proof_index = 0

if n != self.n: return False

marked = self.mark_tree(indices)

for i in range(n - 1, 0, -1):
if marked[i]:
child = 2 * i
if marked[child]:
child += 1

if not marked[child]:
if proof_index >= len(proof):
return False
tmp[child] = proof[proof_index]
proof_index += 1
defined[child] = True

for i in range(k):
pos = indices[i] + n
tmp[pos] = s[i]
defined[pos] = True

for i in range(n - 1, 0, -1):
if defined[2 * i] and defined[2 * i + 1]:
left = tmp[2 * i]
right = tmp[2 * i + 1]
tmp[i] = hash(left + right)
defined[i] = True

return defined[1] and (tmp[1] == root)
```

## Common parameters
Expand Down Expand Up @@ -288,6 +295,8 @@ def layout_quadratic_rows(T, w, lqc[]) {
## Ligero Prove
This section specifies how a Ligero proof for a given sequence of linear constraints and quadratic constraints on the committed witness vector `W` is constructed. The proof consists of a low-degree test on the tableau, a linearity test, and a quadratic constraint test.



### Low-degree test
In the low-degree test, the verifier sends a challenge vector consisting of `NROW` field elements, `u[0..NROW]`. This challenge is generated via the Fiat-Shamir transform. The prover computes the sum of `u[i]*T[i]` where `T[i]` is the i-th row of the tableau, and returns the first BLOCK elements of the result. The verifier applies the `extend` method to this response, and then verifies that the extended row is consistent with the positions of the Merkle tree that the verifier will later request from the Prover.

Expand All @@ -304,11 +313,14 @@ In this sense, the quadratic constraints are reduced to linear constraints, and
The last step of the prove method is for the verifier to select a subset of unique indicies (i.e., they are sampled without replacement) from the range `DBLOCK...NCOL` and request that the prover open these columns of tableau `T`. These opened columns are then used to verify consistency with the previous messages sent by the prover.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
The last step of the prove method is for the verifier to select a subset of unique indicies (i.e., they are sampled without replacement) from the range `DBLOCK...NCOL` and request that the prover open these columns of tableau `T`. These opened columns are then used to verify consistency with the previous messages sent by the prover.
The last step of the prove method is for the verifier to select a subset of unique indices (i.e., they are sampled without replacement) from the range `DBLOCK...NCOL` and request that the prover open these columns of tableau `T`. These opened columns are then used to verify consistency with the previous messages sent by the prover.


### Ligero Prover procedure
The `context` argument is application-dependent and includes information about the theorem statement that is proven.

```
def prove(transcript, digest, linear[], lqc[]) {
def prove(transcript, context, linear[], lqc[]) {

transcript.write(context)

u = transcript.generate_challenge([BLOCK]);
transcript.write(digest)

ldt[0..BLOCK] = T[ILDT][0..BLOCK]

Expand Down
Loading