proofs/crypto/argon2/memory.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
14 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/u32.bend as U import ../../lib/lemmas/proofs/nat_algebra.bend as NA import ../../../src/crypto/blake/blake2b/types.bend as T import ../../../src/crypto/argon2/types.bend as A import ../../../src/crypto/argon2/sub.bend as SB import ../../../src/crypto/argon2/memory.bend as M import ../../../spec/crypto/argon2/blamka.bend as SG import ../../../spec/crypto/argon2/argon2.bend as SA
Definitions
def nthv source · line 28 · raw
@ws:List<&2, U32> -> @i:Nat -> U32
def take_drop source · line 31 · raw
@+xs:List<&2, U32> -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, xs, n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, xs, n)) == xs : List<&2, U32>}
def zsub source · line 40 · raw
@+n:Nat -> {Nat.sub(0n, n) == 0n : Nat}
def length_drop source · line 47 · raw
@+xs:List<&2, U32> -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, xs, n)) == Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs), n) : Nat}
def take_all source · line 56 · raw
@+xs:List<&2, U32> -> @+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs) == n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, xs, n) == xs : List<&2, U32>}
def drop_zero source · line 65 · raw
@+ys:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, ys, 0n) == ys : List<&2, U32>}
def drop_all source · line 72 · raw
@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+n:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs) == n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, xs, ys), n) == ys : List<&2, U32>}
def tree source · line 86 · raw
@d:Nat -> @+ws:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.Tree<U32>
The perfect tree of depth d holding ws (padded by zeros, truncated at 2^d).
def tree_perfect source · line 93 · raw
@+d:Nat -> @+ws:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.perfect(U32, d, tree(d, ws)) == True{} : Bool}
def leaf_slots source · line 100 · raw
@+ws:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws) == 1n : Nat} -> {[nthv(ws, 0n)] == ws : List<&2, U32>}
def double_sub source · line 109 · raw
@+x:Nat -> {Nat.sub(Nat.double(x), x) == x : Nat}
def pow2_le_succ source · line 113 · raw
@+p:Nat -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(p), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(1n+p)) == True{} : Bool}
def tree_slots source · line 117 · raw
@+d:Nat -> @+ws:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.slots(U32, tree(d, ws)) == ws : List<&2, U32>}The words of tree(d, ws) are ws, for 2^d words.
def tree_ext source · line 133 · raw
@+d:Nat -> @+t:0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.Tree<U32> -> @+pf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.perfect(U32, d, t) == True{} : Bool} -> {t == tree(d, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.slots(U32, t)) : 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.Tree<U32>}A perfect tree is the tree of its words.
def nth_some source · line 162 · raw
@+xs:List<&2, U32> -> @+j:Nat -> @+h:{Nat.is_lt(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.nth(U32, xs, j) == Some{nthv(xs, j)} : Maybe<&2, U32>}
def le32 source · line 171 · raw
@+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> {Nat.is_le(d, 32n) == True{} : Bool}
def get_word source · line 175 · raw
@+d:Nat -> @+ws:List<&2, U32> -> @+j:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) : Nat} -> @+hj:{Nat.is_lt(j, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {Array.get(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, ws)), U32.from_nat(j)) == (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, ws)), nthv(ws, j)) : Pair(Array<U32>, U32)}Array.get at word j of the tree of ws.
def slice source · line 186 · raw
@ws:List<&2, U32> -> @+base:Nat -> @n:Nat -> List<&2, U32>
def nth_drop source · line 189 · raw
@+ws:List<&2, U32> -> @+base:Nat -> @+k:Nat -> {nthv(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, ws, base), k) == nthv(ws, Nat.add(base, k)) : U32}
def take_snoc source · line 198 · raw
@+ys:List<&2, U32> -> @+k:Nat -> @+h:{Nat.is_lt(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ys)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, ys, 1n+k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, ys, k), [nthv(ys, k)]) : List<&2, U32>}
def lt_sub source · line 207 · raw
@+base:Nat -> @+k:Nat -> @+n:Nat -> @+h:{Nat.is_lt(Nat.add(base, k), n) == True{} : Bool} -> {Nat.is_lt(k, Nat.sub(n, base)) == True{} : Bool}
def slice_snoc source · line 217 · raw
@+ws:List<&2, U32> -> @+base:Nat -> @+k:Nat -> @+h:{Nat.is_lt(Nat.add(base, k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws)) == True{} : Bool} -> {slice(ws, base, 1n+k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, slice(ws, base, k), [nthv(ws, Nat.add(base, k))]) : List<&2, U32>}slice(ws, base, k + 1) is slice(ws, base, k) and word base + k.
def slice_one source · line 224 · raw
@+ws:List<&2, U32> -> @+base:Nat -> @+h:{Nat.is_lt(base, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws)) == True{} : Bool} -> {slice(ws, base, 1n) == [nthv(ws, base)] : List<&2, U32>}
def append_cons source · line 233 · raw
@+xs:List<&2, U32> -> @+w:U32 -> @+acc:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, xs, [w]), acc) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, xs, w <> acc) : List<&2, U32>}
def lt_pred source · line 236 · raw
@+base:Nat -> @+p:Nat -> @+n:Nat -> @+h:{Nat.is_lt(Nat.add(base, 1n+p), n) == True{} : Bool} -> {Nat.is_lt(Nat.add(base, p), n) == True{} : Bool}
def pred_add source · line 239 · raw
@+base:Nat -> @+p:Nat -> {Nat.sub(Nat.add(base, 1n+p), 1n) == Nat.add(base, p) : Nat}
def rd_words source · line 244 · raw
@+d:Nat -> @+ws:List<&2, U32> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) : Nat} -> @+n:Nat -> @+base:Nat -> @+acc:List<&2, U32> -> @+h:{Nat.is_lt(Nat.add(base, n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.rd(n, Nat.add(base, n), acc, (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, ws)), nthv(ws, Nat.add(base, n)))) == (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, ws)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, slice(ws, base, 1n+n), acc)) : Pair(Array<U32>, List<&2, U32>)}M.rd reads words base + n down to base (onto acc), leaving the memory unchanged.
def flat source · line 265 · raw
@mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, U32>
def pad source · line 272 · raw
@+d:Nat -> @+n:Nat -> List<&2, U32>
def W source · line 276 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, U32>
The words of the memory mem in an array of 2^d words.
def mt source · line 279 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.Tree<U32>
def rw_len source · line 282 · raw
@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.row_words(v)) == 32n : Nat}
def len_app source · line 287 · raw
@+a:List<&2, U32> -> @+b:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.app(a, b)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, b)) : Nat}
def len_row source · line 295 · raw
@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+rest:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.app(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.row_words(v), rest)) == Nat.add(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, rest)) : Nat}One more row: 32 more words.
def words_len source · line 300 · raw
@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(b)) == 256n : Nat}
def row_rw source · line 313 · raw
@+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State -> @+rest:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.row(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.app(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.row_words(v), rest)) == (v, rest) : Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.State, List<&2, U32>)}
def rows8_words source · line 318 · raw
@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.rows8(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(b)) == b : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block}
def flat_len source · line 331 · raw
@+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, flat(mem)) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem), 256n) : Nat}
def W_len source · line 342 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+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} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, W(d, mem)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) : Nat}
def drop_append_add source · line 354 · raw
@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+n:Nat -> @+k:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs) == n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, xs, ys), Nat.add(n, k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, ys, k) : List<&2, U32>}
def drop_append_le source · line 365 · raw
@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+n:Nat -> @+h:{Nat.is_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, xs, ys), n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.drop(U32, xs, n), ys) : List<&2, U32>}
def flat_slice source · line 377 · raw
@+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {slice(flat(mem), Nat.mul(b, 256n), 256n) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.get(mem, b)) : List<&2, U32>}The 256 words of block b of the flattened blocks.
def mul_lt source · line 393 · raw
@+b:Nat -> @+n:Nat -> @+hb:{Nat.is_lt(b, n) == True{} : Bool} -> {Nat.is_le(Nat.add(Nat.mul(b, 256n), 256n), Nat.mul(n, 256n)) == True{} : Bool}
def le_sub source · line 403 · raw
@+base:Nat -> @+k:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(base, k), n) == True{} : Bool} -> {Nat.is_le(k, Nat.sub(n, base)) == True{} : Bool}
def slice_W source · line 412 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {slice(W(d, mem), Nat.mul(b, 256n), 256n) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.get(mem, b)) : List<&2, U32>}
def lt_last source · line 427 · raw
@+base:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(base, 256n), n) == True{} : Bool} -> {Nat.is_lt(Nat.add(base, 255n), n) == True{} : Bool}
def get_block source · line 431 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+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} -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.get(b, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, mt(d, mem))) == (0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, mt(d, mem)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.get(mem, b)) : Pair(Array<U32>, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block)}Reading block b of the memory of mem.
def splice source · line 448 · raw
@ws:List<&2, U32> -> @+i:Nat -> @V:List<&2, U32> -> List<&2, U32>
Words ws stored from index i on.
def lt_add_succ source · line 455 · raw
@+i:Nat -> @+r:Nat -> {Nat.is_lt(i, Nat.add(i, 1n+r)) == True{} : Bool}
def add_one_assoc source · line 459 · raw
@+i:Nat -> @+r:Nat -> {Nat.add(Nat.add(i, 1n), r) == Nat.add(i, 1n+r) : Nat}
def wr_words source · line 463 · raw
@+d:Nat -> @+ws:List<&2, U32> -> @+i:Nat -> @+V:List<&2, U32> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, V) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d) : Nat} -> @+hi:{Nat.is_le(Nat.add(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.wr(ws, i, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, V))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, tree(d, splice(ws, i, V))) : Array<U32>}M.wr stores the words ws from word i on.
def splice_app_left source · line 489 · raw
@+ws:List<&2, U32> -> @+i:Nat -> @+X:List<&2, U32> -> @+P:List<&2, U32> -> @+h:{Nat.is_le(Nat.add(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, X)) == True{} : Bool} -> {splice(ws, i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, X, P)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, splice(ws, i, X), P) : List<&2, U32>}
def splice_app_right source · line 501 · raw
@+ws:List<&2, U32> -> @+n:Nat -> @+k:Nat -> @+X:List<&2, U32> -> @+Y:List<&2, U32> -> @+hX:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, X) == n : Nat} -> {splice(ws, Nat.add(n, k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, X, Y)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, X, splice(ws, k, Y)) : List<&2, U32>}
def take_upd source · line 514 · raw
@+V:List<&2, U32> -> @+i:Nat -> @+w:U32 -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, V)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.update(U32, V, i, w), 1n+i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, V, i), [w]) : List<&2, U32>}
def splice_self source · line 524 · raw
@+ws:List<&2, U32> -> @+i:Nat -> @+V:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, V) == Nat.add(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, ws)) : Nat} -> {splice(ws, i, V) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.append(U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.take(U32, V, i), ws) : List<&2, U32>}Storing ws from word i over V, when V ends exactly there: the first i words of V, then ws.
def splice_full source · line 538 · raw
@+b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> {splice(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(v), 0n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(b)) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(v) : List<&2, U32>}
def flat_splice source · line 543 · raw
@+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {splice(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(v), Nat.mul(b, 256n), flat(mem)) == flat(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.set(mem, b, v)) : List<&2, U32>}
def W_splice source · line 556 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {splice(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(v), Nat.mul(b, 256n), W(d, mem)) == W(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.set(mem, b, v)) : List<&2, U32>}
def set_block source · line 569 · raw
@+d:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+b:Nat -> @+v: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} -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.set(b, v, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, mt(d, mem))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.set(mem, b, v))) : Array<U32>}Writing block b of the memory of mem.
def zero_words source · line 577 · raw
{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.words(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.zero) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(U32, 256n, 0) : List<&2, U32>}
def flat_zero source · line 580 · raw
@+n:Nat -> {flat(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.zero)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(U32, Nat.mul(n, 256n), 0) : List<&2, U32>}
def new_mem source · line 592 · raw
@+d:Nat -> @+mm:Nat -> @+hc:{Nat.is_le(Nat.mul(mm, 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> {Array.new(U32, d, 0) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mm, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.zero))) : Array<U32>}The zeroed array is the memory of mm zero blocks.