proofs/crypto/aes/ghash_bits.bend checks

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

7 imports

import Base
import ../../../src/crypto/aes/types.bend as T
import ../../../src/crypto/aes/gcm.bend as I
import ../../../spec/crypto/aes/poly.bend as P
import ../../../spec/crypto/aes/aes.bend as S
import ../../../spec/crypto/aes/gcm.bend as G
import ./ghash_defs.bend as D

Definitions

def zstep_ok source · line 12 · raw

@+c:Bool -> @+z:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.add_masked(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.bit(c), z, v)) == Word.xor(128n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(128n, c, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(v))) : Word(128n)}

Z xor (V and (0 - bit)) is Z + c*V.

def mulx_w source · line 23 · raw

@+x0:Bool -> @+y0:Bool -> @+z0:Bool -> @+u0:Bool -> @+xt:Word(31n) -> @+yt:Word(31n) -> @+zt:Word(31n) -> @+ut:Word(31n) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.mulx(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(128n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.low, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.B{U32{WCon{x0, xt}}, U32{WCon{y0, yt}}, U32{WCon{z0, zt}}, U32{WCon{u0, ut}}})) : Word(128n)}

def mulx_ok source · line 91 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.mulx(v)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(128n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.low, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(v)) : Word(128n)}

V * x: the shift toward x^127 with the reduction by R.

def mul_byte_steps source · line 96 · raw

@+a:U32 -> @+acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.mul_byte(a, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.byte_bits(a), acc) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc}

def block_xor_ok source · line 101 · raw

@+y0:U32 -> @+y1:U32 -> @+y2:U32 -> @+y3: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 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(128n, Word.xor(128n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.B{y0, y1, y2, y3}), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.string_bits(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.xor_bytes(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.unpack(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) : List<&2, Bool>}

def or_false source · line 106 · raw

@+x:Bool -> {Bool.or(x, False{}) == x : Bool}

def u32_ext source · line 113 · raw

@+x_0:Bool -> @+x_1:Bool -> @+x_2:Bool -> @+x_3:Bool -> @+x_4:Bool -> @+x_5:Bool -> @+x_6:Bool -> @+x_7:Bool -> @+x_8:Bool -> @+x_9:Bool -> @+x_10:Bool -> @+x_11:Bool -> @+x_12:Bool -> @+x_13:Bool -> @+x_14:Bool -> @+x_15:Bool -> @+x_16:Bool -> @+x_17:Bool -> @+x_18:Bool -> @+x_19:Bool -> @+x_20:Bool -> @+x_21:Bool -> @+x_22:Bool -> @+x_23:Bool -> @+x_24:Bool -> @+x_25:Bool -> @+x_26:Bool -> @+x_27:Bool -> @+x_28:Bool -> @+x_29:Bool -> @+x_30:Bool -> @+x_31:Bool -> @+y_0:Bool -> @+y_1:Bool -> @+y_2:Bool -> @+y_3:Bool -> @+y_4:Bool -> @+y_5:Bool -> @+y_6:Bool -> @+y_7:Bool -> @+y_8:Bool -> @+y_9:Bool -> @+y_10:Bool -> @+y_11:Bool -> @+y_12:Bool -> @+y_13:Bool -> @+y_14:Bool -> @+y_15:Bool -> @+y_16:Bool -> @+y_17:Bool -> @+y_18:Bool -> @+y_19:Bool -> @+y_20:Bool -> @+y_21:Bool -> @+y_22:Bool -> @+y_23:Bool -> @+y_24:Bool -> @+y_25:Bool -> @+y_26:Bool -> @+y_27:Bool -> @+y_28:Bool -> @+y_29:Bool -> @+y_30:Bool -> @+y_31:Bool -> @+e0:{x_0 == y_0 : Bool} -> @+e1:{x_1 == y_1 : Bool} -> @+e2:{x_2 == y_2 : Bool} -> @+e3:{x_3 == y_3 : Bool} -> @+e4:{x_4 == y_4 : Bool} -> @+e5:{x_5 == y_5 : Bool} -> @+e6:{x_6 == y_6 : Bool} -> @+e7:{x_7 == y_7 : Bool} -> @+e8:{x_8 == y_8 : Bool} -> @+e9:{x_9 == y_9 : Bool} -> @+e10:{x_10 == y_10 : Bool} -> @+e11:{x_11 == y_11 : Bool} -> @+e12:{x_12 == y_12 : Bool} -> @+e13:{x_13 == y_13 : Bool} -> @+e14:{x_14 == y_14 : Bool} -> @+e15:{x_15 == y_15 : Bool} -> @+e16:{x_16 == y_16 : Bool} -> @+e17:{x_17 == y_17 : Bool} -> @+e18:{x_18 == y_18 : Bool} -> @+e19:{x_19 == y_19 : Bool} -> @+e20:{x_20 == y_20 : Bool} -> @+e21:{x_21 == y_21 : Bool} -> @+e22:{x_22 == y_22 : Bool} -> @+e23:{x_23 == y_23 : Bool} -> @+e24:{x_24 == y_24 : Bool} -> @+e25:{x_25 == y_25 : Bool} -> @+e26:{x_26 == y_26 : Bool} -> @+e27:{x_27 == y_27 : Bool} -> @+e28:{x_28 == y_28 : Bool} -> @+e29:{x_29 == y_29 : Bool} -> @+e30:{x_30 == y_30 : Bool} -> @+e31:{x_31 == y_31 : Bool} -> {U32{WCon{x_0, WCon{x_1, WCon{x_2, WCon{x_3, WCon{x_4, WCon{x_5, WCon{x_6, WCon{x_7, WCon{x_8, WCon{x_9, WCon{x_10, WCon{x_11, WCon{x_12, WCon{x_13, WCon{x_14, WCon{x_15, WCon{x_16, WCon{x_17, WCon{x_18, WCon{x_19, WCon{x_20, WCon{x_21, WCon{x_22, WCon{x_23, WCon{x_24, WCon{x_25, WCon{x_26, WCon{x_27, WCon{x_28, WCon{x_29, WCon{x_30, WCon{x_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{y_0, WCon{y_1, WCon{y_2, WCon{y_3, WCon{y_4, WCon{y_5, WCon{y_6, WCon{y_7, WCon{y_8, WCon{y_9, WCon{y_10, WCon{y_11, WCon{y_12, WCon{y_13, WCon{y_14, WCon{y_15, WCon{y_16, WCon{y_17, WCon{y_18, WCon{y_19, WCon{y_20, WCon{y_21, WCon{y_22, WCon{y_23, WCon{y_24, WCon{y_25, WCon{y_26, WCon{y_27, WCon{y_28, WCon{y_29, WCon{y_30, WCon{y_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}

def word_ok source · line 149 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @+d:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.word(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.W{a, b, c, d}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(a, b, c, d) : U32}

The implementation packs four bytes into a big-endian word.

def pack_int source · line 154 · raw

@+a0:U32 -> @+a1:U32 -> @+a2:U32 -> @+a3:U32 -> @+a4:U32 -> @+a5:U32 -> @+a6:U32 -> @+a7:U32 -> @+a8:U32 -> @+a9:U32 -> @+a10:U32 -> @+a11:U32 -> @+a12:U32 -> @+a13:U32 -> @+a14:U32 -> @+a15:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.B{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(a0, a1, a2, a3), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(a4, a5, a6, a7), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(a8, a9, a10, a11), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(a12, a13, a14, a15)}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}

def bb_ok source · line 159 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block_bytes(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(s)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.unpack(s) : List<&2, U32>}

def int32_ctr source · line 164 · raw

@+c:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.int32(U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)) == c : U32}

def str32_ctr source · line 169 · raw

@+c:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.str32(c) == [U32.and(255, U32.shrn(c, 24n)), U32.and(255, U32.shrn(c, 16n)), U32.and(255, U32.shrn(c, 8n)), U32.and(255, c)] : List<&2, U32>}