ITree.Extra.Secure.SecureEqProgInsensFacts

From ITree Require Import
     Axioms
     ITree
     ITreeFacts.

From ITree.Extra Require Import
     Secure.SecureEqHalt
     Secure.SecureEqProgInsens
.

From Paco Require Import paco.

Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.

Variant case_rel {A1 A2 B : Type} (R1 : B Prop) (R2 : B Prop) : ( + ) B Prop :=
  | crl a1 b : b case_rel (inl ) b
  | crr a2 b : b case_rel (inr ) b.

Lemma pi_eqit_secure_iter_ret E R S1 S2 Label priv l b2 s body
      (Rinv : R Prop) (RS : Prop)
  (HRinv : ( r', Rinv r' s
            pi_eqit_secure Label priv (case_rel Rinv RS) true l (body r') (Ret s) )) :
   r,
  Rinv r s
  @pi_eqit_secure E Label priv RS true l (ITree.iter body r) (Ret s).
Proof.
  ginit. gcofix CIH. intros . setoid_rewrite unfold_iter.
  assert (pi_eqit_secure Label priv (case_rel Rinv RS) true l (body ) (Ret s)).
  auto. remember (body ) as t. clear Heqt. generalize dependent t.
  gcofix CIH'. intros t Ht.
  destruct (observe t) eqn : Heq; symmetry in Heq; apply simpobs in Heq.
  - rewrite Heq.
    assert (pi_eqit_secure Label priv (case_rel Rinv RS) true l (Ret ) (Ret s) ).
    rewrite Heq. auto.
    pinversion H. subst. inv .
    + rewrite bind_ret_l. gstep. constructor; auto.
      gfinal. left. eapply CIH; eauto.
    + rewrite bind_ret_l. gstep. constructor. auto.
  - rewrite Heq. rewrite bind_tau. gstep. constructor; auto.
    gfinal. left. eapply CIH'.
    assert (pi_eqit_secure Label priv (case_rel Rinv RS) true l (Tau ) (Ret s)).
    rewrite Heq. auto. pinversion H. rewrite itree_eta. auto.
  - destruct (classic (leq (priv _ e) l ) ).
    + exfalso. apply HRinv in .
      assert (pi_eqit_secure Label priv (case_rel Rinv RS) true l (Vis e k) (Ret s) ).
      { rewrite Heq. auto. }
      pinversion ; subst. ddestruction. subst. contradiction.
    + rewrite Heq. rewrite bind_vis.
      gstep. constructor; auto. intros x. gfinal. left. eapply CIH'.
      assert ( pi_eqit_secure Label priv (case_rel Rinv RS) true l (Vis e k) (Ret s)) .
      rewrite Heq. auto. pinversion ; subst; ddestruction; subst.
      rewrite itree_eta. apply .
Qed.


Ltac use_simpobs :=
  repeat match goal with
         | H : TauF _ = observe ?t |- _apply simpobs in H
         | H : RetF _ = observe ?t |- _apply simpobs in H
         | H : VisF _ _ = observe ?t |- _apply simpobs in H
  end.

(* I believe we could generalize this lemma for any t2 that converges along all paths *)
Lemma pi_eqit_secure_trans_ret E R1 R2 R3 Label priv l b1 b2
      (RR1 : Prop) (RR2 : Prop)
      (t1 : itree E ) (r : ) (t3 : itree E ) :
  pi_eqit_secure Label priv l (Ret r)
  pi_eqit_secure Label priv l (Ret r)
  pi_eqit_secure Label priv (rcompose ) l .
Proof.
  revert . ginit. gcofix CIH.
  intros. pinversion ; subst; try inv CHECK; use_simpobs.
  - rewrite H. generalize dependent . gcofix CIH'. intros .
    pinversion ; use_simpobs.
    + rewrite . gstep. constructor; auto. econstructor; eauto.
    + rewrite . gstep. constructor; auto. gfinal. left. eapply CIH'.
      symmetry in . use_simpobs. rewrite in . auto.
    + rewrite . gstep. constructor; auto. intros. gfinal. left.
      eapply CIH'. symmetry in . use_simpobs. setoid_rewrite in . apply .
  - symmetry in . use_simpobs. rewrite H. gstep. constructor; auto.
    gfinal. left. eapply CIH; auto. rewrite . auto.
  - symmetry in . use_simpobs. rewrite H. gstep. constructor; auto.
    intros. gfinal. left. apply CIH; auto. rewrite . apply .
Qed.


Lemma pi_eqit_secure_pub_vis E R1 R2 RR Label priv l b1 b2 A (e : E A)
      (k1 : A itree E ) (k2 : A itree E ) :
  leq (priv _ e) l
  ( a, pi_eqit_secure Label priv RR l ( a) ( a) )
  pi_eqit_secure Label priv RR l (Vis e ) (Vis e ).
Proof.
  intros. pfold. constructor; auto. left. apply .
Qed.


Lemma pi_eqit_secure_priv_vislr E R1 R2 RR Label priv l b1 b2 A B (e1 : E A) (e2 : E B)
      (k1 : A itree E ) (k2 : B itree E ) :
  ¬ leq (priv _ ) l ¬ leq (priv _ ) l
  ( a b, pi_eqit_secure Label priv RR l ( a) ( b) )
  pi_eqit_secure Label priv RR l (Vis ) (Vis ).
Proof.
  intros. pfold. constructor; auto. left. apply .
Qed.


Lemma pi_eqit_secure_priv_visl E R1 R2 RR Label priv l b2 A (e1 : E A)
      (k1 : A itree E ) (t2 : itree E ) :
  ¬ leq (priv _ ) l
  ( a, pi_eqit_secure Label priv RR true l ( a) )
  pi_eqit_secure Label priv RR true l (Vis ) .
Proof.
  intros. pfold. constructor; auto. left. apply .
Qed.


Lemma pi_eqit_secure_priv_visr E R1 R2 RR Label priv l b1 A (e1 : E A)
      (t1 : itree E ) (k2 : A itree E ) :
  ¬ leq (priv _ ) l
  ( a, pi_eqit_secure Label priv RR true l ( a) )
  pi_eqit_secure Label priv RR true l (Vis ).
Proof.
  intros. pfold. constructor; auto. left. apply .
Qed.


Lemma pi_secure_eqit_bind'
     : (E : Type Type) (R1 R2 S1 S2 : Type) (RR : Prop)
         (RS : Prop) (b1 b2 : bool) (Label : Preorder)
         (priv : A : Type, E A L) (l : L)
         r
         (t1 : itree E ) (t2 : itree E ) (k1 : itree E )
         (k2 : itree E ),
       ( (r1 : ) (r2 : ),
        RR (pi_secure_eqit_ Label priv RS l id) r ( ) ( ))
       pi_eqit_secure Label priv RR l
        (pi_secure_eqit_ Label priv RS l id) (eqitC RS ) r
              (ITree.bind ) (ITree.bind ).
Proof.
  intros. revert . generalize dependent . generalize dependent .
  gcofix CIH. intros .
  pinversion ; use_simpobs.
  - rewrite , . repeat rewrite bind_ret_l. gfinal. right. eapply paco2_mon; try apply .
    auto.
  - rewrite , . repeat rewrite bind_tau. gstep. constructor. gfinal. left. eapply CIH.
    auto.
  - rewrite . rewrite bind_tau. gstep. constructor; auto.
    gfinal. left. eapply CIH. apply simpobs in . rewrite itree_eta in .
    rewrite . auto.
  - rewrite . rewrite bind_tau. gstep. constructor; auto.
    gfinal. left. eapply CIH. apply simpobs in . rewrite itree_eta in .
    rewrite . auto.
  - rewrite , . repeat rewrite bind_vis. gstep. constructor; auto.
    intros. gfinal. left. eapply CIH; eauto. apply .
  - rewrite , . rewrite bind_vis, bind_tau. gstep. red. cbn. unpriv_pi.
    gfinal. left. eapply CIH; eauto. apply .
  - rewrite , . rewrite bind_vis, bind_tau. gstep. red. cbn. unpriv_pi.
    gfinal. left. eapply CIH; eauto. apply .
  - rewrite , . repeat rewrite bind_vis. gstep. red. cbn. unpriv_pi.
    gfinal. left. eapply CIH. apply .
  - rewrite . rewrite bind_vis. gstep. constructor; auto. gfinal.
    left. eapply CIH. apply simpobs in . rewrite itree_eta in . rewrite .
    apply .
  - rewrite . rewrite bind_vis. gstep. constructor; auto. gfinal.
    left. eapply CIH. apply simpobs in . rewrite itree_eta in . rewrite .
    apply .
Qed.