diff options
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperations.v | 4 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations.v | 246 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations/Relations.v | 181 | ||||
| -rw-r--r-- | src/Reflection/Z/Reify.v | 10 | ||||
| -rw-r--r-- | src/Reflection/Z/Syntax.v | 31 |
5 files changed, 5 insertions, 467 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v index 09a252a06..0c8f3caa0 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v @@ -11,7 +11,3 @@ Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2. neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) neg 0 = 0 *) Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z. - -(** TODO(jadep): Fill in this stub *) -Axiom conditional_subtract_modulus - : forall (limb_count : nat) (int_width : Z) (modulus value : Tuple.tuple Z limb_count), Tuple.tuple Z limb_count. diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 8a31b3947..0c6dcd2f1 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -168,9 +168,7 @@ Module Word64. := 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? *) := fun x y z w => ZToWord64 (ModularBaseSystemListZOperations.cmovl (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w)). - Definition conditional_subtract (pred_limb_count : nat) : word64 -> Tuple.tuple word64 (S pred_limb_count) -> Tuple.tuple word64 (S pred_limb_count) -> Tuple.tuple word64 (S pred_limb_count) - := fun x y z => Tuple.map ZToWord64 (@ModularBaseSystemListZOperations.conditional_subtract_modulus - (S pred_limb_count) (word64ToZ x) (Tuple.map word64ToZ y) (Tuple.map word64ToZ z)). + Infix "+" := add : word64_scope. Infix "-" := sub : word64_scope. Infix "*" := mul : word64_scope. @@ -203,9 +201,6 @@ Module Word64. Local Notation bounds_2statement wop Zop := (forall x y, bounds_statement (wop x y) (Zop (word64ToZ x) (word64ToZ y))). - Local Notation bounds_1_tuple2_statement wop Zop - := (forall x y z, - bounds_statement_tuple (wop x y z) (Zop (word64ToZ x) (Tuple.map word64ToZ y) (Tuple.map word64ToZ z))). Local Notation bounds_4statement wop Zop := (forall x y z w, bounds_statement (wop x y z w) (Zop (word64ToZ x) (word64ToZ y) (word64ToZ z) (word64ToZ w))). @@ -247,20 +242,6 @@ Module Word64. Proof. w64ToZ_t; w64ToZ_extra_t. Qed. Lemma word64ToZ_cmovle : bounds_4statement cmovle ModularBaseSystemListZOperations.cmovl. Proof. w64ToZ_t; w64ToZ_extra_t. Qed. - Lemma word64ToZ_conditional_subtract pred_limb_count - : bounds_1_tuple2_statement (@conditional_subtract pred_limb_count) - (@ModularBaseSystemListZOperations.conditional_subtract_modulus (S pred_limb_count)). - Proof. - w64ToZ_t; unfold conditional_subtract; w64ToZ_extra_t. - repeat first [ progress w64ToZ_extra_t - | rewrite Tuple.map_map - | rewrite HList.Tuple.map_id_ext - | match goal with - | [ H : HList.hlist _ _ |- HList.hlist _ _ ] - => revert H; apply HList.hlist_impl - end - | apply HList.const ]. - Qed. Definition interp_base_type (t : base_type) : Type := match t with @@ -278,9 +259,6 @@ Module Word64. | Neg => fun xy => neg (fst xy) (snd xy) | 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 - | ConditionalSubtract pred_n - => fun xyz => let '(x, y, z) := eta3 xyz in - flat_interp_untuple' (T:=Tbase TZ) (@conditional_subtract pred_n x (flat_interp_tuple y) (flat_interp_tuple z)) end%word64. Definition of_Z ty : Z.interp_base_type ty -> interp_base_type ty @@ -315,8 +293,6 @@ Module Word64. Hint Rewrite <- word64ToZ_cmovne using word64_util_arith : pull_word64ToZ. Hint Rewrite word64ToZ_cmovle using word64_util_arith : push_word64ToZ. Hint Rewrite <- word64ToZ_cmovle using word64_util_arith : pull_word64ToZ. - Hint Rewrite word64ToZ_conditional_subtract using word64_util_arith : push_word64ToZ. - Hint Rewrite <- word64ToZ_conditional_subtract using word64_util_arith : pull_word64ToZ. End Rewrites. End Word64. @@ -458,9 +434,6 @@ Module ZBounds. | Neg => fun xy => neg (fst xy) (snd xy) | 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 - | ConditionalSubtract pred_n - => fun xyz => let '(x, y, z) := eta3 xyz in - flat_interp_untuple' (T:=Tbase TZ) (@conditional_subtract pred_n x (flat_interp_tuple y) (flat_interp_tuple z)) end%bounds. Definition of_word64 ty : Word64.interp_base_type ty -> interp_base_type ty @@ -604,44 +577,6 @@ Module BoundedWord64. | _, _, _, _ => None end. - Definition t_map1_tuple2 {n} - (opW : Word64.word64 -> Tuple.tuple Word64.word64 (S n) -> Tuple.tuple Word64.word64 (S n) -> Tuple.tuple Word64.word64 (S n)) - (opB : ZBounds.t -> Tuple.tuple ZBounds.t (S n) -> Tuple.tuple ZBounds.t (S n) -> Tuple.tuple ZBounds.t (S n)) - (pf : forall x y z bs, - Tuple.lift_option - (opB (Some (BoundedWordToBounds x)) (Tuple.push_option (Some (Tuple.map BoundedWordToBounds y))) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds z)))) - = Some bs - -> let val := opW (value x) (Tuple.map value y) (Tuple.map value z) in - HList.hlist - (fun vlu => let v := fst vlu in - let lu : ZBounds.bounds := snd vlu in - is_bounded_by v (ZBounds.lower lu) (ZBounds.upper lu)) - (Tuple.map2 (fun v (lu : ZBounds.bounds) => (v, lu)) - val bs)) - : t -> Tuple.tuple t (S n) -> Tuple.tuple t (S n) -> Tuple.tuple t (S n) - := fun (x : t) (y z : Tuple.tuple t (S n)) - => Tuple.push_option - match x, Tuple.lift_option y, Tuple.lift_option z with - | Some x, Some y, Some z - => match Tuple.lift_option (opB (Some (BoundedWordToBounds x)) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds y))) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds z)))) - as bop return Tuple.lift_option _ = bop -> option (Tuple.tuple _ (S n)) with - | Some bs - => fun Heq - => let v - := HList.mapt - (fun (vlu : Word64.word64 * ZBounds.bounds) pf - => {| lower := ZBounds.lower (snd vlu) ; value := fst vlu ; upper := ZBounds.upper (snd vlu) ; - in_bounds := pf |}) - (pf _ _ _ _ Heq) in - Some v - | None => fun _ => None - end eq_refl - | _, _, _ => None - end. - Local Opaque Word64.bit_width. Hint Resolve Z.ones_nonneg : zarith. Local Ltac t_prestart := @@ -679,117 +614,11 @@ Module BoundedWord64. => apply (Z.max_case_strong x y) end ]. - (** 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 - [pf] and return the tuple of [{| lower := l ; value := v ; upper - := u ; in_bounds := pf |}]. *) - Lemma conditional_subtract_bounded - (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 : 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. - 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. - 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 /\ - (Z.log2 (ZBounds.upper (snd vlu)) < Word64.bit_width)%Z) - (Tuple.map2 (fun v lu => (v, lu)) - (Word64.conditional_subtract - pred_n (value x) (Tuple.map value y) (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). - 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. - Definition add : t -> t -> t. Proof. refine (t_map2 Word64.add ZBounds.add _); @@ -841,23 +670,6 @@ Module BoundedWord64. Definition cmovle : t -> t -> t -> t -> t. Proof. refine (t_map4 Word64.cmovle ZBounds.cmovle _); abstract t_start. Defined. - Definition conditional_subtract (pred_n : nat) - : forall (int_width : t) (modulus val : Tuple.tuple t (S pred_n)), - Tuple.tuple t (S pred_n). - Proof. - refine (@t_map1_tuple2 pred_n (@Word64.conditional_subtract _) (@ZBounds.conditional_subtract _) _). - abstract ( - repeat first [ progress unfold ZBounds.conditional_subtract - | rewrite !Tuple.lift_push_option - | progress break_match - | congruence - | progress subst - | progress inversion_option - | intro - | solve [ auto using conditional_subtract_bounded_word ] ] - ). - Defined. - 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) @@ -871,17 +683,6 @@ Module BoundedWord64. (Some (BoundedWordToBounds z)) (Some (BoundedWordToBounds w))) (only parsing). - Local Notation op1_tuple2_correct op opW opB := - (forall x y z v, - Tuple.lift_option (op (Some x) (Tuple.push_option (Some y)) (Tuple.push_option (Some z))) = Some v - -> Tuple.map value v = opW (value x) (Tuple.map value y) (Tuple.map value z) - /\ Some (Tuple.map BoundedWordToBounds v) - = Tuple.lift_option - (opB (Some (BoundedWordToBounds x)) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds y))) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds z))))) - (only parsing). - Lemma t_map2_correct opW opB pf : binop_correct (t_map2 opW opB pf) opW opB. Proof. @@ -902,29 +703,6 @@ Module BoundedWord64. eauto. Qed. - (* TODO: Automate this proof more *) - Lemma t_map1_tuple2_correct {n} opW opB pf - : op1_tuple2_correct (t_map1_tuple2 (n:=n) opW opB pf) opW opB. - Proof. - intros ???? H. - unfold t_map1_tuple2 in H; unfold BoundedWordToBounds in *. - rewrite !Tuple.lift_push_option in H. - convoy_destruct_in H; [ | congruence ]. - rewrite_hyp *. - inversion_option. - symmetry in H. - pose proof (f_equal (Tuple.map value) H) as H0'. - pose proof (f_equal (Tuple.map BoundedWordToBounds) H) as H1'. - unfold BoundedWordToBounds in *. - rewrite_hyp !*. - rewrite !HList.map_mapt; simpl @lower; simpl @upper; simpl @value. - rewrite <- !HList.map_is_mapt. - rewrite !Tuple.map_map2; simpl @fst; simpl @snd. - rewrite !Tuple.map2_fst, !Tuple.map2_snd, Tuple.map_id, Tuple.map_id_ext - by (intros [? ?]; reflexivity). - eauto. - Qed. - 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). @@ -936,16 +714,6 @@ Module BoundedWord64. = None) (only parsing). - 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 - (opB (Some (BoundedWordToBounds x)) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds y))) - (Tuple.push_option (Some (Tuple.map BoundedWordToBounds z)))) - = None) - (only parsing). - Lemma t_map2_correct_None opW opB pf : binop_correct_None (t_map2 opW opB pf) opB. Proof. @@ -966,15 +734,6 @@ Module BoundedWord64. eauto. Qed. - Lemma t_map1_tuple2_correct_None {n} opW opB pf - : 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 *. - rewrite !Tuple.lift_push_option in H. - convoy_destruct_in H; congruence. - Qed. - Module Export Notations. Delimit Scope bounded_word_scope with bounded_word. Notation "b[ l ~> u ]" := {| lower := l ; upper := u |} : bounded_word_scope. @@ -998,9 +757,6 @@ Module BoundedWord64. | Neg => fun xy => neg (fst xy) (snd xy) | 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 - | ConditionalSubtract pred_n - => fun xyz => let '(x, y, z) := eta3 xyz in - flat_interp_untuple' (T:=Tbase TZ) (@conditional_subtract pred_n x (flat_interp_tuple y) (flat_interp_tuple z)) end%bounded_word. End BoundedWord64. diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 963834a10..3760b15e0 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -96,15 +96,13 @@ Local Ltac related_word64_op_t_step := => let H' := fresh in rename H into H'; first [ pose proof (@BoundedWord64.t_map2_correct _ _ _ _ _ _ H') as H; clear H' - | pose proof (@BoundedWord64.t_map4_correct _ _ _ _ _ _ H') as H; clear H' - | pose proof (@BoundedWord64.t_map1_tuple2_correct _ _ _ _ _ _ H') as H; clear H' ]; + | pose proof (@BoundedWord64.t_map4_correct _ _ _ _ _ _ H') as H; clear H' ]; simpl in H | [ H : ?op _ _ = None |- _ ] => let H' := fresh in rename H into H'; first [ pose proof (@BoundedWord64.t_map2_correct_None _ _ _ _ _ H') as H; clear H' - | pose proof (@BoundedWord64.t_map4_correct_None _ _ _ _ _ H') as H; clear H' - | pose proof (@BoundedWord64.t_map1_tuple2_correct_None _ _ _ _ _ H') as H; clear H' ]; + | pose proof (@BoundedWord64.t_map4_correct_None _ _ _ _ _ H') as H; clear H' ]; simpl in H end | progress cbv [related'_word64 proj_eq_rel BoundedWord64.to_word64' BoundedWord64.boundedWordToWord64 BoundedWord64.value] in * @@ -318,78 +316,11 @@ Local Arguments LiftOption.lift_relation _ _ _ _ !_ _ / . 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 - | progress subst - | progress destruct_head_hnf' prod - | progress destruct_head_hnf' and - | progress destruct_head_hnf' option - | progress inversion_option - | intro - | apply @related_tuples_None_left; constructor - | apply -> @related_tuples_Some_left - | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _) - | apply <- @related_tuples_lift_relation2_untuple' - | match goal with - | [ H : appcontext[LiftOption.lift_relation] |- _ ] - => eapply related_tuples_Some_left_ext in H; [ | eassumption ] - | [ H : appcontext[proj_eq_rel] |- _ ] - => apply -> @related_tuples_proj_eq_rel_tuple in H - | [ H : appcontext[LiftOption.lift_relation2] |- _ ] - => eapply (fun H => proj1 (related_tuples_lift_relation2_untuple'_ext H)) in H; - [ | first [ left; eexists; eassumption | right; eexists; eassumption ] ] - | [ H : Tuple.lift_option ?x = Some _, H' : context[?x] |- _ ] - => setoid_rewrite H in H' - | [ H : proj_eq_rel _ _ _ |- _ ] => hnf in H - | [ H : Tuple.lift_option (flat_interp_tuple' ?x) = Some _ |- _ ] - => is_var x; apply lift_option_flat_interp_tuple' in H - end - | progress rewrite ?HList.map'_mapt', <- ?HList.map_is_mapt' - | progress rewrite ?Tuple.map_map2, ?Tuple.map2_fst, ?Tuple.map2_snd, ?Tuple.map_id - | progress rewrite Tuple.map_id_ext by repeat (reflexivity || intros [] || intro) - | progress rewrite ?flat_interp_tuple_untuple', ?flat_interp_tuple'_untuple' in * - | progress unfold BoundedWord64.t_map1_tuple2, HList.mapt - | progress unfold related_word64, related'_word64, related_bounds in * - | progress simpl @BoundedWord64.to_word64' in * - | progress simpl @fst in * - | progress simpl @snd in * - | progress simpl @option_map in * - | progress simpl @BoundedWord64.BoundedWordToBounds in * - | progress break_match - | progress convoy_destruct - | progress simpl @interp_flat_type_rel_pointwise2 in * - | progress simpl @LiftOption.lift_relation in * - | progress simpl @LiftOption.lift_relation2 in * - | progress simpl @flat_interp_tuple in * - | progress simpl @LiftOption.of' in * - | progress simpl @smart_interp_flat_map in * - | rewrite_hyp <- !*; reflexivity - | solve [ eauto using lift_option_None_interp_flat_type_rel_pointwise2_1 ] - | match goal with - | [ H : LiftOption.lift_relation2 _ _ _ _ |- _ ] => unfold LiftOption.lift_relation2 in H - | [ H : LiftOption.of' _ = _ |- _ ] => unfold LiftOption.of' in H - | [ H : option_map _ _ = _ |- _ ] => unfold option_map in H - end ]. -Local Ltac t_map1_tuple2_t := repeat t_map1_tuple2_t_step. - -Lemma related_word64_t_map1_tuple2 {n} opW opB pf - sv1 sv2 - : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Tbase TZ) (Syntax.tuple (Tbase TZ) (S n))) (Syntax.tuple (Tbase TZ) (S n))) related_word64 sv1 sv2 - -> interp_flat_type_rel_pointwise2 - (t:=Syntax.tuple (Tbase TZ) (S n)) related_word64 - (Syntax.flat_interp_untuple' (n:=n) (T:=Tbase TZ) (BoundedWord64.t_map1_tuple2 (n:=n) opW opB pf (fst (fst sv1)) (Syntax.flat_interp_tuple (snd (fst sv1))) (Syntax.flat_interp_tuple (snd sv1)))) - (Syntax.flat_interp_untuple' (n:=n) (T:=Tbase TZ) (opW (fst (fst sv2)) (Syntax.flat_interp_tuple (snd (fst sv2))) (Syntax.flat_interp_tuple (snd sv2)))). -Proof. t_map1_tuple2_t. Qed. - 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 - | apply related_word64_t_map4 - | apply related_word64_t_map1_tuple2 ]. + | apply related_word64_t_map4 ]. Qed. Lemma related_bounds_t_map2 opW opB pf @@ -428,36 +359,6 @@ Local Arguments Tuple.push_option : simpl never. Local Arguments Tuple.map : simpl never. Local Arguments Tuple.map2 : simpl never. -Lemma related_bounds_t_map1_tuple2 {n} opW opB pf - (HN0 : forall x y, opB None x y = Tuple.push_option None) - (HN1 : forall x y z, Tuple.lift_option y = None -> opB x y z = Tuple.push_option None) - (HN2 : forall x y z, Tuple.lift_option z = None -> opB x y z = Tuple.push_option None) - (HN3 : forall x y z, Tuple.lift_option (opB x y z) = None -> opB x y z = Tuple.push_option None) - sv1 sv2 - : interp_flat_type_rel_pointwise2 (t:=Prod (Prod (Tbase TZ) (Syntax.tuple (Tbase TZ) (S n))) (Syntax.tuple (Tbase TZ) (S n))) related_bounds sv1 sv2 - -> interp_flat_type_rel_pointwise2 - (t:=Syntax.tuple (Tbase TZ) (S n)) related_bounds - (Syntax.flat_interp_untuple' (n:=n) (T:=Tbase TZ) (BoundedWord64.t_map1_tuple2 (n:=n) opW opB pf (fst (fst sv1)) (Syntax.flat_interp_tuple (snd (fst sv1))) (Syntax.flat_interp_tuple (snd sv1)))) - (Syntax.flat_interp_untuple' (n:=n) (T:=Tbase TZ) (opB (fst (fst sv2)) (Syntax.flat_interp_tuple (snd (fst sv2))) (Syntax.flat_interp_tuple (snd sv2)))). -Proof. - t_map1_tuple2_t; - try first [ rewrite HN0 by (assumption || t_map1_tuple2_t) - | rewrite HN1 by (assumption || t_map1_tuple2_t) - | rewrite HN2 by (assumption || t_map1_tuple2_t) - | rewrite HN3 by (assumption || t_map1_tuple2_t) ]; - t_map1_tuple2_t. - { repeat match goal with - | [ |- context[HList.mapt' _ ?ls] ] - => not is_var ls; generalize ls; intro - | [ H : Tuple.lift_option _ = Some _ |- _ ] - => apply Tuple.push_lift_option in H; setoid_rewrite H - | _ => progress (break_match_hyps; t_map1_tuple2_t) - end. } - { repeat (break_match_hyps; t_map1_tuple2_t). - rewrite HN3 by (assumption || t_map1_tuple2_t). - t_map1_tuple2_t. } -Qed. - Local Arguments ZBounds.SmartBuildBounds _ _ / . Lemma related_bounds_op : related_op related_bounds (@BoundedWord64.interp_op) (@ZBounds.interp_op). Proof. @@ -472,12 +373,6 @@ Proof. { apply related_bounds_t_map2; intros; destruct_head' option; destruct_head' ZBounds.bounds; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } { apply related_bounds_t_map4; intros; destruct_head' option; reflexivity. } - { apply related_bounds_t_map1_tuple2; intros; destruct_head' option; try reflexivity; - unfold ZBounds.conditional_subtract in *; rewrite ?Tuple.lift_push_option in *; - repeat match goal with H : _ |- _ => rewrite !Tuple.lift_push_option in H end; - try reflexivity; - (rewrite_hyp ?* ); - break_match; try reflexivity. } Qed. Local Ltac Word64.Rewrites.word64_util_arith ::= @@ -553,68 +448,6 @@ Qed. Local Arguments related_Z _ !_ _ / . Local Arguments related'_Z _ _ _ / . -Lemma related_Z_t_map1_tuple2 n opZ opW opB pf - (H : forall x y z bxs bys bzs brs, - Some brs = Tuple.lift_option (opB (Some bxs) (Tuple.push_option (Some bys)) (Tuple.push_option (Some bzs))) - -> is_in_bounds x bxs - -> { 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 } - -> Tuple.map Word64.word64ToZ (opW x y z) = (opZ (Word64.word64ToZ x) (Tuple.map Word64.word64ToZ y) (Tuple.map Word64.word64ToZ z))) - sv1 sv2 - : interp_flat_type_rel_pointwise2 (t:=(Tbase TZ * Syntax.tuple (Tbase TZ) (S n) * Syntax.tuple (Tbase TZ) (S n))%ctype) related_Z sv1 sv2 - -> interp_flat_type_rel_pointwise2 - related_Z - (flat_interp_untuple' (T:=Tbase TZ) (BoundedWord64.t_map1_tuple2 opW opB pf (fst (fst sv1)) (flat_interp_tuple' (snd (fst sv1))) (flat_interp_tuple' (snd sv1)))) - (flat_interp_untuple' (T:=Tbase TZ) (opZ (fst (fst sv2)) (flat_interp_tuple' (snd (fst sv2))) (flat_interp_tuple' (snd sv2)))). -Proof. - repeat first [ progress simpl in * - | progress intros - | progress destruct_head_hnf' and - | progress destruct_head_hnf' prod - | progress destruct_head_hnf' option - | progress (unfold proj_eq_rel in *; subst) - | apply @related_tuples_None_left; constructor - | apply -> @related_tuples_Some_left - | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _) - | apply <- @related_tuples_lift_relation2_untuple' - | progress rewrite ?HList.map'_mapt', <- ?HList.map_is_mapt' - | progress rewrite ?Tuple.map_map2, ?Tuple.map2_fst, ?Tuple.map2_snd, ?Tuple.map_id - | progress convoy_destruct - | match goal with - | [ H : interp_flat_type_rel_pointwise2 _ ?u ?v |- _ ] - => let lem := constr:(fun u' H => proj2 (@related_tuples_Some_left_ext _ _ _ (@related'_Z) u v u' H)) in - let H' := fresh in - lazymatch type of lem with - | forall u', ?v = Some u' -> _ - => destruct v eqn:H' - end; - unfold BoundedWord64.t_map1_tuple2; - simpl @flat_interp_tuple in *; - simpl @Tuple.lift_option in *; - change (LiftOption.interp_base_type' BoundedWord64.BoundedWord) - with BoundedWord64.interp_base_type in *; - rewrite H'; - [ apply (lem _ H') in H - | solve [ break_match; apply @related_tuples_None_left; constructor ] ] - | [ H : interp_flat_type_rel_pointwise2 _ _ ?v |- _ ] - => rewrite <- (@flat_interp_untuple'_tuple' _ _ _ _ v) in H; - let H' := fresh in - rename H into H'; - pose proof (proj1 related_tuples_proj_eq_rel_untuple H') as H; - clear H' - end ]. - etransitivity; [ eapply H | ]; - [ symmetry; eassumption - | destruct_head' BoundedWord64.BoundedWord; assumption - | solve [ repeat esplit ].. - | (rewrite_hyp <- !* ); - rewrite !Tuple.map_map; - reflexivity ]. -Qed. Local Ltac related_Z_op_fin_t_step := first [ progress subst @@ -651,14 +484,6 @@ Proof. { apply related_Z_t_map2; 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. } - { apply related_Z_t_map1_tuple2; related_Z_op_fin_t; - 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. diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v index 6734d7d01..451e522d0 100644 --- a/src/Reflection/Z/Reify.v +++ b/src/Reflection/Z/Reify.v @@ -21,16 +21,6 @@ Ltac base_reify_op op op_head extra ::= | @ModularBaseSystemListZOperations.neg => constr:(reify_op op op_head 2 Neg) | @ModularBaseSystemListZOperations.cmovne => constr:(reify_op op op_head 4 Cmovne) | @ModularBaseSystemListZOperations.cmovl => constr:(reify_op op op_head 4 Cmovle) - | @ModularBaseSystemListZOperations.conditional_subtract_modulus - => lazymatch extra with - | @ModularBaseSystemListZOperations.conditional_subtract_modulus ?limb_count _ _ _ - => lazymatch (eval compute in limb_count) with - | 0 => fail 1 "Cannot handle empty limb-list in reifying conditional_subtract_modulus" - | S ?pred_limb_count => constr:(reify_op op op_head 3 (ConditionalSubtract pred_limb_count)) - | ?climb_count => fail 1 "Cannot handle non-ground length of limb-list in reifying conditional_subtract_modulus" "(" limb_count "which computes to" climb_count ")" - end - | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is conditional_subtract_modulus but body is wrong:" extra - end end. Ltac base_reify_type T ::= lazymatch T with diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index 5657fff32..116e3513e 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -41,12 +41,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type := | Lor : op (tZ * tZ) tZ | Neg : op (tZ * tZ) tZ | Cmovne : op (tZ * tZ * tZ * tZ) tZ -| Cmovle : op (tZ * tZ * tZ * tZ) tZ -| ConditionalSubtract (pred_limb_count : nat) - : op (tZ (* int_width *) - * Syntax.tuple tZ (S pred_limb_count) (* modulus *) - * Syntax.tuple tZ (S pred_limb_count) (* value *)) - (Syntax.tuple tZ (S pred_limb_count)). +| Cmovle : op (tZ * tZ * tZ * tZ) tZ. Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with @@ -60,9 +55,6 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_typ | Neg => fun xy => ModularBaseSystemListZOperations.neg (fst xy) (snd xy) | 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 - | ConditionalSubtract pred_n - => fun xyz => let '(x, y, z) := eta3 xyz in - flat_interp_untuple' (T:=tZ) (@ModularBaseSystemListZOperations.conditional_subtract_modulus (S pred_n) x (flat_interp_tuple y) (flat_interp_tuple z)) end%Z. Definition base_type_eq_semidec_transparent (t1 t2 : base_type) @@ -97,8 +89,6 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : reifi | Cmovne, _ => false | Cmovle, Cmovle => true | Cmovle, _ => false - | ConditionalSubtract n, ConditionalSubtract m => NatUtil.nat_beq n m - | ConditionalSubtract _, _ => false end. Definition op_beq t1 tR (f g : op t1 tR) : reified_Prop @@ -107,13 +97,6 @@ Definition op_beq t1 tR (f g : op t1 tR) : reified_Prop Definition op_beq_hetero_type_eq {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1' /\ tR = tR'. Proof. destruct f, g; simpl; try solve [ repeat constructor | intros [] ]. - unfold op_beq_hetero; simpl. - match goal with - | [ |- context[to_prop (reified_Prop_of_bool ?x)] ] - => destruct (Sumbool.sumbool_of_bool x) as [P|P] - end. - { apply NatUtil.internal_nat_dec_bl in P; subst; repeat constructor. } - { intro H'; exfalso; rewrite P in H'; exact H'. } Defined. Definition op_beq_hetero_type_eqs {t1 tR t1' tR'} f g : to_prop (@op_beq_hetero t1 tR t1' tR' f g) -> t1 = t1' @@ -130,18 +113,6 @@ Definition op_beq_hetero_eq {t1 tR t1' tR'} f g = g. Proof. destruct f, g; simpl; try solve [ reflexivity | intros [] ]. - { unfold op_beq_hetero, op_beq_hetero_type_eqs, op_beq_hetero_type_eqd; simpl. - intro pf; edestruct Sumbool.sumbool_of_bool. - { simpl; - lazymatch goal with - | [ |- context[NatUtil.internal_nat_dec_bl ?x ?y ?pf] ] - => generalize dependent (NatUtil.internal_nat_dec_bl x y pf); intro; subst - end; - reflexivity. } - { match goal with - | [ |- context[False_ind _ ?pf] ] - => case pf - end. } } Qed. Lemma op_beq_bl : forall t1 tR x y, to_prop (op_beq t1 tR x y) -> x = y. |