proof/AES_ZipLengthProof.bend checks

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

2 imports

import Base
import ../libs/AES256GCMCore.bend as Core

Definitions

def false_type source · line 4 · raw

@b:Bool -> Data

def false_true source · line 9 · raw

@e:{False{} == True{} : Bool} -> Empty

def predecessor source · line 13 · raw

@n:Nat -> Nat

def zip_length_equal source · line 18 · raw

@+bytes:List<&2, U32> -> @+stream:List<&2, U32> -> @same_length:{List.length(&2, U32, bytes) == List.length(&2, U32, stream) : Nat} -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(bytes, stream)) == List.length(&2, U32, bytes) : Nat}

def encrypt_block_length source · line 47 · raw

@+words:List<&2, U32> -> @+counter:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, counter)) == 16n : Nat}

def nat_add_succ_right source · line 54 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}

def nat_add_zero_right source · line 63 · raw

@+a:Nat -> {Nat.add(a, 0n) == a : Nat}

def nat_add_comm source · line 70 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, b) == Nat.add(b, a) : Nat}

def reverse_go_length source · line 86 · raw

@+xs:List<&2, U32> -> @+acc:List<&2, U32> -> {List.length(&2, U32, List.reverse.go(&2, U32, xs, acc)) == Nat.add(List.length(&2, U32, acc), List.length(&2, U32, xs)) : Nat}

def reverse_length source · line 111 · raw

@+xs:List<&2, U32> -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}

def append_length source · line 116 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}

def stream_step_length source · line 128 · raw

@+words:List<&2, U32> -> @+counter:List<&2, U32> -> @+acc:List<&2, U32> -> {List.length(&2, U32, List.append(&2, U32, List.reverse(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, counter)), acc)) == Nat.add(16n, List.length(&2, U32, acc)) : Nat}

def ctr_stream_exact_go_length source · line 153 · raw

@+fuel:Nat -> @+words:List<&2, U32> -> @+counter:List<&2, U32> -> @+block:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(fuel, words, counter, block)) == fuel : Nat}

def ctr_stream_exact_length source · line 172 · raw

@+fuel:Nat -> @+words:List<&2, U32> -> @+start:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(fuel, words, start)) == fuel : Nat}

def ctr_encrypt_ciphertext_length source · line 178 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ciphertext_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(words, nonce, plaintext))) == List.length(&2, U32, plaintext) : Nat}