def blk_bytes

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:151

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L

151# a 64-bit block's bytes, masked and read back
152def blk_bytes(b: L.LcBlock64) -> {L.lc.block_of(B.mask(L.lc.block_bytes(b, Nil{}))) == Some{b} : Maybe<&2, L.LcBlock64>}:
153  match b:
154    case L.LcBlock64{U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
155      {==}