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	
6	law round_correct:
7	  for +s: T.State
8	  for +rc: T.Lane
9	  {P.round(s,rc) == S.round(s,rc) : T.State}
10	
11	def round_correct(s,rc):
12	  match s rc:
13	    case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},T.W{a4,b4},T.W{a5,b5},T.W{a6,b6},T.W{a7,b7},T.W{a8,b8},T.W{a9,b9},T.W{a10,b10},T.W{a11,b11},T.W{a12,b12},T.W{a13,b13},T.W{a14,b14},T.W{a15,b15},T.W{a16,b16},T.W{a17,b17},T.W{a18,b18},T.W{a19,b19},T.W{a20,b20},T.W{a21,b21},T.W{a22,b22},T.W{a23,b23},T.W{a24,b24}} T.W{lo,hi}: {==}
14	
15	law constants_correct:
16	  for +n: Nat
17	  {P.constant(n) == S.constant(n) : T.Lane}
18	
19	def constants_correct(n):
20	  match n:
21	    case 0n: {==}
22	    case 1n: {==}
23	    case 2n: {==}
24	    case 3n: {==}
25	    case 4n: {==}
26	    case 5n: {==}
27	    case 6n: {==}
28	    case 7n: {==}
29	    case 8n: {==}
30	    case 9n: {==}
31	    case 10n: {==}
32	    case 11n: {==}
33	    case 12n: {==}
34	    case 13n: {==}
35	    case 14n: {==}
36	    case 15n: {==}
37	    case 16n: {==}
38	    case 17n: {==}
39	    case 18n: {==}
40	    case 19n: {==}
41	    case 20n: {==}
42	    case 21n: {==}
43	    case 22n: {==}
44	    case 23n: {==}
45	    case 24n+p: {==}
46	
47	
48	law 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}
53	
54	def pair_step(n,i,s):
55	  match s:
56	    case T.S{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},T.W{a4,b4},T.W{a5,b5},T.W{a6,b6},T.W{a7,b7},T.W{a8,b8},T.W{a9,b9},T.W{a10,b10},T.W{a11,b11},T.W{a12,b12},T.W{a13,b13},T.W{a14,b14},T.W{a15,b15},T.W{a16,b16},T.W{a17,b17},T.W{a18,b18},T.W{a19,b19},T.W{a20,b20},T.W{a21,b21},T.W{a22,b22},T.W{a23,b23},T.W{a24,b24}}: {==}
57	
58	law single_step:
59	  for +i: Nat
60	  for +s: T.State
61	  {P.rounds(1n,i,s) == P.round(s,P.constant(i)) : T.State}
62	
63	def single_step(i,s):
64	  {==}
65	
66	law step_correct:
67	  for +i: Nat
68	  for +s: T.State
69	  {P.round(s,P.constant(i)) == S.round(s,S.constant(i)) : T.State}
70	
71	def step_correct(i,s):
72	  Equal.trans(T.State,P.round(s,P.constant(i)),S.round(s,P.constant(i)),S.round(s,S.constant(i)),
73	    round_correct(s,P.constant(i)),
74	    Equal.cong(T.Lane,T.State,r => S.round(s,r),P.constant(i),S.constant(i),constants_correct(i)))
75	
76	law two_correct:
77	  for +i: Nat
78	  for +s: T.State
79	  {P.round(P.round(s,P.constant(i)),P.constant(1n+i)) == S.round(S.round(s,S.constant(i)),S.constant(1n+i)) : T.State}
80	
81	def two_correct(i,s):
82	  Equal.trans(T.State,
83	    P.round(P.round(s,P.constant(i)),P.constant(1n+i)),
84	    S.round(P.round(s,P.constant(i)),S.constant(1n+i)),
85	    S.round(S.round(s,S.constant(i)),S.constant(1n+i)),
86	    step_correct(1n+i,P.round(s,P.constant(i))),
87	    Equal.cong(T.State,T.State,t => S.round(t,S.constant(1n+i)),P.round(s,P.constant(i)),S.round(s,S.constant(i)),step_correct(i,s)))
88	
89	law rounds_correct:
90	  for +n: Nat
91	  for +i: Nat
92	  for +s: T.State
93	  {P.rounds(n,i,s) == S.rounds(n,i,s) : T.State}
94	
95	def rounds_correct(n,i,s):
96	  match n:
97	    case 0n: {==}
98	    case 1n:
99	      Equal.trans(T.State,P.rounds(1n,i,s),P.round(s,P.constant(i)),S.round(s,S.constant(i)),single_step(i,s),step_correct(i,s))
100	    case 2n+p:
101	      Equal.trans(T.State,P.rounds(2n+p,i,s),P.rounds(p,2n+i,P.round(P.round(s,P.constant(i)),P.constant(1n+i))),S.rounds(2n+p,i,s),pair_step(p,i,s),
102	        Equal.trans(T.State,
103	          P.rounds(p,2n+i,P.round(P.round(s,P.constant(i)),P.constant(1n+i))),
104	          S.rounds(p,2n+i,P.round(P.round(s,P.constant(i)),P.constant(1n+i))),
105	          S.rounds(p,2n+i,S.round(S.round(s,S.constant(i)),S.constant(1n+i))),
106	          rounds_correct(p,2n+i,P.round(P.round(s,P.constant(i)),P.constant(1n+i))),
107	          Equal.cong(T.State,T.State,t => S.rounds(p,2n+i,t),
108	            P.round(P.round(s,P.constant(i)),P.constant(1n+i)),S.round(S.round(s,S.constant(i)),S.constant(1n+i)),two_correct(i,s))))