update to new Iris

examples/memcpy.v

@@ -125,7 +125,7 @@ Proof.
   all: try bv_solve.
   all: try bv_simplify_arith select (bv_extract _ _ _ ≠ _).
   all: try bv_simplify_arith select (bv_extract _ _ _ = _).
-  - rewrite insert_length. bv_solve.
+  - rewrite length_insert. bv_solve.
   - bv_solve.
   - bv_simplify.
     rewrite bv_wrap_small; [|bv_solve].
@@ -141,7 +141,7 @@ Proof.
     + rewrite take_insert; [done|bv_solve].
     + erewrite drop_S. 2: { erewrite <- list_lookup_insert; do 2 f_equal; bv_solve. }
       erewrite (drop_S srcdata). 2: { rewrite <- H6. f_equal. bv_solve. }
-      rewrite !drop_ge ?insert_length; [ |bv_solve..].
+      rewrite !drop_ge ?length_insert; [ |bv_solve..].
       f_equal. bv_solve.
 (*PROOF_END*)
 Time Qed.

examples/memcpy_riscv64.v

@@ -101,15 +101,15 @@ Proof.
   Unshelve. all: prepare_sidecond.
   all: try bv_simplify select (bv_add n _ = _).
   all: try bv_simplify select (bv_add n _ ≠ _).
-  all: try rewrite insert_length.
+  all: try rewrite length_insert.
   all: try bv_solve.
   - rewrite -(take_drop i (<[_ := _]> dstdata)).
     rewrite -(take_drop i srcdata).
     f_equal.
     + rewrite take_insert; [done|bv_solve].
     + erewrite drop_S. 2: { erewrite <- list_lookup_insert; do 2 f_equal; bv_solve. }
       erewrite (drop_S srcdata). 2: { rewrite <- H10. f_equal. bv_solve. }
-      rewrite !drop_ge ?insert_length //; [ |bv_solve..].
+      rewrite !drop_ge ?length_insert //; [ |bv_solve..].
       f_equal. bv_solve.
   - erewrite take_S_r. 2: { erewrite <- list_lookup_insert; do 2 f_equal; bv_solve. }
     erewrite take_S_r. 2: { rewrite <- H10. f_equal. bv_solve. }

islaris.opam

@@ -11,7 +11,8 @@ synopsis: "Islaris assembly verification tool"
 
 depends: [
   "coq" { (= "8.19.0") | (= "dev") }
-  "coq-lithium" { (= "dev.2024-03-12.0.de68b772") | (= "dev") }
+  "coq-lithium" { (= "dev.2024-08-19.0.2d6158dd") | (= "dev") }
+  "coq-stdpp-bitvector"
   "coq-stdpp-unstable"
   "coq-record-update" { (= "0.3.3") | (= "dev") }
   "cmdliner" {>= "1.1.0"}
@@ -25,7 +26,7 @@ depends: [
 ]
 
 pin-depends: [
-  [ "isla-lang.dev" "git+https://github.com/rems-project/isla-lang.git#6a1d25dc35a7f3c8442b61bfed3cca38f958f49f" ]
+  [ "isla-lang.dev" "git+https://github.com/rems-project/isla-lang.git#bda86c9f0bd28bbaa2481f50ddc986ede342805a" ]
 ]
 
 build: [

sail-riscv/README.md

@@ -9,6 +9,9 @@ separately. This can be done by calling `make saildep` in the root
 directory of this repository. This command installs the Coq code
 generated from the RISC-V Sail model into the current opam switch.
 
+Note that this command requires `z3` to be installed. One can install it with
+`opam install z3`.
+
 Afterwards one has to enable compilation of this directory by running
 `make enable-sail-riscv` in the root directory of this repository.
 Afterwards, the files in this folder are compiled together with the

sail-riscv/RV64.v

@@ -306,7 +306,7 @@ Lemma nextPC_nextPC regs n:
 Proof. now rewrite (regstate_eta regs). Qed.
 
 (* This breaks the `with` notations so we have to import it later. *)
-Require Import stdpp.unstable.bitvector_tactics.
+Require Import stdpp.bitvector.bitvector.
 Require Import isla.base.
 
 Local Open Scope Z_scope.
@@ -593,9 +593,9 @@ Lemma length_bits_of_bytes l:
   length (bits_of_bytes l) = (length l * 8)%nat.
 Proof.
   move => Hf.
-  rewrite /bits_of_bytes concat_join map_fmap join_length -list_fmap_compose /compose.
+  rewrite /bits_of_bytes concat_join map_fmap length_join -list_fmap_compose /compose.
   rewrite (sum_list_fmap_same 8) //.
-  apply list.Forall_forall => ?. rewrite /bits_of/= map_fmap fmap_length. apply: Hf.
+  apply list.Forall_forall => ?. rewrite /bits_of/= map_fmap length_fmap. apply: Hf.
 Qed.
 
 Lemma length_bits_of_mem_bytes l:

sail-riscv/sail_opsem.v

@@ -311,16 +311,16 @@ Proof.
   rewrite /mem_bytes_of_bits/bytes_of_bits/bits_of/= option_map_fmap map_fmap.
   apply fmap_Some. eexists (rev _). rewrite rev_involutive. split; [|done].
   rewrite (byte_chunks_reshape (Z.to_nat len)).
-  2: { rewrite fmap_length MachineWord.word_to_bools_length. lia. }
+  2: { rewrite length_fmap MachineWord.word_to_bools_length. lia. }
   f_equal. eapply list_eq_same_length; [done | |].
-  { rewrite reshape_length rev_length replicate_length fmap_length bv_to_little_endian_length; lia. }
+  { rewrite length_reshape rev_length length_replicate length_fmap length_bv_to_little_endian; lia. }
   move => i x y ?. rewrite rev_reverse sublist_lookup_reshape; [|lia|].
-  2: { rewrite fmap_length MachineWord.word_to_bools_length. lia. }
+  2: { rewrite length_fmap MachineWord.word_to_bools_length. lia. }
   move => /sublist_lookup_Some'[??] /reverse_lookup_Some.
-  rewrite list_lookup_fmap fmap_length bv_to_little_endian_length; [|lia] => -[Hl ?].
+  rewrite list_lookup_fmap length_fmap length_bv_to_little_endian; [|lia] => -[Hl ?].
   move: Hl => /fmap_Some[?[/bv_to_little_endian_lookup_Some[|???]]]; [lia|]. simplify_eq.
   apply: list_eq_same_length; [done|..].
-  { rewrite byte_to_memory_byte_length take_length_le ?drop_length; lia. }
+  { rewrite byte_to_memory_byte_length length_take_le ?length_drop; lia. }
   move => i' x y ? /lookup_take_Some. rewrite lookup_drop list_lookup_fmap.
   have H : (Z.to_nat (8 * len) > 0)%nat by lia.
   move => [/fmap_Some[?[/(word_to_bools_lookup_Some _ _ _ _ H)[??]?]]?] /byte_to_memory_byte_lookup_Some[??].
@@ -335,8 +335,8 @@ Lemma just_list_bits_of_mem_bytes bs:
     Some (mjoin (((λ x, reverse (bv_to_bits x)) <$> reverse bs))).
 Proof.
   rewrite just_list_mapM. apply mapM_Some_2. apply Forall2_same_length_lookup_2. {
-    rewrite fmap_length join_length -list_fmap_compose /compose /= sum_list_fmap_const.
-    rewrite length_bits_of_mem_bytes ?fmap_length ?reverse_length //.
+    rewrite length_fmap length_join -list_fmap_compose /compose /= sum_list_fmap_const.
+    rewrite length_bits_of_mem_bytes ?length_fmap ?length_reverse //.
     move => ? /elem_of_list_fmap[?[??]]. subst. by rewrite byte_to_memory_byte_length.
   }
   move => i x y. rewrite list_lookup_fmap /bits_of_mem_bytes/bits_of_bytes concat_join map_fmap.
@@ -347,12 +347,12 @@ Proof.
   move: Hrev => /reverse_lookup_Some. rewrite list_lookup_fmap => -[/fmap_Some[?[Hbs ?]] ?]. subst.
   move: Hl => /byte_to_memory_byte_lookup_Some[??].
   move => /join_lookup_Some_same_length'[| |].
-  { apply list.Forall_forall => ? /elem_of_list_fmap[?[??]]. subst. by rewrite reverse_length bv_to_bits_length. }
+  { apply list.Forall_forall => ? /elem_of_list_fmap[?[??]]. subst. by rewrite length_reverse length_bv_to_bits. }
   { done. }
   move => ?. rewrite list_lookup_fmap => -[/fmap_Some[?[/reverse_lookup_Some[??] ?]] Hl].
-  rewrite fmap_length in Hbs; simplify_eq.
+  rewrite length_fmap in Hbs; simplify_eq.
   move: Hl => /reverse_lookup_Some [/bv_to_bits_lookup_Some[??] ?]; simplify_eq.
-  by rewrite bool_of_bitU_of_bool bv_to_bits_length.
+  by rewrite bool_of_bitU_of_bool length_bv_to_bits.
 Qed.
 
 Lemma wordToN_cast_nat m n w (E: m = n) :
@@ -372,14 +372,14 @@ Proof.
   have n_pos : n >=? 0 = true by lia.
   rewrite /of_bits just_list_bits_of_mem_bytes.
   match goal with |- match ?e with | _ => _ end = _ => destruct e as [Hhyp|Hhyp] end. 2: {
-    rewrite /length_list join_length -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?reverse_length in Hhyp; [lia|].
+    rewrite /length_list length_join -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?length_reverse in Hhyp; [lia|].
     by apply Forall_true.
   }
   f_equal.
   apply get_word_inj. rewrite !get_word_to_word cast_Z_id.
   destruct Hhyp => /=. apply Word.wordToN_inj.
   rewrite Word.wordToN_NToWord_2. 2: {
-    rewrite -Npow2_pow Z_to_bv_unsigned /length_list join_length Nat2Z.id -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?reverse_length; [|by apply Forall_true].
+    rewrite -Npow2_pow Z_to_bv_unsigned /length_list length_join Nat2Z.id -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?length_reverse; [|by apply Forall_true].
     have ? := bv_wrap_in_range (8 * len') (little_endian_to_bv 8 bs).
     unfold bv_modulus in *.
     apply N2Z.inj_lt.
@@ -394,14 +394,14 @@ Proof.
   rewrite get_word_to_word wordToN_cast_nat.
   rewrite bools_to_word_spec rev_reverse.
   rewrite bv_wrap_spec //. case_bool_decide => /=.
-  2: { rewrite lookup_ge_None_2 // reverse_length join_length -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?reverse_length; [lia|]. by apply Forall_true. }
+  2: { rewrite lookup_ge_None_2 // length_reverse length_join -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?length_reverse; [lia|]. by apply Forall_true. }
   rewrite /default. case_match as Hc.
-  2: { rewrite lookup_ge_None reverse_length join_length -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?reverse_length in Hc; [lia|]. by apply Forall_true. }
+  2: { rewrite lookup_ge_None length_reverse length_join -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?length_reverse in Hc; [lia|]. by apply Forall_true. }
   move: Hc => /reverse_lookup_Some [/(join_lookup_Some_same_length 8)[|j1 [?[j2[Hl[Hl2 Hi]]]] ?]]. {
     apply Forall_forall => ? /elem_of_list_fmap[?[??]]. subst.
-    by rewrite reverse_length bv_to_bits_length.
+    by rewrite length_reverse length_bv_to_bits.
   }
-  move: Hi => /Nat2Z.inj_iff. rewrite join_length -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?reverse_length.
+  move: Hi => /Nat2Z.inj_iff. rewrite length_join -list_fmap_compose /compose /= (sum_list_fmap_same 8) ?length_reverse.
   2: { by apply Forall_forall. }
   move => Hi.
   have {Hi} ?: i = (length bs * 8 - 1 - (j1 * 8 + j2))%nat by lia. simplify_eq.
@@ -921,8 +921,8 @@ Proof.
   split. {
     right. move: Hor => [[? Hm]//|[Hm [??]]].
     all: eexists _, _; eapply SailReadMem; [done..| | by rewrite !Z_nat_N !N2Z.id !Heq Z_to_bv_bv_unsigned Hm].
-    - move: Hm => /mapM_Some /Forall2_length <-. rewrite seqZ_length. lia.
-    - apply replicate_length.
+    - move: Hm => /mapM_Some /Forall2_length <-. rewrite length_seqZ. lia.
+    - apply length_replicate.
   }
   move => ? ? ? ? Hstep. inversion_clear Hstep; simplify_eq.
   move: H2. rewrite !Z_nat_N !N2Z.id !Heq Z_to_bv_bv_unsigned.

sail-riscv/tactics.v

@@ -56,7 +56,7 @@
 Require Import Sail.Base.
 Require Import Sail.State_monad.
 Require Import Sail.State_lifting.
-Require Import stdpp.unstable.bitvector_tactics.
+Require Import stdpp.bitvector.bitvector.
 Require Import isla.sail_riscv.sail_opsem.
 
 Arguments read_accessor : simpl nomatch.

theories/adequacy.v

@@ -121,7 +121,7 @@ Proof.
   iModIntro.
   iExists _, (replicate (length regs) (λ _, True%I)), _, _.
   iSplitL "Hs2 Hm1"; last first; [iSplitL|].
-  - rewrite big_sepL2_replicate_r ?fmap_length // big_sepL_fmap.
+  - rewrite big_sepL2_replicate_r ?length_fmap // big_sepL_fmap.
     iApply (big_sepL_impl with "Hwp").
     iIntros "!>" (? rs ?) "Hwp".
     iMod (ghost_map_alloc (rs)) as (γr) "[Hr1 Hr2]".

theories/automation.v

@@ -56,7 +56,7 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From lithium Require Import hooks.
 From lithium Require Export all.
-From stdpp.unstable Require Export bitvector_tactics.
+From stdpp.bitvector Require Export bitvector.
 From isla Require Export lifting.
 Set Default Proof Using "Type".
 

theories/base.v

@@ -59,7 +59,7 @@ From stdpp.unstable Require Export bitblast.
 From RecordUpdate Require Export RecordSet.
 From iris.proofmode Require Import tactics.
 From lithium Require Export base.
-From stdpp.unstable Require Export bitvector.
+From stdpp.bitvector Require Export definitions.
 Export RecordSetNotations.
 
 Open Scope Z_scope.

theories/ghost_state.v

@@ -61,7 +61,7 @@ From iris.bi Require Import fractional.
 From iris.base_logic Require Export lib.own.
 From iris.base_logic.lib Require Import ghost_map ghost_var.
 From iris.proofmode Require Export tactics.
-From stdpp.unstable Require Import bitvector_tactics.
+From stdpp.bitvector Require Import bitvector.
 From isla Require Export opsem spec.
 Set Default Proof Using "Type".
 Import uPred.
@@ -619,7 +619,7 @@ Section mem.
     rewrite mem_mapsto_eq. iIntros "Hmem". iDestruct 1 as (len Hlen ?) "Hlist". subst.
     iExists _. iSplit; [done|].
     iDestruct (mem_mapsto_byte_lookup_big with "Hmem Hlist") as %Hall.
-    iPureIntro. apply mapM_Some. rewrite bv_to_little_endian_length ?Z2Nat.id in Hall; [|lia..].
+    iPureIntro. apply mapM_Some. rewrite length_bv_to_little_endian ?Z2Nat.id in Hall; [|lia..].
     by have ->: (Z.of_N (N.of_nat len) = len) by lia.
   Qed.
 
@@ -641,7 +641,7 @@ Section mem.
     rewrite mem_mapsto_eq. iIntros "Hmem". iDestruct 1 as (len Hlen ?) "Hlist". subst.
     iExists _. iSplitR; [done|].
     iMod (mem_mapsto_byte_update_big with "Hmem Hlist") as "[$ H]".
-    { rewrite !bv_to_little_endian_length; lia. }
+    { rewrite !length_bv_to_little_endian; lia. }
     iExists _. by iFrame.
   Qed.
 
@@ -668,7 +668,7 @@ Section mem.
   Proof.
     rewrite mem_mapsto_array_eq. iIntros (??) "[%len' [% [% Ha]]]". have ? : len = len' by lia. subst.
     iDestruct (big_sepL_insert_acc with "Ha") as "[$ Ha]"; [done|].
-    iIntros (?) "?". iExists _. iSplit; [done|]. rewrite insert_length. iSplit;[done|]. by iApply "Ha".
+    iIntros (?) "?". iExists _. iSplit; [done|]. rewrite length_insert. iSplit;[done|]. by iApply "Ha".
   Qed.
 
   Lemma mem_mapsto_array_lookup_acc n a (i : nat) (l : list (bv n)) q len v :
@@ -706,7 +706,7 @@ Section mem.
     - iExists _. iSplit; [| iSplit; [|done]]; iPureIntro; lia.
     - iExists (nn - Z.to_nat ns)%nat. iSplit; [iPureIntro; lia|]. iSplit; [iPureIntro; lia|].
       iApply (big_sepL_impl with "Hm2").
-      iIntros "!>" (???) "[%v ?]". rewrite replicate_length. iExists _.
+      iIntros "!>" (???) "[%v ?]". rewrite length_replicate. iExists _.
       have -> : (a + (Z.to_nat ns `min` nn + k)%nat) = (a + ns + k) by lia.
       done.
   Qed.
@@ -722,7 +722,7 @@ Section mem.
     iExists (nn1 + nn2)%nat. iSplit; [iPureIntro; lia|]. iSplit; [iPureIntro; lia|].
     rewrite replicate_add big_sepL_app. iFrame.
     iApply (big_sepL_impl with "Hm2").
-    iIntros "!>" (???) "[%v ?]". rewrite replicate_length. iExists _.
+    iIntros "!>" (???) "[%v ?]". rewrite length_replicate. iExists _.
     have -> : (a + nn1 + k) = (a + (nn1 + k)%nat) by lia.
     done.
   Qed.
@@ -733,14 +733,14 @@ Section mem.
     rewrite mem_mapsto_uninit_eq.
     iIntros "[%nn [% [% Hm]]]"; subst.
     iDestruct (big_sepL_exist with "Hm") as (ls Hlen) "Hm".
-    rewrite replicate_length in Hlen. subst.
+    rewrite length_replicate in Hlen. subst.
     iExists _, (Z_to_bv _ (little_endian_to_bv _ ls)). iSplit; [done|].
     rewrite mem_mapsto_eq. iExists (length ls).
     iSplit; [iPureIntro; lia|]. iSplit; [iPureIntro; lia|].
     rewrite Z_to_bv_small ?bv_to_little_endian_to_bv //.
     2: { pose proof (little_endian_to_bv_bound 8 ls).
          unfold bv_modulus. rewrite N2Z.inj_mul Z2N.id; lia. }
-    iApply (big_sepL_impl' with "Hm"). { by rewrite replicate_length. }
+    iApply (big_sepL_impl' with "Hm"). { by rewrite length_replicate. }
     iIntros "!>" (k ? ? ??) "[%y [% ?]]"; by simplify_eq.
   Qed.
 
@@ -749,7 +749,7 @@ Section mem.
   Proof.
     rewrite mem_mapsto_uninit_eq mem_mapsto_eq.
     iIntros "[%len [-> [% Hm]]]". iExists len. iSplit; [iPureIntro; lia|]. iSplit; [iPureIntro; lia|].
-    iApply (big_sepL_impl' with "Hm"). { rewrite replicate_length bv_to_little_endian_length; lia. }
+    iApply (big_sepL_impl' with "Hm"). { rewrite length_replicate length_bv_to_little_endian; lia. }
     iIntros "!>" (k ? ? ??) "?". eauto with iFrame.
   Qed.
 End mem.