Commit 6c840fd4 authored by Michael Sammler's avatar Michael Sammler
Browse files

bump iris

parent 31383716
Pipeline #32043 passed with stage
in 32 minutes and 50 seconds
......@@ -37,9 +37,9 @@ build-dep: build-dep/opam phony
@opam install $(OPAMFLAGS) build-dep/
update-deps: refinedc.opam refinedc-rcgen.opam
opam pin add -n -y refinedc . && \
opam pin add -n -y refinedc-rcgen . && \
opam install --deps-only refinedc refinedc-rcgen
opam pin add -n -y refinedc .
opam pin add -n -y refinedc-rcgen .
opam install --working-dir --deps-only refinedc refinedc-rcgen
.PHONY: update-deps
# Some files that do *not* need to be forwarded to Makefile.coq
......
......@@ -79,7 +79,7 @@ You can then install the dependencies:
opam install --deps-only refinedc refinedc-rcgen
```
**Note:** You can use `make update_deps` to install the right version of the
**Note:** You can use `make update-deps` to install the right version of the
dependencies if the requirements have changed. This should typically done if
the version of Iris on which RefinedC relies has been updated.
......
......@@ -14,7 +14,7 @@ RefinedC: Framework for verifying low-level code using refinement types and owne
depends: [
"coq" { (>= "8.11.0" & < "8.12~") | (= "dev") }
"coq-iris" { (= "dev.2020-07-10.0.3998e1fd") | (= "dev") }
"coq-iris" { (= "dev.2020-07-24.0.9b804e35") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -209,12 +209,12 @@ Ltac liRStep :=
(Q) is part of the goal, because simpl seems to take exponential time
in the number of blocks! *)
(* TODO: don't use i... tactics here *)
Tactic Notation "start_function" constr(name) "(" simple_intropattern(x) ")" :=
Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :=
intros;
repeat iIntros "#?";
rewrite /typed_function;
iIntros ( x );
iSplit; [iPureIntro; simpl; by [repeat constructor] || fail "in" name "argument types don't match layout of arguments" |];
iSplit; [iPureIntro; simpl; by [repeat constructor] || fail "in" fnname "argument types don't match layout of arguments" |];
let lsa := fresh "lsa" in let lsv := fresh "lsv" in
iIntros "!#" (lsa lsv); inv_vec lsv; inv_vec lsa.
......
......@@ -53,9 +53,9 @@ Section globals.
( (Heq : A = ty.(gt_A)), l ◁ₗ{Shr} ty.(gt_type) (rew [λ x, x] Heq in x) - T) -
simplify_hyp (initialized name x) T.
Proof.
unfold FastDone in *. iDestruct 1 as (?) "HT". iDestruct 1 as (l' ??? Heq) "Hl". simplify_eq. iApply "HT" => /=.
unfold FastDone in *. iDestruct 1 as (?) "HT". iDestruct 1 as (l' ??? Heq2) "Hl". simplify_eq. iApply "HT" => /=.
(** HERE WE USE AXIOM K! *)
by rewrite (UIP_refl _ _ Heq).
by rewrite (UIP_refl _ _ Heq2).
Qed.
Global Instance simplify_initialized_hyp_inst A x name ty l `{!FastDone (global_locs !! name = Some l)} `{!FastDone (global_initialized_types !! name = Some ty)}:
SimplifyHyp (initialized name x) (Some 0%N) :=
......
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