Library zoo.language.language
Require Import zoo.prelude.
Require Export zoo.language.semantics.
Require Import zoo.options.
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type κ κs : list observation.
Implicit Type k : ectxi.
Implicit Type K : ectx.
Implicit Type ρ : 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 ˖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.
Require Export zoo.language.semantics.
Require Import zoo.options.
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type σ : state.
Implicit Type κ κs : list observation.
Implicit Type k : ectxi.
Implicit Type K : ectx.
Implicit Type ρ : 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 ˖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.