Require Import ZArith.

Variable eqdec : forall {A} (x y:A), {x=y}+{x<>y}.
Variable extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g.

Variable Label : Set.
Variable Channel : Set.
Variable label : Channel -> Label.
Variable Value : Set.
Definition LabeledValueSeq := list (Value * Label).
Variable Key : Set.
Definition Store := Key -> LabeledValueSeq.
Variable Code : Set.
Inductive Thread :=
  Thrd : Code -> Label -> Thread.
Definition Threads := Thread -> nat.
Definition ReadContinuation := LabeledValueSeq -> Code.
Inductive Operation :=
  | Read : Key -> ReadContinuation -> Operation
  | Write : Key -> Value -> Code -> Operation
  | Delete : Key -> Code -> Operation
  | GetAllKeys : ReadContinuation -> Operation
  | Send : Channel -> Value -> Code -> Operation
  | Fork : Code -> Code -> Operation
  | RaiseLabel : Label -> Code -> Operation
  | Stuck : Operation
  .
Inductive Event :=
  | Input : Thread -> Event
  | Output : Channel -> Value -> Event
  | Epsilon : Event
  .
Inductive State :=
  St : Store -> Threads -> State.
Variable run : Code -> Operation.
Variable Flows : Label -> Label -> Prop.
Variable Flows_dec : forall l1 l2, {Flows l1 l2}+{~Flows l1 l2}.
Variable Flows_trans : forall l1 l2 l3, Flows l1 l2 -> Flows l2 l3 -> Flows l1 l3.
Fixpoint delete (S:LabeledValueSeq) l : LabeledValueSeq :=
  match S with
  | nil =>
      nil
  | cons (v', l') S' =>
      if Flows_dec l l' then
        delete S' l
      else
        cons (v', l') (delete S' l)
  end.
Definition write (S:LabeledValueSeq) v l : LabeledValueSeq :=
  cons (v, l) (delete S l).
Fixpoint pS (S:LabeledValueSeq) l : LabeledValueSeq :=
  match S with
  | nil =>
      nil
  | cons (v', l') S' =>
      if Flows_dec l' l then
        cons (v', l') (pS S' l)
      else
        pS S' l
  end.
Definition thread_label t :=
  match t with
  | Thrd _ l => l
  end.
Definition pts (ts:Threads) l : Threads :=
  fun t =>
    if Flows_dec (thread_label t) l then
      ts t
    else
      0
  .
Definition px (x:Store) l : Store :=
  fun k =>
    pS (x k) l
  .
Definition pe e l : Event :=
  match e with
  | Input t =>
      if Flows_dec (thread_label t) l then
        e
      else
        Epsilon
  | Output ch v =>
      if Flows_dec (label ch) l then
        e
      else
        Epsilon
  | Epsilon =>
      Epsilon
  end
  .
Definition pX (X:State) l : State :=
  match X with
  | St x ts => St (px x l) (pts ts l)
  end
  .
Definition multi_one (t:Thread) : Threads :=
  fun t' =>
    if eqdec t' t then
      1
    else
      0
  .
Definition multi_two (t1:Thread) (t2:Thread) : Threads :=
  fun t' =>
    if eqdec t' t1 then
      1
    else if eqdec t' t2 then
      1
    else
      0
  .
Definition upd (x:Store) k S : Store :=
  fun k' =>
    if eqdec k k' then
      S
    else
      x k'
  .
Inductive Step : Store -> Thread -> Event -> State -> Prop :=
  | SSend : forall x c l ch v c',
      run c = Send ch v c' ->
      Flows l (label ch) ->
      Step x (Thrd c l) (Output ch v) (St x (multi_one (Thrd c' l)))
  | SRead : forall x c l f k,
      run c = Read k f ->
      Step x (Thrd c l) Epsilon (St x (multi_one (Thrd (f (pS (x k) l)) l)))
  | SWrite : forall x c l k v c',
      run c = Write k v c' ->
      Step x (Thrd c l) Epsilon (St (upd x k (write (x k) v l)) (multi_one (Thrd c' l)))
(*
  | SDelete : forall c k c' x l,
      run c = Delete k c' ->
      Step x (Thrd c l) Epsilon (St (upd x k (delete (x k) l)) (multi_one (Thrd c' l)))
  | SGetAllKeys : forall c f x l,
      run c = GetAllKeys f ->
      Step x (Thrd c l) Epsilon (St x (multi_one (Thrd (f (getallkeys x l)) l)))
*)
  | SFork : forall x c l c1 c2,
      run c = Fork c1 c2 ->
      Step x (Thrd c l) Epsilon (St x (multi_two (Thrd c1 l) (Thrd c2 l)))
  | SRaiseLabel : forall c l' c' x l,
      run c = RaiseLabel l' c' ->
      Flows l l' ->
      Step x (Thrd c l) Epsilon (St x (multi_one (Thrd c' l')))
  .
Definition multi_cons (ts:Threads) t : Threads :=
  fun t' =>
    if eqdec t t' then
      1 + ts t'
    else
      ts t'
  .
Definition multi_plus (ts1 ts2:Threads) : Threads :=
  fun t =>
    ts1 t + ts2 t
  .
Inductive SStep : State -> Event -> State -> Prop :=
  | SSStart : forall x ts t,
      SStep (St x ts) (Input t) (St x (multi_cons ts t))
  | SSSkip : forall X,
      SStep X Epsilon X
  | SSThread : forall x ts c l e x' ts',
      Step x (Thrd c l) e (St x' ts') ->
      SStep (St x (multi_cons ts (Thrd c l))) e (St x' (multi_plus ts ts'))
  .

Definition ConjectureTSNI := forall X1 l X2 e1 X1',
  pX X1 l = pX X2 l ->
  SStep X1 e1 X1' ->
  exists X2' e2,
      SStep X2 e2 X2'
    /\
      pX X1' l = pX X2' l
    /\
      pe e1 l = pe e2 l
  .

Fixpoint pes (es : list Event) (l : Label) : list Event :=
  match es with
  | nil => nil
  | cons e xxx => cons (pe e l) (pes xxx l)
  end
  .
Inductive SStepStar : State -> list Event -> State -> Prop :=
  | StarNil : forall X,
      SStepStar X nil X
  | StarCons : forall X e X' es X'',
      SStep X e X' ->
      SStepStar X' es X'' ->
      SStepStar X (cons e es) X''
  .
Definition ConjectureTSNIStar := forall X1 l es1 X1',
  SStepStar X1 es1 X1' ->
  forall X2,
  pX X1 l = pX X2 l ->
  exists X2' es2,
      SStepStar X2 es2 X2'
    /\
      pX X1' l = pX X2' l
    /\
      pes es1 l = pes es2 l
  .

(****************)

Definition LSStep X1 e L X2 := exists e' X2', SStep X1 e' X2' /\ pe e' L = e /\ pX X2' L = X2.

Lemma lemma_pts_multicons_1 : forall ts c l l',
  Flows l' l ->
  pts (multi_cons ts (Thrd c l')) l = multi_cons (pts ts l) (Thrd c l')
  .
Proof.
  intros.
  apply extensionality.
  intros.
  unfold pts, multi_cons, thread_label.
  destruct (eqdec (Thrd c l') x).
  -
    destruct x as (c2, l2).
    injection e; intros.
    rewrite <- H0.
    destruct (Flows_dec l' l); intuition.
  -
    reflexivity.
Qed.

Lemma lemma_pts_multicons_2 : forall ts c l l',
  ~Flows l' l ->
  pts (multi_cons ts (Thrd c l')) l = pts ts l
  .
Proof.
  intros.
  apply extensionality.
  intros.
  unfold pts, multi_cons, thread_label.
  destruct (eqdec (Thrd c l') x).
  -
    destruct x as (c2, l2).
    injection e; intros.
    rewrite <- H0.
    destruct (Flows_dec l' l); intuition.
  -
    reflexivity.
Qed.

Lemma lemma_pts_multiplus : forall ts1 ts2 l ,
  pts (multi_plus ts1 ts2) l = multi_plus (pts ts1 l) (pts ts2 l)
  .
Proof.
  intros.
  apply extensionality.
  intro t.
  destruct t as (c, l').
  unfold pts, multi_plus, thread_label.
  destruct (Flows_dec l' l)
  ; reflexivity.
Qed.

Lemma lemma_multiplus_zero : forall ts,
  multi_plus ts (fun t => 0) = ts.
Proof.
  intros.
  unfold multi_plus.
  apply extensionality; intro t.
  omega.
Qed.

Lemma lemma_pts_multione : forall c l' l,
  Flows l' l ->
  pts (multi_one (Thrd c l')) l = multi_one (Thrd c l')
  .
  intros.
  unfold pts, multi_one, thread_label.
  apply extensionality.
  intro t.
  destruct t.
  destruct (Flows_dec l0 l); auto.
  destruct (eqdec (Thrd c0 l0) (Thrd c l')).
    congruence.
  trivial.
Qed.

Lemma lemma_pts_multitwo : forall c1 c2 l' l,
  Flows l' l ->
  pts (multi_two (Thrd c1 l') (Thrd c2 l')) l = multi_two (Thrd c1 l') (Thrd c2 l')
  .
  intros.
  unfold pts, multi_two, thread_label.
  apply extensionality.
  intro t.
  destruct t.
  destruct (Flows_dec l0 l); auto.
  destruct (eqdec (Thrd c l0) (Thrd c1 l')).
    congruence.
  destruct (eqdec (Thrd c l0) (Thrd c2 l')).
    congruence.
  trivial.
Qed.

Lemma lemma_invisibility_1 : forall x c l' e x' ts' l,
  ~Flows l' l ->
  Step x (Thrd c l') e (St x' ts') ->
  px x' l = px x l
  .
Proof.
  intros.
  rename H into T1, H0 into T2.
  inversion T2; auto.
  unfold px, upd, write.
  apply extensionality; intro k'.
  destruct (eqdec k k'); auto.
  simpl.
  destruct (Flows_dec l' l); try congruence.
  rewrite <- e0.
  clear H4.
  induction (x k); auto.
  simpl.
  destruct a.
  destruct (Flows_dec l2 l).
  - (* This case is copy-pasted below *)
    destruct (Flows_dec l' l2).
      pose (Flows_trans l' l2 l).
      intuition.  (* contradiction *)
    simpl.
    destruct (Flows_dec l2 l); congruence.
  - (* This case is copy-pasted from above *)
    destruct (Flows_dec l' l2).
      pose (Flows_trans l' l2 l).
      intuition.  (* contradiction *)
    simpl.
    destruct (Flows_dec l2 l); congruence.
Qed.

Lemma lemma_invisibility_2 : forall x c l' e x' ts' l,
  ~Flows l' l ->
  Step x (Thrd c l') e (St x' ts') ->
  pe e l = Epsilon
  .
Proof.
  intros.
  rename H0 into T1.
  inversion T1; auto.
  simpl.
  destruct (Flows_dec (label ch) l); auto.
  pose (Flows_trans l' (label ch) l).
  intuition.  (* There's a contradiction. *)
Qed.

Lemma lemma_invisibility_3 : forall x c l' e x' ts' l,
  ~Flows l' l ->
  Step x (Thrd c l') e (St x' ts') ->
  pts ts' l = fun t => 0
  .
Proof.
  intros.
  rename H0 into T1.
  apply extensionality; intro t.
  destruct t as (c'', l'').
  unfold pts, thread_label.
  destruct (Flows_dec l'' l); auto.
  inversion T1.
  - unfold multi_one.
    destruct (eqdec (Thrd c'' l'') (Thrd c' l'))
    ; congruence.
  - unfold multi_one.
    destruct (eqdec (Thrd c'' l'') (Thrd (f0 (pS (x' k) l')) l'))
    ; congruence.
  - unfold multi_one.
    destruct (eqdec (Thrd c'' l'') (Thrd c' l'))
    ; congruence.
  - unfold multi_two.
    destruct (eqdec (Thrd c'' l'') (Thrd c1 l'))
    ; destruct (eqdec (Thrd c'' l'') (Thrd c2 l'))
    ; congruence.
  - unfold multi_one.
    destruct (eqdec (Thrd c'' l'') (Thrd c' l'0)).
      injection e0; intros.
      rewrite H8 in *.
      pose (Flows_trans l' l'0 l).
      intuition.  (* it's a contradiction *)
    reflexivity.
Qed.

Lemma lemma_px_upd : forall l' l x k v,
  Flows l' l ->
  px (upd x k (write (x k) v l')) l = upd (px x l) k (write ((px x l) k) v l')
  .
Proof.
  intros.
  apply extensionality; intro k'.
  unfold px, upd, write.
  destruct (eqdec k k'); auto.
  simpl.
  destruct (Flows_dec l' l); intuition.
  simpl.
  apply f_equal.
  clear.
  induction (x k).
    reflexivity.
  destruct a.
  simpl.
  destruct (Flows_dec l' l1)
  ; simpl
  ; destruct (Flows_dec l1 l)
  ; simpl
  ; destruct (Flows_dec l' l1)
  ; intuition congruence.
Qed.

Lemma lemma_read_helper : forall x' k l' l,
  Flows l' l ->
  pS (x' k) l' = pS (px x' l k) l'
  .
Proof.
  intros.
  unfold px.
  induction (x' k).
    reflexivity.
  destruct a.
  simpl.
  pose (Flows_trans l1 l' l).
  destruct (Flows_dec l1 l')
  ; simpl
  ; destruct (Flows_dec l1 l)
  ; simpl
  ; destruct (Flows_dec l1 l')
  ; intuition congruence.
Qed.

Lemma lemma_idemp_px : forall x l,
  px (px x l) l = px x l.
Proof.
  intros.
  apply extensionality; intro k.
  unfold px.
  induction (x k).
    reflexivity.
  destruct a.
  simpl.
  destruct (Flows_dec l1 l)
  ; simpl
  ; destruct (Flows_dec l1 l)
  ; congruence.
Qed.

Lemma lemma_idemp_pts : forall ts l,
  pts (pts ts l) l = pts ts l.
Proof.
  intros.
  apply extensionality; intro t; destruct t as (c', l').
  unfold pts, thread_label.
  destruct (Flows_dec l' l); reflexivity.
Qed.

Lemma lemma_pts_multicons_pts : forall ts l t,
  pts (multi_cons (pts ts l) t) l = pts (multi_cons ts t) l.
Proof.
  intros.
  apply extensionality; intro t'; destruct t' as (c', l').
  unfold pts, multi_cons, thread_label.
  destruct (Flows_dec l' l); destruct (eqdec t (Thrd c' l')); auto.
Qed.

Lemma lemma_pts_multiplus_pts : forall ts l ts',
  pts (multi_plus (pts ts l) ts') l = pts (multi_plus ts ts') l.
Proof.
  intros.
  apply extensionality; intro t'; destruct t' as (c', l').
  unfold pts, multi_plus, thread_label.
  destruct (Flows_dec l' l); auto.
Qed.

Lemma lemma_idemp_pX : forall X l,
  pX (pX X l) l = pX X l.
Proof.
  intros.
  destruct X as (x, ts).
  simpl.
  rewrite lemma_idemp_px.
  rewrite lemma_idemp_pts.
  reflexivity.
Qed.

Lemma lemma_multicons_multiplus_multione : forall ts t,
  multi_cons ts t = multi_plus ts (multi_one t).
Proof.
  intros.
  apply extensionality; intro t'.
  unfold multi_cons, multi_plus, multi_one.
  destruct (eqdec t t')
  ; destruct (eqdec t' t)
  ; try congruence
  ; omega
  .
Qed.

Theorem projection_1 : forall X e X' l,
  SStep X e X' ->
  LSStep (pX X l) (pe e l) l (pX X' l)
  .
Proof.
  destruct 1 as [| |? ? ? l'].
  -
    do 2 eexists.
    split; [|split].
    + apply SSStart.
    + reflexivity.
    + unfold pX.
      rewrite lemma_idemp_px.
      rewrite lemma_pts_multicons_pts.
      reflexivity.
  -
    do 2 eexists.
    split; [|split].
    + apply SSSkip.
    + reflexivity.
    + apply lemma_idemp_pX.
  -
    destruct (Flows_dec l' l); cycle 1.
    +
      do 2 eexists; split; [|split].
      *
        apply SSSkip.
      *
        destruct e as [|ch v|].
        --  inversion H.
        --  inversion H.
            simpl.
            destruct (Flows_dec (label ch) l); auto.
            pose (Flows_trans l' (label ch) l).
            intuition.  (* contradiction *)
        --  reflexivity.
      *
        simpl.
        rewrite lemma_pts_multiplus.
        rewrite lemma_idemp_px.
        erewrite <- lemma_invisibility_1; cycle 1.
            exact n.
          exact H.
        rewrite lemma_idemp_pts.
        rewrite lemma_pts_multicons_2; auto.
        erewrite lemma_invisibility_3 with (ts' := ts') ; cycle 1.
            exact n.
          exact H.
        rewrite lemma_multiplus_zero.
        reflexivity.
    +
      simpl.
      rewrite lemma_pts_multicons_1; auto.
      inversion H.
      *
        destruct (Flows_dec (label ch) l).
        --
            do 2 eexists; split; [|split].
            ++  apply SSThread.
                apply SSend.
                  exact H5.
                assumption.
            ++  reflexivity.
            ++  simpl.
                rewrite lemma_idemp_px.
                rewrite lemma_pts_multiplus_pts.
                reflexivity.
        --
            do 2 eexists; split; [|split].
            ++  apply SSThread.
                apply SSend.
                  exact H5.
                assumption.
            ++  unfold pe.
                destruct (Flows_dec (label ch) l); intuition.
            ++  simpl.
                rewrite lemma_idemp_px.
                rewrite lemma_pts_multiplus_pts.
                reflexivity.
      *
        do 2 eexists; split; [|split].
        --  apply SSThread.
            apply SRead.
            exact H4.
        --  reflexivity.
        --  simpl.
            rewrite lemma_idemp_px.
            rewrite lemma_pts_multiplus_pts.
            rewrite <- lemma_read_helper with (l := l); auto.
      *
        do 2 eexists; split; [|split].
        --  apply SSThread.
            apply SWrite.
            exact H4.
        --  reflexivity.
        --  simpl.
            rewrite lemma_px_upd; auto.
            rewrite lemma_px_upd; auto.
            rewrite lemma_idemp_px.
            rewrite lemma_pts_multiplus_pts.
            reflexivity.
      *
        do 2 eexists; split; [|split].
        --  apply SSThread.
            apply SFork.
            exact H4.
        --  reflexivity.
        --  simpl.
            rewrite lemma_idemp_px.
            rewrite lemma_pts_multiplus_pts.
            reflexivity.
      *
        do 2 eexists; split; [|split].
        --  apply SSThread.
            apply SRaiseLabel.
              exact H5.
            exact H7.
        --  reflexivity.
        --  simpl.
            rewrite lemma_idemp_px.
            rewrite lemma_pts_multiplus_pts.
            reflexivity.
Qed.

Lemma apply_equation : forall {A}{B} {f g:A->B},
  f = g ->
  forall x,
  f x = g x.
  congruence.
Qed.

Theorem projection_2 : forall X l e1 X1,
  LSStep (pX X l) e1 l X1 ->
  exists X2 e2,
      SStep X e2 X2
    /\
      X1 = pX X2 l
    /\
      e1 = pe e2 l
  .
Proof.
  destruct X as (x, ts).
  destruct 1 as (e', (X', (T8, (T9, T10)))).
  inversion T8.
  -
    destruct t as (c, l0).
    exists (St x (multi_cons ts (Thrd c l0))).
    exists (Input (Thrd c l0)).
    repeat split.
    + apply SSStart.
    + rewrite <- T10.
      rewrite <- H3.
      simpl.
      rewrite lemma_idemp_px.
      rewrite lemma_pts_multicons_pts.
      reflexivity.
    + rewrite <- T9.
      rewrite <- H2.
      reflexivity.
  -
    do 2 eexists.
    split; [|split].
    + apply SSSkip.
    + rewrite <- T10.
      rewrite <- H1.
      simpl.
      rewrite lemma_idemp_px.
      rewrite lemma_idemp_pts.
      reflexivity.
    + rewrite <- T9.
      rewrite <- H0.
      reflexivity.
  -
    rename H1 into T2, H3 into T3.
    assert (Flows l0 l).
      remember (apply_equation T2 (Thrd c l0)) as T4; clear HeqT4.
      unfold multi_cons, pts, thread_label in T4.
      destruct (eqdec (Thrd c l0) (Thrd c l0)); intuition.
      destruct (Flows_dec l0 l); auto.
      omega.
    pose (ts_ := fun t => if eqdec (Thrd c l0) t then ts t - 1 else ts t).
    assert (ts = multi_cons ts_ (Thrd c l0)) as T5.
      remember (apply_equation T2 (Thrd c l0)) as T4; clear HeqT4.
      unfold multi_cons, pts, thread_label in T4.
      destruct (eqdec (Thrd c l0) (Thrd c l0)); destruct (Flows_dec l0 l); intuition.
      unfold multi_cons, ts_.
      apply extensionality; intro t.
      destruct (eqdec (Thrd c l0) t) as [T5|]; auto.
      rewrite T5 in T4.
      omega.
    assert (pts ts_ l = ts0) as T6.
      apply extensionality; intro t.
      generalize (apply_equation T2 t).
      destruct t.
      unfold ts_, multi_cons, pts, thread_label.
      destruct (eqdec (Thrd c l0) (Thrd c0 l1)); try omega.
      destruct (Flows_dec l1 l); omega.
    inversion T3.
    + (* This case is copy-pasted and copy-paste-edited below. *)
      rewrite T5.
      do 2 eexists.
      repeat split.
      * apply SSThread.
        apply SSend.
          exact H8.
        assumption.
      * rewrite <- T10.
        rewrite <- H2.
        simpl.
        rewrite <- T6.
        rewrite lemma_pts_multiplus_pts.
        rewrite <- H6.
        rewrite lemma_idemp_px.
        rewrite <- H9.
        reflexivity.
      * congruence.
    +
      rewrite T5.
      do 2 eexists.
      repeat split.
      * apply SSThread.
        apply SRead.
        exact H7.
      * rewrite <- T10.
        rewrite <- H2.
        simpl.
        rewrite <- T6.
        rewrite lemma_pts_multiplus_pts.
        rewrite <- H8.
        rewrite lemma_idemp_px.
        rewrite <- H9.
        rewrite lemma_pts_multiplus.
        rewrite lemma_pts_multiplus.
        rewrite lemma_pts_multione; auto.
        rewrite lemma_pts_multione; auto.
        rewrite <- lemma_read_helper with (l := l); auto.
      * congruence.
    +
      rewrite T5.
      do 2 eexists.
      repeat split.
      * apply SSThread.
        apply SWrite.
        exact H7.
      * rewrite <- T10.
        rewrite <- H2.
        simpl.
        rewrite <- T6.
        rewrite lemma_pts_multiplus_pts.
        rewrite <- H8.
        rewrite lemma_px_upd; auto.
        rewrite lemma_px_upd; auto.
        rewrite lemma_idemp_px.
        rewrite <- H9.
        reflexivity.
      * congruence.
    +
      rewrite T5.
      do 2 eexists.
      repeat split.
      * apply SSThread.
        apply SFork.
        exact H7.
      * rewrite <- T10.
        rewrite <- H2.
        simpl.
        rewrite <- T6.
        rewrite lemma_pts_multiplus_pts.
        rewrite <- H8.
        rewrite lemma_idemp_px.
        rewrite <- H9.
        reflexivity.
      * congruence.
    +
      rewrite T5.
      do 2 eexists.
      repeat split.
      * apply SSThread.
        apply SRaiseLabel.
          exact H8.
        auto.
      * rewrite <- T10.
        rewrite <- H2.
        simpl.
        rewrite <- T6.
        rewrite lemma_pts_multiplus_pts.
        rewrite <- H6.
        rewrite lemma_idemp_px.
        rewrite <- H9.
        reflexivity.
      * congruence.
Qed.

Theorem tsni : ConjectureTSNI.
Proof.
  unfold ConjectureTSNI.
  intros.
  rename H into T1, H0 into T2.
  apply projection_2.
  rewrite <- T1.
  apply projection_1.
  exact T2.
Qed.

Theorem tsni_star : ConjectureTSNIStar.
Proof.
  induction 1.
  -
    do 2 eexists.
    split.
      apply StarNil.
    auto.
  -
    rename X into X1, X' into X1', X'' into X1'', es into es1, H into T1, H0 into T2.
    intros X2 T3.
    edestruct tsni as (X2', (e2, (T4, (T5, T6)))).
        exact T3.
      exact T1.
    destruct IHSStepStar with X2' as (X2'', (es2, (T7, (T8, T9)))).
      exact T5.
    exists X2''.
    exists (cons e2 es2).
    intuition.
      apply StarCons with X2'; assumption.
    simpl.
    congruence.
Qed.