Add SpecificGen/GF*

For bounds analysis

1 files changed, 12 insertions, 0 deletions

diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/Add.v b/src/SpecificGen/GF25519_32Reflective/Reified/Add.v
new file mode 100644
index 000000000..c35de3c76
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/Add.v
@@ -0,0 +1,12 @@
+Require Import Crypto.SpecificGen.GF25519_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).