law schedule_rounds_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/conformance.bend:179

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C

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