clutch.gen_prob_lang.lang
From Stdlib Require Import Reals Psatz.
From stdpp Require Export binders strings.
From stdpp Require Import gmap fin_maps countable fin.
From iris.algebra Require Export ofe.
From clutch.prelude Require Export stdpp_ext.
From clutch.prob Require Export distribution.
From clutch.common Require Export language ectx_language ectxi_language locations.
From iris.prelude Require Import options.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Module gen_prob_lang.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitLbl (l : loc).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
| AndOp | OrOp | XorOp (* Bitwise *)
| ShiftLOp | ShiftROp (* Shifts *)
| LeOp | LtOp | EqOp (* Relations *)
| OffsetOp. (* Pointer offset *)
Inductive expr :=
(* Values *)
| Val (v : val)
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
(* Heap *)
| AllocN (e1 e2 : expr) (* Array length and initial value *)
| Deref (e : expr)
| Store (e1 : expr) (e2 : expr)
(* Probabilistic choice: sample from distribution family i, parameter value e1, tape e2
(e2 = unit ⇒ direct sampling; a label ⇒ tape-based) *)
| Sample (i : nat) (e1 e2 : expr)
| AllocSampleTape (i : nat) (e1 : expr)
(* No-op operator used for cost *)
| Tick (e : 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 expr_scope with expr.
Bind Scope val_scope with val.
Notation of_val := Val (only parsing).
Definition to_val (e : expr) : option val :=
match e with
| Val v => Some v
| _ => None
end.
Definition def_val : val := LitV LitUnit.
From stdpp Require Export binders strings.
From stdpp Require Import gmap fin_maps countable fin.
From iris.algebra Require Export ofe.
From clutch.prelude Require Export stdpp_ext.
From clutch.prob Require Export distribution.
From clutch.common Require Export language ectx_language ectxi_language locations.
From iris.prelude Require Import options.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Module gen_prob_lang.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) | LitLbl (l : loc).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
| AndOp | OrOp | XorOp (* Bitwise *)
| ShiftLOp | ShiftROp (* Shifts *)
| LeOp | LtOp | EqOp (* Relations *)
| OffsetOp. (* Pointer offset *)
Inductive expr :=
(* Values *)
| Val (v : val)
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
(* Heap *)
| AllocN (e1 e2 : expr) (* Array length and initial value *)
| Deref (e : expr)
| Store (e1 : expr) (e2 : expr)
(* Probabilistic choice: sample from distribution family i, parameter value e1, tape e2
(e2 = unit ⇒ direct sampling; a label ⇒ tape-based) *)
| Sample (i : nat) (e1 e2 : expr)
| AllocSampleTape (i : nat) (e1 : expr)
(* No-op operator used for cost *)
| Tick (e : 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 expr_scope with expr.
Bind Scope val_scope with val.
Notation of_val := Val (only parsing).
Definition to_val (e : expr) : option val :=
match e with
| Val v => Some v
| _ => None
end.
Definition def_val : val := LitV LitUnit.
We assume the following encoding of values to 64-bit words: The least 3
significant bits of every word are a "tag", and we have 61 bits of payload,
which is enough if all pointers are 8-byte-aligned (common on 64bit
architectures). The tags have the following meaning:
0: Payload is the data for a LitV (LitInt _).
1: Payload is the data for a InjLV (LitV (LitInt _)).
2: Payload is the data for a InjRV (LitV (LitInt _)).
3: Payload is the data for a LitV (LitLoc _).
4: Payload is the data for a InjLV (LitV (LitLoc _)).
4: Payload is the data for a InjRV (LitV (LitLoc _)).
6: Payload is one of the following finitely many values, which 61 bits are more
than enough to encode:
LitV LitUnit, InjLV (LitV LitUnit), InjRV (LitV LitUnit),
LitV LitPoison, InjLV (LitV LitPoison), InjRV (LitV LitPoison),
LitV (LitBool _), InjLV (LitV (LitBool _)), InjRV (LitV (LitBool _)).
7: Value is boxed, i.e., payload is a pointer to some read-only memory area on
the heap which stores whether this is a RecV, PairV, InjLV or InjRV and the
relevant data for those cases. However, the boxed representation is never
used if any of the above representations could be used.
Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
bits, this means every value is machine-word-sized and can hence be atomically
read and written. Also notice that the sets of boxed and unboxed values are
disjoint.
Disallow comparing (erased) prophecies with (erased) prophecies, by
considering them boxed.
(* | LitProphecy _ | LitPoison => False *)
| LitInt _ | LitBool _ | LitLoc _ | LitLbl _ | 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 lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
Global Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
| LitInt _ | LitBool _ | LitLoc _ | LitLbl _ | 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 lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
Global Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
We just compare the word-sized representation of two values, without looking
into boxed data. This works out fine if at least one of the to-be-compared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets).
Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl ∨ val_is_unboxed v1.
Global Arguments vals_compare_safe !_ !_ /.
(* ---- generic tape entry: family index, parameter value, presampled outcomes ----
(the distribution signature SampleFamily/Sig/sig_sample is defined below,
after the Countable val instance it relies on.) *)
Definition stape : Type := (nat * val * list val)%type.
val_is_unboxed vl ∨ val_is_unboxed v1.
Global Arguments vals_compare_safe !_ !_ /.
(* ---- generic tape entry: family index, parameter value, presampled outcomes ----
(the distribution signature SampleFamily/Sig/sig_sample is defined below,
after the Countable val instance it relies on.) *)
Definition stape : Type := (nat * val * list val)%type.
Equality and other typeclass stuff
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. by destruct v. Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof. destruct e=>//=. by intros [= <-]. Qed.
Global Instance of_val_inj : Inj (=) (=) of_val.
Proof. intros ??. congruence. Qed.
Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Global Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
Global Instance expr_eq_dec : EqDecision expr.
Proof.
refine (
fix go (e1 e2 : expr) {struct e1} : Decision (e1 = e2) :=
match e1, e2 with
| Val v, Val v' => cast_if (decide (v = v'))
| Var x, Var x' => cast_if (decide (x = x'))
| Rec f x e, Rec f' x' e' =>
cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
| App e1 e2, App e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| UnOp o e, UnOp o' e' => cast_if_and (decide (o = o')) (decide (e = e'))
| BinOp o e1 e2, BinOp o' e1' e2' =>
cast_if_and3 (decide (o = o')) (decide (e1 = e1')) (decide (e2 = e2'))
| If e0 e1 e2, If e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| Pair e1 e2, Pair e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Fst e, Fst e' => cast_if (decide (e = e'))
| Snd e, Snd e' => cast_if (decide (e = e'))
| InjL e, InjL e' => cast_if (decide (e = e'))
| InjR e, InjR e' => cast_if (decide (e = e'))
| Case e0 e1 e2, Case e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| AllocN e1 e2, AllocN e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Deref e, Deref e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Sample i e1 e2, Sample i' e1' e2' =>
cast_if_and3 (decide (i = i')) (decide (e1 = e1')) (decide (e2 = e2'))
| AllocSampleTape i e1, AllocSampleTape i' e1' =>
cast_if_and (decide (i = i')) (decide (e1 = e1'))
| Tick e, Tick e' => cast_if (decide (e = e'))
| _, _ => right _
end
with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
match v1, v2 with
| LitV l, LitV l' => cast_if (decide (l = l'))
| RecV f x e, RecV f' x' e' =>
cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
| PairV e1 e2, PairV e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| InjLV e, InjLV e' => cast_if (decide (e = e'))
| InjRV e, InjRV e' => cast_if (decide (e = e'))
| _, _ => right _
end
for go); try (clear go gov; abstract intuition congruence).
Defined.
Global Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
Global Instance state_eq_dec : EqDecision state.
Proof. solve_decision. Defined.
Global Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => inl (inl n)
| LitBool b => inl (inr b)
| LitUnit => inr (inl ())
| LitLoc l => inr (inr (inr l))
| LitLbl l => inr (inr (inl l))
end) (λ l, match l with
| inl (inl n) => LitInt n
| inl (inr b) => LitBool b
| inr (inl ()) => LitUnit
| inr (inr (inr l)) => LitLoc l
| inr (inr (inl l)) => LitLbl l
end) _); by intros [].
Qed.
Global Instance un_op_finite : Countable un_op.
Proof.
refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
(λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Global Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable' (λ op, match op with
| PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
| AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
| LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
end) (λ n, match n with
| 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
| 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
| 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
end) _); by intros [].
Qed.
Global Instance expr_countable : Countable expr.
Proof.
set (enc :=
fix go e :=
match e with
| Val v => GenNode 0 [gov v]
| Var x => GenLeaf (inl (inl x))
| Rec f x e => GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
| App e1 e2 => GenNode 2 [go e1; go e2]
| UnOp op e => GenNode 3 [GenLeaf (inr (inr (inl op))); go e]
| BinOp op e1 e2 => GenNode 4 [GenLeaf (inr (inr (inr op))); go e1; go e2]
| If e0 e1 e2 => GenNode 5 [go e0; go e1; go e2]
| Pair e1 e2 => GenNode 6 [go e1; go e2]
| Fst e => GenNode 7 [go e]
| Snd e => GenNode 8 [go e]
| InjL e => GenNode 9 [go e]
| InjR e => GenNode 10 [go e]
| Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
| AllocN e1 e2 => GenNode 12 [go e1; go e2]
| Deref e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| AllocSampleTape i e1 => GenNode 15 [GenLeaf (inr (inl (LitInt (Z.of_nat i)))); go e1]
| Sample i e1 e2 => GenNode 16 [GenLeaf (inr (inl (LitInt (Z.of_nat i)))); go e1; go e2]
| Tick e => GenNode 19 [go e]
end
with gov v :=
match v with
| LitV l => GenLeaf (inr (inl l))
| RecV f x e =>
GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
| PairV v1 v2 => GenNode 1 [gov v1; gov v2]
| InjLV v => GenNode 2 [gov v]
| InjRV v => GenNode 3 [gov v]
end
for go).
set (dec :=
fix go e :=
match e with
| GenNode 0 [v] => Val (gov v)
| GenLeaf (inl (inl x)) => Var x
| GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
| GenNode 2 [e1; e2] => App (go e1) (go e2)
| GenNode 3 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
| GenNode 4 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
| GenNode 5 [e0; e1; e2] => If (go e0) (go e1) (go e2)
| GenNode 6 [e1; e2] => Pair (go e1) (go e2)
| GenNode 7 [e] => Fst (go e)
| GenNode 8 [e] => Snd (go e)
| GenNode 9 [e] => InjL (go e)
| GenNode 10 [e] => InjR (go e)
| GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
| GenNode 12 [e1 ; e2] => AllocN (go e1) (go e2)
| GenNode 13 [e] => Deref (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [GenLeaf (inr (inl (LitInt i))); e1] => AllocSampleTape (Z.to_nat i) (go e1)
| GenNode 16 [GenLeaf (inr (inl (LitInt i))); e1; e2] => Sample (Z.to_nat i) (go e1) (go e2)
| GenNode 19 [e] => Tick (go e)
| _ => Val $ LitV LitUnit (* dummy *)
end
with gov v :=
match v with
| GenLeaf (inr (inl l)) => LitV l
| GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => RecV f x (go e)
| GenNode 1 [v1; v2] => PairV (gov v1) (gov v2)
| GenNode 2 [v] => InjLV (gov v)
| GenNode 3 [v] => InjRV (gov v)
| _ => LitV LitUnit (* dummy *)
end
for go).
refine (inj_countable' enc dec _).
refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- destruct e; simpl; f_equal; [exact (gov v) | (by rewrite ?Nat2Z.id) ..].
- destruct v; by f_equal.
Qed.
Global Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Global Program Instance state_countable : Countable state :=
{| encode σ := encode (σ.(heap), σ.(stapes));
decode p := match decode p : option (_ * _) with
| Some (h, st) => Some {|heap:=h; stapes:=st|}
| None => None end |}.
Next Obligation. intros [h st]. rewrite decode_encode //=. Qed.
Global Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; stapes := inhabitant |}.
Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Canonical Structure stateO := leibnizO state.
Canonical Structure locO := leibnizO loc.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
(* ===================== distribution signature =====================
Placed after the Countable/EqDecision val instances, which sig_sample
relies on via dmap. *)
Record SampleFamily := {
sf_param : Type;
sf_param_eqdec :: EqDecision sf_param;
sf_param_count :: Countable sf_param;
sf_out : Type;
sf_out_eqdec :: EqDecision sf_out;
sf_out_count :: Countable sf_out;
sf_inj : sf_out → val;
sf_inj_inj :: Inj (=) (=) sf_inj;
sf_param_of_val : val → option sf_param;
sf_param_to_val : sf_param → val;
sf_roundtrip : ∀ p, sf_param_of_val (sf_param_to_val p) = Some p;
sf_sample : sf_param → distr sf_out;
sf_mass : ∀ p, (SeriesC (sf_sample p) = 1)%R;
(* support predicate (⊇ genuine support); carried by tape ownership *)
sf_supp : sf_param → sf_out → Prop;
sf_supp_spec : ∀ p a, (sf_sample p a > 0)%R → sf_supp p a;
}.
Definition Sig := list SampleFamily.
(* The index serves as the "name" the signature assigns to a SampleFamily. *)
Class SampleIn (D : SampleFamily) (S : Sig) := {
sample_idx : nat;
sample_idx_S : S !! sample_idx = Some D;
}.
Definition sig_sample (S : Sig) (i : nat) (pv : val) : option (distr val) :=
match S !! i with
| Some D =>
(λ μ : distr (sf_out D), dmap (sf_inj D) μ) <$> (sf_sample D <$> sf_param_of_val D pv)
| None => None
end.
Lemma sig_sample_at (D : SampleFamily) (S : Sig) `{!SampleIn D S} (p : sf_param D) :
sig_sample S sample_idx (sf_param_to_val D p)
= Some (dmap (sf_inj D) (sf_sample D p)).
Proof. unfold sig_sample. rewrite sample_idx_S /= sf_roundtrip /=. reflexivity. Qed.
Lemma sig_sample_mass S i pv μ : sig_sample S i pv = Some μ → (SeriesC μ = 1)%R.
Proof.
unfold sig_sample. destruct (S !! i) as [D|]; [|done].
destruct (sf_param_of_val D pv) as [p|]; simpl; [|done].
intros [= <-]. rewrite dmap_mass. apply sf_mass.
Qed.
Proof. by destruct v. Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof. destruct e=>//=. by intros [= <-]. Qed.
Global Instance of_val_inj : Inj (=) (=) of_val.
Proof. intros ??. congruence. Qed.
Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Global Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
Global Instance expr_eq_dec : EqDecision expr.
Proof.
refine (
fix go (e1 e2 : expr) {struct e1} : Decision (e1 = e2) :=
match e1, e2 with
| Val v, Val v' => cast_if (decide (v = v'))
| Var x, Var x' => cast_if (decide (x = x'))
| Rec f x e, Rec f' x' e' =>
cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
| App e1 e2, App e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| UnOp o e, UnOp o' e' => cast_if_and (decide (o = o')) (decide (e = e'))
| BinOp o e1 e2, BinOp o' e1' e2' =>
cast_if_and3 (decide (o = o')) (decide (e1 = e1')) (decide (e2 = e2'))
| If e0 e1 e2, If e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| Pair e1 e2, Pair e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Fst e, Fst e' => cast_if (decide (e = e'))
| Snd e, Snd e' => cast_if (decide (e = e'))
| InjL e, InjL e' => cast_if (decide (e = e'))
| InjR e, InjR e' => cast_if (decide (e = e'))
| Case e0 e1 e2, Case e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| AllocN e1 e2, AllocN e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Deref e, Deref e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Sample i e1 e2, Sample i' e1' e2' =>
cast_if_and3 (decide (i = i')) (decide (e1 = e1')) (decide (e2 = e2'))
| AllocSampleTape i e1, AllocSampleTape i' e1' =>
cast_if_and (decide (i = i')) (decide (e1 = e1'))
| Tick e, Tick e' => cast_if (decide (e = e'))
| _, _ => right _
end
with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
match v1, v2 with
| LitV l, LitV l' => cast_if (decide (l = l'))
| RecV f x e, RecV f' x' e' =>
cast_if_and3 (decide (f = f')) (decide (x = x')) (decide (e = e'))
| PairV e1 e2, PairV e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| InjLV e, InjLV e' => cast_if (decide (e = e'))
| InjRV e, InjRV e' => cast_if (decide (e = e'))
| _, _ => right _
end
for go); try (clear go gov; abstract intuition congruence).
Defined.
Global Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.
Global Instance state_eq_dec : EqDecision state.
Proof. solve_decision. Defined.
Global Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => inl (inl n)
| LitBool b => inl (inr b)
| LitUnit => inr (inl ())
| LitLoc l => inr (inr (inr l))
| LitLbl l => inr (inr (inl l))
end) (λ l, match l with
| inl (inl n) => LitInt n
| inl (inr b) => LitBool b
| inr (inl ()) => LitUnit
| inr (inr (inr l)) => LitLoc l
| inr (inr (inl l)) => LitLbl l
end) _); by intros [].
Qed.
Global Instance un_op_finite : Countable un_op.
Proof.
refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
(λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Global Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable' (λ op, match op with
| PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
| AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
| LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
end) (λ n, match n with
| 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
| 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
| 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
end) _); by intros [].
Qed.
Global Instance expr_countable : Countable expr.
Proof.
set (enc :=
fix go e :=
match e with
| Val v => GenNode 0 [gov v]
| Var x => GenLeaf (inl (inl x))
| Rec f x e => GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
| App e1 e2 => GenNode 2 [go e1; go e2]
| UnOp op e => GenNode 3 [GenLeaf (inr (inr (inl op))); go e]
| BinOp op e1 e2 => GenNode 4 [GenLeaf (inr (inr (inr op))); go e1; go e2]
| If e0 e1 e2 => GenNode 5 [go e0; go e1; go e2]
| Pair e1 e2 => GenNode 6 [go e1; go e2]
| Fst e => GenNode 7 [go e]
| Snd e => GenNode 8 [go e]
| InjL e => GenNode 9 [go e]
| InjR e => GenNode 10 [go e]
| Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
| AllocN e1 e2 => GenNode 12 [go e1; go e2]
| Deref e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| AllocSampleTape i e1 => GenNode 15 [GenLeaf (inr (inl (LitInt (Z.of_nat i)))); go e1]
| Sample i e1 e2 => GenNode 16 [GenLeaf (inr (inl (LitInt (Z.of_nat i)))); go e1; go e2]
| Tick e => GenNode 19 [go e]
end
with gov v :=
match v with
| LitV l => GenLeaf (inr (inl l))
| RecV f x e =>
GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
| PairV v1 v2 => GenNode 1 [gov v1; gov v2]
| InjLV v => GenNode 2 [gov v]
| InjRV v => GenNode 3 [gov v]
end
for go).
set (dec :=
fix go e :=
match e with
| GenNode 0 [v] => Val (gov v)
| GenLeaf (inl (inl x)) => Var x
| GenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
| GenNode 2 [e1; e2] => App (go e1) (go e2)
| GenNode 3 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
| GenNode 4 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
| GenNode 5 [e0; e1; e2] => If (go e0) (go e1) (go e2)
| GenNode 6 [e1; e2] => Pair (go e1) (go e2)
| GenNode 7 [e] => Fst (go e)
| GenNode 8 [e] => Snd (go e)
| GenNode 9 [e] => InjL (go e)
| GenNode 10 [e] => InjR (go e)
| GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
| GenNode 12 [e1 ; e2] => AllocN (go e1) (go e2)
| GenNode 13 [e] => Deref (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [GenLeaf (inr (inl (LitInt i))); e1] => AllocSampleTape (Z.to_nat i) (go e1)
| GenNode 16 [GenLeaf (inr (inl (LitInt i))); e1; e2] => Sample (Z.to_nat i) (go e1) (go e2)
| GenNode 19 [e] => Tick (go e)
| _ => Val $ LitV LitUnit (* dummy *)
end
with gov v :=
match v with
| GenLeaf (inr (inl l)) => LitV l
| GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => RecV f x (go e)
| GenNode 1 [v1; v2] => PairV (gov v1) (gov v2)
| GenNode 2 [v] => InjLV (gov v)
| GenNode 3 [v] => InjRV (gov v)
| _ => LitV LitUnit (* dummy *)
end
for go).
refine (inj_countable' enc dec _).
refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- destruct e; simpl; f_equal; [exact (gov v) | (by rewrite ?Nat2Z.id) ..].
- destruct v; by f_equal.
Qed.
Global Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Global Program Instance state_countable : Countable state :=
{| encode σ := encode (σ.(heap), σ.(stapes));
decode p := match decode p : option (_ * _) with
| Some (h, st) => Some {|heap:=h; stapes:=st|}
| None => None end |}.
Next Obligation. intros [h st]. rewrite decode_encode //=. Qed.
Global Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; stapes := inhabitant |}.
Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Canonical Structure stateO := leibnizO state.
Canonical Structure locO := leibnizO loc.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
(* ===================== distribution signature =====================
Placed after the Countable/EqDecision val instances, which sig_sample
relies on via dmap. *)
Record SampleFamily := {
sf_param : Type;
sf_param_eqdec :: EqDecision sf_param;
sf_param_count :: Countable sf_param;
sf_out : Type;
sf_out_eqdec :: EqDecision sf_out;
sf_out_count :: Countable sf_out;
sf_inj : sf_out → val;
sf_inj_inj :: Inj (=) (=) sf_inj;
sf_param_of_val : val → option sf_param;
sf_param_to_val : sf_param → val;
sf_roundtrip : ∀ p, sf_param_of_val (sf_param_to_val p) = Some p;
sf_sample : sf_param → distr sf_out;
sf_mass : ∀ p, (SeriesC (sf_sample p) = 1)%R;
(* support predicate (⊇ genuine support); carried by tape ownership *)
sf_supp : sf_param → sf_out → Prop;
sf_supp_spec : ∀ p a, (sf_sample p a > 0)%R → sf_supp p a;
}.
Definition Sig := list SampleFamily.
(* The index serves as the "name" the signature assigns to a SampleFamily. *)
Class SampleIn (D : SampleFamily) (S : Sig) := {
sample_idx : nat;
sample_idx_S : S !! sample_idx = Some D;
}.
Definition sig_sample (S : Sig) (i : nat) (pv : val) : option (distr val) :=
match S !! i with
| Some D =>
(λ μ : distr (sf_out D), dmap (sf_inj D) μ) <$> (sf_sample D <$> sf_param_of_val D pv)
| None => None
end.
Lemma sig_sample_at (D : SampleFamily) (S : Sig) `{!SampleIn D S} (p : sf_param D) :
sig_sample S sample_idx (sf_param_to_val D p)
= Some (dmap (sf_inj D) (sf_sample D p)).
Proof. unfold sig_sample. rewrite sample_idx_S /= sf_roundtrip /=. reflexivity. Qed.
Lemma sig_sample_mass S i pv μ : sig_sample S i pv = Some μ → (SeriesC μ = 1)%R.
Proof.
unfold sig_sample. destruct (S !! i) as [D|]; [|done].
destruct (sf_param_of_val D pv) as [p|]; simpl; [|done].
intros [= <-]. rewrite dmap_mass. apply sf_mass.
Qed.
Evaluation contexts
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)
| DerefCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| SampleParamsCtx (i : nat) (v2 : val) (* Sample i · (Val v2) *)
| SampleTapeCtx (i : nat) (e1 : expr) (* Sample i e1 · *)
| AllocSampleTapeCtx (i : nat) (* AllocSampleTape i · *)
| TickCtx.
Definition 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
| DerefCtx => Deref e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| SampleParamsCtx i v2 => Sample i e (Val v2)
| SampleTapeCtx i e1 => Sample i e1 e
| AllocSampleTapeCtx i => AllocSampleTape i e
| TickCtx => Tick e
end.
Definition decomp_item (e : expr) : option (ectx_item * expr) :=
let noval (e : expr) (ei : ectx_item) :=
match e with Val _ => None | _ => Some (ei, e) end in
match e with
| App e1 e2 =>
match e2 with
| (Val v) => noval e1 (AppLCtx v)
| _ => Some (AppRCtx e1, e2)
end
| UnOp op e => noval e (UnOpCtx op)
| BinOp op e1 e2 =>
match e2 with
| Val v => noval e1 (BinOpLCtx op v)
| _ => Some (BinOpRCtx op e1, e2)
end
| If e0 e1 e2 => noval e0 (IfCtx e1 e2)
| Pair e1 e2 =>
match e2 with
| Val v => noval e1 (PairLCtx v)
| _ => Some (PairRCtx e1, e2)
end
| Fst e => noval e FstCtx
| Snd e => noval e SndCtx
| InjL e => noval e InjLCtx
| InjR e => noval e InjRCtx
| Case e0 e1 e2 => noval e0 (CaseCtx e1 e2)
| AllocN e1 e2 =>
match e2 with
| Val v => noval e1 (AllocNLCtx v)
| _ => Some (AllocNRCtx e1, e2)
end
| Deref e => noval e DerefCtx
| Store e1 e2 =>
match e2 with
| Val v => noval e1 (StoreLCtx v)
| _ => Some (StoreRCtx e1, e2)
end
| Sample i e1 e2 =>
match e2 with
| Val v2 => noval e1 (SampleParamsCtx i v2)
| _ => Some (SampleTapeCtx i e1, e2)
end
| AllocSampleTape i e1 => noval e1 (AllocSampleTapeCtx i)
| Tick e => noval e TickCtx
| _ => None
end.
| 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)
| DerefCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| SampleParamsCtx (i : nat) (v2 : val) (* Sample i · (Val v2) *)
| SampleTapeCtx (i : nat) (e1 : expr) (* Sample i e1 · *)
| AllocSampleTapeCtx (i : nat) (* AllocSampleTape i · *)
| TickCtx.
Definition 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
| DerefCtx => Deref e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| SampleParamsCtx i v2 => Sample i e (Val v2)
| SampleTapeCtx i e1 => Sample i e1 e
| AllocSampleTapeCtx i => AllocSampleTape i e
| TickCtx => Tick e
end.
Definition decomp_item (e : expr) : option (ectx_item * expr) :=
let noval (e : expr) (ei : ectx_item) :=
match e with Val _ => None | _ => Some (ei, e) end in
match e with
| App e1 e2 =>
match e2 with
| (Val v) => noval e1 (AppLCtx v)
| _ => Some (AppRCtx e1, e2)
end
| UnOp op e => noval e (UnOpCtx op)
| BinOp op e1 e2 =>
match e2 with
| Val v => noval e1 (BinOpLCtx op v)
| _ => Some (BinOpRCtx op e1, e2)
end
| If e0 e1 e2 => noval e0 (IfCtx e1 e2)
| Pair e1 e2 =>
match e2 with
| Val v => noval e1 (PairLCtx v)
| _ => Some (PairRCtx e1, e2)
end
| Fst e => noval e FstCtx
| Snd e => noval e SndCtx
| InjL e => noval e InjLCtx
| InjR e => noval e InjRCtx
| Case e0 e1 e2 => noval e0 (CaseCtx e1 e2)
| AllocN e1 e2 =>
match e2 with
| Val v => noval e1 (AllocNLCtx v)
| _ => Some (AllocNRCtx e1, e2)
end
| Deref e => noval e DerefCtx
| Store e1 e2 =>
match e2 with
| Val v => noval e1 (StoreLCtx v)
| _ => Some (StoreRCtx e1, e2)
end
| Sample i e1 e2 =>
match e2 with
| Val v2 => noval e1 (SampleParamsCtx i v2)
| _ => Some (SampleTapeCtx i e1, e2)
end
| AllocSampleTape i e1 => noval e1 (AllocSampleTapeCtx i)
| Tick e => noval e TickCtx
| _ => None
end.
Substitution
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)
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Deref e => Deref (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| Sample i e1 e2 => Sample i (subst x v e1) (subst x v e2)
| AllocSampleTape i e1 => AllocSampleTape i (subst x v e1)
| Tick e => Tick (subst x v e)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => λ x, x end.
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)
| AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
| Deref e => Deref (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| Sample i e1 e2 => Sample i (subst x v e1) (subst x v e2)
| AllocSampleTape i e1 => AllocSampleTape i (subst x v e1)
| Tick e => Tick (subst x v e)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => λ x, x end.
The stepping relation
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 z) => Some $ LitV $ LitInt (Z.lnot z)
| MinusUnOp, LitV (LitInt z) => Some $ LitV $ LitInt (- z)
| _, _ => None
end.
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
match op with
| PlusOp => LitInt (n1 + n2)
| MinusOp => LitInt (n1 - n2)
| MultOp => LitInt (n1 * n2)
| QuotOp => LitInt (n1 `quot` n2)
| RemOp => LitInt (n1 `rem` n2)
| AndOp => LitInt (Z.land n1 n2)
| OrOp => LitInt (Z.lor n1 n2)
| XorOp => LitInt (Z.lxor n1 n2)
| ShiftLOp => LitInt (n1 ≪ n2)
| ShiftROp => LitInt (n1 ≫ n2)
| LeOp => LitBool (bool_decide (n1 ≤ n2))
| LtOp => LitBool (bool_decide (n1 < n2))
| EqOp => LitBool (bool_decide (n1 = n2))
| OffsetOp => LitInt (n1 + n2) (* Treat offsets as ints *)
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 (* Arithmetic *)
| AndOp => Some (LitBool (b1 && b2))
| OrOp => Some (LitBool (b1 || b2))
| XorOp => Some (LitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => None (* Shifts *)
| LeOp | LtOp => None (* InEquality *)
| 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)
| LeOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 ≤ₗ l2))
| LtOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 <ₗ l2))
| _, _ => 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) => Some $ 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 val → gmap loc val) (σ : state) : state :=
{| heap := f σ.(heap); stapes := σ.(stapes) |}.
Global Arguments state_upd_heap _ !_ /.
Definition state_upd_stapes (f : gmap loc stape → gmap loc stape) (σ : state) : state :=
{| heap := σ.(heap); stapes := f σ.(stapes) |}.
Global Arguments state_upd_stapes _ !_ /.
Lemma state_upd_stapes_twice σ l t1 t2 :
state_upd_stapes <[l:=t2]> (state_upd_stapes <[l:=t1]> σ) = state_upd_stapes <[l:=t2]> σ.
Proof. rewrite /state_upd_stapes /=. f_equal. apply insert_insert_eq. Qed.
Lemma state_upd_stapes_same σ σ' l t1 t2 :
state_upd_stapes <[l:=t2]> σ = state_upd_stapes <[l:=t1]> σ' -> t1 = t2.
Proof.
rewrite /state_upd_stapes /=. intros K. simplify_eq.
rewrite map_eq_iff in H. specialize (H l).
rewrite !lookup_insert_eq in H. by simplify_eq.
Qed.
Lemma state_upd_stapes_no_change σ l t :
stapes σ !! l = Some t -> state_upd_stapes <[l:=t]> σ = σ.
Proof. destruct σ as [??]. simpl. intros Ht. f_equal. by apply insert_id. Qed.
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val :=
match vs with
| [] => ∅
| v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs'
end.
Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
Proof. by rewrite /heap_array right_id. Qed.
Lemma heap_array_app l vs1 vs2 : heap_array l (vs1 ++ vs2) = (heap_array l vs1) ∪ (heap_array (l +ₗ (length vs1)) vs2) .
Proof.
revert l.
induction vs1; intro l.
- simpl.
rewrite map_empty_union loc_add_0 //.
- rewrite -app_comm_cons /= IHvs1.
rewrite map_union_assoc.
do 2 f_equiv.
rewrite Nat2Z.inj_succ /=.
rewrite /Z.succ
Z.add_comm
loc_add_assoc //.
Qed.
Lemma heap_array_lookup l vs v k :
heap_array l vs !! k = Some v ↔
∃ j, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some v.
Proof.
revert k l; induction vs as [|v' vs IH]=> l' l /=.
{ rewrite lookup_empty. naive_solver lia. }
rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
- intros [[-> ?] | (Hl & j & ? & -> & ?)].
{ eexists 0. rewrite loc_add_0. naive_solver lia. }
eexists (1 + j)%Z. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
- intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
{ rewrite loc_add_0; eauto. }
right. split.
{ rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
{ rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
rewrite Hj /= in Hil.
eexists (j - 1)%Z. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
auto with lia.
Qed.
Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) :
(∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
(heap_array l vs) ##ₘ h.
Proof.
intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
Qed.
Definition state_upd_heap_N (l : loc) (n : nat) (v : val) (σ : state) : state :=
state_upd_heap (λ h, heap_array l (replicate n v) ∪ h) σ.
Lemma state_upd_heap_singleton l v σ :
state_upd_heap_N l 1 v σ = state_upd_heap <[l:= v]> σ.
Proof.
destruct σ as [h p]. rewrite /state_upd_heap_N /=. f_equiv.
rewrite right_id insert_union_singleton_l. done.
Qed.
Lemma state_upd_stapes_heap σ l1 l2 t m v :
state_upd_stapes <[l2:=t]> (state_upd_heap_N l1 m v σ) =
state_upd_heap_N l1 m v (state_upd_stapes <[l2:=t]> σ).
Proof.
by rewrite /state_upd_stapes /state_upd_heap_N /=.
Qed.
Lemma heap_array_replicate_S_end l v n :
heap_array l (replicate (S n) v) = heap_array l (replicate n v) ∪ {[l +ₗ n:= v]}.
Proof.
induction n.
- simpl.
rewrite map_union_empty.
rewrite map_empty_union.
by rewrite loc_add_0.
- rewrite replicate_S_end
heap_array_app
IHn /=.
rewrite map_union_empty length_replicate //.
Qed.
#[local] Open Scope R.
(* The operational semantics is parametric in a distribution signature S. *)
Section semantics.
Context (S : Sig).
Definition head_step (e1 : expr) (σ1 : state) : distr (expr * state) :=
match e1 with
| Rec f x e =>
dret (Val $ RecV f x e, σ1)
| Pair (Val v1) (Val v2) =>
dret (Val $ PairV v1 v2, σ1)
| InjL (Val v) =>
dret (Val $ InjLV v, σ1)
| InjR (Val v) =>
dret (Val $ InjRV v, σ1)
| App (Val (RecV f x e1)) (Val v2) =>
dret (subst' x v2 (subst' f (RecV f x e1) e1) , σ1)
| UnOp op (Val v) =>
match un_op_eval op v with
| Some w => dret (Val w, σ1)
| _ => dzero
end
| BinOp op (Val v1) (Val v2) =>
match bin_op_eval op v1 v2 with
| Some w => dret (Val w, σ1)
| _ => dzero
end
| If (Val (LitV (LitBool true))) e1 e2 =>
dret (e1 , σ1)
| If (Val (LitV (LitBool false))) e1 e2 =>
dret (e2 , σ1)
| Fst (Val (PairV v1 v2)) =>
dret (Val v1, σ1)
| Snd (Val (PairV v1 v2)) =>
dret (Val v2, σ1)
| Case (Val (InjLV v)) e1 e2 =>
dret (App e1 (Val v), σ1)
| Case (Val (InjRV v)) e1 e2 =>
dret (App e2 (Val v), σ1)
| AllocN (Val (LitV (LitInt N))) (Val v) =>
let ℓ := fresh_loc σ1.(heap) in
if bool_decide (0 < Z.to_nat N)%nat
then dret (Val $ LitV $ LitLoc ℓ, state_upd_heap_N ℓ (Z.to_nat N) v σ1)
else dzero
| Deref (Val (LitV (LitLoc l))) =>
match σ1.(heap) !! l with
| Some v => dret (Val v, σ1)
| None => dzero
end
| Store (Val (LitV (LitLoc l))) (Val w) =>
match σ1.(heap) !! l with
| Some v => dret (Val $ LitV LitUnit, state_upd_heap <[l:=w]> σ1)
| None => dzero
end
(* Generic sampling. Direct (tape argument = unit): sample from family i with
parameter value pv. None (unsupported family/parameter) is stuck. *)
| Sample i (Val pv) (Val (LitV LitUnit)) =>
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ
| None => dzero
end
| AllocSampleTape i (Val pv) =>
let ι := fresh_loc σ1.(stapes) in
dret (Val $ LitV $ LitLbl ι, state_upd_stapes <[ι := (i, pv, []) ]> σ1)
(* Labelled sampling, conditional on tape contents. *)
| Sample i (Val pv) (Val (LitV (LitLbl l))) =>
match σ1.(stapes) !! l with
| Some (i', pv', xs) =>
if bool_decide (i = i' ∧ pv = pv') then
match xs with
| x :: xs =>
(* consume the head presampled value *)
dret (Val x, state_upd_stapes <[l := (i', pv', xs)]> σ1)
| [] =>
(* tape allocated but empty: sample fresh *)
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ | None => dzero end
end
else
(* descriptor mismatch: follow the sampling arguments *)
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ | None => dzero end
| None => dzero
end
| Tick (Val (LitV (LitInt n))) => dret (Val $ LitV $ LitUnit, σ1)
| _ => dzero
end.
(* Presampling: extend tape α by one fresh draw from its family. A tape whose
descriptor is unsupported (sig_sample = None) presamples as a no-op
(dret), keeping state_step mass-1. *)
Definition state_step (σ1 : state) (α : loc) : distr state :=
if bool_decide (α ∈ dom σ1.(stapes)) then
let '(i, pv, xs) := (σ1.(stapes) !!! α) in
match sig_sample S i pv with
| Some μ => dmap (λ v, state_upd_stapes (<[α := (i, pv, xs ++ [v])]>) σ1) μ
| None => dret σ1
end
else dzero.
Lemma state_step_unfold σ α i pv xs :
stapes σ !! α = Some (i, pv, xs) ->
state_step σ α =
match sig_sample S i pv with
| Some μ => dmap (λ v, state_upd_stapes (<[α := (i, pv, xs ++ [v])]>) σ) μ
| None => dret σ
end.
Proof.
intros H.
rewrite /state_step.
rewrite bool_decide_eq_true_2; last by apply elem_of_dom.
by rewrite (lookup_total_correct (stapes σ) α (i, pv, xs)).
Qed.
match op, v with
| NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
| NegOp, LitV (LitInt z) => Some $ LitV $ LitInt (Z.lnot z)
| MinusUnOp, LitV (LitInt z) => Some $ LitV $ LitInt (- z)
| _, _ => None
end.
Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
match op with
| PlusOp => LitInt (n1 + n2)
| MinusOp => LitInt (n1 - n2)
| MultOp => LitInt (n1 * n2)
| QuotOp => LitInt (n1 `quot` n2)
| RemOp => LitInt (n1 `rem` n2)
| AndOp => LitInt (Z.land n1 n2)
| OrOp => LitInt (Z.lor n1 n2)
| XorOp => LitInt (Z.lxor n1 n2)
| ShiftLOp => LitInt (n1 ≪ n2)
| ShiftROp => LitInt (n1 ≫ n2)
| LeOp => LitBool (bool_decide (n1 ≤ n2))
| LtOp => LitBool (bool_decide (n1 < n2))
| EqOp => LitBool (bool_decide (n1 = n2))
| OffsetOp => LitInt (n1 + n2) (* Treat offsets as ints *)
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 (* Arithmetic *)
| AndOp => Some (LitBool (b1 && b2))
| OrOp => Some (LitBool (b1 || b2))
| XorOp => Some (LitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => None (* Shifts *)
| LeOp | LtOp => None (* InEquality *)
| 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)
| LeOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 ≤ₗ l2))
| LtOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 <ₗ l2))
| _, _ => 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) => Some $ 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 val → gmap loc val) (σ : state) : state :=
{| heap := f σ.(heap); stapes := σ.(stapes) |}.
Global Arguments state_upd_heap _ !_ /.
Definition state_upd_stapes (f : gmap loc stape → gmap loc stape) (σ : state) : state :=
{| heap := σ.(heap); stapes := f σ.(stapes) |}.
Global Arguments state_upd_stapes _ !_ /.
Lemma state_upd_stapes_twice σ l t1 t2 :
state_upd_stapes <[l:=t2]> (state_upd_stapes <[l:=t1]> σ) = state_upd_stapes <[l:=t2]> σ.
Proof. rewrite /state_upd_stapes /=. f_equal. apply insert_insert_eq. Qed.
Lemma state_upd_stapes_same σ σ' l t1 t2 :
state_upd_stapes <[l:=t2]> σ = state_upd_stapes <[l:=t1]> σ' -> t1 = t2.
Proof.
rewrite /state_upd_stapes /=. intros K. simplify_eq.
rewrite map_eq_iff in H. specialize (H l).
rewrite !lookup_insert_eq in H. by simplify_eq.
Qed.
Lemma state_upd_stapes_no_change σ l t :
stapes σ !! l = Some t -> state_upd_stapes <[l:=t]> σ = σ.
Proof. destruct σ as [??]. simpl. intros Ht. f_equal. by apply insert_id. Qed.
Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val :=
match vs with
| [] => ∅
| v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs'
end.
Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
Proof. by rewrite /heap_array right_id. Qed.
Lemma heap_array_app l vs1 vs2 : heap_array l (vs1 ++ vs2) = (heap_array l vs1) ∪ (heap_array (l +ₗ (length vs1)) vs2) .
Proof.
revert l.
induction vs1; intro l.
- simpl.
rewrite map_empty_union loc_add_0 //.
- rewrite -app_comm_cons /= IHvs1.
rewrite map_union_assoc.
do 2 f_equiv.
rewrite Nat2Z.inj_succ /=.
rewrite /Z.succ
Z.add_comm
loc_add_assoc //.
Qed.
Lemma heap_array_lookup l vs v k :
heap_array l vs !! k = Some v ↔
∃ j, (0 ≤ j)%Z ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some v.
Proof.
revert k l; induction vs as [|v' vs IH]=> l' l /=.
{ rewrite lookup_empty. naive_solver lia. }
rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
- intros [[-> ?] | (Hl & j & ? & -> & ?)].
{ eexists 0. rewrite loc_add_0. naive_solver lia. }
eexists (1 + j)%Z. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
- intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
{ rewrite loc_add_0; eauto. }
right. split.
{ rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
{ rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
rewrite Hj /= in Hil.
eexists (j - 1)%Z. rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
auto with lia.
Qed.
Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) :
(∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
(heap_array l vs) ##ₘ h.
Proof.
intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
Qed.
Definition state_upd_heap_N (l : loc) (n : nat) (v : val) (σ : state) : state :=
state_upd_heap (λ h, heap_array l (replicate n v) ∪ h) σ.
Lemma state_upd_heap_singleton l v σ :
state_upd_heap_N l 1 v σ = state_upd_heap <[l:= v]> σ.
Proof.
destruct σ as [h p]. rewrite /state_upd_heap_N /=. f_equiv.
rewrite right_id insert_union_singleton_l. done.
Qed.
Lemma state_upd_stapes_heap σ l1 l2 t m v :
state_upd_stapes <[l2:=t]> (state_upd_heap_N l1 m v σ) =
state_upd_heap_N l1 m v (state_upd_stapes <[l2:=t]> σ).
Proof.
by rewrite /state_upd_stapes /state_upd_heap_N /=.
Qed.
Lemma heap_array_replicate_S_end l v n :
heap_array l (replicate (S n) v) = heap_array l (replicate n v) ∪ {[l +ₗ n:= v]}.
Proof.
induction n.
- simpl.
rewrite map_union_empty.
rewrite map_empty_union.
by rewrite loc_add_0.
- rewrite replicate_S_end
heap_array_app
IHn /=.
rewrite map_union_empty length_replicate //.
Qed.
#[local] Open Scope R.
(* The operational semantics is parametric in a distribution signature S. *)
Section semantics.
Context (S : Sig).
Definition head_step (e1 : expr) (σ1 : state) : distr (expr * state) :=
match e1 with
| Rec f x e =>
dret (Val $ RecV f x e, σ1)
| Pair (Val v1) (Val v2) =>
dret (Val $ PairV v1 v2, σ1)
| InjL (Val v) =>
dret (Val $ InjLV v, σ1)
| InjR (Val v) =>
dret (Val $ InjRV v, σ1)
| App (Val (RecV f x e1)) (Val v2) =>
dret (subst' x v2 (subst' f (RecV f x e1) e1) , σ1)
| UnOp op (Val v) =>
match un_op_eval op v with
| Some w => dret (Val w, σ1)
| _ => dzero
end
| BinOp op (Val v1) (Val v2) =>
match bin_op_eval op v1 v2 with
| Some w => dret (Val w, σ1)
| _ => dzero
end
| If (Val (LitV (LitBool true))) e1 e2 =>
dret (e1 , σ1)
| If (Val (LitV (LitBool false))) e1 e2 =>
dret (e2 , σ1)
| Fst (Val (PairV v1 v2)) =>
dret (Val v1, σ1)
| Snd (Val (PairV v1 v2)) =>
dret (Val v2, σ1)
| Case (Val (InjLV v)) e1 e2 =>
dret (App e1 (Val v), σ1)
| Case (Val (InjRV v)) e1 e2 =>
dret (App e2 (Val v), σ1)
| AllocN (Val (LitV (LitInt N))) (Val v) =>
let ℓ := fresh_loc σ1.(heap) in
if bool_decide (0 < Z.to_nat N)%nat
then dret (Val $ LitV $ LitLoc ℓ, state_upd_heap_N ℓ (Z.to_nat N) v σ1)
else dzero
| Deref (Val (LitV (LitLoc l))) =>
match σ1.(heap) !! l with
| Some v => dret (Val v, σ1)
| None => dzero
end
| Store (Val (LitV (LitLoc l))) (Val w) =>
match σ1.(heap) !! l with
| Some v => dret (Val $ LitV LitUnit, state_upd_heap <[l:=w]> σ1)
| None => dzero
end
(* Generic sampling. Direct (tape argument = unit): sample from family i with
parameter value pv. None (unsupported family/parameter) is stuck. *)
| Sample i (Val pv) (Val (LitV LitUnit)) =>
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ
| None => dzero
end
| AllocSampleTape i (Val pv) =>
let ι := fresh_loc σ1.(stapes) in
dret (Val $ LitV $ LitLbl ι, state_upd_stapes <[ι := (i, pv, []) ]> σ1)
(* Labelled sampling, conditional on tape contents. *)
| Sample i (Val pv) (Val (LitV (LitLbl l))) =>
match σ1.(stapes) !! l with
| Some (i', pv', xs) =>
if bool_decide (i = i' ∧ pv = pv') then
match xs with
| x :: xs =>
(* consume the head presampled value *)
dret (Val x, state_upd_stapes <[l := (i', pv', xs)]> σ1)
| [] =>
(* tape allocated but empty: sample fresh *)
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ | None => dzero end
end
else
(* descriptor mismatch: follow the sampling arguments *)
match sig_sample S i pv with
| Some μ => dmap (λ v, (Val v, σ1)) μ | None => dzero end
| None => dzero
end
| Tick (Val (LitV (LitInt n))) => dret (Val $ LitV $ LitUnit, σ1)
| _ => dzero
end.
(* Presampling: extend tape α by one fresh draw from its family. A tape whose
descriptor is unsupported (sig_sample = None) presamples as a no-op
(dret), keeping state_step mass-1. *)
Definition state_step (σ1 : state) (α : loc) : distr state :=
if bool_decide (α ∈ dom σ1.(stapes)) then
let '(i, pv, xs) := (σ1.(stapes) !!! α) in
match sig_sample S i pv with
| Some μ => dmap (λ v, state_upd_stapes (<[α := (i, pv, xs ++ [v])]>) σ1) μ
| None => dret σ1
end
else dzero.
Lemma state_step_unfold σ α i pv xs :
stapes σ !! α = Some (i, pv, xs) ->
state_step σ α =
match sig_sample S i pv with
| Some μ => dmap (λ v, state_upd_stapes (<[α := (i, pv, xs ++ [v])]>) σ) μ
| None => dret σ
end.
Proof.
intros H.
rewrite /state_step.
rewrite bool_decide_eq_true_2; last by apply elem_of_dom.
by rewrite (lookup_total_correct (stapes σ) α (i, pv, xs)).
Qed.
Basic properties about the language
Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
Lemma val_head_stuck e σ ρ :
head_step e σ ρ > 0 → to_val e = None.
Proof. destruct ρ, e; [|done..]. rewrite /pmf /=. lra. Qed.
Lemma head_ctx_step_val Ki e σ ρ :
head_step (fill_item Ki e) σ ρ > 0 → is_Some (to_val e).
Proof.
destruct ρ, Ki ;
rewrite /pmf/= ;
repeat case_match; clear -H ; inversion H; intros ; (lra || done).
Qed.
Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
Lemma val_head_stuck e σ ρ :
head_step e σ ρ > 0 → to_val e = None.
Proof. destruct ρ, e; [|done..]. rewrite /pmf /=. lra. Qed.
Lemma head_ctx_step_val Ki e σ ρ :
head_step (fill_item Ki e) σ ρ > 0 → is_Some (to_val e).
Proof.
destruct ρ, Ki ;
rewrite /pmf/= ;
repeat case_match; clear -H ; inversion H; intros ; (lra || done).
Qed.
A relational characterization of the support of head_step to make it easier to
do inversion and prove reducibility easier c.f. lemma below
Inductive head_step_rel : expr → state → expr → state → Prop :=
| RecS f x e σ :
head_step_rel (Rec f x e) σ (Val $ RecV f x e) σ
| PairS v1 v2 σ :
head_step_rel (Pair (Val v1) (Val v2)) σ (Val $ PairV v1 v2) σ
| InjLS v σ :
head_step_rel (InjL $ Val v) σ (Val $ InjLV v) σ
| InjRS v σ :
head_step_rel (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_rel (App (Val $ RecV f x e1) (Val v2)) σ e' σ
| UnOpS op v v' σ :
un_op_eval op v = Some v' →
head_step_rel (UnOp op (Val v)) σ (Val v') σ
| BinOpS op v1 v2 v' σ :
bin_op_eval op v1 v2 = Some v' →
head_step_rel (BinOp op (Val v1) (Val v2)) σ (Val v') σ
| IfTrueS e1 e2 σ :
head_step_rel (If (Val $ LitV $ LitBool true) e1 e2) σ e1 σ
| IfFalseS e1 e2 σ :
head_step_rel (If (Val $ LitV $ LitBool false) e1 e2) σ e2 σ
| FstS v1 v2 σ :
head_step_rel (Fst (Val $ PairV v1 v2)) σ (Val v1) σ
| SndS v1 v2 σ :
head_step_rel (Snd (Val $ PairV v1 v2)) σ (Val v2) σ
| CaseLS v e1 e2 σ :
head_step_rel (Case (Val $ InjLV v) e1 e2) σ (App e1 (Val v)) σ
| CaseRS v e1 e2 σ :
head_step_rel (Case (Val $ InjRV v) e1 e2) σ (App e2 (Val v)) σ
| AllocNS z N v σ l :
l = fresh_loc σ.(heap) →
N = Z.to_nat z →
(0 < N)%nat ->
head_step_rel (AllocN (Val (LitV (LitInt z))) (Val v)) σ
(Val $ LitV $ LitLoc l) (state_upd_heap_N l N v σ)
| DerefS l v σ :
σ.(heap) !! l = Some v →
head_step_rel (Deref (Val $ LitV $ LitLoc l)) σ (of_val v) σ
| StoreS l v w σ :
σ.(heap) !! l = Some v →
head_step_rel (Store (Val $ LitV $ LitLoc l) (Val w)) σ
(Val $ LitV LitUnit) (state_upd_heap <[l:=w]> σ)
| SampleNoTapeS i pv μ v σ :
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV LitUnit)) σ (Val v) σ
| AllocSampleTapeS i pv σ l :
l = fresh_loc σ.(stapes) →
head_step_rel (AllocSampleTape i (Val pv)) σ
(Val $ LitV $ LitLbl l) (state_upd_stapes <[l := (i, pv, [])]> σ)
| SampleTapeConsS i pv l x xs σ :
σ.(stapes) !! l = Some (i, pv, x :: xs) →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ
(Val x) (state_upd_stapes <[l := (i, pv, xs)]> σ)
| SampleTapeEmptyS i pv l μ v σ :
σ.(stapes) !! l = Some (i, pv, []) →
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ (Val v) σ
| SampleTapeOtherS i pv l i' pv' xs μ v σ :
σ.(stapes) !! l = Some (i', pv', xs) →
¬ (i = i' ∧ pv = pv') →
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ (Val v) σ
| TickS σ z :
head_step_rel (Tick $ Val $ LitV $ LitInt z) σ (Val $ LitV $ LitUnit) σ.
Create HintDb head_step.
#[local] Hint Constructors head_step_rel : head_step.
(* (uniform/laplace-specific reduct-proposal hints removed; the generic
support-equivalence proof supplies sample witnesses explicitly) *)
Inductive state_step_rel : state → loc → state → Prop :=
| AddSampleTapeS α i pv xs μ v σ :
α ∈ dom σ.(stapes) →
σ.(stapes) !!! α = (i, pv, xs) →
sig_sample S i pv = Some μ →
μ v > 0 →
state_step_rel σ α (state_upd_stapes <[α := (i, pv, xs ++ [v]) ]> σ)
| AddSampleTapeNoneS α i pv xs σ :
α ∈ dom σ.(stapes) →
σ.(stapes) !!! α = (i, pv, xs) →
sig_sample S i pv = None →
state_step_rel σ α σ.
Ltac inv_head_step :=
repeat
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
try (rewrite bool_decide_eq_true_2 in H; [|done]);
try (rewrite bool_decide_eq_false_2 in H; [|done]);
destruct_decide (@bool_decide_reflect P dec); simplify_eq
| _ => progress simplify_map_eq; simpl in *; inv_distr; repeat case_match; inv_distr
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : is_Some (_ !! _) |- _ => destruct H
end.
Lemma head_step_support_equiv_rel e1 e2 σ1 σ2 :
head_step e1 σ1 (e2, σ2) > 0 ↔ head_step_rel e1 σ1 e2 σ2.
Proof.
split.
- intros Hpos. destruct e1; inv_head_step; try by eauto with head_step.
all: destruct H; subst; eauto with head_step.
- inversion 1; simplify_map_eq/=; try case_bool_decide; simplify_eq;
try (rewrite H); try (rewrite H0); solve_distr; try done.
by destruct (H1 (conj eq_refl eq_refl)).
Qed.
Lemma state_step_support_equiv_rel σ1 α σ2 :
state_step σ1 α σ2 > 0 ↔ state_step_rel σ1 α σ2.
Proof.
rewrite /state_step. split.
- case_bool_decide as Hdom; [|intros; inv_distr].
destruct (stapes σ1 !!! α) as [[i pv] xs] eqn:Hα.
case_match eqn:Hss; intros Hpos; inv_distr.
all: econstructor; eauto.
- inversion_clear 1.
all: rewrite bool_decide_eq_true_2; [|done]; rewrite H1; simpl; rewrite H2; solve_distr.
Qed.
Ltac solve_distr :=
repeat
match goal with
| |- (dret _).(pmf) _ > 0 => rewrite dret_1_1 //; lra
| |- (dret ?x).(pmf) ?x = 1 => by apply dret_1_1
| |- (dbind _ _).(pmf) _ > 0 => apply dbind_pos; eexists; split
| |- (dmap _ _).(pmf) _ > 0 =>
apply dmap_pos; eexists; (split; [done|]); try done
| |- (dunifP _).(pmf) _ > 0 => apply dunifP_pos
| |- (dunifv _ _).(pmf) _ > 0 => apply dunifv_pos
| |- (d_proj_Some _).(pmf) _ > 0 => rewrite d_proj_Some_pos
end.
Lemma state_step_head_step_not_stuck e σ σ' α :
state_step σ α σ' > 0 → (∃ ρ, head_step e σ ρ > 0) ↔ (∃ ρ', head_step e σ' ρ' > 0).
Proof.
rewrite state_step_support_equiv_rel.
inversion_clear 1 as [α' i pv xs μ v Hdom Hα Hss Hμ|]; [|tauto].
apply elem_of_dom in Hα as [t Ht].
rewrite (lookup_total_correct _ _ _ Ht) in Hss. subst t.
split; intros [[e2 σ2] Hs]; destruct e; inv_head_step; try (eexists; solve_distr; done).
all: destruct (decide (l0 = α)) as [->|Hne]; simplify_map_eq;
try (by destruct xs; simplify_eq);
try (eexists; solve_distr; done);
try (match goal with
| Hd : sig_sample _ _ _ = Some ?d |- context [dmap _ ?d] =>
destruct (SeriesC_gtz_ex d (pmf_pos d)) as [? Ha];
[ rewrite (sig_sample_mass _ _ _ _ Hd); lra
| eexists; apply dmap_pos; eexists; split; [reflexivity|exact Ha] ]
end).
all: try (destruct H as [-> ->]);
match goal with
| A : ?x = Some _, B : ?x = None |- _ => by rewrite A in B
end.
Unshelve.
all: destruct (H H1).
Qed.
Lemma state_step_mass σ α :
α ∈ dom σ.(stapes) → SeriesC (state_step σ α) = 1.
Proof.
intros Hdom.
rewrite /state_step bool_decide_eq_true_2 //.
destruct (stapes σ !!! α) as [[i pv] xs].
case_match eqn:Hss.
- rewrite dmap_mass. by eapply sig_sample_mass.
- apply dret_mass.
Qed.
Lemma head_step_mass e σ :
(∃ ρ, head_step e σ ρ > 0) → SeriesC (head_step e σ) = 1.
Proof.
intros [[] Hs%head_step_support_equiv_rel].
inversion Hs; simplify_eq/=; try (solve_distr_mass).
all: repeat (match goal with
| H : un_op_eval _ _ = _ |- _ => rewrite H
| H : bin_op_eval _ _ _ = _ |- _ => rewrite H
| H : heap _ !! _ = _ |- _ => rewrite H
| H : stapes _ !! _ = _ |- _ => rewrite H
| H : sig_sample _ _ _ = _ |- _ => rewrite H
| |- context [bool_decide (?i = ?i ∧ ?p = ?p)] => rewrite bool_decide_eq_true_2; [|done]
| Hn : ¬ (_ ∧ _) |- context [bool_decide (_ ∧ _)] => rewrite (bool_decide_eq_false_2 _ Hn)
| |- context [bool_decide (0 < _)%nat] => rewrite bool_decide_eq_true_2; [|done]
end); simpl.
all: first [ apply dret_mass | (rewrite dmap_mass; by eapply sig_sample_mass) ].
Qed.
Lemma 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.
Proof. destruct Ki2, Ki1; naive_solver eauto with f_equal. Qed.
Fixpoint height (e : expr) : nat :=
match e with
| Val _ => 1
| Var _ => 1
| Rec _ _ e => 1 + height e
| App e1 e2 => 1 + height e1 + height e2
| UnOp _ e => 1 + height e
| BinOp _ e1 e2 => 1 + height e1 + height e2
| If e0 e1 e2 => 1 + height e0 + height e1 + height e2
| Pair e1 e2 => 1 + height e1 + height e2
| Fst e => 1 + height e
| Snd e => 1 + height e
| InjL e => 1 + height e
| InjR e => 1 + height e
| Case e0 e1 e2 => 1 + height e0 + height e1 + height e2
| AllocN e1 e2 => 1 + height e1 + height e2
| Deref e => 1 + height e
| Store e1 e2 => 1 + height e1 + height e2
| Sample _ e1 e2 => 1 + height e1 + height e2
| AllocSampleTape _ e1 => 1 + height e1
| Tick e => 1 + height e
end.
Definition expr_ord (e1 e2 : expr) : Prop := (height e1 < height e2)%nat.
Lemma expr_ord_wf' h e : (height e ≤ h)%nat → Acc expr_ord e.
Proof.
rewrite /expr_ord. revert e; induction h.
{ destruct e; simpl; lia. }
intros []; simpl;
constructor; simpl; intros []; eauto with lia.
Defined.
Lemma expr_ord_wf : well_founded expr_ord.
Proof. red; intro; eapply expr_ord_wf'; eauto. Defined.
(* TODO: this proof is slow, but I do not see how to make it faster... *)
Lemma decomp_expr_ord Ki e e' : decomp_item e = Some (Ki, e') → expr_ord e' e.
Proof.
rewrite /expr_ord /decomp_item.
destruct Ki ; repeat destruct_match ; intros [=] ; subst ; cbn ; lia.
Qed.
Lemma decomp_fill_item Ki e :
to_val e = None → decomp_item (fill_item Ki e) = Some (Ki, e).
Proof. destruct Ki ; simpl ; by repeat destruct_match. Qed.
(* TODO: this proof is slow, but I do not see how to make it faster... *)
Lemma decomp_fill_item_2 e e' Ki :
decomp_item e = Some (Ki, e') → fill_item Ki e' = e ∧ to_val e' = None.
Proof.
rewrite /decomp_item ;
destruct e ; try done ;
destruct Ki ; cbn ; repeat destruct_match ; intros [=] ; subst ; auto.
Qed.
Definition get_active (σ : state) : list loc := elements (dom σ.(stapes)).
Lemma state_step_get_active_mass σ α :
α ∈ get_active σ → SeriesC (state_step σ α) = 1.
Proof. rewrite elem_of_elements. apply state_step_mass. Qed.
Lemma state_steps_mass σ αs :
αs ⊆ get_active σ →
SeriesC (foldlM state_step σ αs) = 1.
Proof.
induction αs as [|α αs IH] in σ |-* ; intros Hact.
{ rewrite /= dret_mass //. }
rewrite foldlM_cons.
rewrite dbind_det //.
- apply state_step_get_active_mass. set_solver.
- intros σ' Hσ'. apply IH.
apply state_step_support_equiv_rel in Hσ'.
inversion Hσ'; simplify_eq; last (intros α' ?; eapply Hact; set_solver).
intros α' ?. rewrite /get_active /=.
apply elem_of_elements, elem_of_dom.
destruct (decide (α = α')); subst.
+ eexists. rewrite lookup_insert_eq //.
+ rewrite lookup_insert_ne //.
apply elem_of_dom. eapply elem_of_elements, Hact. by right.
Qed.
Lemma gen_lang_mixin :
EctxiLanguageMixin of_val to_val fill_item decomp_item expr_ord head_step state_step get_active.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
state_step_head_step_not_stuck, state_step_get_active_mass, head_step_mass,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val,
decomp_fill_item, decomp_fill_item_2, expr_ord_wf, decomp_expr_ord.
Qed.
End semantics.
End gen_prob_lang.
(* Prefer gen_prob_lang names over ectx_language names. *)
Export gen_prob_lang.
| RecS f x e σ :
head_step_rel (Rec f x e) σ (Val $ RecV f x e) σ
| PairS v1 v2 σ :
head_step_rel (Pair (Val v1) (Val v2)) σ (Val $ PairV v1 v2) σ
| InjLS v σ :
head_step_rel (InjL $ Val v) σ (Val $ InjLV v) σ
| InjRS v σ :
head_step_rel (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_rel (App (Val $ RecV f x e1) (Val v2)) σ e' σ
| UnOpS op v v' σ :
un_op_eval op v = Some v' →
head_step_rel (UnOp op (Val v)) σ (Val v') σ
| BinOpS op v1 v2 v' σ :
bin_op_eval op v1 v2 = Some v' →
head_step_rel (BinOp op (Val v1) (Val v2)) σ (Val v') σ
| IfTrueS e1 e2 σ :
head_step_rel (If (Val $ LitV $ LitBool true) e1 e2) σ e1 σ
| IfFalseS e1 e2 σ :
head_step_rel (If (Val $ LitV $ LitBool false) e1 e2) σ e2 σ
| FstS v1 v2 σ :
head_step_rel (Fst (Val $ PairV v1 v2)) σ (Val v1) σ
| SndS v1 v2 σ :
head_step_rel (Snd (Val $ PairV v1 v2)) σ (Val v2) σ
| CaseLS v e1 e2 σ :
head_step_rel (Case (Val $ InjLV v) e1 e2) σ (App e1 (Val v)) σ
| CaseRS v e1 e2 σ :
head_step_rel (Case (Val $ InjRV v) e1 e2) σ (App e2 (Val v)) σ
| AllocNS z N v σ l :
l = fresh_loc σ.(heap) →
N = Z.to_nat z →
(0 < N)%nat ->
head_step_rel (AllocN (Val (LitV (LitInt z))) (Val v)) σ
(Val $ LitV $ LitLoc l) (state_upd_heap_N l N v σ)
| DerefS l v σ :
σ.(heap) !! l = Some v →
head_step_rel (Deref (Val $ LitV $ LitLoc l)) σ (of_val v) σ
| StoreS l v w σ :
σ.(heap) !! l = Some v →
head_step_rel (Store (Val $ LitV $ LitLoc l) (Val w)) σ
(Val $ LitV LitUnit) (state_upd_heap <[l:=w]> σ)
| SampleNoTapeS i pv μ v σ :
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV LitUnit)) σ (Val v) σ
| AllocSampleTapeS i pv σ l :
l = fresh_loc σ.(stapes) →
head_step_rel (AllocSampleTape i (Val pv)) σ
(Val $ LitV $ LitLbl l) (state_upd_stapes <[l := (i, pv, [])]> σ)
| SampleTapeConsS i pv l x xs σ :
σ.(stapes) !! l = Some (i, pv, x :: xs) →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ
(Val x) (state_upd_stapes <[l := (i, pv, xs)]> σ)
| SampleTapeEmptyS i pv l μ v σ :
σ.(stapes) !! l = Some (i, pv, []) →
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ (Val v) σ
| SampleTapeOtherS i pv l i' pv' xs μ v σ :
σ.(stapes) !! l = Some (i', pv', xs) →
¬ (i = i' ∧ pv = pv') →
sig_sample S i pv = Some μ →
μ v > 0 →
head_step_rel (Sample i (Val pv) (Val $ LitV $ LitLbl l)) σ (Val v) σ
| TickS σ z :
head_step_rel (Tick $ Val $ LitV $ LitInt z) σ (Val $ LitV $ LitUnit) σ.
Create HintDb head_step.
#[local] Hint Constructors head_step_rel : head_step.
(* (uniform/laplace-specific reduct-proposal hints removed; the generic
support-equivalence proof supplies sample witnesses explicitly) *)
Inductive state_step_rel : state → loc → state → Prop :=
| AddSampleTapeS α i pv xs μ v σ :
α ∈ dom σ.(stapes) →
σ.(stapes) !!! α = (i, pv, xs) →
sig_sample S i pv = Some μ →
μ v > 0 →
state_step_rel σ α (state_upd_stapes <[α := (i, pv, xs ++ [v]) ]> σ)
| AddSampleTapeNoneS α i pv xs σ :
α ∈ dom σ.(stapes) →
σ.(stapes) !!! α = (i, pv, xs) →
sig_sample S i pv = None →
state_step_rel σ α σ.
Ltac inv_head_step :=
repeat
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
try (rewrite bool_decide_eq_true_2 in H; [|done]);
try (rewrite bool_decide_eq_false_2 in H; [|done]);
destruct_decide (@bool_decide_reflect P dec); simplify_eq
| _ => progress simplify_map_eq; simpl in *; inv_distr; repeat case_match; inv_distr
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : is_Some (_ !! _) |- _ => destruct H
end.
Lemma head_step_support_equiv_rel e1 e2 σ1 σ2 :
head_step e1 σ1 (e2, σ2) > 0 ↔ head_step_rel e1 σ1 e2 σ2.
Proof.
split.
- intros Hpos. destruct e1; inv_head_step; try by eauto with head_step.
all: destruct H; subst; eauto with head_step.
- inversion 1; simplify_map_eq/=; try case_bool_decide; simplify_eq;
try (rewrite H); try (rewrite H0); solve_distr; try done.
by destruct (H1 (conj eq_refl eq_refl)).
Qed.
Lemma state_step_support_equiv_rel σ1 α σ2 :
state_step σ1 α σ2 > 0 ↔ state_step_rel σ1 α σ2.
Proof.
rewrite /state_step. split.
- case_bool_decide as Hdom; [|intros; inv_distr].
destruct (stapes σ1 !!! α) as [[i pv] xs] eqn:Hα.
case_match eqn:Hss; intros Hpos; inv_distr.
all: econstructor; eauto.
- inversion_clear 1.
all: rewrite bool_decide_eq_true_2; [|done]; rewrite H1; simpl; rewrite H2; solve_distr.
Qed.
Ltac solve_distr :=
repeat
match goal with
| |- (dret _).(pmf) _ > 0 => rewrite dret_1_1 //; lra
| |- (dret ?x).(pmf) ?x = 1 => by apply dret_1_1
| |- (dbind _ _).(pmf) _ > 0 => apply dbind_pos; eexists; split
| |- (dmap _ _).(pmf) _ > 0 =>
apply dmap_pos; eexists; (split; [done|]); try done
| |- (dunifP _).(pmf) _ > 0 => apply dunifP_pos
| |- (dunifv _ _).(pmf) _ > 0 => apply dunifv_pos
| |- (d_proj_Some _).(pmf) _ > 0 => rewrite d_proj_Some_pos
end.
Lemma state_step_head_step_not_stuck e σ σ' α :
state_step σ α σ' > 0 → (∃ ρ, head_step e σ ρ > 0) ↔ (∃ ρ', head_step e σ' ρ' > 0).
Proof.
rewrite state_step_support_equiv_rel.
inversion_clear 1 as [α' i pv xs μ v Hdom Hα Hss Hμ|]; [|tauto].
apply elem_of_dom in Hα as [t Ht].
rewrite (lookup_total_correct _ _ _ Ht) in Hss. subst t.
split; intros [[e2 σ2] Hs]; destruct e; inv_head_step; try (eexists; solve_distr; done).
all: destruct (decide (l0 = α)) as [->|Hne]; simplify_map_eq;
try (by destruct xs; simplify_eq);
try (eexists; solve_distr; done);
try (match goal with
| Hd : sig_sample _ _ _ = Some ?d |- context [dmap _ ?d] =>
destruct (SeriesC_gtz_ex d (pmf_pos d)) as [? Ha];
[ rewrite (sig_sample_mass _ _ _ _ Hd); lra
| eexists; apply dmap_pos; eexists; split; [reflexivity|exact Ha] ]
end).
all: try (destruct H as [-> ->]);
match goal with
| A : ?x = Some _, B : ?x = None |- _ => by rewrite A in B
end.
Unshelve.
all: destruct (H H1).
Qed.
Lemma state_step_mass σ α :
α ∈ dom σ.(stapes) → SeriesC (state_step σ α) = 1.
Proof.
intros Hdom.
rewrite /state_step bool_decide_eq_true_2 //.
destruct (stapes σ !!! α) as [[i pv] xs].
case_match eqn:Hss.
- rewrite dmap_mass. by eapply sig_sample_mass.
- apply dret_mass.
Qed.
Lemma head_step_mass e σ :
(∃ ρ, head_step e σ ρ > 0) → SeriesC (head_step e σ) = 1.
Proof.
intros [[] Hs%head_step_support_equiv_rel].
inversion Hs; simplify_eq/=; try (solve_distr_mass).
all: repeat (match goal with
| H : un_op_eval _ _ = _ |- _ => rewrite H
| H : bin_op_eval _ _ _ = _ |- _ => rewrite H
| H : heap _ !! _ = _ |- _ => rewrite H
| H : stapes _ !! _ = _ |- _ => rewrite H
| H : sig_sample _ _ _ = _ |- _ => rewrite H
| |- context [bool_decide (?i = ?i ∧ ?p = ?p)] => rewrite bool_decide_eq_true_2; [|done]
| Hn : ¬ (_ ∧ _) |- context [bool_decide (_ ∧ _)] => rewrite (bool_decide_eq_false_2 _ Hn)
| |- context [bool_decide (0 < _)%nat] => rewrite bool_decide_eq_true_2; [|done]
end); simpl.
all: first [ apply dret_mass | (rewrite dmap_mass; by eapply sig_sample_mass) ].
Qed.
Lemma 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.
Proof. destruct Ki2, Ki1; naive_solver eauto with f_equal. Qed.
Fixpoint height (e : expr) : nat :=
match e with
| Val _ => 1
| Var _ => 1
| Rec _ _ e => 1 + height e
| App e1 e2 => 1 + height e1 + height e2
| UnOp _ e => 1 + height e
| BinOp _ e1 e2 => 1 + height e1 + height e2
| If e0 e1 e2 => 1 + height e0 + height e1 + height e2
| Pair e1 e2 => 1 + height e1 + height e2
| Fst e => 1 + height e
| Snd e => 1 + height e
| InjL e => 1 + height e
| InjR e => 1 + height e
| Case e0 e1 e2 => 1 + height e0 + height e1 + height e2
| AllocN e1 e2 => 1 + height e1 + height e2
| Deref e => 1 + height e
| Store e1 e2 => 1 + height e1 + height e2
| Sample _ e1 e2 => 1 + height e1 + height e2
| AllocSampleTape _ e1 => 1 + height e1
| Tick e => 1 + height e
end.
Definition expr_ord (e1 e2 : expr) : Prop := (height e1 < height e2)%nat.
Lemma expr_ord_wf' h e : (height e ≤ h)%nat → Acc expr_ord e.
Proof.
rewrite /expr_ord. revert e; induction h.
{ destruct e; simpl; lia. }
intros []; simpl;
constructor; simpl; intros []; eauto with lia.
Defined.
Lemma expr_ord_wf : well_founded expr_ord.
Proof. red; intro; eapply expr_ord_wf'; eauto. Defined.
(* TODO: this proof is slow, but I do not see how to make it faster... *)
Lemma decomp_expr_ord Ki e e' : decomp_item e = Some (Ki, e') → expr_ord e' e.
Proof.
rewrite /expr_ord /decomp_item.
destruct Ki ; repeat destruct_match ; intros [=] ; subst ; cbn ; lia.
Qed.
Lemma decomp_fill_item Ki e :
to_val e = None → decomp_item (fill_item Ki e) = Some (Ki, e).
Proof. destruct Ki ; simpl ; by repeat destruct_match. Qed.
(* TODO: this proof is slow, but I do not see how to make it faster... *)
Lemma decomp_fill_item_2 e e' Ki :
decomp_item e = Some (Ki, e') → fill_item Ki e' = e ∧ to_val e' = None.
Proof.
rewrite /decomp_item ;
destruct e ; try done ;
destruct Ki ; cbn ; repeat destruct_match ; intros [=] ; subst ; auto.
Qed.
Definition get_active (σ : state) : list loc := elements (dom σ.(stapes)).
Lemma state_step_get_active_mass σ α :
α ∈ get_active σ → SeriesC (state_step σ α) = 1.
Proof. rewrite elem_of_elements. apply state_step_mass. Qed.
Lemma state_steps_mass σ αs :
αs ⊆ get_active σ →
SeriesC (foldlM state_step σ αs) = 1.
Proof.
induction αs as [|α αs IH] in σ |-* ; intros Hact.
{ rewrite /= dret_mass //. }
rewrite foldlM_cons.
rewrite dbind_det //.
- apply state_step_get_active_mass. set_solver.
- intros σ' Hσ'. apply IH.
apply state_step_support_equiv_rel in Hσ'.
inversion Hσ'; simplify_eq; last (intros α' ?; eapply Hact; set_solver).
intros α' ?. rewrite /get_active /=.
apply elem_of_elements, elem_of_dom.
destruct (decide (α = α')); subst.
+ eexists. rewrite lookup_insert_eq //.
+ rewrite lookup_insert_ne //.
apply elem_of_dom. eapply elem_of_elements, Hact. by right.
Qed.
Lemma gen_lang_mixin :
EctxiLanguageMixin of_val to_val fill_item decomp_item expr_ord head_step state_step get_active.
Proof.
split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
state_step_head_step_not_stuck, state_step_get_active_mass, head_step_mass,
fill_item_val, fill_item_no_val_inj, head_ctx_step_val,
decomp_fill_item, decomp_fill_item_2, expr_ord_wf, decomp_expr_ord.
Qed.
End semantics.
End gen_prob_lang.
(* Prefer gen_prob_lang names over ectx_language names. *)
Export gen_prob_lang.
Language (parametric in the distribution signature S)
Definition gen_ectxi_lang (S : Sig) : ectxiLanguage :=
EctxiLanguage get_active (gen_lang_mixin S) (def_val := def_val).
Definition gen_ectx_lang (S : Sig) : ectxLanguage := EctxLanguageOfEctxi (gen_ectxi_lang S).
Definition gen_lang (S : Sig) : language := LanguageOfEctx (gen_ectx_lang S).
Definition cfg : Type := expr * state.
EctxiLanguage get_active (gen_lang_mixin S) (def_val := def_val).
Definition gen_ectx_lang (S : Sig) : ectxLanguage := EctxLanguageOfEctxi (gen_ectxi_lang S).
Definition gen_lang (S : Sig) : language := LanguageOfEctx (gen_ectx_lang S).
Definition cfg : Type := expr * state.