proof/AES_LengthLimitProof.bend checks

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

3 imports

import Base
import ../libs/AES256GCM.bend as AES
import ./AES_ZipLengthProof.bend as ZipLengthProof

Definitions

def bool_and_true_right source · line 5 · raw

@+a:Bool -> @+b:Bool -> @both:{Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}

def predecessor source · line 17 · raw

@n:Nat -> Nat

def length_limit_go_same source · line 22 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+low:U32 -> @+high:U32 -> @+max_low:U32 -> @+max_high:U32 -> @+within:Bool -> @same_length:{List.length(&2, U32, a) == List.length(&2, U32, b) : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_length_limit.go(List.length(&2, U32, a), a, low, high, max_low, max_high, within) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_length_limit.go(List.length(&2, U32, b), b, low, high, max_low, max_high, within) : Bool}

def bytes_length_limit_same source · line 71 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+max_low:U32 -> @+max_high:U32 -> @same_length:{List.length(&2, U32, a) == List.length(&2, U32, b) : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_length_limit(a, max_low, max_high) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_length_limit(b, max_low, max_high) : Bool}

def plaintext_valid_same_length source · line 80 · raw

@+ciphertext:List<&2, U32> -> @+plaintext:List<&2, U32> -> @ciphertext_bytes_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(ciphertext) == True{} : Bool} -> @plaintext_is_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @same_length:{List.length(&2, U32, ciphertext) == List.length(&2, U32, plaintext) : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(ciphertext) == True{} : Bool}