proof/AES_IdentityProof.bend checks

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

8 imports

import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_EnvelopeProof.bend as Encoding
import ./AES_ConstructorProof.bend as Constructor
import ./AES_KnownAnswerProof.bend as Known
import ./AES_MaskedXorProof.bend as Masked
import ./AES_StringEqProof.bend as Logic

Definitions

def mask_word_same source · line 10 · raw

@+value:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 255) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_hex_mask(value, 255) : U32}

def mask_same source · line 15 · raw

@+bytes:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/proof/AES_EnvelopeProof.aes_hex_mask_bytes(bytes) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_mask_bytes(bytes) : List<&2, U32>}

def mask_identity source · line 27 · raw

@+bytes:List<&2, U32> -> @valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/proof/AES_EnvelopeProof.aes_hex_mask_bytes(bytes) == bytes : List<&2, U32>}

def decoded_or_empty source · line 34 · raw

@value:Maybe<&2, List<&2, U32>> -> List<&2, U32>

def hex_injective source · line 39 · raw

@+first:List<&2, U32> -> @+second:List<&2, U32> -> @first_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(first) == True{} : Bool} -> @second_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(second) == True{} : Bool} -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(first) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(second) : String} -> {first == second : List<&2, U32>}

def fields source · line 60 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> List<&2, String>

def optional_text source · line 65 · raw

@value:Maybe<&2, String> -> String

def field_text source · line 70 · raw

@index:Nat -> @parts:List<&2, String> -> String

def result_text source · line 73 · raw

@value:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String> -> String

def fields_equal source · line 78 · raw

@+first:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+second:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(first) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(second) : String} -> {fields(first) == fields(second) : List<&2, String>}

def fixed_hex_equal source · line 89 · raw

@+n:Nat -> @+first:List<&2, U32> -> @+second:List<&2, U32> -> @first_size:{List.length(&2, U32, first) == n : Nat} -> @second_size:{List.length(&2, U32, second) == n : Nat} -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(n, first)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(n, second)) : String} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(first) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(second) : String}

def encode_injective source · line 103 · raw

@+first:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+second:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @same:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(first) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(second) : String} -> {first == second : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope}

def exact_roundtrip_result source · line 140 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope> -> @encoded:{Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, result) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope)} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>} -> {result == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

def exact_roundtrip source · line 159 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope)) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}