def b64.dualL

bend-osdev-cipher-core@0.1.0.0 · PROOF.bend:138

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

138# a block read from a list of bytes is written back as those bytes
139def 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}:
140  match xs:
141    case Nil{}:
142      h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Nil{}) : B.Octets}, b64.nsome(bl, h))
143    case Con{+a0, +x1}:
144      match x1:
145        case Nil{}:
146          h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Nil{}}) : B.Octets}, b64.nsome(bl, h))
147        case Con{+a1, +x2}:
148          match x2:
149            case Nil{}:
150              h => Empty.absurd({L.LcBlock64.to_octets(bl) == B.Octets.of_list(Con{a0, Con{a1, Nil{}}}) : B.Octets}, b64.nsome(bl, h))
151            case Con{+a2, +x3}:
152              match x3:
153                case Nil{}:
154                  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))
155                case Con{+a3, +x4}:
156                  match x4:
157                    case Nil{}:
158                      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))
159                    case Con{+a4, +x5}:
160                      match x5:
161                        case Nil{}:
162                          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))
163                        case Con{+a5, +x6}:
164                          match x6:
165                            case Nil{}:
166                              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))
167                            case Con{+a6, +x7}:
168                              match x7:
169                                case Nil{}:
170                                  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))
171                                case Con{+a7, +x8}:
172                                  match x8:
173                                    case Nil{}:
174                                      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}
175                                        b64.dbits(a0, a1, a2, a3, a4, a5, a6, a7)
176                                    case Con{+a8, +x9}:
177                                      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))