@@ -72,47 +72,47 @@ function zvk_maj(x, y, z) = (x & y) ^ (x & z) ^ (y & z)
72
72
* ----------------------------------------------------------------------
73
73
*/
74
74
75
- val P0 : forall 'm, 'm == 32. (bits('m)) -> bits('m)
76
- function P0 (X) = X ^ (X <<< 9) ^ (X <<< 17)
75
+ val zvk_p0 : forall 'm, 'm == 32. (bits('m)) -> bits('m)
76
+ function zvk_p0 (X) = X ^ (X <<< 9) ^ (X <<< 17)
77
77
78
- val P1 : forall 'm, 'm == 32. (bits('m)) -> bits('m)
79
- function P1 (X) = X ^ (X <<< 15) ^ (X <<< 23)
78
+ val zvk_p1 : forall 'm, 'm == 32. (bits('m)) -> bits('m)
79
+ function zvk_p1 (X) = X ^ (X <<< 15) ^ (X <<< 23)
80
80
81
- val ZVKSH_W : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), bits('m), bits('m)) -> bits('m)
82
- function ZVKSH_W (M16, M9, M3, M13, M6) = P1 (M16 ^ M9 ^ (M3 <<< 15)) ^ (M13 <<< 7) ^ M6
81
+ val zvk_sh_w : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), bits('m), bits('m)) -> bits('m)
82
+ function zvk_sh_w (M16, M9, M3, M13, M6) = zvk_p1 (M16 ^ M9 ^ (M3 <<< 15)) ^ (M13 <<< 7) ^ M6
83
83
84
- val FF1 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
85
- function FF1 (X, Y, Z) = X ^ Y ^ Z
84
+ val zvk_ff1 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
85
+ function zvk_ff1 (X, Y, Z) = X ^ Y ^ Z
86
86
87
- val FF2 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
88
- function FF2 (X, Y, Z) = (X & Y) | (X & Z) | (Y & Z)
87
+ val zvk_ff2 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
88
+ function zvk_ff2 (X, Y, Z) = (X & Y) | (X & Z) | (Y & Z)
89
89
90
- val FF_j : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), int) -> bits(32)
91
- function FF_j (X, Y, Z, J) = if (J <= 15) then FF1 (X, Y, Z) else FF2 (X, Y, Z)
90
+ val zvk_ff_j : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), int) -> bits(32)
91
+ function zvk_ff_j (X, Y, Z, J) = if (J <= 15) then zvk_ff1 (X, Y, Z) else zvk_ff2 (X, Y, Z)
92
92
93
- val GG1 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
94
- function GG1 (X, Y, Z) = X ^ Y ^ Z
93
+ val zvk_gg1 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
94
+ function zvk_gg1 (X, Y, Z) = X ^ Y ^ Z
95
95
96
- val GG2 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
97
- function GG2 (X, Y, Z) = (X & Y) | (~(X) & Z)
96
+ val zvk_gg2 : forall 'm, 'm == 32. (bits('m), bits('m), bits('m)) -> bits('m)
97
+ function zvk_gg2 (X, Y, Z) = (X & Y) | (~(X) & Z)
98
98
99
- val GG_j : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), int) -> bits(32)
100
- function GG_j (X, Y, Z, J) = if (J <= 15) then GG1 (X, Y, Z) else GG2 (X, Y, Z)
99
+ val zvk_gg_j : forall 'm, 'm == 32. (bits('m), bits('m), bits('m), int) -> bits(32)
100
+ function zvk_gg_j (X, Y, Z, J) = if (J <= 15) then zvk_gg1 (X, Y, Z) else zvk_gg2 (X, Y, Z)
101
101
102
- val T_j : (int) -> bits(32)
103
- function T_j (J) = if (J <= 15) then 0x79CC4519 else 0x7A879D8A
102
+ val zvk_t_j : (int) -> bits(32)
103
+ function zvk_t_j (J) = if (J <= 15) then 0x79CC4519 else 0x7A879D8A
104
104
105
- function sm3_compression (A_H: vector(8, bits(32)), w : bits(32), x : bits(32), j : int) -> vector(8, bits(32)) = {
106
- let t_j = T_j (j) <<< (j % 32);
105
+ function zvk_sm3_compression (A_H: vector(8, bits(32)), w : bits(32), x : bits(32), j : int) -> vector(8, bits(32)) = {
106
+ let t_j = zvk_t_j (j) <<< (j % 32);
107
107
let ss1 = ((A_H[0] <<< 12) + A_H[4] + t_j) <<< 7;
108
108
let ss2 = ss1 ^ (A_H[0] <<< 12);
109
109
110
- let tt1 = FF_j (A_H[0], A_H[1], A_H[2], j) + A_H[3] + ss2 + x;
111
- let tt2 = GG_j (A_H[4], A_H[5], A_H[6], j) + A_H[7] + ss1 + w;
110
+ let tt1 = zvk_ff_j (A_H[0], A_H[1], A_H[2], j) + A_H[3] + ss2 + x;
111
+ let tt2 = zvk_gg_j (A_H[4], A_H[5], A_H[6], j) + A_H[7] + ss1 + w;
112
112
113
113
let A1 = tt1;
114
114
let C1 = A_H[1] <<< 9;
115
- let E1 = P0 (tt2);
115
+ let E1 = zvk_p0 (tt2);
116
116
let G1 = A_H[5] <<< 19;
117
117
118
118
[ A_H[6], G1, A_H[4], E1, A_H[2], C1, A_H[0], A1 ]
0 commit comments