Guarantees by Construction (Mechanization)

Jules Jacobs

From dlfactris.lang Require Import metatheory.
From dlfactris.base_logic Require Export wp.
From dlfactris.base_logic Require Import cgraph.

Definition local_inv (σ : cfg) (ν : obj) : inEdges  aProp :=
  match ν with
  | Thread i => thread_inv (σ.1 !! i)
  | Chan l => heap_val_inv (σ.2 !! l)
  end.

Definition inv (σ : cfg) : siProp :=
  ginv  ν ins, aProp_at (local_inv σ ν ins)).

Lemma inv_unfold tid σ e :
  σ.1 !! tid = Some e 
  inv σ ⊣⊢  Σtid, inv' σ tid Σtid  aProp_at (wp_prim e  _, emp%I)) Σtid.
Proof.
  intros He. iSplit.
  - iDestruct 1 as (g Hg) "#Hinv".
    iPoseProof ("Hinv" $! (Thread tid)) as "Hwp".
    rewrite /= He /=. iDestruct "Hwp" as (?) "Hwp".
    iExists _; iSplit; last done.
    rewrite inv'_unfold. iExists g; iSplit; first done.
    iIntros ([i|l]); [destruct (decide _) as [->|]|]; [|iApply "Hinv"..].
    eauto using lookup_lt_Some.
  - iDestruct 1 as (Σ) "[Hinv Hwp]". rewrite inv'_unfold.
    iDestruct "Hinv" as (g ?) "Hinv". iExists (g); iSplit; first done.
    iIntros (ν); iSpecialize ("Hinv" $! ν).
    destruct ν; [destruct (decide _) as [->|]|]; [|iApply "Hinv"..].
    rewrite /= He /= !aProp_at_sep_affinely_l !aProp_at_pure.
    iDestruct "Hinv" as ([]) "Hinv"; iSplit; first done.
    rewrite /aProp_at. by iRewrite -"Hinv".
Qed.

Lemma inv_initialization e :                                                     (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cbbdb74a *)
  aProp_at (WP e {{ _, emp }})   inv ([e],).
Proof.
  rewrite wp_wp_prim (inv_unfold 0) //.
  iIntros "Hwp". iExists . iFrame "Hwp".
  rewrite inv'_unfold. iExists . iSplit; [iPureIntro; apply empty_wf|].
  iIntros (ν). rewrite out_edges_empty in_labels_empty /=.
  destruct ν as [[|i]|l]; simpl.
  - auto.
  - rewrite aProp_at_affinely aProp_at_pure. auto.
  - rewrite lookup_empty /= aProp_at_affinely aProp_at_pure. auto.
Qed.

Lemma inv_preservation σ1 σ2 :                                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f869fb95 *)
  step σ1 σ2 
  inv σ1   inv σ2.
Proof.
  iIntros (Hstep) "Hinv".
  destruct Hstep.
  assert (i < length es) by eauto using lookup_lt_Some.
  rewrite (inv_unfold i); eauto.
  rewrite (inv_unfold i); last first.
  { rewrite /= lookup_app_l ?insert_length //.
    rewrite list_lookup_insert //. }
  iDestruct "Hinv" as (Σ) "[Hinv Hwp]".
  rewrite wp_prim_unfold.
  erewrite prim_step_not_val; eauto.
  simpl. iDestruct "Hwp" as (Σ1) "#[Heq H]".
  iDestruct (excl_outEdges_injI with "Heq") as "HΣ".
  iMod ("H" with "[Hinv]") as "[_ H1]".
  { iNext. by iRewrite "HΣ". }
  iDestruct ("H1" with "[]") as (Σ') "[G1 G2]"; first eauto.
  iExists Σ'.
  iSplit; eauto.
  rewrite -insert_app_l //.
  by iApply inv'_tid_irrelevant.
Qed.

Definition active (σ : cfg) (o : obj) :=
  match o with
  | Thread i => match σ.1 !! i with
                | Some e => to_val e = None
                | None => False
                end
  | Chan l => is_Some (σ.2 !! l)
  end.

(* Waiting relation *)
Definition waiting (σ : cfg) (o1 o2 : obj) : Prop :=
   i l e, o1 = Thread i  o2 = Chan l  σ.1 !! i = Some e  blocked e l σ.2.

Global Instance waiting_dec σ o1 o2 : Decision (waiting σ o1 o2).
Proof.
  refine
    match o1, o2 with
    | Thread i, Chan l =>
       match Some_dec (σ.1 !! i) with
       | inleft (e  _) => cast_if (decide (blocked e l σ.2))
       | inright _ => right _
       end
    | _, _ => right _
    end; unfold waiting; naive_solver.
Defined.

Lemma inv_active_progress σ o :
  active σ o 
  inv σ     σ', step σ σ' .
Proof.
  iIntros (H) "#Hinv_all".
  iPoseProof "Hinv_all" as (g) "[%Hg Hinv]".
  iInduction o as [] "IH" using (cgraph_ind'  o1 o2 _, waiting σ o1 o2) g Hg).
  iDestruct ("Hinv" $! o) as "Hx".
  destruct o; simpl.
  - unfold active in H.
    destruct (σ.1 !! n) eqn:Heq; try done. simpl.
    iDestruct "Hx" as (Hinl) "HΦ".
    rewrite wp_prim_unfold. rewrite H. simpl.
    iDestruct "HΦ" as (Σ) "[H1 H2]".
    iAssert ( inv' σ n Σ)%I as "Hinv'".
    { rewrite inv'_unfold /ginv.
      iExists g. iSplit; first done.
      iIntros (ν). destruct ν.
      - case_decide; subst.
        + iSplit; first by eauto using lookup_lt_Some. by iApply excl_outEdges_injI.
        + iApply "Hinv".
      - iApply "Hinv". }
    destruct σ as [es h].
    iMod ("H2" with "Hinv'") as ([Hred|[l Hblocked]]) "_".
    { eauto using reducible_step. }
    unfold blocked in *.
    assert (Hblocked' := Hblocked).
    destruct Hblocked' as (Φ & (k & e' & Hctx & -> & Hblocked') & ).
    iAssert (  Φ',
       out_edges g (Thread n) !! Chan l = Some (inr (MiniProt ARecv Φ')) )%I as ">%HΣ'".
    { iDestruct (excl_outEdges_injI with "H1") as "{H1} H1". iNext.
      rewrite gmap_equivI. iSpecialize ("H1" $! (Chan l)).
      rewrite option_equivI .
      case _: (_ !! Chan l)=> [[?|[a' Φ']]|]; rewrite ?sum_equivI //=.
      iExists Φ'. rewrite miniprot_equivI /=. by iDestruct "H1" as "[<- _]". }
    destruct HΣ' as [Φ' HΣ'].
    iApply ("IH" $! (Chan l) (inr (MiniProt ARecv Φ'))).
    + by rewrite HΣ'.
    + unfold waiting. simpl.
      iExists _, _, _. iSplit; first done.
      iSplit; first done. iSplit; first done.
      iPureIntro. unfold blocked. exists k,e'. done.
    + unfold active. simpl in *.
      destruct Hblocked'; eauto.
  - unfold active in H.
    destruct H as [[[v|]|w] Hσl]; rewrite Hσl /=.
    + (* Channel has a value *)
      iDestruct "Hx" as (Φ) "[Heq HΦ]".
      rewrite aProp_at_affinely bi.and_elim_r aProp_at_internal_eq.
      iDestruct (in_labels_out_edges1 with "Heq") as (v1) "Hv1".
      destruct (out_edges g v1 !! Chan l) eqn:Heq; last first.
      { iDestruct "Hv1" as %Hv1. inversion Hv1. }
      iApply ("IH1" with "[] [] [>]").
      * erewrite Heq. done.
      * destruct (decide (waiting σ v1 (Chan l))) as [Hw|Hw]; eauto.
        destruct Hw as (n & l' & e' & -> & [= ->] & Hn & Hbl).
        unfold blocked in Hbl.
        destruct Hbl as (k & e'' & Hctx & -> & Hbl').
        destruct Hbl'. simplify_eq.
      * unfold active.
        iSpecialize ("Hinv" $! v1).
        { destruct v1; simpl.
          - destruct (σ.1 !! n) eqn:Heq'; simpl.
            + iDestruct "Hinv" as (_) "Hinv".
              rewrite wp_prim_unfold.
              destruct (to_val e); eauto.
              rewrite aProp_at_except_0 aProp_at_emp. iMod "Hinv" as %HH.
              rewrite map_empty_equiv_eq in HH.
              rewrite HH lookup_empty // in Heq.
            + iDestruct "Hinv" as (HH) "Hinv".
              rewrite HH lookup_empty // in Heq.
          - destruct (σ.2 !! l0); simpl; eauto.
            iDestruct "Hinv" as (HH) "Hinv".
            rewrite HH lookup_empty // in Heq. }
    + (* Channel has no value *)
      iDestruct "Hx" as (Φ) "[Hout Heq]".
      rewrite in_labels_out_edges2.
      iDestruct "Heq" as (ν1 ν2 Hν12) "[H1 H2]".
      rewrite !aProp_at_internal_eq option_equivI.
      destruct (out_edges g ν1 !! Chan l) eqn:Heq; last done.
      iAssert  active σ ν1 %I with "[>]" as %Hactive.
      { iSpecialize ("Hinv" $! ν1). destruct ν1 as [i|l']; simpl.
        - destruct (σ.1 !! i) eqn:Heq'; simpl.
          + iDestruct "Hinv" as (_) "Hinv".
            rewrite wp_prim_unfold.
            destruct (to_val e); last done.
            rewrite aProp_at_except_0. iMod "Hinv" as %HH.
            rewrite HH lookup_empty // in Heq.
          + iDestruct "Hinv" as (HH) "Hinv".
            rewrite HH lookup_empty // in Heq.
        - destruct (σ.2 !! l'); simpl; eauto.
          iDestruct "Hinv" as (HH) "Hinv".
          rewrite HH lookup_empty // in Heq. }
      destruct (decide (waiting σ ν1 (Chan l))) as [Hw|Hw]; last first.
      { iApply ("IH1" $! ν1); eauto. by rewrite Heq. }
      destruct Hw as (n & l' & e' & -> & [= ->] & Hn & Hbl).
      destruct Hbl as (k & e'' & Hctx & -> & Hbl').
      destruct Hbl'; simplify_eq.
      iDestruct ("Hinv" $! (Thread n)) as "Hwp".
      rewrite /= Hn /=.
      iDestruct "Hwp" as "[%Hinl Hwp]".
      rewrite wp_prim_unfold.
      rewrite to_val_ctx_None //=.
      iDestruct "Hwp" as (Σ) "[Hw1 Hw2]".
      iAssert ( inv' (σ.1, σ.2) n Σ)%I as "Hinv'".
      { rewrite inv'_unfold /ginv.
        iExists g. iSplit; first done.
        iIntros (ν). destruct ν.
        - case_decide; subst.
          + iSplit; first by eauto using lookup_lt_Some. by iApply excl_outEdges_injI.
          + iApply "Hinv".
        - iApply "Hinv". }
      iMod ("Hw2" with "Hinv'") as "[%Hww Hww2]".
      unfold reducible_or_blocked_own in Hww.
      destruct Hww as [Hww|Hww].
      { eauto using reducible_step. }
      destruct Hww as (l' & Φ' & Hblocked & ).
      eapply blocked_chan_unique in Hblocked as <-; eauto.
      rewrite excl_outEdges_injI. iNext.
      rewrite !gmap_equivI. iSpecialize ("Hw1" $! (Chan l)).
      rewrite  Heq.
      rewrite !option_equivI.
      iRewrite "H1" in "Hw1".
      rewrite !sum_equivI !miniprot_equivI /=.
      iDestruct "Hw1" as "[%QED _]". simplify_eq.
    + (* References *)
      iDestruct "Hx" as "[%Houtchan H2]".
      rewrite aProp_at_internal_eq.
      iDestruct (in_labels_out_edges1 with "H2") as (v1) "Hv1".
      rewrite option_equivI.
      destruct (out_edges g v1 !! Chan l) eqn:Heq; last done.
      iAssert  active σ v1 %I with "[>]" as %Hactive.
      { iSpecialize ("Hinv" $! v1). destruct v1 as [i|l']; simpl.
        - destruct (σ.1 !! i) eqn:Heq'; simpl.
          + iDestruct "Hinv" as (_) "Hinv".
            rewrite wp_prim_unfold.
            destruct (to_val e); last done.
            rewrite aProp_at_except_0. iMod "Hinv" as %HH.
            rewrite HH lookup_empty // in Heq.
          + iDestruct "Hinv" as (HH) "Hinv".
            rewrite HH lookup_empty // in Heq.
        - destruct (σ.2 !! l'); simpl; eauto.
          iDestruct "Hinv" as (HH) "Hinv".
          rewrite HH lookup_empty // in Heq. }
      destruct (decide (waiting σ v1 (Chan l))) as [Hw|Hw]; last first.
      { iApply ("IH1" $! v1); try done. by rewrite Heq. }
      destruct Hw as (n & l' & e' & -> & [= ->] & Hn & Hbl).
      destruct Hbl as (k & e'' & Hctx & -> & Hbl').
      destruct Hbl'. simplify_eq.
Qed.

Lemma final_or_active σ :
  (Forall  e', is_Some (to_val e')) σ.1  σ.2 = )   o, active σ o.
Proof.
  destruct (decide (Forall  e', is_Some (to_val e')) σ.1  σ.2 = ))
    as [|[Hforall|]%not_and_r]; simpl.
  - by left.
  - right. apply (not_Forall_Exists _) in Hforall
      as (e & He & ?%eq_None_not_Some)%Exists_exists; simpl in *.
    apply elem_of_list_lookup in He as [l Hl].
    exists (Thread l). by rewrite /= Hl.
  - right. apply map_choose in  as (l&o&Hl). exists (Chan l); naive_solver.
Qed.

Definition global_progress (σ : cfg) :=
  (Forall  e', is_Some (to_val e')) σ.1  σ.2 = )   σ', step σ σ'.

Definition all_progress_or_blocked (σ : cfg) :=
  Forall  e', is_Some (to_val e')  reducible_or_blocked e' σ.2) σ.1.

Lemma inv_global_progress σ :                                                    (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6be5758d *)
  inv σ    global_progress σ .
Proof.
  destruct (final_or_active σ) as [?|[o ?]].
  - iIntros "Hinv !> !%". by left.
  - iIntros "Hinv". iRight. by iApply inv_active_progress.
Qed.

Lemma inv_safety σ :                                                             (* https://apndx.org/pub/icnp/dlfactris.pdf#nameddest=f8ccbcb5 *)
  inv σ    all_progress_or_blocked σ .
Proof.
  iIntros "Hinv". rewrite /all_progress_or_blocked Forall_forall.
  iIntros (e [i Hi]%elem_of_list_lookup).
  iDestruct (inv_unfold with "Hinv") as (Σi) "[Hinv Hwp]"; first done.
  rewrite wp_prim_unfold. destruct (to_val e) eqn:?; simpl; first by eauto.
  iDestruct "Hwp" as (Σi') "[#HΣ Hwp]".
  iDestruct ("Hwp" $! i σ.1 σ.2 with "[Hinv]") as "[>%Hred _]".
  { rewrite excl_outEdges_injI. iNext. iRewrite "HΣ". by destruct σ. }
  rewrite /reducible_or_blocked; destruct Hred as [?|(?&?&?&?)]; eauto.
Qed.

Lemma adequacy e σ :                                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ea7b2c41 *)
  ( WP e {{ _, emp }}) 
  steps ([e],) σ 
  global_progress σ (* deadlock and leak freedom *) 
  all_progress_or_blocked σ (* conventional safety *).
Proof.
  intros Hwp Hsteps. rewrite aProp_emp_valid inv_initialization in Hwp.
  assert ( inv σ).
  { induction Hsteps as [σ|σ1 σ2 σ3 Hstep Hsteps IH]; [done|].
    apply IH, later_soundness. by rewrite -inv_preservation. }
  apply (pure_soundness (PROP:=siProp)), later_soundness. iSplit.
  - by iApply inv_global_progress.
  - by iApply inv_safety.
Qed.