Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.
Require Import ihc drf memsafe initread path.
Require Import GpsSepAlg permission.

Set Implicit Arguments.

Lemma upd_fin T:
  ∀ (ga: nat → option T) max x (FIN: ∀ n, max < n → ga n = None) l (L: max < l),
  ∃ max', ∀ n, max' < n → (mupd ga l x) n = None.

Lemma agrees_trans PS PSg sb rf V hmap hmap' hmap'':
  @agrees PS PSg sb rf V hmap hmap' → agrees sb rf V hmap' hmap'' → agrees sb rf V hmap hmap''.

Lemma new_ghost_def PS PSg :
  ∀ hf (g: ghost_resource) l g' (GL: g l = None),
  Hdef hf g +!+ gsingl _ _ l g' ≠ @Hundef PS PSg.

Lemma no_unallocated_ghosts PS PSg:
  ∀ lab sb rf mo hmap ga V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VLD: ∀ e, In e V → hmap_valid lab sb rf hmap ga e)
    max (GAfin: ∀ n, max < n → ga n = None)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    hf g (MAP: hmap (edge) = @Hdef PS PSg hf g),
  ∀ n, max < n → g n = None.

Lemma clos_trans_sb_implies_hbUrf:
  ∀ sb rf a b, clos_trans _ sb a b → happens_before_union_rf sb rf a b.

Lemma allocating_new_ghosts_helper:
  ∀ ga (e: actid) max l g (gnew : ghost_resource)
    (NG: ∀ x : nat, gnew x ≠ None ↔ ga x = Some e)
    (GAfin: ∀ n : nat, max < n → ga n = None)
    (MAX: max < l),
  ∀ x, (gres_plus_total gnew (gres_one l (Some g))) x ≠ None ↔
            mupd ga l (Some e) x = Some e.

Lemma allocating_new_ghosts_preserves_validity PS PSg:
  ∀ lab sb rf hmap ga e next max l g
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (VLD: hmap_valid lab sb rf hmap ga e)
    (GAfin: ∀ n, max < n → ga n = None)
    (SB: sb e next) (N: max < l)
    (gNEW: ∀ edge (EV: edge_valid lab sb rf edge) (FST: hb_fst edge = e)
                  hf gh (MAP: hmap edge = Hdef hf gh), gh l = None),
  hmap_valid lab sb rf
             (mupd hmap (hb_sb e next) (hmap (hb_sb e next) +!+ gsingl PS PSg l (Some g)))
             (mupd ga l (Some e)) e.

Theorem rule_ghost_intro PS PSg :
  ∀ P E QQ (T: triple P E QQ) PCM (IN: In PCM PSg) g,
    triple P E (fun v ⇒ Astar (QQ v) (Aexists (fun l ⇒ (@Aghost PS PSg PCM IN l g)))).
  Opaque assn_sem.
Opaque assn_sem.
Opaque assn_sem.
  Transparent assn_sem.