Fixing a lot of deprecated stuff + warnings. Bump checkout code.

.github/workflows/test.yml

@@ -1,4 +1,4 @@
-name: "Build vellvm"
+name: "Nix build for vellvm"
 on:
   pull_request:
   push:

.github/workflows/vellvm.yml

@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout Code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Compiling Vellvm
         uses: coq-community/docker-coq-action@v1

src/coq/Analysis/Dom.v

@@ -52,34 +52,34 @@ Module BoundedSet(Import S:FSetInterface.WS) <: LATTICE.
   #[global] Instance eq_equiv : Equivalence eq.
   Proof.
     constructor.
-    red. destruct x; simpl; intuition.
-    red. destruct x, y; simpl; intros; intuition.
-    red. destruct x, y, z; simpl; intros; intuition.
+    red. destruct x; simpl; intuition auto with *.
+    red. destruct x, y; simpl; intros; intuition auto with *.
+    red. destruct x, y, z; simpl; intros; intuition auto with *.
     transitivity t1; auto.
   Qed.
 
   #[global] Instance le_preorder : PreOrder le.
   Proof.
     constructor.
-    red. destruct x; simpl; intuition.
-    red. destruct x, y, z; simpl; intros; intuition.
+    red. destruct x; simpl; intuition auto with *.
+    red. destruct x, y, z; simpl; intros; intuition auto with *.
     transitivity t1; auto.
   Qed.
 
   #[global] Instance le_poset : PartialOrder eq le.
   Proof.
     constructor.
     intro. repeat red. split.
-    destruct x, x0; simpl in *; intuition.
+    destruct x, x0; simpl in *; intuition auto with *.
     unfold Subset. intros. rewrite H; auto.
-    red. destruct x, x0; simpl in *; intuition.
+    red. destruct x, x0; simpl in *; intuition auto with *.
     unfold Subset. intros. rewrite <- H. auto.
 
     destruct x, x0; simpl;
       intros H; repeat red in H; simpl in H;
-      intuition.
+      intuition auto with *.
     repeat red in H1. repeat red in H0.
-    red; intuition.
+    red; intuition auto with *.
   Qed.
 
   Definition eq_dec : forall x y, {x == y} + {x ~= y}.
@@ -300,7 +300,7 @@ Module Spec (Import G:GRAPH).
     mem g v2 -> edge g v1 v2 -> forall v', SDom g v' v2 -> Dom g v' v1.
   Proof.
     unfold SDom, Dom. intros g v1 v2 Hmem Hsucc v' [Hneq Hdom] p Hp.
-    cut (In v' (v2::p)). inversion 1; subst; intuition.
+    cut (In v' (v2::p)). inversion 1; subst; intuition auto with *.
     apply Hdom. eapply path_cons; eauto.
   Qed.
 
@@ -345,7 +345,7 @@ Module AlgdomProperties (Import G:GRAPH) (Import A : Algdom G).
     destruct (sdom (entry g)); try contradiction; simpl in *.
       exfalso. rewrite H2 in H0. eapply L.SFacts.empty_iff. eauto.
 
-    right. destruct (E.eq_dec v2 n1). subst. inversion H1; intuition.
+    right. destruct (E.eq_dec v2 n1). subst. inversion H1; intuition auto with *.
     apply IHPath; auto.
 
     destruct (sdom v2) eqn:Heqv2; simpl in *; auto.

src/coq/Analysis/DomKildall.v

@@ -99,7 +99,7 @@ Module AlgdomKildall (PC:UsualDecidableType) (Import G: GRAPH with Definition V
     assert (In n1 (enum_vs g) \/ NM.In n1 (NM.empty L.t))
            as Hin by exact (or_introl H0).
     generalize (enum_vs g) (NM.empty L.t) Hin.
-    induction l; simpl. intuition.
+    induction l; simpl. intuition auto with *.
     intros to Hin'. destruct Hin' as [[? | ?] | ?]; subst; auto.
     apply FMF.add_in_iff; auto.
     destruct (N.eq_dec a n1).

src/coq/Handlers/Concretization.v

@@ -1679,7 +1679,7 @@ Module MakeBase (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP.A
         induction uvs; try reflexivity.
       Qed.
 
-      Fixpoint eval_select
+      Definition eval_select
         (cnd : dvalue) (v1 v2 : uvalue) : M dvalue
         := match cnd with
            | DVALUE_Poison t =>

src/coq/Handlers/MemoryModel.v

@@ -2,6 +2,14 @@ From Vellvm.Syntax Require Import
      DataLayout
      DynamicTypes.
 
+From ITree Require Import
+     ITree
+     Basics.Basics
+     Events.Exception
+     Eq.Eqit
+     Events.StateFacts
+     Events.State.
+
 From Vellvm.Semantics Require Import
   DynamicValues
   VellvmIntegers
@@ -59,7 +67,10 @@ Import Utils.Monads.
 Import Basics.Basics.Monads.
 Import MonadNotation.
 
+Import Monad.
+Import EitherMonad.
 
+From Coq Require Import FunctionalExtensionality.
 
 Module Type MemoryModelSpecPrimitives (LP : LLVMParams) (MP : MemoryParams LP).
   Import LP.Events.
@@ -378,9 +389,6 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
       reflexivity.
   Qed.
 
-  Require Import MonadReturnsLaws.
-  Import Monad.
-
   Lemma intptr_seq_nil_len :
     forall start len,
       intptr_seq start len = NoOom [] ->
@@ -582,7 +590,7 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
           erewrite IP.from_Z_to_Z in YEQ; eauto.
           replace (1 + Z.of_nat (S len') - 1)%Z with (Z.of_nat (S len'))%Z in YEQ by lia.
           auto.
-      + assert (eq1 (NoOom (l ++ [x])) (map_monad (fun ip : IP.intptr => IP.from_Z (IP.to_Z ip + 1)) (l_shifted ++ [y]))) as EQ.
+      + assert (Monad.eq1 (NoOom (l ++ [x])) (map_monad (fun ip : IP.intptr => IP.from_Z (IP.to_Z ip + 1)) (l_shifted ++ [y]))) as EQ.
         { rewrite map_monad_app.
           cbn.
           rewrite <- MAP_SHIFTED.
@@ -665,9 +673,9 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
       {Pre Post : Type}
       {B} `{MB : Monad B}
       `{WM : @Within M EQM B Pre Post}
-      `{EQV : @Eq1Equivalence M HM EQM}
+      `{EQV : @Monad.Eq1Equivalence M HM EQM}
       `{WRET : @Within_ret_inv M B Pre Post HM _ EQM WM}
-      `{MLAWS : @MonadLawsE M EQM HM}
+      `{MLAWS : @Monad.MonadLawsE M EQM HM}
       `{OOM: RAISE_OOM M} `{ERR: RAISE_ERROR M}
       `{RBMOOM : @RaiseBindM M HM EQM string (@raise_oom M OOM)}
       `{RBMERR : @RaiseBindM M HM EQM string (@raise_error M ERR)}
@@ -684,7 +692,7 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
     destruct (intptr_seq 0 len) eqn:SEQ.
     - (* No OOM *)
       cbn in *.
-      setoid_rewrite bind_ret_l in CONSEC.
+      setoid_rewrite Monad.bind_ret_l in CONSEC.
 
       (* rewrite bind_ret_l in CONSEC. *)
       destruct (map_monad (fun ix : IP.intptr => handle_gep_addr (DTYPE_I 8) ptr [DVALUE_IPTR ix]) l) eqn:HMAPM.
@@ -696,7 +704,7 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
         eapply rw_ret_nin_raise in CONSEC; [contradiction | auto].
       + cbn in CONSEC.
         convert_to_ret_hyp.
-        setoid_rewrite bind_ret_l in CONSEC.
+        setoid_rewrite Monad.bind_ret_l in CONSEC.
         destruct (sequence l0) eqn:HSEQUENCE.
         { cbn in CONSEC.
           apply within_ret_ret in CONSEC; auto.
@@ -722,14 +730,14 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
   Qed.
 
   Lemma get_consecutive_ptrs_covers_range :
-    forall {M} `{HM : Monad M} `{OOM : RAISE_OOM M} `{ERR : RAISE_ERROR M} `{EQM : Eq1 M}
+    forall {M} `{HM : Monad M} `{OOM : RAISE_OOM M} `{ERR : RAISE_ERROR M} `{EQM : Monad.Eq1 M}
       {Pre Post : Type}
       {B} `{MB : Monad B}
       `{WM : @Within M EQM B Pre Post}
-      `{EQV : @Eq1Equivalence M HM EQM}
+      `{EQV : @Monad.Eq1Equivalence M HM EQM}
       `{EQRET : @Eq1_ret_inv M EQM HM}
       `{WRET : @Within_ret_inv M B Pre Post HM _ EQM WM}
-      `{LAWS : @MonadLawsE M EQM HM}
+      `{LAWS : @Monad.MonadLawsE M EQM HM}
       `{RBMOOM : @RaiseBindM M HM EQM string (@raise_oom M OOM)}
       `{RBMERR : @RaiseBindM M  HM EQM string (@raise_error M ERR)}
       `{RWOOM : @RaiseWithin M B _ _ _ EQM WM string (@raise_oom M OOM)}
@@ -758,7 +766,7 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
         setoid_rewrite rbm_raise_bind in CONSEC; auto.
         eapply rw_ret_nin_raise in CONSEC; [contradiction | try typeclasses eauto].
       + cbn in CONSEC.
-        setoid_rewrite bind_ret_l in CONSEC.
+        setoid_rewrite Monad.bind_ret_l in CONSEC.
         rename l0 into addrs.
         destruct (sequence addrs) eqn:HSEQUENCE.
         { apply within_ret_ret in CONSEC; eauto.
@@ -2274,8 +2282,6 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
       lia.
     Defined.
 
-    From Coq Require Import FunctionalExtensionality.
-
     Lemma re_sid_ubytes_helper_equation {M} `{Monad M} `{MonadStoreId M} `{RAISE_ERROR M}
           (bytes : list (N * SByte)) (acc : NMap SByte) :
       re_sid_ubytes_helper bytes acc =
@@ -2668,16 +2674,6 @@ Module MemoryHelpers (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule
   End Serialization.
 End MemoryHelpers.
 
-
-From ITree Require Import
-     ITree
-     Basics.Basics
-     Events.Exception
-     Eq.Eqit
-     Events.StateFacts
-     Events.State.
-
-
 Module Type MemoryModelSpec (LP : LLVMParams) (MP : MemoryParams LP) (MMSP : MemoryModelSpecPrimitives LP MP).
   Import LP.
   Import LP.Events.
@@ -4125,22 +4121,12 @@ Module MakeMemoryModelSpec (LP : LLVMParams) (MP : MemoryParams LP) (MMSP : Memo
 End MakeMemoryModelSpec.
 
 Module Type MemoryExecMonad (LP : LLVMParams) (MP : MemoryParams LP) (MMSP : MemoryModelSpecPrimitives LP MP) (MMS : MemoryModelSpec LP MP MMSP).
-  (* TODO: move these imports *)
-  Import EitherMonad.
-  Import Monad.
-  Require Import Morphisms.
-  From Vellvm Require Import
-       MonadEq1Laws
-       Raise.
-
   Import LP.
+  Import MMS.
   Import PROV.
   Import MMSP.
-  Import MMS.
   Import MemHelpers.
 
-  Require Import Within.
-
   Definition MemMonad_valid_state (ms : MemState) (st : store_id) : Prop
     := let sid := st in
        (forall sid', used_store_id_prop ms sid' -> (sid' < sid)%N).
@@ -4153,22 +4139,22 @@ Module Type MemoryExecMonad (LP : LLVMParams) (MP : MemoryParams LP) (MMSP : Mem
         `{EQM : Eq1 M} `{EQRI : @Eq1_ret_inv M EQM MM} `{MLAWS : @MonadLawsE M EQM MM}
     : Type
     :=
-    { MemMonad_eq1_runm :> Eq1 RunM;
-      MemMonad_runm_monadlaws :> MonadLawsE RunM;
-      MemMonad_eq1_runm_equiv :> Eq1Equivalence RunM;
-      MemMonad_eq1_runm_eq1laws :> Eq1_ret_inv RunM;
-      MemMonad_raisebindm_ub :> RaiseBindM RunM string (@raise_ub RunM RunUB);
-      MemMonad_raisebindm_oom :> RaiseBindM RunM string (@raise_oom RunM RunOOM);
-      MemMonad_raisebindm_err :> RaiseBindM RunM string (@raise_error RunM RunERR);
-      MemMonad_within :> @Within M EQM RunM (store_id * MemState)%type (store_id * MemState)%type;
-
-      MemMonad_eq1_runm_proper :>
+    { #[global] MemMonad_eq1_runm :: Eq1 RunM;
+      #[global] MemMonad_runm_monadlaws :: MonadLawsE RunM;
+      #[global] MemMonad_eq1_runm_equiv :: Eq1Equivalence RunM;
+      #[global] MemMonad_eq1_runm_eq1laws :: Eq1_ret_inv RunM;
+      #[global] MemMonad_raisebindm_ub :: RaiseBindM RunM string (@raise_ub RunM RunUB);
+      #[global] MemMonad_raisebindm_oom :: RaiseBindM RunM string (@raise_oom RunM RunOOM);
+      #[global] MemMonad_raisebindm_err :: RaiseBindM RunM string (@raise_error RunM RunERR);
+      #[global] MemMonad_within :: @Within M EQM RunM (store_id * MemState)%type (store_id * MemState)%type;
+
+      #[global] MemMonad_eq1_runm_proper ::
                                (forall A, Proper ((@eq1 _ MemMonad_eq1_runm) A ==> (@eq1 _ MemMonad_eq1_runm) A ==> iff) ((@eq1 _ MemMonad_eq1_runm) A));
 
       MemMonad_run {A} (ma : M A) (ms : MemState) (st : store_id)
       : RunM (store_id * (MemState * A))%type;
 
-      MemMonad_run_proper :>
+      #[global] MemMonad_run_proper ::
         (forall A, Proper (@eq1 _ EQM A ==> eq ==> eq ==> @eq1 _ MemMonad_eq1_runm (store_id * (MemState * A))) MemMonad_run);
 
       (** Some lemmas about valid states *)
@@ -4623,10 +4609,6 @@ Module Type MemoryExecMonad (LP : LLVMParams) (MP : MemoryParams LP) (MMSP : Mem
              (@within MemM _ err_ub_oom (store_id * MemState)%type (store_id * MemState)%type WEM X exec (st, ms) e (st', ms')) /\
                (e {{ms}} ∈ {{ms'}} spec) /\ ((exists x, e = ret x) -> (MemMonad_valid_state ms' st' /\ (exists x, e = ret x /\ post ms st x ms' st')))).
 
-  Require Import Error.
-  Require Import MonadReturnsLaws.
-
-
   (* TODO: Move this *)
   Lemma exec_correct_weaken_pre :
     forall {MemM Eff} `{MEMM : MemMonad MemM (itree Eff)}
@@ -7934,7 +7916,6 @@ Module MemStateInfiniteHelpers (LP : LLVMParamsBig) (MP : MemoryParams LP) (MMSP
 
       destruct IHl as (ips & IHl).
       exists (i :: ips).
-      Require Import FunctionalExtensionality.
       setoid_rewrite functional_extensionality.
       rewrite IHl.
       reflexivity.

src/coq/Handlers/MemoryModules/FiniteExecPrimitives.v

@@ -62,6 +62,8 @@ From ITree Require Import
      ITree
      Eq.Eqit.
 
+Require Import Error.
+
 Import ListNotations.
 
 Import MonadNotation.
@@ -3691,8 +3693,6 @@ Module FiniteMemoryModelExecPrimitives (LP : LLVMParams) (MP : MemoryParams LP)
       solve_fresh_provenance_invariants.
     Qed.
 
-    Require Import Error.
-
     Lemma byte_allocated_add_all_index :
       forall (ms : MemState) (mem : memory) (bytes : list mem_byte) (ix : Z) (aid : AllocationId),
         mem_state_memory ms = add_all_index bytes ix mem ->

src/coq/Handlers/MemoryModules/Within.v

@@ -20,7 +20,7 @@ Open Scope monad_scope.
 (* Whether a monadic computation M contains something in B *)
 Class Within (M : Type -> Type) `{EQM : Eq1 M} (B : Type -> Type) (PreState PostState : Type) : Type :=
   { within {A} (m : M A) (pre : PreState) (b : B A) (post : PostState) : Prop;
-    within_eq1_Proper {A} :>
+    #[global] within_eq1_Proper {A} ::
       Proper (@eq1 M EQM A ==> eq ==> eq ==> eq ==> iff) within;
   }.
 

src/coq/Handlers/Pick.v

@@ -44,6 +44,8 @@ From ExtLib Require Import
   Data.Monads.IdentityMonad
   Structures.Functor.
 
+Require Import ContainsUB.
+
 Set Implicit Arguments.
 Set Contextual Implicit.
 
@@ -139,7 +141,6 @@ Module Make (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP.ADDR
       Definition F_trigger_prop : F ~> PropT (E +' F) :=
         fun R e => fun t => t ≈ r <- trigger e ;; ret r.
 
-      Require Import ContainsUB.
       Definition model_undef_k_spec
         `{UB: UBE -< E +' F}
         {T R : Type}

src/coq/Numeric/Floats.v

@@ -468,7 +468,7 @@ Theorem of_intu_of_int_1:
 Proof.
   unfold of_intu, of_int, Int.signed, Int.ltu; intro.
   change (Int.unsigned ox8000_0000) with Int.half_modulus.
-  destruct (zlt (Int.unsigned x) Int.half_modulus); now intuition.
+  destruct (zlt (Int.unsigned x) Int.half_modulus); now intuition auto with *.
 Qed.
 
 Theorem of_intu_of_int_2:

src/coq/Numeric/IEEE754_extra.v

@@ -431,7 +431,7 @@ Proof.
     apply integer_representable_2p. auto.
     apply (Zpower_gt_0 radix2).
     lia.
-- assert (IZR x <> 0%R) by (apply (IZR_neq _ _ n)).
+- assert (IZR x <> 0%R) by (apply (eq_IZR_contrapositive _ _ n)).
   destruct (BofZ_finite x H) as (A & B & C).
   destruct (BofZ_representable (2^p)) as (D & E & F).
     apply integer_representable_2p. auto.
@@ -1036,7 +1036,7 @@ Proof with (try discriminate).
   rewrite <- ! bpow_plus.
   replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; lia).
   rewrite bpow_opp. unfold cond_Ropp; destruct s; auto.
-  rewrite Ropp_inv_permute. auto. apply Rgt_not_eq. apply bpow_gt_0.
+  rewrite Rinv_opp. auto.
   split. simpl. apply F2R_neq_0. destruct s; simpl in H; discriminate.
   auto.
 Qed.