Last active
May 16, 2019 18:47
-
-
Save JasonGross/1c3e638e3c7b69c7298943ebc70fe2c2 to your computer and use it in GitHub Desktop.
Fiat-Crypto (https://github.com/mit-plv/fiat-crypto) generated word-by-word montgomery reduction C code for 64-bit modular arithmetic for BLS12-381 based on info at https://z.cash/blog/new-snark-curve/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* Autogenerated */ | |
/* curve description: bls12_381_q */ | |
/* requested operations: (all) */ | |
/* m = 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab (from "0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab") */ | |
/* machine_wordsize = 64 (from "64") */ | |
/* */ | |
/* NOTE: In addition to the bounds specified above each function, all */ | |
/* functions synthesized for this Montgomery arithmetic require the */ | |
/* input to be strictly less than the prime modulus (m), and also */ | |
/* require the input to be in the unique saturated representation. */ | |
/* All functions also ensure that these two properties are true of */ | |
/* return values. */ | |
#include <stdint.h> | |
typedef unsigned char fiat_bls12_381_q_uint1; | |
typedef signed char fiat_bls12_381_q_int1; | |
typedef signed __int128 fiat_bls12_381_q_int128; | |
typedef unsigned __int128 fiat_bls12_381_q_uint128; | |
/* | |
* The function fiat_bls12_381_q_addcarryx_u64 is an addition with carry. | |
* Postconditions: | |
* out1 = (arg1 + arg2 + arg3) mod 2^64 | |
* out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0x1] | |
*/ | |
static void fiat_bls12_381_q_addcarryx_u64(uint64_t* out1, fiat_bls12_381_q_uint1* out2, fiat_bls12_381_q_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_q_uint128 x1 = ((arg1 + (fiat_bls12_381_q_uint128)arg2) + arg3); | |
uint64_t x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
fiat_bls12_381_q_uint1 x3 = (fiat_bls12_381_q_uint1)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_q_subborrowx_u64 is a subtraction with borrow. | |
* Postconditions: | |
* out1 = (-arg1 + arg2 + -arg3) mod 2^64 | |
* out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0x1] | |
*/ | |
static void fiat_bls12_381_q_subborrowx_u64(uint64_t* out1, fiat_bls12_381_q_uint1* out2, fiat_bls12_381_q_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_q_int128 x1 = ((arg2 - (fiat_bls12_381_q_int128)arg1) - arg3); | |
fiat_bls12_381_q_int1 x2 = (fiat_bls12_381_q_int1)(x1 >> 64); | |
uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
*out1 = x3; | |
*out2 = (fiat_bls12_381_q_uint1)(0x0 - x2); | |
} | |
/* | |
* The function fiat_bls12_381_q_mulx_u64 is a multiplication, returning the full double-width result. | |
* Postconditions: | |
* out1 = (arg1 * arg2) mod 2^64 | |
* out2 = ⌊arg1 * arg2 / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0xffffffffffffffff] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_q_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, uint64_t arg2) { | |
fiat_bls12_381_q_uint128 x1 = ((fiat_bls12_381_q_uint128)arg1 * arg2); | |
uint64_t x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x3 = (uint64_t)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_q_cmovznz_u64 is a single-word conditional move. | |
* Postconditions: | |
* out1 = (if arg1 = 0 then arg2 else arg3) | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_q_cmovznz_u64(uint64_t* out1, fiat_bls12_381_q_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_q_uint1 x1 = (!(!arg1)); | |
uint64_t x2 = ((fiat_bls12_381_q_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); | |
uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); | |
*out1 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_q_mul multiplies two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64_t arg2[6]) { | |
uint64_t x1 = (arg1[1]); | |
uint64_t x2 = (arg1[2]); | |
uint64_t x3 = (arg1[3]); | |
uint64_t x4 = (arg1[4]); | |
uint64_t x5 = (arg1[5]); | |
uint64_t x6 = (arg1[0]); | |
uint64_t x7; | |
uint64_t x8; | |
fiat_bls12_381_q_mulx_u64(&x7, &x8, x6, (arg2[5])); | |
uint64_t x9; | |
uint64_t x10; | |
fiat_bls12_381_q_mulx_u64(&x9, &x10, x6, (arg2[4])); | |
uint64_t x11; | |
uint64_t x12; | |
fiat_bls12_381_q_mulx_u64(&x11, &x12, x6, (arg2[3])); | |
uint64_t x13; | |
uint64_t x14; | |
fiat_bls12_381_q_mulx_u64(&x13, &x14, x6, (arg2[2])); | |
uint64_t x15; | |
uint64_t x16; | |
fiat_bls12_381_q_mulx_u64(&x15, &x16, x6, (arg2[1])); | |
uint64_t x17; | |
uint64_t x18; | |
fiat_bls12_381_q_mulx_u64(&x17, &x18, x6, (arg2[0])); | |
uint64_t x19; | |
fiat_bls12_381_q_uint1 x20; | |
fiat_bls12_381_q_addcarryx_u64(&x19, &x20, 0x0, x18, x15); | |
uint64_t x21; | |
fiat_bls12_381_q_uint1 x22; | |
fiat_bls12_381_q_addcarryx_u64(&x21, &x22, x20, x16, x13); | |
uint64_t x23; | |
fiat_bls12_381_q_uint1 x24; | |
fiat_bls12_381_q_addcarryx_u64(&x23, &x24, x22, x14, x11); | |
uint64_t x25; | |
fiat_bls12_381_q_uint1 x26; | |
fiat_bls12_381_q_addcarryx_u64(&x25, &x26, x24, x12, x9); | |
uint64_t x27; | |
fiat_bls12_381_q_uint1 x28; | |
fiat_bls12_381_q_addcarryx_u64(&x27, &x28, x26, x10, x7); | |
uint64_t x29; | |
fiat_bls12_381_q_uint1 x30; | |
fiat_bls12_381_q_addcarryx_u64(&x29, &x30, x28, x8, 0x0); | |
uint64_t x31; | |
uint64_t x32; | |
fiat_bls12_381_q_mulx_u64(&x31, &x32, x17, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x33; | |
uint64_t x34; | |
fiat_bls12_381_q_mulx_u64(&x33, &x34, x31, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x35; | |
uint64_t x36; | |
fiat_bls12_381_q_mulx_u64(&x35, &x36, x31, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x37; | |
uint64_t x38; | |
fiat_bls12_381_q_mulx_u64(&x37, &x38, x31, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x39; | |
uint64_t x40; | |
fiat_bls12_381_q_mulx_u64(&x39, &x40, x31, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x41; | |
uint64_t x42; | |
fiat_bls12_381_q_mulx_u64(&x41, &x42, x31, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x43; | |
uint64_t x44; | |
fiat_bls12_381_q_mulx_u64(&x43, &x44, x31, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x45; | |
fiat_bls12_381_q_uint1 x46; | |
fiat_bls12_381_q_addcarryx_u64(&x45, &x46, 0x0, x44, x41); | |
uint64_t x47; | |
fiat_bls12_381_q_uint1 x48; | |
fiat_bls12_381_q_addcarryx_u64(&x47, &x48, x46, x42, x39); | |
uint64_t x49; | |
fiat_bls12_381_q_uint1 x50; | |
fiat_bls12_381_q_addcarryx_u64(&x49, &x50, x48, x40, x37); | |
uint64_t x51; | |
fiat_bls12_381_q_uint1 x52; | |
fiat_bls12_381_q_addcarryx_u64(&x51, &x52, x50, x38, x35); | |
uint64_t x53; | |
fiat_bls12_381_q_uint1 x54; | |
fiat_bls12_381_q_addcarryx_u64(&x53, &x54, x52, x36, x33); | |
uint64_t x55; | |
fiat_bls12_381_q_uint1 x56; | |
fiat_bls12_381_q_addcarryx_u64(&x55, &x56, x54, x34, 0x0); | |
uint64_t x57; | |
fiat_bls12_381_q_uint1 x58; | |
fiat_bls12_381_q_addcarryx_u64(&x57, &x58, 0x0, x17, x43); | |
uint64_t x59; | |
fiat_bls12_381_q_uint1 x60; | |
fiat_bls12_381_q_addcarryx_u64(&x59, &x60, x58, x19, x45); | |
uint64_t x61; | |
fiat_bls12_381_q_uint1 x62; | |
fiat_bls12_381_q_addcarryx_u64(&x61, &x62, x60, x21, x47); | |
uint64_t x63; | |
fiat_bls12_381_q_uint1 x64; | |
fiat_bls12_381_q_addcarryx_u64(&x63, &x64, x62, x23, x49); | |
uint64_t x65; | |
fiat_bls12_381_q_uint1 x66; | |
fiat_bls12_381_q_addcarryx_u64(&x65, &x66, x64, x25, x51); | |
uint64_t x67; | |
fiat_bls12_381_q_uint1 x68; | |
fiat_bls12_381_q_addcarryx_u64(&x67, &x68, x66, x27, x53); | |
uint64_t x69; | |
fiat_bls12_381_q_uint1 x70; | |
fiat_bls12_381_q_addcarryx_u64(&x69, &x70, x68, x29, x55); | |
uint64_t x71; | |
fiat_bls12_381_q_uint1 x72; | |
fiat_bls12_381_q_addcarryx_u64(&x71, &x72, x70, 0x0, 0x0); | |
uint64_t x73; | |
uint64_t x74; | |
fiat_bls12_381_q_mulx_u64(&x73, &x74, x1, (arg2[5])); | |
uint64_t x75; | |
uint64_t x76; | |
fiat_bls12_381_q_mulx_u64(&x75, &x76, x1, (arg2[4])); | |
uint64_t x77; | |
uint64_t x78; | |
fiat_bls12_381_q_mulx_u64(&x77, &x78, x1, (arg2[3])); | |
uint64_t x79; | |
uint64_t x80; | |
fiat_bls12_381_q_mulx_u64(&x79, &x80, x1, (arg2[2])); | |
uint64_t x81; | |
uint64_t x82; | |
fiat_bls12_381_q_mulx_u64(&x81, &x82, x1, (arg2[1])); | |
uint64_t x83; | |
uint64_t x84; | |
fiat_bls12_381_q_mulx_u64(&x83, &x84, x1, (arg2[0])); | |
uint64_t x85; | |
fiat_bls12_381_q_uint1 x86; | |
fiat_bls12_381_q_addcarryx_u64(&x85, &x86, 0x0, x84, x81); | |
uint64_t x87; | |
fiat_bls12_381_q_uint1 x88; | |
fiat_bls12_381_q_addcarryx_u64(&x87, &x88, x86, x82, x79); | |
uint64_t x89; | |
fiat_bls12_381_q_uint1 x90; | |
fiat_bls12_381_q_addcarryx_u64(&x89, &x90, x88, x80, x77); | |
uint64_t x91; | |
fiat_bls12_381_q_uint1 x92; | |
fiat_bls12_381_q_addcarryx_u64(&x91, &x92, x90, x78, x75); | |
uint64_t x93; | |
fiat_bls12_381_q_uint1 x94; | |
fiat_bls12_381_q_addcarryx_u64(&x93, &x94, x92, x76, x73); | |
uint64_t x95; | |
fiat_bls12_381_q_uint1 x96; | |
fiat_bls12_381_q_addcarryx_u64(&x95, &x96, x94, x74, 0x0); | |
uint64_t x97; | |
fiat_bls12_381_q_uint1 x98; | |
fiat_bls12_381_q_addcarryx_u64(&x97, &x98, 0x0, x59, x83); | |
uint64_t x99; | |
fiat_bls12_381_q_uint1 x100; | |
fiat_bls12_381_q_addcarryx_u64(&x99, &x100, x98, x61, x85); | |
uint64_t x101; | |
fiat_bls12_381_q_uint1 x102; | |
fiat_bls12_381_q_addcarryx_u64(&x101, &x102, x100, x63, x87); | |
uint64_t x103; | |
fiat_bls12_381_q_uint1 x104; | |
fiat_bls12_381_q_addcarryx_u64(&x103, &x104, x102, x65, x89); | |
uint64_t x105; | |
fiat_bls12_381_q_uint1 x106; | |
fiat_bls12_381_q_addcarryx_u64(&x105, &x106, x104, x67, x91); | |
uint64_t x107; | |
fiat_bls12_381_q_uint1 x108; | |
fiat_bls12_381_q_addcarryx_u64(&x107, &x108, x106, x69, x93); | |
uint64_t x109; | |
fiat_bls12_381_q_uint1 x110; | |
fiat_bls12_381_q_addcarryx_u64(&x109, &x110, x108, (fiat_bls12_381_q_uint1)x71, x95); | |
uint64_t x111; | |
uint64_t x112; | |
fiat_bls12_381_q_mulx_u64(&x111, &x112, x97, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x113; | |
uint64_t x114; | |
fiat_bls12_381_q_mulx_u64(&x113, &x114, x111, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x115; | |
uint64_t x116; | |
fiat_bls12_381_q_mulx_u64(&x115, &x116, x111, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x117; | |
uint64_t x118; | |
fiat_bls12_381_q_mulx_u64(&x117, &x118, x111, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x119; | |
uint64_t x120; | |
fiat_bls12_381_q_mulx_u64(&x119, &x120, x111, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x121; | |
uint64_t x122; | |
fiat_bls12_381_q_mulx_u64(&x121, &x122, x111, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x123; | |
uint64_t x124; | |
fiat_bls12_381_q_mulx_u64(&x123, &x124, x111, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x125; | |
fiat_bls12_381_q_uint1 x126; | |
fiat_bls12_381_q_addcarryx_u64(&x125, &x126, 0x0, x124, x121); | |
uint64_t x127; | |
fiat_bls12_381_q_uint1 x128; | |
fiat_bls12_381_q_addcarryx_u64(&x127, &x128, x126, x122, x119); | |
uint64_t x129; | |
fiat_bls12_381_q_uint1 x130; | |
fiat_bls12_381_q_addcarryx_u64(&x129, &x130, x128, x120, x117); | |
uint64_t x131; | |
fiat_bls12_381_q_uint1 x132; | |
fiat_bls12_381_q_addcarryx_u64(&x131, &x132, x130, x118, x115); | |
uint64_t x133; | |
fiat_bls12_381_q_uint1 x134; | |
fiat_bls12_381_q_addcarryx_u64(&x133, &x134, x132, x116, x113); | |
uint64_t x135; | |
fiat_bls12_381_q_uint1 x136; | |
fiat_bls12_381_q_addcarryx_u64(&x135, &x136, x134, x114, 0x0); | |
uint64_t x137; | |
fiat_bls12_381_q_uint1 x138; | |
fiat_bls12_381_q_addcarryx_u64(&x137, &x138, 0x0, x97, x123); | |
uint64_t x139; | |
fiat_bls12_381_q_uint1 x140; | |
fiat_bls12_381_q_addcarryx_u64(&x139, &x140, x138, x99, x125); | |
uint64_t x141; | |
fiat_bls12_381_q_uint1 x142; | |
fiat_bls12_381_q_addcarryx_u64(&x141, &x142, x140, x101, x127); | |
uint64_t x143; | |
fiat_bls12_381_q_uint1 x144; | |
fiat_bls12_381_q_addcarryx_u64(&x143, &x144, x142, x103, x129); | |
uint64_t x145; | |
fiat_bls12_381_q_uint1 x146; | |
fiat_bls12_381_q_addcarryx_u64(&x145, &x146, x144, x105, x131); | |
uint64_t x147; | |
fiat_bls12_381_q_uint1 x148; | |
fiat_bls12_381_q_addcarryx_u64(&x147, &x148, x146, x107, x133); | |
uint64_t x149; | |
fiat_bls12_381_q_uint1 x150; | |
fiat_bls12_381_q_addcarryx_u64(&x149, &x150, x148, x109, x135); | |
uint64_t x151; | |
fiat_bls12_381_q_uint1 x152; | |
fiat_bls12_381_q_addcarryx_u64(&x151, &x152, x150, x110, 0x0); | |
uint64_t x153; | |
uint64_t x154; | |
fiat_bls12_381_q_mulx_u64(&x153, &x154, x2, (arg2[5])); | |
uint64_t x155; | |
uint64_t x156; | |
fiat_bls12_381_q_mulx_u64(&x155, &x156, x2, (arg2[4])); | |
uint64_t x157; | |
uint64_t x158; | |
fiat_bls12_381_q_mulx_u64(&x157, &x158, x2, (arg2[3])); | |
uint64_t x159; | |
uint64_t x160; | |
fiat_bls12_381_q_mulx_u64(&x159, &x160, x2, (arg2[2])); | |
uint64_t x161; | |
uint64_t x162; | |
fiat_bls12_381_q_mulx_u64(&x161, &x162, x2, (arg2[1])); | |
uint64_t x163; | |
uint64_t x164; | |
fiat_bls12_381_q_mulx_u64(&x163, &x164, x2, (arg2[0])); | |
uint64_t x165; | |
fiat_bls12_381_q_uint1 x166; | |
fiat_bls12_381_q_addcarryx_u64(&x165, &x166, 0x0, x164, x161); | |
uint64_t x167; | |
fiat_bls12_381_q_uint1 x168; | |
fiat_bls12_381_q_addcarryx_u64(&x167, &x168, x166, x162, x159); | |
uint64_t x169; | |
fiat_bls12_381_q_uint1 x170; | |
fiat_bls12_381_q_addcarryx_u64(&x169, &x170, x168, x160, x157); | |
uint64_t x171; | |
fiat_bls12_381_q_uint1 x172; | |
fiat_bls12_381_q_addcarryx_u64(&x171, &x172, x170, x158, x155); | |
uint64_t x173; | |
fiat_bls12_381_q_uint1 x174; | |
fiat_bls12_381_q_addcarryx_u64(&x173, &x174, x172, x156, x153); | |
uint64_t x175; | |
fiat_bls12_381_q_uint1 x176; | |
fiat_bls12_381_q_addcarryx_u64(&x175, &x176, x174, x154, 0x0); | |
uint64_t x177; | |
fiat_bls12_381_q_uint1 x178; | |
fiat_bls12_381_q_addcarryx_u64(&x177, &x178, 0x0, x139, x163); | |
uint64_t x179; | |
fiat_bls12_381_q_uint1 x180; | |
fiat_bls12_381_q_addcarryx_u64(&x179, &x180, x178, x141, x165); | |
uint64_t x181; | |
fiat_bls12_381_q_uint1 x182; | |
fiat_bls12_381_q_addcarryx_u64(&x181, &x182, x180, x143, x167); | |
uint64_t x183; | |
fiat_bls12_381_q_uint1 x184; | |
fiat_bls12_381_q_addcarryx_u64(&x183, &x184, x182, x145, x169); | |
uint64_t x185; | |
fiat_bls12_381_q_uint1 x186; | |
fiat_bls12_381_q_addcarryx_u64(&x185, &x186, x184, x147, x171); | |
uint64_t x187; | |
fiat_bls12_381_q_uint1 x188; | |
fiat_bls12_381_q_addcarryx_u64(&x187, &x188, x186, x149, x173); | |
uint64_t x189; | |
fiat_bls12_381_q_uint1 x190; | |
fiat_bls12_381_q_addcarryx_u64(&x189, &x190, x188, x151, x175); | |
uint64_t x191; | |
uint64_t x192; | |
fiat_bls12_381_q_mulx_u64(&x191, &x192, x177, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x193; | |
uint64_t x194; | |
fiat_bls12_381_q_mulx_u64(&x193, &x194, x191, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x195; | |
uint64_t x196; | |
fiat_bls12_381_q_mulx_u64(&x195, &x196, x191, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x197; | |
uint64_t x198; | |
fiat_bls12_381_q_mulx_u64(&x197, &x198, x191, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x199; | |
uint64_t x200; | |
fiat_bls12_381_q_mulx_u64(&x199, &x200, x191, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x201; | |
uint64_t x202; | |
fiat_bls12_381_q_mulx_u64(&x201, &x202, x191, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x203; | |
uint64_t x204; | |
fiat_bls12_381_q_mulx_u64(&x203, &x204, x191, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x205; | |
fiat_bls12_381_q_uint1 x206; | |
fiat_bls12_381_q_addcarryx_u64(&x205, &x206, 0x0, x204, x201); | |
uint64_t x207; | |
fiat_bls12_381_q_uint1 x208; | |
fiat_bls12_381_q_addcarryx_u64(&x207, &x208, x206, x202, x199); | |
uint64_t x209; | |
fiat_bls12_381_q_uint1 x210; | |
fiat_bls12_381_q_addcarryx_u64(&x209, &x210, x208, x200, x197); | |
uint64_t x211; | |
fiat_bls12_381_q_uint1 x212; | |
fiat_bls12_381_q_addcarryx_u64(&x211, &x212, x210, x198, x195); | |
uint64_t x213; | |
fiat_bls12_381_q_uint1 x214; | |
fiat_bls12_381_q_addcarryx_u64(&x213, &x214, x212, x196, x193); | |
uint64_t x215; | |
fiat_bls12_381_q_uint1 x216; | |
fiat_bls12_381_q_addcarryx_u64(&x215, &x216, x214, x194, 0x0); | |
uint64_t x217; | |
fiat_bls12_381_q_uint1 x218; | |
fiat_bls12_381_q_addcarryx_u64(&x217, &x218, 0x0, x177, x203); | |
uint64_t x219; | |
fiat_bls12_381_q_uint1 x220; | |
fiat_bls12_381_q_addcarryx_u64(&x219, &x220, x218, x179, x205); | |
uint64_t x221; | |
fiat_bls12_381_q_uint1 x222; | |
fiat_bls12_381_q_addcarryx_u64(&x221, &x222, x220, x181, x207); | |
uint64_t x223; | |
fiat_bls12_381_q_uint1 x224; | |
fiat_bls12_381_q_addcarryx_u64(&x223, &x224, x222, x183, x209); | |
uint64_t x225; | |
fiat_bls12_381_q_uint1 x226; | |
fiat_bls12_381_q_addcarryx_u64(&x225, &x226, x224, x185, x211); | |
uint64_t x227; | |
fiat_bls12_381_q_uint1 x228; | |
fiat_bls12_381_q_addcarryx_u64(&x227, &x228, x226, x187, x213); | |
uint64_t x229; | |
fiat_bls12_381_q_uint1 x230; | |
fiat_bls12_381_q_addcarryx_u64(&x229, &x230, x228, x189, x215); | |
uint64_t x231; | |
fiat_bls12_381_q_uint1 x232; | |
fiat_bls12_381_q_addcarryx_u64(&x231, &x232, x230, x190, 0x0); | |
uint64_t x233; | |
uint64_t x234; | |
fiat_bls12_381_q_mulx_u64(&x233, &x234, x3, (arg2[5])); | |
uint64_t x235; | |
uint64_t x236; | |
fiat_bls12_381_q_mulx_u64(&x235, &x236, x3, (arg2[4])); | |
uint64_t x237; | |
uint64_t x238; | |
fiat_bls12_381_q_mulx_u64(&x237, &x238, x3, (arg2[3])); | |
uint64_t x239; | |
uint64_t x240; | |
fiat_bls12_381_q_mulx_u64(&x239, &x240, x3, (arg2[2])); | |
uint64_t x241; | |
uint64_t x242; | |
fiat_bls12_381_q_mulx_u64(&x241, &x242, x3, (arg2[1])); | |
uint64_t x243; | |
uint64_t x244; | |
fiat_bls12_381_q_mulx_u64(&x243, &x244, x3, (arg2[0])); | |
uint64_t x245; | |
fiat_bls12_381_q_uint1 x246; | |
fiat_bls12_381_q_addcarryx_u64(&x245, &x246, 0x0, x244, x241); | |
uint64_t x247; | |
fiat_bls12_381_q_uint1 x248; | |
fiat_bls12_381_q_addcarryx_u64(&x247, &x248, x246, x242, x239); | |
uint64_t x249; | |
fiat_bls12_381_q_uint1 x250; | |
fiat_bls12_381_q_addcarryx_u64(&x249, &x250, x248, x240, x237); | |
uint64_t x251; | |
fiat_bls12_381_q_uint1 x252; | |
fiat_bls12_381_q_addcarryx_u64(&x251, &x252, x250, x238, x235); | |
uint64_t x253; | |
fiat_bls12_381_q_uint1 x254; | |
fiat_bls12_381_q_addcarryx_u64(&x253, &x254, x252, x236, x233); | |
uint64_t x255; | |
fiat_bls12_381_q_uint1 x256; | |
fiat_bls12_381_q_addcarryx_u64(&x255, &x256, x254, x234, 0x0); | |
uint64_t x257; | |
fiat_bls12_381_q_uint1 x258; | |
fiat_bls12_381_q_addcarryx_u64(&x257, &x258, 0x0, x219, x243); | |
uint64_t x259; | |
fiat_bls12_381_q_uint1 x260; | |
fiat_bls12_381_q_addcarryx_u64(&x259, &x260, x258, x221, x245); | |
uint64_t x261; | |
fiat_bls12_381_q_uint1 x262; | |
fiat_bls12_381_q_addcarryx_u64(&x261, &x262, x260, x223, x247); | |
uint64_t x263; | |
fiat_bls12_381_q_uint1 x264; | |
fiat_bls12_381_q_addcarryx_u64(&x263, &x264, x262, x225, x249); | |
uint64_t x265; | |
fiat_bls12_381_q_uint1 x266; | |
fiat_bls12_381_q_addcarryx_u64(&x265, &x266, x264, x227, x251); | |
uint64_t x267; | |
fiat_bls12_381_q_uint1 x268; | |
fiat_bls12_381_q_addcarryx_u64(&x267, &x268, x266, x229, x253); | |
uint64_t x269; | |
fiat_bls12_381_q_uint1 x270; | |
fiat_bls12_381_q_addcarryx_u64(&x269, &x270, x268, x231, x255); | |
uint64_t x271; | |
uint64_t x272; | |
fiat_bls12_381_q_mulx_u64(&x271, &x272, x257, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x273; | |
uint64_t x274; | |
fiat_bls12_381_q_mulx_u64(&x273, &x274, x271, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x275; | |
uint64_t x276; | |
fiat_bls12_381_q_mulx_u64(&x275, &x276, x271, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x277; | |
uint64_t x278; | |
fiat_bls12_381_q_mulx_u64(&x277, &x278, x271, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x279; | |
uint64_t x280; | |
fiat_bls12_381_q_mulx_u64(&x279, &x280, x271, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x281; | |
uint64_t x282; | |
fiat_bls12_381_q_mulx_u64(&x281, &x282, x271, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x283; | |
uint64_t x284; | |
fiat_bls12_381_q_mulx_u64(&x283, &x284, x271, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x285; | |
fiat_bls12_381_q_uint1 x286; | |
fiat_bls12_381_q_addcarryx_u64(&x285, &x286, 0x0, x284, x281); | |
uint64_t x287; | |
fiat_bls12_381_q_uint1 x288; | |
fiat_bls12_381_q_addcarryx_u64(&x287, &x288, x286, x282, x279); | |
uint64_t x289; | |
fiat_bls12_381_q_uint1 x290; | |
fiat_bls12_381_q_addcarryx_u64(&x289, &x290, x288, x280, x277); | |
uint64_t x291; | |
fiat_bls12_381_q_uint1 x292; | |
fiat_bls12_381_q_addcarryx_u64(&x291, &x292, x290, x278, x275); | |
uint64_t x293; | |
fiat_bls12_381_q_uint1 x294; | |
fiat_bls12_381_q_addcarryx_u64(&x293, &x294, x292, x276, x273); | |
uint64_t x295; | |
fiat_bls12_381_q_uint1 x296; | |
fiat_bls12_381_q_addcarryx_u64(&x295, &x296, x294, x274, 0x0); | |
uint64_t x297; | |
fiat_bls12_381_q_uint1 x298; | |
fiat_bls12_381_q_addcarryx_u64(&x297, &x298, 0x0, x257, x283); | |
uint64_t x299; | |
fiat_bls12_381_q_uint1 x300; | |
fiat_bls12_381_q_addcarryx_u64(&x299, &x300, x298, x259, x285); | |
uint64_t x301; | |
fiat_bls12_381_q_uint1 x302; | |
fiat_bls12_381_q_addcarryx_u64(&x301, &x302, x300, x261, x287); | |
uint64_t x303; | |
fiat_bls12_381_q_uint1 x304; | |
fiat_bls12_381_q_addcarryx_u64(&x303, &x304, x302, x263, x289); | |
uint64_t x305; | |
fiat_bls12_381_q_uint1 x306; | |
fiat_bls12_381_q_addcarryx_u64(&x305, &x306, x304, x265, x291); | |
uint64_t x307; | |
fiat_bls12_381_q_uint1 x308; | |
fiat_bls12_381_q_addcarryx_u64(&x307, &x308, x306, x267, x293); | |
uint64_t x309; | |
fiat_bls12_381_q_uint1 x310; | |
fiat_bls12_381_q_addcarryx_u64(&x309, &x310, x308, x269, x295); | |
uint64_t x311; | |
fiat_bls12_381_q_uint1 x312; | |
fiat_bls12_381_q_addcarryx_u64(&x311, &x312, x310, x270, 0x0); | |
uint64_t x313; | |
uint64_t x314; | |
fiat_bls12_381_q_mulx_u64(&x313, &x314, x4, (arg2[5])); | |
uint64_t x315; | |
uint64_t x316; | |
fiat_bls12_381_q_mulx_u64(&x315, &x316, x4, (arg2[4])); | |
uint64_t x317; | |
uint64_t x318; | |
fiat_bls12_381_q_mulx_u64(&x317, &x318, x4, (arg2[3])); | |
uint64_t x319; | |
uint64_t x320; | |
fiat_bls12_381_q_mulx_u64(&x319, &x320, x4, (arg2[2])); | |
uint64_t x321; | |
uint64_t x322; | |
fiat_bls12_381_q_mulx_u64(&x321, &x322, x4, (arg2[1])); | |
uint64_t x323; | |
uint64_t x324; | |
fiat_bls12_381_q_mulx_u64(&x323, &x324, x4, (arg2[0])); | |
uint64_t x325; | |
fiat_bls12_381_q_uint1 x326; | |
fiat_bls12_381_q_addcarryx_u64(&x325, &x326, 0x0, x324, x321); | |
uint64_t x327; | |
fiat_bls12_381_q_uint1 x328; | |
fiat_bls12_381_q_addcarryx_u64(&x327, &x328, x326, x322, x319); | |
uint64_t x329; | |
fiat_bls12_381_q_uint1 x330; | |
fiat_bls12_381_q_addcarryx_u64(&x329, &x330, x328, x320, x317); | |
uint64_t x331; | |
fiat_bls12_381_q_uint1 x332; | |
fiat_bls12_381_q_addcarryx_u64(&x331, &x332, x330, x318, x315); | |
uint64_t x333; | |
fiat_bls12_381_q_uint1 x334; | |
fiat_bls12_381_q_addcarryx_u64(&x333, &x334, x332, x316, x313); | |
uint64_t x335; | |
fiat_bls12_381_q_uint1 x336; | |
fiat_bls12_381_q_addcarryx_u64(&x335, &x336, x334, x314, 0x0); | |
uint64_t x337; | |
fiat_bls12_381_q_uint1 x338; | |
fiat_bls12_381_q_addcarryx_u64(&x337, &x338, 0x0, x299, x323); | |
uint64_t x339; | |
fiat_bls12_381_q_uint1 x340; | |
fiat_bls12_381_q_addcarryx_u64(&x339, &x340, x338, x301, x325); | |
uint64_t x341; | |
fiat_bls12_381_q_uint1 x342; | |
fiat_bls12_381_q_addcarryx_u64(&x341, &x342, x340, x303, x327); | |
uint64_t x343; | |
fiat_bls12_381_q_uint1 x344; | |
fiat_bls12_381_q_addcarryx_u64(&x343, &x344, x342, x305, x329); | |
uint64_t x345; | |
fiat_bls12_381_q_uint1 x346; | |
fiat_bls12_381_q_addcarryx_u64(&x345, &x346, x344, x307, x331); | |
uint64_t x347; | |
fiat_bls12_381_q_uint1 x348; | |
fiat_bls12_381_q_addcarryx_u64(&x347, &x348, x346, x309, x333); | |
uint64_t x349; | |
fiat_bls12_381_q_uint1 x350; | |
fiat_bls12_381_q_addcarryx_u64(&x349, &x350, x348, x311, x335); | |
uint64_t x351; | |
uint64_t x352; | |
fiat_bls12_381_q_mulx_u64(&x351, &x352, x337, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x353; | |
uint64_t x354; | |
fiat_bls12_381_q_mulx_u64(&x353, &x354, x351, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x355; | |
uint64_t x356; | |
fiat_bls12_381_q_mulx_u64(&x355, &x356, x351, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x357; | |
uint64_t x358; | |
fiat_bls12_381_q_mulx_u64(&x357, &x358, x351, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x359; | |
uint64_t x360; | |
fiat_bls12_381_q_mulx_u64(&x359, &x360, x351, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x361; | |
uint64_t x362; | |
fiat_bls12_381_q_mulx_u64(&x361, &x362, x351, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x363; | |
uint64_t x364; | |
fiat_bls12_381_q_mulx_u64(&x363, &x364, x351, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x365; | |
fiat_bls12_381_q_uint1 x366; | |
fiat_bls12_381_q_addcarryx_u64(&x365, &x366, 0x0, x364, x361); | |
uint64_t x367; | |
fiat_bls12_381_q_uint1 x368; | |
fiat_bls12_381_q_addcarryx_u64(&x367, &x368, x366, x362, x359); | |
uint64_t x369; | |
fiat_bls12_381_q_uint1 x370; | |
fiat_bls12_381_q_addcarryx_u64(&x369, &x370, x368, x360, x357); | |
uint64_t x371; | |
fiat_bls12_381_q_uint1 x372; | |
fiat_bls12_381_q_addcarryx_u64(&x371, &x372, x370, x358, x355); | |
uint64_t x373; | |
fiat_bls12_381_q_uint1 x374; | |
fiat_bls12_381_q_addcarryx_u64(&x373, &x374, x372, x356, x353); | |
uint64_t x375; | |
fiat_bls12_381_q_uint1 x376; | |
fiat_bls12_381_q_addcarryx_u64(&x375, &x376, x374, x354, 0x0); | |
uint64_t x377; | |
fiat_bls12_381_q_uint1 x378; | |
fiat_bls12_381_q_addcarryx_u64(&x377, &x378, 0x0, x337, x363); | |
uint64_t x379; | |
fiat_bls12_381_q_uint1 x380; | |
fiat_bls12_381_q_addcarryx_u64(&x379, &x380, x378, x339, x365); | |
uint64_t x381; | |
fiat_bls12_381_q_uint1 x382; | |
fiat_bls12_381_q_addcarryx_u64(&x381, &x382, x380, x341, x367); | |
uint64_t x383; | |
fiat_bls12_381_q_uint1 x384; | |
fiat_bls12_381_q_addcarryx_u64(&x383, &x384, x382, x343, x369); | |
uint64_t x385; | |
fiat_bls12_381_q_uint1 x386; | |
fiat_bls12_381_q_addcarryx_u64(&x385, &x386, x384, x345, x371); | |
uint64_t x387; | |
fiat_bls12_381_q_uint1 x388; | |
fiat_bls12_381_q_addcarryx_u64(&x387, &x388, x386, x347, x373); | |
uint64_t x389; | |
fiat_bls12_381_q_uint1 x390; | |
fiat_bls12_381_q_addcarryx_u64(&x389, &x390, x388, x349, x375); | |
uint64_t x391; | |
fiat_bls12_381_q_uint1 x392; | |
fiat_bls12_381_q_addcarryx_u64(&x391, &x392, x390, x350, 0x0); | |
uint64_t x393; | |
uint64_t x394; | |
fiat_bls12_381_q_mulx_u64(&x393, &x394, x5, (arg2[5])); | |
uint64_t x395; | |
uint64_t x396; | |
fiat_bls12_381_q_mulx_u64(&x395, &x396, x5, (arg2[4])); | |
uint64_t x397; | |
uint64_t x398; | |
fiat_bls12_381_q_mulx_u64(&x397, &x398, x5, (arg2[3])); | |
uint64_t x399; | |
uint64_t x400; | |
fiat_bls12_381_q_mulx_u64(&x399, &x400, x5, (arg2[2])); | |
uint64_t x401; | |
uint64_t x402; | |
fiat_bls12_381_q_mulx_u64(&x401, &x402, x5, (arg2[1])); | |
uint64_t x403; | |
uint64_t x404; | |
fiat_bls12_381_q_mulx_u64(&x403, &x404, x5, (arg2[0])); | |
uint64_t x405; | |
fiat_bls12_381_q_uint1 x406; | |
fiat_bls12_381_q_addcarryx_u64(&x405, &x406, 0x0, x404, x401); | |
uint64_t x407; | |
fiat_bls12_381_q_uint1 x408; | |
fiat_bls12_381_q_addcarryx_u64(&x407, &x408, x406, x402, x399); | |
uint64_t x409; | |
fiat_bls12_381_q_uint1 x410; | |
fiat_bls12_381_q_addcarryx_u64(&x409, &x410, x408, x400, x397); | |
uint64_t x411; | |
fiat_bls12_381_q_uint1 x412; | |
fiat_bls12_381_q_addcarryx_u64(&x411, &x412, x410, x398, x395); | |
uint64_t x413; | |
fiat_bls12_381_q_uint1 x414; | |
fiat_bls12_381_q_addcarryx_u64(&x413, &x414, x412, x396, x393); | |
uint64_t x415; | |
fiat_bls12_381_q_uint1 x416; | |
fiat_bls12_381_q_addcarryx_u64(&x415, &x416, x414, x394, 0x0); | |
uint64_t x417; | |
fiat_bls12_381_q_uint1 x418; | |
fiat_bls12_381_q_addcarryx_u64(&x417, &x418, 0x0, x379, x403); | |
uint64_t x419; | |
fiat_bls12_381_q_uint1 x420; | |
fiat_bls12_381_q_addcarryx_u64(&x419, &x420, x418, x381, x405); | |
uint64_t x421; | |
fiat_bls12_381_q_uint1 x422; | |
fiat_bls12_381_q_addcarryx_u64(&x421, &x422, x420, x383, x407); | |
uint64_t x423; | |
fiat_bls12_381_q_uint1 x424; | |
fiat_bls12_381_q_addcarryx_u64(&x423, &x424, x422, x385, x409); | |
uint64_t x425; | |
fiat_bls12_381_q_uint1 x426; | |
fiat_bls12_381_q_addcarryx_u64(&x425, &x426, x424, x387, x411); | |
uint64_t x427; | |
fiat_bls12_381_q_uint1 x428; | |
fiat_bls12_381_q_addcarryx_u64(&x427, &x428, x426, x389, x413); | |
uint64_t x429; | |
fiat_bls12_381_q_uint1 x430; | |
fiat_bls12_381_q_addcarryx_u64(&x429, &x430, x428, x391, x415); | |
uint64_t x431; | |
uint64_t x432; | |
fiat_bls12_381_q_mulx_u64(&x431, &x432, x417, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x433; | |
uint64_t x434; | |
fiat_bls12_381_q_mulx_u64(&x433, &x434, x431, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x435; | |
uint64_t x436; | |
fiat_bls12_381_q_mulx_u64(&x435, &x436, x431, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x437; | |
uint64_t x438; | |
fiat_bls12_381_q_mulx_u64(&x437, &x438, x431, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x439; | |
uint64_t x440; | |
fiat_bls12_381_q_mulx_u64(&x439, &x440, x431, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x441; | |
uint64_t x442; | |
fiat_bls12_381_q_mulx_u64(&x441, &x442, x431, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x443; | |
uint64_t x444; | |
fiat_bls12_381_q_mulx_u64(&x443, &x444, x431, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x445; | |
fiat_bls12_381_q_uint1 x446; | |
fiat_bls12_381_q_addcarryx_u64(&x445, &x446, 0x0, x444, x441); | |
uint64_t x447; | |
fiat_bls12_381_q_uint1 x448; | |
fiat_bls12_381_q_addcarryx_u64(&x447, &x448, x446, x442, x439); | |
uint64_t x449; | |
fiat_bls12_381_q_uint1 x450; | |
fiat_bls12_381_q_addcarryx_u64(&x449, &x450, x448, x440, x437); | |
uint64_t x451; | |
fiat_bls12_381_q_uint1 x452; | |
fiat_bls12_381_q_addcarryx_u64(&x451, &x452, x450, x438, x435); | |
uint64_t x453; | |
fiat_bls12_381_q_uint1 x454; | |
fiat_bls12_381_q_addcarryx_u64(&x453, &x454, x452, x436, x433); | |
uint64_t x455; | |
fiat_bls12_381_q_uint1 x456; | |
fiat_bls12_381_q_addcarryx_u64(&x455, &x456, x454, x434, 0x0); | |
uint64_t x457; | |
fiat_bls12_381_q_uint1 x458; | |
fiat_bls12_381_q_addcarryx_u64(&x457, &x458, 0x0, x417, x443); | |
uint64_t x459; | |
fiat_bls12_381_q_uint1 x460; | |
fiat_bls12_381_q_addcarryx_u64(&x459, &x460, x458, x419, x445); | |
uint64_t x461; | |
fiat_bls12_381_q_uint1 x462; | |
fiat_bls12_381_q_addcarryx_u64(&x461, &x462, x460, x421, x447); | |
uint64_t x463; | |
fiat_bls12_381_q_uint1 x464; | |
fiat_bls12_381_q_addcarryx_u64(&x463, &x464, x462, x423, x449); | |
uint64_t x465; | |
fiat_bls12_381_q_uint1 x466; | |
fiat_bls12_381_q_addcarryx_u64(&x465, &x466, x464, x425, x451); | |
uint64_t x467; | |
fiat_bls12_381_q_uint1 x468; | |
fiat_bls12_381_q_addcarryx_u64(&x467, &x468, x466, x427, x453); | |
uint64_t x469; | |
fiat_bls12_381_q_uint1 x470; | |
fiat_bls12_381_q_addcarryx_u64(&x469, &x470, x468, x429, x455); | |
uint64_t x471; | |
fiat_bls12_381_q_uint1 x472; | |
fiat_bls12_381_q_addcarryx_u64(&x471, &x472, x470, x430, 0x0); | |
uint64_t x473; | |
fiat_bls12_381_q_uint1 x474; | |
fiat_bls12_381_q_subborrowx_u64(&x473, &x474, 0x0, x459, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x475; | |
fiat_bls12_381_q_uint1 x476; | |
fiat_bls12_381_q_subborrowx_u64(&x475, &x476, x474, x461, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x477; | |
fiat_bls12_381_q_uint1 x478; | |
fiat_bls12_381_q_subborrowx_u64(&x477, &x478, x476, x463, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x479; | |
fiat_bls12_381_q_uint1 x480; | |
fiat_bls12_381_q_subborrowx_u64(&x479, &x480, x478, x465, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x481; | |
fiat_bls12_381_q_uint1 x482; | |
fiat_bls12_381_q_subborrowx_u64(&x481, &x482, x480, x467, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x483; | |
fiat_bls12_381_q_uint1 x484; | |
fiat_bls12_381_q_subborrowx_u64(&x483, &x484, x482, x469, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x485; | |
fiat_bls12_381_q_uint1 x486; | |
fiat_bls12_381_q_subborrowx_u64(&x485, &x486, x484, x471, 0x0); | |
uint64_t x487; | |
fiat_bls12_381_q_cmovznz_u64(&x487, x486, x473, x459); | |
uint64_t x488; | |
fiat_bls12_381_q_cmovznz_u64(&x488, x486, x475, x461); | |
uint64_t x489; | |
fiat_bls12_381_q_cmovznz_u64(&x489, x486, x477, x463); | |
uint64_t x490; | |
fiat_bls12_381_q_cmovznz_u64(&x490, x486, x479, x465); | |
uint64_t x491; | |
fiat_bls12_381_q_cmovznz_u64(&x491, x486, x481, x467); | |
uint64_t x492; | |
fiat_bls12_381_q_cmovznz_u64(&x492, x486, x483, x469); | |
out1[0] = x487; | |
out1[1] = x488; | |
out1[2] = x489; | |
out1[3] = x490; | |
out1[4] = x491; | |
out1[5] = x492; | |
} | |
/* | |
* The function fiat_bls12_381_q_square squares a field element in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_square(uint64_t out1[6], const uint64_t arg1[6]) { | |
uint64_t x1 = (arg1[1]); | |
uint64_t x2 = (arg1[2]); | |
uint64_t x3 = (arg1[3]); | |
uint64_t x4 = (arg1[4]); | |
uint64_t x5 = (arg1[5]); | |
uint64_t x6 = (arg1[0]); | |
uint64_t x7; | |
uint64_t x8; | |
fiat_bls12_381_q_mulx_u64(&x7, &x8, x6, (arg1[5])); | |
uint64_t x9; | |
uint64_t x10; | |
fiat_bls12_381_q_mulx_u64(&x9, &x10, x6, (arg1[4])); | |
uint64_t x11; | |
uint64_t x12; | |
fiat_bls12_381_q_mulx_u64(&x11, &x12, x6, (arg1[3])); | |
uint64_t x13; | |
uint64_t x14; | |
fiat_bls12_381_q_mulx_u64(&x13, &x14, x6, (arg1[2])); | |
uint64_t x15; | |
uint64_t x16; | |
fiat_bls12_381_q_mulx_u64(&x15, &x16, x6, (arg1[1])); | |
uint64_t x17; | |
uint64_t x18; | |
fiat_bls12_381_q_mulx_u64(&x17, &x18, x6, (arg1[0])); | |
uint64_t x19; | |
fiat_bls12_381_q_uint1 x20; | |
fiat_bls12_381_q_addcarryx_u64(&x19, &x20, 0x0, x18, x15); | |
uint64_t x21; | |
fiat_bls12_381_q_uint1 x22; | |
fiat_bls12_381_q_addcarryx_u64(&x21, &x22, x20, x16, x13); | |
uint64_t x23; | |
fiat_bls12_381_q_uint1 x24; | |
fiat_bls12_381_q_addcarryx_u64(&x23, &x24, x22, x14, x11); | |
uint64_t x25; | |
fiat_bls12_381_q_uint1 x26; | |
fiat_bls12_381_q_addcarryx_u64(&x25, &x26, x24, x12, x9); | |
uint64_t x27; | |
fiat_bls12_381_q_uint1 x28; | |
fiat_bls12_381_q_addcarryx_u64(&x27, &x28, x26, x10, x7); | |
uint64_t x29; | |
fiat_bls12_381_q_uint1 x30; | |
fiat_bls12_381_q_addcarryx_u64(&x29, &x30, x28, x8, 0x0); | |
uint64_t x31; | |
uint64_t x32; | |
fiat_bls12_381_q_mulx_u64(&x31, &x32, x17, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x33; | |
uint64_t x34; | |
fiat_bls12_381_q_mulx_u64(&x33, &x34, x31, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x35; | |
uint64_t x36; | |
fiat_bls12_381_q_mulx_u64(&x35, &x36, x31, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x37; | |
uint64_t x38; | |
fiat_bls12_381_q_mulx_u64(&x37, &x38, x31, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x39; | |
uint64_t x40; | |
fiat_bls12_381_q_mulx_u64(&x39, &x40, x31, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x41; | |
uint64_t x42; | |
fiat_bls12_381_q_mulx_u64(&x41, &x42, x31, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x43; | |
uint64_t x44; | |
fiat_bls12_381_q_mulx_u64(&x43, &x44, x31, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x45; | |
fiat_bls12_381_q_uint1 x46; | |
fiat_bls12_381_q_addcarryx_u64(&x45, &x46, 0x0, x44, x41); | |
uint64_t x47; | |
fiat_bls12_381_q_uint1 x48; | |
fiat_bls12_381_q_addcarryx_u64(&x47, &x48, x46, x42, x39); | |
uint64_t x49; | |
fiat_bls12_381_q_uint1 x50; | |
fiat_bls12_381_q_addcarryx_u64(&x49, &x50, x48, x40, x37); | |
uint64_t x51; | |
fiat_bls12_381_q_uint1 x52; | |
fiat_bls12_381_q_addcarryx_u64(&x51, &x52, x50, x38, x35); | |
uint64_t x53; | |
fiat_bls12_381_q_uint1 x54; | |
fiat_bls12_381_q_addcarryx_u64(&x53, &x54, x52, x36, x33); | |
uint64_t x55; | |
fiat_bls12_381_q_uint1 x56; | |
fiat_bls12_381_q_addcarryx_u64(&x55, &x56, x54, x34, 0x0); | |
uint64_t x57; | |
fiat_bls12_381_q_uint1 x58; | |
fiat_bls12_381_q_addcarryx_u64(&x57, &x58, 0x0, x17, x43); | |
uint64_t x59; | |
fiat_bls12_381_q_uint1 x60; | |
fiat_bls12_381_q_addcarryx_u64(&x59, &x60, x58, x19, x45); | |
uint64_t x61; | |
fiat_bls12_381_q_uint1 x62; | |
fiat_bls12_381_q_addcarryx_u64(&x61, &x62, x60, x21, x47); | |
uint64_t x63; | |
fiat_bls12_381_q_uint1 x64; | |
fiat_bls12_381_q_addcarryx_u64(&x63, &x64, x62, x23, x49); | |
uint64_t x65; | |
fiat_bls12_381_q_uint1 x66; | |
fiat_bls12_381_q_addcarryx_u64(&x65, &x66, x64, x25, x51); | |
uint64_t x67; | |
fiat_bls12_381_q_uint1 x68; | |
fiat_bls12_381_q_addcarryx_u64(&x67, &x68, x66, x27, x53); | |
uint64_t x69; | |
fiat_bls12_381_q_uint1 x70; | |
fiat_bls12_381_q_addcarryx_u64(&x69, &x70, x68, x29, x55); | |
uint64_t x71; | |
fiat_bls12_381_q_uint1 x72; | |
fiat_bls12_381_q_addcarryx_u64(&x71, &x72, x70, 0x0, 0x0); | |
uint64_t x73; | |
uint64_t x74; | |
fiat_bls12_381_q_mulx_u64(&x73, &x74, x1, (arg1[5])); | |
uint64_t x75; | |
uint64_t x76; | |
fiat_bls12_381_q_mulx_u64(&x75, &x76, x1, (arg1[4])); | |
uint64_t x77; | |
uint64_t x78; | |
fiat_bls12_381_q_mulx_u64(&x77, &x78, x1, (arg1[3])); | |
uint64_t x79; | |
uint64_t x80; | |
fiat_bls12_381_q_mulx_u64(&x79, &x80, x1, (arg1[2])); | |
uint64_t x81; | |
uint64_t x82; | |
fiat_bls12_381_q_mulx_u64(&x81, &x82, x1, (arg1[1])); | |
uint64_t x83; | |
uint64_t x84; | |
fiat_bls12_381_q_mulx_u64(&x83, &x84, x1, (arg1[0])); | |
uint64_t x85; | |
fiat_bls12_381_q_uint1 x86; | |
fiat_bls12_381_q_addcarryx_u64(&x85, &x86, 0x0, x84, x81); | |
uint64_t x87; | |
fiat_bls12_381_q_uint1 x88; | |
fiat_bls12_381_q_addcarryx_u64(&x87, &x88, x86, x82, x79); | |
uint64_t x89; | |
fiat_bls12_381_q_uint1 x90; | |
fiat_bls12_381_q_addcarryx_u64(&x89, &x90, x88, x80, x77); | |
uint64_t x91; | |
fiat_bls12_381_q_uint1 x92; | |
fiat_bls12_381_q_addcarryx_u64(&x91, &x92, x90, x78, x75); | |
uint64_t x93; | |
fiat_bls12_381_q_uint1 x94; | |
fiat_bls12_381_q_addcarryx_u64(&x93, &x94, x92, x76, x73); | |
uint64_t x95; | |
fiat_bls12_381_q_uint1 x96; | |
fiat_bls12_381_q_addcarryx_u64(&x95, &x96, x94, x74, 0x0); | |
uint64_t x97; | |
fiat_bls12_381_q_uint1 x98; | |
fiat_bls12_381_q_addcarryx_u64(&x97, &x98, 0x0, x59, x83); | |
uint64_t x99; | |
fiat_bls12_381_q_uint1 x100; | |
fiat_bls12_381_q_addcarryx_u64(&x99, &x100, x98, x61, x85); | |
uint64_t x101; | |
fiat_bls12_381_q_uint1 x102; | |
fiat_bls12_381_q_addcarryx_u64(&x101, &x102, x100, x63, x87); | |
uint64_t x103; | |
fiat_bls12_381_q_uint1 x104; | |
fiat_bls12_381_q_addcarryx_u64(&x103, &x104, x102, x65, x89); | |
uint64_t x105; | |
fiat_bls12_381_q_uint1 x106; | |
fiat_bls12_381_q_addcarryx_u64(&x105, &x106, x104, x67, x91); | |
uint64_t x107; | |
fiat_bls12_381_q_uint1 x108; | |
fiat_bls12_381_q_addcarryx_u64(&x107, &x108, x106, x69, x93); | |
uint64_t x109; | |
fiat_bls12_381_q_uint1 x110; | |
fiat_bls12_381_q_addcarryx_u64(&x109, &x110, x108, (fiat_bls12_381_q_uint1)x71, x95); | |
uint64_t x111; | |
uint64_t x112; | |
fiat_bls12_381_q_mulx_u64(&x111, &x112, x97, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x113; | |
uint64_t x114; | |
fiat_bls12_381_q_mulx_u64(&x113, &x114, x111, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x115; | |
uint64_t x116; | |
fiat_bls12_381_q_mulx_u64(&x115, &x116, x111, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x117; | |
uint64_t x118; | |
fiat_bls12_381_q_mulx_u64(&x117, &x118, x111, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x119; | |
uint64_t x120; | |
fiat_bls12_381_q_mulx_u64(&x119, &x120, x111, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x121; | |
uint64_t x122; | |
fiat_bls12_381_q_mulx_u64(&x121, &x122, x111, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x123; | |
uint64_t x124; | |
fiat_bls12_381_q_mulx_u64(&x123, &x124, x111, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x125; | |
fiat_bls12_381_q_uint1 x126; | |
fiat_bls12_381_q_addcarryx_u64(&x125, &x126, 0x0, x124, x121); | |
uint64_t x127; | |
fiat_bls12_381_q_uint1 x128; | |
fiat_bls12_381_q_addcarryx_u64(&x127, &x128, x126, x122, x119); | |
uint64_t x129; | |
fiat_bls12_381_q_uint1 x130; | |
fiat_bls12_381_q_addcarryx_u64(&x129, &x130, x128, x120, x117); | |
uint64_t x131; | |
fiat_bls12_381_q_uint1 x132; | |
fiat_bls12_381_q_addcarryx_u64(&x131, &x132, x130, x118, x115); | |
uint64_t x133; | |
fiat_bls12_381_q_uint1 x134; | |
fiat_bls12_381_q_addcarryx_u64(&x133, &x134, x132, x116, x113); | |
uint64_t x135; | |
fiat_bls12_381_q_uint1 x136; | |
fiat_bls12_381_q_addcarryx_u64(&x135, &x136, x134, x114, 0x0); | |
uint64_t x137; | |
fiat_bls12_381_q_uint1 x138; | |
fiat_bls12_381_q_addcarryx_u64(&x137, &x138, 0x0, x97, x123); | |
uint64_t x139; | |
fiat_bls12_381_q_uint1 x140; | |
fiat_bls12_381_q_addcarryx_u64(&x139, &x140, x138, x99, x125); | |
uint64_t x141; | |
fiat_bls12_381_q_uint1 x142; | |
fiat_bls12_381_q_addcarryx_u64(&x141, &x142, x140, x101, x127); | |
uint64_t x143; | |
fiat_bls12_381_q_uint1 x144; | |
fiat_bls12_381_q_addcarryx_u64(&x143, &x144, x142, x103, x129); | |
uint64_t x145; | |
fiat_bls12_381_q_uint1 x146; | |
fiat_bls12_381_q_addcarryx_u64(&x145, &x146, x144, x105, x131); | |
uint64_t x147; | |
fiat_bls12_381_q_uint1 x148; | |
fiat_bls12_381_q_addcarryx_u64(&x147, &x148, x146, x107, x133); | |
uint64_t x149; | |
fiat_bls12_381_q_uint1 x150; | |
fiat_bls12_381_q_addcarryx_u64(&x149, &x150, x148, x109, x135); | |
uint64_t x151; | |
fiat_bls12_381_q_uint1 x152; | |
fiat_bls12_381_q_addcarryx_u64(&x151, &x152, x150, x110, 0x0); | |
uint64_t x153; | |
uint64_t x154; | |
fiat_bls12_381_q_mulx_u64(&x153, &x154, x2, (arg1[5])); | |
uint64_t x155; | |
uint64_t x156; | |
fiat_bls12_381_q_mulx_u64(&x155, &x156, x2, (arg1[4])); | |
uint64_t x157; | |
uint64_t x158; | |
fiat_bls12_381_q_mulx_u64(&x157, &x158, x2, (arg1[3])); | |
uint64_t x159; | |
uint64_t x160; | |
fiat_bls12_381_q_mulx_u64(&x159, &x160, x2, (arg1[2])); | |
uint64_t x161; | |
uint64_t x162; | |
fiat_bls12_381_q_mulx_u64(&x161, &x162, x2, (arg1[1])); | |
uint64_t x163; | |
uint64_t x164; | |
fiat_bls12_381_q_mulx_u64(&x163, &x164, x2, (arg1[0])); | |
uint64_t x165; | |
fiat_bls12_381_q_uint1 x166; | |
fiat_bls12_381_q_addcarryx_u64(&x165, &x166, 0x0, x164, x161); | |
uint64_t x167; | |
fiat_bls12_381_q_uint1 x168; | |
fiat_bls12_381_q_addcarryx_u64(&x167, &x168, x166, x162, x159); | |
uint64_t x169; | |
fiat_bls12_381_q_uint1 x170; | |
fiat_bls12_381_q_addcarryx_u64(&x169, &x170, x168, x160, x157); | |
uint64_t x171; | |
fiat_bls12_381_q_uint1 x172; | |
fiat_bls12_381_q_addcarryx_u64(&x171, &x172, x170, x158, x155); | |
uint64_t x173; | |
fiat_bls12_381_q_uint1 x174; | |
fiat_bls12_381_q_addcarryx_u64(&x173, &x174, x172, x156, x153); | |
uint64_t x175; | |
fiat_bls12_381_q_uint1 x176; | |
fiat_bls12_381_q_addcarryx_u64(&x175, &x176, x174, x154, 0x0); | |
uint64_t x177; | |
fiat_bls12_381_q_uint1 x178; | |
fiat_bls12_381_q_addcarryx_u64(&x177, &x178, 0x0, x139, x163); | |
uint64_t x179; | |
fiat_bls12_381_q_uint1 x180; | |
fiat_bls12_381_q_addcarryx_u64(&x179, &x180, x178, x141, x165); | |
uint64_t x181; | |
fiat_bls12_381_q_uint1 x182; | |
fiat_bls12_381_q_addcarryx_u64(&x181, &x182, x180, x143, x167); | |
uint64_t x183; | |
fiat_bls12_381_q_uint1 x184; | |
fiat_bls12_381_q_addcarryx_u64(&x183, &x184, x182, x145, x169); | |
uint64_t x185; | |
fiat_bls12_381_q_uint1 x186; | |
fiat_bls12_381_q_addcarryx_u64(&x185, &x186, x184, x147, x171); | |
uint64_t x187; | |
fiat_bls12_381_q_uint1 x188; | |
fiat_bls12_381_q_addcarryx_u64(&x187, &x188, x186, x149, x173); | |
uint64_t x189; | |
fiat_bls12_381_q_uint1 x190; | |
fiat_bls12_381_q_addcarryx_u64(&x189, &x190, x188, x151, x175); | |
uint64_t x191; | |
uint64_t x192; | |
fiat_bls12_381_q_mulx_u64(&x191, &x192, x177, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x193; | |
uint64_t x194; | |
fiat_bls12_381_q_mulx_u64(&x193, &x194, x191, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x195; | |
uint64_t x196; | |
fiat_bls12_381_q_mulx_u64(&x195, &x196, x191, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x197; | |
uint64_t x198; | |
fiat_bls12_381_q_mulx_u64(&x197, &x198, x191, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x199; | |
uint64_t x200; | |
fiat_bls12_381_q_mulx_u64(&x199, &x200, x191, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x201; | |
uint64_t x202; | |
fiat_bls12_381_q_mulx_u64(&x201, &x202, x191, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x203; | |
uint64_t x204; | |
fiat_bls12_381_q_mulx_u64(&x203, &x204, x191, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x205; | |
fiat_bls12_381_q_uint1 x206; | |
fiat_bls12_381_q_addcarryx_u64(&x205, &x206, 0x0, x204, x201); | |
uint64_t x207; | |
fiat_bls12_381_q_uint1 x208; | |
fiat_bls12_381_q_addcarryx_u64(&x207, &x208, x206, x202, x199); | |
uint64_t x209; | |
fiat_bls12_381_q_uint1 x210; | |
fiat_bls12_381_q_addcarryx_u64(&x209, &x210, x208, x200, x197); | |
uint64_t x211; | |
fiat_bls12_381_q_uint1 x212; | |
fiat_bls12_381_q_addcarryx_u64(&x211, &x212, x210, x198, x195); | |
uint64_t x213; | |
fiat_bls12_381_q_uint1 x214; | |
fiat_bls12_381_q_addcarryx_u64(&x213, &x214, x212, x196, x193); | |
uint64_t x215; | |
fiat_bls12_381_q_uint1 x216; | |
fiat_bls12_381_q_addcarryx_u64(&x215, &x216, x214, x194, 0x0); | |
uint64_t x217; | |
fiat_bls12_381_q_uint1 x218; | |
fiat_bls12_381_q_addcarryx_u64(&x217, &x218, 0x0, x177, x203); | |
uint64_t x219; | |
fiat_bls12_381_q_uint1 x220; | |
fiat_bls12_381_q_addcarryx_u64(&x219, &x220, x218, x179, x205); | |
uint64_t x221; | |
fiat_bls12_381_q_uint1 x222; | |
fiat_bls12_381_q_addcarryx_u64(&x221, &x222, x220, x181, x207); | |
uint64_t x223; | |
fiat_bls12_381_q_uint1 x224; | |
fiat_bls12_381_q_addcarryx_u64(&x223, &x224, x222, x183, x209); | |
uint64_t x225; | |
fiat_bls12_381_q_uint1 x226; | |
fiat_bls12_381_q_addcarryx_u64(&x225, &x226, x224, x185, x211); | |
uint64_t x227; | |
fiat_bls12_381_q_uint1 x228; | |
fiat_bls12_381_q_addcarryx_u64(&x227, &x228, x226, x187, x213); | |
uint64_t x229; | |
fiat_bls12_381_q_uint1 x230; | |
fiat_bls12_381_q_addcarryx_u64(&x229, &x230, x228, x189, x215); | |
uint64_t x231; | |
fiat_bls12_381_q_uint1 x232; | |
fiat_bls12_381_q_addcarryx_u64(&x231, &x232, x230, x190, 0x0); | |
uint64_t x233; | |
uint64_t x234; | |
fiat_bls12_381_q_mulx_u64(&x233, &x234, x3, (arg1[5])); | |
uint64_t x235; | |
uint64_t x236; | |
fiat_bls12_381_q_mulx_u64(&x235, &x236, x3, (arg1[4])); | |
uint64_t x237; | |
uint64_t x238; | |
fiat_bls12_381_q_mulx_u64(&x237, &x238, x3, (arg1[3])); | |
uint64_t x239; | |
uint64_t x240; | |
fiat_bls12_381_q_mulx_u64(&x239, &x240, x3, (arg1[2])); | |
uint64_t x241; | |
uint64_t x242; | |
fiat_bls12_381_q_mulx_u64(&x241, &x242, x3, (arg1[1])); | |
uint64_t x243; | |
uint64_t x244; | |
fiat_bls12_381_q_mulx_u64(&x243, &x244, x3, (arg1[0])); | |
uint64_t x245; | |
fiat_bls12_381_q_uint1 x246; | |
fiat_bls12_381_q_addcarryx_u64(&x245, &x246, 0x0, x244, x241); | |
uint64_t x247; | |
fiat_bls12_381_q_uint1 x248; | |
fiat_bls12_381_q_addcarryx_u64(&x247, &x248, x246, x242, x239); | |
uint64_t x249; | |
fiat_bls12_381_q_uint1 x250; | |
fiat_bls12_381_q_addcarryx_u64(&x249, &x250, x248, x240, x237); | |
uint64_t x251; | |
fiat_bls12_381_q_uint1 x252; | |
fiat_bls12_381_q_addcarryx_u64(&x251, &x252, x250, x238, x235); | |
uint64_t x253; | |
fiat_bls12_381_q_uint1 x254; | |
fiat_bls12_381_q_addcarryx_u64(&x253, &x254, x252, x236, x233); | |
uint64_t x255; | |
fiat_bls12_381_q_uint1 x256; | |
fiat_bls12_381_q_addcarryx_u64(&x255, &x256, x254, x234, 0x0); | |
uint64_t x257; | |
fiat_bls12_381_q_uint1 x258; | |
fiat_bls12_381_q_addcarryx_u64(&x257, &x258, 0x0, x219, x243); | |
uint64_t x259; | |
fiat_bls12_381_q_uint1 x260; | |
fiat_bls12_381_q_addcarryx_u64(&x259, &x260, x258, x221, x245); | |
uint64_t x261; | |
fiat_bls12_381_q_uint1 x262; | |
fiat_bls12_381_q_addcarryx_u64(&x261, &x262, x260, x223, x247); | |
uint64_t x263; | |
fiat_bls12_381_q_uint1 x264; | |
fiat_bls12_381_q_addcarryx_u64(&x263, &x264, x262, x225, x249); | |
uint64_t x265; | |
fiat_bls12_381_q_uint1 x266; | |
fiat_bls12_381_q_addcarryx_u64(&x265, &x266, x264, x227, x251); | |
uint64_t x267; | |
fiat_bls12_381_q_uint1 x268; | |
fiat_bls12_381_q_addcarryx_u64(&x267, &x268, x266, x229, x253); | |
uint64_t x269; | |
fiat_bls12_381_q_uint1 x270; | |
fiat_bls12_381_q_addcarryx_u64(&x269, &x270, x268, x231, x255); | |
uint64_t x271; | |
uint64_t x272; | |
fiat_bls12_381_q_mulx_u64(&x271, &x272, x257, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x273; | |
uint64_t x274; | |
fiat_bls12_381_q_mulx_u64(&x273, &x274, x271, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x275; | |
uint64_t x276; | |
fiat_bls12_381_q_mulx_u64(&x275, &x276, x271, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x277; | |
uint64_t x278; | |
fiat_bls12_381_q_mulx_u64(&x277, &x278, x271, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x279; | |
uint64_t x280; | |
fiat_bls12_381_q_mulx_u64(&x279, &x280, x271, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x281; | |
uint64_t x282; | |
fiat_bls12_381_q_mulx_u64(&x281, &x282, x271, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x283; | |
uint64_t x284; | |
fiat_bls12_381_q_mulx_u64(&x283, &x284, x271, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x285; | |
fiat_bls12_381_q_uint1 x286; | |
fiat_bls12_381_q_addcarryx_u64(&x285, &x286, 0x0, x284, x281); | |
uint64_t x287; | |
fiat_bls12_381_q_uint1 x288; | |
fiat_bls12_381_q_addcarryx_u64(&x287, &x288, x286, x282, x279); | |
uint64_t x289; | |
fiat_bls12_381_q_uint1 x290; | |
fiat_bls12_381_q_addcarryx_u64(&x289, &x290, x288, x280, x277); | |
uint64_t x291; | |
fiat_bls12_381_q_uint1 x292; | |
fiat_bls12_381_q_addcarryx_u64(&x291, &x292, x290, x278, x275); | |
uint64_t x293; | |
fiat_bls12_381_q_uint1 x294; | |
fiat_bls12_381_q_addcarryx_u64(&x293, &x294, x292, x276, x273); | |
uint64_t x295; | |
fiat_bls12_381_q_uint1 x296; | |
fiat_bls12_381_q_addcarryx_u64(&x295, &x296, x294, x274, 0x0); | |
uint64_t x297; | |
fiat_bls12_381_q_uint1 x298; | |
fiat_bls12_381_q_addcarryx_u64(&x297, &x298, 0x0, x257, x283); | |
uint64_t x299; | |
fiat_bls12_381_q_uint1 x300; | |
fiat_bls12_381_q_addcarryx_u64(&x299, &x300, x298, x259, x285); | |
uint64_t x301; | |
fiat_bls12_381_q_uint1 x302; | |
fiat_bls12_381_q_addcarryx_u64(&x301, &x302, x300, x261, x287); | |
uint64_t x303; | |
fiat_bls12_381_q_uint1 x304; | |
fiat_bls12_381_q_addcarryx_u64(&x303, &x304, x302, x263, x289); | |
uint64_t x305; | |
fiat_bls12_381_q_uint1 x306; | |
fiat_bls12_381_q_addcarryx_u64(&x305, &x306, x304, x265, x291); | |
uint64_t x307; | |
fiat_bls12_381_q_uint1 x308; | |
fiat_bls12_381_q_addcarryx_u64(&x307, &x308, x306, x267, x293); | |
uint64_t x309; | |
fiat_bls12_381_q_uint1 x310; | |
fiat_bls12_381_q_addcarryx_u64(&x309, &x310, x308, x269, x295); | |
uint64_t x311; | |
fiat_bls12_381_q_uint1 x312; | |
fiat_bls12_381_q_addcarryx_u64(&x311, &x312, x310, x270, 0x0); | |
uint64_t x313; | |
uint64_t x314; | |
fiat_bls12_381_q_mulx_u64(&x313, &x314, x4, (arg1[5])); | |
uint64_t x315; | |
uint64_t x316; | |
fiat_bls12_381_q_mulx_u64(&x315, &x316, x4, (arg1[4])); | |
uint64_t x317; | |
uint64_t x318; | |
fiat_bls12_381_q_mulx_u64(&x317, &x318, x4, (arg1[3])); | |
uint64_t x319; | |
uint64_t x320; | |
fiat_bls12_381_q_mulx_u64(&x319, &x320, x4, (arg1[2])); | |
uint64_t x321; | |
uint64_t x322; | |
fiat_bls12_381_q_mulx_u64(&x321, &x322, x4, (arg1[1])); | |
uint64_t x323; | |
uint64_t x324; | |
fiat_bls12_381_q_mulx_u64(&x323, &x324, x4, (arg1[0])); | |
uint64_t x325; | |
fiat_bls12_381_q_uint1 x326; | |
fiat_bls12_381_q_addcarryx_u64(&x325, &x326, 0x0, x324, x321); | |
uint64_t x327; | |
fiat_bls12_381_q_uint1 x328; | |
fiat_bls12_381_q_addcarryx_u64(&x327, &x328, x326, x322, x319); | |
uint64_t x329; | |
fiat_bls12_381_q_uint1 x330; | |
fiat_bls12_381_q_addcarryx_u64(&x329, &x330, x328, x320, x317); | |
uint64_t x331; | |
fiat_bls12_381_q_uint1 x332; | |
fiat_bls12_381_q_addcarryx_u64(&x331, &x332, x330, x318, x315); | |
uint64_t x333; | |
fiat_bls12_381_q_uint1 x334; | |
fiat_bls12_381_q_addcarryx_u64(&x333, &x334, x332, x316, x313); | |
uint64_t x335; | |
fiat_bls12_381_q_uint1 x336; | |
fiat_bls12_381_q_addcarryx_u64(&x335, &x336, x334, x314, 0x0); | |
uint64_t x337; | |
fiat_bls12_381_q_uint1 x338; | |
fiat_bls12_381_q_addcarryx_u64(&x337, &x338, 0x0, x299, x323); | |
uint64_t x339; | |
fiat_bls12_381_q_uint1 x340; | |
fiat_bls12_381_q_addcarryx_u64(&x339, &x340, x338, x301, x325); | |
uint64_t x341; | |
fiat_bls12_381_q_uint1 x342; | |
fiat_bls12_381_q_addcarryx_u64(&x341, &x342, x340, x303, x327); | |
uint64_t x343; | |
fiat_bls12_381_q_uint1 x344; | |
fiat_bls12_381_q_addcarryx_u64(&x343, &x344, x342, x305, x329); | |
uint64_t x345; | |
fiat_bls12_381_q_uint1 x346; | |
fiat_bls12_381_q_addcarryx_u64(&x345, &x346, x344, x307, x331); | |
uint64_t x347; | |
fiat_bls12_381_q_uint1 x348; | |
fiat_bls12_381_q_addcarryx_u64(&x347, &x348, x346, x309, x333); | |
uint64_t x349; | |
fiat_bls12_381_q_uint1 x350; | |
fiat_bls12_381_q_addcarryx_u64(&x349, &x350, x348, x311, x335); | |
uint64_t x351; | |
uint64_t x352; | |
fiat_bls12_381_q_mulx_u64(&x351, &x352, x337, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x353; | |
uint64_t x354; | |
fiat_bls12_381_q_mulx_u64(&x353, &x354, x351, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x355; | |
uint64_t x356; | |
fiat_bls12_381_q_mulx_u64(&x355, &x356, x351, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x357; | |
uint64_t x358; | |
fiat_bls12_381_q_mulx_u64(&x357, &x358, x351, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x359; | |
uint64_t x360; | |
fiat_bls12_381_q_mulx_u64(&x359, &x360, x351, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x361; | |
uint64_t x362; | |
fiat_bls12_381_q_mulx_u64(&x361, &x362, x351, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x363; | |
uint64_t x364; | |
fiat_bls12_381_q_mulx_u64(&x363, &x364, x351, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x365; | |
fiat_bls12_381_q_uint1 x366; | |
fiat_bls12_381_q_addcarryx_u64(&x365, &x366, 0x0, x364, x361); | |
uint64_t x367; | |
fiat_bls12_381_q_uint1 x368; | |
fiat_bls12_381_q_addcarryx_u64(&x367, &x368, x366, x362, x359); | |
uint64_t x369; | |
fiat_bls12_381_q_uint1 x370; | |
fiat_bls12_381_q_addcarryx_u64(&x369, &x370, x368, x360, x357); | |
uint64_t x371; | |
fiat_bls12_381_q_uint1 x372; | |
fiat_bls12_381_q_addcarryx_u64(&x371, &x372, x370, x358, x355); | |
uint64_t x373; | |
fiat_bls12_381_q_uint1 x374; | |
fiat_bls12_381_q_addcarryx_u64(&x373, &x374, x372, x356, x353); | |
uint64_t x375; | |
fiat_bls12_381_q_uint1 x376; | |
fiat_bls12_381_q_addcarryx_u64(&x375, &x376, x374, x354, 0x0); | |
uint64_t x377; | |
fiat_bls12_381_q_uint1 x378; | |
fiat_bls12_381_q_addcarryx_u64(&x377, &x378, 0x0, x337, x363); | |
uint64_t x379; | |
fiat_bls12_381_q_uint1 x380; | |
fiat_bls12_381_q_addcarryx_u64(&x379, &x380, x378, x339, x365); | |
uint64_t x381; | |
fiat_bls12_381_q_uint1 x382; | |
fiat_bls12_381_q_addcarryx_u64(&x381, &x382, x380, x341, x367); | |
uint64_t x383; | |
fiat_bls12_381_q_uint1 x384; | |
fiat_bls12_381_q_addcarryx_u64(&x383, &x384, x382, x343, x369); | |
uint64_t x385; | |
fiat_bls12_381_q_uint1 x386; | |
fiat_bls12_381_q_addcarryx_u64(&x385, &x386, x384, x345, x371); | |
uint64_t x387; | |
fiat_bls12_381_q_uint1 x388; | |
fiat_bls12_381_q_addcarryx_u64(&x387, &x388, x386, x347, x373); | |
uint64_t x389; | |
fiat_bls12_381_q_uint1 x390; | |
fiat_bls12_381_q_addcarryx_u64(&x389, &x390, x388, x349, x375); | |
uint64_t x391; | |
fiat_bls12_381_q_uint1 x392; | |
fiat_bls12_381_q_addcarryx_u64(&x391, &x392, x390, x350, 0x0); | |
uint64_t x393; | |
uint64_t x394; | |
fiat_bls12_381_q_mulx_u64(&x393, &x394, x5, (arg1[5])); | |
uint64_t x395; | |
uint64_t x396; | |
fiat_bls12_381_q_mulx_u64(&x395, &x396, x5, (arg1[4])); | |
uint64_t x397; | |
uint64_t x398; | |
fiat_bls12_381_q_mulx_u64(&x397, &x398, x5, (arg1[3])); | |
uint64_t x399; | |
uint64_t x400; | |
fiat_bls12_381_q_mulx_u64(&x399, &x400, x5, (arg1[2])); | |
uint64_t x401; | |
uint64_t x402; | |
fiat_bls12_381_q_mulx_u64(&x401, &x402, x5, (arg1[1])); | |
uint64_t x403; | |
uint64_t x404; | |
fiat_bls12_381_q_mulx_u64(&x403, &x404, x5, (arg1[0])); | |
uint64_t x405; | |
fiat_bls12_381_q_uint1 x406; | |
fiat_bls12_381_q_addcarryx_u64(&x405, &x406, 0x0, x404, x401); | |
uint64_t x407; | |
fiat_bls12_381_q_uint1 x408; | |
fiat_bls12_381_q_addcarryx_u64(&x407, &x408, x406, x402, x399); | |
uint64_t x409; | |
fiat_bls12_381_q_uint1 x410; | |
fiat_bls12_381_q_addcarryx_u64(&x409, &x410, x408, x400, x397); | |
uint64_t x411; | |
fiat_bls12_381_q_uint1 x412; | |
fiat_bls12_381_q_addcarryx_u64(&x411, &x412, x410, x398, x395); | |
uint64_t x413; | |
fiat_bls12_381_q_uint1 x414; | |
fiat_bls12_381_q_addcarryx_u64(&x413, &x414, x412, x396, x393); | |
uint64_t x415; | |
fiat_bls12_381_q_uint1 x416; | |
fiat_bls12_381_q_addcarryx_u64(&x415, &x416, x414, x394, 0x0); | |
uint64_t x417; | |
fiat_bls12_381_q_uint1 x418; | |
fiat_bls12_381_q_addcarryx_u64(&x417, &x418, 0x0, x379, x403); | |
uint64_t x419; | |
fiat_bls12_381_q_uint1 x420; | |
fiat_bls12_381_q_addcarryx_u64(&x419, &x420, x418, x381, x405); | |
uint64_t x421; | |
fiat_bls12_381_q_uint1 x422; | |
fiat_bls12_381_q_addcarryx_u64(&x421, &x422, x420, x383, x407); | |
uint64_t x423; | |
fiat_bls12_381_q_uint1 x424; | |
fiat_bls12_381_q_addcarryx_u64(&x423, &x424, x422, x385, x409); | |
uint64_t x425; | |
fiat_bls12_381_q_uint1 x426; | |
fiat_bls12_381_q_addcarryx_u64(&x425, &x426, x424, x387, x411); | |
uint64_t x427; | |
fiat_bls12_381_q_uint1 x428; | |
fiat_bls12_381_q_addcarryx_u64(&x427, &x428, x426, x389, x413); | |
uint64_t x429; | |
fiat_bls12_381_q_uint1 x430; | |
fiat_bls12_381_q_addcarryx_u64(&x429, &x430, x428, x391, x415); | |
uint64_t x431; | |
uint64_t x432; | |
fiat_bls12_381_q_mulx_u64(&x431, &x432, x417, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x433; | |
uint64_t x434; | |
fiat_bls12_381_q_mulx_u64(&x433, &x434, x431, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x435; | |
uint64_t x436; | |
fiat_bls12_381_q_mulx_u64(&x435, &x436, x431, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x437; | |
uint64_t x438; | |
fiat_bls12_381_q_mulx_u64(&x437, &x438, x431, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x439; | |
uint64_t x440; | |
fiat_bls12_381_q_mulx_u64(&x439, &x440, x431, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x441; | |
uint64_t x442; | |
fiat_bls12_381_q_mulx_u64(&x441, &x442, x431, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x443; | |
uint64_t x444; | |
fiat_bls12_381_q_mulx_u64(&x443, &x444, x431, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x445; | |
fiat_bls12_381_q_uint1 x446; | |
fiat_bls12_381_q_addcarryx_u64(&x445, &x446, 0x0, x444, x441); | |
uint64_t x447; | |
fiat_bls12_381_q_uint1 x448; | |
fiat_bls12_381_q_addcarryx_u64(&x447, &x448, x446, x442, x439); | |
uint64_t x449; | |
fiat_bls12_381_q_uint1 x450; | |
fiat_bls12_381_q_addcarryx_u64(&x449, &x450, x448, x440, x437); | |
uint64_t x451; | |
fiat_bls12_381_q_uint1 x452; | |
fiat_bls12_381_q_addcarryx_u64(&x451, &x452, x450, x438, x435); | |
uint64_t x453; | |
fiat_bls12_381_q_uint1 x454; | |
fiat_bls12_381_q_addcarryx_u64(&x453, &x454, x452, x436, x433); | |
uint64_t x455; | |
fiat_bls12_381_q_uint1 x456; | |
fiat_bls12_381_q_addcarryx_u64(&x455, &x456, x454, x434, 0x0); | |
uint64_t x457; | |
fiat_bls12_381_q_uint1 x458; | |
fiat_bls12_381_q_addcarryx_u64(&x457, &x458, 0x0, x417, x443); | |
uint64_t x459; | |
fiat_bls12_381_q_uint1 x460; | |
fiat_bls12_381_q_addcarryx_u64(&x459, &x460, x458, x419, x445); | |
uint64_t x461; | |
fiat_bls12_381_q_uint1 x462; | |
fiat_bls12_381_q_addcarryx_u64(&x461, &x462, x460, x421, x447); | |
uint64_t x463; | |
fiat_bls12_381_q_uint1 x464; | |
fiat_bls12_381_q_addcarryx_u64(&x463, &x464, x462, x423, x449); | |
uint64_t x465; | |
fiat_bls12_381_q_uint1 x466; | |
fiat_bls12_381_q_addcarryx_u64(&x465, &x466, x464, x425, x451); | |
uint64_t x467; | |
fiat_bls12_381_q_uint1 x468; | |
fiat_bls12_381_q_addcarryx_u64(&x467, &x468, x466, x427, x453); | |
uint64_t x469; | |
fiat_bls12_381_q_uint1 x470; | |
fiat_bls12_381_q_addcarryx_u64(&x469, &x470, x468, x429, x455); | |
uint64_t x471; | |
fiat_bls12_381_q_uint1 x472; | |
fiat_bls12_381_q_addcarryx_u64(&x471, &x472, x470, x430, 0x0); | |
uint64_t x473; | |
fiat_bls12_381_q_uint1 x474; | |
fiat_bls12_381_q_subborrowx_u64(&x473, &x474, 0x0, x459, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x475; | |
fiat_bls12_381_q_uint1 x476; | |
fiat_bls12_381_q_subborrowx_u64(&x475, &x476, x474, x461, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x477; | |
fiat_bls12_381_q_uint1 x478; | |
fiat_bls12_381_q_subborrowx_u64(&x477, &x478, x476, x463, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x479; | |
fiat_bls12_381_q_uint1 x480; | |
fiat_bls12_381_q_subborrowx_u64(&x479, &x480, x478, x465, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x481; | |
fiat_bls12_381_q_uint1 x482; | |
fiat_bls12_381_q_subborrowx_u64(&x481, &x482, x480, x467, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x483; | |
fiat_bls12_381_q_uint1 x484; | |
fiat_bls12_381_q_subborrowx_u64(&x483, &x484, x482, x469, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x485; | |
fiat_bls12_381_q_uint1 x486; | |
fiat_bls12_381_q_subborrowx_u64(&x485, &x486, x484, x471, 0x0); | |
uint64_t x487; | |
fiat_bls12_381_q_cmovznz_u64(&x487, x486, x473, x459); | |
uint64_t x488; | |
fiat_bls12_381_q_cmovznz_u64(&x488, x486, x475, x461); | |
uint64_t x489; | |
fiat_bls12_381_q_cmovznz_u64(&x489, x486, x477, x463); | |
uint64_t x490; | |
fiat_bls12_381_q_cmovznz_u64(&x490, x486, x479, x465); | |
uint64_t x491; | |
fiat_bls12_381_q_cmovznz_u64(&x491, x486, x481, x467); | |
uint64_t x492; | |
fiat_bls12_381_q_cmovznz_u64(&x492, x486, x483, x469); | |
out1[0] = x487; | |
out1[1] = x488; | |
out1[2] = x489; | |
out1[3] = x490; | |
out1[4] = x491; | |
out1[5] = x492; | |
} | |
/* | |
* The function fiat_bls12_381_q_add adds two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_add(uint64_t out1[6], const uint64_t arg1[6], const uint64_t arg2[6]) { | |
uint64_t x1; | |
fiat_bls12_381_q_uint1 x2; | |
fiat_bls12_381_q_addcarryx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); | |
uint64_t x3; | |
fiat_bls12_381_q_uint1 x4; | |
fiat_bls12_381_q_addcarryx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1])); | |
uint64_t x5; | |
fiat_bls12_381_q_uint1 x6; | |
fiat_bls12_381_q_addcarryx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2])); | |
uint64_t x7; | |
fiat_bls12_381_q_uint1 x8; | |
fiat_bls12_381_q_addcarryx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3])); | |
uint64_t x9; | |
fiat_bls12_381_q_uint1 x10; | |
fiat_bls12_381_q_addcarryx_u64(&x9, &x10, x8, (arg1[4]), (arg2[4])); | |
uint64_t x11; | |
fiat_bls12_381_q_uint1 x12; | |
fiat_bls12_381_q_addcarryx_u64(&x11, &x12, x10, (arg1[5]), (arg2[5])); | |
uint64_t x13; | |
fiat_bls12_381_q_uint1 x14; | |
fiat_bls12_381_q_subborrowx_u64(&x13, &x14, 0x0, x1, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x15; | |
fiat_bls12_381_q_uint1 x16; | |
fiat_bls12_381_q_subborrowx_u64(&x15, &x16, x14, x3, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x17; | |
fiat_bls12_381_q_uint1 x18; | |
fiat_bls12_381_q_subborrowx_u64(&x17, &x18, x16, x5, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x19; | |
fiat_bls12_381_q_uint1 x20; | |
fiat_bls12_381_q_subborrowx_u64(&x19, &x20, x18, x7, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x21; | |
fiat_bls12_381_q_uint1 x22; | |
fiat_bls12_381_q_subborrowx_u64(&x21, &x22, x20, x9, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x23; | |
fiat_bls12_381_q_uint1 x24; | |
fiat_bls12_381_q_subborrowx_u64(&x23, &x24, x22, x11, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x25; | |
fiat_bls12_381_q_uint1 x26; | |
fiat_bls12_381_q_subborrowx_u64(&x25, &x26, x24, x12, 0x0); | |
uint64_t x27; | |
fiat_bls12_381_q_cmovznz_u64(&x27, x26, x13, x1); | |
uint64_t x28; | |
fiat_bls12_381_q_cmovznz_u64(&x28, x26, x15, x3); | |
uint64_t x29; | |
fiat_bls12_381_q_cmovznz_u64(&x29, x26, x17, x5); | |
uint64_t x30; | |
fiat_bls12_381_q_cmovznz_u64(&x30, x26, x19, x7); | |
uint64_t x31; | |
fiat_bls12_381_q_cmovznz_u64(&x31, x26, x21, x9); | |
uint64_t x32; | |
fiat_bls12_381_q_cmovznz_u64(&x32, x26, x23, x11); | |
out1[0] = x27; | |
out1[1] = x28; | |
out1[2] = x29; | |
out1[3] = x30; | |
out1[4] = x31; | |
out1[5] = x32; | |
} | |
/* | |
* The function fiat_bls12_381_q_sub subtracts two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_sub(uint64_t out1[6], const uint64_t arg1[6], const uint64_t arg2[6]) { | |
uint64_t x1; | |
fiat_bls12_381_q_uint1 x2; | |
fiat_bls12_381_q_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); | |
uint64_t x3; | |
fiat_bls12_381_q_uint1 x4; | |
fiat_bls12_381_q_subborrowx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1])); | |
uint64_t x5; | |
fiat_bls12_381_q_uint1 x6; | |
fiat_bls12_381_q_subborrowx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2])); | |
uint64_t x7; | |
fiat_bls12_381_q_uint1 x8; | |
fiat_bls12_381_q_subborrowx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3])); | |
uint64_t x9; | |
fiat_bls12_381_q_uint1 x10; | |
fiat_bls12_381_q_subborrowx_u64(&x9, &x10, x8, (arg1[4]), (arg2[4])); | |
uint64_t x11; | |
fiat_bls12_381_q_uint1 x12; | |
fiat_bls12_381_q_subborrowx_u64(&x11, &x12, x10, (arg1[5]), (arg2[5])); | |
uint64_t x13; | |
fiat_bls12_381_q_cmovznz_u64(&x13, x12, 0x0, UINT64_C(0xffffffffffffffff)); | |
uint64_t x14; | |
fiat_bls12_381_q_uint1 x15; | |
fiat_bls12_381_q_addcarryx_u64(&x14, &x15, 0x0, x1, (x13 & UINT64_C(0xb9feffffffffaaab))); | |
uint64_t x16; | |
fiat_bls12_381_q_uint1 x17; | |
fiat_bls12_381_q_addcarryx_u64(&x16, &x17, x15, x3, (x13 & UINT64_C(0x1eabfffeb153ffff))); | |
uint64_t x18; | |
fiat_bls12_381_q_uint1 x19; | |
fiat_bls12_381_q_addcarryx_u64(&x18, &x19, x17, x5, (x13 & UINT64_C(0x6730d2a0f6b0f624))); | |
uint64_t x20; | |
fiat_bls12_381_q_uint1 x21; | |
fiat_bls12_381_q_addcarryx_u64(&x20, &x21, x19, x7, (x13 & UINT64_C(0x64774b84f38512bf))); | |
uint64_t x22; | |
fiat_bls12_381_q_uint1 x23; | |
fiat_bls12_381_q_addcarryx_u64(&x22, &x23, x21, x9, (x13 & UINT64_C(0x4b1ba7b6434bacd7))); | |
uint64_t x24; | |
fiat_bls12_381_q_uint1 x25; | |
fiat_bls12_381_q_addcarryx_u64(&x24, &x25, x23, x11, (x13 & UINT64_C(0x1a0111ea397fe69a))); | |
out1[0] = x14; | |
out1[1] = x16; | |
out1[2] = x18; | |
out1[3] = x20; | |
out1[4] = x22; | |
out1[5] = x24; | |
} | |
/* | |
* The function fiat_bls12_381_q_opp negates a field element in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_opp(uint64_t out1[6], const uint64_t arg1[6]) { | |
uint64_t x1; | |
fiat_bls12_381_q_uint1 x2; | |
fiat_bls12_381_q_subborrowx_u64(&x1, &x2, 0x0, 0x0, (arg1[0])); | |
uint64_t x3; | |
fiat_bls12_381_q_uint1 x4; | |
fiat_bls12_381_q_subborrowx_u64(&x3, &x4, x2, 0x0, (arg1[1])); | |
uint64_t x5; | |
fiat_bls12_381_q_uint1 x6; | |
fiat_bls12_381_q_subborrowx_u64(&x5, &x6, x4, 0x0, (arg1[2])); | |
uint64_t x7; | |
fiat_bls12_381_q_uint1 x8; | |
fiat_bls12_381_q_subborrowx_u64(&x7, &x8, x6, 0x0, (arg1[3])); | |
uint64_t x9; | |
fiat_bls12_381_q_uint1 x10; | |
fiat_bls12_381_q_subborrowx_u64(&x9, &x10, x8, 0x0, (arg1[4])); | |
uint64_t x11; | |
fiat_bls12_381_q_uint1 x12; | |
fiat_bls12_381_q_subborrowx_u64(&x11, &x12, x10, 0x0, (arg1[5])); | |
uint64_t x13; | |
fiat_bls12_381_q_cmovznz_u64(&x13, x12, 0x0, UINT64_C(0xffffffffffffffff)); | |
uint64_t x14; | |
fiat_bls12_381_q_uint1 x15; | |
fiat_bls12_381_q_addcarryx_u64(&x14, &x15, 0x0, x1, (x13 & UINT64_C(0xb9feffffffffaaab))); | |
uint64_t x16; | |
fiat_bls12_381_q_uint1 x17; | |
fiat_bls12_381_q_addcarryx_u64(&x16, &x17, x15, x3, (x13 & UINT64_C(0x1eabfffeb153ffff))); | |
uint64_t x18; | |
fiat_bls12_381_q_uint1 x19; | |
fiat_bls12_381_q_addcarryx_u64(&x18, &x19, x17, x5, (x13 & UINT64_C(0x6730d2a0f6b0f624))); | |
uint64_t x20; | |
fiat_bls12_381_q_uint1 x21; | |
fiat_bls12_381_q_addcarryx_u64(&x20, &x21, x19, x7, (x13 & UINT64_C(0x64774b84f38512bf))); | |
uint64_t x22; | |
fiat_bls12_381_q_uint1 x23; | |
fiat_bls12_381_q_addcarryx_u64(&x22, &x23, x21, x9, (x13 & UINT64_C(0x4b1ba7b6434bacd7))); | |
uint64_t x24; | |
fiat_bls12_381_q_uint1 x25; | |
fiat_bls12_381_q_addcarryx_u64(&x24, &x25, x23, x11, (x13 & UINT64_C(0x1a0111ea397fe69a))); | |
out1[0] = x14; | |
out1[1] = x16; | |
out1[2] = x18; | |
out1[3] = x20; | |
out1[4] = x22; | |
out1[5] = x24; | |
} | |
/* | |
* The function fiat_bls12_381_q_from_montgomery translates a field element out of the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_from_montgomery(uint64_t out1[6], const uint64_t arg1[6]) { | |
uint64_t x1 = (arg1[0]); | |
uint64_t x2; | |
uint64_t x3; | |
fiat_bls12_381_q_mulx_u64(&x2, &x3, x1, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x4; | |
uint64_t x5; | |
fiat_bls12_381_q_mulx_u64(&x4, &x5, x2, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x6; | |
uint64_t x7; | |
fiat_bls12_381_q_mulx_u64(&x6, &x7, x2, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x8; | |
uint64_t x9; | |
fiat_bls12_381_q_mulx_u64(&x8, &x9, x2, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x10; | |
uint64_t x11; | |
fiat_bls12_381_q_mulx_u64(&x10, &x11, x2, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x12; | |
uint64_t x13; | |
fiat_bls12_381_q_mulx_u64(&x12, &x13, x2, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x14; | |
uint64_t x15; | |
fiat_bls12_381_q_mulx_u64(&x14, &x15, x2, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x16; | |
fiat_bls12_381_q_uint1 x17; | |
fiat_bls12_381_q_addcarryx_u64(&x16, &x17, 0x0, x15, x12); | |
uint64_t x18; | |
fiat_bls12_381_q_uint1 x19; | |
fiat_bls12_381_q_addcarryx_u64(&x18, &x19, x17, x13, x10); | |
uint64_t x20; | |
fiat_bls12_381_q_uint1 x21; | |
fiat_bls12_381_q_addcarryx_u64(&x20, &x21, x19, x11, x8); | |
uint64_t x22; | |
fiat_bls12_381_q_uint1 x23; | |
fiat_bls12_381_q_addcarryx_u64(&x22, &x23, x21, x9, x6); | |
uint64_t x24; | |
fiat_bls12_381_q_uint1 x25; | |
fiat_bls12_381_q_addcarryx_u64(&x24, &x25, x23, x7, x4); | |
uint64_t x26; | |
fiat_bls12_381_q_uint1 x27; | |
fiat_bls12_381_q_addcarryx_u64(&x26, &x27, 0x0, x1, x14); | |
uint64_t x28; | |
fiat_bls12_381_q_uint1 x29; | |
fiat_bls12_381_q_addcarryx_u64(&x28, &x29, x27, 0x0, x16); | |
uint64_t x30; | |
fiat_bls12_381_q_uint1 x31; | |
fiat_bls12_381_q_addcarryx_u64(&x30, &x31, x29, 0x0, x18); | |
uint64_t x32; | |
fiat_bls12_381_q_uint1 x33; | |
fiat_bls12_381_q_addcarryx_u64(&x32, &x33, x31, 0x0, x20); | |
uint64_t x34; | |
fiat_bls12_381_q_uint1 x35; | |
fiat_bls12_381_q_addcarryx_u64(&x34, &x35, x33, 0x0, x22); | |
uint64_t x36; | |
fiat_bls12_381_q_uint1 x37; | |
fiat_bls12_381_q_addcarryx_u64(&x36, &x37, x35, 0x0, x24); | |
uint64_t x38; | |
fiat_bls12_381_q_uint1 x39; | |
fiat_bls12_381_q_addcarryx_u64(&x38, &x39, 0x0, x28, (arg1[1])); | |
uint64_t x40; | |
fiat_bls12_381_q_uint1 x41; | |
fiat_bls12_381_q_addcarryx_u64(&x40, &x41, x39, x30, 0x0); | |
uint64_t x42; | |
fiat_bls12_381_q_uint1 x43; | |
fiat_bls12_381_q_addcarryx_u64(&x42, &x43, x41, x32, 0x0); | |
uint64_t x44; | |
fiat_bls12_381_q_uint1 x45; | |
fiat_bls12_381_q_addcarryx_u64(&x44, &x45, x43, x34, 0x0); | |
uint64_t x46; | |
fiat_bls12_381_q_uint1 x47; | |
fiat_bls12_381_q_addcarryx_u64(&x46, &x47, x45, x36, 0x0); | |
uint64_t x48; | |
uint64_t x49; | |
fiat_bls12_381_q_mulx_u64(&x48, &x49, x38, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x50; | |
uint64_t x51; | |
fiat_bls12_381_q_mulx_u64(&x50, &x51, x48, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x52; | |
uint64_t x53; | |
fiat_bls12_381_q_mulx_u64(&x52, &x53, x48, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x54; | |
uint64_t x55; | |
fiat_bls12_381_q_mulx_u64(&x54, &x55, x48, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x56; | |
uint64_t x57; | |
fiat_bls12_381_q_mulx_u64(&x56, &x57, x48, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x58; | |
uint64_t x59; | |
fiat_bls12_381_q_mulx_u64(&x58, &x59, x48, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x60; | |
uint64_t x61; | |
fiat_bls12_381_q_mulx_u64(&x60, &x61, x48, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x62; | |
fiat_bls12_381_q_uint1 x63; | |
fiat_bls12_381_q_addcarryx_u64(&x62, &x63, 0x0, x61, x58); | |
uint64_t x64; | |
fiat_bls12_381_q_uint1 x65; | |
fiat_bls12_381_q_addcarryx_u64(&x64, &x65, x63, x59, x56); | |
uint64_t x66; | |
fiat_bls12_381_q_uint1 x67; | |
fiat_bls12_381_q_addcarryx_u64(&x66, &x67, x65, x57, x54); | |
uint64_t x68; | |
fiat_bls12_381_q_uint1 x69; | |
fiat_bls12_381_q_addcarryx_u64(&x68, &x69, x67, x55, x52); | |
uint64_t x70; | |
fiat_bls12_381_q_uint1 x71; | |
fiat_bls12_381_q_addcarryx_u64(&x70, &x71, x69, x53, x50); | |
uint64_t x72; | |
fiat_bls12_381_q_uint1 x73; | |
fiat_bls12_381_q_addcarryx_u64(&x72, &x73, 0x0, x38, x60); | |
uint64_t x74; | |
fiat_bls12_381_q_uint1 x75; | |
fiat_bls12_381_q_addcarryx_u64(&x74, &x75, x73, x40, x62); | |
uint64_t x76; | |
fiat_bls12_381_q_uint1 x77; | |
fiat_bls12_381_q_addcarryx_u64(&x76, &x77, x75, x42, x64); | |
uint64_t x78; | |
fiat_bls12_381_q_uint1 x79; | |
fiat_bls12_381_q_addcarryx_u64(&x78, &x79, x77, x44, x66); | |
uint64_t x80; | |
fiat_bls12_381_q_uint1 x81; | |
fiat_bls12_381_q_addcarryx_u64(&x80, &x81, x79, x46, x68); | |
uint64_t x82; | |
fiat_bls12_381_q_uint1 x83; | |
fiat_bls12_381_q_addcarryx_u64(&x82, &x83, x25, x5, 0x0); | |
uint64_t x84; | |
fiat_bls12_381_q_uint1 x85; | |
fiat_bls12_381_q_addcarryx_u64(&x84, &x85, x37, 0x0, x82); | |
uint64_t x86; | |
fiat_bls12_381_q_uint1 x87; | |
fiat_bls12_381_q_addcarryx_u64(&x86, &x87, x47, x84, 0x0); | |
uint64_t x88; | |
fiat_bls12_381_q_uint1 x89; | |
fiat_bls12_381_q_addcarryx_u64(&x88, &x89, x81, x86, x70); | |
uint64_t x90; | |
fiat_bls12_381_q_uint1 x91; | |
fiat_bls12_381_q_addcarryx_u64(&x90, &x91, 0x0, x74, (arg1[2])); | |
uint64_t x92; | |
fiat_bls12_381_q_uint1 x93; | |
fiat_bls12_381_q_addcarryx_u64(&x92, &x93, x91, x76, 0x0); | |
uint64_t x94; | |
fiat_bls12_381_q_uint1 x95; | |
fiat_bls12_381_q_addcarryx_u64(&x94, &x95, x93, x78, 0x0); | |
uint64_t x96; | |
fiat_bls12_381_q_uint1 x97; | |
fiat_bls12_381_q_addcarryx_u64(&x96, &x97, x95, x80, 0x0); | |
uint64_t x98; | |
fiat_bls12_381_q_uint1 x99; | |
fiat_bls12_381_q_addcarryx_u64(&x98, &x99, x97, x88, 0x0); | |
uint64_t x100; | |
uint64_t x101; | |
fiat_bls12_381_q_mulx_u64(&x100, &x101, x90, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x102; | |
uint64_t x103; | |
fiat_bls12_381_q_mulx_u64(&x102, &x103, x100, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x104; | |
uint64_t x105; | |
fiat_bls12_381_q_mulx_u64(&x104, &x105, x100, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x106; | |
uint64_t x107; | |
fiat_bls12_381_q_mulx_u64(&x106, &x107, x100, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x108; | |
uint64_t x109; | |
fiat_bls12_381_q_mulx_u64(&x108, &x109, x100, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x110; | |
uint64_t x111; | |
fiat_bls12_381_q_mulx_u64(&x110, &x111, x100, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x112; | |
uint64_t x113; | |
fiat_bls12_381_q_mulx_u64(&x112, &x113, x100, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x114; | |
fiat_bls12_381_q_uint1 x115; | |
fiat_bls12_381_q_addcarryx_u64(&x114, &x115, 0x0, x113, x110); | |
uint64_t x116; | |
fiat_bls12_381_q_uint1 x117; | |
fiat_bls12_381_q_addcarryx_u64(&x116, &x117, x115, x111, x108); | |
uint64_t x118; | |
fiat_bls12_381_q_uint1 x119; | |
fiat_bls12_381_q_addcarryx_u64(&x118, &x119, x117, x109, x106); | |
uint64_t x120; | |
fiat_bls12_381_q_uint1 x121; | |
fiat_bls12_381_q_addcarryx_u64(&x120, &x121, x119, x107, x104); | |
uint64_t x122; | |
fiat_bls12_381_q_uint1 x123; | |
fiat_bls12_381_q_addcarryx_u64(&x122, &x123, x121, x105, x102); | |
uint64_t x124; | |
fiat_bls12_381_q_uint1 x125; | |
fiat_bls12_381_q_addcarryx_u64(&x124, &x125, 0x0, x90, x112); | |
uint64_t x126; | |
fiat_bls12_381_q_uint1 x127; | |
fiat_bls12_381_q_addcarryx_u64(&x126, &x127, x125, x92, x114); | |
uint64_t x128; | |
fiat_bls12_381_q_uint1 x129; | |
fiat_bls12_381_q_addcarryx_u64(&x128, &x129, x127, x94, x116); | |
uint64_t x130; | |
fiat_bls12_381_q_uint1 x131; | |
fiat_bls12_381_q_addcarryx_u64(&x130, &x131, x129, x96, x118); | |
uint64_t x132; | |
fiat_bls12_381_q_uint1 x133; | |
fiat_bls12_381_q_addcarryx_u64(&x132, &x133, x131, x98, x120); | |
uint64_t x134; | |
fiat_bls12_381_q_uint1 x135; | |
fiat_bls12_381_q_addcarryx_u64(&x134, &x135, x71, x51, 0x0); | |
uint64_t x136; | |
fiat_bls12_381_q_uint1 x137; | |
fiat_bls12_381_q_addcarryx_u64(&x136, &x137, x89, 0x0, x134); | |
uint64_t x138; | |
fiat_bls12_381_q_uint1 x139; | |
fiat_bls12_381_q_addcarryx_u64(&x138, &x139, x99, x136, 0x0); | |
uint64_t x140; | |
fiat_bls12_381_q_uint1 x141; | |
fiat_bls12_381_q_addcarryx_u64(&x140, &x141, x133, x138, x122); | |
uint64_t x142; | |
fiat_bls12_381_q_uint1 x143; | |
fiat_bls12_381_q_addcarryx_u64(&x142, &x143, 0x0, x126, (arg1[3])); | |
uint64_t x144; | |
fiat_bls12_381_q_uint1 x145; | |
fiat_bls12_381_q_addcarryx_u64(&x144, &x145, x143, x128, 0x0); | |
uint64_t x146; | |
fiat_bls12_381_q_uint1 x147; | |
fiat_bls12_381_q_addcarryx_u64(&x146, &x147, x145, x130, 0x0); | |
uint64_t x148; | |
fiat_bls12_381_q_uint1 x149; | |
fiat_bls12_381_q_addcarryx_u64(&x148, &x149, x147, x132, 0x0); | |
uint64_t x150; | |
fiat_bls12_381_q_uint1 x151; | |
fiat_bls12_381_q_addcarryx_u64(&x150, &x151, x149, x140, 0x0); | |
uint64_t x152; | |
uint64_t x153; | |
fiat_bls12_381_q_mulx_u64(&x152, &x153, x142, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x154; | |
uint64_t x155; | |
fiat_bls12_381_q_mulx_u64(&x154, &x155, x152, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x156; | |
uint64_t x157; | |
fiat_bls12_381_q_mulx_u64(&x156, &x157, x152, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x158; | |
uint64_t x159; | |
fiat_bls12_381_q_mulx_u64(&x158, &x159, x152, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x160; | |
uint64_t x161; | |
fiat_bls12_381_q_mulx_u64(&x160, &x161, x152, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x162; | |
uint64_t x163; | |
fiat_bls12_381_q_mulx_u64(&x162, &x163, x152, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x164; | |
uint64_t x165; | |
fiat_bls12_381_q_mulx_u64(&x164, &x165, x152, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x166; | |
fiat_bls12_381_q_uint1 x167; | |
fiat_bls12_381_q_addcarryx_u64(&x166, &x167, 0x0, x165, x162); | |
uint64_t x168; | |
fiat_bls12_381_q_uint1 x169; | |
fiat_bls12_381_q_addcarryx_u64(&x168, &x169, x167, x163, x160); | |
uint64_t x170; | |
fiat_bls12_381_q_uint1 x171; | |
fiat_bls12_381_q_addcarryx_u64(&x170, &x171, x169, x161, x158); | |
uint64_t x172; | |
fiat_bls12_381_q_uint1 x173; | |
fiat_bls12_381_q_addcarryx_u64(&x172, &x173, x171, x159, x156); | |
uint64_t x174; | |
fiat_bls12_381_q_uint1 x175; | |
fiat_bls12_381_q_addcarryx_u64(&x174, &x175, x173, x157, x154); | |
uint64_t x176; | |
fiat_bls12_381_q_uint1 x177; | |
fiat_bls12_381_q_addcarryx_u64(&x176, &x177, 0x0, x142, x164); | |
uint64_t x178; | |
fiat_bls12_381_q_uint1 x179; | |
fiat_bls12_381_q_addcarryx_u64(&x178, &x179, x177, x144, x166); | |
uint64_t x180; | |
fiat_bls12_381_q_uint1 x181; | |
fiat_bls12_381_q_addcarryx_u64(&x180, &x181, x179, x146, x168); | |
uint64_t x182; | |
fiat_bls12_381_q_uint1 x183; | |
fiat_bls12_381_q_addcarryx_u64(&x182, &x183, x181, x148, x170); | |
uint64_t x184; | |
fiat_bls12_381_q_uint1 x185; | |
fiat_bls12_381_q_addcarryx_u64(&x184, &x185, x183, x150, x172); | |
uint64_t x186; | |
fiat_bls12_381_q_uint1 x187; | |
fiat_bls12_381_q_addcarryx_u64(&x186, &x187, x123, x103, 0x0); | |
uint64_t x188; | |
fiat_bls12_381_q_uint1 x189; | |
fiat_bls12_381_q_addcarryx_u64(&x188, &x189, x141, 0x0, x186); | |
uint64_t x190; | |
fiat_bls12_381_q_uint1 x191; | |
fiat_bls12_381_q_addcarryx_u64(&x190, &x191, x151, x188, 0x0); | |
uint64_t x192; | |
fiat_bls12_381_q_uint1 x193; | |
fiat_bls12_381_q_addcarryx_u64(&x192, &x193, x185, x190, x174); | |
uint64_t x194; | |
fiat_bls12_381_q_uint1 x195; | |
fiat_bls12_381_q_addcarryx_u64(&x194, &x195, 0x0, x178, (arg1[4])); | |
uint64_t x196; | |
fiat_bls12_381_q_uint1 x197; | |
fiat_bls12_381_q_addcarryx_u64(&x196, &x197, x195, x180, 0x0); | |
uint64_t x198; | |
fiat_bls12_381_q_uint1 x199; | |
fiat_bls12_381_q_addcarryx_u64(&x198, &x199, x197, x182, 0x0); | |
uint64_t x200; | |
fiat_bls12_381_q_uint1 x201; | |
fiat_bls12_381_q_addcarryx_u64(&x200, &x201, x199, x184, 0x0); | |
uint64_t x202; | |
fiat_bls12_381_q_uint1 x203; | |
fiat_bls12_381_q_addcarryx_u64(&x202, &x203, x201, x192, 0x0); | |
uint64_t x204; | |
uint64_t x205; | |
fiat_bls12_381_q_mulx_u64(&x204, &x205, x194, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x206; | |
uint64_t x207; | |
fiat_bls12_381_q_mulx_u64(&x206, &x207, x204, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x208; | |
uint64_t x209; | |
fiat_bls12_381_q_mulx_u64(&x208, &x209, x204, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x210; | |
uint64_t x211; | |
fiat_bls12_381_q_mulx_u64(&x210, &x211, x204, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x212; | |
uint64_t x213; | |
fiat_bls12_381_q_mulx_u64(&x212, &x213, x204, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x214; | |
uint64_t x215; | |
fiat_bls12_381_q_mulx_u64(&x214, &x215, x204, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x216; | |
uint64_t x217; | |
fiat_bls12_381_q_mulx_u64(&x216, &x217, x204, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x218; | |
fiat_bls12_381_q_uint1 x219; | |
fiat_bls12_381_q_addcarryx_u64(&x218, &x219, 0x0, x217, x214); | |
uint64_t x220; | |
fiat_bls12_381_q_uint1 x221; | |
fiat_bls12_381_q_addcarryx_u64(&x220, &x221, x219, x215, x212); | |
uint64_t x222; | |
fiat_bls12_381_q_uint1 x223; | |
fiat_bls12_381_q_addcarryx_u64(&x222, &x223, x221, x213, x210); | |
uint64_t x224; | |
fiat_bls12_381_q_uint1 x225; | |
fiat_bls12_381_q_addcarryx_u64(&x224, &x225, x223, x211, x208); | |
uint64_t x226; | |
fiat_bls12_381_q_uint1 x227; | |
fiat_bls12_381_q_addcarryx_u64(&x226, &x227, x225, x209, x206); | |
uint64_t x228; | |
fiat_bls12_381_q_uint1 x229; | |
fiat_bls12_381_q_addcarryx_u64(&x228, &x229, 0x0, x194, x216); | |
uint64_t x230; | |
fiat_bls12_381_q_uint1 x231; | |
fiat_bls12_381_q_addcarryx_u64(&x230, &x231, x229, x196, x218); | |
uint64_t x232; | |
fiat_bls12_381_q_uint1 x233; | |
fiat_bls12_381_q_addcarryx_u64(&x232, &x233, x231, x198, x220); | |
uint64_t x234; | |
fiat_bls12_381_q_uint1 x235; | |
fiat_bls12_381_q_addcarryx_u64(&x234, &x235, x233, x200, x222); | |
uint64_t x236; | |
fiat_bls12_381_q_uint1 x237; | |
fiat_bls12_381_q_addcarryx_u64(&x236, &x237, x235, x202, x224); | |
uint64_t x238; | |
fiat_bls12_381_q_uint1 x239; | |
fiat_bls12_381_q_addcarryx_u64(&x238, &x239, x175, x155, 0x0); | |
uint64_t x240; | |
fiat_bls12_381_q_uint1 x241; | |
fiat_bls12_381_q_addcarryx_u64(&x240, &x241, x193, 0x0, x238); | |
uint64_t x242; | |
fiat_bls12_381_q_uint1 x243; | |
fiat_bls12_381_q_addcarryx_u64(&x242, &x243, x203, x240, 0x0); | |
uint64_t x244; | |
fiat_bls12_381_q_uint1 x245; | |
fiat_bls12_381_q_addcarryx_u64(&x244, &x245, x237, x242, x226); | |
uint64_t x246; | |
fiat_bls12_381_q_uint1 x247; | |
fiat_bls12_381_q_addcarryx_u64(&x246, &x247, 0x0, x230, (arg1[5])); | |
uint64_t x248; | |
fiat_bls12_381_q_uint1 x249; | |
fiat_bls12_381_q_addcarryx_u64(&x248, &x249, x247, x232, 0x0); | |
uint64_t x250; | |
fiat_bls12_381_q_uint1 x251; | |
fiat_bls12_381_q_addcarryx_u64(&x250, &x251, x249, x234, 0x0); | |
uint64_t x252; | |
fiat_bls12_381_q_uint1 x253; | |
fiat_bls12_381_q_addcarryx_u64(&x252, &x253, x251, x236, 0x0); | |
uint64_t x254; | |
fiat_bls12_381_q_uint1 x255; | |
fiat_bls12_381_q_addcarryx_u64(&x254, &x255, x253, x244, 0x0); | |
uint64_t x256; | |
uint64_t x257; | |
fiat_bls12_381_q_mulx_u64(&x256, &x257, x246, UINT64_C(0x89f3fffcfffcfffd)); | |
uint64_t x258; | |
uint64_t x259; | |
fiat_bls12_381_q_mulx_u64(&x258, &x259, x256, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x260; | |
uint64_t x261; | |
fiat_bls12_381_q_mulx_u64(&x260, &x261, x256, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x262; | |
uint64_t x263; | |
fiat_bls12_381_q_mulx_u64(&x262, &x263, x256, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x264; | |
uint64_t x265; | |
fiat_bls12_381_q_mulx_u64(&x264, &x265, x256, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x266; | |
uint64_t x267; | |
fiat_bls12_381_q_mulx_u64(&x266, &x267, x256, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x268; | |
uint64_t x269; | |
fiat_bls12_381_q_mulx_u64(&x268, &x269, x256, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x270; | |
fiat_bls12_381_q_uint1 x271; | |
fiat_bls12_381_q_addcarryx_u64(&x270, &x271, 0x0, x269, x266); | |
uint64_t x272; | |
fiat_bls12_381_q_uint1 x273; | |
fiat_bls12_381_q_addcarryx_u64(&x272, &x273, x271, x267, x264); | |
uint64_t x274; | |
fiat_bls12_381_q_uint1 x275; | |
fiat_bls12_381_q_addcarryx_u64(&x274, &x275, x273, x265, x262); | |
uint64_t x276; | |
fiat_bls12_381_q_uint1 x277; | |
fiat_bls12_381_q_addcarryx_u64(&x276, &x277, x275, x263, x260); | |
uint64_t x278; | |
fiat_bls12_381_q_uint1 x279; | |
fiat_bls12_381_q_addcarryx_u64(&x278, &x279, x277, x261, x258); | |
uint64_t x280; | |
fiat_bls12_381_q_uint1 x281; | |
fiat_bls12_381_q_addcarryx_u64(&x280, &x281, 0x0, x246, x268); | |
uint64_t x282; | |
fiat_bls12_381_q_uint1 x283; | |
fiat_bls12_381_q_addcarryx_u64(&x282, &x283, x281, x248, x270); | |
uint64_t x284; | |
fiat_bls12_381_q_uint1 x285; | |
fiat_bls12_381_q_addcarryx_u64(&x284, &x285, x283, x250, x272); | |
uint64_t x286; | |
fiat_bls12_381_q_uint1 x287; | |
fiat_bls12_381_q_addcarryx_u64(&x286, &x287, x285, x252, x274); | |
uint64_t x288; | |
fiat_bls12_381_q_uint1 x289; | |
fiat_bls12_381_q_addcarryx_u64(&x288, &x289, x287, x254, x276); | |
uint64_t x290; | |
fiat_bls12_381_q_uint1 x291; | |
fiat_bls12_381_q_addcarryx_u64(&x290, &x291, x227, x207, 0x0); | |
uint64_t x292; | |
fiat_bls12_381_q_uint1 x293; | |
fiat_bls12_381_q_addcarryx_u64(&x292, &x293, x245, 0x0, x290); | |
uint64_t x294; | |
fiat_bls12_381_q_uint1 x295; | |
fiat_bls12_381_q_addcarryx_u64(&x294, &x295, x255, x292, 0x0); | |
uint64_t x296; | |
fiat_bls12_381_q_uint1 x297; | |
fiat_bls12_381_q_addcarryx_u64(&x296, &x297, x289, x294, x278); | |
uint64_t x298; | |
fiat_bls12_381_q_uint1 x299; | |
fiat_bls12_381_q_addcarryx_u64(&x298, &x299, x279, x259, 0x0); | |
uint64_t x300; | |
fiat_bls12_381_q_uint1 x301; | |
fiat_bls12_381_q_addcarryx_u64(&x300, &x301, x297, 0x0, x298); | |
uint64_t x302; | |
fiat_bls12_381_q_uint1 x303; | |
fiat_bls12_381_q_subborrowx_u64(&x302, &x303, 0x0, x282, UINT64_C(0xb9feffffffffaaab)); | |
uint64_t x304; | |
fiat_bls12_381_q_uint1 x305; | |
fiat_bls12_381_q_subborrowx_u64(&x304, &x305, x303, x284, UINT64_C(0x1eabfffeb153ffff)); | |
uint64_t x306; | |
fiat_bls12_381_q_uint1 x307; | |
fiat_bls12_381_q_subborrowx_u64(&x306, &x307, x305, x286, UINT64_C(0x6730d2a0f6b0f624)); | |
uint64_t x308; | |
fiat_bls12_381_q_uint1 x309; | |
fiat_bls12_381_q_subborrowx_u64(&x308, &x309, x307, x288, UINT64_C(0x64774b84f38512bf)); | |
uint64_t x310; | |
fiat_bls12_381_q_uint1 x311; | |
fiat_bls12_381_q_subborrowx_u64(&x310, &x311, x309, x296, UINT64_C(0x4b1ba7b6434bacd7)); | |
uint64_t x312; | |
fiat_bls12_381_q_uint1 x313; | |
fiat_bls12_381_q_subborrowx_u64(&x312, &x313, x311, x300, UINT64_C(0x1a0111ea397fe69a)); | |
uint64_t x314; | |
fiat_bls12_381_q_uint1 x315; | |
fiat_bls12_381_q_subborrowx_u64(&x314, &x315, x313, 0x0, 0x0); | |
uint64_t x316; | |
fiat_bls12_381_q_cmovznz_u64(&x316, x315, x302, x282); | |
uint64_t x317; | |
fiat_bls12_381_q_cmovznz_u64(&x317, x315, x304, x284); | |
uint64_t x318; | |
fiat_bls12_381_q_cmovznz_u64(&x318, x315, x306, x286); | |
uint64_t x319; | |
fiat_bls12_381_q_cmovznz_u64(&x319, x315, x308, x288); | |
uint64_t x320; | |
fiat_bls12_381_q_cmovznz_u64(&x320, x315, x310, x296); | |
uint64_t x321; | |
fiat_bls12_381_q_cmovznz_u64(&x321, x315, x312, x300); | |
out1[0] = x316; | |
out1[1] = x317; | |
out1[2] = x318; | |
out1[3] = x319; | |
out1[4] = x320; | |
out1[5] = x321; | |
} | |
/* | |
* The function fiat_bls12_381_q_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_q_nonzero(uint64_t* out1, const uint64_t arg1[6]) { | |
uint64_t x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | (uint64_t)0x0)))))); | |
*out1 = x1; | |
} | |
/* | |
* The function fiat_bls12_381_q_selectznz is a multi-limb conditional select. | |
* Postconditions: | |
* eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_selectznz(uint64_t out1[6], fiat_bls12_381_q_uint1 arg1, const uint64_t arg2[6], const uint64_t arg3[6]) { | |
uint64_t x1; | |
fiat_bls12_381_q_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0])); | |
uint64_t x2; | |
fiat_bls12_381_q_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1])); | |
uint64_t x3; | |
fiat_bls12_381_q_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2])); | |
uint64_t x4; | |
fiat_bls12_381_q_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3])); | |
uint64_t x5; | |
fiat_bls12_381_q_cmovznz_u64(&x5, arg1, (arg2[4]), (arg3[4])); | |
uint64_t x6; | |
fiat_bls12_381_q_cmovznz_u64(&x6, arg1, (arg2[5]), (arg3[5])); | |
out1[0] = x1; | |
out1[1] = x2; | |
out1[2] = x3; | |
out1[3] = x4; | |
out1[4] = x5; | |
out1[5] = x6; | |
} | |
/* | |
* The function fiat_bls12_381_q_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47] | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1fffffffffffffff]] | |
* Output Bounds: | |
* 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 ~> 0x1f]] | |
*/ | |
static void fiat_bls12_381_q_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { | |
uint64_t x1 = (arg1[5]); | |
uint64_t x2 = (arg1[4]); | |
uint64_t x3 = (arg1[3]); | |
uint64_t x4 = (arg1[2]); | |
uint64_t x5 = (arg1[1]); | |
uint64_t x6 = (arg1[0]); | |
uint64_t x7 = (x6 >> 8); | |
uint8_t x8 = (uint8_t)(x6 & UINT8_C(0xff)); | |
uint64_t x9 = (x7 >> 8); | |
uint8_t x10 = (uint8_t)(x7 & UINT8_C(0xff)); | |
uint64_t x11 = (x9 >> 8); | |
uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); | |
uint64_t x13 = (x11 >> 8); | |
uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); | |
uint64_t x15 = (x13 >> 8); | |
uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); | |
uint64_t x17 = (x15 >> 8); | |
uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); | |
uint8_t x19 = (uint8_t)(x17 >> 8); | |
uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); | |
uint8_t x21 = (uint8_t)(x19 & UINT8_C(0xff)); | |
uint64_t x22 = (x5 >> 8); | |
uint8_t x23 = (uint8_t)(x5 & UINT8_C(0xff)); | |
uint64_t x24 = (x22 >> 8); | |
uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); | |
uint64_t x26 = (x24 >> 8); | |
uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); | |
uint64_t x28 = (x26 >> 8); | |
uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); | |
uint64_t x30 = (x28 >> 8); | |
uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); | |
uint64_t x32 = (x30 >> 8); | |
uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); | |
uint8_t x34 = (uint8_t)(x32 >> 8); | |
uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); | |
uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); | |
uint64_t x37 = (x4 >> 8); | |
uint8_t x38 = (uint8_t)(x4 & UINT8_C(0xff)); | |
uint64_t x39 = (x37 >> 8); | |
uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); | |
uint64_t x41 = (x39 >> 8); | |
uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); | |
uint64_t x43 = (x41 >> 8); | |
uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); | |
uint64_t x45 = (x43 >> 8); | |
uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); | |
uint64_t x47 = (x45 >> 8); | |
uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); | |
uint8_t x49 = (uint8_t)(x47 >> 8); | |
uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); | |
uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); | |
uint64_t x52 = (x3 >> 8); | |
uint8_t x53 = (uint8_t)(x3 & UINT8_C(0xff)); | |
uint64_t x54 = (x52 >> 8); | |
uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); | |
uint64_t x56 = (x54 >> 8); | |
uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); | |
uint64_t x58 = (x56 >> 8); | |
uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); | |
uint64_t x60 = (x58 >> 8); | |
uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); | |
uint64_t x62 = (x60 >> 8); | |
uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); | |
uint8_t x64 = (uint8_t)(x62 >> 8); | |
uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); | |
uint8_t x66 = (uint8_t)(x64 & UINT8_C(0xff)); | |
uint64_t x67 = (x2 >> 8); | |
uint8_t x68 = (uint8_t)(x2 & UINT8_C(0xff)); | |
uint64_t x69 = (x67 >> 8); | |
uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); | |
uint64_t x71 = (x69 >> 8); | |
uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); | |
uint64_t x73 = (x71 >> 8); | |
uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); | |
uint64_t x75 = (x73 >> 8); | |
uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff)); | |
uint64_t x77 = (x75 >> 8); | |
uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff)); | |
uint8_t x79 = (uint8_t)(x77 >> 8); | |
uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff)); | |
uint8_t x81 = (uint8_t)(x79 & UINT8_C(0xff)); | |
uint64_t x82 = (x1 >> 8); | |
uint8_t x83 = (uint8_t)(x1 & UINT8_C(0xff)); | |
uint64_t x84 = (x82 >> 8); | |
uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff)); | |
uint64_t x86 = (x84 >> 8); | |
uint8_t x87 = (uint8_t)(x84 & UINT8_C(0xff)); | |
uint64_t x88 = (x86 >> 8); | |
uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff)); | |
uint64_t x90 = (x88 >> 8); | |
uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); | |
uint64_t x92 = (x90 >> 8); | |
uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff)); | |
uint8_t x94 = (uint8_t)(x92 >> 8); | |
uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); | |
out1[0] = x8; | |
out1[1] = x10; | |
out1[2] = x12; | |
out1[3] = x14; | |
out1[4] = x16; | |
out1[5] = x18; | |
out1[6] = x20; | |
out1[7] = x21; | |
out1[8] = x23; | |
out1[9] = x25; | |
out1[10] = x27; | |
out1[11] = x29; | |
out1[12] = x31; | |
out1[13] = x33; | |
out1[14] = x35; | |
out1[15] = x36; | |
out1[16] = x38; | |
out1[17] = x40; | |
out1[18] = x42; | |
out1[19] = x44; | |
out1[20] = x46; | |
out1[21] = x48; | |
out1[22] = x50; | |
out1[23] = x51; | |
out1[24] = x53; | |
out1[25] = x55; | |
out1[26] = x57; | |
out1[27] = x59; | |
out1[28] = x61; | |
out1[29] = x63; | |
out1[30] = x65; | |
out1[31] = x66; | |
out1[32] = x68; | |
out1[33] = x70; | |
out1[34] = x72; | |
out1[35] = x74; | |
out1[36] = x76; | |
out1[37] = x78; | |
out1[38] = x80; | |
out1[39] = x81; | |
out1[40] = x83; | |
out1[41] = x85; | |
out1[42] = x87; | |
out1[43] = x89; | |
out1[44] = x91; | |
out1[45] = x93; | |
out1[46] = x95; | |
out1[47] = x94; | |
} | |
/* | |
* The function fiat_bls12_381_q_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. | |
* Preconditions: | |
* 0 ≤ bytes_eval arg1 < m | |
* Postconditions: | |
* eval out1 mod m = bytes_eval arg1 mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* 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 ~> 0x1f]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1fffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_q_from_bytes(uint64_t out1[6], const uint8_t arg1[48]) { | |
uint64_t x1 = ((uint64_t)(arg1[47]) << 56); | |
uint64_t x2 = ((uint64_t)(arg1[46]) << 48); | |
uint64_t x3 = ((uint64_t)(arg1[45]) << 40); | |
uint64_t x4 = ((uint64_t)(arg1[44]) << 32); | |
uint64_t x5 = ((uint64_t)(arg1[43]) << 24); | |
uint64_t x6 = ((uint64_t)(arg1[42]) << 16); | |
uint64_t x7 = ((uint64_t)(arg1[41]) << 8); | |
uint8_t x8 = (arg1[40]); | |
uint64_t x9 = ((uint64_t)(arg1[39]) << 56); | |
uint64_t x10 = ((uint64_t)(arg1[38]) << 48); | |
uint64_t x11 = ((uint64_t)(arg1[37]) << 40); | |
uint64_t x12 = ((uint64_t)(arg1[36]) << 32); | |
uint64_t x13 = ((uint64_t)(arg1[35]) << 24); | |
uint64_t x14 = ((uint64_t)(arg1[34]) << 16); | |
uint64_t x15 = ((uint64_t)(arg1[33]) << 8); | |
uint8_t x16 = (arg1[32]); | |
uint64_t x17 = ((uint64_t)(arg1[31]) << 56); | |
uint64_t x18 = ((uint64_t)(arg1[30]) << 48); | |
uint64_t x19 = ((uint64_t)(arg1[29]) << 40); | |
uint64_t x20 = ((uint64_t)(arg1[28]) << 32); | |
uint64_t x21 = ((uint64_t)(arg1[27]) << 24); | |
uint64_t x22 = ((uint64_t)(arg1[26]) << 16); | |
uint64_t x23 = ((uint64_t)(arg1[25]) << 8); | |
uint8_t x24 = (arg1[24]); | |
uint64_t x25 = ((uint64_t)(arg1[23]) << 56); | |
uint64_t x26 = ((uint64_t)(arg1[22]) << 48); | |
uint64_t x27 = ((uint64_t)(arg1[21]) << 40); | |
uint64_t x28 = ((uint64_t)(arg1[20]) << 32); | |
uint64_t x29 = ((uint64_t)(arg1[19]) << 24); | |
uint64_t x30 = ((uint64_t)(arg1[18]) << 16); | |
uint64_t x31 = ((uint64_t)(arg1[17]) << 8); | |
uint8_t x32 = (arg1[16]); | |
uint64_t x33 = ((uint64_t)(arg1[15]) << 56); | |
uint64_t x34 = ((uint64_t)(arg1[14]) << 48); | |
uint64_t x35 = ((uint64_t)(arg1[13]) << 40); | |
uint64_t x36 = ((uint64_t)(arg1[12]) << 32); | |
uint64_t x37 = ((uint64_t)(arg1[11]) << 24); | |
uint64_t x38 = ((uint64_t)(arg1[10]) << 16); | |
uint64_t x39 = ((uint64_t)(arg1[9]) << 8); | |
uint8_t x40 = (arg1[8]); | |
uint64_t x41 = ((uint64_t)(arg1[7]) << 56); | |
uint64_t x42 = ((uint64_t)(arg1[6]) << 48); | |
uint64_t x43 = ((uint64_t)(arg1[5]) << 40); | |
uint64_t x44 = ((uint64_t)(arg1[4]) << 32); | |
uint64_t x45 = ((uint64_t)(arg1[3]) << 24); | |
uint64_t x46 = ((uint64_t)(arg1[2]) << 16); | |
uint64_t x47 = ((uint64_t)(arg1[1]) << 8); | |
uint8_t x48 = (arg1[0]); | |
uint64_t x49 = (x48 + (x47 + (x46 + (x45 + (x44 + (x43 + (x42 + x41))))))); | |
uint64_t x50 = (x49 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x51 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1))))))); | |
uint64_t x52 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9))))))); | |
uint64_t x53 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); | |
uint64_t x54 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25))))))); | |
uint64_t x55 = (x40 + (x39 + (x38 + (x37 + (x36 + (x35 + (x34 + x33))))))); | |
uint64_t x56 = (x55 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x57 = (x54 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x58 = (x53 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x59 = (x52 & UINT64_C(0xffffffffffffffff)); | |
out1[0] = x50; | |
out1[1] = x56; | |
out1[2] = x57; | |
out1[3] = x58; | |
out1[4] = x59; | |
out1[5] = x51; | |
} | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* Autogenerated */ | |
/* curve description: bls12_381_r */ | |
/* requested operations: (all) */ | |
/* m = 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001 (from "0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001") */ | |
/* machine_wordsize = 64 (from "64") */ | |
/* */ | |
/* NOTE: In addition to the bounds specified above each function, all */ | |
/* functions synthesized for this Montgomery arithmetic require the */ | |
/* input to be strictly less than the prime modulus (m), and also */ | |
/* require the input to be in the unique saturated representation. */ | |
/* All functions also ensure that these two properties are true of */ | |
/* return values. */ | |
#include <stdint.h> | |
typedef unsigned char fiat_bls12_381_r_uint1; | |
typedef signed char fiat_bls12_381_r_int1; | |
typedef signed __int128 fiat_bls12_381_r_int128; | |
typedef unsigned __int128 fiat_bls12_381_r_uint128; | |
/* | |
* The function fiat_bls12_381_r_addcarryx_u64 is an addition with carry. | |
* Postconditions: | |
* out1 = (arg1 + arg2 + arg3) mod 2^64 | |
* out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0x1] | |
*/ | |
static void fiat_bls12_381_r_addcarryx_u64(uint64_t* out1, fiat_bls12_381_r_uint1* out2, fiat_bls12_381_r_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_r_uint128 x1 = ((arg1 + (fiat_bls12_381_r_uint128)arg2) + arg3); | |
uint64_t x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
fiat_bls12_381_r_uint1 x3 = (fiat_bls12_381_r_uint1)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_r_subborrowx_u64 is a subtraction with borrow. | |
* Postconditions: | |
* out1 = (-arg1 + arg2 + -arg3) mod 2^64 | |
* out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0x1] | |
*/ | |
static void fiat_bls12_381_r_subborrowx_u64(uint64_t* out1, fiat_bls12_381_r_uint1* out2, fiat_bls12_381_r_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_r_int128 x1 = ((arg2 - (fiat_bls12_381_r_int128)arg1) - arg3); | |
fiat_bls12_381_r_int1 x2 = (fiat_bls12_381_r_int1)(x1 >> 64); | |
uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
*out1 = x3; | |
*out2 = (fiat_bls12_381_r_uint1)(0x0 - x2); | |
} | |
/* | |
* The function fiat_bls12_381_r_mulx_u64 is a multiplication, returning the full double-width result. | |
* Postconditions: | |
* out1 = (arg1 * arg2) mod 2^64 | |
* out2 = ⌊arg1 * arg2 / 2^64⌋ | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0xffffffffffffffff] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
* out2: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_r_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, uint64_t arg2) { | |
fiat_bls12_381_r_uint128 x1 = ((fiat_bls12_381_r_uint128)arg1 * arg2); | |
uint64_t x2 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x3 = (uint64_t)(x1 >> 64); | |
*out1 = x2; | |
*out2 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_r_cmovznz_u64 is a single-word conditional move. | |
* Postconditions: | |
* out1 = (if arg1 = 0 then arg2 else arg3) | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [0x0 ~> 0xffffffffffffffff] | |
* arg3: [0x0 ~> 0xffffffffffffffff] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_r_cmovznz_u64(uint64_t* out1, fiat_bls12_381_r_uint1 arg1, uint64_t arg2, uint64_t arg3) { | |
fiat_bls12_381_r_uint1 x1 = (!(!arg1)); | |
uint64_t x2 = ((fiat_bls12_381_r_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); | |
uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); | |
*out1 = x3; | |
} | |
/* | |
* The function fiat_bls12_381_r_mul multiplies two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_mul(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) { | |
uint64_t x1 = (arg1[1]); | |
uint64_t x2 = (arg1[2]); | |
uint64_t x3 = (arg1[3]); | |
uint64_t x4 = (arg1[0]); | |
uint64_t x5; | |
uint64_t x6; | |
fiat_bls12_381_r_mulx_u64(&x5, &x6, x4, (arg2[3])); | |
uint64_t x7; | |
uint64_t x8; | |
fiat_bls12_381_r_mulx_u64(&x7, &x8, x4, (arg2[2])); | |
uint64_t x9; | |
uint64_t x10; | |
fiat_bls12_381_r_mulx_u64(&x9, &x10, x4, (arg2[1])); | |
uint64_t x11; | |
uint64_t x12; | |
fiat_bls12_381_r_mulx_u64(&x11, &x12, x4, (arg2[0])); | |
uint64_t x13; | |
fiat_bls12_381_r_uint1 x14; | |
fiat_bls12_381_r_addcarryx_u64(&x13, &x14, 0x0, x12, x9); | |
uint64_t x15; | |
fiat_bls12_381_r_uint1 x16; | |
fiat_bls12_381_r_addcarryx_u64(&x15, &x16, x14, x10, x7); | |
uint64_t x17; | |
fiat_bls12_381_r_uint1 x18; | |
fiat_bls12_381_r_addcarryx_u64(&x17, &x18, x16, x8, x5); | |
uint64_t x19; | |
fiat_bls12_381_r_uint1 x20; | |
fiat_bls12_381_r_addcarryx_u64(&x19, &x20, x18, x6, 0x0); | |
uint64_t x21; | |
uint64_t x22; | |
fiat_bls12_381_r_mulx_u64(&x21, &x22, x11, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x23; | |
uint64_t x24; | |
fiat_bls12_381_r_mulx_u64(&x23, &x24, x21, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x25; | |
uint64_t x26; | |
fiat_bls12_381_r_mulx_u64(&x25, &x26, x21, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x27; | |
uint64_t x28; | |
fiat_bls12_381_r_mulx_u64(&x27, &x28, x21, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x29; | |
uint64_t x30; | |
fiat_bls12_381_r_mulx_u64(&x29, &x30, x21, UINT64_C(0xffffffff00000001)); | |
uint64_t x31; | |
fiat_bls12_381_r_uint1 x32; | |
fiat_bls12_381_r_addcarryx_u64(&x31, &x32, 0x0, x30, x27); | |
uint64_t x33; | |
fiat_bls12_381_r_uint1 x34; | |
fiat_bls12_381_r_addcarryx_u64(&x33, &x34, x32, x28, x25); | |
uint64_t x35; | |
fiat_bls12_381_r_uint1 x36; | |
fiat_bls12_381_r_addcarryx_u64(&x35, &x36, x34, x26, x23); | |
uint64_t x37; | |
fiat_bls12_381_r_uint1 x38; | |
fiat_bls12_381_r_addcarryx_u64(&x37, &x38, x36, x24, 0x0); | |
uint64_t x39; | |
fiat_bls12_381_r_uint1 x40; | |
fiat_bls12_381_r_addcarryx_u64(&x39, &x40, 0x0, x11, x29); | |
uint64_t x41; | |
fiat_bls12_381_r_uint1 x42; | |
fiat_bls12_381_r_addcarryx_u64(&x41, &x42, x40, x13, x31); | |
uint64_t x43; | |
fiat_bls12_381_r_uint1 x44; | |
fiat_bls12_381_r_addcarryx_u64(&x43, &x44, x42, x15, x33); | |
uint64_t x45; | |
fiat_bls12_381_r_uint1 x46; | |
fiat_bls12_381_r_addcarryx_u64(&x45, &x46, x44, x17, x35); | |
uint64_t x47; | |
fiat_bls12_381_r_uint1 x48; | |
fiat_bls12_381_r_addcarryx_u64(&x47, &x48, x46, x19, x37); | |
uint64_t x49; | |
fiat_bls12_381_r_uint1 x50; | |
fiat_bls12_381_r_addcarryx_u64(&x49, &x50, x48, 0x0, 0x0); | |
uint64_t x51; | |
uint64_t x52; | |
fiat_bls12_381_r_mulx_u64(&x51, &x52, x1, (arg2[3])); | |
uint64_t x53; | |
uint64_t x54; | |
fiat_bls12_381_r_mulx_u64(&x53, &x54, x1, (arg2[2])); | |
uint64_t x55; | |
uint64_t x56; | |
fiat_bls12_381_r_mulx_u64(&x55, &x56, x1, (arg2[1])); | |
uint64_t x57; | |
uint64_t x58; | |
fiat_bls12_381_r_mulx_u64(&x57, &x58, x1, (arg2[0])); | |
uint64_t x59; | |
fiat_bls12_381_r_uint1 x60; | |
fiat_bls12_381_r_addcarryx_u64(&x59, &x60, 0x0, x58, x55); | |
uint64_t x61; | |
fiat_bls12_381_r_uint1 x62; | |
fiat_bls12_381_r_addcarryx_u64(&x61, &x62, x60, x56, x53); | |
uint64_t x63; | |
fiat_bls12_381_r_uint1 x64; | |
fiat_bls12_381_r_addcarryx_u64(&x63, &x64, x62, x54, x51); | |
uint64_t x65; | |
fiat_bls12_381_r_uint1 x66; | |
fiat_bls12_381_r_addcarryx_u64(&x65, &x66, x64, x52, 0x0); | |
uint64_t x67; | |
fiat_bls12_381_r_uint1 x68; | |
fiat_bls12_381_r_addcarryx_u64(&x67, &x68, 0x0, x41, x57); | |
uint64_t x69; | |
fiat_bls12_381_r_uint1 x70; | |
fiat_bls12_381_r_addcarryx_u64(&x69, &x70, x68, x43, x59); | |
uint64_t x71; | |
fiat_bls12_381_r_uint1 x72; | |
fiat_bls12_381_r_addcarryx_u64(&x71, &x72, x70, x45, x61); | |
uint64_t x73; | |
fiat_bls12_381_r_uint1 x74; | |
fiat_bls12_381_r_addcarryx_u64(&x73, &x74, x72, x47, x63); | |
uint64_t x75; | |
fiat_bls12_381_r_uint1 x76; | |
fiat_bls12_381_r_addcarryx_u64(&x75, &x76, x74, (fiat_bls12_381_r_uint1)x49, x65); | |
uint64_t x77; | |
uint64_t x78; | |
fiat_bls12_381_r_mulx_u64(&x77, &x78, x67, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x79; | |
uint64_t x80; | |
fiat_bls12_381_r_mulx_u64(&x79, &x80, x77, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x81; | |
uint64_t x82; | |
fiat_bls12_381_r_mulx_u64(&x81, &x82, x77, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x83; | |
uint64_t x84; | |
fiat_bls12_381_r_mulx_u64(&x83, &x84, x77, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x85; | |
uint64_t x86; | |
fiat_bls12_381_r_mulx_u64(&x85, &x86, x77, UINT64_C(0xffffffff00000001)); | |
uint64_t x87; | |
fiat_bls12_381_r_uint1 x88; | |
fiat_bls12_381_r_addcarryx_u64(&x87, &x88, 0x0, x86, x83); | |
uint64_t x89; | |
fiat_bls12_381_r_uint1 x90; | |
fiat_bls12_381_r_addcarryx_u64(&x89, &x90, x88, x84, x81); | |
uint64_t x91; | |
fiat_bls12_381_r_uint1 x92; | |
fiat_bls12_381_r_addcarryx_u64(&x91, &x92, x90, x82, x79); | |
uint64_t x93; | |
fiat_bls12_381_r_uint1 x94; | |
fiat_bls12_381_r_addcarryx_u64(&x93, &x94, x92, x80, 0x0); | |
uint64_t x95; | |
fiat_bls12_381_r_uint1 x96; | |
fiat_bls12_381_r_addcarryx_u64(&x95, &x96, 0x0, x67, x85); | |
uint64_t x97; | |
fiat_bls12_381_r_uint1 x98; | |
fiat_bls12_381_r_addcarryx_u64(&x97, &x98, x96, x69, x87); | |
uint64_t x99; | |
fiat_bls12_381_r_uint1 x100; | |
fiat_bls12_381_r_addcarryx_u64(&x99, &x100, x98, x71, x89); | |
uint64_t x101; | |
fiat_bls12_381_r_uint1 x102; | |
fiat_bls12_381_r_addcarryx_u64(&x101, &x102, x100, x73, x91); | |
uint64_t x103; | |
fiat_bls12_381_r_uint1 x104; | |
fiat_bls12_381_r_addcarryx_u64(&x103, &x104, x102, x75, x93); | |
uint64_t x105; | |
fiat_bls12_381_r_uint1 x106; | |
fiat_bls12_381_r_addcarryx_u64(&x105, &x106, x104, x76, 0x0); | |
uint64_t x107; | |
uint64_t x108; | |
fiat_bls12_381_r_mulx_u64(&x107, &x108, x2, (arg2[3])); | |
uint64_t x109; | |
uint64_t x110; | |
fiat_bls12_381_r_mulx_u64(&x109, &x110, x2, (arg2[2])); | |
uint64_t x111; | |
uint64_t x112; | |
fiat_bls12_381_r_mulx_u64(&x111, &x112, x2, (arg2[1])); | |
uint64_t x113; | |
uint64_t x114; | |
fiat_bls12_381_r_mulx_u64(&x113, &x114, x2, (arg2[0])); | |
uint64_t x115; | |
fiat_bls12_381_r_uint1 x116; | |
fiat_bls12_381_r_addcarryx_u64(&x115, &x116, 0x0, x114, x111); | |
uint64_t x117; | |
fiat_bls12_381_r_uint1 x118; | |
fiat_bls12_381_r_addcarryx_u64(&x117, &x118, x116, x112, x109); | |
uint64_t x119; | |
fiat_bls12_381_r_uint1 x120; | |
fiat_bls12_381_r_addcarryx_u64(&x119, &x120, x118, x110, x107); | |
uint64_t x121; | |
fiat_bls12_381_r_uint1 x122; | |
fiat_bls12_381_r_addcarryx_u64(&x121, &x122, x120, x108, 0x0); | |
uint64_t x123; | |
fiat_bls12_381_r_uint1 x124; | |
fiat_bls12_381_r_addcarryx_u64(&x123, &x124, 0x0, x97, x113); | |
uint64_t x125; | |
fiat_bls12_381_r_uint1 x126; | |
fiat_bls12_381_r_addcarryx_u64(&x125, &x126, x124, x99, x115); | |
uint64_t x127; | |
fiat_bls12_381_r_uint1 x128; | |
fiat_bls12_381_r_addcarryx_u64(&x127, &x128, x126, x101, x117); | |
uint64_t x129; | |
fiat_bls12_381_r_uint1 x130; | |
fiat_bls12_381_r_addcarryx_u64(&x129, &x130, x128, x103, x119); | |
uint64_t x131; | |
fiat_bls12_381_r_uint1 x132; | |
fiat_bls12_381_r_addcarryx_u64(&x131, &x132, x130, x105, x121); | |
uint64_t x133; | |
uint64_t x134; | |
fiat_bls12_381_r_mulx_u64(&x133, &x134, x123, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x135; | |
uint64_t x136; | |
fiat_bls12_381_r_mulx_u64(&x135, &x136, x133, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x137; | |
uint64_t x138; | |
fiat_bls12_381_r_mulx_u64(&x137, &x138, x133, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x139; | |
uint64_t x140; | |
fiat_bls12_381_r_mulx_u64(&x139, &x140, x133, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x141; | |
uint64_t x142; | |
fiat_bls12_381_r_mulx_u64(&x141, &x142, x133, UINT64_C(0xffffffff00000001)); | |
uint64_t x143; | |
fiat_bls12_381_r_uint1 x144; | |
fiat_bls12_381_r_addcarryx_u64(&x143, &x144, 0x0, x142, x139); | |
uint64_t x145; | |
fiat_bls12_381_r_uint1 x146; | |
fiat_bls12_381_r_addcarryx_u64(&x145, &x146, x144, x140, x137); | |
uint64_t x147; | |
fiat_bls12_381_r_uint1 x148; | |
fiat_bls12_381_r_addcarryx_u64(&x147, &x148, x146, x138, x135); | |
uint64_t x149; | |
fiat_bls12_381_r_uint1 x150; | |
fiat_bls12_381_r_addcarryx_u64(&x149, &x150, x148, x136, 0x0); | |
uint64_t x151; | |
fiat_bls12_381_r_uint1 x152; | |
fiat_bls12_381_r_addcarryx_u64(&x151, &x152, 0x0, x123, x141); | |
uint64_t x153; | |
fiat_bls12_381_r_uint1 x154; | |
fiat_bls12_381_r_addcarryx_u64(&x153, &x154, x152, x125, x143); | |
uint64_t x155; | |
fiat_bls12_381_r_uint1 x156; | |
fiat_bls12_381_r_addcarryx_u64(&x155, &x156, x154, x127, x145); | |
uint64_t x157; | |
fiat_bls12_381_r_uint1 x158; | |
fiat_bls12_381_r_addcarryx_u64(&x157, &x158, x156, x129, x147); | |
uint64_t x159; | |
fiat_bls12_381_r_uint1 x160; | |
fiat_bls12_381_r_addcarryx_u64(&x159, &x160, x158, x131, x149); | |
uint64_t x161; | |
fiat_bls12_381_r_uint1 x162; | |
fiat_bls12_381_r_addcarryx_u64(&x161, &x162, x160, x132, 0x0); | |
uint64_t x163; | |
uint64_t x164; | |
fiat_bls12_381_r_mulx_u64(&x163, &x164, x3, (arg2[3])); | |
uint64_t x165; | |
uint64_t x166; | |
fiat_bls12_381_r_mulx_u64(&x165, &x166, x3, (arg2[2])); | |
uint64_t x167; | |
uint64_t x168; | |
fiat_bls12_381_r_mulx_u64(&x167, &x168, x3, (arg2[1])); | |
uint64_t x169; | |
uint64_t x170; | |
fiat_bls12_381_r_mulx_u64(&x169, &x170, x3, (arg2[0])); | |
uint64_t x171; | |
fiat_bls12_381_r_uint1 x172; | |
fiat_bls12_381_r_addcarryx_u64(&x171, &x172, 0x0, x170, x167); | |
uint64_t x173; | |
fiat_bls12_381_r_uint1 x174; | |
fiat_bls12_381_r_addcarryx_u64(&x173, &x174, x172, x168, x165); | |
uint64_t x175; | |
fiat_bls12_381_r_uint1 x176; | |
fiat_bls12_381_r_addcarryx_u64(&x175, &x176, x174, x166, x163); | |
uint64_t x177; | |
fiat_bls12_381_r_uint1 x178; | |
fiat_bls12_381_r_addcarryx_u64(&x177, &x178, x176, x164, 0x0); | |
uint64_t x179; | |
fiat_bls12_381_r_uint1 x180; | |
fiat_bls12_381_r_addcarryx_u64(&x179, &x180, 0x0, x153, x169); | |
uint64_t x181; | |
fiat_bls12_381_r_uint1 x182; | |
fiat_bls12_381_r_addcarryx_u64(&x181, &x182, x180, x155, x171); | |
uint64_t x183; | |
fiat_bls12_381_r_uint1 x184; | |
fiat_bls12_381_r_addcarryx_u64(&x183, &x184, x182, x157, x173); | |
uint64_t x185; | |
fiat_bls12_381_r_uint1 x186; | |
fiat_bls12_381_r_addcarryx_u64(&x185, &x186, x184, x159, x175); | |
uint64_t x187; | |
fiat_bls12_381_r_uint1 x188; | |
fiat_bls12_381_r_addcarryx_u64(&x187, &x188, x186, x161, x177); | |
uint64_t x189; | |
uint64_t x190; | |
fiat_bls12_381_r_mulx_u64(&x189, &x190, x179, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x191; | |
uint64_t x192; | |
fiat_bls12_381_r_mulx_u64(&x191, &x192, x189, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x193; | |
uint64_t x194; | |
fiat_bls12_381_r_mulx_u64(&x193, &x194, x189, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x195; | |
uint64_t x196; | |
fiat_bls12_381_r_mulx_u64(&x195, &x196, x189, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x197; | |
uint64_t x198; | |
fiat_bls12_381_r_mulx_u64(&x197, &x198, x189, UINT64_C(0xffffffff00000001)); | |
uint64_t x199; | |
fiat_bls12_381_r_uint1 x200; | |
fiat_bls12_381_r_addcarryx_u64(&x199, &x200, 0x0, x198, x195); | |
uint64_t x201; | |
fiat_bls12_381_r_uint1 x202; | |
fiat_bls12_381_r_addcarryx_u64(&x201, &x202, x200, x196, x193); | |
uint64_t x203; | |
fiat_bls12_381_r_uint1 x204; | |
fiat_bls12_381_r_addcarryx_u64(&x203, &x204, x202, x194, x191); | |
uint64_t x205; | |
fiat_bls12_381_r_uint1 x206; | |
fiat_bls12_381_r_addcarryx_u64(&x205, &x206, x204, x192, 0x0); | |
uint64_t x207; | |
fiat_bls12_381_r_uint1 x208; | |
fiat_bls12_381_r_addcarryx_u64(&x207, &x208, 0x0, x179, x197); | |
uint64_t x209; | |
fiat_bls12_381_r_uint1 x210; | |
fiat_bls12_381_r_addcarryx_u64(&x209, &x210, x208, x181, x199); | |
uint64_t x211; | |
fiat_bls12_381_r_uint1 x212; | |
fiat_bls12_381_r_addcarryx_u64(&x211, &x212, x210, x183, x201); | |
uint64_t x213; | |
fiat_bls12_381_r_uint1 x214; | |
fiat_bls12_381_r_addcarryx_u64(&x213, &x214, x212, x185, x203); | |
uint64_t x215; | |
fiat_bls12_381_r_uint1 x216; | |
fiat_bls12_381_r_addcarryx_u64(&x215, &x216, x214, x187, x205); | |
uint64_t x217; | |
fiat_bls12_381_r_uint1 x218; | |
fiat_bls12_381_r_addcarryx_u64(&x217, &x218, x216, x188, 0x0); | |
uint64_t x219; | |
fiat_bls12_381_r_uint1 x220; | |
fiat_bls12_381_r_subborrowx_u64(&x219, &x220, 0x0, x209, UINT64_C(0xffffffff00000001)); | |
uint64_t x221; | |
fiat_bls12_381_r_uint1 x222; | |
fiat_bls12_381_r_subborrowx_u64(&x221, &x222, x220, x211, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x223; | |
fiat_bls12_381_r_uint1 x224; | |
fiat_bls12_381_r_subborrowx_u64(&x223, &x224, x222, x213, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x225; | |
fiat_bls12_381_r_uint1 x226; | |
fiat_bls12_381_r_subborrowx_u64(&x225, &x226, x224, x215, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x227; | |
fiat_bls12_381_r_uint1 x228; | |
fiat_bls12_381_r_subborrowx_u64(&x227, &x228, x226, x217, 0x0); | |
uint64_t x229; | |
fiat_bls12_381_r_cmovznz_u64(&x229, x228, x219, x209); | |
uint64_t x230; | |
fiat_bls12_381_r_cmovznz_u64(&x230, x228, x221, x211); | |
uint64_t x231; | |
fiat_bls12_381_r_cmovznz_u64(&x231, x228, x223, x213); | |
uint64_t x232; | |
fiat_bls12_381_r_cmovznz_u64(&x232, x228, x225, x215); | |
out1[0] = x229; | |
out1[1] = x230; | |
out1[2] = x231; | |
out1[3] = x232; | |
} | |
/* | |
* The function fiat_bls12_381_r_square squares a field element in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_square(uint64_t out1[4], const uint64_t arg1[4]) { | |
uint64_t x1 = (arg1[1]); | |
uint64_t x2 = (arg1[2]); | |
uint64_t x3 = (arg1[3]); | |
uint64_t x4 = (arg1[0]); | |
uint64_t x5; | |
uint64_t x6; | |
fiat_bls12_381_r_mulx_u64(&x5, &x6, x4, (arg1[3])); | |
uint64_t x7; | |
uint64_t x8; | |
fiat_bls12_381_r_mulx_u64(&x7, &x8, x4, (arg1[2])); | |
uint64_t x9; | |
uint64_t x10; | |
fiat_bls12_381_r_mulx_u64(&x9, &x10, x4, (arg1[1])); | |
uint64_t x11; | |
uint64_t x12; | |
fiat_bls12_381_r_mulx_u64(&x11, &x12, x4, (arg1[0])); | |
uint64_t x13; | |
fiat_bls12_381_r_uint1 x14; | |
fiat_bls12_381_r_addcarryx_u64(&x13, &x14, 0x0, x12, x9); | |
uint64_t x15; | |
fiat_bls12_381_r_uint1 x16; | |
fiat_bls12_381_r_addcarryx_u64(&x15, &x16, x14, x10, x7); | |
uint64_t x17; | |
fiat_bls12_381_r_uint1 x18; | |
fiat_bls12_381_r_addcarryx_u64(&x17, &x18, x16, x8, x5); | |
uint64_t x19; | |
fiat_bls12_381_r_uint1 x20; | |
fiat_bls12_381_r_addcarryx_u64(&x19, &x20, x18, x6, 0x0); | |
uint64_t x21; | |
uint64_t x22; | |
fiat_bls12_381_r_mulx_u64(&x21, &x22, x11, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x23; | |
uint64_t x24; | |
fiat_bls12_381_r_mulx_u64(&x23, &x24, x21, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x25; | |
uint64_t x26; | |
fiat_bls12_381_r_mulx_u64(&x25, &x26, x21, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x27; | |
uint64_t x28; | |
fiat_bls12_381_r_mulx_u64(&x27, &x28, x21, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x29; | |
uint64_t x30; | |
fiat_bls12_381_r_mulx_u64(&x29, &x30, x21, UINT64_C(0xffffffff00000001)); | |
uint64_t x31; | |
fiat_bls12_381_r_uint1 x32; | |
fiat_bls12_381_r_addcarryx_u64(&x31, &x32, 0x0, x30, x27); | |
uint64_t x33; | |
fiat_bls12_381_r_uint1 x34; | |
fiat_bls12_381_r_addcarryx_u64(&x33, &x34, x32, x28, x25); | |
uint64_t x35; | |
fiat_bls12_381_r_uint1 x36; | |
fiat_bls12_381_r_addcarryx_u64(&x35, &x36, x34, x26, x23); | |
uint64_t x37; | |
fiat_bls12_381_r_uint1 x38; | |
fiat_bls12_381_r_addcarryx_u64(&x37, &x38, x36, x24, 0x0); | |
uint64_t x39; | |
fiat_bls12_381_r_uint1 x40; | |
fiat_bls12_381_r_addcarryx_u64(&x39, &x40, 0x0, x11, x29); | |
uint64_t x41; | |
fiat_bls12_381_r_uint1 x42; | |
fiat_bls12_381_r_addcarryx_u64(&x41, &x42, x40, x13, x31); | |
uint64_t x43; | |
fiat_bls12_381_r_uint1 x44; | |
fiat_bls12_381_r_addcarryx_u64(&x43, &x44, x42, x15, x33); | |
uint64_t x45; | |
fiat_bls12_381_r_uint1 x46; | |
fiat_bls12_381_r_addcarryx_u64(&x45, &x46, x44, x17, x35); | |
uint64_t x47; | |
fiat_bls12_381_r_uint1 x48; | |
fiat_bls12_381_r_addcarryx_u64(&x47, &x48, x46, x19, x37); | |
uint64_t x49; | |
fiat_bls12_381_r_uint1 x50; | |
fiat_bls12_381_r_addcarryx_u64(&x49, &x50, x48, 0x0, 0x0); | |
uint64_t x51; | |
uint64_t x52; | |
fiat_bls12_381_r_mulx_u64(&x51, &x52, x1, (arg1[3])); | |
uint64_t x53; | |
uint64_t x54; | |
fiat_bls12_381_r_mulx_u64(&x53, &x54, x1, (arg1[2])); | |
uint64_t x55; | |
uint64_t x56; | |
fiat_bls12_381_r_mulx_u64(&x55, &x56, x1, (arg1[1])); | |
uint64_t x57; | |
uint64_t x58; | |
fiat_bls12_381_r_mulx_u64(&x57, &x58, x1, (arg1[0])); | |
uint64_t x59; | |
fiat_bls12_381_r_uint1 x60; | |
fiat_bls12_381_r_addcarryx_u64(&x59, &x60, 0x0, x58, x55); | |
uint64_t x61; | |
fiat_bls12_381_r_uint1 x62; | |
fiat_bls12_381_r_addcarryx_u64(&x61, &x62, x60, x56, x53); | |
uint64_t x63; | |
fiat_bls12_381_r_uint1 x64; | |
fiat_bls12_381_r_addcarryx_u64(&x63, &x64, x62, x54, x51); | |
uint64_t x65; | |
fiat_bls12_381_r_uint1 x66; | |
fiat_bls12_381_r_addcarryx_u64(&x65, &x66, x64, x52, 0x0); | |
uint64_t x67; | |
fiat_bls12_381_r_uint1 x68; | |
fiat_bls12_381_r_addcarryx_u64(&x67, &x68, 0x0, x41, x57); | |
uint64_t x69; | |
fiat_bls12_381_r_uint1 x70; | |
fiat_bls12_381_r_addcarryx_u64(&x69, &x70, x68, x43, x59); | |
uint64_t x71; | |
fiat_bls12_381_r_uint1 x72; | |
fiat_bls12_381_r_addcarryx_u64(&x71, &x72, x70, x45, x61); | |
uint64_t x73; | |
fiat_bls12_381_r_uint1 x74; | |
fiat_bls12_381_r_addcarryx_u64(&x73, &x74, x72, x47, x63); | |
uint64_t x75; | |
fiat_bls12_381_r_uint1 x76; | |
fiat_bls12_381_r_addcarryx_u64(&x75, &x76, x74, (fiat_bls12_381_r_uint1)x49, x65); | |
uint64_t x77; | |
uint64_t x78; | |
fiat_bls12_381_r_mulx_u64(&x77, &x78, x67, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x79; | |
uint64_t x80; | |
fiat_bls12_381_r_mulx_u64(&x79, &x80, x77, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x81; | |
uint64_t x82; | |
fiat_bls12_381_r_mulx_u64(&x81, &x82, x77, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x83; | |
uint64_t x84; | |
fiat_bls12_381_r_mulx_u64(&x83, &x84, x77, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x85; | |
uint64_t x86; | |
fiat_bls12_381_r_mulx_u64(&x85, &x86, x77, UINT64_C(0xffffffff00000001)); | |
uint64_t x87; | |
fiat_bls12_381_r_uint1 x88; | |
fiat_bls12_381_r_addcarryx_u64(&x87, &x88, 0x0, x86, x83); | |
uint64_t x89; | |
fiat_bls12_381_r_uint1 x90; | |
fiat_bls12_381_r_addcarryx_u64(&x89, &x90, x88, x84, x81); | |
uint64_t x91; | |
fiat_bls12_381_r_uint1 x92; | |
fiat_bls12_381_r_addcarryx_u64(&x91, &x92, x90, x82, x79); | |
uint64_t x93; | |
fiat_bls12_381_r_uint1 x94; | |
fiat_bls12_381_r_addcarryx_u64(&x93, &x94, x92, x80, 0x0); | |
uint64_t x95; | |
fiat_bls12_381_r_uint1 x96; | |
fiat_bls12_381_r_addcarryx_u64(&x95, &x96, 0x0, x67, x85); | |
uint64_t x97; | |
fiat_bls12_381_r_uint1 x98; | |
fiat_bls12_381_r_addcarryx_u64(&x97, &x98, x96, x69, x87); | |
uint64_t x99; | |
fiat_bls12_381_r_uint1 x100; | |
fiat_bls12_381_r_addcarryx_u64(&x99, &x100, x98, x71, x89); | |
uint64_t x101; | |
fiat_bls12_381_r_uint1 x102; | |
fiat_bls12_381_r_addcarryx_u64(&x101, &x102, x100, x73, x91); | |
uint64_t x103; | |
fiat_bls12_381_r_uint1 x104; | |
fiat_bls12_381_r_addcarryx_u64(&x103, &x104, x102, x75, x93); | |
uint64_t x105; | |
fiat_bls12_381_r_uint1 x106; | |
fiat_bls12_381_r_addcarryx_u64(&x105, &x106, x104, x76, 0x0); | |
uint64_t x107; | |
uint64_t x108; | |
fiat_bls12_381_r_mulx_u64(&x107, &x108, x2, (arg1[3])); | |
uint64_t x109; | |
uint64_t x110; | |
fiat_bls12_381_r_mulx_u64(&x109, &x110, x2, (arg1[2])); | |
uint64_t x111; | |
uint64_t x112; | |
fiat_bls12_381_r_mulx_u64(&x111, &x112, x2, (arg1[1])); | |
uint64_t x113; | |
uint64_t x114; | |
fiat_bls12_381_r_mulx_u64(&x113, &x114, x2, (arg1[0])); | |
uint64_t x115; | |
fiat_bls12_381_r_uint1 x116; | |
fiat_bls12_381_r_addcarryx_u64(&x115, &x116, 0x0, x114, x111); | |
uint64_t x117; | |
fiat_bls12_381_r_uint1 x118; | |
fiat_bls12_381_r_addcarryx_u64(&x117, &x118, x116, x112, x109); | |
uint64_t x119; | |
fiat_bls12_381_r_uint1 x120; | |
fiat_bls12_381_r_addcarryx_u64(&x119, &x120, x118, x110, x107); | |
uint64_t x121; | |
fiat_bls12_381_r_uint1 x122; | |
fiat_bls12_381_r_addcarryx_u64(&x121, &x122, x120, x108, 0x0); | |
uint64_t x123; | |
fiat_bls12_381_r_uint1 x124; | |
fiat_bls12_381_r_addcarryx_u64(&x123, &x124, 0x0, x97, x113); | |
uint64_t x125; | |
fiat_bls12_381_r_uint1 x126; | |
fiat_bls12_381_r_addcarryx_u64(&x125, &x126, x124, x99, x115); | |
uint64_t x127; | |
fiat_bls12_381_r_uint1 x128; | |
fiat_bls12_381_r_addcarryx_u64(&x127, &x128, x126, x101, x117); | |
uint64_t x129; | |
fiat_bls12_381_r_uint1 x130; | |
fiat_bls12_381_r_addcarryx_u64(&x129, &x130, x128, x103, x119); | |
uint64_t x131; | |
fiat_bls12_381_r_uint1 x132; | |
fiat_bls12_381_r_addcarryx_u64(&x131, &x132, x130, x105, x121); | |
uint64_t x133; | |
uint64_t x134; | |
fiat_bls12_381_r_mulx_u64(&x133, &x134, x123, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x135; | |
uint64_t x136; | |
fiat_bls12_381_r_mulx_u64(&x135, &x136, x133, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x137; | |
uint64_t x138; | |
fiat_bls12_381_r_mulx_u64(&x137, &x138, x133, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x139; | |
uint64_t x140; | |
fiat_bls12_381_r_mulx_u64(&x139, &x140, x133, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x141; | |
uint64_t x142; | |
fiat_bls12_381_r_mulx_u64(&x141, &x142, x133, UINT64_C(0xffffffff00000001)); | |
uint64_t x143; | |
fiat_bls12_381_r_uint1 x144; | |
fiat_bls12_381_r_addcarryx_u64(&x143, &x144, 0x0, x142, x139); | |
uint64_t x145; | |
fiat_bls12_381_r_uint1 x146; | |
fiat_bls12_381_r_addcarryx_u64(&x145, &x146, x144, x140, x137); | |
uint64_t x147; | |
fiat_bls12_381_r_uint1 x148; | |
fiat_bls12_381_r_addcarryx_u64(&x147, &x148, x146, x138, x135); | |
uint64_t x149; | |
fiat_bls12_381_r_uint1 x150; | |
fiat_bls12_381_r_addcarryx_u64(&x149, &x150, x148, x136, 0x0); | |
uint64_t x151; | |
fiat_bls12_381_r_uint1 x152; | |
fiat_bls12_381_r_addcarryx_u64(&x151, &x152, 0x0, x123, x141); | |
uint64_t x153; | |
fiat_bls12_381_r_uint1 x154; | |
fiat_bls12_381_r_addcarryx_u64(&x153, &x154, x152, x125, x143); | |
uint64_t x155; | |
fiat_bls12_381_r_uint1 x156; | |
fiat_bls12_381_r_addcarryx_u64(&x155, &x156, x154, x127, x145); | |
uint64_t x157; | |
fiat_bls12_381_r_uint1 x158; | |
fiat_bls12_381_r_addcarryx_u64(&x157, &x158, x156, x129, x147); | |
uint64_t x159; | |
fiat_bls12_381_r_uint1 x160; | |
fiat_bls12_381_r_addcarryx_u64(&x159, &x160, x158, x131, x149); | |
uint64_t x161; | |
fiat_bls12_381_r_uint1 x162; | |
fiat_bls12_381_r_addcarryx_u64(&x161, &x162, x160, x132, 0x0); | |
uint64_t x163; | |
uint64_t x164; | |
fiat_bls12_381_r_mulx_u64(&x163, &x164, x3, (arg1[3])); | |
uint64_t x165; | |
uint64_t x166; | |
fiat_bls12_381_r_mulx_u64(&x165, &x166, x3, (arg1[2])); | |
uint64_t x167; | |
uint64_t x168; | |
fiat_bls12_381_r_mulx_u64(&x167, &x168, x3, (arg1[1])); | |
uint64_t x169; | |
uint64_t x170; | |
fiat_bls12_381_r_mulx_u64(&x169, &x170, x3, (arg1[0])); | |
uint64_t x171; | |
fiat_bls12_381_r_uint1 x172; | |
fiat_bls12_381_r_addcarryx_u64(&x171, &x172, 0x0, x170, x167); | |
uint64_t x173; | |
fiat_bls12_381_r_uint1 x174; | |
fiat_bls12_381_r_addcarryx_u64(&x173, &x174, x172, x168, x165); | |
uint64_t x175; | |
fiat_bls12_381_r_uint1 x176; | |
fiat_bls12_381_r_addcarryx_u64(&x175, &x176, x174, x166, x163); | |
uint64_t x177; | |
fiat_bls12_381_r_uint1 x178; | |
fiat_bls12_381_r_addcarryx_u64(&x177, &x178, x176, x164, 0x0); | |
uint64_t x179; | |
fiat_bls12_381_r_uint1 x180; | |
fiat_bls12_381_r_addcarryx_u64(&x179, &x180, 0x0, x153, x169); | |
uint64_t x181; | |
fiat_bls12_381_r_uint1 x182; | |
fiat_bls12_381_r_addcarryx_u64(&x181, &x182, x180, x155, x171); | |
uint64_t x183; | |
fiat_bls12_381_r_uint1 x184; | |
fiat_bls12_381_r_addcarryx_u64(&x183, &x184, x182, x157, x173); | |
uint64_t x185; | |
fiat_bls12_381_r_uint1 x186; | |
fiat_bls12_381_r_addcarryx_u64(&x185, &x186, x184, x159, x175); | |
uint64_t x187; | |
fiat_bls12_381_r_uint1 x188; | |
fiat_bls12_381_r_addcarryx_u64(&x187, &x188, x186, x161, x177); | |
uint64_t x189; | |
uint64_t x190; | |
fiat_bls12_381_r_mulx_u64(&x189, &x190, x179, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x191; | |
uint64_t x192; | |
fiat_bls12_381_r_mulx_u64(&x191, &x192, x189, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x193; | |
uint64_t x194; | |
fiat_bls12_381_r_mulx_u64(&x193, &x194, x189, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x195; | |
uint64_t x196; | |
fiat_bls12_381_r_mulx_u64(&x195, &x196, x189, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x197; | |
uint64_t x198; | |
fiat_bls12_381_r_mulx_u64(&x197, &x198, x189, UINT64_C(0xffffffff00000001)); | |
uint64_t x199; | |
fiat_bls12_381_r_uint1 x200; | |
fiat_bls12_381_r_addcarryx_u64(&x199, &x200, 0x0, x198, x195); | |
uint64_t x201; | |
fiat_bls12_381_r_uint1 x202; | |
fiat_bls12_381_r_addcarryx_u64(&x201, &x202, x200, x196, x193); | |
uint64_t x203; | |
fiat_bls12_381_r_uint1 x204; | |
fiat_bls12_381_r_addcarryx_u64(&x203, &x204, x202, x194, x191); | |
uint64_t x205; | |
fiat_bls12_381_r_uint1 x206; | |
fiat_bls12_381_r_addcarryx_u64(&x205, &x206, x204, x192, 0x0); | |
uint64_t x207; | |
fiat_bls12_381_r_uint1 x208; | |
fiat_bls12_381_r_addcarryx_u64(&x207, &x208, 0x0, x179, x197); | |
uint64_t x209; | |
fiat_bls12_381_r_uint1 x210; | |
fiat_bls12_381_r_addcarryx_u64(&x209, &x210, x208, x181, x199); | |
uint64_t x211; | |
fiat_bls12_381_r_uint1 x212; | |
fiat_bls12_381_r_addcarryx_u64(&x211, &x212, x210, x183, x201); | |
uint64_t x213; | |
fiat_bls12_381_r_uint1 x214; | |
fiat_bls12_381_r_addcarryx_u64(&x213, &x214, x212, x185, x203); | |
uint64_t x215; | |
fiat_bls12_381_r_uint1 x216; | |
fiat_bls12_381_r_addcarryx_u64(&x215, &x216, x214, x187, x205); | |
uint64_t x217; | |
fiat_bls12_381_r_uint1 x218; | |
fiat_bls12_381_r_addcarryx_u64(&x217, &x218, x216, x188, 0x0); | |
uint64_t x219; | |
fiat_bls12_381_r_uint1 x220; | |
fiat_bls12_381_r_subborrowx_u64(&x219, &x220, 0x0, x209, UINT64_C(0xffffffff00000001)); | |
uint64_t x221; | |
fiat_bls12_381_r_uint1 x222; | |
fiat_bls12_381_r_subborrowx_u64(&x221, &x222, x220, x211, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x223; | |
fiat_bls12_381_r_uint1 x224; | |
fiat_bls12_381_r_subborrowx_u64(&x223, &x224, x222, x213, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x225; | |
fiat_bls12_381_r_uint1 x226; | |
fiat_bls12_381_r_subborrowx_u64(&x225, &x226, x224, x215, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x227; | |
fiat_bls12_381_r_uint1 x228; | |
fiat_bls12_381_r_subborrowx_u64(&x227, &x228, x226, x217, 0x0); | |
uint64_t x229; | |
fiat_bls12_381_r_cmovznz_u64(&x229, x228, x219, x209); | |
uint64_t x230; | |
fiat_bls12_381_r_cmovznz_u64(&x230, x228, x221, x211); | |
uint64_t x231; | |
fiat_bls12_381_r_cmovznz_u64(&x231, x228, x223, x213); | |
uint64_t x232; | |
fiat_bls12_381_r_cmovznz_u64(&x232, x228, x225, x215); | |
out1[0] = x229; | |
out1[1] = x230; | |
out1[2] = x231; | |
out1[3] = x232; | |
} | |
/* | |
* The function fiat_bls12_381_r_add adds two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_add(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) { | |
uint64_t x1; | |
fiat_bls12_381_r_uint1 x2; | |
fiat_bls12_381_r_addcarryx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); | |
uint64_t x3; | |
fiat_bls12_381_r_uint1 x4; | |
fiat_bls12_381_r_addcarryx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1])); | |
uint64_t x5; | |
fiat_bls12_381_r_uint1 x6; | |
fiat_bls12_381_r_addcarryx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2])); | |
uint64_t x7; | |
fiat_bls12_381_r_uint1 x8; | |
fiat_bls12_381_r_addcarryx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3])); | |
uint64_t x9; | |
fiat_bls12_381_r_uint1 x10; | |
fiat_bls12_381_r_subborrowx_u64(&x9, &x10, 0x0, x1, UINT64_C(0xffffffff00000001)); | |
uint64_t x11; | |
fiat_bls12_381_r_uint1 x12; | |
fiat_bls12_381_r_subborrowx_u64(&x11, &x12, x10, x3, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x13; | |
fiat_bls12_381_r_uint1 x14; | |
fiat_bls12_381_r_subborrowx_u64(&x13, &x14, x12, x5, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x15; | |
fiat_bls12_381_r_uint1 x16; | |
fiat_bls12_381_r_subborrowx_u64(&x15, &x16, x14, x7, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x17; | |
fiat_bls12_381_r_uint1 x18; | |
fiat_bls12_381_r_subborrowx_u64(&x17, &x18, x16, x8, 0x0); | |
uint64_t x19; | |
fiat_bls12_381_r_cmovznz_u64(&x19, x18, x9, x1); | |
uint64_t x20; | |
fiat_bls12_381_r_cmovznz_u64(&x20, x18, x11, x3); | |
uint64_t x21; | |
fiat_bls12_381_r_cmovznz_u64(&x21, x18, x13, x5); | |
uint64_t x22; | |
fiat_bls12_381_r_cmovznz_u64(&x22, x18, x15, x7); | |
out1[0] = x19; | |
out1[1] = x20; | |
out1[2] = x21; | |
out1[3] = x22; | |
} | |
/* | |
* The function fiat_bls12_381_r_sub subtracts two field elements in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* 0 ≤ eval arg2 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) { | |
uint64_t x1; | |
fiat_bls12_381_r_uint1 x2; | |
fiat_bls12_381_r_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0])); | |
uint64_t x3; | |
fiat_bls12_381_r_uint1 x4; | |
fiat_bls12_381_r_subborrowx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1])); | |
uint64_t x5; | |
fiat_bls12_381_r_uint1 x6; | |
fiat_bls12_381_r_subborrowx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2])); | |
uint64_t x7; | |
fiat_bls12_381_r_uint1 x8; | |
fiat_bls12_381_r_subborrowx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3])); | |
uint64_t x9; | |
fiat_bls12_381_r_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff)); | |
uint64_t x10; | |
fiat_bls12_381_r_uint1 x11; | |
fiat_bls12_381_r_addcarryx_u64(&x10, &x11, 0x0, x1, (x9 & UINT64_C(0xffffffff00000001))); | |
uint64_t x12; | |
fiat_bls12_381_r_uint1 x13; | |
fiat_bls12_381_r_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT64_C(0x53bda402fffe5bfe))); | |
uint64_t x14; | |
fiat_bls12_381_r_uint1 x15; | |
fiat_bls12_381_r_addcarryx_u64(&x14, &x15, x13, x5, (x9 & UINT64_C(0x3339d80809a1d805))); | |
uint64_t x16; | |
fiat_bls12_381_r_uint1 x17; | |
fiat_bls12_381_r_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0x73eda753299d7d48))); | |
out1[0] = x10; | |
out1[1] = x12; | |
out1[2] = x14; | |
out1[3] = x16; | |
} | |
/* | |
* The function fiat_bls12_381_r_opp negates a field element in the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_opp(uint64_t out1[4], const uint64_t arg1[4]) { | |
uint64_t x1; | |
fiat_bls12_381_r_uint1 x2; | |
fiat_bls12_381_r_subborrowx_u64(&x1, &x2, 0x0, 0x0, (arg1[0])); | |
uint64_t x3; | |
fiat_bls12_381_r_uint1 x4; | |
fiat_bls12_381_r_subborrowx_u64(&x3, &x4, x2, 0x0, (arg1[1])); | |
uint64_t x5; | |
fiat_bls12_381_r_uint1 x6; | |
fiat_bls12_381_r_subborrowx_u64(&x5, &x6, x4, 0x0, (arg1[2])); | |
uint64_t x7; | |
fiat_bls12_381_r_uint1 x8; | |
fiat_bls12_381_r_subborrowx_u64(&x7, &x8, x6, 0x0, (arg1[3])); | |
uint64_t x9; | |
fiat_bls12_381_r_cmovznz_u64(&x9, x8, 0x0, UINT64_C(0xffffffffffffffff)); | |
uint64_t x10; | |
fiat_bls12_381_r_uint1 x11; | |
fiat_bls12_381_r_addcarryx_u64(&x10, &x11, 0x0, x1, (x9 & UINT64_C(0xffffffff00000001))); | |
uint64_t x12; | |
fiat_bls12_381_r_uint1 x13; | |
fiat_bls12_381_r_addcarryx_u64(&x12, &x13, x11, x3, (x9 & UINT64_C(0x53bda402fffe5bfe))); | |
uint64_t x14; | |
fiat_bls12_381_r_uint1 x15; | |
fiat_bls12_381_r_addcarryx_u64(&x14, &x15, x13, x5, (x9 & UINT64_C(0x3339d80809a1d805))); | |
uint64_t x16; | |
fiat_bls12_381_r_uint1 x17; | |
fiat_bls12_381_r_addcarryx_u64(&x16, &x17, x15, x7, (x9 & UINT64_C(0x73eda753299d7d48))); | |
out1[0] = x10; | |
out1[1] = x12; | |
out1[2] = x14; | |
out1[3] = x16; | |
} | |
/* | |
* The function fiat_bls12_381_r_from_montgomery translates a field element out of the Montgomery domain. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_from_montgomery(uint64_t out1[4], const uint64_t arg1[4]) { | |
uint64_t x1 = (arg1[0]); | |
uint64_t x2; | |
uint64_t x3; | |
fiat_bls12_381_r_mulx_u64(&x2, &x3, x1, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x4; | |
uint64_t x5; | |
fiat_bls12_381_r_mulx_u64(&x4, &x5, x2, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x6; | |
uint64_t x7; | |
fiat_bls12_381_r_mulx_u64(&x6, &x7, x2, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x8; | |
uint64_t x9; | |
fiat_bls12_381_r_mulx_u64(&x8, &x9, x2, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x10; | |
uint64_t x11; | |
fiat_bls12_381_r_mulx_u64(&x10, &x11, x2, UINT64_C(0xffffffff00000001)); | |
uint64_t x12; | |
fiat_bls12_381_r_uint1 x13; | |
fiat_bls12_381_r_addcarryx_u64(&x12, &x13, 0x0, x11, x8); | |
uint64_t x14; | |
fiat_bls12_381_r_uint1 x15; | |
fiat_bls12_381_r_addcarryx_u64(&x14, &x15, x13, x9, x6); | |
uint64_t x16; | |
fiat_bls12_381_r_uint1 x17; | |
fiat_bls12_381_r_addcarryx_u64(&x16, &x17, x15, x7, x4); | |
uint64_t x18; | |
fiat_bls12_381_r_uint1 x19; | |
fiat_bls12_381_r_addcarryx_u64(&x18, &x19, 0x0, x1, x10); | |
uint64_t x20; | |
fiat_bls12_381_r_uint1 x21; | |
fiat_bls12_381_r_addcarryx_u64(&x20, &x21, x19, 0x0, x12); | |
uint64_t x22; | |
fiat_bls12_381_r_uint1 x23; | |
fiat_bls12_381_r_addcarryx_u64(&x22, &x23, x21, 0x0, x14); | |
uint64_t x24; | |
fiat_bls12_381_r_uint1 x25; | |
fiat_bls12_381_r_addcarryx_u64(&x24, &x25, x23, 0x0, x16); | |
uint64_t x26; | |
fiat_bls12_381_r_uint1 x27; | |
fiat_bls12_381_r_addcarryx_u64(&x26, &x27, 0x0, x20, (arg1[1])); | |
uint64_t x28; | |
fiat_bls12_381_r_uint1 x29; | |
fiat_bls12_381_r_addcarryx_u64(&x28, &x29, x27, x22, 0x0); | |
uint64_t x30; | |
fiat_bls12_381_r_uint1 x31; | |
fiat_bls12_381_r_addcarryx_u64(&x30, &x31, x29, x24, 0x0); | |
uint64_t x32; | |
uint64_t x33; | |
fiat_bls12_381_r_mulx_u64(&x32, &x33, x26, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x34; | |
uint64_t x35; | |
fiat_bls12_381_r_mulx_u64(&x34, &x35, x32, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x36; | |
uint64_t x37; | |
fiat_bls12_381_r_mulx_u64(&x36, &x37, x32, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x38; | |
uint64_t x39; | |
fiat_bls12_381_r_mulx_u64(&x38, &x39, x32, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x40; | |
uint64_t x41; | |
fiat_bls12_381_r_mulx_u64(&x40, &x41, x32, UINT64_C(0xffffffff00000001)); | |
uint64_t x42; | |
fiat_bls12_381_r_uint1 x43; | |
fiat_bls12_381_r_addcarryx_u64(&x42, &x43, 0x0, x41, x38); | |
uint64_t x44; | |
fiat_bls12_381_r_uint1 x45; | |
fiat_bls12_381_r_addcarryx_u64(&x44, &x45, x43, x39, x36); | |
uint64_t x46; | |
fiat_bls12_381_r_uint1 x47; | |
fiat_bls12_381_r_addcarryx_u64(&x46, &x47, x45, x37, x34); | |
uint64_t x48; | |
fiat_bls12_381_r_uint1 x49; | |
fiat_bls12_381_r_addcarryx_u64(&x48, &x49, 0x0, x26, x40); | |
uint64_t x50; | |
fiat_bls12_381_r_uint1 x51; | |
fiat_bls12_381_r_addcarryx_u64(&x50, &x51, x49, x28, x42); | |
uint64_t x52; | |
fiat_bls12_381_r_uint1 x53; | |
fiat_bls12_381_r_addcarryx_u64(&x52, &x53, x51, x30, x44); | |
uint64_t x54; | |
fiat_bls12_381_r_uint1 x55; | |
fiat_bls12_381_r_addcarryx_u64(&x54, &x55, x17, x5, 0x0); | |
uint64_t x56; | |
fiat_bls12_381_r_uint1 x57; | |
fiat_bls12_381_r_addcarryx_u64(&x56, &x57, x25, 0x0, x54); | |
uint64_t x58; | |
fiat_bls12_381_r_uint1 x59; | |
fiat_bls12_381_r_addcarryx_u64(&x58, &x59, x31, x56, 0x0); | |
uint64_t x60; | |
fiat_bls12_381_r_uint1 x61; | |
fiat_bls12_381_r_addcarryx_u64(&x60, &x61, x53, x58, x46); | |
uint64_t x62; | |
fiat_bls12_381_r_uint1 x63; | |
fiat_bls12_381_r_addcarryx_u64(&x62, &x63, 0x0, x50, (arg1[2])); | |
uint64_t x64; | |
fiat_bls12_381_r_uint1 x65; | |
fiat_bls12_381_r_addcarryx_u64(&x64, &x65, x63, x52, 0x0); | |
uint64_t x66; | |
fiat_bls12_381_r_uint1 x67; | |
fiat_bls12_381_r_addcarryx_u64(&x66, &x67, x65, x60, 0x0); | |
uint64_t x68; | |
uint64_t x69; | |
fiat_bls12_381_r_mulx_u64(&x68, &x69, x62, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x70; | |
uint64_t x71; | |
fiat_bls12_381_r_mulx_u64(&x70, &x71, x68, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x72; | |
uint64_t x73; | |
fiat_bls12_381_r_mulx_u64(&x72, &x73, x68, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x74; | |
uint64_t x75; | |
fiat_bls12_381_r_mulx_u64(&x74, &x75, x68, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x76; | |
uint64_t x77; | |
fiat_bls12_381_r_mulx_u64(&x76, &x77, x68, UINT64_C(0xffffffff00000001)); | |
uint64_t x78; | |
fiat_bls12_381_r_uint1 x79; | |
fiat_bls12_381_r_addcarryx_u64(&x78, &x79, 0x0, x77, x74); | |
uint64_t x80; | |
fiat_bls12_381_r_uint1 x81; | |
fiat_bls12_381_r_addcarryx_u64(&x80, &x81, x79, x75, x72); | |
uint64_t x82; | |
fiat_bls12_381_r_uint1 x83; | |
fiat_bls12_381_r_addcarryx_u64(&x82, &x83, x81, x73, x70); | |
uint64_t x84; | |
fiat_bls12_381_r_uint1 x85; | |
fiat_bls12_381_r_addcarryx_u64(&x84, &x85, 0x0, x62, x76); | |
uint64_t x86; | |
fiat_bls12_381_r_uint1 x87; | |
fiat_bls12_381_r_addcarryx_u64(&x86, &x87, x85, x64, x78); | |
uint64_t x88; | |
fiat_bls12_381_r_uint1 x89; | |
fiat_bls12_381_r_addcarryx_u64(&x88, &x89, x87, x66, x80); | |
uint64_t x90; | |
fiat_bls12_381_r_uint1 x91; | |
fiat_bls12_381_r_addcarryx_u64(&x90, &x91, x47, x35, 0x0); | |
uint64_t x92; | |
fiat_bls12_381_r_uint1 x93; | |
fiat_bls12_381_r_addcarryx_u64(&x92, &x93, x61, 0x0, x90); | |
uint64_t x94; | |
fiat_bls12_381_r_uint1 x95; | |
fiat_bls12_381_r_addcarryx_u64(&x94, &x95, x67, x92, 0x0); | |
uint64_t x96; | |
fiat_bls12_381_r_uint1 x97; | |
fiat_bls12_381_r_addcarryx_u64(&x96, &x97, x89, x94, x82); | |
uint64_t x98; | |
fiat_bls12_381_r_uint1 x99; | |
fiat_bls12_381_r_addcarryx_u64(&x98, &x99, 0x0, x86, (arg1[3])); | |
uint64_t x100; | |
fiat_bls12_381_r_uint1 x101; | |
fiat_bls12_381_r_addcarryx_u64(&x100, &x101, x99, x88, 0x0); | |
uint64_t x102; | |
fiat_bls12_381_r_uint1 x103; | |
fiat_bls12_381_r_addcarryx_u64(&x102, &x103, x101, x96, 0x0); | |
uint64_t x104; | |
uint64_t x105; | |
fiat_bls12_381_r_mulx_u64(&x104, &x105, x98, UINT64_C(0xfffffffeffffffff)); | |
uint64_t x106; | |
uint64_t x107; | |
fiat_bls12_381_r_mulx_u64(&x106, &x107, x104, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x108; | |
uint64_t x109; | |
fiat_bls12_381_r_mulx_u64(&x108, &x109, x104, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x110; | |
uint64_t x111; | |
fiat_bls12_381_r_mulx_u64(&x110, &x111, x104, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x112; | |
uint64_t x113; | |
fiat_bls12_381_r_mulx_u64(&x112, &x113, x104, UINT64_C(0xffffffff00000001)); | |
uint64_t x114; | |
fiat_bls12_381_r_uint1 x115; | |
fiat_bls12_381_r_addcarryx_u64(&x114, &x115, 0x0, x113, x110); | |
uint64_t x116; | |
fiat_bls12_381_r_uint1 x117; | |
fiat_bls12_381_r_addcarryx_u64(&x116, &x117, x115, x111, x108); | |
uint64_t x118; | |
fiat_bls12_381_r_uint1 x119; | |
fiat_bls12_381_r_addcarryx_u64(&x118, &x119, x117, x109, x106); | |
uint64_t x120; | |
fiat_bls12_381_r_uint1 x121; | |
fiat_bls12_381_r_addcarryx_u64(&x120, &x121, 0x0, x98, x112); | |
uint64_t x122; | |
fiat_bls12_381_r_uint1 x123; | |
fiat_bls12_381_r_addcarryx_u64(&x122, &x123, x121, x100, x114); | |
uint64_t x124; | |
fiat_bls12_381_r_uint1 x125; | |
fiat_bls12_381_r_addcarryx_u64(&x124, &x125, x123, x102, x116); | |
uint64_t x126; | |
fiat_bls12_381_r_uint1 x127; | |
fiat_bls12_381_r_addcarryx_u64(&x126, &x127, x83, x71, 0x0); | |
uint64_t x128; | |
fiat_bls12_381_r_uint1 x129; | |
fiat_bls12_381_r_addcarryx_u64(&x128, &x129, x97, 0x0, x126); | |
uint64_t x130; | |
fiat_bls12_381_r_uint1 x131; | |
fiat_bls12_381_r_addcarryx_u64(&x130, &x131, x103, x128, 0x0); | |
uint64_t x132; | |
fiat_bls12_381_r_uint1 x133; | |
fiat_bls12_381_r_addcarryx_u64(&x132, &x133, x125, x130, x118); | |
uint64_t x134; | |
fiat_bls12_381_r_uint1 x135; | |
fiat_bls12_381_r_addcarryx_u64(&x134, &x135, x119, x107, 0x0); | |
uint64_t x136; | |
fiat_bls12_381_r_uint1 x137; | |
fiat_bls12_381_r_addcarryx_u64(&x136, &x137, x133, 0x0, x134); | |
uint64_t x138; | |
fiat_bls12_381_r_uint1 x139; | |
fiat_bls12_381_r_subborrowx_u64(&x138, &x139, 0x0, x122, UINT64_C(0xffffffff00000001)); | |
uint64_t x140; | |
fiat_bls12_381_r_uint1 x141; | |
fiat_bls12_381_r_subborrowx_u64(&x140, &x141, x139, x124, UINT64_C(0x53bda402fffe5bfe)); | |
uint64_t x142; | |
fiat_bls12_381_r_uint1 x143; | |
fiat_bls12_381_r_subborrowx_u64(&x142, &x143, x141, x132, UINT64_C(0x3339d80809a1d805)); | |
uint64_t x144; | |
fiat_bls12_381_r_uint1 x145; | |
fiat_bls12_381_r_subborrowx_u64(&x144, &x145, x143, x136, UINT64_C(0x73eda753299d7d48)); | |
uint64_t x146; | |
fiat_bls12_381_r_uint1 x147; | |
fiat_bls12_381_r_subborrowx_u64(&x146, &x147, x145, 0x0, 0x0); | |
uint64_t x148; | |
fiat_bls12_381_r_cmovznz_u64(&x148, x147, x138, x122); | |
uint64_t x149; | |
fiat_bls12_381_r_cmovznz_u64(&x149, x147, x140, x124); | |
uint64_t x150; | |
fiat_bls12_381_r_cmovznz_u64(&x150, x147, x142, x132); | |
uint64_t x151; | |
fiat_bls12_381_r_cmovznz_u64(&x151, x147, x144, x136); | |
out1[0] = x148; | |
out1[1] = x149; | |
out1[2] = x150; | |
out1[3] = x151; | |
} | |
/* | |
* The function fiat_bls12_381_r_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [0x0 ~> 0xffffffffffffffff] | |
*/ | |
static void fiat_bls12_381_r_nonzero(uint64_t* out1, const uint64_t arg1[4]) { | |
uint64_t x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | (uint64_t)0x0)))); | |
*out1 = x1; | |
} | |
/* | |
* The function fiat_bls12_381_r_selectznz is a multi-limb conditional select. | |
* Postconditions: | |
* eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) | |
* | |
* Input Bounds: | |
* arg1: [0x0 ~> 0x1] | |
* arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_selectznz(uint64_t out1[4], fiat_bls12_381_r_uint1 arg1, const uint64_t arg2[4], const uint64_t arg3[4]) { | |
uint64_t x1; | |
fiat_bls12_381_r_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0])); | |
uint64_t x2; | |
fiat_bls12_381_r_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1])); | |
uint64_t x3; | |
fiat_bls12_381_r_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2])); | |
uint64_t x4; | |
fiat_bls12_381_r_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3])); | |
out1[0] = x1; | |
out1[1] = x2; | |
out1[2] = x3; | |
out1[3] = x4; | |
} | |
/* | |
* The function fiat_bls12_381_r_to_bytes serializes a field element in the Montgomery domain to bytes in little-endian order. | |
* Preconditions: | |
* 0 ≤ eval arg1 < m | |
* Postconditions: | |
* out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] | |
* | |
* Input Bounds: | |
* arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x7fffffffffffffff]] | |
* Output Bounds: | |
* 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 ~> 0x7f]] | |
*/ | |
static void fiat_bls12_381_r_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { | |
uint64_t x1 = (arg1[3]); | |
uint64_t x2 = (arg1[2]); | |
uint64_t x3 = (arg1[1]); | |
uint64_t x4 = (arg1[0]); | |
uint64_t x5 = (x4 >> 8); | |
uint8_t x6 = (uint8_t)(x4 & UINT8_C(0xff)); | |
uint64_t x7 = (x5 >> 8); | |
uint8_t x8 = (uint8_t)(x5 & UINT8_C(0xff)); | |
uint64_t x9 = (x7 >> 8); | |
uint8_t x10 = (uint8_t)(x7 & UINT8_C(0xff)); | |
uint64_t x11 = (x9 >> 8); | |
uint8_t x12 = (uint8_t)(x9 & UINT8_C(0xff)); | |
uint64_t x13 = (x11 >> 8); | |
uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); | |
uint64_t x15 = (x13 >> 8); | |
uint8_t x16 = (uint8_t)(x13 & UINT8_C(0xff)); | |
uint8_t x17 = (uint8_t)(x15 >> 8); | |
uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); | |
uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); | |
uint64_t x20 = (x3 >> 8); | |
uint8_t x21 = (uint8_t)(x3 & UINT8_C(0xff)); | |
uint64_t x22 = (x20 >> 8); | |
uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); | |
uint64_t x24 = (x22 >> 8); | |
uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); | |
uint64_t x26 = (x24 >> 8); | |
uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); | |
uint64_t x28 = (x26 >> 8); | |
uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); | |
uint64_t x30 = (x28 >> 8); | |
uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); | |
uint8_t x32 = (uint8_t)(x30 >> 8); | |
uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); | |
uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); | |
uint64_t x35 = (x2 >> 8); | |
uint8_t x36 = (uint8_t)(x2 & UINT8_C(0xff)); | |
uint64_t x37 = (x35 >> 8); | |
uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); | |
uint64_t x39 = (x37 >> 8); | |
uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); | |
uint64_t x41 = (x39 >> 8); | |
uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); | |
uint64_t x43 = (x41 >> 8); | |
uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); | |
uint64_t x45 = (x43 >> 8); | |
uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); | |
uint8_t x47 = (uint8_t)(x45 >> 8); | |
uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); | |
uint8_t x49 = (uint8_t)(x47 & UINT8_C(0xff)); | |
uint64_t x50 = (x1 >> 8); | |
uint8_t x51 = (uint8_t)(x1 & UINT8_C(0xff)); | |
uint64_t x52 = (x50 >> 8); | |
uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); | |
uint64_t x54 = (x52 >> 8); | |
uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); | |
uint64_t x56 = (x54 >> 8); | |
uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); | |
uint64_t x58 = (x56 >> 8); | |
uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); | |
uint64_t x60 = (x58 >> 8); | |
uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); | |
uint8_t x62 = (uint8_t)(x60 >> 8); | |
uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); | |
out1[0] = x6; | |
out1[1] = x8; | |
out1[2] = x10; | |
out1[3] = x12; | |
out1[4] = x14; | |
out1[5] = x16; | |
out1[6] = x18; | |
out1[7] = x19; | |
out1[8] = x21; | |
out1[9] = x23; | |
out1[10] = x25; | |
out1[11] = x27; | |
out1[12] = x29; | |
out1[13] = x31; | |
out1[14] = x33; | |
out1[15] = x34; | |
out1[16] = x36; | |
out1[17] = x38; | |
out1[18] = x40; | |
out1[19] = x42; | |
out1[20] = x44; | |
out1[21] = x46; | |
out1[22] = x48; | |
out1[23] = x49; | |
out1[24] = x51; | |
out1[25] = x53; | |
out1[26] = x55; | |
out1[27] = x57; | |
out1[28] = x59; | |
out1[29] = x61; | |
out1[30] = x63; | |
out1[31] = x62; | |
} | |
/* | |
* The function fiat_bls12_381_r_from_bytes deserializes a field element in the Montgomery domain from bytes in little-endian order. | |
* Preconditions: | |
* 0 ≤ bytes_eval arg1 < m | |
* Postconditions: | |
* eval out1 mod m = bytes_eval arg1 mod m | |
* 0 ≤ eval out1 < m | |
* | |
* Input Bounds: | |
* 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 ~> 0x7f]] | |
* Output Bounds: | |
* out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x7fffffffffffffff]] | |
*/ | |
static void fiat_bls12_381_r_from_bytes(uint64_t out1[4], const uint8_t arg1[32]) { | |
uint64_t x1 = ((uint64_t)(arg1[31]) << 56); | |
uint64_t x2 = ((uint64_t)(arg1[30]) << 48); | |
uint64_t x3 = ((uint64_t)(arg1[29]) << 40); | |
uint64_t x4 = ((uint64_t)(arg1[28]) << 32); | |
uint64_t x5 = ((uint64_t)(arg1[27]) << 24); | |
uint64_t x6 = ((uint64_t)(arg1[26]) << 16); | |
uint64_t x7 = ((uint64_t)(arg1[25]) << 8); | |
uint8_t x8 = (arg1[24]); | |
uint64_t x9 = ((uint64_t)(arg1[23]) << 56); | |
uint64_t x10 = ((uint64_t)(arg1[22]) << 48); | |
uint64_t x11 = ((uint64_t)(arg1[21]) << 40); | |
uint64_t x12 = ((uint64_t)(arg1[20]) << 32); | |
uint64_t x13 = ((uint64_t)(arg1[19]) << 24); | |
uint64_t x14 = ((uint64_t)(arg1[18]) << 16); | |
uint64_t x15 = ((uint64_t)(arg1[17]) << 8); | |
uint8_t x16 = (arg1[16]); | |
uint64_t x17 = ((uint64_t)(arg1[15]) << 56); | |
uint64_t x18 = ((uint64_t)(arg1[14]) << 48); | |
uint64_t x19 = ((uint64_t)(arg1[13]) << 40); | |
uint64_t x20 = ((uint64_t)(arg1[12]) << 32); | |
uint64_t x21 = ((uint64_t)(arg1[11]) << 24); | |
uint64_t x22 = ((uint64_t)(arg1[10]) << 16); | |
uint64_t x23 = ((uint64_t)(arg1[9]) << 8); | |
uint8_t x24 = (arg1[8]); | |
uint64_t x25 = ((uint64_t)(arg1[7]) << 56); | |
uint64_t x26 = ((uint64_t)(arg1[6]) << 48); | |
uint64_t x27 = ((uint64_t)(arg1[5]) << 40); | |
uint64_t x28 = ((uint64_t)(arg1[4]) << 32); | |
uint64_t x29 = ((uint64_t)(arg1[3]) << 24); | |
uint64_t x30 = ((uint64_t)(arg1[2]) << 16); | |
uint64_t x31 = ((uint64_t)(arg1[1]) << 8); | |
uint8_t x32 = (arg1[0]); | |
uint64_t x33 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25))))))); | |
uint64_t x34 = (x33 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x35 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1))))))); | |
uint64_t x36 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9))))))); | |
uint64_t x37 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); | |
uint64_t x38 = (x37 & UINT64_C(0xffffffffffffffff)); | |
uint64_t x39 = (x36 & UINT64_C(0xffffffffffffffff)); | |
out1[0] = x34; | |
out1[1] = x38; | |
out1[2] = x39; | |
out1[3] = x35; | |
} | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env bash | |
# this should be run from the root directory of fiat-crypto, after building with, e.g., `make standalone` | |
# current files generated with fiat-crypto commit https://github.com/mit-plv/fiat-crypto/commit/a222d8ccbac386767427621affd46992acfb4d1c | |
time ./src/ExtractionOCaml/word_by_word_montgomery bls12_381_q 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab 64 > bls12_381_q_64.c | |
# | |
# real 0m15.631s | |
# user 0m15.372s | |
# sys 0m0.232s | |
time ./src/ExtractionOCaml/word_by_word_montgomery bls12_381_r 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001 64 > bls12_381_r_64.c | |
# | |
# real 0m3.411s | |
# user 0m3.180s | |
# sys 0m0.080s |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment