~/bend-docscommunity

proofs/crypto/argon2/gb.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as Gb

13 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../math/typed/w64mul.bend as W64M
import ./words.bend as LW
import ../../math/typed/width.bend as WW
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/blake/blake2b/lane.bend as L
import ../../../src/crypto/argon2/blamka.bend as I
import ../../../spec/crypto/blake/blake2b.bend as B
import ../../../spec/crypto/argon2/blamka.bend as S

Definitions

def rt source · line 27 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.of_nat(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(x)) == x : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

Every U64 is the U64 of its value.

def mul32_of source · line 37 · raw

@+a:U32 -> @+b:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul32(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.of_nat(Nat.mul(U32.to_nat(a), U32.to_nat(b))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64}

mul32(a, b) is the U64 of a * b.

def prod_correct source · line 43 · raw

@+a:U32 -> @+b:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.prod(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.lane_of(Nat.mul(U32.to_nat(a), U32.to_nat(b))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

The implementation's product lane is the specification's.

def bla_correct source · line 47 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.bla(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.fBlaMka(x, y) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

fBlaMka

def rx32 source · line 55 · raw

@+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.rot32(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.xor(d, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.rotr(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.xor(d, a), 32n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

The rotations of XORs, lane by lane.

def rx24 source · line 60 · raw

@+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.rot24(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.xor(d, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.rotr(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.xor(d, a), 24n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def rx16 source · line 65 · raw

@+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.rot16(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.xor(d, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.rotr(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.xor(d, a), 16n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def rx63 source · line 70 · raw

@+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.rot63(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.xor(d, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.rotr(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.xor(d, a), 63n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def m4 source · line 76 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

The specification's GB after its first k assignment pairs.

def m3 source · line 79 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

def m2 source · line 83 · raw

@+a1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

def m1 source · line 87 · raw

@+a1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad

def gb4_correct source · line 91 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb4(a2, b1, c2, d2) == m4(a2, b1, c2, d2) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

def gb3_correct source · line 94 · raw

@+a2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb3(a2, b1, c1, d1) == m3(a2, b1, c1, d1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

def gb2_correct source · line 103 · raw

@+a1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb2(a1, b, c1, d1) == m2(a1, b, c1, d1) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

def gb1_correct source · line 112 · raw

@+a1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb1(a1, b, c, d) == m1(a1, b, c, d) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

def gb_correct source · line 122 · raw

@+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.gb(a, b, c, d) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.GB(a, b, c, d) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Quad}

GB: the implementation's equals the specification's.