proof/AES_ZipLengthProof.bend
qasim-bend-kit@0.1.0.2 · 195 lines · 15 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
3
4def false_type(b: Bool) -> Data:
5 match b:
6 case False{}: Unit
7 case True{}: Empty
8
9def false_true(e: {False{} == True{} : Bool}) -> Empty:
10 %e : false_type(_)
11 Unit{}
12
13def predecessor(n: Nat) -> Nat:
14 match n:
15 case 0n: 0n
16 case 1n+p: p
17
18def 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
47def 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
54def 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
63def 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
70def 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
86def 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
111def 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
116def 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
128def 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
153def 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
172def 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
178def 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