Library zoo.language.language
From zoo Require Import
prelude.
From zoo.language Require Export
semantics.
From zoo Require Import
options.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Implicit Types k : ectxi.
Implicit Types K : ectx.
Implicit Types ρ : config.
Declare Scope expr_scope.
Delimit Scope expr_scope with E.
Bind Scope expr_scope with expr.
Declare Scope val_scope.
Delimit Scope val_scope with V.
Bind Scope val_scope with val.
Class AsVal e v :=
as_val : of_val v = e.
Variant prim_step tid e1 σ1 κ e2 σ2 es : Prop :=
| base_step_fill_prim_step' K e1' e2' :
e1 = fill K e1' →
e2 = fill K e2' →
base_step tid e1' σ1 κ e2' σ2 es →
prim_step tid e1 σ1 κ e2 σ2 es.
#[global] Arguments base_step_fill_prim_step' {_ _ _ _ _ _ _}.
Definition step ρ1 κ ρ2 :=
∃ tid e1 e2 σ2 es,
prim_step tid e1 ρ1.2 κ e2 σ2 es ∧
ρ1.1 !! tid = Some e1 ∧
ρ2 = (<[tid := e2]> ρ1.1 ++ es, σ2).
Inductive nsteps : nat → config → list observation → config → Prop :=
| nsteps_refl ρ :
nsteps 0 ρ [] ρ
| nsteps_l n ρ1 ρ2 ρ3 κ κs :
step ρ1 κ ρ2 →
nsteps n ρ2 κs ρ3 →
nsteps (S n) ρ1 (κ ++ κs) ρ3.
#[local] Hint Constructors nsteps : core.
Definition silent_step ρ1 ρ2 :=
∃ κ,
step ρ1 κ ρ2.
Definition base_reducible tid e σ :=
∃ κ e' σ' es,
base_step tid e σ κ e' σ' es.
Definition base_reducible_no_obs tid e σ :=
∃ e' σ' es,
base_step tid e σ [] e' σ' es.
Definition base_irreducible tid e σ :=
∀ κ e' σ' es,
¬ base_step tid e σ κ e' σ' es.
Definition base_stuck tid e σ :=
to_val e = None ∧
base_irreducible tid e σ.
Definition base_atomic e :=
∀ tid σ κ e' σ' es,
base_step tid e σ κ e' σ' es →
is_Some (to_val e').
Record pure_base_step e1 e2 :=
{ pure_base_step_safe tid σ1 :
base_reducible_no_obs tid e1 σ1
; pure_base_step_det tid σ1 κ e2' σ2 es :
base_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
}.
Definition reducible tid e σ :=
∃ κ e' σ' es,
prim_step tid e σ κ e' σ' es.
Definition reducible_no_obs tid e σ :=
∃ e' σ' es,
prim_step tid e σ [] e' σ' es.
Definition irreducible tid e σ :=
∀ κ e' σ' es,
¬ prim_step tid e σ κ e' σ' es.
Definition stuck tid e σ :=
to_val e = None ∧
irreducible tid e σ.
Definition not_stuck tid e σ :=
is_Some (to_val e) ∨
reducible tid e σ.
Class Atomic e :=
atomic tid σ e' κ σ' es :
prim_step tid e σ κ e' σ' es →
is_Some (to_val e').
Definition safe ρ :=
∀ ρ',
rtc silent_step ρ ρ' →
Foralli (λ tid e, not_stuck tid e ρ'.2) ρ'.1.
Record pure_step e1 e2 :=
{ pure_step_safe tid σ1 :
reducible_no_obs tid e1 σ1
; pure_step_det tid σ1 κ e2' σ2 es :
prim_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
}.
Class Context (K : expr → expr) :=
{ context_fill_not_val e :
to_val e = None →
to_val (K e) = None
; context_fill_step tid e1 σ1 κ e2 σ2 es :
prim_step tid e1 σ1 κ e2 σ2 es →
prim_step tid (K e1) σ1 κ (K e2) σ2 es
; context_fill_step_inv tid e1' σ1 κ e2 σ2 es :
to_val e1' = None →
prim_step tid (K e1') σ1 κ e2 σ2 es →
∃ e2',
e2 = K e2' ∧
prim_step tid e1' σ1 κ e2' σ2 es
}.
Class PureExec (ϕ : Prop) n e1 e2 :=
pure_exec :
ϕ →
relations.nsteps pure_step n e1 e2.
Definition sub_redexes_are_values e :=
∀ K e', e = fill K e' →
to_val e' = None →
K = [].
#[global] Instance filli_inj k :
Inj (=) (=) (filli k).
Lemma filli_val k e :
is_Some (to_val (filli k e)) →
is_Some (to_val e).
Lemma filli_no_val_inj k1 e1 k2 e2 :
to_val e1 = None →
to_val e2 = None →
filli k1 e1 = filli k2 e2 →
k1 = k2.
Lemma base_step_filli_val tid k e σ1 κ e2 σ2 es :
base_step tid (filli k e) σ1 κ e2 σ2 es →
is_Some (to_val e).
#[global] Instance fill_inj K :
Inj (=) (=) (fill K).
Lemma fill_nil e :
fill [] e = e.
Lemma fill_app K1 K2 e :
fill (K1 ++ K2) e = fill K2 (fill K1 e).
Lemma fill_val K e :
is_Some (to_val (fill K e)) →
is_Some (to_val e).
Lemma fill_not_val K e :
to_val e = None →
to_val (fill K e) = None.
Lemma base_step_not_val tid e1 σ1 κ e2 σ2 es :
base_step tid e1 σ1 κ e2 σ2 es →
to_val e1 = None.
Lemma step_by_val tid K1 K2 e1 e2 σ1 κ e2' σ2 es :
fill K1 e1 = fill K2 e2 →
to_val e1 = None →
base_step tid e2 σ1 κ e2' σ2 es →
∃ K,
K2 = K ++ K1.
Lemma base_step_fill_val tid K e σ1 κ e2 σ2 es :
base_step tid (fill K e) σ1 κ e2 σ2 es →
is_Some (to_val e) ∨
K = [].
Lemma base_reducible_no_obs_base_reducible tid e σ :
base_reducible_no_obs tid e σ →
base_reducible tid e σ.
Lemma base_step_prim_step tid e1 σ1 κ e2 σ2 es :
base_step tid e1 σ1 κ e2 σ2 es →
prim_step tid e1 σ1 κ e2 σ2 es.
Lemma prim_step_not_val tid e σ κ e' σ' es :
prim_step tid e σ κ e' σ' es →
to_val e = None.
Lemma reducible_not_val tid e σ :
reducible tid e σ →
to_val e = None.
Lemma reducible_no_obs_reducible tid e σ :
reducible_no_obs tid e σ →
reducible tid e σ.
Lemma base_reducible_reducible tid e σ :
base_reducible tid e σ →
reducible tid e σ.
Lemma base_atomic_atomic e :
base_atomic e →
sub_redexes_are_values e →
Atomic e.
Lemma base_reducible_fill_prim_step tid K e1 σ1 κ e2 σ2 es :
base_reducible tid e1 σ1 →
prim_step tid (fill K e1) σ1 κ e2 σ2 es →
∃ e2',
e2 = fill K e2' ∧
base_step tid e1 σ1 κ e2' σ2 es.
Lemma base_reducible_prim_step tid e1 σ1 κ e2 σ2 es :
base_reducible tid e1 σ1 →
prim_step tid e1 σ1 κ e2 σ2 es →
base_step tid e1 σ1 κ e2 σ2 es.
Lemma pure_base_step_pure_step e1 e2 :
pure_base_step e1 e2 →
pure_step e1 e2.
#[global] Instance context_id :
Context (@id expr).
#[global] Instance context_fill K :
Context (fill K).
#[global] Instance context_filli k :
Context (filli k).
Lemma reducible_context (K : expr → expr) `{!Context K} tid e σ :
reducible tid e σ →
reducible tid (K e) σ.
Lemma reducible_context_inv (K : expr → expr) `{!Context K} tid e σ :
to_val e = None →
reducible tid (K e) σ →
reducible tid e σ.
Lemma pure_step_context (K : expr → expr) `{!Context K} e1 e2 :
pure_step e1 e2 →
pure_step (K e1) (K e2).
Lemma pure_step_nsteps_context (K : expr → expr) `{!Context K} n e1 e2 :
relations.nsteps pure_step n e1 e2 →
relations.nsteps pure_step n (K e1) (K e2).
Lemma pure_exec_context (K : expr → expr) `{!Context K} ϕ n e1 e2 :
PureExec ϕ n e1 e2 →
PureExec ϕ n (K e1) (K e2).
Lemma pure_exec_fill K ϕ n e1 e2 :
PureExec ϕ n e1 e2 →
PureExec ϕ n (fill K e1) (fill K e2).
Lemma sub_redexes_are_values_alt e :
( ∀ k e',
e = filli k e' →
is_Some (to_val e')
) →
sub_redexes_are_values e.
Lemma to_val_fill_some K e v :
to_val (fill K e) = Some v →
K = [] ∧ e = Val v.
Lemma prim_step_to_val_is_base_step tid e σ1 κ v σ2 es :
prim_step tid e σ1 κ (Val v) σ2 es →
base_step tid e σ1 κ (Val v) σ2 es.
Lemma silent_steps_nsteps ρ1 ρ2 :
rtc silent_step ρ1 ρ2 ↔
∃ n κs,
nsteps n ρ1 κs ρ2.
Lemma step_length ρ1 κ ρ2 :
step ρ1 κ ρ2 →
length ρ1.1 ≤ length ρ2.1.
Lemma nsteps_length n ρ1 κs ρ2 :
nsteps n ρ1 κs ρ2 →
length ρ1.1 ≤ length ρ2.1.
Lemma base_reducible_no_obs_equal tid v1 v2 σ :
base_reducible_no_obs tid (Equal (Val v1) (Val v2)) σ.
Lemma base_reducible_equal tid v1 v2 σ :
base_reducible tid (Equal (Val v1) (Val v2)) σ.
Lemma reducible_equal tid v1 v2 σ :
reducible tid (Equal (Val v1) (Val v2)) σ.
Lemma base_reducible_no_obs_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
base_reducible_no_obs tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma base_reducible_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
base_reducible tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma reducible_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
reducible tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma reducible_resolve tid e σ pid v :
Atomic e →
reducible tid e σ →
reducible tid (Resolve e (Val $ ValProph pid) (Val v)) σ.
Lemma prim_step_resolve_inv tid e v1 v2 σ1 κ e2 σ2 es :
Atomic e →
prim_step tid (Resolve e (Val v1) (Val v2)) σ1 κ e2 σ2 es →
base_step tid (Resolve e (Val v1) (Val v2)) σ1 κ e2 σ2 es.
prelude.
From zoo.language Require Export
semantics.
From zoo Require Import
options.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Implicit Types k : ectxi.
Implicit Types K : ectx.
Implicit Types ρ : config.
Declare Scope expr_scope.
Delimit Scope expr_scope with E.
Bind Scope expr_scope with expr.
Declare Scope val_scope.
Delimit Scope val_scope with V.
Bind Scope val_scope with val.
Class AsVal e v :=
as_val : of_val v = e.
Variant prim_step tid e1 σ1 κ e2 σ2 es : Prop :=
| base_step_fill_prim_step' K e1' e2' :
e1 = fill K e1' →
e2 = fill K e2' →
base_step tid e1' σ1 κ e2' σ2 es →
prim_step tid e1 σ1 κ e2 σ2 es.
#[global] Arguments base_step_fill_prim_step' {_ _ _ _ _ _ _}.
Definition step ρ1 κ ρ2 :=
∃ tid e1 e2 σ2 es,
prim_step tid e1 ρ1.2 κ e2 σ2 es ∧
ρ1.1 !! tid = Some e1 ∧
ρ2 = (<[tid := e2]> ρ1.1 ++ es, σ2).
Inductive nsteps : nat → config → list observation → config → Prop :=
| nsteps_refl ρ :
nsteps 0 ρ [] ρ
| nsteps_l n ρ1 ρ2 ρ3 κ κs :
step ρ1 κ ρ2 →
nsteps n ρ2 κs ρ3 →
nsteps (S n) ρ1 (κ ++ κs) ρ3.
#[local] Hint Constructors nsteps : core.
Definition silent_step ρ1 ρ2 :=
∃ κ,
step ρ1 κ ρ2.
Definition base_reducible tid e σ :=
∃ κ e' σ' es,
base_step tid e σ κ e' σ' es.
Definition base_reducible_no_obs tid e σ :=
∃ e' σ' es,
base_step tid e σ [] e' σ' es.
Definition base_irreducible tid e σ :=
∀ κ e' σ' es,
¬ base_step tid e σ κ e' σ' es.
Definition base_stuck tid e σ :=
to_val e = None ∧
base_irreducible tid e σ.
Definition base_atomic e :=
∀ tid σ κ e' σ' es,
base_step tid e σ κ e' σ' es →
is_Some (to_val e').
Record pure_base_step e1 e2 :=
{ pure_base_step_safe tid σ1 :
base_reducible_no_obs tid e1 σ1
; pure_base_step_det tid σ1 κ e2' σ2 es :
base_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
}.
Definition reducible tid e σ :=
∃ κ e' σ' es,
prim_step tid e σ κ e' σ' es.
Definition reducible_no_obs tid e σ :=
∃ e' σ' es,
prim_step tid e σ [] e' σ' es.
Definition irreducible tid e σ :=
∀ κ e' σ' es,
¬ prim_step tid e σ κ e' σ' es.
Definition stuck tid e σ :=
to_val e = None ∧
irreducible tid e σ.
Definition not_stuck tid e σ :=
is_Some (to_val e) ∨
reducible tid e σ.
Class Atomic e :=
atomic tid σ e' κ σ' es :
prim_step tid e σ κ e' σ' es →
is_Some (to_val e').
Definition safe ρ :=
∀ ρ',
rtc silent_step ρ ρ' →
Foralli (λ tid e, not_stuck tid e ρ'.2) ρ'.1.
Record pure_step e1 e2 :=
{ pure_step_safe tid σ1 :
reducible_no_obs tid e1 σ1
; pure_step_det tid σ1 κ e2' σ2 es :
prim_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
}.
Class Context (K : expr → expr) :=
{ context_fill_not_val e :
to_val e = None →
to_val (K e) = None
; context_fill_step tid e1 σ1 κ e2 σ2 es :
prim_step tid e1 σ1 κ e2 σ2 es →
prim_step tid (K e1) σ1 κ (K e2) σ2 es
; context_fill_step_inv tid e1' σ1 κ e2 σ2 es :
to_val e1' = None →
prim_step tid (K e1') σ1 κ e2 σ2 es →
∃ e2',
e2 = K e2' ∧
prim_step tid e1' σ1 κ e2' σ2 es
}.
Class PureExec (ϕ : Prop) n e1 e2 :=
pure_exec :
ϕ →
relations.nsteps pure_step n e1 e2.
Definition sub_redexes_are_values e :=
∀ K e', e = fill K e' →
to_val e' = None →
K = [].
#[global] Instance filli_inj k :
Inj (=) (=) (filli k).
Lemma filli_val k e :
is_Some (to_val (filli k e)) →
is_Some (to_val e).
Lemma filli_no_val_inj k1 e1 k2 e2 :
to_val e1 = None →
to_val e2 = None →
filli k1 e1 = filli k2 e2 →
k1 = k2.
Lemma base_step_filli_val tid k e σ1 κ e2 σ2 es :
base_step tid (filli k e) σ1 κ e2 σ2 es →
is_Some (to_val e).
#[global] Instance fill_inj K :
Inj (=) (=) (fill K).
Lemma fill_nil e :
fill [] e = e.
Lemma fill_app K1 K2 e :
fill (K1 ++ K2) e = fill K2 (fill K1 e).
Lemma fill_val K e :
is_Some (to_val (fill K e)) →
is_Some (to_val e).
Lemma fill_not_val K e :
to_val e = None →
to_val (fill K e) = None.
Lemma base_step_not_val tid e1 σ1 κ e2 σ2 es :
base_step tid e1 σ1 κ e2 σ2 es →
to_val e1 = None.
Lemma step_by_val tid K1 K2 e1 e2 σ1 κ e2' σ2 es :
fill K1 e1 = fill K2 e2 →
to_val e1 = None →
base_step tid e2 σ1 κ e2' σ2 es →
∃ K,
K2 = K ++ K1.
Lemma base_step_fill_val tid K e σ1 κ e2 σ2 es :
base_step tid (fill K e) σ1 κ e2 σ2 es →
is_Some (to_val e) ∨
K = [].
Lemma base_reducible_no_obs_base_reducible tid e σ :
base_reducible_no_obs tid e σ →
base_reducible tid e σ.
Lemma base_step_prim_step tid e1 σ1 κ e2 σ2 es :
base_step tid e1 σ1 κ e2 σ2 es →
prim_step tid e1 σ1 κ e2 σ2 es.
Lemma prim_step_not_val tid e σ κ e' σ' es :
prim_step tid e σ κ e' σ' es →
to_val e = None.
Lemma reducible_not_val tid e σ :
reducible tid e σ →
to_val e = None.
Lemma reducible_no_obs_reducible tid e σ :
reducible_no_obs tid e σ →
reducible tid e σ.
Lemma base_reducible_reducible tid e σ :
base_reducible tid e σ →
reducible tid e σ.
Lemma base_atomic_atomic e :
base_atomic e →
sub_redexes_are_values e →
Atomic e.
Lemma base_reducible_fill_prim_step tid K e1 σ1 κ e2 σ2 es :
base_reducible tid e1 σ1 →
prim_step tid (fill K e1) σ1 κ e2 σ2 es →
∃ e2',
e2 = fill K e2' ∧
base_step tid e1 σ1 κ e2' σ2 es.
Lemma base_reducible_prim_step tid e1 σ1 κ e2 σ2 es :
base_reducible tid e1 σ1 →
prim_step tid e1 σ1 κ e2 σ2 es →
base_step tid e1 σ1 κ e2 σ2 es.
Lemma pure_base_step_pure_step e1 e2 :
pure_base_step e1 e2 →
pure_step e1 e2.
#[global] Instance context_id :
Context (@id expr).
#[global] Instance context_fill K :
Context (fill K).
#[global] Instance context_filli k :
Context (filli k).
Lemma reducible_context (K : expr → expr) `{!Context K} tid e σ :
reducible tid e σ →
reducible tid (K e) σ.
Lemma reducible_context_inv (K : expr → expr) `{!Context K} tid e σ :
to_val e = None →
reducible tid (K e) σ →
reducible tid e σ.
Lemma pure_step_context (K : expr → expr) `{!Context K} e1 e2 :
pure_step e1 e2 →
pure_step (K e1) (K e2).
Lemma pure_step_nsteps_context (K : expr → expr) `{!Context K} n e1 e2 :
relations.nsteps pure_step n e1 e2 →
relations.nsteps pure_step n (K e1) (K e2).
Lemma pure_exec_context (K : expr → expr) `{!Context K} ϕ n e1 e2 :
PureExec ϕ n e1 e2 →
PureExec ϕ n (K e1) (K e2).
Lemma pure_exec_fill K ϕ n e1 e2 :
PureExec ϕ n e1 e2 →
PureExec ϕ n (fill K e1) (fill K e2).
Lemma sub_redexes_are_values_alt e :
( ∀ k e',
e = filli k e' →
is_Some (to_val e')
) →
sub_redexes_are_values e.
Lemma to_val_fill_some K e v :
to_val (fill K e) = Some v →
K = [] ∧ e = Val v.
Lemma prim_step_to_val_is_base_step tid e σ1 κ v σ2 es :
prim_step tid e σ1 κ (Val v) σ2 es →
base_step tid e σ1 κ (Val v) σ2 es.
Lemma silent_steps_nsteps ρ1 ρ2 :
rtc silent_step ρ1 ρ2 ↔
∃ n κs,
nsteps n ρ1 κs ρ2.
Lemma step_length ρ1 κ ρ2 :
step ρ1 κ ρ2 →
length ρ1.1 ≤ length ρ2.1.
Lemma nsteps_length n ρ1 κs ρ2 :
nsteps n ρ1 κs ρ2 →
length ρ1.1 ≤ length ρ2.1.
Lemma base_reducible_no_obs_equal tid v1 v2 σ :
base_reducible_no_obs tid (Equal (Val v1) (Val v2)) σ.
Lemma base_reducible_equal tid v1 v2 σ :
base_reducible tid (Equal (Val v1) (Val v2)) σ.
Lemma reducible_equal tid v1 v2 σ :
reducible tid (Equal (Val v1) (Val v2)) σ.
Lemma base_reducible_no_obs_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
base_reducible_no_obs tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma base_reducible_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
base_reducible tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma reducible_cas tid l fld v1 v2 v σ :
σ.(state_heap) !! (l +ₗ fld) = Some v →
reducible tid (CAS (Val $ ValTuple [ValLoc l; ValInt fld]) (Val v1) (Val v2)) σ.
Lemma reducible_resolve tid e σ pid v :
Atomic e →
reducible tid e σ →
reducible tid (Resolve e (Val $ ValProph pid) (Val v)) σ.
Lemma prim_step_resolve_inv tid e v1 v2 σ1 κ e2 σ2 es :
Atomic e →
prim_step tid (Resolve e (Val v1) (Val v2)) σ1 κ e2 σ2 es →
base_step tid (Resolve e (Val v1) (Val v2)) σ1 κ e2 σ2 es.