Definition of twoSC from Mastroeni & Pasqua SAS18

Author: Carmine Abate

Criteria.v

@@ -259,17 +259,25 @@ Theorem R2SCHC_R2SCHP : R2SCHC <-> R2SCHP.
 Proof.
   split.
     - intros ssc P H HH. rewrite contra_RHP. intros [C' H0].
-    specialize (ssc P C'). unfold twoSC in HH. destruct HH as [t1 [t2 HH]].
-    specialize (ssc t1 t2). destruct ssc as [C h0].
-    split; firstorder.
-    exists C. firstorder.
-  - unfold R2SCHC. intros h0 P C' t1 t2 [H1 H2].
+      specialize (ssc P C'). rewrite (HH (beh (C' [P ↓]))) in H0.
+      destruct H0 as [t1 [t2 [b_t1 [b_t2 H_t1_t2]]]]. 
+      destruct (ssc t1 t2) as [Cs [bs_t1 bs_t2]]. auto.
+      exists Cs. rewrite (HH _). exists t1, t2. split; auto. 
+  - unfold R2SCHC. intros h0 P C' t1 t2 [H1 H2]. 
     specialize (h0 P).
-    assert (s : twoSC (fun π => (~(sem tgt ( C' [ P ↓ ]) t1 -> π t1)) \/ (~(sem tgt ( C' [ P ↓ ]) t2 -> π t2)))).
-    { unfold twoSC. intros. exists t1, t2. intros b. split.
-      intros. apply de_morgan2 in H. destruct H as [H1' H2'].
-      apply dne in H1'. apply dne in H2'. split; auto.
-      intros H. apply de_morgan2. split; rewrite <- dne; destruct H; intros; try assumption.
+    assert (s : twoSC (fun π => (~(sem tgt ( C' [ P ↓ ]) t1 -> π t1)) \/
+                              (~(sem tgt ( C' [ P ↓ ]) t2 -> π t2)))).
+    { unfold twoSC. intros. split.
+      + intros h.
+        exists t1, t2. rewrite de_morgan2 in h. destruct h as [h1 h2].
+        rewrite <- dne in h1, h2. 
+        repeat (split; auto). 
+        intros [k | k]; apply k; [ now left | now right ]. 
+      +  intros [t3 [t4 [b_t3 [b_t4 K]]]].
+         rewrite de_morgan2. rewrite <- dne. rewrite <- dne.
+         rewrite de_morgan2 in K. destruct K as [k1 k2]. rewrite <- dne in k1,k2.
+         specialize (k1 H1). specialize (k2 H2).
+         destruct k1, k2; now subst.     
     }
     specialize (h0 (fun π => (~(sem tgt ( C' [ P ↓ ]) t1 -> π t1)) \/ (~(sem tgt ( C' [ P ↓ ]) t2 -> π t2)))).
     specialize (h0 s).
@@ -335,12 +343,11 @@ Proof.
 Qed.
 
 Lemma R2SCHC_R2HSC : R2SCHC -> R2HSC.
-Proof. 
-  intros rsc P Ct m1 m2 H. unfold spref in *.
-  destruct (H m1) as [t1 [Ht1 Hpref1]]; auto.   
-  destruct (H m2) as [t2 [Ht2 Hpref2]]; auto.
-  specialize (rsc P Ct t1 t2). destruct rsc as [Cs [K1 K2]]; auto.
-  exists Cs. intros x [H1 | H2]; subst; [now exists t1 | now exists t2].
+Proof.
+  rewrite R2SCHC_R2SCHP. rewrite R2HSC_R2HSP.
+  intros twosc P S two_safetyS.
+  apply twoSC_H2Safe in two_safetyS.
+  now apply (twosc P S).
 Qed.
 
 

Properties.v

@@ -208,12 +208,28 @@ Proof.
     + unfold lifting in *. now apply (subset_trans k h π).
 Qed.
 
+(* definition by "Verifying Bounded Subset-Closed Hyperproperties" 
+   - Mastroeni, Pasqua *)
 Definition twoSC (H : hprop) : Prop :=
-  exists t1 t2, forall b, ~ (H b) <->  (b t1 /\ b t2).
+  forall b, ~ (H b) <-> (exists t1 t2, (b t1 /\ b t2 /\ ~ H (fun t => t = t1 \/ t = t2))).
+
+Lemma twoSC_SSC (H: hprop) : twoSC H -> SSC H.
+Proof.
+  intros twosc b H_b b' b'_leq_b.
+  apply NNPP. intros not_H_b'.
+  rewrite (twosc b') in not_H_b'. destruct not_H_b' as [t1 [t2 [b_t1 [b_t2 H_t1_t2]]]].
+  rewrite dne in H_b. apply H_b.
+  rewrite (twosc _). exists t1, t2. split; auto.
+Qed. 
 
 (* 2SC Hyperproperties *)
 
-(* CA : according to this definition
+(* CA : according to the old definition 
+
+         H ∈ twoSC iff ∃ t1 t2. ∀ b. ~ (H b) <->  (b t1 /\ b t2).
+
+         hence
+
          H ∈ k-SC iff 
          ∃ t1 .. tk, H = lifting (true \ t1) ∪ .. ∪ lifting (true \ tk)
 
@@ -285,7 +301,24 @@ Definition H2Safe (H : hprop) : Prop :=
                     spref (fun m => m = m1 \/ m = m2) b /\
                     forall b', spref (fun m => m = m1 \/ m = m2) b' -> ~(H b')).
 
-
+Lemma twoSC_H2Safe (H : hprop) : H2Safe H -> twoSC H.
+Proof.
+  intros hsafe_H b. split.
+  + intros not_H_b. destruct (hsafe_H b not_H_b) as [m1 [m2 [spref_b wit]]].
+    destruct (spref_b m1) as [t1 [b_t1 m1_t1]]; auto.     
+    destruct (spref_b m2) as [t2 [b_t2 m2_t2]]; auto. 
+    exists t1, t2. repeat (split; auto). apply wit.
+    intros m [M1 | M2]; subst; [exists t1 | exists t2]; auto. 
+  + intros [t1 [t2 [b_t1 [b_t2 not_H]]]].
+    destruct (hsafe_H _ not_H) as [m1 [m2 [spref_b wit]]].
+    apply wit.
+    intros m [M1 | M2]; subst.
+    ++ destruct (spref_b m1) as [t [b_t pref_t]]; auto.
+       destruct b_t; subst; [now exists t1 | now exists t2].
+    ++ destruct (spref_b m2) as [t [b_t pref_t]]; auto.
+       destruct b_t; subst; [now exists t1 | now exists t2].
+Qed.    
+    
 (** *HyperLiveness *)
 Definition HLiv (H : hprop) : Prop :=
   forall M, Observations M ->