src/crypto/blake/blake2b/blake2b.bend

bend-collections-laws-crypto@1.0.0.0 · 331 lines · 75 definitions

1# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as F
5
6def read31(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
7  (a,w31) = pair
8  (a,F.compress(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31))
9
10def read30(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
11  (a,w30) = pair
12  read31(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))
13
14def read29(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
15  (a,w29) = pair
16  read30(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))
17
18def read28(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
19  (a,w28) = pair
20  read29(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))
21
22def read27(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
23  (a,w27) = pair
24  read28(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))
25
26def read26(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
27  (a,w26) = pair
28  read27(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))
29
30def read25(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
31  (a,w25) = pair
32  read26(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))
33
34def read24(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
35  (a,w24) = pair
36  read25(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))
37
38def read23(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
39  (a,w23) = pair
40  read24(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))
41
42def read22(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
43  (a,w22) = pair
44  read23(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))
45
46def read21(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
47  (a,w21) = pair
48  read22(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))
49
50def read20(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
51  (a,w20) = pair
52  read21(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))
53
54def read19(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
55  (a,w19) = pair
56  read20(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))
57
58def read18(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
59  (a,w18) = pair
60  read19(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))
61
62def read17(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
63  (a,w17) = pair
64  read18(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))
65
66def read16(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
67  (a,w16) = pair
68  read17(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))
69
70def read15(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
71  (a,w15) = pair
72  read16(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
73
74def read14(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
75  (a,w14) = pair
76  read15(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
77
78def read13(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
79  (a,w13) = pair
80  read14(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
81
82def read12(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
83  (a,w12) = pair
84  read13(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
85
86def read11(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
87  (a,w11) = pair
88  read12(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
89
90def read10(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
91  (a,w10) = pair
92  read11(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
93
94def read9(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
95  (a,w9) = pair
96  read10(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
97
98def read8(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
99  (a,w8) = pair
100  read9(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
101
102def read7(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
103  (a,w7) = pair
104  read8(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
105
106def read6(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
107  (a,w6) = pair
108  read7(index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
109
110def read5(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
111  (a,w5) = pair
112  read6(index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
113
114def read4(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
115  (a,w4) = pair
116  read5(index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
117
118def read3(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
119  (a,w3) = pair
120  read4(index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
121
122def read2(+index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
123  (a,w2) = pair
124  read3(index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
125
126def read1(+index: U32, t: T.Counter, h: T.Chain, w0: U32, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
127  (a,w1) = pair
128  read2(index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))
129
130def read0(+index: U32, t: T.Counter, h: T.Chain, pair: Array<U32> & U32) -> Array<U32> & T.Chain:
131  (a,w0) = pair
132  read1(index,t,h,w0,Array.get(U32,a,U32.add(index,1)))
133
134def absorb(a: Array<U32>, +index: U32, t: T.Counter, h: T.Chain) -> Array<U32> & T.Chain:
135  read0(index,t,h,Array.get(U32,a,index))
136
137# Only the first n bytes of the word are message bytes; the rest are zero.
138def keep(w: U32, n: Nat) -> U32:
139  match n:
140    case 0n: 0
141    case 1n: U32.and(w,255)
142    case 2n: U32.and(w,65535)
143    case 3n: U32.and(w,16777215)
144    case _: w
145
146def mask(w: U32, +pos: Nat, +remain: Nat) -> U32:
147  keep(w,Nat.sub(remain,pos))
148
149def last31(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, pair: Array<U32> & U32) -> T.Chain:
150  (a,w31) = pair
151  F.compress_last(h,t,mask(w0,0n,remain),mask(w1,4n,remain),mask(w2,8n,remain),mask(w3,12n,remain),mask(w4,16n,remain),mask(w5,20n,remain),mask(w6,24n,remain),mask(w7,28n,remain),mask(w8,32n,remain),mask(w9,36n,remain),mask(w10,40n,remain),mask(w11,44n,remain),mask(w12,48n,remain),mask(w13,52n,remain),mask(w14,56n,remain),mask(w15,60n,remain),mask(w16,64n,remain),mask(w17,68n,remain),mask(w18,72n,remain),mask(w19,76n,remain),mask(w20,80n,remain),mask(w21,84n,remain),mask(w22,88n,remain),mask(w23,92n,remain),mask(w24,96n,remain),mask(w25,100n,remain),mask(w26,104n,remain),mask(w27,108n,remain),mask(w28,112n,remain),mask(w29,116n,remain),mask(w30,120n,remain),mask(w31,124n,remain))
152
153def last30(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, pair: Array<U32> & U32) -> T.Chain:
154  (a,w30) = pair
155  last31(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))
156
157def last29(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, pair: Array<U32> & U32) -> T.Chain:
158  (a,w29) = pair
159  last30(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))
160
161def last28(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, pair: Array<U32> & U32) -> T.Chain:
162  (a,w28) = pair
163  last29(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))
164
165def last27(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, pair: Array<U32> & U32) -> T.Chain:
166  (a,w27) = pair
167  last28(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))
168
169def last26(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, pair: Array<U32> & U32) -> T.Chain:
170  (a,w26) = pair
171  last27(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))
172
173def last25(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, pair: Array<U32> & U32) -> T.Chain:
174  (a,w25) = pair
175  last26(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))
176
177def last24(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, pair: Array<U32> & U32) -> T.Chain:
178  (a,w24) = pair
179  last25(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))
180
181def last23(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, pair: Array<U32> & U32) -> T.Chain:
182  (a,w23) = pair
183  last24(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))
184
185def last22(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, pair: Array<U32> & U32) -> T.Chain:
186  (a,w22) = pair
187  last23(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))
188
189def last21(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, pair: Array<U32> & U32) -> T.Chain:
190  (a,w21) = pair
191  last22(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))
192
193def last20(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, w19: U32, pair: Array<U32> & U32) -> T.Chain:
194  (a,w20) = pair
195  last21(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))
196
197def last19(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, w18: U32, pair: Array<U32> & U32) -> T.Chain:
198  (a,w19) = pair
199  last20(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))
200
201def last18(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, w17: U32, pair: Array<U32> & U32) -> T.Chain:
202  (a,w18) = pair
203  last19(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))
204
205def last17(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, w16: U32, pair: Array<U32> & U32) -> T.Chain:
206  (a,w17) = pair
207  last18(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))
208
209def last16(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, pair: Array<U32> & U32) -> T.Chain:
210  (a,w16) = pair
211  last17(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))
212
213def last15(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, pair: Array<U32> & U32) -> T.Chain:
214  (a,w15) = pair
215  last16(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
216
217def last14(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, pair: Array<U32> & U32) -> T.Chain:
218  (a,w14) = pair
219  last15(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
220
221def last13(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, pair: Array<U32> & U32) -> T.Chain:
222  (a,w13) = pair
223  last14(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
224
225def last12(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, pair: Array<U32> & U32) -> T.Chain:
226  (a,w12) = pair
227  last13(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
228
229def last11(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, pair: Array<U32> & U32) -> T.Chain:
230  (a,w11) = pair
231  last12(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
232
233def last10(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array<U32> & U32) -> T.Chain:
234  (a,w10) = pair
235  last11(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
236
237def last9(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> T.Chain:
238  (a,w9) = pair
239  last10(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
240
241def last8(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> T.Chain:
242  (a,w8) = pair
243  last9(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
244
245def last7(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> T.Chain:
246  (a,w7) = pair
247  last8(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
248
249def last6(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> T.Chain:
250  (a,w6) = pair
251  last7(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
252
253def last5(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> T.Chain:
254  (a,w5) = pair
255  last6(remain,index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
256
257def last4(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> T.Chain:
258  (a,w4) = pair
259  last5(remain,index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
260
261def last3(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> T.Chain:
262  (a,w3) = pair
263  last4(remain,index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
264
265def last2(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, w1: U32, pair: Array<U32> & U32) -> T.Chain:
266  (a,w2) = pair
267  last3(remain,index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
268
269def last1(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, w0: U32, pair: Array<U32> & U32) -> T.Chain:
270  (a,w1) = pair
271  last2(remain,index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))
272
273def last0(+remain: Nat, +index: U32, t: T.Counter, h: T.Chain, pair: Array<U32> & U32) -> T.Chain:
274  (a,w0) = pair
275  last1(remain,index,t,h,w0,Array.get(U32,a,U32.add(index,1)))
276
277# The last block holds the final 1..128 bytes (0 for the empty message).
278def final(a: Array<U32>, +index: U32, +remain: Nat, t: T.Counter, h: T.Chain) -> T.Chain:
279  last0(remain,index,F.bump(t,U32.from_nat(remain)),h,Array.get(U32,a,index))
280
281def blocks(n: Nat, +index: U32, +remain: Nat, t: T.Counter, pair: Array<U32> & T.Chain) -> T.Chain:
282  match n pair:
283    case 0n Tuple{a,h}: final(a,index,remain,t,h)
284    case 1n+p Tuple{a,h}:
285      +t2 = F.bump(t,128)
286      blocks(p,U32.add(index,32),remain,t2,absorb(a,index,t2,h))
287
288# IV with the parameter block folded into h0: digest length 64, no key, fanout 1, depth 1.
289def initial() -> T.Chain:
290  T.H{T.W{4072524104,1779033703},T.W{2227873595,3144134277},T.W{4271175723,1013904242},T.W{1595750129,2773480762},T.W{2917565137,1359893119},T.W{725511199,2600822924},T.W{4215389547,528734635},T.W{327033209,1541459225}}
291
292def unchecked(a: Array<U32>, +length: Nat) -> T.Chain:
293  +n = Nat.div(Nat.sub(length,1n),128n)
294  blocks(n,0,Nat.sub(length,Nat.mul(n,128n)),T.C{0,0,0,0},(a,initial()))
295
296def digest(h: T.Chain) -> Array<U32>:
297  match h:
298    case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}:
299      a = Array.new(U32,4n,0)
300      a = Array.set(U32,a,0,l0)
301      a = Array.set(U32,a,1,u0)
302      a = Array.set(U32,a,2,l1)
303      a = Array.set(U32,a,3,u1)
304      a = Array.set(U32,a,4,l2)
305      a = Array.set(U32,a,5,u2)
306      a = Array.set(U32,a,6,l3)
307      a = Array.set(U32,a,7,u3)
308      a = Array.set(U32,a,8,l4)
309      a = Array.set(U32,a,9,u4)
310      a = Array.set(U32,a,10,l5)
311      a = Array.set(U32,a,11,u5)
312      a = Array.set(U32,a,12,l6)
313      a = Array.set(U32,a,13,u6)
314      a = Array.set(U32,a,14,l7)
315      a = Array.set(U32,a,15,u7)
316      a
317
318def checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
319  match valid:
320    case False{}: None{}
321    case True{}: Some{digest(unchecked(a,length))}
322
323def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
324  (a,capacity) = pair
325  checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
326
327# BLAKE2b-512, unkeyed. The message is packed little-endian, four bytes per word;
328# byte_length is its length in bytes (None when it exceeds 4 * capacity). The
329# digest is 16 little-endian words (64 bytes).
330def blake2b(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:
331  sized(byte_length,Array.size(U32,words))