|
6 | 6 | #include "int128.h"
|
7 | 7 | #include "util.h"
|
8 | 8 |
|
9 |
| -/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static |
10 |
| - * --use-value-barrier secp256k1_dettman 64 5 48 2 '2^256 - 4294968273' mul |
11 |
| - * square */ |
12 |
| -/* curve description: secp256k1_dettman */ |
13 |
| -/* machine_wordsize = 64 (from "64") */ |
14 |
| -/* requested operations: mul, square */ |
15 |
| -/* n = 5 (from "5") */ |
16 |
| -/* last_limb_width = 48 (from "48") */ |
17 |
| -/* last_reduction = 2 (from "2") */ |
18 |
| -/* s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") */ |
19 |
| -/* inbounds_multiplier: None (from "") */ |
20 |
| -/* */ |
21 |
| -/* Computed values: */ |
22 |
| -/* */ |
23 |
| -/* */ |
24 |
| - |
25 | 9 | #if defined(__GNUC__) || defined(__clang__)
|
26 | 10 | # define FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION __extension__
|
27 | 11 | # define FIAT_SECP256K1_DETTMAN_FIAT_INLINE __inline__
|
|
30 | 14 | # define FIAT_SECP256K1_DETTMAN_FIAT_INLINE
|
31 | 15 | #endif
|
32 | 16 |
|
33 |
| -FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef secp256k1_uint128 |
34 |
| - fiat_secp256k1_dettman_uint128; |
35 |
| - |
36 |
| -#define secp256k1_fe_sqr_inner fiat_secp256k1_dettman_square |
37 |
| -#define secp256k1_fe_mul_inner fiat_secp256k1_dettman_mul |
38 |
| - |
39 |
| -#if (-1 & 3) != 3 |
40 |
| -#error "This code only works on a two's complement system" |
41 |
| -#endif |
42 |
| - |
43 | 17 | static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_mul_u64_u64(uint64_t a, uint64_t b) {
|
44 | 18 | secp256k1_uint128 r;
|
45 | 19 | secp256k1_u128_mul(&r, a, b);
|
@@ -68,6 +42,28 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_add_u64_u128(ui
|
68 | 42 | secp256k1_u128_accum_u64(&r, a);
|
69 | 43 | return r;
|
70 | 44 | }
|
| 45 | + |
| 46 | +/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static -use-value-barrier secp256k1_dettman 64 5 48 2 '2^256 - 4294968273' mul square |
| 47 | + * curve description: secp256k1_dettman |
| 48 | + * machine_wordsize = 64 (from "64") |
| 49 | + * requested operations: mul, square |
| 50 | + * n = 5 (from "5") |
| 51 | + * last_limb_width = 48 (from "48") |
| 52 | + * last_reduction = 2 (from "2") |
| 53 | + * s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") |
| 54 | + * inbounds_multiplier: None (from "") |
| 55 | + */ |
| 56 | + |
| 57 | + |
| 58 | +FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef secp256k1_uint128 fiat_secp256k1_dettman_uint128; |
| 59 | + |
| 60 | +#define secp256k1_fe_sqr_inner fiat_secp256k1_dettman_square |
| 61 | +#define secp256k1_fe_mul_inner fiat_secp256k1_dettman_mul |
| 62 | + |
| 63 | +#if (-1 & 3) != 3 |
| 64 | +#error "This code only works on a two's complement system" |
| 65 | +#endif |
| 66 | + |
71 | 67 | /*
|
72 | 68 | * The function fiat_secp256k1_dettman_mul multiplies two field elements.
|
73 | 69 | *
|
|
0 commit comments