law fold256_inv
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/hash/incremental.bend:207
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as Incremental
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
207law fold256_inv:
208 for +cs: List<&2, List<&2, U32>>
209 for +q: Nat
210 for +st: H.Sha256State
211 for +z: List<&2, U32>
212 {C256.block_bytes(List.append(&2, U32, List.append(&2, U32, buf256(st), List.concat(&2, U32, cs)), z), q, C256.round_constants(), st256(st)) == C256.block_bytes(List.append(&2, U32, buf256(fold256(cs, q, st)), z), q, C256.round_constants(), st256(fold256(cs, q, st))) : S256.State}