src/crypto/sha/core.bend source

src/crypto/sha/core.bend on the hub · documented module

import Baseimport ./state.bend as Stype ShaWindow is Data:  W{a: U32, b: U32, c: U32, d: U32, e: U32, f: U32, g: U32, h: U32,    i: U32, j: U32, k: U32, l: U32, m: U32, n: U32, o: U32, p: U32}# SHA-256 for byte sequences. Each input U32 contributes its low 8 bits.# SHA-256 arithmetic is native U32, hence addition wraps modulo 2^32.def initial() -> S.State:  S.H{1779033703, 3144134277, 1013904242, 2773480762,    1359893119, 2600822924, 528734635, 1541459225}def rotr(+x: U32, +n: Nat) -> U32:  (U32.shrn(x, n) .|. U32.shln(x, Nat.sub(32n, n)) : U32)def big0(+x: U32) -> U32:  ((U32.shrn(x, 2n) .|. U32.shln(x, 30n))    .^. (U32.shrn(x, 13n) .|. U32.shln(x, 19n))    .^. (U32.shrn(x, 22n) .|. U32.shln(x, 10n)) : U32)def big1(+x: U32) -> U32:  ((U32.shrn(x, 6n) .|. U32.shln(x, 26n))    .^. (U32.shrn(x, 11n) .|. U32.shln(x, 21n))    .^. (U32.shrn(x, 25n) .|. U32.shln(x, 7n)) : U32)def small0(+x: U32) -> U32:  ((U32.shrn(x, 7n) .|. U32.shln(x, 25n))    .^. (U32.shrn(x, 18n) .|. U32.shln(x, 14n))    .^. U32.shrn(x, 3n) : U32)def small1(+x: U32) -> U32:  ((U32.shrn(x, 17n) .|. U32.shln(x, 15n))    .^. (U32.shrn(x, 19n) .|. U32.shln(x, 13n))    .^. U32.shrn(x, 10n) : U32)def choose(+x: U32, y: U32, z: U32) -> U32:  ((x .&. y) .^. (U32.not(x) .&. z) : U32)def majority(+x: U32, +y: U32, +z: U32) -> U32:  ((x .&. y) .^. (x .&. z) .^. (y .&. z) : U32)def step(s: S.State, k: U32, w: U32) -> S.State:  S.H{+a, +b, +c, d, +e, +f, +g, h} = s  +t1 = (h + big1(e) + choose(e, f, g) + k + w : U32)  t2 = (big0(a) + majority(a, b, c) : U32)  S.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}def feedforward(x: S.State, y: S.State) -> S.State:  S.H{a, b, c, d, e, f, g, h} = x  S.H{i, j, k, l, m, n, o, p} = y  S.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),    (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}def get(xs: List<&2, U32>, n: Nat) -> U32:  match xs n:    case Nil{} _:      0    case h <> t 0n:      h    case h <> t 1n+p:      get(t, p)# Reverse history: at round t, index j contains W[t-1-j].def next_word_slow(+history: List<&2, U32>) -> U32:  (small1(get(history, 1n)) + get(history, 6n)    + small0(get(history, 14n)) + get(history, 15n) : U32)# Schedule histories always contain at least 16 words. Destructuring that prefix# avoids four independent linked-list walks for every expanded word; the fallback# preserves the total behavior used by the universal refinement theorem.def next_word(+history: List<&2, U32>) -> U32:  match history:    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):      (small1(b) + g + small0(o) + p : U32)    case _:      next_word_slow(history)def expand(n: Nat, +history: List<&2, U32>) -> List<&2, U32>:  match n:    case 0n:      Nil{}    case 1n+p:      +w = next_word(history)      w <> expand(p, w <> history)def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:  List.append(&2, U32, block,    expand(extra, List.reverse(&2, U32, block)))def rounds(ks: List<&2, U32>, ws: List<&2, U32>, s: S.State) -> S.State:  match ks ws:    case Nil{} _:      s    case k <> kt Nil{}:      s    case k <> kt w <> wt:      rounds(kt, wt, step(s, k, w))# Compression consumes an already expanded 64-word schedule.def compress(ws: List<&2, U32>, ks: List<&2, U32>, +s: S.State) -> S.State:  feedforward(s, rounds(ks, ws, s))# Generate each derived schedule word immediately before its round. The reverse# history is still retained for the recurrence, but the chronological 48-word# extension is never materialized.def expanded_rounds(n: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:  match n ks:    case 0n _:      s    case 1n+p Nil{}:      s    case 1n+p k <> kt:      +w = next_word(history)      expanded_rounds(p, w <> history, kt, step(s, k, w))# Consume the original block words, then continue directly with its expansion.def schedule_rounds(ws: List<&2, U32>, +extra: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:  match ws ks:    case Nil{} _:      expanded_rounds(extra, history, ks, s)    case w <> wt Nil{}:      s    case w <> wt k <> kt:      schedule_rounds(wt, extra, history, kt, step(s, k, w))# A fixed rolling window drops schedule words as soon as they are older than 16# rounds. This avoids growing and reference-counting the reverse history list.def window_rounds(n: Nat, win: ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:  match n win ks:    case 0n _ _:      s    case 1n+q _ Nil{}:      s    case 1n+q W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:      +w = (small1(b) + g + small0(t) + u : U32)      window_rounds(q, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,        step(s, k, w))def window_schedule_rounds(ws: List<&2, U32>, +extra: Nat, win: ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:  match ws ks:    case Nil{} _:      window_rounds(extra, win, ks, s)    case w <> wt Nil{}:      s    case w <> wt k <> kt:      window_schedule_rounds(wt, extra, win, kt, step(s, k, w))def fused_compress_slow(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:  feedforward(s, schedule_rounds(block, extra, List.reverse(&2, U32, block), ks, s))def fused_compress(+block: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:  match block:    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:      feedforward(s, window_schedule_rounds(        [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra,        W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))    case _:      fused_compress_slow(block, extra, ks, s)# Fast path for the 16-word blocks produced by block_bytes. It executes the# seed rounds directly and constructs only the fixed rolling window.def window_compress16(+a: U32, +b: U32, +c: U32, +d: U32,  +e: U32, +f: U32, +g: U32, +h: U32,  +i: U32, +j: U32, +k: U32, +l: U32,  +m: U32, +n: U32, +o: U32, +p: U32,  +extra: Nat, +ks: List<&2, U32>, +s: S.State) -> S.State:  match ks:    case k0 <> k1 <> k2 <> k3 <> k4 <> k5 <> k6 <> k7 <>      k8 <> k9 <> k10 <> k11 <> k12 <> k13 <> k14 <> k15 <> kt:      s1 = step(s, k0, a)      s2 = step(s1, k1, b)      s3 = step(s2, k2, c)      s4 = step(s3, k3, d)      s5 = step(s4, k4, e)      s6 = step(s5, k5, f)      s7 = step(s6, k6, g)      s8 = step(s7, k7, h)      s9 = step(s8, k8, i)      s10 = step(s9, k9, j)      s11 = step(s10, k10, k)      s12 = step(s11, k11, l)      s13 = step(s12, k12, m)      s14 = step(s13, k13, n)      s15 = step(s14, k14, o)      s16 = step(s15, k15, p)      feedforward(s, window_rounds(extra,        W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, kt, s16))    case _:      fused_compress([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], extra, ks, s)def be32(+x: U32) -> List<&2, U32>:  [U32.shrn(x, 24n), (U32.shrn(x, 16n) .&. 255 : U32),   (U32.shrn(x, 8n) .&. 255 : U32), (x .&. 255 : U32)]def length_octets(count: Nat, +n: Nat, acc: List<&2, U32>) -> List<&2, U32>:  match count:    case 0n:      acc    case 1n+p:      length_octets(p, Nat.div(n, 256n), U32.from_nat(Nat.mod(n, 256n)) <> acc)def bit_length(+n: Nat) -> List<&2, U32>:  length_octets(7n, Nat.div(n, 32n),    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])def pack(a: U32, b: U32, c: U32, d: U32) -> U32:  (U32.shln((a .&. 255 : U32), 24n)    .|. U32.shln((b .&. 255 : U32), 16n)    .|. U32.shln((c .&. 255 : U32), 8n) .|. (d .&. 255) : U32)def digest(s: S.State) -> List<&2, U32>:  S.H{a, b, c, d, e, f, g, h} = s  [a, b, c, d, e, f, g, h]# Generic block decoder over a padded byte list and any constant table. The# fast path below is proved equal to it with the FIPS table.def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, s: S.State) -> S.State:  match bytes:    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:      block_bytes(rest, extra, ks, window_compress16(        pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),        pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),        pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),        pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),        extra, ks, s))    case _:      s# FIPS 180-4 round constants, the table the specialized rounds below inline.def round_constants() -> List<&2, U32>:  [1116352408, 1899447441, 3049323471, 3921009573,   961987163, 1508970993, 2453635748, 2870763221,   3624381080, 310598401, 607225278, 1426881987,   1925078388, 2162078206, 2614888103, 3248222580,   3835390401, 4022224774, 264347078, 604807628,   770255983, 1249150122, 1555081692, 1996064986,   2554220882, 2821834349, 2952996808, 3210313671,   3336571891, 3584528711, 113926993, 338241895,   666307205, 773529912, 1294757372, 1396182291,   1695183700, 1986661051, 2177026350, 2456956037,   2730485921, 2820302411, 3259730800, 3345764771,   3516065817, 3600352804, 4094571909, 275423344,   430227734, 506948616, 659060556, 883997877,   958139571, 1322822218, 1537002063, 1747873779,   1955562222, 2024104815, 2227730452, 2361852424,   2428436474, 2756734187, 3204031479, 3329325298]# SHA-256 round t (16 <= t < 64) with its constant as a literal. Like# window_rounds, q bounds the remaining rounds (48 for SHA-256) and each round# derives its schedule word from the rolling window before continuing with# round t+1. Defined last-to-first because names must precede use.def kr64(q: Nat, win: ShaWindow, s: S.State) -> S.State:  sdef kr63(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr64(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3329325298, w))def kr62(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr63(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3204031479, w))def kr61(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr62(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2756734187, w))def kr60(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr61(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2428436474, w))def kr59(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr60(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2361852424, w))def kr58(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr59(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2227730452, w))def kr57(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr58(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2024104815, w))def kr56(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr57(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1955562222, w))def kr55(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr56(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1747873779, w))def kr54(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr55(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1537002063, w))def kr53(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr54(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1322822218, w))def kr52(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr53(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 958139571, w))def kr51(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr52(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 883997877, w))def kr50(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr51(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 659060556, w))def kr49(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr50(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 506948616, w))def kr48(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr49(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 430227734, w))def kr47(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr48(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 275423344, w))def kr46(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr47(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4094571909, w))def kr45(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr46(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3600352804, w))def kr44(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr45(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3516065817, w))def kr43(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr44(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3345764771, w))def kr42(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr43(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3259730800, w))def kr41(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr42(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2820302411, w))def kr40(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr41(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2730485921, w))def kr39(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr40(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2456956037, w))def kr38(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr39(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2177026350, w))def kr37(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr38(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1986661051, w))def kr36(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr37(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1695183700, w))def kr35(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr36(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1396182291, w))def kr34(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr35(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1294757372, w))def kr33(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr34(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 773529912, w))def kr32(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr33(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 666307205, w))def kr31(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr32(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 338241895, w))def kr30(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr31(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 113926993, w))def kr29(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr30(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3584528711, w))def kr28(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr29(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3336571891, w))def kr27(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr28(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3210313671, w))def kr26(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr27(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2952996808, w))def kr25(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr26(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2821834349, w))def kr24(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr25(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 2554220882, w))def kr23(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr24(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1996064986, w))def kr22(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr23(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1555081692, w))def kr21(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr22(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 1249150122, w))def kr20(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr21(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 770255983, w))def kr19(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr20(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 604807628, w))def kr18(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr19(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 264347078, w))def kr17(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr18(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 4022224774, w))def kr16(q: Nat, win: ShaWindow, s: S.State) -> S.State:  match q win:    case 0n _:      s    case 1n+z W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u}:      +w = (small1(b) + g + small0(t) + u : U32)      kr17(z, W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, step(s, 3835390401, w))# window_compress16 specialized to the FIPS table: no constant list is walked.def fips_compress16(+a: U32, +b: U32, +c: U32, +d: U32,  +e: U32, +f: U32, +g: U32, +h: U32,  +i: U32, +j: U32, +k: U32, +l: U32,  +m: U32, +n: U32, +o: U32, +p: U32, +q: Nat, +s: S.State) -> S.State:  s1 = step(s, 1116352408, a)  s2 = step(s1, 1899447441, b)  s3 = step(s2, 3049323471, c)  s4 = step(s3, 3921009573, d)  s5 = step(s4, 961987163, e)  s6 = step(s5, 1508970993, f)  s7 = step(s6, 2453635748, g)  s8 = step(s7, 2870763221, h)  s9 = step(s8, 3624381080, i)  s10 = step(s9, 310598401, j)  s11 = step(s10, 607225278, k)  s12 = step(s11, 1426881987, l)  s13 = step(s12, 1925078388, m)  s14 = step(s13, 2162078206, n)  s15 = step(s14, 2614888103, o)  s16 = step(s15, 3248222580, p)  feedforward(s, kr16(q, W{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, s16))# FIPS padding suffix for a message of n bytes, computed with modular# arithmetic. The proofs state the streaming hash in terms of it.def suffix(+n: Nat) -> List<&2, U32>:  128 <> List.append(&2, U32,    List.replicate(U32, Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), 0), bit_length(n))# Big-endian words of the 64-bit message bit length 8n, computed from n with# exactly the digit expressions bit_length produces, but without building and# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.def len_hi(+n: Nat) -> U32:  +d0 = Nat.div(n, 32n)  +d1 = Nat.div(d0, 256n)  +d2 = Nat.div(d1, 256n)  +d3 = Nat.div(d2, 256n)  +d4 = Nat.div(d3, 256n)  +d5 = Nat.div(d4, 256n)  +d6 = Nat.div(d5, 256n)  pack(U32.from_nat(Nat.mod(d6, 256n)), U32.from_nat(Nat.mod(d5, 256n)),    U32.from_nat(Nat.mod(d4, 256n)), U32.from_nat(Nat.mod(d3, 256n)))def len_lo(+n: Nat) -> U32:  +d0 = Nat.div(n, 32n)  +d1 = Nat.div(d0, 256n)  +d2 = Nat.div(d1, 256n)  pack(U32.from_nat(Nat.mod(d2, 256n)), U32.from_nat(Nat.mod(d1, 256n)),    U32.from_nat(Nat.mod(d0, 256n)), U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n))# Final block(s) for an n-byte message ending in r = 0..63 tail bytes. Each# tail length has its own padded layout: the tail bytes, the 0x80 marker, the# zero fill and the big-endian bit length are packed straight into schedule# words, so no padded list is built.def fin0(+n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin1(+t0: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin2(+t0: U32, +t1: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, t1, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin3(+t0: U32, +t1: U32, +t2: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, t1, t2, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin4(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, t1, t2, t3), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin5(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)def fin6(+t0: U32, +t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +n: Nat, +extra: Nat, s: S.State) -> S.State:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(128, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, 128, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, 128, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, 128), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(128, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, 128, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, 128, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, 128), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(128, 0, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, 128, 0, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, 128, 0), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, 128), len_hi(n), len_lo(n),    extra, s)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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(128, 0, 0, 0), pack(0, 0, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, 128, 0, 0), pack(0, 0, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, 128, 0), pack(0, 0, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, 128), pack(0, 0, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(128, 0, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, 128, 0, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, t61, 128, 0),    extra, s))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:  fips_compress16(pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), pack(0, 0, 0, 0), len_hi(n), len_lo(n),    extra, fips_compress16(pack(t0, t1, t2, t3), pack(t4, t5, t6, t7), pack(t8, t9, t10, t11), pack(t12, t13, t14, t15), pack(t16, t17, t18, t19), pack(t20, t21, t22, t23), pack(t24, t25, t26, t27), pack(t28, t29, t30, t31), pack(t32, t33, t34, t35), pack(t36, t37, t38, t39), pack(t40, t41, t42, t43), pack(t44, t45, t46, t47), pack(t48, t49, t50, t51), pack(t52, t53, t54, t55), pack(t56, t57, t58, t59), pack(t60, t61, t62, 128),    extra, s))# Tail-recursive block loop over an already padded byte list.def fips_blocks(bytes: List<&2, U32>, +extra: Nat, s: S.State) -> S.State:  match bytes:    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:      fips_blocks(rest, extra, fips_compress16(pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15), pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31), pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47), pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63), extra, s))    case _:      sdef zeros_onto(z: Nat, acc: List<&2, U32>) -> List<&2, U32>:  match z:    case 0n:      acc    case 1n+p:      zeros_onto(p, 0 <> acc)# The padding suffix built only with tail-recursive loops.def padding(+n: Nat) -> List<&2, U32>:  128 <> zeros_onto(Nat.mod(Nat.sub(119n, Nat.mod(n, 64n)), 64n), bit_length(n))def byte_count(bytes: List<&2, U32>, acc: Nat) -> Nat:  match bytes:    case Nil{}:      acc    case h <> t:      byte_count(t, 1n+acc)# Final block(s) of an n-byte message whose tail has fewer than 64 bytes.# stream never passes 64 or more bytes; that case pads with tail-recursive# loops. The match is exhaustive: a default case would make Bend rebuild the# consumed cells at every depth. Length words are computed directly from n; note# that sharing any List<U32> would make Bend reference-count every list match,# including the input loop in stream.def finish_n(+tail: List<&2, U32>, +n: Nat, +extra: Nat, s: S.State) -> S.State:  match tail:    case Nil{}:      fin0(n, extra, s)    case t0 <> Nil{}:      fin1(t0, n, extra, s)    case t0 <> t1 <> Nil{}:      fin2(t0, t1, n, extra, s)    case t0 <> t1 <> t2 <> Nil{}:      fin3(t0, t1, t2, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> Nil{}:      fin4(t0, t1, t2, t3, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> Nil{}:      fin5(t0, t1, t2, t3, t4, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> Nil{}:      fin6(t0, t1, t2, t3, t4, t5, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> Nil{}:      fin7(t0, t1, t2, t3, t4, t5, t6, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> Nil{}:      fin8(t0, t1, t2, t3, t4, t5, t6, t7, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> Nil{}:      fin9(t0, t1, t2, t3, t4, t5, t6, t7, t8, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> Nil{}:      fin10(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> Nil{}:      fin11(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> Nil{}:      fin12(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> Nil{}:      fin13(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> Nil{}:      fin14(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> Nil{}:      fin15(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> Nil{}:      fin16(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> Nil{}:      fin17(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> Nil{}:      fin18(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> Nil{}:      fin19(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> Nil{}:      fin20(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, n, extra, s)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> Nil{}:      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)    case t0 <> t1 <> t2 <> t3 <> t4 <> t5 <> t6 <> t7 <> t8 <> t9 <> t10 <> t11 <> t12 <> t13 <> t14 <> t15 <> t16 <> t17 <> t18 <> t19 <> t20 <> t21 <> Nil{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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{}:      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)    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:      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)# count is the number of bytes already hashed, always a multiple of 64.def finish(+tail: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:  finish_n(tail, byte_count(tail, count), extra, s)# Compress complete 64-byte blocks straight from the input list, so the# message is never copied, counted or reversed. count is the number of bytes# already hashed and extra the number of derived schedule words (48).def stream(+bytes: List<&2, U32>, count: Nat, +extra: Nat, s: S.State) -> S.State:  match bytes:    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:      stream(rest, Nat.add(64n, count), extra, fips_compress16(        pack(b0, b1, b2, b3), pack(b4, b5, b6, b7), pack(b8, b9, b10, b11), pack(b12, b13, b14, b15),        pack(b16, b17, b18, b19), pack(b20, b21, b22, b23), pack(b24, b25, b26, b27), pack(b28, b29, b30, b31),        pack(b32, b33, b34, b35), pack(b36, b37, b38, b39), pack(b40, b41, b42, b43), pack(b44, b45, b46, b47),        pack(b48, b49, b50, b51), pack(b52, b53, b54, b55), pack(b56, b57, b58, b59), pack(b60, b61, b62, b63),        extra, s))    case _:      finish(bytes, count, extra, s)# ASCII convenience only; binary inputs use sha256 directly.def ascii(s: String) -> List<&2, U32>:  match s:    case SNil{}:      Nil{}    case SCon{Chr{c}, t}:      c <> ascii(t)def hex_digit_if(x: U32, small: Bool) -> Char:  match small:    case True{}:      Chr{(48 + x : U32)}    case False{}:      Chr{(87 + x : U32)}def hex_digit(+x: U32) -> Char:  hex_digit_if(x, U32.is_lt(x, 10))def hex_word_go(n: Nat, +x: U32, acc: String) -> String:  match n:    case 0n:      acc    case 1n+p:      hex_word_go(p, U32.shrn(x, 4n), SCon{hex_digit((x .&. 15 : U32)), acc})def hex_word(x: U32) -> String:  hex_word_go(8n, x, "")def hex(ws: List<&2, U32>) -> String:  match ws:    case Nil{}:      ""    case w <> t:      hex_word(w) ++ hex(t)def sha256(bytes: List<&2, U32>) -> List<&2, U32>:  digest(stream(bytes, 0n, 48n, initial()))