def fin0

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

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

206# Big-endian words of the 64-bit message bit length 8n, computed from n with
207# exactly the digit expressions bit_length produces, but without building and
208# matching an eight-element list. bit_length(n) is [o(d6), .., o(d0), low]
209# where d0 = n / 32, d(k+1) = dk / 256 and o(x) = x mod 256.
210def fin0(+n: Nat, +extra: Nat, s: S.State) -> S.State:
211  Runtime.fips_compress16(Runtime.pack(128, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.pack(0, 0, 0, 0), Runtime.len_hi(n), Runtime.len_lo(n),
212    extra, s)