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.

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.

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.

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)).

Theorem ARC_new_spec v:
  triple (Aemp)
         (ARC_new v)
         (fun a ⇒ Aexists (fun g ⇒ Aexists (fun g' ⇒ ARC a v g g'))).

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).

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').

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).