law schedule_rounds_correct

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:180

import Base
import bend-collections@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as C

180law schedule_rounds_correct:
181  for +ws: List<&2, U32>
182  for +extra: Nat
183  for +history: List<&2, U32>
184  for +ks: List<&2, U32>
185  for +s: S.State
186  {C.schedule_rounds(ws, extra, history, ks, s) ==
187    C.rounds(ks, List.append(&2, U32, ws, C.expand(extra, history)), s) : S.State}