From 598ae72e8653a20cfa3e1ded0d6e1aedf6323f18 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Mar 2017 18:41:49 -0400 Subject: Add wordToZ{_gen,}_range --- src/Util/FixedWordSizesEquality.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/FixedWordSizesEquality.v') diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 8c5b1ead0..e1a8f1f79 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -262,6 +262,13 @@ Ltac fixed_size_op_to_word := repeat autounfold with fixed_size_constants in *; syntactic_fixed_size_op_to_word. +Lemma wordToZ_gen_range {sz} w : (0 <= @wordToZ_gen sz w < 2^Z.of_nat sz)%Z. +Proof. apply WordNZ_range; reflexivity. Qed. + +Lemma wordToZ_range {logsz} w : (0 <= @wordToZ logsz w < 2^Z.of_nat (2^logsz))%Z. +Proof. + generalize (@wordToZ_gen_range (2^logsz)); wordToZ_word_case_dep_t. +Qed. Section log_Updates. Local Notation bound n lower value upper := ( -- cgit v1.2.3