~/bend-docscommunity

proofs/crypto/argon2/index.bend checks

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

19 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 ../../lib/u32.bend as U
import ../../lib/logic.bend as L
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/argon2/types.bend as A
import ../../../src/crypto/argon2/blamka.bend as G
import ../../../src/crypto/argon2/argon2.bend as I
import ../../../spec/crypto/blake/blake2b.bend as B
import ../../../spec/crypto/argon2/blamka.bend as SG
import ../../../spec/crypto/argon2/argon2.bend as SA
import ./gb.bend as GB
import ./blamka.bend as BL

Definitions

def row_at_eq source · line 28 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+i:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.row_at(b, i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.row(b, i) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State}

def at_eq source · line 47 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+j:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.at(v, j) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.at(v, j) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def lane_eq source · line 84 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.lane(b, n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.lane(b, n) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def pick_eq source · line 89 · raw

@+indep:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+idx:Nat -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.pick(indep, addr, idx, prev) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.pick(indep, addr, idx, prev) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane}

def hi_eq source · line 96 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hi(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hi(x) : U32}

def lo_eq source · line 101 · raw

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

def ref_lane_eq source · line 108 · raw

@+forced:Bool -> @+l:Nat -> @+j2:U32 -> @+p:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.ref_lane(forced, l, j2, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.ref_lane(forced, l, j2, p) : Nat}

def area_base_eq source · line 115 · raw

@+r0:Bool -> @+s:Nat -> @+sl:Nat -> @+q:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.area_base(r0, s, sl, q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area_base(r0, s, sl, q) : Nat}

def area_other_eq source · line 122 · raw

@+base:Nat -> @+zero:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.area_other(base, zero) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area_other(base, zero) : Nat}

def area_eq source · line 129 · raw

@+base:Nat -> @+idx:Nat -> @+same:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.area(base, idx, same) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area(base, idx, same) : Nat}

def start_last_eq source · line 136 · raw

@+s:Nat -> @+sl:Nat -> @+last:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.start_last(s, sl, last) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.start_last(s, sl, last) : Nat}

def start_eq source · line 143 · raw

@+r0:Bool -> @+s:Nat -> @+sl:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.start(r0, s, sl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.start(r0, s, sl) : Nat}

def prev_index_eq source · line 150 · raw

@+l:Nat -> @+q:Nat -> @+j:Nat -> @+first:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.prev_index(l, q, j, first) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.prev_index(l, q, j, first) : Nat}

def start_index_eq source · line 157 · raw

@+first:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.start_index(first) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.start_index(first) : Nat}

def fits_value source · line 164 · raw

@+x:0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.value(x)) == True{} : Bool}

def hi_mul source · line 172 · raw

@+a:U32 -> @+b:U32 -> {U32.to_nat(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.hi(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.mul32(a, b))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}

The high word of mul32(a, b) is a * b div 2^32.

def rel_eq source · line 180 · raw

@+w:Nat -> @+j1:U32 -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hw:{Nat.is_lt(w, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.rel(w, j1) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rel(w, j1) : Nat}

rel: |W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32, for |W| < 2^k with k <= 32.

def input_eq source · line 192 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.input_block(r, l, s, mm, t, ctr) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.input_block(r, l, s, mm, t, ctr) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def addresses_eq source · line 199 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+ctr:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.addresses(r, l, s, mm, t, ctr) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.addresses(r, l, s, mm, t, ctr) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def regen_eq source · line 207 · raw

@+need:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+mm:Nat -> @+t:Nat -> @+idx:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.regen(need, addr, r, l, s, mm, t, idx) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.regen(need, addr, r, l, s, mm, t, idx) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}