1	# Proof-only historical implementation model; not a production dependency.
2	import Base
3	import ../../../../src/crypto/sha/packed/core.bend as Runtime
4	import ../../../../src/crypto/sha/state.bend as S
5	
6	def rotr(+x: U32, +n: Nat) -> U32:
7	  (U32.shrn(x, n) .|. U32.shln(x, Nat.sub(32n, n)) : U32)
8	
9	def get(xs: List<&2, U32>, n: Nat) -> U32:
10	  match xs n:
11	    case Nil{} _:
12	      0
13	    case h <> t 0n:
14	      h
15	    case h <> t 1n+p:
16	      get(t, p)
17	
18	# Reverse history: at round t, index j contains Runtime.W[t-1-j].
19	def next_word_slow(+history: List<&2, U32>) -> U32:
20	  (Runtime.small1(get(history, 1n)) + get(history, 6n)
21	    + Runtime.small0(get(history, 14n)) + get(history, 15n) : U32)
22	
23	# Schedule histories always contain at least 16 words. Destructuring that prefix
24	# avoids four independent linked-list walks for every expanded word; the fallback
25	# preserves the total behavior used by the universal refinement theorem.
26	def next_word(+history: List<&2, U32>) -> U32:
27	  match history:
28	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):
29	      (Runtime.small1(b) + g + Runtime.small0(o) + p : U32)
30	    case _:
31	      next_word_slow(history)
32	
33	def expand(n: Nat, +history: List<&2, U32>) -> List<&2, U32>:
34	  match n:
35	    case 0n:
36	      Nil{}
37	    case 1n+p:
38	      +w = next_word(history)
39	      w <> expand(p, w <> history)
40	
41	def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
42	  List.append(&2, U32, block,
43	    expand(extra, List.reverse(&2, U32, block)))
44	
45	def rounds(ks: List<&2, U32>, ws: List<&2, U32>, s: S.State) -> S.State:
46	  match ks ws:
47	    case Nil{} _:
48	      s
49	    case k <> kt Nil{}:
50	      s
51	    case k <> kt w <> wt:
52	      rounds(kt, wt, Runtime.step(s, k, w))
53	
54	# Compression consumes an already expanded 64-word schedule.
55	def compress(ws: List<&2, U32>, ks: List<&2, U32>, +s: S.State) -> S.State:
56	  Runtime.feedforward(s, rounds(ks, ws, s))
57	
58	# Generate each derived schedule word immediately before its round. The reverse
59	# history is still retained for the recurrence, but the chronological 48-word
60	# extension is never materialized.
61	def expanded_rounds(n: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:
62	  match n ks:
63	    case 0n _:
64	      s
65	    case 1n+p Nil{}:
66	      s
67	    case 1n+p k <> kt:
68	      +w = next_word(history)
69	      expanded_rounds(p, w <> history, kt, Runtime.step(s, k, w))
70	
71	# Consume the original block words, then continue directly with its expansion.
72	def schedule_rounds(ws: List<&2, U32>, +extra: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:
73	  match ws ks:
74	    case Nil{} _:
75	      expanded_rounds(extra, history, ks, s)
76	    case w <> wt Nil{}:
77	      s
78	    case w <> wt k <> kt:
79	      schedule_rounds(wt, extra, history, kt, Runtime.step(s, k, w))
80	
81	# A fixed rolling window drops schedule words as soon as they are older than 16
82	# rounds. This avoids growing and reference-counting the reverse history list.
83	def window_rounds(n: Nat, win: Runtime.ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:
84	  match n win ks:
85	    case 0n _ _:
86	      s
87	    case 1n+q _ Nil{}:
88	      s
89	    case 1n+q Runtime.W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:
90	      +w = (Runtime.small1(b) + g + Runtime.small0(t) + u : U32)
91	      window_rounds(q, Runtime.W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,
92	        Runtime.step(s, k, w))
93	
94	def window_schedule_rounds(ws: List<&2, U32>, +extra: Nat, win: Runtime.ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:
95	  match ws ks:
96	    case Nil{} _:
97	      window_rounds(extra, win, ks, s)
98	    case w <> wt Nil{}:
99	      s
100	    case w <> wt k <> kt:
101	      window_schedule_rounds(wt, extra, win, kt, Runtime.step(s, k, w))
102	
103	def fused_compress_slow(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
104	  Runtime.feedforward(s, schedule_rounds(block, extra, List.reverse(&2, U32, block), ks, s))
105	
106	def fused_compress(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
107	  match block:
108	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
109	      Runtime.feedforward(s, window_schedule_rounds(
110	        [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra,
111	        Runtime.W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))
112	    case _:
113	      fused_compress_slow(block, extra, ks, s)
114	
115	# Fast path for the 16-word blocks produced by block_bytes. It executes the
116	# seed rounds directly and constructs only the fixed rolling window.
117	def window_compress16(+a: U32, +b: U32, +c: U32, +d: U32,
118	  +e: U32, +f: U32, +g: U32, +h: U32,
119	  +i: U32, +j: U32, +k: U32, +l: U32,
120	  +m: U32, +n: U32, +o: U32, +p: U32,
121	  +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:
122	  match ks:
123	    case k0 <> k1 <> k2 <> k3 <> k4 <> k5 <> k6 <> k7 <>
124	      k8 <> k9 <> k10 <> k11 <> k12 <> k13 <> k14 <> k15 <> kt:
125	      s1 = Runtime.step(s, k0, a)
126	      s2 = Runtime.step(s1, k1, b)
127	      s3 = Runtime.step(s2, k2, c)
128	      s4 = Runtime.step(s3, k3, d)
129	      s5 = Runtime.step(s4, k4, e)
130	      s6 = Runtime.step(s5, k5, f)
131	      s7 = Runtime.step(s6, k6, g)
132	      s8 = Runtime.step(s7, k7, h)
133	      s9 = Runtime.step(s8, k8, i)
134	      s10 = Runtime.step(s9, k9, j)
135	      s11 = Runtime.step(s10, k10, k)
136	      s12 = Runtime.step(s11, k11, l)
137	      s13 = Runtime.step(s12, k12, m)
138	      s14 = Runtime.step(s13, k13, n)
139	      s15 = Runtime.step(s14, k14, o)
140	      s16 = Runtime.step(s15, k15, p)
141	      Runtime.feedforward(s, window_rounds(extra,
142	        Runtime.W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, kt, s16))
143	    case _:
144	      fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s)
145	
146	def be32(+x: U32) -> List<&2, U32>:
147	  [U32.shrn(x, 24n), (U32.shrn(x, 16n) .&. 255 : U32),
148	   (U32.shrn(x, 8n) .&. 255 : U32), (x .&. 255 : U32)]
149	
150	def length_octets(count: Nat, +n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
151	  match count:
152	    case 0n:
153	      acc
154	    case 1n+p:
155	      length_octets(p, Nat.div(n, 256n), U32.from_nat(Nat.mod(n, 256n)) <> acc)
156	
157	def bit_length(+n: Nat) -> List<&2, U32>:
158	  length_octets(7n, Nat.div(n, 32n),
159	    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
160	
161	def digest(s: S.State) -> List<&2, U32>:
162	  S.H{a, b, c, d, e, f, g, h} = s
163	  [a, b, c, d, e, f, g, h]
164	
165	# Generic block decoder over a padded byte list and any constant table. The
166	# fast path below is proved equal to it with the FIPS table.
167	def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, s: S.State) -> S.State:
168	  match bytes:
169	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
170	      block_bytes(rest, extra, ks, window_compress16(
171	        Runtime.pack(b0, b1, b2, b3), Runtime.pack(b4, b5, b6, b7), Runtime.pack(b8, b9, b10, b11), Runtime.pack(b12, b13, b14, b15),
172	        Runtime.pack(b16, b17, b18, b19), Runtime.pack(b20, b21, b22, b23), Runtime.pack(b24, b25, b26, b27), Runtime.pack(b28, b29, b30, b31),
173	        Runtime.pack(b32, b33, b34, b35), Runtime.pack(b36, b37, b38, b39), Runtime.pack(b40, b41, b42, b43), Runtime.pack(b44, b45, b46, b47),
174	        Runtime.pack(b48, b49, b50, b51), Runtime.pack(b52, b53, b54, b55), Runtime.pack(b56, b57, b58, b59), Runtime.pack(b60, b61, b62, b63),
175	        extra, ks, s))
176	    case _:
177	      s
178	
179	# FIPS 180-4 round constants, the table the specialized rounds below inline.
180	def round_constants() -> List<&2, U32>:
181	  [1116352408, 1899447441, 3049323471, 3921009573,
182	   961987163, 1508970993, 2453635748, 2870763221,
183	   3624381080, 310598401, 607225278, 1426881987,
184	   1925078388, 2162078206, 2614888103, 3248222580,
185	   3835390401, 4022224774, 264347078, 604807628,
186	   770255983, 1249150122, 1555081692, 1996064986,
187	   2554220882, 2821834349, 2952996808, 3210313671,
188	   3336571891, 3584528711, 113926993, 338241895,
189	   666307205, 773529912, 1294757372, 1396182291,
190	   1695183700, 1986661051, 2177026350, 2456956037,
191	   2730485921, 2820302411, 3259730800, 3345764771,
192	   3516065817, 3600352804, 4094571909, 275423344,
193	   430227734, 506948616, 659060556, 883997877,
194	   958139571, 1322822218, 1537002063, 1747873779,
195	   1955562222, 2024104815, 2227730452, 2361852424,
196	   2428436474, 2756734187, 3204031479, 3329325298]
197	
198	# SHA-256 round t (16 <= t < 64) with its constant as a literal. Like
199	# window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round
200	# derives its schedule word from the rolling window before continuing with
201	# round t+1. Defined last-to-first because names must precede use.
202	def suffix(+n: Nat) -> List<&2, U32>:
203	  128 <> List.append(&2, U32,
204	    List.replicate(U32, Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), 0), bit_length(n))
205	
206	# Big-endian words of the 64-bit message bit length 8n, computed from n with
207	# exactly the digit expressions bit_length produces, but without building and
208	# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]
209	# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
210	def fin0(+n: Nat, +extra: Nat, s: S.State) -> S.State:
211	  Runtime.fips_compress16(Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
212	    extra, s)
213	
214	def fin1(+t0: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
215	  Runtime.fips_compress16(Runtime.pack(t0, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
216	    extra, s)
217	
218	def fin2(+t0: U32, +t1: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
219	  Runtime.fips_compress16(Runtime.pack(t0, t1, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
220	    extra, s)
221	
222	def fin3(+t0: U32, +t1: U32, +t2: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
223	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
224	    extra, s)
225	
226	def fin4(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
227	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
228	    extra, s)
229	
230	def fin5(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
231	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
232	    extra, s)
233	
234	def fin6(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
235	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
236	    extra, s)
237	
238	def fin7(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
239	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
240	    extra, s)
241	
242	def fin8(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
243	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
244	    extra, s)
245	
246	def fin9(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
247	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
248	    extra, s)
249	
250	def fin10(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
251	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
252	    extra, s)
253	
254	def fin11(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
255	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
256	    extra, s)
257	
258	def fin12(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
259	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
260	    extra, s)
261	
262	def fin13(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
263	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
264	    extra, s)
265	
266	def fin14(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
267	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
268	    extra, s)
269	
270	def fin15(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
271	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
272	    extra, s)
273	
274	def fin16(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
275	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
276	    extra, s)
277	
278	def fin17(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
279	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
280	    extra, s)
281	
282	def fin18(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
283	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
284	    extra, s)
285	
286	def fin19(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
287	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
288	    extra, s)
289	
290	def fin20(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
291	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
292	    extra, s)
293	
294	def fin21(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
295	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
296	    extra, s)
297	
298	def fin22(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
299	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
300	    extra, s)
301	
302	def fin23(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
303	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
304	    extra, s)
305	
306	def fin24(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
307	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
308	    extra, s)
309	
310	def fin25(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
311	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
312	    extra, s)
313	
314	def fin26(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
315	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
316	    extra, s)
317	
318	def fin27(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
319	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
320	    extra, s)
321	
322	def fin28(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
323	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
324	    extra, s)
325	
326	def fin29(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
327	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
328	    extra, s)
329	
330	def fin30(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
331	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
332	    extra, s)
333	
334	def fin31(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
335	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
336	    extra, s)
337	
338	def fin32(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
339	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
340	    extra, s)
341	
342	def fin33(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
343	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
344	    extra, s)
345	
346	def fin34(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
347	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
348	    extra, s)
349	
350	def fin35(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
351	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
352	    extra, s)
353	
354	def fin36(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
355	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
356	    extra, s)
357	
358	def fin37(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
359	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
360	    extra, s)
361	
362	def fin38(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
363	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
364	    extra, s)
365	
366	def fin39(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
367	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
368	    extra, s)
369	
370	def fin40(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
371	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
372	    extra, s)
373	
374	def fin41(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
375	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
376	    extra, s)
377	
378	def fin42(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
379	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
380	    extra, s)
381	
382	def fin43(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
383	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
384	    extra, s)
385	
386	def fin44(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
387	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
388	    extra, s)
389	
390	def fin45(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
391	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
392	    extra, s)
393	
394	def fin46(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
395	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
396	    extra, s)
397	
398	def fin47(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
399	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, 128), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
400	    extra, s)
401	
402	def fin48(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
403	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
404	    extra, s)
405	
406	def fin49(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
407	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, 128, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
408	    extra, s)
409	
410	def fin50(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
411	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, 128, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
412	    extra, s)
413	
414	def fin51(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
415	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, 128), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
416	    extra, s)
417	
418	def fin52(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
419	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(128, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
420	    extra, s)
421	
422	def fin53(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
423	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, 128, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
424	    extra, s)
425	
426	def fin54(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
427	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, 128, 0), Runtime.len_hi(n), Runtime.len_lo(n),
428	    extra, s)
429	
430	def fin55(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
431	  Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, 128), Runtime.len_hi(n), Runtime.len_lo(n),
432	    extra, s)
433	
434	def fin56(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
435	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
436	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0),
437	    extra, s))
438	
439	def fin57(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
440	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
441	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, 128, 0, 0), Runtime.pack(0, 0, 0, 0),
442	    extra, s))
443	
444	def fin58(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
445	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
446	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, 128, 0), Runtime.pack(0, 0, 0, 0),
447	    extra, s))
448	
449	def fin59(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
450	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
451	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, t58, 128), Runtime.pack(0, 0, 0, 0),
452	    extra, s))
453	
454	def fin60(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
455	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
456	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, t58, t59), Runtime.pack(128, 0, 0, 0),
457	    extra, s))
458	
459	def fin61(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
460	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
461	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, t58, t59), Runtime.pack(t60, 128, 0, 0),
462	    extra, s))
463	
464	def fin62(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +t61: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
465	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
466	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, t58, t59), Runtime.pack(t60, t61, 128, 0),
467	    extra, s))
468	
469	def fin63(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32, +t9: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t14: U32, +t15: U32, +t16: U32, +t17: U32, +t18: U32, +t19: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t24: U32, +t25: U32, +t26: U32, +t27: U32, +t28: U32, +t29: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32, +t34: U32, +t35: U32, +t36: U32, +t37: U32, +t38: U32, +t39: U32, +t40: U32, +t41: U32, +t42: U32, +t43: U32, +t44: U32, +t45: U32, +t46: U32, +t47: U32, +t48: U32, +t49: U32, +t50: U32, +t51: U32, +t52: U32, +t53: U32, +t54: U32, +t55: U32, +t56: U32, +t57: U32, +t58: U32, +t59: U32, +t60: U32, +t61: U32, +t62: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:
470	  Runtime.fips_compress16(Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
471	    extra, Runtime.fips_compress16(Runtime.pack(t0, t1, t2, t3), Runtime.pack(t4, t5, t6, t7), Runtime.pack(t8, t9, t10, t11), Runtime.pack(t12, t13, t14, t15), Runtime.pack(t16, t17, t18, t19), Runtime.pack(t20, t21, t22, t23), Runtime.pack(t24, t25, t26, t27), Runtime.pack(t28, t29, t30, t31), Runtime.pack(t32, t33, t34, t35), Runtime.pack(t36, t37, t38, t39), Runtime.pack(t40, t41, t42, t43), Runtime.pack(t44, t45, t46, t47), Runtime.pack(t48, t49, t50, t51), Runtime.pack(t52, t53, t54, t55), Runtime.pack(t56, t57, t58, t59), Runtime.pack(t60, t61, t62, 128),
472	    extra, s))
473	
474	# Tail-recursive block loop over an already padded byte list.
475	def fips_blocks(bytes: List<&2, U32>, +extra: Nat, s: S.State) -> S.State:
476	  match bytes:
477	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
478	      fips_blocks(rest, extra, Runtime.fips_compress16(Runtime.pack(b0, b1, b2, b3), Runtime.pack(b4, b5, b6, b7), Runtime.pack(b8, b9, b10, b11), Runtime.pack(b12, b13, b14, b15), Runtime.pack(b16, b17, b18, b19), Runtime.pack(b20, b21, b22, b23), Runtime.pack(b24, b25, b26, b27), Runtime.pack(b28, b29, b30, b31), Runtime.pack(b32, b33, b34, b35), Runtime.pack(b36, b37, b38, b39), Runtime.pack(b40, b41, b42, b43), Runtime.pack(b44, b45, b46, b47), Runtime.pack(b48, b49, b50, b51), Runtime.pack(b52, b53, b54, b55), Runtime.pack(b56, b57, b58, b59), Runtime.pack(b60, b61, b62, b63), extra, s))
479	    case _:
480	      s
481	
482	def zeros_onto(z: Nat, acc: List<&2, U32>) -> List<&2, U32>:
483	  match z:
484	    case 0n:
485	      acc
486	    case 1n+p:
487	      zeros_onto(p, 0 <> acc)
488	
489	# The padding suffix built only with tail-recursive loops.
490	def padding(+n: Nat) -> List<&2, U32>:
491	  128 <> zeros_onto(Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), bit_length(n))
492	
493	def byte_count(bytes: List<&2, U32>, acc: Nat) -> Nat:
494	  match bytes:
495	    case Nil{}:
496	      acc
497	    case h <> t:
498	      byte_count(t, 1n+acc)
499	
500	# Final block(s) of an n-byte message whose tail has fewer than 64 bytes.
501	# stream never passes 64 or more bytes; that case pads with tail-recursive
502	# loops. The match is exhaustive: a default case would make Bend rebuild the
503	# consumed cells at every depth. Length words are computed directly from n; note
504	# that sharing any List<U32> would make Bend reference-count every list match,
505	# including the input loop in stream.
506	def finish_n(+tail: List<&2, U32>, +n: Nat, +extra: Nat, s: S.State) -> S.State:
507	  match tail:
508	    case Nil{}:
509	      fin0(n, extra, s)
510	    case t0 <> Nil{}:
511	      fin1(t0, n, extra, s)
512	    case t0 <> t1 <> Nil{}:
513	      fin2(t0, t1, n, extra, s)
514	    case t0 <> t1 <> t2 <> Nil{}:
515	      fin3(t0, t1, t2, n, extra, s)
516	    case t0 <> t1 <> t2 <> t3 <> Nil{}:
517	      fin4(t0, t1, t2, t3, n, extra, s)
518	    case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}:
519	      fin5(t0, t1, t2, t3, t4, n, extra, s)
520	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}:
521	      fin6(t0, t1, t2, t3, t4, t5, n, extra, s)
522	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}:
523	      fin7(t0, t1, t2, t3, t4, t5, t6, n, extra, s)
524	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}:
525	      fin8(t0, t1, t2, t3, t4, t5, t6, t7, n, extra, s)
526	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}:
527	      fin9(t0, t1, t2, t3, t4, t5, t6, t7, t8, n, extra, s)
528	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}:
529	      fin10(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, n, extra, s)
530	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}:
531	      fin11(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, n, extra, s)
532	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}:
533	      fin12(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, n, extra, s)
534	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}:
535	      fin13(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, n, extra, s)
536	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}:
537	      fin14(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, n, extra, s)
538	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}:
539	      fin15(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, n, extra, s)
540	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}:
541	      fin16(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, n, extra, s)
542	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> Nil{}:
543	      fin17(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, n, extra, s)
544	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> Nil{}:
545	      fin18(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, n, extra, s)
546	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> Nil{}:
547	      fin19(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, n, extra, s)
548	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> Nil{}:
549	      fin20(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, n, extra, s)
550	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> Nil{}:
551	      fin21(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, n, extra, s)
552	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> Nil{}:
553	      fin22(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, n, extra, s)
554	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> Nil{}:
555	      fin23(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, n, extra, s)
556	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> Nil{}:
557	      fin24(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, n, extra, s)
558	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> Nil{}:
559	      fin25(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, n, extra, s)
560	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> Nil{}:
561	      fin26(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, n, extra, s)
562	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> Nil{}:
563	      fin27(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, n, extra, s)
564	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> Nil{}:
565	      fin28(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, n, extra, s)
566	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> Nil{}:
567	      fin29(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, n, extra, s)
568	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> Nil{}:
569	      fin30(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, n, extra, s)
570	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> Nil{}:
571	      fin31(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, n, extra, s)
572	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> Nil{}:
573	      fin32(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, n, extra, s)
574	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> Nil{}:
575	      fin33(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, n, extra, s)
576	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> Nil{}:
577	      fin34(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, n, extra, s)
578	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> Nil{}:
579	      fin35(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, n, extra, s)
580	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> Nil{}:
581	      fin36(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, n, extra, s)
582	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> Nil{}:
583	      fin37(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, n, extra, s)
584	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> Nil{}:
585	      fin38(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, n, extra, s)
586	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> Nil{}:
587	      fin39(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, n, extra, s)
588	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> Nil{}:
589	      fin40(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, n, extra, s)
590	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> Nil{}:
591	      fin41(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, n, extra, s)
592	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> Nil{}:
593	      fin42(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, n, extra, s)
594	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> Nil{}:
595	      fin43(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, n, extra, s)
596	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> Nil{}:
597	      fin44(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, n, extra, s)
598	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> Nil{}:
599	      fin45(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, n, extra, s)
600	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> Nil{}:
601	      fin46(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, n, extra, s)
602	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> Nil{}:
603	      fin47(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, n, extra, s)
604	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> Nil{}:
605	      fin48(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, n, extra, s)
606	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> Nil{}:
607	      fin49(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, n, extra, s)
608	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> Nil{}:
609	      fin50(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, n, extra, s)
610	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> Nil{}:
611	      fin51(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, n, extra, s)
612	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> Nil{}:
613	      fin52(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, n, extra, s)
614	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> Nil{}:
615	      fin53(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, n, extra, s)
616	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> Nil{}:
617	      fin54(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, n, extra, s)
618	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> Nil{}:
619	      fin55(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, n, extra, s)
620	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> Nil{}:
621	      fin56(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, n, extra, s)
622	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> Nil{}:
623	      fin57(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, n, extra, s)
624	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> Nil{}:
625	      fin58(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, n, extra, s)
626	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> Nil{}:
627	      fin59(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, n, extra, s)
628	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> Nil{}:
629	      fin60(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, n, extra, s)
630	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> Nil{}:
631	      fin61(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, n, extra, s)
632	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> Nil{}:
633	      fin62(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, t61, n, extra, s)
634	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> Nil{}:
635	      fin63(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31, t32, t33, t34, t35, t36, t37, t38, t39, t40, t41, t42, t43, t44, t45, t46, t47, t48, t49, t50, t51, t52, t53, t54, t55, t56, t57, t58, t59, t60, t61, t62, n, extra, s)
636	    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> t63 <> rest:
637	      fips_blocks(List.reverse.go(&2, U32, List.reverse(&2, U32, t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> t22 <> t23 <> t24 <> t25 <> t26 <> t27 <> t28 <> t29 <> t30 <> t31 <> t32 <> t33 <> t34 <> t35 <> t36 <> t37 <> t38 <> t39 <> t40 <> t41 <> t42 <> t43 <> t44 <> t45 <> t46 <> t47 <> t48 <> t49 <> t50 <> t51 <> t52 <> t53 <> t54 <> t55 <> t56 <> t57 <> t58 <> t59 <> t60 <> t61 <> t62 <> t63 <> rest), padding(n)), extra, s)
638	
639	# count is the number of bytes already hashed, always a multiple of 64.
640	def finish(+tail: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:
641	  finish_n(tail, byte_count(tail, count), extra, s)
642	
643	# Compress complete 64-byte blocks straight from the input list, so the
644	# message is never copied, counted or reversed. count is the number of bytes
645	# already hashed and extra the number of derived schedule words (48).
646	def stream(+bytes: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:
647	  match bytes:
648	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
649	      stream(rest, Nat.add(64n, count), extra, Runtime.fips_compress16(
650	        Runtime.pack(b0, b1, b2, b3), Runtime.pack(b4, b5, b6, b7), Runtime.pack(b8, b9, b10, b11), Runtime.pack(b12, b13, b14, b15),
651	        Runtime.pack(b16, b17, b18, b19), Runtime.pack(b20, b21, b22, b23), Runtime.pack(b24, b25, b26, b27), Runtime.pack(b28, b29, b30, b31),
652	        Runtime.pack(b32, b33, b34, b35), Runtime.pack(b36, b37, b38, b39), Runtime.pack(b40, b41, b42, b43), Runtime.pack(b44, b45, b46, b47),
653	        Runtime.pack(b48, b49, b50, b51), Runtime.pack(b52, b53, b54, b55), Runtime.pack(b56, b57, b58, b59), Runtime.pack(b60, b61, b62, b63),
654	        extra, s))
655	    case _:
656	      finish(bytes, count, extra, s)
657	
658	# ASCII convenience only; binary inputs use sha256 directly.
659	def ascii(s: String) -> List<&2, U32>:
660	  match s:
661	    case SNil{}:
662	      Nil{}
663	    case SCon{Chr{c}, t}:
664	      c <> ascii(t)
665	
666	def hex_digit_if(x: U32, small: Bool) -> Char:
667	  match small:
668	    case True{}:
669	      Chr{(48 + x : U32)}
670	    case False{}:
671	      Chr{(87 + x : U32)}
672	
673	def hex_digit(+x: U32) -> Char:
674	  hex_digit_if(x, U32.is_lt(x, 10))
675	
676	def hex_word_go(n: Nat, +x: U32, acc: String) -> String:
677	  match n:
678	    case 0n:
679	      acc
680	    case 1n+p:
681	      hex_word_go(p, U32.shrn(x, 4n), SCon{hex_digit((x .&. 15 : U32)), acc})
682	
683	def hex_word(x: U32) -> String:
684	  hex_word_go(8n, x, "")
685	
686	def hex(ws: List<&2, U32>) -> String:
687	  match ws:
688	    case Nil{}:
689	      ""
690	    case w <> t:
691	      hex_word(w) ++ hex(t)
692	
693	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
694	  digest(stream(bytes, 0n, 48n, Runtime.initial()))