proofs/crypto/keccak/permutation.bend
bend-collections-laws-crypto@1.0.0.0 · 108 lines · 7 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as S
5
6law round_correct:
7 for +s: T.State
8 for +rc: T.Lane
9 {P.round(s,rc) == S.round(s,rc) : T.State}
10
11def 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
15law constants_correct:
16 for +n: Nat
17 {P.constant(n) == S.constant(n) : T.Lane}
18
19def 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
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}
53
54def 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
58law 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
63def single_step(i,s):
64 {==}
65
66law 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
71def 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
76law 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
81def 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
89law 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
95def 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))))