Skip to content

Commit

Permalink
Use tighter loose bounds
Browse files Browse the repository at this point in the history 
We now compute the loose bounds to be as tight as possible given the
tight bounds: they are the tightest bounds that will let us add two
tightly-bounded field elements, and will also let us subtract two
tightly-bounded field elements (with balance), without needing to carry.

This is probably required for having 32-bit p448 work, but even with
this, p448 is still not working; see
#797.  Seems worth merging
anyway.
  • Loading branch information
@JasonGross
JasonGross committed May 21, 2020
1 parent 9ac37a1 commit e47f7bb
Show file tree
Hide file tree
Showing 32 changed files with 277 additions and 264 deletions.
16 changes: 8 additions & 8 deletions fiat-bedrock2/src/curve25519_32.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@

/*
* Input Bounds:
* in0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* in1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* in0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
* in1: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
* Output Bounds:
* out0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
*/
Expand Down Expand Up @@ -713,7 +713,7 @@ void fiat_25519_carry_mul(uintptr_t in0, uintptr_t in1, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* in0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
* Output Bounds:
* out0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
*/
Expand Down Expand Up @@ -1188,7 +1188,7 @@ void fiat_25519_carry_square(uintptr_t in0, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* in0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
* Output Bounds:
* out0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
*/
Expand Down Expand Up @@ -1259,7 +1259,7 @@ void fiat_25519_carry(uintptr_t in0, uintptr_t out0) {
* in0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
* in1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
* Output Bounds:
* out0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* out0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
*/
void fiat_25519_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x10, x1, x11, x2, x12, x3, x13, x4, x14, x5, x15, x6, x16, x7, x17, x8, x18, x9, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39;
Expand Down Expand Up @@ -1327,7 +1327,7 @@ void fiat_25519_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* in0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
* in1: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
* Output Bounds:
* out0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* out0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
*/
void fiat_25519_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x10, x1, x11, x2, x12, x3, x13, x4, x14, x5, x15, x6, x16, x7, x17, x8, x18, x9, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39;
Expand Down Expand Up @@ -1394,7 +1394,7 @@ void fiat_25519_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* Input Bounds:
* in0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
* Output Bounds:
* out0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* out0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
*/
void fiat_25519_opp(uintptr_t in0, uintptr_t out0) {
uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29;
Expand Down Expand Up @@ -1973,7 +1973,7 @@ void fiat_25519_from_bytes(uintptr_t in0, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]]
* in0: [[0x0 ~> 0xc666640], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331], [0x0 ~> 0xc666664], [0x0 ~> 0x6333331]]
* Output Bounds:
* out0: [[0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333], [0x0 ~> 0x4666666], [0x0 ~> 0x2333333]]
*/
Expand Down
16 changes: 8 additions & 8 deletions fiat-bedrock2/src/curve25519_64.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@

/*
* Input Bounds:
* in0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* in1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* in0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
* in1: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
* Output Bounds:
* out0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
*/
Expand Down Expand Up @@ -214,7 +214,7 @@ void fiat_25519_carry_mul(uintptr_t in0, uintptr_t in1, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* in0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
* Output Bounds:
* out0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
*/
Expand Down Expand Up @@ -353,7 +353,7 @@ void fiat_25519_carry_square(uintptr_t in0, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* in0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
* Output Bounds:
* out0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
*/
Expand Down Expand Up @@ -399,7 +399,7 @@ void fiat_25519_carry(uintptr_t in0, uintptr_t out0) {
* in0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
* in1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
* Output Bounds:
* out0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* out0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
*/
void fiat_25519_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x5, x1, x6, x2, x7, x3, x8, x4, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19;
Expand Down Expand Up @@ -442,7 +442,7 @@ void fiat_25519_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* in0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
* in1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
* Output Bounds:
* out0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* out0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
*/
void fiat_25519_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x5, x1, x6, x2, x7, x3, x8, x4, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19;
Expand Down Expand Up @@ -484,7 +484,7 @@ void fiat_25519_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* Input Bounds:
* in0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
* Output Bounds:
* out0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* out0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
*/
void fiat_25519_opp(uintptr_t in0, uintptr_t out0) {
uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14;
Expand Down Expand Up @@ -898,7 +898,7 @@ void fiat_25519_from_bytes(uintptr_t in0, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
* in0: [[0x0 ~> 0x18cccccccccca6], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca], [0x0 ~> 0x18ccccccccccca]]
* Output Bounds:
* out0: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
*/
Expand Down
14 changes: 7 additions & 7 deletions fiat-bedrock2/src/p448_solinas_64.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@

/*
* Input Bounds:
* in0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* in1: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* in0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
* in1: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
* Output Bounds:
* out0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
*/
Expand Down Expand Up @@ -674,7 +674,7 @@ void fiat_p448_carry_mul(uintptr_t in0, uintptr_t in1, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* in0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
* Output Bounds:
* out0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
*/
Expand Down Expand Up @@ -1091,7 +1091,7 @@ void fiat_p448_carry_square(uintptr_t in0, uintptr_t out0) {

/*
* Input Bounds:
* in0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* in0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
* Output Bounds:
* out0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
*/
Expand Down Expand Up @@ -1156,7 +1156,7 @@ void fiat_p448_carry(uintptr_t in0, uintptr_t out0) {
* in0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
* in1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
* Output Bounds:
* out0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* out0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
*/
void fiat_p448_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x8, x1, x9, x2, x10, x3, x11, x4, x12, x5, x13, x6, x14, x7, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31;
Expand Down Expand Up @@ -1214,7 +1214,7 @@ void fiat_p448_add(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* in0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
* in1: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
* Output Bounds:
* out0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* out0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
*/
void fiat_p448_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
uintptr_t x0, x8, x1, x9, x2, x10, x3, x11, x4, x12, x5, x13, x6, x14, x7, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31;
Expand Down Expand Up @@ -1271,7 +1271,7 @@ void fiat_p448_sub(uintptr_t in0, uintptr_t in1, uintptr_t out0) {
* Input Bounds:
* in0: [[0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999], [0x0 ~> 0x119999999999999]]
* Output Bounds:
* out0: [[0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb], [0x0 ~> 0x34ccccccccccccb]]
* out0: [[0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999995], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997], [0x0 ~> 0x319999999999997]]
*/
void fiat_p448_opp(uintptr_t in0, uintptr_t out0) {
uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23;
Expand Down

0 comments on commit e47f7bb

Please sign in to comment.