def ctr_stream_exact_go_length
qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:153
import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
153def ctr_stream_exact_go_length(+fuel: Nat, +words: List<&2, U32>,
154 +counter: List<&2, U32>, +block: List<&2, U32>) ->
155 {List.length(&2, U32,
156 Core.gcm_ctr_stream_exact.go(fuel, words, counter, block)) ==
157 fuel : Nat}:
158 match fuel:
159 case 0n: {==}
160 case 1n+p:
161 +step = Core.gcm_ctr_step(words, counter, block)
162 Equal.cong(Nat, Nat, n => 1n+n,
163 List.length(&2, U32,
164 Core.gcm_ctr_stream_exact.go(p, words,
165 Core.gcm_ctr_step_counter(step),
166 Core.gcm_ctr_step_rest(step))),
167 p,
168 ctr_stream_exact_go_length(p, words,
169 Core.gcm_ctr_step_counter(step),
170 Core.gcm_ctr_step_rest(step)))