Rebase + remove WordizeUtil dependency from Z/Interpretations

2 files changed, 131 insertions, 37 deletions

diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 9b58b5f5c..a3b51f28f 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -1,7 +1,5 @@
 (** * Interpretation of PHOAS syntax for expression trees on ℤ *)
-Require Import Bedrock.Nomega.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.NArith.NArith.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
@@ -16,9 +14,6 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.WordUtil.
 Require Import Bedrock.Word.
-Require Import Crypto.Assembly.WordizeUtil.
-Require Import Crypto.Assembly.Evaluables.
-Require Import Crypto.Assembly.QhasmUtil.
 Export Reflection.Syntax.Notations.
 
 Local Notation eta x := (fst x, snd x).
@@ -215,16 +210,13 @@ Module Word64.
     := (forall x y z w,
            bounds_statement (wop x y z w) (Zop (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w))).
 
-  Require Import Crypto.Assembly.WordizeUtil.
-
   Lemma word64ToZ_add : bounds_2statement add Z.add. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_sub : bounds_2statement sub Z.sub. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_mul : bounds_2statement mul Z.mul. Proof. w64ToZ_t. Qed.
-
   Lemma word64ToZ_shl : bounds_2statement shl Z.shiftl.
   Proof.
     w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin.
-    rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftl; reflexivity|].
+    rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftl; reflexivity|].
     apply N2Z.inj_lt.
     rewrite Z_inj_shiftl. 
     destruct (Z.lt_ge_cases 0 ((word64ToZ x) << (word64ToZ y)))%Z;
@@ -236,7 +228,7 @@ Module Word64.
   Lemma word64ToZ_shr : bounds_2statement shr Z.shiftr.
   Proof.
     w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin.
-    rewrite wordToN_NToWord; [rewrite <- Z_inj_shiftr; reflexivity|].
+    rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftr; reflexivity|].
     apply N2Z.inj_lt.
     rewrite Z_inj_shiftr.
     destruct (Z.lt_ge_cases 0 ((word64ToZ x) >> (word64ToZ y)))%Z;
@@ -434,9 +426,9 @@ Module ZBounds.
     : Tuple.tuple t (S pred_n)
     := Tuple.push_option
          match int_width, Tuple.lift_option modulus, Tuple.lift_option value with
-         | Some int_width, Some modulus, Some value
-           => if check_conditional_subtract_bounds pred_n int_width modulus value
-              then Some (conditional_subtract' pred_n int_width modulus value)
+         | Some int_width, Some modulus, Some value'
+           => if check_conditional_subtract_bounds pred_n int_width modulus value'
+              then Some (conditional_subtract' pred_n int_width modulus value')
               else None
          | _, _, _ => None
          end.
@@ -684,6 +676,10 @@ Module BoundedWord64.
   Ltac ktrans k := do k (etransitivity; [|eassumption]); assumption.
   Ltac trans' := first [ assumption | ktrans ltac:1 | ktrans ltac:2 ].
 
+  Local Hint Resolve Word64.bit_width_pos : zarith.
+  Local Hint Extern 1 (Z.log2 _ < _)%Z => eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | eassumption ] : zarith.
+  (* Local *) Hint Resolve <- Z.log2_lt_pow2_alt : zarith.
+
 
   (** TODO(jadep): Use the bounds lemma here to prove that if each
       component of [ret_val] is [Some (l, v, u)], then we can fill in
@@ -696,6 +692,28 @@ Module BoundedWord64.
                pred_n (BoundedWordToBounds x)
                (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
     : HList.hlist
+        (fun vlu : Z * ZBounds.bounds =>
+           (0 <= ZBounds.lower (snd vlu))%Z /\
+           (ZBounds.lower (snd vlu) <= fst vlu <= ZBounds.upper (snd vlu))%Z /\
+           (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z)
+        (Tuple.map2 (fun v lu => (v, lu))
+                    (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                       (S pred_n)
+                       (Word64.word64ToZ (value x))
+                       (Tuple.map Word64.word64ToZ (Tuple.map value y))
+                       (Tuple.map Word64.word64ToZ (Tuple.map value z)))
+                    (ZBounds.conditional_subtract'
+                       pred_n (BoundedWordToBounds x)
+                       (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))).
+  Proof. Admitted.
+
+  Lemma conditional_subtract_bounded_word
+        (pred_n : nat) (x : BoundedWord)
+        (y z : Tuple.tuple BoundedWord (S pred_n))
+        (H : ZBounds.check_conditional_subtract_bounds
+               pred_n (BoundedWordToBounds x)
+               (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
+    : HList.hlist
         (fun vlu : Word64.word64 * ZBounds.bounds =>
            (0 <= ZBounds.lower (snd vlu))%Z /\
            (ZBounds.lower (snd vlu) <= Word64.word64ToZ (fst vlu) <= ZBounds.upper (snd vlu))%Z /\
@@ -706,12 +724,73 @@ Module BoundedWord64.
                     (ZBounds.conditional_subtract'
                        pred_n (BoundedWordToBounds x)
                        (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))).
-  Proof. Admitted.
+  Proof.
+    generalize (conditional_subtract_bounded pred_n x y z H).
+    unfold Word64.conditional_subtract; rewrite Tuple.map2_map_fst.
+    rewrite <- (Tuple.map_map2 (fun a b => (a, b)) (fun ab => (Word64.ZToWord64 (fst ab), snd ab))).
+    rewrite HList.hlist_map; simpl @fst; simpl @snd.
+    apply HList.hlist_impl, HList.const.
+    intros; destruct_head' and; repeat split;
+      autorewrite with push_word64ToZ; omega.
+  Qed.
 
+  Lemma conditional_subtract_bounded_lite_helper
+        (pred_n : nat) (x : BoundedWord)
+        (y z : Tuple.tuple BoundedWord (S pred_n))
+        (H : ZBounds.check_conditional_subtract_bounds
+               pred_n (BoundedWordToBounds x)
+               (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z) = true)
+    : HList.hlist
+        (fun v : Z =>
+           (0 <= v)%Z /\
+           (Z.log2 v < Word64.bit_width)%Z)
+        (Tuple.map
+           (@fst _ _)
+           (Tuple.map2 (fun v lu => (v, lu))
+                       (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                          (S pred_n)
+                          (Word64.word64ToZ (value x))
+                          (Tuple.map Word64.word64ToZ (Tuple.map value y))
+                          (Tuple.map Word64.word64ToZ (Tuple.map value z)))
+                       (ZBounds.conditional_subtract'
+                          pred_n (BoundedWordToBounds x)
+                          (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z)))).
+  Proof.
+    generalize (conditional_subtract_bounded pred_n x y z H).
+    rewrite HList.hlist_map.
+    apply HList.hlist_impl, HList.const; intros.
+    destruct_head' and.
+    split; try omega; [].
+    eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ]; omega.
+  Qed.
+
+  Lemma conditional_subtract_bounded_lite
+        (pred_n : nat)
+        (xbw : BoundedWord) (ybw zbw : Tuple.tuple BoundedWord (S pred_n))
+        (x : Word64.word64) (y z : Tuple.tuple Word64.word64 (S pred_n))
+        (xb : ZBounds.bounds)  (yb zb : Tuple.tuple ZBounds.bounds (S pred_n))
+        (Hx : value xbw = x) (Hy : Tuple.map value ybw = y) (Hz : Tuple.map value zbw = z)
+        (Hxb : BoundedWordToBounds xbw = xb)
+        (Hyb : Tuple.map BoundedWordToBounds ybw = yb) (Hzb : Tuple.map BoundedWordToBounds zbw = zb)
+        (Hc : ZBounds.check_conditional_subtract_bounds pred_n xb yb zb = true)
+    : HList.hlist (fun v : Z => (0 <= v)%Z /\ (Z.log2 v < Z.of_nat Word64.bit_width)%Z)
+                  (ModularBaseSystemListZOperations.conditional_subtract_modulus
+                     (S pred_n)
+                     (Word64.word64ToZ x)
+                     (Tuple.map Word64.word64ToZ y)
+                     (Tuple.map Word64.word64ToZ z)).
+  Proof.
+    subst.
+    generalize (conditional_subtract_bounded_lite_helper pred_n xbw ybw zbw Hc).
+    rewrite Tuple.map_map2; simpl @fst.
+    rewrite Tuple.map2_fst, Tuple.map_id.
+    trivial.
+  Qed.
+
+  (* TODO (rsloan): not entirely sure what's the best way to match on these... *)
   Local Ltac kill_assumptions :=
     repeat split; abstract (cbn; assumption).
 
-  (* TODO (rsloan): not entirely sure what's the best way to match on these... *)
   Local Ltac apply_update lem lower0 value0 upper0 lower1 value1 upper1 := first
     [ apply (lem 64 lower1 value1 upper1 lower0 value0 upper0); kill_assumptions
     | apply (lem 64 lower0 value0 upper0 lower1 value1 upper1); kill_assumptions].
@@ -780,7 +859,7 @@ Module BoundedWord64.
                      | progress subst
                      | progress inversion_option
                      | intro
-                     | solve [ auto using conditional_subtract_bounded ] ]
+                     | solve [ auto using conditional_subtract_bounded_word ] ]
       ).
   Defined.
 
@@ -851,18 +930,18 @@ Module BoundedWord64.
     eauto.
   Qed.
 
-  Local Notation binop_correct_None op opW opB :=
+  Local Notation binop_correct_None op opB :=
     (forall x y, op (Some x) (Some y) = None -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) = None)
       (only parsing).
 
-  Local Notation op4_correct_None op opW opB :=
+  Local Notation op4_correct_None op opB :=
     (forall x y z w, op (Some x) (Some y) (Some z) (Some w) = None
                      -> opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y))
                             (Some (BoundedWordToBounds z)) (Some (BoundedWordToBounds w))
                         = None)
       (only parsing).
 
-  Local Notation op1_tuple2_correct_None op opW opB :=
+  Local Notation op1_tuple2_correct_None op opB :=
     (forall x y z,
         Tuple.lift_option (op (Some x) (Tuple.push_option (Some y)) (Tuple.push_option (Some z))) = None
         -> Tuple.lift_option
@@ -873,7 +952,7 @@ Module BoundedWord64.
       (only parsing).
 
   Lemma t_map2_correct_None opW opB pf
-    : binop_correct_None (t_map2 opW opB pf) opW opB.
+    : binop_correct_None (t_map2 opW opB pf) opB.
   Proof.
     intros ?? H.
     unfold t_map2 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
@@ -883,7 +962,7 @@ Module BoundedWord64.
   Qed.
 
   Lemma t_map4_correct_None opW opB pf
-    : op4_correct_None (t_map4 opW opB pf) opW opB.
+    : op4_correct_None (t_map4 opW opB pf) opB.
   Proof.
     intros ???? H.
     unfold t_map4 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
@@ -893,7 +972,7 @@ Module BoundedWord64.
   Qed.
 
   Lemma t_map1_tuple2_correct_None {n} opW opB pf
-    : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opW opB.
+    : op1_tuple2_correct_None (t_map1_tuple2 (n:=n) opW opB pf) opB.
   Proof.
     intros ??? H.
     unfold t_map1_tuple2 in H; unfold BoundedWordToBounds in *.
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v
index 457d0d5ad..71d25fa3f 100644
--- a/src/Reflection/Z/Interpretations/Relations.v
+++ b/src/Reflection/Z/Interpretations/Relations.v
@@ -231,8 +231,8 @@ Lemma related_tuples_lift_relation2_untuple'
     <-> LiftOption.lift_relation2
           (interp_flat_type_rel_pointwise2 (fun _ => R))
           TZ
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) t)
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) u).
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) t)
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) u).
 Proof.
   induction n.
   { destruct_head' option; reflexivity. }
@@ -257,8 +257,8 @@ Lemma related_tuples_lift_relation2_untuple'_ext
     <-> LiftOption.lift_relation2
           (interp_flat_type_rel_pointwise2 (fun _ => R))
           TZ
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
-          (option_map (flat_interp_untuple' (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => T) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) t)))
+          (option_map (flat_interp_untuple' (interp_base_type:=fun _ => U) (T:=Tbase TZ)) (Tuple.lift_option (flat_interp_tuple (T:=Tbase TZ) u))).
 Proof.
   induction n.
   { destruct_head_hnf' option; reflexivity. }
@@ -270,7 +270,7 @@ Proof.
         (etransitivity;
          [ | first [ refine (f_equal (option_map (@fst _ _)) (_ : _ = Some (_, _))); eassumption
                    | refine (f_equal (option_map (@snd _ _)) (_ : _ = Some (_, _))); eassumption ] ]);
-        simpl in *; break_match; simpl in *; congruence. }
+        instantiate; simpl in *; break_match; simpl in *; congruence. }
     destruct_head_hnf' prod;
       destruct_head_hnf' option;
       simpl @fst in *; simpl @snd in *;
@@ -319,6 +319,7 @@ Local Arguments LiftOption.of' _ _ !_ / .
 Local Arguments BoundedWord64.BoundedWordToBounds !_ / .
 
 Local Ltac t_map1_tuple2_t_step :=
+  instantiate;
   first [ exact I
         | reflexivity
         | progress destruct_head_hnf' False
@@ -330,7 +331,7 @@ Local Ltac t_map1_tuple2_t_step :=
         | intro
         | apply @related_tuples_None_left; constructor
         | apply -> @related_tuples_Some_left
-        | apply <- @related_tuples_proj_eq_rel_untuple
+        | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _)
         | apply <- @related_tuples_lift_relation2_untuple'
         | match goal with
           | [ H : appcontext[LiftOption.lift_relation] |- _ ]
@@ -491,7 +492,7 @@ Local Ltac Word64.Rewrites.word64_util_arith ::=
                       auto with zarith ]
             | apply Z.land_nonneg; Word64.Rewrites.word64_util_arith
             | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono | eassumption ];
-              apply Z.min_case_strong; intros;
+              instantiate; apply Z.min_case_strong; intros;
               first [ etransitivity; [ apply Z.land_upper_bound_l | ]; omega
                     | etransitivity; [ apply Z.land_upper_bound_r | ]; omega ]
             | rewrite Z.log2_lor by omega;
@@ -556,10 +557,15 @@ Tactic Notation "admit" := abstract case proof_admitted.
 Local Arguments related'_Z _ _ _ / .
 Lemma related_Z_t_map1_tuple2 n opZ opW opB pf
       (H : forall x y z bxs bys bzs brs,
-          Tuple.push_option (Some brs) = opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs))
+          Some brs = Tuple.lift_option (opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs)))
           -> is_in_bounds x bxs
-          (*-> is_in_bounds y bys
-          -> is_in_bounds z bzs
+          -> { ybw : Tuple.tuple BoundedWord64.BoundedWord _
+             | Tuple.map BoundedWord64.value ybw = y
+               /\ Tuple.map BoundedWord64.BoundedWordToBounds ybw = bys }
+          -> { zbw : Tuple.tuple BoundedWord64.BoundedWord _
+             | Tuple.map BoundedWord64.value zbw = z
+               /\ Tuple.map BoundedWord64.BoundedWordToBounds zbw = bzs }
+          (*
           -> is_in_bounds (opW x y z) brs*)
           -> Tuple.map Word64.word64ToZ (opW x y z) = (opZ (Word64.word64ToZ x) (Tuple.map Word64.word64ToZ y) (Tuple.map Word64.word64ToZ z)))
       sv1 sv2
@@ -594,8 +600,13 @@ Local Ltac related_Z_op_fin_t_step :=
         | progress inversion_option
         | intro
         | progress autorewrite with push_word64ToZ
-        | match goal with H : andb _ _ = true |- _ => rewrite Bool.andb_true_iff in H end
-        | progress Z.ltb_to_lt ].
+        | match goal with
+          | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H
+          | [ H : context[Tuple.lift_option (Tuple.push_option _)] |- _ ]
+            => rewrite Tuple.lift_push_option in H
+          end
+        | progress Z.ltb_to_lt
+        | (progress unfold ZBounds.conditional_subtract in * ); break_match_hyps ].
 Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step.
 
 Local Opaque Word64.bit_width.
@@ -614,9 +625,13 @@ Proof.
   { apply related_Z_t_map4; related_Z_op_fin_t. }
   { apply related_Z_t_map4; related_Z_op_fin_t. }
   { apply related_Z_t_map1_tuple2; related_Z_op_fin_t;
-      rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith.
-    pose proof BoundedWord64.conditional_subtract_bounded.
-    admit. (** TODO(jadep or jgross): Fill me in *) }
+      rewrite Word64.word64ToZ_conditional_subtract; try Word64.Rewrites.word64_util_arith; [].
+    destruct_head' sig; destruct_head' and; subst.
+    eapply BoundedWord64.conditional_subtract_bounded_lite
+    with (xbw := {| BoundedWord64.value := _ |});
+      [ .. | eassumption ]; reflexivity.
+    Grab Existential Variables.
+    omega. }
 Qed.
 
 Create HintDb interp_related discriminated.