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 27, 2020
1 parent ea15d52 commit 71a03a6
Show file tree
Hide file tree
Showing 28 changed files with 232 additions and 232 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
Loading

0 comments on commit 71a03a6

Please sign in to comment.