def expanded_rounds

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

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

58# Generate each derived schedule word immediately before its round. The reverse
59# history is still retained for the recurrence, but the chronological 48-word
60# extension is never materialized.
61def expanded_rounds(n: Nat, +history: List<&2, U32>, ks: List<&2, U32>, s: S.State) -> S.State:
62  match n ks:
63    case 0n _:
64      s
65    case 1n+p Nil{}:
66      s
67    case 1n+p k <> kt:
68      +w = next_word(history)
69      expanded_rounds(p, w <> history, kt, Runtime.step(s, k, w))