1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
|
// Code generated by fiat.go using fiat-crypto v0.1.4.
//
// Autogenerated: './FiatCrypto_v.0.1.4-issue1672' word-by-word-montgomery --output 'fp128/fiatMont.go' --lang Go --package-name fp128 --doc-prepend-header 'Code generated by fiat.go using fiat-crypto v0.1.4.' --package-case lowerCamelCase --public-function-case lowerCamelCase --public-type-case lowerCamelCase --doc-newline-before-package-declaration --no-primitives --widen-carry --no-field-element-typedefs --relax-primitive-carry-to-bitwidth 64 Fp 64 0xffffffffffffffe40000000000000001 add sub mul square
//
// curve description: Fp
//
// machine_wordsize = 64 (from "64")
//
// requested operations: add, sub, mul, square
//
// m = 0xffffffffffffffe40000000000000001 (from "0xffffffffffffffe40000000000000001")
//
//
//
// NOTE: In addition to the bounds specified above each function, all
//
// functions synthesized for this Montgomery arithmetic require the
//
// input to be strictly less than the prime modulus (m), and also
//
// require the input to be in the unique saturated representation.
//
// All functions also ensure that these two properties are true of
//
// return values.
//
//
//
// Computed values:
//
// eval z = z[0] + (z[1] << 64)
//
// bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120)
//
// twos_complement_eval z = let x1 := z[0] + (z[1] << 64) in
//
// if x1 & (2^128-1) < 2^127 then x1 & (2^128-1) else (x1 & (2^128-1)) - 2^128
package fp128
import "math/bits"
// The function fiatFpAdd adds two field elements in the Montgomery domain.
//
// Preconditions:
// 0 ≤ eval arg1 < m
// 0 ≤ eval arg2 < m
// Postconditions:
// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
// 0 ≤ eval out1 < m
//
// Input Bounds:
// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// Output Bounds:
// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
func fiatFpAdd(out1 *Fp, arg1 *Fp, arg2 *Fp) {
var x1 uint64
var x2 uint64
x1, x2 = bits.Add64(arg1[0], arg2[0], uint64(0x0))
var x3 uint64
var x4 uint64
x3, x4 = bits.Add64(arg1[1], arg2[1], uint64(x2))
var x5 uint64
var x6 uint64
x5, x6 = bits.Sub64(x1, 0x1, uint64(uint64(0x0)))
var x7 uint64
var x8 uint64
x7, x8 = bits.Sub64(x3, 0xffffffffffffffe4, uint64(x6))
var x10 uint64
_, x10 = bits.Sub64(x4, uint64(0x0), uint64(x8))
var x11 uint64
fiatFpCmovznzU64(&x11, x10, x5, x1)
var x12 uint64
fiatFpCmovznzU64(&x12, x10, x7, x3)
out1[0] = x11
out1[1] = x12
}
// The function fiatFpSub subtracts two field elements in the Montgomery domain.
//
// Preconditions:
// 0 ≤ eval arg1 < m
// 0 ≤ eval arg2 < m
// Postconditions:
// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
// 0 ≤ eval out1 < m
//
// Input Bounds:
// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// Output Bounds:
// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
func fiatFpSub(out1 *Fp, arg1 *Fp, arg2 *Fp) {
x1 := arg2[1]
x2 := arg2[0]
var x3 uint64
var x4 uint64
x3, x4 = bits.Sub64(arg1[0], x2, uint64(0x0))
var x5 uint64
var x6 uint64
x5, x6 = bits.Sub64(arg1[1], x1, uint64(x4))
var x7 uint64
fiatFpCmovznzU64(&x7, x6, uint64(0x0), 0xffffffffffffffff)
var x8 uint64
var x9 uint64
x8, x9 = bits.Add64(x3, (x7 & 0x1), uint64(0x0))
var x10 uint64
x10, _ = bits.Add64(x5, (x7 & 0xffffffffffffffe4), uint64(x9))
out1[0] = x8
out1[1] = x10
}
// The function fiatFpMul multiplies two field elements in the Montgomery domain.
//
// Preconditions:
// 0 ≤ eval arg1 < m
// 0 ≤ eval arg2 < m
// Postconditions:
// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
// 0 ≤ eval out1 < m
//
// Input Bounds:
// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// Output Bounds:
// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
func fiatFpMul(out1 *Fp, arg1 *Fp, arg2 *Fp) {
x1 := arg1[1]
x2 := arg1[0]
var x3 uint64
var x4 uint64
x4, x3 = bits.Mul64(x2, arg2[1])
var x5 uint64
var x6 uint64
x6, x5 = bits.Mul64(x2, arg2[0])
var x7 uint64
var x8 uint64
x7, x8 = bits.Add64(x6, x3, uint64(0x0))
x9 := (x8 + x4)
var x10 uint64
_, x10 = bits.Mul64(x5, 0xffffffffffffffff)
var x12 uint64
var x13 uint64
x13, x12 = bits.Mul64(x10, 0xffffffffffffffe4)
var x15 uint64
_, x15 = bits.Add64(x5, x10, uint64(0x0))
var x16 uint64
var x17 uint64
x16, x17 = bits.Add64(x7, x12, uint64(x15))
var x18 uint64
var x19 uint64
x18, x19 = bits.Add64(x9, x13, uint64(x17))
var x20 uint64
var x21 uint64
x21, x20 = bits.Mul64(x1, arg2[1])
var x22 uint64
var x23 uint64
x23, x22 = bits.Mul64(x1, arg2[0])
var x24 uint64
var x25 uint64
x24, x25 = bits.Add64(x23, x20, uint64(0x0))
x26 := (x25 + x21)
var x27 uint64
var x28 uint64
x27, x28 = bits.Add64(x16, x22, uint64(0x0))
var x29 uint64
var x30 uint64
x29, x30 = bits.Add64(x18, x24, uint64(x28))
var x31 uint64
var x32 uint64
x31, x32 = bits.Add64(x19, x26, uint64(x30))
var x33 uint64
_, x33 = bits.Mul64(x27, 0xffffffffffffffff)
var x35 uint64
var x36 uint64
x36, x35 = bits.Mul64(x33, 0xffffffffffffffe4)
var x38 uint64
_, x38 = bits.Add64(x27, x33, uint64(0x0))
var x39 uint64
var x40 uint64
x39, x40 = bits.Add64(x29, x35, uint64(x38))
var x41 uint64
var x42 uint64
x41, x42 = bits.Add64(x31, x36, uint64(x40))
x43 := (x42 + x32)
var x44 uint64
var x45 uint64
x44, x45 = bits.Sub64(x39, 0x1, uint64(uint64(0x0)))
var x46 uint64
var x47 uint64
x46, x47 = bits.Sub64(x41, 0xffffffffffffffe4, uint64(x45))
var x49 uint64
_, x49 = bits.Sub64(x43, uint64(0x0), uint64(x47))
var x50 uint64
fiatFpCmovznzU64(&x50, x49, x44, x39)
var x51 uint64
fiatFpCmovznzU64(&x51, x49, x46, x41)
out1[0] = x50
out1[1] = x51
}
// The function fiatFpSquare squares a field element in the Montgomery domain.
//
// Preconditions:
// 0 ≤ eval arg1 < m
// Postconditions:
// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
// 0 ≤ eval out1 < m
//
// Input Bounds:
// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// Output Bounds:
// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
func fiatFpSquare(out1 *Fp, arg1 *Fp) {
x1 := arg1[1]
x2 := arg1[0]
var x3 uint64
var x4 uint64
x4, x3 = bits.Mul64(x2, arg1[1])
var x5 uint64
var x6 uint64
x6, x5 = bits.Mul64(x2, arg1[0])
var x7 uint64
var x8 uint64
x7, x8 = bits.Add64(x6, x3, uint64(0x0))
x9 := (x8 + x4)
var x10 uint64
_, x10 = bits.Mul64(x5, 0xffffffffffffffff)
var x12 uint64
var x13 uint64
x13, x12 = bits.Mul64(x10, 0xffffffffffffffe4)
var x15 uint64
_, x15 = bits.Add64(x5, x10, uint64(0x0))
var x16 uint64
var x17 uint64
x16, x17 = bits.Add64(x7, x12, uint64(x15))
var x18 uint64
var x19 uint64
x18, x19 = bits.Add64(x9, x13, uint64(x17))
var x20 uint64
var x21 uint64
x21, x20 = bits.Mul64(x1, arg1[1])
var x22 uint64
var x23 uint64
x23, x22 = bits.Mul64(x1, arg1[0])
var x24 uint64
var x25 uint64
x24, x25 = bits.Add64(x23, x20, uint64(0x0))
x26 := (x25 + x21)
var x27 uint64
var x28 uint64
x27, x28 = bits.Add64(x16, x22, uint64(0x0))
var x29 uint64
var x30 uint64
x29, x30 = bits.Add64(x18, x24, uint64(x28))
var x31 uint64
var x32 uint64
x31, x32 = bits.Add64(x19, x26, uint64(x30))
var x33 uint64
_, x33 = bits.Mul64(x27, 0xffffffffffffffff)
var x35 uint64
var x36 uint64
x36, x35 = bits.Mul64(x33, 0xffffffffffffffe4)
var x38 uint64
_, x38 = bits.Add64(x27, x33, uint64(0x0))
var x39 uint64
var x40 uint64
x39, x40 = bits.Add64(x29, x35, uint64(x38))
var x41 uint64
var x42 uint64
x41, x42 = bits.Add64(x31, x36, uint64(x40))
x43 := (x42 + x32)
var x44 uint64
var x45 uint64
x44, x45 = bits.Sub64(x39, 0x1, uint64(uint64(0x0)))
var x46 uint64
var x47 uint64
x46, x47 = bits.Sub64(x41, 0xffffffffffffffe4, uint64(x45))
var x49 uint64
_, x49 = bits.Sub64(x43, uint64(0x0), uint64(x47))
var x50 uint64
fiatFpCmovznzU64(&x50, x49, x44, x39)
var x51 uint64
fiatFpCmovznzU64(&x51, x49, x46, x41)
out1[0] = x50
out1[1] = x51
}
|
