diff options
60 files changed, 65 insertions, 773 deletions
diff --git a/src/Specific/montgomery32_2e254m127x2e240m1/fenzDisplay.log b/src/Specific/montgomery32_2e254m127x2e240m1/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e254m127x2e240m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e254m127x2e240m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e255m19/fenzDisplay.log b/src/Specific/montgomery32_2e255m19/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e255m19/fenzDisplay.log +++ b/src/Specific/montgomery32_2e255m19/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e255m2e4m2e1m1/fenzDisplay.log b/src/Specific/montgomery32_2e255m2e4m2e1m1/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e255m2e4m2e1m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e255m2e4m2e1m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e255m765/fenzDisplay.log b/src/Specific/montgomery32_2e255m765/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e255m765/fenzDisplay.log +++ b/src/Specific/montgomery32_2e255m765/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e256m189/fenzDisplay.log b/src/Specific/montgomery32_2e256m189/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e256m189/fenzDisplay.log +++ b/src/Specific/montgomery32_2e256m189/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/fenzDisplay.log b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e256m2e32m977/fenzDisplay.log b/src/Specific/montgomery32_2e256m2e32m977/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e256m2e32m977/fenzDisplay.log +++ b/src/Specific/montgomery32_2e256m2e32m977/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e256m88x2e240m1/fenzDisplay.log b/src/Specific/montgomery32_2e256m88x2e240m1/fenzDisplay.log index 19fa61d18..c7c1c2df1 100644 --- a/src/Specific/montgomery32_2e256m88x2e240m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e256m88x2e240m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint32_t x21 = (x2 | x20); return x21) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e266m3/fenzDisplay.log b/src/Specific/montgomery32_2e266m3/fenzDisplay.log index a74ca7400..d8d43b40b 100644 --- a/src/Specific/montgomery32_2e266m3/fenzDisplay.log +++ b/src/Specific/montgomery32_2e266m3/fenzDisplay.log @@ -12,16 +12,4 @@ Interp-η uint32_t x24 = (x2 | x23); return x24) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e285m9/fenzDisplay.log b/src/Specific/montgomery32_2e285m9/fenzDisplay.log index a74ca7400..d8d43b40b 100644 --- a/src/Specific/montgomery32_2e285m9/fenzDisplay.log +++ b/src/Specific/montgomery32_2e285m9/fenzDisplay.log @@ -12,16 +12,4 @@ Interp-η uint32_t x24 = (x2 | x23); return x24) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e291m19/fenzDisplay.log b/src/Specific/montgomery32_2e291m19/fenzDisplay.log index 9bb66fdce..d57ef4050 100644 --- a/src/Specific/montgomery32_2e291m19/fenzDisplay.log +++ b/src/Specific/montgomery32_2e291m19/fenzDisplay.log @@ -13,16 +13,4 @@ Interp-η uint32_t x27 = (x2 | x26); return x27) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e321m9/fenzDisplay.log b/src/Specific/montgomery32_2e321m9/fenzDisplay.log index 0156012bf..4c54f68e5 100644 --- a/src/Specific/montgomery32_2e321m9/fenzDisplay.log +++ b/src/Specific/montgomery32_2e321m9/fenzDisplay.log @@ -14,16 +14,4 @@ Interp-η uint32_t x30 = (x2 | x29); return x30) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e322m2e161m1/fenzDisplay.log b/src/Specific/montgomery32_2e322m2e161m1/fenzDisplay.log index 0156012bf..4c54f68e5 100644 --- a/src/Specific/montgomery32_2e322m2e161m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e322m2e161m1/fenzDisplay.log @@ -14,16 +14,4 @@ Interp-η uint32_t x30 = (x2 | x29); return x30) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e336m17/fenzDisplay.log b/src/Specific/montgomery32_2e336m17/fenzDisplay.log index 0156012bf..4c54f68e5 100644 --- a/src/Specific/montgomery32_2e336m17/fenzDisplay.log +++ b/src/Specific/montgomery32_2e336m17/fenzDisplay.log @@ -14,16 +14,4 @@ Interp-η uint32_t x30 = (x2 | x29); return x30) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e336m3/fenzDisplay.log b/src/Specific/montgomery32_2e336m3/fenzDisplay.log index 0156012bf..4c54f68e5 100644 --- a/src/Specific/montgomery32_2e336m3/fenzDisplay.log +++ b/src/Specific/montgomery32_2e336m3/fenzDisplay.log @@ -14,16 +14,4 @@ Interp-η uint32_t x30 = (x2 | x29); return x30) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e338m15/fenzDisplay.log b/src/Specific/montgomery32_2e338m15/fenzDisplay.log index 0156012bf..4c54f68e5 100644 --- a/src/Specific/montgomery32_2e338m15/fenzDisplay.log +++ b/src/Specific/montgomery32_2e338m15/fenzDisplay.log @@ -14,16 +14,4 @@ Interp-η uint32_t x30 = (x2 | x29); return x30) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e369m25/fenzDisplay.log b/src/Specific/montgomery32_2e369m25/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e369m25/fenzDisplay.log +++ b/src/Specific/montgomery32_2e369m25/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e379m19/fenzDisplay.log b/src/Specific/montgomery32_2e379m19/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e379m19/fenzDisplay.log +++ b/src/Specific/montgomery32_2e379m19/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e382m105/fenzDisplay.log b/src/Specific/montgomery32_2e382m105/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e382m105/fenzDisplay.log +++ b/src/Specific/montgomery32_2e382m105/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e383m187/fenzDisplay.log b/src/Specific/montgomery32_2e383m187/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e383m187/fenzDisplay.log +++ b/src/Specific/montgomery32_2e383m187/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e383m31/fenzDisplay.log b/src/Specific/montgomery32_2e383m31/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e383m31/fenzDisplay.log +++ b/src/Specific/montgomery32_2e383m31/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e383m421/fenzDisplay.log b/src/Specific/montgomery32_2e383m421/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e383m421/fenzDisplay.log +++ b/src/Specific/montgomery32_2e383m421/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/fenzDisplay.log b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e384m317/fenzDisplay.log b/src/Specific/montgomery32_2e384m317/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e384m317/fenzDisplay.log +++ b/src/Specific/montgomery32_2e384m317/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e384m5x2e368m1/fenzDisplay.log b/src/Specific/montgomery32_2e384m5x2e368m1/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e384m5x2e368m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e384m5x2e368m1/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e384m79x2e376m1/fenzDisplay.log b/src/Specific/montgomery32_2e384m79x2e376m1/fenzDisplay.log index 2f8a0a630..7a5f016e0 100644 --- a/src/Specific/montgomery32_2e384m79x2e376m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e384m79x2e376m1/fenzDisplay.log @@ -15,16 +15,4 @@ Interp-η uint32_t x33 = (x2 | x32); return x33) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e389m21/fenzDisplay.log b/src/Specific/montgomery32_2e389m21/fenzDisplay.log index efcdedb96..be61ce3d7 100644 --- a/src/Specific/montgomery32_2e389m21/fenzDisplay.log +++ b/src/Specific/montgomery32_2e389m21/fenzDisplay.log @@ -16,16 +16,4 @@ Interp-η uint32_t x36 = (x2 | x35); return x36) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e401m31/fenzDisplay.log b/src/Specific/montgomery32_2e401m31/fenzDisplay.log index efcdedb96..be61ce3d7 100644 --- a/src/Specific/montgomery32_2e401m31/fenzDisplay.log +++ b/src/Specific/montgomery32_2e401m31/fenzDisplay.log @@ -16,16 +16,4 @@ Interp-η uint32_t x36 = (x2 | x35); return x36) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e413m21/fenzDisplay.log b/src/Specific/montgomery32_2e413m21/fenzDisplay.log index efcdedb96..be61ce3d7 100644 --- a/src/Specific/montgomery32_2e413m21/fenzDisplay.log +++ b/src/Specific/montgomery32_2e413m21/fenzDisplay.log @@ -16,16 +16,4 @@ Interp-η uint32_t x36 = (x2 | x35); return x36) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e414m17/fenzDisplay.log b/src/Specific/montgomery32_2e414m17/fenzDisplay.log index efcdedb96..be61ce3d7 100644 --- a/src/Specific/montgomery32_2e414m17/fenzDisplay.log +++ b/src/Specific/montgomery32_2e414m17/fenzDisplay.log @@ -16,16 +16,4 @@ Interp-η uint32_t x36 = (x2 | x35); return x36) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e416m2e208m1/fenzDisplay.log b/src/Specific/montgomery32_2e416m2e208m1/fenzDisplay.log index efcdedb96..be61ce3d7 100644 --- a/src/Specific/montgomery32_2e416m2e208m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e416m2e208m1/fenzDisplay.log @@ -16,16 +16,4 @@ Interp-η uint32_t x36 = (x2 | x35); return x36) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e444m17/fenzDisplay.log b/src/Specific/montgomery32_2e444m17/fenzDisplay.log index 0554fc66c..265fc8b8c 100644 --- a/src/Specific/montgomery32_2e444m17/fenzDisplay.log +++ b/src/Specific/montgomery32_2e444m17/fenzDisplay.log @@ -17,16 +17,4 @@ Interp-η uint32_t x39 = (x2 | x38); return x39) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e448m2e224m1/fenzDisplay.log b/src/Specific/montgomery32_2e448m2e224m1/fenzDisplay.log index 0554fc66c..265fc8b8c 100644 --- a/src/Specific/montgomery32_2e448m2e224m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e448m2e224m1/fenzDisplay.log @@ -17,16 +17,4 @@ Interp-η uint32_t x39 = (x2 | x38); return x39) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e450m2e225m1/fenzDisplay.log b/src/Specific/montgomery32_2e450m2e225m1/fenzDisplay.log index bca5777fd..8907c292b 100644 --- a/src/Specific/montgomery32_2e450m2e225m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e450m2e225m1/fenzDisplay.log @@ -18,16 +18,4 @@ Interp-η uint32_t x42 = (x2 | x41); return x42) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e452m3/fenzDisplay.log b/src/Specific/montgomery32_2e452m3/fenzDisplay.log index bca5777fd..8907c292b 100644 --- a/src/Specific/montgomery32_2e452m3/fenzDisplay.log +++ b/src/Specific/montgomery32_2e452m3/fenzDisplay.log @@ -18,16 +18,4 @@ Interp-η uint32_t x42 = (x2 | x41); return x42) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e468m17/fenzDisplay.log b/src/Specific/montgomery32_2e468m17/fenzDisplay.log index bca5777fd..8907c292b 100644 --- a/src/Specific/montgomery32_2e468m17/fenzDisplay.log +++ b/src/Specific/montgomery32_2e468m17/fenzDisplay.log @@ -18,16 +18,4 @@ Interp-η uint32_t x42 = (x2 | x41); return x42) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e480m2e240m1/fenzDisplay.log b/src/Specific/montgomery32_2e480m2e240m1/fenzDisplay.log index bca5777fd..8907c292b 100644 --- a/src/Specific/montgomery32_2e480m2e240m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e480m2e240m1/fenzDisplay.log @@ -18,16 +18,4 @@ Interp-η uint32_t x42 = (x2 | x41); return x42) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e488m17/fenzDisplay.log b/src/Specific/montgomery32_2e488m17/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e488m17/fenzDisplay.log +++ b/src/Specific/montgomery32_2e488m17/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e489m21/fenzDisplay.log b/src/Specific/montgomery32_2e489m21/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e489m21/fenzDisplay.log +++ b/src/Specific/montgomery32_2e489m21/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e495m31/fenzDisplay.log b/src/Specific/montgomery32_2e495m31/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e495m31/fenzDisplay.log +++ b/src/Specific/montgomery32_2e495m31/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e510m290x2e496m1/fenzDisplay.log b/src/Specific/montgomery32_2e510m290x2e496m1/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e510m290x2e496m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e510m290x2e496m1/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e511m187/fenzDisplay.log b/src/Specific/montgomery32_2e511m187/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e511m187/fenzDisplay.log +++ b/src/Specific/montgomery32_2e511m187/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e511m481/fenzDisplay.log b/src/Specific/montgomery32_2e511m481/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e511m481/fenzDisplay.log +++ b/src/Specific/montgomery32_2e511m481/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log b/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e512m491x2e496m1/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e512m569/fenzDisplay.log b/src/Specific/montgomery32_2e512m569/fenzDisplay.log index 73c0717f8..eb0b6ea33 100644 --- a/src/Specific/montgomery32_2e512m569/fenzDisplay.log +++ b/src/Specific/montgomery32_2e512m569/fenzDisplay.log @@ -19,16 +19,4 @@ Interp-η uint32_t x45 = (x2 | x44); return x45) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery32_2e521m1/fenzDisplay.log b/src/Specific/montgomery32_2e521m1/fenzDisplay.log index 03f3fcc25..47cc8d6b2 100644 --- a/src/Specific/montgomery32_2e521m1/fenzDisplay.log +++ b/src/Specific/montgomery32_2e521m1/fenzDisplay.log @@ -20,16 +20,4 @@ Interp-η uint32_t x48 = (x2 | x47); return x48) x - : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 5 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType uint32_t diff --git a/src/Specific/montgomery64_2e383m421/femulDisplay.log b/src/Specific/montgomery64_2e383m421/femulDisplay.log index 99137180d..26534e3aa 100644 --- a/src/Specific/montgomery64_2e383m421/femulDisplay.log +++ b/src/Specific/montgomery64_2e383m421/femulDisplay.log @@ -14,7 +14,7 @@ Interp-η uint64_t x52, uint8_t x53 = addcarryx_u64(x50, x35, x37); uint64_t x55, uint8_t x56 = addcarryx_u64(x53, x38, x40); uint64_t x58, uint8_t _ = addcarryx_u64(0x0, x56, x41); - uint64_t x61, uint64_t _ = mulx_u64(x25, Const 14897608040525528621); + uint64_t x61, uint64_t _ = mulx_u64(x25, 0xcebeef94fa86fe2dL); uint64_t x64, uint64_t x65 = mulx_u64(x61, 0xfffffffffffffe5bL); uint64_t x67, uint64_t x68 = mulx_u64(x61, 0xffffffffffffffffL); uint64_t x70, uint64_t x71 = mulx_u64(x61, 0xffffffffffffffffL); @@ -53,7 +53,7 @@ Interp-η uint64_t x169, uint8_t x170 = addcarryx_u64(x167, x115, x148); uint64_t x172, uint8_t x173 = addcarryx_u64(x170, x118, x151); uint64_t x175, uint8_t x176 = addcarryx_u64(x173, x119, x154); - uint64_t x178, uint64_t _ = mulx_u64(x157, Const 14897608040525528621); + uint64_t x178, uint64_t _ = mulx_u64(x157, 0xcebeef94fa86fe2dL); uint64_t x181, uint64_t x182 = mulx_u64(x178, 0xfffffffffffffe5bL); uint64_t x184, uint64_t x185 = mulx_u64(x178, 0xffffffffffffffffL); uint64_t x187, uint64_t x188 = mulx_u64(x178, 0xffffffffffffffffL); @@ -93,7 +93,7 @@ Interp-η uint64_t x287, uint8_t x288 = addcarryx_u64(x285, x232, x266); uint64_t x290, uint8_t x291 = addcarryx_u64(x288, x235, x269); uint64_t x293, uint8_t x294 = addcarryx_u64(x291, x237, x272); - uint64_t x296, uint64_t _ = mulx_u64(x275, Const 14897608040525528621); + uint64_t x296, uint64_t _ = mulx_u64(x275, 0xcebeef94fa86fe2dL); uint64_t x299, uint64_t x300 = mulx_u64(x296, 0xfffffffffffffe5bL); uint64_t x302, uint64_t x303 = mulx_u64(x296, 0xffffffffffffffffL); uint64_t x305, uint64_t x306 = mulx_u64(x296, 0xffffffffffffffffL); @@ -133,7 +133,7 @@ Interp-η uint64_t x405, uint8_t x406 = addcarryx_u64(x403, x350, x384); uint64_t x408, uint8_t x409 = addcarryx_u64(x406, x353, x387); uint64_t x411, uint8_t x412 = addcarryx_u64(x409, x355, x390); - uint64_t x414, uint64_t _ = mulx_u64(x393, Const 14897608040525528621); + uint64_t x414, uint64_t _ = mulx_u64(x393, 0xcebeef94fa86fe2dL); uint64_t x417, uint64_t x418 = mulx_u64(x414, 0xfffffffffffffe5bL); uint64_t x420, uint64_t x421 = mulx_u64(x414, 0xffffffffffffffffL); uint64_t x423, uint64_t x424 = mulx_u64(x414, 0xffffffffffffffffL); @@ -173,7 +173,7 @@ Interp-η uint64_t x523, uint8_t x524 = addcarryx_u64(x521, x468, x502); uint64_t x526, uint8_t x527 = addcarryx_u64(x524, x471, x505); uint64_t x529, uint8_t x530 = addcarryx_u64(x527, x473, x508); - uint64_t x532, uint64_t _ = mulx_u64(x511, Const 14897608040525528621); + uint64_t x532, uint64_t _ = mulx_u64(x511, 0xcebeef94fa86fe2dL); uint64_t x535, uint64_t x536 = mulx_u64(x532, 0xfffffffffffffe5bL); uint64_t x538, uint64_t x539 = mulx_u64(x532, 0xffffffffffffffffL); uint64_t x541, uint64_t x542 = mulx_u64(x532, 0xffffffffffffffffL); @@ -213,7 +213,7 @@ Interp-η uint64_t x641, uint8_t x642 = addcarryx_u64(x639, x586, x620); uint64_t x644, uint8_t x645 = addcarryx_u64(x642, x589, x623); uint64_t x647, uint8_t x648 = addcarryx_u64(x645, x591, x626); - uint64_t x650, uint64_t _ = mulx_u64(x629, Const 14897608040525528621); + uint64_t x650, uint64_t _ = mulx_u64(x629, 0xcebeef94fa86fe2dL); uint64_t x653, uint64_t x654 = mulx_u64(x650, 0xfffffffffffffe5bL); uint64_t x656, uint64_t x657 = mulx_u64(x650, 0xffffffffffffffffL); uint64_t x659, uint64_t x660 = mulx_u64(x650, 0xffffffffffffffffL); diff --git a/src/Specific/montgomery64_2e450m2e225m1/fenzDisplay.log b/src/Specific/montgomery64_2e450m2e225m1/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e450m2e225m1/fenzDisplay.log +++ b/src/Specific/montgomery64_2e450m2e225m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e452m3/fenzDisplay.log b/src/Specific/montgomery64_2e452m3/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e452m3/fenzDisplay.log +++ b/src/Specific/montgomery64_2e452m3/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e468m17/fenzDisplay.log b/src/Specific/montgomery64_2e468m17/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e468m17/fenzDisplay.log +++ b/src/Specific/montgomery64_2e468m17/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e480m2e240m1/fenzDisplay.log b/src/Specific/montgomery64_2e480m2e240m1/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e480m2e240m1/fenzDisplay.log +++ b/src/Specific/montgomery64_2e480m2e240m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e488m17/fenzDisplay.log b/src/Specific/montgomery64_2e488m17/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e488m17/fenzDisplay.log +++ b/src/Specific/montgomery64_2e488m17/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e489m21/fenzDisplay.log b/src/Specific/montgomery64_2e489m21/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e489m21/fenzDisplay.log +++ b/src/Specific/montgomery64_2e489m21/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e495m31/fenzDisplay.log b/src/Specific/montgomery64_2e495m31/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e495m31/fenzDisplay.log +++ b/src/Specific/montgomery64_2e495m31/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e510m290x2e496m1/fenzDisplay.log b/src/Specific/montgomery64_2e510m290x2e496m1/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e510m290x2e496m1/fenzDisplay.log +++ b/src/Specific/montgomery64_2e510m290x2e496m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e511m187/fenzDisplay.log b/src/Specific/montgomery64_2e511m187/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e511m187/fenzDisplay.log +++ b/src/Specific/montgomery64_2e511m187/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e511m481/fenzDisplay.log b/src/Specific/montgomery64_2e511m481/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e511m481/fenzDisplay.log +++ b/src/Specific/montgomery64_2e511m481/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e512m491x2e496m1/fenzDisplay.log b/src/Specific/montgomery64_2e512m491x2e496m1/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e512m491x2e496m1/fenzDisplay.log +++ b/src/Specific/montgomery64_2e512m491x2e496m1/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e512m569/fenzDisplay.log b/src/Specific/montgomery64_2e512m569/fenzDisplay.log index 7ecc26851..a05fc22ab 100644 --- a/src/Specific/montgomery64_2e512m569/fenzDisplay.log +++ b/src/Specific/montgomery64_2e512m569/fenzDisplay.log @@ -11,16 +11,4 @@ Interp-η uint64_t x21 = (x2 | x20); return x21) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/montgomery64_2e521m1/fenzDisplay.log b/src/Specific/montgomery64_2e521m1/fenzDisplay.log index 49e873cbd..d4727163e 100644 --- a/src/Specific/montgomery64_2e521m1/fenzDisplay.log +++ b/src/Specific/montgomery64_2e521m1/fenzDisplay.log @@ -12,16 +12,4 @@ Interp-η uint64_t x24 = (x2 | x23); return x24) x - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in - lower) with - | 0%Z => Eq - | Z.pos _ => Lt - | Z.neg _ => Gt - end with - | Eq => true - | Lt => true - | Gt => false - end then Some 6 else None) with - | Some lgsz => Syntax.TWord lgsz - | None => Syntax.TZ - end) + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType uint64_t |