proof/AES_MaskedXorProof.bend checks

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

6 imports

import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_ZipLengthProof.bend as ZipLengthProof
import ./AES_LengthLimitProof.bend as LengthLimitProof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32.bend as HubU32

Definitions

def bool_mask_xor_inv source · line 8 · raw

@+mask:Bool -> @+x:Bool -> @+y:Bool -> {Bool.and(mask, Bool.xor(Bool.and(mask, Bool.xor(x, y)), y)) == Bool.and(mask, x) : Bool}

def word_mask_xor_inv source · line 22 · raw

@+n:Nat -> @+mask:Word(n) -> @+x:Word(n) -> @+y:Word(n) -> {Word.and(n, mask, Word.xor(n, Word.and(n, mask, Word.xor(n, x, y)), y)) == Word.and(n, mask, x) : Word(n)}

def word_bits source · line 70 · raw

@+value:U32 -> Word(32n)

def gcm_mask_xor_inv source · line 74 · raw

@+x:U32 -> @+y:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_hex_mask(U32.xor(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_hex_mask(U32.xor(x, y), 255), y), 255) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_hex_mask(x, 255) : U32}

def bool_and_comm source · line 88 · raw

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

def word_and_comm source · line 95 · raw

@+n:Nat -> @+x:Word(n) -> @+y:Word(n) -> {Word.and(n, x, y) == Word.and(n, y, x) : Word(n)}

def byte_mask_identity source · line 118 · raw

@+value:U32 -> @below_256:{U32.is_lt(value, 256) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_hex_mask(value, 255) == value : U32}

def bool_and_true_left source · line 156 · raw

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

def bool_and_true_right source · line 168 · raw

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

def mask_bytes_identity source · line 180 · raw

@+bytes:List<&2, U32> -> @+valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_mask_bytes(bytes) == bytes : List<&2, U32>}

def predecessor source · line 203 · raw

@n:Nat -> Nat

def zip_xor_involution source · line 208 · raw

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

def ctr_decrypt_ciphertext_roundtrip source · line 276 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_bytes_valid(plaintext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(words, nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(plaintext, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce))))) == plaintext : List<&2, U32>}

def ctr_ciphertext_plaintext_valid source · line 317 · raw

@+plaintext:List<&2, U32> -> @+stream:List<&2, U32> -> @same_length:{List.length(&2, U32, plaintext) == List.length(&2, U32, stream) : Nat} -> @+plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(plaintext, stream)) == True{} : Bool}