1	import Base
2	import ./types.bend as T
3	import ./lane.bend as L
4	import ./permutation.bend as P
5	
6	def mix(s: T.State,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,w31: U32,w32: U32,w33: U32) -> T.State:
7	  match s:
8	    case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}:
9	      T.S{L.xor(a0,T.W{w0,w1}),L.xor(a1,T.W{w2,w3}),L.xor(a2,T.W{w4,w5}),L.xor(a3,T.W{w6,w7}),L.xor(a4,T.W{w8,w9}),L.xor(a5,T.W{w10,w11}),L.xor(a6,T.W{w12,w13}),L.xor(a7,T.W{w14,w15}),L.xor(a8,T.W{w16,w17}),L.xor(a9,T.W{w18,w19}),L.xor(a10,T.W{w20,w21}),L.xor(a11,T.W{w22,w23}),L.xor(a12,T.W{w24,w25}),L.xor(a13,T.W{w26,w27}),L.xor(a14,T.W{w28,w29}),L.xor(a15,T.W{w30,w31}),L.xor(a16,T.W{w32,w33}),a17,a18,a19,a20,a21,a22,a23,a24}
10	
11	def read33(+round_count: Nat,+index: U32, s: T.State, 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, w31: U32, w32: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
12	  (a,w33) = pair
13	  (a,P.rounds(round_count,0n,mix(s,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,w32,w33)))
14	
15	def read32(+round_count: Nat,+index: U32, s: T.State, 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, w31: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
16	  (a,w32) = pair
17	  read33(round_count,index,s,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,w32,Array.get(U32,a,U32.add(index,33)))
18	
19	def read31(+round_count: Nat,+index: U32, s: T.State, 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.State:
20	  (a,w31) = pair
21	  read32(round_count,index,s,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,Array.get(U32,a,U32.add(index,32)))
22	
23	def read30(+round_count: Nat,+index: U32, s: T.State, 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.State:
24	  (a,w30) = pair
25	  read31(round_count,index,s,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)))
26	
27	def read29(+round_count: Nat,+index: U32, s: T.State, 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.State:
28	  (a,w29) = pair
29	  read30(round_count,index,s,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)))
30	
31	def read28(+round_count: Nat,+index: U32, s: T.State, 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.State:
32	  (a,w28) = pair
33	  read29(round_count,index,s,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)))
34	
35	def read27(+round_count: Nat,+index: U32, s: T.State, 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.State:
36	  (a,w27) = pair
37	  read28(round_count,index,s,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)))
38	
39	def read26(+round_count: Nat,+index: U32, s: T.State, 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.State:
40	  (a,w26) = pair
41	  read27(round_count,index,s,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)))
42	
43	def read25(+round_count: Nat,+index: U32, s: T.State, 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.State:
44	  (a,w25) = pair
45	  read26(round_count,index,s,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)))
46	
47	def read24(+round_count: Nat,+index: U32, s: T.State, 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.State:
48	  (a,w24) = pair
49	  read25(round_count,index,s,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)))
50	
51	def read23(+round_count: Nat,+index: U32, s: T.State, 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.State:
52	  (a,w23) = pair
53	  read24(round_count,index,s,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)))
54	
55	def read22(+round_count: Nat,+index: U32, s: T.State, 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.State:
56	  (a,w22) = pair
57	  read23(round_count,index,s,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)))
58	
59	def read21(+round_count: Nat,+index: U32, s: T.State, 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.State:
60	  (a,w21) = pair
61	  read22(round_count,index,s,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)))
62	
63	def read20(+round_count: Nat,+index: U32, s: T.State, 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.State:
64	  (a,w20) = pair
65	  read21(round_count,index,s,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)))
66	
67	def read19(+round_count: Nat,+index: U32, s: T.State, 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.State:
68	  (a,w19) = pair
69	  read20(round_count,index,s,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)))
70	
71	def read18(+round_count: Nat,+index: U32, s: T.State, 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.State:
72	  (a,w18) = pair
73	  read19(round_count,index,s,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)))
74	
75	def read17(+round_count: Nat,+index: U32, s: T.State, 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.State:
76	  (a,w17) = pair
77	  read18(round_count,index,s,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)))
78	
79	def read16(+round_count: Nat,+index: U32, s: T.State, 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.State:
80	  (a,w16) = pair
81	  read17(round_count,index,s,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)))
82	
83	def read15(+round_count: Nat,+index: U32, s: T.State, 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.State:
84	  (a,w15) = pair
85	  read16(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
86	
87	def read14(+round_count: Nat,+index: U32, s: T.State, 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.State:
88	  (a,w14) = pair
89	  read15(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
90	
91	def read13(+round_count: Nat,+index: U32, s: T.State, 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.State:
92	  (a,w13) = pair
93	  read14(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
94	
95	def read12(+round_count: Nat,+index: U32, s: T.State, 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.State:
96	  (a,w12) = pair
97	  read13(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
98	
99	def read11(+round_count: Nat,+index: U32, s: T.State, 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.State:
100	  (a,w11) = pair
101	  read12(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
102	
103	def read10(+round_count: Nat,+index: U32, s: T.State, 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.State:
104	  (a,w10) = pair
105	  read11(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
106	
107	def read9(+round_count: Nat,+index: U32, s: T.State, 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.State:
108	  (a,w9) = pair
109	  read10(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
110	
111	def read8(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
112	  (a,w8) = pair
113	  read9(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
114	
115	def read7(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
116	  (a,w7) = pair
117	  read8(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
118	
119	def read6(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
120	  (a,w6) = pair
121	  read7(round_count,index,s,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
122	
123	def read5(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
124	  (a,w5) = pair
125	  read6(round_count,index,s,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
126	
127	def read4(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
128	  (a,w4) = pair
129	  read5(round_count,index,s,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
130	
131	def read3(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
132	  (a,w3) = pair
133	  read4(round_count,index,s,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
134	
135	def read2(+round_count: Nat,+index: U32, s: T.State, w0: U32, w1: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
136	  (a,w2) = pair
137	  read3(round_count,index,s,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
138	
139	def read1(+round_count: Nat,+index: U32, s: T.State, w0: U32, pair: Array<U32> & U32) -> Array<U32> & T.State:
140	  (a,w1) = pair
141	  read2(round_count,index,s,w0,w1,Array.get(U32,a,U32.add(index,2)))
142	
143	def read0(+round_count: Nat,+index: U32, s: T.State, pair: Array<U32> & U32) -> Array<U32> & T.State:
144	  (a,w0) = pair
145	  read1(round_count,index,s,w0,Array.get(U32,a,U32.add(index,1)))
146	
147	def absorb(+round_count: Nat,a: Array<U32>, +index: U32, s: T.State) -> Array<U32> & T.State:
148	  read0(round_count,index,s,Array.get(U32,a,index))
149	
150	# Little-endian Keccak pad10*1, domain suffix 0x01.
151	def partial(w: U32, delta: Nat) -> U32:
152	  match delta:
153	    case 0n: 1
154	    case 1n: U32.or(U32.and(w,255),256)
155	    case 2n: U32.or(U32.and(w,65535),65536)
156	    case 3n: U32.or(U32.and(w,16777215),16777216)
157	    case _: w
158	
159	def pad_choose(c: Cmp, w: U32, delta: Nat) -> U32:
160	  match c:
161	    case GT{}: 0
162	    case EQ{}: 1
163	    case LT{}: partial(w,delta)
164	
165	def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
166	  pad_choose(Nat.cmp(pos,remain),w,Nat.sub(remain,pos))
167	
168	def pad33(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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, w31: U32, w32: U32, pair: Array<U32> & U32) -> T.State:
169	  (a,w33) = pair
170	  P.rounds(round_count,0n,mix(s,pad_word(w0,0n,remain),pad_word(w1,4n,remain),pad_word(w2,8n,remain),pad_word(w3,12n,remain),pad_word(w4,16n,remain),pad_word(w5,20n,remain),pad_word(w6,24n,remain),pad_word(w7,28n,remain),pad_word(w8,32n,remain),pad_word(w9,36n,remain),pad_word(w10,40n,remain),pad_word(w11,44n,remain),pad_word(w12,48n,remain),pad_word(w13,52n,remain),pad_word(w14,56n,remain),pad_word(w15,60n,remain),pad_word(w16,64n,remain),pad_word(w17,68n,remain),pad_word(w18,72n,remain),pad_word(w19,76n,remain),pad_word(w20,80n,remain),pad_word(w21,84n,remain),pad_word(w22,88n,remain),pad_word(w23,92n,remain),pad_word(w24,96n,remain),pad_word(w25,100n,remain),pad_word(w26,104n,remain),pad_word(w27,108n,remain),pad_word(w28,112n,remain),pad_word(w29,116n,remain),pad_word(w30,120n,remain),pad_word(w31,124n,remain),pad_word(w32,128n,remain),U32.or(pad_word(w33,132n,remain),2147483648)))
171	
172	def pad32(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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, w31: U32, pair: Array<U32> & U32) -> T.State:
173	  (a,w32) = pair
174	  pad33(round_count,remain,index,s,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,w32,Array.get(U32,a,U32.add(index,33)))
175	
176	def pad31(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
177	  (a,w31) = pair
178	  pad32(round_count,remain,index,s,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,Array.get(U32,a,U32.add(index,32)))
179	
180	def pad30(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
181	  (a,w30) = pair
182	  pad31(round_count,remain,index,s,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)))
183	
184	def pad29(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
185	  (a,w29) = pair
186	  pad30(round_count,remain,index,s,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)))
187	
188	def pad28(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
189	  (a,w28) = pair
190	  pad29(round_count,remain,index,s,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)))
191	
192	def pad27(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
193	  (a,w27) = pair
194	  pad28(round_count,remain,index,s,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)))
195	
196	def pad26(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
197	  (a,w26) = pair
198	  pad27(round_count,remain,index,s,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)))
199	
200	def pad25(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
201	  (a,w25) = pair
202	  pad26(round_count,remain,index,s,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)))
203	
204	def pad24(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
205	  (a,w24) = pair
206	  pad25(round_count,remain,index,s,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)))
207	
208	def pad23(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
209	  (a,w23) = pair
210	  pad24(round_count,remain,index,s,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)))
211	
212	def pad22(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
213	  (a,w22) = pair
214	  pad23(round_count,remain,index,s,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)))
215	
216	def pad21(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
217	  (a,w21) = pair
218	  pad22(round_count,remain,index,s,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)))
219	
220	def pad20(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
221	  (a,w20) = pair
222	  pad21(round_count,remain,index,s,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)))
223	
224	def pad19(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
225	  (a,w19) = pair
226	  pad20(round_count,remain,index,s,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)))
227	
228	def pad18(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
229	  (a,w18) = pair
230	  pad19(round_count,remain,index,s,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)))
231	
232	def pad17(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
233	  (a,w17) = pair
234	  pad18(round_count,remain,index,s,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)))
235	
236	def pad16(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
237	  (a,w16) = pair
238	  pad17(round_count,remain,index,s,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)))
239	
240	def pad15(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
241	  (a,w15) = pair
242	  pad16(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))
243	
244	def pad14(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
245	  (a,w14) = pair
246	  pad15(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
247	
248	def pad13(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
249	  (a,w13) = pair
250	  pad14(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
251	
252	def pad12(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
253	  (a,w12) = pair
254	  pad13(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
255	
256	def pad11(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
257	  (a,w11) = pair
258	  pad12(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
259	
260	def pad10(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, 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.State:
261	  (a,w10) = pair
262	  pad11(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
263	
264	def pad9(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> T.State:
265	  (a,w9) = pair
266	  pad10(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
267	
268	def pad8(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> T.State:
269	  (a,w8) = pair
270	  pad9(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
271	
272	def pad7(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> T.State:
273	  (a,w7) = pair
274	  pad8(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
275	
276	def pad6(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> T.State:
277	  (a,w6) = pair
278	  pad7(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
279	
280	def pad5(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> T.State:
281	  (a,w5) = pair
282	  pad6(round_count,remain,index,s,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
283	
284	def pad4(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> T.State:
285	  (a,w4) = pair
286	  pad5(round_count,remain,index,s,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
287	
288	def pad3(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> T.State:
289	  (a,w3) = pair
290	  pad4(round_count,remain,index,s,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
291	
292	def pad2(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, w1: U32, pair: Array<U32> & U32) -> T.State:
293	  (a,w2) = pair
294	  pad3(round_count,remain,index,s,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
295	
296	def pad1(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, w0: U32, pair: Array<U32> & U32) -> T.State:
297	  (a,w1) = pair
298	  pad2(round_count,remain,index,s,w0,w1,Array.get(U32,a,U32.add(index,2)))
299	
300	def pad0(+round_count: Nat,+remain: Nat, +index: U32, s: T.State, pair: Array<U32> & U32) -> T.State:
301	  (a,w0) = pair
302	  pad1(round_count,remain,index,s,w0,Array.get(U32,a,U32.add(index,1)))
303	
304	def finish(+round_count: Nat,a: Array<U32>, +index: U32, remain: Nat, s: T.State) -> T.State:
305	  pad0(round_count,remain,index,s,Array.get(U32,a,index))
306	
307	def blocks(+round_count: Nat,n: Nat, +index: U32, remain: Nat, pair: Array<U32> & T.State) -> T.State:
308	  match n pair:
309	    case 0n Tuple{a,s}: finish(round_count,a,index,remain,s)
310	    case 1n+p Tuple{a,s}: blocks(round_count,p,U32.add(index,34),remain,absorb(round_count,a,index,s))
311	
312	def unchecked(+round_count: Nat,a: Array<U32>, +length: Nat) -> T.State:
313	  blocks(round_count,Nat.div(length,136n),0,Nat.mod(length,136n),(a,P.initial()))
314	
315	def digest(s: T.State) -> Array<U32>:
316	  match s:
317	    case T.S{T.W{l0,h0},T.W{l1,h1},T.W{l2,h2},T.W{l3,h3},a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}:
318	      a = Array.new(U32,3n,0)
319	      a = Array.set(U32,a,0,l0)
320	      a = Array.set(U32,a,1,h0)
321	      a = Array.set(U32,a,2,l1)
322	      a = Array.set(U32,a,3,h1)
323	      a = Array.set(U32,a,4,l2)
324	      a = Array.set(U32,a,5,h2)
325	      a = Array.set(U32,a,6,l3)
326	      a = Array.set(U32,a,7,h3)
327	      a
328	
329	def checked(+round_count: Nat,valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
330	  match valid:
331	    case False{}: None{}
332	    case True{}: Some{digest(unchecked(round_count,a,length))}
333	
334	def sized(+round_count: Nat,+length: Nat, pair: Array<U32> & U32) -> Maybe<&1,Array<U32>>:
335	  (a,capacity) = pair
336	  checked(round_count,Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
337	
338	def keccak256_rounds(+round_count: Nat,a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
339	  sized(round_count,length,Array.size(U32,a))
340	
341	
342	def keccak256(a: Array<U32>, length: Nat) -> Maybe<&1,Array<U32>>:
343	  keccak256_rounds(24n,a,length)