Add some constants from montgomery

2 files changed, 32 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index db2871f98..962c9a3a8 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -34,6 +34,7 @@ nums = tuple(list(range(128)) + [
     262139,
     262143,
     523807,
+    524101,
     524263,
     524269,
     524271,
@@ -96,6 +97,8 @@ nums = tuple(list(range(128)) + [
     536870911,
     1073741822,
     1073741823,
+    4294967107,
+    4294967294,
     4294967295,
     8589934559,
     8589934567,
@@ -180,6 +183,7 @@ nums = tuple(list(range(128)) + [
     72057594037927935,
     72057594037927936,
     18446744069414584321,
+    18446744073709551614,
     18446744073709551615,
     18446744073709551616,
     38685626227668133590597631,
@@ -535,6 +539,8 @@ Notation "'0b111111111111111111'" (* 262143 (0x3ffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111111000011111'" (* 523807 (0x7fe1f) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
+Notation "'0b1111111111101000101'" (* 524101 (0x7ff45) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1).
 Notation "'0b1111111111111100111'" (* 524263 (0x7ffe7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
 Notation "'0b1111111111111101101'" (* 524269 (0x7ffed) *)
@@ -659,6 +665,10 @@ Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b111111111111111111111111111111'" (* 1073741823 (0x3fffffff) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111111111111111101000011'" (* 4294967107 (0xffffff43) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1).
+Notation "'0b11111111111111111111111111111110'" (* 4294967294 (0xfffffffe) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111'" (* 4294967295 (0xffffffff) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111111111111111111011111'" (* 8589934559 (0x1ffffffdf) *)
@@ -827,6 +837,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000000000'" (* 7205
   := (Const WO~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b1111111111111111111111111111111100000000000000000000000000000001'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111111111110'" (* 18446744073709551614 (0xfffffffffffffffeL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111111111111111111111111111111'" (* 18446744073709551615 (0xffffffffffffffffL) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b10000000000000000000000000000000000000000000000000000000000000000'" (* 18446744073709551616 (0x10000000000000000L) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 1301dc6ac..d76adca88 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -34,6 +34,7 @@ nums = tuple(list(range(128)) + [
     262139,
     262143,
     523807,
+    524101,
     524263,
     524269,
     524271,
@@ -96,6 +97,8 @@ nums = tuple(list(range(128)) + [
     536870911,
     1073741822,
     1073741823,
+    4294967107,
+    4294967294,
     4294967295,
     8589934559,
     8589934567,
@@ -180,6 +183,7 @@ nums = tuple(list(range(128)) + [
     72057594037927935,
     72057594037927936,
     18446744069414584321,
+    18446744073709551614,
     18446744073709551615,
     18446744073709551616,
     38685626227668133590597631,
@@ -835,6 +839,10 @@ Notation "'0x7fe1f'" (* 523807 (0x7fe1f) *)
   := (Const 523807%Z).
 Notation "'0x7fe1f'" (* 523807 (0x7fe1f) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
+Notation "'0x7ff45'" (* 524101 (0x7ff45) *)
+  := (Const 524101%Z).
+Notation "'0x7ff45'" (* 524101 (0x7ff45) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1).
 Notation "'0x7ffe7'" (* 524263 (0x7ffe7) *)
   := (Const 524263%Z).
 Notation "'0x7ffe7'" (* 524263 (0x7ffe7) *)
@@ -1083,6 +1091,14 @@ Notation "'0x3fffffff'" (* 1073741823 (0x3fffffff) *)
   := (Const 1073741823%Z).
 Notation "'0x3fffffff'" (* 1073741823 (0x3fffffff) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
+  := (Const 4294967107%Z).
+Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1).
+Notation "'0xfffffffe'" (* 4294967294 (0xfffffffe) *)
+  := (Const 4294967294%Z).
+Notation "'0xfffffffe'" (* 4294967294 (0xfffffffe) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xffffffff'" (* 4294967295 (0xffffffff) *)
   := (Const 4294967295%Z).
 Notation "'0xffffffff'" (* 4294967295 (0xffffffff) *)
@@ -1419,6 +1435,10 @@ Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *
   := (Const 18446744069414584321%Z).
 Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffffffffffffffeL'" (* 18446744073709551614 (0xfffffffffffffffeL) *)
+  := (Const 18446744073709551614%Z).
+Notation "'0xfffffffffffffffeL'" (* 18446744073709551614 (0xfffffffffffffffeL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xffffffffffffffffL'" (* 18446744073709551615 (0xffffffffffffffffL) *)
   := (Const 18446744073709551615%Z).
 Notation "'0xffffffffffffffffL'" (* 18446744073709551615 (0xffffffffffffffffL) *)