bend-osdev-cipher-core Releases (1): 0.1.0.0 0x5c26418ab13c9e565c5b1309d2f085a0 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-cipher-core@0.1.0.0 Definitions (148, 1 to 100 shown): LAWS.block64_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=block64_octets_round_trip) # 64-bit blocks as bytes: a block read back from its 8 bytes is itself, 8 # bytes read as a block are written back as those bytes, and a list of # blocks read back from its bytes is itself law block64_octets_round_trip: for +b: L.LcBlock64 {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>} LAWS.block64_octets_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=block64_octets_dual) law block64_octets_dual: for +o: B.Octets for +b: L.LcBlock64 for e: {L.LcBlock64.of_octets(o) == Some{b} : Maybe<&2, L.LcBlock64>} {L.LcBlock64.to_octets(b) == o : B.Octets} LAWS.blocks64_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=blocks64_octets_round_trip) law blocks64_octets_round_trip: for +bs: List<&2, L.LcBlock64> {X.Lc64.blocks_of(X.Lc64.octets_of(bs)) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>} LAWS.word_xor_cancel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=word_xor_cancel) # XOR undone, for every word of any width, every 32-bit word and every # 64-bit block law word_xor_cancel: for n: Nat for a: Word(n) for b: Word(n) {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)} LAWS.u32_xor_cancel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=u32_xor_cancel) law u32_xor_cancel: for a: U32 for b: U32 {a == U32.xor(U32.xor(a, b), b) : U32} LAWS.block64_xor_cancel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=block64_xor_cancel) law block64_xor_cancel: for a: L.LcBlock64 for b: L.LcBlock64 {b == L.LcBlock64.xor(a, L.LcBlock64.xor(a, b)) : L.LcBlock64} LAWS.rotl1_rotl31 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=rotl1_rotl31) # the rotations by 1 and 31 bits on bits undo each other, and the byte swap # on bits undoes itself, for every word law rotl1_rotl31: for x: U32 {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32} LAWS.rotl31_rotl1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=rotl31_rotl1) law rotl31_rotl1: for x: U32 {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32} LAWS.bswap_bswap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=bswap_bswap) law bswap_bswap: for x: U32 {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32} LAWS.feistel_unrun_run (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=feistel_unrun_run) # Feistel rounds over any round function f and any round keys: the rounds # undone last to first undo the rounds, and the other way round law feistel_unrun_run: for ~RK: Data for ~f: RK -> U32 -> U32 for ks: List<&2, RK> for +b: L.LcBlock64 {b == L.lc.fe.unrun(~RK, ~f, ks, L.lc.fe.run(~RK, ~f, ks, b)) : L.LcBlock64} LAWS.feistel_run_unrun (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=feistel_run_unrun) law feistel_run_unrun: for ~RK: Data for ~f: RK -> U32 -> U32 for ks: List<&2, RK> for +b: L.LcBlock64 {b == L.lc.fe.run(~RK, ~f, ks, L.lc.fe.unrun(~RK, ~f, ks, b)) : L.LcBlock64} LAWS.modes64_ecb_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=modes64_ecb_blocks) # The 64-bit modes over any cipher: decryption after encryption on blocks is # the structural forms' (X.m64.ecb, X.m64.cbc.enc, X.m64.cbc.dec), over # which a cipher's own round trip proves the mode's by induction; and on # bytes, for the bytes of a list of blocks under the bytes of an IV, it is # the block layer's law modes64_ecb_blocks: for ~K: Data for ~enc: K -> L.LcBlock64 -> L.LcBlock64 for ~dec: K -> L.LcBlock64 -> L.LcBlock64 for +k: K for +bs: List<&2, L.LcBlock64> {X.m64.ecb(~K, ~dec, k, X.m64.ecb(~K, ~enc, k, bs)) == X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)) : List<&2, L.LcBlock64>} LAWS.modes64_cbc_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=modes64_cbc_blocks) law modes64_cbc_blocks: for ~K: Data for ~enc: K -> L.LcBlock64 -> L.LcBlock64 for ~dec: K -> L.LcBlock64 -> L.LcBlock64 for +k: K for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {X.m64.cbc.dec(~K, ~dec, k, X.m64.cbc.enc(~K, ~enc, k, bs, iv), iv) == X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)) : List<&2, L.LcBlock64>} LAWS.modes64_ecb_octets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=modes64_ecb_octets) law modes64_ecb_octets: for ~K: Data for ~enc: K -> L.LcBlock64 -> L.LcBlock64 for ~dec: K -> L.LcBlock64 -> L.LcBlock64 for +k: K for +bs: List<&2, L.LcBlock64> {Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~dec, k, X.Lc64.ecb_encrypt_blocks(~K, ~enc, k, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.ecb_encrypt(~K, ~enc, k, X.Lc64.octets_of(bs)), c => X.Lc64.ecb_decrypt(~K, ~dec, k, c)) : Result<&2, &2, L.LcError, B.Octets>} LAWS.modes64_cbc_octets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=modes64_cbc_octets) law modes64_cbc_octets: for ~K: Data for ~enc: K -> L.LcBlock64 -> L.LcBlock64 for ~dec: K -> L.LcBlock64 -> L.LcBlock64 for +k: K for +iv: L.LcBlock64 for +bs: List<&2, L.LcBlock64> {Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs)))} == Result.bind(&2, &2, L.LcError, B.Octets, B.Octets, X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)), c => X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), c)) : Result<&2, &2, L.LcError, B.Octets>} LAWS.modes64_not_whole_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&name=modes64_not_whole_blocks) # the 64-bit modes refuse a message that is not whole blocks law modes64_not_whole_blocks: {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, Unit, bs => Unit{}, X.Lc64.blocks_of(B.Octets.zeros(12n))) == Fail{L.LcNotBlockMultiple{12n}} : Result<&2, &2, L.LcError, Unit>} PROOF.bool_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=bool_xx) def bool_xx(a: Bool, b: Bool) -> {a == Bool.xor(Bool.xor(a, b), b) : Bool}: PROOF.word_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=word_xx) def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}: PROOF.u32_xx (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=u32_xx) def u32_xx(a: U32, b: U32) -> {a == U32.xor(U32.xor(a, b), b) : U32}: PROOF.rot_1_31 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=rot_1_31) def rot_1_31(x: U32) -> {x == L.lc.rotl1.bits(L.lc.rotl31.bits(x)) : U32}: PROOF.rot_31_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=rot_31_1) def rot_31_1(x: U32) -> {x == L.lc.rotl31.bits(L.lc.rotl1.bits(x)) : U32}: PROOF.bswap2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=bswap2) def bswap2(x: U32) -> {x == L.lc.bswap.bits(L.lc.bswap.bits(x)) : U32}: PROOF.blk_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=blk_bytes) # a 64-bit block's bytes, masked and read back def blk_bytes(b: L.LcBlock64) -> {L.lc.block_of(B.mask(L.lc.block_bytes(b, Nil{}))) == Some{b} : Maybe<&2, L.LcBlock64>}: PROOF.blk8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=blk8) def blk8(hi: U32, lo: U32) -> {L.LcBlock64{hi, lo} == L.lc.block8(B.byte(L.lc.b0.bits(hi)), B.byte(L.lc.b1.bits(hi)), B.byte(L.lc.b2.bits(hi)), B.byte(L.lc.b3.bits(hi)), B.byte(L.lc.b0.bits(lo)), B.byte(L.lc.b1.bits(lo)), B.byte(L.lc.b2.bits(lo)), B.byte(L.lc.b3.bits(lo))) : L.LcBlock64}: PROOF.fe_unstep_step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=fe_unstep_step) def fe_unstep_step(~RK: Data, ~f: RK -> U32 -> U32, +k: RK, b: L.LcBlock64) -> {b == L.lc.fe.unstep(~RK, ~f, k, L.lc.fe.step(~RK, ~f, k, b)) : L.LcBlock64}: PROOF.fe_step_unstep (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=fe_step_unstep) def fe_step_unstep(~RK: Data, ~f: RK -> U32 -> U32, +k: RK, b: L.LcBlock64) -> {b == L.lc.fe.step(~RK, ~f, k, L.lc.fe.unstep(~RK, ~f, k, b)) : L.LcBlock64}: PROOF.fe_unrun_run (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=fe_unrun_run) def fe_unrun_run(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, +b: L.LcBlock64) -> {b == L.lc.fe.unrun(~RK, ~f, ks, L.lc.fe.run(~RK, ~f, ks, b)) : L.LcBlock64}: PROOF.fe_run_unrun (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=fe_run_unrun) def fe_run_unrun(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, +b: L.LcBlock64) -> {b == L.lc.fe.run(~RK, ~f, ks, L.lc.fe.unrun(~RK, ~f, ks, b)) : L.LcBlock64}: PROOF.b64.mget (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.mget) # a block read from 8 bytes is written back as those bytes (on their bits, # and then off a list of any length) def b64.mget(m: Maybe<&2, L.LcBlock64>, +d: L.LcBlock64) -> L.LcBlock64: PROOF.b64.mdisc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.mdisc) def b64.mdisc(m: Maybe<&2, L.LcBlock64>) -> Type: PROOF.b64.nsome (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.nsome) def b64.nsome(+bl: L.LcBlock64, h: {None{} == Some{bl} : Maybe<&2, L.LcBlock64>}) -> Empty: PROOF.b64.dbits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.dbits) # a block's bytes read from 8 bytes are those bytes (on their bits) def b64.dbits(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> {L.LcBlock64.to_octets(b64.mget(L.lc.block_of(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}), L.LcBlock64{0, 0})) == B.Octets.of_list(Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}) : B.Octets}: PROOF.b64.dualL (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.dualL) # 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}: PROOF.b64.dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.dual) def 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}: PROOF.m64_joins (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=m64_joins) # the bytes of the blocks bs in front of ys, structurally def m64_joins(bs: List<&2, L.LcBlock64>, ys: List<&2, U32>) -> List<&2, U32>: PROOF.m64_join_rev (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=m64_join_rev) def m64_join_rev(bs: List<&2, L.LcBlock64>, +zs: List<&2, L.LcBlock64>, +ys: List<&2, U32>) -> {X.m64.join(zs, m64_joins(bs, ys)) == X.m64.join(X.m64.rev_onto(bs, zs), ys) : List<&2, U32>}: PROOF.m64_split_joins (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=m64_split_joins) def m64_split_joins(bs: List<&2, L.LcBlock64>, +acc: List<&2, L.LcBlock64>) -> {X.m64.split(B.mask(m64_joins(bs, Nil{})), acc) == Some{X.m64.rev_onto(acc, bs)} : Maybe<&2, List<&2, L.LcBlock64>>}: PROOF.bool_xx2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=bool_xx2) def bool_xx2(a: Bool, b: Bool) -> {b == Bool.xor(a, Bool.xor(a, b)) : Bool}: PROOF.word_xx2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=word_xx2) def word_xx2(n: Nat, a: Word(n), b: Word(n)) -> {b == Word.xor(n, a, Word.xor(n, a, b)) : Word(n)}: PROOF.u32_xx2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=u32_xx2) def u32_xx2(a: U32, b: U32) -> {b == U32.xor(a, U32.xor(a, b)) : U32}: PROOF.b64_xx2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64_xx2) def b64_xx2(a: L.LcBlock64, b: L.LcBlock64) -> {b == L.LcBlock64.xor(a, L.LcBlock64.xor(a, b)) : L.LcBlock64}: PROOF.ecb_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=ecb_ref) def ecb_ref(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +acc: List<&2, L.LcBlock64>) -> {X.m64.ecb.go(~K, ~f, k, bs, acc) == X.m64.rev_onto(acc, X.m64.ecb(~K, ~f, k, bs)) : List<&2, L.LcBlock64>}: PROOF.cbc_enc_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=cbc_enc_ref) def cbc_enc_ref(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64, +acc: List<&2, L.LcBlock64>) -> {X.m64.cbc.enc.go(~K, ~enc, k, bs, iv, acc) == X.m64.rev_onto(acc, X.m64.cbc.enc(~K, ~enc, k, bs, iv)) : List<&2, L.LcBlock64>}: PROOF.cbc_dec_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=cbc_dec_ref) def cbc_dec_ref(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64, +acc: List<&2, L.LcBlock64>) -> {X.m64.cbc.dec.go(~K, ~dec, k, bs, iv, acc) == X.m64.rev_onto(acc, X.m64.cbc.dec(~K, ~dec, k, bs, iv)) : List<&2, L.LcBlock64>}: PROOF.cbc_enc_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=cbc_enc_ok) def cbc_enc_ok(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: L.LcBlock64, +bs: List<&2, L.LcBlock64>) -> {X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}: PROOF.cbc_dec_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=cbc_dec_ok) def cbc_dec_ok(~K: Data, ~dec: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: L.LcBlock64, +bs: List<&2, L.LcBlock64>) -> {X.Lc64.cbc_decrypt(~K, ~dec, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_decrypt_blocks(~K, ~dec, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}: PROOF.ecb_enc_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=ecb_enc_ok) def ecb_enc_ok(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +bs: List<&2, L.LcBlock64>) -> {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))) == Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}: PROOF.ecb_dec_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=ecb_dec_ok) def ecb_dec_ok(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +bs: List<&2, L.LcBlock64>) -> {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))) == Done{X.Lc64.octets_of(X.Lc64.ecb_decrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}: Check.err (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=err) def err(e: L.LcError) -> String: Check.show (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=show) def show(r: Result<&2, &2, L.LcError, B.Octets>) -> String: Check.show_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=show_blocks) def show_blocks(r: Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>) -> String: Check.show_some (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=show_some) def show_some(m: Maybe<&2, L.LcBlock64>) -> String: Check.word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=word) # a word as hex, through the block's hex form def word(x: U32) -> String: Check.toy (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=toy) # the toy cipher: XOR with the key block, its own inverse def toy(k: L.LcBlock64, b: L.LcBlock64) -> L.LcBlock64: Check.toy_key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=toy_key) def toy_key() -> L.LcBlock64: Check.toy_f (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=toy_f) # a toy round function for the Feistel rounds: x + k, then rotated by 7 def toy_f(k: U32, x: U32) -> U32: Check.msg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=msg) def msg() -> B.Octets: Check.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=iv) def iv() -> B.Octets: Check.ecb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=ecb) def ecb(m: B.Octets) -> String: Check.cbc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=cbc) def cbc(+v: B.Octets, m: B.Octets) -> String: Check.feistel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=feistel) def feistel(+b: L.LcBlock64) -> String: Check.tab (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=tab) def tab() -> String: Check.main (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/check.bend&name=main) def main() -> IO(Unit): CipherCore.LcError (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcError) # Every failure the package reports type LcError is Data: LcBadKeyLength{got: Nat} LcBadIvLength{got: Nat} LcNotBlockMultiple{len: Nat} CipherCore.LcBlock64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64) # A 64-bit block: two 32-bit words, big-endian (hi holds bytes 0 to 3, byte 0 # in its top 8 bits). Every value of the type is a block, so "decryption # inverts encryption" can be stated for every block. The type is open: a # cipher may build and match blocks directly. type LcBlock64 is Data: LcBlock64{hi: U32, lo: U32} CipherCore.LcBlock64.zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.zero) def LcBlock64.zero() -> LcBlock64: CipherCore.LcBlock64.xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.xor) def LcBlock64.xor(a: LcBlock64, b: LcBlock64) -> LcBlock64: CipherCore.lc.rotl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl) def lc.rotl(+x: U32, +n: Nat) -> U32: CipherCore.lc.byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.byte) # byte n of x, counting from the least significant (n = 0 to 3) def lc.byte(x: U32, n: Nat) -> U32: CipherCore.lc.be (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.be) # the word with bytes a (most significant), b, c, d def lc.be(a: U32, b: U32, c: U32, d: U32) -> U32: CipherCore.lc.le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.le) # the word with bytes a (least significant), b, c, d def lc.le(a: U32, b: U32, c: U32, d: U32) -> U32: CipherCore.lc.bit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.bit) # bit i of x (0 the least significant), as 0 or 1 def lc.bit(x: U32, i: Nat) -> U32: CipherCore.lc.at (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.at) # element n of a list of words (0 past the end) def lc.at(xs: List<&2, U32>, n: Nat) -> U32: CipherCore.lc.wrotl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.wrotl) # the (m + n)-bit word w rotated left by n def lc.wrotl(+m: Nat, +n: Nat, +w: Word(Nat.add(m, n))) -> Word(Nat.add(n, m)): CipherCore.lc.rotl1.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl1.bits) def lc.rotl1.bits(x: U32) -> U32: CipherCore.lc.rotl3.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl3.bits) def lc.rotl3.bits(x: U32) -> U32: CipherCore.lc.rotl5.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl5.bits) def lc.rotl5.bits(x: U32) -> U32: CipherCore.lc.rotl7.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl7.bits) def lc.rotl7.bits(x: U32) -> U32: CipherCore.lc.rotl10.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl10.bits) def lc.rotl10.bits(x: U32) -> U32: CipherCore.lc.rotl13.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl13.bits) def lc.rotl13.bits(x: U32) -> U32: CipherCore.lc.rotl19.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl19.bits) def lc.rotl19.bits(x: U32) -> U32: CipherCore.lc.rotl22.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl22.bits) def lc.rotl22.bits(x: U32) -> U32: CipherCore.lc.rotl25.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl25.bits) def lc.rotl25.bits(x: U32) -> U32: CipherCore.lc.rotl27.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl27.bits) def lc.rotl27.bits(x: U32) -> U32: CipherCore.lc.rotl29.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl29.bits) def lc.rotl29.bits(x: U32) -> U32: CipherCore.lc.rotl31.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rotl31.bits) def lc.rotl31.bits(x: U32) -> U32: CipherCore.lc.bits8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.bits8) # the low 8 bits of a word, as bits, and the byte with these bits def lc.bits8(b: U32) -> Word(8n): CipherCore.lc.of8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.of8) def lc.of8(s: Word(8n)) -> U32: CipherCore.lc.be.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.be.bits) # the word with bytes a (most significant), b, c, d, by bits def lc.be.bits(a: U32, b: U32, c: U32, d: U32) -> U32: CipherCore.lc.b0.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.b0.bits) # the bytes of w, by bits: b0 the most significant def lc.b0.bits(w: U32) -> U32: CipherCore.lc.b1.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.b1.bits) def lc.b1.bits(w: U32) -> U32: CipherCore.lc.b2.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.b2.bits) def lc.b2.bits(w: U32) -> U32: CipherCore.lc.b3.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.b3.bits) def lc.b3.bits(w: U32) -> U32: CipherCore.lc.bswap.bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.bswap.bits) # the word with its bytes in reverse order (big-endian to little-endian) def lc.bswap.bits(+w: U32) -> U32: CipherCore.lc.msb.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.msb.go) # the bits of a word, most significant first, in front of acc def lc.msb.go(n: Nat, w: Word(n), acc: List<&2, Bool>) -> List<&2, Bool>: CipherCore.lc.msb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.msb) def lc.msb(x: U32, acc: List<&2, Bool>) -> List<&2, Bool>: CipherCore.lc.rev_bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.rev_bits) # bs reversed, in front of acc def lc.rev_bits(bs: List<&2, Bool>, acc: List<&2, Bool>) -> List<&2, Bool>: CipherCore.lc.drop_bits (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.drop_bits) # all but the first n of bs def lc.drop_bits(n: Nat, bs: List<&2, Bool>) -> List<&2, Bool>: CipherCore.lc.word_lsb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.word_lsb) # the n-bit word whose bits, least significant first, are the first n of bs # (False past the end) def lc.word_lsb(n: Nat, bs: List<&2, Bool>) -> Word(n): CipherCore.lc.nth (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=lc.nth) # the element i of bs (False past the end) def lc.nth(bs: List<&2, Bool>, i: Nat) -> Bool: More: https://jend.leeeet.dev/packages/bend-osdev-cipher-core.txt?definitions_offset=100