~/bend-docscommunity

PROOF.bend timeout

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

26 imports
import Base
import ./proof/AES_NistInputProof.bend as AESNistInputProof
import ./LAWS.bend as L
import ./libs/JSON.bend as Json
import ./libs/URL.bend as URL
import ./libs/AES256GCM.bend as AES
import ./libs/AES256GCMCore.bend as Core
import ./proof/AES_EncryptProof.bend as AESEncryptProof
import ./proof/AES_TamperProof.bend as AESTamperProof
import ./proof/AES_CanonicalProof.bend as AESCanonicalProof
import ./proof/AES_ConstructorProof.bend as AESConstructorProof
import ./proof/AES_IdentityProof.bend as AESIdentityProof
import ./proof/AES_NistKeyScheduleProof.bend as AESNistKeyScheduleProof
import ./proof/AES_NistBlockComposeProof.bend as AESNistBlockComposeProof
import ./proof/AES_NistBlockProof.bend as AESNistBlockProof
import ./proof/AES_NistObservationProof.bend as AESNistObservationProof
import ./proof/AES_NistVectorProof.bend as AESNistVectorProof
import ./proof/AES_NistTamperVectorProof.bend as AESNistTamperVectorProof
import ./proof/JSON_StringProof.bend as StringProof
import ./proof/JSON_PrimitiveProof.bend as PrimitiveProof
import ./proof/JSON_NumberLexProof.bend as NumberLexProof
import ./proof/JSON_ParallelProof.bend as ParallelProof
import ./proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof
import ./proof/JSON_AssemblyProof.bend as AssemblyProof
import ./proof/JSON_SourceProof.bend as SourceProof
import ./proof/JSON_RenderLexProof.bend as RenderLexProof

Definitions

def ResultValue source · line 28 · raw

Type

def parse_for_equality source · line 31 · raw

@text:String -> ResultValue

def assemble_atom source · line 34 · raw

@result:ResultValue -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.assemble([0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Atom{result}], 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NeedValue{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Top{}}) == result : ResultValue}

def parallel_single source · line 39 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.token_list(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.decode_tree(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_tree([0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{text}])), []) == [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.decode_lexeme(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{text})] : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}

def assemble_source source · line 44 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.assemble(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.token_list(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.decode_tree(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_tree(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, False{}, []))), []), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NeedValue{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Top{}}) == Done{value} : ResultValue}

def parse_number_payload source · line 71 · raw

@+text:String -> @+certificate:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NumberCert<text> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse_normalized(text) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{text, certificate}} : ResultValue}

def assembled_string_payload source · line 96 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.assemble([0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Atom{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.decode_payload(String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(text), "\"")))}], 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NeedValue{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Top{}}) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{text}} : ResultValue}

def parse_string_payload source · line 100 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse_normalized(String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(text), "\""))) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Str{text}} : ResultValue}

def parse_leading_space source · line 118 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(" ", text)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_trailing_space source · line 121 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, " ")) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_trailing_tab source · line 128 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, "\t")) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_trailing_return source · line 135 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, "\r")) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_trailing_newline source · line 142 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, "\n")) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_suffix_space source · line 149 · raw

@+text:String -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, String.append(suffix, " "))) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_suffix_tab source · line 156 · raw

@+text:String -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, String.append(suffix, "\t"))) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_suffix_return source · line 163 · raw

@+text:String -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, String.append(suffix, "\r"))) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_suffix_newline source · line 170 · raw

@+text:String -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, String.append(suffix, "\n"))) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_leading_surround source · line 177 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(" \n\t\r", text)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def parse_surrounding_space source · line 180 · raw

@+text:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(String.append(" \n\t\r", String.append(text, "\r\t\n "))) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.parse(text) : Result<&1, &1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>}

def aes_nat_tail_ne source · line 372 · raw

@+a:Nat -> @+b:Nat -> @no:(@_:{1n+a == 1n+b : Nat} -> Empty) -> @_:{a == b : Nat} -> Empty

def aes_nat_pred source · line 376 · raw

@n:Nat -> Nat

def aes_nat_zero_ne_succ source · line 381 · raw

@+p:Nat -> @_:{0n == 1n+p : Nat} -> Empty

def aes_nat_succ_ne_zero source · line 387 · raw

@+p:Nat -> @_:{1n+p == 0n : Nat} -> Empty

def aes_nat_eq_step_status source · line 393 · raw

@+a:Nat -> @+b:Nat -> @result:Maybe<&0, {a == b : Nat}> -> {Maybe.is_some(&0, {1n+a == 1n+b : Nat}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_step(a, b, result)) == Maybe.is_some(&0, {a == b : Nat}, result) : Bool}

def aes_nat_eq_refl_is_some source · line 402 · raw

@+n:Nat -> {Maybe.is_some(&0, {n == n : Nat}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(n, n)) == True{} : Bool}

def aes_nat_eq_is_some source · line 417 · raw

@+a:Nat -> @+b:Nat -> @evidence:{a == b : Nat} -> {Maybe.is_some(&0, {a == b : Nat}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(a, b)) == True{} : Bool}

def aes_nat_eq_none_if_ne source · line 429 · raw

@+a:Nat -> @+b:Nat -> @no:(@_:{a == b : Nat} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(a, b) == None{} : Maybe<&0, {a == b : Nat}>}

def aes_bytes_proof_none_if_invalid source · line 450 · raw

@+bytes:List<&2, U32> -> @generated:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}> -> @no:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == False{} : Bool} -> {generated == None{} : Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}>}

def aes_bytes_valid_none_if_false source · line 466 · raw

@+bytes:List<&2, U32> -> @no:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == False{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_proof(bytes) == None{} : Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}>}

def aes_bytes_valid_status source · line 473 · raw

@+bytes:List<&2, U32> -> @b:Bool -> @link:{b == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) : Bool} -> {Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_from_bool(bytes, b, link)) == b : Bool}

def aes_bytes_cert_is_some source · line 481 · raw

@+bytes:List<&2, U32> -> @evidence:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool} -> {Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_proof(bytes)) == True{} : Bool}

def aes_key_from_no_size source · line 531 · raw

@+bytes:List<&2, U32> -> @valid:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key_from_proofs(bytes, None{}, valid) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidKey{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

def aes_key_from_no_valid source · line 537 · raw

@+bytes:List<&2, U32> -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.key_from_proofs(bytes, size, None{}) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidKey{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey>}

def aes_nonce_from_no_size source · line 574 · raw

@+bytes:List<&2, U32> -> @valid:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(bytes) == True{} : Bool}> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce_from_proofs(bytes, None{}, valid) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidNonce{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

def aes_nonce_from_no_valid source · line 580 · raw

@+bytes:List<&2, U32> -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce_from_proofs(bytes, size, None{}) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidNonce{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce>}

def encrypt_invalid_plaintext source · line 617 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @aad_ok:Bool -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_checked(key, nonce, aad, plaintext, aad_ok, False{}) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

def encrypt_using_plaintext_validity source · line 625 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @plaintext_ok:Bool -> Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>

def encrypt_invalid_aad source · line 643 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @plaintext_ok:Bool -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_checked(key, nonce, aad, plaintext, False{}, plaintext_ok) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>}

def encrypt_using_aad_validity source · line 651 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @aad_ok:Bool -> Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>

def decrypt_invalid_aad source · line 668 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @ciphertext_ok:Bool -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_checked(key, aad, envelope, False{}, ciphertext_ok) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.InvalidBytes{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def decrypt_using_aad_validity source · line 677 · raw

@key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @aad_ok:Bool -> Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>

def aes256gcm_nist_j0_block_checkpoint source · line 727 · raw

{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.block) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.result : List<&2, U32>}

Keep the composed NIST AES block certificate in the law proof book. This checkpoint proves the exact J0 AES result used by the empty-message vector.