Switch to bounded Z

We don't have working word code yet, because the reification code currently
does spurious word->N->Z->N->word conversions everywhere.  So we use Z instead.

1 files changed, 14 insertions, 14 deletions

diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v
index 8d21b8afe..3866b3b22 100644
--- a/src/Assembly/GF25519BoundedInstantiation.v
+++ b/src/Assembly/GF25519BoundedInstantiation.v
@@ -5,7 +5,7 @@ Require Import Crypto.Assembly.Compile.
 Require Import Crypto.Assembly.LL.
 Require Import Crypto.Assembly.GF25519.
 Require Import Crypto.Specific.GF25519.
-Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Import Crypto.Specific.GF25519BoundedCommonWord.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tuple.
@@ -41,13 +41,13 @@ Section Operations.
   Definition ropp : ExprUnOp := Opp.wordProg.
 End Operations.
 
-Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := interp_bexpr'.
-Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := interp_uexpr'.
-Axiom interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64.
-Axiom interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW.
-Axiom interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W.
+Axiom interp_uexpr_FEToZ : ExprUnOpFEToZ -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64.
+Axiom interp_uexpr_FEToWire : ExprUnOpFEToWire -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW.
+Axiom interp_uexpr_WireToFE : ExprUnOpWireToFE -> Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W.
 Axiom rfreeze : ExprUnOp.
 Axiom rge_modulus : ExprUnOpFEToZ.
 Axiom rpack : ExprUnOpFEToWire.
@@ -67,34 +67,34 @@ Declare Reduction asm_interp
             Evaluables.ezero Evaluables.toT Evaluables.fromT Evaluables.eadd Evaluables.esub Evaluables.emul Evaluables.eshiftr Evaluables.eand Evaluables.eltb Evaluables.eeqb
             Evaluables.WordEvaluable Evaluables.ZEvaluable].
 
-Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_radd : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_bexpr radd.
 Print interp_radd.
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
-Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_rsub : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_bexpr rsub.
 (*Print interp_rsub.*)
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
-Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_rmul : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_bexpr rmul.
 (*Print interp_rmul.*)
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
-Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_ropp : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_uexpr ropp.
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
-Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_rfreeze : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_uexpr rfreeze.
 Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
 
-Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
+Definition interp_rge_modulus : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64
   := Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
 Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
 
-Definition interp_rpack : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
+Definition interp_rpack : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.wire_digitsW
   := Eval asm_interp in interp_uexpr_FEToWire rpack.
 Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
 
-Definition interp_runpack : Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
+Definition interp_runpack : Specific.GF25519BoundedCommonWord.wire_digitsW -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_uexpr_WireToFE runpack.
 Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.