def f128_bytes

bend-osdev-crypto@0.1.0.0 · PROOF.bend:91

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-crypto@0.1.0.0/inst_cm.bend as CM

91# a 128-bit block's 16 bytes, masked and read back
92def f128_bytes(b: M.CmBlock) -> {CM.cr.f128.block(B.mask(CM.cr.f128.bytes(b))) == Some{b} : Maybe<&2, M.CmBlock>}:
93  match b:
94    case M.CmBlock{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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{e0, WCon{e1, WCon{e2, WCon{e3, WCon{e4, WCon{e5, WCon{e6, WCon{e7, WCon{e8, WCon{e9, WCon{e10, WCon{e11, WCon{e12, WCon{e13, WCon{e14, WCon{e15, WCon{e16, WCon{e17, WCon{e18, WCon{e19, WCon{e20, WCon{e21, WCon{e22, WCon{e23, WCon{e24, WCon{e25, WCon{e26, WCon{e27, WCon{e28, WCon{e29, WCon{e30, WCon{e31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
95      {==}