From 26ea84f4a13d761a422d236c48ff46500663e923 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 11 Nov 2016 10:27:12 -0500 Subject: 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. --- src/Reflection/Z/Interpretations.v | 120 ++++++++++++++++++++------- src/Reflection/Z/Interpretations/Relations.v | 55 ++++++++++-- src/Reflection/Z/Syntax.v | 25 ++++-- 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 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. -- cgit v1.2.3