def words_len

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

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

300def words_len(+b: A.Block) -> {SC.length(U32, SB.words(b)) == 256n : Nat}:
301  match b:
302    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
303      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r0), SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), len_row(r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))) : {_ == 256n : Nat}
304      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), len_row(r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))) : {Nat.add(32n, _) == 256n : Nat}
305      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), len_row(r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))) : {Nat.add(32n, Nat.add(32n, _)) == 256n : Nat}
306      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), len_row(r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, _))) == 256n : Nat}
307      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), len_row(r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _)))) == 256n : Nat}
308      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), len_row(r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _))))) == 256n : Nat}
309      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), Nat.add(32n, SC.length(U32, SB.app(SB.row_words(r7), Nil{}))), len_row(r6, SB.app(SB.row_words(r7), Nil{}))) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _)))))) == 256n : Nat}
310      %Equal.sym(Nat, SC.length(U32, SB.app(SB.row_words(r7), Nil{})), Nat.add(32n, SC.length(U32, Nil{})), len_row(r7, Nil{})) : {Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, Nat.add(32n, _))))))) == 256n : Nat}
311      {==}