ITree.Extra.Secure.SecureEqEuttHalt
From Coq Require Import Morphisms.
From ITree Require Import
Axioms
ITree
ITreeFacts.
From ITree.Extra Require Import
Secure.Labels
Secure.SecureEqHalt
.
From Paco Require Import paco.
Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.
Lemma tau_eqit_secure : ∀ E R1 R2 Label priv l RR (t1 : itree E R1) (t2 : itree E R2),
eqit_secure Label priv RR true true l (Tau t1) t2 → eqit_secure Label priv RR true true l t1 t2.
Proof.
intros E R1 R2 Label priv l RR. intros t1 t2 Hsec. pstep. red.
punfold Hsec. red in Hsec. cbn in ×. remember (TauF t1) as x.
hinduction Hsec before priv; intros; inv Heqx; pclearbot; try inv CHECK; auto with itree.
- constructor; auto. pstep_reverse.
- unpriv_ind. pstep_reverse.
- punfold H.
Qed.
Lemma unpriv_e_eqit_secure : ∀ E A R1 R2 Label priv l RR (e : E A) (k : A → itree E R1)
(t : itree E R2),
(¬leq (priv A e) l ) →
eqit_secure Label priv RR true true l (Vis e k) t →
∀ a, eqit_secure Label priv RR true true l (k a) t.
Proof.
intros. generalize dependent t. rename H into Hunpriv. generalize dependent a.
intros. punfold H0. red in H0. cbn in ×. pfold. red.
remember (VisF e k) as x. genobs_clear t ot.
hinduction H0 before l; intros; try inv Heqx;
ddestruction; subst; try contradiction; try contra_size; auto.
- constructor; auto. eapply IHsecure_eqitF; eauto.
- pclearbot. constructor; auto. pstep_reverse.
- unpriv_ind. pstep_reverse. pclearbot. apply H.
- unpriv_ind. eapply H0; eauto.
- pclearbot. rewrite itree_eta'. pstep_reverse.
Qed.
(* reformat this lemma? useful but unclear *)
Lemma eses_aux1: ∀ (E : Type → Type) (R2 R1 : Type) (Label : Preorder)
(priv : ∀ A : Type, E A → L) (l : L) (RR : R1 → R2 → Prop)
(r : itree E R1 → itree E R2 → Prop) (m1 m2 : itree E R1),
m1 ≈ m2 →
(∀ (t1 t1' : itree E R1) (t2 : itree E R2),
t1 ≈ t1' → eqit_secure Label priv RR true true l t1 t2 → r t1' t2) →
∀ (X : Type) (e : E X) (k : X → itree E R2),
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) bot2) (observe m1)
(VisF e k) →
leq (priv X e) l →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) r) (observe m2)
(VisF e k).
Proof.
intros E R2 R1 Label priv l RR r m1 m2 REL CIH X e k Hsec SECCHECK.
remember (VisF e k) as x. punfold REL. red in REL. rewrite Heqx.
hinduction Hsec before r; intros; try inv Heqx; ddestruction; subst; try contradiction; auto.
- eapply IHHsec; eauto.
pstep_reverse. setoid_rewrite <- tau_eutt at 1. pfold. auto.
- pclearbot. remember (VisF e0 k1) as y.
hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
+ constructor; auto. right. eapply CIH; eauto; try apply H.
pclearbot. apply REL.
+ constructor; eauto.
- rewrite H2. remember (VisF e k1) as y.
hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
+ pclearbot. rewrite <- H2. unpriv_ind. rewrite H2. eapply H0; eauto.
Unshelve. all: auto. pstep_reverse.
+ constructor; auto. eapply IHREL; eauto.
Qed.
Lemma eses_aux2:
∀ (E : Type → Type) (R2 R1 : Type) (Label : Preorder)
(priv : ∀ A : Type, E A → L) (l : L) (RR : R1 → R2 → Prop)
(r : itree E R1 → itree E R2 → Prop) (m1 m2 : itree E R1) (r0 : R2),
m1 ≈ m2 →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) bot2) (observe m1)
(RetF r0) →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) r) (observe m2)
(RetF r0).
Proof.
intros E R2 R1 Label priv l RR r m1 m2 r0 Heutt Hsec.
punfold Heutt. red in Heutt. remember (RetF r0) as x.
rewrite Heqx. hinduction Hsec before r; intros; inv Heqx; auto with itree.
- remember (RetF r1) as y.
hinduction Heutt before r; intros; inv Heqy; auto with itree.
constructor; auto. eapply IHHeutt; eauto.
- eapply IHHsec; eauto. pstep_reverse. rewrite <- tau_eutt at 1. pfold. auto.
- remember (VisF e k1) as y.
hinduction Heutt before r; intros; inv Heqy; ddestruction; subst; auto.
+ unpriv_ind. rewrite H2. eapply H0; eauto.
pclearbot. pstep_reverse.
+ constructor; auto. eapply IHHeutt; eauto.
Qed.
Definition classic_empty := Secure.Labels.classic_empty.
(*tomorrow start on the transitivity proof *)
Lemma eutt_secure_eqit_secure : ∀ E Label priv l R1 R2 RR (t1 t1': itree E R1) (t2 : itree E R2),
t1 ≈ t1' → eqit_secure Label priv RR true true l t1 t2 →
eqit_secure Label priv RR true true l t1' t2.
Proof.
intros E Label priv l R1 R2 RR. pcofix CIH. intros t1 t1' t2 Heutt Hsec.
punfold Heutt. red in Heutt. punfold Hsec. red in Hsec.
pfold. red. hinduction Heutt before r; intros; subst; auto with itree.
- remember (RetF r2) as x. hinduction Hsec before r; intros; try inv Heqx; auto with itree.
+ constructor; auto. eapply IHHsec; eauto.
+ unpriv_ind. eapply H0; eauto.
- genobs_clear t2 ot2.
assert (Ht2 : (∃ m3, ot2 = TauF m3) ∨ (∀ m3, ot2 ≠ TauF m3) ).
{ destruct ot2; eauto; right; repeat intro; discriminate. }
(* because of the extra inductive cases this is not enough *)
destruct Ht2 as [ [m3 Hm3] | Ht2 ].
+ subst. pclearbot. constructor. right. eapply CIH; eauto.
apply tau_eqit_secure. apply eqit_secure_sym. apply tau_eqit_secure.
apply eqit_secure_sym. pfold. auto.
+ destruct ot2; try (exfalso; eapply Ht2; eauto; fail).
× pclearbot. rewrite itree_eta' at 1. eapply eses_aux2 with (m1 := Tau m1); eauto.
do 2 rewrite tau_eutt. auto.
× assert (leq (priv _ e) l ∨ ¬ leq (priv _ e) l).
{ apply classic. }
destruct H as [SECCHECK | SECCHECK]; destruct ( classic_empty X ).
++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with (m1 := Tau m1); auto.
do 2 rewrite tau_eutt. auto.
++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with (m1 := Tau m1); auto.
do 2 rewrite tau_eutt. auto.
++ unpriv_halt. pclearbot. right. eapply CIH; eauto.
apply tau_eqit_secure. pfold. auto.
++ pclearbot.
unpriv_co. pclearbot. right. eapply CIH. apply REL.
apply tau_eqit_secure.
apply eqit_secure_sym.
eapply unpriv_e_eqit_secure; eauto.
apply eqit_secure_sym. pfold. auto.
- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
assert (eqit_secure Label priv RR true true l (Vis e k1) t2 ).
{ pfold; auto. }
clear Hsec. rename H into Hsec.
destruct (classic (leq (priv _ e) l ) ).
+ pstep. red. punfold Hsec. red in Hsec.
cbn in ×. remember (VisF e k1) as x.
hinduction Hsec before r; intros; inv Heqx; ddestruction; subst; try contradiction; auto.
× constructor; auto. eapply IHHsec; eauto.
× constructor; auto; intros. right. eapply CIH; try apply REL. pclearbot. apply H.
× rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ destruct (classic_empty u).
× pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
destruct (observe t2).
-- inv Hsec; contra_size.
-- unpriv_halt. right. apply CIH with (t1 := Vis e k1).
++ pfold. constructor. left. auto.
++ inv Hsec; ddestruction; subst; try contradiction; try contra_size. pfold. auto.
pclearbot. auto.
-- inv Hsec; ddestruction; subst; try contradiction; try contra_size.
++ unpriv_halt. right. apply CIH with (t1 := Vis e k1).
{ pfold. constructor. red. auto. }
{ rewrite H1 in H3. pfold. apply H3. }
++ pclearbot. unpriv_halt. right. apply CIH with (t1 := Vis e k1).
{ pfold. constructor. red. auto. }
{ apply H2. }
++ pclearbot. unpriv_halt. contra_size.
× pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
destruct (observe t2).
++ rewrite itree_eta' at 1. rewrite itree_eta' in Hsec at 1.
eapply eses_aux2; eauto. pfold. constructor. red. auto.
++ unpriv_co. right. apply CIH with (t1 := k1 a); try apply REL.
eapply unpriv_e_eqit_secure; eauto. apply eqit_secure_sym.
apply tau_eqit_secure. apply eqit_secure_sym. pfold. auto.
++ destruct (classic (leq (priv _ e0) l )).
** rewrite itree_eta' at 1.
eapply eses_aux1 with (m1 := Vis e k1); eauto.
pfold. constructor. red. auto.
** destruct (classic_empty X).
--- unpriv_halt. right. eapply CIH; try apply REL.
eapply unpriv_e_eqit_secure; eauto. pfold. auto.
--- unpriv_co. right. eapply CIH; try apply REL.
(* eapply unpriv_e_eqit_secure; eauto. *)
do 2 (eapply unpriv_e_eqit_secure; eauto; apply eqit_secure_sym).
pfold. auto.
- eapply IHHeutt; eauto. pstep_reverse.
apply tau_eqit_secure. pfold. auto.
Qed.
Lemma eqit_secure_TauLR :
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (t0 : itree E R2)
(t4 : itree E R3),
eqit_secure Label priv RR2 b1 b2 l (Tau t0) (Tau t4) →
eqit_secure Label priv RR2 b1 b2 l t0 t4.
Proof.
intros E R3 Label priv l b1 b2 R2 RR2.
intros. punfold H. red in H. cbn in ×. pstep. red.
remember (TauF t0) as x. remember (TauF t4) as y.
hinduction H before b2; intros; try discriminate.
- inv Heqx; inv Heqy. pclearbot. pstep_reverse.
- inv Heqx. inv H; eauto with itree.
+ pclearbot. unpriv_ind. pstep_reverse.
+ unpriv_ind. rewrite H1 in H2.
specialize (H2 a). genobs (k1 a) ok1. clear Heqok1.
remember (TauF t4) as y.
hinduction H2 before b2; intros; inv Heqy; try inv CHECK; eauto with itree.
× pclearbot. constructor; auto; pstep_reverse.
× pclearbot. unpriv_ind. pstep_reverse.
× pclearbot. punfold H.
+ pclearbot. punfold H2.
- inv Heqy. inv H; eauto with itree.
+ pclearbot. unpriv_ind. pstep_reverse.
+ rewrite H0 in H2. unpriv_ind. specialize (H2 a).
genobs (k2 a) ok2. clear Heqok2.
remember (TauF t0) as y.
hinduction H2 before b2; intros; inv Heqy; try inv CHECK; eauto with itree.
× pclearbot. constructor; auto. pstep_reverse.
× unpriv_ind. pclearbot. pstep_reverse.
× pclearbot. punfold H.
+ pclearbot. punfold H2.
Qed.
Lemma eqit_secure_TauLVisR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop),
∀ (t3 : itree E R2) (X : Type) (e : E X) (k : X → itree E R3) (a : X),
(¬ leq (priv _ e) l) →
eqit_secure Label priv RR2 b1 b2 l (Tau t3) (Vis e k) →
eqit_secure Label priv RR2 b1 b2 l t3 (k a).
Proof.
intros E R3 Label priv l b1 b2 R2 RR t3 A e k a He Hsec.
punfold Hsec. red in Hsec. cbn in ×.
remember (TauF t3) as x. remember (VisF e k) as y.
hinduction Hsec before b2; intros; try discriminate.
- inv Heqx. inv CHECK.
remember (VisF e k) as y. pfold. red. clear IHHsec.
hinduction Hsec before b2; intros; inv Heqy; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ constructor; auto. pclearbot. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
- inv Heqx. inv Heqy. ddestruction; subst. rewrite H2 in H.
clear H0. clear H2 t1. remember (TauF t3) as x.
pfold. red. specialize (H a).
hinduction H before b2; intros; inv Heqx; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_TauRVisL:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) RR2,
∀ (t3 : itree E R2) (X : Type) (e : E X) (k : X → itree E R3) (a : X),
(¬ leq (priv _ e) l) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k) (Tau t3)→
eqit_secure Label priv RR2 b1 b2 l (k a) t3.
Proof.
intros E R3 Label priv l b1 b2 R2 RR t3 A e k a He Hsec.
punfold Hsec. red in Hsec. cbn in ×.
remember (TauF t3) as x. remember (VisF e k) as y.
hinduction Hsec before b2; intros; try discriminate.
- inv Heqx. inv CHECK. remember (VisF e k) as y. pfold. red. clear IHHsec.
hinduction Hsec before b1; intros; inv Heqy; ddestruction; subst;
try contradiction; eauto with itree.
+ constructor; auto with itree. pclearbot. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ contra_size.
+ contra_size.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. rewrite H2 in H. inv CHECK.
specialize (H a). pfold. red. remember (TauF t3) as y.
hinduction H before b2; intros; inv Heqy; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_VisLR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2),
¬ leq (priv A e) l →
∀ (X : Type) (e0 : E X) (k : X → itree E R3) (a : A),
¬ leq (priv X e0) l →
∀ a0 : X,
eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) →
eqit_secure Label priv RR2 b1 b2 l (k2 a) (k a0).
Proof.
intros E R3 Label priv l b1 b2 R2 RR2 A e k2 SECCHECK X e0 k a H0 a0 H1.
pfold. red.
punfold H1. red in H1. cbn in ×. remember (VisF e k2) as x.
remember (VisF e0 k) as y.
hinduction H1 before l; intros; try discriminate.
- inv Heqx. inv Heqy. ddestruction; subst. contradiction.
- pclearbot. inv Heqx. inv Heqy. ddestruction; subst. pstep_reverse.
- inv Heqx. ddestruction; subst. inv CHECK. clear H0.
specialize (H a).
rewrite Heqy in H. clear Heqy. remember (VisF e1 k) as y.
hinduction H before l; intros; inv Heqy; ddestruction; subst; try contradiction;
try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ pclearbot. specialize (H a0). punfold H.
- inv Heqy. ddestruction; subst. inv CHECK. clear H0.
rewrite Heqx in H. specialize (H a0).
remember (VisF e0 k0) as y.
hinduction H before b1; intros; inv Heqy; ddestruction; subst; try contradiction;
try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx; inv Heqy; ddestruction; subst. contra_size.
- inv Heqx; inv Heqy; ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_private_VisLR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2),
nonempty A →
¬ leq (priv A e) l →
∀ (X : Type) (e0 : E X) (k : X → itree E R3),
¬ leq (priv X e0) l →
nonempty X →
(∀ a a0,
eqit_secure Label priv RR2 b1 b2 l (k2 a) (k a0)) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) .
Proof.
intros. pfold. red. cbn. unpriv_co. left. apply H3.
Qed.
Lemma eqit_secure_private_VisL:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2) (t : itree E R3),
nonempty A →
¬ leq (priv A e) l →
(∀ a,
eqit_secure Label priv RR2 true b2 l (k2 a) t) →
eqit_secure Label priv RR2 true b2 l (Vis e k2) t .
Proof.
intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply H1.
Qed.
Lemma eqit_secure_private_VisR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R3) (t : itree E R2),
nonempty A →
¬ leq (priv A e) l →
(∀ a,
eqit_secure Label priv RR2 b1 true l t (k2 a)) →
eqit_secure Label priv RR2 b1 true l t (Vis e k2).
Proof.
intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply H1.
Qed.
Lemma eqit_secure_public_Vis : ∀ (E : Type → Type) (R1 R2 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (RR : R1 → R2 → Prop) (A : Type)
(e : E A) (k1: A → itree E R1) (k2 : A → itree E R2),
leq (priv A e) l →
(eqit_secure Label priv RR b1 b2 l (Vis e k1) (Vis e k2) ↔
∀ a, eqit_secure Label priv RR b1 b2 l (k1 a) (k2 a)).
Proof.
split; intros.
- pinversion H0; ddestruction; subst; try contradiction; apply H2.
- pfold. constructor; auto. left. apply H0.
Qed.
Lemma eqit_secure_trans_aux1:
∀ (E : Type → Type) (R3 R1 : Type) (Label : Preorder)
(priv : ∀ x : Type, E x → L) (l : L) (b2 : bool) (R2 : Type)
(RR1 : R1 → R2 → Prop) (RR2 : R2 → R3 → Prop) (r : itree E R1 → itree E R3 → Prop)
(r0 : R3) (t4 : itree E R2),
secure_eqitF Label priv RR2 true b2 l id
(upaco2 (secure_eqit_ Label priv RR2 true b2 l id) bot2) (observe t4)
(RetF r0) →
∀ t : itree E R1,
paco2 (secure_eqit_ Label priv RR1 true b2 l id) bot2 t t4 →
secure_eqitF Label priv (rcompose RR1 RR2) true b2 l id
(upaco2 (secure_eqit_ Label priv (rcompose RR1 RR2) true b2 l id) r)
(observe t) (RetF r0).
Proof.
intros E R3 R1 Label priv l b2 R2 RR1 RR2 r r0 t4 Ht23 t H.
punfold H. red in H.
remember (RetF r0) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; auto.
- remember (RetF r1) as y.
hinduction H0 before r; intros; inv Heqy; eauto with itree.
rewrite itree_eta'. unpriv_ind. cbn. eapply H0; eauto.
- eapply IHHt23; eauto.
remember (TauF t1) as y.
hinduction H before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- assert (Hne : nonempty A). { eauto. } (* add the condition that lets us assume this*)
inv Hne. eapply (H0 a); eauto.
remember (VisF e k1) as y.
hinduction H1 before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. rewrite itree_eta' at 1. pstep_reverse.
Qed.
Lemma eqit_secure_trans_aux2:
∀ (E : Type → Type) (R3 R1 : Type) (Label : Preorder)
(priv : ∀ x : Type, E x → L) (l : L) (b2 : bool) (R2 : Type)
(RR1 : R1 → R2 → Prop) (RR2 : R2 → R3 → Prop) (r : itree E R1 → itree E R3 → Prop)
(X : Type) (e0 : E X) (k : X → itree E R3) (t4 : itree E R2),
leq (priv X e0) l →
secure_eqitF Label priv RR2 true b2 l id
(upaco2 (secure_eqit_ Label priv RR2 true b2 l id) bot2) (observe t4)
(VisF e0 k) →
(∀ (t1 : itree E R1) (t2 : itree E R2) (t3 : itree E R3),
eqit_secure Label priv RR1 true b2 l t1 t2 →
eqit_secure Label priv RR2 true b2 l t2 t3 → r t1 t3) →
∀ t : itree E R1,
paco2 (secure_eqit_ Label priv RR1 true b2 l id) bot2 t t4 →
secure_eqitF Label priv (rcompose RR1 RR2) true b2 l id
(upaco2 (secure_eqit_ Label priv (rcompose RR1 RR2) true b2 l id) r)
(observe t) (VisF e0 k).
Proof.
intros E R3 R1 Label priv l b2 R2 RR1 RR2 r X e0 k t4 He0 Ht23 CIH0 t Ht.
punfold Ht. red in Ht. remember (VisF e0 k) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK;
ddestruction; subst; try contradiction; eauto.
- eapply IHHt23; eauto. clear IHHt23. remember (TauF t1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. remember (VisF e0 k1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; eauto with itree.
+ pclearbot. constructor; auto. right. eapply CIH0. apply H.
apply H0.
+ rewrite itree_eta'. unpriv_ind. eapply H0; eauto.
- assert (nonempty A); eauto. inv H1. eapply H0; eauto.
Unshelve. all : auto. clear H0. rewrite H2 in H.
remember (VisF e k1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. rewrite itree_eta' at 1. pstep_reverse.
Qed.
Lemma secret_halt_trans_1 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) t1 (e : E A) k t3,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l t1 (Vis e k) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k) t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 A RR1 RR2 t1 e k t3 He HA.
generalize dependent t3. generalize dependent t1.
pcofix CIH. intros t1 t3 Ht1 Ht3.
pfold. red. punfold Ht1. red in Ht1. punfold Ht3. red in Ht3.
cbn in ×.
remember (VisF e k) as x.
hinduction Ht1 before r; intros; inv Heqx; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size.
+ constructor. right. apply CIH; auto. pfold. auto.
+ unpriv_co; auto. right. apply CIH; auto. pfold. rewrite H0 in H2. apply H2.
+ pclearbot. constructor. right. apply CIH; auto.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. apply CIH; auto with itree. pfold.
red. cbn. unpriv_halt.
× unpriv_co. right. apply CIH; auto. apply H1.
+ pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
red. cbn. unpriv_halt. contra_size.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt.
× pfold. auto.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt.
× pfold. auto. rewrite H0 in H2. apply H2.
+ pclearbot. unpriv_halt. right. apply CIH; auto.
pfold. red. cbn. unpriv_halt.
+ pclearbot. unpriv_halt. right. apply CIH.
× pfold. red. cbn. unpriv_halt.
× apply H1.
+ unpriv_halt. contra_size.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size;
destruct (classic_empty A0).
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt. contra_size.
× pfold. auto.
+ unpriv_co. right. apply CIH; auto; try apply H.
pfold. auto.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt. contra_size.
× pfold. rewrite H0 in H2. apply H2.
+ unpriv_co. right. apply CIH. apply H. rewrite H0 in H2.
pfold. apply H2.
+ pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
red. cbn. unpriv_halt. contra_size.
+ pclearbot. unpriv_co. right. apply CIH; auto. apply H.
+ unpriv_halt. pclearbot. right. apply CIH; try apply H1.
pfold. red. cbn. unpriv_halt. contra_size.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. apply CIH; auto. apply H.
pfold. red. cbn. unpriv_halt.
× unpriv_co. right. apply CIH; eauto. apply H. apply H1.
+ pclearbot. unpriv_halt. contra_size.
+ pclearbot. unpriv_halt. right. apply CIH; auto. apply H.
pfold. red. cbn. unpriv_halt. contra_size.
Qed.
Lemma secret_halt_trans_2 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) (e : E A) k t2 t3,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l (Vis e k) t2 →
eqit_secure Label priv RR2 b1 b2 l t2 t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l (Vis e k) t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 A RR1 RR2 e k t2 t3 He HA.
generalize dependent t3. generalize dependent t2.
pcofix CIH. intros t2 t3 Ht2 Ht23. pfold.
red. cbn. punfold Ht2. punfold Ht23. red in Ht2. red in Ht23.
cbn in ×.
hinduction Ht23 before r; intros; eauto with itree.
- inv Ht2. ddestruction; subst. contra_size.
- unpriv_halt. right. pclearbot. eapply CIH; eauto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
pfold. auto.
- eapply IHHt23; eauto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
punfold H0.
- pclearbot.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
- unpriv_halt. pclearbot. inv SIZECHECK. right. eapply CIH; try apply H.
Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
+ pfold. apply H2.
+ apply H1.
- pclearbot. unpriv_halt. right. eapply CIH; try apply H.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
pfold. auto.
- pclearbot. unpriv_halt. inv SIZECHECK1. inv SIZECHECK2. right. eapply CIH; try apply H.
Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
+ pfold. apply H2.
+ apply H1.
- inv SIZECHECK. eapply H0; eauto. Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
rewrite itree_eta' at 1. pstep_reverse.
- unpriv_halt. right. eapply CIH; eauto. pfold. apply Ht2.
pfold. apply H.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. auto.
- unpriv_halt. contra_size.
- unpriv_halt. right. pclearbot. eapply CIH with (t2 := Vis e1 k1); eauto.
+ pfold. auto.
+ apply H.
- unpriv_halt. contra_size.
Qed.
Lemma eqit_secure_RR_imp : ∀ E b1 b2 R1 R2 (RR1 RR2 : R1 → R2 → Prop) Label priv l
(t1 : itree E R1) (t2 : itree E R2),
RR1 <2= RR2 →
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t1 t2.
Proof.
intros. generalize dependent t2. revert t1.
pcofix CIH. intros t1 t2 Ht12. pfold. red.
punfold Ht12. red in Ht12.
hinduction Ht12 before r; intros; eauto;
try (pclearbot; constructor; auto; right; eapply CIH; eauto; fail);
try (pclearbot; unpriv_co; right; eapply CIH; eauto; apply H0; fail).
pclearbot. constructor; auto. right. eapply CIH; eauto. apply H0.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. apply H0.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. apply H0.
Qed.
Lemma secret_halt_trans_3 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) t1 t2 (e : E A) k,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t2 (Vis e k) →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 (Vis e k).
Proof.
intros. apply eqit_secure_sym in H1. apply eqit_secure_sym in H2.
apply eqit_secure_sym. eapply secret_halt_trans_2 in H1; eauto.
eapply eqit_secure_RR_imp; eauto.
intros. inv PR. econstructor; eauto.
Qed.
Lemma eqit_secure_trans : ∀ E Label priv l b1 b2 (R1 R2 R3 : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) (t1 : itree E R1) (t2 : itree E R2) (t3 : itree E R3),
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t2 t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 RR1 RR2.
pcofix CIH0. intros t1 t2 t3 Ht12 Ht23.
punfold Ht12. red in Ht12. punfold Ht23. red in Ht23. pfold. red.
hinduction Ht12 before r; intros; try inv CHECK; auto with itree.
- remember (RetF r2) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; eauto with itree.
rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
- pclearbot. genobs t4 ot4.
assert ( (∃ t5, ot4 = TauF t5) ∨ (∀ t5, ot4 ≠ TauF t5) ).
{ destruct ot4; eauto; right; intros; discriminate. }
destruct H0 as [ [t5 Ht4] | Ht4].
+ subst. rewrite Ht4. rewrite Ht4 in Ht23. constructor.
right. eapply CIH0; eauto. eapply eqit_secure_TauLR. pfold.
auto.
+ destruct ot4; try (exfalso; eapply Ht4; eauto; fail ).
× inv Ht23. inv CHECK. rewrite itree_eta' at 1.
assert (eqit_secure Label priv (rcompose RR1 RR2) true b2 l (Tau t0) (Ret r0) ).
{ pfold. red. cbn. rewrite itree_eta' at 1. eapply eqit_secure_trans_aux1; eauto.
pfold. red. constructor; auto. pstep_reverse. }
rewrite itree_eta'. pstep_reverse. eapply paco2_mon; eauto.
intros; contradiction.
× destruct (classic (leq (priv _ e) l ) ).
-- inv Ht23; ddestruction; subst; try contradiction; try inv CHECK.
constructor; auto. eapply eqit_secure_trans_aux2; eauto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. rewrite itree_eta' at 1.
pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3 with (t2 := Tau t3); eauto.
** pfold. constructor. left. auto.
** pfold. auto.
++ unpriv_co. right. eapply CIH0; eauto.
assert (eqit_secure Label priv RR2 b1 b2 l (Tau t3) (Vis e k)).
pfold. auto. eapply eqit_secure_TauLVisR; eauto.
- apply IHHt12; auto.
remember (TauF t0) as y.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. remember (VisF e k2) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; ddestruction; subst;
try contradiction; eauto with itree.
+ pclearbot. constructor; auto. intros. right. eapply CIH0; eauto; try apply H0.
apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
- pclearbot. remember (TauF t0) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; auto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0.
auto.
+ destruct ot2.
× clear IHHt23. rewrite itree_eta'. unpriv_ind.
remember (k1 a) as t. specialize (H a). setoid_rewrite <- Heqt in H.
clear Heqt a k1. cbn. eapply eqit_secure_trans_aux1; eauto.
× unpriv_co. right. eapply CIH0; try apply H.
clear IHHt23. remember (TauF t) as y.
pfold. red.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK; eauto with itree.
-- pclearbot. constructor; auto. pstep_reverse.
-- pclearbot. unpriv_ind. pstep_reverse.
-- pclearbot. punfold H.
× destruct (classic (leq (priv _ e0) l ) ).
-- rewrite itree_eta'. unpriv_ind. cbn.
clear IHHt23. remember (k1 a) as t. specialize (H a). setoid_rewrite <- Heqt in H.
clear Heqt a k1. eapply eqit_secure_trans_aux2; eauto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. unpriv_ind.
pstep_reverse. apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3; eauto. apply H.
pfold. auto.
++ unpriv_co. right. eapply CIH0. apply H.
clear IHHt23. pstep. red. remember (VisF e0 k) as y.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; eauto with itree.
** pclearbot. constructor; auto. pstep_reverse.
** unpriv_ind. pclearbot. pstep_reverse.
** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
+ constructor; auto. eapply IHHt23; eauto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0. apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ unpriv_halt. right. pclearbot. eapply CIH0; eauto. apply H0.
- pclearbot.
genobs_clear t3 ot3.
assert (Hne : nonempty A); eauto. inv Hne.
assert ( (∃ t4, ot3 = TauF t4) ∨ (∀ t4, ot3 ≠ TauF t4) ).
{ destruct ot3; eauto; right; intros; discriminate. }
destruct H0 as [ [t4 Ht3] | Ht3].
+ subst. constructor. right. eapply CIH0; try apply H.
Unshelve. all: auto.
eapply eqit_secure_TauRVisL; eauto. pfold. auto.
(* should be fine but new lemma, also shelved goal *)
+
destruct ot3; try (exfalso; eapply Ht4; eauto; fail ).
× inv Ht23; inv CHECK. ddestruction. subst. clear CIH0.
constructor; auto. rewrite H4. eapply eqit_secure_trans_aux1; eauto.
rewrite <- H4. apply H1. Unshelve. auto. (* shelved goal*)
× constructor. right. eapply CIH0; try apply H.
eapply eqit_secure_TauRVisL; eauto. pfold. auto.
(* same goal as last admit *)
× destruct (classic (leq (priv _ e0) l ) ).
-- inv Ht23; try inv CHECK; ddestruction; subst; try contradiction.
constructor; auto. rewrite H5. eapply eqit_secure_trans_aux2; eauto.
rewrite <- H5. apply H2. Unshelve. all : auto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. rewrite itree_eta' at 1. pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3 with (t2 := Vis e k2); eauto.
** pfold. red. cbn. unpriv_co.
** pfold. auto.
++ unpriv_co. right. eapply CIH0; try apply H.
Unshelve. all : auto.
assert (eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) ).
pfold. auto. eapply eqit_secure_VisLR; eauto.
- pclearbot. remember (VisF e2 k2) as x.
(* maybe need to separate the inductive and coinductive progress cases? *)
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; try contradiction;
try contra_size;
ddestruction; subst; auto.
+ constructor; auto. eapply IHHt23; eauto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0. apply H.
+ pclearbot. assert (Hne : nonempty B); eauto. inv Hne.
unpriv_co. right. eapply CIH0; eauto; try eapply H0. apply H.
Unshelve. auto.
+ pclearbot. assert (Hne : nonempty B0); eauto. inv Hne.
unpriv_co. right. eapply CIH0; try apply H0. apply H.
Unshelve. auto.
+ genobs t2 ot2. destruct ot2.
× assert (Hne : nonempty B); eauto. inv Hne.
rewrite itree_eta'. unpriv_ind. eapply eqit_secure_trans_aux1; eauto.
Unshelve. auto.
× assert (Hne : nonempty B); eauto. inv Hne.
unpriv_co. right. eapply CIH0; try apply H1. Unshelve. all : auto.
clear H0. specialize (H a). pfold. red. genobs (k2 a) ok2.
clear Heqok2 H1 k2.
remember (TauF t) as y.
hinduction H before r; intros; inv Heqy; try inv CHECK; auto.
-- constructor; auto. pclearbot. pstep_reverse.
-- constructor; eauto.
-- pclearbot. unpriv_ind. pstep_reverse.
-- unpriv_ind. eapply H0; eauto.
-- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
× inv SIZECHECK2.
destruct (classic (leq (priv _ e) l ) ).
-- rewrite itree_eta'. unpriv_ind.
eapply eqit_secure_trans_aux2; eauto. Unshelve. all : auto.
-- destruct (classic_empty X).
++ unpriv_halt. right. eapply CIH0; eauto. apply H1.
pfold. apply H. Unshelve. auto.
++ unpriv_co. right. eapply CIH0; try apply H1.
Unshelve. all : auto.
clear H0. pstep. red. remember (VisF e k) as y.
specialize (H a). clear Heqot2. genobs (k2 a) ok2.
clear Heqok2.
hinduction H before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; eauto with itree.
** pclearbot. constructor; auto. pstep_reverse.
** unpriv_ind. pclearbot. pstep_reverse.
** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ pclearbot. inv SIZECHECK2. unpriv_halt. right. eapply CIH0; eauto. apply H0.
apply H. Unshelve. auto.
- remember (VisF e k2) as x. hinduction Ht23 before r; intros; inv Heqx; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; auto.
+ constructor; auto. eapply IHHt23; eauto.
+ constructor; auto. pclearbot. assert (Hne : nonempty A0); eauto. inv Hne. eapply H0; eauto.
pstep_reverse. Unshelve. auto.
+ unpriv_ind. assert (Hne : nonempty A0); eauto. inv Hne. eapply H0; eauto.
pclearbot. pstep_reverse. Unshelve. auto.
+ assert (Hne : nonempty A0). { eauto. } inv Hne. eauto. Unshelve. auto.
+ unpriv_ind. eauto.
+ pclearbot. rewrite itree_eta'. pstep_reverse.
apply paco2_mon with (r := bot2); intros; try contradiction.
inv SIZECHECK0.
eapply secret_halt_trans_3 with (t2 := k0 a); eauto.
× pfold. apply H1.
× apply H.
- pclearbot.
remember (TauF t0) as y.
hinduction Ht23 before r; intros; inv Heqy; subst; eauto with itree; pclearbot.
+ unpriv_halt. right. eapply CIH0; eauto.
+ clear IHHt23. rewrite itree_eta'. rewrite itree_eta' at 1.
pstep_reverse. apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_2; eauto. pfold. auto.
+ unpriv_halt. right. eapply CIH0; eauto. apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ unpriv_halt. contra_size.
- pclearbot.
inv Ht23; ddestruction; subst; try contra_size; try contradiction;
try inv CHECK.
+ constructor. right. eapply CIH0; eauto. pfold. auto.
+ unpriv_co. right. eapply CIH0; eauto. rewrite H0 in H2.
pfold. apply H2.
+ pclearbot. constructor. right. eapply CIH0; eauto.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. eapply CIH0; eauto. pfold. red. cbn. unpriv_halt.
× unpriv_co. right. eapply CIH0; eauto. apply H1.
+ pclearbot. unpriv_halt. right. eapply CIH0; eauto.
pfold. red. cbn. unpriv_halt. contra_size.
- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_2 with (t2 := Vis e2 k2); eauto.
+ pfold. red. cbn. unpriv_halt.
+ pfold. auto.
- pclearbot. destruct (classic_empty A).
+ inv Ht23; ddestruction; subst; try contradiction; try contra_size; try inv CHECK.
× unpriv_halt. right. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- pfold. auto.
× unpriv_halt. right. rewrite H1 in H3. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- pfold. apply H3.
× unpriv_halt. pclearbot. right. eapply CIH0; eauto.
pfold. red. cbn. unpriv_halt. contra_size.
× unpriv_halt. pclearbot. right. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- apply H2.
× unpriv_halt. contra_size.
+ destruct (observe t3).
× inv Ht23; ddestruction; subst; try contra_size; try contradiction.
× unpriv_co. right. eapply CIH0; eauto. apply H.
inv Ht23; ddestruction; subst; try contra_size; try contradiction.
pfold. auto. pclearbot. auto.
× destruct (classic (leq (priv _ e) l ) ).
{ inv Ht23; ddestruction; subst; try contra_size; try contradiction. }
destruct (classic_empty X).
-- unpriv_halt. right. eapply CIH0; eauto. apply H. pfold. auto.
-- unpriv_co. right. eapply CIH0; eauto. apply H.
inv Ht23; ddestruction; subst; try contra_size; try contradiction.
++ pfold. apply H5.
++ pclearbot. apply H4.
Qed.
Lemma eqit_itree_eqit_secure : ∀ E Label priv l R1 R2 RR (t1 t1': itree E R1) (t2 : itree E R2),
t1 ≅ t1' → eqit_secure Label priv RR false false l t1 t2 →
eqit_secure Label priv RR false false l t1' t2.
Proof.
intros E Label priv l R1 R2 RR. pcofix CIH.
intros t1 t1' t2 Heq Hsec. pstep. red.
punfold Heq. red in Heq. punfold Hsec. red in Hsec.
inv Heq; try inv CHECK.
- rewrite <- H0 in Hsec. rewrite itree_eta' at 1. pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction. pfold.
red. cbn. remember (RetF r2) as x. clear H H0.
hinduction Hsec before r; intros; inv Heqx; eauto with itree.
- pclearbot. genobs t2 ot2.
assert ( (∃ t3, ot2 = TauF t3) ∨ (∀ t3, ot2 ≠ TauF t3) ).
{ destruct ot2; eauto; right; intros; discriminate. }
destruct H1 as [ [t3 Ht2] | Ht2].
+ subst. rewrite Ht2. rewrite Ht2 in Hsec. constructor.
right. eapply CIH; eauto. rewrite <- H0 in Hsec. inv Hsec; try inv CHECK. pclearbot. auto.
+ destruct ot2; try (exfalso; eapply Ht2; eauto; fail ).
× rewrite <- H0 in Hsec. inv Hsec; try inv CHECK.
× rewrite <- H0 in Hsec. inv Hsec; ddestruction; subst; try inv CHECK.
-- pclearbot. unpriv_co. right. eapply CIH; eauto. apply H3.
-- pclearbot. unpriv_halt. right. eapply CIH; eauto.
- rewrite <- H0 in Hsec. inv Hsec; ddestruction; subst; try inv CHECK; try contradiction; try contra_size.
+ pclearbot. constructor; auto. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. constructor. left. auto.
+ pclearbot. unpriv_halt. right. eapply CIH with (t1 := Vis e k1); try apply H2.
pfold. constructor. left. auto.
+ pclearbot. unpriv_halt. right. eapply CIH; eauto with itree. apply H2.
Qed.
Lemma eqit_secure_eq_trans : ∀ E R b1 b2 Label priv l (t1 t2 t3 : itree E R),
eqit_secure Label priv eq b1 b2 l t1 t2 →
eqit_secure Label priv eq b1 b2 l t2 t3 →
eqit_secure Label priv eq b1 b2 l t1 t3.
Proof.
intros. apply eqit_secure_RR_imp with (RR1 := rcompose eq eq).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
Qed.
Lemma eqit_secure_anything : ∀ E R1 b Label priv l
(t1 : itree E R1) t2,
eqit_secure Label priv eq b b l t1 t2 →
eqit_secure Label priv eq b b l t1 t1.
Proof.
intros.
eapply eqit_secure_eq_trans; eauto.
apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto.
Qed.
Global Instance proper_eqit_secure_eqit {E} {R1 R2 : Type} {b} {RR : R1 → R2 → Prop} {Label priv l} :
Proper (eqit eq b b ==> eqit eq b b ==> iff) (@eqit_secure E R1 R2 Label priv RR b b l).
Proof.
repeat intro. destruct b; split; intros.
- eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- assert (x ≈ y); auto. assert (x0 ≈ y0); auto.
symmetry in H2.
eapply eutt_secure_eqit_secure; eauto.
symmetry in H3. apply eqit_secure_sym.
eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- assert (x ≅ y); auto. assert (x0 ≅ y0); auto.
symmetry in H2. symmetry in H3.
eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. auto.
Qed.
Global Instance proper_eqit_secure_eqit_secure
{E} {b} {R1 R2 : Type} {RR : R1 → R2 → Prop} {Label priv l} :
Proper (eqit_secure Label priv eq b b l ==> eqit_secure Label priv eq b b l ==> iff)
(@eqit_secure E R1 R2 Label priv RR b b l).
Proof.
repeat intro; split; intros.
- eapply eqit_secure_RR_imp with (RR1 := rcompose RR eq); eauto.
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
apply eqit_secure_sym.
eapply eqit_secure_RR_imp with (RR1 := rcompose (flip RR) eq); eauto.
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto. apply eqit_secure_sym. auto.
- assert (eqit_secure Label priv eq b b l y0 x0).
{ apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
eapply eqit_secure_RR_imp with (RR1 := rcompose RR eq).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
assert (eqit_secure Label priv eq b b l y x).
{ apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
eapply eqit_secure_RR_imp with (RR1 := rcompose eq RR).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
Qed.
From ITree Require Import
Axioms
ITree
ITreeFacts.
From ITree.Extra Require Import
Secure.Labels
Secure.SecureEqHalt
.
From Paco Require Import paco.
Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.
Lemma tau_eqit_secure : ∀ E R1 R2 Label priv l RR (t1 : itree E R1) (t2 : itree E R2),
eqit_secure Label priv RR true true l (Tau t1) t2 → eqit_secure Label priv RR true true l t1 t2.
Proof.
intros E R1 R2 Label priv l RR. intros t1 t2 Hsec. pstep. red.
punfold Hsec. red in Hsec. cbn in ×. remember (TauF t1) as x.
hinduction Hsec before priv; intros; inv Heqx; pclearbot; try inv CHECK; auto with itree.
- constructor; auto. pstep_reverse.
- unpriv_ind. pstep_reverse.
- punfold H.
Qed.
Lemma unpriv_e_eqit_secure : ∀ E A R1 R2 Label priv l RR (e : E A) (k : A → itree E R1)
(t : itree E R2),
(¬leq (priv A e) l ) →
eqit_secure Label priv RR true true l (Vis e k) t →
∀ a, eqit_secure Label priv RR true true l (k a) t.
Proof.
intros. generalize dependent t. rename H into Hunpriv. generalize dependent a.
intros. punfold H0. red in H0. cbn in ×. pfold. red.
remember (VisF e k) as x. genobs_clear t ot.
hinduction H0 before l; intros; try inv Heqx;
ddestruction; subst; try contradiction; try contra_size; auto.
- constructor; auto. eapply IHsecure_eqitF; eauto.
- pclearbot. constructor; auto. pstep_reverse.
- unpriv_ind. pstep_reverse. pclearbot. apply H.
- unpriv_ind. eapply H0; eauto.
- pclearbot. rewrite itree_eta'. pstep_reverse.
Qed.
(* reformat this lemma? useful but unclear *)
Lemma eses_aux1: ∀ (E : Type → Type) (R2 R1 : Type) (Label : Preorder)
(priv : ∀ A : Type, E A → L) (l : L) (RR : R1 → R2 → Prop)
(r : itree E R1 → itree E R2 → Prop) (m1 m2 : itree E R1),
m1 ≈ m2 →
(∀ (t1 t1' : itree E R1) (t2 : itree E R2),
t1 ≈ t1' → eqit_secure Label priv RR true true l t1 t2 → r t1' t2) →
∀ (X : Type) (e : E X) (k : X → itree E R2),
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) bot2) (observe m1)
(VisF e k) →
leq (priv X e) l →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) r) (observe m2)
(VisF e k).
Proof.
intros E R2 R1 Label priv l RR r m1 m2 REL CIH X e k Hsec SECCHECK.
remember (VisF e k) as x. punfold REL. red in REL. rewrite Heqx.
hinduction Hsec before r; intros; try inv Heqx; ddestruction; subst; try contradiction; auto.
- eapply IHHsec; eauto.
pstep_reverse. setoid_rewrite <- tau_eutt at 1. pfold. auto.
- pclearbot. remember (VisF e0 k1) as y.
hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
+ constructor; auto. right. eapply CIH; eauto; try apply H.
pclearbot. apply REL.
+ constructor; eauto.
- rewrite H2. remember (VisF e k1) as y.
hinduction REL before r; intros; try inv Heqy; ddestruction; subst; auto.
+ pclearbot. rewrite <- H2. unpriv_ind. rewrite H2. eapply H0; eauto.
Unshelve. all: auto. pstep_reverse.
+ constructor; auto. eapply IHREL; eauto.
Qed.
Lemma eses_aux2:
∀ (E : Type → Type) (R2 R1 : Type) (Label : Preorder)
(priv : ∀ A : Type, E A → L) (l : L) (RR : R1 → R2 → Prop)
(r : itree E R1 → itree E R2 → Prop) (m1 m2 : itree E R1) (r0 : R2),
m1 ≈ m2 →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) bot2) (observe m1)
(RetF r0) →
secure_eqitF Label priv RR true true l id
(upaco2 (secure_eqit_ Label priv RR true true l id) r) (observe m2)
(RetF r0).
Proof.
intros E R2 R1 Label priv l RR r m1 m2 r0 Heutt Hsec.
punfold Heutt. red in Heutt. remember (RetF r0) as x.
rewrite Heqx. hinduction Hsec before r; intros; inv Heqx; auto with itree.
- remember (RetF r1) as y.
hinduction Heutt before r; intros; inv Heqy; auto with itree.
constructor; auto. eapply IHHeutt; eauto.
- eapply IHHsec; eauto. pstep_reverse. rewrite <- tau_eutt at 1. pfold. auto.
- remember (VisF e k1) as y.
hinduction Heutt before r; intros; inv Heqy; ddestruction; subst; auto.
+ unpriv_ind. rewrite H2. eapply H0; eauto.
pclearbot. pstep_reverse.
+ constructor; auto. eapply IHHeutt; eauto.
Qed.
Definition classic_empty := Secure.Labels.classic_empty.
(*tomorrow start on the transitivity proof *)
Lemma eutt_secure_eqit_secure : ∀ E Label priv l R1 R2 RR (t1 t1': itree E R1) (t2 : itree E R2),
t1 ≈ t1' → eqit_secure Label priv RR true true l t1 t2 →
eqit_secure Label priv RR true true l t1' t2.
Proof.
intros E Label priv l R1 R2 RR. pcofix CIH. intros t1 t1' t2 Heutt Hsec.
punfold Heutt. red in Heutt. punfold Hsec. red in Hsec.
pfold. red. hinduction Heutt before r; intros; subst; auto with itree.
- remember (RetF r2) as x. hinduction Hsec before r; intros; try inv Heqx; auto with itree.
+ constructor; auto. eapply IHHsec; eauto.
+ unpriv_ind. eapply H0; eauto.
- genobs_clear t2 ot2.
assert (Ht2 : (∃ m3, ot2 = TauF m3) ∨ (∀ m3, ot2 ≠ TauF m3) ).
{ destruct ot2; eauto; right; repeat intro; discriminate. }
(* because of the extra inductive cases this is not enough *)
destruct Ht2 as [ [m3 Hm3] | Ht2 ].
+ subst. pclearbot. constructor. right. eapply CIH; eauto.
apply tau_eqit_secure. apply eqit_secure_sym. apply tau_eqit_secure.
apply eqit_secure_sym. pfold. auto.
+ destruct ot2; try (exfalso; eapply Ht2; eauto; fail).
× pclearbot. rewrite itree_eta' at 1. eapply eses_aux2 with (m1 := Tau m1); eauto.
do 2 rewrite tau_eutt. auto.
× assert (leq (priv _ e) l ∨ ¬ leq (priv _ e) l).
{ apply classic. }
destruct H as [SECCHECK | SECCHECK]; destruct ( classic_empty X ).
++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with (m1 := Tau m1); auto.
do 2 rewrite tau_eutt. auto.
++ pclearbot. rewrite itree_eta' at 1. apply eses_aux1 with (m1 := Tau m1); auto.
do 2 rewrite tau_eutt. auto.
++ unpriv_halt. pclearbot. right. eapply CIH; eauto.
apply tau_eqit_secure. pfold. auto.
++ pclearbot.
unpriv_co. pclearbot. right. eapply CIH. apply REL.
apply tau_eqit_secure.
apply eqit_secure_sym.
eapply unpriv_e_eqit_secure; eauto.
apply eqit_secure_sym. pfold. auto.
- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
assert (eqit_secure Label priv RR true true l (Vis e k1) t2 ).
{ pfold; auto. }
clear Hsec. rename H into Hsec.
destruct (classic (leq (priv _ e) l ) ).
+ pstep. red. punfold Hsec. red in Hsec.
cbn in ×. remember (VisF e k1) as x.
hinduction Hsec before r; intros; inv Heqx; ddestruction; subst; try contradiction; auto.
× constructor; auto. eapply IHHsec; eauto.
× constructor; auto; intros. right. eapply CIH; try apply REL. pclearbot. apply H.
× rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ destruct (classic_empty u).
× pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
destruct (observe t2).
-- inv Hsec; contra_size.
-- unpriv_halt. right. apply CIH with (t1 := Vis e k1).
++ pfold. constructor. left. auto.
++ inv Hsec; ddestruction; subst; try contradiction; try contra_size. pfold. auto.
pclearbot. auto.
-- inv Hsec; ddestruction; subst; try contradiction; try contra_size.
++ unpriv_halt. right. apply CIH with (t1 := Vis e k1).
{ pfold. constructor. red. auto. }
{ rewrite H1 in H3. pfold. apply H3. }
++ pclearbot. unpriv_halt. right. apply CIH with (t1 := Vis e k1).
{ pfold. constructor. red. auto. }
{ apply H2. }
++ pclearbot. unpriv_halt. contra_size.
× pfold. red. cbn. punfold Hsec. red in Hsec. cbn in ×.
destruct (observe t2).
++ rewrite itree_eta' at 1. rewrite itree_eta' in Hsec at 1.
eapply eses_aux2; eauto. pfold. constructor. red. auto.
++ unpriv_co. right. apply CIH with (t1 := k1 a); try apply REL.
eapply unpriv_e_eqit_secure; eauto. apply eqit_secure_sym.
apply tau_eqit_secure. apply eqit_secure_sym. pfold. auto.
++ destruct (classic (leq (priv _ e0) l )).
** rewrite itree_eta' at 1.
eapply eses_aux1 with (m1 := Vis e k1); eauto.
pfold. constructor. red. auto.
** destruct (classic_empty X).
--- unpriv_halt. right. eapply CIH; try apply REL.
eapply unpriv_e_eqit_secure; eauto. pfold. auto.
--- unpriv_co. right. eapply CIH; try apply REL.
(* eapply unpriv_e_eqit_secure; eauto. *)
do 2 (eapply unpriv_e_eqit_secure; eauto; apply eqit_secure_sym).
pfold. auto.
- eapply IHHeutt; eauto. pstep_reverse.
apply tau_eqit_secure. pfold. auto.
Qed.
Lemma eqit_secure_TauLR :
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (t0 : itree E R2)
(t4 : itree E R3),
eqit_secure Label priv RR2 b1 b2 l (Tau t0) (Tau t4) →
eqit_secure Label priv RR2 b1 b2 l t0 t4.
Proof.
intros E R3 Label priv l b1 b2 R2 RR2.
intros. punfold H. red in H. cbn in ×. pstep. red.
remember (TauF t0) as x. remember (TauF t4) as y.
hinduction H before b2; intros; try discriminate.
- inv Heqx; inv Heqy. pclearbot. pstep_reverse.
- inv Heqx. inv H; eauto with itree.
+ pclearbot. unpriv_ind. pstep_reverse.
+ unpriv_ind. rewrite H1 in H2.
specialize (H2 a). genobs (k1 a) ok1. clear Heqok1.
remember (TauF t4) as y.
hinduction H2 before b2; intros; inv Heqy; try inv CHECK; eauto with itree.
× pclearbot. constructor; auto; pstep_reverse.
× pclearbot. unpriv_ind. pstep_reverse.
× pclearbot. punfold H.
+ pclearbot. punfold H2.
- inv Heqy. inv H; eauto with itree.
+ pclearbot. unpriv_ind. pstep_reverse.
+ rewrite H0 in H2. unpriv_ind. specialize (H2 a).
genobs (k2 a) ok2. clear Heqok2.
remember (TauF t0) as y.
hinduction H2 before b2; intros; inv Heqy; try inv CHECK; eauto with itree.
× pclearbot. constructor; auto. pstep_reverse.
× unpriv_ind. pclearbot. pstep_reverse.
× pclearbot. punfold H.
+ pclearbot. punfold H2.
Qed.
Lemma eqit_secure_TauLVisR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop),
∀ (t3 : itree E R2) (X : Type) (e : E X) (k : X → itree E R3) (a : X),
(¬ leq (priv _ e) l) →
eqit_secure Label priv RR2 b1 b2 l (Tau t3) (Vis e k) →
eqit_secure Label priv RR2 b1 b2 l t3 (k a).
Proof.
intros E R3 Label priv l b1 b2 R2 RR t3 A e k a He Hsec.
punfold Hsec. red in Hsec. cbn in ×.
remember (TauF t3) as x. remember (VisF e k) as y.
hinduction Hsec before b2; intros; try discriminate.
- inv Heqx. inv CHECK.
remember (VisF e k) as y. pfold. red. clear IHHsec.
hinduction Hsec before b2; intros; inv Heqy; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ constructor; auto. pclearbot. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
- inv Heqx. inv Heqy. ddestruction; subst. rewrite H2 in H.
clear H0. clear H2 t1. remember (TauF t3) as x.
pfold. red. specialize (H a).
hinduction H before b2; intros; inv Heqx; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_TauRVisL:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) RR2,
∀ (t3 : itree E R2) (X : Type) (e : E X) (k : X → itree E R3) (a : X),
(¬ leq (priv _ e) l) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k) (Tau t3)→
eqit_secure Label priv RR2 b1 b2 l (k a) t3.
Proof.
intros E R3 Label priv l b1 b2 R2 RR t3 A e k a He Hsec.
punfold Hsec. red in Hsec. cbn in ×.
remember (TauF t3) as x. remember (VisF e k) as y.
hinduction Hsec before b2; intros; try discriminate.
- inv Heqx. inv CHECK. remember (VisF e k) as y. pfold. red. clear IHHsec.
hinduction Hsec before b1; intros; inv Heqy; ddestruction; subst;
try contradiction; eauto with itree.
+ constructor; auto with itree. pclearbot. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ contra_size.
+ contra_size.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. apply H.
- inv Heqx. inv Heqy. ddestruction; subst. pclearbot. rewrite H2 in H. inv CHECK.
specialize (H a). pfold. red. remember (TauF t3) as y.
hinduction H before b2; intros; inv Heqy; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- inv Heqx. inv Heqy. ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_VisLR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2),
¬ leq (priv A e) l →
∀ (X : Type) (e0 : E X) (k : X → itree E R3) (a : A),
¬ leq (priv X e0) l →
∀ a0 : X,
eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) →
eqit_secure Label priv RR2 b1 b2 l (k2 a) (k a0).
Proof.
intros E R3 Label priv l b1 b2 R2 RR2 A e k2 SECCHECK X e0 k a H0 a0 H1.
pfold. red.
punfold H1. red in H1. cbn in ×. remember (VisF e k2) as x.
remember (VisF e0 k) as y.
hinduction H1 before l; intros; try discriminate.
- inv Heqx. inv Heqy. ddestruction; subst. contradiction.
- pclearbot. inv Heqx. inv Heqy. ddestruction; subst. pstep_reverse.
- inv Heqx. ddestruction; subst. inv CHECK. clear H0.
specialize (H a).
rewrite Heqy in H. clear Heqy. remember (VisF e1 k) as y.
hinduction H before l; intros; inv Heqy; ddestruction; subst; try contradiction;
try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ unpriv_ind. pclearbot. pstep_reverse.
+ pclearbot. specialize (H a0). punfold H.
- inv Heqy. ddestruction; subst. inv CHECK. clear H0.
rewrite Heqx in H. specialize (H a0).
remember (VisF e0 k0) as y.
hinduction H before b1; intros; inv Heqy; ddestruction; subst; try contradiction;
try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. specialize (H a). punfold H.
- inv Heqx; inv Heqy; ddestruction; subst. contra_size.
- inv Heqx; inv Heqy; ddestruction; subst. contra_size.
Qed.
Lemma eqit_secure_private_VisLR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2),
nonempty A →
¬ leq (priv A e) l →
∀ (X : Type) (e0 : E X) (k : X → itree E R3),
¬ leq (priv X e0) l →
nonempty X →
(∀ a a0,
eqit_secure Label priv RR2 b1 b2 l (k2 a) (k a0)) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) .
Proof.
intros. pfold. red. cbn. unpriv_co. left. apply H3.
Qed.
Lemma eqit_secure_private_VisL:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b2 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R2) (t : itree E R3),
nonempty A →
¬ leq (priv A e) l →
(∀ a,
eqit_secure Label priv RR2 true b2 l (k2 a) t) →
eqit_secure Label priv RR2 true b2 l (Vis e k2) t .
Proof.
intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply H1.
Qed.
Lemma eqit_secure_private_VisR:
∀ (E : Type → Type) (R3 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 : bool) (R2 : Type) (RR2 : R2 → R3 → Prop) (A : Type)
(e : E A) (k2 : A → itree E R3) (t : itree E R2),
nonempty A →
¬ leq (priv A e) l →
(∀ a,
eqit_secure Label priv RR2 b1 true l t (k2 a)) →
eqit_secure Label priv RR2 b1 true l t (Vis e k2).
Proof.
intros. pfold. red. cbn. unpriv_ind. pstep_reverse. apply H1.
Qed.
Lemma eqit_secure_public_Vis : ∀ (E : Type → Type) (R1 R2 : Type) (Label : Preorder) (priv : ∀ x : Type, E x → L)
(l : L) (b1 b2 : bool) (RR : R1 → R2 → Prop) (A : Type)
(e : E A) (k1: A → itree E R1) (k2 : A → itree E R2),
leq (priv A e) l →
(eqit_secure Label priv RR b1 b2 l (Vis e k1) (Vis e k2) ↔
∀ a, eqit_secure Label priv RR b1 b2 l (k1 a) (k2 a)).
Proof.
split; intros.
- pinversion H0; ddestruction; subst; try contradiction; apply H2.
- pfold. constructor; auto. left. apply H0.
Qed.
Lemma eqit_secure_trans_aux1:
∀ (E : Type → Type) (R3 R1 : Type) (Label : Preorder)
(priv : ∀ x : Type, E x → L) (l : L) (b2 : bool) (R2 : Type)
(RR1 : R1 → R2 → Prop) (RR2 : R2 → R3 → Prop) (r : itree E R1 → itree E R3 → Prop)
(r0 : R3) (t4 : itree E R2),
secure_eqitF Label priv RR2 true b2 l id
(upaco2 (secure_eqit_ Label priv RR2 true b2 l id) bot2) (observe t4)
(RetF r0) →
∀ t : itree E R1,
paco2 (secure_eqit_ Label priv RR1 true b2 l id) bot2 t t4 →
secure_eqitF Label priv (rcompose RR1 RR2) true b2 l id
(upaco2 (secure_eqit_ Label priv (rcompose RR1 RR2) true b2 l id) r)
(observe t) (RetF r0).
Proof.
intros E R3 R1 Label priv l b2 R2 RR1 RR2 r r0 t4 Ht23 t H.
punfold H. red in H.
remember (RetF r0) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; auto.
- remember (RetF r1) as y.
hinduction H0 before r; intros; inv Heqy; eauto with itree.
rewrite itree_eta'. unpriv_ind. cbn. eapply H0; eauto.
- eapply IHHt23; eauto.
remember (TauF t1) as y.
hinduction H before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- assert (Hne : nonempty A). { eauto. } (* add the condition that lets us assume this*)
inv Hne. eapply (H0 a); eauto.
remember (VisF e k1) as y.
hinduction H1 before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. rewrite itree_eta' at 1. pstep_reverse.
Qed.
Lemma eqit_secure_trans_aux2:
∀ (E : Type → Type) (R3 R1 : Type) (Label : Preorder)
(priv : ∀ x : Type, E x → L) (l : L) (b2 : bool) (R2 : Type)
(RR1 : R1 → R2 → Prop) (RR2 : R2 → R3 → Prop) (r : itree E R1 → itree E R3 → Prop)
(X : Type) (e0 : E X) (k : X → itree E R3) (t4 : itree E R2),
leq (priv X e0) l →
secure_eqitF Label priv RR2 true b2 l id
(upaco2 (secure_eqit_ Label priv RR2 true b2 l id) bot2) (observe t4)
(VisF e0 k) →
(∀ (t1 : itree E R1) (t2 : itree E R2) (t3 : itree E R3),
eqit_secure Label priv RR1 true b2 l t1 t2 →
eqit_secure Label priv RR2 true b2 l t2 t3 → r t1 t3) →
∀ t : itree E R1,
paco2 (secure_eqit_ Label priv RR1 true b2 l id) bot2 t t4 →
secure_eqitF Label priv (rcompose RR1 RR2) true b2 l id
(upaco2 (secure_eqit_ Label priv (rcompose RR1 RR2) true b2 l id) r)
(observe t) (VisF e0 k).
Proof.
intros E R3 R1 Label priv l b2 R2 RR1 RR2 r X e0 k t4 He0 Ht23 CIH0 t Ht.
punfold Ht. red in Ht. remember (VisF e0 k) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK;
ddestruction; subst; try contradiction; eauto.
- eapply IHHt23; eauto. clear IHHt23. remember (TauF t1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. remember (VisF e0 k1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; eauto with itree.
+ pclearbot. constructor; auto. right. eapply CIH0. apply H.
apply H0.
+ rewrite itree_eta'. unpriv_ind. eapply H0; eauto.
- assert (nonempty A); eauto. inv H1. eapply H0; eauto.
Unshelve. all : auto. clear H0. rewrite H2 in H.
remember (VisF e k1) as y.
hinduction Ht before r; intros; inv Heqy; try inv CHECK; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. rewrite itree_eta' at 1. pstep_reverse.
Qed.
Lemma secret_halt_trans_1 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) t1 (e : E A) k t3,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l t1 (Vis e k) →
eqit_secure Label priv RR2 b1 b2 l (Vis e k) t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 A RR1 RR2 t1 e k t3 He HA.
generalize dependent t3. generalize dependent t1.
pcofix CIH. intros t1 t3 Ht1 Ht3.
pfold. red. punfold Ht1. red in Ht1. punfold Ht3. red in Ht3.
cbn in ×.
remember (VisF e k) as x.
hinduction Ht1 before r; intros; inv Heqx; ddestruction; subst;
try contradiction; try contra_size; eauto with itree.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size.
+ constructor. right. apply CIH; auto. pfold. auto.
+ unpriv_co; auto. right. apply CIH; auto. pfold. rewrite H0 in H2. apply H2.
+ pclearbot. constructor. right. apply CIH; auto.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. apply CIH; auto with itree. pfold.
red. cbn. unpriv_halt.
× unpriv_co. right. apply CIH; auto. apply H1.
+ pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
red. cbn. unpriv_halt. contra_size.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt.
× pfold. auto.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt.
× pfold. auto. rewrite H0 in H2. apply H2.
+ pclearbot. unpriv_halt. right. apply CIH; auto.
pfold. red. cbn. unpriv_halt.
+ pclearbot. unpriv_halt. right. apply CIH.
× pfold. red. cbn. unpriv_halt.
× apply H1.
+ unpriv_halt. contra_size.
- pclearbot. inv Ht3; ddestruction; subst; try contradiction; try contra_size;
destruct (classic_empty A0).
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt. contra_size.
× pfold. auto.
+ unpriv_co. right. apply CIH; auto; try apply H.
pfold. auto.
+ unpriv_halt. right. apply CIH; auto.
× pfold. red. cbn. unpriv_halt. contra_size.
× pfold. rewrite H0 in H2. apply H2.
+ unpriv_co. right. apply CIH. apply H. rewrite H0 in H2.
pfold. apply H2.
+ pclearbot. unpriv_halt. right. apply CIH; auto. pfold.
red. cbn. unpriv_halt. contra_size.
+ pclearbot. unpriv_co. right. apply CIH; auto. apply H.
+ unpriv_halt. pclearbot. right. apply CIH; try apply H1.
pfold. red. cbn. unpriv_halt. contra_size.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. apply CIH; auto. apply H.
pfold. red. cbn. unpriv_halt.
× unpriv_co. right. apply CIH; eauto. apply H. apply H1.
+ pclearbot. unpriv_halt. contra_size.
+ pclearbot. unpriv_halt. right. apply CIH; auto. apply H.
pfold. red. cbn. unpriv_halt. contra_size.
Qed.
Lemma secret_halt_trans_2 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) (e : E A) k t2 t3,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l (Vis e k) t2 →
eqit_secure Label priv RR2 b1 b2 l t2 t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l (Vis e k) t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 A RR1 RR2 e k t2 t3 He HA.
generalize dependent t3. generalize dependent t2.
pcofix CIH. intros t2 t3 Ht2 Ht23. pfold.
red. cbn. punfold Ht2. punfold Ht23. red in Ht2. red in Ht23.
cbn in ×.
hinduction Ht23 before r; intros; eauto with itree.
- inv Ht2. ddestruction; subst. contra_size.
- unpriv_halt. right. pclearbot. eapply CIH; eauto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
pfold. auto.
- eapply IHHt23; eauto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
punfold H0.
- pclearbot.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
- unpriv_halt. pclearbot. inv SIZECHECK. right. eapply CIH; try apply H.
Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
+ pfold. apply H2.
+ apply H1.
- pclearbot. unpriv_halt. right. eapply CIH; try apply H.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
pfold. auto.
- pclearbot. unpriv_halt. inv SIZECHECK1. inv SIZECHECK2. right. eapply CIH; try apply H.
Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
+ pfold. apply H2.
+ apply H1.
- inv SIZECHECK. eapply H0; eauto. Unshelve. all : auto.
inv Ht2; ddestruction; subst; try contra_size; try contradiction; pclearbot; eauto.
rewrite itree_eta' at 1. pstep_reverse.
- unpriv_halt. right. eapply CIH; eauto. pfold. apply Ht2.
pfold. apply H.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. auto.
- unpriv_halt. contra_size.
- unpriv_halt. right. pclearbot. eapply CIH with (t2 := Vis e1 k1); eauto.
+ pfold. auto.
+ apply H.
- unpriv_halt. contra_size.
Qed.
Lemma eqit_secure_RR_imp : ∀ E b1 b2 R1 R2 (RR1 RR2 : R1 → R2 → Prop) Label priv l
(t1 : itree E R1) (t2 : itree E R2),
RR1 <2= RR2 →
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t1 t2.
Proof.
intros. generalize dependent t2. revert t1.
pcofix CIH. intros t1 t2 Ht12. pfold. red.
punfold Ht12. red in Ht12.
hinduction Ht12 before r; intros; eauto;
try (pclearbot; constructor; auto; right; eapply CIH; eauto; fail);
try (pclearbot; unpriv_co; right; eapply CIH; eauto; apply H0; fail).
pclearbot. constructor; auto. right. eapply CIH; eauto. apply H0.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. apply H0.
- pclearbot. unpriv_halt. right. eapply CIH; eauto. apply H0.
Qed.
Lemma secret_halt_trans_3 : ∀ E Label priv l b1 b2 (R1 R2 R3 A : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) t1 t2 (e : E A) k,
(¬ leq (priv A e) l ) →
empty A →
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t2 (Vis e k) →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 (Vis e k).
Proof.
intros. apply eqit_secure_sym in H1. apply eqit_secure_sym in H2.
apply eqit_secure_sym. eapply secret_halt_trans_2 in H1; eauto.
eapply eqit_secure_RR_imp; eauto.
intros. inv PR. econstructor; eauto.
Qed.
Lemma eqit_secure_trans : ∀ E Label priv l b1 b2 (R1 R2 R3 : Type) (RR1 : R1 → R2 → Prop)
(RR2 : R2 → R3 → Prop) (t1 : itree E R1) (t2 : itree E R2) (t3 : itree E R3),
eqit_secure Label priv RR1 b1 b2 l t1 t2 →
eqit_secure Label priv RR2 b1 b2 l t2 t3 →
eqit_secure Label priv (rcompose RR1 RR2) b1 b2 l t1 t3.
Proof.
intros E Label priv l b1 b2 R1 R2 R3 RR1 RR2.
pcofix CIH0. intros t1 t2 t3 Ht12 Ht23.
punfold Ht12. red in Ht12. punfold Ht23. red in Ht23. pfold. red.
hinduction Ht12 before r; intros; try inv CHECK; auto with itree.
- remember (RetF r2) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; eauto with itree.
rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
- pclearbot. genobs t4 ot4.
assert ( (∃ t5, ot4 = TauF t5) ∨ (∀ t5, ot4 ≠ TauF t5) ).
{ destruct ot4; eauto; right; intros; discriminate. }
destruct H0 as [ [t5 Ht4] | Ht4].
+ subst. rewrite Ht4. rewrite Ht4 in Ht23. constructor.
right. eapply CIH0; eauto. eapply eqit_secure_TauLR. pfold.
auto.
+ destruct ot4; try (exfalso; eapply Ht4; eauto; fail ).
× inv Ht23. inv CHECK. rewrite itree_eta' at 1.
assert (eqit_secure Label priv (rcompose RR1 RR2) true b2 l (Tau t0) (Ret r0) ).
{ pfold. red. cbn. rewrite itree_eta' at 1. eapply eqit_secure_trans_aux1; eauto.
pfold. red. constructor; auto. pstep_reverse. }
rewrite itree_eta'. pstep_reverse. eapply paco2_mon; eauto.
intros; contradiction.
× destruct (classic (leq (priv _ e) l ) ).
-- inv Ht23; ddestruction; subst; try contradiction; try inv CHECK.
constructor; auto. eapply eqit_secure_trans_aux2; eauto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. rewrite itree_eta' at 1.
pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3 with (t2 := Tau t3); eauto.
** pfold. constructor. left. auto.
** pfold. auto.
++ unpriv_co. right. eapply CIH0; eauto.
assert (eqit_secure Label priv RR2 b1 b2 l (Tau t3) (Vis e k)).
pfold. auto. eapply eqit_secure_TauLVisR; eauto.
- apply IHHt12; auto.
remember (TauF t0) as y.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK; eauto with itree.
+ pclearbot. constructor; auto. pstep_reverse.
+ pclearbot. unpriv_ind. pstep_reverse.
+ pclearbot. punfold H.
- pclearbot. remember (VisF e k2) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; ddestruction; subst;
try contradiction; eauto with itree.
+ pclearbot. constructor; auto. intros. right. eapply CIH0; eauto; try apply H0.
apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
- pclearbot. remember (TauF t0) as x.
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; auto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0.
auto.
+ destruct ot2.
× clear IHHt23. rewrite itree_eta'. unpriv_ind.
remember (k1 a) as t. specialize (H a). setoid_rewrite <- Heqt in H.
clear Heqt a k1. cbn. eapply eqit_secure_trans_aux1; eauto.
× unpriv_co. right. eapply CIH0; try apply H.
clear IHHt23. remember (TauF t) as y.
pfold. red.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK; eauto with itree.
-- pclearbot. constructor; auto. pstep_reverse.
-- pclearbot. unpriv_ind. pstep_reverse.
-- pclearbot. punfold H.
× destruct (classic (leq (priv _ e0) l ) ).
-- rewrite itree_eta'. unpriv_ind. cbn.
clear IHHt23. remember (k1 a) as t. specialize (H a). setoid_rewrite <- Heqt in H.
clear Heqt a k1. eapply eqit_secure_trans_aux2; eauto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. unpriv_ind.
pstep_reverse. apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3; eauto. apply H.
pfold. auto.
++ unpriv_co. right. eapply CIH0. apply H.
clear IHHt23. pstep. red. remember (VisF e0 k) as y.
hinduction Ht23 before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; eauto with itree.
** pclearbot. constructor; auto. pstep_reverse.
** unpriv_ind. pclearbot. pstep_reverse.
** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
+ constructor; auto. eapply IHHt23; eauto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0. apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ unpriv_halt. right. pclearbot. eapply CIH0; eauto. apply H0.
- pclearbot.
genobs_clear t3 ot3.
assert (Hne : nonempty A); eauto. inv Hne.
assert ( (∃ t4, ot3 = TauF t4) ∨ (∀ t4, ot3 ≠ TauF t4) ).
{ destruct ot3; eauto; right; intros; discriminate. }
destruct H0 as [ [t4 Ht3] | Ht3].
+ subst. constructor. right. eapply CIH0; try apply H.
Unshelve. all: auto.
eapply eqit_secure_TauRVisL; eauto. pfold. auto.
(* should be fine but new lemma, also shelved goal *)
+
destruct ot3; try (exfalso; eapply Ht4; eauto; fail ).
× inv Ht23; inv CHECK. ddestruction. subst. clear CIH0.
constructor; auto. rewrite H4. eapply eqit_secure_trans_aux1; eauto.
rewrite <- H4. apply H1. Unshelve. auto. (* shelved goal*)
× constructor. right. eapply CIH0; try apply H.
eapply eqit_secure_TauRVisL; eauto. pfold. auto.
(* same goal as last admit *)
× destruct (classic (leq (priv _ e0) l ) ).
-- inv Ht23; try inv CHECK; ddestruction; subst; try contradiction.
constructor; auto. rewrite H5. eapply eqit_secure_trans_aux2; eauto.
rewrite <- H5. apply H2. Unshelve. all : auto.
-- destruct (classic_empty X).
++ rewrite itree_eta'. rewrite itree_eta' at 1. pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_3 with (t2 := Vis e k2); eauto.
** pfold. red. cbn. unpriv_co.
** pfold. auto.
++ unpriv_co. right. eapply CIH0; try apply H.
Unshelve. all : auto.
assert (eqit_secure Label priv RR2 b1 b2 l (Vis e k2) (Vis e0 k) ).
pfold. auto. eapply eqit_secure_VisLR; eauto.
- pclearbot. remember (VisF e2 k2) as x.
(* maybe need to separate the inductive and coinductive progress cases? *)
hinduction Ht23 before r; intros; inv Heqx; try inv CHECK; try contradiction;
try contra_size;
ddestruction; subst; auto.
+ constructor; auto. eapply IHHt23; eauto.
+ pclearbot. unpriv_co. right. eapply CIH0; try apply H0. apply H.
+ pclearbot. assert (Hne : nonempty B); eauto. inv Hne.
unpriv_co. right. eapply CIH0; eauto; try eapply H0. apply H.
Unshelve. auto.
+ pclearbot. assert (Hne : nonempty B0); eauto. inv Hne.
unpriv_co. right. eapply CIH0; try apply H0. apply H.
Unshelve. auto.
+ genobs t2 ot2. destruct ot2.
× assert (Hne : nonempty B); eauto. inv Hne.
rewrite itree_eta'. unpriv_ind. eapply eqit_secure_trans_aux1; eauto.
Unshelve. auto.
× assert (Hne : nonempty B); eauto. inv Hne.
unpriv_co. right. eapply CIH0; try apply H1. Unshelve. all : auto.
clear H0. specialize (H a). pfold. red. genobs (k2 a) ok2.
clear Heqok2 H1 k2.
remember (TauF t) as y.
hinduction H before r; intros; inv Heqy; try inv CHECK; auto.
-- constructor; auto. pclearbot. pstep_reverse.
-- constructor; eauto.
-- pclearbot. unpriv_ind. pstep_reverse.
-- unpriv_ind. eapply H0; eauto.
-- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
× inv SIZECHECK2.
destruct (classic (leq (priv _ e) l ) ).
-- rewrite itree_eta'. unpriv_ind.
eapply eqit_secure_trans_aux2; eauto. Unshelve. all : auto.
-- destruct (classic_empty X).
++ unpriv_halt. right. eapply CIH0; eauto. apply H1.
pfold. apply H. Unshelve. auto.
++ unpriv_co. right. eapply CIH0; try apply H1.
Unshelve. all : auto.
clear H0. pstep. red. remember (VisF e k) as y.
specialize (H a). clear Heqot2. genobs (k2 a) ok2.
clear Heqok2.
hinduction H before r; intros; inv Heqy; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; eauto with itree.
** pclearbot. constructor; auto. pstep_reverse.
** unpriv_ind. pclearbot. pstep_reverse.
** pclearbot. rewrite itree_eta' at 1. pstep_reverse.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ pclearbot. inv SIZECHECK2. unpriv_halt. right. eapply CIH0; eauto. apply H0.
apply H. Unshelve. auto.
- remember (VisF e k2) as x. hinduction Ht23 before r; intros; inv Heqx; try inv CHECK;
ddestruction; subst; try contradiction; try contra_size; auto.
+ constructor; auto. eapply IHHt23; eauto.
+ constructor; auto. pclearbot. assert (Hne : nonempty A0); eauto. inv Hne. eapply H0; eauto.
pstep_reverse. Unshelve. auto.
+ unpriv_ind. assert (Hne : nonempty A0); eauto. inv Hne. eapply H0; eauto.
pclearbot. pstep_reverse. Unshelve. auto.
+ assert (Hne : nonempty A0). { eauto. } inv Hne. eauto. Unshelve. auto.
+ unpriv_ind. eauto.
+ pclearbot. rewrite itree_eta'. pstep_reverse.
apply paco2_mon with (r := bot2); intros; try contradiction.
inv SIZECHECK0.
eapply secret_halt_trans_3 with (t2 := k0 a); eauto.
× pfold. apply H1.
× apply H.
- pclearbot.
remember (TauF t0) as y.
hinduction Ht23 before r; intros; inv Heqy; subst; eauto with itree; pclearbot.
+ unpriv_halt. right. eapply CIH0; eauto.
+ clear IHHt23. rewrite itree_eta'. rewrite itree_eta' at 1.
pstep_reverse. apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_2; eauto. pfold. auto.
+ unpriv_halt. right. eapply CIH0; eauto. apply H.
+ rewrite itree_eta' at 1. unpriv_ind. eapply H0; eauto.
+ unpriv_halt. contra_size.
- pclearbot.
inv Ht23; ddestruction; subst; try contra_size; try contradiction;
try inv CHECK.
+ constructor. right. eapply CIH0; eauto. pfold. auto.
+ unpriv_co. right. eapply CIH0; eauto. rewrite H0 in H2.
pfold. apply H2.
+ pclearbot. constructor. right. eapply CIH0; eauto.
+ pclearbot. destruct (classic_empty B).
× unpriv_halt. right. eapply CIH0; eauto. pfold. red. cbn. unpriv_halt.
× unpriv_co. right. eapply CIH0; eauto. apply H1.
+ pclearbot. unpriv_halt. right. eapply CIH0; eauto.
pfold. red. cbn. unpriv_halt. contra_size.
- pclearbot. rewrite itree_eta' at 1. pstep_reverse.
apply paco2_mon with (r := bot2); intros; try contradiction.
eapply secret_halt_trans_2 with (t2 := Vis e2 k2); eauto.
+ pfold. red. cbn. unpriv_halt.
+ pfold. auto.
- pclearbot. destruct (classic_empty A).
+ inv Ht23; ddestruction; subst; try contradiction; try contra_size; try inv CHECK.
× unpriv_halt. right. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- pfold. auto.
× unpriv_halt. right. rewrite H1 in H3. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- pfold. apply H3.
× unpriv_halt. pclearbot. right. eapply CIH0; eauto.
pfold. red. cbn. unpriv_halt. contra_size.
× unpriv_halt. pclearbot. right. eapply CIH0 with (t2 := Vis e2 k2); eauto.
-- pfold. red. cbn. unpriv_halt. contra_size.
-- apply H2.
× unpriv_halt. contra_size.
+ destruct (observe t3).
× inv Ht23; ddestruction; subst; try contra_size; try contradiction.
× unpriv_co. right. eapply CIH0; eauto. apply H.
inv Ht23; ddestruction; subst; try contra_size; try contradiction.
pfold. auto. pclearbot. auto.
× destruct (classic (leq (priv _ e) l ) ).
{ inv Ht23; ddestruction; subst; try contra_size; try contradiction. }
destruct (classic_empty X).
-- unpriv_halt. right. eapply CIH0; eauto. apply H. pfold. auto.
-- unpriv_co. right. eapply CIH0; eauto. apply H.
inv Ht23; ddestruction; subst; try contra_size; try contradiction.
++ pfold. apply H5.
++ pclearbot. apply H4.
Qed.
Lemma eqit_itree_eqit_secure : ∀ E Label priv l R1 R2 RR (t1 t1': itree E R1) (t2 : itree E R2),
t1 ≅ t1' → eqit_secure Label priv RR false false l t1 t2 →
eqit_secure Label priv RR false false l t1' t2.
Proof.
intros E Label priv l R1 R2 RR. pcofix CIH.
intros t1 t1' t2 Heq Hsec. pstep. red.
punfold Heq. red in Heq. punfold Hsec. red in Hsec.
inv Heq; try inv CHECK.
- rewrite <- H0 in Hsec. rewrite itree_eta' at 1. pstep_reverse.
eapply paco2_mon with (r := bot2); intros; try contradiction. pfold.
red. cbn. remember (RetF r2) as x. clear H H0.
hinduction Hsec before r; intros; inv Heqx; eauto with itree.
- pclearbot. genobs t2 ot2.
assert ( (∃ t3, ot2 = TauF t3) ∨ (∀ t3, ot2 ≠ TauF t3) ).
{ destruct ot2; eauto; right; intros; discriminate. }
destruct H1 as [ [t3 Ht2] | Ht2].
+ subst. rewrite Ht2. rewrite Ht2 in Hsec. constructor.
right. eapply CIH; eauto. rewrite <- H0 in Hsec. inv Hsec; try inv CHECK. pclearbot. auto.
+ destruct ot2; try (exfalso; eapply Ht2; eauto; fail ).
× rewrite <- H0 in Hsec. inv Hsec; try inv CHECK.
× rewrite <- H0 in Hsec. inv Hsec; ddestruction; subst; try inv CHECK.
-- pclearbot. unpriv_co. right. eapply CIH; eauto. apply H3.
-- pclearbot. unpriv_halt. right. eapply CIH; eauto.
- rewrite <- H0 in Hsec. inv Hsec; ddestruction; subst; try inv CHECK; try contradiction; try contra_size.
+ pclearbot. constructor; auto. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_co. right. eapply CIH; eauto with itree. apply H2.
+ pclearbot. unpriv_halt. right. eapply CIH; eauto. pfold. constructor. left. auto.
+ pclearbot. unpriv_halt. right. eapply CIH with (t1 := Vis e k1); try apply H2.
pfold. constructor. left. auto.
+ pclearbot. unpriv_halt. right. eapply CIH; eauto with itree. apply H2.
Qed.
Lemma eqit_secure_eq_trans : ∀ E R b1 b2 Label priv l (t1 t2 t3 : itree E R),
eqit_secure Label priv eq b1 b2 l t1 t2 →
eqit_secure Label priv eq b1 b2 l t2 t3 →
eqit_secure Label priv eq b1 b2 l t1 t3.
Proof.
intros. apply eqit_secure_RR_imp with (RR1 := rcompose eq eq).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
Qed.
Lemma eqit_secure_anything : ∀ E R1 b Label priv l
(t1 : itree E R1) t2,
eqit_secure Label priv eq b b l t1 t2 →
eqit_secure Label priv eq b b l t1 t1.
Proof.
intros.
eapply eqit_secure_eq_trans; eauto.
apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto.
Qed.
Global Instance proper_eqit_secure_eqit {E} {R1 R2 : Type} {b} {RR : R1 → R2 → Prop} {Label priv l} :
Proper (eqit eq b b ==> eqit eq b b ==> iff) (@eqit_secure E R1 R2 Label priv RR b b l).
Proof.
repeat intro. destruct b; split; intros.
- eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- assert (x ≈ y); auto. assert (x0 ≈ y0); auto.
symmetry in H2.
eapply eutt_secure_eqit_secure; eauto.
symmetry in H3. apply eqit_secure_sym.
eapply eutt_secure_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. auto.
- assert (x ≅ y); auto. assert (x0 ≅ y0); auto.
symmetry in H2. symmetry in H3.
eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. eapply eqit_itree_eqit_secure; eauto.
apply eqit_secure_sym. auto.
Qed.
Global Instance proper_eqit_secure_eqit_secure
{E} {b} {R1 R2 : Type} {RR : R1 → R2 → Prop} {Label priv l} :
Proper (eqit_secure Label priv eq b b l ==> eqit_secure Label priv eq b b l ==> iff)
(@eqit_secure E R1 R2 Label priv RR b b l).
Proof.
repeat intro; split; intros.
- eapply eqit_secure_RR_imp with (RR1 := rcompose RR eq); eauto.
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
apply eqit_secure_sym.
eapply eqit_secure_RR_imp with (RR1 := rcompose (flip RR) eq); eauto.
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto. apply eqit_secure_sym. auto.
- assert (eqit_secure Label priv eq b b l y0 x0).
{ apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
eapply eqit_secure_RR_imp with (RR1 := rcompose RR eq).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
assert (eqit_secure Label priv eq b b l y x).
{ apply eqit_secure_sym. eapply eqit_secure_RR_imp; eauto. }
eapply eqit_secure_RR_imp with (RR1 := rcompose eq RR).
{ intros. inv PR. auto. }
eapply eqit_secure_trans; eauto.
Qed.