From eb85803875c5a4e90be60d870f01fac380ca18b0 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 16 Jun 2019 18:55:17 +0200
Subject: Relax lemma Val.zero_ext_and and add Val.zero_ext_andl

---
 common/Values.v | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index 52474f99..de317734 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1910,10 +1910,18 @@ Qed.
 
 Lemma zero_ext_and:
   forall n v,
-  0 < n < Int.zwordsize ->
+  0 <= n ->
   Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))).
 Proof.
-  intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega.
+  intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto.
+Qed.
+
+Lemma zero_ext_andl:
+  forall n v,
+  0 <= n ->
+  Val.zero_ext_l n v = Val.andl v (Vlong (Int64.repr (two_p n - 1))).
+Proof.
+  intros. destruct v; simpl; auto. decEq. apply Int64.zero_ext_and; auto.
 Qed.
 
 Lemma rolm_lt_zero:
-- 
cgit