spec/crypto/keccak/permutation.bend
bend-collections-laws-crypto@1.0.0.0 · 114 lines · 16 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
3
4
5def xor(a: T.Lane, b: T.Lane) -> T.Lane:
6 match a b:
7 case T.W{al,ah} T.W{bl,bh}: T.W{U32.xor(al,bl),U32.xor(ah,bh)}
8
9def chi(a: T.Lane, b: T.Lane, c: T.Lane) -> T.Lane:
10 match a b c:
11 case T.W{al,ah} T.W{bl,bh} T.W{cl,ch}:
12 T.W{U32.xor(al,U32.and(U32.xor(bl,4294967295),cl)),U32.xor(ah,U32.and(U32.xor(bh,4294967295),ch))}
13
14def rotate_small(+lo: U32, +hi: U32, +n: Nat) -> T.Lane:
15 T.W{U32.or(U32.shln(lo,n),U32.shrn(hi,Nat.sub(32n,n))),U32.or(U32.shln(hi,n),U32.shrn(lo,Nat.sub(32n,n)))}
16
17def rotate_nonzero(lo: U32, hi: U32, +n: Nat, b: Bool) -> T.Lane:
18 match b:
19 case True{}: rotate_small(lo,hi,n)
20 case False{}: rotate_small(hi,lo,Nat.sub(n,32n))
21
22def rotate(a: T.Lane, +n: Nat) -> T.Lane:
23 match a n:
24 case T.W{lo,hi} 0n: T.W{lo,hi}
25 case T.W{lo,hi} 32n: T.W{hi,lo}
26 case T.W{lo,hi} n: rotate_nonzero(lo,hi,n,Nat.is_lt(n,32n))
27
28def at(s: T.State, i: Nat) -> T.Lane:
29 match s i:
30 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 0n: a0
31 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 1n: a1
32 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 2n: a2
33 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 3n: a3
34 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 4n: a4
35 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 5n: a5
36 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 6n: a6
37 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 7n: a7
38 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 8n: a8
39 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 9n: a9
40 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 10n: a10
41 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 11n: a11
42 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 12n: a12
43 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 13n: a13
44 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 14n: a14
45 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 15n: a15
46 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 16n: a16
47 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 17n: a17
48 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 18n: a18
49 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 19n: a19
50 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 20n: a20
51 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 21n: a21
52 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 22n: a22
53 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 23n: a23
54 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24} 24n: a24
55 case _ _: T.W{0,0}
56
57def column(+s: T.State, +x: Nat) -> T.Lane:
58 xor(at(s,x),xor(at(s,Nat.add(x,5n)),xor(at(s,Nat.add(x,10n)),xor(at(s,Nat.add(x,15n)),at(s,Nat.add(x,20n))))))
59
60def theta_lane(+s: T.State, +x: Nat, y: Nat) -> T.Lane:
61 xor(at(s,Nat.add(x,Nat.mul(5n,y))),xor(column(s,Nat.mod(Nat.add(x,4n),5n)),rotate(column(s,Nat.mod(Nat.add(x,1n),5n)),1n)))
62
63def theta(+s: T.State) -> T.State:
64 T.S{theta_lane(s,0n,0n),theta_lane(s,1n,0n),theta_lane(s,2n,0n),theta_lane(s,3n,0n),theta_lane(s,4n,0n),theta_lane(s,0n,1n),theta_lane(s,1n,1n),theta_lane(s,2n,1n),theta_lane(s,3n,1n),theta_lane(s,4n,1n),theta_lane(s,0n,2n),theta_lane(s,1n,2n),theta_lane(s,2n,2n),theta_lane(s,3n,2n),theta_lane(s,4n,2n),theta_lane(s,0n,3n),theta_lane(s,1n,3n),theta_lane(s,2n,3n),theta_lane(s,3n,3n),theta_lane(s,4n,3n),theta_lane(s,0n,4n),theta_lane(s,1n,4n),theta_lane(s,2n,4n),theta_lane(s,3n,4n),theta_lane(s,4n,4n)}
65
66def rho_pi(+s: T.State) -> T.State:
67 T.S{rotate(at(s,0n),0n),rotate(at(s,6n),44n),rotate(at(s,12n),43n),rotate(at(s,18n),21n),rotate(at(s,24n),14n),rotate(at(s,3n),28n),rotate(at(s,9n),20n),rotate(at(s,10n),3n),rotate(at(s,16n),45n),rotate(at(s,22n),61n),rotate(at(s,1n),1n),rotate(at(s,7n),6n),rotate(at(s,13n),25n),rotate(at(s,19n),8n),rotate(at(s,20n),18n),rotate(at(s,4n),27n),rotate(at(s,5n),36n),rotate(at(s,11n),10n),rotate(at(s,17n),15n),rotate(at(s,23n),56n),rotate(at(s,2n),62n),rotate(at(s,8n),55n),rotate(at(s,14n),39n),rotate(at(s,15n),41n),rotate(at(s,21n),2n)}
68
69def chi_state(+s: T.State) -> T.State:
70 T.S{chi(at(s,0n),at(s,1n),at(s,2n)),chi(at(s,1n),at(s,2n),at(s,3n)),chi(at(s,2n),at(s,3n),at(s,4n)),chi(at(s,3n),at(s,4n),at(s,0n)),chi(at(s,4n),at(s,0n),at(s,1n)),chi(at(s,5n),at(s,6n),at(s,7n)),chi(at(s,6n),at(s,7n),at(s,8n)),chi(at(s,7n),at(s,8n),at(s,9n)),chi(at(s,8n),at(s,9n),at(s,5n)),chi(at(s,9n),at(s,5n),at(s,6n)),chi(at(s,10n),at(s,11n),at(s,12n)),chi(at(s,11n),at(s,12n),at(s,13n)),chi(at(s,12n),at(s,13n),at(s,14n)),chi(at(s,13n),at(s,14n),at(s,10n)),chi(at(s,14n),at(s,10n),at(s,11n)),chi(at(s,15n),at(s,16n),at(s,17n)),chi(at(s,16n),at(s,17n),at(s,18n)),chi(at(s,17n),at(s,18n),at(s,19n)),chi(at(s,18n),at(s,19n),at(s,15n)),chi(at(s,19n),at(s,15n),at(s,16n)),chi(at(s,20n),at(s,21n),at(s,22n)),chi(at(s,21n),at(s,22n),at(s,23n)),chi(at(s,22n),at(s,23n),at(s,24n)),chi(at(s,23n),at(s,24n),at(s,20n)),chi(at(s,24n),at(s,20n),at(s,21n))}
71
72def iota(s: T.State, rc: T.Lane) -> T.State:
73 match s:
74 case T.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}:
75 T.S{xor(a0,rc),a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24}
76
77def round(s: T.State, rc: T.Lane) -> T.State:
78 iota(chi_state(rho_pi(theta(s))),rc)
79
80def constant(i: Nat) -> T.Lane:
81 match i:
82 case 0n: T.W{1,0}
83 case 1n: T.W{32898,0}
84 case 2n: T.W{32906,2147483648}
85 case 3n: T.W{2147516416,2147483648}
86 case 4n: T.W{32907,0}
87 case 5n: T.W{2147483649,0}
88 case 6n: T.W{2147516545,2147483648}
89 case 7n: T.W{32777,2147483648}
90 case 8n: T.W{138,0}
91 case 9n: T.W{136,0}
92 case 10n: T.W{2147516425,0}
93 case 11n: T.W{2147483658,0}
94 case 12n: T.W{2147516555,0}
95 case 13n: T.W{139,2147483648}
96 case 14n: T.W{32905,2147483648}
97 case 15n: T.W{32771,2147483648}
98 case 16n: T.W{32770,2147483648}
99 case 17n: T.W{128,2147483648}
100 case 18n: T.W{32778,0}
101 case 19n: T.W{2147483658,2147483648}
102 case 20n: T.W{2147516545,2147483648}
103 case 21n: T.W{32896,2147483648}
104 case 22n: T.W{2147483649,0}
105 case 23n: T.W{2147516424,2147483648}
106 case _: T.W{0,0}
107
108def rounds(n: Nat, +i: Nat, s: T.State) -> T.State:
109 match n:
110 case 0n: s
111 case 1n+p: rounds(p,1n+i,round(s,constant(i)))
112
113def permute(s: T.State) -> T.State:
114 rounds(24n,0n,s)