1	# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2	import Base
3	import ./types.bend as T
4	import ./compress.bend as F
5	
6	def 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	
10	def 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	
14	def 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	
18	def 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	
22	def 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	
26	def 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	
30	def 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	
34	def 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	
38	def 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	
42	def 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	
46	def 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	
50	def 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	
54	def 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	
58	def 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	
62	def 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	
66	def 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	
70	def 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	
74	def 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	
78	def 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	
82	def 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	
86	def 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	
90	def 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	
94	def 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	
98	def 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	
102	def 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	
106	def 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	
110	def 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	
114	def 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	
118	def 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	
122	def 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	
126	def 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	
130	def 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	
134	def 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.
138	def 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	
146	def mask(w: U32, +pos: Nat, +remain: Nat) -> U32:
147	  keep(w,Nat.sub(remain,pos))
148	
149	def 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	
153	def 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	
157	def 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	
161	def 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	
165	def 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	
169	def 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	
173	def 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	
177	def 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	
181	def 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	
185	def 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	
189	def 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	
193	def 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	
197	def 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	
201	def 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	
205	def 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	
209	def 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	
213	def 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	
217	def 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	
221	def 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	
225	def 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	
229	def 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	
233	def 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	
237	def 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	
241	def 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	
245	def 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	
249	def 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	
253	def 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	
257	def 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	
261	def 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	
265	def 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	
269	def 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	
273	def 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).
278	def 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	
281	def 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.
289	def 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	
292	def 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	
296	def 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	
318	def 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	
323	def 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).
330	def blake2b(words: Array<U32>, byte_length: Nat) -> Maybe<&1,Array<U32>>:
331	  sized(byte_length,Array.size(U32,words))