1 import Base 2 import ../libs/AES256GCM.bend as AES 3 import ./AES_CanonicalProof.bend as Canonical 4 5 def 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 10 def 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 15 def aes_bool_and_false(b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}: 16 match b: 17 case False{}: {==} 18 case True{}: {==} 19 20 def aes_bool_and_true(b: Bool) -> {Bool.and(b, True{}) == b : Bool}: 21 match b: 22 case False{}: {==} 23 case True{}: {==} 24 25 def 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 52 def 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 76 def 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 88 def 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 109 def 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 129 def 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 138 def 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 144 def 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 150 def 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 184 def 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 189 def 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 214 def 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 261 def 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, {==})) 295 def 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 300 def 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 372 def 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 377 def 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 451 def aes_split_leading_dot(+suffix: String) -> 452 {String.split("." ++ suffix, Chr{46}) == 453 "" <> String.split(suffix, Chr{46}) : List<&2, String>}: 454 {==} 455 456 def 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 461 def 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 470 def 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 512 def 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 528 def aes_false_type(b: Bool) -> Data: 529 match b: 530 case False{}: Unit 531 case True{}: Empty 532 533 def aes_false_true(e: {False{} == True{} : Bool}) -> Empty: 534 %e : aes_false_type(_) 535 Unit{} 536 537 def aes_nat_predecessor(n: Nat) -> Nat: 538 match n: 539 case 0n: 0n 540 case 1n+p: p 541 542 def 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 555 def 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 582 def 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 663 def 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 673 def 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 695 def 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 707 def 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 715 def 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 727 def 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 744 def 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 759 def 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 765 def 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 775 def 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 795 def 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 873 def 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 904 def 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 976 def 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 989 def 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 1009 def 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 1034 def 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