Require Import Vbase List QArith helpers_rationals.
Require Import Relations Classical ClassicalDescription.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fsl rmw fsl_addons fslassnlemmas2.
Require Import arc_permissions arc_ghosts arc_lemmas.

Set Implicit Arguments.

Opaque Aexists.

ARC implementation

We need some injection from pairs of naturals into naturals.

Structure PairEncoder :=
  mk_PairEncoder {
      pack: val → val → val;
      get_first: val → val;
      get_second: val → val;
      get_first_ok: ∀ a b, get_first (pack a b) = a;
      get_second_ok: ∀ a b, get_second (pack a b) = b
    }.

Parameter PE : PairEncoder.

Definition pack_pair := pack PE.
Definition data := get_first PE.
Definition counter := get_second PE.

Definition ARC_new (v: val) :=
  LET d <- Ealloc in
  LET c <- Ealloc in
  Estore ATna d v ;;
  Estore ATrlx c 1 ;;
  Evalue (pack_pair d c).

Definition ARC_load a :=
  Eload ATna (data a).

Definition ARC_clone a :=
  increment ATrlx (counter a).

Definition ARC_drop a :=
  LET t <- decrement ATrel (counter a) in
  if (t == 1%nat)%bool then (Efence ATacq ;; Evalue t) else Evalue t.

Correctness of ARC

ARC invariant

Definition QQ (g g' v dat c : val) : arc_assn :=
  match c with
    | O ⇒ GhostMinus g 0 &*& GhostMinus g' 0
    | _ ⇒ Aexists (fun numerator ⇒ Aexists (fun denominator ⇒ let f := frac numerator denominator in
             if excluded_middle_informative (0 ≤ f ≤ 1)
             then Pointsto dat f v &*& GhostMinus g ((frac c 1) + f - 1) &*& GhostMinus g' (1 - f)
             else Afalse))
  end.

ARC predicate

Definition ARC (a v g g': val) : arc_assn :=
  RMW (counter a) (QQ g g' v (data a)) &*&
  Aexists (fun numerator ⇒ Aexists (fun denominator ⇒ let q := frac numerator denominator in
    if excluded_middle_informative (0 < q ∧ q ≤ 1)
    then Pointsto (data a) q v &*& GhostPlus g (1 - q) &*& GhostPlus g' q
    else Afalse)).

We can now prove the correctness of ARC.

Theorem ARC_new_spec v:
  triple (Aemp)
         (ARC_new v)
         (fun a ⇒ Aexists (fun g ⇒ Aexists (fun g' ⇒ ARC a v g g'))).
Proof.
  eapply rule_let.
    by apply rule_alloc_na_with_two_ghosts.
  intro d.
  apply rule_exists; intro g.
  apply rule_exists; intro g'.
  eapply rule_let.
    by apply rule_alloc_atom_rmwacq_frame.
  intro c.
  instantiate (1 := QQ g g' v d).
  eapply rule_let. eapply rule_let.
  {
    eapply rule_conseq_pre.
      2: by apply implies_star_r, equivalent_starAC.
    eapply rule_conseq_pre.
      2: by apply equivalent_starAC.
    apply rule_frame.
    apply rule_store_na2.
  }
  {
    ins; clear x.
    match goal with |- (triple ?F _ _) ⇒
      assert (I: implies F ((Arel c (QQ g g' v d) &*& Armwacq c (QQ g g' v d)
                             &*& GhostMinus g 0 &*& GhostMinus g' 1)
                             &*& GhostPlus g 0 &*& GhostPlus g' 1 &*& Pointsto d 1 v)) end.
    {
      rewrite !equivalent_starA, equivalent_starAC.
      apply implies_star_r.
      rewrite equivalent_starAC.
      apply implies_star_r.
      rewrite <- (empty_ghost_r g) at 1; eauto.
      rewrite !equivalent_starA, equivalent_starAC.
      apply implies_star_r.
      rewrite !(equivalent_starAC (GhostPlus g 0)).
      apply implies_star_r.
      rewrite <- (equivalent_starA _ _ (Pointsto _ _ _)), (equivalent_starC _ (Pointsto _ _ _)).
      rewrite produce_one_token.
      apply implies_star_l.
      unfold Pointsto; desf.
      by refl_implies; eapply Apt_equal; eq_rect_simpl; try apply QP_equal.
      by destruct n.
    }
    eapply rule_conseq_pre; try exact I; clear I.
    apply rule_frame.
    assert(I: implies (GhostMinus g 0 &*& GhostMinus g' 1) (Atriangle (QQ g g' v d 1%nat))).
    {
      ins. red. intros h SEM.
      apply triangle_exists.
      apply assn_sem_exists; ∃ 0%nat.
      apply triangle_exists.
      apply assn_sem_exists; ∃ 1%nat.
      change (frac 0 1) with 0.
      change (frac 1 1 + 0 - 1) with 0.
      change (1 - 0) with 1.
      desf; desf; [ | by destruct n].
      apply triangle_star_dist.
      rewrite empty_pointsto.
      eapply implies_star_l.
        by apply triangle_emp.
      revert h SEM; fold_implies.
      by rewrite <- star_emp_l, triangle_star_dist, !triangle_GhostMinus.
    }
    eapply rule_conseq_pre.
      2: eby rewrite I.
    by apply rule_store_rlx_rmw.
  }
  {
    ins; clear x.
    eapply rule_conseq.
    apply rule_value.
    instantiate (1 := (fun a ⇒ RMW (counter a) (QQ g g' v (data a)) &*&
                                GhostPlus g 0 &*& GhostPlus g' 1 &*& Pointsto (data a) 1 v)).
      by ins; unfold data, counter; rewrite get_first_ok, get_second_ok.
    red. intros a h SEM.
    apply assn_sem_exists; ∃ g.
    apply assn_sem_exists; ∃ g'.
    unfold ARC.
    revert SEM.
    apply implies_star_r.
    red; intros ? SEM.
    apply assn_sem_exists; ∃ 1%nat.
    apply assn_sem_exists; ∃ 1%nat.
    change (frac 1 1) with 1.
    change (1 - 1) with 0.
    desf; [ | by destruct n].
    eapply equivalent_starAC.
    revert h0 SEM; fold_implies.
    by apply implies_star_r; rewrite equivalent_starC.
  }
  
  Grab Existential Variables. done. by apply in_eq.
Qed.

Theorem ARC_load_spec a v g g':
  triple (ARC a v g g')
         (ARC_load a)
         (fun x ⇒ if (x == v)%bool then ARC a v g g' else Afalse).
Proof.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro numerator.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro denominator; desf.
  Focus 2.
    eapply rule_conseq_pre.
    by apply triple_false.
    by red; ins; desf.
  eapply rule_conseq.
    2: by rewrite equivalent_starAC; apply implies_refl.
    by apply rule_frame, rule_load_poinsto; desf.
  ins; desf; desf.
    2: by red; ins; desf.
  rewrite equivalent_starAC; unfold ARC.
  apply implies_star_r.
  red; intros.
  apply assn_sem_exists; ∃ numerator.
  apply assn_sem_exists; ∃ denominator.
  desf.
  by destruct n; split.
Qed.

Theorem ARC_clone_spec a v g g':
   triple (ARC a v g g')
          (ARC_clone a)
          (fun x ⇒ if (x == 0%nat)%bool then Afalse else ARC a v g g' &*& ARC a v g g').
Proof.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro numerator.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro denominator; desf.
    Focus 2.
    eapply rule_conseq_pre.
    by apply triple_false.
    by red; ins; desf.
  remember (frac numerator denominator) as q.
  remember (Pointsto (data a) q v &*& GhostPlus g (1 - q) &*& GhostPlus g' q) as whole_formula.
  eapply rule_conseq.
    2: eby rewrite RMW_split, !equivalent_starA, (equivalent_starC _ whole_formula), <- equivalent_starA.
  apply rule_frame.
  eapply rule_conseq_pre.
    2: by rewrite rmw_permission_rmw_precondition; apply implies_refl.

  apply rule_fetch_and_modify with
        (Psend := fun x : val ⇒ if (x == 0%nat)%bool then whole_formula else Atriangle Aemp)
        (Pkeep := fun x : val ⇒ if (x == 0%nat)%bool then Aemp else whole_formula)
        (RR := fun x : val ⇒ if (x == 0%nat)%bool then Afalse else GhostPlus g 1).
  subst whole_formula.

  by ins; desf; rewrite ?triangle_emp, <- ?star_emp_l, <- ?star_emp_r; apply equivalent_refl.

  {
    ins; destruct t.
    {
      desf; desf.
      eapply rule_conseq_post.
      × apply rule_cas_shortcut_simple; ins.
        rewrite !equivalent_starA, <- !(equivalent_starAC (GhostMinus g' _)), consume_token.
        unfold GhostMinus at 2; desf.
          2: by rewrite !star_false.
        exfalso; unfold Qminus in *; rewrite Qred_correct, Qplus_0_l in ×.
        eapply Qplus_lt_le_compat in q; try edone.
        by rewrite Qplus_0_l, Qplus_opp_r in ×.
      × ins; desf; desf.
    }
    {
      assert (S t ≠ 0%nat) by done.
      remember (S t) as t' eqn:X; clear X.
      desf; desf.
      eapply rule_conseq_post.
      × apply rule_cas_rlx_simple with (TT := fun _ ⇒ QQ g g' v (data a) (t' + 1%nat)%nat)
                                       (AA := fun _ ⇒ GhostPlus g 1) (phi := fun _ ⇒ True);
        try done.
        + unfold QQ; desf; desf.
          red; intros.
          apply assn_sem_exists in H0; destruct H0 as [p].
          apply assn_sem_exists in H0; destruct H0 as [q]; desf.
          apply assn_sem_exists; eexists; try done.
          revert h H0; fold_implies.
          rewrite !star_exists.
          unfold implies; intros.
          apply assn_sem_exists; ∃ p.
          revert h H0; fold_implies; rewrite !star_exists.
          unfold implies; intros.
          apply assn_sem_exists; ∃ q.
          revert h H0; fold_implies.
          desf; desf.
            2: by destruct n1; done.
          rewrite (equivalent_starAC (Pointsto _ _ _)); apply implies_star_r.
          rewrite <- equivalent_starA; apply implies_star_l.
          rewrite equivalent_starC, produce_one_token; apply implies_star_l.
          refl_implies; apply GhostMinus_eq.
          unfold Qminus; rewrite <- !Qplus_assoc, Qplus_opp_l, Qplus_0_r,
                                 (Qplus_comm _ (- _)), Qplus_assoc.
          apply Qplus_inj_r.
          assert (N: (S n0 = S n + 1)%nat) by omega; rewrite N.
          by rewrite frac_plus_1, <- Qplus_assoc, Qplus_opp_r, Qplus_0_r.
        + unfold satisfying; ins; desf.
           by rewrite <- star_emp_l.
      × ins; desf; desf.
        unfold satisfying; red; ins.
        apply assn_sem_exists in H0; desf.
        revert h H0; fold_implies.
        by rewrite nabla_GhostPlus.
    }
  }
  
  ins; desf.
    by rewrite !false_star; apply false_implies.
  unfold ARC; rewrite !equivalent_starA, !star_exists.
  unfold implies; intros.
  apply assn_sem_exists; ∃ numerator.
  revert h H; fold_implies; rewrite !star_exists.
  unfold implies; intros.
  apply assn_sem_exists; ∃ (2 × denominator)%nat.
  revert h H; fold_implies. rewrite !star_exists2, !star_exists.
  unfold implies; intros.
  apply assn_sem_exists; ∃ numerator.
  revert h H; fold_implies. rewrite !star_exists2, !star_exists.
  unfold implies; intros.
  apply assn_sem_exists; ∃ (2 × denominator)%nat.
  assert (0 < frac numerator (2 × denominator) ∧ frac numerator (2 × denominator) ≤ 1).
  {
    clear H; split.
    × unfold frac; desf.
        by destruct denominator; try omega.
      unfold Qlt; ins.
      rewrite Z.mul_1_r.
      unfold Z.of_nat; desf.
      unfold frac in a1; desf; try omega.
      by destruct denominator.
    × eapply Qle_trans; try edone.
      unfold frac; desf; desf; try omega.
      unfold Qle; ins.
      apply Z.mul_le_mono_nonneg_l.
        by unfold Z.of_nat; desf.
      rewrite Nat.add_0_r, Nat2Pos.inj_add, Pos2Z.inj_add; try done.
      remember (Zpos (Pos.of_nat denominator)) as n.
      apply Zplus_le_reg_r with (p := (- n)%Z).
      rewrite <- Z.add_assoc, Z.add_opp_diag_r, Z.add_0_r; desf.
  }
  desf; desf; try by destruct n.
  revert h H; fold_implies.
  rewrite (equivalent_starC _ (RMW _ _)); rewrite !(equivalent_starAC (RMW _ _)),
          <- !equivalent_starA, <- RMW_split, !equivalent_starA.
  apply implies_star_r.
  rewrite <- !(equivalent_starAC (GhostPlus g' _)).
  rewrite <- split_tokens; try solve [by rewrite sum_halves | by apply Qlt_le_weak].
  rewrite <- !equivalent_starA; apply implies_star_l; rewrite !equivalent_starA.
  rewrite !(equivalent_starAC (Pointsto _ _ _)).
  rewrite combine_tokens.
  rewrite split_tokens with (a := 1 + (1 - frac numerator denominator))
                            (b := 1 - frac numerator (2 × denominator))
                            (c := 1 - frac numerator (2 × denominator)).
  do 2 (rewrite <- !equivalent_starA; apply implies_star_l; rewrite ?equivalent_starA).
  by rewrite <- split_pointsto; try solve [by rewrite sum_halves | by apply Qlt_le_weak].
  × unfold Qminus; rewrite (Qplus_comm 1 (- frac _ (_ × _))) at 2.
    by rewrite <- !Qplus_assoc, (Qplus_comm 1 (- _ + _)), !Qplus_assoc, <- Qopp_plus, sum_halves,
               Qplus_comm, Qplus_assoc.
  × apply Qplus_le_l with (z := frac numerator (2 × denominator)).
    by unfold Qminus; rewrite <- Qplus_assoc, Qplus_opp_l, Qplus_0_l, Qplus_0_r.
  × apply Qplus_le_l with (z := frac numerator (2 × denominator)).
    by unfold Qminus; rewrite <- Qplus_assoc, Qplus_opp_l, Qplus_0_l, Qplus_0_r.
Qed.

Theorem ARC_drop_spec a v g g' :
  triple (ARC a v g g')
         (ARC_drop a)
         (fun x ⇒ if (x == 0%nat)%bool then Afalse
                   else if (x == 1%nat)%bool then Pointsto (data a) 1 v
                   else Aemp).
Proof.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro numerator.
  eapply rule_conseq_pre.
     2: by unfold ARC; rewrite !star_exists; apply implies_refl.
  apply rule_exists; intro denominator; desf.
    Focus 2.
    eapply rule_conseq_pre.
    by apply triple_false.
    by red; ins; desf.
  remember (frac numerator denominator) as q.
  remember (Pointsto (data a) q v &*& GhostPlus g (1 - q) &*& GhostPlus g' q) as whole_formula.
  eapply rule_let.

  {
    eapply rule_conseq_pre.
      2: by rewrite rmw_permission_rmw_precondition; apply implies_refl.
    apply rule_fetch_and_modify with
          (Psend := fun x : val ⇒ if (x == 0%nat)%bool then whole_formula
                                   else if (x == 1%nat)%bool then GhostPlus g (1 - q) &*& GhostPlus g' q
                                   else whole_formula)
          (Pkeep := fun x : val ⇒ if (x == 0%nat)%bool then Aemp else
                                   if (x == 1%nat)%bool then Pointsto (data a) q v
                                   else Aemp)
          (RR := fun x : val ⇒ if (x == 0%nat)%bool then Afalse
                                 else if (x == 1%nat)%bool then Anabla (Pointsto (data a) (1 - q) v)
                                 else Aemp).
    subst whole_formula.
    × ins; desf; desf; rewrite <- ?star_emp_r, ?equivalent_starA; try apply equivalent_refl.
      rewrite equivalent_starC, equivalent_starA; apply equivalent_refl.
    × ins; desf; desf.
      {
        apply rule_cas_shortcut_simple; ins.
        remember (frac numerator denominator) as q; clear Heqq.
        rewrite !equivalent_starA, <- !(equivalent_starAC (GhostMinus g' _)), consume_token.
        unfold GhostMinus at 2; desf.
          2: by red; ins; desf.
        exfalso; exploit Qplus_lt_le_compat.
        by exact a0.
        by exact q0.
        by unfold Qminus; rewrite Qred_correct, !Qplus_0_l, Qplus_opp_r.
      }
      {
        remember (frac numerator denominator) as q.
        eapply rule_conseq_post.
        eapply rule_cas_rel_simple with
          (TT := fun z ⇒ let f := frac (get_first PE z) (get_second PE z) in
                           GhostMinus g f &*& GhostMinus g' (1 - f))
          (AA := fun z ⇒ let f := frac (get_first PE z) (get_second PE z) in
                           Pointsto (data a) f v)
          (phi := fun z ⇒ let f := frac (get_first PE z) (get_second PE z) in
                           f + q == 1); try by vauto.
        × by apply normalizable_star; apply normalizable_GhostPlus.
        × clear; unfold QQ; ins.
          red; intros.
          apply assn_sem_exists in H; destruct H as [numerator].
          apply assn_sem_exists in H; destruct H as [denominator]; desf.
          apply assn_sem_exists; ∃ (pack PE numerator denominator).
          rewrite get_first_ok, get_second_ok.
          revert h H; fold_implies.
          apply implies_star_r, implies_star_l.
          refl_implies; apply GhostMinus_eq.
          by unfold Qminus; rewrite frac11, Qplus_comm, Qplus_assoc, Qplus_opp_l, Qplus_0_l.
        × clear Heqq; unfold satisfying; ins.
          remember (frac (get_first PE z) (get_second PE z)) as f; clear Heqf.
          rewrite equivalent_starA, (equivalent_starAC (GhostMinus g _)), <- equivalent_starA, !consume_token2.
          desf.
          + apply implies_star; refl_implies; apply GhostMinus_eq; unfold Qminus.
            by rewrite (Qplus_comm 1), Qopp_plus, Qopp_opp, Qplus_assoc, q0.
            by rewrite <- Qplus_assoc, <- Qopp_plus, q0.
          + clear - n; apply Qneq in n; desf.
            - unfold GhostMinus at 1; unfold Qminus; desf.
                2: by red; ins; desf.
              exfalso; rewrite Qred_correct in ×.
              exploit Qplus_lt_le_compat; ins; try edone.
              rewrite (Qplus_comm f (- _)), Qopp_plus, !Qplus_assoc, Qopp_opp, Qplus_opp_r,
                      Qplus_0_r, Qplus_0_l, Qplus_comm in x0.
              eby eapply Qlt_irrefl.
            - unfold GhostMinus at 2; unfold Qminus; desf.
                2: by red; ins; desf.
              exfalso; rewrite Qred_correct in ×.
              exploit Qplus_lt_le_compat; ins; try edone.
              rewrite <- (Qplus_assoc 1), <- Qopp_plus, (Qplus_comm 1 (- _)), Qplus_assoc,
                      Qplus_opp_r, Qplus_comm in x0.
              eby eapply Qlt_irrefl.
        × ins; desf; desf.
          red; intros.
          apply assn_sem_exists in H; unfold satisfying in H; desf.
          revert h H; fold_implies; refl_implies.
          f_equal; apply Pointsto_eq.
          by unfold Qminus; rewrite <- q, <- Qplus_assoc, Qplus_opp_r, Qplus_0_r.
      }
      {
        remember (frac numerator denominator) as q; clear Heqq.
        eapply rule_conseq_post.
        eapply rule_cas_rel_simple with (TT := fun _ ⇒ QQ g g' v (data a) t) (AA := fun _ ⇒ Aemp)
                                        (phi := fun _ ⇒ True); try by vauto.
        × repeat apply normalizable_star; try apply normalizable_GhostPlus.
          by apply normalizable_Pointsto.
        × red; ins.
          apply assn_sem_exists; eexists; try done.
          revert h H; fold_implies.
          by rewrite <- star_emp_l.
        × ins; unfold satisfying; desf.
          unfold QQ; desf; ins; desf; try omega.
          remember (S n0) as n; assert (N: n ≠ 0%nat) by omega; clear Heqn Heq Heq0.
          rewrite !star_exists.
          red; intros.
          apply assn_sem_exists in H; destruct H as [num H].
          revert h H; fold_implies; rewrite !star_exists.
          red; intros.
          apply assn_sem_exists in H; destruct H as [den H]; desf; desf.
            2: by ins; desf.
          revert h H; fold_implies.
          remember (frac num den) as f; clear Heqf.
          rewrite !equivalent_starA, !(equivalent_starAC (Pointsto _ f _)),
                  (equivalent_starAC (GhostMinus g _)), <- (equivalent_starA (Pointsto _ _ _)),
                  <- (equivalent_starA (GhostPlus g _)), !consume_token2, <- split_pointsto; try by edone.
                  2: by apply Qlt_le_weak.
          exploit Q_to_frac.
            by apply Qplus_le_compat with (x := 0) (z := 0) (y := f) (t := q); try done; apply Qlt_le_weak.
          intro EQ; destruct EQ as [x [y EQ]].
          red; intros.
          apply assn_sem_exists; ∃ x.
          apply assn_sem_exists; ∃ y; desf.
          + revert h H; fold_implies.
            repeat apply implies_star; refl_implies.
            - by apply Pointsto_eq.
            - apply GhostMinus_eq.
              replace (S n) with (n + 1%nat)%nat by omega.
              unfold Qminus; rewrite frac_plus_1, <- !Qplus_assoc.
              apply Qplus_inj_l.
              rewrite Qopp_plus, Qopp_opp, (Qplus_comm f), !Qplus_assoc, Qplus_opp_r, Qplus_0_l.
              rewrite <- Qplus_assoc, Qplus_comm.
              apply Qplus_inj_r.
              by rewrite Qplus_comm.
            - apply GhostMinus_eq.
              by unfold Qminus; rewrite <- Qplus_assoc, <- Qopp_plus, EQ.
          + revert h H; fold_implies.
            rewrite <- EQ in n1.
            apply not_and_or in n1; desf.
            - unfold Pointsto; desf; desf.
              by red; ins; desf.
            - unfold GhostMinus at 2; desf.
                2: by red; ins; desf.
              destruct n1; rewrite Qred_correct in ×.
              by rewrite Qle_minus_iff; unfold Qminus in *; rewrite Qopp_plus, Qplus_assoc.
        × ins; desf; desf.
          red; unfold satisfying; intros.
          apply assn_sem_exists in H; desf.
          revert h H; fold_implies.
          by rewrite nabla_emp.
      }
  }
  
  ins; desf; desf.
  × eapply rule_conseq_pre.
    by apply triple_false.
    by red; ins; desf.
  × eapply rule_let.
      by apply rule_frame, rule_fence_acq; vauto.
    ins; eapply rule_conseq_pre.
      by apply rule_value.
    desf; desf.
    rewrite <- split_pointsto; try edone.
    by unfold Qminus; rewrite <- Qplus_assoc, Qplus_opp_l.
    by unfold Qminus; rewrite <- Qle_minus_iff.
    by apply Qlt_le_weak.
  × eapply rule_conseq_pre.
      by apply rule_value.
    desf; desf.
    by rewrite <- star_emp_r.
Qed.

This page has been generated by coqdoc