def checkpoint_ctr3_stream

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

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_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3BlockProof.bend as B3
import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr3ComposeProof.bend as P3

35def checkpoint_ctr3_stream(+remaining: Nat, +fuel: Nat, +next_counter: List<&2, U32>,
36    count: {remaining == 16n+fuel : Nat},
37    counter: {Core.gcm_inc32(B3.block()) == next_counter : List<&2, U32>}) ->
38    {Core.gcm_ctr_stream_exact.go(remaining, Key.words_60(), B3.block(), Nil{}) == List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})) : List<&2, U32>}:
39    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(remaining, Key.words_60(), B3.block(), Nil{}), Core.aes_byte_at(B3.result(), 0n) <> Core.gcm_ctr_stream_exact.go(15n+fuel, Key.words_60(), Core.gcm_inc32(B3.block()), List.tail(&2, U32, B3.result())), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})),
40        stream_step(remaining, 15n+fuel, Key.words_60(), B3.block(), B3.result(), count, P3.expanded_block_matches()),
41        Equal.trans(List<&2, U32>, Core.aes_byte_at(B3.result(), 0n) <> Core.gcm_ctr_stream_exact.go(15n+fuel, Key.words_60(), Core.gcm_inc32(B3.block()), List.tail(&2, U32, B3.result())), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), Core.gcm_inc32(B3.block()), Nil{})), List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next_counter, Nil{})), {==},
42            Equal.cong(List<&2, U32>, List<&2, U32>, next => List.append(&2, U32, B3.result(), Core.gcm_ctr_stream_exact.go(fuel, Key.words_60(), next, Nil{})),
43                Core.gcm_inc32(B3.block()), next_counter, counter)))