~/bend-docscommunity

proof/AES_NistCtrProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend as AES_NistCtrProof

11 imports
import Base
import ../libs/AES256GCMCore.bend as Core
import ./AES_NistKeyScheduleProof.bend as Key
import ./AES_NistCtr2BlockProof.bend as B2
import ./AES_NistCtr2ComposeProof.bend as P2
import ./AES_NistCtr3BlockProof.bend as B3
import ./AES_NistCtr3ComposeProof.bend as P3
import ./AES_NistCtr4BlockProof.bend as B4
import ./AES_NistCtr4ComposeProof.bend as P4
import ./AES_NistCtr5BlockProof.bend as B5
import ./AES_NistCtr5ComposeProof.bend as P5

Definitions

def stream_step source · line 13 · raw

@+remaining:Nat -> @+fuel:Nat -> @+words:List<&2, U32> -> @+counter:List<&2, U32> -> @+block:List<&2, U32> -> @count:{remaining == 1n+fuel : Nat} -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, counter) == block : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(remaining, words, counter, []) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes_byte_at(block, 0n) <> 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(counter), List.tail(&2, U32, block)) : List<&2, U32>}

def checkpoint_ctr2_stream source · line 25 · raw

@+remaining:Nat -> @+fuel:Nat -> @+next_counter:List<&2, U32> -> @count:{remaining == 16n+fuel : Nat} -> @counter:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr2BlockProof.block) == next_counter : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(remaining, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr2BlockProof.block, []) == List.append(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr2BlockProof.result, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, next_counter, [])) : List<&2, U32>}

def checkpoint_ctr3_stream source · line 35 · raw

@+remaining:Nat -> @+fuel:Nat -> @+next_counter:List<&2, U32> -> @count:{remaining == 16n+fuel : Nat} -> @counter:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr3BlockProof.block) == next_counter : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(remaining, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr3BlockProof.block, []) == List.append(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr3BlockProof.result, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, next_counter, [])) : List<&2, U32>}

def checkpoint_ctr4_stream source · line 45 · raw

@+remaining:Nat -> @+fuel:Nat -> @+next_counter:List<&2, U32> -> @count:{remaining == 16n+fuel : Nat} -> @counter:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr4BlockProof.block) == next_counter : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(remaining, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr4BlockProof.block, []) == List.append(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr4BlockProof.result, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, next_counter, [])) : List<&2, U32>}

def checkpoint_ctr5_stream source · line 55 · raw

@+remaining:Nat -> @+fuel:Nat -> @+next_counter:List<&2, U32> -> @count:{remaining == 16n+fuel : Nat} -> @counter:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr5BlockProof.block) == next_counter : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(remaining, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr5BlockProof.block, []) == List.append(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr5BlockProof.result, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, next_counter, [])) : List<&2, U32>}

def counter_6 source · line 65 · raw

List<&2, U32>

def stream_64 source · line 68 · raw

List<&2, U32>

def stream_60 source · line 71 · raw

List<&2, U32>

def checkpoint_stream_64 source · line 74 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(64n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr2BlockProof.block, []) == stream_64 : List<&2, U32>}

def checkpoint_ctr5_partial source · line 78 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(12n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr5BlockProof.block, []) == List.take(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr5BlockProof.result, 12n) : List<&2, U32>}

def checkpoint_stream_60 source · line 84 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(60n, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistCtr2BlockProof.block, []) == stream_60 : List<&2, U32>}