law absorb512_inv

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

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

298law absorb512_inv:
299  for +fuel: Nat
300  for +bytes: List<&2, U32>
301  for +q: Nat
302  for +s: T512.State
303  for +z: List<&2, U32>
304  {C512.blocks(C512.lanes(List.append(&2, U32, bytes, z)), q, C512.round_constants(), s) == C512.blocks(C512.lanes(List.append(&2, U32, buf512(H.absorb512(fuel, H.read512_0(bytes), bytes, q, s)), z)), q, C512.round_constants(), st512(H.absorb512(fuel, H.read512_0(bytes), bytes, q, s))) : T512.State}