def stream_step

qasim-bend-kit@0.1.0.2 · proof/AES_NistCtrProof.bend:13

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

13def stream_step(+remaining: Nat, +fuel: Nat, +words: List<&2, U32>, +counter: List<&2, U32>, +block: List<&2, U32>,
14    count: {remaining == 1n+fuel : Nat}, same: {Core.aes256_encrypt_expanded(words, counter) == block : List<&2, U32>}) ->
15    {Core.gcm_ctr_stream_exact.go(remaining, words, counter, Nil{}) ==
16     Core.aes_byte_at(block, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, block)) : List<&2, U32>}:
17    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(remaining, words, counter, Nil{}),
18        Core.gcm_ctr_stream_exact.go(1n+fuel, words, counter, Nil{}),
19        Core.aes_byte_at(block, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, block)),
20        Equal.cong(Nat, List<&2, U32>, n => Core.gcm_ctr_stream_exact.go(n, words, counter, Nil{}), remaining, 1n+fuel, count),
21        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
22            Core.aes_byte_at(value, 0n) <> Core.gcm_ctr_stream_exact.go(fuel, words, Core.gcm_inc32(counter), List.tail(&2, U32, value)),
23            Core.aes256_encrypt_expanded(words, counter), block, same))