diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 9 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
2 files changed, 10 insertions, 0 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 809f9d89..7e4abe29 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -185,10 +185,19 @@ assert ((Z.to_nat m <= Z.to_nat n)%nat). { apply Z2Nat.inj_le; omega. } omega. Qed. +Lemma truncateLSB_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat. +intros. +assert ((Z.to_nat m <= Z.to_nat n)%nat). +{ apply Z2Nat.inj_le; omega. } +omega. +Qed. Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m := cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m). +Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m := + cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m). + Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b. intros. rewrite Nat2Z.inj_add. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e3e039c2..2eabacb3 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -9,6 +9,7 @@ Require Export List. Require Export Sumbool. Require Export DecidableClass. Require Import Eqdep_dec. +Require Export Zeuclid. Import ListNotations. Open Scope Z. |