def wr_words

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:462

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as M

462# M.wr stores the words ws from word i on.
463def wr_words(+d: Nat, +ws: List<&2, U32>, +i: Nat, +V: List<&2, U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hl: {SC.length(U32, V) == SC.pow2(d) : Nat}, +hi: {Nat.is_le(Nat.add(i, SC.length(U32, ws)), SC.pow2(d)) == True{} : Bool}) -> {M.wr(ws, i, AR.thaw(U32, tree(d, V))) == AR.thaw(U32, tree(d, splice(ws, i, V))) : Array<U32>}:
464  match ws:
465    case Nil{}:
466      {==}
467    case +w <> +rest:
468      +t = tree(d, V)
469      +hi1 = N.lt_le_trans(i, Nat.add(i, 1n+SC.length(U32, rest)), SC.pow2(d), lt_add_succ(i, SC.length(U32, rest)), hi)
470      +ei = U.to_nat_from_nat(i, d, le32(d, hd), hi1)
471      +hin = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), hi1)
472      +hn = nth_some(V, i, L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.pow2(d), SC.length(U32, V), Equal.sym(Nat, SC.length(U32, V), SC.pow2(d), hl), hi1))
473      +hx = L.subst(List<&2, U32>, z => {SC.nth(U32, z, U32.to_nat(U32.from_nat(i))) == Some{nthv(V, i)} : Maybe<&2, U32>}, V, AR.slots(U32, t), Equal.sym(List<&2, U32>, AR.slots(U32, t), V, tree_slots(d, V, hl)),
474        L.subst(Nat, z => {SC.nth(U32, V, z) == Some{nthv(V, i)} : Maybe<&2, U32>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ei), hn))
475      +es = AR.set(U32, d, t, U32.from_nat(i), w, nthv(V, i), hd, hin, hx, tree_perfect(d, V))
476      +t2 = AR.upd(U32, d, t, i, w)
477      +V2 = SC.update(U32, V, i, w)
478      +e_slots = Equal.trans(List<&2, U32>, AR.slots(U32, t2), SC.update(U32, AR.slots(U32, t), i, w), V2,
479        AR.upd_slots(U32, d, t, i, w, hi1, tree_perfect(d, V)),
480        Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, i, w), AR.slots(U32, t), V, tree_slots(d, V, hl)))
481      +e_ext = Equal.trans(AR.Tree<U32>, t2, tree(d, AR.slots(U32, t2)), tree(d, V2), tree_ext(d, t2, AR.upd_perfect(U32, d, t, i, w, tree_perfect(d, V))), Equal.cong(List<&2, U32>, AR.Tree<U32>, z => tree(d, z), AR.slots(U32, t2), V2, e_slots))
482      +hl2 = Equal.trans(Nat, SC.length(U32, V2), SC.length(U32, V), SC.pow2(d), LL.length_update(U32, V, i, w), hl)
483      +hi2 = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, Nat.add(i, 1n+SC.length(U32, rest)), Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Equal.sym(Nat, Nat.add(Nat.add(i, 1n), SC.length(U32, rest)), Nat.add(i, 1n+SC.length(U32, rest)), add_one_assoc(i, SC.length(U32, rest))), hi)
484      %Equal.sym(Array<U32>, Array.set(U32, AR.thaw(U32, t), U32.from_nat(i), w), AR.thaw(U32, AR.upd(U32, d, t, U32.to_nat(U32.from_nat(i)), w)), es) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
485      %Equal.sym(Array<U32>, AR.thaw(U32, AR.upd(U32, d, t, U32.to_nat(U32.from_nat(i)), w)), AR.thaw(U32, t2), Equal.cong(Nat, Array<U32>, z => AR.thaw(U32, AR.upd(U32, d, t, z, w)), U32.to_nat(U32.from_nat(i)), i, ei)) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
486      %Equal.sym(Array<U32>, AR.thaw(U32, t2), AR.thaw(U32, tree(d, V2)), Equal.cong(AR.Tree<U32>, Array<U32>, z => AR.thaw(U32, z), t2, tree(d, V2), e_ext)) : {M.wr(rest, Nat.add(i, 1n), _) == AR.thaw(U32, tree(d, splice(rest, Nat.add(i, 1n), V2))) : Array<U32>}
487      wr_words(d, rest, Nat.add(i, 1n), V2, hd, hl2, hi2)