Add SpecificGen/GF*

For bounds analysis

11 files changed, 172 insertions, 0 deletions

diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Add.v b/src/SpecificGen/GF2213_32Reflective/Reified/Add.v
new file mode 100644
index 000000000..d278a8f26
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Add.v
@@ -0,0 +1,12 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+
+Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined.
+Definition raddW := Eval vm_compute in rword_of_Z raddZ_sig.
+Lemma raddW_correct_and_bounded_gen : correct_and_bounded_genT raddW raddZ_sig.
+Proof. rexpr_correct. Qed.
+Definition radd_output_bounds := Eval vm_compute in compute_bounds raddW ExprBinOp_bounds.
+
+Local Open Scope string_scope.
+Compute ("Add", compute_bounds_for_display raddW ExprBinOp_bounds).
+Compute ("Add overflows? ", sanity_compute raddW ExprBinOp_bounds).
+Compute ("Add overflows (error if it does)? ", sanity_check raddW ExprBinOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/CarryAdd.v b/src/SpecificGen/GF2213_32Reflective/Reified/CarryAdd.v
new file mode 100644
index 000000000..516a36bf5
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/CarryAdd.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+
+Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined.
+Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig.
+Lemma rcarry_addW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_addW rcarry_addZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rcarry_add_output_bounds := Eval vm_compute in compute_bounds rcarry_addW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_addW_correct_and_bounded
+  := ExprBinOp_correct_and_bounded
+       rcarry_addW carry_add rcarry_addZ_sig rcarry_addW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds).
+Compute ("Carry_Add overflows? ", sanity_compute rcarry_addW ExprBinOp_bounds).
+Compute ("Carry_Add overflows (error if it does)? ", sanity_check rcarry_addW ExprBinOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/CarryOpp.v b/src/SpecificGen/GF2213_32Reflective/Reified/CarryOpp.v
new file mode 100644
index 000000000..a2ab83ce2
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/CarryOpp.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOp.
+
+Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined.
+Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig.
+Lemma rcarry_oppW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_oppW rcarry_oppZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rcarry_opp_output_bounds := Eval vm_compute in compute_bounds rcarry_oppW ExprUnOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_oppW_correct_and_bounded
+  := ExprUnOp_correct_and_bounded
+       rcarry_oppW carry_opp rcarry_oppZ_sig rcarry_oppW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Carry_Opp", compute_bounds_for_display rcarry_oppW ExprUnOp_bounds).
+Compute ("Carry_Opp overflows? ", sanity_compute rcarry_oppW ExprUnOp_bounds).
+Compute ("Carry_Opp overflows (error if it does)? ", sanity_check rcarry_oppW ExprUnOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/CarrySub.v b/src/SpecificGen/GF2213_32Reflective/Reified/CarrySub.v
new file mode 100644
index 000000000..04a097dd7
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/CarrySub.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+
+Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined.
+Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig.
+Lemma rcarry_subW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_subW rcarry_subZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_subW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_subW_correct_and_bounded
+  := ExprBinOp_correct_and_bounded
+       rcarry_subW carry_sub rcarry_subZ_sig rcarry_subW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds).
+Compute ("Carry_Sub overflows? ", sanity_compute rcarry_subW ExprBinOp_bounds).
+Compute ("Carry_Sub overflows (error if it does)? ", sanity_check rcarry_subW ExprBinOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/GeModulus.v b/src/SpecificGen/GF2213_32Reflective/Reified/GeModulus.v
new file mode 100644
index 000000000..659e712d9
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/GeModulus.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOpFEToZ.
+
+Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined.
+Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig.
+Lemma rge_modulusW_correct_and_bounded_gen : correct_and_bounded_genT rge_modulusW rge_modulusZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rge_modulus_output_bounds := Eval vm_compute in compute_bounds rge_modulusW ExprUnOpFEToZ_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rge_modulusW_correct_and_bounded
+  := ExprUnOpFEToZ_correct_and_bounded
+       rge_modulusW ge_modulus rge_modulusZ_sig rge_modulusW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Ge_Modulus", compute_bounds_for_display rge_modulusW ExprUnOpFEToZ_bounds).
+Compute ("Ge_Modulus overflows? ", sanity_compute rge_modulusW ExprUnOpFEToZ_bounds).
+Compute ("Ge_Modulus overflows (error if it does)? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Mul.v b/src/SpecificGen/GF2213_32Reflective/Reified/Mul.v
new file mode 100644
index 000000000..08c235a9c
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Mul.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+
+Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined.
+Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig.
+Lemma rmulW_correct_and_bounded_gen : correct_and_bounded_genT rmulW rmulZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rmul_output_bounds := Eval vm_compute in compute_bounds rmulW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rmulW_correct_and_bounded
+  := ExprBinOp_correct_and_bounded
+       rmulW mul rmulZ_sig rmulW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds).
+Compute ("Mul overflows? ", sanity_compute rmulW ExprBinOp_bounds).
+Compute ("Mul overflows (error if it does)? ", sanity_check rmulW ExprBinOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Opp.v b/src/SpecificGen/GF2213_32Reflective/Reified/Opp.v
new file mode 100644
index 000000000..091cb96de
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Opp.v
@@ -0,0 +1,12 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOp.
+
+Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined.
+Definition roppW := Eval vm_compute in rword_of_Z roppZ_sig.
+Lemma roppW_correct_and_bounded_gen : correct_and_bounded_genT roppW roppZ_sig.
+Proof. rexpr_correct. Qed.
+Definition ropp_output_bounds := Eval vm_compute in compute_bounds roppW ExprUnOp_bounds.
+
+Local Open Scope string_scope.
+Compute ("Opp", compute_bounds_for_display roppW ExprUnOp_bounds).
+Compute ("Opp overflows? ", sanity_compute roppW ExprUnOp_bounds).
+Compute ("Opp overflows (error if it does)? ", sanity_check roppW ExprUnOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Pack.v b/src/SpecificGen/GF2213_32Reflective/Reified/Pack.v
new file mode 100644
index 000000000..f96f81a53
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Pack.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOpFEToWire.
+
+Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined.
+Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig.
+Lemma rpackW_correct_and_bounded_gen : correct_and_bounded_genT rpackW rpackZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rpack_output_bounds := Eval vm_compute in compute_bounds rpackW ExprUnOpFEToWire_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rpackW_correct_and_bounded
+  := ExprUnOpFEToWire_correct_and_bounded
+       rpackW pack rpackZ_sig rpackW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds).
+Compute ("Pack overflows? ", sanity_compute rpackW ExprUnOpFEToWire_bounds).
+Compute ("Pack overflows (error if it does)? ", sanity_check rpackW ExprUnOpFEToWire_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/PreFreeze.v b/src/SpecificGen/GF2213_32Reflective/Reified/PreFreeze.v
new file mode 100644
index 000000000..60ab908b0
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/PreFreeze.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOp.
+
+Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. cbv [prefreeze GF2213_32.prefreeze]. reify_sig. Defined.
+Definition rprefreezeW := Eval vm_compute in rword_of_Z rprefreezeZ_sig.
+Lemma rprefreezeW_correct_and_bounded_gen : correct_and_bounded_genT rprefreezeW rprefreezeZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rprefreeze_output_bounds := Eval vm_compute in compute_bounds rprefreezeW ExprUnOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rprefreezeW_correct_and_bounded
+  := ExprUnOp_correct_and_bounded
+       rprefreezeW prefreeze rprefreezeZ_sig rprefreezeW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("PreFreeze", compute_bounds_for_display rprefreezeW ExprUnOp_bounds).
+Compute ("PreFreeze overflows? ", sanity_compute rprefreezeW ExprUnOp_bounds).
+Compute ("PreFreeze overflows (error if it does)? ", sanity_check rprefreezeW ExprUnOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Sub.v b/src/SpecificGen/GF2213_32Reflective/Reified/Sub.v
new file mode 100644
index 000000000..cc7ba69dd
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Sub.v
@@ -0,0 +1,12 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonBinOp.
+
+Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined.
+Definition rsubW := Eval vm_compute in rword_of_Z rsubZ_sig.
+Lemma rsubW_correct_and_bounded_gen : correct_and_bounded_genT rsubW rsubZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rsub_output_bounds := Eval vm_compute in compute_bounds rsubW ExprBinOp_bounds.
+
+Local Open Scope string_scope.
+Compute ("Sub", compute_bounds_for_display rsubW ExprBinOp_bounds).
+Compute ("Sub overflows? ", sanity_compute rsubW ExprBinOp_bounds).
+Compute ("Sub overflows (error if it does)? ", sanity_check rsubW ExprBinOp_bounds).
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/Unpack.v b/src/SpecificGen/GF2213_32Reflective/Reified/Unpack.v
new file mode 100644
index 000000000..5ef4ff3d8
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/Unpack.v
@@ -0,0 +1,17 @@
+Require Import Crypto.SpecificGen.GF2213_32Reflective.CommonUnOpWireToFE.
+
+Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined.
+Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig.
+Lemma runpackW_correct_and_bounded_gen : correct_and_bounded_genT runpackW runpackZ_sig.
+Proof. rexpr_correct. Qed.
+Definition runpack_output_bounds := Eval vm_compute in compute_bounds runpackW ExprUnOpWireToFE_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition runpackW_correct_and_bounded
+  := ExprUnOpWireToFE_correct_and_bounded
+       runpackW unpack runpackZ_sig runpackW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds).
+Compute ("Unpack overflows? ", sanity_compute runpackW ExprUnOpWireToFE_bounds).
+Compute ("Unpack overflows (error if it does)? ", sanity_check runpackW ExprUnOpWireToFE_bounds).