update to Coq 8.19

.github/workflows/ci.yml

@@ -22,7 +22,7 @@ jobs:
 
     env:
       OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
-      OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
+      OPAM_PINS: "coq version 8.19.0   isla-lang git git+https://github.com/rems-project/isla-lang.git"
       CPU_CORES: "1"
       DENY_WARNINGS: "1"
       CI_RUNNER: "dummy"

.gitlab-ci.yml

@@ -30,10 +30,10 @@ variables:
   - api
 
 ## Build jobs
-build-coq.8.18.0-timing:
+build-coq.8.19.0-timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.19.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
     DENY_WARNINGS: "1"
     # OPAM_PKG: "1"
   only:
@@ -43,18 +43,18 @@ build-coq.8.18.0-timing:
   tags:
   - fp-timing
 
-build-coq.8.18.0:
+build-coq.8.19.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.19.0   isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
     DENY_WARNINGS: "1"
   only:
   - /^ci/@iris/isla-coq
 
 trigger-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.18.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
+    OPAM_PINS: "coq version 8.19.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV  isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779"
   except:
   only:
   - triggers

bin/coqc_timing.sh

@@ -6,9 +6,14 @@ set -e
 # Variable TIMECMD is expected to contain an absolute path to the perf script.
 # If TIMECMD is not set (or empty), fallback to just calling coqc.
 # we need to use opam exec -- coqc to get the coqc installed by opam, not this script
+# If PROFILE is set, generate a profile in the $PROFILE file (relative to the root of the repo).
 
-if [ -z "${TIMECMD}" ]; then
-  opam exec -- coqc "$@"
-else
-  opam exec -- ${TIMECMD} coqc "$@"
+# This file is in "_build/default/bin"
+REPO_DIR="$(dirname $(readlink -f $0))/../../../"
+
+PROFILE_ARG=()
+if [[ ! -z "$PROFILE" ]]; then
+    PROFILE_ARG=("-profile" "$REPO_DIR/$PROFILE")
 fi
+
+opam exec -- ${TIMECMD} coqc "${PROFILE_ARG[@]}" "$@"

examples/binary_search.v

@@ -172,8 +172,8 @@ Definition binary_search_loop_spec : iProp Σ :=
   ⌜bv_unsigned xs `mod` 8 = 0⌝ ∗
   ⌜bv_unsigned xs + (length data) * 8 < 2 ^ 52⌝ ∗
   ⌜StronglySorted R data⌝ ∗ ⌜Transitive R⌝ ∗
-  ⌜∀ (i : nat) y, i < bv_unsigned l → data !! i = Some y → R y x⌝ ∗
-  ⌜∀ (i : nat) y, bv_unsigned r ≤ i → data !! i = Some y → ¬ R y x⌝ ∗
+  ⌜list_Forall (λ i y, i < bv_unsigned l → R y x) data⌝ ∗
+  ⌜list_Forall (λ i y, bv_unsigned r ≤ i → ¬ R y x) data⌝ ∗
   instr_pre 0x0000000010300054 (
     ∃ (l' r' tmp2 : bv 64),
       reg_col sys_regs ∗
@@ -193,8 +193,8 @@ Definition binary_search_loop_spec : iProp Σ :=
       bv_unsigned xs ↦ₘ∗ data ∗
       P ∗
       (bv_unsigned sp - stack_size) ↦ₘ? stack_size ∗
-      ⌜∀ (i : nat) y, i < bv_unsigned l' → data !! i = Some y → R y x⌝ ∗
-      ⌜∀ (i : nat) y, bv_unsigned l' ≤ i → data !! i = Some y → ¬ R y x⌝ ∗
+      ⌜list_Forall (λ i y, i < bv_unsigned l' → R y x) data⌝ ∗
+      ⌜list_Forall (λ i y, bv_unsigned l' ≤ i → ¬ R y x) data⌝ ∗
       True
   )
 .
@@ -260,7 +260,7 @@ Proof.
     bv_solve.
   - bv_simplify_arith select (ite _ _ _ = ite _ _ _).
     bv_simplify_arith select (_ ≤ i).
-    destruct bres; simpl in *; [solve_goal|].
+    destruct bres; simpl in *; [refined_solver (trigger_foralls; lia) |].
     apply: binary_search_cond_2; [solve_goal..|].
     bv_solve.
   - bv_simplify_arith select (i < _).
@@ -289,8 +289,8 @@ Definition binary_search_spec (stack_size : Z) : iProp Σ :=
     RET (λ rets,
       bv_unsigned (args !!! 1%nat) ↦ₘ∗ data ∗
       P ∗
-      ⌜∀ (i : nat) y, i < bv_unsigned (rets !!! 0%nat) → data !! i = Some y → R y (args !!! 3%nat)⌝ ∗
-      ⌜∀ (i : nat) y, bv_unsigned (rets !!! 0%nat) ≤ i → data !! i = Some y → ¬ R y (args !!! 3%nat)⌝ ∗
+      ⌜list_Forall (λ i y, i < bv_unsigned (rets !!! 0%nat) → R y (args !!! 3%nat)) data⌝ ∗
+      ⌜list_Forall (λ i y, bv_unsigned (rets !!! 0%nat) ≤ i → ¬ R y (args !!! 3%nat)) data⌝ ∗
       True))
   )%I.
 (*SPEC_END*)

examples/binary_search_riscv64.v

@@ -119,8 +119,8 @@ Definition binary_search_loop_spec : iProp Σ :=
   ⌜0x0000000080000000 ≤ bv_unsigned sp - stack_size ∧ bv_unsigned sp < 0x0000000080000000 + 0x0000000004000000⌝ ∗
   ⌜bv_unsigned sp `mod` 16 = 0⌝ ∗
   ⌜StronglySorted R data⌝ ∗ ⌜Transitive R⌝ ∗
-  ⌜∀ (i : nat) y, i < bv_unsigned l → data !! i = Some y → R y x⌝ ∗
-  ⌜∀ (i : nat) y, bv_unsigned r ≤ i → data !! i = Some y → ¬ R y x⌝ ∗
+  ⌜list_Forall (λ i y, i < bv_unsigned l → R y x) data⌝ ∗
+  ⌜list_Forall (λ i y, bv_unsigned r ≤ i → ¬ R y x) data⌝ ∗
   instr_pre 0x0000000010300078 (
     ∃ (l' r' tmp1 : bv 64),
       reg_col sys_regs ∗
@@ -141,8 +141,8 @@ Definition binary_search_loop_spec : iProp Σ :=
       bv_unsigned xs ↦ₘ∗ data ∗
       P ∗
       (bv_unsigned sp - stack_size) ↦ₘ? stack_size ∗
-      ⌜∀ (i : nat) y, i < bv_unsigned l' → data !! i = Some y → R y x⌝ ∗
-      ⌜∀ (i : nat) y, bv_unsigned l' ≤ i → data !! i = Some y → ¬ R y x⌝ ∗
+      ⌜list_Forall (λ i y, i < bv_unsigned l' → R y x) data⌝ ∗
+      ⌜list_Forall (λ i y, bv_unsigned l' ≤ i → ¬ R y x) data⌝ ∗
       True
   )
 .
@@ -201,7 +201,7 @@ Proof.
     apply: binary_search_cond_1; [solve_goal..| bv_solve].
   - bv_simplify_arith select (_ ≤ _).
     bv_simplify_arith select (¬ (_ < _)).
-    naive_solver bv_solve.
+    trigger_foralls. refined_solver bv_solve.
 (*PROOF_END*)
 Time Qed.
 
@@ -221,8 +221,8 @@ Definition binary_search_spec (stack_size : Z) : iProp Σ :=
     RET (λ rets,
       bv_unsigned (args !!! 1%nat) ↦ₘ∗ data ∗
       P ∗
-      ⌜∀ (i : nat) y, i < bv_unsigned (rets !!! 0%nat) → data !! i = Some y → R y (args !!! 3%nat)⌝ ∗
-      ⌜∀ (i : nat) y, bv_unsigned (rets !!! 0%nat) ≤ i → data !! i = Some y → ¬ R y (args !!! 3%nat)⌝ ∗
+      ⌜list_Forall (λ i y, i < bv_unsigned (rets !!! 0%nat) → R y (args !!! 3%nat)) data⌝ ∗
+      ⌜list_Forall (λ i y, bv_unsigned (rets !!! 0%nat) ≤ i → ¬ R y (args !!! 3%nat)) data⌝ ∗
       True))
   )%I.
 (*SPEC_END*)

islaris.opam

@@ -10,8 +10,8 @@ dev-repo: "git+https://github.com/rems-project/islaris.git"
 synopsis: "Islaris assembly verification tool"
 
 depends: [
-  "coq" { (= "8.18.0") | (= "dev") }
-  "coq-lithium" { (= "dev.2023-11-30.0.65d25ad4") | (= "dev") }
+  "coq" { (= "8.19.0") | (= "dev") }
+  "coq-lithium" { (= "dev.2024-03-12.0.de68b772") | (= "dev") }
   "coq-stdpp-unstable"
   "coq-record-update" { (= "0.3.3") | (= "dev") }
   "cmdliner" {>= "1.1.0"}

theories/automation.v

@@ -558,11 +558,11 @@ Proof.
         }
         iIntros "[? %]". iExists _. by iFrame.
     + iDestruct ("IH" with "[//] Hregs") as (???) "[? Hregs]". iExists _, _. iSplit;[done|]. iFrame.
-      iIntros "Hr". rewrite ->reg_col_cons. iDestruct ("Hregs" with "Hr") as "$". eauto with iFrame.
+      iIntros "Hr". iDestruct ("Hregs" with "Hr") as "$". eauto with iFrame.
   - rewrite !String_eqb_eq andb_bool_decide in Hr. case_bool_decide; destruct_and?; simplify_eq/=.
     + iExists _, _. rewrite ->reg_col_cons. iSplit; [done|]. iFrame. iIntros "?". iExists _. by iFrame.
     + iDestruct ("IH" with "[//] Hregs") as (???) "[? Hregs]". iExists _, _. iSplit;[done|]. iFrame.
-      iIntros "Hr". rewrite ->reg_col_cons. iDestruct ("Hregs" with "Hr") as "$". eauto with iFrame.
+      iIntros "Hr". iDestruct ("Hregs" with "Hr") as "$". eauto with iFrame.
       Unshelve. all: by apply inhabitant.
 Qed.
 
@@ -585,8 +585,7 @@ Proof.
   { iExists _. by iFrame. }
   move: Hr => /fmap_Some[[??]/=[??]]; subst => /=.
   iDestruct ("IH" with "[//] Hregs") as (v' ?) "[? ?]" => /=.
-  iExists _. rewrite reg_col_cons. iFrame. iSplit; [done|].
-  iExists _. by iFrame.
+  iExists _. rewrite reg_col_cons. by iFrame.
 Qed.
 
 Fixpoint regcol_cancel (regs1 regs2 : list (reg_kind * valu_shape)) : list (reg_kind * valu_shape) * list (reg_kind * valu_shape) * list (valu_shape * valu_shape) :=

theories/base.v

@@ -304,8 +304,7 @@ Proof.
   { iExists []. iSplit; done. }
   simpl. iDestruct "Hl" as "[[%x Hx] Hl]".
   iDestruct ("IH" with "Hl") as (xs) "[%Heq ?]".
-  iExists (x::xs) => /=. iSplit; [by rewrite /= Heq|]. iFrame.
-  iExists _. by iFrame.
+  iExists (x::xs) => /=. iSplit; [by rewrite /= Heq|]. by iFrame.
 Qed.
 
 (** fixpoints based on iris/bi/lib/fixpoint.v *)

theories/ghost_state.v

@@ -445,7 +445,7 @@ Section reg.
     iIntros (?). rewrite /reg_col. erewrite (delete_Permutation regs); [|done] => /=.
     iSplit.
     - iDestruct 1 as "[[%vact [??] ]?]". iExists _. iFrame.
-    - iDestruct 1 as (v ?) "[??]". iFrame. iExists _. by iFrame.
+    - iDestruct 1 as (v ?) "[??]". by iFrame.
   Qed.
 End reg.
 
@@ -575,7 +575,7 @@ Section mem.
     rewrite Z_to_bv_bv_unsigned.
     iMod (ghost_map_update with "Hmem Hbyte") as "[$ ?]".
     rewrite -{1}(insert_id mem a' v) // !dom_insert_L. iFrame.
-    iExists _. iFrame. by rewrite Z_to_bv_checked_bv_unsigned.
+    by rewrite Z_to_bv_checked_bv_unsigned.
   Qed.
 
   Lemma mem_mapsto_byte_update_big mem a bs bs' :