PROOF.b64.dualL: def of bend-osdev-cipher-core@0.1.0.0
Import: import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as PROOF
Lines 138-177 of bend-osdev-cipher-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&start_line=138&end_line=177

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L

# a block read from a list of bytes is written back as those bytes
def b64.dualL(+xs: List<&2, U32>, +bl: L.LcBlock64) -> {L.lc.block_of(xs) == Some{bl} : Maybe<&2, L.LcBlock64>} -> {L.LcBlock64.to_octets(bl) == B.Octets.of_list(xs) : B.Octets}:
  match xs:
    case Nil{}:
      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Nil{}) : B.Octets}, b64.nsome(bl, h))
    case Con{+a0, +x1}:
      match x1:
        case Nil{}:
          h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Nil{}}) : B.Octets}, b64.nsome(bl, h))
        case Con{+a1, +x2}:
          match x2:
            case Nil{}:
              h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Nil{}}}) : B.Octets}, b64.nsome(bl, h))
            case Con{+a2, +x3}:
              match x3:
                case Nil{}:
                  h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Nil{}}}}) : B.Octets}, b64.nsome(bl, h))
                case Con{+a3, +x4}:
                  match x4:
                    case Nil{}:
                      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Nil{}}}}}) : B.Octets}, b64.nsome(bl, h))
                    case Con{+a4, +x5}:
                      match x5:
                        case Nil{}:
                          h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Nil{}}}}}}) : B.Octets}, b64.nsome(bl, h))
                        case Con{+a5, +x6}:
                          match x6:
                            case Nil{}:
                              h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Nil{}}}}}}}) : B.Octets}, b64.nsome(bl, h))
                            case Con{+a6, +x7}:
                              match x7:
                                case Nil{}:
                                  h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Nil{}}}}}}}}) : B.Octets}, b64.nsome(bl, h))
                                case Con{+a7, +x8}:
                                  match x8:
                                    case Nil{}:
                                      h => %Equal.cong(Maybe<&2, L.LcBlock64>, L.LcBlock64, mm => b64.mget(mm, bl), L.lc.block_of(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}), Some{bl}, h) : {L.LcBlock64.to_octets(_) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}) : B.Octets}
                                        b64.dbits(a0, a1, a2, a3, a4, a5, a6, a7)
                                    case Con{+a8, +x9}:
                                      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, x9}}}}}}}}}) : B.Octets}, b64.nsome(bl, h))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.dbits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.mget
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.nsome
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.to_octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.block_of