WIP on main theorem

proofs/ssprove/handwritten/Core.v

@@ -158,9 +158,24 @@ Section Core.
     all: Lia.lia.
   Qed.
 
+Lemma trimmed_eq_rect_r :
+  forall L I1 I2 E (m : package L I1 E) (f : I2 = I1),
+    trimmed E (eq_rect_r (fun I => package L I E) m f) = trimmed E m.
+Proof. now destruct f. Qed.
+
+Lemma trimmed_eq_rect_r2 :
+  forall L I E1 E2 (m : package L I E1) (f : E2 = E1),
+    trimmed E1 (eq_rect_r [eta package L I] m f) = trimmed E2 m.
+Proof. now destruct f. Qed.
+
+Lemma trimmed_eq_rect :
+  forall L I E1 E2 (m : package L I E1) g H,
+    trimmed E2 (eq_rect E1 (fun E => package L I E) m g H) = trimmed E2 m.
+Proof. now destruct H. Qed.
+
   Obligation Tactic := (* try timeout 8 *) idtac.
   Program Definition Gcore_real (* (d : nat) *) :
-    package L_K
+    package (L_K :|: L_L)
       ((GET_XPD
           :|: SET_XPD
           :|: DH_Set_interface
@@ -172,9 +187,69 @@ Section Core.
     (*   #val #[DHEXP] : 'unit → 'unit ] :|: XTR_n_ℓ d :|: XPD_n_ℓ d :|:  *)
     (*    GET_o_star_ℓ d) *)
     :=
-    {package (K_O_star false) ∘ ((* Gcore_hyb ∘ *) (par (par (XPD_packages (* d *)) (XTR_packages (* d *))) (DH_package)))}.
+    {package ((* par  *)(K_O_star false) ∘ (Ls O_star F (erefl))) ∘ ((* Gcore_hyb ∘ *)
+         (par (par (XPD_packages (* d *)) (XTR_packages (* d *))) (DH_package)))}.
   Final Obligation.
-  Admitted.
+
+  rewrite <- fsetU0.
+  eapply valid_link.
+  {
+    eapply valid_link.
+    2: apply (Ls _ _ _).
+    1: apply K_O_star.
+  }
+  ssprove_valid.
+    - 
+    apply @parable.
+    rewrite <- trimmed_dh.
+    eassert (trimmed _ XPD_packages) by apply trimmed_ℓ_packages.
+    rewrite <- H ; clear H.
+    eassert (trimmed _ XTR_packages) by apply trimmed_ℓ_packages.
+    rewrite <- H ; clear H.
+    solve_Parable.
+    {
+      rewrite fdisjointC.
+      apply idents_interface_hierachy2.
+      intros.
+      unfold idents.
+      unfold DH_interface.
+      rewrite fset_cons.
+      solve_imfset_disjoint.
+      all: unfold DHGEN, DHEXP, XPD, serialize_name ; Lia.lia.
+    }
+    {
+      rewrite fdisjointC.
+      apply idents_interface_hierachy2.
+      intros.
+      unfold idents.
+      unfold DH_interface.
+      rewrite fset_cons.
+      solve_imfset_disjoint.
+      all: unfold DHGEN, DHEXP, XTR, serialize_name ; Lia.lia.
+    }
+  - apply @parable.
+    eassert (trimmed _ XPD_packages) by apply trimmed_ℓ_packages.
+    rewrite <- H ; clear H.
+    eassert (trimmed _ XTR_packages) by apply trimmed_ℓ_packages.
+    rewrite <- H ; clear H.
+    solve_Parable.
+    {
+      apply idents_interface_hierachy2.
+      intros.
+      rewrite fdisjointC.
+      apply idents_interface_hierachy2.
+      intros.
+      unfold idents.
+      solve_imfset_disjoint.
+    }
+  - rewrite fsetUid.
+    apply fsubsetxx.
+  - apply fsubsetxx.
+  - apply fsubsetxx.
+  - rewrite fsetUid.
+    apply fsubsetxx.
+  - solve_in_fset.
+  Defined.
   Fail Next Obligation.
 
   Program Definition Gcore_ideal (* (d : nat) *) (Score : Simulator) :

proofs/ssprove/handwritten/CoreTheorem.v

@@ -113,7 +113,7 @@ Lemma core_theorem :
   (* forall (d : nat), *)
   forall (Score : Simulator),
   forall (LA : {fset Location}) (A : raw_package),
-      ValidPackage LA [interface #val #[ KS ] : 'unit → chTranscript ] A_export A →
+      ValidPackage LA KS_interface A_export A →
     (AdvantageE
        (Gcore_real (* d *))
        (Gcore_ideal (* d *) Score) (A (* ∘ R d M H *))
@@ -127,7 +127,7 @@ Lemma equation20_lhs :
   forall (Score : Simulator),
   forall i,
   forall (LA : {fset Location}) (A : raw_package),
-      ValidPackage LA [interface #val #[ KS ] : 'unit → chTranscript ] A_export A →
+      ValidPackage LA KS_interface A_export A →
     (AdvantageE Gcore_sodh (Gcore_hyb 0) (Ai A i) = 0)%R.
 Proof. Admitted.
 
@@ -136,7 +136,7 @@ Lemma equation20_rhs :
   forall (Score : Simulator),
   forall i,
   forall (LA : {fset Location}) (A : raw_package),
-      ValidPackage LA [interface #val #[ KS ] : 'unit → chTranscript ] A_export A →
+      ValidPackage LA KS_interface A_export A →
     (AdvantageE Gcore_ki (Gcore_hyb d) (Ai A i) = 0)%R.
 Proof. Admitted.
 
@@ -146,7 +146,7 @@ Lemma hyb_telescope :
   (* forall (K_table : chHandle -> nat), *)
   forall i,
   forall (LA : {fset Location}) (A : raw_package),
-      ValidPackage LA [interface #val #[ KS ] : 'unit → chTranscript ] A_export A →
+      ValidPackage LA KS_interface A_export A →
       (AdvantageE (Gcore_hyb 0) (Gcore_hyb d) (Ai A i)
        = sumR 0 (d-1) (fun ℓ => AdvantageE (Gcore_hyb ℓ) (Gcore_hyb (ℓ+1)) (Ai A i))
       )%R.
@@ -158,7 +158,7 @@ Lemma equation20_eq :
   (* forall (K_table : chHandle -> nat), *)
   forall i,
   forall (LA : {fset Location}) (A : raw_package),
-      ValidPackage LA [interface #val #[ KS ] : 'unit → chTranscript ] A_export A →
+      ValidPackage LA KS_interface A_export A →
     (AdvantageE Gcore_sodh (Gcore_ideal (* d *) Score) (Ai A i)
      <= AdvantageE Gcore_ki (Gcore_ideal (* d *) Score) (Ai A i)
      +sumR 0 (d-1) (fun ℓ => AdvantageE (Gcore_hyb ℓ) (Gcore_hyb (ℓ + 1)) (Ai A i))

proofs/ssprove/handwritten/ExtraTypes.v

@@ -74,7 +74,7 @@ Notation " 'chTranscript' " :=
   (t_Handle)
     (in custom pack_type at level 2).
 
-Definition KS : nat := 0%nat.
+(* Definition KS : nat := 0%nat. *)
 
 (* Fig. 12, p. 18 *)
 (* Fig.29, P.63 *)

proofs/ssprove/handwritten/KeyPackages.v

@@ -137,10 +137,6 @@ Fail Next Obligation.
 (* Definition fin_K_table : finType := Casts.prod_finType fin_key 'bool. *)
 (* Definition chK_table := chFin (mkpos #|fin_K_table|). *)
 
-(* Definition fset_K_table : {fset Location}. Admitted. *)
-(* Lemma in_K_table : forall x, ('option chK_table; K_table x) \in fset_K_table. *)
-(* Proof. Admitted. *)
-
 Definition K_package (n : name) (ℓ : nat) (* (d : nat) *) (_ : (ℓ <= d)%nat) (b : bool) :
   package
     L_K
@@ -332,7 +328,7 @@ Proof.
       unfold valid_pairs ; fold valid_pairs.
 
       destruct Names ; [ apply (L_package a P) | split ; [ apply (L_package a P)  | apply IHNames ] ].
-Qed.
+Defined.
 
 Definition Ks (Names : list name) (b : bool) :
   uniq Names ->

proofs/ssprove/handwritten/KeySchedulePackages.v

@@ -103,7 +103,7 @@ Section KeySchedulePackages.
   Obligation Tactic := (* try timeout 8 *) idtac.
   Definition Gks_real (* (d : nat) *) :
     package
-      L_K
+      (L_K :|: L_L)
       (GET_XPD :|: SET_XPD :|: DH_Set_interface :|: [interface #val #[HASH] : chHASHout → chHASHout ] :|: (GET_XTR :|: SET_XTR))
       (SET_O_star_ℓ :|: GET_O_star_ℓ)
     (* ] *) :=