def gctr_inv
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:304
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
304
305def gctr_inv(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +xs: List<&2, U32>, +cb: List<&2, U32>) -> {G.gctr(nk, nr, key, G.gctr(nk, nr, key, xs, cb), cb) == xs : List<&2, U32>}:
306 match xs:
307 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest:
308 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest, cb), U32.xor(x0, kb(nk, nr, key, cb, 0n)) <> U32.xor(x1, kb(nk, nr, key, cb, 1n)) <> U32.xor(x2, kb(nk, nr, key, cb, 2n)) <> U32.xor(x3, kb(nk, nr, key, cb, 3n)) <> U32.xor(x4, kb(nk, nr, key, cb, 4n)) <> U32.xor(x5, kb(nk, nr, key, cb, 5n)) <> U32.xor(x6, kb(nk, nr, key, cb, 6n)) <> U32.xor(x7, kb(nk, nr, key, cb, 7n)) <> U32.xor(x8, kb(nk, nr, key, cb, 8n)) <> U32.xor(x9, kb(nk, nr, key, cb, 9n)) <> U32.xor(x10, kb(nk, nr, key, cb, 10n)) <> U32.xor(x11, kb(nk, nr, key, cb, 11n)) <> U32.xor(x12, kb(nk, nr, key, cb, 12n)) <> U32.xor(x13, kb(nk, nr, key, cb, 13n)) <> U32.xor(x14, kb(nk, nr, key, cb, 14n)) <> U32.xor(x15, kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, rest, G.inc32(cb)), gctr_block(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, rest, cb)) : {G.gctr(nk, nr, key, _, cb) == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest : List<&2, U32>}
309 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)) <> U32.xor(x1, kb(nk, nr, key, cb, 1n)) <> U32.xor(x2, kb(nk, nr, key, cb, 2n)) <> U32.xor(x3, kb(nk, nr, key, cb, 3n)) <> U32.xor(x4, kb(nk, nr, key, cb, 4n)) <> U32.xor(x5, kb(nk, nr, key, cb, 5n)) <> U32.xor(x6, kb(nk, nr, key, cb, 6n)) <> U32.xor(x7, kb(nk, nr, key, cb, 7n)) <> U32.xor(x8, kb(nk, nr, key, cb, 8n)) <> U32.xor(x9, kb(nk, nr, key, cb, 9n)) <> U32.xor(x10, kb(nk, nr, key, cb, 10n)) <> U32.xor(x11, kb(nk, nr, key, cb, 11n)) <> U32.xor(x12, kb(nk, nr, key, cb, 12n)) <> U32.xor(x13, kb(nk, nr, key, cb, 13n)) <> U32.xor(x14, kb(nk, nr, key, cb, 14n)) <> U32.xor(x15, kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, rest, G.inc32(cb)), cb), U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)) <> U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)) <> U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)) <> U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)) <> U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)) <> U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)) <> U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)) <> U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)) <> U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)) <> U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)) <> U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)) <> U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)) <> U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)) <> U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n)) <> U32.xor(U32.xor(x14, kb(nk, nr, key, cb, 14n)), kb(nk, nr, key, cb, 14n)) <> U32.xor(U32.xor(x15, kb(nk, nr, key, cb, 15n)), kb(nk, nr, key, cb, 15n)) <> G.gctr(nk, nr, key, G.gctr(nk, nr, key, rest, G.inc32(cb)), G.inc32(cb)), gctr_block(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n)), U32.xor(x15, kb(nk, nr, key, cb, 15n)), G.gctr(nk, nr, key, rest, G.inc32(cb)), cb)) : {_ == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest : List<&2, U32>}
310 cancel16(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n), kb(nk, nr, key, cb, 14n), kb(nk, nr, key, cb, 15n), G.gctr(nk, nr, key, G.gctr(nk, nr, key, rest, G.inc32(cb)), G.inc32(cb)), rest, gctr_inv(nk, nr, key, rest, G.inc32(cb)))
311 case Nil{}:
312 {==}
313 case x0 <> Nil{}:
314 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n))], gctr_part1(nk, nr, key, x0, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0] : List<&2, U32>}
315 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n))], gctr_part1(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), cb)) : {_ == [x0] : List<&2, U32>}
316 cancel1(x0, kb(nk, nr, key, cb, 0n))
317 case x0 <> x1 <> Nil{}:
318 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n))], gctr_part2(nk, nr, key, x0, x1, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1] : List<&2, U32>}
319 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n))], gctr_part2(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), cb)) : {_ == [x0, x1] : List<&2, U32>}
320 cancel2(x0, x1, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n))
321 case x0 <> x1 <> x2 <> Nil{}:
322 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n))], gctr_part3(nk, nr, key, x0, x1, x2, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2] : List<&2, U32>}
323 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n))], gctr_part3(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), cb)) : {_ == [x0, x1, x2] : List<&2, U32>}
324 cancel3(x0, x1, x2, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n))
325 case x0 <> x1 <> x2 <> x3 <> Nil{}:
326 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n))], gctr_part4(nk, nr, key, x0, x1, x2, x3, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3] : List<&2, U32>}
327 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n))], gctr_part4(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), cb)) : {_ == [x0, x1, x2, x3] : List<&2, U32>}
328 cancel4(x0, x1, x2, x3, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n))
329 case x0 <> x1 <> x2 <> x3 <> x4 <> Nil{}:
330 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n))], gctr_part5(nk, nr, key, x0, x1, x2, x3, x4, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4] : List<&2, U32>}
331 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n))], gctr_part5(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), cb)) : {_ == [x0, x1, x2, x3, x4] : List<&2, U32>}
332 cancel5(x0, x1, x2, x3, x4, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n))
333 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> Nil{}:
334 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n))], gctr_part6(nk, nr, key, x0, x1, x2, x3, x4, x5, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}
335 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n))], gctr_part6(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}
336 cancel6(x0, x1, x2, x3, x4, x5, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n))
337 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> Nil{}:
338 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n))], gctr_part7(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}
339 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n))], gctr_part7(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}
340 cancel7(x0, x1, x2, x3, x4, x5, x6, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n))
341 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> Nil{}:
342 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n))], gctr_part8(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}
343 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n))], gctr_part8(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}
344 cancel8(x0, x1, x2, x3, x4, x5, x6, x7, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n))
345 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> Nil{}:
346 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n))], gctr_part9(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}
347 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n))], gctr_part9(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}
348 cancel9(x0, x1, x2, x3, x4, x5, x6, x7, x8, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n))
349 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> Nil{}:
350 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n))], gctr_part10(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}
351 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n))], gctr_part10(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}
352 cancel10(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n))
353 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> Nil{}:
354 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))], gctr_part11(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}
355 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n))], gctr_part11(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}
356 cancel11(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n))
357 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> Nil{}:
358 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n))], gctr_part12(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
359 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n))], gctr_part12(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}
360 cancel12(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n))
361 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> Nil{}:
362 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n))], gctr_part13(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
363 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n))], gctr_part13(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}
364 cancel13(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n))
365 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> Nil{}:
366 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n))], gctr_part14(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] : List<&2, U32>}
367 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)), U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n))], gctr_part14(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] : List<&2, U32>}
368 cancel14(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n))
369 case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> Nil{}:
370 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14], cb), [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))], gctr_part15(nk, nr, key, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, cb)) : {G.gctr(nk, nr, key, _, cb) == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] : List<&2, U32>}
371 %Equal.sym(List<&2, U32>, G.gctr(nk, nr, key, [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))], cb), [U32.xor(U32.xor(x0, kb(nk, nr, key, cb, 0n)), kb(nk, nr, key, cb, 0n)), U32.xor(U32.xor(x1, kb(nk, nr, key, cb, 1n)), kb(nk, nr, key, cb, 1n)), U32.xor(U32.xor(x2, kb(nk, nr, key, cb, 2n)), kb(nk, nr, key, cb, 2n)), U32.xor(U32.xor(x3, kb(nk, nr, key, cb, 3n)), kb(nk, nr, key, cb, 3n)), U32.xor(U32.xor(x4, kb(nk, nr, key, cb, 4n)), kb(nk, nr, key, cb, 4n)), U32.xor(U32.xor(x5, kb(nk, nr, key, cb, 5n)), kb(nk, nr, key, cb, 5n)), U32.xor(U32.xor(x6, kb(nk, nr, key, cb, 6n)), kb(nk, nr, key, cb, 6n)), U32.xor(U32.xor(x7, kb(nk, nr, key, cb, 7n)), kb(nk, nr, key, cb, 7n)), U32.xor(U32.xor(x8, kb(nk, nr, key, cb, 8n)), kb(nk, nr, key, cb, 8n)), U32.xor(U32.xor(x9, kb(nk, nr, key, cb, 9n)), kb(nk, nr, key, cb, 9n)), U32.xor(U32.xor(x10, kb(nk, nr, key, cb, 10n)), kb(nk, nr, key, cb, 10n)), U32.xor(U32.xor(x11, kb(nk, nr, key, cb, 11n)), kb(nk, nr, key, cb, 11n)), U32.xor(U32.xor(x12, kb(nk, nr, key, cb, 12n)), kb(nk, nr, key, cb, 12n)), U32.xor(U32.xor(x13, kb(nk, nr, key, cb, 13n)), kb(nk, nr, key, cb, 13n)), U32.xor(U32.xor(x14, kb(nk, nr, key, cb, 14n)), kb(nk, nr, key, cb, 14n))], gctr_part15(nk, nr, key, U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n)), cb)) : {_ == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] : List<&2, U32>}
372 cancel15(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, kb(nk, nr, key, cb, 0n), kb(nk, nr, key, cb, 1n), kb(nk, nr, key, cb, 2n), kb(nk, nr, key, cb, 3n), kb(nk, nr, key, cb, 4n), kb(nk, nr, key, cb, 5n), kb(nk, nr, key, cb, 6n), kb(nk, nr, key, cb, 7n), kb(nk, nr, key, cb, 8n), kb(nk, nr, key, cb, 9n), kb(nk, nr, key, cb, 10n), kb(nk, nr, key, cb, 11n), kb(nk, nr, key, cb, 12n), kb(nk, nr, key, cb, 13n), kb(nk, nr, key, cb, 14n))