def stream_step_length

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

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

128def stream_step_length(+words: List<&2, U32>,
129    +counter: List<&2, U32>, +acc: List<&2, U32>) ->
130    {List.length(&2, U32, List.append(&2, U32,
131        List.reverse(&2, U32,
132            Core.aes256_encrypt_expanded(words, counter)), acc)) ==
133     Nat.add(16n, List.length(&2, U32, acc)) : Nat}:
134    +block = Core.aes256_encrypt_expanded(words, counter)
135    Equal.trans(Nat,
136        List.length(&2, U32,
137            List.append(&2, U32, List.reverse(&2, U32, block), acc)),
138        Nat.add(List.length(&2, U32,
139            List.reverse(&2, U32, block)),
140            List.length(&2, U32, acc)),
141        Nat.add(16n, List.length(&2, U32, acc)),
142        append_length(List.reverse(&2, U32, block), acc),
143        Equal.cong(Nat, Nat,
144            n => Nat.add(n, List.length(&2, U32, acc)),
145            List.length(&2, U32, List.reverse(&2, U32, block)),
146            16n,
147            Equal.trans(Nat,
148                List.length(&2, U32, List.reverse(&2, U32, block)),
149                List.length(&2, U32, block), 16n,
150                reverse_length(block),
151                encrypt_block_length(words, counter))))