def zip_length_equal

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:18

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

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))