From a21d16e80b6d509b6ba9a85a132b5770b402d2ad Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Sun, 13 Sep 2026 10:34:49 -0400 Subject: [PATCH 1/2] Add a pure Lean BLAKE3 implementation with checked proofs --- Blake3/Pure.lean | 155 +++++++++++++ Blake3/Pure/Proofs.lean | 409 ++++++++++++++++++++++++++++++++++ Blake3Test.lean | 3 + README.md | 44 +++- Tests/Pure.lean | 73 ++++++ Tests/PureAudit.lean | 160 +++++++++++++ Tests/PureVectors.lean | 114 ++++++++++ lakefile.lean | 4 +- rust/examples/pure_vectors.rs | 47 ++++ 9 files changed, 1007 insertions(+), 2 deletions(-) create mode 100644 Blake3/Pure.lean create mode 100644 Blake3/Pure/Proofs.lean create mode 100644 Tests/Pure.lean create mode 100644 Tests/PureAudit.lean create mode 100644 Tests/PureVectors.lean create mode 100644 rust/examples/pure_vectors.rs diff --git a/Blake3/Pure.lean b/Blake3/Pure.lean new file mode 100644 index 0000000..78b0eb9 --- /dev/null +++ b/Blake3/Pure.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2026 Argument Computer Corporation. +SPDX-License-Identifier: MIT OR Apache-2.0 +-/ + +module +public import Blake3 +public import Std + +@[expose] public section + +/-! Total, unkeyed, 32-byte BLAKE3 with a checked canonical tree. +Words and compression blocks have checked dimensions. The canonical tree +splits at the largest power of two strictly below the input byte length. +The native input bound is separate from the total mathematical function. +-/ + +namespace Blake3.Pure + +abbrev CV := Vector UInt32 8 +abbrev Block := Vector UInt32 16 +abbrev Digest := Vector UInt8 32 + +def iv : CV := #v[ + 0x6A09E667, 0xBB67AE85, 0x3C6EF372, 0xA54FF53A, + 0x510E527F, 0x9B05688C, 0x1F83D9AB, 0x5BE0CD19] + +def schedules : Vector (Vector (Fin 16) 16) 7 := #v[ + #v[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15], + #v[2, 6, 3, 10, 7, 0, 4, 13, 1, 11, 12, 5, 9, 14, 15, 8], + #v[3, 4, 10, 12, 13, 2, 7, 14, 6, 5, 9, 0, 11, 15, 8, 1], + #v[10, 7, 12, 9, 14, 3, 13, 15, 4, 0, 11, 2, 5, 8, 1, 6], + #v[12, 13, 9, 11, 15, 10, 14, 8, 7, 2, 5, 3, 0, 1, 6, 4], + #v[9, 14, 11, 5, 8, 12, 15, 1, 13, 3, 0, 10, 2, 6, 4, 7], + #v[11, 15, 5, 0, 1, 9, 8, 6, 14, 10, 2, 12, 3, 4, 7, 13]] + +def rotateRight (word count : UInt32) : UInt32 := + (word >>> count) ||| (word <<< (32 - count)) + +def mix (a b c d x y : UInt32) : Vector UInt32 4 := + let a := a + b + x + let d := rotateRight (d ^^^ a) 16 + let c := c + d + let b := rotateRight (b ^^^ c) 12 + let a := a + b + y + let d := rotateRight (d ^^^ a) 8 + let c := c + d + let b := rotateRight (b ^^^ c) 7 + #v[a, b, c, d] + +def g (state : Block) (a b c d : Fin 16) (x y : UInt32) : Block := + let words := mix state[a] state[b] state[c] state[d] x y + (((state.set a words[0]).set b words[1]).set c words[2]).set d words[3] + +def round (state message : Block) (schedule : Vector (Fin 16) 16) : Block := + let state := g state 0 4 8 12 message[schedule[0]] message[schedule[1]] + let state := g state 1 5 9 13 message[schedule[2]] message[schedule[3]] + let state := g state 2 6 10 14 message[schedule[4]] message[schedule[5]] + let state := g state 3 7 11 15 message[schedule[6]] message[schedule[7]] + let state := g state 0 5 10 15 message[schedule[8]] message[schedule[9]] + let state := g state 1 6 11 12 message[schedule[10]] message[schedule[11]] + let state := g state 2 7 8 13 message[schedule[12]] message[schedule[13]] + g state 3 4 9 14 message[schedule[14]] message[schedule[15]] + +def initialWords (cv : CV) (counter : UInt64) (blockLen flags : UInt32) : Block := + #v[cv[0], cv[1], cv[2], cv[3], cv[4], cv[5], cv[6], cv[7], + iv[0], iv[1], iv[2], iv[3], counter.toUInt32, (counter >>> 32).toUInt32, blockLen, flags] + +def compress (cv : CV) (message : Block) (counter : UInt64) (blockLen flags : UInt32) : CV := + let state := schedules.foldl (fun state schedule => round state message schedule) + (initialWords cv counter blockLen flags) + Vector.ofFn fun index => state[index.val] ^^^ state[index.val + 8] + +def wordBytes (word : UInt32) : Vector UInt8 4 := + Vector.ofFn fun index => (word.toNat / 256^index.val).toUInt8 + +def littleEndian (bytes : List UInt8) : Nat := + bytes.foldr (fun byte rest => byte.toNat + 256 * rest) 0 + +def bytesWord (bytes : Vector UInt8 4) : UInt32 := + UInt32.ofNat (littleEndian bytes.toList) + +/-- Zero padding is part of block framing, including the empty input block. -/ +def blockWords (bytes : List UInt8) : Block := + let input := bytes.toArray + Vector.ofFn fun word => bytesWord (Vector.ofFn fun byte => input[word.val * 4 + byte.val]?.getD 0) + +def cvBytes (cv : CV) : Digest := + Vector.ofFn fun index => (wordBytes cv[index.val / 4])[index.val % 4] + +structure Output where + cv : CV + block : Block + blockLen : UInt32 + counter : UInt64 + flags : UInt32 + deriving DecidableEq, Repr + +def Output.chainingValue (output : Output) : CV := + compress output.cv output.block output.counter output.blockLen output.flags + +def Output.rootHash (output : Output) : Digest := + cvBytes (compress output.cv output.block 0 output.blockLen (output.flags ||| 8)) + +/-- A full last block receives CHUNK_END; it is never followed by an empty block. -/ +def chunkLoop (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) : Output := + if h : input.length ≤ 64 then + ⟨cv, blockWords input, input.length.toUInt32, counter, (if start then 1 else 0) ||| 2⟩ + else + let next := compress cv (blockWords (input.take 64)) counter 64 (if start then 1 else 0) + chunkLoop counter next false (input.drop 64) +termination_by input.length +decreasing_by simp only [List.length_drop]; omega + +def chunkOutput (counter : UInt64) (input : List UInt8) : Output := + chunkLoop counter iv true input + +/-- Construct an internal BLAKE3 parent from two chaining values. -/ +def parentOutput (left right : CV) : Output := + ⟨iv, left ++ right, 64, 0, 4⟩ + +def leftLen (size : Nat) : Nat := 2 ^ (size - 1).log2 + +theorem leftLen_positive (size : Nat) : 0 < leftLen size := Nat.two_pow_pos _ + +theorem leftLen_lt {size : Nat} (large : 1024 < size) : leftLen size < size := by + have := Nat.log2_self_le (n := size - 1) (by omega) + unfold leftLen + omega + +def subtree (counter : Nat) (input : List UInt8) : Output := + if _h : input.length ≤ 1024 then chunkOutput counter.toUInt64 input + else + let split := leftLen input.length + let left := subtree counter (input.take split) + let right := subtree (counter + split / 1024) (input.drop split) + parentOutput left.chainingValue right.chainingValue +termination_by input.length +decreasing_by + · have := leftLen_lt (size := input.length) (by omega) + simp only [List.length_take]; omega + · have := leftLen_positive input.length + simp only [List.length_drop]; omega + +def digest (input : List UInt8) : Digest := (subtree 0 input).rootHash + +/-- Native BLAKE3 supports at most 2^64 - 1 input bytes. -/ +def NativeInput (input : List UInt8) : Prop := input.length < 2^64 + +/-- Compute the standard unkeyed 32-byte digest using total Lean code. -/ +def hash (input : ByteArray) : Blake3Hash := + let bytes := digest input.data.toList + ⟨⟨bytes.toArray⟩, bytes.size_toArray⟩ + +end Blake3.Pure diff --git a/Blake3/Pure/Proofs.lean b/Blake3/Pure/Proofs.lean new file mode 100644 index 0000000..8ab12b4 --- /dev/null +++ b/Blake3/Pure/Proofs.lean @@ -0,0 +1,409 @@ +/- +Copyright (c) 2026 Argument Computer Corporation. +SPDX-License-Identifier: MIT OR Apache-2.0 +-/ + +module +public import Blake3.Pure + +public section + +namespace Blake3.Pure + +def encodeLittleEndian : Nat → Nat → List UInt8 + | 0, _ => [] + | count + 1, value => value.toUInt8 :: encodeLittleEndian count (value / 256) + +theorem encodeLittleEndian_length (count value : Nat) : (encodeLittleEndian count value).length = count := by + induction count generalizing value with + | zero => rfl + | succ count ih => simp [encodeLittleEndian, ih] + +theorem littleEndian_bound (bytes : List UInt8) : littleEndian bytes < 256^bytes.length := by + induction bytes with + | nil => decide + | cons byte bytes ih => + have bounded := byte.toNat_lt + simp only [littleEndian, List.foldr_cons, List.length_cons, Nat.pow_succ] at * + omega + +theorem littleEndian_encode (count value : Nat) (bounded : value < 256^count) : + littleEndian (encodeLittleEndian count value) = value := by + induction count generalizing value with + | zero => + have zero : value = 0 := by simpa using bounded + subst value + rfl + | succ count ih => + have small : value / 256 < 256^count := by + apply (Nat.div_lt_iff_lt_mul (by decide : 0 < 256)).mpr + simpa only [Nat.pow_succ] using bounded + simp only [encodeLittleEndian, littleEndian, List.foldr_cons] + change value.toUInt8.toNat + 256 * littleEndian (encodeLittleEndian count (value / 256)) = value + rw [ih _ small] + exact Nat.mod_add_div _ _ + + +theorem schedules_permute : ∀ index : Fin 7, + schedules[index].toList.Perm (List.finRange 16) := by decide + +theorem schedules_next : ∀ index : Fin 6, + schedules[index.val + 1] = Vector.ofFn (fun position : Fin 16 => + schedules[index.val][schedules[1][position]]) := by + have entries : ∀ index : Fin 6, ∀ position : Fin 16, + schedules[index.val + 1][position] = schedules[index.val][schedules[1][position]] := by decide + intro index + apply Vector.ext + intro position bounded + simpa using entries index ⟨position, bounded⟩ + +theorem rotateRight_bits (word : UInt32) (count : UInt32) + (positive : 0 < count.toNat) (bounded : count.toNat < 32) : + (rotateRight word count).toBitVec = word.toBitVec.rotateRight count.toNat := by + simp [rotateRight, UInt32.toBitVec_shiftRight, UInt32.toBitVec_shiftLeft, + BitVec.rotateRight_def, Nat.mod_eq_of_lt bounded] + congr 2 + omega + +theorem bytesWord_value (bytes : Vector UInt8 4) : + (bytesWord bytes).toNat = littleEndian bytes.toList := by + have bound := littleEndian_bound bytes.toList + simp only [Vector.length_toList] at bound + exact Nat.mod_eq_of_lt (by simpa using bound) + +theorem wordBytes_encoding (word : UInt32) : (wordBytes word).toList = encodeLittleEndian 4 word.toNat := by + simp [wordBytes, Vector.toList_ofFn, List.ofFn_succ, encodeLittleEndian, Nat.div_div_eq_div_mul] + +theorem bytesWord_wordBytes (word : UInt32) : bytesWord (wordBytes word) = word := by + apply UInt32.toNat_inj.mp + rw [bytesWord_value, wordBytes_encoding] + exact littleEndian_encode 4 word.toNat (by exact word.toNat_lt) + +theorem bytesWord_pack (a b c d : UInt8) : (bytesWord #v[a, b, c, d]).toNat = + a.toNat + 256 * (b.toNat + 256 * (c.toNat + 256 * d.toNat)) := by + rw [bytesWord_value] + simp [littleEndian] + +theorem wordBytes_pack (a b c d : UInt8) : wordBytes (bytesWord #v[a, b, c, d]) = #v[a, b, c, d] := by + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + have hd := d.toNat_lt + apply Vector.ext + intro index bounded + have cases : index = 0 ∨ index = 1 ∨ index = 2 ∨ index = 3 := by omega + rcases cases with rfl | rfl | rfl | rfl <;> + apply UInt8.toNat_inj.mp <;> simp [wordBytes, bytesWord_pack] <;> omega + +theorem wordBytes_bytesWord (bytes : Vector UInt8 4) : wordBytes (bytesWord bytes) = bytes := by + have value : bytes = #v[bytes[0], bytes[1], bytes[2], bytes[3]] := by + apply Vector.ext + intro index bounded + have cases : index = 0 ∨ index = 1 ∨ index = 2 ∨ index = 3 := by omega + rcases cases with rfl | rfl | rfl | rfl <;> rfl + conv => lhs; rw [value] + rw [wordBytes_pack, ← value] + +theorem bytesWord_injective {first second : Vector UInt8 4} (equal : bytesWord first = bytesWord second) : + first = second := by rw [← wordBytes_bytesWord first, equal, wordBytes_bytesWord] + +theorem blockWords_byte (input : List UInt8) (word : Fin 16) (byte : Fin 4) : + ((Vector.ofFn fun byte : Fin 4 => input.toArray[word.val * 4 + byte.val]?.getD 0) : Vector UInt8 4)[byte] + = input[word.val * 4 + byte.val]?.getD 0 := by simp + +theorem blockWords_value (input : List UInt8) (word : Fin 16) : + (blockWords input)[word].toNat = + littleEndian (List.ofFn fun byte : Fin 4 => input[word.val * 4 + byte.val]?.getD 0) := by + simpa [blockWords, Vector.toList_ofFn] using bytesWord_value + (Vector.ofFn fun byte : Fin 4 => input.toArray[word.val * 4 + byte.val]?.getD 0) + +theorem cvBytes_value (cv : CV) (index : Fin 32) : + (cvBytes cv)[index] = (cv[index.val / 4].toNat / 256^(index.val % 4)).toUInt8 := by + simp [cvBytes, wordBytes] + +theorem g_unchanged (state : Block) (a b c d index : Fin 16) (x y : UInt32) + (ha : a ≠ index) (hb : b ≠ index) (hc : c ≠ index) (hd : d ≠ index) : + (g state a b c d x y)[index] = state[index] := by + simp [g, Fin.getElem_fin, Fin.val_inj, ha, hb, hc, hd] + +theorem g_values (state : Block) (a b c d : Fin 16) (x y : UInt32) + (ab : a ≠ b) (ac : a ≠ c) (ad : a ≠ d) (bc : b ≠ c) (bd : b ≠ d) (cd : c ≠ d) : + let words := mix state[a] state[b] state[c] state[d] x y + (g state a b c d x y)[a] = words[0] ∧ (g state a b c d x y)[b] = words[1] ∧ + (g state a b c d x y)[c] = words[2] ∧ (g state a b c d x y)[d] = words[3] := by + simp [g, Fin.getElem_fin, Fin.val_inj, + Ne.symm ab, Ne.symm ac, Ne.symm ad, Ne.symm bc, Ne.symm bd, Ne.symm cd] + +theorem initialWords_counter (cv : CV) (counter : UInt64) (blockLen flags : UInt32) : + (initialWords cv counter blockLen flags)[12].toNat + + 2^32 * (initialWords cv counter blockLen flags)[13].toNat = counter.toNat := by + have bounded := counter.toNat_lt + simp [initialWords, Nat.shiftRight_eq_div_pow] + omega + +theorem parentOutput_values (left right : CV) : + (parentOutput left right).cv = iv ∧ (parentOutput left right).block = left ++ right ∧ + (parentOutput left right).blockLen = 64 ∧ (parentOutput left right).counter = 0 ∧ + (parentOutput left right).flags = 4 := ⟨rfl, rfl, rfl, rfl, rfl⟩ + +theorem leftLen_bounds {size : Nat} (large : 1024 < size) : + leftLen size < size ∧ size ≤ 2 * leftLen size := by + have upper := Nat.lt_log2_self (n := size - 1) + rw [Nat.pow_succ] at upper + exact ⟨leftLen_lt large, by unfold leftLen; omega⟩ + +theorem leftLen_chunks {size : Nat} (large : 1024 < size) : + ∃ exponent, leftLen size = 1024 * 2^exponent := by + have exponent : 10 ≤ (size - 1).log2 := (Nat.le_log2 (by omega)).mpr (by omega) + refine ⟨(size - 1).log2 - 10, ?_⟩ + unfold leftLen + conv => lhs; rw [show (size - 1).log2 = 10 + ((size - 1).log2 - 10) by omega] + rw [Nat.pow_add] + +theorem leftLen_chunk_multiple {size : Nat} (large : 1024 < size) : + leftLen size / 1024 * 1024 = leftLen size := by + obtain ⟨exponent, value⟩ := leftLen_chunks large + rw [value] + omega + +theorem leftLen_unique {left right exponent : Nat} + (power : left = 1024 * 2^exponent) (positive : 0 < right) (bounded : right ≤ left) : + leftLen (left + right) = left := by + have pow : left = 2^(10 + exponent) := by rw [Nat.pow_add]; exact power + have nonzero : left + right - 1 ≠ 0 := by + have := Nat.two_pow_pos (10 + exponent) + omega + have log : (left + right - 1).log2 = 10 + exponent := + (Nat.log2_eq_iff nonzero).mpr ⟨by omega, by rw [Nat.pow_succ, ← pow]; omega⟩ + rw [leftLen, log, ← pow] + +theorem chunkLoop_small (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) + (small : input.length ≤ 64) : + chunkLoop counter cv start input = + ⟨cv, blockWords input, input.length.toUInt32, counter, (if start then 1 else 0) ||| 2⟩ := by + rw [chunkLoop, dif_pos small] + +theorem chunkLoop_step (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) + (large : 64 < input.length) : + chunkLoop counter cv start input = + chunkLoop counter (compress cv (blockWords (input.take 64)) counter 64 (if start then 1 else 0)) + false (input.drop 64) := by + rw [chunkLoop, dif_neg (by omega)] + +theorem chunkLoop_counter (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) : + (chunkLoop counter cv start input).counter = counter := by + rw [chunkLoop] + split + · rfl + · exact chunkLoop_counter _ _ _ _ +termination_by input.length +decreasing_by simp only [List.length_drop]; omega + +theorem chunkOutput_counter (counter : UInt64) (input : List UInt8) : + (chunkOutput counter input).counter = counter := chunkLoop_counter _ _ _ _ + +/-- Every non-final block has exactly 64 bytes. The final block may be full; +only the empty input has an empty final block. -/ +inductive ChunkReads (counter : UInt64) : CV → Bool → List UInt8 → Output → Prop where + | last (cv : CV) (start : Bool) (input : List UInt8) (small : input.length ≤ 64) : + ChunkReads counter cv start input + ⟨cv, blockWords input, input.length.toUInt32, counter, (if start then 1 else 0) ||| 2⟩ + | step (cv : CV) (start : Bool) (input : List UInt8) (output : Output) + (large : 64 < input.length) + (rest : ChunkReads counter + (compress cv (blockWords (input.take 64)) counter 64 (if start then 1 else 0)) + false (input.drop 64) output) : ChunkReads counter cv start input output + +theorem chunkLoop_reads (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) : + ChunkReads counter cv start input (chunkLoop counter cv start input) := by + by_cases small : input.length ≤ 64 + · rw [chunkLoop_small _ _ _ _ small] + exact .last _ _ _ small + · rw [chunkLoop_step _ _ _ _ (by omega)] + exact .step _ _ _ _ (by omega) (chunkLoop_reads _ _ _ _) +termination_by input.length +decreasing_by simp only [List.length_drop]; omega + +theorem ChunkReads.complete {counter : UInt64} {cv : CV} {start : Bool} {input : List UInt8} {output : Output} + (reads : ChunkReads counter cv start input output) : chunkLoop counter cv start input = output := by + induction reads with + | last cv start input small => exact chunkLoop_small _ _ _ _ small + | step cv start input output large rest ih => rw [chunkLoop_step _ _ _ _ large, ih] + +theorem chunkLoop_iff (counter : UInt64) (cv : CV) (start : Bool) (input : List UInt8) (output : Output) : + chunkLoop counter cv start input = output ↔ ChunkReads counter cv start input output := + ⟨fun equal => equal ▸ chunkLoop_reads _ _ _ _, ChunkReads.complete⟩ + +theorem ChunkReads.framing {counter : UInt64} {cv : CV} {start : Bool} {input : List UInt8} {output : Output} + (reads : ChunkReads counter cv start input output) : + ∃ count, let remaining := input.drop (64 * count) + remaining.length ≤ 64 ∧ (input ≠ [] → 0 < remaining.length) ∧ + output.block = blockWords remaining ∧ output.blockLen.toNat = remaining.length ∧ + output.counter = counter ∧ output.flags = (if start && count == 0 then 1 else 0) ||| 2 := by + induction reads with + | last cv start input small => + refine ⟨0, ?_⟩ + simp only [Nat.mul_zero, List.drop_zero, Nat.reduceBEq, Bool.and_true] + refine ⟨small, ?_, by trivial, ?_, by trivial, by trivial⟩ + · intro nonempty; exact List.length_pos_iff.mpr nonempty + · exact Nat.mod_eq_of_lt (by omega) + | step cv start input output large rest ih => + obtain ⟨count, bound, positive, block, length, counterEq, flags⟩ := ih + refine ⟨count + 1, ?_⟩ + simp only [List.drop_drop] at bound positive block length + have advance : 64 * (count + 1) = 64 + 64 * count := by omega + rw [advance] + refine ⟨bound, fun _ => positive (by simp only [← List.length_pos_iff, List.length_drop]; omega), + block, length, counterEq, ?_⟩ + simpa using flags + +theorem chunkOutput_framing (counter : UInt64) (input : List UInt8) (bounded : input.length ≤ 1024) : + ∃ count, count < 16 ∧ + let remaining := input.drop (64 * count) + remaining.length ≤ 64 ∧ (input ≠ [] → 0 < remaining.length) ∧ + (chunkOutput counter input).block = blockWords remaining ∧ + (chunkOutput counter input).blockLen.toNat = remaining.length ∧ + (chunkOutput counter input).counter = counter ∧ + (chunkOutput counter input).flags = (if count = 0 then 3 else 2) := by + obtain ⟨count, bound, positive, block, length, counterEq, flags⟩ := (chunkLoop_reads counter iv true input).framing + have countBound : count < 16 := by + by_cases nonempty : input = [] + · subst input + have : count = 0 := by + have flagEmpty : (chunkLoop counter iv true []).flags = 3 := by rw [chunkLoop_small _ _ _ _ (by decide)]; rfl + rw [flagEmpty] at flags + by_cases zero : count = 0 + · exact zero + · simp [zero] at flags + omega + · have := positive nonempty + simp only [List.length_drop] at this + omega + refine ⟨count, countBound, bound, positive, block, length, counterEq, ?_⟩ + change (chunkLoop counter iv true input).flags = _ + rw [flags] + by_cases zero : count = 0 <;> simp [zero] <;> decide + +theorem subtree_small (counter : Nat) (input : List UInt8) (small : input.length ≤ 1024) : + subtree counter input = chunkOutput counter.toUInt64 input := by + rw [subtree, dif_pos small] + +theorem subtree_step (counter : Nat) (input : List UInt8) (large : 1024 < input.length) : + subtree counter input = parentOutput + (subtree counter (input.take (leftLen input.length))).chainingValue + (subtree (counter + leftLen input.length / 1024) (input.drop (leftLen input.length))).chainingValue := by + rw [subtree, dif_neg (by omega)] + +theorem subtree_root_counter (input : List UInt8) : (subtree 0 input).counter = 0 := by + by_cases small : input.length ≤ 1024 + · rw [subtree_small _ _ small, chunkOutput_counter]; rfl + · rw [subtree_step _ _ (by omega)]; rfl + +/-- Canonical BLAKE3 trees, specified by full power-of-two left subtrees +and nonempty right subtrees no larger than their siblings. -/ +inductive TreeHash : Nat → List UInt8 → Output → Prop where + | chunk (counter : Nat) (input : List UInt8) (output : Output) (small : input.length ≤ 1024) + (blocks : ChunkReads counter.toUInt64 iv true input output) : TreeHash counter input output + | parent (counter exponent : Nat) (left right : List UInt8) (leftOutput rightOutput : Output) + (full : left.length = 1024 * 2^exponent) (nonempty : 0 < right.length) (bounded : right.length ≤ left.length) + (leftHash : TreeHash counter left leftOutput) + (rightHash : TreeHash (counter + left.length / 1024) right rightOutput) : + TreeHash counter (left ++ right) (parentOutput leftOutput.chainingValue rightOutput.chainingValue) + +theorem subtree_tree (counter : Nat) (input : List UInt8) : TreeHash counter input (subtree counter input) := by + by_cases small : input.length ≤ 1024 + · rw [subtree_small _ _ small] + exact .chunk _ _ _ small (chunkLoop_reads _ _ _ _) + · have large : 1024 < input.length := by omega + have splitBound := leftLen_bounds large + obtain ⟨exponent, full⟩ := leftLen_chunks large + have takeLength : (input.take (leftLen input.length)).length = leftLen input.length := by + simp only [List.length_take]; omega + have result := TreeHash.parent counter exponent (input.take (leftLen input.length)) + (input.drop (leftLen input.length)) _ _ (by rw [takeLength]; exact full) + (by simp only [List.length_drop]; omega) + (by simp only [List.length_drop, takeLength]; omega) + (subtree_tree _ _) (subtree_tree _ _) + rw [List.take_append_drop, takeLength] at result + rw [subtree_step _ _ large] + exact result +termination_by input.length +decreasing_by + · have := leftLen_lt (size := input.length) (by omega) + simp only [List.length_take]; omega + · have := leftLen_positive input.length + simp only [List.length_drop]; omega + +theorem TreeHash.complete {counter : Nat} {input : List UInt8} {output : Output} + (tree : TreeHash counter input output) : subtree counter input = output := by + induction tree with + | chunk counter input output small blocks => rw [subtree_small _ _ small]; exact blocks.complete + | parent counter exponent left right leftOutput rightOutput full nonempty bounded leftHash rightHash ihLeft ihRight => + have positive := Nat.two_pow_pos exponent + have large : 1024 < (left ++ right).length := by simp only [List.length_append]; omega + have split := leftLen_unique full nonempty bounded + rw [subtree_step _ _ large, List.length_append, split, + List.take_left, List.drop_left, ihLeft, ihRight] + +theorem subtree_iff (counter : Nat) (input : List UInt8) (output : Output) : + subtree counter input = output ↔ TreeHash counter input output := + ⟨fun equal => equal ▸ subtree_tree _ _, TreeHash.complete⟩ + +theorem TreeHash.unique {counter : Nat} {input : List UInt8} {first second : Output} + (one : TreeHash counter input first) (two : TreeHash counter input second) : first = second := + one.complete.symm.trans two.complete + +theorem native_counter {counter : Nat} {input : List UInt8} + (span : counter * 1024 + input.length < 2^64) : + counter < 2^54 ∧ counter.toUInt64.toNat = counter := by + constructor + · omega + · exact Nat.mod_eq_of_lt (by omega) + +theorem native_child_spans {counter : Nat} {input : List UInt8} + (span : counter * 1024 + input.length < 2^64) (large : 1024 < input.length) : + counter * 1024 + (input.take (leftLen input.length)).length < 2^64 ∧ + (counter + leftLen input.length / 1024) * 1024 + (input.drop (leftLen input.length)).length < 2^64 := by + have splitBound := leftLen_lt large + have multiple := leftLen_chunk_multiple large + simp only [List.length_take, List.length_drop, Nat.add_mul] + omega + +/-- A particular leaf reached by the actual canonical subtree recursion. -/ +inductive ChunkAt : Nat → List UInt8 → Nat → List UInt8 → Prop where + | leaf (counter : Nat) (input : List UInt8) (small : input.length ≤ 1024) : + ChunkAt counter input counter input + | left {counter leaf : Nat} {input bytes : List UInt8} (large : 1024 < input.length) + (path : ChunkAt counter (input.take (leftLen input.length)) leaf bytes) : + ChunkAt counter input leaf bytes + | right {counter leaf : Nat} {input bytes : List UInt8} (large : 1024 < input.length) + (path : ChunkAt (counter + leftLen input.length / 1024) (input.drop (leftLen input.length)) leaf bytes) : + ChunkAt counter input leaf bytes + +theorem ChunkAt.native {counter leaf : Nat} {input bytes : List UInt8} + (path : ChunkAt counter input leaf bytes) (span : counter * 1024 + input.length < 2^64) : + bytes.length ≤ 1024 ∧ leaf < 2^54 ∧ leaf.toUInt64.toNat = leaf := by + induction path with + | leaf counter input small => exact ⟨small, native_counter span⟩ + | left large path ih => exact ih (native_child_spans span large).1 + | right large path ih => exact ih (native_child_spans span large).2 + +theorem digest_native_counters {input bytes : List UInt8} (native : NativeInput input) {leaf : Nat} + (path : ChunkAt 0 input leaf bytes) : bytes.length ≤ 1024 ∧ leaf < 2^54 ∧ leaf.toUInt64.toNat = leaf := + path.native (by simpa only [NativeInput, Nat.zero_mul, Nat.zero_add] using native) + +theorem digest_tree (input : List UInt8) : + ∃ output, TreeHash 0 input output ∧ output.counter = 0 ∧ digest input = output.rootHash := + ⟨subtree 0 input, subtree_tree _ _, subtree_root_counter _, rfl⟩ + +theorem hash_size (input : ByteArray) : (hash input).val.size = 32 := (hash input).property + +theorem hash_digest (input : ByteArray) : (hash input).val.data.toList = (digest input.data.toList).toList := rfl + +theorem hash_tree (input : ByteArray) : + ∃ output, TreeHash 0 input.data.toList output ∧ output.counter = 0 ∧ + (hash input).val.data.toList = output.rootHash.toList := by + obtain ⟨output, tree, counter, equal⟩ := digest_tree input.data.toList + exact ⟨output, tree, counter, congrArg Vector.toList equal⟩ + +end Blake3.Pure diff --git a/Blake3Test.lean b/Blake3Test.lean index 9a58ed0..4fa5f93 100644 --- a/Blake3Test.lean +++ b/Blake3Test.lean @@ -1,5 +1,6 @@ import Blake3.C import Blake3.Rust +import Tests.Pure open Blake3 @@ -77,4 +78,6 @@ def main (args : List String) : IO UInt32 := do let mut ok := true if runC then ok := (← runTests Blake3.C.Hasher) && ok if runRust then ok := (← runTests Blake3.Rust.Hasher) && ok + if args.isEmpty || args.contains "pure" || runC || runRust then + Blake3.PureTests.run runC runRust return if ok then 0 else 1 diff --git a/README.md b/README.md index ebf98ce..1f6dbcf 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # Blake3.lean -Lean bindings to the [BLAKE3 hasher](https://github.com/BLAKE3-team/BLAKE3) for the C and Rust implementations. +The [BLAKE3 hash function](https://github.com/BLAKE3-team/BLAKE3) in Lean: +C and Rust bindings, plus a total pure Lean implementation with checked proofs. ## Usage @@ -21,6 +22,47 @@ def main : IO Unit := do IO.println s!"BLAKE3: {hash.val.toList}" ``` +### Pure Lean hashing + +```lean +import Blake3.Pure + +def helloHash : Blake3.Blake3Hash := + Blake3.Pure.hash "Hello".toUTF8 +``` + +`Blake3.Pure.hash` computes an unkeyed 32-byte digest entirely in Lean. Its +definitions are exposed for kernel reduction and proof. It imports neither +FFI backend and has no dependencies beyond this package and Lean's standard +library. Import `Blake3.Pure.Proofs` for byte/word round trips, rotation and +message-schedule properties, exact block framing, canonical tree correctness +and uniqueness, and chunk-counter bounds for inputs shorter than 2^64 bytes. + +The pure API currently supports one-shot unkeyed hashing. The C and Rust +backends provide the `HasherOps` interface, including streaming, keyed hashing, +key derivation and variable-length output. The pure implementation prioritizes +explicit checked computation; no performance parity with the native backends +is claimed. The proofs establish the stated algorithmic properties. Collision +resistance and universal refinement of C or Rust are separate obligations. + +`lake test` runs the existing backend tests, two standard known answers, +258 pure/native comparisons at block and tree boundaries, 58 subtree +compositions, 42 native chunk vectors including large counters, and 64 +internal-parent/digest-pair vectors. It also audits the exact axiom sets of +50 proof roots by traversing checked types, bodies and inductive constructors. +These roots use only `propext`, `Classical.choice` and `Quot.sound`, with no +FFI, opaque BLAKE3 implementation or native-decision axiom in their dependency +closure. The audit checks three generated recursion workers against their +safe source definitions; Lean/Std runtime primitives remain an execution +boundary. + +Regenerate the component vectors from the pinned Rust dependency with: + +```sh +cd rust +cargo run --locked --release --example pure_vectors > ../Tests/PureVectors.lean +``` + ### Rust backend ```lean diff --git a/Tests/Pure.lean b/Tests/Pure.lean new file mode 100644 index 0000000..ceb19fc --- /dev/null +++ b/Tests/Pure.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Argument Computer Corporation. +SPDX-License-Identifier: MIT OR Apache-2.0 +-/ + +import Blake3.Pure.Proofs +import Blake3.C +import Blake3.Rust +import Tests.PureAudit +import Tests.PureVectors + +namespace Blake3.PureTests + +private def testInput (length salt : Nat) : ByteArray := + ⟨Array.ofFn fun index : Fin length => ((index.val * 17 + index.val / 251 * 13 + salt * 29) % 256).toUInt8⟩ + +private def lengths : List Nat := + ((List.range 129) ++ (List.range 65).map (960 + ·) ++ [255, 256, 257, 511, 512, 513] ++ + (((List.range 17).map (· + 1) ++ [32, 64, 128]).flatMap fun chunks => + [chunks * 1024 - 1, chunks * 1024, chunks * 1024 + 1])).eraseDups + +private def knownAnswer (input : ByteArray) (expected : List UInt8) : IO Unit := do + unless (Pure.hash input).val.data.toList == expected do + throw (IO.userError "pure Blake3 known-answer test failed") + +def run (compareC compareRust : Bool) : IO Unit := do + -- First 32 output bytes from the BLAKE3 team's standard unkeyed vectors. + knownAnswer ByteArray.empty [ + 0xaf, 0x13, 0x49, 0xb9, 0xf5, 0xf9, 0xa1, 0xa6, + 0xa0, 0x40, 0x4d, 0xea, 0x36, 0xdc, 0xc9, 0x49, + 0x9b, 0xcb, 0x25, 0xc9, 0xad, 0xc1, 0x12, 0xb7, + 0xcc, 0x9a, 0x93, 0xca, 0xe4, 0x1f, 0x32, 0x62] + knownAnswer ⟨#[0]⟩ [ + 0x2d, 0x3a, 0xde, 0xdf, 0xf1, 0x1b, 0x61, 0xf1, + 0x4c, 0x88, 0x6e, 0x35, 0xaf, 0xa0, 0x36, 0x73, + 0x6d, 0xcd, 0x87, 0xa7, 0x4d, 0x27, 0xb5, 0xc1, + 0x51, 0x02, 0x25, 0xd0, 0xf5, 0x92, 0xe2, 0x13] + unless lengths.length == 258 do throw (IO.userError "incomplete pure Blake3 boundary cases") + let mut trees := 0 + for (length, salt) in lengths.zipIdx do + let input := testInput length salt + let actual := (Pure.hash input).val + if compareC then + unless actual == (C.hash input).val do throw (IO.userError s!"pure/C Blake3 differs at {length} bytes") + if compareRust then + unless actual == (Rust.hash input).val do throw (IO.userError s!"pure/Rust Blake3 differs at {length} bytes") + if length > 1024 then + trees := trees + 1 + let split := Pure.leftLen length + let left := Pure.subtree 0 (input.data.toList.take split) + let right := Pure.subtree (split / 1024) (input.data.toList.drop split) + let parent := Pure.parentOutput left.chainingValue right.chainingValue + unless parent.rootHash.toList == actual.data.toList do throw (IO.userError "pure Blake3 subtree composition differs") + unless trees == 58 do throw (IO.userError "incomplete pure Blake3 tree cases") + unless chunkVectors.length == 42 && parentVectors.length == 64 do + throw (IO.userError "incomplete native component vectors") + for (counter, length, expected) in chunkVectors do + let input := testInput length (counter % 251) + let actual := Pure.cvBytes (Pure.chunkOutput counter.toUInt64 input.data.toList).chainingValue + unless actual.toList == expected do throw (IO.userError s!"pure Blake3 chunk differs at {counter}, {length}") + for ((expectedCV, expectedRoot, expectedOrdinary), salt) in parentVectors.zipIdx do + let left := testInput 32 salt + let right := testInput 32 (salt + 83) + let cv := fun bytes : ByteArray => Vector.ofFn fun word : Fin 8 => + Pure.bytesWord (Vector.ofFn fun byte : Fin 4 => bytes[word.val * 4 + byte.val]!) + let parent := Pure.parentOutput (cv left) (cv right) + unless (Pure.cvBytes parent.chainingValue).toList == expectedCV && parent.rootHash.toList == expectedRoot do + throw (IO.userError "pure Blake3 internal parent differs") + unless (Pure.hash (left ++ right)).val.data.toList == expectedOrdinary do + throw (IO.userError "pure Blake3 digest-pair hash differs") + IO.println s!"Pure Blake3: 2 known answers, 258 inputs, 58 splits, 42 chunks and 64 parents passed (C={compareC}, Rust={compareRust})" + +end Blake3.PureTests diff --git a/Tests/PureAudit.lean b/Tests/PureAudit.lean new file mode 100644 index 0000000..2643459 --- /dev/null +++ b/Tests/PureAudit.lean @@ -0,0 +1,160 @@ +/- +Copyright (c) 2026 Argument Computer Corporation. +SPDX-License-Identifier: MIT OR Apache-2.0 +-/ + +import Lean +import Blake3.Pure.Proofs + +open Lean Lean.Elab Command + +namespace Blake3.PureAudit + +private def roots : Array (Name × Array Name) := #[ + (`Blake3.Pure.leftLen_positive, #[]), + (`Blake3.Pure.leftLen_lt, #[``propext, ``Quot.sound]), + (`Blake3.Pure.encodeLittleEndian_length, #[``propext]), + (`Blake3.Pure.littleEndian_bound, #[``propext, ``Quot.sound]), + (`Blake3.Pure.littleEndian_encode, #[``propext]), + (`Blake3.Pure.schedules_permute, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.schedules_next, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.rotateRight_bits, #[``propext, ``Quot.sound]), + (`Blake3.Pure.bytesWord_value, #[``propext, ``Quot.sound]), + (`Blake3.Pure.wordBytes_encoding, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.bytesWord_wordBytes, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.bytesWord_pack, #[``propext, ``Quot.sound]), + (`Blake3.Pure.wordBytes_pack, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.wordBytes_bytesWord, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.bytesWord_injective, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.blockWords_byte, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.blockWords_value, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.cvBytes_value, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.g_unchanged, #[``propext, ``Quot.sound]), + (`Blake3.Pure.g_values, #[``propext, ``Quot.sound]), + (`Blake3.Pure.initialWords_counter, #[``propext, ``Quot.sound]), + (`Blake3.Pure.parentOutput_values, #[``propext, ``Quot.sound]), + (`Blake3.Pure.leftLen_bounds, #[``propext, ``Quot.sound]), + (`Blake3.Pure.leftLen_chunks, #[``propext, ``Quot.sound]), + (`Blake3.Pure.leftLen_chunk_multiple, #[``propext, ``Quot.sound]), + (`Blake3.Pure.leftLen_unique, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkLoop_small, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkLoop_step, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkLoop_counter, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkOutput_counter, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkLoop_reads, #[``propext, ``Quot.sound]), + (`Blake3.Pure.ChunkReads.complete, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkLoop_iff, #[``propext, ``Quot.sound]), + (`Blake3.Pure.ChunkReads.framing, #[``propext, ``Quot.sound]), + (`Blake3.Pure.chunkOutput_framing, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.subtree_small, #[``propext, ``Quot.sound]), + (`Blake3.Pure.subtree_step, #[``propext, ``Quot.sound]), + (`Blake3.Pure.subtree_root_counter, #[``propext, ``Quot.sound]), + (`Blake3.Pure.subtree_tree, #[``propext, ``Quot.sound]), + (`Blake3.Pure.TreeHash.complete, #[``propext, ``Quot.sound]), + (`Blake3.Pure.subtree_iff, #[``propext, ``Quot.sound]), + (`Blake3.Pure.TreeHash.unique, #[``propext, ``Quot.sound]), + (`Blake3.Pure.native_counter, #[``propext, ``Quot.sound]), + (`Blake3.Pure.native_child_spans, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.ChunkAt.native, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.digest_native_counters, #[``propext, ``Classical.choice, ``Quot.sound]), + (`Blake3.Pure.digest_tree, #[``propext, ``Quot.sound]), + (`Blake3.Pure.hash_size, #[``propext, ``Quot.sound]), + (`Blake3.Pure.hash_digest, #[``propext, ``Quot.sound]), + (`Blake3.Pure.hash_tree, #[``propext, ``Quot.sound])] + +private def constants (info : Lean.ConstantInfo) : Array Lean.Name := + info.type.getUsedConstants ++ match info with + | .thmInfo value => value.value.getUsedConstants + | .defnInfo value => value.value.getUsedConstants + | .opaqueInfo value => value.value.getUsedConstants + | .inductInfo value => value.ctors.toArray + | _ => #[] + +private partial def closure (env : Lean.Environment) (runtime : Bool) (pending : List Lean.Name) + (seen : NameSet := {}) : NameSet := + match pending with + | [] => seen + | name :: rest => + if seen.contains name then closure env runtime rest seen + else match env.checked.get.find? name with + | none => closure env runtime rest (seen.insert name) + | some info => + let extras := if runtime then Id.run do + let mut names := #[] + let worker := Lean.Compiler.mkUnsafeRecName name + if (env.checked.get.find? worker).isSome then names := names.push worker + if let some other := Lean.Compiler.getImplementedBy? env name then + names := names.push other + if let some other := (Lean.Compiler.CSimp.ext.getState env).map.find? name then + names := names.push other.toDeclName + return names + else #[] + closure env runtime ((constants info ++ extras).toList ++ rest) (seen.insert name) + +private def projectConstant (env : Lean.Environment) (name : Lean.Name) : Bool := + match env.getModuleIdxFor? name with + | none => false + | some idx => (`Blake3).isPrefixOf env.allImportedModuleNames[idx.toNat]! + +private def sortedNames (names : Array Name) : Array Name := names.qsort Name.lt + +/-- Read checked types, bodies and constructors; imported cached axiom +summaries can omit constructor dependencies. -/ +private def checkAxioms (env : Environment) (root : Name) (expected : Array Name) : + CommandElabM (Array Name) := do + let reachable := closure env false [root] + let mut actual := #[] + for name in reachable do + let some info := env.checked.get.find? name + | throwError "BLAKE3 audit: unavailable checked dependency: {name}" + if info.isAxiom then actual := actual.push name + let sorted := sortedNames actual + unless sorted == sortedNames expected do + throwError "BLAKE3 axiom boundary changed for {root}: expected {sortedNames expected}, actual {sorted}" + return sorted + +-- Constructor closure and exact-set failure paths are part of the audit. +private inductive ConstructorAuditFixture where + | plain + | withProof (proof : propext (Iff.refl True) = rfl) + +run_cmd do + let _ ← checkAxioms (← getEnv) ``ConstructorAuditFixture.plain #[``propext] + let _ ← checkAxioms (← getEnv) ``Eq.refl #[] + +/-- error: BLAKE3 axiom boundary changed for Eq.refl: expected [propext], actual [] -/ +#guard_msgs in +run_cmd do + let _ ← checkAxioms (← getEnv) ``Eq.refl #[``propext] + +/-- error: BLAKE3 axiom boundary changed for propext: expected [], actual [propext] -/ +#guard_msgs in +run_cmd do + let _ ← checkAxioms (← getEnv) ``propext #[] + +run_cmd do + let env ← getEnv + for (root, expected) in roots do + let _ ← checkAxioms env root expected + let mut workers := #[] + for name in closure env true (roots.toList.map Prod.fst) do + let some info := env.checked.get.find? name | throwError "Unavailable runtime dependency: {name}" + if projectConstant env name then + if Lean.isExtern env name then throwError "Unexpected BLAKE3 FFI dependency: {name}" + if (Lean.Compiler.getImplementedBy? env name).isSome || + ((Lean.Compiler.CSimp.ext.getState env).map.find? name).isSome then + throwError "Unexpected BLAKE3 implementation replacement: {name}" + if let some parent := Lean.Compiler.isUnsafeRecName? name then + let some (.defnInfo source) := env.checked.get.find? parent | throwError "Missing recursion source: {name}" + unless source.safety == .safe do throwError "Unsafe recursion source: {parent}" + workers := workers.push name + else match info with + | .defnInfo value => unless value.safety == .safe do throwError "Unsafe BLAKE3 definition: {name}" + | .opaqueInfo _ => throwError "Opaque BLAKE3 implementation: {name}" + | _ => pure () + unless workers.qsort Name.lt == #[`Blake3.Pure.chunkLoop._unsafe_rec, + `Blake3.Pure.encodeLittleEndian._unsafe_rec, `Blake3.Pure.subtree._unsafe_rec] do + throwError "BLAKE3 recursion inventory changed: {workers}" + logInfo "Pure BLAKE3 audit: 50 exact axiom sets, 3 safe recursion sources, no BLAKE3 FFI or opaque implementations" + +end Blake3.PureAudit diff --git a/Tests/PureVectors.lean b/Tests/PureVectors.lean new file mode 100644 index 0000000..7975073 --- /dev/null +++ b/Tests/PureVectors.lean @@ -0,0 +1,114 @@ +/- Generated by rust/examples/pure_vectors.rs using BLAKE3 1.8.7. -/ +namespace Blake3.PureTests + +def chunkVectors : List (Nat × Nat × List UInt8) := [ + (0, 1, [13, 241, 167, 136, 29, 113, 210, 135, 208, 175, 194, 252, 215, 210, 61, 40, 241, 46, 64, 26, 184, 88, 202, 38, 127, 17, 197, 241, 113, 13, 243, 21]), + (0, 63, [124, 122, 4, 126, 78, 9, 90, 75, 72, 194, 149, 16, 99, 175, 53, 135, 125, 189, 61, 97, 82, 123, 66, 130, 178, 99, 193, 107, 176, 149, 118, 130]), + (0, 64, [31, 147, 133, 199, 42, 181, 73, 178, 14, 102, 138, 242, 173, 120, 201, 120, 156, 1, 17, 33, 232, 55, 210, 132, 20, 212, 28, 113, 167, 54, 176, 52]), + (0, 65, [121, 229, 202, 199, 36, 142, 37, 200, 116, 173, 184, 246, 79, 94, 118, 182, 105, 46, 212, 129, 246, 197, 54, 146, 4, 167, 155, 2, 215, 197, 48, 255]), + (0, 1023, [213, 123, 249, 134, 24, 2, 103, 214, 2, 203, 200, 239, 124, 4, 149, 253, 21, 32, 195, 112, 13, 139, 208, 149, 47, 106, 109, 137, 42, 46, 61, 38]), + (0, 1024, [112, 206, 128, 171, 170, 231, 196, 29, 215, 181, 127, 83, 162, 42, 116, 117, 121, 82, 135, 33, 217, 198, 119, 227, 90, 199, 145, 87, 206, 196, 20, 127]), + (1, 1, [67, 221, 33, 31, 197, 45, 139, 27, 83, 105, 16, 43, 31, 158, 113, 32, 250, 212, 179, 84, 132, 131, 132, 210, 238, 121, 140, 218, 255, 102, 105, 189]), + (1, 63, [149, 251, 28, 255, 217, 210, 100, 68, 216, 225, 151, 28, 192, 104, 245, 57, 27, 97, 143, 109, 78, 76, 195, 71, 243, 43, 5, 16, 44, 27, 198, 142]), + (1, 64, [54, 177, 124, 34, 205, 114, 130, 187, 67, 182, 87, 90, 212, 180, 242, 206, 18, 201, 35, 60, 146, 29, 184, 81, 251, 238, 215, 158, 22, 148, 121, 103]), + (1, 65, [213, 17, 166, 171, 57, 234, 23, 176, 17, 54, 215, 82, 75, 80, 19, 96, 154, 202, 205, 219, 12, 212, 185, 141, 63, 43, 69, 50, 9, 223, 246, 167]), + (1, 1023, [221, 180, 243, 233, 51, 62, 8, 151, 72, 208, 151, 220, 196, 85, 248, 42, 56, 119, 204, 41, 47, 155, 3, 52, 65, 239, 106, 50, 192, 199, 137, 140]), + (1, 1024, [243, 82, 196, 190, 7, 100, 234, 6, 10, 68, 157, 57, 83, 136, 250, 177, 125, 7, 177, 221, 205, 166, 23, 13, 65, 70, 51, 225, 255, 174, 14, 249]), + (2, 1, [61, 150, 210, 68, 247, 92, 86, 216, 227, 194, 11, 40, 108, 0, 17, 173, 227, 25, 206, 15, 10, 125, 103, 235, 99, 59, 139, 205, 84, 184, 41, 255]), + (2, 63, [28, 132, 249, 139, 156, 144, 237, 39, 110, 61, 178, 92, 98, 97, 5, 124, 83, 146, 178, 230, 163, 148, 88, 61, 201, 129, 204, 39, 226, 222, 142, 242]), + (2, 64, [109, 200, 127, 28, 230, 178, 211, 66, 200, 246, 132, 208, 40, 171, 64, 209, 146, 81, 173, 139, 29, 143, 22, 221, 168, 28, 172, 210, 184, 50, 120, 91]), + (2, 65, [74, 193, 127, 6, 32, 207, 177, 112, 238, 26, 14, 109, 177, 199, 156, 119, 86, 190, 14, 213, 165, 98, 39, 248, 11, 56, 2, 204, 19, 14, 14, 161]), + (2, 1023, [7, 208, 158, 235, 209, 225, 225, 66, 246, 235, 206, 25, 33, 216, 210, 69, 56, 81, 210, 136, 73, 184, 28, 144, 134, 36, 212, 138, 15, 23, 161, 162]), + (2, 1024, [69, 130, 50, 166, 164, 41, 151, 116, 13, 199, 224, 104, 12, 192, 62, 177, 199, 6, 135, 241, 55, 91, 200, 178, 171, 196, 208, 93, 27, 23, 120, 24]), + (255, 1, [62, 182, 108, 102, 133, 226, 50, 15, 0, 31, 194, 97, 20, 192, 18, 123, 149, 66, 105, 62, 120, 172, 192, 251, 250, 250, 170, 83, 104, 104, 16, 140]), + (255, 63, [110, 117, 147, 47, 69, 24, 108, 25, 104, 20, 8, 46, 241, 198, 104, 177, 29, 195, 227, 190, 89, 137, 205, 153, 180, 127, 167, 190, 78, 205, 124, 214]), + (255, 64, [223, 215, 76, 230, 242, 215, 238, 85, 51, 228, 83, 117, 220, 56, 19, 55, 125, 16, 82, 105, 93, 195, 40, 96, 21, 179, 129, 102, 161, 59, 39, 133]), + (255, 65, [20, 173, 14, 113, 212, 89, 235, 16, 129, 98, 81, 83, 63, 246, 55, 195, 191, 37, 251, 234, 74, 51, 1, 167, 43, 183, 34, 139, 111, 55, 238, 20]), + (255, 1023, [2, 119, 251, 63, 222, 182, 130, 105, 162, 64, 54, 97, 31, 228, 138, 215, 146, 87, 107, 223, 253, 120, 60, 32, 243, 85, 29, 195, 241, 162, 40, 236]), + (255, 1024, [19, 46, 53, 175, 147, 230, 14, 121, 90, 170, 72, 68, 214, 45, 43, 37, 48, 1, 5, 101, 53, 238, 108, 170, 3, 197, 119, 205, 132, 219, 184, 139]), + (4294967295, 1, [56, 83, 7, 164, 241, 213, 58, 174, 6, 144, 97, 99, 226, 239, 170, 130, 124, 241, 142, 54, 75, 1, 127, 159, 213, 104, 229, 44, 133, 104, 121, 90]), + (4294967295, 63, [243, 21, 13, 211, 190, 57, 251, 229, 128, 107, 209, 98, 249, 43, 1, 255, 4, 110, 199, 114, 44, 157, 154, 56, 247, 178, 167, 7, 25, 63, 34, 87]), + (4294967295, 64, [54, 8, 165, 77, 235, 26, 131, 170, 146, 124, 80, 189, 27, 120, 215, 119, 217, 86, 101, 60, 15, 100, 113, 220, 183, 210, 174, 70, 28, 28, 97, 121]), + (4294967295, 65, [127, 132, 168, 234, 163, 32, 231, 3, 20, 60, 2, 144, 180, 255, 222, 62, 199, 162, 209, 103, 163, 137, 252, 208, 43, 49, 11, 195, 94, 114, 44, 63]), + (4294967295, 1023, [53, 238, 165, 239, 73, 107, 185, 129, 75, 65, 87, 62, 73, 102, 229, 137, 6, 223, 142, 138, 32, 96, 38, 81, 78, 139, 112, 147, 100, 200, 38, 252]), + (4294967295, 1024, [111, 128, 112, 124, 200, 172, 70, 160, 154, 70, 245, 114, 233, 230, 202, 226, 249, 8, 41, 96, 27, 146, 35, 18, 106, 38, 253, 19, 168, 182, 145, 129]), + (4294967296, 1, [174, 117, 32, 84, 47, 154, 23, 29, 230, 227, 210, 29, 37, 0, 76, 232, 149, 77, 32, 234, 226, 72, 77, 93, 65, 42, 45, 225, 102, 209, 123, 142]), + (4294967296, 63, [84, 240, 16, 108, 78, 126, 85, 30, 168, 31, 22, 239, 16, 140, 159, 123, 90, 244, 110, 7, 6, 38, 61, 224, 97, 76, 250, 194, 99, 163, 205, 44]), + (4294967296, 64, [202, 131, 113, 175, 159, 193, 210, 191, 156, 120, 206, 77, 183, 251, 225, 10, 227, 17, 121, 60, 114, 205, 19, 143, 178, 120, 55, 83, 240, 47, 178, 108]), + (4294967296, 65, [240, 91, 163, 80, 83, 213, 102, 206, 11, 94, 238, 99, 64, 209, 55, 13, 253, 92, 92, 11, 124, 54, 90, 55, 8, 229, 173, 197, 137, 103, 186, 170]), + (4294967296, 1023, [53, 93, 188, 131, 120, 54, 213, 74, 164, 76, 58, 247, 234, 30, 200, 78, 175, 32, 172, 246, 224, 9, 83, 68, 244, 31, 7, 67, 247, 17, 114, 150]), + (4294967296, 1024, [225, 170, 71, 199, 103, 170, 44, 110, 180, 240, 57, 57, 20, 67, 15, 110, 185, 227, 82, 166, 247, 131, 217, 179, 178, 231, 135, 36, 155, 37, 210, 84]), + (18014398509481983, 1, [121, 145, 221, 95, 240, 247, 137, 175, 15, 63, 175, 243, 241, 154, 114, 229, 73, 54, 165, 24, 158, 25, 120, 5, 203, 138, 125, 18, 30, 44, 147, 118]), + (18014398509481983, 63, [120, 100, 48, 141, 72, 255, 192, 166, 100, 125, 80, 239, 218, 118, 232, 133, 181, 191, 135, 131, 143, 13, 169, 100, 241, 52, 234, 201, 130, 226, 81, 20]), + (18014398509481983, 64, [13, 186, 25, 87, 101, 59, 40, 55, 141, 74, 225, 25, 33, 148, 30, 146, 11, 107, 88, 165, 68, 188, 218, 190, 50, 12, 183, 189, 230, 54, 171, 59]), + (18014398509481983, 65, [20, 52, 91, 192, 249, 204, 13, 156, 105, 174, 56, 90, 206, 137, 18, 128, 151, 71, 68, 203, 5, 118, 98, 155, 21, 74, 21, 95, 118, 164, 13, 173]), + (18014398509481983, 1023, [219, 239, 75, 169, 67, 20, 50, 75, 75, 115, 96, 55, 183, 22, 183, 234, 57, 198, 45, 93, 219, 12, 90, 84, 215, 72, 93, 96, 199, 75, 163, 188]), + (18014398509481983, 1024, [237, 157, 154, 128, 246, 72, 81, 81, 137, 65, 39, 160, 1, 118, 173, 225, 80, 241, 79, 20, 60, 25, 117, 248, 36, 249, 166, 186, 81, 253, 130, 159])] + +def parentVectors : List (List UInt8 × List UInt8 × List UInt8) := [ + ([156, 70, 127, 251, 125, 94, 185, 157, 129, 32, 72, 205, 5, 182, 245, 135, 72, 142, 116, 25, 7, 8, 86, 120, 218, 237, 172, 164, 241, 144, 255, 179], [136, 142, 105, 104, 77, 32, 135, 115, 76, 76, 20, 191, 208, 229, 126, 244, 229, 168, 37, 174, 101, 62, 62, 50, 14, 154, 221, 218, 215, 151, 108, 147], [191, 194, 194, 226, 169, 140, 29, 68, 162, 205, 105, 249, 58, 164, 41, 189, 178, 153, 145, 33, 234, 46, 161, 207, 78, 196, 35, 21, 83, 181, 114, 44]), + ([85, 199, 73, 119, 254, 194, 44, 173, 206, 116, 189, 89, 71, 178, 75, 244, 49, 176, 211, 21, 69, 88, 1, 222, 195, 64, 210, 35, 77, 58, 67, 206], [52, 236, 141, 88, 223, 11, 168, 175, 86, 169, 147, 150, 4, 253, 10, 204, 194, 226, 8, 82, 63, 102, 210, 247, 45, 174, 57, 79, 179, 56, 208, 97], [69, 37, 73, 166, 188, 74, 142, 86, 109, 115, 198, 123, 170, 73, 4, 121, 32, 142, 190, 45, 102, 233, 93, 233, 154, 158, 50, 83, 28, 133, 42, 85]), + ([225, 154, 194, 235, 123, 234, 134, 121, 221, 29, 85, 76, 85, 230, 197, 174, 32, 126, 170, 235, 169, 194, 102, 237, 54, 181, 188, 118, 163, 137, 10, 227], [54, 231, 177, 182, 89, 39, 48, 211, 12, 66, 191, 43, 99, 197, 121, 12, 190, 17, 166, 168, 129, 37, 202, 192, 231, 28, 151, 151, 1, 82, 148, 25], [88, 104, 8, 221, 221, 77, 212, 153, 113, 25, 230, 2, 51, 227, 210, 20, 154, 201, 247, 90, 160, 226, 77, 15, 153, 155, 207, 20, 58, 253, 227, 218]), + ([165, 109, 161, 68, 103, 205, 239, 42, 5, 245, 228, 61, 85, 52, 123, 250, 34, 83, 213, 17, 63, 134, 67, 148, 168, 165, 204, 35, 140, 158, 232, 223], [42, 139, 61, 80, 0, 117, 209, 91, 9, 109, 184, 224, 63, 142, 91, 134, 98, 203, 133, 98, 134, 162, 252, 197, 212, 70, 181, 107, 197, 123, 166, 152], [154, 254, 134, 214, 153, 241, 210, 10, 181, 171, 228, 186, 128, 114, 234, 61, 11, 9, 135, 162, 140, 196, 74, 12, 25, 175, 56, 111, 255, 90, 1, 80]), + ([163, 117, 68, 174, 252, 193, 177, 136, 49, 85, 49, 84, 117, 128, 111, 120, 1, 43, 188, 138, 154, 8, 194, 117, 28, 225, 80, 105, 241, 143, 4, 64], [79, 242, 39, 81, 154, 43, 61, 93, 129, 28, 246, 111, 24, 106, 218, 206, 123, 67, 40, 40, 97, 215, 233, 146, 121, 207, 242, 87, 149, 249, 211, 142], [31, 196, 13, 217, 125, 98, 20, 194, 93, 175, 206, 166, 65, 111, 87, 10, 71, 203, 171, 194, 20, 48, 127, 19, 14, 191, 75, 148, 20, 144, 247, 18]), + ([120, 59, 171, 131, 171, 12, 92, 77, 110, 17, 190, 250, 190, 125, 158, 196, 83, 197, 100, 148, 248, 226, 169, 14, 178, 0, 238, 135, 1, 97, 28, 248], [108, 42, 144, 23, 155, 199, 142, 194, 44, 180, 75, 70, 73, 29, 103, 99, 60, 64, 22, 157, 198, 88, 20, 147, 135, 56, 4, 214, 226, 196, 9, 189], [146, 198, 10, 144, 75, 230, 170, 143, 34, 79, 252, 20, 203, 130, 85, 26, 52, 198, 230, 184, 144, 123, 105, 208, 17, 231, 101, 215, 110, 78, 111, 87]), + ([60, 28, 174, 193, 77, 219, 18, 137, 54, 176, 181, 83, 162, 103, 4, 95, 136, 122, 225, 129, 62, 64, 76, 48, 113, 185, 245, 202, 255, 141, 21, 245], [227, 131, 158, 118, 221, 169, 156, 73, 181, 165, 236, 78, 111, 31, 30, 247, 123, 73, 73, 242, 95, 43, 251, 84, 98, 197, 119, 219, 1, 44, 160, 70], [47, 182, 170, 160, 160, 193, 34, 54, 76, 107, 79, 105, 212, 116, 27, 65, 183, 79, 177, 54, 120, 211, 199, 1, 145, 112, 34, 105, 188, 48, 147, 14]), + ([107, 211, 65, 87, 173, 227, 27, 14, 55, 230, 28, 135, 252, 57, 10, 225, 150, 103, 131, 163, 243, 193, 121, 163, 28, 181, 175, 128, 26, 120, 149, 11], [32, 133, 68, 145, 77, 218, 143, 140, 175, 51, 76, 13, 76, 113, 157, 234, 150, 25, 68, 123, 203, 67, 119, 122, 96, 49, 184, 25, 124, 77, 143, 218], [24, 118, 176, 78, 93, 8, 29, 180, 41, 206, 137, 158, 178, 20, 44, 66, 183, 42, 141, 62, 197, 46, 132, 177, 171, 186, 19, 39, 187, 237, 7, 111]), + ([115, 10, 106, 207, 79, 253, 160, 44, 125, 91, 0, 232, 91, 252, 166, 183, 158, 154, 3, 151, 243, 28, 245, 2, 156, 188, 201, 138, 197, 147, 244, 3], [244, 130, 148, 152, 227, 34, 148, 173, 210, 8, 46, 255, 62, 119, 147, 142, 239, 180, 138, 89, 66, 195, 124, 144, 69, 34, 255, 118, 1, 251, 174, 173], [34, 242, 49, 109, 176, 226, 189, 4, 128, 3, 126, 141, 102, 0, 97, 215, 120, 121, 52, 38, 195, 142, 186, 155, 107, 218, 18, 85, 47, 110, 29, 228]), + ([42, 189, 9, 120, 18, 164, 169, 55, 226, 46, 28, 142, 198, 228, 227, 28, 128, 175, 154, 33, 168, 49, 176, 172, 147, 57, 71, 2, 246, 47, 119, 186], [208, 128, 126, 7, 21, 155, 51, 14, 159, 59, 11, 5, 123, 253, 119, 234, 182, 141, 65, 49, 129, 133, 8, 97, 248, 221, 66, 231, 196, 96, 215, 126], [194, 49, 3, 173, 44, 253, 180, 226, 108, 223, 87, 65, 71, 227, 200, 175, 7, 24, 2, 136, 200, 33, 213, 111, 188, 3, 170, 156, 108, 126, 199, 189]), + ([134, 62, 12, 173, 102, 52, 69, 239, 89, 173, 148, 185, 24, 23, 217, 125, 87, 127, 196, 131, 31, 167, 123, 37, 16, 198, 84, 189, 53, 189, 29, 225], [93, 179, 118, 184, 163, 249, 55, 197, 117, 78, 243, 98, 86, 76, 128, 127, 52, 189, 4, 240, 90, 196, 15, 162, 158, 125, 207, 196, 49, 193, 113, 110], [1, 187, 37, 135, 77, 133, 224, 180, 247, 59, 183, 69, 13, 200, 83, 7, 188, 128, 222, 18, 44, 147, 138, 10, 234, 71, 247, 126, 146, 139, 61, 154]), + ([6, 10, 0, 36, 25, 16, 41, 106, 254, 222, 164, 170, 189, 165, 129, 233, 74, 238, 209, 92, 118, 11, 238, 179, 132, 70, 126, 102, 191, 211, 202, 215], [201, 180, 1, 205, 120, 151, 199, 245, 92, 9, 120, 152, 234, 96, 200, 7, 27, 216, 148, 201, 70, 43, 100, 43, 214, 252, 58, 225, 5, 97, 184, 195], [51, 155, 58, 213, 3, 188, 210, 221, 234, 141, 184, 107, 233, 175, 200, 96, 200, 4, 36, 186, 199, 219, 14, 60, 20, 184, 137, 89, 28, 65, 45, 173]), + ([25, 253, 15, 179, 15, 157, 57, 99, 140, 95, 181, 244, 113, 33, 3, 205, 78, 113, 87, 224, 103, 57, 76, 53, 130, 123, 51, 12, 146, 141, 234, 143], [217, 106, 226, 226, 139, 119, 145, 82, 190, 6, 112, 195, 157, 248, 149, 26, 138, 67, 118, 202, 136, 188, 135, 252, 34, 105, 243, 92, 96, 186, 170, 133], [150, 27, 232, 13, 172, 56, 135, 216, 88, 26, 115, 52, 97, 198, 77, 190, 7, 102, 126, 192, 15, 230, 222, 239, 243, 66, 183, 202, 244, 0, 116, 72]), + ([24, 184, 244, 191, 98, 238, 161, 60, 212, 77, 131, 107, 47, 142, 150, 231, 172, 232, 110, 73, 145, 34, 111, 26, 172, 131, 179, 99, 84, 183, 187, 21], [236, 236, 82, 100, 77, 175, 207, 222, 120, 136, 94, 32, 217, 183, 181, 238, 43, 133, 96, 4, 210, 236, 233, 241, 184, 48, 32, 214, 48, 244, 66, 234], [14, 142, 71, 26, 83, 212, 254, 132, 200, 143, 14, 126, 243, 125, 147, 245, 119, 160, 79, 216, 68, 162, 193, 122, 75, 24, 91, 22, 91, 228, 255, 244]), + ([182, 29, 251, 223, 14, 213, 49, 49, 77, 101, 181, 146, 240, 234, 90, 149, 73, 97, 171, 125, 52, 250, 200, 212, 78, 216, 245, 68, 88, 77, 142, 104], [194, 51, 243, 192, 8, 188, 81, 34, 47, 16, 242, 17, 191, 181, 113, 142, 112, 6, 171, 2, 27, 250, 7, 27, 203, 79, 144, 147, 41, 123, 195, 184], [108, 192, 138, 57, 61, 137, 73, 145, 103, 174, 231, 172, 177, 114, 188, 82, 203, 4, 16, 178, 139, 251, 112, 163, 240, 84, 52, 149, 113, 42, 252, 0]), + ([156, 0, 231, 76, 30, 159, 199, 94, 223, 2, 111, 46, 144, 54, 98, 102, 34, 237, 33, 178, 36, 86, 141, 194, 189, 248, 252, 251, 230, 201, 89, 124], [47, 235, 152, 1, 15, 146, 31, 150, 201, 93, 2, 58, 130, 82, 30, 235, 12, 145, 205, 90, 102, 111, 240, 249, 246, 49, 74, 239, 192, 212, 34, 57], [58, 2, 105, 151, 31, 133, 165, 136, 2, 174, 156, 254, 0, 146, 250, 74, 14, 190, 148, 81, 78, 99, 140, 66, 35, 71, 133, 244, 221, 196, 10, 93]), + ([70, 193, 40, 218, 223, 227, 140, 150, 32, 164, 13, 76, 125, 168, 175, 167, 178, 253, 189, 13, 86, 66, 203, 12, 104, 40, 104, 96, 223, 4, 136, 198], [239, 20, 139, 250, 1, 102, 209, 158, 61, 142, 151, 191, 190, 152, 15, 102, 117, 37, 175, 146, 207, 155, 197, 249, 251, 48, 137, 81, 6, 64, 31, 26], [198, 240, 187, 31, 170, 122, 230, 103, 177, 207, 191, 18, 26, 133, 149, 196, 24, 238, 76, 184, 205, 193, 167, 205, 151, 142, 145, 211, 81, 78, 5, 158]), + ([164, 233, 117, 8, 7, 196, 138, 200, 134, 92, 161, 211, 201, 141, 206, 208, 211, 0, 103, 64, 123, 221, 86, 145, 125, 233, 207, 193, 192, 58, 132, 31], [11, 170, 117, 102, 11, 73, 109, 207, 137, 120, 222, 252, 41, 132, 253, 193, 142, 103, 104, 180, 111, 56, 22, 68, 27, 89, 155, 67, 128, 189, 104, 23], [188, 236, 186, 160, 156, 34, 7, 49, 161, 220, 33, 32, 101, 208, 168, 8, 156, 36, 214, 58, 74, 102, 205, 165, 212, 73, 122, 47, 95, 16, 212, 18]), + ([11, 49, 186, 130, 169, 13, 61, 1, 168, 214, 201, 230, 91, 31, 60, 76, 164, 7, 101, 144, 108, 179, 212, 79, 215, 241, 153, 34, 58, 47, 70, 94], [186, 212, 202, 149, 230, 113, 134, 218, 65, 110, 175, 254, 73, 79, 246, 238, 184, 228, 53, 21, 201, 111, 194, 213, 250, 243, 18, 250, 65, 57, 57, 23], [216, 95, 249, 98, 201, 23, 188, 146, 166, 183, 71, 150, 55, 126, 197, 108, 254, 92, 105, 106, 139, 13, 166, 89, 116, 19, 217, 186, 166, 228, 97, 100]), + ([1, 51, 217, 181, 27, 162, 152, 22, 0, 171, 37, 92, 171, 127, 173, 211, 252, 102, 86, 110, 38, 6, 58, 35, 132, 149, 35, 40, 97, 112, 128, 66], [6, 214, 84, 108, 177, 115, 84, 41, 221, 178, 36, 93, 105, 210, 13, 191, 95, 238, 226, 211, 168, 23, 222, 210, 57, 87, 204, 236, 137, 203, 78, 70], [233, 28, 77, 91, 129, 125, 134, 142, 240, 201, 226, 238, 122, 98, 3, 237, 181, 188, 35, 115, 205, 215, 105, 184, 198, 84, 132, 12, 145, 107, 22, 32]), + ([48, 101, 149, 177, 160, 20, 207, 44, 240, 52, 144, 251, 42, 77, 59, 187, 152, 171, 249, 205, 104, 94, 161, 187, 191, 54, 164, 71, 125, 213, 108, 91], [203, 224, 200, 252, 130, 250, 9, 230, 105, 199, 27, 249, 198, 249, 17, 67, 99, 3, 144, 74, 170, 38, 26, 58, 134, 90, 195, 121, 46, 57, 31, 63], [241, 172, 251, 158, 60, 67, 54, 246, 213, 40, 170, 48, 131, 168, 112, 205, 153, 123, 204, 120, 182, 104, 235, 152, 38, 124, 35, 160, 58, 85, 127, 149]), + ([127, 203, 214, 209, 86, 3, 143, 109, 221, 220, 240, 175, 15, 123, 43, 174, 114, 212, 61, 144, 114, 14, 238, 12, 44, 87, 229, 32, 62, 48, 238, 244], [212, 1, 167, 28, 181, 83, 121, 219, 73, 226, 137, 58, 156, 166, 219, 53, 223, 182, 139, 0, 65, 142, 32, 190, 128, 172, 130, 107, 108, 123, 127, 66], [30, 113, 179, 96, 250, 4, 175, 75, 88, 116, 115, 205, 85, 29, 36, 97, 97, 206, 13, 84, 219, 226, 215, 245, 82, 71, 100, 28, 109, 153, 166, 41]), + ([155, 236, 19, 62, 208, 10, 60, 137, 215, 47, 116, 161, 233, 247, 239, 201, 108, 220, 235, 89, 145, 72, 255, 229, 33, 153, 178, 237, 146, 62, 174, 52], [46, 181, 9, 136, 93, 236, 182, 207, 139, 189, 48, 186, 117, 149, 147, 88, 165, 195, 86, 107, 105, 254, 159, 245, 232, 148, 9, 97, 186, 191, 166, 37], [158, 52, 153, 121, 175, 201, 99, 223, 241, 178, 172, 60, 224, 122, 222, 87, 31, 25, 131, 139, 209, 135, 78, 42, 237, 12, 101, 118, 185, 87, 139, 100]), + ([167, 188, 96, 103, 143, 26, 218, 92, 255, 163, 221, 60, 107, 227, 170, 58, 125, 228, 75, 25, 172, 67, 100, 225, 157, 171, 169, 156, 159, 148, 92, 175], [5, 133, 176, 95, 96, 150, 94, 52, 131, 199, 191, 101, 159, 113, 194, 76, 107, 102, 119, 55, 0, 55, 2, 153, 9, 157, 24, 202, 249, 151, 85, 142], [127, 109, 8, 66, 241, 196, 0, 23, 231, 154, 201, 68, 211, 246, 76, 71, 153, 149, 79, 26, 208, 7, 79, 146, 104, 35, 129, 65, 245, 17, 74, 249]), + ([207, 201, 114, 76, 252, 125, 175, 152, 176, 182, 165, 212, 56, 63, 49, 174, 44, 186, 251, 78, 123, 255, 152, 42, 191, 153, 36, 135, 132, 2, 102, 109], [24, 64, 15, 193, 87, 214, 204, 192, 52, 127, 102, 19, 154, 168, 114, 62, 100, 140, 144, 201, 142, 139, 189, 78, 110, 223, 8, 55, 30, 185, 134, 238], [100, 155, 22, 23, 183, 228, 122, 206, 160, 82, 87, 105, 166, 195, 92, 145, 184, 46, 17, 5, 184, 3, 237, 254, 234, 103, 46, 135, 104, 95, 68, 208]), + ([225, 127, 99, 112, 148, 153, 93, 182, 124, 139, 183, 95, 44, 162, 254, 94, 1, 169, 38, 6, 151, 215, 81, 246, 191, 188, 50, 73, 168, 4, 109, 1], [128, 246, 225, 64, 13, 76, 122, 91, 93, 1, 69, 16, 114, 193, 88, 203, 31, 131, 36, 197, 93, 26, 160, 3, 168, 198, 126, 172, 137, 121, 91, 134], [212, 245, 228, 72, 207, 238, 118, 238, 87, 178, 159, 25, 47, 163, 183, 181, 230, 100, 192, 31, 234, 83, 52, 173, 47, 172, 230, 55, 11, 167, 84, 12]), + ([247, 78, 93, 39, 56, 67, 4, 81, 213, 192, 22, 183, 6, 88, 231, 24, 128, 80, 239, 240, 96, 149, 231, 108, 48, 9, 211, 111, 41, 40, 43, 163], [169, 161, 187, 134, 250, 82, 137, 40, 179, 4, 137, 233, 197, 132, 81, 216, 6, 152, 69, 207, 216, 53, 10, 179, 1, 36, 99, 104, 121, 222, 179, 207], [13, 175, 3, 222, 125, 95, 136, 172, 250, 7, 126, 238, 198, 254, 223, 189, 163, 222, 55, 63, 154, 159, 73, 231, 73, 119, 232, 68, 190, 200, 86, 134]), + ([38, 93, 146, 213, 173, 240, 29, 255, 187, 247, 58, 47, 227, 138, 165, 239, 56, 27, 221, 160, 108, 130, 67, 115, 118, 69, 247, 102, 69, 135, 49, 94], [120, 67, 170, 92, 144, 11, 148, 72, 175, 109, 193, 111, 98, 214, 247, 250, 35, 126, 186, 126, 135, 55, 80, 110, 4, 239, 0, 37, 214, 247, 189, 24], [33, 123, 43, 104, 78, 67, 131, 212, 179, 160, 37, 120, 123, 65, 56, 230, 160, 194, 193, 183, 101, 190, 90, 139, 33, 173, 239, 250, 216, 70, 233, 171]), + ([61, 165, 226, 160, 202, 223, 135, 82, 150, 162, 143, 16, 78, 42, 214, 187, 213, 8, 124, 170, 126, 115, 210, 120, 174, 219, 251, 26, 241, 4, 83, 13], [148, 249, 248, 155, 198, 141, 186, 3, 149, 18, 237, 166, 4, 71, 158, 111, 189, 62, 73, 231, 205, 217, 43, 246, 56, 45, 41, 218, 236, 0, 169, 251], [73, 22, 88, 119, 159, 146, 133, 15, 117, 156, 48, 175, 40, 50, 76, 149, 88, 72, 145, 18, 101, 180, 85, 99, 202, 170, 211, 37, 251, 234, 188, 61]), + ([134, 129, 118, 82, 194, 145, 226, 246, 139, 43, 156, 14, 210, 117, 43, 151, 233, 11, 167, 166, 175, 66, 52, 133, 124, 38, 148, 244, 99, 78, 96, 133], [88, 206, 254, 44, 109, 90, 242, 64, 27, 66, 59, 166, 150, 110, 194, 46, 35, 253, 27, 27, 226, 120, 99, 99, 75, 114, 32, 24, 195, 181, 99, 53], [58, 191, 34, 120, 122, 251, 23, 171, 156, 103, 240, 33, 146, 43, 139, 143, 231, 120, 79, 60, 236, 128, 63, 62, 66, 149, 134, 224, 29, 192, 0, 92]), + ([73, 224, 84, 90, 110, 252, 174, 53, 163, 64, 34, 253, 82, 106, 67, 155, 191, 61, 236, 29, 192, 147, 121, 96, 199, 36, 129, 112, 121, 71, 170, 25], [239, 207, 1, 81, 168, 123, 151, 189, 73, 134, 139, 86, 65, 153, 105, 109, 187, 193, 92, 177, 34, 18, 100, 127, 24, 169, 210, 100, 171, 81, 166, 93], [89, 113, 156, 239, 209, 176, 141, 82, 199, 188, 194, 201, 196, 71, 2, 32, 86, 222, 196, 166, 162, 64, 117, 50, 220, 118, 204, 210, 182, 162, 13, 174]), + ([42, 229, 76, 7, 132, 249, 150, 105, 93, 218, 253, 223, 181, 139, 27, 228, 162, 139, 135, 92, 208, 180, 59, 32, 220, 9, 231, 234, 213, 88, 251, 67], [58, 109, 204, 74, 98, 183, 97, 172, 239, 24, 164, 212, 21, 56, 192, 170, 20, 205, 54, 102, 139, 249, 143, 14, 22, 142, 251, 111, 95, 220, 11, 166], [3, 157, 190, 43, 18, 149, 162, 159, 46, 147, 20, 59, 109, 234, 100, 70, 237, 136, 41, 234, 96, 143, 104, 231, 67, 45, 242, 142, 198, 147, 167, 248]), + ([66, 215, 63, 51, 174, 170, 106, 28, 126, 239, 221, 24, 215, 207, 217, 98, 134, 73, 60, 42, 15, 74, 34, 108, 15, 253, 63, 138, 49, 199, 137, 186], [14, 63, 87, 49, 129, 182, 60, 197, 228, 142, 121, 203, 11, 52, 236, 173, 184, 87, 212, 97, 184, 89, 109, 46, 82, 29, 120, 148, 99, 109, 183, 106], [106, 234, 153, 98, 123, 22, 144, 249, 238, 55, 23, 238, 36, 209, 180, 113, 163, 18, 33, 202, 236, 157, 172, 105, 232, 141, 61, 128, 70, 213, 109, 35]), + ([124, 71, 19, 31, 54, 190, 116, 153, 227, 162, 166, 124, 67, 94, 190, 13, 200, 142, 43, 98, 66, 30, 135, 175, 221, 56, 180, 11, 141, 97, 178, 217], [117, 97, 155, 201, 18, 91, 209, 156, 106, 16, 58, 107, 175, 235, 29, 24, 50, 16, 53, 55, 7, 246, 68, 163, 161, 101, 219, 145, 2, 3, 49, 23], [165, 102, 151, 110, 207, 245, 191, 142, 35, 130, 62, 86, 46, 139, 123, 157, 93, 231, 195, 152, 174, 59, 203, 24, 140, 228, 111, 126, 67, 176, 212, 105]), + ([125, 91, 107, 117, 112, 61, 212, 236, 70, 71, 203, 11, 135, 64, 251, 73, 187, 10, 10, 148, 199, 151, 13, 213, 246, 53, 149, 221, 121, 30, 250, 210], [17, 182, 122, 168, 52, 195, 78, 210, 229, 165, 196, 39, 230, 103, 65, 129, 252, 164, 162, 15, 172, 37, 197, 15, 211, 6, 1, 91, 129, 213, 42, 120], [133, 239, 244, 216, 48, 1, 182, 106, 125, 191, 179, 82, 240, 90, 73, 79, 78, 28, 231, 171, 139, 155, 207, 251, 173, 48, 0, 98, 145, 97, 86, 134]), + ([104, 87, 71, 7, 237, 252, 140, 193, 184, 249, 66, 77, 140, 166, 223, 250, 106, 213, 89, 84, 13, 175, 48, 252, 129, 92, 196, 255, 105, 114, 166, 172], [107, 44, 151, 161, 29, 65, 166, 163, 37, 255, 157, 248, 137, 183, 183, 197, 35, 147, 27, 246, 173, 176, 225, 134, 221, 116, 201, 190, 72, 170, 225, 30], [55, 49, 116, 95, 15, 6, 106, 74, 247, 39, 48, 36, 232, 29, 100, 107, 112, 100, 20, 168, 144, 9, 174, 55, 122, 25, 45, 19, 76, 210, 168, 143]), + ([153, 235, 190, 211, 173, 192, 142, 247, 26, 197, 246, 158, 51, 2, 44, 205, 68, 57, 94, 237, 75, 167, 180, 123, 255, 241, 6, 143, 161, 247, 60, 86], [189, 42, 153, 50, 49, 10, 172, 238, 174, 185, 30, 191, 9, 3, 237, 243, 104, 147, 195, 225, 116, 228, 218, 134, 146, 147, 133, 117, 213, 91, 48, 94], [75, 23, 236, 202, 211, 127, 35, 133, 30, 178, 176, 230, 194, 142, 73, 59, 138, 189, 44, 86, 95, 162, 37, 56, 162, 98, 33, 187, 222, 73, 191, 38]), + ([214, 155, 79, 217, 55, 27, 250, 118, 49, 107, 228, 63, 192, 71, 53, 100, 221, 15, 170, 241, 48, 106, 180, 137, 144, 70, 9, 36, 94, 241, 60, 207], [142, 183, 48, 186, 248, 197, 53, 242, 254, 58, 131, 41, 6, 4, 150, 141, 221, 68, 68, 23, 29, 73, 22, 236, 1, 120, 219, 198, 184, 33, 231, 231], [37, 96, 159, 217, 235, 227, 44, 140, 162, 166, 208, 161, 31, 21, 215, 106, 184, 99, 60, 237, 157, 230, 137, 126, 95, 151, 143, 61, 4, 68, 104, 164]), + ([236, 254, 222, 224, 230, 116, 219, 147, 186, 233, 54, 196, 175, 160, 79, 223, 107, 150, 5, 81, 62, 209, 96, 85, 55, 0, 21, 175, 207, 108, 132, 36], [91, 252, 139, 101, 136, 140, 201, 245, 130, 238, 136, 37, 10, 40, 246, 67, 104, 16, 254, 141, 90, 246, 53, 171, 151, 225, 121, 43, 71, 54, 10, 165], [140, 12, 230, 0, 72, 140, 161, 124, 39, 173, 246, 207, 178, 141, 134, 128, 83, 156, 132, 18, 107, 188, 124, 229, 79, 51, 48, 137, 111, 89, 135, 160]), + ([113, 77, 121, 185, 67, 23, 66, 229, 19, 186, 85, 47, 81, 131, 217, 246, 125, 90, 205, 206, 135, 84, 177, 144, 3, 129, 101, 243, 77, 47, 69, 7], [159, 148, 82, 14, 237, 144, 194, 168, 163, 32, 51, 58, 60, 63, 54, 55, 205, 21, 138, 181, 253, 253, 84, 43, 203, 114, 16, 2, 9, 234, 70, 81], [147, 101, 229, 180, 213, 251, 40, 224, 209, 229, 72, 192, 124, 224, 207, 104, 224, 175, 94, 168, 14, 174, 78, 129, 116, 32, 168, 42, 218, 95, 210, 18]), + ([151, 14, 136, 217, 152, 105, 37, 247, 64, 226, 131, 87, 251, 91, 17, 74, 25, 245, 150, 50, 65, 225, 18, 203, 121, 138, 228, 188, 162, 21, 110, 120], [227, 67, 32, 205, 67, 202, 89, 172, 196, 71, 163, 67, 105, 177, 25, 77, 68, 173, 201, 131, 153, 51, 212, 211, 143, 234, 44, 196, 198, 120, 99, 189], [196, 245, 112, 247, 198, 125, 143, 133, 134, 155, 26, 54, 94, 108, 101, 9, 192, 169, 11, 66, 159, 59, 118, 94, 112, 83, 154, 189, 7, 26, 210, 245]), + ([26, 250, 53, 136, 41, 39, 92, 63, 195, 200, 187, 184, 72, 102, 252, 140, 139, 195, 58, 245, 61, 84, 201, 22, 239, 190, 1, 52, 216, 68, 129, 29], [108, 11, 207, 62, 69, 54, 89, 126, 118, 82, 239, 27, 208, 137, 216, 80, 110, 98, 185, 175, 120, 30, 118, 88, 207, 77, 6, 50, 204, 141, 0, 56], [229, 106, 141, 185, 68, 80, 96, 128, 199, 100, 4, 238, 193, 106, 160, 143, 104, 76, 163, 230, 72, 34, 29, 22, 105, 56, 176, 232, 75, 56, 121, 237]), + ([115, 109, 225, 5, 58, 242, 142, 48, 252, 177, 191, 21, 62, 83, 235, 213, 195, 172, 49, 13, 232, 10, 252, 194, 255, 61, 54, 61, 103, 0, 163, 215], [24, 38, 64, 140, 3, 208, 250, 38, 189, 31, 101, 239, 102, 208, 234, 37, 137, 86, 120, 27, 244, 92, 242, 32, 215, 232, 247, 207, 20, 160, 135, 225], [17, 78, 166, 79, 217, 162, 184, 229, 116, 253, 15, 2, 51, 101, 159, 41, 46, 230, 17, 228, 160, 95, 167, 153, 46, 90, 100, 1, 247, 212, 130, 18]), + ([208, 12, 83, 60, 151, 222, 197, 24, 127, 22, 125, 11, 60, 20, 155, 137, 22, 154, 166, 165, 173, 16, 203, 134, 207, 151, 126, 2, 95, 54, 66, 214], [58, 107, 50, 43, 89, 202, 204, 164, 40, 218, 106, 248, 105, 254, 246, 96, 177, 85, 146, 42, 239, 170, 55, 19, 213, 71, 219, 37, 237, 129, 17, 240], [192, 131, 212, 113, 89, 120, 121, 14, 131, 184, 17, 11, 106, 209, 138, 194, 6, 46, 251, 128, 115, 190, 78, 74, 247, 247, 133, 234, 128, 170, 55, 21]), + ([104, 51, 136, 239, 189, 133, 98, 24, 222, 132, 10, 122, 113, 192, 27, 10, 181, 163, 186, 118, 96, 242, 180, 136, 102, 135, 94, 102, 25, 232, 216, 48], [182, 114, 104, 141, 237, 20, 189, 1, 59, 191, 109, 224, 40, 185, 72, 139, 62, 178, 186, 59, 76, 178, 192, 210, 152, 81, 37, 44, 137, 242, 237, 105], [106, 216, 125, 65, 242, 253, 176, 157, 148, 222, 134, 164, 110, 243, 2, 222, 143, 199, 85, 128, 11, 67, 219, 109, 125, 224, 182, 76, 186, 62, 0, 179]), + ([133, 23, 182, 94, 140, 187, 41, 122, 203, 234, 113, 42, 111, 160, 210, 250, 219, 11, 57, 113, 238, 48, 190, 240, 70, 24, 105, 17, 32, 64, 142, 135], [177, 130, 179, 134, 255, 105, 134, 55, 19, 7, 227, 157, 194, 83, 60, 15, 163, 121, 91, 147, 73, 254, 119, 61, 97, 3, 172, 12, 167, 85, 39, 53], [83, 191, 191, 38, 47, 224, 85, 147, 245, 174, 25, 152, 24, 193, 27, 154, 128, 93, 136, 34, 87, 171, 224, 246, 196, 111, 215, 15, 208, 140, 2, 59]), + ([181, 211, 68, 72, 60, 29, 116, 128, 195, 45, 3, 155, 124, 115, 8, 196, 16, 194, 39, 232, 201, 123, 78, 92, 246, 96, 253, 70, 235, 125, 69, 206], [157, 33, 69, 12, 136, 4, 46, 127, 154, 159, 30, 7, 171, 124, 65, 166, 27, 36, 55, 201, 137, 142, 112, 64, 242, 180, 175, 119, 177, 11, 78, 158], [250, 210, 177, 197, 83, 79, 54, 219, 40, 147, 10, 209, 165, 79, 13, 128, 203, 145, 243, 34, 183, 154, 40, 156, 178, 215, 250, 23, 51, 180, 209, 149]), + ([218, 128, 195, 2, 218, 88, 117, 165, 113, 187, 237, 76, 236, 252, 3, 155, 233, 93, 93, 112, 70, 217, 125, 241, 114, 211, 251, 251, 17, 20, 131, 228], [29, 29, 105, 25, 243, 135, 10, 215, 176, 130, 122, 177, 65, 124, 28, 244, 37, 145, 192, 255, 175, 147, 154, 95, 118, 100, 186, 216, 245, 8, 215, 207], [68, 84, 187, 149, 190, 24, 56, 245, 35, 19, 8, 200, 8, 157, 24, 160, 192, 162, 164, 135, 186, 211, 133, 67, 123, 36, 112, 156, 205, 195, 17, 141]), + ([231, 206, 109, 216, 141, 221, 57, 136, 105, 246, 114, 82, 191, 144, 252, 31, 34, 214, 124, 83, 91, 55, 207, 55, 184, 163, 70, 134, 44, 199, 136, 3], [112, 130, 131, 95, 234, 111, 61, 127, 131, 251, 45, 243, 63, 235, 98, 42, 241, 79, 186, 196, 178, 4, 224, 159, 69, 190, 129, 157, 150, 254, 222, 205], [76, 39, 224, 141, 82, 141, 182, 24, 124, 162, 173, 24, 77, 146, 12, 236, 30, 123, 50, 168, 82, 61, 119, 248, 149, 240, 180, 117, 11, 85, 191, 72]), + ([20, 220, 60, 1, 146, 13, 229, 31, 99, 196, 29, 119, 194, 99, 192, 152, 178, 195, 106, 62, 74, 23, 72, 174, 4, 24, 33, 68, 193, 249, 153, 131], [137, 182, 24, 88, 166, 181, 183, 28, 29, 225, 13, 148, 81, 30, 68, 196, 229, 135, 76, 238, 59, 152, 68, 42, 82, 147, 39, 180, 163, 227, 49, 93], [149, 17, 247, 176, 209, 224, 132, 162, 82, 38, 196, 227, 49, 109, 254, 92, 1, 252, 167, 178, 215, 204, 6, 193, 98, 39, 211, 62, 102, 212, 2, 185]), + ([127, 61, 50, 95, 9, 172, 55, 55, 149, 251, 199, 131, 38, 54, 172, 220, 156, 202, 190, 116, 246, 221, 114, 205, 154, 100, 155, 129, 6, 183, 22, 160], [118, 229, 189, 78, 251, 125, 35, 246, 68, 172, 103, 136, 109, 20, 61, 161, 220, 226, 106, 243, 165, 192, 61, 48, 207, 163, 87, 93, 112, 161, 177, 138], [148, 237, 13, 66, 189, 177, 250, 243, 178, 155, 90, 139, 83, 5, 92, 92, 4, 50, 24, 195, 114, 210, 167, 102, 11, 98, 151, 236, 22, 117, 243, 228]), + ([148, 33, 246, 153, 134, 122, 131, 81, 173, 100, 76, 155, 113, 8, 51, 79, 63, 54, 32, 95, 98, 10, 84, 151, 152, 55, 159, 58, 23, 79, 37, 206], [220, 82, 90, 84, 166, 89, 128, 246, 105, 72, 89, 226, 100, 27, 253, 238, 148, 39, 168, 174, 144, 49, 239, 30, 175, 112, 136, 190, 36, 85, 59, 169], [36, 36, 148, 39, 180, 29, 174, 144, 51, 67, 46, 170, 239, 34, 27, 24, 59, 52, 37, 252, 199, 245, 70, 190, 255, 64, 220, 70, 207, 230, 81, 10]), + ([13, 240, 126, 43, 227, 253, 72, 216, 247, 54, 225, 59, 196, 71, 222, 57, 203, 28, 13, 136, 13, 110, 71, 12, 203, 214, 98, 214, 210, 193, 25, 126], [246, 5, 39, 196, 146, 200, 35, 38, 21, 95, 53, 28, 135, 174, 103, 26, 60, 148, 40, 243, 230, 124, 218, 154, 244, 56, 204, 8, 168, 87, 229, 216], [73, 118, 249, 94, 251, 26, 213, 94, 56, 82, 58, 68, 45, 66, 188, 49, 189, 202, 141, 212, 207, 18, 28, 12, 11, 169, 217, 94, 229, 159, 234, 212]), + ([6, 27, 228, 183, 77, 103, 229, 186, 78, 206, 77, 45, 231, 31, 59, 145, 57, 110, 79, 149, 229, 211, 134, 124, 136, 3, 248, 21, 243, 29, 250, 192], [61, 101, 156, 141, 136, 172, 29, 247, 54, 211, 80, 15, 175, 168, 170, 22, 102, 43, 3, 230, 224, 65, 234, 55, 224, 162, 225, 196, 169, 155, 183, 123], [206, 16, 152, 199, 114, 227, 105, 222, 219, 142, 230, 86, 164, 186, 228, 12, 7, 160, 31, 10, 168, 123, 208, 218, 137, 47, 92, 240, 110, 181, 220, 210]), + ([111, 117, 101, 25, 54, 15, 141, 150, 217, 96, 105, 217, 190, 33, 176, 255, 160, 221, 59, 255, 41, 41, 173, 62, 212, 167, 156, 102, 133, 147, 142, 176], [138, 135, 215, 42, 23, 175, 25, 174, 43, 138, 179, 12, 5, 182, 4, 118, 51, 84, 190, 163, 31, 237, 81, 239, 15, 37, 219, 121, 177, 229, 5, 181], [29, 190, 72, 233, 86, 28, 44, 21, 137, 106, 227, 78, 193, 221, 214, 2, 86, 35, 163, 214, 74, 229, 45, 109, 47, 102, 203, 245, 178, 173, 191, 215]), + ([122, 66, 84, 53, 251, 174, 251, 39, 71, 30, 85, 165, 34, 110, 178, 253, 4, 61, 253, 65, 178, 142, 10, 195, 122, 89, 89, 222, 94, 109, 18, 106], [160, 124, 128, 167, 37, 76, 152, 156, 79, 225, 70, 52, 66, 163, 9, 162, 77, 195, 249, 214, 101, 137, 219, 100, 11, 28, 231, 177, 171, 88, 67, 219], [91, 63, 80, 243, 26, 203, 67, 12, 34, 154, 68, 60, 224, 198, 188, 13, 165, 198, 131, 161, 11, 179, 0, 195, 201, 247, 10, 194, 40, 41, 249, 97]), + ([162, 215, 70, 8, 250, 5, 164, 149, 11, 106, 159, 0, 183, 247, 247, 31, 138, 19, 214, 28, 7, 155, 168, 224, 191, 7, 241, 185, 0, 168, 158, 193], [234, 211, 17, 41, 116, 10, 40, 236, 60, 195, 70, 98, 60, 40, 255, 63, 221, 146, 139, 71, 228, 43, 179, 242, 18, 152, 247, 178, 140, 158, 117, 12], [214, 165, 16, 35, 199, 39, 252, 205, 161, 100, 0, 14, 150, 187, 153, 180, 165, 189, 10, 255, 213, 169, 5, 175, 244, 157, 186, 58, 58, 21, 209, 78]), + ([181, 218, 187, 152, 193, 195, 150, 211, 92, 74, 179, 160, 143, 235, 5, 224, 152, 134, 106, 198, 97, 241, 220, 2, 223, 14, 134, 11, 141, 227, 255, 87], [67, 128, 71, 7, 170, 21, 12, 212, 60, 254, 60, 212, 72, 124, 13, 152, 199, 64, 42, 190, 161, 16, 158, 248, 125, 43, 254, 82, 94, 88, 1, 248], [176, 28, 221, 7, 166, 44, 62, 39, 147, 112, 50, 3, 92, 177, 55, 18, 240, 26, 30, 12, 143, 82, 178, 64, 184, 151, 184, 219, 156, 104, 224, 43]), + ([34, 174, 137, 13, 106, 163, 43, 10, 10, 77, 47, 115, 151, 154, 184, 225, 76, 9, 127, 237, 248, 217, 248, 146, 238, 163, 40, 135, 83, 32, 137, 136], [155, 141, 172, 10, 171, 73, 204, 71, 38, 5, 204, 81, 118, 133, 140, 160, 207, 219, 173, 188, 6, 223, 254, 201, 90, 164, 43, 121, 134, 147, 177, 164], [193, 208, 141, 68, 65, 179, 171, 237, 69, 128, 203, 96, 112, 109, 254, 125, 116, 60, 121, 169, 198, 7, 237, 75, 48, 147, 99, 143, 155, 18, 181, 6]), + ([80, 246, 173, 195, 114, 110, 216, 58, 211, 187, 188, 119, 95, 47, 159, 219, 124, 184, 215, 2, 148, 212, 136, 255, 35, 177, 76, 227, 158, 25, 111, 98], [172, 248, 253, 201, 247, 175, 237, 105, 245, 219, 220, 201, 243, 206, 189, 58, 214, 85, 209, 173, 221, 186, 219, 54, 169, 44, 185, 40, 105, 6, 247, 162], [77, 228, 177, 144, 82, 190, 157, 245, 154, 140, 49, 70, 124, 160, 32, 182, 106, 47, 9, 1, 251, 219, 166, 213, 124, 207, 231, 133, 48, 78, 142, 169]), + ([55, 110, 157, 149, 86, 207, 218, 62, 94, 108, 205, 144, 49, 193, 55, 62, 245, 0, 92, 138, 112, 94, 145, 70, 39, 13, 15, 222, 66, 218, 176, 133], [164, 27, 115, 230, 91, 254, 150, 13, 218, 78, 180, 243, 115, 105, 98, 185, 121, 155, 132, 164, 146, 156, 60, 126, 8, 172, 234, 190, 197, 196, 230, 157], [49, 34, 121, 14, 175, 99, 135, 217, 203, 64, 29, 144, 228, 28, 250, 97, 109, 223, 240, 110, 241, 208, 157, 14, 69, 25, 255, 123, 0, 7, 184, 164]), + ([148, 101, 68, 59, 189, 50, 244, 246, 122, 204, 98, 253, 73, 246, 91, 228, 220, 226, 152, 133, 28, 19, 187, 199, 219, 26, 85, 119, 37, 87, 106, 50], [53, 250, 43, 60, 24, 217, 246, 165, 22, 122, 184, 138, 206, 156, 12, 218, 80, 29, 20, 157, 179, 183, 74, 247, 146, 53, 93, 249, 187, 138, 205, 211], [40, 25, 113, 237, 128, 98, 32, 114, 12, 43, 28, 74, 25, 79, 37, 3, 165, 164, 230, 248, 123, 121, 250, 46, 82, 1, 246, 92, 202, 100, 16, 136]), + ([104, 91, 13, 175, 5, 129, 30, 5, 253, 235, 54, 39, 255, 38, 15, 105, 70, 251, 62, 35, 152, 45, 113, 225, 203, 59, 33, 93, 68, 22, 75, 31], [252, 184, 169, 194, 163, 58, 138, 153, 64, 179, 187, 185, 51, 67, 68, 68, 15, 37, 154, 190, 110, 65, 138, 166, 50, 230, 254, 37, 78, 170, 64, 40], [202, 65, 211, 25, 28, 82, 27, 53, 107, 54, 173, 253, 124, 38, 190, 125, 168, 58, 109, 246, 69, 60, 190, 135, 83, 109, 26, 207, 238, 203, 78, 239]), + ([78, 238, 18, 72, 5, 63, 248, 76, 167, 23, 67, 3, 101, 14, 230, 80, 181, 99, 100, 120, 175, 220, 17, 76, 18, 78, 146, 245, 19, 211, 246, 99], [220, 95, 235, 29, 236, 223, 65, 236, 104, 164, 146, 253, 177, 192, 30, 87, 207, 108, 56, 88, 155, 27, 68, 129, 68, 102, 162, 193, 248, 136, 88, 143], [115, 160, 181, 24, 2, 73, 215, 19, 232, 200, 123, 41, 49, 25, 164, 204, 64, 168, 216, 6, 46, 210, 116, 67, 217, 119, 95, 111, 38, 47, 45, 109])] + +end Blake3.PureTests diff --git a/lakefile.lean b/lakefile.lean index 735ae95..1d2146c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -18,6 +18,9 @@ lean_lib Blake3 where @[test_driver] lean_exe Blake3Test +lean_lib Blake3Tests where + roots := #[`Tests.Pure, `Tests.PureAudit, `Tests.PureVectors] + -- BLAKE3 C source abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3" abbrev blake3RepoTag := "1.8.7" @@ -100,4 +103,3 @@ lean_lib Blake3Rust where precompileModules := true roots := #[`Blake3.Rust] moreLinkObjs := #[blake3_rs] - diff --git a/rust/examples/pure_vectors.rs b/rust/examples/pure_vectors.rs new file mode 100644 index 0000000..1aca67d --- /dev/null +++ b/rust/examples/pure_vectors.rs @@ -0,0 +1,47 @@ +//! Regenerate Tests/PureVectors.lean with: +//! cargo run --locked --release --example pure_vectors > ../Tests/PureVectors.lean + +use blake3::hazmat::{HasherExt, Mode, merge_subtrees_non_root, merge_subtrees_root}; + +fn input(length: usize, salt: usize) -> Vec { + (0..length) + .map(|i| u8::try_from((i * 17 + i / 251 * 13 + salt * 29) % 256).unwrap()) + .collect() +} + +fn main() { + println!("/- Generated by rust/examples/pure_vectors.rs using BLAKE3 1.8.7. -/"); + println!("namespace Blake3.PureTests\n"); + println!("def chunkVectors : List (Nat × Nat × List UInt8) := ["); + let counters = [ + 0, + 1, + 2, + 255, + (1_u64 << 32) - 1, + 1_u64 << 32, + (1_u64 << 54) - 1, + ]; + for (index, counter) in counters.into_iter().enumerate() { + for (part, length) in [1, 63, 64, 65, 1023, 1024].into_iter().enumerate() { + let data = input(length, usize::try_from(counter % 251).unwrap()); + let cv = blake3::Hasher::new() + .set_input_offset(counter * 1024) + .update(&data) + .finalize_non_root(); + let separator = if index == 6 && part == 5 { "]" } else { "," }; + println!(" ({counter}, {length}, {cv:?}){separator}"); + } + } + println!("\ndef parentVectors : List (List UInt8 × List UInt8 × List UInt8) := ["); + for salt in 0..64 { + let left: [u8; 32] = input(32, salt).try_into().unwrap(); + let right: [u8; 32] = input(32, salt + 83).try_into().unwrap(); + let cv = merge_subtrees_non_root(&left, &right, Mode::Hash); + let root = *merge_subtrees_root(&left, &right, Mode::Hash).as_bytes(); + let ordinary = *blake3::hash(&[left, right].concat()).as_bytes(); + let separator = if salt == 63 { "]" } else { "," }; + println!(" ({cv:?}, {root:?}, {ordinary:?}){separator}"); + } + println!("\nend Blake3.PureTests"); +} From 220ffa45cbb6ab86d3ec5e9f150e65f97d1cb272 Mon Sep 17 00:00:00 2001 From: "J. C. Burnham" Date: Tue, 15 Sep 2026 09:30:35 -0400 Subject: [PATCH 2/2] Generate the pure test vectors as a typed structure literal Move the vector schema into Tests/Vectors.lean and have rust/examples/pure_vectors.rs emit one Blake3.PureTests.Vectors literal with named fields, so the generated file is data only: an import, one def line, and records with trailing commas. Tests/Pure.lean reads the records by field name, parent records carry their salt, and the recorded crate version is checked against the linked Rust backend. 32-byte values are lowercase hex strings rather than byte lists. A single declaration holding both record lists as List UInt8 exceeds a code generator recursion cliff at roughly 8k bindings and fails with "maximum recursion depth has been reached" even though it elaborates; hex keeps each record at a few bindings and matches the BLAKE3 team's own test vector format. The vector values are unchanged. --- Tests/Pure.lean | 32 +++-- Tests/PureVectors.lean | 228 +++++++++++++++++----------------- Tests/Vectors.lean | 35 ++++++ lakefile.lean | 2 +- rust/examples/pure_vectors.rs | 45 ++++--- 5 files changed, 201 insertions(+), 141 deletions(-) create mode 100644 Tests/Vectors.lean diff --git a/Tests/Pure.lean b/Tests/Pure.lean index ceb19fc..816e797 100644 --- a/Tests/Pure.lean +++ b/Tests/Pure.lean @@ -19,6 +19,9 @@ private def lengths : List Nat := (((List.range 17).map (· + 1) ++ [32, 64, 128]).flatMap fun chunks => [chunks * 1024 - 1, chunks * 1024, chunks * 1024 + 1])).eraseDups +private def hex (bytes : List UInt8) : String := + String.ofList (bytes.flatMap fun byte => [Nat.digitChar (byte.toNat / 16), Nat.digitChar (byte.toNat % 16)]) + private def knownAnswer (input : ByteArray) (expected : List UInt8) : IO Unit := do unless (Pure.hash input).val.data.toList == expected do throw (IO.userError "pure Blake3 known-answer test failed") @@ -52,22 +55,25 @@ def run (compareC compareRust : Bool) : IO Unit := do let parent := Pure.parentOutput left.chainingValue right.chainingValue unless parent.rootHash.toList == actual.data.toList do throw (IO.userError "pure Blake3 subtree composition differs") unless trees == 58 do throw (IO.userError "incomplete pure Blake3 tree cases") - unless chunkVectors.length == 42 && parentVectors.length == 64 do + if compareRust then + unless vectors.reference == Rust.version do + throw (IO.userError s!"native component vectors are from BLAKE3 {vectors.reference}, Rust backend is {Rust.version}") + unless vectors.chunks.length == 42 && vectors.parents.length == 64 do throw (IO.userError "incomplete native component vectors") - for (counter, length, expected) in chunkVectors do - let input := testInput length (counter % 251) - let actual := Pure.cvBytes (Pure.chunkOutput counter.toUInt64 input.data.toList).chainingValue - unless actual.toList == expected do throw (IO.userError s!"pure Blake3 chunk differs at {counter}, {length}") - for ((expectedCV, expectedRoot, expectedOrdinary), salt) in parentVectors.zipIdx do - let left := testInput 32 salt - let right := testInput 32 (salt + 83) + for chunk in vectors.chunks do + let input := testInput chunk.length (chunk.counter % 251) + let actual := Pure.cvBytes (Pure.chunkOutput chunk.counter.toUInt64 input.data.toList).chainingValue + unless hex actual.toList == chunk.cv do throw (IO.userError s!"pure Blake3 chunk differs at {chunk.counter}, {chunk.length}") + for parent in vectors.parents do + let left := testInput 32 parent.salt + let right := testInput 32 (parent.salt + 83) let cv := fun bytes : ByteArray => Vector.ofFn fun word : Fin 8 => Pure.bytesWord (Vector.ofFn fun byte : Fin 4 => bytes[word.val * 4 + byte.val]!) - let parent := Pure.parentOutput (cv left) (cv right) - unless (Pure.cvBytes parent.chainingValue).toList == expectedCV && parent.rootHash.toList == expectedRoot do - throw (IO.userError "pure Blake3 internal parent differs") - unless (Pure.hash (left ++ right)).val.data.toList == expectedOrdinary do - throw (IO.userError "pure Blake3 digest-pair hash differs") + let output := Pure.parentOutput (cv left) (cv right) + unless hex (Pure.cvBytes output.chainingValue).toList == parent.cv && hex output.rootHash.toList == parent.root do + throw (IO.userError s!"pure Blake3 internal parent differs at salt {parent.salt}") + unless hex (Pure.hash (left ++ right)).val.data.toList == parent.ordinary do + throw (IO.userError s!"pure Blake3 digest-pair hash differs at salt {parent.salt}") IO.println s!"Pure Blake3: 2 known answers, 258 inputs, 58 splits, 42 chunks and 64 parents passed (C={compareC}, Rust={compareRust})" end Blake3.PureTests diff --git a/Tests/PureVectors.lean b/Tests/PureVectors.lean index 7975073..b2ea076 100644 --- a/Tests/PureVectors.lean +++ b/Tests/PureVectors.lean @@ -1,114 +1,116 @@ -/- Generated by rust/examples/pure_vectors.rs using BLAKE3 1.8.7. -/ -namespace Blake3.PureTests +/- Generated by rust/examples/pure_vectors.rs. Do not edit. -/ +import Tests.Vectors -def chunkVectors : List (Nat × Nat × List UInt8) := [ - (0, 1, [13, 241, 167, 136, 29, 113, 210, 135, 208, 175, 194, 252, 215, 210, 61, 40, 241, 46, 64, 26, 184, 88, 202, 38, 127, 17, 197, 241, 113, 13, 243, 21]), - (0, 63, [124, 122, 4, 126, 78, 9, 90, 75, 72, 194, 149, 16, 99, 175, 53, 135, 125, 189, 61, 97, 82, 123, 66, 130, 178, 99, 193, 107, 176, 149, 118, 130]), - (0, 64, [31, 147, 133, 199, 42, 181, 73, 178, 14, 102, 138, 242, 173, 120, 201, 120, 156, 1, 17, 33, 232, 55, 210, 132, 20, 212, 28, 113, 167, 54, 176, 52]), - (0, 65, [121, 229, 202, 199, 36, 142, 37, 200, 116, 173, 184, 246, 79, 94, 118, 182, 105, 46, 212, 129, 246, 197, 54, 146, 4, 167, 155, 2, 215, 197, 48, 255]), - (0, 1023, [213, 123, 249, 134, 24, 2, 103, 214, 2, 203, 200, 239, 124, 4, 149, 253, 21, 32, 195, 112, 13, 139, 208, 149, 47, 106, 109, 137, 42, 46, 61, 38]), - (0, 1024, [112, 206, 128, 171, 170, 231, 196, 29, 215, 181, 127, 83, 162, 42, 116, 117, 121, 82, 135, 33, 217, 198, 119, 227, 90, 199, 145, 87, 206, 196, 20, 127]), - (1, 1, [67, 221, 33, 31, 197, 45, 139, 27, 83, 105, 16, 43, 31, 158, 113, 32, 250, 212, 179, 84, 132, 131, 132, 210, 238, 121, 140, 218, 255, 102, 105, 189]), - (1, 63, [149, 251, 28, 255, 217, 210, 100, 68, 216, 225, 151, 28, 192, 104, 245, 57, 27, 97, 143, 109, 78, 76, 195, 71, 243, 43, 5, 16, 44, 27, 198, 142]), - (1, 64, [54, 177, 124, 34, 205, 114, 130, 187, 67, 182, 87, 90, 212, 180, 242, 206, 18, 201, 35, 60, 146, 29, 184, 81, 251, 238, 215, 158, 22, 148, 121, 103]), - (1, 65, [213, 17, 166, 171, 57, 234, 23, 176, 17, 54, 215, 82, 75, 80, 19, 96, 154, 202, 205, 219, 12, 212, 185, 141, 63, 43, 69, 50, 9, 223, 246, 167]), - (1, 1023, [221, 180, 243, 233, 51, 62, 8, 151, 72, 208, 151, 220, 196, 85, 248, 42, 56, 119, 204, 41, 47, 155, 3, 52, 65, 239, 106, 50, 192, 199, 137, 140]), - (1, 1024, [243, 82, 196, 190, 7, 100, 234, 6, 10, 68, 157, 57, 83, 136, 250, 177, 125, 7, 177, 221, 205, 166, 23, 13, 65, 70, 51, 225, 255, 174, 14, 249]), - (2, 1, [61, 150, 210, 68, 247, 92, 86, 216, 227, 194, 11, 40, 108, 0, 17, 173, 227, 25, 206, 15, 10, 125, 103, 235, 99, 59, 139, 205, 84, 184, 41, 255]), - (2, 63, [28, 132, 249, 139, 156, 144, 237, 39, 110, 61, 178, 92, 98, 97, 5, 124, 83, 146, 178, 230, 163, 148, 88, 61, 201, 129, 204, 39, 226, 222, 142, 242]), - (2, 64, [109, 200, 127, 28, 230, 178, 211, 66, 200, 246, 132, 208, 40, 171, 64, 209, 146, 81, 173, 139, 29, 143, 22, 221, 168, 28, 172, 210, 184, 50, 120, 91]), - (2, 65, [74, 193, 127, 6, 32, 207, 177, 112, 238, 26, 14, 109, 177, 199, 156, 119, 86, 190, 14, 213, 165, 98, 39, 248, 11, 56, 2, 204, 19, 14, 14, 161]), - (2, 1023, [7, 208, 158, 235, 209, 225, 225, 66, 246, 235, 206, 25, 33, 216, 210, 69, 56, 81, 210, 136, 73, 184, 28, 144, 134, 36, 212, 138, 15, 23, 161, 162]), - (2, 1024, [69, 130, 50, 166, 164, 41, 151, 116, 13, 199, 224, 104, 12, 192, 62, 177, 199, 6, 135, 241, 55, 91, 200, 178, 171, 196, 208, 93, 27, 23, 120, 24]), - (255, 1, [62, 182, 108, 102, 133, 226, 50, 15, 0, 31, 194, 97, 20, 192, 18, 123, 149, 66, 105, 62, 120, 172, 192, 251, 250, 250, 170, 83, 104, 104, 16, 140]), - (255, 63, [110, 117, 147, 47, 69, 24, 108, 25, 104, 20, 8, 46, 241, 198, 104, 177, 29, 195, 227, 190, 89, 137, 205, 153, 180, 127, 167, 190, 78, 205, 124, 214]), - (255, 64, [223, 215, 76, 230, 242, 215, 238, 85, 51, 228, 83, 117, 220, 56, 19, 55, 125, 16, 82, 105, 93, 195, 40, 96, 21, 179, 129, 102, 161, 59, 39, 133]), - (255, 65, [20, 173, 14, 113, 212, 89, 235, 16, 129, 98, 81, 83, 63, 246, 55, 195, 191, 37, 251, 234, 74, 51, 1, 167, 43, 183, 34, 139, 111, 55, 238, 20]), - (255, 1023, [2, 119, 251, 63, 222, 182, 130, 105, 162, 64, 54, 97, 31, 228, 138, 215, 146, 87, 107, 223, 253, 120, 60, 32, 243, 85, 29, 195, 241, 162, 40, 236]), - (255, 1024, [19, 46, 53, 175, 147, 230, 14, 121, 90, 170, 72, 68, 214, 45, 43, 37, 48, 1, 5, 101, 53, 238, 108, 170, 3, 197, 119, 205, 132, 219, 184, 139]), - (4294967295, 1, [56, 83, 7, 164, 241, 213, 58, 174, 6, 144, 97, 99, 226, 239, 170, 130, 124, 241, 142, 54, 75, 1, 127, 159, 213, 104, 229, 44, 133, 104, 121, 90]), - (4294967295, 63, [243, 21, 13, 211, 190, 57, 251, 229, 128, 107, 209, 98, 249, 43, 1, 255, 4, 110, 199, 114, 44, 157, 154, 56, 247, 178, 167, 7, 25, 63, 34, 87]), - (4294967295, 64, [54, 8, 165, 77, 235, 26, 131, 170, 146, 124, 80, 189, 27, 120, 215, 119, 217, 86, 101, 60, 15, 100, 113, 220, 183, 210, 174, 70, 28, 28, 97, 121]), - (4294967295, 65, [127, 132, 168, 234, 163, 32, 231, 3, 20, 60, 2, 144, 180, 255, 222, 62, 199, 162, 209, 103, 163, 137, 252, 208, 43, 49, 11, 195, 94, 114, 44, 63]), - (4294967295, 1023, [53, 238, 165, 239, 73, 107, 185, 129, 75, 65, 87, 62, 73, 102, 229, 137, 6, 223, 142, 138, 32, 96, 38, 81, 78, 139, 112, 147, 100, 200, 38, 252]), - (4294967295, 1024, [111, 128, 112, 124, 200, 172, 70, 160, 154, 70, 245, 114, 233, 230, 202, 226, 249, 8, 41, 96, 27, 146, 35, 18, 106, 38, 253, 19, 168, 182, 145, 129]), - (4294967296, 1, [174, 117, 32, 84, 47, 154, 23, 29, 230, 227, 210, 29, 37, 0, 76, 232, 149, 77, 32, 234, 226, 72, 77, 93, 65, 42, 45, 225, 102, 209, 123, 142]), - (4294967296, 63, [84, 240, 16, 108, 78, 126, 85, 30, 168, 31, 22, 239, 16, 140, 159, 123, 90, 244, 110, 7, 6, 38, 61, 224, 97, 76, 250, 194, 99, 163, 205, 44]), - (4294967296, 64, [202, 131, 113, 175, 159, 193, 210, 191, 156, 120, 206, 77, 183, 251, 225, 10, 227, 17, 121, 60, 114, 205, 19, 143, 178, 120, 55, 83, 240, 47, 178, 108]), - (4294967296, 65, [240, 91, 163, 80, 83, 213, 102, 206, 11, 94, 238, 99, 64, 209, 55, 13, 253, 92, 92, 11, 124, 54, 90, 55, 8, 229, 173, 197, 137, 103, 186, 170]), - (4294967296, 1023, [53, 93, 188, 131, 120, 54, 213, 74, 164, 76, 58, 247, 234, 30, 200, 78, 175, 32, 172, 246, 224, 9, 83, 68, 244, 31, 7, 67, 247, 17, 114, 150]), - (4294967296, 1024, [225, 170, 71, 199, 103, 170, 44, 110, 180, 240, 57, 57, 20, 67, 15, 110, 185, 227, 82, 166, 247, 131, 217, 179, 178, 231, 135, 36, 155, 37, 210, 84]), - (18014398509481983, 1, [121, 145, 221, 95, 240, 247, 137, 175, 15, 63, 175, 243, 241, 154, 114, 229, 73, 54, 165, 24, 158, 25, 120, 5, 203, 138, 125, 18, 30, 44, 147, 118]), - (18014398509481983, 63, [120, 100, 48, 141, 72, 255, 192, 166, 100, 125, 80, 239, 218, 118, 232, 133, 181, 191, 135, 131, 143, 13, 169, 100, 241, 52, 234, 201, 130, 226, 81, 20]), - (18014398509481983, 64, [13, 186, 25, 87, 101, 59, 40, 55, 141, 74, 225, 25, 33, 148, 30, 146, 11, 107, 88, 165, 68, 188, 218, 190, 50, 12, 183, 189, 230, 54, 171, 59]), - (18014398509481983, 65, [20, 52, 91, 192, 249, 204, 13, 156, 105, 174, 56, 90, 206, 137, 18, 128, 151, 71, 68, 203, 5, 118, 98, 155, 21, 74, 21, 95, 118, 164, 13, 173]), - (18014398509481983, 1023, [219, 239, 75, 169, 67, 20, 50, 75, 75, 115, 96, 55, 183, 22, 183, 234, 57, 198, 45, 93, 219, 12, 90, 84, 215, 72, 93, 96, 199, 75, 163, 188]), - (18014398509481983, 1024, [237, 157, 154, 128, 246, 72, 81, 81, 137, 65, 39, 160, 1, 118, 173, 225, 80, 241, 79, 20, 60, 25, 117, 248, 36, 249, 166, 186, 81, 253, 130, 159])] - -def parentVectors : List (List UInt8 × List UInt8 × List UInt8) := [ - ([156, 70, 127, 251, 125, 94, 185, 157, 129, 32, 72, 205, 5, 182, 245, 135, 72, 142, 116, 25, 7, 8, 86, 120, 218, 237, 172, 164, 241, 144, 255, 179], [136, 142, 105, 104, 77, 32, 135, 115, 76, 76, 20, 191, 208, 229, 126, 244, 229, 168, 37, 174, 101, 62, 62, 50, 14, 154, 221, 218, 215, 151, 108, 147], [191, 194, 194, 226, 169, 140, 29, 68, 162, 205, 105, 249, 58, 164, 41, 189, 178, 153, 145, 33, 234, 46, 161, 207, 78, 196, 35, 21, 83, 181, 114, 44]), - ([85, 199, 73, 119, 254, 194, 44, 173, 206, 116, 189, 89, 71, 178, 75, 244, 49, 176, 211, 21, 69, 88, 1, 222, 195, 64, 210, 35, 77, 58, 67, 206], [52, 236, 141, 88, 223, 11, 168, 175, 86, 169, 147, 150, 4, 253, 10, 204, 194, 226, 8, 82, 63, 102, 210, 247, 45, 174, 57, 79, 179, 56, 208, 97], [69, 37, 73, 166, 188, 74, 142, 86, 109, 115, 198, 123, 170, 73, 4, 121, 32, 142, 190, 45, 102, 233, 93, 233, 154, 158, 50, 83, 28, 133, 42, 85]), - ([225, 154, 194, 235, 123, 234, 134, 121, 221, 29, 85, 76, 85, 230, 197, 174, 32, 126, 170, 235, 169, 194, 102, 237, 54, 181, 188, 118, 163, 137, 10, 227], [54, 231, 177, 182, 89, 39, 48, 211, 12, 66, 191, 43, 99, 197, 121, 12, 190, 17, 166, 168, 129, 37, 202, 192, 231, 28, 151, 151, 1, 82, 148, 25], [88, 104, 8, 221, 221, 77, 212, 153, 113, 25, 230, 2, 51, 227, 210, 20, 154, 201, 247, 90, 160, 226, 77, 15, 153, 155, 207, 20, 58, 253, 227, 218]), - ([165, 109, 161, 68, 103, 205, 239, 42, 5, 245, 228, 61, 85, 52, 123, 250, 34, 83, 213, 17, 63, 134, 67, 148, 168, 165, 204, 35, 140, 158, 232, 223], [42, 139, 61, 80, 0, 117, 209, 91, 9, 109, 184, 224, 63, 142, 91, 134, 98, 203, 133, 98, 134, 162, 252, 197, 212, 70, 181, 107, 197, 123, 166, 152], [154, 254, 134, 214, 153, 241, 210, 10, 181, 171, 228, 186, 128, 114, 234, 61, 11, 9, 135, 162, 140, 196, 74, 12, 25, 175, 56, 111, 255, 90, 1, 80]), - ([163, 117, 68, 174, 252, 193, 177, 136, 49, 85, 49, 84, 117, 128, 111, 120, 1, 43, 188, 138, 154, 8, 194, 117, 28, 225, 80, 105, 241, 143, 4, 64], [79, 242, 39, 81, 154, 43, 61, 93, 129, 28, 246, 111, 24, 106, 218, 206, 123, 67, 40, 40, 97, 215, 233, 146, 121, 207, 242, 87, 149, 249, 211, 142], [31, 196, 13, 217, 125, 98, 20, 194, 93, 175, 206, 166, 65, 111, 87, 10, 71, 203, 171, 194, 20, 48, 127, 19, 14, 191, 75, 148, 20, 144, 247, 18]), - ([120, 59, 171, 131, 171, 12, 92, 77, 110, 17, 190, 250, 190, 125, 158, 196, 83, 197, 100, 148, 248, 226, 169, 14, 178, 0, 238, 135, 1, 97, 28, 248], [108, 42, 144, 23, 155, 199, 142, 194, 44, 180, 75, 70, 73, 29, 103, 99, 60, 64, 22, 157, 198, 88, 20, 147, 135, 56, 4, 214, 226, 196, 9, 189], [146, 198, 10, 144, 75, 230, 170, 143, 34, 79, 252, 20, 203, 130, 85, 26, 52, 198, 230, 184, 144, 123, 105, 208, 17, 231, 101, 215, 110, 78, 111, 87]), - ([60, 28, 174, 193, 77, 219, 18, 137, 54, 176, 181, 83, 162, 103, 4, 95, 136, 122, 225, 129, 62, 64, 76, 48, 113, 185, 245, 202, 255, 141, 21, 245], [227, 131, 158, 118, 221, 169, 156, 73, 181, 165, 236, 78, 111, 31, 30, 247, 123, 73, 73, 242, 95, 43, 251, 84, 98, 197, 119, 219, 1, 44, 160, 70], [47, 182, 170, 160, 160, 193, 34, 54, 76, 107, 79, 105, 212, 116, 27, 65, 183, 79, 177, 54, 120, 211, 199, 1, 145, 112, 34, 105, 188, 48, 147, 14]), - ([107, 211, 65, 87, 173, 227, 27, 14, 55, 230, 28, 135, 252, 57, 10, 225, 150, 103, 131, 163, 243, 193, 121, 163, 28, 181, 175, 128, 26, 120, 149, 11], [32, 133, 68, 145, 77, 218, 143, 140, 175, 51, 76, 13, 76, 113, 157, 234, 150, 25, 68, 123, 203, 67, 119, 122, 96, 49, 184, 25, 124, 77, 143, 218], [24, 118, 176, 78, 93, 8, 29, 180, 41, 206, 137, 158, 178, 20, 44, 66, 183, 42, 141, 62, 197, 46, 132, 177, 171, 186, 19, 39, 187, 237, 7, 111]), - ([115, 10, 106, 207, 79, 253, 160, 44, 125, 91, 0, 232, 91, 252, 166, 183, 158, 154, 3, 151, 243, 28, 245, 2, 156, 188, 201, 138, 197, 147, 244, 3], [244, 130, 148, 152, 227, 34, 148, 173, 210, 8, 46, 255, 62, 119, 147, 142, 239, 180, 138, 89, 66, 195, 124, 144, 69, 34, 255, 118, 1, 251, 174, 173], [34, 242, 49, 109, 176, 226, 189, 4, 128, 3, 126, 141, 102, 0, 97, 215, 120, 121, 52, 38, 195, 142, 186, 155, 107, 218, 18, 85, 47, 110, 29, 228]), - ([42, 189, 9, 120, 18, 164, 169, 55, 226, 46, 28, 142, 198, 228, 227, 28, 128, 175, 154, 33, 168, 49, 176, 172, 147, 57, 71, 2, 246, 47, 119, 186], [208, 128, 126, 7, 21, 155, 51, 14, 159, 59, 11, 5, 123, 253, 119, 234, 182, 141, 65, 49, 129, 133, 8, 97, 248, 221, 66, 231, 196, 96, 215, 126], [194, 49, 3, 173, 44, 253, 180, 226, 108, 223, 87, 65, 71, 227, 200, 175, 7, 24, 2, 136, 200, 33, 213, 111, 188, 3, 170, 156, 108, 126, 199, 189]), - ([134, 62, 12, 173, 102, 52, 69, 239, 89, 173, 148, 185, 24, 23, 217, 125, 87, 127, 196, 131, 31, 167, 123, 37, 16, 198, 84, 189, 53, 189, 29, 225], [93, 179, 118, 184, 163, 249, 55, 197, 117, 78, 243, 98, 86, 76, 128, 127, 52, 189, 4, 240, 90, 196, 15, 162, 158, 125, 207, 196, 49, 193, 113, 110], [1, 187, 37, 135, 77, 133, 224, 180, 247, 59, 183, 69, 13, 200, 83, 7, 188, 128, 222, 18, 44, 147, 138, 10, 234, 71, 247, 126, 146, 139, 61, 154]), - ([6, 10, 0, 36, 25, 16, 41, 106, 254, 222, 164, 170, 189, 165, 129, 233, 74, 238, 209, 92, 118, 11, 238, 179, 132, 70, 126, 102, 191, 211, 202, 215], [201, 180, 1, 205, 120, 151, 199, 245, 92, 9, 120, 152, 234, 96, 200, 7, 27, 216, 148, 201, 70, 43, 100, 43, 214, 252, 58, 225, 5, 97, 184, 195], [51, 155, 58, 213, 3, 188, 210, 221, 234, 141, 184, 107, 233, 175, 200, 96, 200, 4, 36, 186, 199, 219, 14, 60, 20, 184, 137, 89, 28, 65, 45, 173]), - ([25, 253, 15, 179, 15, 157, 57, 99, 140, 95, 181, 244, 113, 33, 3, 205, 78, 113, 87, 224, 103, 57, 76, 53, 130, 123, 51, 12, 146, 141, 234, 143], [217, 106, 226, 226, 139, 119, 145, 82, 190, 6, 112, 195, 157, 248, 149, 26, 138, 67, 118, 202, 136, 188, 135, 252, 34, 105, 243, 92, 96, 186, 170, 133], [150, 27, 232, 13, 172, 56, 135, 216, 88, 26, 115, 52, 97, 198, 77, 190, 7, 102, 126, 192, 15, 230, 222, 239, 243, 66, 183, 202, 244, 0, 116, 72]), - ([24, 184, 244, 191, 98, 238, 161, 60, 212, 77, 131, 107, 47, 142, 150, 231, 172, 232, 110, 73, 145, 34, 111, 26, 172, 131, 179, 99, 84, 183, 187, 21], [236, 236, 82, 100, 77, 175, 207, 222, 120, 136, 94, 32, 217, 183, 181, 238, 43, 133, 96, 4, 210, 236, 233, 241, 184, 48, 32, 214, 48, 244, 66, 234], [14, 142, 71, 26, 83, 212, 254, 132, 200, 143, 14, 126, 243, 125, 147, 245, 119, 160, 79, 216, 68, 162, 193, 122, 75, 24, 91, 22, 91, 228, 255, 244]), - ([182, 29, 251, 223, 14, 213, 49, 49, 77, 101, 181, 146, 240, 234, 90, 149, 73, 97, 171, 125, 52, 250, 200, 212, 78, 216, 245, 68, 88, 77, 142, 104], [194, 51, 243, 192, 8, 188, 81, 34, 47, 16, 242, 17, 191, 181, 113, 142, 112, 6, 171, 2, 27, 250, 7, 27, 203, 79, 144, 147, 41, 123, 195, 184], [108, 192, 138, 57, 61, 137, 73, 145, 103, 174, 231, 172, 177, 114, 188, 82, 203, 4, 16, 178, 139, 251, 112, 163, 240, 84, 52, 149, 113, 42, 252, 0]), - ([156, 0, 231, 76, 30, 159, 199, 94, 223, 2, 111, 46, 144, 54, 98, 102, 34, 237, 33, 178, 36, 86, 141, 194, 189, 248, 252, 251, 230, 201, 89, 124], [47, 235, 152, 1, 15, 146, 31, 150, 201, 93, 2, 58, 130, 82, 30, 235, 12, 145, 205, 90, 102, 111, 240, 249, 246, 49, 74, 239, 192, 212, 34, 57], [58, 2, 105, 151, 31, 133, 165, 136, 2, 174, 156, 254, 0, 146, 250, 74, 14, 190, 148, 81, 78, 99, 140, 66, 35, 71, 133, 244, 221, 196, 10, 93]), - ([70, 193, 40, 218, 223, 227, 140, 150, 32, 164, 13, 76, 125, 168, 175, 167, 178, 253, 189, 13, 86, 66, 203, 12, 104, 40, 104, 96, 223, 4, 136, 198], [239, 20, 139, 250, 1, 102, 209, 158, 61, 142, 151, 191, 190, 152, 15, 102, 117, 37, 175, 146, 207, 155, 197, 249, 251, 48, 137, 81, 6, 64, 31, 26], [198, 240, 187, 31, 170, 122, 230, 103, 177, 207, 191, 18, 26, 133, 149, 196, 24, 238, 76, 184, 205, 193, 167, 205, 151, 142, 145, 211, 81, 78, 5, 158]), - ([164, 233, 117, 8, 7, 196, 138, 200, 134, 92, 161, 211, 201, 141, 206, 208, 211, 0, 103, 64, 123, 221, 86, 145, 125, 233, 207, 193, 192, 58, 132, 31], [11, 170, 117, 102, 11, 73, 109, 207, 137, 120, 222, 252, 41, 132, 253, 193, 142, 103, 104, 180, 111, 56, 22, 68, 27, 89, 155, 67, 128, 189, 104, 23], [188, 236, 186, 160, 156, 34, 7, 49, 161, 220, 33, 32, 101, 208, 168, 8, 156, 36, 214, 58, 74, 102, 205, 165, 212, 73, 122, 47, 95, 16, 212, 18]), - ([11, 49, 186, 130, 169, 13, 61, 1, 168, 214, 201, 230, 91, 31, 60, 76, 164, 7, 101, 144, 108, 179, 212, 79, 215, 241, 153, 34, 58, 47, 70, 94], [186, 212, 202, 149, 230, 113, 134, 218, 65, 110, 175, 254, 73, 79, 246, 238, 184, 228, 53, 21, 201, 111, 194, 213, 250, 243, 18, 250, 65, 57, 57, 23], [216, 95, 249, 98, 201, 23, 188, 146, 166, 183, 71, 150, 55, 126, 197, 108, 254, 92, 105, 106, 139, 13, 166, 89, 116, 19, 217, 186, 166, 228, 97, 100]), - ([1, 51, 217, 181, 27, 162, 152, 22, 0, 171, 37, 92, 171, 127, 173, 211, 252, 102, 86, 110, 38, 6, 58, 35, 132, 149, 35, 40, 97, 112, 128, 66], [6, 214, 84, 108, 177, 115, 84, 41, 221, 178, 36, 93, 105, 210, 13, 191, 95, 238, 226, 211, 168, 23, 222, 210, 57, 87, 204, 236, 137, 203, 78, 70], [233, 28, 77, 91, 129, 125, 134, 142, 240, 201, 226, 238, 122, 98, 3, 237, 181, 188, 35, 115, 205, 215, 105, 184, 198, 84, 132, 12, 145, 107, 22, 32]), - ([48, 101, 149, 177, 160, 20, 207, 44, 240, 52, 144, 251, 42, 77, 59, 187, 152, 171, 249, 205, 104, 94, 161, 187, 191, 54, 164, 71, 125, 213, 108, 91], [203, 224, 200, 252, 130, 250, 9, 230, 105, 199, 27, 249, 198, 249, 17, 67, 99, 3, 144, 74, 170, 38, 26, 58, 134, 90, 195, 121, 46, 57, 31, 63], [241, 172, 251, 158, 60, 67, 54, 246, 213, 40, 170, 48, 131, 168, 112, 205, 153, 123, 204, 120, 182, 104, 235, 152, 38, 124, 35, 160, 58, 85, 127, 149]), - ([127, 203, 214, 209, 86, 3, 143, 109, 221, 220, 240, 175, 15, 123, 43, 174, 114, 212, 61, 144, 114, 14, 238, 12, 44, 87, 229, 32, 62, 48, 238, 244], [212, 1, 167, 28, 181, 83, 121, 219, 73, 226, 137, 58, 156, 166, 219, 53, 223, 182, 139, 0, 65, 142, 32, 190, 128, 172, 130, 107, 108, 123, 127, 66], [30, 113, 179, 96, 250, 4, 175, 75, 88, 116, 115, 205, 85, 29, 36, 97, 97, 206, 13, 84, 219, 226, 215, 245, 82, 71, 100, 28, 109, 153, 166, 41]), - ([155, 236, 19, 62, 208, 10, 60, 137, 215, 47, 116, 161, 233, 247, 239, 201, 108, 220, 235, 89, 145, 72, 255, 229, 33, 153, 178, 237, 146, 62, 174, 52], [46, 181, 9, 136, 93, 236, 182, 207, 139, 189, 48, 186, 117, 149, 147, 88, 165, 195, 86, 107, 105, 254, 159, 245, 232, 148, 9, 97, 186, 191, 166, 37], [158, 52, 153, 121, 175, 201, 99, 223, 241, 178, 172, 60, 224, 122, 222, 87, 31, 25, 131, 139, 209, 135, 78, 42, 237, 12, 101, 118, 185, 87, 139, 100]), - ([167, 188, 96, 103, 143, 26, 218, 92, 255, 163, 221, 60, 107, 227, 170, 58, 125, 228, 75, 25, 172, 67, 100, 225, 157, 171, 169, 156, 159, 148, 92, 175], [5, 133, 176, 95, 96, 150, 94, 52, 131, 199, 191, 101, 159, 113, 194, 76, 107, 102, 119, 55, 0, 55, 2, 153, 9, 157, 24, 202, 249, 151, 85, 142], [127, 109, 8, 66, 241, 196, 0, 23, 231, 154, 201, 68, 211, 246, 76, 71, 153, 149, 79, 26, 208, 7, 79, 146, 104, 35, 129, 65, 245, 17, 74, 249]), - ([207, 201, 114, 76, 252, 125, 175, 152, 176, 182, 165, 212, 56, 63, 49, 174, 44, 186, 251, 78, 123, 255, 152, 42, 191, 153, 36, 135, 132, 2, 102, 109], [24, 64, 15, 193, 87, 214, 204, 192, 52, 127, 102, 19, 154, 168, 114, 62, 100, 140, 144, 201, 142, 139, 189, 78, 110, 223, 8, 55, 30, 185, 134, 238], [100, 155, 22, 23, 183, 228, 122, 206, 160, 82, 87, 105, 166, 195, 92, 145, 184, 46, 17, 5, 184, 3, 237, 254, 234, 103, 46, 135, 104, 95, 68, 208]), - ([225, 127, 99, 112, 148, 153, 93, 182, 124, 139, 183, 95, 44, 162, 254, 94, 1, 169, 38, 6, 151, 215, 81, 246, 191, 188, 50, 73, 168, 4, 109, 1], [128, 246, 225, 64, 13, 76, 122, 91, 93, 1, 69, 16, 114, 193, 88, 203, 31, 131, 36, 197, 93, 26, 160, 3, 168, 198, 126, 172, 137, 121, 91, 134], [212, 245, 228, 72, 207, 238, 118, 238, 87, 178, 159, 25, 47, 163, 183, 181, 230, 100, 192, 31, 234, 83, 52, 173, 47, 172, 230, 55, 11, 167, 84, 12]), - ([247, 78, 93, 39, 56, 67, 4, 81, 213, 192, 22, 183, 6, 88, 231, 24, 128, 80, 239, 240, 96, 149, 231, 108, 48, 9, 211, 111, 41, 40, 43, 163], [169, 161, 187, 134, 250, 82, 137, 40, 179, 4, 137, 233, 197, 132, 81, 216, 6, 152, 69, 207, 216, 53, 10, 179, 1, 36, 99, 104, 121, 222, 179, 207], [13, 175, 3, 222, 125, 95, 136, 172, 250, 7, 126, 238, 198, 254, 223, 189, 163, 222, 55, 63, 154, 159, 73, 231, 73, 119, 232, 68, 190, 200, 86, 134]), - ([38, 93, 146, 213, 173, 240, 29, 255, 187, 247, 58, 47, 227, 138, 165, 239, 56, 27, 221, 160, 108, 130, 67, 115, 118, 69, 247, 102, 69, 135, 49, 94], [120, 67, 170, 92, 144, 11, 148, 72, 175, 109, 193, 111, 98, 214, 247, 250, 35, 126, 186, 126, 135, 55, 80, 110, 4, 239, 0, 37, 214, 247, 189, 24], [33, 123, 43, 104, 78, 67, 131, 212, 179, 160, 37, 120, 123, 65, 56, 230, 160, 194, 193, 183, 101, 190, 90, 139, 33, 173, 239, 250, 216, 70, 233, 171]), - ([61, 165, 226, 160, 202, 223, 135, 82, 150, 162, 143, 16, 78, 42, 214, 187, 213, 8, 124, 170, 126, 115, 210, 120, 174, 219, 251, 26, 241, 4, 83, 13], [148, 249, 248, 155, 198, 141, 186, 3, 149, 18, 237, 166, 4, 71, 158, 111, 189, 62, 73, 231, 205, 217, 43, 246, 56, 45, 41, 218, 236, 0, 169, 251], [73, 22, 88, 119, 159, 146, 133, 15, 117, 156, 48, 175, 40, 50, 76, 149, 88, 72, 145, 18, 101, 180, 85, 99, 202, 170, 211, 37, 251, 234, 188, 61]), - ([134, 129, 118, 82, 194, 145, 226, 246, 139, 43, 156, 14, 210, 117, 43, 151, 233, 11, 167, 166, 175, 66, 52, 133, 124, 38, 148, 244, 99, 78, 96, 133], [88, 206, 254, 44, 109, 90, 242, 64, 27, 66, 59, 166, 150, 110, 194, 46, 35, 253, 27, 27, 226, 120, 99, 99, 75, 114, 32, 24, 195, 181, 99, 53], [58, 191, 34, 120, 122, 251, 23, 171, 156, 103, 240, 33, 146, 43, 139, 143, 231, 120, 79, 60, 236, 128, 63, 62, 66, 149, 134, 224, 29, 192, 0, 92]), - ([73, 224, 84, 90, 110, 252, 174, 53, 163, 64, 34, 253, 82, 106, 67, 155, 191, 61, 236, 29, 192, 147, 121, 96, 199, 36, 129, 112, 121, 71, 170, 25], [239, 207, 1, 81, 168, 123, 151, 189, 73, 134, 139, 86, 65, 153, 105, 109, 187, 193, 92, 177, 34, 18, 100, 127, 24, 169, 210, 100, 171, 81, 166, 93], [89, 113, 156, 239, 209, 176, 141, 82, 199, 188, 194, 201, 196, 71, 2, 32, 86, 222, 196, 166, 162, 64, 117, 50, 220, 118, 204, 210, 182, 162, 13, 174]), - ([42, 229, 76, 7, 132, 249, 150, 105, 93, 218, 253, 223, 181, 139, 27, 228, 162, 139, 135, 92, 208, 180, 59, 32, 220, 9, 231, 234, 213, 88, 251, 67], [58, 109, 204, 74, 98, 183, 97, 172, 239, 24, 164, 212, 21, 56, 192, 170, 20, 205, 54, 102, 139, 249, 143, 14, 22, 142, 251, 111, 95, 220, 11, 166], [3, 157, 190, 43, 18, 149, 162, 159, 46, 147, 20, 59, 109, 234, 100, 70, 237, 136, 41, 234, 96, 143, 104, 231, 67, 45, 242, 142, 198, 147, 167, 248]), - ([66, 215, 63, 51, 174, 170, 106, 28, 126, 239, 221, 24, 215, 207, 217, 98, 134, 73, 60, 42, 15, 74, 34, 108, 15, 253, 63, 138, 49, 199, 137, 186], [14, 63, 87, 49, 129, 182, 60, 197, 228, 142, 121, 203, 11, 52, 236, 173, 184, 87, 212, 97, 184, 89, 109, 46, 82, 29, 120, 148, 99, 109, 183, 106], [106, 234, 153, 98, 123, 22, 144, 249, 238, 55, 23, 238, 36, 209, 180, 113, 163, 18, 33, 202, 236, 157, 172, 105, 232, 141, 61, 128, 70, 213, 109, 35]), - ([124, 71, 19, 31, 54, 190, 116, 153, 227, 162, 166, 124, 67, 94, 190, 13, 200, 142, 43, 98, 66, 30, 135, 175, 221, 56, 180, 11, 141, 97, 178, 217], [117, 97, 155, 201, 18, 91, 209, 156, 106, 16, 58, 107, 175, 235, 29, 24, 50, 16, 53, 55, 7, 246, 68, 163, 161, 101, 219, 145, 2, 3, 49, 23], [165, 102, 151, 110, 207, 245, 191, 142, 35, 130, 62, 86, 46, 139, 123, 157, 93, 231, 195, 152, 174, 59, 203, 24, 140, 228, 111, 126, 67, 176, 212, 105]), - ([125, 91, 107, 117, 112, 61, 212, 236, 70, 71, 203, 11, 135, 64, 251, 73, 187, 10, 10, 148, 199, 151, 13, 213, 246, 53, 149, 221, 121, 30, 250, 210], [17, 182, 122, 168, 52, 195, 78, 210, 229, 165, 196, 39, 230, 103, 65, 129, 252, 164, 162, 15, 172, 37, 197, 15, 211, 6, 1, 91, 129, 213, 42, 120], [133, 239, 244, 216, 48, 1, 182, 106, 125, 191, 179, 82, 240, 90, 73, 79, 78, 28, 231, 171, 139, 155, 207, 251, 173, 48, 0, 98, 145, 97, 86, 134]), - ([104, 87, 71, 7, 237, 252, 140, 193, 184, 249, 66, 77, 140, 166, 223, 250, 106, 213, 89, 84, 13, 175, 48, 252, 129, 92, 196, 255, 105, 114, 166, 172], [107, 44, 151, 161, 29, 65, 166, 163, 37, 255, 157, 248, 137, 183, 183, 197, 35, 147, 27, 246, 173, 176, 225, 134, 221, 116, 201, 190, 72, 170, 225, 30], [55, 49, 116, 95, 15, 6, 106, 74, 247, 39, 48, 36, 232, 29, 100, 107, 112, 100, 20, 168, 144, 9, 174, 55, 122, 25, 45, 19, 76, 210, 168, 143]), - ([153, 235, 190, 211, 173, 192, 142, 247, 26, 197, 246, 158, 51, 2, 44, 205, 68, 57, 94, 237, 75, 167, 180, 123, 255, 241, 6, 143, 161, 247, 60, 86], [189, 42, 153, 50, 49, 10, 172, 238, 174, 185, 30, 191, 9, 3, 237, 243, 104, 147, 195, 225, 116, 228, 218, 134, 146, 147, 133, 117, 213, 91, 48, 94], [75, 23, 236, 202, 211, 127, 35, 133, 30, 178, 176, 230, 194, 142, 73, 59, 138, 189, 44, 86, 95, 162, 37, 56, 162, 98, 33, 187, 222, 73, 191, 38]), - ([214, 155, 79, 217, 55, 27, 250, 118, 49, 107, 228, 63, 192, 71, 53, 100, 221, 15, 170, 241, 48, 106, 180, 137, 144, 70, 9, 36, 94, 241, 60, 207], [142, 183, 48, 186, 248, 197, 53, 242, 254, 58, 131, 41, 6, 4, 150, 141, 221, 68, 68, 23, 29, 73, 22, 236, 1, 120, 219, 198, 184, 33, 231, 231], [37, 96, 159, 217, 235, 227, 44, 140, 162, 166, 208, 161, 31, 21, 215, 106, 184, 99, 60, 237, 157, 230, 137, 126, 95, 151, 143, 61, 4, 68, 104, 164]), - ([236, 254, 222, 224, 230, 116, 219, 147, 186, 233, 54, 196, 175, 160, 79, 223, 107, 150, 5, 81, 62, 209, 96, 85, 55, 0, 21, 175, 207, 108, 132, 36], [91, 252, 139, 101, 136, 140, 201, 245, 130, 238, 136, 37, 10, 40, 246, 67, 104, 16, 254, 141, 90, 246, 53, 171, 151, 225, 121, 43, 71, 54, 10, 165], [140, 12, 230, 0, 72, 140, 161, 124, 39, 173, 246, 207, 178, 141, 134, 128, 83, 156, 132, 18, 107, 188, 124, 229, 79, 51, 48, 137, 111, 89, 135, 160]), - ([113, 77, 121, 185, 67, 23, 66, 229, 19, 186, 85, 47, 81, 131, 217, 246, 125, 90, 205, 206, 135, 84, 177, 144, 3, 129, 101, 243, 77, 47, 69, 7], [159, 148, 82, 14, 237, 144, 194, 168, 163, 32, 51, 58, 60, 63, 54, 55, 205, 21, 138, 181, 253, 253, 84, 43, 203, 114, 16, 2, 9, 234, 70, 81], [147, 101, 229, 180, 213, 251, 40, 224, 209, 229, 72, 192, 124, 224, 207, 104, 224, 175, 94, 168, 14, 174, 78, 129, 116, 32, 168, 42, 218, 95, 210, 18]), - ([151, 14, 136, 217, 152, 105, 37, 247, 64, 226, 131, 87, 251, 91, 17, 74, 25, 245, 150, 50, 65, 225, 18, 203, 121, 138, 228, 188, 162, 21, 110, 120], [227, 67, 32, 205, 67, 202, 89, 172, 196, 71, 163, 67, 105, 177, 25, 77, 68, 173, 201, 131, 153, 51, 212, 211, 143, 234, 44, 196, 198, 120, 99, 189], [196, 245, 112, 247, 198, 125, 143, 133, 134, 155, 26, 54, 94, 108, 101, 9, 192, 169, 11, 66, 159, 59, 118, 94, 112, 83, 154, 189, 7, 26, 210, 245]), - ([26, 250, 53, 136, 41, 39, 92, 63, 195, 200, 187, 184, 72, 102, 252, 140, 139, 195, 58, 245, 61, 84, 201, 22, 239, 190, 1, 52, 216, 68, 129, 29], [108, 11, 207, 62, 69, 54, 89, 126, 118, 82, 239, 27, 208, 137, 216, 80, 110, 98, 185, 175, 120, 30, 118, 88, 207, 77, 6, 50, 204, 141, 0, 56], [229, 106, 141, 185, 68, 80, 96, 128, 199, 100, 4, 238, 193, 106, 160, 143, 104, 76, 163, 230, 72, 34, 29, 22, 105, 56, 176, 232, 75, 56, 121, 237]), - ([115, 109, 225, 5, 58, 242, 142, 48, 252, 177, 191, 21, 62, 83, 235, 213, 195, 172, 49, 13, 232, 10, 252, 194, 255, 61, 54, 61, 103, 0, 163, 215], [24, 38, 64, 140, 3, 208, 250, 38, 189, 31, 101, 239, 102, 208, 234, 37, 137, 86, 120, 27, 244, 92, 242, 32, 215, 232, 247, 207, 20, 160, 135, 225], [17, 78, 166, 79, 217, 162, 184, 229, 116, 253, 15, 2, 51, 101, 159, 41, 46, 230, 17, 228, 160, 95, 167, 153, 46, 90, 100, 1, 247, 212, 130, 18]), - ([208, 12, 83, 60, 151, 222, 197, 24, 127, 22, 125, 11, 60, 20, 155, 137, 22, 154, 166, 165, 173, 16, 203, 134, 207, 151, 126, 2, 95, 54, 66, 214], [58, 107, 50, 43, 89, 202, 204, 164, 40, 218, 106, 248, 105, 254, 246, 96, 177, 85, 146, 42, 239, 170, 55, 19, 213, 71, 219, 37, 237, 129, 17, 240], [192, 131, 212, 113, 89, 120, 121, 14, 131, 184, 17, 11, 106, 209, 138, 194, 6, 46, 251, 128, 115, 190, 78, 74, 247, 247, 133, 234, 128, 170, 55, 21]), - ([104, 51, 136, 239, 189, 133, 98, 24, 222, 132, 10, 122, 113, 192, 27, 10, 181, 163, 186, 118, 96, 242, 180, 136, 102, 135, 94, 102, 25, 232, 216, 48], [182, 114, 104, 141, 237, 20, 189, 1, 59, 191, 109, 224, 40, 185, 72, 139, 62, 178, 186, 59, 76, 178, 192, 210, 152, 81, 37, 44, 137, 242, 237, 105], [106, 216, 125, 65, 242, 253, 176, 157, 148, 222, 134, 164, 110, 243, 2, 222, 143, 199, 85, 128, 11, 67, 219, 109, 125, 224, 182, 76, 186, 62, 0, 179]), - ([133, 23, 182, 94, 140, 187, 41, 122, 203, 234, 113, 42, 111, 160, 210, 250, 219, 11, 57, 113, 238, 48, 190, 240, 70, 24, 105, 17, 32, 64, 142, 135], [177, 130, 179, 134, 255, 105, 134, 55, 19, 7, 227, 157, 194, 83, 60, 15, 163, 121, 91, 147, 73, 254, 119, 61, 97, 3, 172, 12, 167, 85, 39, 53], [83, 191, 191, 38, 47, 224, 85, 147, 245, 174, 25, 152, 24, 193, 27, 154, 128, 93, 136, 34, 87, 171, 224, 246, 196, 111, 215, 15, 208, 140, 2, 59]), - ([181, 211, 68, 72, 60, 29, 116, 128, 195, 45, 3, 155, 124, 115, 8, 196, 16, 194, 39, 232, 201, 123, 78, 92, 246, 96, 253, 70, 235, 125, 69, 206], [157, 33, 69, 12, 136, 4, 46, 127, 154, 159, 30, 7, 171, 124, 65, 166, 27, 36, 55, 201, 137, 142, 112, 64, 242, 180, 175, 119, 177, 11, 78, 158], [250, 210, 177, 197, 83, 79, 54, 219, 40, 147, 10, 209, 165, 79, 13, 128, 203, 145, 243, 34, 183, 154, 40, 156, 178, 215, 250, 23, 51, 180, 209, 149]), - ([218, 128, 195, 2, 218, 88, 117, 165, 113, 187, 237, 76, 236, 252, 3, 155, 233, 93, 93, 112, 70, 217, 125, 241, 114, 211, 251, 251, 17, 20, 131, 228], [29, 29, 105, 25, 243, 135, 10, 215, 176, 130, 122, 177, 65, 124, 28, 244, 37, 145, 192, 255, 175, 147, 154, 95, 118, 100, 186, 216, 245, 8, 215, 207], [68, 84, 187, 149, 190, 24, 56, 245, 35, 19, 8, 200, 8, 157, 24, 160, 192, 162, 164, 135, 186, 211, 133, 67, 123, 36, 112, 156, 205, 195, 17, 141]), - ([231, 206, 109, 216, 141, 221, 57, 136, 105, 246, 114, 82, 191, 144, 252, 31, 34, 214, 124, 83, 91, 55, 207, 55, 184, 163, 70, 134, 44, 199, 136, 3], [112, 130, 131, 95, 234, 111, 61, 127, 131, 251, 45, 243, 63, 235, 98, 42, 241, 79, 186, 196, 178, 4, 224, 159, 69, 190, 129, 157, 150, 254, 222, 205], [76, 39, 224, 141, 82, 141, 182, 24, 124, 162, 173, 24, 77, 146, 12, 236, 30, 123, 50, 168, 82, 61, 119, 248, 149, 240, 180, 117, 11, 85, 191, 72]), - ([20, 220, 60, 1, 146, 13, 229, 31, 99, 196, 29, 119, 194, 99, 192, 152, 178, 195, 106, 62, 74, 23, 72, 174, 4, 24, 33, 68, 193, 249, 153, 131], [137, 182, 24, 88, 166, 181, 183, 28, 29, 225, 13, 148, 81, 30, 68, 196, 229, 135, 76, 238, 59, 152, 68, 42, 82, 147, 39, 180, 163, 227, 49, 93], [149, 17, 247, 176, 209, 224, 132, 162, 82, 38, 196, 227, 49, 109, 254, 92, 1, 252, 167, 178, 215, 204, 6, 193, 98, 39, 211, 62, 102, 212, 2, 185]), - ([127, 61, 50, 95, 9, 172, 55, 55, 149, 251, 199, 131, 38, 54, 172, 220, 156, 202, 190, 116, 246, 221, 114, 205, 154, 100, 155, 129, 6, 183, 22, 160], [118, 229, 189, 78, 251, 125, 35, 246, 68, 172, 103, 136, 109, 20, 61, 161, 220, 226, 106, 243, 165, 192, 61, 48, 207, 163, 87, 93, 112, 161, 177, 138], [148, 237, 13, 66, 189, 177, 250, 243, 178, 155, 90, 139, 83, 5, 92, 92, 4, 50, 24, 195, 114, 210, 167, 102, 11, 98, 151, 236, 22, 117, 243, 228]), - ([148, 33, 246, 153, 134, 122, 131, 81, 173, 100, 76, 155, 113, 8, 51, 79, 63, 54, 32, 95, 98, 10, 84, 151, 152, 55, 159, 58, 23, 79, 37, 206], [220, 82, 90, 84, 166, 89, 128, 246, 105, 72, 89, 226, 100, 27, 253, 238, 148, 39, 168, 174, 144, 49, 239, 30, 175, 112, 136, 190, 36, 85, 59, 169], [36, 36, 148, 39, 180, 29, 174, 144, 51, 67, 46, 170, 239, 34, 27, 24, 59, 52, 37, 252, 199, 245, 70, 190, 255, 64, 220, 70, 207, 230, 81, 10]), - ([13, 240, 126, 43, 227, 253, 72, 216, 247, 54, 225, 59, 196, 71, 222, 57, 203, 28, 13, 136, 13, 110, 71, 12, 203, 214, 98, 214, 210, 193, 25, 126], [246, 5, 39, 196, 146, 200, 35, 38, 21, 95, 53, 28, 135, 174, 103, 26, 60, 148, 40, 243, 230, 124, 218, 154, 244, 56, 204, 8, 168, 87, 229, 216], [73, 118, 249, 94, 251, 26, 213, 94, 56, 82, 58, 68, 45, 66, 188, 49, 189, 202, 141, 212, 207, 18, 28, 12, 11, 169, 217, 94, 229, 159, 234, 212]), - ([6, 27, 228, 183, 77, 103, 229, 186, 78, 206, 77, 45, 231, 31, 59, 145, 57, 110, 79, 149, 229, 211, 134, 124, 136, 3, 248, 21, 243, 29, 250, 192], [61, 101, 156, 141, 136, 172, 29, 247, 54, 211, 80, 15, 175, 168, 170, 22, 102, 43, 3, 230, 224, 65, 234, 55, 224, 162, 225, 196, 169, 155, 183, 123], [206, 16, 152, 199, 114, 227, 105, 222, 219, 142, 230, 86, 164, 186, 228, 12, 7, 160, 31, 10, 168, 123, 208, 218, 137, 47, 92, 240, 110, 181, 220, 210]), - ([111, 117, 101, 25, 54, 15, 141, 150, 217, 96, 105, 217, 190, 33, 176, 255, 160, 221, 59, 255, 41, 41, 173, 62, 212, 167, 156, 102, 133, 147, 142, 176], [138, 135, 215, 42, 23, 175, 25, 174, 43, 138, 179, 12, 5, 182, 4, 118, 51, 84, 190, 163, 31, 237, 81, 239, 15, 37, 219, 121, 177, 229, 5, 181], [29, 190, 72, 233, 86, 28, 44, 21, 137, 106, 227, 78, 193, 221, 214, 2, 86, 35, 163, 214, 74, 229, 45, 109, 47, 102, 203, 245, 178, 173, 191, 215]), - ([122, 66, 84, 53, 251, 174, 251, 39, 71, 30, 85, 165, 34, 110, 178, 253, 4, 61, 253, 65, 178, 142, 10, 195, 122, 89, 89, 222, 94, 109, 18, 106], [160, 124, 128, 167, 37, 76, 152, 156, 79, 225, 70, 52, 66, 163, 9, 162, 77, 195, 249, 214, 101, 137, 219, 100, 11, 28, 231, 177, 171, 88, 67, 219], [91, 63, 80, 243, 26, 203, 67, 12, 34, 154, 68, 60, 224, 198, 188, 13, 165, 198, 131, 161, 11, 179, 0, 195, 201, 247, 10, 194, 40, 41, 249, 97]), - ([162, 215, 70, 8, 250, 5, 164, 149, 11, 106, 159, 0, 183, 247, 247, 31, 138, 19, 214, 28, 7, 155, 168, 224, 191, 7, 241, 185, 0, 168, 158, 193], [234, 211, 17, 41, 116, 10, 40, 236, 60, 195, 70, 98, 60, 40, 255, 63, 221, 146, 139, 71, 228, 43, 179, 242, 18, 152, 247, 178, 140, 158, 117, 12], [214, 165, 16, 35, 199, 39, 252, 205, 161, 100, 0, 14, 150, 187, 153, 180, 165, 189, 10, 255, 213, 169, 5, 175, 244, 157, 186, 58, 58, 21, 209, 78]), - ([181, 218, 187, 152, 193, 195, 150, 211, 92, 74, 179, 160, 143, 235, 5, 224, 152, 134, 106, 198, 97, 241, 220, 2, 223, 14, 134, 11, 141, 227, 255, 87], [67, 128, 71, 7, 170, 21, 12, 212, 60, 254, 60, 212, 72, 124, 13, 152, 199, 64, 42, 190, 161, 16, 158, 248, 125, 43, 254, 82, 94, 88, 1, 248], [176, 28, 221, 7, 166, 44, 62, 39, 147, 112, 50, 3, 92, 177, 55, 18, 240, 26, 30, 12, 143, 82, 178, 64, 184, 151, 184, 219, 156, 104, 224, 43]), - ([34, 174, 137, 13, 106, 163, 43, 10, 10, 77, 47, 115, 151, 154, 184, 225, 76, 9, 127, 237, 248, 217, 248, 146, 238, 163, 40, 135, 83, 32, 137, 136], [155, 141, 172, 10, 171, 73, 204, 71, 38, 5, 204, 81, 118, 133, 140, 160, 207, 219, 173, 188, 6, 223, 254, 201, 90, 164, 43, 121, 134, 147, 177, 164], [193, 208, 141, 68, 65, 179, 171, 237, 69, 128, 203, 96, 112, 109, 254, 125, 116, 60, 121, 169, 198, 7, 237, 75, 48, 147, 99, 143, 155, 18, 181, 6]), - ([80, 246, 173, 195, 114, 110, 216, 58, 211, 187, 188, 119, 95, 47, 159, 219, 124, 184, 215, 2, 148, 212, 136, 255, 35, 177, 76, 227, 158, 25, 111, 98], [172, 248, 253, 201, 247, 175, 237, 105, 245, 219, 220, 201, 243, 206, 189, 58, 214, 85, 209, 173, 221, 186, 219, 54, 169, 44, 185, 40, 105, 6, 247, 162], [77, 228, 177, 144, 82, 190, 157, 245, 154, 140, 49, 70, 124, 160, 32, 182, 106, 47, 9, 1, 251, 219, 166, 213, 124, 207, 231, 133, 48, 78, 142, 169]), - ([55, 110, 157, 149, 86, 207, 218, 62, 94, 108, 205, 144, 49, 193, 55, 62, 245, 0, 92, 138, 112, 94, 145, 70, 39, 13, 15, 222, 66, 218, 176, 133], [164, 27, 115, 230, 91, 254, 150, 13, 218, 78, 180, 243, 115, 105, 98, 185, 121, 155, 132, 164, 146, 156, 60, 126, 8, 172, 234, 190, 197, 196, 230, 157], [49, 34, 121, 14, 175, 99, 135, 217, 203, 64, 29, 144, 228, 28, 250, 97, 109, 223, 240, 110, 241, 208, 157, 14, 69, 25, 255, 123, 0, 7, 184, 164]), - ([148, 101, 68, 59, 189, 50, 244, 246, 122, 204, 98, 253, 73, 246, 91, 228, 220, 226, 152, 133, 28, 19, 187, 199, 219, 26, 85, 119, 37, 87, 106, 50], [53, 250, 43, 60, 24, 217, 246, 165, 22, 122, 184, 138, 206, 156, 12, 218, 80, 29, 20, 157, 179, 183, 74, 247, 146, 53, 93, 249, 187, 138, 205, 211], [40, 25, 113, 237, 128, 98, 32, 114, 12, 43, 28, 74, 25, 79, 37, 3, 165, 164, 230, 248, 123, 121, 250, 46, 82, 1, 246, 92, 202, 100, 16, 136]), - ([104, 91, 13, 175, 5, 129, 30, 5, 253, 235, 54, 39, 255, 38, 15, 105, 70, 251, 62, 35, 152, 45, 113, 225, 203, 59, 33, 93, 68, 22, 75, 31], [252, 184, 169, 194, 163, 58, 138, 153, 64, 179, 187, 185, 51, 67, 68, 68, 15, 37, 154, 190, 110, 65, 138, 166, 50, 230, 254, 37, 78, 170, 64, 40], [202, 65, 211, 25, 28, 82, 27, 53, 107, 54, 173, 253, 124, 38, 190, 125, 168, 58, 109, 246, 69, 60, 190, 135, 83, 109, 26, 207, 238, 203, 78, 239]), - ([78, 238, 18, 72, 5, 63, 248, 76, 167, 23, 67, 3, 101, 14, 230, 80, 181, 99, 100, 120, 175, 220, 17, 76, 18, 78, 146, 245, 19, 211, 246, 99], [220, 95, 235, 29, 236, 223, 65, 236, 104, 164, 146, 253, 177, 192, 30, 87, 207, 108, 56, 88, 155, 27, 68, 129, 68, 102, 162, 193, 248, 136, 88, 143], [115, 160, 181, 24, 2, 73, 215, 19, 232, 200, 123, 41, 49, 25, 164, 204, 64, 168, 216, 6, 46, 210, 116, 67, 217, 119, 95, 111, 38, 47, 45, 109])] - -end Blake3.PureTests +def Blake3.PureTests.vectors : Blake3.PureTests.Vectors := { + reference := "1.8.7", + chunks := [ + { counter := 0, length := 1, cv := "0df1a7881d71d287d0afc2fcd7d23d28f12e401ab858ca267f11c5f1710df315" }, + { counter := 0, length := 63, cv := "7c7a047e4e095a4b48c2951063af35877dbd3d61527b4282b263c16bb0957682" }, + { counter := 0, length := 64, cv := "1f9385c72ab549b20e668af2ad78c9789c011121e837d28414d41c71a736b034" }, + { counter := 0, length := 65, cv := "79e5cac7248e25c874adb8f64f5e76b6692ed481f6c5369204a79b02d7c530ff" }, + { counter := 0, length := 1023, cv := "d57bf986180267d602cbc8ef7c0495fd1520c3700d8bd0952f6a6d892a2e3d26" }, + { counter := 0, length := 1024, cv := "70ce80abaae7c41dd7b57f53a22a747579528721d9c677e35ac79157cec4147f" }, + { counter := 1, length := 1, cv := "43dd211fc52d8b1b5369102b1f9e7120fad4b354848384d2ee798cdaff6669bd" }, + { counter := 1, length := 63, cv := "95fb1cffd9d26444d8e1971cc068f5391b618f6d4e4cc347f32b05102c1bc68e" }, + { counter := 1, length := 64, cv := "36b17c22cd7282bb43b6575ad4b4f2ce12c9233c921db851fbeed79e16947967" }, + { counter := 1, length := 65, cv := "d511a6ab39ea17b01136d7524b5013609acacddb0cd4b98d3f2b453209dff6a7" }, + { counter := 1, length := 1023, cv := "ddb4f3e9333e089748d097dcc455f82a3877cc292f9b033441ef6a32c0c7898c" }, + { counter := 1, length := 1024, cv := "f352c4be0764ea060a449d395388fab17d07b1ddcda6170d414633e1ffae0ef9" }, + { counter := 2, length := 1, cv := "3d96d244f75c56d8e3c20b286c0011ade319ce0f0a7d67eb633b8bcd54b829ff" }, + { counter := 2, length := 63, cv := "1c84f98b9c90ed276e3db25c6261057c5392b2e6a394583dc981cc27e2de8ef2" }, + { counter := 2, length := 64, cv := "6dc87f1ce6b2d342c8f684d028ab40d19251ad8b1d8f16dda81cacd2b832785b" }, + { counter := 2, length := 65, cv := "4ac17f0620cfb170ee1a0e6db1c79c7756be0ed5a56227f80b3802cc130e0ea1" }, + { counter := 2, length := 1023, cv := "07d09eebd1e1e142f6ebce1921d8d2453851d28849b81c908624d48a0f17a1a2" }, + { counter := 2, length := 1024, cv := "458232a6a42997740dc7e0680cc03eb1c70687f1375bc8b2abc4d05d1b177818" }, + { counter := 255, length := 1, cv := "3eb66c6685e2320f001fc26114c0127b9542693e78acc0fbfafaaa536868108c" }, + { counter := 255, length := 63, cv := "6e75932f45186c196814082ef1c668b11dc3e3be5989cd99b47fa7be4ecd7cd6" }, + { counter := 255, length := 64, cv := "dfd74ce6f2d7ee5533e45375dc3813377d1052695dc3286015b38166a13b2785" }, + { counter := 255, length := 65, cv := "14ad0e71d459eb10816251533ff637c3bf25fbea4a3301a72bb7228b6f37ee14" }, + { counter := 255, length := 1023, cv := "0277fb3fdeb68269a24036611fe48ad792576bdffd783c20f3551dc3f1a228ec" }, + { counter := 255, length := 1024, cv := "132e35af93e60e795aaa4844d62d2b253001056535ee6caa03c577cd84dbb88b" }, + { counter := 4294967295, length := 1, cv := "385307a4f1d53aae06906163e2efaa827cf18e364b017f9fd568e52c8568795a" }, + { counter := 4294967295, length := 63, cv := "f3150dd3be39fbe5806bd162f92b01ff046ec7722c9d9a38f7b2a707193f2257" }, + { counter := 4294967295, length := 64, cv := "3608a54deb1a83aa927c50bd1b78d777d956653c0f6471dcb7d2ae461c1c6179" }, + { counter := 4294967295, length := 65, cv := "7f84a8eaa320e703143c0290b4ffde3ec7a2d167a389fcd02b310bc35e722c3f" }, + { counter := 4294967295, length := 1023, cv := "35eea5ef496bb9814b41573e4966e58906df8e8a206026514e8b709364c826fc" }, + { counter := 4294967295, length := 1024, cv := "6f80707cc8ac46a09a46f572e9e6cae2f90829601b9223126a26fd13a8b69181" }, + { counter := 4294967296, length := 1, cv := "ae7520542f9a171de6e3d21d25004ce8954d20eae2484d5d412a2de166d17b8e" }, + { counter := 4294967296, length := 63, cv := "54f0106c4e7e551ea81f16ef108c9f7b5af46e0706263de0614cfac263a3cd2c" }, + { counter := 4294967296, length := 64, cv := "ca8371af9fc1d2bf9c78ce4db7fbe10ae311793c72cd138fb2783753f02fb26c" }, + { counter := 4294967296, length := 65, cv := "f05ba35053d566ce0b5eee6340d1370dfd5c5c0b7c365a3708e5adc58967baaa" }, + { counter := 4294967296, length := 1023, cv := "355dbc837836d54aa44c3af7ea1ec84eaf20acf6e0095344f41f0743f7117296" }, + { counter := 4294967296, length := 1024, cv := "e1aa47c767aa2c6eb4f0393914430f6eb9e352a6f783d9b3b2e787249b25d254" }, + { counter := 18014398509481983, length := 1, cv := "7991dd5ff0f789af0f3faff3f19a72e54936a5189e197805cb8a7d121e2c9376" }, + { counter := 18014398509481983, length := 63, cv := "7864308d48ffc0a6647d50efda76e885b5bf87838f0da964f134eac982e25114" }, + { counter := 18014398509481983, length := 64, cv := "0dba1957653b28378d4ae11921941e920b6b58a544bcdabe320cb7bde636ab3b" }, + { counter := 18014398509481983, length := 65, cv := "14345bc0f9cc0d9c69ae385ace891280974744cb0576629b154a155f76a40dad" }, + { counter := 18014398509481983, length := 1023, cv := "dbef4ba94314324b4b736037b716b7ea39c62d5ddb0c5a54d7485d60c74ba3bc" }, + { counter := 18014398509481983, length := 1024, cv := "ed9d9a80f6485151894127a00176ade150f14f143c1975f824f9a6ba51fd829f" }, + ], + parents := [ + { salt := 0, cv := "9c467ffb7d5eb99d812048cd05b6f587488e741907085678daedaca4f190ffb3", root := "888e69684d2087734c4c14bfd0e57ef4e5a825ae653e3e320e9adddad7976c93", ordinary := "bfc2c2e2a98c1d44a2cd69f93aa429bdb2999121ea2ea1cf4ec4231553b5722c" }, + { salt := 1, cv := "55c74977fec22cadce74bd5947b24bf431b0d315455801dec340d2234d3a43ce", root := "34ec8d58df0ba8af56a9939604fd0accc2e208523f66d2f72dae394fb338d061", ordinary := "452549a6bc4a8e566d73c67baa490479208ebe2d66e95de99a9e32531c852a55" }, + { salt := 2, cv := "e19ac2eb7bea8679dd1d554c55e6c5ae207eaaeba9c266ed36b5bc76a3890ae3", root := "36e7b1b6592730d30c42bf2b63c5790cbe11a6a88125cac0e71c979701529419", ordinary := "586808dddd4dd4997119e60233e3d2149ac9f75aa0e24d0f999bcf143afde3da" }, + { salt := 3, cv := "a56da14467cdef2a05f5e43d55347bfa2253d5113f864394a8a5cc238c9ee8df", root := "2a8b3d500075d15b096db8e03f8e5b8662cb856286a2fcc5d446b56bc57ba698", ordinary := "9afe86d699f1d20ab5abe4ba8072ea3d0b0987a28cc44a0c19af386fff5a0150" }, + { salt := 4, cv := "a37544aefcc1b1883155315475806f78012bbc8a9a08c2751ce15069f18f0440", root := "4ff227519a2b3d5d811cf66f186adace7b43282861d7e99279cff25795f9d38e", ordinary := "1fc40dd97d6214c25dafcea6416f570a47cbabc214307f130ebf4b941490f712" }, + { salt := 5, cv := "783bab83ab0c5c4d6e11befabe7d9ec453c56494f8e2a90eb200ee8701611cf8", root := "6c2a90179bc78ec22cb44b46491d67633c40169dc6581493873804d6e2c409bd", ordinary := "92c60a904be6aa8f224ffc14cb82551a34c6e6b8907b69d011e765d76e4e6f57" }, + { salt := 6, cv := "3c1caec14ddb128936b0b553a267045f887ae1813e404c3071b9f5caff8d15f5", root := "e3839e76dda99c49b5a5ec4e6f1f1ef77b4949f25f2bfb5462c577db012ca046", ordinary := "2fb6aaa0a0c122364c6b4f69d4741b41b74fb13678d3c70191702269bc30930e" }, + { salt := 7, cv := "6bd34157ade31b0e37e61c87fc390ae1966783a3f3c179a31cb5af801a78950b", root := "208544914dda8f8caf334c0d4c719dea9619447bcb43777a6031b8197c4d8fda", ordinary := "1876b04e5d081db429ce899eb2142c42b72a8d3ec52e84b1abba1327bbed076f" }, + { salt := 8, cv := "730a6acf4ffda02c7d5b00e85bfca6b79e9a0397f31cf5029cbcc98ac593f403", root := "f4829498e32294add2082eff3e77938eefb48a5942c37c904522ff7601fbaead", ordinary := "22f2316db0e2bd0480037e8d660061d778793426c38eba9b6bda12552f6e1de4" }, + { salt := 9, cv := "2abd097812a4a937e22e1c8ec6e4e31c80af9a21a831b0ac93394702f62f77ba", root := "d0807e07159b330e9f3b0b057bfd77eab68d413181850861f8dd42e7c460d77e", ordinary := "c23103ad2cfdb4e26cdf574147e3c8af07180288c821d56fbc03aa9c6c7ec7bd" }, + { salt := 10, cv := "863e0cad663445ef59ad94b91817d97d577fc4831fa77b2510c654bd35bd1de1", root := "5db376b8a3f937c5754ef362564c807f34bd04f05ac40fa29e7dcfc431c1716e", ordinary := "01bb25874d85e0b4f73bb7450dc85307bc80de122c938a0aea47f77e928b3d9a" }, + { salt := 11, cv := "060a00241910296afedea4aabda581e94aeed15c760beeb384467e66bfd3cad7", root := "c9b401cd7897c7f55c097898ea60c8071bd894c9462b642bd6fc3ae10561b8c3", ordinary := "339b3ad503bcd2ddea8db86be9afc860c80424bac7db0e3c14b889591c412dad" }, + { salt := 12, cv := "19fd0fb30f9d39638c5fb5f4712103cd4e7157e067394c35827b330c928dea8f", root := "d96ae2e28b779152be0670c39df8951a8a4376ca88bc87fc2269f35c60baaa85", ordinary := "961be80dac3887d8581a733461c64dbe07667ec00fe6deeff342b7caf4007448" }, + { salt := 13, cv := "18b8f4bf62eea13cd44d836b2f8e96e7ace86e4991226f1aac83b36354b7bb15", root := "ecec52644dafcfde78885e20d9b7b5ee2b856004d2ece9f1b83020d630f442ea", ordinary := "0e8e471a53d4fe84c88f0e7ef37d93f577a04fd844a2c17a4b185b165be4fff4" }, + { salt := 14, cv := "b61dfbdf0ed531314d65b592f0ea5a954961ab7d34fac8d44ed8f544584d8e68", root := "c233f3c008bc51222f10f211bfb5718e7006ab021bfa071bcb4f9093297bc3b8", ordinary := "6cc08a393d89499167aee7acb172bc52cb0410b28bfb70a3f0543495712afc00" }, + { salt := 15, cv := "9c00e74c1e9fc75edf026f2e9036626622ed21b224568dc2bdf8fcfbe6c9597c", root := "2feb98010f921f96c95d023a82521eeb0c91cd5a666ff0f9f6314aefc0d42239", ordinary := "3a0269971f85a58802ae9cfe0092fa4a0ebe94514e638c42234785f4ddc40a5d" }, + { salt := 16, cv := "46c128dadfe38c9620a40d4c7da8afa7b2fdbd0d5642cb0c68286860df0488c6", root := "ef148bfa0166d19e3d8e97bfbe980f667525af92cf9bc5f9fb30895106401f1a", ordinary := "c6f0bb1faa7ae667b1cfbf121a8595c418ee4cb8cdc1a7cd978e91d3514e059e" }, + { salt := 17, cv := "a4e9750807c48ac8865ca1d3c98dced0d30067407bdd56917de9cfc1c03a841f", root := "0baa75660b496dcf8978defc2984fdc18e6768b46f3816441b599b4380bd6817", ordinary := "bcecbaa09c220731a1dc212065d0a8089c24d63a4a66cda5d4497a2f5f10d412" }, + { salt := 18, cv := "0b31ba82a90d3d01a8d6c9e65b1f3c4ca40765906cb3d44fd7f199223a2f465e", root := "bad4ca95e67186da416eaffe494ff6eeb8e43515c96fc2d5faf312fa41393917", ordinary := "d85ff962c917bc92a6b74796377ec56cfe5c696a8b0da6597413d9baa6e46164" }, + { salt := 19, cv := "0133d9b51ba2981600ab255cab7fadd3fc66566e26063a238495232861708042", root := "06d6546cb1735429ddb2245d69d20dbf5feee2d3a817ded23957ccec89cb4e46", ordinary := "e91c4d5b817d868ef0c9e2ee7a6203edb5bc2373cdd769b8c654840c916b1620" }, + { salt := 20, cv := "306595b1a014cf2cf03490fb2a4d3bbb98abf9cd685ea1bbbf36a4477dd56c5b", root := "cbe0c8fc82fa09e669c71bf9c6f911436303904aaa261a3a865ac3792e391f3f", ordinary := "f1acfb9e3c4336f6d528aa3083a870cd997bcc78b668eb98267c23a03a557f95" }, + { salt := 21, cv := "7fcbd6d156038f6ddddcf0af0f7b2bae72d43d90720eee0c2c57e5203e30eef4", root := "d401a71cb55379db49e2893a9ca6db35dfb68b00418e20be80ac826b6c7b7f42", ordinary := "1e71b360fa04af4b587473cd551d246161ce0d54dbe2d7f55247641c6d99a629" }, + { salt := 22, cv := "9bec133ed00a3c89d72f74a1e9f7efc96cdceb599148ffe52199b2ed923eae34", root := "2eb509885decb6cf8bbd30ba75959358a5c3566b69fe9ff5e8940961babfa625", ordinary := "9e349979afc963dff1b2ac3ce07ade571f19838bd1874e2aed0c6576b9578b64" }, + { salt := 23, cv := "a7bc60678f1ada5cffa3dd3c6be3aa3a7de44b19ac4364e19daba99c9f945caf", root := "0585b05f60965e3483c7bf659f71c24c6b66773700370299099d18caf997558e", ordinary := "7f6d0842f1c40017e79ac944d3f64c4799954f1ad0074f9268238141f5114af9" }, + { salt := 24, cv := "cfc9724cfc7daf98b0b6a5d4383f31ae2cbafb4e7bff982abf9924878402666d", root := "18400fc157d6ccc0347f66139aa8723e648c90c98e8bbd4e6edf08371eb986ee", ordinary := "649b1617b7e47acea0525769a6c35c91b82e1105b803edfeea672e87685f44d0" }, + { salt := 25, cv := "e17f637094995db67c8bb75f2ca2fe5e01a9260697d751f6bfbc3249a8046d01", root := "80f6e1400d4c7a5b5d01451072c158cb1f8324c55d1aa003a8c67eac89795b86", ordinary := "d4f5e448cfee76ee57b29f192fa3b7b5e664c01fea5334ad2face6370ba7540c" }, + { salt := 26, cv := "f74e5d2738430451d5c016b70658e7188050eff06095e76c3009d36f29282ba3", root := "a9a1bb86fa528928b30489e9c58451d8069845cfd8350ab30124636879deb3cf", ordinary := "0daf03de7d5f88acfa077eeec6fedfbda3de373f9a9f49e74977e844bec85686" }, + { salt := 27, cv := "265d92d5adf01dffbbf73a2fe38aa5ef381bdda06c8243737645f7664587315e", root := "7843aa5c900b9448af6dc16f62d6f7fa237eba7e8737506e04ef0025d6f7bd18", ordinary := "217b2b684e4383d4b3a025787b4138e6a0c2c1b765be5a8b21adeffad846e9ab" }, + { salt := 28, cv := "3da5e2a0cadf875296a28f104e2ad6bbd5087caa7e73d278aedbfb1af104530d", root := "94f9f89bc68dba039512eda604479e6fbd3e49e7cdd92bf6382d29daec00a9fb", ordinary := "491658779f92850f759c30af28324c955848911265b45563caaad325fbeabc3d" }, + { salt := 29, cv := "86817652c291e2f68b2b9c0ed2752b97e90ba7a6af4234857c2694f4634e6085", root := "58cefe2c6d5af2401b423ba6966ec22e23fd1b1be27863634b722018c3b56335", ordinary := "3abf22787afb17ab9c67f021922b8b8fe7784f3cec803f3e429586e01dc0005c" }, + { salt := 30, cv := "49e0545a6efcae35a34022fd526a439bbf3dec1dc0937960c72481707947aa19", root := "efcf0151a87b97bd49868b564199696dbbc15cb12212647f18a9d264ab51a65d", ordinary := "59719cefd1b08d52c7bcc2c9c447022056dec4a6a2407532dc76ccd2b6a20dae" }, + { salt := 31, cv := "2ae54c0784f996695ddafddfb58b1be4a28b875cd0b43b20dc09e7ead558fb43", root := "3a6dcc4a62b761acef18a4d41538c0aa14cd36668bf98f0e168efb6f5fdc0ba6", ordinary := "039dbe2b1295a29f2e93143b6dea6446ed8829ea608f68e7432df28ec693a7f8" }, + { salt := 32, cv := "42d73f33aeaa6a1c7eefdd18d7cfd96286493c2a0f4a226c0ffd3f8a31c789ba", root := "0e3f573181b63cc5e48e79cb0b34ecadb857d461b8596d2e521d7894636db76a", ordinary := "6aea99627b1690f9ee3717ee24d1b471a31221caec9dac69e88d3d8046d56d23" }, + { salt := 33, cv := "7c47131f36be7499e3a2a67c435ebe0dc88e2b62421e87afdd38b40b8d61b2d9", root := "75619bc9125bd19c6a103a6bafeb1d183210353707f644a3a165db9102033117", ordinary := "a566976ecff5bf8e23823e562e8b7b9d5de7c398ae3bcb188ce46f7e43b0d469" }, + { salt := 34, cv := "7d5b6b75703dd4ec4647cb0b8740fb49bb0a0a94c7970dd5f63595dd791efad2", root := "11b67aa834c34ed2e5a5c427e6674181fca4a20fac25c50fd306015b81d52a78", ordinary := "85eff4d83001b66a7dbfb352f05a494f4e1ce7ab8b9bcffbad30006291615686" }, + { salt := 35, cv := "68574707edfc8cc1b8f9424d8ca6dffa6ad559540daf30fc815cc4ff6972a6ac", root := "6b2c97a11d41a6a325ff9df889b7b7c523931bf6adb0e186dd74c9be48aae11e", ordinary := "3731745f0f066a4af7273024e81d646b706414a89009ae377a192d134cd2a88f" }, + { salt := 36, cv := "99ebbed3adc08ef71ac5f69e33022ccd44395eed4ba7b47bfff1068fa1f73c56", root := "bd2a9932310aaceeaeb91ebf0903edf36893c3e174e4da8692938575d55b305e", ordinary := "4b17eccad37f23851eb2b0e6c28e493b8abd2c565fa22538a26221bbde49bf26" }, + { salt := 37, cv := "d69b4fd9371bfa76316be43fc0473564dd0faaf1306ab489904609245ef13ccf", root := "8eb730baf8c535f2fe3a83290604968ddd4444171d4916ec0178dbc6b821e7e7", ordinary := "25609fd9ebe32c8ca2a6d0a11f15d76ab8633ced9de6897e5f978f3d044468a4" }, + { salt := 38, cv := "ecfedee0e674db93bae936c4afa04fdf6b9605513ed16055370015afcf6c8424", root := "5bfc8b65888cc9f582ee88250a28f6436810fe8d5af635ab97e1792b47360aa5", ordinary := "8c0ce600488ca17c27adf6cfb28d8680539c84126bbc7ce54f3330896f5987a0" }, + { salt := 39, cv := "714d79b9431742e513ba552f5183d9f67d5acdce8754b190038165f34d2f4507", root := "9f94520eed90c2a8a320333a3c3f3637cd158ab5fdfd542bcb72100209ea4651", ordinary := "9365e5b4d5fb28e0d1e548c07ce0cf68e0af5ea80eae4e817420a82ada5fd212" }, + { salt := 40, cv := "970e88d9986925f740e28357fb5b114a19f5963241e112cb798ae4bca2156e78", root := "e34320cd43ca59acc447a34369b1194d44adc9839933d4d38fea2cc4c67863bd", ordinary := "c4f570f7c67d8f85869b1a365e6c6509c0a90b429f3b765e70539abd071ad2f5" }, + { salt := 41, cv := "1afa358829275c3fc3c8bbb84866fc8c8bc33af53d54c916efbe0134d844811d", root := "6c0bcf3e4536597e7652ef1bd089d8506e62b9af781e7658cf4d0632cc8d0038", ordinary := "e56a8db944506080c76404eec16aa08f684ca3e648221d166938b0e84b3879ed" }, + { salt := 42, cv := "736de1053af28e30fcb1bf153e53ebd5c3ac310de80afcc2ff3d363d6700a3d7", root := "1826408c03d0fa26bd1f65ef66d0ea258956781bf45cf220d7e8f7cf14a087e1", ordinary := "114ea64fd9a2b8e574fd0f0233659f292ee611e4a05fa7992e5a6401f7d48212" }, + { salt := 43, cv := "d00c533c97dec5187f167d0b3c149b89169aa6a5ad10cb86cf977e025f3642d6", root := "3a6b322b59cacca428da6af869fef660b155922aefaa3713d547db25ed8111f0", ordinary := "c083d4715978790e83b8110b6ad18ac2062efb8073be4e4af7f785ea80aa3715" }, + { salt := 44, cv := "683388efbd856218de840a7a71c01b0ab5a3ba7660f2b48866875e6619e8d830", root := "b672688ded14bd013bbf6de028b9488b3eb2ba3b4cb2c0d29851252c89f2ed69", ordinary := "6ad87d41f2fdb09d94de86a46ef302de8fc755800b43db6d7de0b64cba3e00b3" }, + { salt := 45, cv := "8517b65e8cbb297acbea712a6fa0d2fadb0b3971ee30bef04618691120408e87", root := "b182b386ff6986371307e39dc2533c0fa3795b9349fe773d6103ac0ca7552735", ordinary := "53bfbf262fe05593f5ae199818c11b9a805d882257abe0f6c46fd70fd08c023b" }, + { salt := 46, cv := "b5d344483c1d7480c32d039b7c7308c410c227e8c97b4e5cf660fd46eb7d45ce", root := "9d21450c88042e7f9a9f1e07ab7c41a61b2437c9898e7040f2b4af77b10b4e9e", ordinary := "fad2b1c5534f36db28930ad1a54f0d80cb91f322b79a289cb2d7fa1733b4d195" }, + { salt := 47, cv := "da80c302da5875a571bbed4cecfc039be95d5d7046d97df172d3fbfb111483e4", root := "1d1d6919f3870ad7b0827ab1417c1cf42591c0ffaf939a5f7664bad8f508d7cf", ordinary := "4454bb95be1838f5231308c8089d18a0c0a2a487bad385437b24709ccdc3118d" }, + { salt := 48, cv := "e7ce6dd88ddd398869f67252bf90fc1f22d67c535b37cf37b8a346862cc78803", root := "7082835fea6f3d7f83fb2df33feb622af14fbac4b204e09f45be819d96fedecd", ordinary := "4c27e08d528db6187ca2ad184d920cec1e7b32a8523d77f895f0b4750b55bf48" }, + { salt := 49, cv := "14dc3c01920de51f63c41d77c263c098b2c36a3e4a1748ae04182144c1f99983", root := "89b61858a6b5b71c1de10d94511e44c4e5874cee3b98442a529327b4a3e3315d", ordinary := "9511f7b0d1e084a25226c4e3316dfe5c01fca7b2d7cc06c16227d33e66d402b9" }, + { salt := 50, cv := "7f3d325f09ac373795fbc7832636acdc9ccabe74f6dd72cd9a649b8106b716a0", root := "76e5bd4efb7d23f644ac67886d143da1dce26af3a5c03d30cfa3575d70a1b18a", ordinary := "94ed0d42bdb1faf3b29b5a8b53055c5c043218c372d2a7660b6297ec1675f3e4" }, + { salt := 51, cv := "9421f699867a8351ad644c9b7108334f3f36205f620a549798379f3a174f25ce", root := "dc525a54a65980f6694859e2641bfdee9427a8ae9031ef1eaf7088be24553ba9", ordinary := "24249427b41dae9033432eaaef221b183b3425fcc7f546beff40dc46cfe6510a" }, + { salt := 52, cv := "0df07e2be3fd48d8f736e13bc447de39cb1c0d880d6e470ccbd662d6d2c1197e", root := "f60527c492c82326155f351c87ae671a3c9428f3e67cda9af438cc08a857e5d8", ordinary := "4976f95efb1ad55e38523a442d42bc31bdca8dd4cf121c0c0ba9d95ee59fead4" }, + { salt := 53, cv := "061be4b74d67e5ba4ece4d2de71f3b91396e4f95e5d3867c8803f815f31dfac0", root := "3d659c8d88ac1df736d3500fafa8aa16662b03e6e041ea37e0a2e1c4a99bb77b", ordinary := "ce1098c772e369dedb8ee656a4bae40c07a01f0aa87bd0da892f5cf06eb5dcd2" }, + { salt := 54, cv := "6f756519360f8d96d96069d9be21b0ffa0dd3bff2929ad3ed4a79c6685938eb0", root := "8a87d72a17af19ae2b8ab30c05b604763354bea31fed51ef0f25db79b1e505b5", ordinary := "1dbe48e9561c2c15896ae34ec1ddd6025623a3d64ae52d6d2f66cbf5b2adbfd7" }, + { salt := 55, cv := "7a425435fbaefb27471e55a5226eb2fd043dfd41b28e0ac37a5959de5e6d126a", root := "a07c80a7254c989c4fe1463442a309a24dc3f9d66589db640b1ce7b1ab5843db", ordinary := "5b3f50f31acb430c229a443ce0c6bc0da5c683a10bb300c3c9f70ac22829f961" }, + { salt := 56, cv := "a2d74608fa05a4950b6a9f00b7f7f71f8a13d61c079ba8e0bf07f1b900a89ec1", root := "ead31129740a28ec3cc346623c28ff3fdd928b47e42bb3f21298f7b28c9e750c", ordinary := "d6a51023c727fccda164000e96bb99b4a5bd0affd5a905aff49dba3a3a15d14e" }, + { salt := 57, cv := "b5dabb98c1c396d35c4ab3a08feb05e098866ac661f1dc02df0e860b8de3ff57", root := "43804707aa150cd43cfe3cd4487c0d98c7402abea1109ef87d2bfe525e5801f8", ordinary := "b01cdd07a62c3e27937032035cb13712f01a1e0c8f52b240b897b8db9c68e02b" }, + { salt := 58, cv := "22ae890d6aa32b0a0a4d2f73979ab8e14c097fedf8d9f892eea3288753208988", root := "9b8dac0aab49cc472605cc5176858ca0cfdbadbc06dffec95aa42b798693b1a4", ordinary := "c1d08d4441b3abed4580cb60706dfe7d743c79a9c607ed4b3093638f9b12b506" }, + { salt := 59, cv := "50f6adc3726ed83ad3bbbc775f2f9fdb7cb8d70294d488ff23b14ce39e196f62", root := "acf8fdc9f7afed69f5dbdcc9f3cebd3ad655d1adddbadb36a92cb9286906f7a2", ordinary := "4de4b19052be9df59a8c31467ca020b66a2f0901fbdba6d57ccfe785304e8ea9" }, + { salt := 60, cv := "376e9d9556cfda3e5e6ccd9031c1373ef5005c8a705e9146270d0fde42dab085", root := "a41b73e65bfe960dda4eb4f3736962b9799b84a4929c3c7e08aceabec5c4e69d", ordinary := "3122790eaf6387d9cb401d90e41cfa616ddff06ef1d09d0e4519ff7b0007b8a4" }, + { salt := 61, cv := "9465443bbd32f4f67acc62fd49f65be4dce298851c13bbc7db1a557725576a32", root := "35fa2b3c18d9f6a5167ab88ace9c0cda501d149db3b74af792355df9bb8acdd3", ordinary := "281971ed806220720c2b1c4a194f2503a5a4e6f87b79fa2e5201f65cca641088" }, + { salt := 62, cv := "685b0daf05811e05fdeb3627ff260f6946fb3e23982d71e1cb3b215d44164b1f", root := "fcb8a9c2a33a8a9940b3bbb9334344440f259abe6e418aa632e6fe254eaa4028", ordinary := "ca41d3191c521b356b36adfd7c26be7da83a6df6453cbe87536d1acfeecb4eef" }, + { salt := 63, cv := "4eee1248053ff84ca7174303650ee650b5636478afdc114c124e92f513d3f663", root := "dc5feb1decdf41ec68a492fdb1c01e57cf6c38589b1b44814466a2c1f888588f", ordinary := "73a0b5180249d713e8c87b293119a4cc40a8d8062ed27443d9775f6f262f2d6d" }, + ], +} diff --git a/Tests/Vectors.lean b/Tests/Vectors.lean new file mode 100644 index 0000000..e9ba51d --- /dev/null +++ b/Tests/Vectors.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Argument Computer Corporation. +SPDX-License-Identifier: MIT OR Apache-2.0 +-/ + +/-! Schema for the native component vectors in `Tests/PureVectors.lean`, which +`rust/examples/pure_vectors.rs` generates as one `Vectors` literal. Inputs are +described by their parameters; `Tests/Pure.lean` rebuilds the bytes with the +generator's formula. 32-byte values are lowercase hex strings, as in the +BLAKE3 team's test vectors. -/ + +namespace Blake3.PureTests + +/-- Chaining value of one chunk at an explicit chunk counter. -/ +structure ChunkVector where + counter : Nat + length : Nat + cv : String + +/-- Merges of two 32-byte chaining values derived from `salt`: the internal +parent chaining value, the root hash of the same pair, and the ordinary hash +of their 64-byte concatenation, which must differ from both. -/ +structure ParentVector where + salt : Nat + cv : String + root : String + ordinary : String + +structure Vectors where + /-- Version of the Rust BLAKE3 crate that produced the vectors. -/ + reference : String + chunks : List ChunkVector + parents : List ParentVector + +end Blake3.PureTests diff --git a/lakefile.lean b/lakefile.lean index 1d2146c..06008d6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,7 +19,7 @@ lean_lib Blake3 where lean_exe Blake3Test lean_lib Blake3Tests where - roots := #[`Tests.Pure, `Tests.PureAudit, `Tests.PureVectors] + roots := #[`Tests.Pure, `Tests.PureAudit, `Tests.Vectors, `Tests.PureVectors] -- BLAKE3 C source abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3" diff --git a/rust/examples/pure_vectors.rs b/rust/examples/pure_vectors.rs index 1aca67d..c60ac76 100644 --- a/rust/examples/pure_vectors.rs +++ b/rust/examples/pure_vectors.rs @@ -1,5 +1,11 @@ //! Regenerate Tests/PureVectors.lean with: //! cargo run --locked --release --example pure_vectors > ../Tests/PureVectors.lean +//! +//! The output is one `Blake3.PureTests.Vectors` literal; the schema lives in +//! Tests/Vectors.lean. Only literals are emitted, so the generator needs no +//! knowledge of Lean beyond field names and brackets. + +use std::fmt::Write; use blake3::hazmat::{HasherExt, Mode, merge_subtrees_non_root, merge_subtrees_root}; @@ -9,10 +15,20 @@ fn input(length: usize, salt: usize) -> Vec { .collect() } +fn hex(bytes: &[u8; 32]) -> String { + bytes.iter().fold(String::with_capacity(64), |mut out, byte| { + write!(out, "{byte:02x}").unwrap(); + out + }) +} + fn main() { - println!("/- Generated by rust/examples/pure_vectors.rs using BLAKE3 1.8.7. -/"); - println!("namespace Blake3.PureTests\n"); - println!("def chunkVectors : List (Nat × Nat × List UInt8) := ["); + println!("/- Generated by rust/examples/pure_vectors.rs. Do not edit. -/"); + println!("import Tests.Vectors"); + println!(); + println!("def Blake3.PureTests.vectors : Blake3.PureTests.Vectors := {{"); + println!(" reference := \"1.8.7\","); + println!(" chunks := ["); let counters = [ 0, 1, @@ -22,26 +38,27 @@ fn main() { 1_u64 << 32, (1_u64 << 54) - 1, ]; - for (index, counter) in counters.into_iter().enumerate() { - for (part, length) in [1, 63, 64, 65, 1023, 1024].into_iter().enumerate() { + for counter in counters { + for length in [1, 63, 64, 65, 1023, 1024] { let data = input(length, usize::try_from(counter % 251).unwrap()); let cv = blake3::Hasher::new() .set_input_offset(counter * 1024) .update(&data) .finalize_non_root(); - let separator = if index == 6 && part == 5 { "]" } else { "," }; - println!(" ({counter}, {length}, {cv:?}){separator}"); + let cv = hex(&cv); + println!(" {{ counter := {counter}, length := {length}, cv := \"{cv}\" }},"); } } - println!("\ndef parentVectors : List (List UInt8 × List UInt8 × List UInt8) := ["); + println!(" ],"); + println!(" parents := ["); for salt in 0..64 { let left: [u8; 32] = input(32, salt).try_into().unwrap(); let right: [u8; 32] = input(32, salt + 83).try_into().unwrap(); - let cv = merge_subtrees_non_root(&left, &right, Mode::Hash); - let root = *merge_subtrees_root(&left, &right, Mode::Hash).as_bytes(); - let ordinary = *blake3::hash(&[left, right].concat()).as_bytes(); - let separator = if salt == 63 { "]" } else { "," }; - println!(" ({cv:?}, {root:?}, {ordinary:?}){separator}"); + let cv = hex(&merge_subtrees_non_root(&left, &right, Mode::Hash)); + let root = hex(merge_subtrees_root(&left, &right, Mode::Hash).as_bytes()); + let ordinary = hex(blake3::hash(&[left, right].concat()).as_bytes()); + println!(" {{ salt := {salt}, cv := \"{cv}\", root := \"{root}\", ordinary := \"{ordinary}\" }},"); } - println!("\nend Blake3.PureTests"); + println!(" ],"); + println!("}}"); }