1 files changed, 143 insertions, 0 deletions

diff --git a/theories/nix/wp.v b/theories/nix/wp.v
new file mode 100644
index 0000000..0eca6e1
--- /dev/null
+++ b/theories/nix/wp.v
@@ -0,0 +1,143 @@
+From mininix Require Export nix.operational_props.
+From stdpp Require Import options.
+
+Definition wp (μ : mode) (e : expr) (Φ : expr → Prop) : Prop :=
+  ∃ e', e -{μ}->* e' ∧ final μ e' ∧ Φ e'.
+
+Lemma Lit_wp μ Φ bl :
+  base_lit_ok bl →
+  Φ (ELit bl) →
+  wp μ (ELit bl) Φ.
+Proof. exists (ELit bl). by repeat constructor. Qed.
+
+Lemma Abs_wp μ Φ x e :
+  Φ (EAbs x e) →
+  wp μ (EAbs x e) Φ.
+Proof. exists (EAbs x e). by repeat constructor. Qed.
+
+Lemma AbsMatch_wp μ Φ ms strict e :
+  Φ (EAbsMatch ms strict e) →
+  wp μ (EAbsMatch ms strict e) Φ.
+Proof. exists (EAbsMatch ms strict e). by repeat constructor. Qed.
+
+Lemma LetAttr_no_recs_wp μ Φ k αs e :
+  no_recs αs →
+  wp μ (subst ((k,.) ∘ attr_expr <$> αs) e) Φ →
+  wp μ (ELetAttr k (EAttr αs) e) Φ.
+Proof.
+  intros Hαs (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
+  etrans; [|apply Hsteps]. apply rtc_once. by constructor.
+Qed.
+
+Lemma BinOp_wp μ Φ op e1 e2 :
+  wp SHALLOW e1 (λ e1', ∃ Φop,
+    sem_bin_op op e1' Φop ∧ 
+    wp SHALLOW e2 (λ e2', ∃ e', Φop e2' e' ∧ wp μ e' Φ)) →
+  wp μ (EBinOp op e1 e2) Φ.
+Proof.
+  intros (e1' & Hsteps1 & ? & Φop & Hop1 & e2' & Hsteps2 & ?
+          & e' & Hop2 & e'' & Hsteps & ? & HΦ).
+  exists e''. split; [|done].
+  etrans; [by apply SBinOpL_rtc|].
+  etrans; [by eapply SBinOpR_rtc|].
+  eapply rtc_l; [by econstructor|]. done.
+Qed.
+
+Lemma Id_wp μ Φ x k e :
+  wp μ e Φ →
+  wp μ (EId x (Some (k,e))) Φ.
+Proof.
+  intros (e' & Hsteps & ? & HΦ). exists e'. split; [|done].
+  etrans; [|apply Hsteps]. apply rtc_once. constructor.
+Qed.
+
+Lemma App_wp μ Φ e1 e2 :
+  wp SHALLOW e1 (λ e1', wp μ (EApp e1' e2) Φ) ↔
+  wp μ (EApp e1 e2) Φ.
+Proof.
+  split.
+  - intros (e1' & Hsteps1 & ? & e' & Hsteps2 & ? & HΦ).
+    exists e'; split; [|done]. etrans; [|apply Hsteps2].
+    by apply SAppL_rtc.
+  - intros (e' & Hsteps & Hfinal & HΦ).
+    cut (∃ e1', e1 -{SHALLOW}->* e1' ∧ final SHALLOW e1' ∧ EApp e1' e2 -{μ}->* e').
+    { intros (e1'&?&?&?). exists e1'. split_and!; [done..|]. by exists e'. }
+    clear Φ HΦ. apply rtc_nsteps in Hsteps as [n Hsteps].
+    revert e1 Hsteps. induction n as [|n IH]; intros e1 Hsteps.
+    { inv Hsteps. inv Hfinal. }
+    inv Hsteps. inv H0.
+    + eexists; split_and!; [done|by constructor|].
+      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+    + eexists; split_and!; [done|by constructor|].
+      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+    + eexists; split_and!; [done|by constructor|].
+      eapply rtc_l; [by constructor|by eapply rtc_nsteps_2].
+    + inv H2.
+      * apply IH in H1 as (e'' & Hsteps & ? & ?).
+        exists e''; split; [|done]. by eapply rtc_l.
+      * eexists; split_and!; [done|by constructor|].
+        eapply rtc_l; [by eapply SAppR|]. by eapply rtc_nsteps_2.
+Qed.
+
+Lemma Attr_wp_shallow Φ αs :
+  Φ (EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs)) →
+  wp SHALLOW (EAttr αs) Φ.
+Proof.
+  eexists (EAttr (AttrN ∘ _ <$> αs)); split_and!; [ |by constructor|done].
+  destruct (decide (no_recs αs)); [|apply rtc_once; by constructor].
+  apply reflexive_eq; f_equal. apply map_eq=> x. rewrite lookup_fmap.
+  destruct (αs !! x) as [[? e]|] eqn:?; f_equal/=.
+  by assert (τ = NONREC) as -> by eauto using no_recs_lookup.
+Qed.
+
+Lemma β_wp μ Φ x e1 e2 :
+  wp μ (subst {[x:=(ABS, e2)]} e1) Φ →
+  wp μ (EApp (EAbs x e1) e2) Φ.
+Proof.
+  intros (e' & Hsteps & ? & ?). exists e'. split; [|done].
+  eapply rtc_l; [|done]. by constructor.
+Qed.
+
+Lemma βMatch_wp μ Φ ms strict e1 αs βs :
+  no_recs αs →
+  matches (attr_expr <$> αs) ms strict βs →
+  wp μ (subst (indirects βs) e1) Φ →
+  wp μ (EApp (EAbsMatch ms strict e1) (EAttr αs)) Φ.
+Proof.
+  intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
+  eapply rtc_l; [|done]. by constructor.
+Qed.
+
+Lemma Functor_wp μ Φ αs e1 e2 :
+  no_recs αs →
+  αs !! "__functor" = Some (AttrN e1) →
+  wp μ (EApp (EApp e1 (EAttr αs)) e2) Φ →
+  wp μ (EApp (EAttr αs) e2) Φ.
+Proof.
+  intros ?? (e' & Hsteps & ? & ?). exists e'. split; [|done].
+  eapply rtc_l; [|done]. by constructor.
+Qed.
+
+Lemma If_wp μ Φ e1 e2 e3 :
+  wp SHALLOW e1 (λ e1', ∃ b : bool,
+    e1' = ELit (LitBool b) ∧ wp μ (if b then e2 else e3) Φ) →
+  wp μ (EIf e1 e2 e3) Φ.
+Proof.
+  intros (e1' & Hsteps & ? & b & -> & e' & Hsteps' & ? & HΦ).
+  exists e'; split; [|done]. etrans; [by apply SIf_rtc|].
+  eapply rtc_l; [|done]. destruct b; constructor.
+Qed.
+
+Lemma wp_mono μ e Φ Ψ :
+  wp μ e Φ →
+  (∀ e', Φ e' → Ψ e') →
+  wp μ e Ψ.
+Proof. intros (e' & ? & ? & ?) ?. exists e'. naive_solver. Qed.
+
+Lemma union_kinded_abs {A} mkv (v2 : A) :
+  union_kinded (pair WITH <$> mkv) (Some (ABS, v2)) = Some (ABS, v2).
+Proof. by destruct mkv. Qed.
+
+Lemma union_kinded_with {A} (v : A) mkv2 :
+  union_kinded (Some (WITH, v)) (pair WITH <$> mkv2) = Some (WITH, v).
+Proof. by destruct mkv2. Qed.