check.bend

bend-osdev-mode-core@0.1.0.0 · 66 lines · 9 definitions

1# mode-core on its own: a block's hex and byte forms, XOR, the round-trip
2# hypothesis over a toy permutation, and the refusal of a byte string that
3# is not 16 bytes. The modes' own packages test the modes.
4import Base
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
7
8# A toy permutation of blocks, NOT a cipher: the words rotated, then XOR
9# with the key block. Enough to run the mode's code paths (encryption and
10# decryption differ, so mixing them up shows); the mode is tested against
11# its specification over AES in bend-osdev-aes-modes (the specifications'
12# vectors) and in ref/ (against Python's cryptography).
13def toy.rot(b: M.CmBlock) -> M.CmBlock:
14  match b:
15    case M.CmBlock{w0, w1, w2, w3}:
16      M.CmBlock{w1, w2, w3, w0}
17
18def toy.unrot(b: M.CmBlock) -> M.CmBlock:
19  match b:
20    case M.CmBlock{w0, w1, w2, w3}:
21      M.CmBlock{w3, w0, w1, w2}
22
23def toy.enc(k: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
24  M.CmBlock.xor(k, toy.rot(b))
25
26def toy.dec(k: M.CmBlock, c: M.CmBlock) -> M.CmBlock:
27  toy.unrot(M.CmBlock.xor(k, c))
28
29def key() -> M.CmBlock:
30  M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}
31
32def key2() -> M.CmBlock:
33  M.CmBlock{2882400001, 305419896, 3735928559, 4027432973}
34
35def hexs(bs: List<&2, M.CmBlock>) -> String:
36  match bs:
37    case Nil{}:
38      ""
39    case Con{b, t}:
40      M.CmBlock.hex(b) ++ hexs(t)
41
42def maybe(m: Maybe<&2, M.CmBlock>) -> String:
43  match m:
44    case None{}:
45      "none"
46    case Some{b}:
47      M.CmBlock.hex(b)
48
49def main() -> IO(Unit):
50  +b : M.CmBlock = M.CmBlock{1122867, 1146447479, 2291772091, 3437096703}
51  do IO<Unit>:
52    IO.print("zero " ++ M.CmBlock.hex(M.CmBlock.zero()))
53    IO.print("block " ++ M.CmBlock.hex(b))
54    IO.print("xor " ++ M.CmBlock.hex(M.CmBlock.xor(b, key())))
55    IO.print("to_octets " ++ B.Octets.hex(M.CmBlock.to_octets(b)))
56    IO.print("of_octets " ++ maybe(M.CmBlock.of_octets(M.CmBlock.to_octets(b))))
57    IO.print("of_octets_15 " ++ maybe(M.CmBlock.of_octets(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14]))))
58    IO.print("dec_enc " ++ hexs(M.CmBlock.dec_enc(~M.CmBlock, ~toy.enc, ~toy.dec, key(), [b, key(), M.CmBlock.zero()])))
59
60#|zero 00000000000000000000000000000000
61#|block 00112233445566778899aabbccddeeff
62#|xor 01326754cdfeab9876451023ba89dcef
63#|to_octets 00112233445566778899aabbccddeeff
64#|of_octets 00112233445566778899aabbccddeeff
65#|of_octets_15 none
66#|dec_enc 00112233445566778899aabbccddeeff0123456789abcdeffedcba987654321000000000000000000000000000000000