...
 
Commits (174)
......@@ -13,3 +13,4 @@ build-dep/
Makefile.coq
Makefile.coq.conf
*.crashcoqide
.coqdeps.d
image: ralfjung/opam-ci:latest
image: ralfjung/opam-ci:opam2
stages:
- build
- deploy
- build_more
variables:
CPU_CORES: "9"
CPU_CORES: "10"
MTAC2_88_COMMIT: "a607c93656f046066a4ea45b2b5e7bf1816f3fe6"
.template: &template
stage: build
tags:
- fp-timing
- fp
script:
# prepare
- . build/opam-ci.sh $OPAM_PINS
- env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
key: "$CI_JOB_NAME-mtac2-tt"
paths:
- opamroot/
only:
- master
- /^ci/
opam:
stage: deploy
script:
# Send a trigger to the repository doing the work
- curl --fail -X POST -F "token=$OPAM_UPDATE_SECRET" -F "ref=master" -F "variables[REPO]=$CI_PROJECT_URL.git" -F "variables[REF]=$CI_COMMIT_REF_NAME" -F "variables[SHA]=$CI_COMMIT_SHA" -F "variables[NAME]=$OPAM_PKG" https://gitlab.mpi-sws.org/api/v4/projects/581/trigger/pipeline
variables:
OPAM_PKG: "coq-iris"
only:
- master
except:
- triggers
reverse-deps:
stage: deploy
script:
# Send a trigger to reverse dependencies to have them tested
- curl --fail -X POST -F "token=$IRIS_EXAMPLES_SECRET" -F "ref=master" -F "variables[IRIS_REV]=$CI_COMMIT_SHA" https://gitlab.mpi-sws.org/api/v4/projects/615/trigger/pipeline
only:
- master
except:
- triggers
build-coq.8.7.dev:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
except:
- triggers
- schedules
- api
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1 coq-mathcomp-ssreflect version 1.6.4"
except:
- triggers
## Build jobs
build-coq.8.7.0:
build-coq.8.8.2-flambda:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.0 coq-mathcomp-ssreflect version 1.6.4"
except:
- triggers
OCAML: "ocaml-variants.4.07.0+flambda"
OPAM_PINS: "coq version 8.8.2 coq-mathcomp-ssreflect version 1.7.0 coq-mtac.dev git git+https://github.com/Mtac2/Mtac2#$MTAC2_88_COMMIT"
TIMING_CONF: "coq-8.8.2-ocaml-4.07.0+flambda"
tags:
- fp-timing
build-coq.8.6.1:
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
artifacts:
paths:
- build-time.txt
- build-env.txt
except:
- triggers
OPAM_PINS: "coq version 8.8.2 coq-mathcomp-ssreflect version 1.7.0 coq-mtac.dev git git+https://github.com/Mtac2/Mtac2#$MTAC2_88_COMMIT"
TIMING_CONF: "coq-8.8.2"
tags:
- fp-timing
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
......@@ -8,19 +8,17 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
# Install build-dependencies
build-dep/opam: opam Makefile
# Creating the build-dep package.
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
......@@ -30,18 +28,19 @@ build-dep: build-dep/opam phony
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything.
@# Upgrading is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
echo "# Updating build-dep package." && \
opam upgrade "$$BUILD_DEP_PACKAGE"
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
# Phony wildcard targets
......
uninstall::
@# This makes sure we also delete stale files in the destination directory
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
......@@ -6,7 +6,7 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
This version is known to compile with:
- Coq 8.6.1 / 8.7.0 / 8.7.1
- Coq 8.7.0 / 8.8.0 / 8.8.2
- Ssreflect 1.6.4
- [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp) 1.1.0
......
......@@ -83,6 +83,7 @@ theories/proofmode/intro_patterns.v
theories/proofmode/spec_patterns.v
theories/proofmode/sel_patterns.v
theories/proofmode/tactics.v
theories/proofmode/tactics_mtac.v
theories/proofmode/notation.v
theories/proofmode/classes.v
theories/proofmode/class_instances.v
......
# awk program that patches the Makefile generated by Coq.
# Detect the name this project will be installed under.
/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
# we can just split the string at '/' here.
split($0, PIECES, /\//);
PROJECT=PIECES[2];
}
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines
1
#!/bin/bash
set -e
set -x
## This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export OPAMROOT="$(pwd)/opamroot"
export OPAMJOBS="$((2*$CPU_CORES))"
export OPAM_EDITOR="$(which false)"
# Make sure we got a good OPAM.
test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
eval `opam conf env`
# Make sure the pin for the builddep package is not stale.
make build-dep/opam
# Update repositories
opam update
# Make sure we got the right set of repositories registered
if echo "$@" | fgrep "dev" > /dev/null; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
else
# No dev version, make sure we do not have the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
test -d "$OPAMROOT/repo/coq-core-dev" && opam repo remove coq-core-dev
fi
test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
echo
# We really want to run all of the following in one opam transaction, but due to opam limitations,
# that is not currently possible.
# Install fixed versions of some dependencies.
echo
while (( "$#" )); do # while there are arguments left
PACKAGE="$1" ; shift
KIND="$1" ; shift
VERSION="$1" ; shift
# Check if the pin is already set
read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
else
echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
fi
done
# Upgrade cached things.
echo
echo "[opam-ci] Upgrading opam"
opam upgrade -y --fixup && opam upgrade -y
# Install build-dependencies.
echo
echo "[opam-ci] Installing build-dependencies"
make build-dep OPAMFLAGS=-y
# done
echo
coqc -v
......@@ -10,7 +10,8 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq" { (>= "8.7" & < "8.9~") | (= "dev") }
"coq-mtac"
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.8~") | (= "dev") }
"coq-stdpp" { (= "1.1.0") | (= "dev") }
]
......@@ -4,14 +4,15 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition assert : val :=
(* FIXME: I had to rename [assert] since it is a keyword in Mtac *)
Definition assert' : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Notation "'assert:' e" := (assert' (λ: <>, e))%E (at level 99) : expr_scope.
Lemma wp_assert `{heapG Σ} E (Φ : val iProp Σ) e `{!Closed [] e} :
WP e @ E {{ v, v = #true Φ #() }} - WP assert: e @ E {{ Φ }}.
Proof.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iIntros "HΦ". rewrite /assert'. wp_let. wp_seq.
wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
......@@ -53,7 +53,7 @@ Section mono_proof.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
as %[ ?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
......@@ -73,7 +73,7 @@ Section mono_proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
as %[ ?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
......
......@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition spawn : val :=
λ: "f",
let: "c" := ref NONE in
Fork ("c" <- SOME ("f" #())) ;; "c".
Fork ("c" <<- SOME ("f" #())) ;; "c".
Definition join : val :=
rec: "join" "c" :=
match: !"c" with
......
......@@ -10,7 +10,7 @@ Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true.
Definition acquire : val :=
rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
Definition release : val := λ: "l", "l" <- #false.
Definition release : val := λ: "l", "l" <<- #false.
(** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
......
......@@ -25,7 +25,7 @@ Definition acquire : val :=
else "acquire" "lk".
Definition release : val :=
λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
λ: "lk", (Fst "lk") <<- !(Fst "lk") + #1.
(** The CMRAs we need. *)
Class tlockG Σ :=
......@@ -67,7 +67,7 @@ Section proof.
Lemma locked_exclusive (γ : gname) : locked γ - locked γ - False.
Proof.
iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
iDestruct (own_valid_2 with "H1 H2") as %[[] _].
iDestruct (own_valid_2 with "H1 H2") as %[ [] _].
Qed.
Lemma newlock_spec (R : iProp Σ) :
......@@ -93,7 +93,7 @@ Section proof.
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
iModIntro. wp_let. wp_op. case_bool_decide; [|done].
iModIntro. wp_let. wp_op. case_bool_decide; [ |done].
wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
+ iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
......@@ -116,7 +116,7 @@ Section proof.
iModIntro. wp_let. wp_proj. wp_op.
wp_bind (CAS _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
destruct (decide (#n' = #n))%V as [ [= ->%Nat2Z.inj] | Hneq].
- wp_cas_suc.
iMod (own_update with "Hauth") as "[Hauth Hofull]".
{ eapply auth_update_alloc, prod_local_update_2.
......@@ -145,16 +145,16 @@ Section proof.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
%[ [<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_op.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
%[ [<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|Haown]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[ [] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
......
......@@ -74,7 +74,7 @@ Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
unfold IntoVal, AsVal in *; subst;
repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
repeat match goal with H : is_Some _ |- _ => destruct H as [ ??] end;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
......@@ -114,11 +114,11 @@ Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
PureExec True (heap_lang.Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
PureExec True (heap_lang.Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pure_exec. Qed.
(** Heap *)
......
......@@ -75,7 +75,7 @@ Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) : expr_scope.
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <<- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
(* The breaking point '/ ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
......
This diff is collapsed.
This diff is collapsed.
......@@ -4,6 +4,7 @@ From iris.base_logic Require Export base_logic big_op.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import hlist pretty.
Set Default Proof Using "Type".
Export ident.
......@@ -20,19 +21,18 @@ Ltac env_cbv :=
match goal with |- ?u => let v := eval env_cbv in u in change v end.
Ltac env_reflexivity := env_cbv; exact eq_refl.
(** * Misc *)
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh :=
lazymatch goal with
|- envs_entails ?Δ _ =>
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so *)
(* first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
eval vm_compute in
(IAnon (match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end))%positive
end))%positive%list
| _ => constr:(IAnon 1)
end.
......@@ -54,6 +54,7 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
(** * Start a proof *)
Class AsValid {M} (φ : Prop) (P : uPred M) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
......@@ -71,7 +72,6 @@ Proof. split. apply uPred.entails_wand. apply uPred.wand_entails. Qed.
Instance as_valid_equiv {M} (P Q : uPred M) : AsValid (P Q) (P Q).
Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
(** * Start a proof *)
Ltac iStartProof :=
lazymatch goal with
| |- envs_entails _ _ => idtac
......@@ -98,11 +98,11 @@ Ltac iElaborateSelPat pat :=
| SelPersistent :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)%stdpp%list
| SelSpatial :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)%stdpp%list
| SelIdent ?H :: ?pat =>
lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
| Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
......@@ -397,7 +397,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
let P := match goal with |- IntoForall ?P _ => P end in
fail "iSpecialize: cannot instantiate" P "with" x
|lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _))
| |- (_ : ?A), _ => refine (@ex_intro A _ x (conj _ _))
end; [env_reflexivity|go xs]]
end in
go xs.
......@@ -445,7 +445,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
| SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
fail "iSpecialize: cannot select hypotheses for persistent premise"
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs)%list in
eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
......@@ -546,7 +546,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let rec go t :=
let tT := type of t in
lazymatch eval hnf in tT with
| ?P ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
| ?P ?Q => let H := fresh in assert P as H; [ |go uconstr:(t H); clear H]
| _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
(* This is a workarround for Coq bug #4969. *)
......@@ -717,7 +717,7 @@ Tactic Notation "iSplit" :=
Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let Hs := eval vm_compute in (INamed <$> Hs)%stdpp in
eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
......@@ -730,7 +730,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let Hs := eval vm_compute in (INamed <$> Hs)%stdpp in
eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
......@@ -762,7 +762,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let Hs := eval vm_compute in (INamed <$> Hs)%stdpp in
eapply tac_combine with _ _ Hs _ _ H _;
[env_reflexivity ||
let Hs := iMissingHyps Hs in
......@@ -867,12 +867,12 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IDrop => iClearHyp Hz
| IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
| IList [[?pat1; ?pat2]] =>
| IList [ []] => iExFalso; iExact Hz
| IList [ [ ?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
| IList [ [IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
| IList [ [ ?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
| IList [ [ ?pat1];[ ?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
| IPureElim => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
......@@ -1571,7 +1571,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
| [SGoal (SpecGoal GPersistent false ?Hs_frame _ ?d)] =>
fail "iAssert: cannot select hypotheses for persistent proposition"
| [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d)] =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs)%list in
let p' := eval cbv in (match m with GModal => false | _ => p end) in
lazymatch p' with
| false =>
......
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances tactics.
From Mtac2 Require Import Mtac2 Ttactics DecomposeApp.
Import TT.notations.
Delimit Scope typed_tactic_scope with TT.
Set Default Proof Using "Type".
Export ident.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Notation env_Reduction := (
RedStrong [rl:RedBeta; RedMatch; RedFix; RedZeta;
RedDeltaOnly
[rl:Dyn (@beq); Dyn (@ascii_beq); Dyn (@string_beq);
Dyn (@env_lookup); Dyn (@env_lookup_delete); Dyn (@env_delete);
Dyn (@env_app); Dyn (@env_replace); Dyn (@env_dom);
Dyn (@env_persistent); Dyn (@env_spatial); Dyn (@env_spatial_is_nil);
Dyn (@envs_dom); Dyn (@envs_lookup); Dyn (@envs_lookup_delete);
Dyn (@envs_delete); Dyn (@envs_snoc); Dyn (@envs_app);
Dyn (@envs_simple_replace); Dyn (@envs_replace); Dyn (@envs_split);
Dyn (@envs_clear_spatial); Dyn (@envs_clear_persistent);
Dyn (@envs_split_go); Dyn (@envs_split)]]
).
Definition env_cbv :=
match_goal with [[? u |- u ] ] => let v := reduce env_Reduction u in T.change v end.
Definition env_reflexivity := env_cbv &> (T <- M.evar Type; t <- M.evar T; T.exact (@eq_refl T t)).
(** * Misc *)
Definition iFresh' (H : string) : gtactic ident :=
match_goal with
| [[? M (Δ : envs M) P |- envs_entails Δ P ]] =>
let Hs := reduce env_Reduction (envs_dom Δ) in (* should we just use RedNF? *)
let H := reduce RedVmCompute ((IAnon (match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end))%positive%list) in
T.ret H
| [[? T (G:T) |- G ]] => T.ret (IAnon 1)
end.
Definition iFresh : gtactic ident := iFresh' "~".
Definition iHypNotFound (s : string) : Exception. exact exception. Qed.
Definition iTypeOf {M} (H : string) : gtactic (option (bool * uPred M)) :=
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] =>
let H := reduce RedHNF (envs_lookup H Δ) in
T.ret H
end.
Definition iMissingHyps (Hs : list ident) : gtactic (list ident) :=
M <- M.evar _;
Δ <-
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] => T.ret Δ
| [[? b S (Δ : envs M) |- context C [ envs_split b S Δ ] ]] => T.ret Δ
end;
let Hhyps := reduce env_Reduction (envs_dom Δ) in
let H := reduce RedVmCompute (list_difference Hs Hhyps) in
T.ret H.
Inductive iGoal : Type :=
| IGoal M : envs M uPred M iGoal.
Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ P.
Monomorphic Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with
| [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist _) with
| [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P))
| _ =>
`M P <- M.evar _;
TT.apply (@as_valid_2 G _ P)
<**> TT.by' (T.apply_ || M.failwith "iStartProof: not a uPred")
<**> (TT.apply (@tac_adequate _ _)
<**> C (IGoal M (Envs Enil Enil) P))
end
end%MC
)%TT.
Definition iAssumptionCore :=
let find :=
(mfix4 f (A : _) (Γ : env A) (i : ident) (P : A) : M unit :=
<[decapp Γ with (@Esnoc A)]> UniMatchNoRed (
fun Γ j Q =>
mtry M.unify_or_fail UniCoq P Q;; M.unify_or_fail UniCoq i j;; M.ret ()
with | [? T x y] @NotUnifiable T x y => f _ Γ i P end
)
)%MC in
match_goal with
| [[? A i Γp Γs P _unused |- @envs_lookup A i (Envs Γp Γs) = Some (_unused, P) ] ] =>
mif M.is_evar i then
(find _ Γp i P || find _ Γs i P) &> env_reflexivity
else
M.raise DoesNotMatch
end%tactic.
......@@ -12,16 +12,14 @@ Section LiftingTests.
Definition simpl_test :
(10 = 4 + 6)%nat -
WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, v = #1 }}.
WP let: "x" := ref #1 in "x" <<- !"x";; !"x" {{ v, v = #1 }}.
Proof.
iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
match goal with
| |- context [ (10 = 4 + 6)%nat ] => done
end.
done.
Qed.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
let: "x" := ref #1 in "x" <<- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof.
......@@ -32,7 +30,7 @@ Section LiftingTests.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
"x" <<- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, v = #2 }}%I.
Proof.
......
......@@ -63,7 +63,7 @@ Section list_reverse.
| SOME "l" =>
let: "tmp1" := Fst !"l" in
let: "tmp2" := Snd !"l" in
"l" <- ("tmp1", "acc");;
"l" <<- ("tmp1", "acc");;
"rev" "tmp2" "hd"
end.
......@@ -72,7 +72,7 @@ Section list_reverse.
Proof.
iIntros "!# [Hxs Hys]".
iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
destruct xs as [|x xs]; iSimplifyEq.
destruct xs as [ |x xs]; iSimplifyEq.
- (* nil *) by wp_match.
- (* cons *) iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
......@@ -146,7 +146,7 @@ Section M.
- intros [n1|i1|] [n2|i2|]; repeat (simpl; case_decide); f_equal/=; lia.
- intros [n|i|]; repeat (simpl; case_decide); f_equal/=; lia.
- by intros [n|i|].
- intros [n1|i1|] y [[n2|i2|] ?]; exists (core y); simplify_eq/=;
- intros [n1|i1|] y [ [n2|i2|] ?]; exists (core y); simplify_eq/=;
repeat (simpl; case_decide); f_equal/=; lia.
- intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
Qed.
......@@ -158,7 +158,7 @@ Section M.
Definition M_ucmra_mixin : UcmraMixin M.
Proof.
split; try (done || apply _).
intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
intros [ ?|?|]; simpl; try case_decide; f_equal/=; lia.
Qed.
Canonical Structure M_UR : ucmraT := UcmraT M M_ucmra_mixin.
......@@ -178,7 +178,7 @@ End M.
Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. intros [ ?%subG_inG _]%subG_inv. split; apply _. Qed.
Section counter_proof.
Context `{!heapG Σ, !counterG Σ}.
......
......@@ -22,7 +22,7 @@ Definition rev : val :=
| SOME "l" =>
let: "tmp1" := Fst !"l" in
let: "tmp2" := Snd !"l" in
"l" <- ("tmp1", "acc");;
"l" <<- ("tmp1", "acc");;
"rev" "tmp2" "hd"
end.
......@@ -33,7 +33,7 @@ Lemma rev_acc_wp hd acc xs ys :
Proof.
iIntros (Φ) "[Hxs Hys] HΦ".
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq.
destruct xs as [ |x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
......
......@@ -25,7 +25,7 @@ Fixpoint sum (t : tree) : Z :=
Definition sum_loop : val :=
rec: "sum_loop" "t" "l" :=
match: "t" with
InjL "n" => "l" <- "n" + !"l"
InjL "n" => "l" <<- "n" + !"l"
| InjR "tt" => "sum_loop" !(Fst "tt") "l" ;; "sum_loop" !(Snd "tt") "l"
end.
......