JAR: Join-Accumulate Refine

17.3. Binary Merkle Tree🔗

🔗def
Jar.Merkle.binaryMerkleRoot (items : Array Hash) : Hash
Jar.Merkle.binaryMerkleRoot
  (items : Array Hash) : Hash

M_B(items) : Binary Merkle tree root. GP Appendix D eq (D.7). Recursively splits the array in half, hashing left and right subtrees with Blake2b. Empty → H₀, single item → item, otherwise → H(left ++ right).

🔗def
Jar.Merkle.constDepthMerkleRoot (items : Array Hash) (depth : Nat) :
  Hash
Jar.Merkle.constDepthMerkleRoot
  (items : Array Hash) (depth : Nat) :
  Hash

M(data, depth) : Constant-depth binary Merkle tree. GP Appendix E eq (E.4). Pads to 2^depth leaves with zero hashes, then computes binary Merkle root.