most of jgross' admits

'

3 files changed, 146 insertions, 18 deletions

diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v
index 6526c94ac..f12c6449d 100644
--- a/src/Assembly/WordizeUtil.v
+++ b/src/Assembly/WordizeUtil.v
@@ -252,6 +252,11 @@ 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.
@@ -926,6 +931,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 5c75e35be..1732e036b 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Tactics.
 Require Import Bedrock.Word.
+Require Import Crypto.Assembly.WordizeUtil.
 Require Import Crypto.Util.WordUtil.
 Export Reflection.Syntax.Notations.
 
@@ -40,9 +41,9 @@ Module Word64.
   Definition w64minus : word64 -> word64 -> word64 := @wminus _.
   Definition w64mul : word64 -> word64 -> word64 := @wmult _.
   Definition w64shl : word64 -> word64 -> word64
-    := fun x y => NToWord _ (Z.to_N (Z.shiftl (Z.of_N (wordToN x)) (Z.of_N (wordToN x)))).
+    := fun x y => NToWord _ (Z.to_N (Z.shiftl (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))).
   Definition w64shr : word64 -> word64 -> word64
-    := fun x y => NToWord _ (Z.to_N (Z.shiftr (Z.of_N (wordToN x)) (Z.of_N (wordToN x)))).
+    := fun x y => NToWord _ (Z.to_N (Z.shiftr (Z.of_N (wordToN x)) (Z.of_N (wordToN y)))).
   Definition w64land : word64 -> word64 -> word64 := @wand _.
   Definition w64lor : word64 -> word64 -> word64 := @wor _.
   Definition w64neg : word64 -> word64 -> word64 (* TODO: FIXME? *)
@@ -72,17 +73,69 @@ Module Word64.
             -> Z.log2 (Zop (word64ToZ x) (word64ToZ y)) < Z.of_nat bit_width
             -> word64ToZ (wop x y) = (Zop (word64ToZ x) (word64ToZ y)))%Z).
 
+  Require Import Crypto.Assembly.WordizeUtil.
+
   Lemma word64ToZ_w64plus : bounds_2statement w64plus Z.add. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_w64minus : bounds_2statement w64minus Z.sub. Proof. w64ToZ_t. Qed.
   Lemma word64ToZ_w64mul : bounds_2statement w64mul Z.mul. Proof. w64ToZ_t. Qed.
+  Lemma word64ToZ_w64land : bounds_2statement w64land Z.land. Proof. w64ToZ_t. Qed.
+  Lemma word64ToZ_w64lor : bounds_2statement w64lor Z.lor. Proof. w64ToZ_t. Qed.
+
   Lemma word64ToZ_w64shl : bounds_2statement w64shl Z.shiftl.
-  Proof. w64ToZ_t. admit. Admitted.
+  Proof.
+    intros x y H H0.
+    w64ToZ_t.
+
+    destruct (N.eq_dec (Z.to_N (Z.of_N (wordToN x) << Z.of_N (wordToN y))) 0%N) as [e|e]; [
+      rewrite e; rewrite wordToN_NToWord; [|apply Npow2_gt0];
+      rewrite <- e; rewrite Z2N.id; [reflexivity|assumption]
+    | apply N.neq_0_lt_0 in e].
+
+    apply Z.bits_inj_iff'; intros k Hpos.
+    rewrite Z.shiftl_spec; [|assumption].
+    rewrite Z2N.inj_testbit; [|assumption].
+    rewrite wordToN_NToWord.
+
+    - rewrite <- N2Z.inj_testbit.
+      rewrite (Z2N.id k); [|assumption].
+      rewrite Z2N.id; [|assumption].
+      rewrite Z.shiftl_spec; [reflexivity|assumption].
+
+    - rewrite Npow2_N.
+      apply N.log2_lt_pow2; [assumption|].
+      apply N2Z.inj_lt.
+      rewrite nat_N_Z.
+      refine (Z.le_lt_trans _ _ _ _ H0).
+      rewrite log2_conv; reflexivity.
+  Qed.
+
   Lemma word64ToZ_w64shr : bounds_2statement w64shr Z.shiftr.
-  Proof. admit. Admitted.
-  Lemma word64ToZ_w64land : bounds_2statement w64land Z.land.
-  Proof. w64ToZ_t. Qed.
-  Lemma word64ToZ_w64lor : bounds_2statement w64lor Z.lor.
-  Proof. w64ToZ_t. Qed.
+  Proof.
+    intros x y H H0.
+    w64ToZ_t.
+
+    destruct (N.eq_dec (Z.to_N (Z.of_N (wordToN x) >> Z.of_N (wordToN y))) 0%N) as [e|e]; [
+      rewrite e; rewrite wordToN_NToWord; [|apply Npow2_gt0];
+      rewrite <- e; rewrite Z2N.id; [reflexivity|assumption]
+    | apply N.neq_0_lt_0 in e].
+
+    apply Z.bits_inj_iff'; intros k Hpos.
+    rewrite Z.shiftr_spec; [|assumption].
+    rewrite Z2N.inj_testbit; [|assumption].
+    rewrite wordToN_NToWord.
+
+    - rewrite <- N2Z.inj_testbit.
+      rewrite (Z2N.id k); [|assumption].
+      rewrite Z2N.id; [|assumption].
+      rewrite Z.shiftr_spec; [reflexivity|assumption].
+
+    - rewrite Npow2_N.
+      apply N.log2_lt_pow2; [assumption|].
+      apply N2Z.inj_lt.
+      rewrite nat_N_Z.
+      refine (Z.le_lt_trans _ _ _ _ H0).
+      rewrite log2_conv; reflexivity.
+  Qed.
 
   Definition interp_base_type (t : base_type) : Type
     := match t with
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index fd2e5e098..5f4dc9c7a 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -277,37 +277,92 @@ Local Notation bounds_2statement wop Zop
           -> 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.