~/jendhub

def b64.dual

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

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

180def b64.dual(+o: B.Octets, +bl: L.LcBlock64, em: {L.LcBlock64.of_octets(o) == Some{bl} : Maybe<&2, L.LcBlock64>}) -> {L.LcBlock64.to_octets(bl) == o : B.Octets}:
181  Equal.trans(B.Octets, L.LcBlock64.to_octets(bl), B.Octets.of_list(B.Octets.to_list(o)), o, b64.dualL(B.Octets.to_list(o), bl)(em), BL.octets_of_to(o))

Uses (10)

Used by (1)