~/bend-docscommunity

proofs/crypto/argon2/fill.bend checks

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

19 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 ./index.bend as IX

Definitions

def mod_lt source · line 27 · raw

@+v:Nat -> @+q:Nat -> @+hq:{Nat.is_le(1n, q) == True{} : Bool} -> {Nat.is_lt(Nat.mod(v, q), q) == True{} : Bool}

def lt_mul_add source · line 35 · raw

@+a:Nat -> @+p:Nat -> @+b:Nat -> @+q:Nat -> @+ha:{Nat.is_lt(a, p) == True{} : Bool} -> @+hb:{Nat.is_lt(b, q) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.mul(a, q), b), Nat.mul(p, q)) == True{} : Bool}

a < p and b < q give a * q + b < p * q.

def seg_lt source · line 42 · raw

@+s:Nat -> @+sl:Nat -> @+idx:Nat -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> {Nat.is_lt(Nat.add(Nat.mul(s, sl), idx), Nat.mul(4n, sl)) == True{} : Bool}

s < 4 and idx < sl give s * sl + idx < 4 sl.

def le_of_lt source · line 45 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def other_le source · line 48 · raw

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

def area_le source · line 56 · raw

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

The size of the reference area is below the base plus the index.

def base_lt source · line 64 · raw

@+r0:Bool -> @+s:Nat -> @+sl:Nat -> @+idx:Nat -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> {Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area_base(r0, s, sl, Nat.mul(4n, sl)), idx), Nat.mul(4n, sl)) == True{} : Bool}

The base of the reference area plus the index stays below q = 4 sl.

def store_eq source · line 78 · raw

@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+r0:Bool -> @+cur:Nat -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+refb: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} -> @+hcur:{Nat.is_lt(cur, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.store(r0, cur, prev, refb, 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.store(r0, cur, prev, refb, mem))) : Array<U32>}

def store_len source · line 89 · raw

@+r0:Bool -> @+cur:Nat -> @+prev:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+refb:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+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.store(r0, cur, prev, refb, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def ixi source · line 97 · raw

@+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> Nat

The reference block index from the pseudo-random lane pr, as the implementation computes it.

def ixi_mid source · line 103 · raw

@+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+rl:Nat -> Nat

The same after the reference lane, and as the specification computes it.

def ixs_mid source · line 106 · raw

@+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+rl:Nat -> Nat

def ixs source · line 109 · raw

@+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> Nat

def le_mul256 source · line 114 · raw

@+n:Nat -> {Nat.is_le(n, Nat.mul(n, 256n)) == True{} : Bool}

def area_bound source · line 119 · raw

@+d:Nat -> @+n:Nat -> @+r0:Bool -> @+s:Nat -> @+sl:Nat -> @+q:Nat -> @+idx:Nat -> @+same:Bool -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> @+hqn:{Nat.is_le(q, n) == True{} : Bool} -> @+hn:{Nat.is_le(Nat.mul(n, 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.area_base(r0, s, sl, q), idx, same), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool}

|W| < 2^d.

def mid_eq source · line 126 · raw

@+d:Nat -> @+n:Nat -> @+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+rl:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> @+hqn:{Nat.is_le(q, n) == True{} : Bool} -> @+hn:{Nat.is_le(Nat.mul(n, 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {ixi_mid(r0, s, l, idx, q, sl, pr, rl) == ixs_mid(r0, s, l, idx, q, sl, pr, rl) : Nat}

def ix_eq source · line 142 · raw

@+d:Nat -> @+n:Nat -> @+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> @+hqn:{Nat.is_le(q, n) == True{} : Bool} -> @+hn:{Nat.is_le(Nat.mul(n, 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {ixi(r0, s, l, idx, p, q, sl, pr) == ixs(r0, s, l, idx, p, q, sl, pr) : Nat}

def ref_lane_lt source · line 153 · raw

@+f:Bool -> @+l:Nat -> @+j2:U32 -> @+p:Nat -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.ref_lane(f, l, j2, p), p) == True{} : Bool}

def q_pos source · line 160 · raw

@+q:Nat -> @+sl:Nat -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hsl:{Nat.is_le(1n, sl) == True{} : Bool} -> {Nat.is_le(1n, q) == True{} : Bool}

def ix_lt source · line 164 · raw

@+r0:Bool -> @+s:Nat -> @+l:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.Lane -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hq1:{Nat.is_le(1n, q) == True{} : Bool} -> {Nat.is_lt(ixs(r0, s, l, idx, p, q, sl, pr), Nat.mul(p, q)) == True{} : Bool}

The reference block is in the memory.

def le_mul_left source · line 168 · raw

@+p:Nat -> @+q:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.is_le(q, Nat.mul(p, q)) == True{} : Bool}

def step_eq source · line 176 · raw

@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+cur:Nat -> @+indep:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+pb: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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(1n, sl) == True{} : Bool} -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hi:{Nat.is_lt(idx, sl) == True{} : Bool} -> @+hcur:{Nat.is_lt(cur, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.step(r, l, s, idx, p, q, sl, cur, indep, addr, (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, mem)), pb)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem))) : Array<U32>}

One block of a segment.

def step_len source · line 194 · raw

@+r:Nat -> @+l:Nat -> @+s:Nat -> @+idx:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+cur:Nat -> @+indep:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+pb:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+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.step(r, l, s, idx, p, q, sl, cur, indep, addr, pb, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def sub1_lt source · line 198 · raw

@+q:Nat -> @+hq1:{Nat.is_le(1n, q) == True{} : Bool} -> {Nat.is_lt(Nat.sub(q, 1n), q) == True{} : Bool}

def prev_lt source · line 207 · raw

@+l:Nat -> @+p:Nat -> @+q:Nat -> @+j:Nat -> @+b:Bool -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hj:{Nat.is_lt(j, q) == True{} : Bool} -> @+hq1:{Nat.is_le(1n, q) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.prev_index(l, q, j, b), Nat.mul(p, q)) == True{} : Bool}

The previous block is in the memory.

def lt_of_add_succ source · line 214 · raw

@+a:Nat -> @+r:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(a, 1n+r), n) == True{} : Bool} -> {Nat.is_lt(a, n) == True{} : Bool}

def le_shift source · line 217 · raw

@+a:Nat -> @+r:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(a, 1n+r), n) == True{} : Bool} -> {Nat.is_le(Nat.add(Nat.add(a, 1n), r), n) == True{} : Bool}

def lt_q source · line 220 · raw

@+q:Nat -> @+sl:Nat -> @+x:Nat -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+h:{Nat.is_lt(x, Nat.mul(4n, sl)) == True{} : Bool} -> {Nat.is_lt(x, q) == True{} : Bool}

def lt_len source · line 223 · raw

@+x:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+p:Nat -> @+q:Nat -> @+hlen:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) == Nat.mul(p, q) : Nat} -> @+h:{Nat.is_lt(x, Nat.mul(p, q)) == True{} : Bool} -> {Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool}

def seg_len source · line 226 · raw

@+n:Nat -> @+idx:Nat -> @+first:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+indep:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.seg_go(n, idx, first, addr, mem, r, l, s, p, q, sl, mm, t, indep)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def seg_eq source · line 239 · raw

@+d:Nat -> @+n:Nat -> @+idx:Nat -> @+first:Bool -> @+addr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+r:Nat -> @+l:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+indep:Bool -> @+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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(1n, sl) == True{} : Bool} -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hidx:{Nat.is_le(Nat.add(idx, n), sl) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.seg_go(n, idx, first, addr, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, mem)), r, l, s, p, q, sl, mm, t, indep) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.seg_go(n, idx, first, addr, mem, r, l, s, p, q, sl, mm, t, indep))) : Array<U32>}

Positions idx .. idx + n - 1 of a segment.

def start_index_le source · line 270 · raw

@+f:Bool -> @+sl:Nat -> @+h2:{Nat.is_le(2n, sl) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.start_index(f), sl) == True{} : Bool}

def segment_len source · line 277 · raw

@+r:Nat -> @+s:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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.segment(r, s, l, p, q, sl, mm, t, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def segment_eq source · line 283 · raw

@+d:Nat -> @+r:Nat -> @+s:Nat -> @+l:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> @+hl:{Nat.is_lt(l, p) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.segment(r, s, l, p, q, sl, mm, t, 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.segment(r, s, l, p, q, sl, mm, t, mem))) : Array<U32>}

One segment.

def lanes_len source · line 297 · raw

@+n:Nat -> @+l:Nat -> @+r:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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.lanes_go(n, l, r, s, p, q, sl, mm, t, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def keep_c source · line 306 · raw

@+d:Nat -> @+m1:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+m2:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m2) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m1) : Nat} -> @+hc:{Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m1), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m2), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool}

def keep_len source · line 309 · raw

@+m1:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+m2:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+x:Nat -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m2) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m1) : Nat} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m1) == x : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, m2) == x : Nat}

def lanes_eq source · line 313 · raw

@+d:Nat -> @+n:Nat -> @+l:Nat -> @+r:Nat -> @+s:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 4n) == True{} : Bool} -> @+hln:{Nat.is_le(Nat.add(l, n), p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.lanes_go(n, l, r, s, p, q, sl, mm, t, 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.lanes_go(n, l, r, s, p, q, sl, mm, t, mem))) : Array<U32>}

The lanes l .. l + n - 1 of a slice.

def slices_len source · line 323 · raw

@+n:Nat -> @+s:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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.slices_go(n, s, r, p, q, sl, mm, t, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def slices_eq source · line 333 · raw

@+d:Nat -> @+n:Nat -> @+s:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> @+hsn:{Nat.is_le(Nat.add(s, n), 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.slices_go(n, s, r, p, q, sl, mm, t, 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.slices_go(n, s, r, p, q, sl, mm, t, mem))) : Array<U32>}

Slices s .. s + n - 1 of a pass.

def passes_len source · line 343 · raw

@+n:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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.passes_go(n, r, p, q, sl, mm, t, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) : Nat}

def passes_eq source · line 353 · raw

@+d:Nat -> @+n:Nat -> @+r:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+t:Nat -> @+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} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.passes_go(n, r, p, q, sl, mm, t, 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.passes_go(n, r, p, q, sl, mm, t, mem))) : Array<U32>}

Passes r .. r + n - 1.