./copy_bounds

36 files changed, 144 insertions, 0 deletions

diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..c660ee7ec
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..7d88c2a6d
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..068ab659e
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..e01da5b9a
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..eacf666a4
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..67f57ed42
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..3721cfa71
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..e9819e147
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..357921f6f
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..40196eed3
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..74541b3a5
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..5b5740fc3
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..ba6c45088
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..55d7ad833
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..9985b1278
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..60d6c0388
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..d8ee19fd4
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..8600068c6
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..8ebe500fd
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..675d9b7fa
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..209d0eedb
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..b9f31f4ac
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..3e3e7e878
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..19253200b
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..fa19e88c0
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..57b1e5e15
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..4d4666dee
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..bd85dba88
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..5f820de6c
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF41417_32Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..c94de07bd
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/AddDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddDisplay.v
new file mode 100644
index 000000000..5ecbc061e
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/AddJavaDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddJavaDisplay.v
new file mode 100644
index 000000000..e01c1dbfb
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Add.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print raddW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepDisplay.v
new file mode 100644
index 000000000..9dd11cbcc
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepJavaDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepJavaDisplay.v
new file mode 100644
index 000000000..8c01dd87d
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStepJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.LadderStep.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rladderstepW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/MulDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/MulDisplay.v
new file mode 100644
index 000000000..43f08dbbb
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/MulDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.CNotations.
+
+Print rmulW.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/MulJavaDisplay.v b/src/SpecificGen/GF5211_32Reflective/Reified/MulJavaDisplay.v
new file mode 100644
index 000000000..8ca5b4c0c
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/MulJavaDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.Mul.
+Require Export Crypto.Reflection.Z.JavaNotations.
+
+Print rmulW.