proof/AES_EnvelopeProof.bend
qasim-bend-kit@0.1.0.2 · 1,043 lines · 49 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import qasim-bend-kit@0.1.0.2/proof/AES_CanonicalProof.bend as Canonical
4
5def aes_hex_mask_15_lt_16(+value: U32) ->
6 {U32.is_lt(AES.hex_mask(value, 15), 16) == True{} : Bool}:
7 match value:
8 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
9
10def aes_hex_mask_255_lt_256(+value: U32) ->
11 {U32.is_lt(AES.hex_mask(value, 255), 256) == True{} : Bool}:
12 match value:
13 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
14
15def aes_bool_and_false(b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
16 match b:
17 case False{}: {==}
18 case True{}: {==}
19
20def aes_bool_and_true(b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
21 match b:
22 case False{}: {==}
23 case True{}: {==}
24
25def aes_hex_word_and_equiv(n: Nat, mask: Word(n), value: Word(n)) ->
26 {AES.hex_word_and(n, mask, value) == Word.and(n, value, mask) : Word(n)}:
27 match n mask value:
28 case 0n WNil{} WNil{}: {==}
29 case 1n+p WCon{False{}, mask_tail} WCon{value_bit, value_tail}:
30 recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
31 Equal.trans(Word(1n+p),
32 WCon{False{}, AES.hex_word_and(p, mask_tail, value_tail)},
33 WCon{False{}, Word.and(p, value_tail, mask_tail)},
34 WCon{Bool.and(value_bit, False{}), Word.and(p, value_tail, mask_tail)},
35 Equal.cong(Word(p), Word(1n+p), tail => WCon{False{}, tail},
36 AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
37 Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
38 False{}, Bool.and(value_bit, False{}), Equal.sym(Bool,
39 Bool.and(value_bit, False{}), False{}, aes_bool_and_false(value_bit))))
40 case 1n+p WCon{True{}, mask_tail} WCon{value_bit, value_tail}:
41 recursive = aes_hex_word_and_equiv(p, mask_tail, value_tail)
42 Equal.trans(Word(1n+p),
43 WCon{value_bit, AES.hex_word_and(p, mask_tail, value_tail)},
44 WCon{value_bit, Word.and(p, value_tail, mask_tail)},
45 WCon{Bool.and(value_bit, True{}), Word.and(p, value_tail, mask_tail)},
46 Equal.cong(Word(p), Word(1n+p), tail => WCon{value_bit, tail},
47 AES.hex_word_and(p, mask_tail, value_tail), Word.and(p, value_tail, mask_tail), recursive),
48 Equal.cong(Bool, Word(1n+p), bit => WCon{bit, Word.and(p, value_tail, mask_tail)},
49 value_bit, Bool.and(value_bit, True{}), Equal.sym(Bool,
50 Bool.and(value_bit, True{}), value_bit, aes_bool_and_true(value_bit))))
51
52def aes_hex_word_and_idempotent(n: Nat, mask: Word(n), +value: Word(n)) ->
53 {AES.hex_word_and(n, mask, AES.hex_word_and(n, mask, value)) ==
54 AES.hex_word_and(n, mask, value) : Word(n)}:
55 match n mask value:
56 case 0n WNil{} WNil{}: {==}
57 case 1n+p WCon{False{}, mask_tail} WCon{value_bit, value_tail}:
58 recursive = aes_hex_word_and_idempotent(p, mask_tail, value_tail)
59 Equal.cong(Word(p), Word(1n+p), tail => WCon{False{}, tail},
60 AES.hex_word_and(p, mask_tail,
61 AES.hex_word_and(p, mask_tail, value_tail)),
62 AES.hex_word_and(p, mask_tail, value_tail), recursive)
63 case 1n+p WCon{True{}, mask_tail} WCon{False{}, value_tail}:
64 recursive = aes_hex_word_and_idempotent(p, mask_tail, value_tail)
65 Equal.cong(Word(p), Word(1n+p), tail => WCon{False{}, tail},
66 AES.hex_word_and(p, mask_tail,
67 AES.hex_word_and(p, mask_tail, value_tail)),
68 AES.hex_word_and(p, mask_tail, value_tail), recursive)
69 case 1n+p WCon{True{}, mask_tail} WCon{True{}, value_tail}:
70 recursive = aes_hex_word_and_idempotent(p, mask_tail, value_tail)
71 Equal.cong(Word(p), Word(1n+p), tail => WCon{True{}, tail},
72 AES.hex_word_and(p, mask_tail,
73 AES.hex_word_and(p, mask_tail, value_tail)),
74 AES.hex_word_and(p, mask_tail, value_tail), recursive)
75
76def aes_hex_mask_idempotent(+value: U32, mask: U32) ->
77 {AES.hex_mask(AES.hex_mask(value, mask), mask) ==
78 AES.hex_mask(value, mask) : U32}:
79 match value mask:
80 case U32{value_word} U32{mask_word}:
81 Equal.cong(Word(32n), U32,
82 word => U32{word},
83 AES.hex_word_and(32n, mask_word,
84 AES.hex_word_and(32n, mask_word, value_word)),
85 AES.hex_word_and(32n, mask_word, value_word),
86 aes_hex_word_and_idempotent(32n, mask_word, value_word))
87
88def aes_hex_digit_inverse(+value: U32) ->
89 {AES.hex_nibble(Char.to_u32(AES.hex_digit(value))) ==
90 Some{AES.hex_mask(value, 15)} : Maybe<&2, U32>}:
91 match value:
92 case U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
93 case U32{WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
94 case U32{WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
95 case U32{WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
96 case U32{WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
97 case U32{WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
98 case U32{WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
99 case U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
100 case U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
101 case U32{WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
102 case U32{WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
103 case U32{WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
104 case U32{WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
105 case U32{WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
106 case U32{WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
107 case U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
108
109def aes_hex_digit_no_dot(+value: U32) ->
110 {Char.is_eq(AES.hex_digit(value), Chr{46}) == False{} : Bool}:
111 match value:
112 case U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
113 case U32{WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
114 case U32{WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
115 case U32{WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
116 case U32{WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
117 case U32{WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
118 case U32{WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
119 case U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
120 case U32{WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
121 case U32{WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
122 case U32{WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
123 case U32{WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
124 case U32{WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
125 case U32{WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
126 case U32{WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
127 case U32{WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
128
129def aes_split_hex_digit_no_dot(value: U32, +parts: List<&2, String>) ->
130 {String.split.fin(AES.hex_digit(value), parts,
131 Char.is_eq(AES.hex_digit(value), Chr{46})) ==
132 String.split.push(AES.hex_digit(value), parts) : List<&2, String>}:
133 Equal.cong(Bool, List<&2, String>,
134 cut => String.split.fin(AES.hex_digit(value), parts, cut),
135 Char.is_eq(AES.hex_digit(value), Chr{46}), False{},
136 aes_hex_digit_no_dot(value))
137
138def aes_hex_join_shift_mask(+value: U32) ->
139 {AES.hex_join(U32.shrn(value, 4n), AES.hex_mask(value, 15)) ==
140 AES.hex_mask(value, 255) : U32}:
141 match value:
142 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
143
144def aes_hex_join_masked_shift_mask(+value: U32) ->
145 {AES.hex_join(AES.hex_mask(U32.shrn(value, 4n), 15), AES.hex_mask(value, 15)) ==
146 AES.hex_mask(value, 255) : U32}:
147 match value:
148 case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: {==}
149
150def aes_hex_byte_prefix_idempotent(+byte: U32, +tail: String) ->
151 {SCon{AES.hex_digit(U32.shrn(AES.hex_mask(AES.hex_mask(byte, 255), 255), 4n)),
152 SCon{AES.hex_digit(AES.hex_mask(AES.hex_mask(byte, 255), 255)), tail}} ==
153 SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
154 SCon{AES.hex_digit(AES.hex_mask(byte, 255)), tail}} : String}:
155 +normalized = AES.hex_mask(byte, 255)
156 +twice = AES.hex_mask(normalized, 255)
157 +mask_equal = aes_hex_mask_idempotent(byte, 255)
158 low_equal = Equal.cong(U32, Char, value => AES.hex_digit(value),
159 twice, normalized,
160 mask_equal)
161 high_equal = Equal.cong(U32, Char,
162 value => AES.hex_digit(U32.shrn(value, 4n)), twice, normalized,
163 mask_equal)
164 inner_equal = Equal.cong(Char, String,
165 value => SCon{value, tail}, AES.hex_digit(twice),
166 AES.hex_digit(normalized), low_equal)
167 inner_path = Equal.cong(String, String,
168 rest => SCon{AES.hex_digit(U32.shrn(twice, 4n)), rest},
169 SCon{AES.hex_digit(twice), tail},
170 SCon{AES.hex_digit(normalized), tail}, inner_equal)
171 high_path = Equal.cong(Char, String,
172 value => SCon{value, SCon{AES.hex_digit(normalized), tail}},
173 AES.hex_digit(U32.shrn(twice, 4n)),
174 AES.hex_digit(U32.shrn(normalized, 4n)), high_equal)
175 Equal.trans(String,
176 SCon{AES.hex_digit(U32.shrn(twice, 4n)),
177 SCon{AES.hex_digit(twice), tail}},
178 SCon{AES.hex_digit(U32.shrn(twice, 4n)),
179 SCon{AES.hex_digit(normalized), tail}},
180 SCon{AES.hex_digit(U32.shrn(normalized, 4n)),
181 SCon{AES.hex_digit(normalized), tail}},
182 inner_path, high_path)
183
184def aes_hex_mask_bytes(+bytes: List<&2, U32>) -> List<&2, U32>:
185 match bytes:
186 case Nil{}: Nil{}
187 case byte <> tail: AES.hex_mask(byte, 255) <> aes_hex_mask_bytes(tail)
188
189def aes_hex_bytes_mask_idempotent(+bytes: List<&2, U32>) ->
190 {AES.hex_bytes(aes_hex_mask_bytes(bytes)) == AES.hex_bytes(bytes) : String}:
191 match bytes:
192 case Nil{}: {==}
193 case byte <> tail:
194 +left_tail = AES.hex_bytes(aes_hex_mask_bytes(tail))
195 +right_tail = AES.hex_bytes(tail)
196 tail_equal = aes_hex_bytes_mask_idempotent(tail)
197 prefix_equal = aes_hex_byte_prefix_idempotent(byte, left_tail)
198 tail_congruent = Equal.cong(String, String,
199 rest => SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
200 SCon{AES.hex_digit(AES.hex_mask(byte, 255)), rest}},
201 left_tail, right_tail, tail_equal)
202 Equal.trans(String,
203 SCon{AES.hex_digit(U32.shrn(
204 AES.hex_mask(AES.hex_mask(byte, 255), 255), 4n)),
205 SCon{AES.hex_digit(AES.hex_mask(
206 AES.hex_mask(byte, 255), 255)), left_tail}},
207 SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
208 SCon{AES.hex_digit(AES.hex_mask(byte, 255)), left_tail}},
209 SCon{AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
210 SCon{AES.hex_digit(AES.hex_mask(byte, 255)), right_tail}},
211 prefix_equal, tail_congruent)
212
213
214def aes_hex_pair_roundtrip(+byte: U32) ->
215 {AES.hex_pair(
216 AES.hex_digit(U32.shrn(AES.hex_mask(byte, 255), 4n)),
217 AES.hex_digit(AES.hex_mask(byte, 255))) ==
218 Some{AES.hex_mask(byte, 255)} : Maybe<&2, U32>}:
219 +normalized = AES.hex_mask(byte, 255)
220 +high = U32.shrn(normalized, 4n)
221 +low = normalized
222 high_decoded = AES.hex_nibble(Char.to_u32(AES.hex_digit(high)))
223 low_decoded = AES.hex_nibble(Char.to_u32(AES.hex_digit(low)))
224 high_inverse = aes_hex_digit_inverse(high)
225 low_inverse = aes_hex_digit_inverse(low)
226 low_changed = Equal.cong(Maybe<&2, U32>, Maybe<&2, U32>,
227 nibble => AES.hex_pair.combine(high_decoded, nibble),
228 low_decoded, Some{AES.hex_mask(low, 15)}, low_inverse)
229 high_changed = Equal.cong(Maybe<&2, U32>, Maybe<&2, U32>,
230 nibble => AES.hex_pair.combine(nibble, Some{AES.hex_mask(low, 15)}),
231 high_decoded, Some{AES.hex_mask(high, 15)}, high_inverse)
232 pair_changed = Equal.trans(Maybe<&2, U32>,
233 AES.hex_pair.combine(high_decoded, low_decoded),
234 AES.hex_pair.combine(high_decoded, Some{AES.hex_mask(low, 15)}),
235 AES.hex_pair.combine(Some{AES.hex_mask(high, 15)}, Some{AES.hex_mask(low, 15)}),
236 low_changed, high_changed)
237 join_equal = aes_hex_join_masked_shift_mask(normalized)
238 normalized_equal = aes_hex_mask_idempotent(byte, 255)
239 joined_to_byte = Equal.trans(U32,
240 AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15)),
241 AES.hex_mask(normalized, 255), normalized,
242 join_equal, normalized_equal)
243 joined_some = Equal.cong(U32, Maybe<&2, U32>, value => Some{value},
244 AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15)),
245 normalized, joined_to_byte)
246 Equal.trans(Maybe<&2, U32>, AES.hex_pair(
247 AES.hex_digit(U32.shrn(normalized, 4n)), AES.hex_digit(normalized)),
248 AES.hex_pair.combine(high_decoded, low_decoded), Some{normalized},
249 {==},
250 Equal.trans(Maybe<&2, U32>,
251 AES.hex_pair.combine(high_decoded, low_decoded),
252 AES.hex_pair.combine(Some{AES.hex_mask(high, 15)},
253 Some{AES.hex_mask(low, 15)}),
254 Some{normalized}, pair_changed,
255 Equal.trans(Maybe<&2, U32>,
256 AES.hex_pair.combine(Some{AES.hex_mask(high, 15)},
257 Some{AES.hex_mask(low, 15)}),
258 Some{AES.hex_join(AES.hex_mask(high, 15), AES.hex_mask(low, 15))},
259 Some{normalized}, {==}, joined_some)))
260
261def aes_decode_hex_bytes(+bytes: List<&2, U32>) ->
262 {AES.decode_hex(AES.hex_bytes(bytes)) == Some{aes_hex_mask_bytes(bytes)} : Maybe<&2, List<&2, U32>>}:
263 match bytes:
264 case Nil{}: {==}
265 case byte <> tail:
266 +normalized = AES.hex_mask(byte, 255)
267 +rest_pairs = AES.hex_pairs(String.to_list(AES.hex_bytes(tail)))
268 +rest_decoded = AES.collect_hex(rest_pairs)
269 tail_proof = aes_decode_hex_bytes(tail)
270 pair_proof = aes_hex_pair_roundtrip(byte)
271 pair_changed = Equal.cong(Maybe<&2, U32>,
272 Maybe<&2, List<&2, U32>>,
273 pair => AES.collect_hex.cons(pair, rest_decoded),
274 AES.hex_pair(
275 AES.hex_digit(U32.shrn(normalized, 4n)),
276 AES.hex_digit(normalized)),
277 Some{normalized}, pair_proof)
278 tail_changed = Equal.cong(Maybe<&2, List<&2, U32>>,
279 Maybe<&2, List<&2, U32>>,
280 result => AES.collect_hex.cons(Some{normalized}, result),
281 rest_decoded, Some{aes_hex_mask_bytes(tail)}, tail_proof)
282 Equal.trans(Maybe<&2, List<&2, U32>>,
283 AES.collect_hex.cons(
284 AES.hex_pair(
285 AES.hex_digit(U32.shrn(normalized, 4n)),
286 AES.hex_digit(normalized)), rest_decoded),
287 AES.collect_hex.cons(Some{normalized}, rest_decoded),
288 Some{normalized <> aes_hex_mask_bytes(tail)},
289 pair_changed,
290 Equal.trans(Maybe<&2, List<&2, U32>>,
291 AES.collect_hex.cons(Some{normalized}, rest_decoded),
292 Some{normalized <> aes_hex_mask_bytes(tail)},
293 Some{normalized <> aes_hex_mask_bytes(tail)},
294 tail_changed, {==}))
295def aes_split_push_single(value: U32, +suffix: String) ->
296 {String.split.push(AES.hex_digit(value), [suffix]) ==
297 [SCon{AES.hex_digit(value), suffix}] : List<&2, String>}:
298 {==}
299
300def aes_hex_bytes_split_single(+bytes: List<&2, U32>) ->
301 {String.split(AES.hex_bytes(bytes), Chr{46}) == [AES.hex_bytes(bytes)] : List<&2, String>}:
302 match bytes:
303 case Nil{}: {==}
304 case byte <> tail:
305 +normalized = AES.hex_mask(byte, 255)
306 +encoded_tail = AES.hex_bytes(tail)
307 +high = U32.shrn(normalized, 4n)
308 +low = normalized
309 tail_proof = aes_hex_bytes_split_single(tail)
310 low_shift = Equal.cong(List<&2, String>, List<&2, String>,
311 parts => String.split.fin(AES.hex_digit(low), parts,
312 Char.is_eq(AES.hex_digit(low), Chr{46})),
313 String.split(encoded_tail, Chr{46}), [encoded_tail], tail_proof)
314 low_join = Equal.trans(List<&2, String>,
315 String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
316 Char.is_eq(AES.hex_digit(low), Chr{46})),
317 String.split.push(AES.hex_digit(low), [encoded_tail]),
318 [SCon{AES.hex_digit(low), encoded_tail}],
319 Equal.trans(List<&2, String>,
320 String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
321 Char.is_eq(AES.hex_digit(low), Chr{46})),
322 String.split.fin(AES.hex_digit(low), [encoded_tail],
323 Char.is_eq(AES.hex_digit(low), Chr{46})),
324 String.split.push(AES.hex_digit(low), [encoded_tail]),
325 low_shift, aes_split_hex_digit_no_dot(low, [encoded_tail])),
326 aes_split_push_single(low, encoded_tail))
327 inner_split = Equal.trans(List<&2, String>,
328 String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
329 String.split.fin(AES.hex_digit(low), String.split(encoded_tail, Chr{46}),
330 Char.is_eq(AES.hex_digit(low), Chr{46})),
331 [SCon{AES.hex_digit(low), encoded_tail}],
332 {==}, low_join)
333 high_shift = Equal.cong(List<&2, String>, List<&2, String>,
334 parts => String.split.fin(AES.hex_digit(high), parts,
335 Char.is_eq(AES.hex_digit(high), Chr{46})),
336 String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
337 [SCon{AES.hex_digit(low), encoded_tail}], inner_split)
338 high_join = Equal.trans(List<&2, String>,
339 String.split.fin(AES.hex_digit(high),
340 String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
341 Char.is_eq(AES.hex_digit(high), Chr{46})),
342 String.split.push(AES.hex_digit(high),
343 [SCon{AES.hex_digit(low), encoded_tail}]),
344 [SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}}],
345 Equal.trans(List<&2, String>,
346 String.split.fin(AES.hex_digit(high),
347 String.split(SCon{AES.hex_digit(low), encoded_tail}, Chr{46}),
348 Char.is_eq(AES.hex_digit(high), Chr{46})),
349 String.split.fin(AES.hex_digit(high),
350 [SCon{AES.hex_digit(low), encoded_tail}],
351 Char.is_eq(AES.hex_digit(high), Chr{46})),
352 String.split.push(AES.hex_digit(high),
353 [SCon{AES.hex_digit(low), encoded_tail}]),
354 high_shift, aes_split_hex_digit_no_dot(high,
355 [SCon{AES.hex_digit(low), encoded_tail}])),
356 aes_split_push_single(high,
357 SCon{AES.hex_digit(low), encoded_tail}))
358 Equal.trans(List<&2, String>,
359 String.split(AES.hex_bytes(byte <> tail), Chr{46}),
360 String.split(SCon{AES.hex_digit(high),
361 SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
362 [AES.hex_bytes(byte <> tail)],
363 {==},
364 Equal.trans(List<&2, String>,
365 String.split(SCon{AES.hex_digit(high),
366 SCon{AES.hex_digit(low), encoded_tail}}, Chr{46}),
367 [SCon{AES.hex_digit(high),
368 SCon{AES.hex_digit(low), encoded_tail}}],
369 [AES.hex_bytes(byte <> tail)], high_join,
370 {==}))
371
372def aes_split_push_cons(value: U32, +head: String, +tail: List<&2, String>) ->
373 {String.split.push(AES.hex_digit(value), head <> tail) ==
374 SCon{AES.hex_digit(value), head} <> tail : List<&2, String>}:
375 {==}
376
377def aes_hex_bytes_split_before_period(+bytes: List<&2, U32>, +suffix: String) ->
378 {String.split(AES.hex_bytes(bytes) ++ "." ++ suffix, Chr{46}) ==
379 AES.hex_bytes(bytes) <> String.split(suffix, Chr{46}) : List<&2, String>}:
380 match bytes:
381 case Nil{}: {==}
382 case byte <> tail:
383 +normalized = AES.hex_mask(byte, 255)
384 +encoded_tail = AES.hex_bytes(tail)
385 +suffix_fields = String.split(suffix, Chr{46})
386 +tail_text = encoded_tail ++ "." ++ suffix
387 +high = U32.shrn(normalized, 4n)
388 +low = normalized
389 tail_proof = aes_hex_bytes_split_before_period(tail, suffix)
390 low_shift = Equal.cong(List<&2, String>, List<&2, String>,
391 parts => String.split.fin(AES.hex_digit(low), parts,
392 Char.is_eq(AES.hex_digit(low), Chr{46})),
393 String.split(tail_text, Chr{46}), encoded_tail <> suffix_fields,
394 tail_proof)
395 low_join = Equal.trans(List<&2, String>,
396 String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
397 Char.is_eq(AES.hex_digit(low), Chr{46})),
398 String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
399 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
400 Equal.trans(List<&2, String>,
401 String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
402 Char.is_eq(AES.hex_digit(low), Chr{46})),
403 String.split.fin(AES.hex_digit(low), encoded_tail <> suffix_fields,
404 Char.is_eq(AES.hex_digit(low), Chr{46})),
405 String.split.push(AES.hex_digit(low), encoded_tail <> suffix_fields),
406 low_shift, aes_split_hex_digit_no_dot(low,
407 encoded_tail <> suffix_fields)),
408 aes_split_push_cons(low, encoded_tail, suffix_fields))
409 inner_split = Equal.trans(List<&2, String>,
410 String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
411 String.split.fin(AES.hex_digit(low), String.split(tail_text, Chr{46}),
412 Char.is_eq(AES.hex_digit(low), Chr{46})),
413 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
414 {==}, low_join)
415 high_shift = Equal.cong(List<&2, String>, List<&2, String>,
416 parts => String.split.fin(AES.hex_digit(high), parts,
417 Char.is_eq(AES.hex_digit(high), Chr{46})),
418 String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
419 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
420 inner_split)
421 high_join = Equal.trans(List<&2, String>,
422 String.split.fin(AES.hex_digit(high),
423 String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
424 Char.is_eq(AES.hex_digit(high), Chr{46})),
425 String.split.push(AES.hex_digit(high),
426 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
427 SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
428 Equal.trans(List<&2, String>,
429 String.split.fin(AES.hex_digit(high),
430 String.split(SCon{AES.hex_digit(low), tail_text}, Chr{46}),
431 Char.is_eq(AES.hex_digit(high), Chr{46})),
432 String.split.fin(AES.hex_digit(high),
433 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields,
434 Char.is_eq(AES.hex_digit(high), Chr{46})),
435 String.split.push(AES.hex_digit(high),
436 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields),
437 high_shift, aes_split_hex_digit_no_dot(high,
438 SCon{AES.hex_digit(low), encoded_tail} <> suffix_fields)),
439 aes_split_push_cons(high,
440 SCon{AES.hex_digit(low), encoded_tail}, suffix_fields))
441 Equal.trans(List<&2, String>,
442 String.split(AES.hex_bytes(byte <> tail) ++ "." ++ suffix, Chr{46}),
443 String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
444 AES.hex_bytes(byte <> tail) <> suffix_fields,
445 {==}, Equal.trans(List<&2, String>,
446 String.split(SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), tail_text}}, Chr{46}),
447 SCon{AES.hex_digit(high), SCon{AES.hex_digit(low), encoded_tail}} <> suffix_fields,
448 AES.hex_bytes(byte <> tail) <> suffix_fields,
449 high_join, {==}))
450
451def aes_split_leading_dot(+suffix: String) ->
452 {String.split("." ++ suffix, Chr{46}) ==
453 "" <> String.split(suffix, Chr{46}) : List<&2, String>}:
454 {==}
455
456def aes_split_v1_prefix(+suffix: String) ->
457 {String.split("v1." ++ suffix, Chr{46}) ==
458 "v1" <> String.split(suffix, Chr{46}) : List<&2, String>}:
459 {==}
460
461def aes_string_append_assoc(+a: String, +b: String, +c: String) ->
462 {a ++ b ++ c == a ++ (b ++ c) : String}:
463 match a:
464 case SNil{}: {==}
465 case SCon{head, tail}:
466 Equal.cong(String, String, rest => SCon{head, rest},
467 tail ++ b ++ c, tail ++ (b ++ c),
468 aes_string_append_assoc(tail, b, c))
469
470def aes_split_v1_hex_fields(+nonce: List<&2, U32>, +tag: List<&2, U32>,
471 +ciphertext: List<&2, U32>) ->
472 {String.split("v1." ++ AES.hex_bytes(nonce) ++ "." ++
473 AES.hex_bytes(tag) ++ "." ++ AES.hex_bytes(ciphertext), Chr{46}) ==
474 ["v1", AES.hex_bytes(nonce), AES.hex_bytes(tag), AES.hex_bytes(ciphertext)] : List<&2, String>}:
475 +nonce_hex = AES.hex_bytes(nonce)
476 +tag_hex = AES.hex_bytes(tag)
477 +cipher_hex = AES.hex_bytes(ciphertext)
478 +tag_suffix = tag_hex ++ "." ++ cipher_hex
479 +nonce_suffix = nonce_hex ++ "." ++ tag_suffix
480 cipher_split = aes_hex_bytes_split_single(ciphertext)
481 tag_split = aes_hex_bytes_split_before_period(tag, cipher_hex)
482 nonce_split = aes_hex_bytes_split_before_period(nonce, tag_suffix)
483 tag_final = Equal.cong(List<&2, String>, List<&2, String>,
484 fields => tag_hex <> fields,
485 String.split(cipher_hex, Chr{46}), [cipher_hex], cipher_split)
486 tag_complete = Equal.trans(List<&2, String>,
487 String.split(tag_suffix, Chr{46}),
488 tag_hex <> String.split(cipher_hex, Chr{46}),
489 tag_hex <> [cipher_hex], tag_split, tag_final)
490 nonce_final = Equal.cong(List<&2, String>, List<&2, String>,
491 fields => nonce_hex <> fields,
492 String.split(tag_suffix, Chr{46}), tag_hex <> [cipher_hex], tag_complete)
493 rest_fields = Equal.cong(List<&2, String>, List<&2, String>,
494 fields => "v1" <> fields,
495 String.split(nonce_suffix, Chr{46}), nonce_hex <> (tag_hex <> [cipher_hex]),
496 Equal.trans(List<&2, String>,
497 String.split(nonce_suffix, Chr{46}),
498 nonce_hex <> String.split(tag_suffix, Chr{46}),
499 nonce_hex <> (tag_hex <> [cipher_hex]),
500 nonce_split, nonce_final))
501 Equal.trans(List<&2, String>,
502 String.split("v1." ++ nonce_suffix, Chr{46}),
503 "v1" <> String.split(nonce_suffix, Chr{46}),
504 ["v1", nonce_hex, tag_hex, cipher_hex],
505 aes_split_v1_prefix(nonce_suffix),
506 Equal.trans(List<&2, String>,
507 "v1" <> String.split(nonce_suffix, Chr{46}),
508 "v1" <> (nonce_hex <> (tag_hex <> [cipher_hex])),
509 ["v1", nonce_hex, tag_hex, cipher_hex],
510 rest_fields, {==}))
511
512def aes_encode_fields_split(+envelope: AES.Envelope) ->
513 {String.split(AES.encode_impl(envelope), Chr{46}) ==
514 ["v1", AES.hex_bytes(AES.fixed_bytes(12n,
515 AES.nonce_bytes(AES.envelope_nonce(envelope)))),
516 AES.hex_bytes(AES.fixed_bytes(16n,
517 AES.tag_bytes(AES.envelope_tag(envelope)))),
518 AES.hex_bytes(AES.ciphertext(envelope))] : List<&2, String>}:
519 match envelope:
520 case AES.Envelope{nonce, ciphertext, tag, valid}:
521 match nonce:
522 case AES.Nonce{nonce_bytes, size, valid}:
523 aes_split_v1_hex_fields(
524 AES.fixed_bytes(12n, nonce_bytes),
525 AES.fixed_bytes(16n, AES.tag_bytes(tag)), ciphertext)
526
527
528def aes_false_type(b: Bool) -> Data:
529 match b:
530 case False{}: Unit
531 case True{}: Empty
532
533def aes_false_true(e: {False{} == True{} : Bool}) -> Empty:
534 %e : aes_false_type(_)
535 Unit{}
536
537def aes_nat_predecessor(n: Nat) -> Nat:
538 match n:
539 case 0n: 0n
540 case 1n+p: p
541
542def aes_fixed_bytes_length(+n: Nat, +bytes: List<&2, U32>) ->
543 {List.length(&2, U32, AES.fixed_bytes(n, bytes)) == n : Nat}:
544 match n bytes:
545 case 0n _: {==}
546 case 1n+p Nil{}:
547 Equal.cong(Nat, Nat, x => 1n+x,
548 List.length(&2, U32, AES.fixed_bytes(p, Nil{})), p,
549 aes_fixed_bytes_length(p, Nil{}))
550 case 1n+p byte <> tail:
551 Equal.cong(Nat, Nat, x => 1n+x,
552 List.length(&2, U32, AES.fixed_bytes(p, tail)), p,
553 aes_fixed_bytes_length(p, tail))
554
555def aes_fixed_bytes_identity(+n: Nat, +bytes: List<&2, U32>,
556 size: {List.length(&2, U32, bytes) == n : Nat}) ->
557 {AES.fixed_bytes(n, bytes) == bytes : List<&2, U32>}:
558 match n bytes:
559 case 0n Nil{}: {==}
560 case 0n byte <> tail:
561 contradiction = Equal.cong(Nat, Bool,
562 x => Nat.is_eq(x, 0n),
563 1n+List.length(&2, U32, tail), 0n, size)
564 Empty.absurd({AES.fixed_bytes(0n, byte <> tail) ==
565 byte <> tail : List<&2, U32>},
566 aes_false_true(contradiction))
567 case 1n+p Nil{}:
568 contradiction = Equal.cong(Nat, Bool,
569 x => Nat.is_eq(x, 0n), 0n, 1n+p, size)
570 Empty.absurd({AES.fixed_bytes(1n+p, Nil{}) == Nil{} :
571 List<&2, U32>},
572 aes_false_true(Equal.sym(Bool, True{}, False{},
573 contradiction)))
574 case 1n+p byte <> tail:
575 tail_size = Equal.cong(Nat, Nat, aes_nat_predecessor,
576 1n+List.length(&2, U32, tail), 1n+p, size)
577 Equal.cong(List<&2, U32>, List<&2, U32>,
578 xs => byte <> xs,
579 AES.fixed_bytes(p, tail), tail,
580 aes_fixed_bytes_identity(p, tail, tail_size))
581
582def aes_parse_decoded_masked_map(+nonce: List<&2, U32>, +tag: List<&2, U32>,
583 +ciphertext: List<&2, U32>,
584 nonce_size: {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat},
585 tag_size: {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat},
586 nonce_valid: {AES.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool},
587 tag_valid: {AES.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool},
588 ciphertext_valid: {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}) ->
589 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
590 AES.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag),
591 aes_hex_mask_bytes(ciphertext),
592 Some{nonce_size}, Some{tag_size}, Some{nonce_valid},
593 Some{tag_valid}, Some{ciphertext_valid})) ==
594 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++ "." ++
595 AES.hex_bytes(ciphertext)} : Result<&2, &2, AES.Error, String>}:
596 +masked_nonce = aes_hex_mask_bytes(nonce)
597 +masked_tag = aes_hex_mask_bytes(tag)
598 +masked_ciphertext = aes_hex_mask_bytes(ciphertext)
599 encoded_fixed = "v1." ++
600 AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
601 AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)) ++ "." ++
602 AES.hex_bytes(masked_ciphertext)
603 encoded_masked = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
604 AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(masked_ciphertext)
605 encoded_raw = "v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
606 "." ++ AES.hex_bytes(ciphertext)
607 cipher_equal = aes_hex_bytes_mask_idempotent(ciphertext)
608 tag_equal = aes_hex_bytes_mask_idempotent(tag)
609 nonce_equal = aes_hex_bytes_mask_idempotent(nonce)
610 cipher_path = Equal.cong(String, String,
611 last => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
612 AES.hex_bytes(masked_tag) ++ "." ++ last),
613 AES.hex_bytes(masked_ciphertext), AES.hex_bytes(ciphertext), cipher_equal)
614 tag_path = Equal.cong(String, String,
615 value => ("v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++ value ++
616 "." ++ AES.hex_bytes(ciphertext)),
617 AES.hex_bytes(masked_tag), AES.hex_bytes(tag), tag_equal)
618 nonce_path = Equal.cong(String, String,
619 value => ("v1." ++ value ++ "." ++ AES.hex_bytes(tag) ++ "." ++
620 AES.hex_bytes(ciphertext)),
621 AES.hex_bytes(masked_nonce), AES.hex_bytes(nonce), nonce_equal)
622 cipher_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
623 AES.hex_bytes(masked_tag) ++ "." ++ AES.hex_bytes(ciphertext)
624 tag_intermediate = "v1." ++ AES.hex_bytes(masked_nonce) ++ "." ++
625 AES.hex_bytes(tag) ++ "." ++ AES.hex_bytes(ciphertext)
626 cipher_tag_path = Equal.trans(String, encoded_masked,
627 cipher_intermediate, tag_intermediate, cipher_path, tag_path)
628 encode_fields_equal = Equal.trans(String, encoded_masked,
629 tag_intermediate, encoded_raw, cipher_tag_path, nonce_path)
630 fixed_nonce_equal = Equal.cong(List<&2, U32>, String,
631 xs => AES.hex_bytes(xs),
632 AES.fixed_bytes(12n, masked_nonce), masked_nonce,
633 aes_fixed_bytes_identity(12n, masked_nonce, nonce_size))
634 fixed_tag_equal = Equal.cong(List<&2, U32>, String,
635 xs => AES.hex_bytes(xs),
636 AES.fixed_bytes(16n, masked_tag), masked_tag,
637 aes_fixed_bytes_identity(16n, masked_tag, tag_size))
638 fixed_tag_intermediate = "v1." ++
639 AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
640 AES.hex_bytes(masked_tag) ++ "." ++
641 AES.hex_bytes(masked_ciphertext)
642 fixed_tag_path = Equal.cong(String, String,
643 value => "v1." ++
644 AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)) ++ "." ++
645 value ++ "." ++ AES.hex_bytes(masked_ciphertext),
646 AES.hex_bytes(AES.fixed_bytes(16n, masked_tag)),
647 AES.hex_bytes(masked_tag), fixed_tag_equal)
648 fixed_nonce_path = Equal.cong(String, String,
649 value => "v1." ++ value ++ "." ++ AES.hex_bytes(masked_tag) ++
650 "." ++ AES.hex_bytes(masked_ciphertext),
651 AES.hex_bytes(AES.fixed_bytes(12n, masked_nonce)),
652 AES.hex_bytes(masked_nonce), fixed_nonce_equal)
653 fixed_to_masked = Equal.trans(String, encoded_fixed,
654 fixed_tag_intermediate, encoded_masked,
655 fixed_tag_path, fixed_nonce_path)
656 fixed_to_raw = Equal.trans(String, encoded_fixed,
657 encoded_masked, encoded_raw,
658 fixed_to_masked, encode_fields_equal)
659 Equal.cong(String, Result<&2, &2, AES.Error, String>,
660 text => Done{text}, encoded_fixed, encoded_raw, fixed_to_raw)
661
662
663def aes_hex_mask_bytes_length(+bytes: List<&2, U32>) ->
664 {List.length(&2, U32, aes_hex_mask_bytes(bytes)) ==
665 List.length(&2, U32, bytes) : Nat}:
666 match bytes:
667 case Nil{}: {==}
668 case byte <> tail:
669 Equal.cong(Nat, Nat, n => 1n+n,
670 List.length(&2, U32, aes_hex_mask_bytes(tail)),
671 List.length(&2, U32, tail), aes_hex_mask_bytes_length(tail))
672
673def aes_hex_mask_bytes_valid(+bytes: List<&2, U32>) ->
674 {AES.bytes_valid(aes_hex_mask_bytes(bytes)) == True{} : Bool}:
675 match bytes:
676 case Nil{}: {==}
677 case byte <> tail:
678 recursive = aes_hex_mask_bytes_valid(tail)
679 range = aes_hex_mask_255_lt_256(byte)
680 head_changed = Equal.cong(Bool, Bool,
681 head => Bool.and(head, AES.bytes_valid(aes_hex_mask_bytes(tail))),
682 U32.is_lt(AES.hex_mask(byte, 255), 256), True{}, range)
683 tail_changed = Equal.cong(Bool, Bool,
684 valid => Bool.and(True{}, valid),
685 AES.bytes_valid(aes_hex_mask_bytes(tail)), True{}, recursive)
686 Equal.trans(Bool,
687 Bool.and(U32.is_lt(AES.hex_mask(byte, 255), 256),
688 AES.bytes_valid(aes_hex_mask_bytes(tail))),
689 Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
690 True{}, head_changed,
691 Equal.trans(Bool,
692 Bool.and(True{}, AES.bytes_valid(aes_hex_mask_bytes(tail))),
693 Bool.and(True{}, True{}), True{}, tail_changed, {==}))
694
695def aes_nat_eq_self(+n: Nat) ->
696 {AES.aes_nat_eq_proof(n, n) == Some{{==}} :
697 Maybe<&0, {n == n : Nat}>}:
698 match n:
699 case 0n: {==}
700 case 1n+p:
701 Equal.cong(Maybe<&0, {p == p : Nat}>,
702 Maybe<&0, {1n+p == 1n+p : Nat}>,
703 result => AES.aes_nat_eq_step(p, p, result),
704 AES.aes_nat_eq_proof(p, p), Some{{==}},
705 aes_nat_eq_self(p))
706
707def aes_bytes_valid_status(+bytes: List<&2, U32>, b: Bool,
708 link: {b == AES.bytes_valid(bytes) : Bool}) ->
709 {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
710 AES.aes_bytes_valid_from_bool(bytes, b, link)) == b : Bool}:
711 match b:
712 case False{}: {==}
713 case True{}: {==}
714
715def aes_masked_bytes_cert_is_some(+bytes: List<&2, U32>) ->
716 {Maybe.is_some(&0,
717 {AES.bytes_valid(aes_hex_mask_bytes(bytes)) == True{} : Bool},
718 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(bytes))) == True{} : Bool}:
719 +masked = aes_hex_mask_bytes(bytes)
720 Equal.trans(Bool,
721 Maybe.is_some(&0, {AES.bytes_valid(masked) == True{} : Bool},
722 AES.aes_bytes_valid_proof(masked)),
723 AES.bytes_valid(masked), True{},
724 aes_bytes_valid_status(masked, AES.bytes_valid(masked), {==}),
725 aes_hex_mask_bytes_valid(bytes))
726
727def aes_nat_eq_is_some(+a: Nat, +b: Nat,
728 evidence: {a == b : Nat}) ->
729 {Maybe.is_some(&0, {a == b : Nat},
730 AES.aes_nat_eq_proof(a, b)) == True{} : Bool}:
731 Equal.trans(Bool,
732 Maybe.is_some(&0, {a == b : Nat}, AES.aes_nat_eq_proof(a, b)),
733 Maybe.is_some(&0, {b == b : Nat}, AES.aes_nat_eq_proof(b, b)),
734 True{},
735 Equal.cong(Nat, Bool,
736 value => Maybe.is_some(&0, {value == b : Nat},
737 AES.aes_nat_eq_proof(value, b)),
738 a, b, evidence),
739 Equal.cong(Maybe<&0, {b == b : Nat}>, Bool,
740 result => Maybe.is_some(&0, {b == b : Nat}, result),
741 AES.aes_nat_eq_proof(b, b), Some{{==}},
742 aes_nat_eq_self(b)))
743
744def aes_masked_size_is_some(+bytes: List<&2, U32>, +expected: Nat,
745 size: {List.length(&2, U32, bytes) == expected : Nat}) ->
746 {Maybe.is_some(&0,
747 {List.length(&2, U32, aes_hex_mask_bytes(bytes)) == expected : Nat},
748 AES.aes_nat_eq_proof(
749 List.length(&2, U32, aes_hex_mask_bytes(bytes)), expected)) ==
750 True{} : Bool}:
751 aes_nat_eq_is_some(
752 List.length(&2, U32, aes_hex_mask_bytes(bytes)),
753 expected,
754 Equal.trans(Nat,
755 List.length(&2, U32, aes_hex_mask_bytes(bytes)),
756 List.length(&2, U32, bytes), expected,
757 aes_hex_mask_bytes_length(bytes), size))
758
759def aes_maybe_cert_value(A: Type, cert: Maybe<&0, A>,
760 present: {Maybe.is_some(&0, A, cert) == True{} : Bool}) -> A:
761 match cert:
762 case None{}: Empty.absurd(A, aes_false_true(present))
763 case Some{value}: value
764
765def aes_maybe_cert_reconstruct(A: Type, cert: Maybe<&0, A>,
766 present: {Maybe.is_some(&0, A, cert) == True{} : Bool}) ->
767 {cert == Some{aes_maybe_cert_value(A, cert, present)} : Maybe<&0, A>}:
768 match cert:
769 case None{}:
770 Empty.absurd({None{} ==
771 Some{aes_maybe_cert_value(A, None{}, present)} :
772 Maybe<&0, A>}, aes_false_true(present))
773 case Some{value}: {==}
774
775def aes_parse_decoded_map_goal(nonce: List<&2, U32>,
776 tag: List<&2, U32>, ciphertext: List<&2, U32>,
777 ns: Maybe<&0, {List.length(&2, U32,
778 aes_hex_mask_bytes(nonce)) == 12n : Nat}>,
779 ts: Maybe<&0, {List.length(&2, U32,
780 aes_hex_mask_bytes(tag)) == 16n : Nat}>,
781 nv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(nonce)) ==
782 True{} : Bool}>,
783 tv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(tag)) ==
784 True{} : Bool}>,
785 cv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) ==
786 True{} : Bool}>) -> Type:
787 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
788 AES.parse_decoded(aes_hex_mask_bytes(nonce),
789 aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext),
790 ns, ts, nv, tv, cv)) ==
791 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
792 "." ++ AES.hex_bytes(ciphertext)} :
793 Result<&2, &2, AES.Error, String>}
794
795def aes_parse_decoded_if_some(+nonce: List<&2, U32>,
796 +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
797 ns: Maybe<&0, {List.length(&2, U32,
798 aes_hex_mask_bytes(nonce)) == 12n : Nat}>,
799 ts: Maybe<&0, {List.length(&2, U32,
800 aes_hex_mask_bytes(tag)) == 16n : Nat}>,
801 nv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(nonce)) ==
802 True{} : Bool}>,
803 tv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(tag)) ==
804 True{} : Bool}>,
805 cv: Maybe<&0, {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) ==
806 True{} : Bool}>,
807 ns_present: {Maybe.is_some(&0,
808 {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat},
809 ns) == True{} : Bool},
810 ts_present: {Maybe.is_some(&0,
811 {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat},
812 ts) == True{} : Bool},
813 nv_present: {Maybe.is_some(&0,
814 {AES.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool},
815 nv) == True{} : Bool},
816 tv_present: {Maybe.is_some(&0,
817 {AES.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool},
818 tv) == True{} : Bool},
819 cv_present: {Maybe.is_some(&0,
820 {AES.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool},
821 cv) == True{} : Bool}) ->
822 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
823 AES.parse_decoded(aes_hex_mask_bytes(nonce),
824 aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext),
825 ns, ts, nv, tv, cv)) ==
826 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
827 "." ++ AES.hex_bytes(ciphertext)} :
828 Result<&2, &2, AES.Error, String>}:
829 match ns:
830 case None{}:
831 Empty.absurd(aes_parse_decoded_map_goal(nonce, tag,
832 ciphertext, None{}, ts, nv, tv, cv),
833 aes_false_true(ns_present))
834 case Some{ns_proof}:
835 match ts:
836 case None{}:
837 Empty.absurd(aes_parse_decoded_map_goal(nonce, tag,
838 ciphertext, Some{ns_proof}, None{}, nv, tv, cv),
839 aes_false_true(ts_present))
840 case Some{ts_proof}:
841 match nv:
842 case None{}:
843 Empty.absurd(aes_parse_decoded_map_goal(nonce,
844 tag, ciphertext, Some{ns_proof},
845 Some{ts_proof}, None{}, tv, cv),
846 aes_false_true(nv_present))
847 case Some{nv_proof}:
848 match tv:
849 case None{}:
850 Empty.absurd(aes_parse_decoded_map_goal(
851 nonce, tag, ciphertext,
852 Some{ns_proof}, Some{ts_proof},
853 Some{nv_proof}, None{}, cv),
854 aes_false_true(tv_present))
855 case Some{tv_proof}:
856 match cv:
857 case None{}:
858 Empty.absurd(
859 aes_parse_decoded_map_goal(
860 nonce, tag, ciphertext,
861 Some{ns_proof},
862 Some{ts_proof},
863 Some{nv_proof},
864 Some{tv_proof}, None{}),
865 aes_false_true(cv_present))
866 case Some{cv_proof}:
867 aes_parse_decoded_masked_map(
868 nonce, tag, ciphertext,
869 ns_proof, ts_proof,
870 nv_proof, tv_proof,
871 cv_proof)
872
873def aes_parse_decoded_checked_map(+nonce: List<&2, U32>,
874 +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
875 nonce_size: {List.length(&2, U32, nonce) == 12n : Nat},
876 tag_size: {List.length(&2, U32, tag) == 16n : Nat}) ->
877 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
878 AES.parse_decoded(aes_hex_mask_bytes(nonce),
879 aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext),
880 AES.aes_nat_eq_proof(
881 List.length(&2, U32, aes_hex_mask_bytes(nonce)), 12n),
882 AES.aes_nat_eq_proof(
883 List.length(&2, U32, aes_hex_mask_bytes(tag)), 16n),
884 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(nonce)),
885 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(tag)),
886 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(ciphertext)))) ==
887 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
888 "." ++ AES.hex_bytes(ciphertext)} :
889 Result<&2, &2, AES.Error, String>}:
890 aes_parse_decoded_if_some(nonce, tag, ciphertext,
891 AES.aes_nat_eq_proof(
892 List.length(&2, U32, aes_hex_mask_bytes(nonce)), 12n),
893 AES.aes_nat_eq_proof(
894 List.length(&2, U32, aes_hex_mask_bytes(tag)), 16n),
895 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(nonce)),
896 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(tag)),
897 AES.aes_bytes_valid_proof(aes_hex_mask_bytes(ciphertext)),
898 aes_masked_size_is_some(nonce, 12n, nonce_size),
899 aes_masked_size_is_some(tag, 16n, tag_size),
900 aes_masked_bytes_cert_is_some(nonce),
901 aes_masked_bytes_cert_is_some(tag),
902 aes_masked_bytes_cert_is_some(ciphertext))
903
904def aes_parse_decoded_hex_map(+nonce: List<&2, U32>,
905 +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
906 nonce_size: {List.length(&2, U32, nonce) == 12n : Nat},
907 tag_size: {List.length(&2, U32, tag) == 16n : Nat}) ->
908 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
909 AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
910 AES.decode_hex(AES.hex_bytes(tag)),
911 AES.decode_hex(AES.hex_bytes(ciphertext)))) ==
912 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
913 "." ++ AES.hex_bytes(ciphertext)} :
914 Result<&2, &2, AES.Error, String>}:
915 +n = aes_hex_mask_bytes(nonce)
916 +t = aes_hex_mask_bytes(tag)
917 +c = aes_hex_mask_bytes(ciphertext)
918 nonce_step = Equal.cong(Maybe<&2, List<&2, U32>>,
919 Result<&2, &2, AES.Error, String>,
920 value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
921 AES.encode, AES.parse_decoded_hex(value,
922 AES.decode_hex(AES.hex_bytes(tag)),
923 AES.decode_hex(AES.hex_bytes(ciphertext)))),
924 AES.decode_hex(AES.hex_bytes(nonce)), Some{n},
925 aes_decode_hex_bytes(nonce))
926 tag_step = Equal.cong(Maybe<&2, List<&2, U32>>,
927 Result<&2, &2, AES.Error, String>,
928 value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
929 AES.encode, AES.parse_decoded_hex(Some{n}, value,
930 AES.decode_hex(AES.hex_bytes(ciphertext)))),
931 AES.decode_hex(AES.hex_bytes(tag)), Some{t},
932 aes_decode_hex_bytes(tag))
933 cipher_step = Equal.cong(Maybe<&2, List<&2, U32>>,
934 Result<&2, &2, AES.Error, String>,
935 value => Result.map(&2, &2, AES.Error, AES.Envelope, String,
936 AES.encode, AES.parse_decoded_hex(Some{n}, Some{t}, value)),
937 AES.decode_hex(AES.hex_bytes(ciphertext)), Some{c},
938 aes_decode_hex_bytes(ciphertext))
939 first_two = Equal.trans(Result<&2, &2, AES.Error, String>,
940 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
941 AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
942 AES.decode_hex(AES.hex_bytes(tag)),
943 AES.decode_hex(AES.hex_bytes(ciphertext)))),
944 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
945 AES.parse_decoded_hex(Some{n},
946 AES.decode_hex(AES.hex_bytes(tag)),
947 AES.decode_hex(AES.hex_bytes(ciphertext)))),
948 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
949 AES.parse_decoded_hex(Some{n}, Some{t},
950 AES.decode_hex(AES.hex_bytes(ciphertext)))),
951 nonce_step, tag_step)
952 all_three = Equal.trans(Result<&2, &2, AES.Error, String>,
953 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
954 AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
955 AES.decode_hex(AES.hex_bytes(tag)),
956 AES.decode_hex(AES.hex_bytes(ciphertext)))),
957 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
958 AES.parse_decoded_hex(Some{n}, Some{t},
959 AES.decode_hex(AES.hex_bytes(ciphertext)))),
960 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
961 AES.parse_decoded_hex(Some{n}, Some{t}, Some{c})),
962 first_two, cipher_step)
963 Equal.trans(Result<&2, &2, AES.Error, String>,
964 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
965 AES.parse_decoded_hex(AES.decode_hex(AES.hex_bytes(nonce)),
966 AES.decode_hex(AES.hex_bytes(tag)),
967 AES.decode_hex(AES.hex_bytes(ciphertext)))),
968 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
969 AES.parse_decoded_hex(Some{n}, Some{t}, Some{c})),
970 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
971 "." ++ AES.hex_bytes(ciphertext)},
972 all_three,
973 aes_parse_decoded_checked_map(nonce, tag, ciphertext,
974 nonce_size, tag_size))
975
976def aes_parse_fields_hex_map(+nonce: List<&2, U32>,
977 +tag: List<&2, U32>, +ciphertext: List<&2, U32>,
978 nonce_size: {List.length(&2, U32, nonce) == 12n : Nat},
979 tag_size: {List.length(&2, U32, tag) == 16n : Nat}) ->
980 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
981 AES.parse_fields(["v1", AES.hex_bytes(nonce),
982 AES.hex_bytes(tag), AES.hex_bytes(ciphertext)])) ==
983 Done{"v1." ++ AES.hex_bytes(nonce) ++ "." ++ AES.hex_bytes(tag) ++
984 "." ++ AES.hex_bytes(ciphertext)} :
985 Result<&2, &2, AES.Error, String>}:
986 aes_parse_decoded_hex_map(nonce, tag, ciphertext,
987 nonce_size, tag_size)
988
989def aes_parse_encoder_fields_map(+envelope: AES.Envelope) ->
990 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
991 AES.parse_fields(["v1",
992 AES.hex_bytes(AES.fixed_bytes(12n,
993 AES.nonce_bytes(AES.envelope_nonce(envelope)))),
994 AES.hex_bytes(AES.fixed_bytes(16n,
995 AES.tag_bytes(AES.envelope_tag(envelope)))),
996 AES.hex_bytes(AES.ciphertext(envelope))])) ==
997 Done{AES.encode(envelope)} :
998 Result<&2, &2, AES.Error, String>}:
999 match envelope:
1000 case AES.Envelope{nonce, ciphertext, tag, valid}:
1001 match nonce:
1002 case AES.Nonce{nonce_bytes, nonce_size, nonce_valid}:
1003 aes_parse_fields_hex_map(
1004 AES.fixed_bytes(12n, nonce_bytes),
1005 AES.fixed_bytes(16n, AES.tag_bytes(tag)), ciphertext,
1006 aes_fixed_bytes_length(12n, nonce_bytes),
1007 aes_fixed_bytes_length(16n, AES.tag_bytes(tag)))
1008
1009def aes_parse_fields_encoded_map(+envelope: AES.Envelope) ->
1010 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
1011 AES.parse_fields(String.split(AES.encode(envelope), Chr{46}))) ==
1012 Done{AES.encode(envelope)} :
1013 Result<&2, &2, AES.Error, String>}:
1014 fields: List<&2, String> = "v1" <>
1015 AES.hex_bytes(AES.fixed_bytes(12n,
1016 AES.nonce_bytes(AES.envelope_nonce(envelope)))) <>
1017 AES.hex_bytes(AES.fixed_bytes(16n,
1018 AES.tag_bytes(AES.envelope_tag(envelope)))) <>
1019 AES.hex_bytes(AES.ciphertext(envelope)) <> Nil{}
1020 Equal.trans(Result<&2, &2, AES.Error, String>,
1021 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
1022 AES.parse_fields(String.split(AES.encode(envelope), Chr{46}))),
1023 Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
1024 AES.parse_fields(fields)),
1025 Done{AES.encode(envelope)},
1026 Equal.cong(List<&2, String>,
1027 Result<&2, &2, AES.Error, String>,
1028 parts => Result.map(&2, &2, AES.Error, AES.Envelope,
1029 String, AES.encode, AES.parse_fields(parts)),
1030 String.split(AES.encode(envelope), Chr{46}), fields,
1031 aes_encode_fields_split(envelope)),
1032 aes_parse_encoder_fields_map(envelope))
1033
1034def aes_envelope_roundtrip(+envelope: AES.Envelope) ->
1035 {Result.map(&2, &2, AES.Error, AES.Envelope, String, AES.encode,
1036 AES.parse(AES.encode(envelope))) == Done{AES.encode(envelope)} :
1037 Result<&2, &2, AES.Error, String>}:
1038 Canonical.canonical_map_from_encoded(AES.encode(envelope),
1039 AES.parse_fields(String.split(AES.encode(envelope), Chr{46})),
1040 aes_parse_fields_encoded_map(envelope))
1041
1042
1043