Merge branch 'riscv:master' into master

Makefile

@@ -369,7 +369,7 @@ ifndef EXPLICIT_COQ_SAIL
   EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
 endif
 
-COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R generated_definitions/coq '' -R handwritten_support ''
+COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common
 ifeq ($(EXPLICIT_COQ_BBV),yes)
   COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
 endif

handwritten_support/riscv_extras.v

@@ -69,6 +69,7 @@
 Require Import Sail.Base.
 Require Import String.
 Require Import List.
+Require Import Lia.
 Import List.ListNotations.
 Open Scope Z.
 
@@ -190,7 +191,7 @@ unbool_comparisons.
 unbool_comparisons_goal.
 assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
 rewrite <- H at 3.
-lapply (ZEuclid.mod_always_pos m n); omega.
+lapply (ZEuclid.mod_always_pos m n); lia.
 Qed.
 
 (* Override the more general version *)
@@ -210,13 +211,14 @@ Axiom sys_enable_writable_misa : unit -> bool.
 Axiom sys_enable_rvc : unit -> bool.
 Axiom sys_enable_fdext : unit -> bool.
 Axiom sys_enable_next : unit -> bool.
+Axiom sys_enable_zfinx : unit -> bool.
 
 (* The constraint solver can do this itself, but a Coq bug puts
    anonymous_subproof into the term instead of an actual subproof. *)
 Lemma n_leading_spaces_fact {w__0} :
   w__0 >= 0 -> exists ex17629_ : Z, 1 + w__0 = 1 + ex17629_ /\ 0 <= ex17629_.
 intro.
 exists w__0.
-omega.
+lia.
 Qed.
 Hint Resolve n_leading_spaces_fact : sail.