def next_word

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/packed/core_model.bend:23

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/core.bend as Runtime

23# Schedule histories always contain at least 16 words. Destructuring that prefix
24# avoids four independent linked-list walks for every expanded word; the fallback
25# preserves the total behavior used by the universal refinement theorem.
26def next_word(+history: List<&2, U32>) -> U32:
27  match history:
28    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> (p <> rest):
29      (Runtime.small1(b) + g + Runtime.small0(o) + p : U32)
30    case _:
31      next_word_slow(history)