smt.py 2.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133
  1. import hashlib
  2. # SMT non-membership check
  3. # https://hackmd.io/@aztec-network/ryJ8wxfKK
  4. # We set this to all
  5. NULL = bytearray([0xff] * 32)
  6. def from_value(value):
  7. return value.to_bytes(32, 'little')
  8. def hash_node(left, right):
  9. return hashlib.sha256(left + right).digest()
  10. # R
  11. # / \
  12. # o o i = 2
  13. # / \ / \
  14. # o o o o i = 1
  15. # / \ / \ / \ / \
  16. # 110 4 77 5 - - 6 - i = 0
  17. # 0 1 2 3 4 5 6 7
  18. # root 0
  19. # (2, 0) 1
  20. # (2, 1) 2
  21. # (1, 0) 3
  22. # (1, 1) 4
  23. # (1, 2) 5
  24. # (1, 3) 6
  25. # (0, 0) 7
  26. # (0, 1) 8
  27. # (0, 2) 9
  28. # (0, 3) 10
  29. # (0, 4) 11
  30. # (0, 5) 12
  31. # (0, 6) 13
  32. # (0, 7) 14
  33. empties = [
  34. NULL,
  35. hash_node(NULL, NULL),
  36. ]
  37. empties.append(hash_node(empties[-1], empties[-1]))
  38. # root for an empty tree
  39. empties.append(hash_node(empties[-1], empties[-1]))
  40. # Positions 4, 5 and 7 are empty
  41. layer_0 = [
  42. from_value(110),
  43. from_value(4),
  44. from_value(77),
  45. from_value(5),
  46. NULL,
  47. NULL,
  48. from_value(6),
  49. NULL,
  50. ]
  51. layer_1 = [
  52. hash_node(layer_0[0], layer_0[1]),
  53. hash_node(layer_0[2], layer_0[3]),
  54. # Subtree has empty leaves so just use NULL instead
  55. hash_node(layer_0[4], layer_0[5]),
  56. hash_node(layer_0[6], layer_0[7]),
  57. ]
  58. layer_2 = [
  59. hash_node(layer_1[0], layer_1[1]),
  60. hash_node(layer_1[2], layer_1[3]),
  61. ]
  62. root = hash_node(layer_2[0], layer_2[1])
  63. table = {
  64. # root
  65. 0: root,
  66. # (2, 0)
  67. 1: layer_2[0],
  68. # This subtree contains a single value
  69. # (2, 1)
  70. 2: layer_2[1],
  71. # (1, 0)
  72. 3: layer_1[0],
  73. # (1, 1)
  74. 4: layer_1[1],
  75. # ... (1, 2) (idx=5) is not needed
  76. # (1, 3)
  77. 6: layer_1[3],
  78. # Don't add (0, 4), (0, 5) and (0, 7)
  79. 7: layer_0[0],
  80. 8: layer_0[1],
  81. 9: layer_0[2],
  82. 10: layer_0[3],
  83. 13: layer_0[6],
  84. }
  85. # Prove that leaf 5 is set to None
  86. leaf = NULL
  87. pos = 0b101
  88. path = []
  89. # Sibling of 5 is pos=4, with loc=(0, 4), which is idx=11
  90. sibling_idx = 11
  91. assert sibling_idx not in table
  92. path.append(empties[0])
  93. # Next node is (1, 2) with sibling (1, 3) and idx=6
  94. path.append(table[6])
  95. # Next node is (2, 1) with sibling (2, 0) and idx=1
  96. path.append(table[1])
  97. assert path == [
  98. NULL,
  99. layer_1[3],
  100. layer_2[0]
  101. ]
  102. assert hash_node(path[2], hash_node(hash_node(path[0], leaf), path[1])) == root
  103. # Starting from the bottom here
  104. # Now do verification
  105. assert leaf == NULL
  106. bits = [bool(pos & (1<<n)) for n in range(3)]
  107. node = leaf
  108. for bit, other_node in zip(bits, path):
  109. nodes = (other_node, node) if bit else (node, other_node)
  110. node = hash_node(*nodes)
  111. assert root == node
  112. assert pos == 5
  113. print("Passed")