clutch.con_prob_lang.lang
From Stdlib Require Import Reals Psatz.
From Coquelicot Require Import Rbar Lim_seq.
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 mdp.
From clutch.common Require Export con_language con_ectx_language con_ectxi_language locations.
From iris.prelude Require Import options.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Module con_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 *)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
(* Probabilistic choice *)
| AllocTape (e : expr)
| Rand (e1 e2 : expr)
(* No-op operator used for cost *)
| Tick (e : expr)
(* concurrency *)
| Fork (e : expr)
(* arbitrary atomic expressions*)
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
| Xchg (e0 : expr) (e1 : expr)
| FAA (e1 : expr) (e2 : expr)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope 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.
From Coquelicot Require Import Rbar Lim_seq.
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 mdp.
From clutch.common Require Export con_language con_ectx_language con_ectxi_language locations.
From iris.prelude Require Import options.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Module con_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 *)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
(* Probabilistic choice *)
| AllocTape (e : expr)
| Rand (e1 e2 : expr)
(* No-op operator used for cost *)
| Tick (e : expr)
(* concurrency *)
| Fork (e : expr)
(* arbitrary atomic expressions*)
| CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
| Xchg (e0 : expr) (e1 : expr)
| FAA (e1 : expr) (e2 : expr)
with val :=
| LitV (l : base_lit)
| RecV (f x : binder) (e : expr)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope 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.
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 !_ !_ /.
Definition tape := { n : nat & list (fin (S n)) }.
Global Instance tape_inhabited : Inhabited tape := populate (existT 0%nat []).
Global Instance tape_eq_dec : EqDecision tape. Proof. apply _. Defined.
Global Instance tape_countable : EqDecision tape. Proof. apply _. Qed.
Global Instance tapes_lookup_total : LookupTotal loc tape (gmap loc tape).
Proof. apply map_lookup_total. Defined.
Global Instance tapes_insert : Insert loc tape (gmap loc tape).
Proof. apply map_insert. Defined.
val_is_unboxed vl ∨ val_is_unboxed v1.
Global Arguments vals_compare_safe !_ !_ /.
Definition tape := { n : nat & list (fin (S n)) }.
Global Instance tape_inhabited : Inhabited tape := populate (existT 0%nat []).
Global Instance tape_eq_dec : EqDecision tape. Proof. apply _. Defined.
Global Instance tape_countable : EqDecision tape. Proof. apply _. Qed.
Global Instance tapes_lookup_total : LookupTotal loc tape (gmap loc tape).
Proof. apply map_lookup_total. Defined.
Global Instance tapes_insert : Insert loc tape (gmap loc tape).
Proof. apply map_insert. Defined.
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'))
| Load e, Load e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| AllocTape e, AllocTape e' => cast_if (decide (e = e'))
| Rand e1 e2, Rand e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Tick e, Tick e' => cast_if (decide (e = e'))
| Fork e, Fork e' => cast_if (decide (e = e'))
| CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| Xchg e1 e2, Xchg e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| FAA e1 e2, FAA e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| _, _ => 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]
| Load e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| AllocTape e => GenNode 15 [go e]
| Rand e1 e2 => GenNode 16 [go e1; go e2]
| Tick e => GenNode 17 [go e]
| Fork e => GenNode 18 [go e]
| CmpXchg e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
| Xchg e1 e2 => GenNode 20 [go e1; go e2]
| FAA e1 e2 => GenNode 21 [go e1; go e2]
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] => Load (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e] => AllocTape (go e)
| GenNode 16 [e1; e2] => Rand (go e1) (go e2)
| GenNode 17 [e] => Tick (go e)
| GenNode 18 [e] => Fork (go e)
| GenNode 19 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
| GenNode 20 [e1; e2] => Xchg (go e1) (go e2)
| GenNode 21 [e1; e2] => FAA (go e1) (go e2)
| _ => 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 as [v| | | | | | | | | | | | | | | | | | | | | | ]; simpl; f_equal;
[exact (gov v)|done..].
- 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), σ.(tapes));
decode p := '(h, t) ← decode p; mret {|heap:=h; tapes:=t|} |}.
Next Obligation. intros [h t]. rewrite decode_encode //=. Qed.
Global Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; tapes := 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.
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'))
| Load e, Load e' => cast_if (decide (e = e'))
| Store e1 e2, Store e1' e2' =>
cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| AllocTape e, AllocTape e' => cast_if (decide (e = e'))
| Rand e1 e2, Rand e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| Tick e, Tick e' => cast_if (decide (e = e'))
| Fork e, Fork e' => cast_if (decide (e = e'))
| CmpXchg e0 e1 e2, CmpXchg e0' e1' e2' =>
cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
| Xchg e1 e2, Xchg e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| FAA e1 e2, FAA e1' e2' => cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
| _, _ => 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]
| Load e => GenNode 13 [go e]
| Store e1 e2 => GenNode 14 [go e1; go e2]
| AllocTape e => GenNode 15 [go e]
| Rand e1 e2 => GenNode 16 [go e1; go e2]
| Tick e => GenNode 17 [go e]
| Fork e => GenNode 18 [go e]
| CmpXchg e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
| Xchg e1 e2 => GenNode 20 [go e1; go e2]
| FAA e1 e2 => GenNode 21 [go e1; go e2]
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] => Load (go e)
| GenNode 14 [e1; e2] => Store (go e1) (go e2)
| GenNode 15 [e] => AllocTape (go e)
| GenNode 16 [e1; e2] => Rand (go e1) (go e2)
| GenNode 17 [e] => Tick (go e)
| GenNode 18 [e] => Fork (go e)
| GenNode 19 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
| GenNode 20 [e1; e2] => Xchg (go e1) (go e2)
| GenNode 21 [e1; e2] => FAA (go e1) (go e2)
| _ => 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 as [v| | | | | | | | | | | | | | | | | | | | | | ]; simpl; f_equal;
[exact (gov v)|done..].
- 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), σ.(tapes));
decode p := '(h, t) ← decode p; mret {|heap:=h; tapes:=t|} |}.
Next Obligation. intros [h t]. rewrite decode_encode //=. Qed.
Global Instance state_inhabited : Inhabited state :=
populate {| heap := inhabitant; tapes := 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.
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)
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| AllocTapeCtx
| RandLCtx (v2 : val)
| RandRCtx (e1 : expr)
| TickCtx
| XchgLCtx (v2 : val)
| XchgRCtx (e1 : expr)
| CmpXchgLCtx (v1 : val) (v2 : val)
| CmpXchgMCtx (e0 : expr) (v2 : val)
| CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
.
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
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| AllocTapeCtx => AllocTape e
| RandLCtx v2 => Rand e (Val v2)
| RandRCtx e1 => Rand e1 e
| TickCtx => Tick e
| XchgLCtx v2 => Xchg e (Val v2)
| XchgRCtx e1 => Xchg e1 e
| CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
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
| Load e => noval e LoadCtx
| Store e1 e2 =>
match e2 with
| Val v => noval e1 (StoreLCtx v)
| _ => Some (StoreRCtx e1, e2)
end
| AllocTape e => noval e AllocTapeCtx
| Rand e1 e2 =>
match e2 with
| Val v => noval e1 (RandLCtx v)
| _ => Some (RandRCtx e1, e2)
end
| Tick e => noval e TickCtx
| Fork e => None
| CmpXchg e0 e1 e2 =>
match e2 with
| Val v2 =>
match e1 with
| Val v1 =>
noval e0 (CmpXchgLCtx v1 v2)
| _ =>Some (CmpXchgMCtx e0 v2, e1)
end
| _ => Some (CmpXchgRCtx e0 e1, e2)
end
| Xchg e1 e2 =>
match e2 with
| Val v => noval e1 (XchgLCtx v)
| _ => Some (XchgRCtx e1, e2)
end
| FAA e1 e2 =>
match e2 with
| Val v => noval e1 (FaaLCtx v)
| _ => Some (FaaRCtx e1, e2)
end
| _ => 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)
| LoadCtx
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| AllocTapeCtx
| RandLCtx (v2 : val)
| RandRCtx (e1 : expr)
| TickCtx
| XchgLCtx (v2 : val)
| XchgRCtx (e1 : expr)
| CmpXchgLCtx (v1 : val) (v2 : val)
| CmpXchgMCtx (e0 : expr) (v2 : val)
| CmpXchgRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr)
.
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
| LoadCtx => Load e
| StoreLCtx v2 => Store e (Val v2)
| StoreRCtx e1 => Store e1 e
| AllocTapeCtx => AllocTape e
| RandLCtx v2 => Rand e (Val v2)
| RandRCtx e1 => Rand e1 e
| TickCtx => Tick e
| XchgLCtx v2 => Xchg e (Val v2)
| XchgRCtx e1 => Xchg e1 e
| CmpXchgLCtx v1 v2 => CmpXchg e (Val v1) (Val v2)
| CmpXchgMCtx e0 v2 => CmpXchg e0 e (Val v2)
| CmpXchgRCtx e0 e1 => CmpXchg e0 e1 e
| FaaLCtx v2 => FAA e (Val v2)
| FaaRCtx e1 => FAA e1 e
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
| Load e => noval e LoadCtx
| Store e1 e2 =>
match e2 with
| Val v => noval e1 (StoreLCtx v)
| _ => Some (StoreRCtx e1, e2)
end
| AllocTape e => noval e AllocTapeCtx
| Rand e1 e2 =>
match e2 with
| Val v => noval e1 (RandLCtx v)
| _ => Some (RandRCtx e1, e2)
end
| Tick e => noval e TickCtx
| Fork e => None
| CmpXchg e0 e1 e2 =>
match e2 with
| Val v2 =>
match e1 with
| Val v1 =>
noval e0 (CmpXchgLCtx v1 v2)
| _ =>Some (CmpXchgMCtx e0 v2, e1)
end
| _ => Some (CmpXchgRCtx e0 e1, e2)
end
| Xchg e1 e2 =>
match e2 with
| Val v => noval e1 (XchgLCtx v)
| _ => Some (XchgRCtx e1, e2)
end
| FAA e1 e2 =>
match e2 with
| Val v => noval e1 (FaaLCtx v)
| _ => Some (FaaRCtx e1, e2)
end
| _ => 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)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| AllocTape e => AllocTape (subst x v e)
| Rand e1 e2 => Rand (subst x v e1) (subst x v e2)
| Tick e => Tick (subst x v e)
| Fork e => Fork (subst x v e)
| CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
| Xchg e1 e2 => Xchg (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => λ 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)
| Load e => Load (subst x v e)
| Store e1 e2 => Store (subst x v e1) (subst x v e2)
| AllocTape e => AllocTape (subst x v e)
| Rand e1 e2 => Rand (subst x v e1) (subst x v e2)
| Tick e => Tick (subst x v e)
| Fork e => Fork (subst x v e)
| CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
| Xchg e1 e2 => Xchg (subst x v e1) (subst x v e2)
| FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
end.
Definition subst' (mx : binder) (v : val) : expr → expr :=
match mx with BNamed x => subst x v | BAnon => λ 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); tapes := σ.(tapes) |}.
Global Arguments state_upd_heap _ !_ /.
Definition state_upd_tapes (f : gmap loc tape → gmap loc tape) (σ : state) : state :=
{| heap := σ.(heap); tapes := f σ.(tapes) |}.
Global Arguments state_upd_tapes _ !_ /.
Lemma state_upd_tapes_twice σ l n xs ys :
state_upd_tapes <[l:=(n; ys)]> (state_upd_tapes <[l:=(n; xs)]> σ) = state_upd_tapes <[l:=(n; ys)]> σ.
Proof. rewrite /state_upd_tapes /=. f_equal. apply insert_insert_eq. Qed.
Lemma state_upd_tapes_same σ σ' l n xs ys :
state_upd_tapes <[l:=(n; ys)]> σ = state_upd_tapes <[l:=(n; xs)]> σ' -> xs = ys.
Proof. rewrite /state_upd_tapes /=. 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_tapes_no_change σ l n ys :
tapes σ !! l = Some (n; ys)->
state_upd_tapes <[l:=(n; ys)]> σ = σ .
Proof.
destruct σ as [? t]. simpl.
intros Ht.
f_equal.
apply insert_id. done.
Qed.
Lemma state_upd_tapes_same' σ σ' l n xs (x y : fin (S n)) :
state_upd_tapes <[l:=(n; xs++[x])]> σ = state_upd_tapes <[l:=(n; xs++[y])]> σ' -> x = y.
Proof. intros H. apply state_upd_tapes_same in H.
by simplify_eq.
Qed.
Lemma state_upd_tapes_neq' σ σ' l n xs (x y : fin (S n)) :
x≠y -> state_upd_tapes <[l:=(n; xs++[x])]> σ ≠ state_upd_tapes <[l:=(n; xs++[y])]> σ'.
Proof. move => H /state_upd_tapes_same ?. simplify_eq.
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_tapes_heap σ l1 l2 n xs m v :
state_upd_tapes <[l2:=(n; xs)]> (state_upd_heap_N l1 m v σ) =
state_upd_heap_N l1 m v (state_upd_tapes <[l2:=(n; xs)]> σ).
Proof.
by rewrite /state_upd_tapes /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.
Definition head_step (e1 : expr) (σ1 : state) : distr (expr * state * list (expr)) :=
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
| Load (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
(* Since our language only has integers, we use Z.to_nat, which maps positive
integers to the corresponding nat, and the rest to 0. We sample from
dunifP N = dunif (1 + N) to avoid the case dunif 0 = dzero. *)
(* Uniform sampling from 0, 1 , ..., N *)
| Rand (Val (LitV (LitInt N))) (Val (LitV LitUnit)) =>
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP (Z.to_nat N))
| AllocTape (Val (LitV (LitInt z))) =>
let ι := fresh_loc σ1.(tapes) in
dret (Val $ LitV $ LitLbl ι, state_upd_tapes <[ι := (Z.to_nat z; []) ]> σ1, [])
(* Labelled sampling, conditional on tape contents *)
| Rand (Val (LitV (LitInt N))) (Val (LitV (LitLbl l))) =>
match σ1.(tapes) !! l with
| Some (M; ns) =>
if bool_decide (M = Z.to_nat N) then
match ns with
| n :: ns =>
(* the tape is non-empty so we consume the first number *)
dret (Val $ LitV $ LitInt $ fin_to_nat n, state_upd_tapes <[l:=(M; ns)]> σ1, [])
| [] =>
(* the tape is allocated but empty, so we sample from 0, 1, ..., M uniformly *)
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP M)
end
else
(* bound did not match the bound of the tape *)
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP (Z.to_nat N))
| None => dzero
end
| Tick (Val (LitV (LitInt n))) => dret (Val $ LitV $ LitUnit, σ1, [])
| Fork e => dret (Val $ LitV $ LitUnit, σ1, [e])
| CmpXchg (Val (LitV (LitLoc l))) (Val v1) (Val v2) =>
match σ1.(heap) !! l with
| Some v =>
if decide (vals_compare_safe v v1)
then
let b:= bool_decide (v=v1) in
dret (Val $ PairV v (LitV $ LitBool b),
(if b then state_upd_heap <[l:=v2]> σ1 else σ1),
[])
else dzero
| None => dzero
end
| Xchg (Val (LitV (LitLoc l))) (Val v2) =>
match σ1.(heap)!!l with
| Some v1 => dret (Val v1, state_upd_heap <[l:=v2]> σ1, [])
| None => dzero
end
| FAA (Val (LitV (LitLoc l))) (Val (LitV (LitInt i2))) =>
match σ1.(heap)!!l with
| Some (LitV (LitInt i1)) => dret (Val $ LitV $ LitInt i1,
state_upd_heap <[l:=LitV (LitInt (i1+i2))]> σ1,
[])
| _ => dzero
end
| _ => dzero
end.
Definition state_step (σ1 : state) (α : loc) : distr state :=
if bool_decide (α ∈ dom σ1.(tapes)) then
let: (N; ns) := (σ1.(tapes) !!! α) in
dmap (λ n, state_upd_tapes (<[α := (N; ns ++ [n])]>) σ1) (dunifP N)
else dzero.
Lemma state_step_unfold σ α N ns:
tapes σ !! α = Some (N; ns) ->
state_step σ α = dmap (λ n, state_upd_tapes (<[α := (N; ns ++ [n])]>) σ) (dunifP N).
Proof.
intros H.
rewrite /state_step.
rewrite bool_decide_eq_true_2; last first.
{ by apply elem_of_dom. }
by rewrite (lookup_total_correct (tapes σ) α (N; ns)); last done.
Qed.
Lemma iterM_state_step_unfold σ (N p:nat) α xs :
σ.(tapes) !! α = Some (N%nat; xs) ->
(iterM p (λ σ1', state_step σ1' α) σ) =
dmap (λ v, state_upd_tapes <[α := (N%nat; xs ++ v)]> σ)
(dunifv N p).
Proof.
revert σ N α xs.
induction p as [|p' IH].
{ (* base case *)
intros. simpl.
apply distr_ext.
intros. rewrite /dret/dret_pmf{1}/pmf/=.
rewrite dmap_unfold_pmf.
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); tapes := σ.(tapes) |}.
Global Arguments state_upd_heap _ !_ /.
Definition state_upd_tapes (f : gmap loc tape → gmap loc tape) (σ : state) : state :=
{| heap := σ.(heap); tapes := f σ.(tapes) |}.
Global Arguments state_upd_tapes _ !_ /.
Lemma state_upd_tapes_twice σ l n xs ys :
state_upd_tapes <[l:=(n; ys)]> (state_upd_tapes <[l:=(n; xs)]> σ) = state_upd_tapes <[l:=(n; ys)]> σ.
Proof. rewrite /state_upd_tapes /=. f_equal. apply insert_insert_eq. Qed.
Lemma state_upd_tapes_same σ σ' l n xs ys :
state_upd_tapes <[l:=(n; ys)]> σ = state_upd_tapes <[l:=(n; xs)]> σ' -> xs = ys.
Proof. rewrite /state_upd_tapes /=. 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_tapes_no_change σ l n ys :
tapes σ !! l = Some (n; ys)->
state_upd_tapes <[l:=(n; ys)]> σ = σ .
Proof.
destruct σ as [? t]. simpl.
intros Ht.
f_equal.
apply insert_id. done.
Qed.
Lemma state_upd_tapes_same' σ σ' l n xs (x y : fin (S n)) :
state_upd_tapes <[l:=(n; xs++[x])]> σ = state_upd_tapes <[l:=(n; xs++[y])]> σ' -> x = y.
Proof. intros H. apply state_upd_tapes_same in H.
by simplify_eq.
Qed.
Lemma state_upd_tapes_neq' σ σ' l n xs (x y : fin (S n)) :
x≠y -> state_upd_tapes <[l:=(n; xs++[x])]> σ ≠ state_upd_tapes <[l:=(n; xs++[y])]> σ'.
Proof. move => H /state_upd_tapes_same ?. simplify_eq.
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_tapes_heap σ l1 l2 n xs m v :
state_upd_tapes <[l2:=(n; xs)]> (state_upd_heap_N l1 m v σ) =
state_upd_heap_N l1 m v (state_upd_tapes <[l2:=(n; xs)]> σ).
Proof.
by rewrite /state_upd_tapes /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.
Definition head_step (e1 : expr) (σ1 : state) : distr (expr * state * list (expr)) :=
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
| Load (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
(* Since our language only has integers, we use Z.to_nat, which maps positive
integers to the corresponding nat, and the rest to 0. We sample from
dunifP N = dunif (1 + N) to avoid the case dunif 0 = dzero. *)
(* Uniform sampling from 0, 1 , ..., N *)
| Rand (Val (LitV (LitInt N))) (Val (LitV LitUnit)) =>
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP (Z.to_nat N))
| AllocTape (Val (LitV (LitInt z))) =>
let ι := fresh_loc σ1.(tapes) in
dret (Val $ LitV $ LitLbl ι, state_upd_tapes <[ι := (Z.to_nat z; []) ]> σ1, [])
(* Labelled sampling, conditional on tape contents *)
| Rand (Val (LitV (LitInt N))) (Val (LitV (LitLbl l))) =>
match σ1.(tapes) !! l with
| Some (M; ns) =>
if bool_decide (M = Z.to_nat N) then
match ns with
| n :: ns =>
(* the tape is non-empty so we consume the first number *)
dret (Val $ LitV $ LitInt $ fin_to_nat n, state_upd_tapes <[l:=(M; ns)]> σ1, [])
| [] =>
(* the tape is allocated but empty, so we sample from 0, 1, ..., M uniformly *)
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP M)
end
else
(* bound did not match the bound of the tape *)
dmap (λ n : fin _, (Val $ LitV $ LitInt n, σ1, [])) (dunifP (Z.to_nat N))
| None => dzero
end
| Tick (Val (LitV (LitInt n))) => dret (Val $ LitV $ LitUnit, σ1, [])
| Fork e => dret (Val $ LitV $ LitUnit, σ1, [e])
| CmpXchg (Val (LitV (LitLoc l))) (Val v1) (Val v2) =>
match σ1.(heap) !! l with
| Some v =>
if decide (vals_compare_safe v v1)
then
let b:= bool_decide (v=v1) in
dret (Val $ PairV v (LitV $ LitBool b),
(if b then state_upd_heap <[l:=v2]> σ1 else σ1),
[])
else dzero
| None => dzero
end
| Xchg (Val (LitV (LitLoc l))) (Val v2) =>
match σ1.(heap)!!l with
| Some v1 => dret (Val v1, state_upd_heap <[l:=v2]> σ1, [])
| None => dzero
end
| FAA (Val (LitV (LitLoc l))) (Val (LitV (LitInt i2))) =>
match σ1.(heap)!!l with
| Some (LitV (LitInt i1)) => dret (Val $ LitV $ LitInt i1,
state_upd_heap <[l:=LitV (LitInt (i1+i2))]> σ1,
[])
| _ => dzero
end
| _ => dzero
end.
Definition state_step (σ1 : state) (α : loc) : distr state :=
if bool_decide (α ∈ dom σ1.(tapes)) then
let: (N; ns) := (σ1.(tapes) !!! α) in
dmap (λ n, state_upd_tapes (<[α := (N; ns ++ [n])]>) σ1) (dunifP N)
else dzero.
Lemma state_step_unfold σ α N ns:
tapes σ !! α = Some (N; ns) ->
state_step σ α = dmap (λ n, state_upd_tapes (<[α := (N; ns ++ [n])]>) σ) (dunifP N).
Proof.
intros H.
rewrite /state_step.
rewrite bool_decide_eq_true_2; last first.
{ by apply elem_of_dom. }
by rewrite (lookup_total_correct (tapes σ) α (N; ns)); last done.
Qed.
Lemma iterM_state_step_unfold σ (N p:nat) α xs :
σ.(tapes) !! α = Some (N%nat; xs) ->
(iterM p (λ σ1', state_step σ1' α) σ) =
dmap (λ v, state_upd_tapes <[α := (N%nat; xs ++ v)]> σ)
(dunifv N p).
Proof.
revert σ N α xs.
induction p as [|p' IH].
{ (* base case *)
intros. simpl.
apply distr_ext.
intros. rewrite /dret/dret_pmf{1}/pmf/=.
rewrite dmap_unfold_pmf.
Why doesnt this work??
(* rewrite (@SeriesC_subset _ _ _ (λ x, x= (nil:list (fin (S N)))) _ _). *)
(* - rewrite (SeriesC_singleton_dependent nil). *)
erewrite (SeriesC_ext ).
- erewrite (SeriesC_singleton_dependent [] (λ a0:list (fin (S N)), dunifv N 0 a0 * (if bool_decide (a = state_upd_tapes <[α:=(N; xs ++ a0)]> σ) then 1 else 0))).
rewrite dunifv_pmf. simpl.
case_bool_decide.
+ rewrite bool_decide_eq_true_2; [lra|]. rewrite app_nil_r.
rewrite state_upd_tapes_no_change; done.
+ rewrite bool_decide_eq_false_2; [lra|]. rewrite app_nil_r.
rewrite state_upd_tapes_no_change; done.
- intros. simpl.
symmetry.
case_bool_decide; first done.
rewrite dunifv_pmf.
rewrite bool_decide_eq_false_2; first lra.
intros ?%nil_length_inv. done.
}
(* inductive case *)
intros σ N α xs Ht.
replace (S p') with (p'+1)%nat; last lia.
rewrite iterM_plus; simpl.
erewrite IH; last done.
erewrite dbind_ext_right; last first.
{ intros. apply dret_id_right. }
apply distr_ext. intros σ'. rewrite dmap_unfold_pmf.
replace (p'+1)%nat with (S p') by lia.
assert (Decision (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as Hdec.
{ (* can be improved *)
apply make_decision. }
destruct (decide (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as [K|K].
- (* σ' is reachable *)
destruct K as [v [Hlen ->]].
rewrite (SeriesC_subset (λ a, a = v)); last first.
{ intros a Ha.
rewrite bool_decide_eq_false_2; first lra.
move => /state_upd_tapes_same. intros L. simplify_eq.
}
rewrite SeriesC_singleton_dependent. rewrite bool_decide_eq_true_2; last done.
rewrite dunifv_pmf. rewrite Rmult_1_r.
remember (/ (S N ^ S p')%nat) as val eqn:Hval.
rewrite /dbind/dbind_pmf{1}/pmf/=.
rewrite (SeriesC_subset (λ a, a = state_upd_tapes <[α := (N; xs ++ take p' v)]> σ)).
+ rewrite SeriesC_singleton_dependent. erewrite state_step_unfold; last first.
{ simpl. rewrite lookup_insert_eq. done. }
rewrite !dmap_unfold_pmf.
rewrite (SeriesC_subset (λ a, a = take p' v)); last first.
{ intros. rewrite bool_decide_eq_false_2; first lra.
move => /state_upd_tapes_same. intros L. simplify_eq.
}
rewrite SeriesC_singleton_dependent.
rewrite bool_decide_eq_true_2; last done.
rewrite dunifv_pmf.
rewrite bool_decide_eq_true_2; last first.
{ rewrite firstn_length_le; lia. }
assert (is_Some (last v)) as [x Hsome].
{ rewrite last_is_Some. intros ?. subst. done. }
rewrite (SeriesC_subset (λ a, a = x)); last first.
{ intros a H'. rewrite bool_decide_eq_false_2; first lra.
rewrite state_upd_tapes_twice. move => /state_upd_tapes_same.
rewrite <-app_assoc. intros K.
simplify_eq. apply H'.
rewrite -K in Hsome.
rewrite last_snoc in Hsome. by simplify_eq.
}
rewrite SeriesC_singleton_dependent.
rewrite /dunifP dunif_pmf. rewrite bool_decide_eq_true_2; last rewrite state_upd_tapes_twice.
* rewrite bool_decide_eq_true_2; last done.
rewrite Hval.
cut ( / INR (S N ^ p') * (/ INR (S N)) = / INR (S N ^ S p')); first lra.
rewrite -Rinv_mult.
f_equal. rewrite -mult_INR. f_equal. simpl. lia.
* rewrite -app_assoc. repeat f_equal.
rewrite <-(firstn_all v) at 1.
rewrite Hlen. erewrite take_S_r; first done.
rewrite -Hsome last_lookup.
f_equal. rewrite Hlen. done.
+ (* prove that σ' is not an intermediate step*)
intros σ'.
intros Hσ.
assert (dmap (λ v0, state_upd_tapes <[α:=(N; xs ++ v0)]> σ) (dunifv N p') σ' * state_step σ' α (state_upd_tapes <[α:=(N; xs ++ v)]> σ) >= 0) as [H|H]; last done.
{ apply Rle_ge. apply Rmult_le_pos; auto. }
exfalso.
apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
{ pose proof pmf_pos (state_step σ' α) (state_upd_tapes <[α:=(N; xs ++ v)]> σ). lra. }
rewrite dmap_pos in H1.
destruct H1 as [v' [-> H1]].
apply Hσ. repeat f_equal.
erewrite state_step_unfold in H2; last first.
{ simpl. apply lookup_insert_eq. }
apply dmap_pos in H2.
destruct H2 as [a [H2?]].
rewrite state_upd_tapes_twice in H2.
apply state_upd_tapes_same in H2. rewrite -app_assoc in H2. simplify_eq.
rewrite take_app_length'; first done.
rewrite length_app in Hlen. simpl in *; lia.
- (* σ' is not reachable, i.e. both sides are zero *)
rewrite SeriesC_0; last first.
{ intros x.
assert (0<=dunifv N (S p') x) as [H|<-] by auto; last lra.
apply Rlt_gt in H.
rewrite -dunifv_pos in H.
rewrite bool_decide_eq_false_2; [lra|naive_solver].
}
rewrite /dbind/dbind_pmf{1}/pmf/=.
apply SeriesC_0.
intros σ''.
rewrite /dmap/dbind/dbind_pmf{1}/pmf/=.
setoid_rewrite dunifv_pmf.
assert (SeriesC
(λ a : list (fin (S N)),
(if bool_decide (length a = p') then / (S N ^ p')%nat else 0) *
dret (state_upd_tapes <[α:=(N; xs ++ a)]> σ) σ'') * state_step σ'' α σ' >= 0) as [H|H]; last done.
{ apply Rle_ge. apply Rmult_le_pos; auto. apply SeriesC_ge_0'.
intros. apply Rmult_le_pos; auto. case_bool_decide; try lra.
rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
apply lt_0_INR.
epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
Unshelve.
all: lia.
}
apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
{ pose proof pmf_pos (state_step σ'' α) σ'. lra. }
epose proof SeriesC_gtz_ex _ _ H1. simpl in *.
destruct H as [v H].
apply Rmult_pos_cases in H as [[? H]|[]]; last first.
{ epose proof pmf_pos (dret (state_upd_tapes <[α:=(N; xs ++ v)]> σ)) σ''. lra. }
apply dret_pos in H; subst.
case_bool_decide; last lra.
erewrite state_step_unfold in H2; last first.
{ simpl. rewrite lookup_insert_eq. done. }
exfalso.
apply K. rewrite dmap_pos in H2. destruct H2 as [x[-> H2]]. subst.
setoid_rewrite state_upd_tapes_twice.
rewrite -app_assoc.
exists (v++[x]); rewrite length_app; simpl; split; first lia. done.
Unshelve.
simpl.
intros. case_bool_decide; last real_solver.
apply Rmult_le_pos; last auto.
rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
apply lt_0_INR.
epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
Unshelve.
all: lia.
Qed.
(* - rewrite (SeriesC_singleton_dependent nil). *)
erewrite (SeriesC_ext ).
- erewrite (SeriesC_singleton_dependent [] (λ a0:list (fin (S N)), dunifv N 0 a0 * (if bool_decide (a = state_upd_tapes <[α:=(N; xs ++ a0)]> σ) then 1 else 0))).
rewrite dunifv_pmf. simpl.
case_bool_decide.
+ rewrite bool_decide_eq_true_2; [lra|]. rewrite app_nil_r.
rewrite state_upd_tapes_no_change; done.
+ rewrite bool_decide_eq_false_2; [lra|]. rewrite app_nil_r.
rewrite state_upd_tapes_no_change; done.
- intros. simpl.
symmetry.
case_bool_decide; first done.
rewrite dunifv_pmf.
rewrite bool_decide_eq_false_2; first lra.
intros ?%nil_length_inv. done.
}
(* inductive case *)
intros σ N α xs Ht.
replace (S p') with (p'+1)%nat; last lia.
rewrite iterM_plus; simpl.
erewrite IH; last done.
erewrite dbind_ext_right; last first.
{ intros. apply dret_id_right. }
apply distr_ext. intros σ'. rewrite dmap_unfold_pmf.
replace (p'+1)%nat with (S p') by lia.
assert (Decision (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as Hdec.
{ (* can be improved *)
apply make_decision. }
destruct (decide (∃ v: list (fin (S N)), length v = S p' /\ σ' = state_upd_tapes <[α:=(N; xs ++ v)]> σ)) as [K|K].
- (* σ' is reachable *)
destruct K as [v [Hlen ->]].
rewrite (SeriesC_subset (λ a, a = v)); last first.
{ intros a Ha.
rewrite bool_decide_eq_false_2; first lra.
move => /state_upd_tapes_same. intros L. simplify_eq.
}
rewrite SeriesC_singleton_dependent. rewrite bool_decide_eq_true_2; last done.
rewrite dunifv_pmf. rewrite Rmult_1_r.
remember (/ (S N ^ S p')%nat) as val eqn:Hval.
rewrite /dbind/dbind_pmf{1}/pmf/=.
rewrite (SeriesC_subset (λ a, a = state_upd_tapes <[α := (N; xs ++ take p' v)]> σ)).
+ rewrite SeriesC_singleton_dependent. erewrite state_step_unfold; last first.
{ simpl. rewrite lookup_insert_eq. done. }
rewrite !dmap_unfold_pmf.
rewrite (SeriesC_subset (λ a, a = take p' v)); last first.
{ intros. rewrite bool_decide_eq_false_2; first lra.
move => /state_upd_tapes_same. intros L. simplify_eq.
}
rewrite SeriesC_singleton_dependent.
rewrite bool_decide_eq_true_2; last done.
rewrite dunifv_pmf.
rewrite bool_decide_eq_true_2; last first.
{ rewrite firstn_length_le; lia. }
assert (is_Some (last v)) as [x Hsome].
{ rewrite last_is_Some. intros ?. subst. done. }
rewrite (SeriesC_subset (λ a, a = x)); last first.
{ intros a H'. rewrite bool_decide_eq_false_2; first lra.
rewrite state_upd_tapes_twice. move => /state_upd_tapes_same.
rewrite <-app_assoc. intros K.
simplify_eq. apply H'.
rewrite -K in Hsome.
rewrite last_snoc in Hsome. by simplify_eq.
}
rewrite SeriesC_singleton_dependent.
rewrite /dunifP dunif_pmf. rewrite bool_decide_eq_true_2; last rewrite state_upd_tapes_twice.
* rewrite bool_decide_eq_true_2; last done.
rewrite Hval.
cut ( / INR (S N ^ p') * (/ INR (S N)) = / INR (S N ^ S p')); first lra.
rewrite -Rinv_mult.
f_equal. rewrite -mult_INR. f_equal. simpl. lia.
* rewrite -app_assoc. repeat f_equal.
rewrite <-(firstn_all v) at 1.
rewrite Hlen. erewrite take_S_r; first done.
rewrite -Hsome last_lookup.
f_equal. rewrite Hlen. done.
+ (* prove that σ' is not an intermediate step*)
intros σ'.
intros Hσ.
assert (dmap (λ v0, state_upd_tapes <[α:=(N; xs ++ v0)]> σ) (dunifv N p') σ' * state_step σ' α (state_upd_tapes <[α:=(N; xs ++ v)]> σ) >= 0) as [H|H]; last done.
{ apply Rle_ge. apply Rmult_le_pos; auto. }
exfalso.
apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
{ pose proof pmf_pos (state_step σ' α) (state_upd_tapes <[α:=(N; xs ++ v)]> σ). lra. }
rewrite dmap_pos in H1.
destruct H1 as [v' [-> H1]].
apply Hσ. repeat f_equal.
erewrite state_step_unfold in H2; last first.
{ simpl. apply lookup_insert_eq. }
apply dmap_pos in H2.
destruct H2 as [a [H2?]].
rewrite state_upd_tapes_twice in H2.
apply state_upd_tapes_same in H2. rewrite -app_assoc in H2. simplify_eq.
rewrite take_app_length'; first done.
rewrite length_app in Hlen. simpl in *; lia.
- (* σ' is not reachable, i.e. both sides are zero *)
rewrite SeriesC_0; last first.
{ intros x.
assert (0<=dunifv N (S p') x) as [H|<-] by auto; last lra.
apply Rlt_gt in H.
rewrite -dunifv_pos in H.
rewrite bool_decide_eq_false_2; [lra|naive_solver].
}
rewrite /dbind/dbind_pmf{1}/pmf/=.
apply SeriesC_0.
intros σ''.
rewrite /dmap/dbind/dbind_pmf{1}/pmf/=.
setoid_rewrite dunifv_pmf.
assert (SeriesC
(λ a : list (fin (S N)),
(if bool_decide (length a = p') then / (S N ^ p')%nat else 0) *
dret (state_upd_tapes <[α:=(N; xs ++ a)]> σ) σ'') * state_step σ'' α σ' >= 0) as [H|H]; last done.
{ apply Rle_ge. apply Rmult_le_pos; auto. apply SeriesC_ge_0'.
intros. apply Rmult_le_pos; auto. case_bool_decide; try lra.
rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
apply lt_0_INR.
epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
Unshelve.
all: lia.
}
apply Rmult_pos_cases in H as [[H1 H2]|[? H]]; last first.
{ pose proof pmf_pos (state_step σ'' α) σ'. lra. }
epose proof SeriesC_gtz_ex _ _ H1. simpl in *.
destruct H as [v H].
apply Rmult_pos_cases in H as [[? H]|[]]; last first.
{ epose proof pmf_pos (dret (state_upd_tapes <[α:=(N; xs ++ v)]> σ)) σ''. lra. }
apply dret_pos in H; subst.
case_bool_decide; last lra.
erewrite state_step_unfold in H2; last first.
{ simpl. rewrite lookup_insert_eq. done. }
exfalso.
apply K. rewrite dmap_pos in H2. destruct H2 as [x[-> H2]]. subst.
setoid_rewrite state_upd_tapes_twice.
rewrite -app_assoc.
exists (v++[x]); rewrite length_app; simpl; split; first lia. done.
Unshelve.
simpl.
intros. case_bool_decide; last real_solver.
apply Rmult_le_pos; last auto.
rewrite -Rdiv_1_l. apply Rcomplements.Rdiv_le_0_compat; first lra.
apply lt_0_INR.
epose proof Nat.pow_le_mono_r (S N) 0 p' _ _ as H0; simpl in H0; lia.
Unshelve.
all: lia.
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 -> list expr → 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 σ) []
| LoadS l v σ :
σ.(heap) !! l = Some v →
head_step_rel (Load (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]> σ) []
| RandNoTapeS z N (n : fin (S N)) σ:
N = Z.to_nat z →
head_step_rel (Rand (Val $ LitV $ LitInt z) (Val $ LitV LitUnit)) σ (Val $ LitV $ LitInt n) σ []
| AllocTapeS z N σ l :
l = fresh_loc σ.(tapes) →
N = Z.to_nat z →
head_step_rel (AllocTape (Val (LitV (LitInt z)))) σ
(Val $ LitV $ LitLbl l) (state_upd_tapes <[l := (N; []) : tape]> σ) []
| RandTapeS l z N n ns σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((N; n :: ns) : tape) →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val (LitV (LitLbl l)))) σ
(Val $ LitV $ LitInt $ n) (state_upd_tapes <[l := (N; ns) : tape]> σ) []
| RandTapeEmptyS l z N (n : fin (S N)) σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((N; []) : tape) →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val $ LitV $ LitLbl l)) σ (Val $ LitV $ LitInt n) σ []
| RandTapeOtherS l z M N ms (n : fin (S N)) σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((M; ms) : tape) →
N ≠ M →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val $ LitV $ LitLbl l)) σ (Val $ LitV $ LitInt n) σ []
| TickS σ z :
head_step_rel (Tick $ Val $ LitV $ LitInt z) σ (Val $ LitV $ LitUnit) σ []
| ForkS e σ:
head_step_rel (Fork $ e) σ (Val $ LitV $ LitUnit) σ [e]
| CmpXchgS σ l vl v1 v2 b:
σ.(heap) !! l = Some vl ->
vals_compare_safe vl v1 ->
b = bool_decide (vl = v1) ->
head_step_rel (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ) []
| XchgS σ l v1 v2:
σ.(heap) !! l = Some v1 ->
head_step_rel (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ (Val v1) (state_upd_heap <[l:=v2]> σ) []
| FAAS σ l i1 i2:
σ.(heap) !! l = Some (LitV (LitInt i1)) ->
head_step_rel (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ (Val $ LitV $ LitInt i1)
(state_upd_heap <[l:= LitV (LitInt (i1+i2))]> σ) []
.
Create HintDb head_step.
Global Hint Constructors head_step_rel : head_step.
(* 0*)
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV LitUnit))) _ _ _ _) =>
eapply (RandNoTapeS _ _ 0%fin) : head_step.
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _ _) =>
eapply (RandTapeEmptyS _ _ _ 0%fin) : head_step.
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _ _) =>
eapply (RandTapeOtherS _ _ _ _ _ 0%fin) : head_step.
Inductive state_step_rel : state → loc → state → Prop :=
| AddTapeS α N (n : fin (S N)) ns σ :
α ∈ dom σ.(tapes) →
σ.(tapes) !!! α = ((N; ns) : tape) →
state_step_rel σ α (state_upd_tapes <[α := (N; ns ++ [n]) : tape]> σ).
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 l :
head_step e1 σ1 (e2, σ2, l) > 0 ↔ head_step_rel e1 σ1 e2 σ2 l.
Proof.
split.
- intros ?. destruct e1; inv_head_step; eauto with head_step.
all: constructor; try done; by case_bool_decide.
- inversion 1; simplify_map_eq/=; try case_bool_decide; simplify_eq; solve_distr; done.
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; [|intros; inv_distr].
case_match. intros ?. inv_distr.
econstructor; eauto with lia.
- inversion_clear 1.
rewrite bool_decide_eq_true_2 // H1. solve_distr.
Qed.
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.
split; intros [[e2 σ2] Hs].
(* TODO: the sub goals used to be solved by simplify_map_eq *)
- destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)).
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H11. done.
* rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H11. done.
* rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H10. done.
* rewrite lookup_insert_ne // in H10. rewrite H10 in H7. done.
- destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)).
+ destruct (decide (α = l1)); simplify_eq.
* apply not_elem_of_dom_2 in H11. done.
* rewrite lookup_insert_ne // in H7. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq // in H7.
apply not_elem_of_dom_2 in H11. done.
* rewrite lookup_insert_ne // in H7. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq // in H7.
apply not_elem_of_dom_2 in H10. done.
* rewrite lookup_insert_ne // in H7. rewrite H10 in H7. done.
Qed.
Lemma state_step_mass σ α :
α ∈ dom σ.(tapes) → SeriesC (state_step σ α) = 1.
Proof.
intros Hdom.
rewrite /state_step bool_decide_eq_true_2 //=.
case_match.
rewrite dmap_mass dunif_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;
repeat (simplify_map_eq/=; solve_distr_mass || case_match; try (case_bool_decide; done)).
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
| Load e => 1 + height e
| Store e1 e2 => 1 + height e1 + height e2
| AllocTape e => 1 + height e
| Rand e1 e2 => 1 + height e1 + height e2
| Tick e => 1 + height e
| Fork e => 1 + height e
| CmpXchg e0 e1 e2 => 1 + height e0 + height e1 + height e2
| Xchg e1 e2 => 1 + height e1 + height e2
| FAA e1 e2 => 1 + height e1 + height e2
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 σ.(tapes)).
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.
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 con_prob_lang_mixin :
ConEctxiLanguageMixin 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 con_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 σ) []
| LoadS l v σ :
σ.(heap) !! l = Some v →
head_step_rel (Load (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]> σ) []
| RandNoTapeS z N (n : fin (S N)) σ:
N = Z.to_nat z →
head_step_rel (Rand (Val $ LitV $ LitInt z) (Val $ LitV LitUnit)) σ (Val $ LitV $ LitInt n) σ []
| AllocTapeS z N σ l :
l = fresh_loc σ.(tapes) →
N = Z.to_nat z →
head_step_rel (AllocTape (Val (LitV (LitInt z)))) σ
(Val $ LitV $ LitLbl l) (state_upd_tapes <[l := (N; []) : tape]> σ) []
| RandTapeS l z N n ns σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((N; n :: ns) : tape) →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val (LitV (LitLbl l)))) σ
(Val $ LitV $ LitInt $ n) (state_upd_tapes <[l := (N; ns) : tape]> σ) []
| RandTapeEmptyS l z N (n : fin (S N)) σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((N; []) : tape) →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val $ LitV $ LitLbl l)) σ (Val $ LitV $ LitInt n) σ []
| RandTapeOtherS l z M N ms (n : fin (S N)) σ :
N = Z.to_nat z →
σ.(tapes) !! l = Some ((M; ms) : tape) →
N ≠ M →
head_step_rel (Rand (Val (LitV (LitInt z))) (Val $ LitV $ LitLbl l)) σ (Val $ LitV $ LitInt n) σ []
| TickS σ z :
head_step_rel (Tick $ Val $ LitV $ LitInt z) σ (Val $ LitV $ LitUnit) σ []
| ForkS e σ:
head_step_rel (Fork $ e) σ (Val $ LitV $ LitUnit) σ [e]
| CmpXchgS σ l vl v1 v2 b:
σ.(heap) !! l = Some vl ->
vals_compare_safe vl v1 ->
b = bool_decide (vl = v1) ->
head_step_rel (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ) []
| XchgS σ l v1 v2:
σ.(heap) !! l = Some v1 ->
head_step_rel (Xchg (Val $ LitV $ LitLoc l) (Val v2)) σ (Val v1) (state_upd_heap <[l:=v2]> σ) []
| FAAS σ l i1 i2:
σ.(heap) !! l = Some (LitV (LitInt i1)) ->
head_step_rel (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ (Val $ LitV $ LitInt i1)
(state_upd_heap <[l:= LitV (LitInt (i1+i2))]> σ) []
.
Create HintDb head_step.
Global Hint Constructors head_step_rel : head_step.
(* 0*)
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV LitUnit))) _ _ _ _) =>
eapply (RandNoTapeS _ _ 0%fin) : head_step.
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _ _) =>
eapply (RandTapeEmptyS _ _ _ 0%fin) : head_step.
Global Hint Extern 1
(head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _ _) =>
eapply (RandTapeOtherS _ _ _ _ _ 0%fin) : head_step.
Inductive state_step_rel : state → loc → state → Prop :=
| AddTapeS α N (n : fin (S N)) ns σ :
α ∈ dom σ.(tapes) →
σ.(tapes) !!! α = ((N; ns) : tape) →
state_step_rel σ α (state_upd_tapes <[α := (N; ns ++ [n]) : tape]> σ).
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 l :
head_step e1 σ1 (e2, σ2, l) > 0 ↔ head_step_rel e1 σ1 e2 σ2 l.
Proof.
split.
- intros ?. destruct e1; inv_head_step; eauto with head_step.
all: constructor; try done; by case_bool_decide.
- inversion 1; simplify_map_eq/=; try case_bool_decide; simplify_eq; solve_distr; done.
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; [|intros; inv_distr].
case_match. intros ?. inv_distr.
econstructor; eauto with lia.
- inversion_clear 1.
rewrite bool_decide_eq_true_2 // H1. solve_distr.
Qed.
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.
split; intros [[e2 σ2] Hs].
(* TODO: the sub goals used to be solved by simplify_map_eq *)
- destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)).
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H11. done.
* rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H11. done.
* rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq in H10. done.
* rewrite lookup_insert_ne // in H10. rewrite H10 in H7. done.
- destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)).
+ destruct (decide (α = l1)); simplify_eq.
* apply not_elem_of_dom_2 in H11. done.
* rewrite lookup_insert_ne // in H7. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq // in H7.
apply not_elem_of_dom_2 in H11. done.
* rewrite lookup_insert_ne // in H7. rewrite H11 in H7. done.
+ destruct (decide (α = l1)); simplify_eq.
* rewrite lookup_insert_eq // in H7.
apply not_elem_of_dom_2 in H10. done.
* rewrite lookup_insert_ne // in H7. rewrite H10 in H7. done.
Qed.
Lemma state_step_mass σ α :
α ∈ dom σ.(tapes) → SeriesC (state_step σ α) = 1.
Proof.
intros Hdom.
rewrite /state_step bool_decide_eq_true_2 //=.
case_match.
rewrite dmap_mass dunif_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;
repeat (simplify_map_eq/=; solve_distr_mass || case_match; try (case_bool_decide; done)).
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
| Load e => 1 + height e
| Store e1 e2 => 1 + height e1 + height e2
| AllocTape e => 1 + height e
| Rand e1 e2 => 1 + height e1 + height e2
| Tick e => 1 + height e
| Fork e => 1 + height e
| CmpXchg e0 e1 e2 => 1 + height e0 + height e1 + height e2
| Xchg e1 e2 => 1 + height e1 + height e2
| FAA e1 e2 => 1 + height e1 + height e2
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 σ.(tapes)).
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.
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 con_prob_lang_mixin :
ConEctxiLanguageMixin 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 con_prob_lang.
Language
Canonical Structure con_prob_ectxi_lang := ConEctxiLanguage con_prob_lang.get_active con_prob_lang.con_prob_lang_mixin.
Canonical Structure con_prob_ectx_lang := ConEctxLanguageOfEctxi con_prob_ectxi_lang.
Canonical Structure con_prob_lang := ConLanguageOfEctx con_prob_ectx_lang.
(* Prefer prob_lang names over ectx_language names. *)
Export con_prob_lang.
Definition cfg : Type := list expr * state.
Section sch_typeclasses.
Class TapeOblivious `{Countable sch_int_σ} (sch : scheduler (con_lang_mdp con_prob_lang) sch_int_σ) : Prop :=
tape_oblivious :
∀ ζ ρ ρ', ρ.1 = ρ'.1 -> heap ρ.2 = heap ρ'.2 -> sch (ζ, ρ) = sch (ζ, ρ')
.
Global Arguments TapeOblivious (_) {_ _} (_).
Lemma sch_tape_oblivious `{TapeOblivious si sch} ζ ρ ρ' :
ρ.1 = ρ'.1 -> heap ρ.2 = heap ρ'.2 -> sch (ζ, ρ) = sch (ζ, ρ').
Proof.
apply tape_oblivious.
Qed.
Lemma sch_tape_oblivious_state_upd_tapes `{TapeOblivious si sch} ζ α t σ es:
sch (ζ, (es, state_upd_tapes <[α:=t]> σ)) = sch (ζ, (es, σ)).
Proof.
apply sch_tape_oblivious; by simpl.
Qed.
(* non-stutter *)
Context `{Countable sch_int_σ}.
Context (sch: scheduler (con_lang_mdp con_prob_lang) sch_int_σ).
Fixpoint non_stutter_step' (n:nat) (p : sch_int_σ * cfg) {struct n} : distr (sch_int_σ * nat) :=
let '(sch_σ, ρ) := p in
match n with
| 0 => dzero
| S n' =>
dbind (λ '(sch_σ', tid),
if bool_decide (tid< length (ρ.1))%nat
then dret (sch_σ', tid)
else non_stutter_step' n' (sch_σ', ρ)
) (sch p)
end
.
Lemma non_stutter_step'_mono p n x:
(non_stutter_step' n p x <= non_stutter_step' (S n) p x)%R.
Proof.
revert p.
induction n; first (intros []; by rewrite dzero_0).
simpl. intros [].
rewrite {1 2}/dbind/dbind_pmf{1 4}/pmf.
apply SeriesC_le.
{ real_solver. }
apply pmf_ex_seriesC_mult_fn; exists 1.
intros []. simpl.
real_solver.
Qed.
Lemma non_stutter_step'_property n ζ ρ ζ' tid:
(0 < non_stutter_step' n (ζ, ρ) (ζ', tid))%R -> tid < length ρ.1.
Proof.
revert ζ ρ ζ' tid.
induction n; simpl.
- intros ????. rewrite dzero_0. lra.
- intros ???? H'. apply Rlt_gt in H'.
inv_distr.
case_match. subst.
case_bool_decide; first by inv_distr.
eapply IHn. by apply Rgt_lt.
Qed.
Definition non_stutter_step p :=
lim_distr (λ n, non_stutter_step' n p) (non_stutter_step'_mono p).
Lemma non_stutter_step_unfold a b :
non_stutter_step a b = Sup_seq (λ n, (non_stutter_step' n a) b).
Proof.
apply lim_distr_pmf.
Qed.
Lemma non_stutter_step_prefix ζ ρ:
non_stutter_step (ζ, ρ) =
dbind (λ '(ζ', tid),
if bool_decide (tid < length (ρ.1))
then dret (ζ', tid)
else non_stutter_step (ζ', ρ)) (sch (ζ, ρ)).
Proof.
apply distr_ext; intros v.
rewrite /dbind/dbind_pmf{2}/pmf.
symmetry.
erewrite (SeriesC_ext _
(λ a, Sup_seq (λ n, sch (ζ, ρ) a * if bool_decide (a.2<length ρ.1)%nat
then dret a v else
non_stutter_step' n (a.1, ρ) v
)))%R; last first.
{ intros [].
apply eq_rbar_finite.
rewrite rmult_finite.
erewrite Sup_seq_ext; last first.
- intros. by rewrite rmult_finite.
- rewrite Sup_seq_scal_l //.
f_equal.
case_bool_decide.
+ erewrite Sup_seq_ext; last first.
* intros. by rewrite bool_decide_eq_true_2.
* apply Rbar_le_antisym.
-- etrans; last apply (sup_is_upper_bound _ 0%nat).
done.
-- by apply upper_bound_ge_sup.
+ rewrite non_stutter_step_unfold.
rewrite rbar_finite_real_eq; last first.
* eapply (is_finite_bounded 0 1).
-- by apply Sup_seq_minor_le with 0%nat.
-- apply upper_bound_ge_sup. intros. by simpl.
* apply Sup_seq_ext.
intros. by rewrite bool_decide_eq_false_2.
}
apply (MCT_seriesC _ (λ n, non_stutter_step' (S n) (ζ, ρ) v)).
- real_solver.
- intros. apply Rmult_le_compat_l; first done.
case_bool_decide; first done.
apply non_stutter_step'_mono.
- intros [].
exists 1%R.
real_solver.
- intros.
simpl.
rewrite /dbind/dbind_pmf{4}/pmf.
erewrite SeriesC_ext; first apply SeriesC_correct.
+ apply pmf_ex_seriesC_mult_fn.
exists 1. intros [] => /=. real_solver.
+ intros []. simpl. f_equal.
by case_bool_decide.
- rewrite non_stutter_step_unfold.
rewrite mon_sup_succ.
+ rewrite (Rbar_le_sandwich 0 1).
* apply Sup_seq_correct.
* by apply (Sup_seq_minor_le _ _ 0%nat)=>/=.
* by apply upper_bound_ge_sup=>/=.
+ intro; apply non_stutter_step'_mono.
Qed.
Definition non_stutter_scheduler :=
Build_scheduler {|
scheduler_f := non_stutter_step : _* mdpstate (con_lang_mdp con_prob_lang) -> _
|}.
Lemma non_stutter_scheduler_tape_oblivious
{HTO:TapeOblivious _ sch} : TapeOblivious _ non_stutter_scheduler.
Proof.
rewrite /TapeOblivious in HTO *.
rewrite /non_stutter_scheduler/=.
intros ? [?[]][?[]]. simpl. intros -> ->.
apply distr_ext => v.
rewrite !non_stutter_step_unfold.
f_equal.
apply Sup_seq_ext.
intros n.
revert ζ.
induction n; first done.
intros ζ.
simpl.
rewrite {1 2}/dbind/dbind_pmf{1 4}/pmf.
f_equal.
apply SeriesC_ext.
intros [].
f_equal.
- f_equal. by apply HTO.
- case_bool_decide; first done.
naive_solver.
Qed.
Class NonStuttering `{Countable sch_int_σ} (sch : scheduler (con_lang_mdp con_prob_lang) sch_int_σ) : Prop :=
non_stuttering :
∀ ζ ρ ζ' tid, (sch (ζ, ρ) (ζ', tid) > 0)%R -> tid < length ρ.1.
Global Arguments NonStuttering {_ _} (_).
Lemma non_stutter_scheduler_non_stuttering : NonStuttering non_stutter_scheduler.
Proof.
rewrite /NonStuttering /non_stutter_scheduler/=.
intros ???? H1.
apply Rgt_lt in H1.
assert (Rbar_lt 0 (non_stutter_step (ζ, ρ) (ζ', tid))) as H2 by done.
rewrite non_stutter_step_unfold in H2.
rewrite rbar_finite_real_eq in H2; last first.
{ eapply (is_finite_bounded 0%R 1%R); first by eapply Sup_seq_minor_le with 0.
apply upper_bound_ge_sup. intros.
by rewrite rbar_le_rle.
}
rewrite Sup_seq_minor_lt in H2.
destruct H2 as [n H2].
simpl in H2.
by eapply non_stutter_step'_property.
Qed.
Lemma non_stutter_scheduler_same_semantics ζ ρ v:
(sch_lim_exec sch (ζ, ρ) v<= sch_lim_exec non_stutter_scheduler (ζ, ρ) v)%R.
Proof.
apply sch_lim_exec_leq.
intros n.
revert ρ ζ.
induction (lt_wf n) as [n _ IH1].
intros ρ ζ.
destruct (to_final ρ) eqn:Heqn.
{ erewrite sch_exec_is_final; last done. by erewrite sch_lim_exec_final. }
rewrite sch_lim_exec_not_final; last first.
{ rewrite /is_final. by rewrite Heqn. }
rewrite {2}/non_stutter_scheduler/sch_step/=.
revert ρ ζ Heqn.
induction (lt_wf n) as [n _ IH2].
intros ρ ζ Heqn.
destruct n.
{ rewrite sch_exec_O_not_final; last by rewrite /is_final Heqn.
by rewrite dzero_0. }
rewrite sch_exec_Sn_not_final; last first.
{ rewrite /is_final. by rewrite Heqn. }
rewrite non_stutter_step_prefix.
rewrite {1}/sch_step/=.
rewrite -!dbind_assoc'.
rewrite {1 3}/dbind/dbind_pmf{1 4}/pmf.
apply SeriesC_le; last first.
{ apply pmf_ex_seriesC_mult_fn. exists 1. naive_solver. }
intros []; split; first real_solver.
apply Rmult_le_compat_l; first done.
case_bool_decide as Hineq.
- rewrite dret_id_left/=.
rewrite -!dbind_assoc'.
rewrite {1 3}/dbind/dbind_pmf {1 4}/pmf.
apply SeriesC_le; last first.
{ apply pmf_ex_seriesC_mult_fn. exists 1. naive_solver. }
intros. split; first real_solver.
apply Rmult_le_compat_l; first done.
rewrite !dret_id_left.
apply IH1. lia.
- replace (con_lang_mdp_step _ _ ρ) with (dret ρ); last first.
{ rewrite /con_lang_mdp_step.
destruct ρ.
simpl in *.
case_match; simpl.
+ rewrite Heqn. rewrite lookup_ge_None_2; [done|lia].
+ rewrite lookup_ge_None_2; [done|lia].
}
rewrite dmap_dret dret_id_left.
etrans; first eapply IH2; first lia.
+ intros. eapply IH1. lia.
+ done.
+ by rewrite -dbind_assoc'.
Qed.
End sch_typeclasses.
Canonical Structure con_prob_ectx_lang := ConEctxLanguageOfEctxi con_prob_ectxi_lang.
Canonical Structure con_prob_lang := ConLanguageOfEctx con_prob_ectx_lang.
(* Prefer prob_lang names over ectx_language names. *)
Export con_prob_lang.
Definition cfg : Type := list expr * state.
Section sch_typeclasses.
Class TapeOblivious `{Countable sch_int_σ} (sch : scheduler (con_lang_mdp con_prob_lang) sch_int_σ) : Prop :=
tape_oblivious :
∀ ζ ρ ρ', ρ.1 = ρ'.1 -> heap ρ.2 = heap ρ'.2 -> sch (ζ, ρ) = sch (ζ, ρ')
.
Global Arguments TapeOblivious (_) {_ _} (_).
Lemma sch_tape_oblivious `{TapeOblivious si sch} ζ ρ ρ' :
ρ.1 = ρ'.1 -> heap ρ.2 = heap ρ'.2 -> sch (ζ, ρ) = sch (ζ, ρ').
Proof.
apply tape_oblivious.
Qed.
Lemma sch_tape_oblivious_state_upd_tapes `{TapeOblivious si sch} ζ α t σ es:
sch (ζ, (es, state_upd_tapes <[α:=t]> σ)) = sch (ζ, (es, σ)).
Proof.
apply sch_tape_oblivious; by simpl.
Qed.
(* non-stutter *)
Context `{Countable sch_int_σ}.
Context (sch: scheduler (con_lang_mdp con_prob_lang) sch_int_σ).
Fixpoint non_stutter_step' (n:nat) (p : sch_int_σ * cfg) {struct n} : distr (sch_int_σ * nat) :=
let '(sch_σ, ρ) := p in
match n with
| 0 => dzero
| S n' =>
dbind (λ '(sch_σ', tid),
if bool_decide (tid< length (ρ.1))%nat
then dret (sch_σ', tid)
else non_stutter_step' n' (sch_σ', ρ)
) (sch p)
end
.
Lemma non_stutter_step'_mono p n x:
(non_stutter_step' n p x <= non_stutter_step' (S n) p x)%R.
Proof.
revert p.
induction n; first (intros []; by rewrite dzero_0).
simpl. intros [].
rewrite {1 2}/dbind/dbind_pmf{1 4}/pmf.
apply SeriesC_le.
{ real_solver. }
apply pmf_ex_seriesC_mult_fn; exists 1.
intros []. simpl.
real_solver.
Qed.
Lemma non_stutter_step'_property n ζ ρ ζ' tid:
(0 < non_stutter_step' n (ζ, ρ) (ζ', tid))%R -> tid < length ρ.1.
Proof.
revert ζ ρ ζ' tid.
induction n; simpl.
- intros ????. rewrite dzero_0. lra.
- intros ???? H'. apply Rlt_gt in H'.
inv_distr.
case_match. subst.
case_bool_decide; first by inv_distr.
eapply IHn. by apply Rgt_lt.
Qed.
Definition non_stutter_step p :=
lim_distr (λ n, non_stutter_step' n p) (non_stutter_step'_mono p).
Lemma non_stutter_step_unfold a b :
non_stutter_step a b = Sup_seq (λ n, (non_stutter_step' n a) b).
Proof.
apply lim_distr_pmf.
Qed.
Lemma non_stutter_step_prefix ζ ρ:
non_stutter_step (ζ, ρ) =
dbind (λ '(ζ', tid),
if bool_decide (tid < length (ρ.1))
then dret (ζ', tid)
else non_stutter_step (ζ', ρ)) (sch (ζ, ρ)).
Proof.
apply distr_ext; intros v.
rewrite /dbind/dbind_pmf{2}/pmf.
symmetry.
erewrite (SeriesC_ext _
(λ a, Sup_seq (λ n, sch (ζ, ρ) a * if bool_decide (a.2<length ρ.1)%nat
then dret a v else
non_stutter_step' n (a.1, ρ) v
)))%R; last first.
{ intros [].
apply eq_rbar_finite.
rewrite rmult_finite.
erewrite Sup_seq_ext; last first.
- intros. by rewrite rmult_finite.
- rewrite Sup_seq_scal_l //.
f_equal.
case_bool_decide.
+ erewrite Sup_seq_ext; last first.
* intros. by rewrite bool_decide_eq_true_2.
* apply Rbar_le_antisym.
-- etrans; last apply (sup_is_upper_bound _ 0%nat).
done.
-- by apply upper_bound_ge_sup.
+ rewrite non_stutter_step_unfold.
rewrite rbar_finite_real_eq; last first.
* eapply (is_finite_bounded 0 1).
-- by apply Sup_seq_minor_le with 0%nat.
-- apply upper_bound_ge_sup. intros. by simpl.
* apply Sup_seq_ext.
intros. by rewrite bool_decide_eq_false_2.
}
apply (MCT_seriesC _ (λ n, non_stutter_step' (S n) (ζ, ρ) v)).
- real_solver.
- intros. apply Rmult_le_compat_l; first done.
case_bool_decide; first done.
apply non_stutter_step'_mono.
- intros [].
exists 1%R.
real_solver.
- intros.
simpl.
rewrite /dbind/dbind_pmf{4}/pmf.
erewrite SeriesC_ext; first apply SeriesC_correct.
+ apply pmf_ex_seriesC_mult_fn.
exists 1. intros [] => /=. real_solver.
+ intros []. simpl. f_equal.
by case_bool_decide.
- rewrite non_stutter_step_unfold.
rewrite mon_sup_succ.
+ rewrite (Rbar_le_sandwich 0 1).
* apply Sup_seq_correct.
* by apply (Sup_seq_minor_le _ _ 0%nat)=>/=.
* by apply upper_bound_ge_sup=>/=.
+ intro; apply non_stutter_step'_mono.
Qed.
Definition non_stutter_scheduler :=
Build_scheduler {|
scheduler_f := non_stutter_step : _* mdpstate (con_lang_mdp con_prob_lang) -> _
|}.
Lemma non_stutter_scheduler_tape_oblivious
{HTO:TapeOblivious _ sch} : TapeOblivious _ non_stutter_scheduler.
Proof.
rewrite /TapeOblivious in HTO *.
rewrite /non_stutter_scheduler/=.
intros ? [?[]][?[]]. simpl. intros -> ->.
apply distr_ext => v.
rewrite !non_stutter_step_unfold.
f_equal.
apply Sup_seq_ext.
intros n.
revert ζ.
induction n; first done.
intros ζ.
simpl.
rewrite {1 2}/dbind/dbind_pmf{1 4}/pmf.
f_equal.
apply SeriesC_ext.
intros [].
f_equal.
- f_equal. by apply HTO.
- case_bool_decide; first done.
naive_solver.
Qed.
Class NonStuttering `{Countable sch_int_σ} (sch : scheduler (con_lang_mdp con_prob_lang) sch_int_σ) : Prop :=
non_stuttering :
∀ ζ ρ ζ' tid, (sch (ζ, ρ) (ζ', tid) > 0)%R -> tid < length ρ.1.
Global Arguments NonStuttering {_ _} (_).
Lemma non_stutter_scheduler_non_stuttering : NonStuttering non_stutter_scheduler.
Proof.
rewrite /NonStuttering /non_stutter_scheduler/=.
intros ???? H1.
apply Rgt_lt in H1.
assert (Rbar_lt 0 (non_stutter_step (ζ, ρ) (ζ', tid))) as H2 by done.
rewrite non_stutter_step_unfold in H2.
rewrite rbar_finite_real_eq in H2; last first.
{ eapply (is_finite_bounded 0%R 1%R); first by eapply Sup_seq_minor_le with 0.
apply upper_bound_ge_sup. intros.
by rewrite rbar_le_rle.
}
rewrite Sup_seq_minor_lt in H2.
destruct H2 as [n H2].
simpl in H2.
by eapply non_stutter_step'_property.
Qed.
Lemma non_stutter_scheduler_same_semantics ζ ρ v:
(sch_lim_exec sch (ζ, ρ) v<= sch_lim_exec non_stutter_scheduler (ζ, ρ) v)%R.
Proof.
apply sch_lim_exec_leq.
intros n.
revert ρ ζ.
induction (lt_wf n) as [n _ IH1].
intros ρ ζ.
destruct (to_final ρ) eqn:Heqn.
{ erewrite sch_exec_is_final; last done. by erewrite sch_lim_exec_final. }
rewrite sch_lim_exec_not_final; last first.
{ rewrite /is_final. by rewrite Heqn. }
rewrite {2}/non_stutter_scheduler/sch_step/=.
revert ρ ζ Heqn.
induction (lt_wf n) as [n _ IH2].
intros ρ ζ Heqn.
destruct n.
{ rewrite sch_exec_O_not_final; last by rewrite /is_final Heqn.
by rewrite dzero_0. }
rewrite sch_exec_Sn_not_final; last first.
{ rewrite /is_final. by rewrite Heqn. }
rewrite non_stutter_step_prefix.
rewrite {1}/sch_step/=.
rewrite -!dbind_assoc'.
rewrite {1 3}/dbind/dbind_pmf{1 4}/pmf.
apply SeriesC_le; last first.
{ apply pmf_ex_seriesC_mult_fn. exists 1. naive_solver. }
intros []; split; first real_solver.
apply Rmult_le_compat_l; first done.
case_bool_decide as Hineq.
- rewrite dret_id_left/=.
rewrite -!dbind_assoc'.
rewrite {1 3}/dbind/dbind_pmf {1 4}/pmf.
apply SeriesC_le; last first.
{ apply pmf_ex_seriesC_mult_fn. exists 1. naive_solver. }
intros. split; first real_solver.
apply Rmult_le_compat_l; first done.
rewrite !dret_id_left.
apply IH1. lia.
- replace (con_lang_mdp_step _ _ ρ) with (dret ρ); last first.
{ rewrite /con_lang_mdp_step.
destruct ρ.
simpl in *.
case_match; simpl.
+ rewrite Heqn. rewrite lookup_ge_None_2; [done|lia].
+ rewrite lookup_ge_None_2; [done|lia].
}
rewrite dmap_dret dret_id_left.
etrans; first eapply IH2; first lia.
+ intros. eapply IH1. lia.
+ done.
+ by rewrite -dbind_assoc'.
Qed.
End sch_typeclasses.