proofs/crypto/aes/aead.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead

10 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ../../../spec/crypto/subtle.bend as Eq
import ../subtle/laws.bend as EqLaws
import ../subtle/proof.bend as EqProof

Definitions

def bxor_inv source · line 19 · raw

@+x:Bool -> @+y:Bool -> {Bool.xor(Bool.xor(x, y), y) == x : Bool}

def word_xor_inv source · line 30 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}

def xor_inv source · line 39 · raw

@+x:U32 -> @+k:U32 -> {U32.xor(U32.xor(x, k), k) == x : U32}

def ks_ok source · line 44 · raw

@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st) == [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 3n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 4n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 5n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 6n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 7n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 8n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 9n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 10n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 11n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 12n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 13n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 14n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st), 15n)] : List<&2, U32>}

def kb source · line 50 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+cb:List<&2, U32> -> @+i:Nat -> U32

Byte i of the keystream block of counter block cb.

def cancel16 source · line 54 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> @+k11:U32 -> @+k12:U32 -> @+k13:U32 -> @+k14:U32 -> @+k15:U32 -> @+r1:List<&2, U32> -> @+r2:List<&2, U32> -> @+e:{r1 == r2 : List<&2, U32>} -> {U32.xor(U32.xor(x0, k0), k0) <> U32.xor(U32.xor(x1, k1), k1) <> U32.xor(U32.xor(x2, k2), k2) <> U32.xor(U32.xor(x3, k3), k3) <> U32.xor(U32.xor(x4, k4), k4) <> U32.xor(U32.xor(x5, k5), k5) <> U32.xor(U32.xor(x6, k6), k6) <> U32.xor(U32.xor(x7, k7), k7) <> U32.xor(U32.xor(x8, k8), k8) <> U32.xor(U32.xor(x9, k9), k9) <> U32.xor(U32.xor(x10, k10), k10) <> U32.xor(U32.xor(x11, k11), k11) <> U32.xor(U32.xor(x12, k12), k12) <> U32.xor(U32.xor(x13, k13), k13) <> U32.xor(U32.xor(x14, k14), k14) <> U32.xor(U32.xor(x15, k15), k15) <> r1 == x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> r2 : List<&2, U32>}

(x xor k) xor k == x, position by position.

def cancel1 source · line 74 · raw

@+x0:U32 -> @+k0:U32 -> {[U32.xor(U32.xor(x0, k0), k0)] == [x0] : List<&2, U32>}

def cancel2 source · line 78 · raw

@+x0:U32 -> @+x1:U32 -> @+k0:U32 -> @+k1:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1)] == [x0, x1] : List<&2, U32>}

def cancel3 source · line 83 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2)] == [x0, x1, x2] : List<&2, U32>}

def cancel4 source · line 89 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3)] == [x0, x1, x2, x3] : List<&2, U32>}

def cancel5 source · line 96 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4)] == [x0, x1, x2, x3, x4] : List<&2, U32>}

def cancel6 source · line 104 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5)] == [x0, x1, x2, x3, x4, x5] : List<&2, U32>}

def cancel7 source · line 113 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6)] == [x0, x1, x2, x3, x4, x5, x6] : List<&2, U32>}

def cancel8 source · line 123 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7)] == [x0, x1, x2, x3, x4, x5, x6, x7] : List<&2, U32>}

def cancel9 source · line 134 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8] : List<&2, U32>}

def cancel10 source · line 146 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] : List<&2, U32>}

def cancel11 source · line 159 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] : List<&2, U32>}

def cancel12 source · line 173 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> @+k11:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] : List<&2, U32>}

def cancel13 source · line 188 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> @+k11:U32 -> @+k12:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11), U32.xor(U32.xor(x12, k12), k12)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] : List<&2, U32>}

def cancel14 source · line 204 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> @+k11:U32 -> @+k12:U32 -> @+k13:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11), U32.xor(U32.xor(x12, k12), k12), U32.xor(U32.xor(x13, k13), k13)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] : List<&2, U32>}

def cancel15 source · line 221 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+k0:U32 -> @+k1:U32 -> @+k2:U32 -> @+k3:U32 -> @+k4:U32 -> @+k5:U32 -> @+k6:U32 -> @+k7:U32 -> @+k8:U32 -> @+k9:U32 -> @+k10:U32 -> @+k11:U32 -> @+k12:U32 -> @+k13:U32 -> @+k14:U32 -> {[U32.xor(U32.xor(x0, k0), k0), U32.xor(U32.xor(x1, k1), k1), U32.xor(U32.xor(x2, k2), k2), U32.xor(U32.xor(x3, k3), k3), U32.xor(U32.xor(x4, k4), k4), U32.xor(U32.xor(x5, k5), k5), U32.xor(U32.xor(x6, k6), k6), U32.xor(U32.xor(x7, k7), k7), U32.xor(U32.xor(x8, k8), k8), U32.xor(U32.xor(x9, k9), k9), U32.xor(U32.xor(x10, k10), k10), U32.xor(U32.xor(x11, k11), k11), U32.xor(U32.xor(x12, k12), k12), U32.xor(U32.xor(x13, k13), k13), U32.xor(U32.xor(x14, k14), k14)] == [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] : List<&2, U32>}

def gctr_block source · line 240 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> @+rest:List<&2, U32> -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> rest, cb) == U32.xor(x0, kb(nk, nr, key, cb, 0n)) <> U32.xor(x1, kb(nk, nr, key, cb, 1n)) <> U32.xor(x2, kb(nk, nr, key, cb, 2n)) <> U32.xor(x3, kb(nk, nr, key, cb, 3n)) <> U32.xor(x4, kb(nk, nr, key, cb, 4n)) <> U32.xor(x5, kb(nk, nr, key, cb, 5n)) <> U32.xor(x6, kb(nk, nr, key, cb, 6n)) <> U32.xor(x7, kb(nk, nr, key, cb, 7n)) <> U32.xor(x8, kb(nk, nr, key, cb, 8n)) <> U32.xor(x9, kb(nk, nr, key, cb, 9n)) <> U32.xor(x10, kb(nk, nr, key, cb, 10n)) <> U32.xor(x11, kb(nk, nr, key, cb, 11n)) <> U32.xor(x12, kb(nk, nr, key, cb, 12n)) <> U32.xor(x13, kb(nk, nr, key, cb, 13n)) <> U32.xor(x14, kb(nk, nr, key, cb, 14n)) <> U32.xor(x15, kb(nk, nr, key, cb, 15n)) <> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, rest, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.inc32(cb)) : List<&2, U32>}

One whole block of counter mode.

def gctr_part1 source · line 244 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n))] : List<&2, U32>}

def gctr_part2 source · line 248 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n))] : List<&2, U32>}

def gctr_part3 source · line 252 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n))] : List<&2, U32>}

def gctr_part4 source · line 256 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n))] : List<&2, U32>}

def gctr_part5 source · line 260 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n))] : List<&2, U32>}

def gctr_part6 source · line 264 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n))] : List<&2, U32>}

def gctr_part7 source · line 268 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n))] : List<&2, U32>}

def gctr_part8 source · line 272 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n))] : List<&2, U32>}

def gctr_part9 source · line 276 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n))] : List<&2, U32>}

def gctr_part10 source · line 280 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n))] : List<&2, U32>}

def gctr_part11 source · line 284 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))] : List<&2, U32>}

def gctr_part12 source · line 288 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n))] : List<&2, U32>}

def gctr_part13 source · line 292 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n))] : List<&2, U32>}

def gctr_part14 source · line 296 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n))] : List<&2, U32>}

def gctr_part15 source · line 300 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n)), U32.xor(x11, kb(nk, nr, key, cb, 11n)), U32.xor(x12, kb(nk, nr, key, cb, 12n)), U32.xor(x13, kb(nk, nr, key, cb, 13n)), U32.xor(x14, kb(nk, nr, key, cb, 14n))] : List<&2, U32>}

def gctr_inv source · line 305 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+xs:List<&2, U32> -> @+cb:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.gctr(nk, nr, key, xs, cb), cb) == xs : List<&2, U32>}

Counter mode is an involution (the keystream is XORed twice).

def bb16 source · line 374 · raw

@+w:Word(128n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w) == [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 0n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 2n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 3n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 4n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 5n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 6n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 7n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 8n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 9n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 10n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 11n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 12n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 13n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 14n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.nth_byte(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(w), 15n)] : List<&2, U32>}

def hb source · line 380 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> List<&2, U32>

The GHASH block of the tag, as bytes, and byte i of the tag.

def tb source · line 383 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+i:Nat -> U32

def tag16 source · line 387 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.tag(nk, nr, key, iv, aad, c) == [tb(nk, nr, key, iv, aad, c, 0n), tb(nk, nr, key, iv, aad, c, 1n), tb(nk, nr, key, iv, aad, c, 2n), tb(nk, nr, key, iv, aad, c, 3n), tb(nk, nr, key, iv, aad, c, 4n), tb(nk, nr, key, iv, aad, c, 5n), tb(nk, nr, key, iv, aad, c, 6n), tb(nk, nr, key, iv, aad, c, 7n), tb(nk, nr, key, iv, aad, c, 8n), tb(nk, nr, key, iv, aad, c, 9n), tb(nk, nr, key, iv, aad, c, 10n), tb(nk, nr, key, iv, aad, c, 11n), tb(nk, nr, key, iv, aad, c, 12n), tb(nk, nr, key, iv, aad, c, 13n), tb(nk, nr, key, iv, aad, c, 14n), tb(nk, nr, key, iv, aad, c, 15n)] : List<&2, U32>}

The tag is a 16-byte list.

def not_short source · line 393 · raw

@+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> {Nat.is_lt(List.length(&2, U32, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), 16n) == False{} : Bool}

Splitting C || T (T of 16 bytes) back into C and T.

def sub16 source · line 403 · raw

@+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> {Nat.sub(List.length(&2, U32, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])), 16n) == List.length(&2, U32, c) : Nat}

def take_app source · line 412 · raw

@+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> {List.take(&2, U32, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15]), List.length(&2, U32, c)) == c : List<&2, U32>}

def drop_app source · line 420 · raw

@+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> {List.drop(&2, U32, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15]), List.length(&2, U32, c)) == [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] : List<&2, U32>}

def open_append source · line 427 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open_checked(nk, nr, key, iv, aad, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15]) : Maybe<&2, List<&2, U32>>}

def equal_refl source · line 434 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(xs, xs) == True{} : Bool}

def false_of source · line 437 · raw

@+b:Bool -> @f:(@_:{b == True{} : Bool} -> Empty) -> {b == False{} : Bool}

def equal_false source · line 444 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @ne:(@_:{a == b : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(a, b) == False{} : Bool}

def roundtrip source · line 448 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+pt:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, aad, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.seal(nk, nr, key, iv, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}

Opening what seal produced gives the plaintext back.

def forgery source · line 457 · raw

@+nk:Nat -> @+nr:Nat -> @+key:List<&2, U32> -> @+iv:List<&2, U32> -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> @+t0:U32 -> @+t1:U32 -> @+t2:U32 -> @+t3:U32 -> @+t4:U32 -> @+t5:U32 -> @+t6:U32 -> @+t7:U32 -> @+t8:U32 -> @+t9:U32 -> @+t10:U32 -> @+t11:U32 -> @+t12:U32 -> @+t13:U32 -> @+t14:U32 -> @+t15:U32 -> @ne:(@_:{[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.tag(nk, nr, key, iv, aad, c) : List<&2, U32>} -> Empty) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.open(nk, nr, key, iv, aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}

Opening C || T with T other than the tag of C gives None.