Not quite done with WordUtil lemmas.

12 files changed, 202 insertions, 0 deletions

diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v
new file mode 100644
index 000000000..36357fcb7
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Add.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check raddW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
new file mode 100644
index 000000000..0ff563a8c
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rcarry_addW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
new file mode 100644
index 000000000..4c21fbeb8
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rcarry_oppW ExprUnOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
new file mode 100644
index 000000000..3acfb1f45
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rcarry_subW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
new file mode 100644
index 000000000..e3ecc62c8
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Freeze.v
@@ -0,0 +1,18 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined.
+Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig.
+Lemma rfreezeW_correct_and_bounded_gen : correct_and_bounded_genT rfreezeW rfreezeZ_sig.
+Proof. rexpr_correct. Qed.
+Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW ExprUnOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Axiom proof_admitted : False.
+(** XXX TODO: Fix bounds analysis on freeze *)
+Definition rfreezeW_correct_and_bounded
+  := ExprUnOp_correct_and_bounded
+       rfreezeW freeze rfreezeZ_sig rfreezeW_correct_and_bounded_gen
+       match proof_admitted with end match proof_admitted with end.
+
+Local Open Scope string_scope.
+Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds).
+(*Compute ("Freeze overflows? ", sanity_check rfreezeW ExprUnOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v
new file mode 100644
index 000000000..73ee6904a
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rge_modulusW ExprUnOpFEToZ_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
new file mode 100644
index 000000000..a206f02a1
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rmulW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v
new file mode 100644
index 000000000..907771b14
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Opp.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check roppW ExprUnOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
new file mode 100644
index 000000000..a7cf4fc13
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rpackW ExprUnOpFEToWire_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v
new file mode 100644
index 000000000..9b684248d
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Sub.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check rsubW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
new file mode 100644
index 000000000..027eedf39
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -0,0 +1,16 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+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_check runpackW ExprUnOpWireToFE_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
new file mode 100755
index 000000000..76ac2c91b
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -0,0 +1,39 @@
+#!/usr/bin/env python2.7
+from __future__ import with_statement
+
+for name, opkind in ([(name, 'BinOp') for name in ('Add', 'Carry_Add', 'Sub', 'Carry_Sub', 'Mul')]
+                     + [(name, 'UnOp') for name in ('Opp', 'Carry_Opp', 'Freeze')]
+                     + [('Ge_Modulus', 'UnOp_FEToZ'), ('Pack', 'UnOp_FEToWire'), ('Unpack', 'UnOp_WireToFE')]):
+    lname = name.lower()
+    lopkind = opkind.replace('UnOp', 'unop').replace('BinOp', 'binop')
+    uopkind = opkind.replace('_', '')
+    extra = ''
+    if name in ('Carry_Add', 'Carry_Sub', 'Mul', 'Carry_Opp', 'Pack', 'Unpack', 'Ge_Modulus'):
+        extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition r%(lname)sW_correct_and_bounded
+  := Expr%(uopkind)s_correct_and_bounded
+       r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
+       _ _.
+""" % locals()
+    elif name == 'Freeze':
+        extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
+Axiom proof_admitted : False.
+(** XXX TODO: Fix bounds analysis on freeze *)
+Definition r%(lname)sW_correct_and_bounded
+  := Expr%(uopkind)s_correct_and_bounded
+       r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
+       match proof_admitted with end match proof_admitted with end.
+""" % locals()
+    with open(name.replace('_', '') + '.v', 'w') as f:
+        f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition r%(lname)sZ_sig : rexpr_%(lopkind)s_sig %(lname)s. Proof. reify_sig. Defined.
+Definition r%(lname)sW := Eval vm_compute in rword_of_Z r%(lname)sZ_sig.
+Lemma r%(lname)sW_correct_and_bounded_gen : correct_and_bounded_genT r%(lname)sW r%(lname)sZ_sig.
+Proof. rexpr_correct. Qed.
+Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lname)sW Expr%(uopkind)s_bounds.
+%(extra)s
+Local Open Scope string_scope.
+Compute ("%(name)s", compute_bounds_for_display r%(lname)sW Expr%(uopkind)s_bounds).
+(*Compute ("%(name)s overflows? ", sanity_check r%(lname)sW Expr%(uopkind)s_bounds).*)
+""" % locals())