proofs/crypto/argon2/run.bend checks

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

20 imports

import Base
import ../../../spec/lib/common.bend as SC
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR2
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/argon2/types.bend as A
import ../../../src/crypto/argon2/blamka.bend as G
import ../../../src/crypto/argon2/memory.bend as M
import ../../../src/crypto/argon2/argon2.bend as I
import ../../../spec/crypto/argon2/blamka.bend as SG
import ../../../spec/crypto/argon2/argon2.bend as SA
import ./blamka.bend as BL
import ./memory.bend as MEM
import ./hash.bend as HS
import ./fill.bend as F

Definitions

def init_block_eq source · line 28 · raw

@+hh:List<&2, U32> -> @+i:Nat -> @+l:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.block_of(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hprime(1024n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.cat(hh, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.cat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.le32(i), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.le32(l))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.block_of(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hprime(1024n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.cat(hh, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.cat(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.le32(i), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.le32(l))))) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def init_len source · line 34 · raw

@+n:Nat -> @+l:Nat -> @+q:Nat -> @+hh:List<&2, U32> -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.init_go(n, l, q, hh, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def lt_first source · line 47 · raw

@+l:Nat -> @+p:Nat -> @+q:Nat -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hq2:{Nat.is_le(2n, q) == True{} : Bool} -> {Nat.is_lt(Nat.mul(l, q), Nat.mul(p, q)) == True{} : Bool}

def lt_second source · line 50 · raw

@+l:Nat -> @+p:Nat -> @+q:Nat -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hq2:{Nat.is_le(2n, q) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.mul(l, q), 1n), Nat.mul(p, q)) == True{} : Bool}

def init_eq source · line 54 · raw

@+d:Nat -> @+n:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+hh:List<&2, U32> -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hc:{Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) == Nat.mul(p, q) : Nat} -> @+hq2:{Nat.is_le(2n, q) == True{} : Bool} -> @+hln:{Nat.is_le(Nat.add(l, n), p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.init_go(n, l, q, hh, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, mem))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.init_go(n, l, q, hh, mem))) : Array<U32>}

B[l][0] and B[l][1] for the lanes l .. l + n - 1.

def final_eq source · line 80 · raw

@+d:Nat -> @+n:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hc:{Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) == Nat.mul(p, q) : Nat} -> @+hq1:{Nat.is_le(1n, q) == True{} : Bool} -> @+hln:{Nat.is_lt(Nat.add(l, n), p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.final_go(n, l, q, c, (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, mem)), b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.final_go(n, l, q, c, b, mem) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

C = B[l][q-1] XOR .. for the lanes l .. l + n (b is B[l][q-1]).