~/bend-docscommunity

libs/AES256GCMCore.bend checks

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

2 imports
import Base
import ./AES256SBox.bend as SBox

Types

type AesColumn source · line 163 · raw

Data

type GcmTag source · line 293 · raw

Data

type GcmCiphertext source · line 300 · raw

Data

type GhashField source · line 328 · raw

Data

Keep the 128-bit GHASH accumulator in four machine words during its hot loop.

type GcmCtrStep source · line 478 · raw

Data

type GcmOutput source · line 628 · raw

Data

Definitions

def xor_if source · line 6 · raw

@a:U32 -> @b:U32 -> @yes:Bool -> U32

Byte arithmetic. Inputs and outputs are represented by U32 values in [0,255]. Turn a boolean into an all-zero or all-one word to keep field arithmetic branchless.

def gf8_xtime.high source · line 10 · raw

@+a:U32 -> @high:Bool -> U32

def gf8_xtime source · line 13 · raw

@+a:U32 -> U32

def gf8_mul.go source · line 16 · raw

@fuel:Nat -> @+a:U32 -> @+b:U32 -> @acc:U32 -> U32

def gf8_mul source · line 24 · raw

@a:U32 -> @b:U32 -> U32

def gf8_pow.go source · line 27 · raw

@fuel:Nat -> @+base:U32 -> @+exp:U32 -> @+acc:U32 -> U32

def gf8_pow source · line 34 · raw

@a:U32 -> @exp:U32 -> U32

def rotl8 source · line 37 · raw

@+a:U32 -> @+shift:Nat -> U32

def aes_sbox_algebraic source · line 40 · raw

@+x:U32 -> U32

def aes_sbox source · line 46 · raw

@+x:U32 -> U32

def aes_subword source · line 49 · raw

@+w:U32 -> U32

def aes_rotword source · line 55 · raw

@+w:U32 -> U32

def aes_rcon_step source · line 58 · raw

@r:U32 -> U32

def aes_word source · line 61 · raw

@a:U32 -> @b:U32 -> @c:U32 -> @d:U32 -> U32

def aes_words source · line 65 · raw

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

def aes_word_from_maybe source · line 71 · raw

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

def aes_word_at source · line 76 · raw

@words:List<&2, U32> -> @i:Nat -> U32

def aes_key_word_kind.step source · line 79 · raw

@previous:U32 -> @rcon:U32 -> @mod4:Bool -> U32

def aes_key_word_kind.rcon source · line 84 · raw

@previous:U32 -> @rcon:U32 -> @mod4:Bool -> U32

def aes_key_word_kind source · line 87 · raw

@previous:U32 -> @rcon:U32 -> @mod0:Bool -> @mod4:Bool -> U32

def aes_rcon_kind source · line 92 · raw

@rcon:U32 -> @advance:Bool -> U32

def aes_expand.go source · line 97 · raw

@fuel:Nat -> @+i:U32 -> @+rcon:U32 -> @+words:List<&2, U32> -> List<&2, U32>

def aes256_expand_impl source · line 110 · raw

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

def aes_expand_key source · line 115 · raw

@+fuel:Nat -> @+key:List<&2, U32> -> List<&2, U32>

An abstract key remains neutral. The explicit fuel parameter also lets computation certificates compose without unfolding all 52 expansion steps.

def aes256_expand source · line 120 · raw

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

def aes_add_key.go source · line 123 · raw

@+state:List<&2, U32> -> @+words:List<&2, U32> -> @+round:Nat -> @+index:Nat -> @fuel:Nat -> @acc:List<&2, U32> -> List<&2, U32>

def aes_add_key source · line 137 · raw

@state:List<&2, U32> -> @words:List<&2, U32> -> @round:Nat -> List<&2, U32>

def aes_sub_state.go source · line 140 · raw

@+state:List<&2, U32> -> @+acc:List<&2, U32> -> List<&2, U32>

def aes_sub_state source · line 146 · raw

@state:List<&2, U32> -> List<&2, U32>

def aes_byte_from_maybe source · line 149 · raw

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

def aes_byte_at source · line 154 · raw

@state:List<&2, U32> -> @index:Nat -> U32

def aes_shift_rows source · line 157 · raw

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

def aes_mix_column source · line 166 · raw

@col:AesColumn -> AesColumn

def aes_mix_column.first source · line 175 · raw

@col:AesColumn -> U32

def aes_mix_column.second source · line 180 · raw

@col:AesColumn -> U32

def aes_mix_column.third source · line 185 · raw

@col:AesColumn -> U32

def aes_mix_column.fourth source · line 190 · raw

@col:AesColumn -> U32

def aes_mix_row source · line 195 · raw

@col:AesColumn -> @row:Nat -> U32

def aes_mix_byte source · line 202 · raw

@+state:List<&2, U32> -> @row:Nat -> @+col:Nat -> U32

def aes_mix_state.finish source · line 210 · raw

@col0:AesColumn -> @col1:AesColumn -> @col2:AesColumn -> @col3:AesColumn -> List<&2, U32>

def aes_mix_state source · line 215 · raw

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

def aes_middle_round source · line 223 · raw

@state:List<&2, U32> -> @words:List<&2, U32> -> @round:Nat -> List<&2, U32>

def aes_final_round source · line 226 · raw

@state:List<&2, U32> -> @words:List<&2, U32> -> List<&2, U32>

def aes_rounds.go source · line 229 · raw

@fuel:Nat -> @+state:List<&2, U32> -> @+words:List<&2, U32> -> @+round:Nat -> List<&2, U32>

def aes256_encrypt_expanded source · line 235 · raw

@+words:List<&2, U32> -> @block:List<&2, U32> -> List<&2, U32>

def aes256_encrypt_block source · line 240 · raw

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

def gcm_hex_mask source · line 244 · raw

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

GCM counter mode and GHASH use 16-byte blocks in network byte order.

def gcm_mask_byte_valid source · line 247 · raw

@+value:U32 -> {U32.is_lt(gcm_hex_mask(value, 255), 256) == True{} : Bool}

def gcm_bytes_valid source · line 252 · raw

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

def gcm_mask_bytes source · line 258 · raw

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

def gcm_mask_bytes_valid source · line 264 · raw

@+bytes:List<&2, U32> -> {gcm_bytes_valid(gcm_mask_bytes(bytes)) == True{} : Bool}

def gcm_mask_bytes_length source · line 282 · raw

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

def gcm_ciphertext_bytes source · line 306 · raw

@ciphertext:GcmCiphertext -> List<&2, U32>

def ghash_xor_if source · line 311 · raw

@a:U32 -> @b:U32 -> @yes:Bool -> U32

def ghash_xor_list.go source · line 316 · raw

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

def ghash_xor_list source · line 324 · raw

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

def ghash_field source · line 331 · raw

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

def ghash_field_bytes source · line 336 · raw

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

def ghash_field_word source · line 348 · raw

@value:GhashField -> @index:Nat -> U32

def ghash_field_shift_top source · line 355 · raw

@w0:U32 -> @reduce:Bool -> U32

def ghash_field_shift_right source · line 359 · raw

@value:GhashField -> GhashField

def ghash_field_xor_if source · line 368 · raw

@a:U32 -> @b:U32 -> @yes:Bool -> U32

def ghash_field_xor_if.all source · line 372 · raw

@a:GhashField -> @b:GhashField -> @+yes:Bool -> GhashField

def ghash_mul.go source · line 378 · raw

@fuel:Nat -> @+x:GhashField -> @+v:GhashField -> @+z:GhashField -> @+bit_index:Nat -> GhashField

def ghash_mul source · line 389 · raw

@x:List<&2, U32> -> @h:List<&2, U32> -> List<&2, U32>

def ghash_update source · line 393 · raw

@y:List<&2, U32> -> @h:List<&2, U32> -> @block:List<&2, U32> -> List<&2, U32>

def ghash_zero_pad.go source · line 396 · raw

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

def ghash_finish source · line 401 · raw

@space:Nat -> @block_rev:List<&2, U32> -> @h:List<&2, U32> -> @y:List<&2, U32> -> List<&2, U32>

def ghash_bytes.go source · line 408 · raw

@fuel:Nat -> @bytes:List<&2, U32> -> @space:Nat -> @+block_rev:List<&2, U32> -> @+h:List<&2, U32> -> @+y:List<&2, U32> -> List<&2, U32>

def ghash_bytes source · line 420 · raw

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

def ghash_nat_bytes.go source · line 423 · raw

@fuel:Nat -> @qr:Pair(Nat, Nat) -> @+acc:List<&2, U32> -> List<&2, U32>

def ghash_nat_bytes source · line 430 · raw

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

def ghash_auth_with_hash_impl source · line 433 · raw

@+h:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> List<&2, U32>

def ghash_auth_with_hash source · line 442 · raw

@+h:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> List<&2, U32>

Do not expand a symbolic GHASH multiplication while transporting its hash.

def ghash_auth_expanded source · line 447 · raw

@words:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> List<&2, U32>

def gcm_j0 source · line 451 · raw

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

def gcm_inc32 source · line 454 · raw

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

def gcm_ctr_stream.go source · line 464 · raw

@fuel:Nat -> @+words:List<&2, U32> -> @+counter:List<&2, U32> -> @+acc:List<&2, U32> -> List<&2, U32>

def gcm_ctr_advance source · line 473 · raw

@fuel:Nat -> @+counter:List<&2, U32> -> List<&2, U32>

def gcm_ctr_step source · line 481 · raw

@+words:List<&2, U32> -> @+counter:List<&2, U32> -> @block:List<&2, U32> -> GcmCtrStep

def gcm_ctr_step_byte source · line 490 · raw

@step:GcmCtrStep -> U32

def gcm_ctr_step_counter source · line 494 · raw

@step:GcmCtrStep -> List<&2, U32>

def gcm_ctr_step_rest source · line 498 · raw

@step:GcmCtrStep -> List<&2, U32>

def gcm_ctr_stream_exact.go source · line 504 · raw

@fuel:Nat -> @+words:List<&2, U32> -> @counter:List<&2, U32> -> @block:List<&2, U32> -> List<&2, U32>

Generate each AES counter block once and consume all of its bytes. Fuel is still a byte count, so partial final blocks have exactly the requested length.

def gcm_ctr_stream_exact source · line 514 · raw

@fuel:Nat -> @+words:List<&2, U32> -> @+start:List<&2, U32> -> List<&2, U32>

def gcm_zip_xor source · line 518 · raw

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

def gcm_zip_xor_nil_left source · line 526 · raw

@+stream:List<&2, U32> -> {gcm_zip_xor([], stream) == [] : List<&2, U32>}

def gcm_zip_xor_nil_right source · line 532 · raw

@+bytes:List<&2, U32> -> {gcm_zip_xor(bytes, []) == [] : List<&2, U32>}

def gcm_zip_xor_valid source · line 538 · raw

@+bytes:List<&2, U32> -> @+stream:List<&2, U32> -> {gcm_bytes_valid(gcm_zip_xor(bytes, stream)) == True{} : Bool}

def gcm_tag_parts source · line 581 · raw

@+auth:List<&2, U32> -> @+mask:List<&2, U32> -> List<&2, U32>

A GCM tag is exactly sixteen bytes. Expose that shape without unfolding abstract AES rounds or GHASH values when checking its certificates.

def gcm_tag_output_impl source · line 599 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> GcmTag

def gcm_tag_output source · line 608 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> GcmTag

Keep an abstract key schedule abstract during proof normalization. Splitting on the nonce leaves the key schedule abstract in both identical branches.

def gcm_tag_bytes source · line 614 · raw

@tag_output:GcmTag -> List<&2, U32>

def gcm_tag_valid source · line 618 · raw

@tag_output:GcmTag -> {gcm_bytes_valid(gcm_tag_bytes(tag_output)) == True{} : Bool}

def gcm_tag_size source · line 623 · raw

@tag_output:GcmTag -> {List.length(&2, U32, gcm_tag_bytes(tag_output)) == 16n : Nat}

def gcm_output_tag_bytes source · line 643 · raw

@output:GcmOutput -> List<&2, U32>

def gcm_output_tag_valid source · line 649 · raw

@output:GcmOutput -> {gcm_bytes_valid(gcm_output_tag_bytes(output)) == True{} : Bool}

def gcm_output_tag_size source · line 656 · raw

@output:GcmOutput -> {List.length(&2, U32, gcm_output_tag_bytes(output)) == 16n : Nat}

def gcm_output_from_tag source · line 663 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @ciphertext_valid:{gcm_bytes_valid(ciphertext) == True{} : Bool} -> GcmOutput

def gcm_output_from_ciphertext source · line 672 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @cipher_output:GcmCiphertext -> GcmOutput

def gcm_ctr_encrypt source · line 679 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @+plaintext:List<&2, U32> -> GcmCiphertext

def gcm_encrypt_raw source · line 687 · raw

@+key:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> GcmOutput

def gcm_decrypt_expanded source · line 693 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @+ciphertext:List<&2, U32> -> List<&2, U32>

def gcm_decrypt_raw source · line 699 · raw

@+key:List<&2, U32> -> @nonce:List<&2, U32> -> @+ciphertext:List<&2, U32> -> List<&2, U32>

def gcm_tag_expanded source · line 703 · raw

@+words:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> List<&2, U32>

Authenticate ciphertext directly; expand the key once for both AES calls.

def gcm_tag source · line 706 · raw

@+key:List<&2, U32> -> @nonce:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> List<&2, U32>

def ghash_auth source · line 709 · raw

@key:List<&2, U32> -> @aad:List<&2, U32> -> @ciphertext:List<&2, U32> -> List<&2, U32>