moved ra coq files out of iris repo

coq/_CoqProject

+-Q . ra
+lang.v
+lifting.v
+inv.v

coq/lifting.v

+From iris.program_logic Require Export ectx_weakestpre.
+From iris.program_logic Require Import ownership. (* for ownP *)
+From ra Require Export lang.
+(* From iris.heap_lang Require Import tactics. *)
+From iris.proofmode Require Import weakestpre.
+Import uPred.
+(* Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2. *)
+
+Section lifting.
+Context {Σ : iFunctor}.
+Implicit Types P Q : iProp ra_lang Σ.
+Implicit Types Φ : val → iProp ra_lang Σ.
+Implicit Types ef : option (expr []).
+
+(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
+Lemma wp_bind {E e} K Φ :
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Proof. exact: wp_ectx_bind. Qed.
+
+Lemma wp_bindi {E e} Ki Φ :
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ E {{ Φ }}.
+Proof. exact: weakestpre.wp_bind. Qed.
+
+(** Base axioms for core primitives of the language: Stateful reductions. *)
+Lemma wp_alloc_pst E σ π e (v : raval) bπ Φ :
+  e = Lit (LitInt v) →
+  sbuf σ !! π = Some bπ →
+  (▷ ownP σ ★ ▷ (∀ l ts, stime σ !! l = None ∧
+                      ownP ({| sbuf := <[π := (mkevent l v ts) :: bπ]>(sbuf σ);
+                                      sind := sind σ;
+                                      stime := <[l := {[ts]}]>(stime σ) |})
+                      -★ Φ (LocV l, π)))
+  ⊢ WP (Alloc e,π) @ E {{ Φ }}.
+Proof.
+  iIntros {? ?}  "[HP HΦ]".
+  (* TODO: This works around ssreflect bug #22. *)
+  set (φ (e' : expr []) σ' ef := ∃ l ts,
+    ef = None ∧ e' = (Loc l, π) ∧ σ' = {| sbuf := <[π := (mkevent l v ts) :: bπ]>(sbuf σ);
+                                      sind := sind σ;
+                                      stime := <[l := {[ts]}]>(stime σ) |} ∧ stime σ !! l = None).
+  iApply (wp_lift_atomic_head_step (Alloc e,π) φ σ); try (by simpl; eauto).
+  - by rewrite H.
+  - econstructor. eexists. exists None. constructor. econstructor => [//|].
+    econstructor => [//| |//]. instantiate (1 := fresh (dom _ (stime σ))).
+    by apply (not_elem_of_dom (D:=gset _)), is_fresh.
+  - move => ? ? ?. inversion 1; subst; first by inversion HStep.
+    inversion_clear HStep; subst. inversion_clear HAct; subst.
+    exists l, 1%positive. by naive_solver.
+  iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
+  (* FIXME: I should not have to refer to "H0". *)
+  destruct H1 as (l & ? & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
+  iSplit; last done. iApply "HΦ"; by iSplit.
+Qed.