AESMaskedXorProof.zip_xor_involution: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as AESMaskedXorProof
Lines 208-274 of qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&start_line=208&end_line=274

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

def zip_xor_involution(+bytes: List<&2, U32>,
    +stream: List<&2, U32>,
    same_length: {List.length(&2, U32, bytes) ==
        List.length(&2, U32, stream) : Nat}) ->
    {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, stream), stream) ==
     Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
    match bytes stream:
        case Nil{} _:
            +inner = Core.gcm_zip_xor_nil_left(stream)
            Equal.trans(List<&2, U32>,
                Core.gcm_zip_xor(Core.gcm_zip_xor(Nil{}, stream), stream),
                Core.gcm_zip_xor(Nil{}, stream), Nil{},
                Equal.cong(List<&2, U32>, List<&2, U32>,
                    xs => Core.gcm_zip_xor(xs, stream),
                    Core.gcm_zip_xor(Nil{}, stream), Nil{}, inner),
                inner)
        case _ <> _ Nil{}:
            unequal = Equal.cong(Nat, Bool,
                n => Nat.is_eq(n, 0n),
                List.length(&2, U32, bytes),
                List.length(&2, U32, Nil{}), same_length)
            Empty.absurd(
                {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, Nil{}), Nil{}) ==
                 Core.gcm_mask_bytes(bytes) : List<&2, U32>},
                ZipLengthProof.false_true(unequal))
        case byte <> tail stream_byte <> stream_tail:
            tail_length = Equal.cong(Nat, Nat, predecessor,
                List.length(&2, U32, byte <> tail),
                List.length(&2, U32, stream_byte <> stream_tail),
                same_length)
            recursive = zip_xor_involution(tail, stream_tail, tail_length)
            Equal.trans(List<&2, U32>,
                Core.gcm_zip_xor(
                    Core.gcm_zip_xor(byte <> tail,
                        stream_byte <> stream_tail),
                    stream_byte <> stream_tail),
                Core.gcm_hex_mask(U32.xor(
                    Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
                    stream_byte), 255) <>
                    Core.gcm_zip_xor(
                        Core.gcm_zip_xor(tail, stream_tail), stream_tail),
                Core.gcm_mask_bytes(byte <> tail),
                {==},
                Equal.trans(List<&2, U32>,
                    Core.gcm_hex_mask(U32.xor(
                        Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
                        stream_byte), 255) <>
                        Core.gcm_zip_xor(
                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
                    Core.gcm_hex_mask(byte, 255) <>
                        Core.gcm_zip_xor(
                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
                    Core.gcm_mask_bytes(byte <> tail),
                    Equal.cong(U32, List<&2, U32>,
                        head => head <>
                            Core.gcm_zip_xor(
                                Core.gcm_zip_xor(tail, stream_tail), stream_tail),
                        Core.gcm_hex_mask(U32.xor(
                            Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
                            stream_byte), 255),
                        Core.gcm_hex_mask(byte, 255),
                        gcm_mask_xor_inv(byte, stream_byte)),
                    Equal.cong(List<&2, U32>, List<&2, U32>,
                        rest => Core.gcm_hex_mask(byte, 255) <> rest,
                        Core.gcm_zip_xor(
                            Core.gcm_zip_xor(tail, stream_tail), stream_tail),
                        Core.gcm_mask_bytes(tail), recursive)))

Uses (17):
  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=Equal.trans
  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=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_hex_mask
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_mask_bytes
  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_MaskedXorProof.bend&name=gcm_mask_xor_inv
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend&name=predecessor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=false_true