Commit dd8c1d4f authored by Michael Sammler's avatar Michael Sammler
Browse files

update Iris dependency

parent c9162734
Pipeline #53508 passed with stage
in 20 minutes and 19 seconds
......@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.13.2" & < "8.14~") }
"coq-iris" { (= "dev.2021-07-29.2.bfccb2a2") | (= "dev") }
"coq-iris" { (= "dev.2021-09-13.0.6575260a") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
......@@ -12,13 +12,13 @@ Class refinedcG Σ := RefinedCG {
}.
Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
iris_invG := refinedcG_invG;
iris_invGS := refinedcG_invG;
state_interp σ κs _ _ := state_ctx σ;
fork_post _ := True%I;
num_laters_per_step _ := 0%nat;
state_interp_mono _ _ _ _ := fupd_intro _ _;
}.
Global Opaque iris_invG.
Global Opaque iris_invGS.
Instance into_val_val v : IntoVal (to_rtexpr (Val v)) v.
Proof. done. Qed.
......
......@@ -251,7 +251,7 @@ Global Instance simpl_both_forall2_nil {A B} (f : A → B → Prop):
Proof. split; [by move => /(Forall2_nil_inv_l _ _)| naive_solver]. Qed.
Global Instance simpl_both_forall2_cons {A B} f (x : A) (y : B) xs ys:
SimplBoth (Forall2 f (x::xs)(y::ys)) (f x y Forall2 f xs ys).
Proof. split; [by move => /(Forall2_cons_inv _ _ _ _)|naive_solver]. Qed.
Proof. split; [by move => /(Forall2_cons _ _ _ _)|naive_solver]. Qed.
Global Instance simpl_length_0 {A} (l : list A):
SimplBothRel (=) (length l) (0%nat) (l = []).
......
......@@ -167,7 +167,7 @@ Section function.
iExists _. iFrame. by rewrite Forall_forall. }
destruct atys, lsa'' => //.
move: Hl => /(Forall2_cons_inv_l _ _)[[??][?[?[??]]]]; simplify_eq. csimpl in *.
move: Hly => /(Forall2_cons_inv _ _ _ _)[??].
move: Hly => /(Forall2_cons _ _ _ _)[??].
iDestruct "Hvl" as "[Hvl ?]".
iDestruct "Ha" as "[Ha ?]".
iDestruct (ty_ref with "[] Ha Hvl") as "$"; [done..|].
......@@ -275,8 +275,8 @@ Section inline_function.
iDestruct (big_sepL2_cons_inv_r with "Ha") as (???) "[Hmt ?]".
iDestruct (big_sepL2_cons_inv_l with "Htys") as (???) "[Hv' ?]". simplify_eq/=.
move: Hl => /(Forall2_cons_inv_l _ _ _ _)[[??][?[?[??]]]]. simplify_eq/=.
move: Hly => /(Forall2_cons_inv _ _ _ _)[??].
move: Hall => /(Forall2_cons_inv _ _ _ _)[??].
move: Hly => /(Forall2_cons _ _ _ _)[??].
move: Hall => /(Forall2_cons _ _ _ _)[??].
iDestruct (ty_ref with "[] Hmt Hv'") as "Hl"; [done..|].
iSpecialize ("HT" with "Hl").
iApply ("IH" with "[%] [//] [//] [//] HT [$] [$] [$] [$]").
......
......@@ -173,7 +173,7 @@ Section struct.
iSplit. { rewrite -Hv. by iApply heap_mapsto_loc_in_bounds. }
iInduction (sl_members sl) as [|[n ly] ms] "IH" forall (tys' l v Hlys Hv Hcount Hly); csimpl in * => //.
iDestruct "Htys" as "[Hty Htys]".
move: Hlys. intros [[?[?[??]]] ?]%Forall2_cons_inv. move: Hly => [??].
move: Hlys. intros [[?[?[??]]] ?]%Forall2_cons. move: Hly => [??].
rewrite -(take_drop (ly_size ly) v).
rewrite shift_loc_0 heap_mapsto_app take_app_alt ?take_length_le // ?Hv; try by cbn; lia.
iDestruct "Hl" as "[Hl Hl']". cbn. simplify_eq/=.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment