Make [neg] a unary operation in reflection

It now takes a meta-level [Z] argument which is the bit width.  I
haven't modified any of the extraction directives, so I don't know if
extraction still works nicely.

3 files changed, 159 insertions, 41 deletions

diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index c1256cbd6..5a015651a 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -162,11 +162,11 @@ Module Word64.
   Definition shr : word64 -> word64 -> word64 := @wordBin N.shiftr _.
   Definition land : word64 -> word64 -> word64 := @wand _.
   Definition lor : word64 -> word64 -> word64 := @wor _.
-  Definition neg : word64 -> word64 -> word64 (* TODO: FIXME? *)
-    := fun x y => ZToWord64 (ModularBaseSystemListZOperations.neg (word64ToZ x) (word64ToZ y)).
-  Definition cmovne : word64 -> word64 -> word64 -> word64 -> word64 (* TODO: FIXME? *)
+  Definition neg (int_width : Z) : word64 -> word64 (* TODO: Is this right? *)
+    := fun x => ZToWord64 (ModularBaseSystemListZOperations.neg int_width (word64ToZ x)).
+  Definition cmovne : word64 -> word64 -> word64 -> word64 -> word64 (* TODO: Is this right? *)
     := fun x y z w => ZToWord64 (ModularBaseSystemListZOperations.cmovne (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w)).
-  Definition cmovle : word64 -> word64 -> word64 -> word64 -> word64 (* TODO: FIXME? *)
+  Definition cmovle : word64 -> word64 -> word64 -> word64 -> word64 (* TODO: Is this right? *)
     := fun x y z w => ZToWord64 (ModularBaseSystemListZOperations.cmovl (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w)).
 
   Infix "+" := add : word64_scope.
@@ -198,6 +198,9 @@ Module Word64.
     := ((0 <= Zop -> Z.log2 Zop < Z.of_nat bit_width -> word64ToZ wop = Zop)%Z).
   Local Notation bounds_statement_tuple wop Zop
     := ((HList.hlist (fun v => 0 <= v /\ Z.log2 v < Z.of_nat bit_width) Zop -> Tuple.map word64ToZ wop = Zop)%Z).
+  Local Notation bounds_1statement wop Zop
+    := (forall x,
+           bounds_statement (wop x) (Zop (word64ToZ x))).
   Local Notation bounds_2statement wop Zop
     := (forall x y,
            bounds_statement (wop x y) (Zop (word64ToZ x) (word64ToZ y))).
@@ -236,7 +239,7 @@ Module Word64.
   Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_lor : bounds_2statement lor Z.lor.
   Proof. w64ToZ_t. Qed.
-  Lemma word64ToZ_neg : bounds_2statement neg ModularBaseSystemListZOperations.neg.
+  Lemma word64ToZ_neg int_width : bounds_1statement (neg int_width) (ModularBaseSystemListZOperations.neg int_width).
   Proof. w64ToZ_t; w64ToZ_extra_t. Qed.
   Lemma word64ToZ_cmovne : bounds_4statement cmovne ModularBaseSystemListZOperations.cmovne.
   Proof. w64ToZ_t; w64ToZ_extra_t. Qed.
@@ -256,7 +259,7 @@ Module Word64.
        | Shr => fun xy => fst xy >> snd xy
        | Land => fun xy => land (fst xy) (snd xy)
        | Lor => fun xy => lor (fst xy) (snd xy)
-       | Neg => fun xy => neg (fst xy) (snd xy)
+       | Neg int_width => fun x => neg int_width x
        | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
        | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w
        end%word64.
@@ -308,6 +311,15 @@ Module ZBounds.
     := if ((0 <=? l) && (Z.log2 u <? Word64.bit_width))%Z%bool
        then Some {| lower := l ; upper := u |}
        else None.
+  Definition t_map1 (f : bounds -> bounds) (x : t)
+    := match x with
+       | Some x
+         => match f x with
+            | Build_bounds l u
+              => SmartBuildBounds l u
+            end
+       | _ => None
+       end%Z.
   Definition t_map2 (f : bounds -> bounds -> bounds) (x y : t)
     := match x, y with
        | Some x, Some y
@@ -349,26 +361,21 @@ Module ZBounds.
                                        {| lower := Z.max lx ly;
                                           upper := 2^(Z.max (Z.log2_up (ux+1)) (Z.log2_up (uy+1))) - 1 |}.
   Definition lor : t -> t -> t := t_map2 lor'.
-  Definition neg' : bounds -> bounds -> bounds
-    := fun int_width v
-       => let (lint_width, uint_width) := int_width in
-          let (lb, ub) := v in
+  Definition neg' (int_width : Z) : bounds -> bounds
+    := fun v
+       => let (lb, ub) := v in
           let might_be_one := ((lb <=? 1) && (1 <=? ub))%Z%bool in
           let must_be_one := ((lb =? 1) && (ub =? 1))%Z%bool in
           if must_be_one
-          then {| lower := Z.ones lint_width ; upper := Z.ones uint_width |}
+          then {| lower := Z.ones int_width ; upper := Z.ones int_width |}
           else if might_be_one
-               then {| lower := 0 ; upper := Z.ones uint_width |}
+               then {| lower := 0 ; upper := Z.ones int_width |}
                else {| lower := 0 ; upper := 0 |}.
-  Definition neg : t -> t -> t
-    := fun int_width v
-       => match int_width, v with
-          | Some (Build_bounds lint_width uint_width as int_width), Some (Build_bounds lb ub as v)
-            => if ((0 <=? lint_width) && (uint_width <=? Word64.bit_width))%Z%bool
-               then Some (neg' int_width v)
-               else None
-          | _, _ => None
-          end.
+  Definition neg (int_width : Z) : t -> t
+    := fun v
+       => if ((0 <=? int_width) && (int_width <=? Word64.bit_width))%Z%bool
+          then t_map1 (neg' int_width) v
+          else None.
   Definition cmovne' (r1 r2 : bounds) : bounds
     := let (lr1, ur1) := r1 in let (lr2, ur2) := r2 in {| lower := Z.min lr1 lr2 ; upper := Z.max ur1 ur2 |}.
   Definition cmovne (x y r1 r2 : t) : t := t_map4 (fun _ _ => cmovne') x y r1 r2.
@@ -398,7 +405,7 @@ Module ZBounds.
        | Shr => fun xy => fst xy >> snd xy
        | Land => fun xy => land (fst xy) (snd xy)
        | Lor => fun xy => lor (fst xy) (snd xy)
-       | Neg => fun xy => neg (fst xy) (snd xy)
+       | Neg int_width => fun x => neg int_width x
        | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
        | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w
        end%bounds.
@@ -497,6 +504,29 @@ Module BoundedWord64.
        | TZ => to_bounds'
        end.
 
+  Definition t_map1
+             (opW : Word64.word64 -> Word64.word64)
+             (opB : ZBounds.t -> ZBounds.t)
+             (pf : forall x l u,
+                 opB (Some (BoundedWordToBounds x))
+                 = Some {| ZBounds.lower := l ; ZBounds.upper := u |}
+                 -> let val :=  opW (value x) in
+                    is_bounded_by val l u)
+    : t -> t
+    := fun x : t
+       => match x with
+          | Some x
+            => match opB (Some (BoundedWordToBounds x))
+                     as bop return opB (Some (BoundedWordToBounds x)) = bop -> t
+               with
+               | Some (ZBounds.Build_bounds l u)
+                 => fun Heq => Some {| lower := l ; value := opW (value x) ; upper := u;
+                                       in_bounds := pf _ _ _ Heq |}
+               | None => fun _ => None
+               end eq_refl
+          | _ => None
+          end.
+
   Definition t_map2
              (opW : Word64.word64 -> Word64.word64 -> Word64.word64)
              (opB : ZBounds.t -> ZBounds.t -> ZBounds.t)
@@ -548,11 +578,15 @@ Module BoundedWord64.
   Hint Resolve Z.ones_nonneg : zarith.
   Local Ltac t_prestart :=
     repeat first [ match goal with
+                   | [ |- forall x l u, ?opB (Some (BoundedWordToBounds x)) = Some _ -> let val := ?opW (value x) in _ ]
+                     => let opB' := head opB in let opW' := head opW in progress (try unfold opB'; try unfold opW')
                    | [ |- forall x y l u, ?opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) = Some _ -> let val := ?opW (value x) (value y) in _ ]
-                     => try unfold opB; try unfold opW
+                     => progress (try unfold opB; try unfold opW)
                    | [ |- forall x y z w l u, ?opB _ _ _ _ = Some _ -> let val := ?opW (value x) (value y) (value z) (value w) in _ ]
-                     => try unfold opB; try unfold opW
-                   | [ |- appcontext[ZBounds.t_map2 ?op] ] => unfold op
+                     => progress (try unfold opB; try unfold opW)
+                   | [ |- appcontext[ZBounds.t_map1 ?op] ] => let op' := head op in unfold op'
+                   | [ |- appcontext[ZBounds.t_map2 ?op] ] => let op' := head op in unfold op'
+                   | [ |- appcontext[?op (ZBounds.Build_bounds _ _)] ] => let op' := head op in unfold op'
                    | [ |- appcontext[?op (ZBounds.Build_bounds _ _) (ZBounds.Build_bounds _ _)] ] => unfold op
                    end
                  | progress cbv [BoundedWordToBounds ZBounds.SmartBuildBounds cmovne cmovl ModularBaseSystemListZOperations.neg] in *
@@ -628,8 +662,8 @@ Module BoundedWord64.
       abstract (t_start; eapply shr_valid_update; eauto).
   Defined.
 
-  Definition neg : t -> t -> t.
-  Proof. refine (t_map2 Word64.neg ZBounds.neg _); abstract t_start. Defined.
+  Definition neg (int_width : Z) : t -> t.
+  Proof. refine (t_map1 (Word64.neg int_width) (ZBounds.neg int_width) _); abstract t_start. Defined.
 
   Definition cmovne : t -> t -> t -> t -> t.
   Proof. refine (t_map4 Word64.cmovne ZBounds.cmovne _); abstract t_start. Defined.
@@ -637,6 +671,12 @@ Module BoundedWord64.
   Definition cmovle : t -> t -> t -> t -> t.
   Proof. refine (t_map4 Word64.cmovle ZBounds.cmovle _); abstract t_start. Defined.
 
+  Local Notation unop_correct op opW opB :=
+    (forall x v, op (Some x) = Some v
+                 -> value v = opW (value x)
+                    /\ Some (BoundedWordToBounds v) = opB (Some (BoundedWordToBounds x)))
+      (only parsing).
+
   Local Notation binop_correct op opW opB :=
     (forall x y v, op (Some x) (Some y) = Some v
                    -> value v = opW (value x) (value y)
@@ -650,6 +690,16 @@ Module BoundedWord64.
                                                                 (Some (BoundedWordToBounds z)) (Some (BoundedWordToBounds w)))
       (only parsing).
 
+  Lemma t_map1_correct opW opB pf
+    : unop_correct (t_map1 opW opB pf) opW opB.
+  Proof.
+    intros ?? H.
+    unfold t_map1 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
+      unfold BoundedWordToBounds in *;
+      inversion_option; subst; simpl.
+    eauto.
+  Qed.
+
   Lemma t_map2_correct opW opB pf
     : binop_correct (t_map2 opW opB pf) opW opB.
   Proof.
@@ -670,6 +720,10 @@ Module BoundedWord64.
     eauto.
   Qed.
 
+  Local Notation unop_correct_None op opB :=
+    (forall x, op (Some x) = None -> opB (Some (BoundedWordToBounds x)) = None)
+      (only parsing).
+
   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).
@@ -681,6 +735,16 @@ Module BoundedWord64.
                         = None)
       (only parsing).
 
+  Lemma t_map1_correct_None opW opB pf
+    : unop_correct_None (t_map1 opW opB pf) opB.
+  Proof.
+    intros ? H.
+    unfold t_map1 in H; convoy_destruct_in H; destruct_head' ZBounds.bounds;
+      unfold BoundedWordToBounds in *;
+      inversion_option; subst; simpl.
+    eauto.
+  Qed.
+
   Lemma t_map2_correct_None opW opB pf
     : binop_correct_None (t_map2 opW opB pf) opB.
   Proof.
@@ -721,7 +785,7 @@ Module BoundedWord64.
        | Shr => fun xy => fst xy >> snd xy
        | Land => fun xy => land (fst xy) (snd xy)
        | Lor => fun xy => lor (fst xy) (snd xy)
-       | Neg => fun xy => neg (fst xy) (snd xy)
+       | Neg int_width => fun x => neg int_width x
        | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
        | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovle x y z w
      end%bounded_word.
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v
index 3e018678d..281f4d7a7 100644
--- a/src/Reflection/Z/Interpretations/Relations.v
+++ b/src/Reflection/Z/Interpretations/Relations.v
@@ -92,16 +92,18 @@ Local Ltac related_word64_op_t_step :=
         | progress break_match_hyps
         | congruence
         | match goal with
-          | [ H : ?op _ _ = Some _ |- _ ]
+          | [ H : ?op _ = Some _ |- _ ]
             => let H' := fresh in
                rename H into H';
-               first [ pose proof (@BoundedWord64.t_map2_correct _ _ _ _ _ _ H') as H; clear H'
+               first [ pose proof (@BoundedWord64.t_map1_correct _ _ _ _ _ H') as H; clear H'
+                     | pose proof (@BoundedWord64.t_map2_correct _ _ _ _ _ _ H') as H; clear H'
                      | pose proof (@BoundedWord64.t_map4_correct _ _ _ _ _ _ H') as H; clear H' ];
                simpl in H
-          | [ H : ?op _ _ = None |- _ ]
+          | [ H : ?op _ = None |- _ ]
             => let H' := fresh in
                rename H into H';
-               first [ pose proof (@BoundedWord64.t_map2_correct_None _ _ _ _ _ H') as H; clear H'
+               first [ pose proof (@BoundedWord64.t_map1_correct_None _ _ _ _ H') as H; clear H'
+                     | pose proof (@BoundedWord64.t_map2_correct_None _ _ _ _ _ H') as H; clear H'
                      | pose proof (@BoundedWord64.t_map4_correct_None _ _ _ _ _ H') as H; clear H' ];
                simpl in H
           end
@@ -114,6 +116,15 @@ Local Ltac related_word64_op_t_step :=
           end ].
 Local Ltac related_word64_op_t := repeat related_word64_op_t_step.
 
+Lemma related_word64_t_map1 opW opB pf
+      sv1 sv2
+  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_word64 sv1 sv2
+    -> @related_word64 TZ (BoundedWord64.t_map1 opW opB pf sv1) (opW sv2).
+Proof.
+  cbv [interp_flat_type BoundedWord64.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  related_word64_op_t.
+Qed.
+
 Lemma related_word64_t_map2 opW opB pf
       sv1 sv2
   : interp_flat_type_rel_pointwise2 (t:=Prod (Tbase TZ) (Tbase TZ)) related_word64 sv1 sv2
@@ -319,10 +330,21 @@ Local Arguments BoundedWord64.BoundedWordToBounds !_ / .
 Lemma related_word64_op : related_op related_word64 (@BoundedWord64.interp_op) (@Word64.interp_op).
 Proof.
   (let op := fresh in intros ?? op; destruct op; simpl);
-    try first [ apply related_word64_t_map2
+    try first [ apply related_word64_t_map1
+              | apply related_word64_t_map2
               | apply related_word64_t_map4 ].
 Qed.
 
+Lemma related_bounds_t_map1 opW opB pf
+      (HN : opB None = None)
+      sv1 sv2
+  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_bounds sv1 sv2
+    -> @related_bounds TZ (BoundedWord64.t_map1 opW opB pf sv1) (opB sv2).
+Proof.
+  cbv [interp_flat_type BoundedWord64.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  related_word64_op_t.
+Qed.
+
 Lemma related_bounds_t_map2 opW opB pf
       (HN0 : forall v, opB None v = None)
       (HN1 : forall v, opB v None = None)
@@ -370,7 +392,7 @@ Proof.
   { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
   { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
   { apply related_bounds_t_map2; intros; destruct_head' option; reflexivity. }
-  { apply related_bounds_t_map2; intros; destruct_head' option; destruct_head' ZBounds.bounds; reflexivity. }
+  { apply related_bounds_t_map1; intros; destruct_head' option; unfold ZBounds.neg; break_match; reflexivity. }
   { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. }
   { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. }
 Qed.
@@ -395,7 +417,7 @@ Local Ltac Word64.Rewrites.word64_util_arith ::=
               (eapply Z.le_lt_trans; [ eapply Z.log2_le_mono; eassumption | assumption ])
             | eapply Z.le_lt_trans; [ eapply Z.log2_le_mono, neg_upperbound | ];
               Word64.Rewrites.word64_util_arith
-            | (progress unfold ModularBaseSystemListZOperations.cmovne, ModularBaseSystemListZOperations.cmovl); break_match;
+            | (progress unfold ModularBaseSystemListZOperations.cmovne, ModularBaseSystemListZOperations.cmovl, ModularBaseSystemListZOperations.neg); break_match;
               Word64.Rewrites.word64_util_arith ].
 Local Ltac related_Z_op_t_step :=
   first [ progress related_word64_op_t_step
@@ -410,6 +432,21 @@ Local Notation is_in_bounds value bounds
   := (is_bounded_by value (ZBounds.lower bounds) (ZBounds.upper bounds))
        (only parsing).
 
+Lemma related_Z_t_map1 opZ opW opB pf
+      (H : forall x bxs brs,
+          Some brs = opB (Some bxs)
+          -> is_in_bounds x bxs
+          -> is_in_bounds (opW x) brs
+          -> Word64.word64ToZ (opW x) = (opZ (Word64.word64ToZ x)))
+      sv1 sv2
+  : interp_flat_type_rel_pointwise2 (t:=Tbase TZ) related_Z sv1 sv2
+    -> @related_Z TZ (BoundedWord64.t_map1 opW opB pf sv1) (opZ sv2).
+Proof.
+  cbv [interp_flat_type BoundedWord64.interp_base_type ZBounds.interp_base_type LiftOption.interp_base_type' interp_flat_type_rel_pointwise2 interp_flat_type_rel_pointwise2_gen_Prop] in *.
+  related_Z_op_t.
+  eapply H; eauto.
+Qed.
+
 Lemma related_Z_t_map2 opZ opW opB pf
       (H : forall x y bxs bys brs,
           Some brs = opB (Some bxs) (Some bys)
@@ -470,6 +507,8 @@ Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step.
 
 Local Opaque Word64.bit_width.
 
+Local Arguments ZBounds.neg _ !_ / .
+
 Lemma related_Z_op : related_op related_Z (@BoundedWord64.interp_op) (@Z.interp_op).
 Proof.
   let op := fresh in intros ?? op; destruct op; simpl.
@@ -480,7 +519,7 @@ Proof.
   { apply related_Z_t_map2; related_Z_op_fin_t. }
   { apply related_Z_t_map2; related_Z_op_fin_t. }
   { apply related_Z_t_map2; related_Z_op_fin_t. }
-  { apply related_Z_t_map2; related_Z_op_fin_t. }
+  { apply related_Z_t_map1; related_Z_op_fin_t. }
   { apply related_Z_t_map4; related_Z_op_fin_t. }
   { apply related_Z_t_map4; related_Z_op_fin_t. }
 Qed.
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index 116e3513e..ab47929b1 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -39,7 +39,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type :=
 | Shr : op (tZ * tZ) tZ
 | Land : op (tZ * tZ) tZ
 | Lor : op (tZ * tZ) tZ
-| Neg : op (tZ * tZ) tZ
+| Neg (int_width : Z) : op tZ tZ
 | Cmovne : op (tZ * tZ * tZ * tZ) tZ
 | Cmovle : op (tZ * tZ * tZ * tZ) tZ.
 
@@ -52,7 +52,7 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_typ
      | Shr => fun xy => fst xy >> snd xy
      | Land => fun xy => Z.land (fst xy) (snd xy)
      | Lor => fun xy => Z.lor (fst xy) (snd xy)
-     | Neg => fun xy => ModularBaseSystemListZOperations.neg (fst xy) (snd xy)
+     | Neg int_width => fun x => ModularBaseSystemListZOperations.neg int_width x
      | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
      | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovl x y z w
      end%Z.
@@ -83,8 +83,8 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reifi
      | Land, _ => false
      | Lor, Lor => true
      | Lor, _ => false
-     | Neg, Neg => true
-     | Neg, _ => false
+     | Neg n, Neg m => Z.eqb n m
+     | Neg _, _ => false
      | Cmovne, Cmovne => true
      | Cmovne, _ => false
      | Cmovle, Cmovle => true
@@ -112,7 +112,22 @@ Definition op_beq_hetero_eq {t1 tR t1' tR'} f g
       _ (op_beq_hetero_type_eqs f g pf)
     = g.
 Proof.
-  destruct f, g; simpl; try solve [ reflexivity | intros [] ].
+  destruct f, g; simpl; try solve [ reflexivity | intros [] ];
+    unfold op_beq_hetero; simpl;
+      repeat match goal with
+             | [ |- context[to_prop (reified_Prop_of_bool ?x)] ]
+               => destruct (Sumbool.sumbool_of_bool x) as [P|P]
+             | [ H : NatUtil.nat_beq _ _ = true |- _ ]
+               => apply NatUtil.internal_nat_dec_bl in H
+             | [ H : Z.eqb _ _ = true |- _ ]
+               => apply Z.eqb_eq in H
+             | _ => progress subst
+             | _ => reflexivity
+             | [ H : ?x = false |- context[reified_Prop_of_bool ?x] ]
+               => rewrite H
+             | _ => progress simpl @to_prop
+             | _ => tauto
+             end.
 Qed.
 
 Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y.