~/bend-docscommunity

proofs/crypto/argon2/hash.bend checks

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

10 imports
import Base
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/blake/blake2b/blake2b.bend as IB
import ../../../src/crypto/blake/blake2b/sized.bend as IH
import ../../../src/crypto/argon2/types.bend as A
import ../../../src/crypto/argon2/sub.bend as SB
import ../../../src/crypto/argon2/argon2.bend as I
import ../../../spec/crypto/blake/blake2b.bend as SBL
import ../../../spec/crypto/argon2/argon2.bend as SA
import ../blake/blake2b/blocks.bend as BB

Definitions

def words_eq source · line 20 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.words(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.words(bs) : List<&2, U32>}

def fill_eq source · line 33 · raw

@+ws:List<&2, U32> -> @+i:U32 -> @a:Array<U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.fill(ws, i, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.fill(ws, i, a) : Array<U32>}

def pw_eq source · line 40 · raw

@+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.pw(k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.pw(k) : Nat}

def depth_eq source · line 47 · raw

@+fuel:Nat -> @+n:Nat -> @+d:Nat -> @+done:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.depth_go(fuel, n, d, done) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.depth_go(fuel, n, d, done) : Nat}

def pack_fin source · line 58 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.fill(ws, 0, Array.new(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.depth_go(32n, List.length(&2, U32, ws), 0n, Nat.is_le(List.length(&2, U32, ws), 1n)), 0)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.fill(ws, 0, Array.new(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.depth_go(32n, List.length(&2, U32, ws), 0n, Nat.is_le(List.length(&2, U32, ws), 1n)), 0)) : Array<U32>}

def pack_eq source · line 64 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.pack(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.pack(bs) : Array<U32>}

def initial_eq source · line 71 · raw

@+nn:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.initial(nn) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.initial(nn) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain}

def chain_bytes_eq source · line 74 · raw

@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Chain -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.chain_bytes(h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.chain_bytes(h) : List<&2, U32>}

def hash_eq source · line 79 · raw

@+nn:Nat -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.hash(nn, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hash(nn, bs) : List<&2, U32>}

def hp_go_eq source · line 94 · raw

@+n:Nat -> @+v:List<&2, U32> -> @+last:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_go(n, v, last) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hp_go(n, v, last) : List<&2, U32>}

def hp_pick_eq source · line 105 · raw

@+tl:Nat -> @+x:List<&2, U32> -> @+short:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hp_pick(tl, x, short) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hp_pick(tl, x, short) : List<&2, U32>}

def hprime_eq source · line 117 · raw

@+tl:Nat -> @+a:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.hprime(tl, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.hprime(tl, a) : List<&2, U32>}

H'^T

def h0_eq source · line 121 · raw

@+p:Nat -> @+tl:Nat -> @+m:Nat -> @+t:Nat -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.h0(p, tl, m, t, pw, salt, key, ad) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.h0(p, tl, m, t, pw, salt, key, ad) : List<&2, U32>}

H0

def row_eq source · line 126 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.row(ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.row_of(ws) : Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>)}

def rows_eq7 source · line 195 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r6:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_7(r0, r1, r2, r3, r4, r5, r6, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of7(r0, r1, r2, r3, r4, r5, r6, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq6 source · line 200 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r5:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_6(r0, r1, r2, r3, r4, r5, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of6(r0, r1, r2, r3, r4, r5, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq5 source · line 207 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r4:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_5(r0, r1, r2, r3, r4, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of5(r0, r1, r2, r3, r4, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq4 source · line 214 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r3:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_4(r0, r1, r2, r3, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of4(r0, r1, r2, r3, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq3 source · line 221 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r2:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_3(r0, r1, r2, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of3(r0, r1, r2, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq2 source · line 228 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+r1:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_2(r0, r1, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of2(r0, r1, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq1 source · line 235 · raw

@+r0:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_1(r0, p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of1(r0, p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows_eq0 source · line 242 · raw

@p:Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8_0(p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of0(p) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def rows8_eq source · line 249 · raw

@+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8(ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.rows_of0(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.row_of(ws)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

def block_of_eq source · line 255 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.block_of(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.block_of(bs) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}

A block from 1024 bytes.

def state_bytes_eq source · line 260 · raw

@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.state_bytes(v) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.state_bytes(v) : List<&2, U32>}

def block_bytes_eq source · line 266 · raw

@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.block_bytes(b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.block_bytes(b) : List<&2, U32>}

The bytes of a block, row by row.