~/bend-docscommunity

proofs/crypto/aes/gf.bend checks

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

4 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/crypto/aes/poly.bend as P

Definitions

def bxor_false source · line 14 · raw

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

def bxor_comm source · line 21 · raw

@+a:Bool -> @+b:Bool -> {Bool.xor(a, b) == Bool.xor(b, a) : Bool}

def bxor_assoc source · line 32 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}

def bxor_self source · line 51 · raw

@+a:Bool -> {Bool.xor(a, a) == False{} : Bool}

def bswap4 source · line 58 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> @+d:Bool -> {Bool.xor(Bool.xor(a, b), Bool.xor(c, d)) == Bool.xor(Bool.xor(a, c), Bool.xor(b, d)) : Bool}

def xor_zero_l source · line 95 · raw

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

def xor_zero_r source · line 103 · raw

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

def xor_self source · line 112 · raw

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

def xor_assoc source · line 121 · raw

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

def xor_swap4 source · line 130 · raw

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

def put_xor source · line 139 · raw

@+p:Nat -> @+c:Bool -> @+d:Bool -> @+s:Word(p) -> @+t:Word(p) -> {Word.shl.put(p, Bool.xor(c, d), Word.xor(p, s, t)) == Word.xor(p, Word.shl.put(p, c, s), Word.shl.put(p, d, t)) : Word(p)}

def shl_xor source · line 147 · raw

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

def top_xor source · line 155 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.top(n, Word.xor(n, a, b)) == Bool.xor(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.top(n, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.top(n, b)) : Bool}

def top_zero source · line 164 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.top(n, Word.zero(n)) == False{} : Bool}

def put_zero source · line 173 · raw

@+p:Nat -> {Word.shl.put(p, False{}, Word.zero(p)) == Word.zero(p) : Word(p)}

def shl_zero source · line 181 · raw

@+n:Nat -> {Word.shl(n, Word.zero(n)) == Word.zero(n) : Word(n)}

def wscale_xor source · line 189 · raw

@+n:Nat -> @+c:Bool -> @+d:Bool -> @+w:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, Bool.xor(c, d), w) == Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, c, w), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, d, w)) : Word(n)}

def tx_xor source · line 202 · raw

@+n:Nat -> @+low:Word(n) -> @+a:Word(n) -> @+b:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, Word.xor(n, a, b)) == Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, b)) : Word(n)}

def tx_zero source · line 208 · raw

@+n:Nat -> @+low:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, Word.zero(n)) == Word.zero(n) : Word(n)}

def tx_wscale source · line 213 · raw

@+n:Nat -> @+low:Word(n) -> @+c:Bool -> @+v:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, c, v)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, c, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, v)) : Word(n)}

def constant_xor source · line 222 · raw

@+n:Nat -> @+c:Bool -> @+d:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.constant(n, Bool.xor(c, d)) == Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.constant(n, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.constant(n, d)) : Word(n)}

def red_add source · line 230 · raw

@+n:Nat -> @+low:Word(n) -> @+p:List<&2, Bool> -> @+q:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.add(p, q)) == Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, p), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, q)) : Word(n)}

def scale_true source · line 242 · raw

@+b:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.scale(True{}, b) == b : List<&2, Bool>}

def constant_false_xor source · line 250 · raw

@+n:Nat -> {Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.constant(n, False{}), Word.zero(n)) == Word.zero(n) : Word(n)}

def red_scale_false source · line 257 · raw

@+n:Nat -> @+low:Word(n) -> @+b:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.scale(False{}, b)) == Word.zero(n) : Word(n)}

def red_scale source · line 266 · raw

@+n:Nat -> @+low:Word(n) -> @+c:Bool -> @+b:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.scale(c, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.wscale(n, c, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, b)) : Word(n)}

def constant_false_l source · line 274 · raw

@+n:Nat -> @+w:Word(n) -> {Word.xor(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.constant(n, False{}), w) == w : Word(n)}

def red_shift source · line 283 · raw

@+n:Nat -> @+low:Word(n) -> @+p:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, False{} <> p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, p)) : Word(n)}

def sm source · line 289 · raw

@+n:Nat -> @+low:Word(n) -> @a:List<&2, Bool> -> @+v:Word(n) -> Word(n)

sum over the set coefficients a_i of v * x^i (mod m)

def sa source · line 297 · raw

@+n:Nat -> @+low:Word(n) -> @a:List<&2, Bool> -> @z:Word(n) -> @+v:Word(n) -> Word(n)

Algorithm 1 of SP 800-38D: Z ^= a_i ? V : 0, V = V * x.

def tx_sm source · line 304 · raw

@+n:Nat -> @+low:Word(n) -> @+a:List<&2, Bool> -> @+v:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, sm(n, low, a, v)) == sm(n, low, a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.times_x(n, low, v)) : Word(n)}

def red_mul source · line 313 · raw

@+n:Nat -> @+low:Word(n) -> @+a:List<&2, Bool> -> @+b:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.mul(a, b)) == sm(n, low, a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, b)) : Word(n)}

def sa_sm source · line 324 · raw

@+n:Nat -> @+low:Word(n) -> @+a:List<&2, Bool> -> @+z:Word(n) -> @+v:Word(n) -> {sa(n, low, a, z, v) == Word.xor(n, z, sm(n, low, a, v)) : Word(n)}

def wof source · line 335 · raw

@n:Nat -> @bs:List<&2, Bool> -> Word(n)

The first n coefficients of a list, zero-filled.

def wof_nil source · line 344 · raw

@+n:Nat -> {Word.zero(n) == wof(n, []) : Word(n)}

def wof_false_nil source · line 352 · raw

@+q:Nat -> {wof(q, [False{}]) == wof(q, []) : Word(q)}

def put_wof source · line 359 · raw

@+p:Nat -> @+c:Bool -> @+l:List<&2, Bool> -> {Word.shl.put(p, c, wof(p, l)) == wof(p, c <> l) : Word(p)}

def shl_wof source · line 371 · raw

@+n:Nat -> @+l:List<&2, Bool> -> {Word.shl(n, wof(n, l)) == wof(n, False{} <> l) : Word(n)}

def top_short source · line 383 · raw

@+p:Nat -> @+l:List<&2, Bool> -> @+h:{Nat.is_le(List.length(&2, Bool, l), p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.top(1n+p, wof(1n+p, l)) == False{} : Bool}

def red_short source · line 394 · raw

@+n:Nat -> @+low:Word(n) -> @+l:List<&2, Bool> -> @+h:{Nat.is_le(List.length(&2, Bool, l), n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, l) == wof(n, l) : Word(n)}

def wof_coefficients source · line 410 · raw

@+n:Nat -> @+w:Word(n) -> {wof(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, w)) == w : Word(n)}

def coefficients_le source · line 418 · raw

@+n:Nat -> @+w:Word(n) -> {Nat.is_le(List.length(&2, Bool, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, w)), n) == True{} : Bool}

def red_coefficients source · line 425 · raw

@+n:Nat -> @+low:Word(n) -> @+w:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, w)) == w : Word(n)}

def mul_sa source · line 430 · raw

@+n:Nat -> @+low:Word(n) -> @+a:Word(n) -> @+b:Word(n) -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.reduce(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, b))) == sa(n, low, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.coefficients(n, a), Word.zero(n), b) : Word(n)}

The product of two residues, reduced, is Algorithm 1 from Z = 0.