proof/AES_EnvelopeProof.bend checks

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

3 imports

import Base
import ../libs/AES256GCM.bend as AES
import ./AES_CanonicalProof.bend as Canonical

Definitions

def aes_hex_mask_15_lt_16 source · line 5 · raw

@+value:U32 -> {U32.is_lt(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 15), 16) == True{} : Bool}

def aes_hex_mask_255_lt_256 source · line 10 · raw

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

def aes_bool_and_false source · line 15 · raw

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

def aes_bool_and_true source · line 20 · raw

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

def aes_hex_word_and_equiv source · line 25 · raw

@n:Nat -> @mask:Word(n) -> @value:Word(n) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_word_and(n, mask, value) == Word.and(n, value, mask) : Word(n)}

def aes_hex_word_and_idempotent source · line 52 · raw

@n:Nat -> @mask:Word(n) -> @+value:Word(n) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_word_and(n, mask, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_word_and(n, mask, value)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_word_and(n, mask, value) : Word(n)}

def aes_hex_mask_idempotent source · line 76 · raw

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

def aes_hex_digit_inverse source · line 88 · raw

@+value:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_nibble(Char.to_u32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value))) == Some{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 15)} : Maybe<&2, U32>}

def aes_hex_digit_no_dot source · line 109 · raw

@+value:U32 -> {Char.is_eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), '.') == False{} : Bool}

def aes_split_hex_digit_no_dot source · line 129 · raw

@value:U32 -> @+parts:List<&2, String> -> {String.split.fin(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), parts, Char.is_eq(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), '.')) == String.split.push(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), parts) : List<&2, String>}

def aes_hex_join_shift_mask source · line 138 · raw

@+value:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_join(U32.shrn(value, 4n), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 15)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 255) : U32}

def aes_hex_join_masked_shift_mask source · line 144 · raw

@+value:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_join(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(U32.shrn(value, 4n), 15), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 15)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(value, 255) : U32}

def aes_hex_byte_prefix_idempotent source · line 150 · raw

@+byte:U32 -> @+tail:String -> {SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(U32.shrn(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255), 255), 4n)), SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255), 255)), tail}} == SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(U32.shrn(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255), 4n)), SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255)), tail}} : String}

def aes_hex_mask_bytes source · line 184 · raw

@+bytes:List<&2, U32> -> List<&2, U32>

def aes_hex_bytes_mask_idempotent source · line 189 · raw

@+bytes:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(aes_hex_mask_bytes(bytes)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes) : String}

def aes_hex_pair_roundtrip source · line 214 · raw

@+byte:U32 -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_pair(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(U32.shrn(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255), 4n)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255))) == Some{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_mask(byte, 255)} : Maybe<&2, U32>}

def aes_decode_hex_bytes source · line 261 · raw

@+bytes:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decode_hex(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes)) == Some{aes_hex_mask_bytes(bytes)} : Maybe<&2, List<&2, U32>>}

def aes_split_push_single source · line 295 · raw

@value:U32 -> @+suffix:String -> {String.split.push(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), [suffix]) == [SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), suffix}] : List<&2, String>}

def aes_hex_bytes_split_single source · line 300 · raw

@+bytes:List<&2, U32> -> {String.split(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes), '.') == [0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes)] : List<&2, String>}

def aes_split_push_cons source · line 372 · raw

@value:U32 -> @+head:String -> @+tail:List<&2, String> -> {String.split.push(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), head <> tail) == SCon{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_digit(value), head} <> tail : List<&2, String>}

def aes_hex_bytes_split_before_period source · line 377 · raw

@+bytes:List<&2, U32> -> @+suffix:String -> {String.split(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes), String.append(".", suffix)), '.') == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(bytes) <> String.split(suffix, '.') : List<&2, String>}

def aes_split_leading_dot source · line 451 · raw

@+suffix:String -> {String.split(String.append(".", suffix), '.') == "" <> String.split(suffix, '.') : List<&2, String>}

def aes_split_v1_prefix source · line 456 · raw

@+suffix:String -> {String.split(String.append("v1.", suffix), '.') == "v1" <> String.split(suffix, '.') : List<&2, String>}

def aes_string_append_assoc source · line 461 · raw

@+a:String -> @+b:String -> @+c:String -> {String.append(a, String.append(b, c)) == String.append(a, String.append(b, c)) : String}

def aes_split_v1_hex_fields source · line 470 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> {String.split(String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext)))))), '.') == ["v1", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext)] : List<&2, String>}

def aes_encode_fields_split source · line 512 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {String.split(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode_impl(envelope), '.') == ["v1", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(12n, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)))), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(16n, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)))), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))] : List<&2, String>}

def aes_false_type source · line 528 · raw

@b:Bool -> Data

def aes_false_true source · line 533 · raw

@e:{False{} == True{} : Bool} -> Empty

def aes_nat_predecessor source · line 537 · raw

@n:Nat -> Nat

def aes_fixed_bytes_length source · line 542 · raw

@+n:Nat -> @+bytes:List<&2, U32> -> {List.length(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(n, bytes)) == n : Nat}

def aes_fixed_bytes_identity source · line 555 · raw

@+n:Nat -> @+bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == n : Nat} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(n, bytes) == bytes : List<&2, U32>}

def aes_parse_decoded_masked_map source · line 582 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @nonce_size:{List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat} -> @tag_size:{List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat} -> @nonce_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool} -> @tag_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool} -> @ciphertext_valid:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext), Some{nonce_size}, Some{tag_size}, Some{nonce_valid}, Some{tag_valid}, Some{ciphertext_valid})) == Done{String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext))))))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_hex_mask_bytes_length source · line 663 · raw

@+bytes:List<&2, U32> -> {List.length(&2, U32, aes_hex_mask_bytes(bytes)) == List.length(&2, U32, bytes) : Nat}

def aes_hex_mask_bytes_valid source · line 673 · raw

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

def aes_nat_eq_self source · line 695 · raw

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

def aes_bytes_valid_status source · line 707 · 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_masked_bytes_cert_is_some source · line 715 · raw

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

def aes_nat_eq_is_some source · line 727 · 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_masked_size_is_some source · line 744 · raw

@+bytes:List<&2, U32> -> @+expected:Nat -> @size:{List.length(&2, U32, bytes) == expected : Nat} -> {Maybe.is_some(&0, {List.length(&2, U32, aes_hex_mask_bytes(bytes)) == expected : Nat}, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(List.length(&2, U32, aes_hex_mask_bytes(bytes)), expected)) == True{} : Bool}

def aes_maybe_cert_value source · line 759 · raw

@A:Type -> @cert:Maybe<&0, A> -> @present:{Maybe.is_some(&0, A, cert) == True{} : Bool} -> A

def aes_maybe_cert_reconstruct source · line 765 · raw

@A:Type -> @cert:Maybe<&0, A> -> @present:{Maybe.is_some(&0, A, cert) == True{} : Bool} -> {cert == Some{aes_maybe_cert_value(A, cert, present)} : Maybe<&0, A>}

def aes_parse_decoded_map_goal source · line 775 · raw

@nonce:List<&2, U32> -> @tag:List<&2, U32> -> @ciphertext:List<&2, U32> -> @ns:Maybe<&0, {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat}> -> @ts:Maybe<&0, {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat}> -> @nv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool}> -> @tv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool}> -> @cv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}> -> Type

def aes_parse_decoded_if_some source · line 795 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @ns:Maybe<&0, {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat}> -> @ts:Maybe<&0, {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat}> -> @nv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool}> -> @tv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool}> -> @cv:Maybe<&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}> -> @ns_present:{Maybe.is_some(&0, {List.length(&2, U32, aes_hex_mask_bytes(nonce)) == 12n : Nat}, ns) == True{} : Bool} -> @ts_present:{Maybe.is_some(&0, {List.length(&2, U32, aes_hex_mask_bytes(tag)) == 16n : Nat}, ts) == True{} : Bool} -> @nv_present:{Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(nonce)) == True{} : Bool}, nv) == True{} : Bool} -> @tv_present:{Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(tag)) == True{} : Bool}, tv) == True{} : Bool} -> @cv_present:{Maybe.is_some(&0, {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_valid(aes_hex_mask_bytes(ciphertext)) == True{} : Bool}, cv) == True{} : Bool} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext), ns, ts, nv, tv, cv)) == Done{String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext))))))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_parse_decoded_checked_map source · line 873 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @nonce_size:{List.length(&2, U32, nonce) == 12n : Nat} -> @tag_size:{List.length(&2, U32, tag) == 16n : Nat} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_decoded(aes_hex_mask_bytes(nonce), aes_hex_mask_bytes(tag), aes_hex_mask_bytes(ciphertext), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(List.length(&2, U32, aes_hex_mask_bytes(nonce)), 12n), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_nat_eq_proof(List.length(&2, U32, aes_hex_mask_bytes(tag)), 16n), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_proof(aes_hex_mask_bytes(nonce)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_proof(aes_hex_mask_bytes(tag)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aes_bytes_valid_proof(aes_hex_mask_bytes(ciphertext)))) == Done{String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext))))))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_parse_decoded_hex_map source · line 904 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @nonce_size:{List.length(&2, U32, nonce) == 12n : Nat} -> @tag_size:{List.length(&2, U32, tag) == 16n : Nat} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_decoded_hex(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decode_hex(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decode_hex(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decode_hex(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext)))) == Done{String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext))))))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_parse_fields_hex_map source · line 976 · raw

@+nonce:List<&2, U32> -> @+tag:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @nonce_size:{List.length(&2, U32, nonce) == 12n : Nat} -> @tag_size:{List.length(&2, U32, tag) == 16n : Nat} -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_fields(["v1", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext)])) == Done{String.append("v1.", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(nonce), String.append(".", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(tag), String.append(".", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(ciphertext))))))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_parse_encoder_fields_map source · line 989 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {Result.map(&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope, String, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.parse_fields(["v1", 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(12n, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)))), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.fixed_bytes(16n, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)))), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.hex_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))])) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encode(envelope)} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, String>}

def aes_parse_fields_encoded_map source · line 1009 · raw

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

def aes_envelope_roundtrip source · line 1034 · raw

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