|
| 1 | +// ======================================================================= |
| 2 | +// LazyTower Circuit |
| 3 | +// ======================================================================= |
| 4 | +// A recursive hash-chain circuit that verifies membership proofs over a |
| 5 | +// multi-level tree structure, similar to a Merkle tree. |
| 6 | +// |
| 7 | +// Parameters: |
| 8 | +// - H (u32): Max number of levels (tree height). |
| 9 | +// - W (u32): Max number of elements per level. |
| 10 | +// - W_BITS (u32): Bit-width used to encode each level's length. |
| 11 | +// |
| 12 | +// - Verifies that a claimed item is covered by a valid Merkle-like |
| 13 | +// proof rooted at `digest_of_digest`. |
| 14 | +// |
| 15 | +// See `lazy_tower_hash_chain()` for expected inputs and proof structure. |
| 16 | +// ======================================================================= |
| 17 | + |
| 18 | +use poseidon::poseidon::bn254::hash_2; |
| 19 | + |
| 20 | +pub struct LazyTower<let H: u32, let W: u32, let W_BITS: u32> {} |
| 21 | + |
| 22 | +impl<let H: u32, let W: u32, let W_BITS: u32> LazyTower<H, W, W_BITS> { |
| 23 | + // len 0: 0 |
| 24 | + // len 1 in[0] |
| 25 | + // len 2: H(in[0], in[1]) |
| 26 | + // len 3: H(H(in[0], in[1]), in[2]) |
| 27 | + // len 4: H(H(H(in[0], in[1]), in[2]), in[3]) |
| 28 | + /// Compute hash chain of given length using Poseidon. |
| 29 | + fn hash_chain<let N: u32>(inputs: [Field; N], len: u32) -> Field { |
| 30 | + let mut outs = [0; (N + 1)]; |
| 31 | + outs[1] = inputs[0]; |
| 32 | + |
| 33 | + // outs[0] = 0; |
| 34 | + // outs[1] = inputs[0] |
| 35 | + // Start from i = 2: outs[2] = H(inputs[0], inputs[1]) |
| 36 | + for i in 2..(N + 1) { |
| 37 | + outs[i] = hash_2([outs[i - 1], inputs[i - 1]]); |
| 38 | + } |
| 39 | + outs[len] |
| 40 | + } |
| 41 | + |
| 42 | + /// Check if `inputs` is in array (returns 1 or 0). |
| 43 | + fn include(inputs: [Field; W], item: Field) -> u32 { |
| 44 | + let mut acc = 1; |
| 45 | + |
| 46 | + for i in 0..inputs.len() { |
| 47 | + acc *= inputs[i] - item; |
| 48 | + } |
| 49 | + |
| 50 | + (acc == 0) as u32 |
| 51 | + } |
| 52 | + |
| 53 | + // (N)(len) |
| 54 | + // leading_ones(4)(0) = [0, 0, 0, 0] |
| 55 | + // leading_ones(4)(1) = [1, 0, 0, 0] |
| 56 | + // leading_ones(4)(2) = [1, 1, 0, 0] |
| 57 | + // leading_ones(4)(3) = [1, 1, 1, 0] |
| 58 | + // leading_ones(4)(4) = [1, 1, 1, 1] |
| 59 | + // leading_ones(4)(5) = fail |
| 60 | + /// Return array of N bits with `len` leading ones. |
| 61 | + fn leading_ones<let N: u32>(len: u32) -> [u32; N] { |
| 62 | + let mut output = [0; N]; |
| 63 | + let mut one_count = 0; |
| 64 | + |
| 65 | + for i in 0..N { |
| 66 | + if i < len { output[i] = 1; }; |
| 67 | + let val = output[i] as Field; |
| 68 | + assert(val * (val - 1) == 0); |
| 69 | + one_count += output[i]; |
| 70 | + } |
| 71 | + assert(one_count == len); |
| 72 | + |
| 73 | + let mut from_0_to_1 = [0; (N - 1)]; |
| 74 | + let mut from_0_to_1_count = 0; |
| 75 | + |
| 76 | + for i in 0..(N - 1) { |
| 77 | + from_0_to_1[i] = (1 - output[i]) * output[i + 1]; |
| 78 | + from_0_to_1_count += from_0_to_1[i]; |
| 79 | + } |
| 80 | + assert(from_0_to_1_count == 0); |
| 81 | + |
| 82 | + output |
| 83 | + } |
| 84 | + |
| 85 | + // Is root being included in the first prefix_len elements of inputs[]? |
| 86 | + /// Ensure root appears within the first `prefix_len` items. |
| 87 | + fn include_prefix(inputs: [Field; W], prefix_len: u32, root: Field) -> u32 { |
| 88 | + let leading_ones: [u32; W] = Self::leading_ones(prefix_len); |
| 89 | + let mut is_good = [0; W]; |
| 90 | + let mut good_count = 0; |
| 91 | + |
| 92 | + for i in 0..W { |
| 93 | + let result = if inputs[i] == root { 1 } else { 0 }; |
| 94 | + is_good[i] = result & leading_ones[i]; |
| 95 | + good_count += is_good[i]; |
| 96 | + } |
| 97 | + |
| 98 | + assert(good_count == 1); |
| 99 | + good_count |
| 100 | + } |
| 101 | + |
| 102 | + // Computes a Merkle root at root_lv made from childrens[0 .. root_lv - 1][] and leaf. |
| 103 | + // |
| 104 | + // Each childrens[i] must include the digest of childrens[i - 1] for i = 1 ... root_lv - 1 |
| 105 | + // childrens[0] must include leaf. |
| 106 | + // |
| 107 | + // root = digest of childrens[root_lv - 1] if root_lv > 0 |
| 108 | + // root = leaf if root_lv == 0 |
| 109 | + /// Verify Merkle proof up to root_lv and return root. |
| 110 | + fn check_merkle_proof_and_compute_root( |
| 111 | + childrens: [[Field; W]; H - 1], |
| 112 | + root_lv: u32, |
| 113 | + leaf: Field, |
| 114 | + ) -> Field { |
| 115 | + // TBI: to be included |
| 116 | + // |
| 117 | + // childrens[lv] must include TBI[lv] for all lv in [0 ... root_lv - 1] |
| 118 | + // |
| 119 | + // TBI[0] = leaf |
| 120 | + // TBI[lv] = digest of children[lv - 1] for all lv in [1 ... root_lv] |
| 121 | + // TBI[root_lv] is the root |
| 122 | + // |
| 123 | + // For root_lv = 3, H = 5: mustInclude[] |
| 124 | + // TBI[4] 0 |
| 125 | + // root_lv => TBI[3] <== digest of childrens[2] ==> *root* 0 |
| 126 | + // childrens[2] include TBI[2] <== digest of childrens[1] 1 |
| 127 | + // childrens[1] include TBI[1] <== digest of childrens[0] 1 |
| 128 | + // childrens[0] include TBI[0] <== *leaf* 1 |
| 129 | + let mut TBI = [0; H]; |
| 130 | + TBI[0] = leaf; |
| 131 | + |
| 132 | + let must_include: [u32; H - 1] = Self::leading_ones(root_lv); |
| 133 | + |
| 134 | + for lv in 0..(H - 1) { |
| 135 | + let not_must_include = 1 - (must_include[lv] != 0) as u32; |
| 136 | + assert((Self::include(childrens[lv], TBI[lv]) | not_must_include) == 1); |
| 137 | + |
| 138 | + TBI[lv + 1] = Self::hash_chain(childrens[lv], W); |
| 139 | + } |
| 140 | + |
| 141 | + let root = TBI[root_lv]; |
| 142 | + |
| 143 | + root |
| 144 | + } |
| 145 | + |
| 146 | + /// Count nonzero level slots in packed level_lengths. |
| 147 | + fn compute_data_height(mut level_lengths: u32) -> u32 { |
| 148 | + let mut h = 0; |
| 149 | + |
| 150 | + for _ in 0..(32 / W_BITS) { |
| 151 | + let is_nonzero = (level_lengths != 0) as u32; |
| 152 | + h += is_nonzero; |
| 153 | + level_lengths >>= W_BITS; |
| 154 | + } |
| 155 | + |
| 156 | + h |
| 157 | + } |
| 158 | + |
| 159 | + /// Extract W_BITS-wide level length at index lv. |
| 160 | + fn compute_single_level_length(level_lengths: u32, lv: u32) -> u32 { |
| 161 | + let mask = (1 << W_BITS) - 1; |
| 162 | + level_lengths >> (lv * W_BITS) & mask |
| 163 | + } |
| 164 | + |
| 165 | + // The code relies on the following statement: |
| 166 | + // If |
| 167 | + // 1. levelLengthArray[i] belongs to [1, W] for i in [0, dataHeight - 1], otherwise levelLengthArray[i] = 0 |
| 168 | + // 2. dataHeight belongs to [0, H - 1] |
| 169 | + // 3. the W^i weighted sum of levelLengthArray = levelLengths |
| 170 | + // |
| 171 | + // , then levelLengthArray[] and dataHeight will be unique. |
| 172 | + // |
| 173 | + // A very rough analogy would be like in the 10-base system, |
| 174 | + // the only sequence matches with 492 could only be the length 3 [2, 9, 4]. |
| 175 | + /// Parse packed level_lengths into array and data height. |
| 176 | + fn compute_data_height_and_level_length_array(level_lengths: u32) -> (u32, [u32; H]) { |
| 177 | + let mut level_length_array = [0; H]; |
| 178 | + let data_height = Self::compute_data_height(level_lengths); |
| 179 | + |
| 180 | + for lv in 0..H { |
| 181 | + level_length_array[lv] = Self::compute_single_level_length(level_lengths, lv); |
| 182 | + } |
| 183 | + |
| 184 | + let ones: [u32; H] = Self::leading_ones(data_height); |
| 185 | + let mut dummy = [[0; W_BITS]; H]; |
| 186 | + let mut s = 0; |
| 187 | + |
| 188 | + for lv in 0..H { |
| 189 | + let level_length_array_to_field = level_length_array[lv] as Field; |
| 190 | + dummy[lv] = level_length_array_to_field.to_le_bits(); |
| 191 | + assert(level_length_array[lv] <= W); |
| 192 | + assert((level_length_array[lv] != 0) == (ones[lv] == 1)); |
| 193 | + s += level_length_array[lv] as Field * 2.pow_32(lv as Field * W_BITS as Field); |
| 194 | + } |
| 195 | + |
| 196 | + assert(level_lengths as Field == s); |
| 197 | + (data_height, level_length_array) |
| 198 | + } |
| 199 | + |
| 200 | + /// Verifies a claimed item's inclusion in a multi-level hash chain ending in `digest_of_digest`. |
| 201 | + pub fn lazy_tower_hash_chain( |
| 202 | + level_lengths: u32, |
| 203 | + digest_of_digest: Field, |
| 204 | + top_down_digest: [Field; H], |
| 205 | + root_lv: u32, |
| 206 | + root_level: [Field; W], |
| 207 | + childrens: [[Field; W]; H - 1], |
| 208 | + item: Field, |
| 209 | + ) { |
| 210 | + // Ensure at least one level exists; cannot prove inclusion with no data. |
| 211 | + assert(level_lengths != 0); |
| 212 | + |
| 213 | + // Unpack level_lengths and compute how many levels have non-zero data. |
| 214 | + let (data_height, level_length_array) = |
| 215 | + Self::compute_data_height_and_level_length_array(level_lengths); |
| 216 | + |
| 217 | + // Ensure dataHeight < 2^8 |
| 218 | + assert(data_height < (2.pow_32(8)) as u32); |
| 219 | + |
| 220 | + // Ensure the claimed root level is within the active levels. |
| 221 | + assert(root_lv < data_height); |
| 222 | + |
| 223 | + // Fetch the number of elements at the root level. |
| 224 | + let root_level_length = level_length_array[root_lv]; |
| 225 | + |
| 226 | + // Root level index must be valid. |
| 227 | + assert(root_lv < H); |
| 228 | + |
| 229 | + // Confirm that top-down digests compress correctly to digest_of_digest. |
| 230 | + assert(Self::hash_chain(top_down_digest, data_height) == digest_of_digest); |
| 231 | + |
| 232 | + // Reconstruct root_level digest and compare it to expected value. |
| 233 | + let root_level_digest = top_down_digest[data_height - root_lv - 1]; |
| 234 | + assert(Self::hash_chain(root_level, root_level_length) == root_level_digest); |
| 235 | + |
| 236 | + // Check that the Merkle root includes the item and is present in root_level. |
| 237 | + let root = Self::check_merkle_proof_and_compute_root(childrens, root_lv, item); |
| 238 | + assert(Self::include_prefix(root_level, root_level_length, root) == 1); |
| 239 | + } |
| 240 | +} |
0 commit comments