diff options
| -rw-r--r-- | src/Assembly/WordizeUtil.v | 22 | ||||
| -rw-r--r-- | src/Reflection/Z/Interpretations.v | 94 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 371 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 38 |
4 files changed, 478 insertions, 47 deletions
diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v index 2727bac07..b5f246fb1 100644 --- a/src/Assembly/WordizeUtil.v +++ b/src/Assembly/WordizeUtil.v @@ -252,6 +252,12 @@ Section Misc. apply N.sub_le_mono_l. apply N_ge_0. Qed. + + Lemma log2_conv: forall z, Z.log2 z = Z.of_N (N.log2 (Z.to_N z)). + Proof. + intro z; induction z as [| |p]; auto. + induction p; auto. + Qed. End Misc. Section Exp. @@ -348,7 +354,6 @@ Section Exp. apply N.mul_le_mono_l. assumption. Qed. - End Exp. Section Conversions. @@ -923,6 +928,21 @@ Section TopLevel. reflexivity. Qed. + Lemma wordize_or: forall {n} (x y: word n), + & (wor x y) = N.lor (&x) (&y). + Proof. + intros. + apply N.bits_inj_iff; unfold N.eqf; intro k. + rewrite N.lor_spec. + repeat rewrite wordToN_testbit. + revert x y. + generalize (N.to_nat k) as k'; clear k. + induction n; intros; shatter x; shatter y; simpl; [reflexivity|]. + induction k'; [reflexivity|]. + rewrite IHn. + reflexivity. + Qed. + Lemma conv_mask: forall {n} (x: word n) (k: nat), (k <= n)%nat -> mask k x = x ^& (NToWord _ (N.ones (N.of_nat k))). diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 8d0ab0c1b..336376c9e 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -1,5 +1,7 @@ (** * 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. @@ -12,8 +14,11 @@ Require Crypto.Util.HList. Require Import Crypto.Util.Bool. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Tactics. -Require Import Bedrock.Word. 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). @@ -210,17 +215,38 @@ 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. admit. Admitted. + Proof. + w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin. + rewrite wordToN_NToWord; [rewrite <- Z.N2Z.inj_shiftl; reflexivity|]. + apply N2Z.inj_lt. + rewrite Z.N2Z.inj_shiftl. + destruct (Z.lt_ge_cases 0 ((word64ToZ x) << (word64ToZ y)))%Z; + [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. + rewrite Npow2_N, N2Z.inj_pow. + apply Z.log2_lt_pow2; assumption. + Qed. + Lemma word64ToZ_shr : bounds_2statement shr Z.shiftr. - Proof. admit. Admitted. - Lemma word64ToZ_land : bounds_2statement land Z.land. - Proof. w64ToZ_t. Qed. - Lemma word64ToZ_lor : bounds_2statement lor Z.lor. - Proof. w64ToZ_t. Qed. + Proof. + w64ToZ_t; w64ToZ_extra_t; unfold word64ToZ, wordBin. + rewrite wordToN_NToWord; [rewrite <- Z.N2Z.inj_shiftr; reflexivity|]. + apply N2Z.inj_lt. + rewrite Z.N2Z.inj_shiftr. + destruct (Z.lt_ge_cases 0 ((word64ToZ x) >> (word64ToZ y)))%Z; + [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. + rewrite Npow2_N, N2Z.inj_pow. + apply Z.log2_lt_pow2; assumption. + Qed. + + Lemma word64ToZ_land : bounds_2statement land Z.land. Proof. w64ToZ_t. Qed. + Lemma word64ToZ_lor : bounds_2statement lor Z.lor. Proof. w64ToZ_t. Qed. Lemma word64ToZ_neg : bounds_2statement neg ModularBaseSystemListZOperations.neg. Proof. w64ToZ_t; w64ToZ_extra_t. Qed. Lemma word64ToZ_cmovne : bounds_4statement cmovne ModularBaseSystemListZOperations.cmovne. @@ -330,6 +356,7 @@ Module ZBounds. end | _, _, _, _ => None end%Z. + Definition add' : bounds -> bounds -> bounds := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx + ly ; upper := ux + uy |}. Definition add : t -> t -> t := t_map2 add'. @@ -345,6 +372,7 @@ Module ZBounds. Definition shr' : bounds -> bounds -> bounds := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := lx >> uy ; upper := ux >> ly |}. Definition shr : t -> t -> t := t_map2 shr'. + Definition land' : bounds -> bounds -> bounds := fun x y => let (lx, ux) := x in let (ly, uy) := y in {| lower := 0 ; upper := Z.min ux uy |}. Definition land : t -> t -> t := t_map2 land'. @@ -625,6 +653,7 @@ Module BoundedWord64. Axiom proof_admitted : False. Local Opaque Word64.bit_width. Hint Resolve Z.ones_nonneg : zarith. + Local Ltac t_start := repeat first [ match goal with | [ |- forall x y l u, ?opB (Some (BoundedWordToBounds x)) (Some (BoundedWordToBounds y)) = Some _ -> let val := ?opW (value x) (value y) in _ ] @@ -650,15 +679,10 @@ Module BoundedWord64. | progress autorewrite with push_word64ToZ | progress repeat apply conj | solve [ Word64.arith ] - | match goal with - | [ |- appcontext[Z.min ?x ?y] ] - => apply (Z.min_case_strong x y) - | [ |- appcontext[Z.max ?x ?y] ] - => apply (Z.max_case_strong x y) - end | progress destruct_head' or ]. - Tactic Notation "admit" := abstract case proof_admitted. + Ltac ktrans k := do k (etransitivity; [|eassumption]); assumption. + Ltac trans' := first [ assumption | ktrans ltac:1 | ktrans ltac:2 ]. (** TODO(jadep): Use the bounds lemma here to prove that if each @@ -684,46 +708,54 @@ Module BoundedWord64. (Tuple.map BoundedWordToBounds y) (Tuple.map BoundedWordToBounds z))). Proof. Admitted. + 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]. Definition add : t -> t -> t. Proof. - refine (t_map2 Word64.add ZBounds.add _); t_start; admit. + refine (t_map2 Word64.add ZBounds.add _); t_start; + apply_update @add_valid_update lower0 value0 upper0 lower1 value1 upper1. Defined. Definition sub : t -> t -> t. Proof. refine (t_map2 Word64.sub ZBounds.sub _); t_start; - admit. + apply_update @sub_valid_update lower0 value0 upper0 lower1 value1 upper1. Defined. Definition mul : t -> t -> t. Proof. refine (t_map2 Word64.mul ZBounds.mul _); t_start; - admit. + apply_update @mul_valid_update lower0 value0 upper0 lower1 value1 upper1. Defined. - Definition shl : t -> t -> t. + Definition land : t -> t -> t. Proof. - refine (t_map2 Word64.shl ZBounds.shl _); t_start; - admit. - Defined. + refine (t_map2 Word64.land ZBounds.land _); t_start; + apply_update @land_valid_update lower0 value0 upper0 lower1 value1 upper1. + Qed. - Definition shr : t -> t -> t. + Definition lor : t -> t -> t. Proof. - refine (t_map2 Word64.shr ZBounds.shr _); t_start; - admit. - Defined. + refine (t_map2 Word64.lor ZBounds.lor _); t_start; + apply_update @lor_valid_update lower0 value0 upper0 lower1 value1 upper1. + Qed. - Definition land : t -> t -> t. + Definition shl : t -> t -> t. Proof. - refine (t_map2 Word64.land ZBounds.land _); t_start; - admit. + refine (t_map2 Word64.shl ZBounds.shl _); t_start; + apply_update @shl_valid_update lower0 value0 upper0 lower1 value1 upper1. Defined. - Definition lor : t -> t -> t. + Definition shr : t -> t -> t. Proof. - refine (t_map2 Word64.lor ZBounds.lor _); t_start; - admit. + refine (t_map2 Word64.shr ZBounds.shr _); t_start; + apply_update @shr_valid_update lower0 value0 upper0 lower1 value1 upper1. Defined. Definition neg : t -> t -> t. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 7a856f1e9..24160d83e 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -34,6 +34,15 @@ Proof. auto. Qed. +Lemma Z_land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. +Proof. + intros; apply Z.ldiff_le; [assumption|]. + rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc. + rewrite <- Z.land_0_l with (a := y); f_equal. + rewrite Z.land_comm, Z.land_lnot_diag. + reflexivity. +Qed. + Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N -> wordToN (NToWord sz n) = n. Proof. @@ -271,47 +280,379 @@ Proof. end. Qed. -Local Notation bounds_2statement wop Zop - := (forall {sz} (x y : word sz), - (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)) - -> Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz - -> Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))))%Z). +Local Notation bounds_2statement wop Zop := (forall {sz} (x y : word sz), + (0 <= Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)) + -> (Z.log2 (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y))) < Z.of_nat sz) + -> (Z.of_N (wordToN (wop x y)) = (Zop (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))))%Z). + +Require Import Crypto.Assembly.WordizeUtil. +Require Import Crypto.Assembly.Bounds. Lemma wordToN_wplus : bounds_2statement (@wplus _) Z.add. Proof. - admit. -Admitted. + intros. + rewrite <- wordize_plus; [rewrite N2Z.inj_add; reflexivity|]. + destruct (N.eq_dec (wordToN x + wordToN y) 0%N) as [e|e]; + [rewrite e; apply Npow2_gt0|]. + apply N.neq_0_lt_0 in e. + apply N2Z.inj_lt in e. + apply N2Z.inj_lt. + rewrite N2Z.inj_add in *. + rewrite Npow2_N. + rewrite N2Z.inj_pow. + replace (Z.of_N 2%N) with 2%Z by auto. + apply Z.log2_lt_pow2; [auto|]. + rewrite nat_N_Z. + assumption. +Qed. + Hint Rewrite @wordToN_wplus using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wplus using word_util_arith : pull_wordToN. Lemma wordToN_wminus : bounds_2statement (@wminus _) Z.sub. Proof. - admit. -Admitted. + intros sz x y H ?. + assert (wordToN y <= wordToN x)%N. { + apply N2Z.inj_le. + rewrite <- (Z.add_0_l (Z.of_N (wordToN y))). + apply Z.le_add_le_sub_r; assumption. + } + + rewrite <- N2Z.inj_sub; [|assumption]. + rewrite <- wordize_minus; [reflexivity|apply N.le_ge; assumption]. +Qed. + Hint Rewrite @wordToN_wminus using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wminus using word_util_arith : pull_wordToN. Lemma wordToN_wmult : bounds_2statement (@wmult _) Z.mul. Proof. - admit. -Admitted. + intros. + rewrite <- wordize_mult; [rewrite N2Z.inj_mul; reflexivity|]. + destruct (N.eq_dec (wordToN x * wordToN y) 0%N) as [e|e]; + [rewrite e; apply Npow2_gt0|]. + apply N.neq_0_lt_0 in e. + apply N2Z.inj_lt in e. + apply N2Z.inj_lt. + rewrite N2Z.inj_mul in *. + rewrite Npow2_N. + rewrite N2Z.inj_pow. + replace (Z.of_N 2%N) with 2%Z by auto. + apply Z.log2_lt_pow2; [auto|]. + rewrite nat_N_Z. + assumption. +Qed. + Hint Rewrite @wordToN_wmult using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wmult using word_util_arith : pull_wordToN. Lemma wordToN_wand : bounds_2statement (@wand _) Z.land. Proof. - admit. -Admitted. + intros. + rewrite wordize_and. + apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. + rewrite Z.land_spec. + rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption]. + rewrite N.land_spec. + repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]). + reflexivity. +Qed. Hint Rewrite @wordToN_wand using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wand using word_util_arith : pull_wordToN. Lemma wordToN_wor : bounds_2statement (@wor _) Z.lor. Proof. - admit. -Admitted. + intros. + rewrite wordize_or. + apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. + rewrite Z.lor_spec. + rewrite Z2N.inj_testbit; [|apply Z.ge_le; assumption]. + rewrite N.lor_spec. + repeat (rewrite <- Z2N.inj_testbit; [|apply Z.ge_le; assumption]). + reflexivity. +Qed. Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. +Local Notation bound n lower value upper := ( + (0 <= lower)%Z + /\ (lower <= Z.of_N (@wordToN n value))%Z + /\ (Z.of_N (@wordToN n value) <= upper)%Z). + +Definition valid_update n lowerF valueF upperF : Prop := + forall lower0 value0 upper0 + lower1 value1 upper1, + + bound n lower0 value0 upper0 + -> bound n lower1 value1 upper1 + -> (0 <= lowerF lower0 upper0 lower1 upper1)%Z + -> (Z.log2 (upperF lower0 upper0 lower1 upper1) < Z.of_nat n)%Z + -> bound n (lowerF lower0 upper0 lower1 upper1) + (valueF value0 value1) + (upperF lower0 upper0 lower1 upper1). + +Local Ltac add_mono := + etransitivity; [| apply Z.add_le_mono_r; eassumption]; omega. + +Lemma add_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => l0 + l1)%Z + (@wplus n) + (fun l0 u0 l1 u1 => u0 + u1)%Z. +Proof. + unfold valid_update; intros until upper1; intros B0 B1. + destruct B0 as [? B0], B1 as [? B1], B0, B1. + repeat split; [add_mono| |]; ( + rewrite wordToN_wplus; [add_mono|add_mono|]; + eapply Z.le_lt_trans; [| eassumption]; + apply Z.log2_le_mono; add_mono). +Qed. + +Local Ltac sub_mono := + etransitivity; + [| apply Z.sub_le_mono_r]; eauto; + first [ reflexivity + | apply Z.sub_le_mono_l; assumption + | apply Z.le_add_le_sub_l; etransitivity; [|eassumption]; + repeat rewrite Z.add_0_r; assumption]. + +Lemma sub_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => l0 - u1)%Z + (@wminus n) + (fun l0 u0 l1 u1 => u0 - l1)%Z. +Proof. + unfold valid_update; intros until upper1; intros B0 B1. + destruct B0 as [? B0], B1 as [? B1], B0, B1. + repeat split; [sub_mono| |]; ( + rewrite wordToN_wminus; [sub_mono|omega|]; + eapply Z.le_lt_trans; [apply Z.log2_le_mono|eassumption]; sub_mono). +Qed. + +Local Ltac mul_mono := + etransitivity; [|apply Z.mul_le_mono_nonneg_r]; + repeat first + [ eassumption + | reflexivity + | apply Z.mul_le_mono_nonneg_l + | rewrite Z.mul_0_l + | omega]. + +Lemma mul_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => l0 * l1)%Z + (@wmult n) + (fun l0 u0 l1 u1 => u0 * u1)%Z. +Proof. + unfold valid_update; intros until upper1; intros B0 B1. + destruct B0 as [? B0], B1 as [? B1], B0, B1. + repeat split; [mul_mono| |]; ( + rewrite wordToN_wmult; [mul_mono|mul_mono|]; + eapply Z.le_lt_trans; [| eassumption]; + apply Z.log2_le_mono; mul_mono). +Qed. + +Local Ltac solve_land_ge0 := + apply Z.land_nonneg; left; etransitivity; [|eassumption]; assumption. + +Local Ltac land_mono := + first [assumption | etransitivity; [|eassumption]; assumption]. + +Lemma land_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => 0)%Z + (@wand n) + (fun l0 u0 l1 u1 => Z.min u0 u1)%Z. +Proof. + unfold valid_update; intros until upper1; intros B0 B1. + destruct B0 as [? B0], B1 as [? B1], B0, B1. + repeat split; [reflexivity| |]. + + - rewrite wordToN_wand; [solve_land_ge0|solve_land_ge0|]. + eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|]; + eapply Z.le_lt_trans; [| eassumption]; + repeat match goal with + | [|- context[Z.min ?a ?b]] => + destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g + end; apply Z.log2_le_mono; try assumption. + + admit. admit. + + - rewrite wordToN_wand; [|solve_land_ge0|]. + eapply Z.le_lt_trans; [apply Z.log2_land; land_mono|]; + match goal with + | [|- (Z.min ?a ?b < _)%Z] => + destruct (Z.min_dec a b) as [g|g]; rewrite g; clear g + end. + + . + (* +[apply N2Z.is_nonneg|]; + unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id; + rewrite wordize_and. + + destruct (Z_ge_dec upper1 upper0) as [g|g]. + + - rewrite Z.min_r; [|abstract (apply Z.log2_le_mono; omega)]. + abstract ( + rewrite (land_intro_ones (wordToN value0)); + rewrite N.land_assoc; + etransitivity; [apply N2Z.inj_le; apply N.lt_le_incl; apply land_lt_Npow2|]; + rewrite N2Z.inj_pow; + apply Z.pow_le_mono; [abstract (split; cbn; [omega|reflexivity])|]; + unfold getBits; rewrite N2Z.inj_succ; + apply -> Z.succ_le_mono; + rewrite <- (N2Z.id (wordToN value0)), <- log2_conv; + apply Z.log2_le_mono; + etransitivity; [eassumption|reflexivity]). + + - rewrite Z.min_l; [|abstract (apply Z.log2_le_mono; omega)]. + abstract ( + rewrite (land_intro_ones (wordToN value1)); + rewrite <- N.land_comm, N.land_assoc; + etransitivity; [apply N2Z.inj_le; apply N.lt_le_incl; apply land_lt_Npow2|]; + rewrite N2Z.inj_pow; + apply Z.pow_le_mono; [abstract (split; cbn; [omega|reflexivity])|]; + unfold getBits; rewrite N2Z.inj_succ; + apply -> Z.succ_le_mono; + rewrite <- (N2Z.id (wordToN value1)), <- log2_conv; + apply Z.log2_le_mono; + etransitivity; [eassumption|reflexivity]). + +*) +Admitted. + +Lemma lor_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => Z.max l0 l1)%Z + (@wor n) + (fun l0 u0 l1 u1 => 2^(Z.max (Z.log2 (u0+1)) (Z.log2 (u1+1))) - 1)%Z. +Proof. +(* unfold Word64.word64ToZ in *; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id; + rewrite wordize_or. + + - transitivity (Z.max (Z.of_N (wordToN value1)) (Z.of_N (wordToN value0))); + [ abstract (destruct + (Z_ge_dec lower1 lower0) as [l|l], + (Z_ge_dec (Z.of_N (& value1)%w) (Z.of_N (& value0)%w)) as [v|v]; + [ rewrite Z.max_l, Z.max_l | rewrite Z.max_l, Z.max_r + | rewrite Z.max_r, Z.max_l | rewrite Z.max_r, Z.max_r ]; + + try (omega || assumption)) + | ]. + + rewrite <- N2Z.inj_max. + apply Z2N.inj_le; [apply N2Z.is_nonneg|apply N2Z.is_nonneg|]. + repeat rewrite N2Z.id. + + abstract ( + destruct (N.max_dec (wordToN value1) (wordToN value0)) as [v|v]; + rewrite v; + apply N.ldiff_le, N.bits_inj_iff; intros k; + rewrite N.ldiff_spec, N.lor_spec; + induction (N.testbit (wordToN value1)), (N.testbit (wordToN value0)); simpl; + reflexivity). + + - apply Z.lt_le_incl, Z.log2_lt_cancel. + rewrite Z.log2_pow2; [| abstract ( + destruct (Z.max_dec (Z.log2 upper1) (Z.log2 upper0)) as [g|g]; + rewrite g; apply Z.le_le_succ_r, Z.log2_nonneg)]. + + eapply (Z.le_lt_trans _ (Z.log2 (Z.lor _ _)) _). + + + apply Z.log2_le_mono, Z.eq_le_incl. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit, Z.lor_spec, N.lor_spec; [|assumption]. + repeat (rewrite <- Z2N.inj_testbit; [|assumption]). + reflexivity. + + + abstract ( + rewrite Z.log2_lor; [|trans'|trans']; + destruct + (Z_ge_dec (Z.of_N (wordToN value1)) (Z.of_N (wordToN value0))) as [g0|g0], + (Z_ge_dec upper1 upper0) as [g1|g1]; + [ rewrite Z.max_l, Z.max_l + | rewrite Z.max_l, Z.max_r + | rewrite Z.max_r, Z.max_l + | rewrite Z.max_r, Z.max_r]; + try apply Z.log2_le_mono; try omega; + apply Z.le_succ_l; + apply -> Z.succ_le_mono; + apply Z.log2_le_mono; + assumption || (etransitivity; [eassumption|]; omega)). +*) +Admitted. + +Lemma shr_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => Z.shiftr l0 u1)%Z + (@wordBin N.shiftr n) + (fun l0 u0 l1 u1 => Z.shiftr u0 l1)%Z. +Proof. + (* + Ltac shr_mono := etransitivity; + [apply Z.div_le_compat_l | apply Z.div_le_mono]. + + assert (forall x, (0 <= x)%Z -> (0 < 2^x)%Z) as gt0. { + intros; rewrite <- (Z2Nat.id x); [|assumption]. + induction (Z.to_nat x) as [|n]; [cbv; auto|]. + eapply Z.lt_le_trans; [eassumption|rewrite Nat2Z.inj_succ]. + apply Z.pow_le_mono_r; [cbv; auto|omega]. + } + + build_binop Word64.w64shr ZBounds.shr; t_start; abstract ( + unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id; + rewrite Z.shiftr_div_pow2 in *; + repeat match goal with + | [|- _ /\ _ ] => split + | [|- (0 <= 2 ^ _)%Z ] => apply Z.pow_nonneg + | [|- (0 < 2 ^ ?X)%Z ] => apply gt0 + | [|- (0 <= _ / _)%Z ] => apply Z.div_le_lower_bound; [|rewrite Z.mul_0_r] + | [|- (2 ^ _ <= 2 ^ _)%Z ] => apply Z.pow_le_mono_r + | [|- context[(?a >> ?b)%Z]] => rewrite Z.shiftr_div_pow2 in * + | [|- (_ < Npow2 _)%N] => + apply N2Z.inj_lt, Z.log2_lt_cancel; simpl; + eapply Z.le_lt_trans; [|eassumption]; apply Z.log2_le_mono; rewrite Z2N.id + + | _ => progress shr_mono + | _ => progress trans' + | _ => progress omega + end). + +*) +Admitted. + +Lemma shl_valid_update: forall n, + valid_update n + (fun l0 u0 l1 u1 => Z.shiftl l0 l1)%Z + (@wordBin N.shiftl n) + (fun l0 u0 l1 u1 => Z.shiftl u0 u1)%Z. +Proof. + (* + Ltac shl_mono := etransitivity; + [apply Z.mul_le_mono_nonneg_l | apply Z.mul_le_mono_nonneg_r]. + + build_binop Word64.w64shl ZBounds.shl; t_start; abstract ( + unfold Word64.word64ToZ; repeat rewrite wordToN_NToWord; repeat rewrite Z2N.id; + rewrite Z.shiftl_mul_pow2 in *; + repeat match goal with + | [|- (0 <= 2 ^ _)%Z ] => apply Z.pow_nonneg + | [|- (0 <= _ * _)%Z ] => apply Z.mul_nonneg_nonneg + | [|- (2 ^ _ <= 2 ^ _)%Z ] => apply Z.pow_le_mono_r + | [|- context[(?a << ?b)%Z]] => rewrite Z.shiftl_mul_pow2 + | [|- (_ < Npow2 _)%N] => + apply N2Z.inj_lt, Z.log2_lt_cancel; simpl; + eapply Z.le_lt_trans; [|eassumption]; apply Z.log2_le_mono; rewrite Z2N.id + + | _ => progress shl_mono + | _ => progress trans' + | _ => progress omega + end). + +*) +Admitted. + + Axiom wlast : forall sz, word (sz+1) -> bool. Arguments wlast {_} _. Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _. Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)), diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 17e8d62bf..d6ffa4a53 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2911,6 +2911,44 @@ for name in names: Module RemoveEquivModuloInstances (dummy : Nop). Global Remove Hints equiv_modulo_Reflexive equiv_modulo_Symmetric equiv_modulo_Transitive mul_mod_Proper add_mod_Proper sub_mod_Proper opp_mod_Proper modulo_equiv_modulo_Proper eq_to_ProperProxy : typeclass_instances. End RemoveEquivModuloInstances. + + Module N2Z. + Require Import Coq.NArith.NArith. + + Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftl_spec; [|assumption]. + + assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( + unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; + intro H; inversion H). + + destruct g as [g|g]; + [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] + | rewrite N.shiftl_spec_low]; try assumption. + + - rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. + + - apply N2Z.inj_lt in g. + rewrite Z2N.id in g; [symmetry|assumption]. + apply Z.testbit_neg_r; omega. + Qed. + + Lemma inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. + rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_add; f_equal. + apply Z2N.id; assumption. + Qed. + End N2Z. End Z. Module Export BoundsTactics. |