1	import Base
2	import ../../../src/crypto/keccak/types.bend as T
3	import ../../../src/crypto/keccak/permutation.bend as P
4	import ../../../spec/crypto/keccak/permutation.bend as S
5	import ../../../src/crypto/keccak/keccak.bend as K
6	import ../../../spec/crypto/keccak/main.bend as Sponge
7	
8	# Universal permutation refinement; instantiating n=24 and i=0 gives Keccak-f[1600].
9	law permutation_rounds:
10	  for +n: Nat
11	  for +i: Nat
12	  for +s: T.State
13	  {P.rounds(n,i,s) == S.rounds(n,i,s) : T.State}
14	
15	law digest_size:
16	  for s: T.State
17	  {Pair.snd(Array<U32>,U32,Array.size(U32,K.digest(s))) == 8 : U32}
18	
19	law capacity_rejection:
20	  for a: Array<U32>
21	  for +n: Nat
22	  for +capacity: U32
23	  for invalid: {Nat.is_le(n,Nat.mul(4n,U32.to_nat(capacity))) == False{} : Bool}
24	  {K.sized(24n,n,(a,capacity)) == None{} : Maybe<&1,Array<U32>>}
25	
26	law packed_sponge_correct:
27	  for +r: Nat
28	  for a: Array<U32>
29	  for +length: Nat
30	  {K.keccak256_rounds(r,a,length) == Sponge.keccak256_rounds(r,a,length) : Maybe<&1,Array<U32>>}
31	
32	law ethereum_round_count:
33	  for a: Array<U32>
34	  for +length: Nat
35	  {K.keccak256(a,length) == K.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}
36	
37	law ethereum_keccak256:
38	  for a: Array<U32>
39	  for +length: Nat
40	  {K.keccak256(a,length) == Sponge.keccak256_rounds(24n,a,length) : Maybe<&1,Array<U32>>}