libs/AES256GCM.bend checks

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

2 imports

import Base
import ./AES256GCMCore.bend as Core

Laws

law key provedsource · line 103 · raw

@bytes:List<&2, U32> -> Result<&2, &2, Error, SecretKey>

Constructors validate raw input; SecretKey/Nonce/Tag certificates enforce sizes.

law nonce provedsource · line 107 · raw

@bytes:List<&2, U32> -> Result<&2, &2, Error, Nonce>

law encrypt provedsource · line 113 · raw

@key:SecretKey -> @nonce:Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> Result<&2, &2, Error, Envelope>

Deterministic primitive: the caller supplies a nonce unique for this key. The eventual effectful wrapper must generate nonces using an OS CSPRNG.

law decrypt provedsource · line 121 · raw

@key:SecretKey -> @aad:List<&2, U32> -> @envelope:Envelope -> Result<&2, &2, Error, List<&2, U32>>

Fail contains only an Error, never unauthenticated or partial plaintext.

law encode provedsource · line 130 · raw

@envelope:Envelope -> String

Canonical envelope: v1.<lowercase nonce hex>.<lowercase tag hex>.<ciphertext hex>. The nonce has 24 hex characters, the tag 32, ciphertext an even number (or 0). AAD is external and must be supplied unchanged when decrypting.

law parse provedsource · line 134 · raw

@text:String -> Result<&2, &2, Error, Envelope>

Types

type SecretKey source · line 66 · raw

Data

SecretKey

@bytes:List<&2, U32> -> @-size:{List.length(&2, U32, bytes) == 32n : Nat} -> @-valid:{bytes_valid(bytes) == True{} : Bool} -> SecretKey

type Nonce source · line 73 · raw

Data

Nonce

@bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == 12n : Nat} -> @valid:{bytes_valid(bytes) == True{} : Bool} -> Nonce

type Tag source · line 80 · raw

Data

Tag

@bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == 16n : Nat} -> @valid:{bytes_valid(bytes) == True{} : Bool} -> Tag

type Envelope source · line 87 · raw

Data

Envelope

@nonce:Nonce -> @ciphertext:List<&2, U32> -> @tag:Tag -> @valid:{bytes_valid(ciphertext) == True{} : Bool} -> Envelope

type Error source · line 95 · raw

Data

InvalidKey
```
Error
```
InvalidNonce
```
Error
```
InvalidBytes
```
Error
```
InvalidEnvelope
```
Error
```
AuthenticationFailed
```
Error
```

Definitions

def bytes_valid source · line 6 · raw

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

AES-256-GCM with validated inputs and canonical envelope serialization. Bytes use U32 storage, with validation certificates excluding values above 255.

def core_bytes_valid_eq source · line 12 · raw

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

def core_bytes_valid_proof source · line 22 · raw

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

def length_pair_high source · line 31 · raw

@low:U32 -> @high_cmp:Cmp -> @max_low:U32 -> Bool

def length_pair_within source · line 37 · raw

@low:U32 -> @high:U32 -> @max_low:U32 -> @max_high:U32 -> Bool

def bytes_length_limit.go source · line 40 · raw

@fuel:Nat -> @bytes:List<&2, U32> -> @low:U32 -> @+high:U32 -> @+max_low:U32 -> @+max_high:U32 -> @within:Bool -> Bool

def bytes_length_limit source · line 55 · raw

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

def plaintext_valid source · line 60 · raw

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

GCM limits are expressed in bytes after requiring byte-aligned input.

def aad_valid source · line 63 · raw

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

def nonce_bytes source · line 139 · raw

@nonce:Nonce -> List<&2, U32>

Read-only projections needed to state the contract.

def tag_bytes source · line 143 · raw

@tag:Tag -> List<&2, U32>

def tag_bytes_size source · line 147 · raw

@tag:Tag -> {List.length(&2, U32, tag_bytes(tag)) == 16n : Nat}

def tag_bytes_valid source · line 152 · raw

@tag:Tag -> {bytes_valid(tag_bytes(tag)) == True{} : Bool}

def ciphertext source · line 157 · raw

@envelope:Envelope -> List<&2, U32>

def envelope_ciphertext_valid source · line 161 · raw

@envelope:Envelope -> {bytes_valid(ciphertext(envelope)) == True{} : Bool}

def envelope_nonce source · line 166 · raw

@envelope:Envelope -> Nonce

def envelope_tag source · line 170 · raw

@envelope:Envelope -> Tag

def hex_digit_kind source · line 175 · raw

@+n:U32 -> @decimal:Bool -> Char

Canonical lowercase hexadecimal envelope serialization.

def hex_word_and source · line 182 · raw

@n:Nat -> @mask:Word(n) -> @+value:Word(n) -> Word(n)

The mask-first implementation keeps zero mask bits visibly false to Bend's checker, which supports the nibble range proofs used by the codec.

def hex_mask source · line 196 · raw

@value:U32 -> @mask:U32 -> U32

def hex_digit.nibble source · line 201 · raw

@+n:U32 -> Char

def hex_digit source · line 221 · raw

@+n:U32 -> Char

def hex_bytes source · line 224 · raw

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

def fixed_bytes source · line 235 · raw

@n:Nat -> @bytes:List<&2, U32> -> List<&2, U32>

Serialize validated fixed-size fields through a fixed-size byte view. This makes the wire length structural even when the constructor certificate is erased from runtime storage.

def encode_impl source · line 243 · raw

@envelope:Envelope -> String

def hex_nibble source · line 253 · raw

@+code:U32 -> Maybe<&2, U32>

Match the ASCII code point directly so each accepted nibble normalizes to a literal.

def hex_join source · line 273 · raw

@high:U32 -> @low:U32 -> U32

def hex_pair.combine source · line 280 · raw

@high:Maybe<&2, U32> -> @low:Maybe<&2, U32> -> Maybe<&2, U32>

def hex_pair source · line 286 · raw

@first:Char -> @second:Char -> Maybe<&2, U32>

def hex_pairs source · line 290 · raw

@chars:List<&2, Char> -> List<&2, Maybe<&2, U32>>

def collect_hex.cons source · line 297 · raw

@pair:Maybe<&2, U32> -> @result:Maybe<&2, List<&2, U32>> -> Maybe<&2, List<&2, U32>>

def collect_hex source · line 304 · raw

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

def decode_hex source · line 309 · raw

@text:String -> Maybe<&2, List<&2, U32>>

def aes_nat_eq_step source · line 312 · raw

@+a:Nat -> @+b:Nat -> @result:Maybe<&0, {a == b : Nat}> -> Maybe<&0, {1n+a == 1n+b : Nat}>

def aes_nat_eq_proof source · line 318 · raw

@+a:Nat -> @+b:Nat -> Maybe<&0, {a == b : Nat}>

def aes_bool_true_proof source · line 325 · raw

@+x:U32 -> @b:Bool -> @link:{b == U32.is_lt(x, 256) : Bool} -> Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>

def aes_bytes_valid_cons_proof source · line 333 · raw

@x:U32 -> @tail:List<&2, U32> -> @head_proof:Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}> -> @tail_proof:Maybe<&0, {bytes_valid(tail) == True{} : Bool}> -> Maybe<&0, {bytes_valid(x <> tail) == True{} : Bool}>

def aes_bytes_valid_from_bool source · line 348 · raw

@+bytes:List<&2, U32> -> @b:Bool -> @link:{b == bytes_valid(bytes) : Bool} -> Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>

def aes_bytes_valid_proof source · line 356 · raw

@+bytes:List<&2, U32> -> Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>

def key_checked source · line 360 · raw

@bytes:List<&2, U32> -> @-size:{List.length(&2, U32, bytes) == 32n : Nat} -> @-valid:{bytes_valid(bytes) == True{} : Bool} -> Result<&2, &2, Error, SecretKey>

def key_from_proofs source · line 364 · raw

@+bytes:List<&2, U32> -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}> -> @valid:Maybe<&0, {bytes_valid(bytes) == True{} : Bool}> -> Result<&2, &2, Error, SecretKey>

def key_impl source · line 371 · raw

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

def nonce_checked source · line 375 · raw

@bytes:List<&2, U32> -> @size:{List.length(&2, U32, bytes) == 12n : Nat} -> @valid:{bytes_valid(bytes) == True{} : Bool} -> Result<&2, &2, Error, Nonce>

def nonce_from_proofs source · line 379 · raw

@+bytes:List<&2, U32> -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}> -> @valid:Maybe<&0, {bytes_valid(bytes) == True{} : Bool}> -> Result<&2, &2, Error, Nonce>

def nonce_impl source · line 386 · raw

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

def secret_key_bytes source · line 390 · raw

@key:SecretKey -> List<&2, U32>

def raw_nonce_bytes source · line 394 · raw

@nonce:Nonce -> List<&2, U32>

def tag_from_proofs source · line 398 · raw

@bytes:List<&2, U32> -> @size:Maybe<&0, {List.length(&2, U32, bytes) == 16n : Nat}> -> @valid:Maybe<&0, {bytes_valid(bytes) == True{} : Bool}> -> Maybe<&2, Tag>

def envelope_from_proofs source · line 405 · raw

@nonce:Nonce -> @+ciphertext:List<&2, U32> -> @tag:Tag -> @valid:Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}> -> Maybe<&2, Envelope>

def envelope_from_tag_proof source · line 411 · raw

@nonce:Nonce -> @+ciphertext:List<&2, U32> -> @tag_bytes:List<&2, U32> -> @tag:Maybe<&2, Tag> -> @valid:Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}> -> Maybe<&2, Envelope>

def envelope_from_gcm source · line 417 · raw

@nonce:Nonce -> @output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> Maybe<&2, Envelope>

def envelope_from_gcm_checked source · line 426 · raw

@nonce:Nonce -> @output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> Envelope

def encrypt_output source · line 435 · raw

@nonce:Nonce -> @maybe_envelope:Maybe<&2, Envelope> -> Result<&2, &2, Error, Envelope>

def encrypt_output_from_gcm source · line 440 · raw

@+nonce:Nonce -> @output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput -> Result<&2, &2, Error, Envelope>

def encrypt_valid_output source · line 444 · raw

@key:SecretKey -> @+nonce:Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmOutput

def encrypt_valid source · line 449 · raw

@key:SecretKey -> @+nonce:Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> Result<&2, &2, Error, Envelope>

def encrypt_checked source · line 454 · raw

@key:SecretKey -> @nonce:Nonce -> @aad:List<&2, U32> -> @plaintext:List<&2, U32> -> @aad_ok:Bool -> @plaintext_ok:Bool -> Result<&2, &2, Error, Envelope>

def encrypt_impl source · line 460 · raw

@key:SecretKey -> @nonce:Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> Result<&2, &2, Error, Envelope>

def bytes_difference.go source · line 464 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> @+difference:U32 -> U32

def bytes_equal_full_scan source · line 471 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> Bool

def decrypt_payload source · line 474 · raw

@words:List<&2, U32> -> @envelope:Envelope -> Result<&2, &2, Error, List<&2, U32>>

def decrypt_auth_result source · line 479 · raw

@words:List<&2, U32> -> @envelope:Envelope -> @authenticated:Bool -> Result<&2, &2, Error, List<&2, U32>>

def decrypt_authenticated_tag source · line 484 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @+envelope:Envelope -> @tag:Tag -> Result<&2, &2, Error, List<&2, U32>>

def decrypt_authenticated source · line 495 · raw

@key:SecretKey -> @+aad:List<&2, U32> -> @+envelope:Envelope -> Result<&2, &2, Error, List<&2, U32>>

def decrypt_checked source · line 502 · raw

@+key:SecretKey -> @aad:List<&2, U32> -> @+envelope:Envelope -> @aad_ok:Bool -> @ciphertext_ok:Bool -> Result<&2, &2, Error, List<&2, U32>>

def decrypt_impl source · line 509 · raw

@key:SecretKey -> @+aad:List<&2, U32> -> @+envelope:Envelope -> Result<&2, &2, Error, List<&2, U32>>

def parse_decoded source · line 512 · raw

@+nonce_bytes:List<&2, U32> -> @+tag_bytes:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @nonce_size:Maybe<&0, {List.length(&2, U32, nonce_bytes) == 12n : Nat}> -> @tag_size:Maybe<&0, {List.length(&2, U32, tag_bytes) == 16n : Nat}> -> @nonce_valid:Maybe<&0, {bytes_valid(nonce_bytes) == True{} : Bool}> -> @tag_valid:Maybe<&0, {bytes_valid(tag_bytes) == True{} : Bool}> -> @ciphertext_valid:Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}> -> Result<&2, &2, Error, Envelope>

def parse_decoded_hex source · line 523 · raw

@nonce:Maybe<&2, List<&2, U32>> -> @tag:Maybe<&2, List<&2, U32>> -> @ciphertext:Maybe<&2, List<&2, U32>> -> Result<&2, &2, Error, Envelope>

def parse_version_fields source · line 532 · raw

@fields:List<&2, String> -> Result<&2, &2, Error, Envelope>

def parse_version source · line 538 · raw

@fields:List<&2, String> -> @valid_version:Bool -> Result<&2, &2, Error, Envelope>

def parse_string_cmp_is_eq source · line 543 · raw

@result:Pair(Pair(String, String), Cmp) -> Bool

def parse_fields source · line 548 · raw

@fields:List<&2, String> -> Result<&2, &2, Error, Envelope>

def parse_canonical_decision source · line 554 · raw

@text:String -> @envelope:Envelope -> @canonical:Bool -> Result<&2, &2, Error, Envelope>

def parse_canonical source · line 560 · raw

@+text:String -> @result:Result<&2, &2, Error, Envelope> -> Result<&2, &2, Error, Envelope>

def parse_impl source · line 569 · raw

@+text:String -> Result<&2, &2, Error, Envelope>