Cts.cr.cts.enc.go: def of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/cts.bend as Cts
Lines 47-67 of bend-osdev-crypto@0.1.0.0/cts.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/cts.bend&start_line=47&end_line=67

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/octets.bend as O

# Encryption over the pieces (at least two; the last 1 to b bytes) from the
# chaining value v; acc holds the ciphertext so far, last first
def cr.cts.enc.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ps: List<&2, List<&2, U32>>, +k: K, +v: B.Octets, acc: List<&2, B.Octets>) -> B.Octets:
  match ps:
    case Con{p, t}:
      match t:
        case Con{q, u}:
          match u:
            case Nil{}:
              +x = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v))
              +last = B.Octets.of_list(q)
              +d = B.Octets.len(last)
              +cn = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.append(last, B.Octets.zeros(Nat.sub(bsize, d))), x))
              cr.cts.out(Con{B.Octets.take(d, x), Con{cn, acc}})
            case Con{r, w}:
              +c = cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v))
              cr.cts.enc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, Con{q, Con{r, w}}, k, c, Con{c, acc})
        case Nil{}:
          cr.cts.out(Con{cr.cts.b(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.xor(B.Octets.of_list(p), v)), acc})
    case Nil{}:
      cr.cts.out(acc)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.zeros
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/cts.bend&name=cr.cts.b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/cts.bend&name=cr.cts.out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/octets.bend&name=CrOct.xor