AESZipLengthProof.zip_length_equal: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
Lines 18-45 of qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&start_line=18&end_line=45

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

def zip_length_equal(+bytes: List<&2, U32>, +stream: List<&2, U32>,
    same_length: {List.length(&2, U32, bytes) ==
        List.length(&2, U32, stream) : Nat}) ->
    {List.length(&2, U32, Core.gcm_zip_xor(bytes, stream)) ==
        List.length(&2, U32, bytes) : Nat}:
    match bytes stream:
        case Nil{} _:
            Equal.cong(List<&2, U32>, Nat,
                xs => List.length(&2, U32, xs),
                Core.gcm_zip_xor(Nil{}, stream), Nil{},
                Core.gcm_zip_xor_nil_left(stream))
        case byte <> tail Nil{}:
            impossible = Equal.cong(Nat, Bool,
                n => Nat.is_eq(n, 0n),
                1n+List.length(&2, U32, tail), 0n, same_length)
            Empty.absurd(
                {List.length(&2, U32,
                    Core.gcm_zip_xor(byte <> tail, Nil{})) ==
                 List.length(&2, U32, byte <> tail) : Nat},
                false_true(impossible))
        case byte <> tail stream_byte <> stream_tail:
            tail_length = Equal.cong(Nat, Nat, predecessor,
                1n+List.length(&2, U32, tail),
                1n+List.length(&2, U32, stream_tail), same_length)
            Equal.cong(Nat, Nat, n => 1n+n,
                List.length(&2, U32, Core.gcm_zip_xor(tail, stream_tail)),
                List.length(&2, U32, tail),
                zip_length_equal(tail, stream_tail, tail_length))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_zip_xor_nil_left
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=predecessor