AESZipLengthProof.ctr_stream_exact_go_length: 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 153-170 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=153&end_line=170

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

def ctr_stream_exact_go_length(+fuel: Nat, +words: List<&2, U32>,
    +counter: List<&2, U32>, +block: List<&2, U32>) ->
    {List.length(&2, U32,
        Core.gcm_ctr_stream_exact.go(fuel, words, counter, block)) ==
     fuel : Nat}:
    match fuel:
        case 0n: {==}
        case 1n+p:
            +step = Core.gcm_ctr_step(words, counter, block)
            Equal.cong(Nat, Nat, n => 1n+n,
                List.length(&2, U32,
                    Core.gcm_ctr_stream_exact.go(p, words,
                        Core.gcm_ctr_step_counter(step),
                        Core.gcm_ctr_step_rest(step))),
                p,
                ctr_stream_exact_go_length(p, words,
                    Core.gcm_ctr_step_counter(step),
                    Core.gcm_ctr_step_rest(step)))

Uses (9):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_step_counter
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_step_rest
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=gcm_ctr_stream_exact.go