Coq: add zeros library function (used by MIPS)

1 files changed, 7 insertions, 0 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index e37e9d26..809f9d89 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -172,6 +172,13 @@ Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n
 
 Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v.
 
+Definition zeros (n : Z) `{ArithFact (n >= 0)} : mword n.
+refine (cast_to_mword (Word.wzero (Z.to_nat n)) _).
+unwrap_ArithFacts.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
+
 Lemma truncate_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat.
 intros.
 assert ((Z.to_nat m <= Z.to_nat n)%nat).