Commit f81eedba authored by Amin Timany's avatar Amin Timany

Change iris_logrel to logrel

parent 61a4a07a
...@@ -7,44 +7,44 @@ theories/barrier/protocol.v ...@@ -7,44 +7,44 @@ theories/barrier/protocol.v
theories/barrier/example_client.v theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v theories/barrier/example_joining_existentials.v
theories/iris_logrel/prelude/base.v theories/logrel/prelude/base.v
theories/iris_logrel/stlc/lang.v theories/logrel/stlc/lang.v
theories/iris_logrel/stlc/typing.v theories/logrel/stlc/typing.v
theories/iris_logrel/stlc/rules.v theories/logrel/stlc/rules.v
theories/iris_logrel/stlc/logrel.v theories/logrel/stlc/logrel.v
theories/iris_logrel/stlc/fundamental.v theories/logrel/stlc/fundamental.v
theories/iris_logrel/stlc/soundness.v theories/logrel/stlc/soundness.v
theories/iris_logrel/F_mu/lang.v theories/logrel/F_mu/lang.v
theories/iris_logrel/F_mu/typing.v theories/logrel/F_mu/typing.v
theories/iris_logrel/F_mu/rules.v theories/logrel/F_mu/rules.v
theories/iris_logrel/F_mu/logrel.v theories/logrel/F_mu/logrel.v
theories/iris_logrel/F_mu/fundamental.v theories/logrel/F_mu/fundamental.v
theories/iris_logrel/F_mu/soundness.v theories/logrel/F_mu/soundness.v
theories/iris_logrel/F_mu_ref/lang.v theories/logrel/F_mu_ref/lang.v
theories/iris_logrel/F_mu_ref/typing.v theories/logrel/F_mu_ref/typing.v
theories/iris_logrel/F_mu_ref/rules.v theories/logrel/F_mu_ref/rules.v
theories/iris_logrel/F_mu_ref/rules_binary.v theories/logrel/F_mu_ref/rules_binary.v
theories/iris_logrel/F_mu_ref/logrel.v theories/logrel/F_mu_ref/logrel.v
theories/iris_logrel/F_mu_ref/logrel_binary.v theories/logrel/F_mu_ref/logrel_binary.v
theories/iris_logrel/F_mu_ref/fundamental.v theories/logrel/F_mu_ref/fundamental.v
theories/iris_logrel/F_mu_ref/fundamental_binary.v theories/logrel/F_mu_ref/fundamental_binary.v
theories/iris_logrel/F_mu_ref/soundness.v theories/logrel/F_mu_ref/soundness.v
theories/iris_logrel/F_mu_ref/context_refinement.v theories/logrel/F_mu_ref/context_refinement.v
theories/iris_logrel/F_mu_ref/soundness_binary.v theories/logrel/F_mu_ref/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/lang.v theories/logrel/F_mu_ref_conc/lang.v
theories/iris_logrel/F_mu_ref_conc/rules.v theories/logrel/F_mu_ref_conc/rules.v
theories/iris_logrel/F_mu_ref_conc/typing.v theories/logrel/F_mu_ref_conc/typing.v
theories/iris_logrel/F_mu_ref_conc/logrel_unary.v theories/logrel/F_mu_ref_conc/logrel_unary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_unary.v theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/iris_logrel/F_mu_ref_conc/rules_binary.v theories/logrel/F_mu_ref_conc/rules_binary.v
theories/iris_logrel/F_mu_ref_conc/logrel_binary.v theories/logrel/F_mu_ref_conc/logrel_binary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_binary.v theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/iris_logrel/F_mu_ref_conc/soundness_unary.v theories/logrel/F_mu_ref_conc/soundness_unary.v
theories/iris_logrel/F_mu_ref_conc/context_refinement.v theories/logrel/F_mu_ref_conc/context_refinement.v
theories/iris_logrel/F_mu_ref_conc/soundness_binary.v theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/examples/lock.v theories/logrel/F_mu_ref_conc/examples/lock.v
theories/iris_logrel/F_mu_ref_conc/examples/counter.v theories/logrel/F_mu_ref_conc/examples/counter.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/stack_rules.v theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/CG_stack.v theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/FG_stack.v theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/refinement.v theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file \ No newline at end of file
From iris_examples.iris_logrel.F_mu Require Export logrel. From iris_examples.logrel.F_mu Require Export logrel.
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.F_mu Require Import rules. From iris_examples.logrel.F_mu Require Import rules.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs, Definition log_typed `{irisG F_mu_lang Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
......
From iris.program_logic Require Export language ectx_language ectxi_language. From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.iris_logrel.prelude Require Export base. From iris_examples.logrel.prelude Require Export base.
Module F_mu. Module F_mu.
Inductive expr := Inductive expr :=
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris_examples.iris_logrel.F_mu Require Export lang typing. From iris_examples.logrel.F_mu Require Export lang typing.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
Import uPred. Import uPred.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
From iris_examples.iris_logrel.F_mu Require Export lang. From iris_examples.logrel.F_mu Require Export lang.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
Section lang_rules. Section lang_rules.
......
From iris_examples.iris_logrel.F_mu Require Export fundamental. From iris_examples.logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
......
From iris_examples.iris_logrel.F_mu Require Export lang. From iris_examples.logrel.F_mu Require Export lang.
Inductive type := Inductive type :=
| TUnit : type | TUnit : type
......
From iris_examples.iris_logrel.F_mu_ref Require Export fundamental_binary. From iris_examples.logrel.F_mu_ref Require Export fundamental_binary.
Inductive ctx_item := Inductive ctx_item :=
| CTX_Lam | CTX_Lam
......
From iris_examples.iris_logrel.F_mu_ref Require Export logrel. From iris_examples.logrel.F_mu_ref Require Export logrel.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
From iris_examples.iris_logrel.F_mu_ref Require Import rules. From iris_examples.logrel.F_mu_ref Require Import rules.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs, Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := Δ vs,
......
From iris_examples.iris_logrel.F_mu_ref Require Export logrel_binary. From iris_examples.logrel.F_mu_ref Require Export logrel_binary.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
From iris_examples.iris_logrel.F_mu_ref Require Import rules_binary. From iris_examples.logrel.F_mu_ref Require Import rules_binary.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
Section bin_log_def. Section bin_log_def.
......
From iris.program_logic Require Export language ectx_language ectxi_language. From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.iris_logrel.prelude Require Export base. From iris_examples.logrel.prelude Require Export base.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
From stdpp Require Import gmap. From stdpp Require Import gmap.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris_examples.iris_logrel.F_mu_ref Require Export rules typing. From iris_examples.logrel.F_mu_ref Require Export rules typing.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
Import uPred. Import uPred.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op invariants. From iris.base_logic Require Export big_op invariants.
From iris_examples.iris_logrel.F_mu_ref Require Export rules_binary typing. From iris_examples.logrel.F_mu_ref Require Export rules_binary typing.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From stdpp Require Import tactics. From stdpp Require Import tactics.
Import uPred. Import uPred.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants big_op. From iris.base_logic Require Export invariants big_op.
From iris.algebra Require Import auth frac agree gmap. From iris.algebra Require Import auth frac agree gmap.
From iris_examples.iris_logrel.F_mu_ref Require Export lang. From iris_examples.logrel.F_mu_ref Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap. From iris.base_logic Require Export gen_heap.
Import uPred. Import uPred.
......
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
From iris.algebra Require Import auth frac agree gmap list. From iris.algebra Require Import auth frac agree gmap list.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris_examples.iris_logrel.F_mu_ref Require Export rules. From iris_examples.logrel.F_mu_ref Require Export rules.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
......
From iris_examples.iris_logrel.F_mu_ref Require Export fundamental. From iris_examples.logrel.F_mu_ref Require Export fundamental.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth. From iris.base_logic Require Import auth.
......
From iris_examples.iris_logrel.F_mu_ref Require Export context_refinement. From iris_examples.logrel.F_mu_ref Require Export context_refinement.
From iris.algebra Require Import auth frac agree. From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
From iris_examples.iris_logrel.F_mu_ref Require Import soundness. From iris_examples.logrel.F_mu_ref Require Import soundness.
Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)} Lemma basic_soundness Σ `{heapPreG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp : e e' τ v thp hp :
......
From iris_examples.iris_logrel.F_mu_ref Require Export lang. From iris_examples.logrel.F_mu_ref Require Export lang.
Inductive type := Inductive type :=
| TUnit : type | TUnit : type
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export lang fundamental_binary. From iris_examples.logrel.F_mu_ref_conc Require Export lang fundamental_binary.
Export F_mu_ref_conc. Export F_mu_ref_conc.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export examples.lock. From iris_examples.logrel.F_mu_ref_conc Require Export examples.lock.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import soundness_binary. From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
Definition CG_increment (x : expr) : expr := Definition CG_increment (x : expr) : expr :=
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export rules_binary typing. From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.base_logic Require Import namespaces. From iris.base_logic Require Import namespaces.
(** [newlock = alloc false] *) (** [newlock = alloc false] *)
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.base_logic Require Import namespaces. From iris.base_logic Require Import namespaces.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import examples.lock. From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
Import uPred. Import uPred.
Definition CG_StackType τ := Definition CG_StackType τ :=
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Import typing. From iris_examples.logrel.F_mu_ref_conc Require Import typing.
Definition FG_StackType τ := Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))). TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
......
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris.program_logic Require Import adequacy ectxi_language. From iris.program_logic Require Import adequacy ectxi_language.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import soundness_binary. From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.iris_logrel.F_mu_ref_conc.examples Require Import lock. From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.iris_logrel.F_mu_ref_conc.examples.stack Require Import From iris_examples.logrel.F_mu_ref_conc.examples.stack Require Import
CG_stack FG_stack stack_rules. CG_stack FG_stack stack_rules.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import logrel_binary. From iris_examples.logrel.F_mu_ref_conc Require Import logrel_binary.
From iris.algebra Require Import auth gmap agree. From iris.algebra Require Import auth gmap agree.
Import uPred. Import uPred.
From iris.algebra Require deprecated. From iris.algebra Require deprecated.
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export logrel_binary. From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import rules_binary. From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
From iris.program_logic Require Export lifting. From iris.program_logic Require Export lifting.
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export logrel_unary. From iris_examples.logrel.F_mu_ref_conc Require Export logrel_unary.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import rules. From iris_examples.logrel.F_mu_ref_conc Require Import rules.
From iris.base_logic Require Export big_op invariants. From iris.base_logic Require Export big_op invariants.
From iris.program_logic Require Export lifting. From iris.program_logic Require Export lifting.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
......
From iris.program_logic Require Export language ectx_language ectxi_language. From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.iris_logrel.prelude Require Export base. From iris_examples.logrel.prelude Require Export base.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
From stdpp Require Import gmap. From stdpp Require Import gmap.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op invariants. From iris.base_logic Require Export big_op invariants.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export rules_binary typing. From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From stdpp Require Import tactics. From stdpp Require Import tactics.
Import uPred. Import uPred.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export rules typing. From iris_examples.logrel.F_mu_ref_conc Require Export rules typing.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From iris.base_logic Require Import big_op namespaces invariants. From iris.base_logic Require Import big_op namespaces invariants.
Import uPred. Import uPred.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
From iris.base_logic Require Export invariants big_op. From iris.base_logic Require Export invariants big_op.
From iris.algebra Require Import auth frac agree gmap. From iris.algebra Require Import auth frac agree gmap.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export lang. From iris_examples.logrel.F_mu_ref_conc Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.base_logic Require Export gen_heap. From iris.base_logic Require Export gen_heap.
Import uPred. Import uPred.
......
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
From iris.algebra Require Import auth frac agree gmap list. From iris.algebra Require Import auth frac agree gmap list.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris_examples.iris_logrel.F_mu_ref_conc Require Export rules. From iris_examples.logrel.F_mu_ref_conc Require Export rules.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export context_refinement. From iris_examples.logrel.F_mu_ref_conc Require Export context_refinement.
From iris.algebra Require Import auth frac agree. From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
From iris_examples.iris_logrel.F_mu_ref_conc Require Import soundness_unary. From iris_examples.logrel.F_mu_ref_conc Require Import soundness_unary.
Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} Lemma basic_soundness Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
e e' τ v thp hp : e e' τ v thp hp :
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export fundamental_unary. From iris_examples.logrel.F_mu_ref_conc Require Export fundamental_unary.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
From iris.base_logic Require Import auth. From iris.base_logic Require Import auth.
......
From iris_examples.iris_logrel.F_mu_ref_conc Require Export lang. From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Inductive type := Inductive type :=
| TUnit : type | TUnit : type
......
From iris_examples.iris_logrel.stlc Require Export logrel. From iris_examples.logrel.stlc Require Export logrel.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris_examples.iris_logrel.stlc Require Import rules. From iris_examples.logrel.stlc Require Import rules.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
From iris.program_logic Require Import lifting. From iris.program_logic Require Import lifting.
......
From iris.program_logic Require Export language ectx_language ectxi_language. From iris.program_logic Require Export language ectx_language ectxi_language.
From iris_examples.iris_logrel.prelude Require Export base. From iris_examples.logrel.prelude Require Export base.
Module stlc. Module stlc.
Inductive expr := Inductive expr :=
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op. From iris.base_logic Require Export big_op.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris_examples.iris_logrel.stlc Require Export lang typing. From iris_examples.logrel.stlc Require Export lang typing.
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
From iris_examples.iris_logrel.stlc Require Export lang. From iris_examples.logrel.stlc Require Export lang.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
Section stlc_rules. Section stlc_rules.
......
From iris_examples.iris_logrel.stlc Require Export fundamental. From iris_examples.logrel.stlc Require Export fundamental.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy. From iris.program_logic Require Import adequacy.
......
From iris_examples.iris_logrel.stlc Require Export lang. From iris_examples.logrel.stlc Require Export lang.
Inductive type := Inductive type :=
| TUnit : type | TUnit : type
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment