law fold512_inv

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/hash/incremental.bend:591

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H

591law fold512_inv:
592  for +cs: List<&2, List<&2, U32>>
593  for +q: Nat
594  for +st: H.Sha512State
595  for +z: List<&2, U32>
596  {C512.blocks(C512.lanes(List.append(&2, U32, List.append(&2, U32, buf512(st), List.concat(&2, U32, cs)), z)), q, C512.round_constants(), st512(st)) == C512.blocks(C512.lanes(List.append(&2, U32, buf512(fold512(cs, q, st)), z)), q, C512.round_constants(), st512(fold512(cs, q, st))) : T512.State}