1 import Base 2 import ../libs/AES256GCMCore.bend as Core 3 4 def false_type(b: Bool) -> Data: 5 match b: 6 case False{}: Unit 7 case True{}: Empty 8 9 def false_true(e: {False{} == True{} : Bool}) -> Empty: 10 %e : false_type(_) 11 Unit{} 12 13 def predecessor(n: Nat) -> Nat: 14 match n: 15 case 0n: 0n 16 case 1n+p: p 17 18 def zip_length_equal(+bytes: List<&2, U32>, +stream: List<&2, U32>, 19 same_length: {List.length(&2, U32, bytes) == 20 List.length(&2, U32, stream) : Nat}) -> 21 {List.length(&2, U32, Core.gcm_zip_xor(bytes, stream)) == 22 List.length(&2, U32, bytes) : Nat}: 23 match bytes stream: 24 case Nil{} _: 25 Equal.cong(List<&2, U32>, Nat, 26 xs => List.length(&2, U32, xs), 27 Core.gcm_zip_xor(Nil{}, stream), Nil{}, 28 Core.gcm_zip_xor_nil_left(stream)) 29 case byte <> tail Nil{}: 30 impossible = Equal.cong(Nat, Bool, 31 n => Nat.is_eq(n, 0n), 32 1n+List.length(&2, U32, tail), 0n, same_length) 33 Empty.absurd( 34 {List.length(&2, U32, 35 Core.gcm_zip_xor(byte <> tail, Nil{})) == 36 List.length(&2, U32, byte <> tail) : Nat}, 37 false_true(impossible)) 38 case byte <> tail stream_byte <> stream_tail: 39 tail_length = Equal.cong(Nat, Nat, predecessor, 40 1n+List.length(&2, U32, tail), 41 1n+List.length(&2, U32, stream_tail), same_length) 42 Equal.cong(Nat, Nat, n => 1n+n, 43 List.length(&2, U32, Core.gcm_zip_xor(tail, stream_tail)), 44 List.length(&2, U32, tail), 45 zip_length_equal(tail, stream_tail, tail_length)) 46 47 def encrypt_block_length(+words: List<&2, U32>, +counter: List<&2, U32>) -> 48 {List.length(&2, U32, Core.aes256_encrypt_expanded(words, counter)) == 49 16n : Nat}: 50 match words: 51 case Nil{}: {==} 52 case head <> tail: {==} 53 54 def nat_add_succ_right(+a: Nat, +b: Nat) -> 55 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}: 56 match a: 57 case 0n: {==} 58 case 1n+p: 59 Equal.cong(Nat, Nat, n => 1n+n, 60 Nat.add(p, 1n+b), 1n+Nat.add(p, b), 61 nat_add_succ_right(p, b)) 62 63 def nat_add_zero_right(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}: 64 match a: 65 case 0n: {==} 66 case 1n+p: 67 Equal.cong(Nat, Nat, n => 1n+n, 68 Nat.add(p, 0n), p, nat_add_zero_right(p)) 69 70 def nat_add_comm(+a: Nat, +b: Nat) -> 71 {Nat.add(a, b) == Nat.add(b, a) : Nat}: 72 match a: 73 case 0n: 74 Equal.sym(Nat, Nat.add(b, 0n), b, 75 nat_add_zero_right(b)) 76 case 1n+p: 77 Equal.trans(Nat, 78 Nat.add(1n+p, b), 1n+Nat.add(b, p), 79 Nat.add(b, 1n+p), 80 Equal.cong(Nat, Nat, n => 1n+n, 81 Nat.add(p, b), Nat.add(b, p), nat_add_comm(p, b)), 82 Equal.sym(Nat, 83 Nat.add(b, 1n+p), 1n+Nat.add(b, p), 84 nat_add_succ_right(b, p))) 85 86 def reverse_go_length(+xs: List<&2, U32>, +acc: List<&2, U32>) -> 87 {List.length(&2, U32, List.reverse.go(&2, U32, xs, acc)) == 88 (List.length(&2, U32, acc) + List.length(&2, U32, xs) : Nat) : Nat}: 89 match xs: 90 case Nil{}: 91 Equal.sym(Nat, Nat.add(List.length(&2, U32, acc), 0n), 92 List.length(&2, U32, acc), 93 nat_add_zero_right(List.length(&2, U32, acc))) 94 case x <> tail: 95 Equal.trans(Nat, 96 List.length(&2, U32, 97 List.reverse.go(&2, U32, x <> tail, acc)), 98 (List.length(&2, U32, x <> acc) + 99 List.length(&2, U32, tail) : Nat), 100 (List.length(&2, U32, acc) + 101 List.length(&2, U32, x <> tail) : Nat), 102 reverse_go_length(tail, x <> acc), 103 Equal.sym(Nat, 104 (List.length(&2, U32, acc) + 105 List.length(&2, U32, x <> tail) : Nat), 106 (List.length(&2, U32, x <> acc) + 107 List.length(&2, U32, tail) : Nat), 108 nat_add_succ_right(List.length(&2, U32, acc), 109 List.length(&2, U32, tail)))) 110 111 def reverse_length(+xs: List<&2, U32>) -> 112 {List.length(&2, U32, List.reverse(&2, U32, xs)) == 113 List.length(&2, U32, xs) : Nat}: 114 reverse_go_length(xs, Nil{}) 115 116 def append_length(+xs: List<&2, U32>, +ys: List<&2, U32>) -> 117 {List.length(&2, U32, List.append(&2, U32, xs, ys)) == 118 Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}: 119 match xs: 120 case Nil{}: {==} 121 case x <> tail: 122 Equal.cong(Nat, Nat, n => 1n+n, 123 List.length(&2, U32, List.append(&2, U32, tail, ys)), 124 Nat.add(List.length(&2, U32, tail), 125 List.length(&2, U32, ys)), 126 append_length(tail, ys)) 127 128 def stream_step_length(+words: List<&2, U32>, 129 +counter: List<&2, U32>, +acc: List<&2, U32>) -> 130 {List.length(&2, U32, List.append(&2, U32, 131 List.reverse(&2, U32, 132 Core.aes256_encrypt_expanded(words, counter)), acc)) == 133 Nat.add(16n, List.length(&2, U32, acc)) : Nat}: 134 +block = Core.aes256_encrypt_expanded(words, counter) 135 Equal.trans(Nat, 136 List.length(&2, U32, 137 List.append(&2, U32, List.reverse(&2, U32, block), acc)), 138 Nat.add(List.length(&2, U32, 139 List.reverse(&2, U32, block)), 140 List.length(&2, U32, acc)), 141 Nat.add(16n, List.length(&2, U32, acc)), 142 append_length(List.reverse(&2, U32, block), acc), 143 Equal.cong(Nat, Nat, 144 n => Nat.add(n, List.length(&2, U32, acc)), 145 List.length(&2, U32, List.reverse(&2, U32, block)), 146 16n, 147 Equal.trans(Nat, 148 List.length(&2, U32, List.reverse(&2, U32, block)), 149 List.length(&2, U32, block), 16n, 150 reverse_length(block), 151 encrypt_block_length(words, counter)))) 152 153 def ctr_stream_exact_go_length(+fuel: Nat, +words: List<&2, U32>, 154 +counter: List<&2, U32>, +block: List<&2, U32>) -> 155 {List.length(&2, U32, 156 Core.gcm_ctr_stream_exact.go(fuel, words, counter, block)) == 157 fuel : Nat}: 158 match fuel: 159 case 0n: {==} 160 case 1n+p: 161 +step = Core.gcm_ctr_step(words, counter, block) 162 Equal.cong(Nat, Nat, n => 1n+n, 163 List.length(&2, U32, 164 Core.gcm_ctr_stream_exact.go(p, words, 165 Core.gcm_ctr_step_counter(step), 166 Core.gcm_ctr_step_rest(step))), 167 p, 168 ctr_stream_exact_go_length(p, words, 169 Core.gcm_ctr_step_counter(step), 170 Core.gcm_ctr_step_rest(step))) 171 172 def ctr_stream_exact_length(+fuel: Nat, +words: List<&2, U32>, 173 +start: List<&2, U32>) -> 174 {List.length(&2, U32, 175 Core.gcm_ctr_stream_exact(fuel, words, start)) == fuel : Nat}: 176 ctr_stream_exact_go_length(fuel, words, start, Nil{}) 177 178 def ctr_encrypt_ciphertext_length(+words: List<&2, U32>, 179 +nonce: List<&2, U32>, +plaintext: List<&2, U32>) -> 180 {List.length(&2, U32, 181 Core.gcm_ciphertext_bytes( 182 Core.gcm_ctr_encrypt(words, nonce, plaintext))) == 183 List.length(&2, U32, plaintext) : Nat}: 184 +start = Core.gcm_inc32(Core.gcm_j0(nonce)) 185 +stream = Core.gcm_ctr_stream_exact( 186 List.length(&2, U32, plaintext), words, start) 187 zip_length_equal(plaintext, stream, 188 Equal.sym(Nat, 189 List.length(&2, U32, stream), 190 List.length(&2, U32, plaintext), 191 ctr_stream_exact_length(List.length(&2, U32, plaintext), 192 words, start))) 193 194 195