def zip_xor_involution

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:208

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as ZipLengthProof

208def zip_xor_involution(+bytes: List<&2, U32>,
209    +stream: List<&2, U32>,
210    same_length: {List.length(&2, U32, bytes) ==
211        List.length(&2, U32, stream) : Nat}) ->
212    {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, stream), stream) ==
213     Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
214    match bytes stream:
215        case Nil{} _:
216            +inner = Core.gcm_zip_xor_nil_left(stream)
217            Equal.trans(List<&2, U32>,
218                Core.gcm_zip_xor(Core.gcm_zip_xor(Nil{}, stream), stream),
219                Core.gcm_zip_xor(Nil{}, stream), Nil{},
220                Equal.cong(List<&2, U32>, List<&2, U32>,
221                    xs => Core.gcm_zip_xor(xs, stream),
222                    Core.gcm_zip_xor(Nil{}, stream), Nil{}, inner),
223                inner)
224        case _ <> _ Nil{}:
225            unequal = Equal.cong(Nat, Bool,
226                n => Nat.is_eq(n, 0n),
227                List.length(&2, U32, bytes),
228                List.length(&2, U32, Nil{}), same_length)
229            Empty.absurd(
230                {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, Nil{}), Nil{}) ==
231                 Core.gcm_mask_bytes(bytes) : List<&2, U32>},
232                ZipLengthProof.false_true(unequal))
233        case byte <> tail stream_byte <> stream_tail:
234            tail_length = Equal.cong(Nat, Nat, predecessor,
235                List.length(&2, U32, byte <> tail),
236                List.length(&2, U32, stream_byte <> stream_tail),
237                same_length)
238            recursive = zip_xor_involution(tail, stream_tail, tail_length)
239            Equal.trans(List<&2, U32>,
240                Core.gcm_zip_xor(
241                    Core.gcm_zip_xor(byte <> tail,
242                        stream_byte <> stream_tail),
243                    stream_byte <> stream_tail),
244                Core.gcm_hex_mask(U32.xor(
245                    Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
246                    stream_byte), 255) <>
247                    Core.gcm_zip_xor(
248                        Core.gcm_zip_xor(tail, stream_tail), stream_tail),
249                Core.gcm_mask_bytes(byte <> tail),
250                {==},
251                Equal.trans(List<&2, U32>,
252                    Core.gcm_hex_mask(U32.xor(
253                        Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
254                        stream_byte), 255) <>
255                        Core.gcm_zip_xor(
256                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
257                    Core.gcm_hex_mask(byte, 255) <>
258                        Core.gcm_zip_xor(
259                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
260                    Core.gcm_mask_bytes(byte <> tail),
261                    Equal.cong(U32, List<&2, U32>,
262                        head => head <>
263                            Core.gcm_zip_xor(
264                                Core.gcm_zip_xor(tail, stream_tail), stream_tail),
265                        Core.gcm_hex_mask(U32.xor(
266                            Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
267                            stream_byte), 255),
268                        Core.gcm_hex_mask(byte, 255),
269                        gcm_mask_xor_inv(byte, stream_byte)),
270                    Equal.cong(List<&2, U32>, List<&2, U32>,
271                        rest => Core.gcm_hex_mask(byte, 255) <> rest,
272                        Core.gcm_zip_xor(
273                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
274                        Core.gcm_mask_bytes(tail), recursive)))