def len_row

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

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/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend as SB

294# One more row: 32 more words.
295def len_row(+v: T.State, +rest: List<&2, U32>) -> {SC.length(U32, SB.app(SB.row_words(v), rest)) == Nat.add(32n, SC.length(U32, rest)) : Nat}:
296  %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(v), rest)), Nat.add(SC.length(U32, SB.row_words(v)), SC.length(U32, rest)), len_app(SB.row_words(v), rest)) : {_ == Nat.add(32n, SC.length(U32, rest)) : Nat}
297  %Equal.sym(Nat, SC.length(U32, SB.row_words(v)), 32n, rw_len(v)) : {Nat.add(_, SC.length(U32, rest)) == Nat.add(32n, SC.length(U32, rest)) : Nat}
298  {==}