Library iris.heap_lang.lang

From stdpp Require Export binders strings.
From stdpp Require Import gmap.
From iris.algebra Require Export ofe.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
Set Default Proof Using "Type".

heap_lang. A fairly simple language used for common Iris examples.
  • This is a right-to-left evaluated language, like CakeML and OCaml. The reason for this is that it makes curried functions usable: Given a WP for f a b, we know that any effects f might have to not matter until after *both* a and b are evaluated. With left-to-right evaluation, that triple is basically useless unless the user let-expands b.
  • For prophecy variables, we annotate the reduction steps with an "observation" and tweak adequacy such that WP knows all future observations. There is another possible choice: Use non-deterministic choice when creating a prophecy variable (NewProph), and when resolving it (Resolve) make the program diverge unless the variable matches. That, however, requires an erasure proof that this endless loop does not make specifications useless.
The expression Resolve e p v attaches a prophecy resolution (for prophecy variable p to value v) to the top-level head-reduction step of e. The prophecy resolution happens simultaneously with the head-step being taken. Furthermore, it is required that the head-step produces a value (otherwise the Resolve is stuck), and this value is also attached to the resolution. A prophecy variable is thus resolved to a pair containing (1) the result value of the wrapped expression (called e above), and (2) the value that was attached by the Resolve (called v above). This allows, for example, to distinguish a resolution originating from a successful CmpXchg from one originating from a failing CmpXchg. For example:
  • Resolve (CmpXchg #l #n #(n+1)) #p v will behave as CmpXchg #l #n #(n+1), which means step to a value-boole pair (n', b) while updating the heap, but in the meantime the prophecy variable p will be resolved to (n', b), v).
  • Resolve (! #l) #p v will behave as ! #l, that is return the value w pointed to by l on the heap (assuming it was allocated properly), but it will additionally resolve p to the pair (w,v).
Note that the sub-expressions of Resolve e p v (i.e., e, p and v) are reduced as usual, from right to left. However, the evaluation of e is restricted so that the head-step to which the resolution is attached cannot be taken by the context. For example:
  • Resolve (CmpXchg #l #n (#n + #1)) #p v will first be reduced (with by a context-step) to Resolve (CmpXchg #l #n #(n+1) #p v, and then behave as described above.
  • However, Resolve ((λ: "n", CmpXchg #l "n" ("n" + #1)) #n) #p v is stuck. Indeed, it can only be evaluated using a head-step (it is a β-redex), but the process does not yield a value.
The mechanism described above supports nesting Resolve expressions to attach several prophecy resolutions to a head-redex.

Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

Module heap_lang.
Open Scope Z_scope.

Expressions and vals.
Definition proph_id := positive.

We have a notion of "poison" as a variant of unit that may not be compared with anything. This is useful for erasure proofs: if we erased things to unit, <erased> == unit would evaluate to true after erasure, changing program behavior. So we erase to the poison value instead, making sure that no legal comparisons could be affected.
Inductive base_lit : Set :=
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison
  | LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set :=
  | NegOp | MinusUnOp.
Inductive bin_op : Set :=
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp
  | AndOp | OrOp | XorOp
  | ShiftLOp | ShiftROp
  | LeOp | LtOp | EqOp
  | OffsetOp.
Inductive expr :=
  
  | Val (v : val)
  
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
  
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
  
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
  
  | Fork (e : expr)
  
  | AllocN (e1 e2 : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr)
  
  | NewProph
  | Resolve (e0 : expr) (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.

An observation associates a prophecy variable (identifier) to a pair of values. The first value is the one that was returned by the (atomic) operation during which the prophecy resolution happened (typically, a boolean when the wrapped operation is a CmpXchg). The second value is the one that the prophecy variable was actually resolved to.
Definition observation : Set := proph_id × (val × val).

Notation of_val := Val (only parsing).

Definition to_val (e : expr) : option val :=
  match e with
  | Val vSome 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.
Definition lit_is_unboxed (l: base_lit) : Prop :=
  match l with
  
Disallow comparing (erased) prophecies with (erased) prophecies, by considering them boxed.
  | LitProphecy _ | LitPoisonFalse
  | _True
  end.
Definition val_is_unboxed (v : val) : Prop :=
  match v with
  | LitV llit_is_unboxed l
  | InjLV (LitV l) ⇒ lit_is_unboxed l
  | InjRV (LitV l) ⇒ lit_is_unboxed l
  | _False
  end.

Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
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.
Arguments vals_compare_safe !_ !_ /.

The state: heaps of vals.
Record state : Type := {
  heap: gmap loc val;
  used_proph_id: gset proph_id;
}.

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.

Instance of_val_inj : Inj (=) (=) of_val.
Proof. intros ??. congruence. Qed.

Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
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'))
     | Fork e, Fork e'cast_if (decide (e = e'))
     | 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'))
     | CmpXchg e0 e1 e2, CmpXchg e0' e1' e2'
        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
     | FAA e1 e2, FAA e1' e2'
        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
     | NewProph, NewProphleft _
     | Resolve e0 e1 e2, Resolve e0' e1' e2'
        cast_if_and3 (decide (e0 = e0')) (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.
Instance val_eq_dec : EqDecision val.
Proof. solve_decision. Defined.

Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
  | LitInt n(inl (inl n), None)
  | LitBool b(inl (inr b), None)
  | LitUnit(inr (inl false), None)
  | LitPoison(inr (inl true), None)
  | LitLoc l(inr (inr l), None)
  | LitProphecy p(inr (inl false), Some p)
  end) (λ l, match l with
  | (inl (inl n), None)LitInt n
  | (inl (inr b), None)LitBool b
  | (inr (inl false), None)LitUnit
  | (inr (inl true), None)LitPoison
  | (inr (inr l), None)LitLoc l
  | (_, Some p)LitProphecy p
  end) _); by intros [].
Qed.
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.
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.
Instance expr_countable : Countable expr.
Proof.
 set (enc :=
   fix go e :=
     match e with
     | Val vGenNode 0 [gov v]
     | Var xGenLeaf (inl (inl x))
     | Rec f x eGenNode 1 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
     | App e1 e2GenNode 2 [go e1; go e2]
     | UnOp op eGenNode 3 [GenLeaf (inr (inr (inl op))); go e]
     | BinOp op e1 e2GenNode 4 [GenLeaf (inr (inr (inr op))); go e1; go e2]
     | If e0 e1 e2GenNode 5 [go e0; go e1; go e2]
     | Pair e1 e2GenNode 6 [go e1; go e2]
     | Fst eGenNode 7 [go e]
     | Snd eGenNode 8 [go e]
     | InjL eGenNode 9 [go e]
     | InjR eGenNode 10 [go e]
     | Case e0 e1 e2GenNode 11 [go e0; go e1; go e2]
     | Fork eGenNode 12 [go e]
     | AllocN e1 e2GenNode 13 [go e1; go e2]
     | Load eGenNode 14 [go e]
     | Store e1 e2GenNode 15 [go e1; go e2]
     | CmpXchg e0 e1 e2GenNode 16 [go e0; go e1; go e2]
     | FAA e1 e2GenNode 17 [go e1; go e2]
     | NewProphGenNode 18 []
     | Resolve e0 e1 e2GenNode 19 [go e0; go e1; go e2]
     end
   with gov v :=
     match v with
     | LitV lGenLeaf (inr (inl l))
     | RecV f x e
        GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
     | PairV v1 v2GenNode 1 [gov v1; gov v2]
     | InjLV vGenNode 2 [gov v]
     | InjRV vGenNode 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 [e]Fork (go e)
     | GenNode 13 [e1; e2]AllocN (go e1) (go e2)
     | GenNode 14 [e]Load (go e)
     | GenNode 15 [e1; e2]Store (go e1) (go e2)
     | GenNode 16 [e0; e1; e2]CmpXchg (go e0) (go e1) (go e2)
     | GenNode 17 [e1; e2]FAA (go e1) (go e2)
     | GenNode 18 []NewProph
     | GenNode 19 [e0; e1; e2]Resolve (go e0) (go e1) (go e2)
     | _Val $ LitV LitUnit
     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
     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.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

Instance state_inhabited : Inhabited state :=
  populate {| heap := inhabitant; used_proph_id := inhabitant |}.
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
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)
  | CmpXchgLCtx (v1 : val) (v2 : val)
  | CmpXchgMCtx (e0 : expr) (v2 : val)
  | CmpXchgRCtx (e0 : expr) (e1 : expr)
  | FaaLCtx (v2 : val)
  | FaaRCtx (e1 : expr)
  | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
  | ResolveMCtx (e0 : expr) (v2 : val)
  | ResolveRCtx (e0 : expr) (e1 : expr).

Contextual closure will only reduce e in Resolve e (Val _) (Val _) if the local context of e is non-empty. As a consequence, the first argument of Resolve is not completely evaluated (down to a value) by contextual closure: no head steps (i.e., surface reductions) are taken. This means that contextual closure will reduce Resolve (CmpXchg #l #n (#n + #1)) #p #v into Resolve (CmpXchg #l #n #(n+1)) #p #v, but it cannot context-step any further.

Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
  match Ki with
  | AppLCtx v2App e (of_val v2)
  | AppRCtx e1App e1 e
  | UnOpCtx opUnOp op e
  | BinOpLCtx op v2BinOp op e (Val v2)
  | BinOpRCtx op e1BinOp op e1 e
  | IfCtx e1 e2If e e1 e2
  | PairLCtx v2Pair e (Val v2)
  | PairRCtx e1Pair e1 e
  | FstCtxFst e
  | SndCtxSnd e
  | InjLCtxInjL e
  | InjRCtxInjR e
  | CaseCtx e1 e2Case e e1 e2
  | AllocNLCtx v2AllocN e (Val v2)
  | AllocNRCtx e1AllocN e1 e
  | LoadCtxLoad e
  | StoreLCtx v2Store e (Val v2)
  | StoreRCtx e1Store e1 e
  | CmpXchgLCtx v1 v2CmpXchg e (Val v1) (Val v2)
  | CmpXchgMCtx e0 v2CmpXchg e0 e (Val v2)
  | CmpXchgRCtx e0 e1CmpXchg e0 e1 e
  | FaaLCtx v2FAA e (Val v2)
  | FaaRCtx e1FAA e1 e
  | ResolveLCtx K v1 v2Resolve (fill_item K e) (Val v1) (Val v2)
  | ResolveMCtx ex v2Resolve ex e (Val v2)
  | ResolveRCtx ex e1Resolve ex e1 e
  end.

Substitution
Fixpoint subst (x : string) (v : val) (e : expr) : expr :=
  match e with
  | Val _e
  | Var yif 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 e2App (subst x v e1) (subst x v e2)
  | UnOp op eUnOp op (subst x v e)
  | BinOp op e1 e2BinOp op (subst x v e1) (subst x v e2)
  | If e0 e1 e2If (subst x v e0) (subst x v e1) (subst x v e2)
  | Pair e1 e2Pair (subst x v e1) (subst x v e2)
  | Fst eFst (subst x v e)
  | Snd eSnd (subst x v e)
  | InjL eInjL (subst x v e)
  | InjR eInjR (subst x v e)
  | Case e0 e1 e2Case (subst x v e0) (subst x v e1) (subst x v e2)
  | Fork eFork (subst x v e)
  | AllocN e1 e2AllocN (subst x v e1) (subst x v e2)
  | Load eLoad (subst x v e)
  | Store e1 e2Store (subst x v e1) (subst x v e2)
  | CmpXchg e0 e1 e2CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
  | FAA e1 e2FAA (subst x v e1) (subst x v e2)
  | NewProphNewProph
  | Resolve ex e1 e2Resolve (subst x v ex) (subst x v e1) (subst x v e2)
  end.

Definition subst' (mx : binder) (v : val) : expr expr :=
  match mx with BNamed xsubst x v | BAnonid 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 n) ⇒ Some $ LitV $ LitInt (Z.lnot n)
  | MinusUnOp, LitV (LitInt n) ⇒ Some $ LitV $ LitInt (- n)
  | _, _None
  end.

Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
  match op with
  | PlusOpSome $ LitInt (n1 + n2)
  | MinusOpSome $ LitInt (n1 - n2)
  | MultOpSome $ LitInt (n1 × n2)
  | QuotOpSome $ LitInt (n1 `quot` n2)
  | RemOpSome $ LitInt (n1 `rem` n2)
  | AndOpSome $ LitInt (Z.land n1 n2)
  | OrOpSome $ LitInt (Z.lor n1 n2)
  | XorOpSome $ LitInt (Z.lxor n1 n2)
  | ShiftLOpSome $ LitInt (n1 n2)
  | ShiftROpSome $ LitInt (n1 n2)
  | LeOpSome $ LitBool (bool_decide (n1 n2))
  | LtOpSome $ LitBool (bool_decide (n1 < n2))
  | EqOpSome $ LitBool (bool_decide (n1 = n2))
  | OffsetOpNone
  end.

Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
  match op with
  | PlusOp | MinusOp | MultOp | QuotOp | RemOpNone
  | AndOpSome (LitBool (b1 && b2))
  | OrOpSome (LitBool (b1 || b2))
  | XorOpSome (LitBool (xorb b1 b2))
  | ShiftLOp | ShiftROpNone
  | LeOp | LtOpNone
  | EqOpSome (LitBool (bool_decide (b1 = b2)))
  | OffsetOpNone
  end.

Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
  match op, v2 with
  | OffsetOp, LitInt offSome $ LitLoc (l1 +ₗ off)
  | _, _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) ⇒ 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 v2LitV <$> 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); used_proph_id := σ.(used_proph_id) |}.
Arguments state_upd_heap _ !_ /.

Definition state_upd_used_proph_id (f: gset proph_id gset proph_id) (σ: state) : state :=
  {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
Arguments state_upd_used_proph_id _ !_ /.

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_lookup l vs w k :
  heap_array l vs !! k = Some w
   j, 0 j k = l +ₗ j vs !! (Z.to_nat j) = Some w.
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 & ? & → & ?)].
    { 0. rewrite loc_add_0. naive_solver lia. }
     (1 + j). 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 _); 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.
     (j - 1). 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) (i < length vs) h !! (l +ₗ i) = None)
  (heap_array l vs) ##ₘ h.
Proof.
  intros Hdisj. apply map_disjoint_specl' v1 v2.
  intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
  move: Hj. rewrite Z2Nat.id // ⇒ ?. by rewrite Hdisj.
Qed.

Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
  state_upd_heap (λ h, heap_array l (replicate (Z.to_nat n) v) h) σ.

Lemma state_init_heap_singleton l v σ :
  state_init_heap l 1 v σ = state_upd_heap <[l:=v]> σ.
Proof.
  destruct σ as [h p]. rewrite /state_init_heap /=. f_equiv.
  rewrite right_id insert_union_singleton_l. done.
Qed.

Inductive head_step : expr state list observation expr state list expr Prop :=
  | RecS f x e σ :
     head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
  | PairS v1 v2 σ :
     head_step (Pair (Val v1) (Val v2)) σ [] (Val $ PairV v1 v2) σ []
  | InjLS v σ :
     head_step (InjL $ Val v) σ [] (Val $ InjLV v) σ []
  | InjRS v σ :
     head_step (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 (App (Val $ RecV f x e1) (Val v2)) σ [] e' σ []
  | UnOpS op v v' σ :
     un_op_eval op v = Some v'
     head_step (UnOp op (Val v)) σ [] (Val v') σ []
  | BinOpS op v1 v2 v' σ :
     bin_op_eval op v1 v2 = Some v'
     head_step (BinOp op (Val v1) (Val v2)) σ [] (Val v') σ []
  | IfTrueS e1 e2 σ :
     head_step (If (Val $ LitV $ LitBool true) e1 e2) σ [] e1 σ []
  | IfFalseS e1 e2 σ :
     head_step (If (Val $ LitV $ LitBool false) e1 e2) σ [] e2 σ []
  | FstS v1 v2 σ :
     head_step (Fst (Val $ PairV v1 v2)) σ [] (Val v1) σ []
  | SndS v1 v2 σ :
     head_step (Snd (Val $ PairV v1 v2)) σ [] (Val v2) σ []
  | CaseLS v e1 e2 σ :
     head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
  | CaseRS v e1 e2 σ :
     head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
  | ForkS e σ:
     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
  | AllocNS n v σ l :
     0 < n
     ( i, 0 i i < n σ.(heap) !! (l +ₗ i) = None)
     head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
               []
               (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
               []
  | LoadS l v σ :
     σ.(heap) !! l = Some v
     head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
  | StoreS l v σ :
     is_Some (σ.(heap) !! l)
     head_step (Store (Val $ LitV $ LitLoc l) (Val v)) σ
               []
               (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
               []
  | CmpXchgS l v1 v2 vl σ b :
     σ.(heap) !! l = Some vl
     
     vals_compare_safe vl v1
     b = bool_decide (vl = v1)
     head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
               []
               (Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
               []
  | FaaS l i1 i2 σ :
     σ.(heap) !! l = Some (LitV (LitInt i1))
     head_step (FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2)) σ
               []
               (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]>σ)
               []
  | NewProphS σ p :
     p σ.(used_proph_id)
     head_step NewProph σ
               []
               (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪.) σ)
               []
  | ResolveS p v e σ w σ' κs ts :
     head_step e σ κs (Val v) σ' ts
     head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
               (κs ++ [(p, (v, w))]) (Val v) σ' ts.

Basic properties about the language
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 e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.

Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
  head_step (fill_item Ki e) σ1 κ e2 σ2 efs is_Some (to_val e).
Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto. 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. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.

Lemma alloc_fresh v n σ :
  let l := fresh_locs (dom (gset loc) σ.(heap)) in
  0 < n
  head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
            (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
Proof.
  intros.
  apply AllocNS; first done.
  intros. apply (not_elem_of_dom (D := gset loc)).
  by apply fresh_locs_fresh.
Qed.

Lemma new_proph_id_fresh σ :
  let p := fresh σ.(used_proph_id) in
  head_step NewProph σ [] (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪.) σ) [].
Proof. constructor. apply is_fresh. Qed.

Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
    fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
End heap_lang.

Language
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.

Export heap_lang.

The following lemma is not provable using the axioms of ectxi_language. The proof requires a case analysis over context items (destruct i on the last line), which in all cases yields a non-value. To prove this lemma for ectxi_language in general, we would require that a term of the form fill_item i e is never a value.
Lemma to_val_fill_some K e v : to_val (fill K e) = Some v K = [] e = Val v.
Proof.
  intro H. destruct K as [|Ki K]; first by apply of_to_val in H. exfalso.
  assert (to_val e None) as He.
  { intro A. by rewrite fill_not_val in H. }
  assert ( w, e = Val w) as [w ->].
  { destruct e; try done; eauto. }
  assert (to_val (fill (Ki :: K) (Val w)) = None).
  { destruct Ki; simpl; apply fill_not_val; done. }
  by simplify_eq.
Qed.

Lemma prim_step_to_val_is_head_step e σ1 κs w σ2 efs :
  prim_step e σ1 κs (Val w) σ2 efs head_step e σ1 κs (Val w) σ2 efs.
Proof.
  intro H. destruct H as [K e1 e2 H1 H2].
  assert (to_val (fill K e2) = Some w) as H3; first by rewrite -H2.
  apply to_val_fill_some in H3 as [-> ->]. subst e. done.
Qed.

If e1 makes a head step to a value under some state σ1 then any head step from e1 under any other state σ1' must necessarily be to a value.
Lemma head_step_to_val e1 σ1 κ e2 σ2 efs σ1' κ' e2' σ2' efs' :
  head_step e1 σ1 κ e2 σ2 efs
  head_step e1 σ1' κ' e2' σ2' efs' is_Some (to_val e2) is_Some (to_val e2').
Proof. destruct 1; inversion 1; naive_solver. Qed.

Lemma irreducible_resolve e v1 v2 σ :
  irreducible e σ irreducible (Resolve e (Val v1) (Val v2)) σ.
Proof.
  intros H κs ** [Ks e1' e2' Hfillstep]. simpl in ×.
  induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
  - subst e1'. inversion step. eapply H. by apply head_prim_step.
  - rewrite fill_app /= in Hfill.
    destruct K; (inversion Hfill; subst; clear Hfill; try
      match goal with | H : Val ?v = fill Ks ?e |- _
        (assert (to_val (fill Ks e) = Some v) as HEq by rewrite -H //);
        apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
      end).
    apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs).
    econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
Qed.