JAR: JAM Axiomatic Reference

12.1. Trie Nodes🔗

🔗inductive type
Jar.Merkle.Node : Type
Jar.Merkle.Node : Type

A Merkle trie node is always 64 bytes (512 bits). GP Appendix D. Encoded as the first bit distinguishing branch (0) from leaf (1).

Constructors

branch (left right : Hash) : Node

Branch node: first bit = 0. Contains left (255 bits) and right (256 bits) child hashes.

embeddedLeaf (key : OctetSeq 31) (value : ByteArray) : Node

Embedded-value leaf: first bit = 1, second bit = 0. Bits 2-7 encode value size. 31-byte key, ≤32-byte value.

regularLeaf (key : OctetSeq 31) (valueHash : Hash) : Node

Regular leaf: first bit = 1, second bit = 1. 31-byte key, 32-byte hash of value.

🔗def
Jar.Merkle.encodeBranch (left right : Hash) : OctetSeq 64
Jar.Merkle.encodeBranch
  (left right : Hash) : OctetSeq 64

Encode a branch node to 64 bytes. GP Appendix D §D.3. B(l, r) = [0] ∥ bits(l)[1..256] ∥ bits(r). Bit 0 = 0 (branch marker). Bits 1-255 = left hash bits 1-255 (skip MSB). Bits 256-511 = all 256 bits of right hash.

🔗def
Jar.Merkle.encodeLeaf (key : OctetSeq 31) (value : ByteArray) :
  OctetSeq 64
Jar.Merkle.encodeLeaf (key : OctetSeq 31)
  (value : ByteArray) : OctetSeq 64

Encode a leaf node to 64 bytes. GP Appendix D §D.4. If |v| ≤ 32 (embedded): [1,0] ∥ |v|(6 bits) ∥ key(248 bits) ∥ v_padded(256 bits). If |v| > 32 (regular): [1,1,0,0,0,0,0,0] ∥ key(248 bits) ∥ H(v)(256 bits).