~/bend-docscommunity

proofs/crypto/argon2/words.bend checks

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

6 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ../../math/typed/u32.bend as U32P
import ../../math/typed/width.bend as WW

Definitions

def v source · line 14 · raw

@+x:U32 -> Nat

def vb_k source · line 17 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, v(x)) == True{} : Bool}

def vb source · line 22 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, v(x)) == True{} : Bool}

every U32 value fits 32 bits

def lt_k source · line 25 · raw

@+k:Nat -> @+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, n) == True{} : Bool} -> {Nat.is_lt(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool}

def vo_k source · line 29 · raw

@+k:Nat -> @+hk:{k == 32n : Nat} -> @+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, n) == True{} : Bool} -> {v(U32.from_nat(n)) == n : Nat}

def vo source · line 33 · raw

@+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, n) == True{} : Bool} -> {v(U32.from_nat(n)) == n : Nat}

a value that fits is the value of its U32

def rt source · line 36 · raw

@+x:U32 -> {U32.from_nat(v(x)) == x : U32}

def fits_high source · line 40 · raw

@+t:Nat -> @+s:Nat -> @+x:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(t, s), x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(s, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(t, x)) == True{} : Bool}

the high part of a value of t + s bits has s bits