law blocks_step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2b/blocks.bend:1846

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/array.bend as A

1846law blocks_step:
1847  for +n: Nat
1848  for +index: U32
1849  for +remain: Nat
1850  for +t: T.Counter
1851  for -a: Array<U32>
1852  for +h: T.Chain
1853  for view: Sigma<&2,&1,A.Tree,z => {a == A.thaw(z) : Array<U32>}>
1854  for recurse: @pair: (Array<U32> & T.Chain) -> {I.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) == S.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) : T.Chain}
1855  {I.blocks(1n+n,index,remain,t,(a,h)) == S.blocks(1n+n,index,remain,t,(a,h)) : T.Chain}