From cbcbd2ed83454324567e5bd39ca245c8b31979d8 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Mon, 19 Aug 2024 16:04:49 +0200 Subject: [PATCH] update to new Iris --- examples/memcpy.v | 4 ++-- examples/memcpy_riscv64.v | 4 ++-- islaris.opam | 5 +++-- sail-riscv/README.md | 3 +++ sail-riscv/RV64.v | 6 +++--- sail-riscv/sail_opsem.v | 36 ++++++++++++++++++------------------ sail-riscv/tactics.v | 2 +- theories/adequacy.v | 2 +- theories/automation.v | 2 +- theories/base.v | 2 +- theories/ghost_state.v | 18 +++++++++--------- 11 files changed, 44 insertions(+), 40 deletions(-) diff --git a/examples/memcpy.v b/examples/memcpy.v index 2c1c163..adca240 100644 --- a/examples/memcpy.v +++ b/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. diff --git a/examples/memcpy_riscv64.v b/examples/memcpy_riscv64.v index b2880a1..8430b5a 100644 --- a/examples/memcpy_riscv64.v +++ b/examples/memcpy_riscv64.v @@ -101,7 +101,7 @@ 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). @@ -109,7 +109,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 <- 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. } diff --git a/islaris.opam b/islaris.opam index 8ae988b..1775528 100644 --- a/islaris.opam +++ b/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: [ diff --git a/sail-riscv/README.md b/sail-riscv/README.md index 096481a..19cb5e0 100644 --- a/sail-riscv/README.md +++ b/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 diff --git a/sail-riscv/RV64.v b/sail-riscv/RV64.v index b6cbd14..8bd1b30 100644 --- a/sail-riscv/RV64.v +++ b/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: diff --git a/sail-riscv/sail_opsem.v b/sail-riscv/sail_opsem.v index 1cbf9df..20e285d 100644 --- a/sail-riscv/sail_opsem.v +++ b/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. diff --git a/sail-riscv/tactics.v b/sail-riscv/tactics.v index cd24c3e..40c0d30 100644 --- a/sail-riscv/tactics.v +++ b/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. diff --git a/theories/adequacy.v b/theories/adequacy.v index d4f9781..2e0fc81 100644 --- a/theories/adequacy.v +++ b/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]". diff --git a/theories/automation.v b/theories/automation.v index b04069a..41ad382 100644 --- a/theories/automation.v +++ b/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". diff --git a/theories/base.v b/theories/base.v index bf3b218..5d64b59 100644 --- a/theories/base.v +++ b/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. diff --git a/theories/ghost_state.v b/theories/ghost_state.v index 2dc0080..ae15c28 100644 --- a/theories/ghost_state.v +++ b/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.