text:
From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import CoreExpr.CESyntax.
From Velus Require Import Stc.StcSyntax.
From Velus Require Import Clocks.

From Velus Require Export CoreExpr.CEIsFree.

From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

Module Type STCISFREE
       (Import Ids   : IDS)
       (Import Op    : OPERATORS)
       (Import CESyn : CESYNTAX      Op)
       (Import Syn   : STCSYNTAX Ids Op CESyn)
       (Import CEIsF : CEISFREE  Ids Op CESyn).

  Inductive Is_free_in_tc: ident -> trconstr -> Prop :=
  | FreeTcDef:
      forall x ck e y,
        Is_free_in_caexp y ck e ->
        Is_free_in_tc y (TcDef x ck e)
  | FreeTcNext:
      forall x ck e y,
        Is_free_in_aexp y ck e ->
        Is_free_in_tc y (TcNext x ck e)
  | FreeTcReset:
      forall s ck b x,
        Is_free_in_clock x ck ->
        Is_free_in_tc x (TcReset s ck b)
  | FreeTcCall:
      forall s x ck rst b es y,
        Is_free_in_aexps y ck es ->
        Is_free_in_tc y (TcCall s x ck rst b es).

  Definition Is_free_in (x: ident) (tcs: list trconstr) : Prop :=
    Exists (Is_free_in_tc x) tcs.

  Definition free_in_tc (tc: trconstr) (fvs: PS.t) : PS.t :=
    match tc with
    | TcDef _ ck e => free_in_caexp ck e fvs
    | TcNext _ ck e => free_in_aexp ck e fvs
    | TcReset _ ck _ => free_in_clock ck fvs
    | TcCall _ _ ck _ _ es => free_in_aexps ck es fvs
    end.

  Hint Constructors Is_free_in_clock Is_free_in_exp
       Is_free_in_aexp Is_free_in_aexps Is_free_in_cexp
       Is_free_in_caexp Is_free_in_tc.

  Lemma free_in_tc_spec:
    forall x tc m,
      PS.In x (free_in_tc tc m)
      <-> (Is_free_in_tc x tc \/ PS.In x m).
  Proof.
    Local Ltac aux :=
      repeat (match goal with
              | H:Is_free_in_tc _ _ |- _ => inversion_clear H
              | H:PS.In _ (free_in_tc _ _) |- _ =>
                apply free_in_clock_spec in H
                || apply free_in_caexp_spec in H
                || apply free_in_aexp_spec in H
                || apply free_in_aexps_spec in H
              | |- PS.In _ (free_in_tc _ _) =>
                apply free_in_clock_spec
                || apply free_in_caexp_spec
                || apply free_in_aexp_spec
                || apply free_in_aexps_spec
              | _ => intuition; eauto
              end).
    destruct tc; split; intro H; aux.
  Qed.

  Corollary free_in_tc_spec':
    forall x tc,
      PS.In x (free_in_tc tc PS.empty)
      <-> Is_free_in_tc x tc.
  Proof.
    intros; rewrite free_in_tc_spec. intuition.
  Qed.

End STCISFREE.

Module StcIsFreeFun
       (Ids   : IDS)
       (Op    : OPERATORS)
       (CESyn : CESYNTAX     Op)
       (Syn   : STCSYNTAX Ids Op CESyn)
       (CEIsF : CEISFREE Ids Op CESyn)
<: STCISFREE Ids Op CESyn Syn CEIsF.
  Include STCISFREE Ids Op CESyn Syn CEIsF.
End StcIsFreeFun.

author: INRIA

repo: velus

save_path: github-repos/coq/INRIA-velus


text:
From Coq Require Import Reals.
From Coquelicot Require Import Coquelicot.

Require Import Lra Lia.
Require Import List Permutation.
Require Import Morphisms EquivDec Program.
Require Import Classical_Prop.
Require Import Classical.

Require Import Utils.
Require Import RealRandomVariable.
Require Import Almost.
Require Import Event.
Require Import SigmaAlgebras.
Require Import ProbSpace.
Require Import BorelSigmaAlgebra.
Require Import LInt_p.sigma_algebra.
Require Import LInt_p.measure.
Require Import LInt_p.measurable_fun.
Require Import LInt_p.LInt_p.
Require Import LInt_p.sigma_algebra_R_Rbar.
Require Import LInt_p.sum_Rbar_nonneg.
Require Import LInt_p.Rbar_compl.
Require Import Classical.

Set Bullet Behavior "Strict Subproofs".

Import ListNotations.

Definition lintp_borel_sa : SigmaAlgebra R := generated_sa gen_R_uc.

Program Instance measurable_sigma_algebra {T} (F:pre_event T -> Prop) : SigmaAlgebra T
  := { sa_sigma := measurable F }.
Next Obligation.
  now apply measurable_union_countable.
Qed.
Next Obligation.
  apply measurable_compl.
  unfold pre_event_complement.
  apply measurable_ext with (A).
  intro x; tauto.
  apply H.
Qed.
Next Obligation.
  apply measurable_compl.
  unfold pre_Ω.
  apply measurable_ext with (fun _ => False).
  tauto.
  apply measurable_empty.
Qed.

Theorem measurable_sa {T} (F:pre_event T -> Prop) :
  forall a, prob_space_closure F a <-> measurable F a.
Proof.
  split; intros.
  - induction H.
    + unfold pre_Ω.
      apply measurable_compl.
      apply measurable_ext with (fun _ => False).
      tauto.
      apply measurable_empty.
    + now apply measurable_gen.
    + now apply measurable_union_countable.
    + apply measurable_compl.
      unfold pre_event_complement.
      apply measurable_ext with (q).
      intro; tauto.
      trivial.
  - induction H.
    + now apply psc_refl.
    + assert (@pre_event_equiv T (fun _ => False) (pre_event_complement (fun _ => True))).
      {
        intro x.
        unfold pre_event_complement.
        tauto.
      }
      rewrite H.
      apply psc_complement.
      apply psc_all.
    + assert (@pre_event_equiv T A (pre_event_complement (fun x => ~ A x))).
      {
        intro x.
        unfold pre_event_complement.
        tauto.
      }
      rewrite H0.
      now apply psc_complement.
    + now apply psc_countable.
Qed.

Definition dec_pre_event {Ts} (dom : SigmaAlgebra Ts) ( A : pre_event Ts) :
  {sa_sigma A} + {~ sa_sigma A} :=
  ClassicalDescription.excluded_middle_informative (sa_sigma A).

Program Definition ps_P_pre {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) :
  (pre_event Ts -> R) :=
  fun (A : pre_event Ts) =>
    if (dec_pre_event dom A) then ps_P A else 0.

Lemma ps_P_pre_sa_sigma {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom)
        (E : pre_event Ts)
        (sa : sa_sigma E) :
    ps_P_pre prts E = ps_P (exist _ E sa).
  Proof.
    unfold ps_P_pre, ps_P_pre_obligation_1.
    match_destr; try easy.
    apply ps_proper.
    now intro x; simpl.
  Qed.

Lemma disjoint_pre_collection {T} (coll : nat -> pre_event T) :
  pre_collection_is_pairwise_disjoint coll <->
  (forall n m x, coll n x -> coll m x -> n = m).
Proof.
  unfold pre_collection_is_pairwise_disjoint.
  unfold pre_event_disjoint.
  split; intros.
  - specialize (H n m).
    assert ((n <> m) -> False).
    + intros.
      now specialize (H H2 x H0 H1).
    + tauto.
  - specialize (H n1 n2 x H1 H2).
    lia.
Qed.

Lemma measurable_pre_event {Ts} (dom : SigmaAlgebra Ts) (E : pre_event Ts) :
  measurable sa_sigma E <-> sa_sigma E.
Proof.
  split; intros.
  - induction H; trivial.
    + apply sa_none.
    + apply sa_complement in IHmeasurable.
      assert (pre_event_equiv (pre_event_complement (fun x : Ts => ~ A x))
                              A).
      * intro x.
        unfold pre_event_complement.
        tauto.
      * now rewrite H0 in IHmeasurable.
    + now apply sa_countable_union.
  - now apply measurable_gen.
 Qed.

Lemma sum_Rbar_finite (f : nat -> R) (n : nat) :
  sum_Rbar n (fun n => Finite (f n)) = Finite (sum_f_R0 f n).
Proof.
  induction n.
  - now simpl.
  - simpl.
    rewrite IHn.
    simpl.
    apply Rbar_finite_eq.
    lra.
 Qed.

(* need to create a (measure gen) from probspace. *)
Program Definition ProbSpace_measure {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) : measure sa_sigma :=
  mk_measure _ (ps_P_pre prts) _ _ _  .
Next Obligation.
  unfold ps_P_pre, ps_P_pre_obligation_1.
  match_destr.
  assert (event_equiv
            (exist sa_sigma (fun _ : Ts => False) s)
            event_none) by
      (intro x; simpl; tauto).
  rewrite H.
  now rewrite ps_none.
Qed.
Next Obligation.
  unfold ps_P_pre.
  match_destr.
  apply ps_pos.
  lra.
Qed.
Next Obligation.
  assert (forall n, sa_sigma (A n)) by (intros; now apply measurable_pre_event).
  generalize (sa_countable_union A H1); intros.
  rewrite ps_P_pre_sa_sigma with (sa := H2).
  assert (event_equiv
            (exist sa_sigma (pre_union_of_collection A) H2)
            (union_of_collection (fun n => exist _ (A n) (H1 n)))) by
      (intro x; now simpl).
  rewrite H3.
  generalize (ps_countable_disjoint_union (fun n => exist _ (A n) (H1 n))); intros.
  cut_to H4.
  - unfold sum_of_probs_equals in H4.
    rewrite <- infinite_sum_infinite_sum' in H4.
    rewrite <- infinite_sum_is_lim_seq in H4.
    apply lim_seq_sup_seq_incr in H4.
    + apply is_sup_seq_unique in H4.
      rewrite <- H4.
      symmetry.
      rewrite Sup_seq_ext with
          (v :=
             (fun n => Finite (sum_f_R0 (fun m => ps_P (exist sa_sigma (A m) (H1 m))) n))).
      * apply Sup_seq_ext.
        now intros.
      * intros.
        replace (Finite (sum_f_R0 (fun m => ps_P (exist sa_sigma (A m) (H1 m))) n)) with
            (sum_Rbar n (fun m => ps_P (exist sa_sigma (A m) (H1 m)))).
        -- apply sum_Rbar_ext; intros.
           generalize (H1 i); intros.
           now rewrite ps_P_pre_sa_sigma with (sa := s).
        -- now rewrite sum_Rbar_finite.
    + intros.
      rewrite sum_f_R0_peel.
      apply Rplus_le_pos_l.
      apply ps_pos.
  - unfold collection_is_pairwise_disjoint.
    intros.
    unfold event_disjoint, pre_event_disjoint; simpl.
    intros.
    specialize (H0 n1 n2 x H6 H7).
    lia.
  Qed.

  Definition Rbar_NonnegExpectation {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f : Ts -> Rbar) :=
    LInt_p (ProbSpace_measure prts) f.

  Class Rbar_NonnegativeFunction {Ts}
          (rv_X:Ts->Rbar) : Prop :=
    nnf : forall (x:Ts), (Rbar_le 0 (rv_X x)).

  Lemma Rbar_pos_nonneg {Ts} (f : Ts -> Rbar)
        (nnf : Rbar_NonnegativeFunction f) :
    non_neg f.
  Proof.
    easy.
  Qed.

  Lemma measurable_fun_sa_sigma {Ts} {dom : SigmaAlgebra Ts} (f : Ts -> Rbar)
        {rv : RandomVariable dom Rbar_borel_sa f} :
     measurable_fun_Rbar sa_sigma f.
  Proof.
    unfold measurable_fun_Rbar, measurable_fun.
    intros.
    unfold RandomVariable in rv.
    rewrite <- Rbar_borel_sa_preimage2 in rv.
    unfold gen_Rbar, gen_Rbar_cu in H.
    induction H.
    - destruct H.
      apply measurable_gen.
      assert (pre_event_equiv (fun x0 : Ts => A (f x0))
                              (fun x0 => Rbar_ge (f x0) x)) by (intro z; apply H).
      rewrite H0.
      now apply Rbar_sa_le_ge.
    - apply measurable_empty.
    - now apply measurable_compl.
    - now apply measurable_union_countable.
  Qed.

  Lemma Rbar_NonnegExpectation_plus {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f g : Ts -> Rbar)
    {nnf1 : Rbar_NonnegativeFunction f}
    {nnf2 : Rbar_NonnegativeFunction g}
    {rv1 : RandomVariable dom Rbar_borel_sa f}
    {rv2 : RandomVariable dom Rbar_borel_sa g}    :
    inhabited Ts ->
    Rbar_NonnegExpectation prts (fun x => Rbar_plus (f x) (g x)) =
    Rbar_plus (Rbar_NonnegExpectation prts f) (Rbar_NonnegExpectation prts g).
  Proof.
    intros.
    unfold Rbar_NonnegExpectation.
    apply LInt_p_plus; trivial.
    now apply measurable_fun_sa_sigma.
    now apply measurable_fun_sa_sigma.
  Qed.

  Lemma Rbar_NonnegExpectation_finite_ae_finite {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f : Ts -> Rbar)
    {nnf : Rbar_NonnegativeFunction f}
    {rv : RandomVariable dom Rbar_borel_sa f} :
    inhabited Ts ->
    is_finite (Rbar_NonnegExpectation prts f) ->
    ae (ProbSpace_measure prts) (fun x => is_finite (f x)).
  Proof.
    intros.
    apply LInt_p_ae_finite; trivial.
    now apply measurable_fun_sa_sigma.
  Qed.

  Lemma is_finite_ps_P  {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) :
    is_finite_measure (ProbSpace_measure prts).
  Proof.
    unfold is_finite_measure, ProbSpace_measure; simpl.
    generalize (sa_all); intros.
    now rewrite ps_P_pre_sa_sigma with (sa := H).
  Qed.

  Lemma sa_sigma_is_finite {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f : Ts -> Rbar)
    {nnf : Rbar_NonnegativeFunction f}
    {rv : RandomVariable dom Rbar_borel_sa f} :
    sa_sigma (fun x => is_finite (f x)).
  Proof.
    intros.
    assert (pre_event_equiv (fun x => is_finite (f x))
                            (fun x => Rbar_lt (f x) p_infty)).
    {
      intro x.
      case_eq (f x); intros.
      - now simpl.
      - now simpl.
      - specialize (nnf x).
        rewrite H in nnf.
        now simpl in nnf.
    }
    rewrite H.
    apply Rbar_sa_le_lt.
    unfold RandomVariable in rv.
    now apply Rbar_borel_sa_preimage2.
  Qed.

  Lemma Rbar_NonnegExpectation_finite_ps_P_1 {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f : Ts -> Rbar)
    {nnf : Rbar_NonnegativeFunction f}
    {rv : RandomVariable dom Rbar_borel_sa f} :
    inhabited Ts ->
    is_finite (Rbar_NonnegExpectation prts f) ->
    ps_P (exist sa_sigma (fun x => is_finite (f x)) (sa_sigma_is_finite prts f)) = 1.
  Proof.
    intros.
    generalize (Rbar_NonnegExpectation_finite_ae_finite prts f H H0); intros.
    unfold ae in H1.
    unfold negligible in H1.
    destruct H1 as [? [? [? ?]]].
    unfold ProbSpace_measure in H3; simpl in H3.
    apply measurable_pre_event in H2.
    rewrite ps_P_pre_sa_sigma with (sa := H2) in H3.
    assert (1 - ps_P (exist sa_sigma (fun x0 => is_finite (f x0)) (sa_sigma_is_finite prts f)) = 0).
    {
      rewrite <- ps_complement.
      generalize (ps_sub prts
                         (event_complement (exist sa_sigma (fun x0 => is_finite (f x0)) (sa_sigma_is_finite prts f)))
                         (exist sa_sigma x H2)); intros.
      cut_to H4.
      - generalize (ps_pos (event_complement (exist sa_sigma (fun x0 => is_finite (f x0)) (sa_sigma_is_finite prts f)))); intros.
        apply Rbar_finite_eq in H3.
        rewrite H3 in H4.
        lra.
      - intro z; simpl.
        apply H1.
    }
    lra.
  Qed.

  Lemma Rbar_NonnegExpectation_Sup_seq {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom) (f : nat -> Ts -> Rbar)
    {nnf : forall n, Rbar_NonnegativeFunction (f n)}
    {rv : forall n, RandomVariable dom Rbar_borel_sa (f n)} :
    inhabited Ts ->
    (forall x n, Rbar_le (f n x) (f (S n) x)) ->
    Rbar_NonnegExpectation prts (fun x => Sup_seq (fun n => f n x)) =
    Sup_seq (fun n => Rbar_NonnegExpectation prts (f n)).
  Proof.
    intros.
    apply Beppo_Levi; trivial.
    intros.
    now apply measurable_fun_sa_sigma.
  Qed.

  Lemma Rbar_NonnegExpectation_monotone {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom)
        (f g : Ts -> Rbar) :
    (forall x, Rbar_le (f x) (g x)) ->
    Rbar_le (Rbar_NonnegExpectation prts f) (Rbar_NonnegExpectation prts g).
  Proof.
    apply LInt_p_monotone.
  Qed.

  Lemma measurable_fun_rv {Ts} {dom : SigmaAlgebra Ts} (f : Ts -> Rbar) :
    measurable_fun_Rbar sa_sigma f ->
    RandomVariable dom Rbar_borel_sa f.
  Proof.
    unfold measurable_fun_Rbar, RandomVariable.
    intro mfun.
    apply Rbar_borel_sa_preimage2.
    apply Rbar_sa_ge_le.
    intros.

    unfold gen_Rbar, gen_Rbar_cu in mfun.
    unfold measurable_fun in mfun.
    specialize (mfun (fun x => Rbar_ge x r)).
    induction mfun; trivial.
    - apply sa_none.
    - generalize sa_complement; intros.
      apply sa_complement in IHm.
      assert (pre_event_equiv (pre_event_complement (fun x : Ts => ~ A x)) A).
      {
        intro x.
        unfold pre_event_complement.
        tauto.
      }
      now rewrite H0 in IHm.
    - now apply sa_countable_union.
    - apply measurable_gen.
      exists r.
      now unfold Rbar_ge.
  Qed.

  Lemma measurable_lim_seq' {Ts} (dom : SigmaAlgebra Ts)
        (f : nat -> Ts -> Rbar)
        (nnf: forall n, Rbar_NonnegativeFunction (f n))
        (rv : forall n, RandomVariable dom Rbar_borel_sa (f n)) :
    RandomVariable dom Rbar_borel_sa (fun x => Lim_seq' (fun n => f n x)).
  Proof.
    assert (forall n, measurable_fun_Rbar sa_sigma (f n)) by
        (intros; now apply measurable_fun_sa_sigma).
    apply measurable_fun_rv.
    now apply measurable_fun_Lim_seq'.
  Qed.

  Lemma Rbar_NonnegExpectation_Lim_seq' {Ts} {dom : SigmaAlgebra Ts} (prts : ProbSpace dom)
        (f : nat -> Ts -> Rbar)
        (nnf : forall n, Rbar_NonnegativeFunction (f n))
        (rv : forall n, RandomVariable dom Rbar_borel_sa (f n)) :
        inhabited Ts ->
        (forall x, ex_lim_seq' (fun n => f n x)) ->
        let lim_f := fun x => Lim_seq' (fun n => f n x) in
        (forall x n, Rbar_le (f n x) (lim_f x)) ->
        Rbar_NonnegExpectation prts lim_f = Lim_seq' (fun n => Rbar_NonnegExpectation prts (f n)).
  Proof.
    intros.
    apply LInt_p_Lim_seq'; trivial.
    intros.
    now apply measurable_fun_sa_sigma.
  Qed.

author: IBM

repo: FormalML

save_path: github-repos/coq/IBM-FormalML


text:
From Goose.github_com.mit_pdos.go_journal Require Import wal.

From Perennial.Helpers Require Import List.
From Perennial.program_proof Require Export wal.abstraction.
From Perennial.program_proof Require Import disk_prelude disk_lib.
From Perennial.program_proof Require util_proof.

Section heap.
Context `{!heapGS Σ}.
Definition update_val (up:u64*Slice.t): val :=
  (#(fst up), (slice_val (snd up), #()))%V.

Theorem update_val_t u : val_ty (update_val u) (struct.t Update).
Proof.
  repeat constructor.
  destruct u; rewrite /blockT; val_ty.
Qed.

Hint Resolve update_val_t : core.

Definition is_update (uv: u64*Slice.t) (q:Qp) (u: update.t): iProp Σ :=
  ⌜uv.1 = u.(update.addr)⌝ ∗
  is_block uv.2 q u.(update.b).

Theorem is_update_addr uv q u :
  is_update uv q u -∗ ⌜uv.1 = u.(update.addr)⌝.
Proof.
  iIntros "[$ _]".
Qed.

Definition updates_slice' q (bk_s: Slice.t) (bs: list update.t): iProp Σ :=
  ∃ bks, is_slice bk_s (struct.t Update) 1 (update_val <$> bks) ∗
   [∗ list] _ ↦ b_upd;upd ∈ bks;bs , let '(update.mk a b) := upd in
                                     is_block (snd b_upd) q b ∗
                                     ⌜fst b_upd = a⌝.

Definition updates_slice (bk_s: Slice.t) (bs: list update.t): iProp Σ :=
  updates_slice' 1 bk_s bs.

Definition updates_slice_frag' (bk_s: Slice.t) (q1 q2:Qp) (bs: list update.t): iProp Σ :=
  ∃ bks, is_slice_small bk_s (struct.t Update) q1 (update_val <$> bks) ∗
   [∗ list] _ ↦ uv;upd ∈ bks;bs, is_update uv q2 upd.

Definition updates_slice_frag (bk_s: Slice.t) (q:Qp) (bs: list update.t): iProp Σ :=
  updates_slice_frag' bk_s q q bs.

Theorem updates_slice_cap_acc' bk_s q bs :
  updates_slice' q bk_s bs ⊣⊢
  updates_slice_frag' bk_s 1 q bs ∗ is_slice_cap bk_s (struct.t Update).
Proof.
  iSplit.
  - iIntros "Hupds".
    iDestruct "Hupds" as (bks) "[Hbks Hupds]".
    iDestruct (is_slice_split with "Hbks") as "[Hbks_small $]".
    iExists _; iFrame.
    iApply (big_sepL2_mono with "Hupds").
    intros ? ? [a b] **.
      by iIntros "[$ %]".
  - iIntros "[Hupds Hcap]".
    iDestruct "Hupds" as (bks) "[Hbks Hupds]".
    iDestruct (is_slice_split with "[$Hbks $Hcap]") as "Hbks".
    iExists _; iFrame.
    iApply (big_sepL2_mono with "Hupds").
    intros ? ? [a b] **.
      by iIntros "[% $]".
Qed.

Theorem updates_slice_cap_acc bk_s bs :
  updates_slice bk_s bs ⊣⊢
  updates_slice_frag bk_s 1 bs ∗ is_slice_cap bk_s (struct.t Update).
Proof. iApply updates_slice_cap_acc'. Qed.

Theorem updates_slice_frag_acc q bk_s bs :
  updates_slice' q bk_s bs -∗
  updates_slice_frag' bk_s 1 q bs ∗
   (∀ bs', updates_slice_frag' bk_s 1 q bs' -∗ updates_slice' q bk_s bs').
Proof.
  iIntros "Hupds".
  rewrite updates_slice_cap_acc'.
  iDestruct "Hupds" as "[$ Hcap]".
  iIntros (bs') "Hupds".
  rewrite updates_slice_cap_acc'.
  iFrame.
Qed.

Theorem updates_slice_to_frag bk_s q bs :
  updates_slice' q bk_s bs -∗
  updates_slice_frag' bk_s 1 q bs.
Proof.
  rewrite updates_slice_cap_acc'.
  iIntros "[$ _]".
Qed.

Lemma updates_slice_frag_len bk_s q1 q2 bs :
  updates_slice_frag' bk_s q1 q2 bs -∗ ⌜int.Z bk_s.(Slice.sz) = length bs⌝.
Proof.
  iIntros "Hupds".
  iDestruct "Hupds" as (bks) "[Hbs Hbks]".
  iDestruct (is_slice_small_sz with "Hbs") as %Hbs_sz.
  iDestruct (big_sepL2_length with "Hbks") as %Hbks_len.
  rewrite fmap_length in Hbs_sz.
  iPureIntro.
  rewrite -Hbks_len.
  rewrite Hbs_sz.
  destruct bk_s; simpl.
  word.
Qed.

Lemma updates_slice_frag_wf bk_s q1 q2 bs :
  updates_slice_frag' bk_s q1 q2 bs -∗ ⌜int.Z bk_s.(Slice.sz) ≤ int.Z bk_s.(Slice.cap)⌝.
Proof.
  iIntros "Hupds".
  iDestruct "Hupds" as (bks) "[Hbs Hbks]".
  iDestruct (is_slice_small_wf with "Hbs") as %Hbs_wf.
  auto.
Qed.

Lemma updates_slice_len bk_s q bs :
  updates_slice' q bk_s bs -∗ ⌜int.Z bk_s.(Slice.sz) = length bs⌝.
Proof.
  iIntros "Hupds".
  iDestruct (updates_slice_frag_acc with "Hupds") as "[Hupds _]".
  iDestruct (updates_slice_frag_len with "Hupds") as %Hlen.
  auto.
Qed.

Lemma updates_slice_wf bk_s q bs :
  updates_slice' q bk_s bs -∗ ⌜int.Z bk_s.(Slice.sz) ≤ int.Z bk_s.(Slice.cap)⌝.
Proof.
  iIntros "Hupds".
  iDestruct (updates_slice_frag_acc with "Hupds") as "[Hupds _]".
  iDestruct (updates_slice_frag_wf with "Hupds") as %Hwf.
  auto.
Qed.

Existing Instance is_slice_small_as_fractional.

Global Instance fractional_big_sepL2:
  ∀ (PROP : bi) (A B : Type) (l1 : list A) (l2: list B) (Ψ : nat → A → B -> Qp → PROP),
    (∀ (k : nat) (x : A) (y:B), fractional.Fractional (Ψ k x y))
    → fractional.Fractional (λ q : Qp, ([∗ list] k↦x;y ∈ l1; l2, Ψ k x y q)%I).
Proof.
  intros.
  intros q1 q2.
  rewrite -big_sepL2_sep.
  setoid_rewrite H.
  auto.
Qed.

Instance is_blocks_AsFractional bks q v :
  fractional.AsFractional
    ([∗ list] b_upd;upd ∈ bks;v, is_update b_upd q upd)
    (λ q, [∗ list] b_upd;upd ∈ bks;v, is_update b_upd q upd)%I
    q.
Proof.
  constructor; auto.
  apply _.
Qed.

Global Instance update_into_val : IntoVal (u64 * Slice.t).
Proof.
  refine {| to_val := update_val;
           from_val := λ v, match v with
                            | (#(LitInt a), (slice_v, #()))%V =>
                                match from_val slice_v with
                                | Some s => Some (a, s)
                                | None => None
                                end
                            | _ => None
                            end;
           IntoVal_def := (U64 0, IntoVal_def Slice.t);
         |}.
  destruct v as [a []]; done.
Defined.

Global Instance update_into_val_for_type : IntoValForType (u64 * Slice.t) (uint64T * (blockT * unitT)%ht).
Proof. constructor; simpl; done. Qed.

Instance update_val_inj : Inj eq eq update_val.
Proof.
  intros u1 u2.
  rewrite /update_val.
  destruct u1, u2; simpl.
  destruct t, t0; simpl in *; subst.
  inversion 1; subst.
  congruence.
Qed.

Global Instance updates_slice_frag_fractional bk_s q bs :
  fractional.AsFractional (updates_slice_frag bk_s q bs) (λ q, updates_slice_frag bk_s q bs) q.
Proof.
  split; auto.
  hnf; intros q1 q2.
  iSplit.
  + iIntros "Hupds".
    iDestruct "Hupds" as (bks) "[Hupds Hbs]".
    iDestruct (fractional.fractional_split_1 with "Hupds") as "[Hupds1 Hupds2]".
    iDestruct (fractional.fractional_split_1 with "Hbs") as "[Hbs1 Hbs2]".
    iSplitL "Hupds1 Hbs1".
    * iExists _; iFrame.
    * iExists _; iFrame.
  + iIntros "[Hupds1 Hupds2]".
    iDestruct "Hupds1" as (bks) "[Hbs1 Hupds1]".
    iDestruct "Hupds2" as (bks') "[Hbs2 Hupds2]".
    iDestruct (is_slice_small_agree with "Hbs1 Hbs2") as %Heq.
    apply (fmap_inj update_val) in Heq; auto using update_val_inj; subst.
    iDestruct (fractional.fractional_split_2 with "Hbs1 Hbs2") as "Hbs".
    { apply _. }
    iDestruct (fractional.fractional_split_2 _ _ _ _ q1 q2 with "Hupds1 Hupds2") as "Hupds".
    { apply _. }
    iExists _; iFrame.
Qed.

Global Instance updates_slice_frag_AsMapsTo bk_s bs :
  AsMapsTo (updates_slice_frag bk_s 1 bs) (λ q, updates_slice_frag bk_s q bs).
Proof.
  constructor; auto; intros; apply _.
  Unshelve.
  exact 1%Qp.
Qed.

Theorem wp_SliceGet_updates stk E bk_s bs (i: u64) q (u: update.t) :
  {{{ updates_slice_frag bk_s q bs ∗ ⌜bs !! int.nat i = Some u⌝ }}}
    SliceGet (struct.t Update) (slice_val bk_s) #i @ stk; E
  {{{ uv, RET (update_val uv);
      is_update uv q u ∗
      (is_block uv.2 q u.(update.b) -∗ updates_slice_frag bk_s q bs)
  }}}.
Proof.
  iIntros (Φ) "[Hupds %Hlookup] HΦ".
  iDestruct "Hupds" as (bks) "[Hbk_s Hbks]".
  iDestruct (big_sepL2_lookup_2_some _ _ _ _ _ Hlookup with "Hbks")
    as %[b_upd Hlookup_bs].
  wp_apply (wp_SliceGet with "[$Hbk_s]").
  { iPureIntro.
    rewrite list_lookup_fmap.
    rewrite Hlookup_bs //. }
  iIntros "[Hbk_s _]".
  iApply "HΦ".
  iDestruct (big_sepL2_lookup_acc with "Hbks") as "[Hbi Hbks]"; eauto.
  destruct u as [a b]; simpl.
  iDestruct "Hbi" as "[%Heq Hbi]".
  iSplitL "Hbi".
  { by iFrame. }
  iIntros "Hbi".
  iSpecialize ("Hbks" with "[$Hbi //]").
  iExists _; iFrame.
Qed.

Theorem wp_SliceSet_updates stk E bk_s q_b bs (i: u64) (u0 u: update.t) uv :
  bs !! int.nat i = Some u0 ->
  {{{ updates_slice_frag' bk_s 1 q_b bs ∗ is_update uv q_b u }}}
    SliceSet (struct.t Update) (slice_val bk_s) #i (update_val uv) @ stk; E
  {{{ RET #(); updates_slice_frag' bk_s 1 q_b (<[int.nat i := u]> bs)
  }}}.
Proof.
  iIntros (Hlookup Φ) "[Hupds Hu] HΦ".
  iDestruct "Hupds" as (bks) "[Hbk_s Hbks]".
  iDestruct (big_sepL2_length with "Hbks") as %Hlen.
  assert (exists uv0, bks !! int.nat i = Some uv0) as [uv0 Hlookup_bks].
  { apply lookup_lt_Some in Hlookup.
    apply list_lookup_lt.
    lia. }
  iDestruct (big_sepL2_insert_acc _ _ _ _ _ _ Hlookup_bks Hlookup with "Hbks")
    as "[Hbki Hbks]".
  wp_apply (wp_SliceSet with "[$Hbk_s]").
  { iPureIntro.
    split; last val_ty.
    rewrite list_lookup_fmap.
    apply fmap_is_Some.
    eauto. }
  iIntros "Hbk_s".
  iApply "HΦ".
  iSpecialize ("Hbks" with "[$Hu //]").
  rewrite -list_fmap_insert.
  iExists _; iFrame.
Qed.

Theorem wp_SliceSet_updates' stk E bk_s q_b bs (i: u64) (u0 u: update.t) uv :
  bs !! int.nat i = Some u0 ->
  {{{ updates_slice_frag' bk_s 1 q_b bs ∗ is_update uv q_b u }}}
    SliceSet (struct.t Update) (slice_val bk_s) #i (update_val uv) @ stk; E
  {{{ RET #(); updates_slice_frag' bk_s 1 q_b (<[int.nat i := u]> bs)
  }}}.
Proof.
  iIntros (Hlookup Φ) "[Hupds Hu] HΦ".
  iDestruct "Hupds" as (bks) "[Hbk_s Hbks]".
  iDestruct (big_sepL2_length with "Hbks") as %Hlen.
  assert (exists uv0, bks !! int.nat i = Some uv0) as [uv0 Hlookup_bks].
  { apply lookup_lt_Some in Hlookup.
    apply list_lookup_lt.
    lia. }
  iDestruct (big_sepL2_insert_acc _ _ _ _ _ _ Hlookup_bks Hlookup with "Hbks")
    as "[Hbki Hbks]".
  wp_apply (wp_SliceSet with "[$Hbk_s]").
  { iPureIntro.
    split; auto.
    rewrite list_lookup_fmap.
    apply fmap_is_Some.
    eauto. }
  iIntros "Hbk_s".
  iApply "HΦ".
  iSpecialize ("Hbks" with "[$Hu //]").
  rewrite -list_fmap_insert.
  iExists _; iFrame.
Qed.

Lemma has_zero_update : has_zero (struct.t Update).
Proof.
  repeat constructor.
Qed.

Hint Resolve has_zero_update : core.

Theorem wp_SliceAppend_updates {stk E bk_s q bs} {uv: u64 * Slice.t} {b} :
  {{{ updates_slice' q bk_s bs ∗ is_block uv.2 q b }}}
    SliceAppend (struct.t Update) (slice_val bk_s) (update_val uv) @ stk; E
  {{{ bk_s', RET slice_val bk_s';
      updates_slice' q bk_s' (bs ++ [update.mk uv.1 b])
  }}}.
Proof.
  iIntros (Φ) "[Hupds Hub] HΦ".
  iDestruct (updates_slice_len with "Hupds") as %Hlen.
  iDestruct "Hupds" as (bks) "[Hbks Hupds]".
  wp_apply (wp_SliceAppend with "[$Hbks]"); auto.
  iIntros (s') "Hs".
  iApply "HΦ".
  change ([update_val uv]) with (update_val <$> [uv]).
  rewrite -fmap_app.
  rewrite /updates_slice.
  iExists (bks ++ [uv]).
  iFrame "Hs".
  iApply (big_sepL2_app with "Hupds").
  simpl. auto.
Qed.

Theorem wp_SliceAppend_updates_frag {stk E bk_s bs} {uv: u64 * Slice.t} {b} (n : u64) (q q_b q_b' : Qp) :
  0 ≤ int.Z n ≤ int.Z (Slice.sz bk_s) ≤ int.Z (Slice.cap bk_s) ->
  (q < 1)%Qp ->
  {{{ updates_slice_frag' (slice_take bk_s n) q q_b (take (int.nat n) bs) ∗
      updates_slice' q_b' (slice_skip bk_s (struct.t Update) n) (drop (int.nat n) bs) ∗
      is_block uv.2 q_b' b }}}
    SliceAppend (struct.t Update) (slice_val bk_s) (update_val uv) @ stk; E
  {{{ bk_s', RET slice_val bk_s';
      updates_slice_frag' (slice_take bk_s' n) q q_b (take (int.nat n) (bs ++ [update.mk uv.1 b])) ∗
      updates_slice' q_b' (slice_skip bk_s' (struct.t Update) n) (drop (int.nat n) (bs ++ [update.mk uv.1 b])) ∗
      ⌜int.Z (Slice.sz bk_s') ≤ int.Z (Slice.cap bk_s') ∧
       int.Z (Slice.sz bk_s') = (int.Z (Slice.sz bk_s) + 1)%Z⌝
  }}}.
Proof.
  iIntros (Hn Hq Φ) "(Hfrag & Hupds & Hub) HΦ".
  iDestruct (updates_slice_frag_len with "Hfrag") as %Hfraglen.
  iDestruct (updates_slice_len with "Hupds") as %Hlen.
  iDestruct "Hfrag" as (bks1) "[Hbks1 Hfrag]".
  iDestruct "Hupds" as (bks2) "[Hbks2 Hupds]".
  wp_apply (wp_SliceAppend'' with "[$Hbks1 $Hbks2]"); auto.
  iIntros (s') "(Hbks1 & Hbks2 & %Hn')".
  iApply "HΦ".
  change ([update_val uv]) with (update_val <$> [uv]).
  rewrite -fmap_app.
  rewrite /updates_slice /updates_slice_frag.
  iSplitL "Hbks1 Hfrag".
  {
    iExists (bks1).
    iFrame "Hbks1".
    rewrite take_app_le; first by iFrame.
    revert Hfraglen.
    rewrite /slice_take /= take_length. word. }
  iSplitL; last by eauto.
  iExists (bks2 ++ [uv]).
  iFrame "Hbks2".
  rewrite drop_app_le.
  2: { revert Hfraglen. rewrite /slice_take /= take_length. word. }
  iApply (big_sepL2_app with "Hupds").
  simpl. auto.
Qed.

Theorem wp_forSlice_updates (I: u64 -> iProp Σ) stk E s q q_b us (body: val) :
  (∀ (i: u64) (uv: u64 * Slice.t) (u: update.t),
      {{{ I i ∗ ⌜(int.nat i < length us)%nat⌝ ∗
                is_update uv q_b u ∗
                ⌜us !! int.nat i = Some u⌝ }}}
        body #i (update_val uv) @ stk; E
      {{{ RET #(); I (word.add i (U64 1)) ∗
                   is_block uv.2 q_b u.(update.b) }}}) -∗
    {{{ I (U64 0) ∗ updates_slice_frag' s q q_b us }}}
      forSlice (struct.t Update) body (slice_val s) @ stk; E
    {{{ RET #(); I s.(Slice.sz) ∗ updates_slice_frag' s q q_b us }}}.
Proof.
  iIntros "#Hwp".
  iIntros "!>" (Φ) "(I0&Hupds) HΦ".
  iDestruct "Hupds" as (bks) "(Hs&Hbs)".
  iDestruct (is_slice_small_sz with "Hs") as %Hslen.
  autorewrite with len in Hslen.
  iDestruct (big_sepL2_length with "Hbs") as %Hlen_eq.
  wp_apply (wp_forSlice
              (fun i => I i ∗
               [∗ list] b_upd;upd ∈ bks;us, is_update b_upd q_b upd)%I
    with "[] [$I0 $Hs $Hbs]").
  {
    clear Φ.
    iIntros (i x).
    iIntros "!>" (Φ) "[(HI&Hbs) %] HΦ".
    destruct H as [Hbound Hlookup].
    rewrite list_lookup_fmap in Hlookup.
    apply fmap_Some_1 in Hlookup as [uv [Hlookup ->]].
    list_elem us i as u.
    iDestruct (big_sepL2_lookup_acc with "Hbs") as "[[% Hb] Hbs]"; eauto.
    wp_apply ("Hwp" with "[$HI $Hb]").
    - iPureIntro.
      split; auto.
      word.
    - iIntros "(HI&Hb)".
      iSpecialize ("Hbs" with "[$Hb //]").
      iApply ("HΦ" with "[$]").
  }
  iIntros "[(HI&Hbs) Hs]".
  iApply "HΦ".
  iFrame.
  iExists _; iFrame.
Qed.

Theorem wp_forSlice_updates_consume {stk E}
        (I: u64 -> iProp Σ) s q q_b us (body: val) :
  (∀ (i: u64) (uv: u64 * Slice.t) (u: update.t),
      {{{ I i ∗ ⌜(int.nat i < length us)%nat⌝ ∗
                is_update uv q_b u ∗
                ⌜us !! int.nat i = Some u⌝ }}}
        body #i (update_val uv) @ stk; E
      {{{ RET #(); I (word.add i (U64 1)) }}}) -∗
    {{{ I (U64 0) ∗ updates_slice_frag' s q q_b us }}}
      forSlice (struct.t Update) body (slice_val s) @ stk; E
    {{{ RET #(); I s.(Slice.sz) }}}.
Proof.
  iIntros "#Hwp".
  iIntros "!>" (Φ) "(I0&Hupds) HΦ".
  iDestruct "Hupds" as (bks) "(Hs&Hbs)".
  iDestruct (is_slice_small_sz with "Hs") as %Hslen.
  autorewrite with len in Hslen.
  iDestruct (big_sepL2_length with "Hbs") as %Hlen_eq.
  wp_apply (wp_forSlice
              (fun i => I i ∗
                       [∗ list] b_upd;upd ∈ (drop (int.nat i) bks);(drop (int.nat i) us),
                                            is_update b_upd q_b upd)%I
              with "[] [$I0 $Hs $Hbs]").
  {
    clear Φ.
    iIntros (i x).
    iIntros "!>" (Φ) "[(HI&Hbs) %] HΦ".
    destruct H as [Hbound Hlookup].
    rewrite list_lookup_fmap in Hlookup.
    apply fmap_Some_1 in Hlookup as [uv [Hlookup ->]].
    list_elem us i as u.
    erewrite (drop_S bks); eauto.
    erewrite (drop_S us); eauto.
    simpl.
    iDestruct "Hbs" as "[[% Hb] Hbs]".
    wp_apply ("Hwp" with "[$HI $Hb]").
    - iPureIntro.
      split; auto.
      word.
    - iIntros "HI".
      iApply "HΦ".
      iFrame.
      iExactEq "Hbs".
      repeat (f_equal; try word).
  }
  iIntros "[(HI&Hbs) Hs]".
  iApply "HΦ".
  iFrame.
Qed.

(* TODO(tej): not actually used *)
Theorem wp_forSlicePrefix_updates (I: list update.t -> list update.t -> iProp Σ) stk E s q us (body: val) :
  (∀ (i: u64) (uv: u64 * Slice.t) (u: update.t) (upds upds': list update.t),
      {{{ I upds (u :: upds') ∗
            is_update uv q u ∗
            ⌜(int.nat i < length us)%nat⌝ ∗
            ⌜us !! int.nat i = Some u⌝ ∗
            ⌜upds ++ u :: upds' = us⌝ ∗
            ⌜length upds = int.nat i⌝ }}}
        body #i (update_val uv) @ stk; E
      {{{ RET #(); I (upds ++ [u]) upds' ∗
                   is_block uv.2 q u.(update.b) }}}) -∗
    {{{ I [] us ∗ updates_slice_frag s q us }}}
      forSlice (struct.t Update) body (slice_val s) @ stk; E
    {{{ RET #(); I us [] ∗ updates_slice_frag s q us }}}.
Proof.
  iIntros "#Hwp".
  iIntros "!>" (Φ) "[HI Hupds] HΦ".
  iDestruct (updates_slice_frag_len with "Hupds") as %Hsz.
  wp_apply (wp_forSlice_updates
              (λ i, I (take (int.nat i) us) (drop (int.nat i) us))
              with "[] [$HI $Hupds]").
  {
    clear Φ.
    iIntros (i uv u) "!>".
    iIntros (Φ) "(HI&%&Hu&%) HΦ".
    wp_apply ("Hwp" with "[HI $Hu]").
    { rewrite (drop_S _ _ _ H0). iFrame.
      iPureIntro.
      split_and!; auto; len.
      rewrite take_drop_middle; auto.
    }
    iIntros "(HI&Hu)".
    iApply "HΦ"; iFrame.
    iExactEq "HI".
    f_equal; auto.
    - apply take_S_r in H0. rewrite -H0. f_equal. word.
    - f_equal; word.
  }
  rewrite -> take_ge, drop_ge by word.
  iFrame.
Qed.

Theorem wp_forSlicePrefix_updates_consume {stk E}
        (I: list update.t -> list update.t -> iProp Σ)
        s q q_b us (body: val) :
  (∀ (i: u64) (uv: u64 * Slice.t) (u: update.t) (upds upds': list update.t),
      {{{ I upds (u :: upds') ∗
            is_update uv q_b u ∗
            ⌜(int.nat i < length us)%nat⌝ ∗
            ⌜us !! int.nat i = Some u⌝ ∗
            ⌜upds ++ u :: upds' = us⌝ ∗
            ⌜length upds = int.nat i⌝ }}}
        body #i (update_val uv) @ stk; E
      {{{ RET #(); I (upds ++ [u]) upds' }}}) -∗
    {{{ I [] us ∗ updates_slice_frag' s q q_b us }}}
      forSlice (struct.t Update) body (slice_val s) @ stk; E
    {{{ RET #(); I us [] }}}.
Proof.
  iIntros "#Hwp".
  iIntros "!>" (Φ) "[HI Hupds] HΦ".
  iDestruct (updates_slice_frag_len with "Hupds") as %Hsz.
  wp_apply (wp_forSlice_updates_consume
              (λ i, I (take (int.nat i) us) (drop (int.nat i) us))
              with "[] [$HI $Hupds]").
  {
    clear Φ.
    iIntros (i uv u) "!>".
    iIntros (Φ) "(HI&%&Hu&%) HΦ".
    wp_apply ("Hwp" with "[HI $Hu]").
    { rewrite (drop_S _ _ _ H0). iFrame.
      iPureIntro.
      split_and!; auto; len.
      rewrite take_drop_middle; auto.
    }
    iIntros "HI".
    iApply "HΦ"; iFrame.
    iExactEq "HI".
    f_equal; auto.
    - apply take_S_r in H0. rewrite -H0. f_equal. word.
    - f_equal; word.
  }
  rewrite -> take_ge, drop_ge by word.
  iFrame.
Qed.

Theorem wp_copyUpdateBlock stk E (u: u64 * Slice.t) q b :
  {{{ is_block (snd u) q b }}}
    copyUpdateBlock (update_val u) @ stk; E
  {{{ (s':Slice.t), RET (slice_val s'); is_block (snd u) q b ∗ is_block s' 1 b }}}.
Proof.
  iIntros (Φ) "Hb HΦ".
  destruct u as [a s]; simpl.
  wp_call.
  wp_apply (util_proof.wp_CloneByteSlice with "Hb").
  iIntros (s') "(Hb&Hb')".
  iDestruct (is_slice_to_small with "Hb'") as "Hb'".
  iApply ("HΦ" with "[$]").
Qed.

End heap.

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


(* This probably doesn't belong in progs. Talk to Santiago about where it should go. *)
Require Import progs.conclib.

Class PCM (A : Type) :=
  { join : A -> A -> A -> Prop;
    join_comm : forall a b c (Hjoin : join a b c), join b a c;
    join_assoc : forall a b c d e (Hjoin1 : join a b c) (Hjoin2 : join c d e),
                 exists c', join b d c' /\ join a c' e }.

Section Ghost.

Context {CS : compspecs}.

Section PCM.

Context `{M : PCM}.

(* This is an overapproximation of IRIS's concept of view shift. *)
Definition view_shift A B := forall (Espec : OracleKind) D P Q R C P',
  semax D (PROPx P (LOCALx Q (SEPx (B :: R)))) C P' ->
  semax D (PROPx P (LOCALx Q (SEPx (A :: R)))) C P'.

Section ViewShift.

Axiom view_shift_super_non_expansive : forall n P Q, compcert_rmaps.RML.R.approx n (!!view_shift P Q) =
  compcert_rmaps.RML.R.approx n (!!view_shift (compcert_rmaps.RML.R.approx n P) (compcert_rmaps.RML.R.approx n Q)).

Axiom view_shift_later : forall P Q, view_shift P Q -> view_shift (|>P) (|>Q).

Global Instance view_shift_refl : RelationClasses.Reflexive view_shift.
Proof.
  repeat intro; auto.
Qed.

Global Instance view_shift_trans : RelationClasses.Transitive view_shift.
Proof.
  repeat intro; apply H; auto.
Qed.

Lemma derives_view_shift : forall P Q, P |-- Q -> view_shift P Q.
Proof.
  repeat intro; eapply semax_pre; [|eauto].
  go_lowerx; cancel.
Qed.

Lemma view_shift_sepcon : forall P Q P' Q' (HP : view_shift P P') (HQ : view_shift Q Q'),
  view_shift (P * Q) (P' * Q').
Proof.
  repeat intro.
  rewrite flatten_sepcon_in_SEP in *; apply HP.
  focus_SEP 1; apply HQ.
  focus_SEP 1; auto.
Qed.

Lemma view_shift_exists : forall {A} (P : A -> mpred) Q,
  (forall x, view_shift (P x) Q) -> view_shift (EX x : _, P x) Q.
Proof.
  repeat intro.
  rewrite extract_exists_in_SEP; Intro x.
  apply H; auto.
Qed.

Lemma view_shift_prop : forall (P1 : Prop) P Q,
  (P1 -> view_shift P Q) -> view_shift (!!P1 && P) Q.
Proof.
  repeat intro.
  erewrite extract_prop_in_SEP with (n := O); [|simpl; eauto].
  Intros; simpl; apply H; auto.
Qed.

End ViewShift.

Definition joins a b := exists c, join a b c.

Definition update a b := forall c, joins a c -> joins b c.

(* General PCM-based ghost state *)
Parameter ghost : forall (g : A) (p : val), mpred.

(* subject to change *)
(* We need to make sure we can't allocate invalid ghost state (which would immediately entail False). *)
Axiom ghost_alloc : forall (g : A) P, (exists g', joins g g') -> view_shift P (EX p : val, ghost g p * P).
Axiom ghost_dealloc : forall (g : A) p, view_shift (ghost g p) emp.

Axiom ghost_join : forall g1 g2 g p, join g1 g2 g -> ghost g1 p * ghost g2 p = ghost g p.
Axiom ghost_conflict : forall g1 g2 p, ghost g1 p * ghost g2 p |-- !!joins g1 g2.
Axiom ghost_update : forall g g' p, update g g' -> view_shift (ghost g p) (ghost g' p).
Axiom ghost_inj : forall p g1 g2 r1 r2 r
  (Hp1 : predicates_hered.app_pred (ghost g1 p) r1)
  (Hp1 : predicates_hered.app_pred (ghost g2 p) r2)
  (Hr1 : sepalg.join_sub r1 r) (Hr2 : sepalg.join_sub r2 r),
  r1 = r2 /\ g1 = g2.

Lemma ex_ghost_precise : forall p, precise (EX g : A, ghost g p).
Proof.
  intros ???? (? & ?) (? & ?) ??.
  eapply ghost_inj; eauto.
Qed.

Corollary ghost_precise : forall g p, precise (ghost g p).
Proof.
  intros.
  eapply derives_precise, ex_ghost_precise.
  intros ??; exists g; eauto.
Qed.

End PCM.

(* operations on PCMs *)

Section Ops.

Context {A B : Type} {MA : PCM A} {MB : PCM B}.

Instance prod_PCM : PCM (A * B) := { join a b c := join (fst a) (fst b) (fst c) /\ join (snd a) (snd b) (snd c) }.
Proof.
  - intros ??? (? & ?); split; apply join_comm; auto.
  - intros ????? (? & ?) (HA & HB).
    eapply join_assoc in HA; eauto.
    eapply join_assoc in HB; eauto.
    destruct HA as (c'a & ? & ?), HB as (c'b & ? & ?); exists (c'a, c'b); split; split; auto.
Defined.

(* Two different ways of adding a unit to a PCM. *)
Instance option_PCM : PCM (option A) := { join a b c :=
  match a, b, c with
  | Some a', Some b', Some c' => join a' b' c'
  | Some a', None, Some c' => c' = a'
  | None, Some b', Some c' => c' = b'
  | None, None, None => True
  | _, _, _ => False
  end }.
Proof.
  - destruct a, b, c; auto.
    apply join_comm.
  - destruct a, b, c, d, e; try contradiction; intros; subst;
      try solve [eexists (Some _); split; auto; auto]; try solve [exists None; split; auto].
    eapply join_assoc in Hjoin2; eauto.
    destruct Hjoin2 as (c' & ? & ?); exists (Some c'); auto.
Defined.

Instance exclusive_PCM : PCM (option A) := { join a b c := a = c /\ b = None \/ b = c /\ a = None }.
Proof.
  - tauto.
  - intros ????? [(? & ?) | (? & ?)]; subst; eauto.
Defined.

End Ops.

Global Instance share_PCM : PCM share := { join := sepalg.join }.
Proof.
  - intros; apply sepalg.join_comm; auto.
  - intros.
    eapply sepalg.join_assoc in Hjoin2; eauto.
    destruct Hjoin2; eauto.
Defined.

(* Instances of ghost state *)
Section GVar.

Context {A : Type}.

Lemma join_Bot : forall a b, sepalg.join a b Share.bot -> a = Share.bot /\ b = Share.bot.
Proof.
  intros ?? (? & ?).
  apply lub_bot_e; auto.
Qed.

Global Instance Var_PCM : PCM (share * A) := { join a b c := sepalg.join (fst a) (fst b) (fst c) /\
  (fst a = Share.bot /\ c = b \/ fst b = Share.bot /\ c = a \/ snd a = snd b /\ snd b = snd c) }.
Proof.
  - intros ??? (? & Hcase); split; [apply sepalg.join_comm; auto|].
    destruct Hcase as [? | [? | (-> & ?)]]; auto.
  - intros ????? (? & Hcase1) (Hj2 & Hcase2).
    eapply sepalg.join_assoc in Hj2; eauto.
    destruct Hj2 as (sh & Hj1' & Hj2').
    destruct Hcase2 as [(Hbot & ?) | [(Hbot & ?) | (? & He)]]; subst.
    + rewrite Hbot in H; apply join_Bot in H; destruct H as (Ha & Hb); rewrite Ha in *.
      assert (fst d = sh).
      { eapply sepalg.join_eq; eauto. }
      exists (sh, snd d); split; split; auto; destruct d; subst; auto.
    + rewrite Hbot in *; assert (fst b = sh).
      { eapply sepalg.join_eq; eauto. }
      exists (sh, snd b); split; split; auto; destruct b; subst; auto.
    + destruct Hcase1 as [(Hbot & ?) | [(Hbot & ?) | (? & ?)]]; subst.
      * exists (sh, snd b); split; split; auto; destruct b; subst; auto.
        rewrite Hbot in *; assert (fst e = sh).
        { eapply sepalg.join_eq; eauto. }
        destruct e; subst; simpl in *.
        rewrite He in *; auto.
      * exists (sh, snd d); split; split; auto.
        rewrite Hbot in *; assert (fst d = sh).
        { eapply sepalg.join_eq; eauto. }
        destruct d; auto.
      * rewrite <- He.
        exists (sh, snd d); split; split; auto; destruct d; simpl in *; subst; auto.
        replace (snd a) with (snd b) in *; auto.
Defined.

Lemma joins_id : forall a b, sepalg.joins (fst a) (fst b) -> snd a = snd b -> joins a b.
Proof.
  intros ?? (sh & ?) ?.
  exists (sh, snd a); simpl; auto.
Qed.

Definition ghost_var (sh : share) (v : A) p := ghost (sh, v) p.

Lemma ghost_var_share_join : forall sh1 sh2 sh v p, sepalg.join sh1 sh2 sh ->
  ghost_var sh1 v p * ghost_var sh2 v p = ghost_var sh v p.
Proof.
  intros; apply ghost_join; simpl; auto.
Qed.

Lemma ghost_var_inj : forall sh1 sh2 v1 v2 p, readable_share sh1 -> readable_share sh2 ->
  ghost_var sh1 v1 p * ghost_var sh2 v2 p |-- !!(v1 = v2).
Proof.
  intros.
  eapply derives_trans; [apply ghost_conflict|].
  apply prop_left; intros (? & ? & [(? & ?) | [(? & ?) | (? & ?)]]); simpl in *; subst;
    try (exploit unreadable_bot; eauto; contradiction).
  apply prop_right; auto.
Qed.

Lemma ghost_var_share_join' : forall sh1 sh2 sh v1 v2 p, readable_share sh1 -> readable_share sh2 ->
  sepalg.join sh1 sh2 sh ->
  ghost_var sh1 v1 p * ghost_var sh2 v2 p = !!(v1 = v2) && ghost_var sh v2 p.
Proof.
  intros; apply mpred_ext.
  - assert_PROP (v1 = v2) by (apply ghost_var_inj; auto).
    subst; erewrite ghost_var_share_join; eauto; entailer!.
  - Intros; subst.
    erewrite ghost_var_share_join; eauto.
Qed.

Lemma join_Tsh : forall a b, sepalg.join Tsh a b -> b = Tsh /\ a = Share.bot.
Proof.
  intros ?? (? & ?).
  rewrite Share.glb_commute, Share.glb_top in H; subst; split; auto.
  apply Share.lub_bot.
Qed.

Lemma ghost_var_update : forall v p v', view_shift (ghost_var Tsh v p) (ghost_var Tsh v' p).
Proof.
  intros; apply ghost_update; intros ? (? & ? & Hcase); simpl in *.
  apply join_Tsh in H; destruct H as (? & Hbot).
  exists (Tsh, v'); simpl; split; auto.
  rewrite Hbot; auto.
Qed.

Lemma ghost_var_precise : forall sh p, precise (EX v : A, ghost_var sh v p).
Proof.
  intros; eapply derives_precise, ex_ghost_precise.
  intros ? (x & ?); exists (sh, x); eauto.
Qed.

Lemma ghost_var_precise' : forall sh v p, precise (ghost_var sh v p).
Proof.
  intros; apply derives_precise with (Q := EX v : A, ghost_var sh v p);
    [exists v; auto | apply ghost_var_precise].
Qed.

Lemma ghost_var_init : forall (g : share * A), exists g', joins g g'.
Proof.
  intros (sh, a); exists (Share.bot, a), (sh, a); simpl; auto.
Qed.

End GVar.

Section Reference.
(* One common kind of PCM is one in which a central authority has a reference copy, and clients pass around
   partial knowledge. When a client recovers all pieces, it can gain full knowledge. *)
(* This is related to the snapshot PCM, but the parts have different types. *)

Context `{P : PCM}.

Instance pos_PCM : PCM (option (share * A)) := { join a b c :=
  match a, b, c with
  | Some (sha, a'), Some (shb, b'), Some (shc, c') =>
      sha <> Share.bot /\ shb <> Share.bot /\ sepalg.join sha shb shc /\ join a' b' c'
  | Some (sha, a'), None, Some c' => sha <> Share.bot /\ c' = (sha, a')
  | None, Some (shb, b'), Some c' => shb <> Share.bot /\ c' = (shb, b')
  | None, None, None => True
  | _, _, _ => False
  end }.
Proof.
  - destruct a as [(?, ?)|], b as [(?, ?)|], c as [(?, ?)|]; auto.
    intros (? & ? & ? & ?); repeat (split; auto); apply join_comm; auto.
  - destruct a as [(?, ?)|], b as [(?, ?)|], c as [(?, ?)|], d as [(?, ?)|], e as [(?, ?)|]; try contradiction;
      intros; decompose [and] Hjoin1; decompose [and] Hjoin2;
      repeat match goal with H : (_, _) = (_, _) |- _ => inv H end;
      try solve [eexists (Some _); split; auto; auto]; try solve [exists None; split; auto].
    + destruct (@sepalg.join_assoc _ _ _ s s0 s2 s1 s3) as (sh' & ? & ?); auto.
      destruct (join_assoc a a0 a1 a2 a3) as (a' & ? & ?); auto.
      exists (Some (sh', a')); repeat (split; auto).
      intro; subst.
      exploit join_Bot; eauto; tauto.
    + exists (Some (s2, a2)); repeat (split; auto).
      intro; subst.
      exploit join_Bot; eauto; tauto.
Defined.

Definition completable a r := exists x, join a x (Some (Tsh, r)).

Global Instance ref_PCM : PCM (option (share * A) * option A) :=
  { join a b c := join (fst a) (fst b) (fst c) /\ @join _ exclusive_PCM (snd a) (snd b) (snd c) /\
      match snd c with Some r => completable (fst c) r | None => True end }.
Proof.
  - intros ??? (Hfst & Hsnd & ?).
    split; [|split]; try apply join_comm; auto.
  - intros ????? (Hfst1 & Hsnd1 & Hcase1) (Hfst2 & Hsnd2 & Hcase2).
    destruct (join_assoc _ _ _ _ _ Hfst1 Hfst2) as (c'1 & ? & Hc'1).
    destruct (join_assoc _ _ _ _ _ Hsnd1 Hsnd2) as (c'2 & ? & Hc'2).
    exists (c'1, c'2).
    destruct Hc'2 as [(He & ?) | (? & ?)]; subst; [repeat split; simpl; auto|].
    repeat split; try solve [simpl; auto].
    simpl snd; destruct (snd e); auto.
    unfold completable.
    destruct Hcase2 as (? & Hcase2).
    apply join_comm in Hc'1.
    destruct (join_assoc _ _ _ _ _ Hc'1 Hcase2) as (? & ? & ?); eauto.
Defined.

Lemma ref_sub : forall (sh : share) (a b : A) p,
  ghost (Some (sh, a), @None A) p * ghost (@None (share * A), Some b) p |--
    !!(if eq_dec sh Tsh then a = b else exists x, join a x b).
Proof.
  intros.
  eapply derives_trans; [apply ghost_conflict|].
  apply prop_left; intros (c & Hjoin & [(? & ?) | (Hc & ?)] & Hcompat); [discriminate | apply prop_right].
  rewrite <- Hc in Hcompat; destruct Hcompat as (c' & Hsub).
  simpl in Hjoin.
  destruct (fst c); [|contradiction].
  destruct Hjoin; subst.
  simpl in Hsub.
  destruct c' as [(?, ?)|].
  - destruct Hsub as (? & ? & Hsh & ?).
    if_tac; eauto; subst.
    apply join_Tsh in Hsh; tauto.
  - destruct Hsub as (? & Hsub); inv Hsub.
    rewrite eq_dec_refl; auto.
Qed.

End Reference.

Class PCM_order `{P : PCM} (ord : A -> A -> Prop) := { ord_refl :> RelationClasses.Reflexive ord;
  ord_trans :> RelationClasses.Transitive ord;
  join_ord : forall a b c, join a b c -> ord a c /\ ord b c; ord_join : forall a b, ord b a -> join a b a }.

Section Snapshot.
(* One common kind of PCM is one in which a central authority has a reference copy, and clients pass around
   partial knowledge. *)

Context `{ORD : PCM_order}.

Definition lift_ord a b := match a with Some a => ord a b | None => True end.

Lemma join_lift_ord : forall a b c, @join _ option_PCM a b (Some c) -> lift_ord a c /\ lift_ord b c.
Proof.
  simpl; intros.
  destruct a, b; subst; simpl; try apply join_ord; try split; auto; reflexivity.
Qed.

Global Instance snap_PCM : PCM (option A * option A) :=
  { join a b c := @join _ option_PCM (fst a) (fst b) (fst c) /\ @join _ exclusive_PCM (snd a) (snd b) (snd c) /\
      match snd c with Some r => lift_ord (fst c) r | None => True end }.
Proof.
  - intros ??? (Hfst & Hsnd & ?).
    split; [|split]; try apply join_comm; auto.
  - intros ????? (Hfst1 & Hsnd1 & Hcase1) (Hfst2 & Hsnd2 & Hcase2).
    destruct (join_assoc _ _ _ _ _ Hfst1 Hfst2) as (c'1 & ? & Hc'1).
    destruct (join_assoc _ _ _ _ _ Hsnd1 Hsnd2) as (c'2 & ? & Hc'2).
    exists (c'1, c'2).
    destruct Hc'2 as [(He & ?) | (? & ?)]; subst; [repeat split; simpl; auto|].
    repeat split; try solve [simpl; auto].
    simpl snd; destruct (snd e); auto; simpl.
    destruct c'1; simpl; auto.
    destruct (fst e).
    apply join_lift_ord in Hc'1; destruct Hc'1.
    eapply ord_trans; eauto.
    { destruct (fst a); contradiction. }
Defined.

Definition ghost_snap (a : A) p := ghost (Some a, @None A) p.
Definition ghost_master (a : A) p := ghost (@None A, Some a) p.

Lemma ghost_snap_join : forall v1 v2 p v, join v1 v2 v ->
  ghost_snap v1 p * ghost_snap v2 p = ghost_snap v p.
Proof.
  intros; apply ghost_join; simpl; auto.
Qed.

Lemma snap_master_join : forall v1 v2 p,
  ghost_snap v1 p * ghost_master v2 p = !!(ord v1 v2) && ghost (Some v1, Some v2) p.
Proof.
  unfold ghost_snap, ghost_master; intros; apply mpred_ext.
  - eapply derives_trans; [apply prop_and_same_derives, ghost_conflict|].
    apply derives_extract_prop; intros (x & Hj1 & Hj2 & Hcompat).
    assert (ord v1 v2).
    { destruct Hj2 as [(? & ?) | (Hsnd & ?)]; [discriminate|].
      rewrite <- Hsnd in Hcompat; simpl in *.
      destruct (fst x); [subst; auto | contradiction]. }
    erewrite ghost_join; [entailer!|].
    simpl; auto.
  - Intros; erewrite ghost_join; eauto.
    simpl; auto.
Qed.

Lemma snap_master_update : forall v1 v2 p v', ord v2 v' ->
  view_shift (ghost_snap v1 p * ghost_master v2 p) (ghost_snap v' p * ghost_master v' p).
Proof.
  intros; rewrite !snap_master_join.
  repeat intro.
  erewrite extract_prop_in_SEP with (n := O); simpl; eauto; Intros.
  apply ghost_update with (g' := (Some v', Some v')).
  { unfold update; intros ? (? & Hfst & Hcase & Hcompat); simpl in *.
    destruct Hcase as [(Hx & ?) | (? & ?)]; [|discriminate].
    rewrite <- Hx in Hcompat.
    eexists (Some v', Some v'); simpl; repeat split; eauto; simpl; try reflexivity.
    destruct (fst c), (fst x); auto; try contradiction.
    apply join_ord in Hfst; destruct Hfst.
    eapply ord_join, ord_trans; eauto.
    eapply ord_trans; eauto. }
  eapply semax_pre; [|eauto].
  go_lowerx; entailer!.
Qed.

Lemma snap_master_init : forall (a : A), exists g', joins (Some a, Some a) g'.
Proof.
  intros; exists (None, None), (Some a, Some a); simpl.
  repeat (split; auto); reflexivity.
Qed.

End Snapshot.

Section PVar.
(* Like ghost variables, but the partial values may be out of date. *)

Instance max_PCM : PCM Z := { join a b c := c = Z.max a b }.
Proof.
  - intros; rewrite Z.max_comm; auto.
  - intros; do 2 eexists; eauto; subst.
    rewrite Z.max_assoc; auto.
Defined.

Global Instance max_order : PCM_order Z.le.
Proof.
  constructor; simpl; intros.
  - intro; omega.
  - intros ???; omega.
  - subst; split; [apply Z.le_max_l | apply Z.le_max_r].
  - rewrite Z.max_l; auto.
Defined.

Lemma ghost_snap_join' : forall v1 v2 p, ghost_snap v1 p * ghost_snap v2 p = ghost_snap (Z.max v1 v2) p.
Proof.
  intros; apply ghost_snap_join; simpl; auto.
Qed.

Lemma snap_master_join' : forall v1 v2 p,
  ghost_snap v1 p * ghost_master v2 p = !!(v1 <= v2) && ghost (Some v1, Some v2) p.
Proof.
  intros; apply snap_master_join.
Qed.

Lemma snap_master_update' : forall (v1 v2 : Z) p v', v2 <= v' ->
  view_shift (ghost_snap v1 p * ghost_master v2 p) (ghost_snap v' p * ghost_master v' p).
Proof.
  intros; apply snap_master_update; auto.
Qed.

Lemma snap_master_init' : forall (v : Z), exists g', joins (Some v, Some v) g'.
Proof.
  intro; apply snap_master_init.
Qed.

End PVar.

Section GHist.

(* Ghost histories in the style of Nanevsky *)
Context {hist_el : Type}.

Notation hist_part := (list (nat * hist_el)).

Require Import Sorting.Permutation.

Definition disjoint (h1 h2 : hist_part) := forall n e, In (n, e) h1 -> forall e', ~In (n, e') h2.

Lemma disjoint_nil : forall l, disjoint l [].
Proof.
  repeat intro; contradiction.
Qed.
Hint Resolve disjoint_nil.

Lemma disjoint_comm : forall a b, disjoint a b -> disjoint b a.
Proof.
  intros ?? Hdisj ?? Hin ? Hin'.
  eapply Hdisj; eauto.
Qed.

Lemma disjoint_app : forall a b c, disjoint (a ++ b) c <-> disjoint a c /\ disjoint b c.
Proof.
  split.
  - intro; split; repeat intro; eapply H; eauto; rewrite in_app; eauto.
  - intros (Ha & Hb) ?????.
    rewrite in_app in H; destruct H; [eapply Ha | eapply Hb]; eauto.
Qed.

Require Import Morphisms.

Global Instance Permutation_disjoint :
  Proper (@Permutation _ ==> @Permutation _ ==> iff) disjoint.
Proof.
  intros ?? Hp1 ?? Hp2.
  split; intro Hdisj; repeat intro.
  - eapply Hdisj; [rewrite Hp1 | rewrite Hp2]; eauto.
  - eapply Hdisj; [rewrite <- Hp1 | rewrite <- Hp2]; eauto.
Qed.

Instance map_PCM : PCM hist_part := { join a b c := disjoint a b /\ Permutation (a ++ b) c }.
Proof.
  - intros ??? (Hdisj & ?); split.
    + apply disjoint_comm; auto.
    + etransitivity; [|eauto].
      apply Permutation_app_comm.
  - intros ????? (Hd1 & Hc) (Hd2 & He).
    rewrite <- Hc, disjoint_app in Hd2; destruct Hd2 as (Hd2 & Hd3).
    exists (b ++ d); repeat split; auto.
    + apply disjoint_comm; rewrite disjoint_app; split; apply disjoint_comm; auto.
    + etransitivity; [|eauto].
      rewrite app_assoc; apply Permutation_app_tail; auto.
Defined.

Definition hist_sub sh h hr := if eq_dec sh Tsh then h = hr
  else sh <> Share.bot /\ exists h', disjoint h h' /\ Permutation (h ++ h') hr.

Lemma completable_alt : forall sh h hr, completable (Some (sh, h)) hr <-> hist_sub sh h hr.
Proof.
  unfold completable, hist_sub; intros; simpl; split.
  - intros ([(?, ?)|] & Hcase).
    + destruct Hcase as (? & ? & Hsh & ? & ?).
      if_tac; eauto.
      subst; apply join_Tsh in Hsh; tauto.
    + destruct Hcase as (? & Heq); inv Heq.
      rewrite eq_dec_refl; auto.
  - if_tac.
    + intro; subst; exists None; split; auto.
      apply Share.nontrivial.
    + intros (? & h' & ?); exists (Some (Share.comp sh, h')).
      split; auto.
      split.
      { intro Hbot; contradiction H.
        rewrite <- Share.comp_inv at 1.
        rewrite Hbot; apply comp_bot. }
      split; [apply comp_join_top | auto].
Qed.

Lemma hist_sub_snoc : forall sh h hr t' e (Hsub : hist_sub sh h hr) (Hfresh : ~In t' (map fst hr)),
  hist_sub sh (h ++ [(t', e)]) (hr ++ [(t', e)]).
Proof.
  unfold hist_sub; intros.
  if_tac; subst; auto.
  destruct Hsub as (? & h' & ? & Hperm); split; auto.
  exists h'; split.
  - rewrite disjoint_app; split; auto.
    intros ?? [Heq | ?]; [inv Heq | contradiction].
    intros ??; contradiction Hfresh; rewrite in_map_iff.
    do 2 eexists; [|rewrite <- Hperm, in_app; eauto]; auto.
  - rewrite <- app_assoc; etransitivity; [apply Permutation_app_head, Permutation_app_comm|].
    rewrite app_assoc; apply Permutation_app; auto.
Qed.

Definition ghost_hist (sh : share) (h : hist_part) p := (ghost (Some (sh, h), @None hist_part) p).

Lemma ghost_hist_join : forall sh1 sh2 sh h1 h2 h p (Hsh : sepalg.join sh1 sh2 sh)
  (Hh : Permutation (h1 ++ h2) h) (Hsh1 : sh1 <> Share.bot) (Hsh2 : sh2 <> Share.bot),
  ghost_hist sh1 h1 p * ghost_hist sh2 h2 p = !!(disjoint h1 h2) && ghost_hist sh h p.
Proof.
  intros; unfold ghost_hist.
  apply mpred_ext.
  - assert_PROP (disjoint h1 h2).
    { eapply derives_trans; [apply ghost_conflict|].
      apply prop_left; intros (x & ? & ?); simpl in *.
      apply prop_right; destruct (fst x) as [(?, ?)|]; [tauto | contradiction]. }
    erewrite ghost_join; [entailer!|].
    repeat (split; simpl; auto).
  - Intros.
    erewrite ghost_join; eauto.
    repeat (split; simpl; auto).
Qed.

Definition hist_incl (h : hist_part) l := forall t e, In (t, e) h -> nth_error l t = Some e.

Definition hist_list (h : hist_part) l := NoDup h /\ forall t e, In (t, e) h <-> nth_error l t = Some e.

Lemma hist_list_inj : forall h l1 l2 (Hl1 : hist_list h l1) (Hl2 : hist_list h l2), l1 = l2.
Proof.
  unfold hist_list; intros; apply list_nth_error_eq.
  destruct Hl1 as (? & Hl1), Hl2 as (? & Hl2).
  intro j; specialize (Hl1 j); specialize (Hl2 j).
  destruct (nth_error l1 j).
  - symmetry; rewrite <- Hl2, Hl1; auto.
  - destruct (nth_error l2 j); auto.
    specialize (Hl2 h0); rewrite Hl1 in Hl2; tauto.
Qed.

Lemma hist_list_nil_inv1 : forall l, hist_list [] l -> l = [].
Proof.
  unfold hist_list; intros.
  destruct l; auto.
  destruct H as (_ & H).
  specialize (H O h); destruct H; simpl in *; contradiction.
Qed.

Lemma hist_list_nil_inv2 : forall h, hist_list h [] -> h = [].
Proof.
  unfold hist_list; intros.
  destruct h as [|(t, e)]; auto.
  destruct H as (_ & H).
  specialize (H t e); destruct H as (H & _).
  exploit H; [simpl; auto | rewrite nth_error_nil; discriminate].
Qed.

Lemma NoDup_remove_0 : forall {A} (l : list (nat * A)), NoDup (map fst l) -> ~In O (map fst l) ->
  NoDup (map fst (map (fun '(t, e) => ((t - 1)%nat, e)) l)).
Proof.
  induction l; auto; simpl; intros.
  inv H.
  constructor; auto.
  destruct a.
  rewrite in_map_iff; intros ((?, ?) & Heq & Hin); simpl in *; inv Heq.
  rewrite in_map_iff in Hin; destruct Hin as ((?, ?) & Heq & ?); inv Heq.
  assert (In n (map fst l)); [|contradiction].
  rewrite in_map_iff; do 2 eexists; eauto.
  destruct n; [tauto|].
  destruct n0; [|simpl in *; omega].
  assert (In O (map fst l)); [|tauto].
  rewrite in_map_iff; do 2 eexists; eauto; auto.
Qed.

Lemma NoDup_remove_0' : forall {A} (l : list (nat * A)), NoDup l -> ~In O (map fst l) ->
  NoDup (map (fun '(t, e) => ((t - 1)%nat, e)) l).
Proof.
  induction l; auto; simpl; intros.
  inv H.
  constructor; auto.
  destruct a.
  rewrite in_map_iff; intros ((?, ?) & Heq & Hin); simpl in *; inv Heq.
  destruct n; [tauto|].
  destruct n0; [|simpl in *; assert (n0 = n) by omega; subst; contradiction].
  assert (In O (map fst l)); [|tauto].
  rewrite in_map_iff; do 2 eexists; eauto; auto.
Qed.

Lemma remove_0_inj : forall {A} (l : list (nat * A)), ~In O (map fst l) ->
  map fst (map (fun '(t, e) => ((t - 1)%nat, e)) l) = map (fun t => t - 1)%nat (map fst l).
Proof.
  induction l; auto; simpl; intros.
  destruct a; rewrite IHl; auto.
Qed.

Lemma hist_list_NoDup : forall l h (Hl : hist_list h l), NoDup (map fst h).
Proof.
  induction l; intros; [apply hist_list_nil_inv2 in Hl; subst; constructor|].
  destruct Hl as (Hd & Hl).
  assert (In (O, a) h) as Hin.
  { unfold hist_list in Hl; rewrite Hl; auto. }
  exploit in_split; eauto; intros (h1 & h2 & ?); subst.
  apply NoDup_remove in Hd; destruct Hd as (? & Hn).
  assert (~In O (map fst (h1 ++ h2))) as HO.
  { rewrite in_map_iff; intros ((?, e) & ? & ?); simpl in *; subst.
    specialize (Hl O e); destruct Hl as (Hl & _); exploit Hl.
    { rewrite in_app in *; simpl; tauto. }
    simpl; intro X; inv X; contradiction. }
  exploit (IHl (map (fun x => let '(t, e) := x in ((t - 1)%nat, e)) (h1 ++ h2))).
  { split.
    { apply NoDup_remove_0'; auto. }
    intros t e.
    rewrite in_map_iff; split.
    + intros ((?, ?) & Heq & ?); inv Heq.
      specialize (Hl n e).
      destruct Hl as (Hl & _); exploit Hl.
      { rewrite in_app in *; simpl; tauto. }
      destruct n; simpl; [|rewrite Nat.sub_0_r; auto].
      contradiction HO.
      rewrite in_map_iff; do 2 eexists; eauto; auto.
    + intro Ht; specialize (Hl (S t) e); simpl in Hl.
      destruct Hl as (_ & Hl); specialize (Hl Ht).
      exists (S t, e); split; [simpl; rewrite Nat.sub_0_r; auto|].
      rewrite in_app in *; destruct Hl as [? | [Heq | ?]]; auto.
      inv Heq. }
  intro Hd; rewrite map_app; simpl; apply NoDup_add; rewrite <- map_app; auto.
  rewrite remove_0_inj in Hd; auto.
  eapply NoDup_map_inv; eauto.
Qed.

Lemma hist_list_length : forall l h (Hl : hist_list h l), Zlength h = Zlength l.
Proof.
  induction l; intros.
  - apply hist_list_nil_inv2 in Hl; subst; auto.
  - pose proof (hist_list_NoDup _ _ Hl) as Hdisj; destruct Hl as (? & Hl).
    assert (In (O, a) h) as Hin.
    { unfold hist_list in Hl; rewrite Hl; auto. }
    exploit in_split; eauto; intros (h1 & h2 & ?); subst.
    rewrite map_app in Hdisj; simpl in Hdisj; apply NoDup_remove in Hdisj.
    destruct Hdisj as (Hdisj & Hn).
    exploit (IHl (map (fun x => let '(t, e) := x in ((t - 1)%nat, e)) (h1 ++ h2))).
    { split.
      { apply NoDup_remove in H; destruct H.
        apply NoDup_remove_0'; auto.
        rewrite map_app; auto. }
      intros t e.
      rewrite in_map_iff; split.
      + intros ((?, ?) & Heq & ?); inv Heq.
        specialize (Hl n e).
        destruct Hl as (Hl & _); exploit Hl.
        { rewrite in_app in *; simpl; tauto. }
        destruct n; simpl; [|rewrite Nat.sub_0_r; auto].
        contradiction Hn.
        rewrite <- map_app, in_map_iff; do 2 eexists; eauto; auto.
      + intro Ht; specialize (Hl (S t) e); simpl in Hl.
        destruct Hl as (_ & Hl); specialize (Hl Ht).
        exists (S t, e); split; [simpl; rewrite Nat.sub_0_r; auto|].
        rewrite in_app in *; destruct Hl as [? | [Heq | ?]]; auto.
        inv Heq. }
    rewrite Zlength_map, !Zlength_app, !Zlength_cons; omega.
Qed.

Definition ghost_ref l p := EX hr : hist_part, !!(hist_list hr l) &&
  ghost (@None (share * hist_part), Some hr) p.

Lemma hist_next : forall h l (Hlist : hist_list h l), ~In (length l) (map fst h).
Proof.
  intros; rewrite in_map_iff; intros ((?, ?) & ? & Hin); simpl in *; subst.
  destruct Hlist as (? & Hlist); rewrite Hlist in Hin.
  pose proof (nth_error_Some l (length l)) as (Hlt & _).
  exploit Hlt; [|omega].
  rewrite Hin; discriminate.
Qed.

Lemma hist_add : forall (sh : share) (h h' : hist_part) e p t' (Hfresh : ~In t' (map fst h')),
  view_shift (ghost (Some (sh, h), Some h') p) (ghost (Some (sh, h ++ [(t', e)]), Some (h' ++ [(t', e)])) p).
Proof.
  intros; apply ghost_update.
  intros (c1, c2) ((d1, d2) & Hjoin1 & [(<- & ?) | (? & ?)] & Hcompat); try discriminate.
  simpl in *.
  destruct c1 as [(shc, hc)|], d1 as [(?, ?)|]; try contradiction.
  - destruct Hjoin1 as (? & ? & ? & Hdisj & Hperm).
    rewrite completable_alt in Hcompat; unfold hist_sub in Hcompat.
    destruct (eq_dec s Tsh).
    + subst; exists (Some (Tsh, h' ++ [(t', e)]), Some (h' ++ [(t', e)])).
      repeat (split; simpl; auto).
      * rewrite disjoint_app; split; auto.
        intros ?? [Heq | ?]; [inv Heq | contradiction].
        intros ??; contradiction Hfresh; rewrite in_map_iff.
        do 2 eexists; [|rewrite <- Hperm, in_app; eauto]; auto.
      * rewrite <- app_assoc.
        etransitivity; [apply Permutation_app_head, Permutation_app_comm|].
        rewrite app_assoc; apply Permutation_app; auto.
      * rewrite completable_alt; apply hist_sub_snoc; auto.
        unfold hist_sub; rewrite eq_dec_refl; auto.
    + destruct Hcompat as (? & l' & ? & Hperm').
      exists (Some (s, h ++ hc ++ [(t', e)]), Some (h' ++ [(t', e)])); repeat (split; simpl; auto).
      * rewrite disjoint_app; split; auto.
        intros ?? [Heq | ?]; [inv Heq | contradiction].
        intros ??; contradiction Hfresh; rewrite in_map_iff.
        do 2 eexists; [|rewrite <- Hperm', in_app, <- Hperm, in_app; eauto]; auto.
      * rewrite <- app_assoc; apply Permutation_app_head, Permutation_app_comm.
      * rewrite completable_alt, app_assoc; apply hist_sub_snoc; auto.
        unfold hist_sub; if_tac; [contradiction n; auto|].
        split; auto; exists l'; split.
        { eapply Permutation_disjoint; eauto. }
        etransitivity; [|eauto].
        apply Permutation_app; auto.
  - simpl in H; destruct Hjoin1 as (? & Hjoin1); inv Hjoin1.
    exists (Some (sh, h ++ [(t', e)]), Some (h' ++ [(t', e)])); simpl; repeat (split; auto).
    rewrite completable_alt in *; apply hist_sub_snoc; auto.
Qed.

Lemma hist_incl_nil : forall h, hist_incl [] h.
Proof.
  repeat intro; contradiction.
Qed.

Lemma hist_list_nil : hist_list [] [].
Proof.
  split; [constructor|].
  split; [contradiction | rewrite nth_error_nil; discriminate].
Qed.

Lemma hist_list_snoc : forall h l e, hist_list h l -> hist_list (h ++ [(length l, e)]) (l ++ [e]).
Proof.
  unfold hist_list; intros.
  destruct H as (Hd & H).
  assert (~In (length l, e) h).
  { rewrite H; intro Hnth.
    assert (length l < length l)%nat; [|omega].
    rewrite <- nth_error_Some, Hnth; discriminate. }
  split.
  { apply NoDup_app_iff; repeat constructor; auto.
    intros ?? [? | ?]; subst; contradiction. }
  intros; rewrite in_app; split.
  - intros [Hin | [Heq | ?]]; try contradiction.
    + rewrite H in Hin.
      rewrite nth_error_app1; auto.
      rewrite <- nth_error_Some, Hin; discriminate.
    + inv Heq; rewrite nth_error_app2, minus_diag; auto.
  - destruct (lt_dec t (length l)).
    + rewrite nth_error_app1 by auto.
      rewrite <- H; auto.
    + rewrite nth_error_app2 by omega.
      destruct (eq_dec t (length l)).
      * subst; rewrite minus_diag.
        intro Heq; inv Heq; simpl; auto.
      * destruct (t - length l)%nat eqn: Hminus; [omega | simpl; rewrite nth_error_nil; discriminate].
Qed.

Lemma hist_incl_permute : forall h1 h2 h' (Hincl : hist_incl h1 h') (Hperm : Permutation h1 h2),
  hist_incl h2 h'.
Proof.
  repeat intro.
  rewrite <- Hperm in H; auto.
Qed.

Lemma hist_sub_incl : forall sh h h', hist_sub sh h h' -> incl h h'.
Proof.
  unfold hist_sub; intros.
  destruct (eq_dec sh Tsh); [subst; apply incl_refl|].
  destruct H as (? & ? & ? & Hperm); repeat intro.
  rewrite <- Hperm, in_app; auto.
Qed.

Corollary hist_sub_list_incl : forall sh h h' l (Hsub : hist_sub sh h h') (Hlist : hist_list h' l),
  hist_incl h l.
Proof.
  unfold hist_list, hist_incl; intros.
  destruct Hlist as (_ & <-); eapply hist_sub_incl; eauto.
Qed.

Lemma hist_sub_Tsh : forall h h', hist_sub Tsh h h' = (h = h').
Proof.
  intros; unfold hist_sub; rewrite eq_dec_refl; auto.
Qed.

Lemma hist_ref_join : forall sh h l p, sh <> Share.bot ->
  ghost_hist sh h p * ghost_ref l p =
  EX h' : hist_part, !!(hist_list h' l /\ hist_sub sh h h') && ghost (Some (sh, h), Some h') p.
Proof.
  unfold ghost_hist, ghost_ref; intros; apply mpred_ext.
  - Intros hr; Exists hr.
    eapply derives_trans; [apply prop_and_same_derives, ghost_conflict|].
    apply derives_extract_prop; intros (x & Hj1 & Hj2 & Hcompat).
    destruct Hj2 as [(? & ?) | (Hsnd & ?)]; [discriminate|].
    rewrite <- Hsnd in Hcompat; simpl in *.
    destruct (fst x); [destruct Hj1 as (_ & Heq); inv Heq | contradiction].
    assert (hist_sub sh h hr) by (rewrite <- completable_alt; auto).
    entailer!.
    erewrite ghost_join; eauto.
    simpl; auto.
  - Intros h'.
    Exists h'; entailer!.
    erewrite ghost_join; eauto.
    repeat (split; simpl; auto).
    rewrite completable_alt; auto.
Qed.

Corollary hist_ref_join_nil : forall sh p, sh <> Share.bot ->
  ghost_hist sh [] p * ghost_ref [] p = ghost (Some (sh, [] : hist_part), Some ([] : hist_part)) p.
Proof.
  intros; rewrite hist_ref_join by auto.
  apply mpred_ext; entailer!.
  - destruct h' as [|(t, e)]; auto.
    match goal with H : hist_list _ _ |- _ => destruct H as (_ & H);
      specialize (H t e); destruct H as (Hin & _) end.
    exploit Hin; [simpl; auto | rewrite nth_error_nil; discriminate].
  - Exists ([] : hist_part); entailer!.
    split; [apply hist_list_nil|].
    unfold hist_sub; if_tac; auto.
    split; auto; exists []; auto.
Qed.

Lemma hist_add' : forall sh h h' e p, sh <> Share.bot ->
  view_shift (ghost_hist sh h p * ghost_ref h' p)
  (ghost_hist sh (h ++ [(length h', e)]) p * ghost_ref (h' ++ [e]) p).
Proof.
  intros; rewrite hist_ref_join by auto.
  repeat intro.
  rewrite extract_exists_in_SEP; Intro hr.
  erewrite extract_prop_in_SEP with (n := O); simpl; eauto; Intros.
  match goal with H : hist_list _ _ |- _ => pose proof (hist_next _ _ H) end.
  apply hist_add with (e := e)(t' := length h'); auto.
  eapply semax_pre; [|eauto].
  go_lowerx; rewrite hist_ref_join by auto.
  Exists (hr ++ [(length h', e)]); entailer!.
  split; [apply hist_list_snoc | apply hist_sub_snoc]; auto.
Qed.

Definition newer (l : hist_part) t := Forall (fun x => fst x < t)%nat l.

Lemma newer_trans : forall l t1 t2, newer l t1 -> (t1 <= t2)%nat -> newer l t2.
Proof.
  intros.
  eapply Forall_impl, H; simpl; intros; omega.
Qed.

Corollary newer_snoc : forall l t1 e t2, newer l t1 -> (t1 < t2)%nat -> newer (l ++ [(t1, e)]) t2.
Proof.
  unfold newer; intros.
  rewrite Forall_app; split; [|repeat constructor; auto].
  eapply newer_trans; eauto; omega.
Qed.

Lemma hist_incl_lt : forall h l, hist_incl h l -> newer h (length l).
Proof.
  unfold hist_incl; intros.
  unfold newer; rewrite Forall_forall; intros (?, ?) Hin.
  erewrite <- nth_error_Some, H; eauto; discriminate.
Qed.

Variable (d : hist_el).

Definition ordered_hist h := forall i j (Hi : 0 <= i < j) (Hj : j < Zlength h),
  (fst (Znth i h (O, d)) < fst (Znth j h (O, d)))%nat.

Lemma ordered_nil : ordered_hist [].
Proof.
  repeat intro.
  rewrite Zlength_nil in *; omega.
Qed.

Lemma ordered_cons : forall t e h, ordered_hist ((t, e) :: h) ->
  Forall (fun x => let '(m, _) := x in t < m)%nat h /\ ordered_hist h.
Proof.
  unfold ordered_hist; split.
  - rewrite Forall_forall; intros (?, ?) Hin.
    apply In_Znth with (d0 := (O, d)) in Hin.
    destruct Hin as (j & ? & Hj).
    exploit (H 0 (j + 1)); try omega.
    { rewrite Zlength_cons; omega. }
    rewrite Znth_0_cons, Znth_pos_cons, Z.add_simpl_r, Hj by omega; auto.
  - intros; exploit (H (i + 1) (j + 1)); try omega.
    { rewrite Zlength_cons; omega. }
    rewrite !Znth_pos_cons, !Z.add_simpl_r by omega; auto.
Qed.

Lemma ordered_last : forall t e h (Hordered : ordered_hist h) (Hin : In (t, e) h)
  (Ht : Forall (fun x => let '(m, _) := x in m <= t)%nat h), last h (O, d) = (t, e).
Proof.
  induction h; [contradiction | simpl; intros].
  destruct a; apply ordered_cons in Hordered; destruct Hordered as (Ha & ?).
  inversion Ht as [|??? Hp]; subst.
  destruct Hin as [Hin | Hin]; [inv Hin|].
  - destruct h; auto.
    inv Ha; inv Hp; destruct p; omega.
  - rewrite IHh; auto.
    destruct h; auto; contradiction.
Qed.

Lemma ordered_snoc : forall h t e, ordered_hist h -> newer h t -> ordered_hist (h ++ [(t, e)]).
Proof.
  repeat intro.
  rewrite Zlength_app, Zlength_cons, Zlength_nil in Hj.
  rewrite app_Znth1 by omega.
  destruct (eq_dec j (Zlength h)).
  - rewrite Znth_app1; auto.
    apply Forall_Znth; auto; omega.
  - specialize (H i j).
    rewrite app_Znth1 by omega; apply H; auto; omega.
Qed.

Lemma ordered_hist_list : forall l h i (Hordered : ordered_hist h) (Hl : hist_list h l)
  (Hi : 0 <= i < Zlength l), Znth i h (O, d) = (Z.to_nat i, Znth i l d).
Proof.
  intros.
  pose proof (hist_list_length _ _ Hl) as Hlen.
  destruct Hl as (? & Hl).
  assert (nth (Z.to_nat i) (map fst h) (fst (O, d)) = Z.to_nat i) as Ht.
  { assert (length h = length l) as Hlen'
      by (rewrite Zlength_length, ZtoNat_Zlength in Hlen by (apply Zlength_nonneg); auto).
    apply nat_sorted_list_eq with (n := length h).
    - intro j; specialize (Hl j).
      split; intro Hin.
      + specialize (Hl (nth j l d)).
        erewrite nth_error_nth in Hl by omega.
        destruct Hl as (_ & Hl); rewrite in_map_iff; do 2 eexists; [|apply Hl]; eauto.
      + rewrite in_map_iff in Hin; destruct Hin as ((?, e) & ? & Hin); simpl in *; subst.
        rewrite Hl in Hin; rewrite Hlen', <- nth_error_Some, Hin; discriminate.
    - apply map_length.
    - intros i' j' ?.
      exploit (Hordered (Z.of_nat i') (Z.of_nat j')).
      { split; [omega|].
        apply Nat2Z.inj_lt; tauto. }
      { rewrite Zlength_correct; apply Nat2Z.inj_lt; tauto. }
      rewrite !map_nth, !nth_Znth; auto.
    - rewrite <- ZtoNat_Zlength; apply Z2Nat.inj_lt; omega. }
  rewrite nth_Znth, Z2Nat.id in Ht by tauto.
  erewrite Znth_map with (d' := (O, d)) in Ht by omega.
  destruct (Znth i h (O, d)) as (t, e) eqn: Heq.
  specialize (Hl t e); rewrite <- Heq in Hl.
  destruct Hl as (Hl & _); exploit Hl.
  { apply Znth_In; omega. }
  intro Hnth; rewrite nth_error_nth with (d := d) in Hnth by (rewrite <- nth_error_Some, Hnth; discriminate).
  simpl in *; inv Hnth.
  rewrite nth_Znth, Z2Nat.id; tauto.
Qed.

(* We want to be able to remove irrelevant operations from a history, leading to a slightly weaker
   correspondence between history and list of operations. *)
Inductive hist_list' : hist_part -> list hist_el -> Prop :=
| hist_list'_nil : hist_list' [] []
| hist_list'_snoc : forall h l t e h1 h2 (He : h = h1 ++ (t, e) :: h2)
    (Hlast : newer (h1 ++ h2) t) (Hrest : hist_list' (h1 ++ h2) l),
    hist_list' h (l ++ [e]).
Hint Resolve hist_list'_nil.

Lemma hist_list'_in : forall h l (Hl : hist_list' h l) e, (exists t, In (t, e) h) <-> In e l.
Proof.
  induction 1.
  - split; [intros (? & ?)|]; contradiction.
  - intro; subst; split.
    + intros (? & Hin); rewrite in_app in *.
      destruct Hin as [? | [Heq | ?]]; try solve [left; rewrite <- IHHl; eexists; rewrite in_app; eauto].
      inv Heq; simpl; auto.
    + rewrite in_app; intros [Hin | [Heq | ?]]; [| inv Heq | contradiction].
      * rewrite <- IHHl in Hin; destruct Hin as (? & ?).
        eexists; rewrite in_app in *; simpl; destruct H; eauto.
      * eexists; rewrite in_app; simpl; eauto.
Qed.

Lemma hist_list_weak : forall l h (Hl : hist_list h l), hist_list' h l.
Proof.
  induction l using rev_ind; intros.
  - apply hist_list_nil_inv2 in Hl; subst; auto.
  - pose proof (hist_list_NoDup _ _ Hl) as HNoDup.
    destruct Hl as (Hd & Hl).
    destruct (Hl (length l) x) as (_ & H); exploit H.
    { rewrite nth_error_app2, minus_diag by omega; auto. }
    intro; exploit in_split; eauto; intros (h1 & h2 & ?).
    subst; rewrite map_app in HNoDup; simpl in HNoDup; apply NoDup_remove in HNoDup.
    rewrite <- map_app in HNoDup.
    assert (hist_list (h1 ++ h2) l) as Hl'.
    { split.
      { apply NoDup_remove in Hd; tauto. }
      intros t e; specialize (Hl t e).
      split; intro Hin.
      + destruct Hl as (Hl & _); exploit Hl.
        { rewrite in_app in *; simpl; tauto. }
        intro Hnth; assert (t < length (l ++ [x]))%nat.
        { rewrite <- nth_error_Some, Hnth; discriminate. }
        rewrite app_length in *; simpl in *.
        rewrite nth_error_app1 in Hnth; auto.
        destruct (eq_dec t (length l)); [|omega].
        destruct HNoDup as (? & HNoDup); contradiction HNoDup.
        rewrite in_map_iff; do 2 eexists; eauto; auto.
      + assert (t < length l)%nat.
        { rewrite <- nth_error_Some, Hin; discriminate. }
        destruct Hl as (_ & Hl); exploit Hl.
        { rewrite nth_error_app1; auto. }
        rewrite !in_app; intros [? | [Heq | ?]]; auto; inv Heq; omega. }
    econstructor; eauto.
    subst; unfold newer; rewrite Forall_forall; intros (t, e) Hin.
    rewrite <- nth_error_Some.
    destruct Hl' as (? & Hl').
    destruct (Hl' t e) as (Hnth & _); simpl; rewrite Hnth by auto; discriminate.
Qed.

Lemma hist_list'_NoDup : forall h l, hist_list' h l -> NoDup (map fst h).
Proof.
  induction 1.
  - constructor.
  - subst; rewrite map_app in *; simpl.
    apply NoDup_add; auto.
    rewrite <- map_app, in_map_iff; intros ((?, ?) & ? & ?); subst.
    unfold newer in Hlast; rewrite Forall_forall in Hlast.
    exploit Hlast; eauto; omega.
Qed.

Lemma ghost_hist_init : exists g', joins (Some (Tsh, []), Some []) g'.
Proof.
  exists (None, None), (Some (Tsh, []), Some []); simpl.
  pose proof Share.nontrivial.
  unfold completable; repeat split; auto.
  exists None; simpl.
  split; auto.
Qed.

End GHist.

Section AEHist.

(* These histories should be usable for any atomically accessed location. *)
Inductive AE_hist_el := AE (r : val) (w : val).

Fixpoint apply_hist a h :=
  match h with
  | [] => Some a
  | AE r w :: h' => if eq_dec r a then apply_hist w h' else None
  end.

Arguments eq_dec _ _ _ _ : simpl never.

Lemma apply_hist_app : forall h1 i h2, apply_hist i (h1 ++ h2) =
  match apply_hist i h1 with Some v => apply_hist v h2 | None => None end.
Proof.
  induction h1; auto; simpl; intros.
  destruct a.
  destruct (eq_dec r i); auto.
Qed.

End AEHist.

Notation AE_hist := (list (nat * AE_hist_el)).

End Ghost.

Hint Resolve disjoint_nil hist_incl_nil hist_list_nil ordered_nil hist_list'_nil.
Hint Resolve ghost_var_precise ghost_var_precise'.
Hint Resolve ghost_var_init snap_master_init' ghost_hist_init : init.


text:
(*
 This is the definition of formal syntax for Dan Grossman's Thesis,
  "SAFE PROGRAMMING AT THE C LEVEL OF ABSTRACTION".

  A very simple module for two flags on existential types.

*)

Require Import List.
Export ListNotations.
Require Import ZArith.
Require Import Init.Datatypes.
Require Import Coq.Init.Logic.
Require Import Coq.Bool.Bool.

Require Export BoolEqualitySigDef.

Require Export CpdtTactics.
Require Export Case.
Require Export NatLemmas.

Module PhiModule.

Inductive Phi : Type :=
 | witnesschanges  : Phi                            (* Allowing witness changes. \delta *)
 | aliases        : Phi.                            (* Allowing aliases as the opened type. \amp *)

Function beq_phi (p p' : Phi) : bool :=
  match p, p' with
    | witnesschanges, witnesschanges => true
    | aliases, aliases => true
    | _, _ => false
  end.
Hint Unfold  beq_phi.
Hint Resolve beq_phi.

Lemma beq_phi_refl:
  forall (k : Phi),
    beq_phi k k = true.
Proof.
  destruct k.
  reflexivity.
  reflexivity.
Qed.
Hint Resolve beq_phi_refl.

Lemma beq_phi_sym : forall x y : Phi, beq_phi x y = beq_phi y x.
Proof.
  intros.
  destruct x;  destruct y; crush.
Qed.
Hint Immediate beq_phi_sym.

Lemma beq_phi_trans :
  forall x y z,
    beq_phi x y = true -> beq_phi y z = true -> beq_phi x z = true.
Proof.
   destruct x; destruct y; destruct z; crush.
Qed.
Hint Resolve beq_phi_trans.

Lemma beq_phi_eq:
  forall (k k': Phi),
    beq_phi k k' = true ->
    k = k'.
Proof.
  intros.
  destruct k; destruct k'.
  reflexivity.
  inversion H.
  inversion H.
  reflexivity.
Qed.
Hint Resolve beq_phi_eq.

Lemma beq_phi_neq:
  forall (k k': Phi),
    beq_phi k k' = false ->
    k <> k'.
Proof.
  intros.
  destruct k; destruct k'.
  inversion H.
  discriminate.
  discriminate.
  inversion H.
Qed.
Hint Resolve beq_phi_neq.

Lemma beq_phi_iff_eq:    forall a b, beq_phi a b = true <-> a = b.
Proof.
  destruct a; destruct b; crush.
Qed.
Hint Resolve beq_phi_iff_eq.

Lemma beq_phi_iff_neq:   forall a b, beq_phi a b = false <-> a <> b.
Proof.
  destruct a; destruct b; crush.
Qed.
Hint Resolve beq_phi_iff_neq.
End PhiModule.

author: briangmilnes

repo: CycloneCoqSemantics


text:
From cap_machine Require Import rules_base.
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac.

Section cap_lang_rules.
  Context `{memG Σ, regG Σ, MonRef: MonRefG (leibnizO _) CapR_rtc Σ}.
  Context `{MachineParameters}.
  Implicit Types P Q : iProp Σ.
  Implicit Types σ : ExecConf.
  Implicit Types c : cap_lang.expr.
  Implicit Types a b : Addr.
  Implicit Types r : RegName.
  Implicit Types v : cap_lang.val.
  Implicit Types w : Word.
  Implicit Types reg : gmap RegName Word.
  Implicit Types ms : gmap Addr Word.

  Inductive PromoteU_failure (regs: Reg) (dst: RegName): Prop :=
  | PromoteU_fail_const n:
      regs !! dst = Some (inl n) ->
      PromoteU_failure regs dst
  | PromoteU_fail_E g b e a:
      regs !! dst = Some (inr ((E, g), b, e, a)) ->
      PromoteU_failure regs dst
  | PromoteU_fail_incrementPC p g b e a:
      p <> E ->
      regs !! dst = Some (inr ((p, g), b, e, a)) ->
      incrementPC (<[ dst := inr (promote_perm p, g, b, min a e, a) ]> regs) = None ->
      PromoteU_failure regs dst.

  Inductive PromoteU_spec (regs: Reg) (dst: RegName) (regs': Reg): cap_lang.val → Prop :=
  | PromoteU_spec_success p g b e a:
      p <> E ->
      regs !! dst = Some (inr ((p, g), b, e, a)) ->
      incrementPC (<[ dst := inr (promote_perm p, g, b, min a e, a) ]> regs) = Some regs' ->
      PromoteU_spec regs dst regs' NextIV
  | PromoteU_spec_failure:
      PromoteU_failure regs dst ->
      PromoteU_spec regs dst regs' FailedV.

  Lemma wp_PromoteU Ep pc_p pc_g pc_b pc_e pc_a pc_p' dst w regs :
   decodeInstrW w = PromoteU dst →
   PermFlows pc_p pc_p' →
   isCorrectPC (inr ((pc_p, pc_g), pc_b, pc_e, pc_a)) →
   regs !! PC = Some (inr ((pc_p, pc_g), pc_b, pc_e, pc_a)) →
   regs_of (PromoteU dst) ⊆ dom _ regs →

   {{{ ▷ pc_a ↦ₐ[pc_p'] w ∗
       ▷ [∗ map] k↦y ∈ regs, k ↦ᵣ y }}}
     Instr Executable @ Ep
   {{{ regs' retv, RET retv;
       ⌜ PromoteU_spec regs dst regs' retv⌝ ∗
       pc_a ↦ₐ[pc_p'] w ∗
       [∗ map] k↦y ∈ regs', k ↦ᵣ y }}}.
  Proof.
     iIntros (Hinstr Hfl Hvpc HPC Dregs φ) "(>Hpc_a & >Hmap) Hφ".
     iApply wp_lift_atomic_head_step_no_fork; auto.
     iIntros (σ1 l1 l2 n) "Hσ1 /=". destruct σ1; simpl.
     iDestruct "Hσ1" as "[Hr Hm]".
     assert (pc_p' ≠ O).
     { destruct pc_p'; auto. destruct pc_p; inversion Hfl. inversion Hvpc; naive_solver. }
     iDestruct (gen_heap_valid_inclSepM with "Hr Hmap") as %Hregs.
     pose proof (regs_lookup_eq _ _ _ HPC) as HPC'.
     pose proof (lookup_weaken _ _ _ _ HPC Hregs).
     iDestruct (@gen_heap_valid_cap with "Hm Hpc_a") as %Hpc_a; auto.
     iModIntro. iSplitR. by iPureIntro; apply normal_always_head_reducible.
     iNext. iIntros (e2 σ2 efs Hpstep).
     apply prim_step_exec_inv in Hpstep as (-> & -> & (c & -> & Hstep)).
     iSplitR; auto. eapply step_exec_inv in Hstep; eauto.

     specialize (indom_regs_incl _ _ _ Dregs Hregs) as Hri. unfold regs_of in Hri.

     feed destruct (Hri dst) as [rdstv [Hdst' Hdst]]. by set_solver+.
     pose proof (regs_lookup_eq _ _ _ Hdst) as Hrdst'.
     cbn in Hstep. rewrite Hrdst' in Hstep.
     destruct rdstv as [| (([[p g] b] & e) & a) ] eqn:Hdstv.
     { (* Failure: dst is not a capability *)
       inv Hstep.
       iFailWP "Hφ" PromoteU_fail_const. }

     destruct (perm_eq_dec p E).
     { subst p. inv Hstep.
       iFailWP "Hφ" PromoteU_fail_E. }

     destruct (incrementPC (<[ dst := inr ((promote_perm p, g), b, min a e, a) ]> regs)) as [ regs' |] eqn:Hregs'; cycle 1.
     { assert (incrementPC (<[ dst := inr ((promote_perm p, g, b, min a e, a))]> r) = None).
       { eapply incrementPC_overflow_mono; first eapply Hregs'.
         by rewrite lookup_insert_is_Some'; eauto.
         by apply insert_mono; eauto. }
       rewrite incrementPC_fail_updatePC //= in Hstep; inversion Hstep; subst.
       iMod (@gen_heap_update_inSepM with "Hr Hmap") as "[Hr Hmap]"; eauto.
       iFailWP "Hφ" PromoteU_fail_incrementPC. }

     generalize Hregs'; intros HH.
     eapply (incrementPC_success_updatePC _ m) in Hregs'
       as (p' & g' & b' & e' & a'' & a_pc' & HPC'' & Ha_pc' & HuPC & ->).
     eapply updatePC_success_incl in HuPC. 2: by eapply insert_mono; eauto.
     rewrite HuPC in Hstep; clear HuPC; inversion Hstep. subst c σ2. cbn.
     iFrame. iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
     iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
     iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro.
     econstructor; eauto.
     Unshelve. auto.
  Qed.

End cap_lang_rules.

author: logsem

repo: cerise-stack

save_path: github-repos/coq/logsem-cerise-stack


text:
(**
MathComp の subset について
======
2019/05/01

2019/08/03 追記

この文書のソースコードは以下にあります。

https://github.com/suharahiromichi/coq/blob/master/pearl/ssr_subset_1.v

 *)

(**
OCaml 4.07.1, Coq 8.9.0, MathComp 1.9.0
 *)

(**
# はじめに

この小文は、「補題がMathCompに無かったから自分で証明した」というストーリー
だったのですが、Qiitaに公開した後で、「その補題は存在する」旨の指摘をいただきました。

御指摘ありがとうございます。

そこで、MathCompの定義とは無関係に自分で証明を試みたものとして、
文言を修正すると同時に、独自の補題であることを示すために、補題名を変更しました。

また、MathComp側の定義についての説明に間違いがあったため、該当箇所の解説も修正しました。

以上については、証明のコードは自体は修正していません。
追記のかたちで、MathCompにある補題を使う場合の説明を補足しました。
*)

(**
# 説明

MathComp では、``∈`` を示す `\in` は広く使われるために、``ssrbool.v`` で導入されますが、
部分集合 ``⊆`` を示す、``\subset`` は、fintype.v で導入されています。

要素がすべて列挙できる有限型 ``T : finType`` の上で、そのT の enumを全集合とすることで、
ひと通りの集合演算が定義できるようになるからです。

``T : finType`` のとき、booleanな関数 ``P : T -> bool`` を集合と同一視して、
``P x`` を ``x \in P`` と同一視します。

すると、その上で、集合 A と B の積を
``x ∈ A ∩ B`` <-> `` (λx. A x ∧ B x) x``

P の補集合を
``x ∈ P^c`` <-> `` (λx. ¬ P x)``

と定義できます。

T の enum に対してPでフィルタすることで、Pの要素がすべて求められるので、
その数を数えるとPの濃度を求めることができます。

表記法 Notation については、文献[1.]の表5.1などを参照してください。

また、``P : T -> bool`` を ``P : pred T`` と書くこともありますが、
これは表記のみの違いです。

さて、ここからが本題です。

集合Aが集合Bの部分集合 ``A ⊆ B`` であるとは、A の任意の要素が B の要素であることです。
``\subset`` 演算子が定義されている MathComp の finset.v のコメントには、
実際、そのように記載されています。

``A \subset B == all x \in A satisfy x \in B.`` ..................... (1)

しかし、MathComp の実際の定義は、

``pred0b [predD A & B]`` ............................................ (2)

となっていて、これは、
「論理式 A を満たし、論理式 B を満たさない要素の数が 0 である」という意味です
（predD は difference の意味）。

そこで、(1)と(2)は同値であることを証明してみました。
これは、MathComp の ``fintype.v`` にも類似の補題が証明されているため、
それを使う場合の証明については、補足を参照してください。
*)

(**
# コード例

最初に、通常の Prop 型論理式について同値であることを証明します。

 ``s1 ⊆ s2 <-> ∀x. x ⊆ s1 -> x ⊆ s2``

その後、（MathComp らしく）boolean な論理式について真偽値が一致することを証明します。
*)

From mathcomp Require Import all_ssreflect.

Section Test.

  Variable T : finType.

(**
## Prop な論理式での証明
 *)

  Lemma mySubsetP (s1 s2 : pred T) :
    s1 \subset s2 <-> (forall x, x \in s1 -> x \in s2).
  Proof.
    rewrite subset_disjoint /disjoint.
    split.
    - move/pred0P => H.
      move=> x Hs1.
      move: (H x) => {H} /= /eqP.
      rewrite inE eqbF_neg negb_and /=.
      move/orP => [Hn1 | Hnn2].
      + by move/negP : Hn1.
      + by rewrite Bool.negb_involutive in Hnn2.

    - move=> H.
      apply/pred0P => x.
      apply/andP => [[H1 Hn2]].
      rewrite inE /= in Hn2.
      move/negP in Hn2.
        by apply/Hn2/H.
  Qed.

(**
## boolean な論理式での証明
 *)

  Lemma mySubsetE (s1 s2 : pred T) :
    s1 \subset s2 = [forall x, (x \in s1) ==> (x \in s2)].
  Proof.
    apply/idP/idP.
    - move=> H.
      apply/forallP => x.
      apply/implyP.
      by apply/mySubsetP : x.

    - move=> H.
      apply/mySubsetP => x.
      move/forallP in H.
      by move: (H x) => {H} /implyP H /=.
  Qed.

(**
# 最初に使った箇所

単一化の証明 http://fetburner.hatenablog.com/entry/2015/12/06/224619

Unify.v を MathComp への移植するときに必要になりました。移植例：

https://github.com/suharahiromichi/coq/blob/master/unify/ssr_unify_bool_3.v
*)

(**
# おまけ

## 直接 boolean の式を証明する
 *)

  Lemma mySubsetE' (s1 s2 : pred T) :
    s1 \subset s2 = [forall x, (x \in s1) ==> (x \in s2)].
  Proof.
    rewrite subset_disjoint /disjoint.
    apply/idP/idP.
    - move/pred0P => H.
      apply/forallP => x.
      apply/implyP => Hs1.
      move: (H x) => {H} /= /eqP.
      rewrite inE eqbF_neg negb_and /=.
      move/orP => [Hn1 | Hnn2].
      + by move/negP : Hn1.
      + by rewrite Bool.negb_involutive in Hnn2.

    - move/forallP => H.
      apply/pred0P => x.
      move: (H x) => {H} /implyP H /=.
      apply/andP => [[H1 Hn2]].
      rewrite inE /= in Hn2.
      move/negP in Hn2.
        by apply/Hn2/H.
  Qed.

(**
# 補足

## 補足1. \subsetの定義について

MathComp での \subset の定義と同じものを ``mySubset1`` とします。
*)
  Definition mySubset1 (s1 s2 : pred T) := pred0b [predD s1 & s2].

(**
\subset は simplify タクティクが使えないようにロックされているので、
unlock する必要があります。``rewrite unlock`` すると判ります。
*)

  Goal forall  (s1 s2 : pred T),  s1 \subset s2 = mySubset1 s1 s2.
  Proof.
    move=> s1 s2.
    rewrite unlock /mySubset1.
    done.
  Qed.

(**
   predD は差集合を意味して、

``[predD A & B] == difference of collective predicates A and B.``

です。しかし、積集合 ``predI`` と、補集合 ``predC`` を使っても定義できるはずです。
``mySubset2`` に示します。
*)
  Definition mySubset2 (s1 s2 : pred T) := pred0b [predI s1 & [predC s2]].

(**
mySubset1 と mySubset2 が同じなのは自明ですが、
それを証明するためには、predI の可換性が必要になります。
その証明には、FunctionalExtension が必要になってしまいました。
*)
  Require Import Coq.Logic.FunctionalExtensionality.
  Goal forall (s1 s2 : pred T), predI s1 s2 = predI s2 s1.
  Proof.
    move=> s1 s2.
    rewrite /predI.
    rewrite /SimplPred.
    f_equal.
    apply: functional_extensionality => x.
      by rewrite Bool.andb_comm.
  Qed.

(**
FunctionalExtension を使わないで済ますために、pred0b までを含めて、
次の補題を証明してみました。あるいは、もっとよい方法があるかもしれません。
 *)
  Lemma predIComm (A B : pred T) : pred0b [predI A & B] = pred0b [predI B & A].
    apply/idP/idP.
    - move/pred0P => H.
      apply/pred0P.
      move=> x.
      move: (H x) => {H} /=.
        by rewrite Bool.andb_comm.
    - move/pred0P => H.
      apply/pred0P.
      move=> x.
      move: (H x) => {H} /=.
        by rewrite Bool.andb_comm.
  Qed.

  Goal forall  (s1 s2 : pred T),  mySubset1 s1 s2 = mySubset2 s1 s2.
  Proof.
    move=> s1 s2.
    rewrite /mySubset1 /mySubset2.
    by rewrite predIComm.
  Qed.

(**
## 補足2. MathComp の補題を使う

fintype で定義された subsetP は、リフレクティブ補題ですから、
``apply/`` と ``move/`` で適用します。[1.]の3.7節を参照してください。
*)

  Check @fintype.subsetP : forall (T : finType) (s1 s2 : pred T),
      reflect (forall x, x \in s1 -> x \in s2) (s1 \subset s2).

  Lemma mySubsetP' (s1 s2 : pred T) :
    s1 \subset s2 <-> (forall x, x \in s1 -> x \in s2).
  Proof.
    split.
    - by apply/subsetP.                     (* fintype.subsetP *)
    - by move/subsetP.                      (* fintype.subsetP *)
  Qed.

(**
fintype で定義された subsetE は、\subset の定義を展開したものでしかないので、
あまり使いではありません。

そこで、ここでも subsetP を使います。
*)
  Check @fintype.subsetE : forall (T : finType) (A B : pred T),
      (A \subset B) = pred0b [predD A & B].

  Lemma mySubsetE'' (s1 s2 : pred T) :
    s1 \subset s2 = [forall x, (x \in s1) ==> (x \in s2)].
  Proof.
      by apply/subsetP/forallP => H x; move/implyP: (H x).
  Qed.

(**
これは首記の御指摘のなかで教えていただいたものを使わせていただきました。
重ねて感謝します。
*)

End Test.

(**
# 参考文献

[1.] 萩原学 アフェルト・レナルド 「Coq/SSReflect/MathCompによる定理証明」 森北出版

*)

(* END *)

author: suharahiromichi

repo: coq

save_path: github-repos/coq/suharahiromichi-coq


text:
From Undecidability.L.Prelim Require Import ARS MoreBase.

Definition loopSum {X} {Y} :=
  fix loopSum n (f:X -> X + Y) (x:X) {struct n}:=
  match n with
    0 => None
  | S n => match f x with
          | inl x' => loopSum n f x'
          | inr y => Some y
          end
  end.

Arguments loopSum _ _ !_.

Definition loopSum_mono X Y f x y n n':
  n <= n' -> @loopSum X Y n f x = Some y -> loopSum n' f x = Some y.
Proof.
  induction n in n',x|-*;intros H. now inversion 1.
  -inv H. easy. cbn. destruct _. 2:easy. apply IHn. lia.
Qed.

Lemma loopSum_sound_rel X Y {R:X->X->Prop} k n x y (f: X -> X + Y):
  (forall x y, R x y -> f x = inl y) ->
  pow R k x y ->
  loopSum (k+n) f x = loopSum n f y.
Proof.
  intros H1 R1.
  induction k in R1,x|-*.
  -inv R1. reflexivity.
  -change (S k) with (1+k) in R1. eapply pow_add in R1 as (x'&R2&R1).
   eapply rcomp_1 in R2. apply H1 in R2. cbn.
   rewrite R2. now apply IHk.
Qed.

Lemma loopSum_rel_correct2 X Y {R:X->X->Prop} k x y (f: X -> X + Y):
  (forall x, match f x with
        | inl y => R x y
        | inr _ => terminal R x
        end)->
  loopSum k f x = Some y ->
  exists i x', i < k /\ loopSum k f x = loopSum (k-i) f x'
          /\ pow R i x x'
          /\ terminal R x'
          /\ f x' = inr y.
Proof.
  intros H1 Heq.
  induction k in Heq,x|-*. now inv Heq.
  cbn in Heq.
  specialize (H1 x).
  destruct (f x) eqn:eqf.
  -eapply IHk in Heq as (i&x'&?&?&?&?&?).
   eexists (1 + i),x'.
   repeat eapply conj.
   +lia.
   +cbn. rewrite eqf. easy.
   +eapply pow_add;do 2 esplit.
    eapply rcomp_1 with (R:=R). all:eassumption.
   +easy.
   +easy.
  -inv Heq.
   exists 0,x.
   repeat eapply conj.
   all:solve [easy|lia].
Qed.

Definition optionFToSum {X} f (x:X) : X + X :=
  match f x with
    None => inr x
  | Some y => inl y
  end.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
Goal forall x, x = 0 -> S x = 7 -> x = 22 .
Proof.
replace 0 with 33.
Undo.
intros x H H0.
replace x with 0.
Undo.
replace x with 0 in  |- *.
Undo.
replace x with 1 in *.
Undo.
replace x with 0 in *|- *.
Undo.
replace x with 0 in *|-.
Undo.
replace x with 0 in H0 .
Undo.
replace x with 0 in H0 |- * .
Undo.

replace x with 0 in H,H0 |- * .
Undo.
Admitted.

(* This failed at some point when "replace" started to support arguments
   with evars but "abstract" did not supported any evars even defined ones *)

Class U.
Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0.
replace (f _) with 0 by abstract apply H.
reflexivity.
Qed.

repo: Coq-misc