]>
Commit | Line | Data |
---|---|---|
0a29b90c FG |
1 | //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p448 32 16 '2^448 - 2^224 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax |
2 | //! curve description: p448 | |
3 | //! machine_wordsize = 32 (from "32") | |
4 | //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax | |
5 | //! n = 16 (from "16") | |
6 | //! s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1") | |
7 | //! tight_bounds_multiplier = 1 (from "") | |
8 | //! | |
9 | //! Computed values: | |
10 | //! carry_chain = [7, 15, 8, 0, 9, 1, 10, 2, 11, 3, 12, 4, 13, 5, 14, 6, 15, 7, 8, 0] | |
11 | //! eval z = z[0] + (z[1] << 28) + (z[2] << 56) + (z[3] << 84) + (z[4] << 112) + (z[5] << 140) + (z[6] << 168) + (z[7] << 196) + (z[8] << 224) + (z[9] << 252) + (z[10] << 0x118) + (z[11] << 0x134) + (z[12] << 0x150) + (z[13] << 0x16c) + (z[14] << 0x188) + (z[15] << 0x1a4) | |
12 | //! 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) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) | |
13 | //! balance = [0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffc, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe] | |
14 | ||
15 | #![allow(unused_parens)] | |
16 | #![allow(non_camel_case_types)] | |
17 | ||
18 | pub type fiat_p448_u1 = u8; | |
19 | pub type fiat_p448_i1 = i8; | |
20 | pub type fiat_p448_u2 = u8; | |
21 | pub type fiat_p448_i2 = i8; | |
22 | ||
23 | /* The type fiat_p448_loose_field_element is a field element with loose bounds. */ | |
24 | /* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]] */ | |
25 | pub type fiat_p448_loose_field_element = [u32; 16]; | |
26 | ||
27 | /* The type fiat_p448_tight_field_element is a field element with tight bounds. */ | |
28 | /* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]] */ | |
29 | pub type fiat_p448_tight_field_element = [u32; 16]; | |
30 | ||
31 | ||
32 | /// The function fiat_p448_addcarryx_u28 is an addition with carry. | |
33 | /// | |
34 | /// Postconditions: | |
35 | /// out1 = (arg1 + arg2 + arg3) mod 2^28 | |
36 | /// out2 = ⌊(arg1 + arg2 + arg3) / 2^28⌋ | |
37 | /// | |
38 | /// Input Bounds: | |
39 | /// arg1: [0x0 ~> 0x1] | |
40 | /// arg2: [0x0 ~> 0xfffffff] | |
41 | /// arg3: [0x0 ~> 0xfffffff] | |
42 | /// Output Bounds: | |
43 | /// out1: [0x0 ~> 0xfffffff] | |
44 | /// out2: [0x0 ~> 0x1] | |
45 | #[inline] | |
46 | pub fn fiat_p448_addcarryx_u28(out1: &mut u32, out2: &mut fiat_p448_u1, arg1: fiat_p448_u1, arg2: u32, arg3: u32) -> () { | |
47 | let x1: u32 = (((arg1 as u32) + arg2) + arg3); | |
48 | let x2: u32 = (x1 & 0xfffffff); | |
49 | let x3: fiat_p448_u1 = ((x1 >> 28) as fiat_p448_u1); | |
50 | *out1 = x2; | |
51 | *out2 = x3; | |
52 | } | |
53 | ||
54 | /// The function fiat_p448_subborrowx_u28 is a subtraction with borrow. | |
55 | /// | |
56 | /// Postconditions: | |
57 | /// out1 = (-arg1 + arg2 + -arg3) mod 2^28 | |
58 | /// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^28⌋ | |
59 | /// | |
60 | /// Input Bounds: | |
61 | /// arg1: [0x0 ~> 0x1] | |
62 | /// arg2: [0x0 ~> 0xfffffff] | |
63 | /// arg3: [0x0 ~> 0xfffffff] | |
64 | /// Output Bounds: | |
65 | /// out1: [0x0 ~> 0xfffffff] | |
66 | /// out2: [0x0 ~> 0x1] | |
67 | #[inline] | |
68 | pub fn fiat_p448_subborrowx_u28(out1: &mut u32, out2: &mut fiat_p448_u1, arg1: fiat_p448_u1, arg2: u32, arg3: u32) -> () { | |
69 | let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32); | |
70 | let x2: fiat_p448_i1 = ((x1 >> 28) as fiat_p448_i1); | |
71 | let x3: u32 = (((x1 as i64) & (0xfffffff as i64)) as u32); | |
72 | *out1 = x3; | |
73 | *out2 = (((0x0 as fiat_p448_i2) - (x2 as fiat_p448_i2)) as fiat_p448_u1); | |
74 | } | |
75 | ||
76 | /// The function fiat_p448_cmovznz_u32 is a single-word conditional move. | |
77 | /// | |
78 | /// Postconditions: | |
79 | /// out1 = (if arg1 = 0 then arg2 else arg3) | |
80 | /// | |
81 | /// Input Bounds: | |
82 | /// arg1: [0x0 ~> 0x1] | |
83 | /// arg2: [0x0 ~> 0xffffffff] | |
84 | /// arg3: [0x0 ~> 0xffffffff] | |
85 | /// Output Bounds: | |
86 | /// out1: [0x0 ~> 0xffffffff] | |
87 | #[inline] | |
88 | pub fn fiat_p448_cmovznz_u32(out1: &mut u32, arg1: fiat_p448_u1, arg2: u32, arg3: u32) -> () { | |
89 | let x1: fiat_p448_u1 = (!(!arg1)); | |
90 | let x2: u32 = ((((((0x0 as fiat_p448_i2) - (x1 as fiat_p448_i2)) as fiat_p448_i1) as i64) & (0xffffffff as i64)) as u32); | |
91 | let x3: u32 = ((x2 & arg3) | ((!x2) & arg2)); | |
92 | *out1 = x3; | |
93 | } | |
94 | ||
95 | /// The function fiat_p448_carry_mul multiplies two field elements and reduces the result. | |
96 | /// | |
97 | /// Postconditions: | |
98 | /// eval out1 mod m = (eval arg1 * eval arg2) mod m | |
99 | /// | |
100 | #[inline] | |
101 | pub fn fiat_p448_carry_mul(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element, arg2: &fiat_p448_loose_field_element) -> () { | |
102 | let x1: u64 = (((arg1[15]) as u64) * ((arg2[15]) as u64)); | |
103 | let x2: u64 = (((arg1[15]) as u64) * ((arg2[14]) as u64)); | |
104 | let x3: u64 = (((arg1[15]) as u64) * ((arg2[13]) as u64)); | |
105 | let x4: u64 = (((arg1[15]) as u64) * ((arg2[12]) as u64)); | |
106 | let x5: u64 = (((arg1[15]) as u64) * ((arg2[11]) as u64)); | |
107 | let x6: u64 = (((arg1[15]) as u64) * ((arg2[10]) as u64)); | |
108 | let x7: u64 = (((arg1[15]) as u64) * ((arg2[9]) as u64)); | |
109 | let x8: u64 = (((arg1[14]) as u64) * ((arg2[15]) as u64)); | |
110 | let x9: u64 = (((arg1[14]) as u64) * ((arg2[14]) as u64)); | |
111 | let x10: u64 = (((arg1[14]) as u64) * ((arg2[13]) as u64)); | |
112 | let x11: u64 = (((arg1[14]) as u64) * ((arg2[12]) as u64)); | |
113 | let x12: u64 = (((arg1[14]) as u64) * ((arg2[11]) as u64)); | |
114 | let x13: u64 = (((arg1[14]) as u64) * ((arg2[10]) as u64)); | |
115 | let x14: u64 = (((arg1[13]) as u64) * ((arg2[15]) as u64)); | |
116 | let x15: u64 = (((arg1[13]) as u64) * ((arg2[14]) as u64)); | |
117 | let x16: u64 = (((arg1[13]) as u64) * ((arg2[13]) as u64)); | |
118 | let x17: u64 = (((arg1[13]) as u64) * ((arg2[12]) as u64)); | |
119 | let x18: u64 = (((arg1[13]) as u64) * ((arg2[11]) as u64)); | |
120 | let x19: u64 = (((arg1[12]) as u64) * ((arg2[15]) as u64)); | |
121 | let x20: u64 = (((arg1[12]) as u64) * ((arg2[14]) as u64)); | |
122 | let x21: u64 = (((arg1[12]) as u64) * ((arg2[13]) as u64)); | |
123 | let x22: u64 = (((arg1[12]) as u64) * ((arg2[12]) as u64)); | |
124 | let x23: u64 = (((arg1[11]) as u64) * ((arg2[15]) as u64)); | |
125 | let x24: u64 = (((arg1[11]) as u64) * ((arg2[14]) as u64)); | |
126 | let x25: u64 = (((arg1[11]) as u64) * ((arg2[13]) as u64)); | |
127 | let x26: u64 = (((arg1[10]) as u64) * ((arg2[15]) as u64)); | |
128 | let x27: u64 = (((arg1[10]) as u64) * ((arg2[14]) as u64)); | |
129 | let x28: u64 = (((arg1[9]) as u64) * ((arg2[15]) as u64)); | |
130 | let x29: u64 = (((arg1[15]) as u64) * ((arg2[15]) as u64)); | |
131 | let x30: u64 = (((arg1[15]) as u64) * ((arg2[14]) as u64)); | |
132 | let x31: u64 = (((arg1[15]) as u64) * ((arg2[13]) as u64)); | |
133 | let x32: u64 = (((arg1[15]) as u64) * ((arg2[12]) as u64)); | |
134 | let x33: u64 = (((arg1[15]) as u64) * ((arg2[11]) as u64)); | |
135 | let x34: u64 = (((arg1[15]) as u64) * ((arg2[10]) as u64)); | |
136 | let x35: u64 = (((arg1[15]) as u64) * ((arg2[9]) as u64)); | |
137 | let x36: u64 = (((arg1[14]) as u64) * ((arg2[15]) as u64)); | |
138 | let x37: u64 = (((arg1[14]) as u64) * ((arg2[14]) as u64)); | |
139 | let x38: u64 = (((arg1[14]) as u64) * ((arg2[13]) as u64)); | |
140 | let x39: u64 = (((arg1[14]) as u64) * ((arg2[12]) as u64)); | |
141 | let x40: u64 = (((arg1[14]) as u64) * ((arg2[11]) as u64)); | |
142 | let x41: u64 = (((arg1[14]) as u64) * ((arg2[10]) as u64)); | |
143 | let x42: u64 = (((arg1[13]) as u64) * ((arg2[15]) as u64)); | |
144 | let x43: u64 = (((arg1[13]) as u64) * ((arg2[14]) as u64)); | |
145 | let x44: u64 = (((arg1[13]) as u64) * ((arg2[13]) as u64)); | |
146 | let x45: u64 = (((arg1[13]) as u64) * ((arg2[12]) as u64)); | |
147 | let x46: u64 = (((arg1[13]) as u64) * ((arg2[11]) as u64)); | |
148 | let x47: u64 = (((arg1[12]) as u64) * ((arg2[15]) as u64)); | |
149 | let x48: u64 = (((arg1[12]) as u64) * ((arg2[14]) as u64)); | |
150 | let x49: u64 = (((arg1[12]) as u64) * ((arg2[13]) as u64)); | |
151 | let x50: u64 = (((arg1[12]) as u64) * ((arg2[12]) as u64)); | |
152 | let x51: u64 = (((arg1[11]) as u64) * ((arg2[15]) as u64)); | |
153 | let x52: u64 = (((arg1[11]) as u64) * ((arg2[14]) as u64)); | |
154 | let x53: u64 = (((arg1[11]) as u64) * ((arg2[13]) as u64)); | |
155 | let x54: u64 = (((arg1[10]) as u64) * ((arg2[15]) as u64)); | |
156 | let x55: u64 = (((arg1[10]) as u64) * ((arg2[14]) as u64)); | |
157 | let x56: u64 = (((arg1[9]) as u64) * ((arg2[15]) as u64)); | |
158 | let x57: u64 = (((arg1[15]) as u64) * ((arg2[15]) as u64)); | |
159 | let x58: u64 = (((arg1[15]) as u64) * ((arg2[14]) as u64)); | |
160 | let x59: u64 = (((arg1[15]) as u64) * ((arg2[13]) as u64)); | |
161 | let x60: u64 = (((arg1[15]) as u64) * ((arg2[12]) as u64)); | |
162 | let x61: u64 = (((arg1[15]) as u64) * ((arg2[11]) as u64)); | |
163 | let x62: u64 = (((arg1[15]) as u64) * ((arg2[10]) as u64)); | |
164 | let x63: u64 = (((arg1[15]) as u64) * ((arg2[9]) as u64)); | |
165 | let x64: u64 = (((arg1[15]) as u64) * ((arg2[8]) as u64)); | |
166 | let x65: u64 = (((arg1[15]) as u64) * ((arg2[7]) as u64)); | |
167 | let x66: u64 = (((arg1[15]) as u64) * ((arg2[6]) as u64)); | |
168 | let x67: u64 = (((arg1[15]) as u64) * ((arg2[5]) as u64)); | |
169 | let x68: u64 = (((arg1[15]) as u64) * ((arg2[4]) as u64)); | |
170 | let x69: u64 = (((arg1[15]) as u64) * ((arg2[3]) as u64)); | |
171 | let x70: u64 = (((arg1[15]) as u64) * ((arg2[2]) as u64)); | |
172 | let x71: u64 = (((arg1[15]) as u64) * ((arg2[1]) as u64)); | |
173 | let x72: u64 = (((arg1[14]) as u64) * ((arg2[15]) as u64)); | |
174 | let x73: u64 = (((arg1[14]) as u64) * ((arg2[14]) as u64)); | |
175 | let x74: u64 = (((arg1[14]) as u64) * ((arg2[13]) as u64)); | |
176 | let x75: u64 = (((arg1[14]) as u64) * ((arg2[12]) as u64)); | |
177 | let x76: u64 = (((arg1[14]) as u64) * ((arg2[11]) as u64)); | |
178 | let x77: u64 = (((arg1[14]) as u64) * ((arg2[10]) as u64)); | |
179 | let x78: u64 = (((arg1[14]) as u64) * ((arg2[9]) as u64)); | |
180 | let x79: u64 = (((arg1[14]) as u64) * ((arg2[8]) as u64)); | |
181 | let x80: u64 = (((arg1[14]) as u64) * ((arg2[7]) as u64)); | |
182 | let x81: u64 = (((arg1[14]) as u64) * ((arg2[6]) as u64)); | |
183 | let x82: u64 = (((arg1[14]) as u64) * ((arg2[5]) as u64)); | |
184 | let x83: u64 = (((arg1[14]) as u64) * ((arg2[4]) as u64)); | |
185 | let x84: u64 = (((arg1[14]) as u64) * ((arg2[3]) as u64)); | |
186 | let x85: u64 = (((arg1[14]) as u64) * ((arg2[2]) as u64)); | |
187 | let x86: u64 = (((arg1[13]) as u64) * ((arg2[15]) as u64)); | |
188 | let x87: u64 = (((arg1[13]) as u64) * ((arg2[14]) as u64)); | |
189 | let x88: u64 = (((arg1[13]) as u64) * ((arg2[13]) as u64)); | |
190 | let x89: u64 = (((arg1[13]) as u64) * ((arg2[12]) as u64)); | |
191 | let x90: u64 = (((arg1[13]) as u64) * ((arg2[11]) as u64)); | |
192 | let x91: u64 = (((arg1[13]) as u64) * ((arg2[10]) as u64)); | |
193 | let x92: u64 = (((arg1[13]) as u64) * ((arg2[9]) as u64)); | |
194 | let x93: u64 = (((arg1[13]) as u64) * ((arg2[8]) as u64)); | |
195 | let x94: u64 = (((arg1[13]) as u64) * ((arg2[7]) as u64)); | |
196 | let x95: u64 = (((arg1[13]) as u64) * ((arg2[6]) as u64)); | |
197 | let x96: u64 = (((arg1[13]) as u64) * ((arg2[5]) as u64)); | |
198 | let x97: u64 = (((arg1[13]) as u64) * ((arg2[4]) as u64)); | |
199 | let x98: u64 = (((arg1[13]) as u64) * ((arg2[3]) as u64)); | |
200 | let x99: u64 = (((arg1[12]) as u64) * ((arg2[15]) as u64)); | |
201 | let x100: u64 = (((arg1[12]) as u64) * ((arg2[14]) as u64)); | |
202 | let x101: u64 = (((arg1[12]) as u64) * ((arg2[13]) as u64)); | |
203 | let x102: u64 = (((arg1[12]) as u64) * ((arg2[12]) as u64)); | |
204 | let x103: u64 = (((arg1[12]) as u64) * ((arg2[11]) as u64)); | |
205 | let x104: u64 = (((arg1[12]) as u64) * ((arg2[10]) as u64)); | |
206 | let x105: u64 = (((arg1[12]) as u64) * ((arg2[9]) as u64)); | |
207 | let x106: u64 = (((arg1[12]) as u64) * ((arg2[8]) as u64)); | |
208 | let x107: u64 = (((arg1[12]) as u64) * ((arg2[7]) as u64)); | |
209 | let x108: u64 = (((arg1[12]) as u64) * ((arg2[6]) as u64)); | |
210 | let x109: u64 = (((arg1[12]) as u64) * ((arg2[5]) as u64)); | |
211 | let x110: u64 = (((arg1[12]) as u64) * ((arg2[4]) as u64)); | |
212 | let x111: u64 = (((arg1[11]) as u64) * ((arg2[15]) as u64)); | |
213 | let x112: u64 = (((arg1[11]) as u64) * ((arg2[14]) as u64)); | |
214 | let x113: u64 = (((arg1[11]) as u64) * ((arg2[13]) as u64)); | |
215 | let x114: u64 = (((arg1[11]) as u64) * ((arg2[12]) as u64)); | |
216 | let x115: u64 = (((arg1[11]) as u64) * ((arg2[11]) as u64)); | |
217 | let x116: u64 = (((arg1[11]) as u64) * ((arg2[10]) as u64)); | |
218 | let x117: u64 = (((arg1[11]) as u64) * ((arg2[9]) as u64)); | |
219 | let x118: u64 = (((arg1[11]) as u64) * ((arg2[8]) as u64)); | |
220 | let x119: u64 = (((arg1[11]) as u64) * ((arg2[7]) as u64)); | |
221 | let x120: u64 = (((arg1[11]) as u64) * ((arg2[6]) as u64)); | |
222 | let x121: u64 = (((arg1[11]) as u64) * ((arg2[5]) as u64)); | |
223 | let x122: u64 = (((arg1[10]) as u64) * ((arg2[15]) as u64)); | |
224 | let x123: u64 = (((arg1[10]) as u64) * ((arg2[14]) as u64)); | |
225 | let x124: u64 = (((arg1[10]) as u64) * ((arg2[13]) as u64)); | |
226 | let x125: u64 = (((arg1[10]) as u64) * ((arg2[12]) as u64)); | |
227 | let x126: u64 = (((arg1[10]) as u64) * ((arg2[11]) as u64)); | |
228 | let x127: u64 = (((arg1[10]) as u64) * ((arg2[10]) as u64)); | |
229 | let x128: u64 = (((arg1[10]) as u64) * ((arg2[9]) as u64)); | |
230 | let x129: u64 = (((arg1[10]) as u64) * ((arg2[8]) as u64)); | |
231 | let x130: u64 = (((arg1[10]) as u64) * ((arg2[7]) as u64)); | |
232 | let x131: u64 = (((arg1[10]) as u64) * ((arg2[6]) as u64)); | |
233 | let x132: u64 = (((arg1[9]) as u64) * ((arg2[15]) as u64)); | |
234 | let x133: u64 = (((arg1[9]) as u64) * ((arg2[14]) as u64)); | |
235 | let x134: u64 = (((arg1[9]) as u64) * ((arg2[13]) as u64)); | |
236 | let x135: u64 = (((arg1[9]) as u64) * ((arg2[12]) as u64)); | |
237 | let x136: u64 = (((arg1[9]) as u64) * ((arg2[11]) as u64)); | |
238 | let x137: u64 = (((arg1[9]) as u64) * ((arg2[10]) as u64)); | |
239 | let x138: u64 = (((arg1[9]) as u64) * ((arg2[9]) as u64)); | |
240 | let x139: u64 = (((arg1[9]) as u64) * ((arg2[8]) as u64)); | |
241 | let x140: u64 = (((arg1[9]) as u64) * ((arg2[7]) as u64)); | |
242 | let x141: u64 = (((arg1[8]) as u64) * ((arg2[15]) as u64)); | |
243 | let x142: u64 = (((arg1[8]) as u64) * ((arg2[14]) as u64)); | |
244 | let x143: u64 = (((arg1[8]) as u64) * ((arg2[13]) as u64)); | |
245 | let x144: u64 = (((arg1[8]) as u64) * ((arg2[12]) as u64)); | |
246 | let x145: u64 = (((arg1[8]) as u64) * ((arg2[11]) as u64)); | |
247 | let x146: u64 = (((arg1[8]) as u64) * ((arg2[10]) as u64)); | |
248 | let x147: u64 = (((arg1[8]) as u64) * ((arg2[9]) as u64)); | |
249 | let x148: u64 = (((arg1[8]) as u64) * ((arg2[8]) as u64)); | |
250 | let x149: u64 = (((arg1[7]) as u64) * ((arg2[15]) as u64)); | |
251 | let x150: u64 = (((arg1[7]) as u64) * ((arg2[14]) as u64)); | |
252 | let x151: u64 = (((arg1[7]) as u64) * ((arg2[13]) as u64)); | |
253 | let x152: u64 = (((arg1[7]) as u64) * ((arg2[12]) as u64)); | |
254 | let x153: u64 = (((arg1[7]) as u64) * ((arg2[11]) as u64)); | |
255 | let x154: u64 = (((arg1[7]) as u64) * ((arg2[10]) as u64)); | |
256 | let x155: u64 = (((arg1[7]) as u64) * ((arg2[9]) as u64)); | |
257 | let x156: u64 = (((arg1[6]) as u64) * ((arg2[15]) as u64)); | |
258 | let x157: u64 = (((arg1[6]) as u64) * ((arg2[14]) as u64)); | |
259 | let x158: u64 = (((arg1[6]) as u64) * ((arg2[13]) as u64)); | |
260 | let x159: u64 = (((arg1[6]) as u64) * ((arg2[12]) as u64)); | |
261 | let x160: u64 = (((arg1[6]) as u64) * ((arg2[11]) as u64)); | |
262 | let x161: u64 = (((arg1[6]) as u64) * ((arg2[10]) as u64)); | |
263 | let x162: u64 = (((arg1[5]) as u64) * ((arg2[15]) as u64)); | |
264 | let x163: u64 = (((arg1[5]) as u64) * ((arg2[14]) as u64)); | |
265 | let x164: u64 = (((arg1[5]) as u64) * ((arg2[13]) as u64)); | |
266 | let x165: u64 = (((arg1[5]) as u64) * ((arg2[12]) as u64)); | |
267 | let x166: u64 = (((arg1[5]) as u64) * ((arg2[11]) as u64)); | |
268 | let x167: u64 = (((arg1[4]) as u64) * ((arg2[15]) as u64)); | |
269 | let x168: u64 = (((arg1[4]) as u64) * ((arg2[14]) as u64)); | |
270 | let x169: u64 = (((arg1[4]) as u64) * ((arg2[13]) as u64)); | |
271 | let x170: u64 = (((arg1[4]) as u64) * ((arg2[12]) as u64)); | |
272 | let x171: u64 = (((arg1[3]) as u64) * ((arg2[15]) as u64)); | |
273 | let x172: u64 = (((arg1[3]) as u64) * ((arg2[14]) as u64)); | |
274 | let x173: u64 = (((arg1[3]) as u64) * ((arg2[13]) as u64)); | |
275 | let x174: u64 = (((arg1[2]) as u64) * ((arg2[15]) as u64)); | |
276 | let x175: u64 = (((arg1[2]) as u64) * ((arg2[14]) as u64)); | |
277 | let x176: u64 = (((arg1[1]) as u64) * ((arg2[15]) as u64)); | |
278 | let x177: u64 = (((arg1[15]) as u64) * ((arg2[8]) as u64)); | |
279 | let x178: u64 = (((arg1[15]) as u64) * ((arg2[7]) as u64)); | |
280 | let x179: u64 = (((arg1[15]) as u64) * ((arg2[6]) as u64)); | |
281 | let x180: u64 = (((arg1[15]) as u64) * ((arg2[5]) as u64)); | |
282 | let x181: u64 = (((arg1[15]) as u64) * ((arg2[4]) as u64)); | |
283 | let x182: u64 = (((arg1[15]) as u64) * ((arg2[3]) as u64)); | |
284 | let x183: u64 = (((arg1[15]) as u64) * ((arg2[2]) as u64)); | |
285 | let x184: u64 = (((arg1[15]) as u64) * ((arg2[1]) as u64)); | |
286 | let x185: u64 = (((arg1[14]) as u64) * ((arg2[9]) as u64)); | |
287 | let x186: u64 = (((arg1[14]) as u64) * ((arg2[8]) as u64)); | |
288 | let x187: u64 = (((arg1[14]) as u64) * ((arg2[7]) as u64)); | |
289 | let x188: u64 = (((arg1[14]) as u64) * ((arg2[6]) as u64)); | |
290 | let x189: u64 = (((arg1[14]) as u64) * ((arg2[5]) as u64)); | |
291 | let x190: u64 = (((arg1[14]) as u64) * ((arg2[4]) as u64)); | |
292 | let x191: u64 = (((arg1[14]) as u64) * ((arg2[3]) as u64)); | |
293 | let x192: u64 = (((arg1[14]) as u64) * ((arg2[2]) as u64)); | |
294 | let x193: u64 = (((arg1[13]) as u64) * ((arg2[10]) as u64)); | |
295 | let x194: u64 = (((arg1[13]) as u64) * ((arg2[9]) as u64)); | |
296 | let x195: u64 = (((arg1[13]) as u64) * ((arg2[8]) as u64)); | |
297 | let x196: u64 = (((arg1[13]) as u64) * ((arg2[7]) as u64)); | |
298 | let x197: u64 = (((arg1[13]) as u64) * ((arg2[6]) as u64)); | |
299 | let x198: u64 = (((arg1[13]) as u64) * ((arg2[5]) as u64)); | |
300 | let x199: u64 = (((arg1[13]) as u64) * ((arg2[4]) as u64)); | |
301 | let x200: u64 = (((arg1[13]) as u64) * ((arg2[3]) as u64)); | |
302 | let x201: u64 = (((arg1[12]) as u64) * ((arg2[11]) as u64)); | |
303 | let x202: u64 = (((arg1[12]) as u64) * ((arg2[10]) as u64)); | |
304 | let x203: u64 = (((arg1[12]) as u64) * ((arg2[9]) as u64)); | |
305 | let x204: u64 = (((arg1[12]) as u64) * ((arg2[8]) as u64)); | |
306 | let x205: u64 = (((arg1[12]) as u64) * ((arg2[7]) as u64)); | |
307 | let x206: u64 = (((arg1[12]) as u64) * ((arg2[6]) as u64)); | |
308 | let x207: u64 = (((arg1[12]) as u64) * ((arg2[5]) as u64)); | |
309 | let x208: u64 = (((arg1[12]) as u64) * ((arg2[4]) as u64)); | |
310 | let x209: u64 = (((arg1[11]) as u64) * ((arg2[12]) as u64)); | |
311 | let x210: u64 = (((arg1[11]) as u64) * ((arg2[11]) as u64)); | |
312 | let x211: u64 = (((arg1[11]) as u64) * ((arg2[10]) as u64)); | |
313 | let x212: u64 = (((arg1[11]) as u64) * ((arg2[9]) as u64)); | |
314 | let x213: u64 = (((arg1[11]) as u64) * ((arg2[8]) as u64)); | |
315 | let x214: u64 = (((arg1[11]) as u64) * ((arg2[7]) as u64)); | |
316 | let x215: u64 = (((arg1[11]) as u64) * ((arg2[6]) as u64)); | |
317 | let x216: u64 = (((arg1[11]) as u64) * ((arg2[5]) as u64)); | |
318 | let x217: u64 = (((arg1[10]) as u64) * ((arg2[13]) as u64)); | |
319 | let x218: u64 = (((arg1[10]) as u64) * ((arg2[12]) as u64)); | |
320 | let x219: u64 = (((arg1[10]) as u64) * ((arg2[11]) as u64)); | |
321 | let x220: u64 = (((arg1[10]) as u64) * ((arg2[10]) as u64)); | |
322 | let x221: u64 = (((arg1[10]) as u64) * ((arg2[9]) as u64)); | |
323 | let x222: u64 = (((arg1[10]) as u64) * ((arg2[8]) as u64)); | |
324 | let x223: u64 = (((arg1[10]) as u64) * ((arg2[7]) as u64)); | |
325 | let x224: u64 = (((arg1[10]) as u64) * ((arg2[6]) as u64)); | |
326 | let x225: u64 = (((arg1[9]) as u64) * ((arg2[14]) as u64)); | |
327 | let x226: u64 = (((arg1[9]) as u64) * ((arg2[13]) as u64)); | |
328 | let x227: u64 = (((arg1[9]) as u64) * ((arg2[12]) as u64)); | |
329 | let x228: u64 = (((arg1[9]) as u64) * ((arg2[11]) as u64)); | |
330 | let x229: u64 = (((arg1[9]) as u64) * ((arg2[10]) as u64)); | |
331 | let x230: u64 = (((arg1[9]) as u64) * ((arg2[9]) as u64)); | |
332 | let x231: u64 = (((arg1[9]) as u64) * ((arg2[8]) as u64)); | |
333 | let x232: u64 = (((arg1[9]) as u64) * ((arg2[7]) as u64)); | |
334 | let x233: u64 = (((arg1[8]) as u64) * ((arg2[15]) as u64)); | |
335 | let x234: u64 = (((arg1[8]) as u64) * ((arg2[14]) as u64)); | |
336 | let x235: u64 = (((arg1[8]) as u64) * ((arg2[13]) as u64)); | |
337 | let x236: u64 = (((arg1[8]) as u64) * ((arg2[12]) as u64)); | |
338 | let x237: u64 = (((arg1[8]) as u64) * ((arg2[11]) as u64)); | |
339 | let x238: u64 = (((arg1[8]) as u64) * ((arg2[10]) as u64)); | |
340 | let x239: u64 = (((arg1[8]) as u64) * ((arg2[9]) as u64)); | |
341 | let x240: u64 = (((arg1[8]) as u64) * ((arg2[8]) as u64)); | |
342 | let x241: u64 = (((arg1[7]) as u64) * ((arg2[15]) as u64)); | |
343 | let x242: u64 = (((arg1[7]) as u64) * ((arg2[14]) as u64)); | |
344 | let x243: u64 = (((arg1[7]) as u64) * ((arg2[13]) as u64)); | |
345 | let x244: u64 = (((arg1[7]) as u64) * ((arg2[12]) as u64)); | |
346 | let x245: u64 = (((arg1[7]) as u64) * ((arg2[11]) as u64)); | |
347 | let x246: u64 = (((arg1[7]) as u64) * ((arg2[10]) as u64)); | |
348 | let x247: u64 = (((arg1[7]) as u64) * ((arg2[9]) as u64)); | |
349 | let x248: u64 = (((arg1[6]) as u64) * ((arg2[15]) as u64)); | |
350 | let x249: u64 = (((arg1[6]) as u64) * ((arg2[14]) as u64)); | |
351 | let x250: u64 = (((arg1[6]) as u64) * ((arg2[13]) as u64)); | |
352 | let x251: u64 = (((arg1[6]) as u64) * ((arg2[12]) as u64)); | |
353 | let x252: u64 = (((arg1[6]) as u64) * ((arg2[11]) as u64)); | |
354 | let x253: u64 = (((arg1[6]) as u64) * ((arg2[10]) as u64)); | |
355 | let x254: u64 = (((arg1[5]) as u64) * ((arg2[15]) as u64)); | |
356 | let x255: u64 = (((arg1[5]) as u64) * ((arg2[14]) as u64)); | |
357 | let x256: u64 = (((arg1[5]) as u64) * ((arg2[13]) as u64)); | |
358 | let x257: u64 = (((arg1[5]) as u64) * ((arg2[12]) as u64)); | |
359 | let x258: u64 = (((arg1[5]) as u64) * ((arg2[11]) as u64)); | |
360 | let x259: u64 = (((arg1[4]) as u64) * ((arg2[15]) as u64)); | |
361 | let x260: u64 = (((arg1[4]) as u64) * ((arg2[14]) as u64)); | |
362 | let x261: u64 = (((arg1[4]) as u64) * ((arg2[13]) as u64)); | |
363 | let x262: u64 = (((arg1[4]) as u64) * ((arg2[12]) as u64)); | |
364 | let x263: u64 = (((arg1[3]) as u64) * ((arg2[15]) as u64)); | |
365 | let x264: u64 = (((arg1[3]) as u64) * ((arg2[14]) as u64)); | |
366 | let x265: u64 = (((arg1[3]) as u64) * ((arg2[13]) as u64)); | |
367 | let x266: u64 = (((arg1[2]) as u64) * ((arg2[15]) as u64)); | |
368 | let x267: u64 = (((arg1[2]) as u64) * ((arg2[14]) as u64)); | |
369 | let x268: u64 = (((arg1[1]) as u64) * ((arg2[15]) as u64)); | |
370 | let x269: u64 = (((arg1[15]) as u64) * ((arg2[0]) as u64)); | |
371 | let x270: u64 = (((arg1[14]) as u64) * ((arg2[1]) as u64)); | |
372 | let x271: u64 = (((arg1[14]) as u64) * ((arg2[0]) as u64)); | |
373 | let x272: u64 = (((arg1[13]) as u64) * ((arg2[2]) as u64)); | |
374 | let x273: u64 = (((arg1[13]) as u64) * ((arg2[1]) as u64)); | |
375 | let x274: u64 = (((arg1[13]) as u64) * ((arg2[0]) as u64)); | |
376 | let x275: u64 = (((arg1[12]) as u64) * ((arg2[3]) as u64)); | |
377 | let x276: u64 = (((arg1[12]) as u64) * ((arg2[2]) as u64)); | |
378 | let x277: u64 = (((arg1[12]) as u64) * ((arg2[1]) as u64)); | |
379 | let x278: u64 = (((arg1[12]) as u64) * ((arg2[0]) as u64)); | |
380 | let x279: u64 = (((arg1[11]) as u64) * ((arg2[4]) as u64)); | |
381 | let x280: u64 = (((arg1[11]) as u64) * ((arg2[3]) as u64)); | |
382 | let x281: u64 = (((arg1[11]) as u64) * ((arg2[2]) as u64)); | |
383 | let x282: u64 = (((arg1[11]) as u64) * ((arg2[1]) as u64)); | |
384 | let x283: u64 = (((arg1[11]) as u64) * ((arg2[0]) as u64)); | |
385 | let x284: u64 = (((arg1[10]) as u64) * ((arg2[5]) as u64)); | |
386 | let x285: u64 = (((arg1[10]) as u64) * ((arg2[4]) as u64)); | |
387 | let x286: u64 = (((arg1[10]) as u64) * ((arg2[3]) as u64)); | |
388 | let x287: u64 = (((arg1[10]) as u64) * ((arg2[2]) as u64)); | |
389 | let x288: u64 = (((arg1[10]) as u64) * ((arg2[1]) as u64)); | |
390 | let x289: u64 = (((arg1[10]) as u64) * ((arg2[0]) as u64)); | |
391 | let x290: u64 = (((arg1[9]) as u64) * ((arg2[6]) as u64)); | |
392 | let x291: u64 = (((arg1[9]) as u64) * ((arg2[5]) as u64)); | |
393 | let x292: u64 = (((arg1[9]) as u64) * ((arg2[4]) as u64)); | |
394 | let x293: u64 = (((arg1[9]) as u64) * ((arg2[3]) as u64)); | |
395 | let x294: u64 = (((arg1[9]) as u64) * ((arg2[2]) as u64)); | |
396 | let x295: u64 = (((arg1[9]) as u64) * ((arg2[1]) as u64)); | |
397 | let x296: u64 = (((arg1[9]) as u64) * ((arg2[0]) as u64)); | |
398 | let x297: u64 = (((arg1[8]) as u64) * ((arg2[7]) as u64)); | |
399 | let x298: u64 = (((arg1[8]) as u64) * ((arg2[6]) as u64)); | |
400 | let x299: u64 = (((arg1[8]) as u64) * ((arg2[5]) as u64)); | |
401 | let x300: u64 = (((arg1[8]) as u64) * ((arg2[4]) as u64)); | |
402 | let x301: u64 = (((arg1[8]) as u64) * ((arg2[3]) as u64)); | |
403 | let x302: u64 = (((arg1[8]) as u64) * ((arg2[2]) as u64)); | |
404 | let x303: u64 = (((arg1[8]) as u64) * ((arg2[1]) as u64)); | |
405 | let x304: u64 = (((arg1[8]) as u64) * ((arg2[0]) as u64)); | |
406 | let x305: u64 = (((arg1[7]) as u64) * ((arg2[8]) as u64)); | |
407 | let x306: u64 = (((arg1[7]) as u64) * ((arg2[7]) as u64)); | |
408 | let x307: u64 = (((arg1[7]) as u64) * ((arg2[6]) as u64)); | |
409 | let x308: u64 = (((arg1[7]) as u64) * ((arg2[5]) as u64)); | |
410 | let x309: u64 = (((arg1[7]) as u64) * ((arg2[4]) as u64)); | |
411 | let x310: u64 = (((arg1[7]) as u64) * ((arg2[3]) as u64)); | |
412 | let x311: u64 = (((arg1[7]) as u64) * ((arg2[2]) as u64)); | |
413 | let x312: u64 = (((arg1[7]) as u64) * ((arg2[1]) as u64)); | |
414 | let x313: u64 = (((arg1[7]) as u64) * ((arg2[0]) as u64)); | |
415 | let x314: u64 = (((arg1[6]) as u64) * ((arg2[9]) as u64)); | |
416 | let x315: u64 = (((arg1[6]) as u64) * ((arg2[8]) as u64)); | |
417 | let x316: u64 = (((arg1[6]) as u64) * ((arg2[7]) as u64)); | |
418 | let x317: u64 = (((arg1[6]) as u64) * ((arg2[6]) as u64)); | |
419 | let x318: u64 = (((arg1[6]) as u64) * ((arg2[5]) as u64)); | |
420 | let x319: u64 = (((arg1[6]) as u64) * ((arg2[4]) as u64)); | |
421 | let x320: u64 = (((arg1[6]) as u64) * ((arg2[3]) as u64)); | |
422 | let x321: u64 = (((arg1[6]) as u64) * ((arg2[2]) as u64)); | |
423 | let x322: u64 = (((arg1[6]) as u64) * ((arg2[1]) as u64)); | |
424 | let x323: u64 = (((arg1[6]) as u64) * ((arg2[0]) as u64)); | |
425 | let x324: u64 = (((arg1[5]) as u64) * ((arg2[10]) as u64)); | |
426 | let x325: u64 = (((arg1[5]) as u64) * ((arg2[9]) as u64)); | |
427 | let x326: u64 = (((arg1[5]) as u64) * ((arg2[8]) as u64)); | |
428 | let x327: u64 = (((arg1[5]) as u64) * ((arg2[7]) as u64)); | |
429 | let x328: u64 = (((arg1[5]) as u64) * ((arg2[6]) as u64)); | |
430 | let x329: u64 = (((arg1[5]) as u64) * ((arg2[5]) as u64)); | |
431 | let x330: u64 = (((arg1[5]) as u64) * ((arg2[4]) as u64)); | |
432 | let x331: u64 = (((arg1[5]) as u64) * ((arg2[3]) as u64)); | |
433 | let x332: u64 = (((arg1[5]) as u64) * ((arg2[2]) as u64)); | |
434 | let x333: u64 = (((arg1[5]) as u64) * ((arg2[1]) as u64)); | |
435 | let x334: u64 = (((arg1[5]) as u64) * ((arg2[0]) as u64)); | |
436 | let x335: u64 = (((arg1[4]) as u64) * ((arg2[11]) as u64)); | |
437 | let x336: u64 = (((arg1[4]) as u64) * ((arg2[10]) as u64)); | |
438 | let x337: u64 = (((arg1[4]) as u64) * ((arg2[9]) as u64)); | |
439 | let x338: u64 = (((arg1[4]) as u64) * ((arg2[8]) as u64)); | |
440 | let x339: u64 = (((arg1[4]) as u64) * ((arg2[7]) as u64)); | |
441 | let x340: u64 = (((arg1[4]) as u64) * ((arg2[6]) as u64)); | |
442 | let x341: u64 = (((arg1[4]) as u64) * ((arg2[5]) as u64)); | |
443 | let x342: u64 = (((arg1[4]) as u64) * ((arg2[4]) as u64)); | |
444 | let x343: u64 = (((arg1[4]) as u64) * ((arg2[3]) as u64)); | |
445 | let x344: u64 = (((arg1[4]) as u64) * ((arg2[2]) as u64)); | |
446 | let x345: u64 = (((arg1[4]) as u64) * ((arg2[1]) as u64)); | |
447 | let x346: u64 = (((arg1[4]) as u64) * ((arg2[0]) as u64)); | |
448 | let x347: u64 = (((arg1[3]) as u64) * ((arg2[12]) as u64)); | |
449 | let x348: u64 = (((arg1[3]) as u64) * ((arg2[11]) as u64)); | |
450 | let x349: u64 = (((arg1[3]) as u64) * ((arg2[10]) as u64)); | |
451 | let x350: u64 = (((arg1[3]) as u64) * ((arg2[9]) as u64)); | |
452 | let x351: u64 = (((arg1[3]) as u64) * ((arg2[8]) as u64)); | |
453 | let x352: u64 = (((arg1[3]) as u64) * ((arg2[7]) as u64)); | |
454 | let x353: u64 = (((arg1[3]) as u64) * ((arg2[6]) as u64)); | |
455 | let x354: u64 = (((arg1[3]) as u64) * ((arg2[5]) as u64)); | |
456 | let x355: u64 = (((arg1[3]) as u64) * ((arg2[4]) as u64)); | |
457 | let x356: u64 = (((arg1[3]) as u64) * ((arg2[3]) as u64)); | |
458 | let x357: u64 = (((arg1[3]) as u64) * ((arg2[2]) as u64)); | |
459 | let x358: u64 = (((arg1[3]) as u64) * ((arg2[1]) as u64)); | |
460 | let x359: u64 = (((arg1[3]) as u64) * ((arg2[0]) as u64)); | |
461 | let x360: u64 = (((arg1[2]) as u64) * ((arg2[13]) as u64)); | |
462 | let x361: u64 = (((arg1[2]) as u64) * ((arg2[12]) as u64)); | |
463 | let x362: u64 = (((arg1[2]) as u64) * ((arg2[11]) as u64)); | |
464 | let x363: u64 = (((arg1[2]) as u64) * ((arg2[10]) as u64)); | |
465 | let x364: u64 = (((arg1[2]) as u64) * ((arg2[9]) as u64)); | |
466 | let x365: u64 = (((arg1[2]) as u64) * ((arg2[8]) as u64)); | |
467 | let x366: u64 = (((arg1[2]) as u64) * ((arg2[7]) as u64)); | |
468 | let x367: u64 = (((arg1[2]) as u64) * ((arg2[6]) as u64)); | |
469 | let x368: u64 = (((arg1[2]) as u64) * ((arg2[5]) as u64)); | |
470 | let x369: u64 = (((arg1[2]) as u64) * ((arg2[4]) as u64)); | |
471 | let x370: u64 = (((arg1[2]) as u64) * ((arg2[3]) as u64)); | |
472 | let x371: u64 = (((arg1[2]) as u64) * ((arg2[2]) as u64)); | |
473 | let x372: u64 = (((arg1[2]) as u64) * ((arg2[1]) as u64)); | |
474 | let x373: u64 = (((arg1[2]) as u64) * ((arg2[0]) as u64)); | |
475 | let x374: u64 = (((arg1[1]) as u64) * ((arg2[14]) as u64)); | |
476 | let x375: u64 = (((arg1[1]) as u64) * ((arg2[13]) as u64)); | |
477 | let x376: u64 = (((arg1[1]) as u64) * ((arg2[12]) as u64)); | |
478 | let x377: u64 = (((arg1[1]) as u64) * ((arg2[11]) as u64)); | |
479 | let x378: u64 = (((arg1[1]) as u64) * ((arg2[10]) as u64)); | |
480 | let x379: u64 = (((arg1[1]) as u64) * ((arg2[9]) as u64)); | |
481 | let x380: u64 = (((arg1[1]) as u64) * ((arg2[8]) as u64)); | |
482 | let x381: u64 = (((arg1[1]) as u64) * ((arg2[7]) as u64)); | |
483 | let x382: u64 = (((arg1[1]) as u64) * ((arg2[6]) as u64)); | |
484 | let x383: u64 = (((arg1[1]) as u64) * ((arg2[5]) as u64)); | |
485 | let x384: u64 = (((arg1[1]) as u64) * ((arg2[4]) as u64)); | |
486 | let x385: u64 = (((arg1[1]) as u64) * ((arg2[3]) as u64)); | |
487 | let x386: u64 = (((arg1[1]) as u64) * ((arg2[2]) as u64)); | |
488 | let x387: u64 = (((arg1[1]) as u64) * ((arg2[1]) as u64)); | |
489 | let x388: u64 = (((arg1[1]) as u64) * ((arg2[0]) as u64)); | |
490 | let x389: u64 = (((arg1[0]) as u64) * ((arg2[15]) as u64)); | |
491 | let x390: u64 = (((arg1[0]) as u64) * ((arg2[14]) as u64)); | |
492 | let x391: u64 = (((arg1[0]) as u64) * ((arg2[13]) as u64)); | |
493 | let x392: u64 = (((arg1[0]) as u64) * ((arg2[12]) as u64)); | |
494 | let x393: u64 = (((arg1[0]) as u64) * ((arg2[11]) as u64)); | |
495 | let x394: u64 = (((arg1[0]) as u64) * ((arg2[10]) as u64)); | |
496 | let x395: u64 = (((arg1[0]) as u64) * ((arg2[9]) as u64)); | |
497 | let x396: u64 = (((arg1[0]) as u64) * ((arg2[8]) as u64)); | |
498 | let x397: u64 = (((arg1[0]) as u64) * ((arg2[7]) as u64)); | |
499 | let x398: u64 = (((arg1[0]) as u64) * ((arg2[6]) as u64)); | |
500 | let x399: u64 = (((arg1[0]) as u64) * ((arg2[5]) as u64)); | |
501 | let x400: u64 = (((arg1[0]) as u64) * ((arg2[4]) as u64)); | |
502 | let x401: u64 = (((arg1[0]) as u64) * ((arg2[3]) as u64)); | |
503 | let x402: u64 = (((arg1[0]) as u64) * ((arg2[2]) as u64)); | |
504 | let x403: u64 = (((arg1[0]) as u64) * ((arg2[1]) as u64)); | |
505 | let x404: u64 = (((arg1[0]) as u64) * ((arg2[0]) as u64)); | |
506 | let x405: u64 = (x397 + (x382 + (x368 + (x355 + (x343 + (x332 + (x322 + (x313 + (x141 + (x133 + (x124 + (x114 + (x103 + (x91 + (x78 + x64))))))))))))))); | |
507 | let x406: u64 = (x405 >> 28); | |
508 | let x407: u32 = ((x405 & (0xfffffff as u64)) as u32); | |
509 | let x408: u64 = (x389 + (x374 + (x360 + (x347 + (x335 + (x324 + (x314 + (x305 + (x297 + (x290 + (x284 + (x279 + (x275 + (x272 + (x270 + (x269 + (x233 + (x225 + (x217 + (x209 + (x201 + (x193 + (x185 + x177))))))))))))))))))))))); | |
510 | let x409: u64 = (x390 + (x375 + (x361 + (x348 + (x336 + (x325 + (x315 + (x306 + (x298 + (x291 + (x285 + (x280 + (x276 + (x273 + (x271 + (x241 + (x234 + (x226 + (x218 + (x210 + (x202 + (x194 + (x186 + (x178 + (x57 + x29))))))))))))))))))))))))); | |
511 | let x410: u64 = (x391 + (x376 + (x362 + (x349 + (x337 + (x326 + (x316 + (x307 + (x299 + (x292 + (x286 + (x281 + (x277 + (x274 + (x248 + (x242 + (x235 + (x227 + (x219 + (x211 + (x203 + (x195 + (x187 + (x179 + (x72 + (x58 + (x36 + x30))))))))))))))))))))))))))); | |
512 | let x411: u128 = ((x392 as u128) + ((x377 as u128) + ((x363 + (x350 + (x338 + (x327 + (x317 + (x308 + (x300 + (x293 + (x287 + (x282 + (x278 + (x254 + (x249 + (x243 + (x236 + (x228 + (x220 + (x212 + (x204 + (x196 + (x188 + (x180 + (x86 + (x73 + (x59 + (x42 + (x37 + x31))))))))))))))))))))))))))) as u128))); | |
513 | let x412: u128 = ((x393 as u128) + ((x378 as u128) + ((x364 as u128) + ((x351 as u128) + ((x339 + (x328 + (x318 + (x309 + (x301 + (x294 + (x288 + (x283 + (x259 + (x255 + (x250 + (x244 + (x237 + (x229 + (x221 + (x213 + (x205 + (x197 + (x189 + (x181 + (x99 + (x87 + (x74 + (x60 + (x47 + (x43 + (x38 + x32))))))))))))))))))))))))))) as u128))))); | |
514 | let x413: u128 = ((x394 as u128) + ((x379 as u128) + ((x365 as u128) + ((x352 as u128) + ((x340 as u128) + ((x329 as u128) + ((x319 + (x310 + (x302 + (x295 + (x289 + (x263 + (x260 + (x256 + (x251 + (x245 + (x238 + (x230 + (x222 + (x214 + (x206 + (x198 + (x190 + (x182 + (x111 + (x100 + (x88 + (x75 + (x61 + (x51 + (x48 + (x44 + (x39 + x33))))))))))))))))))))))))))) as u128))))))); | |
515 | let x414: u128 = ((x395 as u128) + ((x380 as u128) + ((x366 as u128) + ((x353 as u128) + ((x341 as u128) + ((x330 as u128) + ((x320 as u128) + ((x311 as u128) + ((x303 + (x296 + (x266 + (x264 + (x261 + (x257 + (x252 + (x246 + (x239 + (x231 + (x223 + (x215 + (x207 + (x199 + (x191 + (x183 + (x122 + (x112 + (x101 + (x89 + (x76 + (x62 + (x54 + (x52 + (x49 + (x45 + (x40 + x34))))))))))))))))))))))))))) as u128))))))))); | |
516 | let x415: u128 = ((x396 as u128) + ((x381 as u128) + ((x367 as u128) + ((x354 as u128) + ((x342 as u128) + ((x331 as u128) + ((x321 as u128) + ((x312 as u128) + ((x304 as u128) + ((x268 as u128) + ((x267 + (x265 + (x262 + (x258 + (x253 + (x247 + (x240 + (x232 + (x224 + (x216 + (x208 + (x200 + (x192 + (x184 + (x132 + (x123 + (x113 + (x102 + (x90 + (x77 + (x63 + (x56 + (x55 + (x53 + (x50 + (x46 + (x41 + x35))))))))))))))))))))))))))) as u128))))))))))); | |
517 | let x416: u64 = (x398 + (x383 + (x369 + (x356 + (x344 + (x333 + (x323 + (x149 + (x142 + (x134 + (x125 + (x115 + (x104 + (x92 + (x79 + (x65 + x1)))))))))))))))); | |
518 | let x417: u64 = (x399 + (x384 + (x370 + (x357 + (x345 + (x334 + (x156 + (x150 + (x143 + (x135 + (x126 + (x116 + (x105 + (x93 + (x80 + (x66 + (x8 + x2))))))))))))))))); | |
519 | let x418: u64 = (x400 + (x385 + (x371 + (x358 + (x346 + (x162 + (x157 + (x151 + (x144 + (x136 + (x127 + (x117 + (x106 + (x94 + (x81 + (x67 + (x14 + (x9 + x3)))))))))))))))))); | |
520 | let x419: u64 = (x401 + (x386 + (x372 + (x359 + (x167 + (x163 + (x158 + (x152 + (x145 + (x137 + (x128 + (x118 + (x107 + (x95 + (x82 + (x68 + (x19 + (x15 + (x10 + x4))))))))))))))))))); | |
521 | let x420: u64 = (x402 + (x387 + (x373 + (x171 + (x168 + (x164 + (x159 + (x153 + (x146 + (x138 + (x129 + (x119 + (x108 + (x96 + (x83 + (x69 + (x23 + (x20 + (x16 + (x11 + x5)))))))))))))))))))); | |
522 | let x421: u64 = (x403 + (x388 + (x174 + (x172 + (x169 + (x165 + (x160 + (x154 + (x147 + (x139 + (x130 + (x120 + (x109 + (x97 + (x84 + (x70 + (x26 + (x24 + (x21 + (x17 + (x12 + x6))))))))))))))))))))); | |
523 | let x422: u64 = (x404 + (x176 + (x175 + (x173 + (x170 + (x166 + (x161 + (x155 + (x148 + (x140 + (x131 + (x121 + (x110 + (x98 + (x85 + (x71 + (x28 + (x27 + (x25 + (x22 + (x18 + (x13 + x7)))))))))))))))))))))); | |
524 | let x423: u128 = ((x406 as u128) + x415); | |
525 | let x424: u64 = (x408 >> 28); | |
526 | let x425: u32 = ((x408 & (0xfffffff as u64)) as u32); | |
527 | let x426: u128 = (x423 + (x424 as u128)); | |
528 | let x427: u64 = ((x426 >> 28) as u64); | |
529 | let x428: u32 = ((x426 & (0xfffffff as u128)) as u32); | |
530 | let x429: u64 = (x422 + x424); | |
531 | let x430: u128 = ((x427 as u128) + x414); | |
532 | let x431: u64 = (x429 >> 28); | |
533 | let x432: u32 = ((x429 & (0xfffffff as u64)) as u32); | |
534 | let x433: u64 = (x431 + x421); | |
535 | let x434: u64 = ((x430 >> 28) as u64); | |
536 | let x435: u32 = ((x430 & (0xfffffff as u128)) as u32); | |
537 | let x436: u128 = ((x434 as u128) + x413); | |
538 | let x437: u64 = (x433 >> 28); | |
539 | let x438: u32 = ((x433 & (0xfffffff as u64)) as u32); | |
540 | let x439: u64 = (x437 + x420); | |
541 | let x440: u64 = ((x436 >> 28) as u64); | |
542 | let x441: u32 = ((x436 & (0xfffffff as u128)) as u32); | |
543 | let x442: u128 = ((x440 as u128) + x412); | |
544 | let x443: u64 = (x439 >> 28); | |
545 | let x444: u32 = ((x439 & (0xfffffff as u64)) as u32); | |
546 | let x445: u64 = (x443 + x419); | |
547 | let x446: u64 = ((x442 >> 28) as u64); | |
548 | let x447: u32 = ((x442 & (0xfffffff as u128)) as u32); | |
549 | let x448: u128 = ((x446 as u128) + x411); | |
550 | let x449: u64 = (x445 >> 28); | |
551 | let x450: u32 = ((x445 & (0xfffffff as u64)) as u32); | |
552 | let x451: u64 = (x449 + x418); | |
553 | let x452: u64 = ((x448 >> 28) as u64); | |
554 | let x453: u32 = ((x448 & (0xfffffff as u128)) as u32); | |
555 | let x454: u64 = (x452 + x410); | |
556 | let x455: u64 = (x451 >> 28); | |
557 | let x456: u32 = ((x451 & (0xfffffff as u64)) as u32); | |
558 | let x457: u64 = (x455 + x417); | |
559 | let x458: u64 = (x454 >> 28); | |
560 | let x459: u32 = ((x454 & (0xfffffff as u64)) as u32); | |
561 | let x460: u64 = (x458 + x409); | |
562 | let x461: u64 = (x457 >> 28); | |
563 | let x462: u32 = ((x457 & (0xfffffff as u64)) as u32); | |
564 | let x463: u64 = (x461 + x416); | |
565 | let x464: u64 = (x460 >> 28); | |
566 | let x465: u32 = ((x460 & (0xfffffff as u64)) as u32); | |
567 | let x466: u64 = (x464 + (x425 as u64)); | |
568 | let x467: u64 = (x463 >> 28); | |
569 | let x468: u32 = ((x463 & (0xfffffff as u64)) as u32); | |
570 | let x469: u64 = (x467 + (x407 as u64)); | |
571 | let x470: u32 = ((x466 >> 28) as u32); | |
572 | let x471: u32 = ((x466 & (0xfffffff as u64)) as u32); | |
573 | let x472: u32 = ((x469 >> 28) as u32); | |
574 | let x473: u32 = ((x469 & (0xfffffff as u64)) as u32); | |
575 | let x474: u32 = (x428 + x470); | |
576 | let x475: u32 = (x432 + x470); | |
577 | let x476: u32 = (x472 + x474); | |
578 | let x477: fiat_p448_u1 = ((x476 >> 28) as fiat_p448_u1); | |
579 | let x478: u32 = (x476 & 0xfffffff); | |
580 | let x479: u32 = ((x477 as u32) + x435); | |
581 | let x480: fiat_p448_u1 = ((x475 >> 28) as fiat_p448_u1); | |
582 | let x481: u32 = (x475 & 0xfffffff); | |
583 | let x482: u32 = ((x480 as u32) + x438); | |
584 | out1[0] = x481; | |
585 | out1[1] = x482; | |
586 | out1[2] = x444; | |
587 | out1[3] = x450; | |
588 | out1[4] = x456; | |
589 | out1[5] = x462; | |
590 | out1[6] = x468; | |
591 | out1[7] = x473; | |
592 | out1[8] = x478; | |
593 | out1[9] = x479; | |
594 | out1[10] = x441; | |
595 | out1[11] = x447; | |
596 | out1[12] = x453; | |
597 | out1[13] = x459; | |
598 | out1[14] = x465; | |
599 | out1[15] = x471; | |
600 | } | |
601 | ||
602 | /// The function fiat_p448_carry_square squares a field element and reduces the result. | |
603 | /// | |
604 | /// Postconditions: | |
605 | /// eval out1 mod m = (eval arg1 * eval arg1) mod m | |
606 | /// | |
607 | #[inline] | |
608 | pub fn fiat_p448_carry_square(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element) -> () { | |
609 | let x1: u32 = (arg1[15]); | |
610 | let x2: u32 = (arg1[15]); | |
611 | let x3: u32 = (x1 * 0x2); | |
612 | let x4: u32 = (x2 * 0x2); | |
613 | let x5: u32 = ((arg1[15]) * 0x2); | |
614 | let x6: u32 = (arg1[14]); | |
615 | let x7: u32 = (arg1[14]); | |
616 | let x8: u32 = (x6 * 0x2); | |
617 | let x9: u32 = (x7 * 0x2); | |
618 | let x10: u32 = ((arg1[14]) * 0x2); | |
619 | let x11: u32 = (arg1[13]); | |
620 | let x12: u32 = (arg1[13]); | |
621 | let x13: u32 = (x11 * 0x2); | |
622 | let x14: u32 = (x12 * 0x2); | |
623 | let x15: u32 = ((arg1[13]) * 0x2); | |
624 | let x16: u32 = (arg1[12]); | |
625 | let x17: u32 = (arg1[12]); | |
626 | let x18: u32 = (x16 * 0x2); | |
627 | let x19: u32 = (x17 * 0x2); | |
628 | let x20: u32 = ((arg1[12]) * 0x2); | |
629 | let x21: u32 = (arg1[11]); | |
630 | let x22: u32 = (arg1[11]); | |
631 | let x23: u32 = (x21 * 0x2); | |
632 | let x24: u32 = (x22 * 0x2); | |
633 | let x25: u32 = ((arg1[11]) * 0x2); | |
634 | let x26: u32 = (arg1[10]); | |
635 | let x27: u32 = (arg1[10]); | |
636 | let x28: u32 = (x26 * 0x2); | |
637 | let x29: u32 = (x27 * 0x2); | |
638 | let x30: u32 = ((arg1[10]) * 0x2); | |
639 | let x31: u32 = (arg1[9]); | |
640 | let x32: u32 = (arg1[9]); | |
641 | let x33: u32 = (x31 * 0x2); | |
642 | let x34: u32 = (x32 * 0x2); | |
643 | let x35: u32 = ((arg1[9]) * 0x2); | |
644 | let x36: u32 = (arg1[8]); | |
645 | let x37: u32 = (arg1[8]); | |
646 | let x38: u32 = ((arg1[8]) * 0x2); | |
647 | let x39: u32 = ((arg1[7]) * 0x2); | |
648 | let x40: u32 = ((arg1[6]) * 0x2); | |
649 | let x41: u32 = ((arg1[5]) * 0x2); | |
650 | let x42: u32 = ((arg1[4]) * 0x2); | |
651 | let x43: u32 = ((arg1[3]) * 0x2); | |
652 | let x44: u32 = ((arg1[2]) * 0x2); | |
653 | let x45: u32 = ((arg1[1]) * 0x2); | |
654 | let x46: u64 = (((arg1[15]) as u64) * (x1 as u64)); | |
655 | let x47: u64 = (((arg1[14]) as u64) * (x3 as u64)); | |
656 | let x48: u64 = (((arg1[14]) as u64) * (x6 as u64)); | |
657 | let x49: u64 = (((arg1[13]) as u64) * (x3 as u64)); | |
658 | let x50: u64 = (((arg1[13]) as u64) * (x8 as u64)); | |
659 | let x51: u64 = (((arg1[13]) as u64) * (x11 as u64)); | |
660 | let x52: u64 = (((arg1[12]) as u64) * (x3 as u64)); | |
661 | let x53: u64 = (((arg1[12]) as u64) * (x8 as u64)); | |
662 | let x54: u64 = (((arg1[12]) as u64) * (x13 as u64)); | |
663 | let x55: u64 = (((arg1[12]) as u64) * (x16 as u64)); | |
664 | let x56: u64 = (((arg1[11]) as u64) * (x3 as u64)); | |
665 | let x57: u64 = (((arg1[11]) as u64) * (x8 as u64)); | |
666 | let x58: u64 = (((arg1[11]) as u64) * (x13 as u64)); | |
667 | let x59: u64 = (((arg1[10]) as u64) * (x3 as u64)); | |
668 | let x60: u64 = (((arg1[10]) as u64) * (x8 as u64)); | |
669 | let x61: u64 = (((arg1[9]) as u64) * (x3 as u64)); | |
670 | let x62: u64 = (((arg1[15]) as u64) * (x1 as u64)); | |
671 | let x63: u64 = (((arg1[14]) as u64) * (x3 as u64)); | |
672 | let x64: u64 = (((arg1[14]) as u64) * (x6 as u64)); | |
673 | let x65: u64 = (((arg1[13]) as u64) * (x3 as u64)); | |
674 | let x66: u64 = (((arg1[13]) as u64) * (x8 as u64)); | |
675 | let x67: u64 = (((arg1[13]) as u64) * (x11 as u64)); | |
676 | let x68: u64 = (((arg1[12]) as u64) * (x3 as u64)); | |
677 | let x69: u64 = (((arg1[12]) as u64) * (x8 as u64)); | |
678 | let x70: u64 = (((arg1[12]) as u64) * (x13 as u64)); | |
679 | let x71: u64 = (((arg1[12]) as u64) * (x16 as u64)); | |
680 | let x72: u64 = (((arg1[11]) as u64) * (x3 as u64)); | |
681 | let x73: u64 = (((arg1[11]) as u64) * (x8 as u64)); | |
682 | let x74: u64 = (((arg1[11]) as u64) * (x13 as u64)); | |
683 | let x75: u64 = (((arg1[10]) as u64) * (x3 as u64)); | |
684 | let x76: u64 = (((arg1[10]) as u64) * (x8 as u64)); | |
685 | let x77: u64 = (((arg1[9]) as u64) * (x3 as u64)); | |
686 | let x78: u64 = (((arg1[15]) as u64) * (x2 as u64)); | |
687 | let x79: u64 = (((arg1[14]) as u64) * (x4 as u64)); | |
688 | let x80: u64 = (((arg1[14]) as u64) * (x7 as u64)); | |
689 | let x81: u64 = (((arg1[13]) as u64) * (x4 as u64)); | |
690 | let x82: u64 = (((arg1[13]) as u64) * (x9 as u64)); | |
691 | let x83: u64 = (((arg1[13]) as u64) * (x12 as u64)); | |
692 | let x84: u64 = (((arg1[12]) as u64) * (x4 as u64)); | |
693 | let x85: u64 = (((arg1[12]) as u64) * (x9 as u64)); | |
694 | let x86: u64 = (((arg1[12]) as u64) * (x14 as u64)); | |
695 | let x87: u64 = (((arg1[12]) as u64) * (x17 as u64)); | |
696 | let x88: u64 = (((arg1[11]) as u64) * (x4 as u64)); | |
697 | let x89: u64 = (((arg1[11]) as u64) * (x9 as u64)); | |
698 | let x90: u64 = (((arg1[11]) as u64) * (x14 as u64)); | |
699 | let x91: u64 = (((arg1[11]) as u64) * (x19 as u64)); | |
700 | let x92: u64 = (((arg1[11]) as u64) * (x18 as u64)); | |
701 | let x93: u64 = (((arg1[11]) as u64) * (x22 as u64)); | |
702 | let x94: u64 = (((arg1[11]) as u64) * (x21 as u64)); | |
703 | let x95: u64 = (((arg1[10]) as u64) * (x4 as u64)); | |
704 | let x96: u64 = (((arg1[10]) as u64) * (x9 as u64)); | |
705 | let x97: u64 = (((arg1[10]) as u64) * (x14 as u64)); | |
706 | let x98: u64 = (((arg1[10]) as u64) * (x13 as u64)); | |
707 | let x99: u64 = (((arg1[10]) as u64) * (x19 as u64)); | |
708 | let x100: u64 = (((arg1[10]) as u64) * (x18 as u64)); | |
709 | let x101: u64 = (((arg1[10]) as u64) * (x24 as u64)); | |
710 | let x102: u64 = (((arg1[10]) as u64) * (x23 as u64)); | |
711 | let x103: u64 = (((arg1[10]) as u64) * (x27 as u64)); | |
712 | let x104: u64 = (((arg1[10]) as u64) * (x26 as u64)); | |
713 | let x105: u64 = (((arg1[9]) as u64) * (x4 as u64)); | |
714 | let x106: u64 = (((arg1[9]) as u64) * (x9 as u64)); | |
715 | let x107: u64 = (((arg1[9]) as u64) * (x8 as u64)); | |
716 | let x108: u64 = (((arg1[9]) as u64) * (x14 as u64)); | |
717 | let x109: u64 = (((arg1[9]) as u64) * (x13 as u64)); | |
718 | let x110: u64 = (((arg1[9]) as u64) * (x19 as u64)); | |
719 | let x111: u64 = (((arg1[9]) as u64) * (x18 as u64)); | |
720 | let x112: u64 = (((arg1[9]) as u64) * (x24 as u64)); | |
721 | let x113: u64 = (((arg1[9]) as u64) * (x23 as u64)); | |
722 | let x114: u64 = (((arg1[9]) as u64) * (x29 as u64)); | |
723 | let x115: u64 = (((arg1[9]) as u64) * (x28 as u64)); | |
724 | let x116: u64 = (((arg1[9]) as u64) * (x32 as u64)); | |
725 | let x117: u64 = (((arg1[9]) as u64) * (x31 as u64)); | |
726 | let x118: u64 = (((arg1[8]) as u64) * (x4 as u64)); | |
727 | let x119: u64 = (((arg1[8]) as u64) * (x3 as u64)); | |
728 | let x120: u64 = (((arg1[8]) as u64) * (x9 as u64)); | |
729 | let x121: u64 = (((arg1[8]) as u64) * (x8 as u64)); | |
730 | let x122: u64 = (((arg1[8]) as u64) * (x14 as u64)); | |
731 | let x123: u64 = (((arg1[8]) as u64) * (x13 as u64)); | |
732 | let x124: u64 = (((arg1[8]) as u64) * (x19 as u64)); | |
733 | let x125: u64 = (((arg1[8]) as u64) * (x18 as u64)); | |
734 | let x126: u64 = (((arg1[8]) as u64) * (x24 as u64)); | |
735 | let x127: u64 = (((arg1[8]) as u64) * (x23 as u64)); | |
736 | let x128: u64 = (((arg1[8]) as u64) * (x29 as u64)); | |
737 | let x129: u64 = (((arg1[8]) as u64) * (x28 as u64)); | |
738 | let x130: u64 = (((arg1[8]) as u64) * (x34 as u64)); | |
739 | let x131: u64 = (((arg1[8]) as u64) * (x33 as u64)); | |
740 | let x132: u64 = (((arg1[8]) as u64) * (x37 as u64)); | |
741 | let x133: u64 = (((arg1[8]) as u64) * (x36 as u64)); | |
742 | let x134: u64 = (((arg1[7]) as u64) * (x4 as u64)); | |
743 | let x135: u64 = (((arg1[7]) as u64) * (x3 as u64)); | |
744 | let x136: u64 = (((arg1[7]) as u64) * (x9 as u64)); | |
745 | let x137: u64 = (((arg1[7]) as u64) * (x8 as u64)); | |
746 | let x138: u64 = (((arg1[7]) as u64) * (x14 as u64)); | |
747 | let x139: u64 = (((arg1[7]) as u64) * (x13 as u64)); | |
748 | let x140: u64 = (((arg1[7]) as u64) * (x19 as u64)); | |
749 | let x141: u64 = (((arg1[7]) as u64) * (x18 as u64)); | |
750 | let x142: u64 = (((arg1[7]) as u64) * (x24 as u64)); | |
751 | let x143: u64 = (((arg1[7]) as u64) * (x23 as u64)); | |
752 | let x144: u64 = (((arg1[7]) as u64) * (x29 as u64)); | |
753 | let x145: u64 = (((arg1[7]) as u64) * (x28 as u64)); | |
754 | let x146: u64 = (((arg1[7]) as u64) * (x34 as u64)); | |
755 | let x147: u64 = (((arg1[7]) as u64) * (x33 as u64)); | |
756 | let x148: u64 = (((arg1[7]) as u64) * (x38 as u64)); | |
757 | let x149: u64 = (((arg1[7]) as u64) * ((arg1[7]) as u64)); | |
758 | let x150: u64 = (((arg1[6]) as u64) * (x4 as u64)); | |
759 | let x151: u64 = (((arg1[6]) as u64) * (x3 as u64)); | |
760 | let x152: u64 = (((arg1[6]) as u64) * (x9 as u64)); | |
761 | let x153: u64 = (((arg1[6]) as u64) * (x8 as u64)); | |
762 | let x154: u64 = (((arg1[6]) as u64) * (x14 as u64)); | |
763 | let x155: u64 = (((arg1[6]) as u64) * (x13 as u64)); | |
764 | let x156: u64 = (((arg1[6]) as u64) * (x19 as u64)); | |
765 | let x157: u64 = (((arg1[6]) as u64) * (x18 as u64)); | |
766 | let x158: u64 = (((arg1[6]) as u64) * (x24 as u64)); | |
767 | let x159: u64 = (((arg1[6]) as u64) * (x23 as u64)); | |
768 | let x160: u64 = (((arg1[6]) as u64) * (x29 as u64)); | |
769 | let x161: u64 = (((arg1[6]) as u64) * (x28 as u64)); | |
770 | let x162: u64 = (((arg1[6]) as u64) * (x35 as u64)); | |
771 | let x163: u64 = (((arg1[6]) as u64) * (x38 as u64)); | |
772 | let x164: u64 = (((arg1[6]) as u64) * (x39 as u64)); | |
773 | let x165: u64 = (((arg1[6]) as u64) * ((arg1[6]) as u64)); | |
774 | let x166: u64 = (((arg1[5]) as u64) * (x4 as u64)); | |
775 | let x167: u64 = (((arg1[5]) as u64) * (x3 as u64)); | |
776 | let x168: u64 = (((arg1[5]) as u64) * (x9 as u64)); | |
777 | let x169: u64 = (((arg1[5]) as u64) * (x8 as u64)); | |
778 | let x170: u64 = (((arg1[5]) as u64) * (x14 as u64)); | |
779 | let x171: u64 = (((arg1[5]) as u64) * (x13 as u64)); | |
780 | let x172: u64 = (((arg1[5]) as u64) * (x19 as u64)); | |
781 | let x173: u64 = (((arg1[5]) as u64) * (x18 as u64)); | |
782 | let x174: u64 = (((arg1[5]) as u64) * (x24 as u64)); | |
783 | let x175: u64 = (((arg1[5]) as u64) * (x23 as u64)); | |
784 | let x176: u64 = (((arg1[5]) as u64) * (x30 as u64)); | |
785 | let x177: u64 = (((arg1[5]) as u64) * (x35 as u64)); | |
786 | let x178: u64 = (((arg1[5]) as u64) * (x38 as u64)); | |
787 | let x179: u64 = (((arg1[5]) as u64) * (x39 as u64)); | |
788 | let x180: u64 = (((arg1[5]) as u64) * (x40 as u64)); | |
789 | let x181: u64 = (((arg1[5]) as u64) * ((arg1[5]) as u64)); | |
790 | let x182: u64 = (((arg1[4]) as u64) * (x4 as u64)); | |
791 | let x183: u64 = (((arg1[4]) as u64) * (x3 as u64)); | |
792 | let x184: u64 = (((arg1[4]) as u64) * (x9 as u64)); | |
793 | let x185: u64 = (((arg1[4]) as u64) * (x8 as u64)); | |
794 | let x186: u64 = (((arg1[4]) as u64) * (x14 as u64)); | |
795 | let x187: u64 = (((arg1[4]) as u64) * (x13 as u64)); | |
796 | let x188: u64 = (((arg1[4]) as u64) * (x19 as u64)); | |
797 | let x189: u64 = (((arg1[4]) as u64) * (x18 as u64)); | |
798 | let x190: u64 = (((arg1[4]) as u64) * (x25 as u64)); | |
799 | let x191: u64 = (((arg1[4]) as u64) * (x30 as u64)); | |
800 | let x192: u64 = (((arg1[4]) as u64) * (x35 as u64)); | |
801 | let x193: u64 = (((arg1[4]) as u64) * (x38 as u64)); | |
802 | let x194: u64 = (((arg1[4]) as u64) * (x39 as u64)); | |
803 | let x195: u64 = (((arg1[4]) as u64) * (x40 as u64)); | |
804 | let x196: u64 = (((arg1[4]) as u64) * (x41 as u64)); | |
805 | let x197: u64 = (((arg1[4]) as u64) * ((arg1[4]) as u64)); | |
806 | let x198: u64 = (((arg1[3]) as u64) * (x4 as u64)); | |
807 | let x199: u64 = (((arg1[3]) as u64) * (x3 as u64)); | |
808 | let x200: u64 = (((arg1[3]) as u64) * (x9 as u64)); | |
809 | let x201: u64 = (((arg1[3]) as u64) * (x8 as u64)); | |
810 | let x202: u64 = (((arg1[3]) as u64) * (x14 as u64)); | |
811 | let x203: u64 = (((arg1[3]) as u64) * (x13 as u64)); | |
812 | let x204: u64 = (((arg1[3]) as u64) * (x20 as u64)); | |
813 | let x205: u64 = (((arg1[3]) as u64) * (x25 as u64)); | |
814 | let x206: u64 = (((arg1[3]) as u64) * (x30 as u64)); | |
815 | let x207: u64 = (((arg1[3]) as u64) * (x35 as u64)); | |
816 | let x208: u64 = (((arg1[3]) as u64) * (x38 as u64)); | |
817 | let x209: u64 = (((arg1[3]) as u64) * (x39 as u64)); | |
818 | let x210: u64 = (((arg1[3]) as u64) * (x40 as u64)); | |
819 | let x211: u64 = (((arg1[3]) as u64) * (x41 as u64)); | |
820 | let x212: u64 = (((arg1[3]) as u64) * (x42 as u64)); | |
821 | let x213: u64 = (((arg1[3]) as u64) * ((arg1[3]) as u64)); | |
822 | let x214: u64 = (((arg1[2]) as u64) * (x4 as u64)); | |
823 | let x215: u64 = (((arg1[2]) as u64) * (x3 as u64)); | |
824 | let x216: u64 = (((arg1[2]) as u64) * (x9 as u64)); | |
825 | let x217: u64 = (((arg1[2]) as u64) * (x8 as u64)); | |
826 | let x218: u64 = (((arg1[2]) as u64) * (x15 as u64)); | |
827 | let x219: u64 = (((arg1[2]) as u64) * (x20 as u64)); | |
828 | let x220: u64 = (((arg1[2]) as u64) * (x25 as u64)); | |
829 | let x221: u64 = (((arg1[2]) as u64) * (x30 as u64)); | |
830 | let x222: u64 = (((arg1[2]) as u64) * (x35 as u64)); | |
831 | let x223: u64 = (((arg1[2]) as u64) * (x38 as u64)); | |
832 | let x224: u64 = (((arg1[2]) as u64) * (x39 as u64)); | |
833 | let x225: u64 = (((arg1[2]) as u64) * (x40 as u64)); | |
834 | let x226: u64 = (((arg1[2]) as u64) * (x41 as u64)); | |
835 | let x227: u64 = (((arg1[2]) as u64) * (x42 as u64)); | |
836 | let x228: u64 = (((arg1[2]) as u64) * (x43 as u64)); | |
837 | let x229: u64 = (((arg1[2]) as u64) * ((arg1[2]) as u64)); | |
838 | let x230: u64 = (((arg1[1]) as u64) * (x4 as u64)); | |
839 | let x231: u64 = (((arg1[1]) as u64) * (x3 as u64)); | |
840 | let x232: u64 = (((arg1[1]) as u64) * (x10 as u64)); | |
841 | let x233: u64 = (((arg1[1]) as u64) * (x15 as u64)); | |
842 | let x234: u64 = (((arg1[1]) as u64) * (x20 as u64)); | |
843 | let x235: u64 = (((arg1[1]) as u64) * (x25 as u64)); | |
844 | let x236: u64 = (((arg1[1]) as u64) * (x30 as u64)); | |
845 | let x237: u64 = (((arg1[1]) as u64) * (x35 as u64)); | |
846 | let x238: u64 = (((arg1[1]) as u64) * (x38 as u64)); | |
847 | let x239: u64 = (((arg1[1]) as u64) * (x39 as u64)); | |
848 | let x240: u64 = (((arg1[1]) as u64) * (x40 as u64)); | |
849 | let x241: u64 = (((arg1[1]) as u64) * (x41 as u64)); | |
850 | let x242: u64 = (((arg1[1]) as u64) * (x42 as u64)); | |
851 | let x243: u64 = (((arg1[1]) as u64) * (x43 as u64)); | |
852 | let x244: u64 = (((arg1[1]) as u64) * (x44 as u64)); | |
853 | let x245: u64 = (((arg1[1]) as u64) * ((arg1[1]) as u64)); | |
854 | let x246: u64 = (((arg1[0]) as u64) * (x5 as u64)); | |
855 | let x247: u64 = (((arg1[0]) as u64) * (x10 as u64)); | |
856 | let x248: u64 = (((arg1[0]) as u64) * (x15 as u64)); | |
857 | let x249: u64 = (((arg1[0]) as u64) * (x20 as u64)); | |
858 | let x250: u64 = (((arg1[0]) as u64) * (x25 as u64)); | |
859 | let x251: u64 = (((arg1[0]) as u64) * (x30 as u64)); | |
860 | let x252: u64 = (((arg1[0]) as u64) * (x35 as u64)); | |
861 | let x253: u64 = (((arg1[0]) as u64) * (x38 as u64)); | |
862 | let x254: u64 = (((arg1[0]) as u64) * (x39 as u64)); | |
863 | let x255: u64 = (((arg1[0]) as u64) * (x40 as u64)); | |
864 | let x256: u64 = (((arg1[0]) as u64) * (x41 as u64)); | |
865 | let x257: u64 = (((arg1[0]) as u64) * (x42 as u64)); | |
866 | let x258: u64 = (((arg1[0]) as u64) * (x43 as u64)); | |
867 | let x259: u64 = (((arg1[0]) as u64) * (x44 as u64)); | |
868 | let x260: u64 = (((arg1[0]) as u64) * (x45 as u64)); | |
869 | let x261: u64 = (((arg1[0]) as u64) * ((arg1[0]) as u64)); | |
870 | let x262: u64 = (x254 + (x240 + (x226 + (x212 + (x118 + (x106 + (x97 + x91))))))); | |
871 | let x263: u64 = (x262 >> 28); | |
872 | let x264: u32 = ((x262 & (0xfffffff as u64)) as u32); | |
873 | let x265: u64 = (x246 + (x232 + (x218 + (x204 + (x190 + (x176 + (x162 + (x148 + (x119 + (x107 + (x98 + x92))))))))))); | |
874 | let x266: u64 = (x247 + (x233 + (x219 + (x205 + (x191 + (x177 + (x163 + (x149 + (x135 + (x121 + (x109 + (x100 + (x94 + (x78 + x62)))))))))))))); | |
875 | let x267: u64 = (x248 + (x234 + (x220 + (x206 + (x192 + (x178 + (x164 + (x151 + (x137 + (x123 + (x111 + (x102 + (x79 + x63))))))))))))); | |
876 | let x268: u128 = ((x249 as u128) + ((x235 + (x221 + (x207 + (x193 + (x179 + (x167 + (x165 + (x153 + (x139 + (x125 + (x113 + (x104 + (x81 + (x80 + (x65 + x64))))))))))))))) as u128)); | |
877 | let x269: u128 = ((x250 as u128) + ((x236 as u128) + ((x222 + (x208 + (x194 + (x183 + (x180 + (x169 + (x155 + (x141 + (x127 + (x115 + (x84 + (x82 + (x68 + x66))))))))))))) as u128))); | |
878 | let x270: u128 = ((x251 as u128) + ((x237 as u128) + ((x223 as u128) + ((x209 + (x199 + (x195 + (x185 + (x181 + (x171 + (x157 + (x143 + (x129 + (x117 + (x88 + (x85 + (x83 + (x72 + (x69 + x67))))))))))))))) as u128)))); | |
879 | let x271: u128 = ((x252 as u128) + ((x238 as u128) + ((x224 as u128) + ((x215 as u128) + ((x210 + (x201 + (x196 + (x187 + (x173 + (x159 + (x145 + (x131 + (x95 + (x89 + (x86 + (x75 + (x73 + x70))))))))))))) as u128))))); | |
880 | let x272: u128 = ((x253 as u128) + ((x239 as u128) + ((x231 as u128) + ((x225 as u128) + ((x217 as u128) + ((x211 + (x203 + (x197 + (x189 + (x175 + (x161 + (x147 + (x133 + (x105 + (x96 + (x90 + (x87 + (x77 + (x76 + (x74 + x71))))))))))))))) as u128)))))); | |
881 | let x273: u64 = (x255 + (x241 + (x227 + (x213 + (x134 + (x120 + (x108 + (x99 + (x93 + x46))))))))); | |
882 | let x274: u64 = (x256 + (x242 + (x228 + (x150 + (x136 + (x122 + (x110 + (x101 + x47)))))))); | |
883 | let x275: u64 = (x257 + (x243 + (x229 + (x166 + (x152 + (x138 + (x124 + (x112 + (x103 + (x49 + x48)))))))))); | |
884 | let x276: u64 = (x258 + (x244 + (x182 + (x168 + (x154 + (x140 + (x126 + (x114 + (x52 + x50))))))))); | |
885 | let x277: u64 = (x259 + (x245 + (x198 + (x184 + (x170 + (x156 + (x142 + (x128 + (x116 + (x56 + (x53 + x51))))))))))); | |
886 | let x278: u64 = (x260 + (x214 + (x200 + (x186 + (x172 + (x158 + (x144 + (x130 + (x59 + (x57 + x54)))))))))); | |
887 | let x279: u64 = (x261 + (x230 + (x216 + (x202 + (x188 + (x174 + (x160 + (x146 + (x132 + (x61 + (x60 + (x58 + x55)))))))))))); | |
888 | let x280: u128 = ((x263 as u128) + x272); | |
889 | let x281: u64 = (x265 >> 28); | |
890 | let x282: u32 = ((x265 & (0xfffffff as u64)) as u32); | |
891 | let x283: u128 = (x280 + (x281 as u128)); | |
892 | let x284: u64 = ((x283 >> 28) as u64); | |
893 | let x285: u32 = ((x283 & (0xfffffff as u128)) as u32); | |
894 | let x286: u64 = (x279 + x281); | |
895 | let x287: u128 = ((x284 as u128) + x271); | |
896 | let x288: u64 = (x286 >> 28); | |
897 | let x289: u32 = ((x286 & (0xfffffff as u64)) as u32); | |
898 | let x290: u64 = (x288 + x278); | |
899 | let x291: u64 = ((x287 >> 28) as u64); | |
900 | let x292: u32 = ((x287 & (0xfffffff as u128)) as u32); | |
901 | let x293: u128 = ((x291 as u128) + x270); | |
902 | let x294: u64 = (x290 >> 28); | |
903 | let x295: u32 = ((x290 & (0xfffffff as u64)) as u32); | |
904 | let x296: u64 = (x294 + x277); | |
905 | let x297: u64 = ((x293 >> 28) as u64); | |
906 | let x298: u32 = ((x293 & (0xfffffff as u128)) as u32); | |
907 | let x299: u128 = ((x297 as u128) + x269); | |
908 | let x300: u64 = (x296 >> 28); | |
909 | let x301: u32 = ((x296 & (0xfffffff as u64)) as u32); | |
910 | let x302: u64 = (x300 + x276); | |
911 | let x303: u64 = ((x299 >> 28) as u64); | |
912 | let x304: u32 = ((x299 & (0xfffffff as u128)) as u32); | |
913 | let x305: u128 = ((x303 as u128) + x268); | |
914 | let x306: u64 = (x302 >> 28); | |
915 | let x307: u32 = ((x302 & (0xfffffff as u64)) as u32); | |
916 | let x308: u64 = (x306 + x275); | |
917 | let x309: u64 = ((x305 >> 28) as u64); | |
918 | let x310: u32 = ((x305 & (0xfffffff as u128)) as u32); | |
919 | let x311: u64 = (x309 + x267); | |
920 | let x312: u64 = (x308 >> 28); | |
921 | let x313: u32 = ((x308 & (0xfffffff as u64)) as u32); | |
922 | let x314: u64 = (x312 + x274); | |
923 | let x315: u64 = (x311 >> 28); | |
924 | let x316: u32 = ((x311 & (0xfffffff as u64)) as u32); | |
925 | let x317: u64 = (x315 + x266); | |
926 | let x318: u64 = (x314 >> 28); | |
927 | let x319: u32 = ((x314 & (0xfffffff as u64)) as u32); | |
928 | let x320: u64 = (x318 + x273); | |
929 | let x321: u64 = (x317 >> 28); | |
930 | let x322: u32 = ((x317 & (0xfffffff as u64)) as u32); | |
931 | let x323: u64 = (x321 + (x282 as u64)); | |
932 | let x324: u64 = (x320 >> 28); | |
933 | let x325: u32 = ((x320 & (0xfffffff as u64)) as u32); | |
934 | let x326: u64 = (x324 + (x264 as u64)); | |
935 | let x327: u32 = ((x323 >> 28) as u32); | |
936 | let x328: u32 = ((x323 & (0xfffffff as u64)) as u32); | |
937 | let x329: u32 = ((x326 >> 28) as u32); | |
938 | let x330: u32 = ((x326 & (0xfffffff as u64)) as u32); | |
939 | let x331: u32 = (x285 + x327); | |
940 | let x332: u32 = (x289 + x327); | |
941 | let x333: u32 = (x329 + x331); | |
942 | let x334: fiat_p448_u1 = ((x333 >> 28) as fiat_p448_u1); | |
943 | let x335: u32 = (x333 & 0xfffffff); | |
944 | let x336: u32 = ((x334 as u32) + x292); | |
945 | let x337: fiat_p448_u1 = ((x332 >> 28) as fiat_p448_u1); | |
946 | let x338: u32 = (x332 & 0xfffffff); | |
947 | let x339: u32 = ((x337 as u32) + x295); | |
948 | out1[0] = x338; | |
949 | out1[1] = x339; | |
950 | out1[2] = x301; | |
951 | out1[3] = x307; | |
952 | out1[4] = x313; | |
953 | out1[5] = x319; | |
954 | out1[6] = x325; | |
955 | out1[7] = x330; | |
956 | out1[8] = x335; | |
957 | out1[9] = x336; | |
958 | out1[10] = x298; | |
959 | out1[11] = x304; | |
960 | out1[12] = x310; | |
961 | out1[13] = x316; | |
962 | out1[14] = x322; | |
963 | out1[15] = x328; | |
964 | } | |
965 | ||
966 | /// The function fiat_p448_carry reduces a field element. | |
967 | /// | |
968 | /// Postconditions: | |
969 | /// eval out1 mod m = eval arg1 mod m | |
970 | /// | |
971 | #[inline] | |
972 | pub fn fiat_p448_carry(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element) -> () { | |
973 | let x1: u32 = (arg1[7]); | |
974 | let x2: u32 = (arg1[15]); | |
975 | let x3: u32 = (x2 >> 28); | |
976 | let x4: u32 = (((x1 >> 28) + (arg1[8])) + x3); | |
977 | let x5: u32 = ((arg1[0]) + x3); | |
978 | let x6: u32 = ((x4 >> 28) + (arg1[9])); | |
979 | let x7: u32 = ((x5 >> 28) + (arg1[1])); | |
980 | let x8: u32 = ((x6 >> 28) + (arg1[10])); | |
981 | let x9: u32 = ((x7 >> 28) + (arg1[2])); | |
982 | let x10: u32 = ((x8 >> 28) + (arg1[11])); | |
983 | let x11: u32 = ((x9 >> 28) + (arg1[3])); | |
984 | let x12: u32 = ((x10 >> 28) + (arg1[12])); | |
985 | let x13: u32 = ((x11 >> 28) + (arg1[4])); | |
986 | let x14: u32 = ((x12 >> 28) + (arg1[13])); | |
987 | let x15: u32 = ((x13 >> 28) + (arg1[5])); | |
988 | let x16: u32 = ((x14 >> 28) + (arg1[14])); | |
989 | let x17: u32 = ((x15 >> 28) + (arg1[6])); | |
990 | let x18: u32 = ((x16 >> 28) + (x2 & 0xfffffff)); | |
991 | let x19: u32 = ((x17 >> 28) + (x1 & 0xfffffff)); | |
992 | let x20: fiat_p448_u1 = ((x18 >> 28) as fiat_p448_u1); | |
993 | let x21: u32 = ((x5 & 0xfffffff) + (x20 as u32)); | |
994 | let x22: u32 = ((((x19 >> 28) as fiat_p448_u1) as u32) + ((x4 & 0xfffffff) + (x20 as u32))); | |
995 | let x23: u32 = (x21 & 0xfffffff); | |
996 | let x24: u32 = ((((x21 >> 28) as fiat_p448_u1) as u32) + (x7 & 0xfffffff)); | |
997 | let x25: u32 = (x9 & 0xfffffff); | |
998 | let x26: u32 = (x11 & 0xfffffff); | |
999 | let x27: u32 = (x13 & 0xfffffff); | |
1000 | let x28: u32 = (x15 & 0xfffffff); | |
1001 | let x29: u32 = (x17 & 0xfffffff); | |
1002 | let x30: u32 = (x19 & 0xfffffff); | |
1003 | let x31: u32 = (x22 & 0xfffffff); | |
1004 | let x32: u32 = ((((x22 >> 28) as fiat_p448_u1) as u32) + (x6 & 0xfffffff)); | |
1005 | let x33: u32 = (x8 & 0xfffffff); | |
1006 | let x34: u32 = (x10 & 0xfffffff); | |
1007 | let x35: u32 = (x12 & 0xfffffff); | |
1008 | let x36: u32 = (x14 & 0xfffffff); | |
1009 | let x37: u32 = (x16 & 0xfffffff); | |
1010 | let x38: u32 = (x18 & 0xfffffff); | |
1011 | out1[0] = x23; | |
1012 | out1[1] = x24; | |
1013 | out1[2] = x25; | |
1014 | out1[3] = x26; | |
1015 | out1[4] = x27; | |
1016 | out1[5] = x28; | |
1017 | out1[6] = x29; | |
1018 | out1[7] = x30; | |
1019 | out1[8] = x31; | |
1020 | out1[9] = x32; | |
1021 | out1[10] = x33; | |
1022 | out1[11] = x34; | |
1023 | out1[12] = x35; | |
1024 | out1[13] = x36; | |
1025 | out1[14] = x37; | |
1026 | out1[15] = x38; | |
1027 | } | |
1028 | ||
1029 | /// The function fiat_p448_add adds two field elements. | |
1030 | /// | |
1031 | /// Postconditions: | |
1032 | /// eval out1 mod m = (eval arg1 + eval arg2) mod m | |
1033 | /// | |
1034 | #[inline] | |
1035 | pub fn fiat_p448_add(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element, arg2: &fiat_p448_tight_field_element) -> () { | |
1036 | let x1: u32 = ((arg1[0]) + (arg2[0])); | |
1037 | let x2: u32 = ((arg1[1]) + (arg2[1])); | |
1038 | let x3: u32 = ((arg1[2]) + (arg2[2])); | |
1039 | let x4: u32 = ((arg1[3]) + (arg2[3])); | |
1040 | let x5: u32 = ((arg1[4]) + (arg2[4])); | |
1041 | let x6: u32 = ((arg1[5]) + (arg2[5])); | |
1042 | let x7: u32 = ((arg1[6]) + (arg2[6])); | |
1043 | let x8: u32 = ((arg1[7]) + (arg2[7])); | |
1044 | let x9: u32 = ((arg1[8]) + (arg2[8])); | |
1045 | let x10: u32 = ((arg1[9]) + (arg2[9])); | |
1046 | let x11: u32 = ((arg1[10]) + (arg2[10])); | |
1047 | let x12: u32 = ((arg1[11]) + (arg2[11])); | |
1048 | let x13: u32 = ((arg1[12]) + (arg2[12])); | |
1049 | let x14: u32 = ((arg1[13]) + (arg2[13])); | |
1050 | let x15: u32 = ((arg1[14]) + (arg2[14])); | |
1051 | let x16: u32 = ((arg1[15]) + (arg2[15])); | |
1052 | out1[0] = x1; | |
1053 | out1[1] = x2; | |
1054 | out1[2] = x3; | |
1055 | out1[3] = x4; | |
1056 | out1[4] = x5; | |
1057 | out1[5] = x6; | |
1058 | out1[6] = x7; | |
1059 | out1[7] = x8; | |
1060 | out1[8] = x9; | |
1061 | out1[9] = x10; | |
1062 | out1[10] = x11; | |
1063 | out1[11] = x12; | |
1064 | out1[12] = x13; | |
1065 | out1[13] = x14; | |
1066 | out1[14] = x15; | |
1067 | out1[15] = x16; | |
1068 | } | |
1069 | ||
1070 | /// The function fiat_p448_sub subtracts two field elements. | |
1071 | /// | |
1072 | /// Postconditions: | |
1073 | /// eval out1 mod m = (eval arg1 - eval arg2) mod m | |
1074 | /// | |
1075 | #[inline] | |
1076 | pub fn fiat_p448_sub(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element, arg2: &fiat_p448_tight_field_element) -> () { | |
1077 | let x1: u32 = ((0x1ffffffe + (arg1[0])) - (arg2[0])); | |
1078 | let x2: u32 = ((0x1ffffffe + (arg1[1])) - (arg2[1])); | |
1079 | let x3: u32 = ((0x1ffffffe + (arg1[2])) - (arg2[2])); | |
1080 | let x4: u32 = ((0x1ffffffe + (arg1[3])) - (arg2[3])); | |
1081 | let x5: u32 = ((0x1ffffffe + (arg1[4])) - (arg2[4])); | |
1082 | let x6: u32 = ((0x1ffffffe + (arg1[5])) - (arg2[5])); | |
1083 | let x7: u32 = ((0x1ffffffe + (arg1[6])) - (arg2[6])); | |
1084 | let x8: u32 = ((0x1ffffffe + (arg1[7])) - (arg2[7])); | |
1085 | let x9: u32 = ((0x1ffffffc + (arg1[8])) - (arg2[8])); | |
1086 | let x10: u32 = ((0x1ffffffe + (arg1[9])) - (arg2[9])); | |
1087 | let x11: u32 = ((0x1ffffffe + (arg1[10])) - (arg2[10])); | |
1088 | let x12: u32 = ((0x1ffffffe + (arg1[11])) - (arg2[11])); | |
1089 | let x13: u32 = ((0x1ffffffe + (arg1[12])) - (arg2[12])); | |
1090 | let x14: u32 = ((0x1ffffffe + (arg1[13])) - (arg2[13])); | |
1091 | let x15: u32 = ((0x1ffffffe + (arg1[14])) - (arg2[14])); | |
1092 | let x16: u32 = ((0x1ffffffe + (arg1[15])) - (arg2[15])); | |
1093 | out1[0] = x1; | |
1094 | out1[1] = x2; | |
1095 | out1[2] = x3; | |
1096 | out1[3] = x4; | |
1097 | out1[4] = x5; | |
1098 | out1[5] = x6; | |
1099 | out1[6] = x7; | |
1100 | out1[7] = x8; | |
1101 | out1[8] = x9; | |
1102 | out1[9] = x10; | |
1103 | out1[10] = x11; | |
1104 | out1[11] = x12; | |
1105 | out1[12] = x13; | |
1106 | out1[13] = x14; | |
1107 | out1[14] = x15; | |
1108 | out1[15] = x16; | |
1109 | } | |
1110 | ||
1111 | /// The function fiat_p448_opp negates a field element. | |
1112 | /// | |
1113 | /// Postconditions: | |
1114 | /// eval out1 mod m = -eval arg1 mod m | |
1115 | /// | |
1116 | #[inline] | |
1117 | pub fn fiat_p448_opp(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element) -> () { | |
1118 | let x1: u32 = (0x1ffffffe - (arg1[0])); | |
1119 | let x2: u32 = (0x1ffffffe - (arg1[1])); | |
1120 | let x3: u32 = (0x1ffffffe - (arg1[2])); | |
1121 | let x4: u32 = (0x1ffffffe - (arg1[3])); | |
1122 | let x5: u32 = (0x1ffffffe - (arg1[4])); | |
1123 | let x6: u32 = (0x1ffffffe - (arg1[5])); | |
1124 | let x7: u32 = (0x1ffffffe - (arg1[6])); | |
1125 | let x8: u32 = (0x1ffffffe - (arg1[7])); | |
1126 | let x9: u32 = (0x1ffffffc - (arg1[8])); | |
1127 | let x10: u32 = (0x1ffffffe - (arg1[9])); | |
1128 | let x11: u32 = (0x1ffffffe - (arg1[10])); | |
1129 | let x12: u32 = (0x1ffffffe - (arg1[11])); | |
1130 | let x13: u32 = (0x1ffffffe - (arg1[12])); | |
1131 | let x14: u32 = (0x1ffffffe - (arg1[13])); | |
1132 | let x15: u32 = (0x1ffffffe - (arg1[14])); | |
1133 | let x16: u32 = (0x1ffffffe - (arg1[15])); | |
1134 | out1[0] = x1; | |
1135 | out1[1] = x2; | |
1136 | out1[2] = x3; | |
1137 | out1[3] = x4; | |
1138 | out1[4] = x5; | |
1139 | out1[5] = x6; | |
1140 | out1[6] = x7; | |
1141 | out1[7] = x8; | |
1142 | out1[8] = x9; | |
1143 | out1[9] = x10; | |
1144 | out1[10] = x11; | |
1145 | out1[11] = x12; | |
1146 | out1[12] = x13; | |
1147 | out1[13] = x14; | |
1148 | out1[14] = x15; | |
1149 | out1[15] = x16; | |
1150 | } | |
1151 | ||
1152 | /// The function fiat_p448_selectznz is a multi-limb conditional select. | |
1153 | /// | |
1154 | /// Postconditions: | |
1155 | /// out1 = (if arg1 = 0 then arg2 else arg3) | |
1156 | /// | |
1157 | /// Input Bounds: | |
1158 | /// arg1: [0x0 ~> 0x1] | |
1159 | /// arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] | |
1160 | /// arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] | |
1161 | /// Output Bounds: | |
1162 | /// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] | |
1163 | #[inline] | |
1164 | pub fn fiat_p448_selectznz(out1: &mut [u32; 16], arg1: fiat_p448_u1, arg2: &[u32; 16], arg3: &[u32; 16]) -> () { | |
1165 | let mut x1: u32 = 0; | |
1166 | fiat_p448_cmovznz_u32(&mut x1, arg1, (arg2[0]), (arg3[0])); | |
1167 | let mut x2: u32 = 0; | |
1168 | fiat_p448_cmovznz_u32(&mut x2, arg1, (arg2[1]), (arg3[1])); | |
1169 | let mut x3: u32 = 0; | |
1170 | fiat_p448_cmovznz_u32(&mut x3, arg1, (arg2[2]), (arg3[2])); | |
1171 | let mut x4: u32 = 0; | |
1172 | fiat_p448_cmovznz_u32(&mut x4, arg1, (arg2[3]), (arg3[3])); | |
1173 | let mut x5: u32 = 0; | |
1174 | fiat_p448_cmovznz_u32(&mut x5, arg1, (arg2[4]), (arg3[4])); | |
1175 | let mut x6: u32 = 0; | |
1176 | fiat_p448_cmovznz_u32(&mut x6, arg1, (arg2[5]), (arg3[5])); | |
1177 | let mut x7: u32 = 0; | |
1178 | fiat_p448_cmovznz_u32(&mut x7, arg1, (arg2[6]), (arg3[6])); | |
1179 | let mut x8: u32 = 0; | |
1180 | fiat_p448_cmovznz_u32(&mut x8, arg1, (arg2[7]), (arg3[7])); | |
1181 | let mut x9: u32 = 0; | |
1182 | fiat_p448_cmovznz_u32(&mut x9, arg1, (arg2[8]), (arg3[8])); | |
1183 | let mut x10: u32 = 0; | |
1184 | fiat_p448_cmovznz_u32(&mut x10, arg1, (arg2[9]), (arg3[9])); | |
1185 | let mut x11: u32 = 0; | |
1186 | fiat_p448_cmovznz_u32(&mut x11, arg1, (arg2[10]), (arg3[10])); | |
1187 | let mut x12: u32 = 0; | |
1188 | fiat_p448_cmovznz_u32(&mut x12, arg1, (arg2[11]), (arg3[11])); | |
1189 | let mut x13: u32 = 0; | |
1190 | fiat_p448_cmovznz_u32(&mut x13, arg1, (arg2[12]), (arg3[12])); | |
1191 | let mut x14: u32 = 0; | |
1192 | fiat_p448_cmovznz_u32(&mut x14, arg1, (arg2[13]), (arg3[13])); | |
1193 | let mut x15: u32 = 0; | |
1194 | fiat_p448_cmovznz_u32(&mut x15, arg1, (arg2[14]), (arg3[14])); | |
1195 | let mut x16: u32 = 0; | |
1196 | fiat_p448_cmovznz_u32(&mut x16, arg1, (arg2[15]), (arg3[15])); | |
1197 | out1[0] = x1; | |
1198 | out1[1] = x2; | |
1199 | out1[2] = x3; | |
1200 | out1[3] = x4; | |
1201 | out1[4] = x5; | |
1202 | out1[5] = x6; | |
1203 | out1[6] = x7; | |
1204 | out1[7] = x8; | |
1205 | out1[8] = x9; | |
1206 | out1[9] = x10; | |
1207 | out1[10] = x11; | |
1208 | out1[11] = x12; | |
1209 | out1[12] = x13; | |
1210 | out1[13] = x14; | |
1211 | out1[14] = x15; | |
1212 | out1[15] = x16; | |
1213 | } | |
1214 | ||
1215 | /// The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order. | |
1216 | /// | |
1217 | /// Postconditions: | |
1218 | /// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55] | |
1219 | /// | |
1220 | /// Output Bounds: | |
1221 | /// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] | |
1222 | #[inline] | |
1223 | pub fn fiat_p448_to_bytes(out1: &mut [u8; 56], arg1: &fiat_p448_tight_field_element) -> () { | |
1224 | let mut x1: u32 = 0; | |
1225 | let mut x2: fiat_p448_u1 = 0; | |
1226 | fiat_p448_subborrowx_u28(&mut x1, &mut x2, 0x0, (arg1[0]), 0xfffffff); | |
1227 | let mut x3: u32 = 0; | |
1228 | let mut x4: fiat_p448_u1 = 0; | |
1229 | fiat_p448_subborrowx_u28(&mut x3, &mut x4, x2, (arg1[1]), 0xfffffff); | |
1230 | let mut x5: u32 = 0; | |
1231 | let mut x6: fiat_p448_u1 = 0; | |
1232 | fiat_p448_subborrowx_u28(&mut x5, &mut x6, x4, (arg1[2]), 0xfffffff); | |
1233 | let mut x7: u32 = 0; | |
1234 | let mut x8: fiat_p448_u1 = 0; | |
1235 | fiat_p448_subborrowx_u28(&mut x7, &mut x8, x6, (arg1[3]), 0xfffffff); | |
1236 | let mut x9: u32 = 0; | |
1237 | let mut x10: fiat_p448_u1 = 0; | |
1238 | fiat_p448_subborrowx_u28(&mut x9, &mut x10, x8, (arg1[4]), 0xfffffff); | |
1239 | let mut x11: u32 = 0; | |
1240 | let mut x12: fiat_p448_u1 = 0; | |
1241 | fiat_p448_subborrowx_u28(&mut x11, &mut x12, x10, (arg1[5]), 0xfffffff); | |
1242 | let mut x13: u32 = 0; | |
1243 | let mut x14: fiat_p448_u1 = 0; | |
1244 | fiat_p448_subborrowx_u28(&mut x13, &mut x14, x12, (arg1[6]), 0xfffffff); | |
1245 | let mut x15: u32 = 0; | |
1246 | let mut x16: fiat_p448_u1 = 0; | |
1247 | fiat_p448_subborrowx_u28(&mut x15, &mut x16, x14, (arg1[7]), 0xfffffff); | |
1248 | let mut x17: u32 = 0; | |
1249 | let mut x18: fiat_p448_u1 = 0; | |
1250 | fiat_p448_subborrowx_u28(&mut x17, &mut x18, x16, (arg1[8]), 0xffffffe); | |
1251 | let mut x19: u32 = 0; | |
1252 | let mut x20: fiat_p448_u1 = 0; | |
1253 | fiat_p448_subborrowx_u28(&mut x19, &mut x20, x18, (arg1[9]), 0xfffffff); | |
1254 | let mut x21: u32 = 0; | |
1255 | let mut x22: fiat_p448_u1 = 0; | |
1256 | fiat_p448_subborrowx_u28(&mut x21, &mut x22, x20, (arg1[10]), 0xfffffff); | |
1257 | let mut x23: u32 = 0; | |
1258 | let mut x24: fiat_p448_u1 = 0; | |
1259 | fiat_p448_subborrowx_u28(&mut x23, &mut x24, x22, (arg1[11]), 0xfffffff); | |
1260 | let mut x25: u32 = 0; | |
1261 | let mut x26: fiat_p448_u1 = 0; | |
1262 | fiat_p448_subborrowx_u28(&mut x25, &mut x26, x24, (arg1[12]), 0xfffffff); | |
1263 | let mut x27: u32 = 0; | |
1264 | let mut x28: fiat_p448_u1 = 0; | |
1265 | fiat_p448_subborrowx_u28(&mut x27, &mut x28, x26, (arg1[13]), 0xfffffff); | |
1266 | let mut x29: u32 = 0; | |
1267 | let mut x30: fiat_p448_u1 = 0; | |
1268 | fiat_p448_subborrowx_u28(&mut x29, &mut x30, x28, (arg1[14]), 0xfffffff); | |
1269 | let mut x31: u32 = 0; | |
1270 | let mut x32: fiat_p448_u1 = 0; | |
1271 | fiat_p448_subborrowx_u28(&mut x31, &mut x32, x30, (arg1[15]), 0xfffffff); | |
1272 | let mut x33: u32 = 0; | |
1273 | fiat_p448_cmovznz_u32(&mut x33, x32, (0x0 as u32), 0xffffffff); | |
1274 | let mut x34: u32 = 0; | |
1275 | let mut x35: fiat_p448_u1 = 0; | |
1276 | fiat_p448_addcarryx_u28(&mut x34, &mut x35, 0x0, x1, (x33 & 0xfffffff)); | |
1277 | let mut x36: u32 = 0; | |
1278 | let mut x37: fiat_p448_u1 = 0; | |
1279 | fiat_p448_addcarryx_u28(&mut x36, &mut x37, x35, x3, (x33 & 0xfffffff)); | |
1280 | let mut x38: u32 = 0; | |
1281 | let mut x39: fiat_p448_u1 = 0; | |
1282 | fiat_p448_addcarryx_u28(&mut x38, &mut x39, x37, x5, (x33 & 0xfffffff)); | |
1283 | let mut x40: u32 = 0; | |
1284 | let mut x41: fiat_p448_u1 = 0; | |
1285 | fiat_p448_addcarryx_u28(&mut x40, &mut x41, x39, x7, (x33 & 0xfffffff)); | |
1286 | let mut x42: u32 = 0; | |
1287 | let mut x43: fiat_p448_u1 = 0; | |
1288 | fiat_p448_addcarryx_u28(&mut x42, &mut x43, x41, x9, (x33 & 0xfffffff)); | |
1289 | let mut x44: u32 = 0; | |
1290 | let mut x45: fiat_p448_u1 = 0; | |
1291 | fiat_p448_addcarryx_u28(&mut x44, &mut x45, x43, x11, (x33 & 0xfffffff)); | |
1292 | let mut x46: u32 = 0; | |
1293 | let mut x47: fiat_p448_u1 = 0; | |
1294 | fiat_p448_addcarryx_u28(&mut x46, &mut x47, x45, x13, (x33 & 0xfffffff)); | |
1295 | let mut x48: u32 = 0; | |
1296 | let mut x49: fiat_p448_u1 = 0; | |
1297 | fiat_p448_addcarryx_u28(&mut x48, &mut x49, x47, x15, (x33 & 0xfffffff)); | |
1298 | let mut x50: u32 = 0; | |
1299 | let mut x51: fiat_p448_u1 = 0; | |
1300 | fiat_p448_addcarryx_u28(&mut x50, &mut x51, x49, x17, (x33 & 0xffffffe)); | |
1301 | let mut x52: u32 = 0; | |
1302 | let mut x53: fiat_p448_u1 = 0; | |
1303 | fiat_p448_addcarryx_u28(&mut x52, &mut x53, x51, x19, (x33 & 0xfffffff)); | |
1304 | let mut x54: u32 = 0; | |
1305 | let mut x55: fiat_p448_u1 = 0; | |
1306 | fiat_p448_addcarryx_u28(&mut x54, &mut x55, x53, x21, (x33 & 0xfffffff)); | |
1307 | let mut x56: u32 = 0; | |
1308 | let mut x57: fiat_p448_u1 = 0; | |
1309 | fiat_p448_addcarryx_u28(&mut x56, &mut x57, x55, x23, (x33 & 0xfffffff)); | |
1310 | let mut x58: u32 = 0; | |
1311 | let mut x59: fiat_p448_u1 = 0; | |
1312 | fiat_p448_addcarryx_u28(&mut x58, &mut x59, x57, x25, (x33 & 0xfffffff)); | |
1313 | let mut x60: u32 = 0; | |
1314 | let mut x61: fiat_p448_u1 = 0; | |
1315 | fiat_p448_addcarryx_u28(&mut x60, &mut x61, x59, x27, (x33 & 0xfffffff)); | |
1316 | let mut x62: u32 = 0; | |
1317 | let mut x63: fiat_p448_u1 = 0; | |
1318 | fiat_p448_addcarryx_u28(&mut x62, &mut x63, x61, x29, (x33 & 0xfffffff)); | |
1319 | let mut x64: u32 = 0; | |
1320 | let mut x65: fiat_p448_u1 = 0; | |
1321 | fiat_p448_addcarryx_u28(&mut x64, &mut x65, x63, x31, (x33 & 0xfffffff)); | |
1322 | let x66: u32 = (x64 << 4); | |
1323 | let x67: u32 = (x60 << 4); | |
1324 | let x68: u32 = (x56 << 4); | |
1325 | let x69: u32 = (x52 << 4); | |
1326 | let x70: u32 = (x48 << 4); | |
1327 | let x71: u32 = (x44 << 4); | |
1328 | let x72: u32 = (x40 << 4); | |
1329 | let x73: u32 = (x36 << 4); | |
1330 | let x74: u8 = ((x34 & (0xff as u32)) as u8); | |
1331 | let x75: u32 = (x34 >> 8); | |
1332 | let x76: u8 = ((x75 & (0xff as u32)) as u8); | |
1333 | let x77: u32 = (x75 >> 8); | |
1334 | let x78: u8 = ((x77 & (0xff as u32)) as u8); | |
1335 | let x79: u8 = ((x77 >> 8) as u8); | |
1336 | let x80: u32 = (x73 + (x79 as u32)); | |
1337 | let x81: u8 = ((x80 & (0xff as u32)) as u8); | |
1338 | let x82: u32 = (x80 >> 8); | |
1339 | let x83: u8 = ((x82 & (0xff as u32)) as u8); | |
1340 | let x84: u32 = (x82 >> 8); | |
1341 | let x85: u8 = ((x84 & (0xff as u32)) as u8); | |
1342 | let x86: u8 = ((x84 >> 8) as u8); | |
1343 | let x87: u8 = ((x38 & (0xff as u32)) as u8); | |
1344 | let x88: u32 = (x38 >> 8); | |
1345 | let x89: u8 = ((x88 & (0xff as u32)) as u8); | |
1346 | let x90: u32 = (x88 >> 8); | |
1347 | let x91: u8 = ((x90 & (0xff as u32)) as u8); | |
1348 | let x92: u8 = ((x90 >> 8) as u8); | |
1349 | let x93: u32 = (x72 + (x92 as u32)); | |
1350 | let x94: u8 = ((x93 & (0xff as u32)) as u8); | |
1351 | let x95: u32 = (x93 >> 8); | |
1352 | let x96: u8 = ((x95 & (0xff as u32)) as u8); | |
1353 | let x97: u32 = (x95 >> 8); | |
1354 | let x98: u8 = ((x97 & (0xff as u32)) as u8); | |
1355 | let x99: u8 = ((x97 >> 8) as u8); | |
1356 | let x100: u8 = ((x42 & (0xff as u32)) as u8); | |
1357 | let x101: u32 = (x42 >> 8); | |
1358 | let x102: u8 = ((x101 & (0xff as u32)) as u8); | |
1359 | let x103: u32 = (x101 >> 8); | |
1360 | let x104: u8 = ((x103 & (0xff as u32)) as u8); | |
1361 | let x105: u8 = ((x103 >> 8) as u8); | |
1362 | let x106: u32 = (x71 + (x105 as u32)); | |
1363 | let x107: u8 = ((x106 & (0xff as u32)) as u8); | |
1364 | let x108: u32 = (x106 >> 8); | |
1365 | let x109: u8 = ((x108 & (0xff as u32)) as u8); | |
1366 | let x110: u32 = (x108 >> 8); | |
1367 | let x111: u8 = ((x110 & (0xff as u32)) as u8); | |
1368 | let x112: u8 = ((x110 >> 8) as u8); | |
1369 | let x113: u8 = ((x46 & (0xff as u32)) as u8); | |
1370 | let x114: u32 = (x46 >> 8); | |
1371 | let x115: u8 = ((x114 & (0xff as u32)) as u8); | |
1372 | let x116: u32 = (x114 >> 8); | |
1373 | let x117: u8 = ((x116 & (0xff as u32)) as u8); | |
1374 | let x118: u8 = ((x116 >> 8) as u8); | |
1375 | let x119: u32 = (x70 + (x118 as u32)); | |
1376 | let x120: u8 = ((x119 & (0xff as u32)) as u8); | |
1377 | let x121: u32 = (x119 >> 8); | |
1378 | let x122: u8 = ((x121 & (0xff as u32)) as u8); | |
1379 | let x123: u32 = (x121 >> 8); | |
1380 | let x124: u8 = ((x123 & (0xff as u32)) as u8); | |
1381 | let x125: u8 = ((x123 >> 8) as u8); | |
1382 | let x126: u8 = ((x50 & (0xff as u32)) as u8); | |
1383 | let x127: u32 = (x50 >> 8); | |
1384 | let x128: u8 = ((x127 & (0xff as u32)) as u8); | |
1385 | let x129: u32 = (x127 >> 8); | |
1386 | let x130: u8 = ((x129 & (0xff as u32)) as u8); | |
1387 | let x131: u8 = ((x129 >> 8) as u8); | |
1388 | let x132: u32 = (x69 + (x131 as u32)); | |
1389 | let x133: u8 = ((x132 & (0xff as u32)) as u8); | |
1390 | let x134: u32 = (x132 >> 8); | |
1391 | let x135: u8 = ((x134 & (0xff as u32)) as u8); | |
1392 | let x136: u32 = (x134 >> 8); | |
1393 | let x137: u8 = ((x136 & (0xff as u32)) as u8); | |
1394 | let x138: u8 = ((x136 >> 8) as u8); | |
1395 | let x139: u8 = ((x54 & (0xff as u32)) as u8); | |
1396 | let x140: u32 = (x54 >> 8); | |
1397 | let x141: u8 = ((x140 & (0xff as u32)) as u8); | |
1398 | let x142: u32 = (x140 >> 8); | |
1399 | let x143: u8 = ((x142 & (0xff as u32)) as u8); | |
1400 | let x144: u8 = ((x142 >> 8) as u8); | |
1401 | let x145: u32 = (x68 + (x144 as u32)); | |
1402 | let x146: u8 = ((x145 & (0xff as u32)) as u8); | |
1403 | let x147: u32 = (x145 >> 8); | |
1404 | let x148: u8 = ((x147 & (0xff as u32)) as u8); | |
1405 | let x149: u32 = (x147 >> 8); | |
1406 | let x150: u8 = ((x149 & (0xff as u32)) as u8); | |
1407 | let x151: u8 = ((x149 >> 8) as u8); | |
1408 | let x152: u8 = ((x58 & (0xff as u32)) as u8); | |
1409 | let x153: u32 = (x58 >> 8); | |
1410 | let x154: u8 = ((x153 & (0xff as u32)) as u8); | |
1411 | let x155: u32 = (x153 >> 8); | |
1412 | let x156: u8 = ((x155 & (0xff as u32)) as u8); | |
1413 | let x157: u8 = ((x155 >> 8) as u8); | |
1414 | let x158: u32 = (x67 + (x157 as u32)); | |
1415 | let x159: u8 = ((x158 & (0xff as u32)) as u8); | |
1416 | let x160: u32 = (x158 >> 8); | |
1417 | let x161: u8 = ((x160 & (0xff as u32)) as u8); | |
1418 | let x162: u32 = (x160 >> 8); | |
1419 | let x163: u8 = ((x162 & (0xff as u32)) as u8); | |
1420 | let x164: u8 = ((x162 >> 8) as u8); | |
1421 | let x165: u8 = ((x62 & (0xff as u32)) as u8); | |
1422 | let x166: u32 = (x62 >> 8); | |
1423 | let x167: u8 = ((x166 & (0xff as u32)) as u8); | |
1424 | let x168: u32 = (x166 >> 8); | |
1425 | let x169: u8 = ((x168 & (0xff as u32)) as u8); | |
1426 | let x170: u8 = ((x168 >> 8) as u8); | |
1427 | let x171: u32 = (x66 + (x170 as u32)); | |
1428 | let x172: u8 = ((x171 & (0xff as u32)) as u8); | |
1429 | let x173: u32 = (x171 >> 8); | |
1430 | let x174: u8 = ((x173 & (0xff as u32)) as u8); | |
1431 | let x175: u32 = (x173 >> 8); | |
1432 | let x176: u8 = ((x175 & (0xff as u32)) as u8); | |
1433 | let x177: u8 = ((x175 >> 8) as u8); | |
1434 | out1[0] = x74; | |
1435 | out1[1] = x76; | |
1436 | out1[2] = x78; | |
1437 | out1[3] = x81; | |
1438 | out1[4] = x83; | |
1439 | out1[5] = x85; | |
1440 | out1[6] = x86; | |
1441 | out1[7] = x87; | |
1442 | out1[8] = x89; | |
1443 | out1[9] = x91; | |
1444 | out1[10] = x94; | |
1445 | out1[11] = x96; | |
1446 | out1[12] = x98; | |
1447 | out1[13] = x99; | |
1448 | out1[14] = x100; | |
1449 | out1[15] = x102; | |
1450 | out1[16] = x104; | |
1451 | out1[17] = x107; | |
1452 | out1[18] = x109; | |
1453 | out1[19] = x111; | |
1454 | out1[20] = x112; | |
1455 | out1[21] = x113; | |
1456 | out1[22] = x115; | |
1457 | out1[23] = x117; | |
1458 | out1[24] = x120; | |
1459 | out1[25] = x122; | |
1460 | out1[26] = x124; | |
1461 | out1[27] = x125; | |
1462 | out1[28] = x126; | |
1463 | out1[29] = x128; | |
1464 | out1[30] = x130; | |
1465 | out1[31] = x133; | |
1466 | out1[32] = x135; | |
1467 | out1[33] = x137; | |
1468 | out1[34] = x138; | |
1469 | out1[35] = x139; | |
1470 | out1[36] = x141; | |
1471 | out1[37] = x143; | |
1472 | out1[38] = x146; | |
1473 | out1[39] = x148; | |
1474 | out1[40] = x150; | |
1475 | out1[41] = x151; | |
1476 | out1[42] = x152; | |
1477 | out1[43] = x154; | |
1478 | out1[44] = x156; | |
1479 | out1[45] = x159; | |
1480 | out1[46] = x161; | |
1481 | out1[47] = x163; | |
1482 | out1[48] = x164; | |
1483 | out1[49] = x165; | |
1484 | out1[50] = x167; | |
1485 | out1[51] = x169; | |
1486 | out1[52] = x172; | |
1487 | out1[53] = x174; | |
1488 | out1[54] = x176; | |
1489 | out1[55] = x177; | |
1490 | } | |
1491 | ||
1492 | /// The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order. | |
1493 | /// | |
1494 | /// Postconditions: | |
1495 | /// eval out1 mod m = bytes_eval arg1 mod m | |
1496 | /// | |
1497 | /// Input Bounds: | |
1498 | /// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] | |
1499 | #[inline] | |
1500 | pub fn fiat_p448_from_bytes(out1: &mut fiat_p448_tight_field_element, arg1: &[u8; 56]) -> () { | |
1501 | let x1: u32 = (((arg1[55]) as u32) << 20); | |
1502 | let x2: u32 = (((arg1[54]) as u32) << 12); | |
1503 | let x3: u32 = (((arg1[53]) as u32) << 4); | |
1504 | let x4: u32 = (((arg1[52]) as u32) << 24); | |
1505 | let x5: u32 = (((arg1[51]) as u32) << 16); | |
1506 | let x6: u32 = (((arg1[50]) as u32) << 8); | |
1507 | let x7: u8 = (arg1[49]); | |
1508 | let x8: u32 = (((arg1[48]) as u32) << 20); | |
1509 | let x9: u32 = (((arg1[47]) as u32) << 12); | |
1510 | let x10: u32 = (((arg1[46]) as u32) << 4); | |
1511 | let x11: u32 = (((arg1[45]) as u32) << 24); | |
1512 | let x12: u32 = (((arg1[44]) as u32) << 16); | |
1513 | let x13: u32 = (((arg1[43]) as u32) << 8); | |
1514 | let x14: u8 = (arg1[42]); | |
1515 | let x15: u32 = (((arg1[41]) as u32) << 20); | |
1516 | let x16: u32 = (((arg1[40]) as u32) << 12); | |
1517 | let x17: u32 = (((arg1[39]) as u32) << 4); | |
1518 | let x18: u32 = (((arg1[38]) as u32) << 24); | |
1519 | let x19: u32 = (((arg1[37]) as u32) << 16); | |
1520 | let x20: u32 = (((arg1[36]) as u32) << 8); | |
1521 | let x21: u8 = (arg1[35]); | |
1522 | let x22: u32 = (((arg1[34]) as u32) << 20); | |
1523 | let x23: u32 = (((arg1[33]) as u32) << 12); | |
1524 | let x24: u32 = (((arg1[32]) as u32) << 4); | |
1525 | let x25: u32 = (((arg1[31]) as u32) << 24); | |
1526 | let x26: u32 = (((arg1[30]) as u32) << 16); | |
1527 | let x27: u32 = (((arg1[29]) as u32) << 8); | |
1528 | let x28: u8 = (arg1[28]); | |
1529 | let x29: u32 = (((arg1[27]) as u32) << 20); | |
1530 | let x30: u32 = (((arg1[26]) as u32) << 12); | |
1531 | let x31: u32 = (((arg1[25]) as u32) << 4); | |
1532 | let x32: u32 = (((arg1[24]) as u32) << 24); | |
1533 | let x33: u32 = (((arg1[23]) as u32) << 16); | |
1534 | let x34: u32 = (((arg1[22]) as u32) << 8); | |
1535 | let x35: u8 = (arg1[21]); | |
1536 | let x36: u32 = (((arg1[20]) as u32) << 20); | |
1537 | let x37: u32 = (((arg1[19]) as u32) << 12); | |
1538 | let x38: u32 = (((arg1[18]) as u32) << 4); | |
1539 | let x39: u32 = (((arg1[17]) as u32) << 24); | |
1540 | let x40: u32 = (((arg1[16]) as u32) << 16); | |
1541 | let x41: u32 = (((arg1[15]) as u32) << 8); | |
1542 | let x42: u8 = (arg1[14]); | |
1543 | let x43: u32 = (((arg1[13]) as u32) << 20); | |
1544 | let x44: u32 = (((arg1[12]) as u32) << 12); | |
1545 | let x45: u32 = (((arg1[11]) as u32) << 4); | |
1546 | let x46: u32 = (((arg1[10]) as u32) << 24); | |
1547 | let x47: u32 = (((arg1[9]) as u32) << 16); | |
1548 | let x48: u32 = (((arg1[8]) as u32) << 8); | |
1549 | let x49: u8 = (arg1[7]); | |
1550 | let x50: u32 = (((arg1[6]) as u32) << 20); | |
1551 | let x51: u32 = (((arg1[5]) as u32) << 12); | |
1552 | let x52: u32 = (((arg1[4]) as u32) << 4); | |
1553 | let x53: u32 = (((arg1[3]) as u32) << 24); | |
1554 | let x54: u32 = (((arg1[2]) as u32) << 16); | |
1555 | let x55: u32 = (((arg1[1]) as u32) << 8); | |
1556 | let x56: u8 = (arg1[0]); | |
1557 | let x57: u32 = (x55 + (x56 as u32)); | |
1558 | let x58: u32 = (x54 + x57); | |
1559 | let x59: u32 = (x53 + x58); | |
1560 | let x60: u32 = (x59 & 0xfffffff); | |
1561 | let x61: u8 = ((x59 >> 28) as u8); | |
1562 | let x62: u32 = (x52 + (x61 as u32)); | |
1563 | let x63: u32 = (x51 + x62); | |
1564 | let x64: u32 = (x50 + x63); | |
1565 | let x65: u32 = (x48 + (x49 as u32)); | |
1566 | let x66: u32 = (x47 + x65); | |
1567 | let x67: u32 = (x46 + x66); | |
1568 | let x68: u32 = (x67 & 0xfffffff); | |
1569 | let x69: u8 = ((x67 >> 28) as u8); | |
1570 | let x70: u32 = (x45 + (x69 as u32)); | |
1571 | let x71: u32 = (x44 + x70); | |
1572 | let x72: u32 = (x43 + x71); | |
1573 | let x73: u32 = (x41 + (x42 as u32)); | |
1574 | let x74: u32 = (x40 + x73); | |
1575 | let x75: u32 = (x39 + x74); | |
1576 | let x76: u32 = (x75 & 0xfffffff); | |
1577 | let x77: u8 = ((x75 >> 28) as u8); | |
1578 | let x78: u32 = (x38 + (x77 as u32)); | |
1579 | let x79: u32 = (x37 + x78); | |
1580 | let x80: u32 = (x36 + x79); | |
1581 | let x81: u32 = (x34 + (x35 as u32)); | |
1582 | let x82: u32 = (x33 + x81); | |
1583 | let x83: u32 = (x32 + x82); | |
1584 | let x84: u32 = (x83 & 0xfffffff); | |
1585 | let x85: u8 = ((x83 >> 28) as u8); | |
1586 | let x86: u32 = (x31 + (x85 as u32)); | |
1587 | let x87: u32 = (x30 + x86); | |
1588 | let x88: u32 = (x29 + x87); | |
1589 | let x89: u32 = (x27 + (x28 as u32)); | |
1590 | let x90: u32 = (x26 + x89); | |
1591 | let x91: u32 = (x25 + x90); | |
1592 | let x92: u32 = (x91 & 0xfffffff); | |
1593 | let x93: u8 = ((x91 >> 28) as u8); | |
1594 | let x94: u32 = (x24 + (x93 as u32)); | |
1595 | let x95: u32 = (x23 + x94); | |
1596 | let x96: u32 = (x22 + x95); | |
1597 | let x97: u32 = (x20 + (x21 as u32)); | |
1598 | let x98: u32 = (x19 + x97); | |
1599 | let x99: u32 = (x18 + x98); | |
1600 | let x100: u32 = (x99 & 0xfffffff); | |
1601 | let x101: u8 = ((x99 >> 28) as u8); | |
1602 | let x102: u32 = (x17 + (x101 as u32)); | |
1603 | let x103: u32 = (x16 + x102); | |
1604 | let x104: u32 = (x15 + x103); | |
1605 | let x105: u32 = (x13 + (x14 as u32)); | |
1606 | let x106: u32 = (x12 + x105); | |
1607 | let x107: u32 = (x11 + x106); | |
1608 | let x108: u32 = (x107 & 0xfffffff); | |
1609 | let x109: u8 = ((x107 >> 28) as u8); | |
1610 | let x110: u32 = (x10 + (x109 as u32)); | |
1611 | let x111: u32 = (x9 + x110); | |
1612 | let x112: u32 = (x8 + x111); | |
1613 | let x113: u32 = (x6 + (x7 as u32)); | |
1614 | let x114: u32 = (x5 + x113); | |
1615 | let x115: u32 = (x4 + x114); | |
1616 | let x116: u32 = (x115 & 0xfffffff); | |
1617 | let x117: u8 = ((x115 >> 28) as u8); | |
1618 | let x118: u32 = (x3 + (x117 as u32)); | |
1619 | let x119: u32 = (x2 + x118); | |
1620 | let x120: u32 = (x1 + x119); | |
1621 | out1[0] = x60; | |
1622 | out1[1] = x64; | |
1623 | out1[2] = x68; | |
1624 | out1[3] = x72; | |
1625 | out1[4] = x76; | |
1626 | out1[5] = x80; | |
1627 | out1[6] = x84; | |
1628 | out1[7] = x88; | |
1629 | out1[8] = x92; | |
1630 | out1[9] = x96; | |
1631 | out1[10] = x100; | |
1632 | out1[11] = x104; | |
1633 | out1[12] = x108; | |
1634 | out1[13] = x112; | |
1635 | out1[14] = x116; | |
1636 | out1[15] = x120; | |
1637 | } | |
1638 | ||
1639 | /// The function fiat_p448_relax is the identity function converting from tight field elements to loose field elements. | |
1640 | /// | |
1641 | /// Postconditions: | |
1642 | /// out1 = arg1 | |
1643 | /// | |
1644 | #[inline] | |
1645 | pub fn fiat_p448_relax(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element) -> () { | |
1646 | let x1: u32 = (arg1[0]); | |
1647 | let x2: u32 = (arg1[1]); | |
1648 | let x3: u32 = (arg1[2]); | |
1649 | let x4: u32 = (arg1[3]); | |
1650 | let x5: u32 = (arg1[4]); | |
1651 | let x6: u32 = (arg1[5]); | |
1652 | let x7: u32 = (arg1[6]); | |
1653 | let x8: u32 = (arg1[7]); | |
1654 | let x9: u32 = (arg1[8]); | |
1655 | let x10: u32 = (arg1[9]); | |
1656 | let x11: u32 = (arg1[10]); | |
1657 | let x12: u32 = (arg1[11]); | |
1658 | let x13: u32 = (arg1[12]); | |
1659 | let x14: u32 = (arg1[13]); | |
1660 | let x15: u32 = (arg1[14]); | |
1661 | let x16: u32 = (arg1[15]); | |
1662 | out1[0] = x1; | |
1663 | out1[1] = x2; | |
1664 | out1[2] = x3; | |
1665 | out1[3] = x4; | |
1666 | out1[4] = x5; | |
1667 | out1[5] = x6; | |
1668 | out1[6] = x7; | |
1669 | out1[7] = x8; | |
1670 | out1[8] = x9; | |
1671 | out1[9] = x10; | |
1672 | out1[10] = x11; | |
1673 | out1[11] = x12; | |
1674 | out1[12] = x13; | |
1675 | out1[13] = x14; | |
1676 | out1[14] = x15; | |
1677 | out1[15] = x16; | |
1678 | } |