law compress_correct

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/packed_proof.bend:12

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

12law compress_correct:
13  for +a: U32
14  for +b: U32
15  for +c: U32
16  for +d: U32
17  for +e: U32
18  for +f: U32
19  for +g: U32
20  for +h: U32
21  for +i: U32
22  for +j: U32
23  for +k: U32
24  for +l: U32
25  for +m: U32
26  for +n: U32
27  for +o: U32
28  for +p: U32
29  for +extra: Nat
30  for +s: S.State
31  {Runtime.fips_compress16(a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,extra,s) == R.compress([a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p],extra,s) : S.State}