diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-08 13:40:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-08 13:40:24 -0400 |
| commit | 3c674d6d86483bf6e0647c5662b63581c3777011 (patch) | |
| tree | a0bcc2c1d45c00f5de58472254299c2090803c05 /src/Compilers/Z/Syntax/Util.v | |
| parent | 655b67f9600b862447d7f0bcf271a41d50c2e32a (diff) | |
Add interpToZ_range
Diffstat (limited to 'src/Compilers/Z/Syntax/Util.v')
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 3e442b4d8..26803e851 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -180,6 +180,16 @@ Proof. congruence. Qed. +Lemma interpToZ_range {a} (v : interp_base_type a) + : match a with + | TZ => True + | TWord lgsz => 0 <= interpToZ v < 2^Z.of_nat (2^lgsz) + end%Z. +Proof. + destruct a; trivial; simpl. + apply wordToZ_range. +Qed. + Lemma make_const_correct : forall T v, interp_op Unit (Tbase T) (make_const T v) tt = v. Proof. destruct T; cbv -[FixedWordSizes.ZToWord FixedWordSizes.wordToZ FixedWordSizes.wordT]; |