law pair_step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/keccak/permutation.bend:48

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P

48law pair_step:
49  for +n: Nat
50  for +i: Nat
51  for +s: T.State
52  {P.rounds(2n+n,i,s) == P.rounds(n,2n+i,P.round(P.round(s,P.constant(i)),P.constant(1n+i))) : T.State}