proof/AES_ConstructorProof.bend checks

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

4 imports

import Base
import ../libs/AES256GCM.bend as AES
import ./AES_CertificateProof.bend as Certificate
import ./AES_StringEqProof.bend as Logic

Definitions

def key_certificates source · line 6 · raw

@+bytes:List<&2, U32> -> @+first_size:{List.length(&2, U32, bytes) == 32n : Nat} -> @+first_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @+second_size:{List.length(&2, U32, bytes) == 32n : Nat} -> @+second_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey{bytes, first_size, first_valid} == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey{bytes, second_size, second_valid} : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey}

def key_accepts source · line 28 · raw

@+bytes:List<&2, U32> -> @+expected_size:{List.length(&2, U32, bytes) == 32n : Nat} -> @+expected_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}> -> @valid:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}> -> @size_present:{Maybe.is_some(&0, {List.length(&2, U32, bytes) == 32n : Nat}, size) == True{} : Bool} -> @valid_present:{Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key_from_proofs(bytes, size, valid) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey{bytes, expected_size, expected_valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

def nonce_certificates source · line 58 · raw

@+bytes:List<&2, U32> -> @+first_size:{List.length(&2, U32, bytes) == 12n : Nat} -> @+first_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @+second_size:{List.length(&2, U32, bytes) == 12n : Nat} -> @+second_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{bytes, first_size, first_valid} == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{bytes, second_size, second_valid} : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}

def nonce_accepts source · line 80 · raw

@+bytes:List<&2, U32> -> @+expected_size:{List.length(&2, U32, bytes) == 12n : Nat} -> @+expected_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}> -> @valid:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}> -> @size_present:{Maybe.is_some(&0, {List.length(&2, U32, bytes) == 12n : Nat}, size) == True{} : Bool} -> @valid_present:{Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce_from_proofs(bytes, size, valid) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{bytes, expected_size, expected_valid}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

def nonce_equal source · line 111 · raw

@+bytes:List<&2, U32> -> @+size:{List.length(&2, U32, bytes) == 12n : Nat} -> @+valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> @+expected:List<&2, U32> -> @same:{bytes == expected : List<&2, U32>} -> @+expected_size:{List.length(&2, U32, expected) == 12n : Nat} -> @+expected_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(expected) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{bytes, size, valid} == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce{expected, expected_size, expected_valid} : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce}