most of jgross' admits

'

1 files changed, 20 insertions, 0 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))).