def window_rounds

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

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

81# A fixed rolling window drops schedule words as soon as they are older than 16
82# rounds. This avoids growing and reference-counting the reverse history list.
83def window_rounds(n: Nat, win: Runtime.ShaWindow, ks: List<&2, U32>, s: S.State) -> S.State:
84  match n win ks:
85    case 0n _ _:
86      s
87    case 1n+q _ Nil{}:
88      s
89    case 1n+q Runtime.W{a, +b, c, d, e, f, +g, h, i, j, l, m, o, r, +t, +u} k <> kt:
90      +w = (Runtime.small1(b) + g + Runtime.small0(t) + u : U32)
91      window_rounds(q, Runtime.W{w, a, b, c, d, e, f, g, h, i, j, l, m, o, r, t}, kt,
92        Runtime.step(s, k, w))