Closed JasonGross closed 3 years ago
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voGuess not :-(
coqbot
commented
3 years ago Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago Oh, I guess it is
coqbot
commented
3 years ago @JasonGross, Error: Could not minimize file /github/workspace/iris/tests/one_shot.v
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, Minimized File /github/workspace/iris/tests/one_shot.v
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, Minimized File /github/workspace/iris/tests/one_shot.v
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, Minimized File /github/workspace/iris/tests/one_shot.v (full log on GitHub Actions)
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.vo@coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, Minimized File /github/workspace/iris/tests/one_shot.v (full log on GitHub Actions)
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.vo
export extra_args=("-vvvv")Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, Minimized File /github/workspace/iris/tests/one_shot.v (full log on GitHub Actions)
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
JasonGross
commented
3 years ago @coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
#export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
#export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
#export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
cat > tests/one_shot.v <<EOF
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-notation-overridden" "-w" "-redundant-canonical-projection" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/iris/iris/prelude" "iris.prelude" "-Q" "/github/workspace/iris/iris/algebra" "iris.algebra" "-Q" "/github/workspace/iris/iris/si_logic" "iris.si_logic" "-Q" "/github/workspace/iris/iris/bi" "iris.bi" "-Q" "/github/workspace/iris/iris/proofmode" "iris.proofmode" "-Q" "/github/workspace/iris/iris/base_logic" "iris.base_logic" "-Q" "/github/workspace/iris/iris/program_logic" "iris.program_logic" "-Q" "/github/workspace/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/iris/iris_staging" "iris.staging" "-Q" "/github/workspace/iris/iris_deprecated" "iris.deprecated" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/stdpp" "stdpp" "-top" "one_shot" "-test-mode") -*- *)
(* File reduced by coq-bug-finder from original input, then from 313 lines to 37 lines, then from 206 lines to 243 lines, then from 247 lines to 42 lines, then from 210 lines to 1000 lines, then from 1004 lines to 43 lines, then from 207 lines to 585 lines, then from 589 lines to 43 lines, then from 206 lines to 673 lines, then from 677 lines to 66 lines, then from 219 lines to 393 lines, then from 397 lines to 73 lines, then from 224 lines to 390 lines, then from 394 lines to 131 lines, then from 281 lines to 1089 lines, then from 1093 lines to 504 lines, then from 651 lines to 704 lines, then from 708 lines to 537 lines, then from 684 lines to 857 lines, then from 861 lines to 613 lines, then from 759 lines to 1092 lines, then from 1096 lines to 697 lines, then from 843 lines to 952 lines, then from 956 lines to 704 lines, then from 850 lines to 1278 lines, then from 1282 lines to 716 lines, then from 861 lines to 1200 lines, then from 1204 lines to 763 lines, then from 907 lines to 1162 lines, then from 1166 lines to 785 lines, then from 929 lines to 1225 lines, then from 1229 lines to 817 lines, then from 958 lines to 1285 lines, then from 1289 lines to 945 lines *)
(* coqc version 8.13.1 (March 2021) compiled on Mar 6 2021 14:27:01 with OCaml 4.05.0
coqtop version 8.13.1 (March 2021) *)
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False := .
End LocalFalse.
Axiom proof_admitted : False.
Declare ML Module "ltac_plugin".
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Coq.QArith.QArith_base.
Require Coq.QArith.Qcanon.
Require Coq.Sorting.Permutation.
Require Coq.Logic.EqdepFacts.
Require Coq.PArith.PArith.
Require Coq.NArith.NArith.
Require Coq.ZArith.ZArith.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.QArith.QArith.
Require Coq.Classes.Morphisms.
Require Coq.Classes.RelationClasses.
Require Coq.Lists.List.
Require Coq.Bool.Bool.
Require Coq.Setoids.Setoid.
Require Coq.Init.Peano.
Require Coq.Unicode.Utf8.
Require Coq.Program.Basics.
Require Coq.Program.Syntax.
Require stdpp.options.
Require stdpp.base.
Require stdpp.proof_irrel.
Require stdpp.decidable.
Require Coq.micromega.Lia.
Require stdpp.tactics.
Require stdpp.option.
Require stdpp.numbers.
Require stdpp.list.
Require stdpp.list_numbers.
Require stdpp.fin.
Require stdpp.countable.
Require stdpp.orders.
Require stdpp.vector.
Require stdpp.finite.
Require stdpp.sets.
Require Coq.Arith.Wf_nat.
Require stdpp.relations.
Require stdpp.fin_sets.
Require stdpp.fin_maps.
Require stdpp.fin_map_dom.
Require stdpp.mapset.
Require stdpp.pmap.
Require Coq.Strings.Ascii.
Require Coq.Strings.String.
Require stdpp.strings.
Require stdpp.pretty.
Require stdpp.infinite.
Require stdpp.propset.
Require stdpp.gmap.
Require stdpp.coPset.
Require stdpp.namespaces.
Require stdpp.hlist.
Require Coq.ssr.ssreflect.
Require stdpp.listset.
Require stdpp.lexico.
Require stdpp.prelude.
Require iris.prelude.options.
Require iris.prelude.prelude.
Require iris.algebra.ofe.
Require iris.algebra.monoid.
Require iris.bi.notation.
Require iris.bi.interface.
Require iris.bi.derived_connectives.
Require iris.bi.derived_laws.
Require iris.bi.derived_laws_later.
Require stdpp.functions.
Require stdpp.gmultiset.
Require iris.algebra.big_op.
Require iris.algebra.cmra.
Require iris.algebra.updates.
Require iris.algebra.local_updates.
Require iris.algebra.list.
Require iris.algebra.proofmode_classes.
Require iris.algebra.gmap.
Require iris.bi.big_op.
Require iris.base_logic.lib.proph_map.
Require iris.base_logic.lib.fancy_updates.
Require iris.algebra.reservation_map.
Module Export iris_DOT_base_logic_DOT_lib_DOT_gen_heap.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export gen_heap.
Export stdpp.namespaces.
Import iris.algebra.reservation_map.
Import iris.algebra.agree.
Export iris.base_logic.lib.own.
Import iris.base_logic.lib.ghost_map.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> ghost_mapG Σ L V;
gen_meta_preG_inG :> ghost_mapG Σ L gname;
gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
}.
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> gen_heapPreG L V Σ;
gen_heap_name : gname;
gen_meta_name : gname
}.
Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
Section definitions.
Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∗
ghost_map_auth (gen_heap_name hG) 1 σ ∗
ghost_map_auth (gen_meta_name hG) 1 m.
End definitions.
Section gen_heap.
End gen_heap.
End gen_heap.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_gen_heap.
Module Export iris_DOT_base_logic_DOT_lib_DOT_gen_inv_heap.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export gen_inv_heap.
Import iris.algebra.auth.
Import iris.algebra.excl.
Import iris.algebra.gmap.
Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
(optionR $ exclR $ leibnizO V)
(agreeR (V -d> PropO)).
Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
}.
Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
inv_heap_inG :> inv_heapPreG L V Σ;
inv_heap_name : gname
}.
End gen_inv_heap.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_gen_inv_heap.
Module Export iris_DOT_bi_DOT_weakestpre.
Module Export iris.
Module Export bi.
Module Export weakestpre.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Inductive stuckness := NotStuck | MaybeStuck.
Class Wp (PROP EXPR VAL A : Type) :=
wp : A → coPset → EXPR → (VAL → PROP) → PROP.
Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
End weakestpre.
End bi.
End iris.
End iris_DOT_bi_DOT_weakestpre.
Module Export iris_DOT_program_logic_DOT_language.
Module Export iris.
Module Export program_logic.
Module Export language.
Section language_mixin.
Context {expr val state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (prim_step : expr → state → list observation → expr → state → list expr → Prop).
Record LanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
}.
End language_mixin.
Structure language := Language {
expr : Type;
val : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → list observation → expr → state → list expr → Prop;
language_mixin : LanguageMixin of_val to_val prim_step
}.
Global Arguments to_val {_} _.
Global Arguments prim_step {_} _ _ _ _ _ _.
Section language.
Context {Λ : language}.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
End language.
End language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_language.
Module Export iris_DOT_program_logic_DOT_weakestpre.
Module Export iris.
Module Export program_logic.
Module Export weakestpre.
Export iris.base_logic.lib.fancy_updates.
Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
iris_invG :> invG Σ;
state_interp : state Λ → nat → list (observation Λ) → nat → iProp Σ;
fork_post : val Λ → iProp Σ;
num_laters_per_step : nat → nat;
state_interp_mono σ ns κs nt:
state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
}.
Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
(wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 ns κ κs nt,
state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝
={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
state_interp σ2 (S ns) κs (length efs + nt) ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
end%I.
Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
admit.
Defined.
Definition wp_def `{!irisG Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
λ s : stuckness, fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def).
admit.
Defined.
Definition wp' := wp_aux.(unseal).
Existing Instance wp'.
End weakestpre.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_weakestpre.
Export stdpp.strings.
Delimit Scope binder_scope with binder.
Inductive binder := BAnon | BNamed :> string → binder.
Notation "<>" := BAnon : binder_scope.
Global Instance binder_dec_eq : EqDecision binder.
admit.
Defined.
Module Export iris_DOT_program_logic_DOT_ectx_language.
Module Export iris.
Module Export program_logic.
Module Export ectx_language.
Section ectx_language_mixin.
Context {expr val ectx state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (empty_ectx : ectx).
Context (comp_ectx : ectx → ectx → ectx).
Context (fill : ectx → expr → expr).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_head_stuck e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
mixin_fill_empty e : fill empty_ectx e = e;
mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
mixin_fill_inj K : Inj (=) (=) (fill K);
mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);
mixin_step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
fill K' e1' = fill K_redex e1_redex →
to_val e1' = None →
head_step e1_redex σ1 κ e2 σ2 efs →
∃ K'', K_redex = comp_ectx K' K'';
mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx;
}.
End ectx_language_mixin.
Structure ectxLanguage := EctxLanguage {
expr : Type;
val : Type;
ectx : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
empty_ectx : ectx;
comp_ectx : ectx → ectx → ectx;
fill : ectx → expr → expr;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectx_language_mixin :
EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
}.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments fill {_} _ _.
Global Arguments head_step {_} _ _ _ _ _ _.
Section ectx_language.
Context {Λ : ectxLanguage}.
Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
(e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' → e2 = fill K e2' →
head_step e1' σ1 κ e2' σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
admit.
Defined.
End ectx_language.
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
@Language E V St K of_val to_val _
(@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
End ectx_language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_ectx_language.
Module Export iris_DOT_program_logic_DOT_ectxi_language.
Module Export iris.
Module Export program_logic.
Module Export ectxi_language.
Section ectxi_language_mixin.
Context {expr val ectx_item state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (fill_item : ectx_item → expr → expr).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxiLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
mixin_head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e);
}.
End ectxi_language_mixin.
Structure ectxiLanguage := EctxiLanguage {
expr : Type;
val : Type;
ectx_item : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectxi_language_mixin :
EctxiLanguageMixin of_val to_val fill_item head_step
}.
Global Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments fill_item {_} _ _.
Global Arguments head_step {_} _ _ _ _ _ _.
Section ectxi_language.
Context {Λ : ectxiLanguage}.
Notation ectx := (list (ectx_item Λ)).
Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
Definition ectxi_lang_ectx_mixin :
EctxLanguageMixin of_val to_val [] (flip (++)) fill head_step.
admit.
Defined.
End ectxi_language.
Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
let '@EctxiLanguage E V C St K of_val to_val fill head mix := Λ in
@EctxLanguage E V (list C) St K of_val to_val _ _ _ _
(@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
End ectxi_language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_ectxi_language.
Module Export iris.
Module Export heap_lang.
Module Export locations.
Record loc := { loc_car : Z }.
Global Instance loc_eq_decision : EqDecision loc.
admit.
Defined.
Global Instance loc_countable : Countable loc.
admit.
Defined.
Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation.
admit.
Defined.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
Notation "l +ₗ off" :=
(loc_add l off) (at level 50, left associativity) : stdpp_scope.
End locations.
End heap_lang.
End iris.
Module Export heap_lang.
Definition proph_id := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison
| LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | MultOp | QuotOp | RemOp
| AndOp | OrOp | XorOp
| ShiftLOp | ShiftROp
| LeOp | LtOp | EqOp
| OffsetOp.
Inductive expr :=
| Val (v : val)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
| Fork (e : expr)
| AllocN (e1 e2 : expr)
| Free (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr)
| NewProph
| Resolve (e0 : expr) (e1 : expr) (e2 : expr)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope val_scope with val.
Definition observation : Set := proph_id * (val * val).
Notation of_val := Val (only parsing).
Definition to_val (e : expr) : option val :=
match e with
| Val v => Some v
| _ => None
end.
Definition lit_is_unboxed (l: base_lit) : Prop :=
match l with
| LitProphecy _ | LitPoison => False
| LitInt _ | LitBool _ | LitLoc _ | LitUnit => True
end.
Definition val_is_unboxed (v : val) : Prop :=
match v with
| LitV l => lit_is_unboxed l
| InjLV (LitV l) => lit_is_unboxed l
| InjRV (LitV l) => lit_is_unboxed l
| _ => False
end.
Global Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
admit.
Defined.
Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl ∨ val_is_unboxed v1.
Record state : Type := {
heap: gmap loc (option val);
used_proph_id: gset proph_id;
}.
Global Instance bin_op_eq_dec : EqDecision bin_op.
admit.
Defined.
Global Instance val_eq_dec : EqDecision val.
admit.
Defined.
Inductive ectx_item :=
| AppLCtx (v2 : val)
| AppRCtx (e1 : expr)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (v2 : val)
| BinOpRCtx (op : bin_op) (e1 : expr)
| IfCtx (e1 e2 : expr)
| PairLCtx (v2 : val)
| PairRCtx (e1 : expr)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : expr) (e2 : expr)
| AllocNLCtx (v2 : val)
| AllocNRCtx (e1 : expr)
| FreeCtx
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| CmpXchgLCtx (v1 : val) (v2 : val)
| CmpXchgMCtx (e0 : expr) (v2 : val)
| CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
| ResolveMCtx (e0 : expr) (v2 : val)
| ResolveRCtx (e0 : expr) (e1 : expr).
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
| UnOpCtx op => UnOp op e
| BinOpLCtx op v2 => BinOp op e (Val v2)
| BinOpRCtx op e1 => BinOp op e1 e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx v2 => Pair e (Val v2)
| PairRCtx e1 => Pair e1 e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| AllocNLCtx v2 => AllocN e (Val v2)
| AllocNRCtx e1 => AllocN e1 e
| FreeCtx => Free e
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
| ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
| ResolveMCtx ex v2 => Resolve ex e (Val v2)
| ResolveRCtx ex e1 => Resolve ex e1 e
end.
Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
match e with
| Val _ => e
| Var y => if decide (x = y) then Val v else Var y
| Rec f y e =>
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x v e else e
| App e1 e2 => App (subst x v e1) (subst x v e2)
| UnOp op e => UnOp op (subst x v e)
| BinOp op e1 e2 => BinOp op (subst x v e1) (subst x v e2)
| If e0 e1 e2 => If (subst x v e0) (subst x v e1) (subst x v e2)
| Pair e1 e2 => Pair (subst x v e1) (subst x v e2)
| Fst e => Fst (subst x v e)
| Snd e => Snd (subst x v e)
| InjL e => InjL (subst x v e)
| InjR e => InjR (subst x v e)
| Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
| Fork e => Fork (subst x v e)
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Free e => Free (subst x v e)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => id end.
Definition un_op_eval (op : un_op) (v : val) : option val :=
match op, v with
| NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
| NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
| MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
| _, _ => None
end.
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
match op with
| PlusOp => Some $ LitInt (n1 + n2)
| MinusOp => Some $ LitInt (n1 - n2)
| MultOp => Some $ LitInt (n1 * n2)
| QuotOp => Some $ LitInt (n1 `quot` n2)
| RemOp => Some $ LitInt (n1 `rem` n2)
| AndOp => Some $ LitInt (Z.land n1 n2)
| OrOp => Some $ LitInt (Z.lor n1 n2)
| XorOp => Some $ LitInt (Z.lxor n1 n2)
| ShiftLOp => Some $ LitInt (n1 ≪ n2)
| ShiftROp => Some $ LitInt (n1 ≫ n2)
| LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
| LtOp => Some $ LitBool (bool_decide (n1 < n2))
| EqOp => Some $ LitBool (bool_decide (n1 = n2))
| OffsetOp => None
end%Z.
Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
match op with
| PlusOp | MinusOp | MultOp | QuotOp | RemOp => None
| AndOp => Some (LitBool (b1 && b2))
| OrOp => Some (LitBool (b1 || b2))
| XorOp => Some (LitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => None
| LeOp | LtOp => None
| EqOp => Some (LitBool (bool_decide (b1 = b2)))
| OffsetOp => None
end.
Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
match op, v2 with
| OffsetOp, LitInt off => Some $ LitLoc (l1 +ₗ off)
| _, _ => None
end.
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
| LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
| LitV (LitLoc l1), LitV v2 => LitV <$> bin_op_eval_loc op l1 v2
| _, _ => None
end.
Definition state_upd_heap (f: gmap loc (option val) → gmap loc (option val)) (σ: state) : state :=
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: state) : state :=
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc (option val) :=
match vs with
| [] => ∅
| v :: vs' => {[l := Some v]} ∪ heap_array (l +ₗ 1) vs'
end.
Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
Inductive head_step : expr → state → list observation → expr → state → list expr → Prop :=
| RecS f x e σ :
head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
| PairS v1 v2 σ :
head_step (Pair (Val v1) (Val v2)) σ [] (Val $ PairV v1 v2) σ []
| InjLS v σ :
head_step (InjL $ Val v) σ [] (Val $ InjLV v) σ []
| InjRS v σ :
head_step (InjR $ Val v) σ [] (Val $ InjRV v) σ []
| BetaS f x e1 v2 e' σ :
e' = subst' x v2 (subst' f (RecV f x e1) e1) →
head_step (App (Val $ RecV f x e1) (Val v2)) σ [] e' σ []
| UnOpS op v v' σ :
un_op_eval op v = Some v' →
head_step (UnOp op (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 v' σ :
bin_op_eval op v1 v2 = Some v' →
head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
| IfTrueS e1 e2 σ :
head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
| IfFalseS e1 e2 σ :
head_step (If (Val $ LitV $ LitBool false) e1 e2) σ [] e2 σ []
| FstS v1 v2 σ :
head_step (Fst (Val $ PairV v1 v2)) σ [] (Val v1) σ []
| SndS v1 v2 σ :
head_step (Snd (Val $ PairV v1 v2)) σ [] (Val v2) σ []
| CaseLS v e1 e2 σ :
head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
| CaseRS v e1 e2 σ :
head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
| ForkS e σ:
head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
| AllocNS n v σ l :
(0 < n)%Z →
(∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
[]
(Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
[]
| FreeS l v σ :
σ.(heap) !! l = Some $ Some v →
head_step (Free (Val $ LitV $ LitLoc l)) σ
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=None]> σ)
[]
| LoadS l v σ :
σ.(heap) !! l = Some $ Some v →
head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
| StoreS l v w σ :
σ.(heap) !! l = Some $ Some v →
head_step (Store (Val $ LitV $ LitLoc l) (Val w)) σ
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=Some w]> σ)
[]
| CmpXchgS l v1 v2 vl σ b :
σ.(heap) !! l = Some $ Some vl →
vals_compare_safe vl v1 →
b = bool_decide (vl = v1) →
head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
(Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=Some v2]> σ else σ)
[]
| FaaS l i1 i2 σ :
σ.(heap) !! l = Some $ Some (LitV (LitInt i1)) →
head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
[]
(Val $ LitV $ LitInt i1) (state_upd_heap <[l:=Some $ LitV (LitInt (i1 + i2))]>σ)
[]
| NewProphS σ p :
p ∉ σ.(used_proph_id) →
head_step NewProph σ
[]
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪.) σ)
[]
| ResolveS p v e σ w σ' κs ts :
head_step e σ κs (Val v) σ' ts →
head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
(κs ++ [(p, (v, w))]) (Val v) σ' ts.
Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
admit.
Defined.
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion Val : val >-> expr.
Coercion Var : string >-> expr.
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation LamV x e := (RecV BAnon x e) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
Notation SOME x := (InjR x) (only parsing).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Export iris.base_logic.lib.proph_map.
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc (option val) Σ;
heapG_inv_heapG :> inv_heapG loc (option val) Σ;
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
}.
Global Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ _ κs _ :=
(gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
fork_post _ := True%I;
num_laters_per_step _ := 0;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0.
Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
Import iris.algebra.excl.
Import iris.algebra.agree.
Import iris.algebra.csum.
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(λ: "n",
CAS "x" NONE (SOME "n")),
(λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
NONE => #()
| SOME "n" =>
match: !"x" with
NONE => assert: #false
| SOME "m" => assert: "n" = "m"
end
end)).
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Section proof.
Context `{!heapG Σ, !one_shotG Σ}.
Lemma wp_one_shot (Φ : val → iProp Σ) :
(∀ f1 f2 : val,
(∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
□ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
⊢ WP one_shot_example #() {{ Φ }}.
EOF
make -j2 tests/one_shot.vo@coqbot minimize
cat > extra-args.sh <<EOF
#!/usr/bin/env bash
#export extra_args=("-vvvv")
EOF
chmod +x extra-args.sh
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
cat > tests/one_shot.v <<EOF
(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-notation-overridden" "-w" "-redundant-canonical-projection" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/iris/iris/prelude" "iris.prelude" "-Q" "/github/workspace/iris/iris/algebra" "iris.algebra" "-Q" "/github/workspace/iris/iris/si_logic" "iris.si_logic" "-Q" "/github/workspace/iris/iris/bi" "iris.bi" "-Q" "/github/workspace/iris/iris/proofmode" "iris.proofmode" "-Q" "/github/workspace/iris/iris/base_logic" "iris.base_logic" "-Q" "/github/workspace/iris/iris/program_logic" "iris.program_logic" "-Q" "/github/workspace/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/iris/iris_staging" "iris.staging" "-Q" "/github/workspace/iris/iris_deprecated" "iris.deprecated" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.05.0/lib/coq/user-contrib/stdpp" "stdpp" "-top" "one_shot" "-test-mode") -*- *)
(* File reduced by coq-bug-finder from original input, then from 313 lines to 37 lines, then from 206 lines to 243 lines, then from 247 lines to 42 lines, then from 210 lines to 1000 lines, then from 1004 lines to 43 lines, then from 207 lines to 585 lines, then from 589 lines to 43 lines, then from 206 lines to 673 lines, then from 677 lines to 66 lines, then from 219 lines to 393 lines, then from 397 lines to 73 lines, then from 224 lines to 390 lines, then from 394 lines to 131 lines, then from 281 lines to 1089 lines, then from 1093 lines to 504 lines, then from 651 lines to 704 lines, then from 708 lines to 537 lines, then from 684 lines to 857 lines, then from 861 lines to 613 lines, then from 759 lines to 1092 lines, then from 1096 lines to 697 lines, then from 843 lines to 952 lines, then from 956 lines to 704 lines, then from 850 lines to 1278 lines, then from 1282 lines to 716 lines, then from 861 lines to 1200 lines, then from 1204 lines to 763 lines, then from 907 lines to 1162 lines, then from 1166 lines to 785 lines, then from 929 lines to 1225 lines, then from 1229 lines to 817 lines, then from 958 lines to 1285 lines, then from 1289 lines to 945 lines *)
(* coqc version 8.13.1 (March 2021) compiled on Mar 6 2021 14:27:01 with OCaml 4.05.0
coqtop version 8.13.1 (March 2021) *)
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False := .
End LocalFalse.
Axiom proof_admitted : False.
Declare ML Module "ltac_plugin".
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Coq.QArith.QArith_base.
Require Coq.QArith.Qcanon.
Require Coq.Sorting.Permutation.
Require Coq.Logic.EqdepFacts.
Require Coq.PArith.PArith.
Require Coq.NArith.NArith.
Require Coq.ZArith.ZArith.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.QArith.QArith.
Require Coq.Classes.Morphisms.
Require Coq.Classes.RelationClasses.
Require Coq.Lists.List.
Require Coq.Bool.Bool.
Require Coq.Setoids.Setoid.
Require Coq.Init.Peano.
Require Coq.Unicode.Utf8.
Require Coq.Program.Basics.
Require Coq.Program.Syntax.
Require stdpp.options.
Require stdpp.base.
Require stdpp.proof_irrel.
Require stdpp.decidable.
Require Coq.micromega.Lia.
Require stdpp.tactics.
Require stdpp.option.
Require stdpp.numbers.
Require stdpp.list.
Require stdpp.list_numbers.
Require stdpp.fin.
Require stdpp.countable.
Require stdpp.orders.
Require stdpp.vector.
Require stdpp.finite.
Require stdpp.sets.
Require Coq.Arith.Wf_nat.
Require stdpp.relations.
Require stdpp.fin_sets.
Require stdpp.fin_maps.
Require stdpp.fin_map_dom.
Require stdpp.mapset.
Require stdpp.pmap.
Require Coq.Strings.Ascii.
Require Coq.Strings.String.
Require stdpp.strings.
Require stdpp.pretty.
Require stdpp.infinite.
Require stdpp.propset.
Require stdpp.gmap.
Require stdpp.coPset.
Require stdpp.namespaces.
Require stdpp.hlist.
Require Coq.ssr.ssreflect.
Require stdpp.listset.
Require stdpp.lexico.
Require stdpp.prelude.
Require iris.prelude.options.
Require iris.prelude.prelude.
Require iris.algebra.ofe.
Require iris.algebra.monoid.
Require iris.bi.notation.
Require iris.bi.interface.
Require iris.bi.derived_connectives.
Require iris.bi.derived_laws.
Require iris.bi.derived_laws_later.
Require stdpp.functions.
Require stdpp.gmultiset.
Require iris.algebra.big_op.
Require iris.algebra.cmra.
Require iris.algebra.updates.
Require iris.algebra.local_updates.
Require iris.algebra.list.
Require iris.algebra.proofmode_classes.
Require iris.algebra.gmap.
Require iris.bi.big_op.
Require iris.base_logic.lib.proph_map.
Require iris.base_logic.lib.fancy_updates.
Require iris.algebra.reservation_map.
Module Export iris_DOT_base_logic_DOT_lib_DOT_gen_heap.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export gen_heap.
Export stdpp.namespaces.
Import iris.algebra.reservation_map.
Import iris.algebra.agree.
Export iris.base_logic.lib.own.
Import iris.base_logic.lib.ghost_map.
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> ghost_mapG Σ L V;
gen_meta_preG_inG :> ghost_mapG Σ L gname;
gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
}.
Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG :> gen_heapPreG L V Σ;
gen_heap_name : gname;
gen_meta_name : gname
}.
Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
Section definitions.
Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∗
ghost_map_auth (gen_heap_name hG) 1 σ ∗
ghost_map_auth (gen_meta_name hG) 1 m.
End definitions.
Section gen_heap.
End gen_heap.
End gen_heap.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_gen_heap.
Module Export iris_DOT_base_logic_DOT_lib_DOT_gen_inv_heap.
Module Export iris.
Module Export base_logic.
Module Export lib.
Module Export gen_inv_heap.
Import iris.algebra.auth.
Import iris.algebra.excl.
Import iris.algebra.gmap.
Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
(optionR $ exclR $ leibnizO V)
(agreeR (V -d> PropO)).
Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
}.
Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
inv_heap_inG :> inv_heapPreG L V Σ;
inv_heap_name : gname
}.
End gen_inv_heap.
End lib.
End base_logic.
End iris.
End iris_DOT_base_logic_DOT_lib_DOT_gen_inv_heap.
Module Export iris_DOT_bi_DOT_weakestpre.
Module Export iris.
Module Export bi.
Module Export weakestpre.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Inductive stuckness := NotStuck | MaybeStuck.
Class Wp (PROP EXPR VAL A : Type) :=
wp : A → coPset → EXPR → (VAL → PROP) → PROP.
Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
(at level 20, e, Φ at level 200, only parsing) : bi_scope.
Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
(at level 20, e, Q at level 200,
format "'[' 'WP' e '/' '[ ' {{ v , Q } } ']' ']'") : bi_scope.
End weakestpre.
End bi.
End iris.
End iris_DOT_bi_DOT_weakestpre.
Module Export iris_DOT_program_logic_DOT_language.
Module Export iris.
Module Export program_logic.
Module Export language.
Section language_mixin.
Context {expr val state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (prim_step : expr → state → list observation → expr → state → list expr → Prop).
Record LanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
}.
End language_mixin.
Structure language := Language {
expr : Type;
val : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → list observation → expr → state → list expr → Prop;
language_mixin : LanguageMixin of_val to_val prim_step
}.
Global Arguments to_val {_} _.
Global Arguments prim_step {_} _ _ _ _ _ _.
Section language.
Context {Λ : language}.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
End language.
End language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_language.
Module Export iris_DOT_program_logic_DOT_weakestpre.
Module Export iris.
Module Export program_logic.
Module Export weakestpre.
Export iris.base_logic.lib.fancy_updates.
Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
iris_invG :> invG Σ;
state_interp : state Λ → nat → list (observation Λ) → nat → iProp Σ;
fork_post : val Λ → iProp Σ;
num_laters_per_step : nat → nat;
state_interp_mono σ ns κs nt:
state_interp σ ns κs nt ={∅}=∗ state_interp σ (S ns) κs nt
}.
Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
(wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => ∀ σ1 ns κ κs nt,
state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝
={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
state_interp σ2 (S ns) κs (length efs + nt) ∗
wp E e2 Φ ∗
[∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
end%I.
Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
admit.
Defined.
Definition wp_def `{!irisG Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
λ s : stuckness, fixpoint (wp_pre s).
Definition wp_aux : seal (@wp_def).
admit.
Defined.
Definition wp' := wp_aux.(unseal).
Existing Instance wp'.
End weakestpre.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_weakestpre.
Export stdpp.strings.
Delimit Scope binder_scope with binder.
Inductive binder := BAnon | BNamed :> string → binder.
Notation "<>" := BAnon : binder_scope.
Global Instance binder_dec_eq : EqDecision binder.
admit.
Defined.
Module Export iris_DOT_program_logic_DOT_ectx_language.
Module Export iris.
Module Export program_logic.
Module Export ectx_language.
Section ectx_language_mixin.
Context {expr val ectx state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (empty_ectx : ectx).
Context (comp_ectx : ectx → ectx → ectx).
Context (fill : ectx → expr → expr).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_head_stuck e1 σ1 κ e2 σ2 efs :
head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
mixin_fill_empty e : fill empty_ectx e = e;
mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
mixin_fill_inj K : Inj (=) (=) (fill K);
mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);
mixin_step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
fill K' e1' = fill K_redex e1_redex →
to_val e1' = None →
head_step e1_redex σ1 κ e2 σ2 efs →
∃ K'', K_redex = comp_ectx K' K'';
mixin_head_ctx_step_val K e σ1 κ e2 σ2 efs :
head_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx;
}.
End ectx_language_mixin.
Structure ectxLanguage := EctxLanguage {
expr : Type;
val : Type;
ectx : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
empty_ectx : ectx;
comp_ectx : ectx → ectx → ectx;
fill : ectx → expr → expr;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectx_language_mixin :
EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
}.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments fill {_} _ _.
Global Arguments head_step {_} _ _ _ _ _ _.
Section ectx_language.
Context {Λ : ectxLanguage}.
Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
(e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' → e2 = fill K e2' →
head_step e1' σ1 κ e2' σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
admit.
Defined.
End ectx_language.
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
@Language E V St K of_val to_val _
(@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
End ectx_language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_ectx_language.
Module Export iris_DOT_program_logic_DOT_ectxi_language.
Module Export iris.
Module Export program_logic.
Module Export ectxi_language.
Section ectxi_language_mixin.
Context {expr val ectx_item state observation : Type}.
Context (of_val : val → expr).
Context (to_val : expr → option val).
Context (fill_item : ectx_item → expr → expr).
Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
Record EctxiLanguageMixin := {
mixin_to_of_val v : to_val (of_val v) = Some v;
mixin_of_to_val e v : to_val e = Some v → of_val v = e;
mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
mixin_head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e);
}.
End ectxi_language_mixin.
Structure ectxiLanguage := EctxiLanguage {
expr : Type;
val : Type;
ectx_item : Type;
state : Type;
observation : Type;
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
head_step : expr → state → list observation → expr → state → list expr → Prop;
ectxi_language_mixin :
EctxiLanguageMixin of_val to_val fill_item head_step
}.
Global Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
Global Arguments of_val {_} _.
Global Arguments to_val {_} _.
Global Arguments fill_item {_} _ _.
Global Arguments head_step {_} _ _ _ _ _ _.
Section ectxi_language.
Context {Λ : ectxiLanguage}.
Notation ectx := (list (ectx_item Λ)).
Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
Definition ectxi_lang_ectx_mixin :
EctxLanguageMixin of_val to_val [] (flip (++)) fill head_step.
admit.
Defined.
End ectxi_language.
Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
let '@EctxiLanguage E V C St K of_val to_val fill head mix := Λ in
@EctxLanguage E V (list C) St K of_val to_val _ _ _ _
(@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
End ectxi_language.
End program_logic.
End iris.
End iris_DOT_program_logic_DOT_ectxi_language.
Module Export iris.
Module Export heap_lang.
Module Export locations.
Record loc := { loc_car : Z }.
Global Instance loc_eq_decision : EqDecision loc.
admit.
Defined.
Global Instance loc_countable : Countable loc.
admit.
Defined.
Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation.
admit.
Defined.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
Notation "l +ₗ off" :=
(loc_add l off) (at level 50, left associativity) : stdpp_scope.
End locations.
End heap_lang.
End iris.
Module Export heap_lang.
Definition proph_id := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison
| LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | MultOp | QuotOp | RemOp
| AndOp | OrOp | XorOp
| ShiftLOp | ShiftROp
| LeOp | LtOp | EqOp
| OffsetOp.
Inductive expr :=
| Val (v : val)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
| Fork (e : expr)
| AllocN (e1 e2 : expr)
| Free (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr)
| NewProph
| Resolve (e0 : expr) (e1 : expr) (e2 : expr)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope val_scope with val.
Definition observation : Set := proph_id * (val * val).
Notation of_val := Val (only parsing).
Definition to_val (e : expr) : option val :=
match e with
| Val v => Some v
| _ => None
end.
Definition lit_is_unboxed (l: base_lit) : Prop :=
match l with
| LitProphecy _ | LitPoison => False
| LitInt _ | LitBool _ | LitLoc _ | LitUnit => True
end.
Definition val_is_unboxed (v : val) : Prop :=
match v with
| LitV l => lit_is_unboxed l
| InjLV (LitV l) => lit_is_unboxed l
| InjRV (LitV l) => lit_is_unboxed l
| _ => False
end.
Global Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
admit.
Defined.
Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl ∨ val_is_unboxed v1.
Record state : Type := {
heap: gmap loc (option val);
used_proph_id: gset proph_id;
}.
Global Instance bin_op_eq_dec : EqDecision bin_op.
admit.
Defined.
Global Instance val_eq_dec : EqDecision val.
admit.
Defined.
Inductive ectx_item :=
| AppLCtx (v2 : val)
| AppRCtx (e1 : expr)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (v2 : val)
| BinOpRCtx (op : bin_op) (e1 : expr)
| IfCtx (e1 e2 : expr)
| PairLCtx (v2 : val)
| PairRCtx (e1 : expr)
| FstCtx
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : expr) (e2 : expr)
| AllocNLCtx (v2 : val)
| AllocNRCtx (e1 : expr)
| FreeCtx
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| CmpXchgLCtx (v1 : val) (v2 : val)
| CmpXchgMCtx (e0 : expr) (v2 : val)
| CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
| ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
| ResolveMCtx (e0 : expr) (v2 : val)
| ResolveRCtx (e0 : expr) (e1 : expr).
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
| UnOpCtx op => UnOp op e
| BinOpLCtx op v2 => BinOp op e (Val v2)
| BinOpRCtx op e1 => BinOp op e1 e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx v2 => Pair e (Val v2)
| PairRCtx e1 => Pair e1 e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| AllocNLCtx v2 => AllocN e (Val v2)
| AllocNRCtx e1 => AllocN e1 e
| FreeCtx => Free e
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
| ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
| ResolveMCtx ex v2 => Resolve ex e (Val v2)
| ResolveRCtx ex e1 => Resolve ex e1 e
end.
Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
match e with
| Val _ => e
| Var y => if decide (x = y) then Val v else Var y
| Rec f y e =>
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x v e else e
| App e1 e2 => App (subst x v e1) (subst x v e2)
| UnOp op e => UnOp op (subst x v e)
| BinOp op e1 e2 => BinOp op (subst x v e1) (subst x v e2)
| If e0 e1 e2 => If (subst x v e0) (subst x v e1) (subst x v e2)
| Pair e1 e2 => Pair (subst x v e1) (subst x v e2)
| Fst e => Fst (subst x v e)
| Snd e => Snd (subst x v e)
| InjL e => InjL (subst x v e)
| InjR e => InjR (subst x v e)
| Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
| Fork e => Fork (subst x v e)
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Free e => Free (subst x v e)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
| NewProph => NewProph
| Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => id end.
Definition un_op_eval (op : un_op) (v : val) : option val :=
match op, v with
| NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
| NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
| MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
| _, _ => None
end.
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
match op with
| PlusOp => Some $ LitInt (n1 + n2)
| MinusOp => Some $ LitInt (n1 - n2)
| MultOp => Some $ LitInt (n1 * n2)
| QuotOp => Some $ LitInt (n1 `quot` n2)
| RemOp => Some $ LitInt (n1 `rem` n2)
| AndOp => Some $ LitInt (Z.land n1 n2)
| OrOp => Some $ LitInt (Z.lor n1 n2)
| XorOp => Some $ LitInt (Z.lxor n1 n2)
| ShiftLOp => Some $ LitInt (n1 ≪ n2)
| ShiftROp => Some $ LitInt (n1 ≫ n2)
| LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
| LtOp => Some $ LitBool (bool_decide (n1 < n2))
| EqOp => Some $ LitBool (bool_decide (n1 = n2))
| OffsetOp => None
end%Z.
Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
match op with
| PlusOp | MinusOp | MultOp | QuotOp | RemOp => None
| AndOp => Some (LitBool (b1 && b2))
| OrOp => Some (LitBool (b1 || b2))
| XorOp => Some (LitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => None
| LeOp | LtOp => None
| EqOp => Some (LitBool (bool_decide (b1 = b2)))
| OffsetOp => None
end.
Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
match op, v2 with
| OffsetOp, LitInt off => Some $ LitLoc (l1 +ₗ off)
| _, _ => None
end.
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
| LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
| LitV (LitLoc l1), LitV v2 => LitV <$> bin_op_eval_loc op l1 v2
| _, _ => None
end.
Definition state_upd_heap (f: gmap loc (option val) → gmap loc (option val)) (σ: state) : state :=
{| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: state) : state :=
{| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc (option val) :=
match vs with
| [] => ∅
| v :: vs' => {[l := Some v]} ∪ heap_array (l +ₗ 1) vs'
end.
Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) ∪ h) σ.
Inductive head_step : expr → state → list observation → expr → state → list expr → Prop :=
| RecS f x e σ :
head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
| PairS v1 v2 σ :
head_step (Pair (Val v1) (Val v2)) σ [] (Val $ PairV v1 v2) σ []
| InjLS v σ :
head_step (InjL $ Val v) σ [] (Val $ InjLV v) σ []
| InjRS v σ :
head_step (InjR $ Val v) σ [] (Val $ InjRV v) σ []
| BetaS f x e1 v2 e' σ :
e' = subst' x v2 (subst' f (RecV f x e1) e1) →
head_step (App (Val $ RecV f x e1) (Val v2)) σ [] e' σ []
| UnOpS op v v' σ :
un_op_eval op v = Some v' →
head_step (UnOp op (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 v' σ :
bin_op_eval op v1 v2 = Some v' →
head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
| IfTrueS e1 e2 σ :
head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
| IfFalseS e1 e2 σ :
head_step (If (Val $ LitV $ LitBool false) e1 e2) σ [] e2 σ []
| FstS v1 v2 σ :
head_step (Fst (Val $ PairV v1 v2)) σ [] (Val v1) σ []
| SndS v1 v2 σ :
head_step (Snd (Val $ PairV v1 v2)) σ [] (Val v2) σ []
| CaseLS v e1 e2 σ :
head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
| CaseRS v e1 e2 σ :
head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
| ForkS e σ:
head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
| AllocNS n v σ l :
(0 < n)%Z →
(∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
[]
(Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
[]
| FreeS l v σ :
σ.(heap) !! l = Some $ Some v →
head_step (Free (Val $ LitV $ LitLoc l)) σ
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=None]> σ)
[]
| LoadS l v σ :
σ.(heap) !! l = Some $ Some v →
head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
| StoreS l v w σ :
σ.(heap) !! l = Some $ Some v →
head_step (Store (Val $ LitV $ LitLoc l) (Val w)) σ
[]
(Val $ LitV LitUnit) (state_upd_heap <[l:=Some w]> σ)
[]
| CmpXchgS l v1 v2 vl σ b :
σ.(heap) !! l = Some $ Some vl →
vals_compare_safe vl v1 →
b = bool_decide (vl = v1) →
head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
(Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=Some v2]> σ else σ)
[]
| FaaS l i1 i2 σ :
σ.(heap) !! l = Some $ Some (LitV (LitInt i1)) →
head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
[]
(Val $ LitV $ LitInt i1) (state_upd_heap <[l:=Some $ LitV (LitInt (i1 + i2))]>σ)
[]
| NewProphS σ p :
p ∉ σ.(used_proph_id) →
head_step NewProph σ
[]
(Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪.) σ)
[]
| ResolveS p v e σ w σ' κs ts :
head_step e σ κs (Val v) σ' ts →
head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
(κs ++ [(p, (v, w))]) (Val v) σ' ts.
Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
admit.
Defined.
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
Coercion App : expr >-> Funclass.
Coercion Val : val >-> expr.
Coercion Var : string >-> expr.
Notation Lam x e := (Rec BAnon x e) (only parsing).
Notation LamV x e := (RecV BAnon x e) (only parsing).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "()" := LitUnit : val_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
Notation SOME x := (InjR x) (only parsing).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Export iris.base_logic.lib.proph_map.
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc (option val) Σ;
heapG_inv_heapG :> inv_heapG loc (option val) Σ;
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
}.
Global Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ _ κs _ :=
(gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
fork_post _ := True%I;
num_laters_per_step _ := 0;
state_interp_mono _ _ _ _ := fupd_intro _ _
}.
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0.
Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
Import iris.algebra.excl.
Import iris.algebra.agree.
Import iris.algebra.csum.
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(λ: "n",
CAS "x" NONE (SOME "n")),
(λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
NONE => #()
| SOME "n" =>
match: !"x" with
NONE => assert: #false
| SOME "m" => assert: "n" = "m"
end
end)).
Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Section proof.
Context `{!heapG Σ, !one_shotG Σ}.
Lemma wp_one_shot (Φ : val → iProp Σ) :
(∀ f1 f2 : val,
(∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
□ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
⊢ WP one_shot_example #() {{ Φ }}.
EOF
make -j2 tests/one_shot.vo@coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
coqbot
commented
3 years ago @JasonGross, test comment
coqbot
commented
3 years ago @JasonGross, test comment
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
Zimmi48
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.voHey @Zimmi48, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.
JasonGross
commented
3 years ago GitHub has a comment length limit of 65536 characters. Let's try again now that I've updated the truncation code.
JasonGross
commented
3 years ago @coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.vo@coqbot minimize
git clone https://gitlab.mpi-sws.org/iris/iris.git && cd iris && git checkout 59d18188f9db844a75f5e37dc7cbc6c39ecbb24f
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
make builddep OPAMFLAGS=-y
make -j2 tests/one_shot.vo
Sort-of a dummy issue to test the bug minimizer here, hopefully @coqbot is watching
Spun off from https://github.com/coq/coq/issues/13942