diff options
Diffstat (limited to 'common/Memdata.v')
-rw-r--r-- | common/Memdata.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 1bd87169..c80b3754 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -24,6 +24,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Lia. (** * Properties of memory chunks *) @@ -45,6 +46,13 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Many64 => 8 end. +Definition largest_size_chunk := 8. + +Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. +Proof. + destruct chunk; simpl; lia. +Qed. + Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. |