From 5c511b1a1b4aa965c872c4bb00fbffe65ccc655d Mon Sep 17 00:00:00 2001
From: Lasse Letager Hansen <letager@cs.au.dk>
Date: Fri, 6 Jun 2025 16:39:46 +0200
Subject: [PATCH 1/7] Add some useful advantage properties

---
 theories/Crypt/package/pkg_advantage.v | 120 +++++++++++++++++++++++++
 1 file changed, 120 insertions(+)

diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index d5ba65a8..e09ead97 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -418,3 +418,123 @@ Tactic Notation
   "ssprove" "triangle" constr(p₀) constr(l) constr(p₁) constr(A)
   "as" ident(ineq) :=
   ssprove_triangle_as p₀ l p₁ A ineq.
+
+Lemma advantage_helper :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  forall {LK IK EK},
+  forall {A : bool -> raw_package}
+    {B : bool -> raw_package}
+    {K : bool -> raw_package},
+    fsubset IA EK ->
+    fsubset IB EK ->
+    fsubset IK [interface] ->
+    (forall b, ValidPackage LA IA EA (A b)) ->
+    (forall b, ValidPackage LB IB EB (B b)) ->
+    (forall b, ValidPackage LK IK EK (K b)) ->
+    (forall b, trimmed EA (A b)) ->
+    (forall b, trimmed EB (B b)) ->
+    (forall b, trimmed EK (K b)) ->
+    forall ε ν,
+      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R) ->
+      (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= ν)%R) ->
+      (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= ν + ε)%R).
+Proof.
+  intros.
+  rewrite (package_split (K false)).
+  rewrite (package_split (K true)).
+  erewrite <- !interchange ; [ | try (easy || apply ignore_Parable) .. ].
+  2-5: eapply valid_package_inject_export ; [ | easy ] ; assumption.
+  eapply Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
+  apply Num.Theory.lerD.
+  {
+    erewrite Advantage_par ;
+      [ | (eapply valid_link || eapply flat_valid_package || apply trimmed_link) ; try easy.. ].
+    2-4: eapply valid_package_inject_export ; [ | eapply valid_package_inject_import ; easy ] ; assumption.
+    apply H9.
+  }
+  {
+    erewrite Advantage_parR ;
+      [ | (eapply valid_link || eapply flat_valid_package || apply trimmed_link) ; try easy.. ].
+    2-4: eapply valid_package_inject_export ; [ | eapply valid_package_inject_import ; easy ] ; assumption.
+    apply H8.
+  }
+  Unshelve. all: apply false.
+Qed.
+
+Corollary advantage_helper0 :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  forall {LK IK EK},
+  forall {A : bool -> raw_package}
+    {B : bool -> raw_package}
+    {K : bool -> raw_package},
+    fsubset IA EK ->
+    fsubset IB EK ->
+    fsubset IK [interface] ->
+    (forall b, ValidPackage LA IA EA (A b)) ->
+    (forall b, ValidPackage LB IB EB (B b)) ->
+    (forall b, ValidPackage LK IK EK (K b)) ->
+    (forall b, trimmed EA (A b)) ->
+    (forall b, trimmed EB (B b)) ->
+    (forall b, trimmed EK (K b)) ->
+    (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= 0)%R) ->
+    (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= 0)%R) ->
+    (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= 0)%R).
+Proof. intros. rewrite <- (add0r 0%R). now rewrite advantage_helper. Qed.
+
+Lemma link_par_right :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  (* forall {LC IC EC}, *)
+  forall {A : raw_package}
+    {B : raw_package}
+    {C : raw_package},
+    fsubset IA EB ->
+    ValidPackage LA IA EA A ->
+    ValidPackage LB IB EB B ->
+    (* ValidPackage LC IC EC C -> *)
+    trimmed EA A ->
+    A ∘ par B C = A ∘ B.
+Proof.
+  intros.
+  apply eq_fmap.
+  unfold link.
+  intro n. repeat rewrite ?mapmE.
+  destruct (A n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity.
+  cbn. f_equal. f_equal. f_equal. extensionality x.
+  erewrite (code_link_par_left _ _ _ _ IA) ; [ reflexivity | | eapply valid_package_inject_export ; easy ].
+
+  eapply trimmed_valid_Some_in in e as hi ; [ | eassumption.. ].
+  eapply from_valid_package in H0.
+  specialize (H0 _ hi).
+  destruct H0 as [g [eg hg]].
+  rewrite e in eg.
+  noconf eg.
+  cbn in hg.
+  apply hg.
+Qed.
+
+Lemma advantage_helper2 :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  forall {A : bool -> raw_package}
+    {B : bool -> raw_package}
+    {C : bool -> raw_package}
+    {K : bool -> raw_package},
+    fsubset IA EB ->
+    (forall b, ValidPackage LA IA EA (A b)) ->
+    (forall b, ValidPackage LB IB EB (B b)) ->
+    (forall b, trimmed EA (A b)) ->
+    (forall b, K b = par (B b) (C b)) ->
+    forall ε,
+      (forall Adv, (AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
+      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
+Proof.
+  intros.
+  subst.
+  rewrite !H3.
+  rewrite link_par_right ; [ | easy .. ].
+  rewrite link_par_right ; [ | easy .. ].
+  apply H4.
+Qed.

From 94fe0e89bec1ec8461f040f6db5a9e699bd01d5d Mon Sep 17 00:00:00 2001
From: Lasse Letager Hansen <letager@cs.au.dk>
Date: Tue, 10 Jun 2025 20:48:49 +0200
Subject: [PATCH 2/7] Fixed to main

---
 theories/Crypt/package/fmap_extra.v      |  11 ++
 theories/Crypt/package/pkg_advantage.v   | 211 ++++++++++++++---------
 theories/Crypt/package/pkg_composition.v |  84 +++++++++
 3 files changed, 221 insertions(+), 85 deletions(-)

diff --git a/theories/Crypt/package/fmap_extra.v b/theories/Crypt/package/fmap_extra.v
index cbe54637..5c41a993 100644
--- a/theories/Crypt/package/fmap_extra.v
+++ b/theories/Crypt/package/fmap_extra.v
@@ -153,6 +153,17 @@ Qed.
 Lemma fsubmapxx {T : ordType} {S} (m : {fmap T → S}) : fsubmap m m.
 Proof. rewrite /fsubmap unionmI //. Qed.
 
+Lemma fsubmap_implies_fcompat :
+  forall {T : ordType} {S} {E E' : _},
+    fsubmap E' E →
+    fcompat (T := T) (S := S) E' E.
+Proof.
+  intros.
+  eapply fsubmap_fcompat.
+  1: apply H.
+  apply fsubmapxx.
+Qed.
+
 Lemma fsubmap_eq {T : ordType} {S} (m m' : {fmap T → S}) :
   fsubmap m m' → fsubmap m' m → m = m'.
 Proof.
diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index e09ead97..6317af24 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -294,6 +294,44 @@ Proof.
   rewrite -Advantage_link Advantage_par_empty //.
 Qed.
 
+Lemma Advantage_par_emptyR :
+  ∀ G₀ G₁ A,
+  AdvantageE (par G₀ emptym) (par G₁ emptym) A = AdvantageE G₀ G₁ A.
+Proof.
+  intros G₀ G₁ A.
+  unfold AdvantageE.
+  unfold par.
+  rewrite !unionm0.
+  reflexivity.
+Qed.
+
+Lemma Advantage_parR :
+  ∀ G₀ G₁ G₁' A L₀ L₁ L₁' E₀ E₁,
+    ValidPackage L₀ Game_import E₀ G₀ →
+    ValidPackage L₁ Game_import E₁ G₁ →
+    ValidPackage L₁' Game_import E₁ G₁' →
+    AdvantageE (par G₁ G₀) (par G₁' G₀) A =
+    AdvantageE G₁ G₁' (A ∘ par (ID E₁) G₀).
+Proof.
+  intros G₀ G₁ G₁' A L₀ L₁ L₁' E₀ E₁ Va0 Va1 Va1'.
+  replace (par G₁ G₀) with ((par (ID E₁) G₀) ∘ (par G₁ (ID Game_import))).
+  2:{
+    erewrite <- interchange.
+    all: ssprove_valid.
+    2: fmap_solve.
+    rewrite link_id // id_link //.
+  }
+  replace (par G₁' G₀) with ((par (ID E₁) G₀) ∘ (par G₁' (ID Game_import))).
+  2:{
+    erewrite <- interchange.
+    all: ssprove_valid.
+    2: fmap_solve.
+    rewrite link_id // id_link //.
+  }
+  replace (ID Game_import) with (emptym : raw_package) by now apply eq_fmap.
+  rewrite -Advantage_link !Advantage_par_emptyR //.
+Qed.
+
 Lemma Advantage_sym :
   ∀ P Q A,
     AdvantageE P Q A = AdvantageE Q P A.
@@ -419,122 +457,125 @@ Tactic Notation
   "as" ident(ineq) :=
   ssprove_triangle_as p₀ l p₁ A ineq.
 
-Lemma advantage_helper :
+Lemma valid_package_inject_export_weak :
+  ∀ L I E1 E2 p,
+    fsubmap E1 E2 →
+    ValidPackage L I E2 p →
+    ValidPackage L I E1 p.
+Proof.
+Admitted.
+
+Lemma package_duplicate :
+  forall p, p = par p p.
+Proof.
+  intros.
+  unfold par.
+  now rewrite unionmI.
+Qed.
+
+Lemma Advantage_split_par :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  forall {A : bool -> raw_package}
+    {B : bool -> raw_package}
+    {C : bool -> raw_package}
+    {K : bool -> raw_package},
+    fsubmap IA EB ->
+    (forall b, ValidPackage LA IA EA (A b)) ->
+    (forall b, ValidPackage LB IB EB (B b)) ->
+    (forall b, K b = par (B b) (C b)) ->
+    forall ε,
+      (forall Adv, (AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
+      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
+Proof.
+  intros.
+  subst.
+  rewrite !H2.
+  rewrite link_par_left ; [ | easy .. ].
+  rewrite link_par_left ; [ | easy .. ].
+  apply H3.
+Qed.
+
+Lemma Advantage_split_parR :
+  forall {LA IA EA},
+  forall {LC IC EC},
+  forall {A : bool -> raw_package}
+    {B : bool -> raw_package}
+    {C : bool -> raw_package}
+    {K : bool -> raw_package},
+    fsubmap IA EC ->
+    (forall b, fseparate (B b) (C b)) ->
+    (forall b, ValidPackage LA IA EA (A b)) ->
+    (forall b, ValidPackage LC IC EC (C b)) ->
+    (forall b, K b = par (B b) (C b)) ->
+    forall ε,
+      (forall Adv, (AdvantageE (A false ∘ C false) (A true ∘ C true) Adv <= ε)%R) ->
+      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
+Proof.
+  intros.
+  subst.
+  rewrite !H3.
+  rewrite link_par_right ; [ | easy .. ].
+  rewrite link_par_right ; [ | easy .. ].
+  apply H4.
+Qed.
+
+Lemma Advantage_common_par :
   forall {LA IA EA},
   forall {LB IB EB},
   forall {LK IK EK},
   forall {A : bool -> raw_package}
     {B : bool -> raw_package}
     {K : bool -> raw_package},
-    fsubset IA EK ->
-    fsubset IB EK ->
-    fsubset IK [interface] ->
+    fsubmap IA EK ->
+    fsubmap IB EK ->
+    fsubmap IK [interface] ->
     (forall b, ValidPackage LA IA EA (A b)) ->
     (forall b, ValidPackage LB IB EB (B b)) ->
     (forall b, ValidPackage LK IK EK (K b)) ->
-    (forall b, trimmed EA (A b)) ->
-    (forall b, trimmed EB (B b)) ->
-    (forall b, trimmed EK (K b)) ->
+    fcompat LA LK ->
+    fcompat LB LK ->
     forall ε ν,
       (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R) ->
       (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= ν)%R) ->
       (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= ν + ε)%R).
 Proof.
   intros.
-  rewrite (package_split (K false)).
-  rewrite (package_split (K true)).
-  erewrite <- !interchange ; [ | try (easy || apply ignore_Parable) .. ].
-  2-5: eapply valid_package_inject_export ; [ | easy ] ; assumption.
-  eapply Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
+  rewrite (package_duplicate (K false)).
+  rewrite (package_duplicate (K true)).
+  erewrite <- !interchange_alt ; [ | try (easy || apply fsubmapxx) .. ].
+  2-5: eapply valid_package_inject_export_weak ; [ | easy ] ; assumption.
+  Locate le_trans.
+  eapply order.Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
   apply Num.Theory.lerD.
   {
-    erewrite Advantage_par ;
-      [ | (eapply valid_link || eapply flat_valid_package || apply trimmed_link) ; try easy.. ].
-    2-4: eapply valid_package_inject_export ; [ | eapply valid_package_inject_import ; easy ] ; assumption.
-    apply H9.
+    erewrite Advantage_par.
+    2-4: eapply valid_link ; try eapply valid_package_inject_import ; auto ; assumption.
+    apply H8.
   }
   {
-    erewrite Advantage_parR ;
-      [ | (eapply valid_link || eapply flat_valid_package || apply trimmed_link) ; try easy.. ].
-    2-4: eapply valid_package_inject_export ; [ | eapply valid_package_inject_import ; easy ] ; assumption.
-    apply H8.
+    erewrite Advantage_parR.
+    2-4: eapply valid_link ; try eapply valid_package_inject_import ; auto ; assumption.
+    apply H7.
   }
-  Unshelve. all: apply false.
 Qed.
 
-Corollary advantage_helper0 :
+Corollary Advantage_common_par0 :
   forall {LA IA EA},
   forall {LB IB EB},
   forall {LK IK EK},
   forall {A : bool -> raw_package}
     {B : bool -> raw_package}
     {K : bool -> raw_package},
-    fsubset IA EK ->
-    fsubset IB EK ->
-    fsubset IK [interface] ->
+    fsubmap IA EK ->
+    fsubmap IB EK ->
+    fsubmap IK [interface] ->
     (forall b, ValidPackage LA IA EA (A b)) ->
     (forall b, ValidPackage LB IB EB (B b)) ->
     (forall b, ValidPackage LK IK EK (K b)) ->
-    (forall b, trimmed EA (A b)) ->
-    (forall b, trimmed EB (B b)) ->
-    (forall b, trimmed EK (K b)) ->
+    fcompat LA LK ->
+    fcompat LB LK ->
     (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= 0)%R) ->
     (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= 0)%R) ->
     (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= 0)%R).
-Proof. intros. rewrite <- (add0r 0%R). now rewrite advantage_helper. Qed.
-
-Lemma link_par_right :
-  forall {LA IA EA},
-  forall {LB IB EB},
-  (* forall {LC IC EC}, *)
-  forall {A : raw_package}
-    {B : raw_package}
-    {C : raw_package},
-    fsubset IA EB ->
-    ValidPackage LA IA EA A ->
-    ValidPackage LB IB EB B ->
-    (* ValidPackage LC IC EC C -> *)
-    trimmed EA A ->
-    A ∘ par B C = A ∘ B.
-Proof.
-  intros.
-  apply eq_fmap.
-  unfold link.
-  intro n. repeat rewrite ?mapmE.
-  destruct (A n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity.
-  cbn. f_equal. f_equal. f_equal. extensionality x.
-  erewrite (code_link_par_left _ _ _ _ IA) ; [ reflexivity | | eapply valid_package_inject_export ; easy ].
-
-  eapply trimmed_valid_Some_in in e as hi ; [ | eassumption.. ].
-  eapply from_valid_package in H0.
-  specialize (H0 _ hi).
-  destruct H0 as [g [eg hg]].
-  rewrite e in eg.
-  noconf eg.
-  cbn in hg.
-  apply hg.
-Qed.
-
-Lemma advantage_helper2 :
-  forall {LA IA EA},
-  forall {LB IB EB},
-  forall {A : bool -> raw_package}
-    {B : bool -> raw_package}
-    {C : bool -> raw_package}
-    {K : bool -> raw_package},
-    fsubset IA EB ->
-    (forall b, ValidPackage LA IA EA (A b)) ->
-    (forall b, ValidPackage LB IB EB (B b)) ->
-    (forall b, trimmed EA (A b)) ->
-    (forall b, K b = par (B b) (C b)) ->
-    forall ε,
-      (forall Adv, (AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
-      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
-Proof.
-  intros.
-  subst.
-  rewrite !H3.
-  rewrite link_par_right ; [ | easy .. ].
-  rewrite link_par_right ; [ | easy .. ].
-  apply H4.
-Qed.
+Proof. intros. rewrite <- (GRing.add0r 0%R). now rewrite Advantage_common_par. Qed.
diff --git a/theories/Crypt/package/pkg_composition.v b/theories/Crypt/package/pkg_composition.v
index b2be1904..399f21ef 100644
--- a/theories/Crypt/package/pkg_composition.v
+++ b/theories/Crypt/package/pkg_composition.v
@@ -370,6 +370,55 @@ Proof.
   all: eauto.
 Qed.
 
+Lemma link_par_left :
+  forall {LA IA EA},
+  forall {LB IB EB},
+  forall {A : raw_package}
+    {B : raw_package}
+    {C : raw_package},
+    fsubmap IA EB ->
+    ValidPackage LA IA EA A ->
+    ValidPackage LB IB EB B ->
+    link A (par B C) = link A B.
+Proof.
+  intros.
+  apply eq_fmap.
+  unfold link.
+  intro n. repeat rewrite ?mapmE.
+  destruct (A n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity.
+  cbn. f_equal. f_equal. f_equal. extensionality x.
+  erewrite code_link_par_left ; [ reflexivity |  | apply H1 ].
+  eapply valid_injectMap.
+  1: apply H.
+  apply (valid_imports LA IA EA A H0 n (S1; T1; f1) x).
+  apply e.
+Qed.
+
+Lemma link_par_right :
+  forall {LA IA EA},
+  forall {LC IC EC},
+  forall {A : raw_package}
+    {B : raw_package}
+    {C : raw_package},
+    fsubmap IA EC ->
+    fseparate B C ->
+    ValidPackage LA IA EA A ->
+    ValidPackage LC IC EC C ->
+    link A (par B C) = link A C.
+Proof.
+  intros.
+  apply eq_fmap.
+  unfold link.
+  intro n. repeat rewrite ?mapmE.
+  destruct (A n) as [[S1 [T1 f1]]|] eqn:e. 2: reflexivity.
+  cbn. f_equal. f_equal. f_equal. extensionality x.
+  erewrite code_link_par_right ; [ reflexivity | assumption |  | apply H2 ].
+  eapply valid_injectMap.
+  1: apply H.
+  apply (valid_imports LA IA EA A H1 n (S1; T1; f1) x).
+  apply e.
+Qed.
+
 Lemma interchange :
   ∀ A B C D E F L1 L2 L3 L4 p1 p2 p3 p4,
     ValidPackage L1 B A p1 →
@@ -408,6 +457,41 @@ Proof.
     apply (hi2 n (S; T; f) x), e'.
 Qed.
 
+Lemma interchange_alt :
+  ∀ A B C D E F L1 L2 L3 L4 p1 p2 p3 p4,
+    ValidPackage L1 B A p1 →
+    ValidPackage L2 E D p2 →
+    ValidPackage L3 C B p3 →
+    ValidPackage L4 F E p4 →
+    (fsubmap p3 p4) ->
+    par (link p1 p3) (link p2 p4) = link (par p1 p2) (par p3 p4).
+Proof.
+  intros A B C D E F L1 L2 L3 L4 p1 p2 p3 p4 h1 h2 h3 h4 s34.
+  apply eq_fmap => n.
+  rewrite /par unionmE 3!mapmE unionmE.
+  destruct (A n) as [[S T]|] eqn:e.
+  - destruct h1 as [he1 hi1].
+    specialize (he1 (n, (S, T))).
+    simpl in he1.
+    rewrite he1 in e.
+    destruct e as [f e].
+    rewrite e //=.
+    do 3 f_equal. extensionality x.
+    erewrite code_link_par_left => //.
+    2: apply h3.
+    apply (hi1 n (S; T; f) x), e.
+  - move: e => /dommPn; rewrite valid_domm; move=> /dommPn -> //=.
+    destruct (D n) as [[S T]|] eqn:e'.
+    2: move: e' => /dommPn; rewrite valid_domm; move=> /dommPn -> //=.
+    destruct h2 as [he2 hi2].
+    specialize (he2 (n, (S, T))).
+    simpl in he2.
+    rewrite he2 in e'.
+    destruct e' as [f e'].
+    rewrite e' //=.
+    do 3 f_equal. extensionality x.
+    now rewrite s34.
+Qed.
 
 Local Open Scope type_scope.
 

From c6b6799c704df53e06fc28731dfeab22e7e5ccf2 Mon Sep 17 00:00:00 2001
From: Lasse Letager Hansen <letager@cs.au.dk>
Date: Sun, 15 Jun 2025 15:37:04 +0200
Subject: [PATCH 3/7] Remove admits and make advantage statements useful

---
 theories/Crypt/package/pkg_advantage.v | 345 +++++++++++++++++++++++--
 1 file changed, 318 insertions(+), 27 deletions(-)

diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index 6317af24..61de735d 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -258,14 +258,14 @@ Proof.
   unfold AdvantageE. rewrite !link_assoc. reflexivity.
 Qed.
 
+Lemma par_empty : forall G, par emptym G = G.
+Proof. now setoid_rewrite union0m. Qed.
+
 Lemma Advantage_par_empty :
   ∀ G₀ G₁ A,
   AdvantageE (par emptym G₀) (par emptym G₁) A = AdvantageE G₀ G₁ A.
 Proof.
-  intros G₀ G₁ A.
-  unfold AdvantageE.
-  rewrite distrC.
-  reflexivity.
+  intros G₀ G₁ A. now rewrite !par_empty.
 Qed.
 
 Lemma Advantage_par :
@@ -294,15 +294,14 @@ Proof.
   rewrite -Advantage_link Advantage_par_empty //.
 Qed.
 
+Lemma par_emptyR : forall G, par G emptym = G.
+Proof. now setoid_rewrite unionm0. Qed.
+
 Lemma Advantage_par_emptyR :
   ∀ G₀ G₁ A,
   AdvantageE (par G₀ emptym) (par G₁ emptym) A = AdvantageE G₀ G₁ A.
 Proof.
-  intros G₀ G₁ A.
-  unfold AdvantageE.
-  unfold par.
-  rewrite !unionm0.
-  reflexivity.
+  intros G₀ G₁ A. now rewrite !par_emptyR.
 Qed.
 
 Lemma Advantage_parR :
@@ -457,13 +456,217 @@ Tactic Notation
   "as" ident(ineq) :=
   ssprove_triangle_as p₀ l p₁ A ineq.
 
+Lemma unionm_isSome :
+  forall {T : ordType} {S} (m m' : {fmap T -> S}) o,
+    isSome (unionm m m' o) <-> isSome (m o) ∨ isSome (m' o).
+Proof.
+  intros ? ? ? ? ?.
+  rewrite unionmE.
+  destruct (m o) ; split ; [  left |  |  right | intros [] ] ; easy.
+Qed.
+
+Lemma fhas_unionm_iff : forall {T : ordType} {S} (m m' : {fmap T -> S}) o,
+    fhas (unionm m m') o <-> (fhas m o ∨ (m o.1 = None /\ fhas m' o)).
+Proof.
+  intros ? ? ? ? [k v].
+  unfold fhas.
+  simpl.
+  rewrite unionmE.
+  destruct (m k) ; split ; [ left | intros [ | [] ] | right | intros [] ] ; easy.
+Qed.
+
+Lemma simple_neg :
+  forall (E1 : Interface) (p1 : raw_package),
+  ∀ o,
+    (forall (s t : choice_type), fhas E1 (o, (s, t)) ↔ (∃ f, fhas p1 (o, (s; t; f)))) ->
+    (E1 o = None ↔ p1 o = None).
+Proof.
+  intros E1 p1 o.
+  intros.
+  split ; [
+      destruct (p1 o) as [ [s [t f]] | ] eqn:p1o ; [ intros ; exfalso | reflexivity ]
+    | destruct (E1 o) as [ [ s t ] | ] eqn:E1o ; [ intros ; exfalso | reflexivity ] ] ; specialize (H s t).
+  all: rewrite <- (boolp.iff_not2) in H ; rewrite <- boolp.forallNP in H ;  simpl in H.
+  - assert (E1 o <> Some (s, t)) by now rewrite H0.
+    now specialize (proj1 H H1 f).
+  - assert (forall x, p1 o <> Some (s; t; x)) by now intros ; rewrite H0.
+    now specialize (proj2 H H1).
+Qed.
+
+Lemma simple_neg2 :
+  forall (E1 : Interface) (p1 : raw_package),
+  ∀ o,
+    (E1 o = None ↔ p1 o = None) -> (E1 = mapm (λ '(So; To; _), (So, To)) p1) ->
+    forall (s t : choice_type), fhas E1 (o, (s, t)) ↔ (∃ f, fhas p1 (o, (s; t; f))).
+Proof.
+  intros E1 p1 o.
+  intros ?.
+  intros ?.
+
+  apply eq_fmap in H0.
+  specialize (H0 o).
+  rewrite mapmE in H0.
+  unfold omap, obind, oapp in H0.
+  simpl.
+  rewrite H0 ; clear H0.
+
+  destruct (getm p1 o) as [[s1 [t1 f1]]|] eqn:p1o_eq ; rewrite p1o_eq.
+  2: now split ; [ | intros [] ].
+  intros.
+  split.
+  - intros. inversion H0 ; subst. now exists f1.
+  - now intros [] ; inversion H0 ; subst.
+Qed.
+
+
+Lemma ValidPackage_eq : forall L I E p, ValidPackage L I E p <-> E = mapm (λ '(So; To; _), (So, To)) p /\ ∀ (n : Datatypes_nat__canonical__Ord_Ord) (F : typed_raw_function) (x : F.π1),
+    fhas p (n, F) → ValidCode L I ((F.π2).π2 x).
+Proof.
+  clear ; intros.
+  split.
+  - intros ?.
+    split.
+    + apply (valid_exports_eq _).
+    + apply H.
+  - intros [] ; subst.
+    constructor.
+    + intros [o [s t]].
+      simpl.
+      rewrite mapmE.
+      unfold omap, obind, oapp.
+      destruct (getm p o) as [[s1 [t1 f1]]|] eqn:p1o_eq ; rewrite p1o_eq ; [ clear p1o_eq | split ; [ | intros [] ] ; discriminate ].
+      split.
+      * intros. inversion H ; subst. now exists f1.
+      * intros []. now inversion H ; subst.
+    + apply H0.
+Qed.
+
+(* Lemma valid_link_iff: *)
+(*   ∀ (L1 L2 : Locations) (I M E : Interface) (p1 p2 : raw_package), *)
+(*     (ValidPackage L1 M E p1 *)
+(*      /\ ValidPackage L2 I M p2 *)
+(*      /\ fcompat L1 L2) <-> ValidPackage (unionm L1 L2) I E (p1 ∘ p2). *)
+(* Proof. *)
+(*   split ; [ intros [? []] | intros ]. *)
+(*   - now apply (valid_link L1 L2 I M E). *)
+(*   - split. *)
+(*     + (* epose unionm_isSome. *) *)
+(*       (* fhas_unionm_iff *) *)
+
+
+(* Lemma fcompat_split_unionm : *)
+(*   forall {E1 E2 : Interface}, *)
+(*   fcompat E1 E2 -> *)
+(*   forall o s t, *)
+(*   fhas E1 (o, (s, t)) ∨ E1 o = None ∧ fhas E2 (o, (s, t)) *)
+(*   ↔ fhas E2 (o, (s, t)) ∨ E2 o = None ∧ fhas E1 (o, (s, t)). *)
+(* Proof. *)
+(*   intros. *)
+(*   rewrite <- (fhas_unionm_iff E1 E2 (o, (s, t))). *)
+(*   rewrite <- (fhas_unionm_iff E2 E1 (o, (s, t))). *)
+(*   now rewrite H. *)
+(* Qed. *)
+
+Lemma fcompat_fhas_case :
+  forall {T : ordType} {S} {E1 E2 : {fmap T -> S}},
+  fcompat E1 E2 ->
+  forall o, (fhas E1 o -> (fhas E2 o \/ E2 o.1 = None)).
+Proof.
+  intros ? ? ? ? ? [k v] ?.
+  simpl.
+  epose proof (proj1 (fhas_unionm_iff E2 E1 (k, v))).
+  rewrite <- H in H1.
+  specialize (H1 ((fhas_union_l _ _ _ _ H0))).
+
+  epose proof (proj1 (fhas_unionm_iff E1 E2 (k, v)) (fhas_union_l _ _ _ _ H0)).
+
+  destruct H1 as [| []].
+  + now left.
+  + destruct H2 as [| [] ].
+    * now right.
+    * now left.
+Qed.
+
+Lemma fcompat_split_unionm :
+  forall {T : ordType} {S} {E1 E2 : {fmap T -> S}},
+  fcompat E1 E2 ->
+  forall o,
+    fhas (unionm E1 E2) o ->
+    (E1 o.1 = Some o.2 <-> E2 o.1 = None)
+    \/ (E1 o.1 = None <-> E2 o.1 = Some o.2)
+    \/ (E1 o.1 = Some o.2 <-> E2 o.1 = Some o.2).
+Proof.
+  intros ? ? ? ? ? [k v] ?.
+  
+  simpl.
+  epose proof (proj1 (fhas_unionm_iff E2 E1 (k, v))).
+  rewrite <- H in H1.
+  specialize (H1 H0).
+
+  epose proof (proj1 (fhas_unionm_iff E1 E2 (k, v)) H0).
+
+  destruct H1 as [| []].
+  + destruct H2 as [| [] ].
+    * rewrite H1 H2.
+      now right ; right.
+    * rewrite H1 H2.
+      now right ; left.
+  + rewrite H1 H3.
+    now left.
+Qed.
+
+Lemma fmap_as_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  exists l, mkfmap l = p2.
+Proof.
+  destruct p2.
+  exists fmval.
+  - apply eq_fmap.
+    apply mkfmapE.
+Qed.
+
+Lemma fmapK_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  mkfmap (FMap.fmval p2) = p2.
+Proof.
+  destruct p2.
+  apply eq_fmap.
+  apply mkfmapE.
+Qed.
+
 Lemma valid_package_inject_export_weak :
-  ∀ L I E1 E2 p,
-    fsubmap E1 E2 →
-    ValidPackage L I E2 p →
-    ValidPackage L I E1 p.
+  ∀ L I E1 E2 p1 p2,
+    fseparate E1 E2 ->
+    E1 = mapm (λ '(So; To; _), (So, To)) p1 ->
+    E2 = mapm (λ '(So; To; _), (So, To)) p2 ->
+    ValidPackage L I E1 p1 /\ ValidPackage L I E2 p2 <->
+    ValidPackage L I (unionm E1 E2) (unionm p1 p2).
 Proof.
-Admitted.
+  intros ? ? ? ? ? ? ?.
+  split ; [ intros [] | intros ].
+  - rewrite <- (unionmI L).
+    rewrite <- (unionmI I).
+    now apply valid_par.
+  - rewrite ValidPackage_eq in H2. destruct H2.
+    rewrite !ValidPackage_eq.
+    split ; split ; [ assumption | | assumption | ].
+    + intros.
+      eapply H3.
+      apply fhas_union_l.
+      apply H4.
+    + intros.
+
+      rewrite unionmC in H3.
+      2:{
+        destruct H.
+        subst.
+        rewrite !domm_map in H.
+        apply H.
+      }
+      eapply H3.
+      apply fhas_union_l.
+      apply H4.
+Qed.
 
 Lemma package_duplicate :
   forall p, p = par p p.
@@ -484,9 +687,10 @@ Lemma Advantage_split_par :
     (forall b, ValidPackage LA IA EA (A b)) ->
     (forall b, ValidPackage LB IB EB (B b)) ->
     (forall b, K b = par (B b) (C b)) ->
+    forall Adv, 
     forall ε,
-      (forall Adv, (AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
-      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
+      ((AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
+      ((AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
 Proof.
   intros.
   subst.
@@ -508,9 +712,10 @@ Lemma Advantage_split_parR :
     (forall b, ValidPackage LA IA EA (A b)) ->
     (forall b, ValidPackage LC IC EC (C b)) ->
     (forall b, K b = par (B b) (C b)) ->
+    forall Adv,
     forall ε,
-      (forall Adv, (AdvantageE (A false ∘ C false) (A true ∘ C true) Adv <= ε)%R) ->
-      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
+      ((AdvantageE (A false ∘ C false) (A true ∘ C true) Adv <= ε)%R) ->
+      ((AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
 Proof.
   intros.
   subst.
@@ -520,6 +725,89 @@ Proof.
   apply H4.
 Qed.
 
+  Lemma in_cat :
+    forall (X : eqType) l1 l2, forall (x : X), (x \in (l1 ++ l2)) = ((x \in l1) || (x \in l2)).
+  Proof.
+    intros.
+    generalize dependent l1.
+    induction l2 ; intros.
+    + setoid_rewrite List.app_nil_r.
+      now rewrite Bool.orb_false_r.
+    + replace (l1 ++ _) with ((l1 ++ [:: a]) ++ l2).
+      2:{
+        rewrite <- List.app_assoc.
+        reflexivity.
+      }
+      rewrite IHl2.
+      rewrite in_cons.
+      induction l1.
+      * simpl.
+        rewrite in_cons.
+        rewrite in_nil.
+        now rewrite Bool.orb_false_r.
+      * simpl.
+        rewrite !in_cons.
+        rewrite <- !orbA.
+        now rewrite IHl1.
+  Qed.
+
+Lemma fdisjoint_weak : (forall {T : ordType}, forall (A B C : {fset T}), A :#: B -> A :#: (B :\: C)).
+Proof.
+  intros.
+  apply /fsetDidPl.
+  rewrite fsetDDr.
+  move /fsetDidPl: H ->.
+  apply eq_fset.
+  intros i.
+  rewrite in_fset.
+  simpl.
+  rewrite in_cat.
+  rewrite in_fsetI.
+  destruct (i \in A) eqn:i_in ; now rewrite i_in.
+Qed.
+
+Lemma fsubmap_split :
+  forall {T : ordType} {S}, forall (A B : {fmap T -> S}), fsubmap A B -> exists C, unionm A C = B /\ fseparate A C.
+Proof.
+  clear ; intros.
+  exists (filterm (fun x y => x \notin domm A) B).
+
+  assert (unionm A (filterm (λ (x : T) (_ : S), x \notin domm A) B) = B).
+  {
+    apply eq_fmap.
+    intros ?.
+    rewrite unionmE.
+    destruct (A x) eqn:Ahas.
+    + simpl.
+      symmetry.
+      apply (fsubmap_fhas _ _ (x, s) H Ahas).
+    + simpl.
+      rewrite filtermE.
+      unfold obind, oapp.
+      move /dommPn: Ahas ->.
+      now destruct (B x).
+  }
+  split.
+  - apply H0.
+  - simpl.
+    rewrite <- (fmapK_list B) in H, H0 |- *.
+    destruct B ; simpl in *.
+    simpl.
+    constructor.
+    clear i H H0.
+    induction fmval.
+    + rewrite filterm0.
+      rewrite domm0.
+      apply fdisjoints0.
+    + simpl.
+      rewrite filterm_set.
+
+      destruct (a.1 \notin domm A) eqn:a_not_in_A.
+      2: rewrite domm_rem ; apply fdisjoint_weak.
+      1: rewrite domm_set ; rewrite fdisjointUr ; rewrite fdisjoints1 ; rewrite a_not_in_A ; simpl.
+      1,2: apply IHfmval.
+Qed.
+
 Lemma Advantage_common_par :
   forall {LA IA EA},
   forall {LB IB EB},
@@ -535,17 +823,19 @@ Lemma Advantage_common_par :
     (forall b, ValidPackage LK IK EK (K b)) ->
     fcompat LA LK ->
     fcompat LB LK ->
+    forall Adv,
     forall ε ν,
-      (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R) ->
-      (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= ν)%R) ->
-      (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= ν + ε)%R).
+      ((AdvantageE (A false ∘ K false) (A true ∘ K true) (Adv ∘ par (ID EA) (B true ∘ K true)) <= ε)%R) ->
+      ((AdvantageE (B false ∘ K false) (B true ∘ K true) (Adv ∘ par (A false ∘ K false) (ID EB)) <= ν)%R) ->
+      ((AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= ν + ε)%R).
 Proof.
   intros.
   rewrite (package_duplicate (K false)).
   rewrite (package_duplicate (K true)).
-  erewrite <- !interchange_alt ; [ | try (easy || apply fsubmapxx) .. ].
-  2-5: eapply valid_package_inject_export_weak ; [ | easy ] ; assumption.
-  Locate le_trans.
+  erewrite <- !interchange_alt ; [ | try apply fsubmapxx .. ].
+  4,5,8,9: apply H4.
+  2,4: now eapply valid_package_inject_import ; [ | eapply H2 ].
+  2,3: now eapply valid_package_inject_import ; [ | eapply H3 ].
   eapply order.Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
   apply Num.Theory.lerD.
   {
@@ -575,7 +865,8 @@ Corollary Advantage_common_par0 :
     (forall b, ValidPackage LK IK EK (K b)) ->
     fcompat LA LK ->
     fcompat LB LK ->
-    (forall Adv, (AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= 0)%R) ->
-    (forall Adv, (AdvantageE (B false ∘ K false) (B true ∘ K true) Adv <= 0)%R) ->
-    (forall Adv, (AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= 0)%R).
+    forall Adv,
+    ((AdvantageE (A false ∘ K false) (A true ∘ K true) (Adv ∘ par (ID EA) (B true ∘ K true)) <= 0)%R) ->
+    ((AdvantageE (B false ∘ K false) (B true ∘ K true) (Adv ∘ par (A false ∘ K false) (ID EB)) <= 0)%R) ->
+    ((AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= 0)%R).
 Proof. intros. rewrite <- (GRing.add0r 0%R). now rewrite Advantage_common_par. Qed.

From 3aaee8c8911bc034f149d40cfa989c814884f6d6 Mon Sep 17 00:00:00 2001
From: Lasse Letager Hansen <letager@cs.au.dk>
Date: Sun, 15 Jun 2025 15:51:28 +0200
Subject: [PATCH 4/7] Minor fixes

---
 theories/Crypt/package/fmap_extra.v      | 102 +++++++++++++++++
 theories/Crypt/package/pkg_advantage.v   | 138 +----------------------
 theories/Crypt/package/pkg_composition.v |  22 +---
 3 files changed, 109 insertions(+), 153 deletions(-)

diff --git a/theories/Crypt/package/fmap_extra.v b/theories/Crypt/package/fmap_extra.v
index 5c41a993..6116bf80 100644
--- a/theories/Crypt/package/fmap_extra.v
+++ b/theories/Crypt/package/fmap_extra.v
@@ -524,3 +524,105 @@ Qed.
 
 Hint Extern 4 (is_true (_ \notin _)) =>
   eapply notin_has_separate; [ eassumption | ] : fmap_solve_db.
+
+Lemma fmap_as_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  exists l, mkfmap l = p2.
+Proof.
+  destruct p2.
+  exists fmval.
+  - apply eq_fmap.
+    apply mkfmapE.
+Qed.
+
+Lemma fmapK_list :
+  forall {T : ordType} {S} (p2 : {fmap T -> S}),
+  mkfmap (FMap.fmval p2) = p2.
+Proof.
+  destruct p2.
+  apply eq_fmap.
+  apply mkfmapE.
+Qed.
+
+Lemma in_cat :
+  forall (X : eqType) l1 l2, forall (x : X), (x \in (l1 ++ l2)) = ((x \in l1) || (x \in l2)).
+Proof.
+  intros.
+  generalize dependent l1.
+  induction l2 ; intros.
+  + setoid_rewrite List.app_nil_r.
+    now rewrite Bool.orb_false_r.
+  + replace (l1 ++ _) with ((l1 ++ [:: a]) ++ l2).
+    2:{
+      rewrite <- List.app_assoc.
+      reflexivity.
+    }
+    rewrite IHl2.
+    rewrite in_cons.
+    induction l1.
+    * simpl.
+      rewrite in_cons.
+      rewrite in_nil.
+      now rewrite Bool.orb_false_r.
+    * simpl.
+      rewrite !in_cons.
+      rewrite <- !orbA.
+      now rewrite IHl1.
+Qed.
+
+Lemma fdisjoint_weak : (forall {T : ordType}, forall (A B C : {fset T}), A :#: B -> A :#: (B :\: C)).
+Proof.
+  intros.
+  apply /fsetDidPl.
+  rewrite fsetDDr.
+  move /fsetDidPl: H ->.
+  apply eq_fset.
+  intros i.
+  rewrite in_fset.
+  simpl.
+  rewrite in_cat.
+  rewrite in_fsetI.
+  destruct (i \in A) eqn:i_in ; now rewrite i_in.
+Qed.
+
+Lemma fsubmap_split :
+  forall {T : ordType} {S}, forall (A B : {fmap T -> S}), fsubmap A B -> exists C, unionm A C = B /\ fseparate A C.
+Proof.
+  clear ; intros.
+  exists (filterm (fun x y => x \notin domm A) B).
+
+  assert (unionm A (filterm (λ (x : T) (_ : S), x \notin domm A) B) = B).
+  {
+    apply eq_fmap.
+    intros ?.
+    rewrite unionmE.
+    destruct (A x) eqn:Ahas.
+    + simpl.
+      symmetry.
+      apply (fsubmap_fhas _ _ (x, s) H Ahas).
+    + simpl.
+      rewrite filtermE.
+      unfold obind, oapp.
+      move /dommPn: Ahas ->.
+      now destruct (B x).
+  }
+  split.
+  - apply H0.
+  - simpl.
+    rewrite <- (fmapK_list B) in H, H0 |- *.
+    destruct B ; simpl in *.
+    simpl.
+    constructor.
+    clear i H H0.
+    induction fmval.
+    + rewrite filterm0.
+      rewrite domm0.
+      apply fdisjoints0.
+    + simpl.
+      rewrite filterm_set.
+
+      destruct (a.1 \notin domm A) eqn:a_not_in_A.
+      2: rewrite domm_rem ; apply fdisjoint_weak.
+      1: rewrite domm_set ; rewrite fdisjointUr ; rewrite fdisjoints1 ; rewrite a_not_in_A ; simpl.
+      1,2: apply IHfmval.
+Qed.
diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index 61de735d..1fbcc272 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -541,32 +541,6 @@ Proof.
     + apply H0.
 Qed.
 
-(* Lemma valid_link_iff: *)
-(*   ∀ (L1 L2 : Locations) (I M E : Interface) (p1 p2 : raw_package), *)
-(*     (ValidPackage L1 M E p1 *)
-(*      /\ ValidPackage L2 I M p2 *)
-(*      /\ fcompat L1 L2) <-> ValidPackage (unionm L1 L2) I E (p1 ∘ p2). *)
-(* Proof. *)
-(*   split ; [ intros [? []] | intros ]. *)
-(*   - now apply (valid_link L1 L2 I M E). *)
-(*   - split. *)
-(*     + (* epose unionm_isSome. *) *)
-(*       (* fhas_unionm_iff *) *)
-
-
-(* Lemma fcompat_split_unionm : *)
-(*   forall {E1 E2 : Interface}, *)
-(*   fcompat E1 E2 -> *)
-(*   forall o s t, *)
-(*   fhas E1 (o, (s, t)) ∨ E1 o = None ∧ fhas E2 (o, (s, t)) *)
-(*   ↔ fhas E2 (o, (s, t)) ∨ E2 o = None ∧ fhas E1 (o, (s, t)). *)
-(* Proof. *)
-(*   intros. *)
-(*   rewrite <- (fhas_unionm_iff E1 E2 (o, (s, t))). *)
-(*   rewrite <- (fhas_unionm_iff E2 E1 (o, (s, t))). *)
-(*   now rewrite H. *)
-(* Qed. *)
-
 Lemma fcompat_fhas_case :
   forall {T : ordType} {S} {E1 E2 : {fmap T -> S}},
   fcompat E1 E2 ->
@@ -597,7 +571,7 @@ Lemma fcompat_split_unionm :
     \/ (E1 o.1 = Some o.2 <-> E2 o.1 = Some o.2).
 Proof.
   intros ? ? ? ? ? [k v] ?.
-  
+
   simpl.
   epose proof (proj1 (fhas_unionm_iff E2 E1 (k, v))).
   rewrite <- H in H1.
@@ -615,25 +589,6 @@ Proof.
     now left.
 Qed.
 
-Lemma fmap_as_list :
-  forall {T : ordType} {S} (p2 : {fmap T -> S}),
-  exists l, mkfmap l = p2.
-Proof.
-  destruct p2.
-  exists fmval.
-  - apply eq_fmap.
-    apply mkfmapE.
-Qed.
-
-Lemma fmapK_list :
-  forall {T : ordType} {S} (p2 : {fmap T -> S}),
-  mkfmap (FMap.fmval p2) = p2.
-Proof.
-  destruct p2.
-  apply eq_fmap.
-  apply mkfmapE.
-Qed.
-
 Lemma valid_package_inject_export_weak :
   ∀ L I E1 E2 p1 p2,
     fseparate E1 E2 ->
@@ -725,89 +680,6 @@ Proof.
   apply H4.
 Qed.
 
-  Lemma in_cat :
-    forall (X : eqType) l1 l2, forall (x : X), (x \in (l1 ++ l2)) = ((x \in l1) || (x \in l2)).
-  Proof.
-    intros.
-    generalize dependent l1.
-    induction l2 ; intros.
-    + setoid_rewrite List.app_nil_r.
-      now rewrite Bool.orb_false_r.
-    + replace (l1 ++ _) with ((l1 ++ [:: a]) ++ l2).
-      2:{
-        rewrite <- List.app_assoc.
-        reflexivity.
-      }
-      rewrite IHl2.
-      rewrite in_cons.
-      induction l1.
-      * simpl.
-        rewrite in_cons.
-        rewrite in_nil.
-        now rewrite Bool.orb_false_r.
-      * simpl.
-        rewrite !in_cons.
-        rewrite <- !orbA.
-        now rewrite IHl1.
-  Qed.
-
-Lemma fdisjoint_weak : (forall {T : ordType}, forall (A B C : {fset T}), A :#: B -> A :#: (B :\: C)).
-Proof.
-  intros.
-  apply /fsetDidPl.
-  rewrite fsetDDr.
-  move /fsetDidPl: H ->.
-  apply eq_fset.
-  intros i.
-  rewrite in_fset.
-  simpl.
-  rewrite in_cat.
-  rewrite in_fsetI.
-  destruct (i \in A) eqn:i_in ; now rewrite i_in.
-Qed.
-
-Lemma fsubmap_split :
-  forall {T : ordType} {S}, forall (A B : {fmap T -> S}), fsubmap A B -> exists C, unionm A C = B /\ fseparate A C.
-Proof.
-  clear ; intros.
-  exists (filterm (fun x y => x \notin domm A) B).
-
-  assert (unionm A (filterm (λ (x : T) (_ : S), x \notin domm A) B) = B).
-  {
-    apply eq_fmap.
-    intros ?.
-    rewrite unionmE.
-    destruct (A x) eqn:Ahas.
-    + simpl.
-      symmetry.
-      apply (fsubmap_fhas _ _ (x, s) H Ahas).
-    + simpl.
-      rewrite filtermE.
-      unfold obind, oapp.
-      move /dommPn: Ahas ->.
-      now destruct (B x).
-  }
-  split.
-  - apply H0.
-  - simpl.
-    rewrite <- (fmapK_list B) in H, H0 |- *.
-    destruct B ; simpl in *.
-    simpl.
-    constructor.
-    clear i H H0.
-    induction fmval.
-    + rewrite filterm0.
-      rewrite domm0.
-      apply fdisjoints0.
-    + simpl.
-      rewrite filterm_set.
-
-      destruct (a.1 \notin domm A) eqn:a_not_in_A.
-      2: rewrite domm_rem ; apply fdisjoint_weak.
-      1: rewrite domm_set ; rewrite fdisjointUr ; rewrite fdisjoints1 ; rewrite a_not_in_A ; simpl.
-      1,2: apply IHfmval.
-Qed.
-
 Lemma Advantage_common_par :
   forall {LA IA EA},
   forall {LB IB EB},
@@ -830,12 +702,10 @@ Lemma Advantage_common_par :
       ((AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= ν + ε)%R).
 Proof.
   intros.
-  rewrite (package_duplicate (K false)).
-  rewrite (package_duplicate (K true)).
-  erewrite <- !interchange_alt ; [ | try apply fsubmapxx .. ].
-  4,5,8,9: apply H4.
+  erewrite <- !interchange_alt.
+  4,7: apply H4.
   2,4: now eapply valid_package_inject_import ; [ | eapply H2 ].
-  2,3: now eapply valid_package_inject_import ; [ | eapply H3 ].
+  2,3: eapply H3.
   eapply order.Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
   apply Num.Theory.lerD.
   {
diff --git a/theories/Crypt/package/pkg_composition.v b/theories/Crypt/package/pkg_composition.v
index 399f21ef..f5182a82 100644
--- a/theories/Crypt/package/pkg_composition.v
+++ b/theories/Crypt/package/pkg_composition.v
@@ -458,15 +458,13 @@ Proof.
 Qed.
 
 Lemma interchange_alt :
-  ∀ A B C D E F L1 L2 L3 L4 p1 p2 p3 p4,
+  ∀ A B C D E L1 L2 L3 p1 p2 p3,
     ValidPackage L1 B A p1 →
     ValidPackage L2 E D p2 →
     ValidPackage L3 C B p3 →
-    ValidPackage L4 F E p4 →
-    (fsubmap p3 p4) ->
-    par (link p1 p3) (link p2 p4) = link (par p1 p2) (par p3 p4).
+    par (link p1 p3) (link p2 p3) = link (par p1 p2) p3.
 Proof.
-  intros A B C D E F L1 L2 L3 L4 p1 p2 p3 p4 h1 h2 h3 h4 s34.
+  intros A B C D E L1 L2 L3 p1 p2 p3 h1 h2 h3.
   apply eq_fmap => n.
   rewrite /par unionmE 3!mapmE unionmE.
   destruct (A n) as [[S T]|] eqn:e.
@@ -476,21 +474,7 @@ Proof.
     rewrite he1 in e.
     destruct e as [f e].
     rewrite e //=.
-    do 3 f_equal. extensionality x.
-    erewrite code_link_par_left => //.
-    2: apply h3.
-    apply (hi1 n (S; T; f) x), e.
   - move: e => /dommPn; rewrite valid_domm; move=> /dommPn -> //=.
-    destruct (D n) as [[S T]|] eqn:e'.
-    2: move: e' => /dommPn; rewrite valid_domm; move=> /dommPn -> //=.
-    destruct h2 as [he2 hi2].
-    specialize (he2 (n, (S, T))).
-    simpl in he2.
-    rewrite he2 in e'.
-    destruct e' as [f e'].
-    rewrite e' //=.
-    do 3 f_equal. extensionality x.
-    now rewrite s34.
 Qed.
 
 Local Open Scope type_scope.

From 1479074240a1890e48f70dacb93ad0b9b48c7b7b Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 16 Jun 2025 15:04:45 +0200
Subject: [PATCH 5/7] Fixes

---
 theories/Crypt/package/pkg_advantage.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index 1fbcc272..1a8d94d9 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -613,7 +613,7 @@ Proof.
 
       rewrite unionmC in H3.
       2:{
-        destruct H.
+        destruct H as [H].
         subst.
         rewrite !domm_map in H.
         apply H.
@@ -642,7 +642,7 @@ Lemma Advantage_split_par :
     (forall b, ValidPackage LA IA EA (A b)) ->
     (forall b, ValidPackage LB IB EB (B b)) ->
     (forall b, K b = par (B b) (C b)) ->
-    forall Adv, 
+    forall Adv,
     forall ε,
       ((AdvantageE (A false ∘ B false) (A true ∘ B true) Adv <= ε)%R) ->
       ((AdvantageE (A false ∘ K false) (A true ∘ K true) Adv <= ε)%R).
@@ -706,7 +706,7 @@ Proof.
   4,7: apply H4.
   2,4: now eapply valid_package_inject_import ; [ | eapply H2 ].
   2,3: eapply H3.
-  eapply order.Order.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
+  eapply order.Order.POrderTheory.le_trans ; [ eapply Advantage_triangle with (R := par (A false ∘ K false) (B true ∘ K true)) | ].
   apply Num.Theory.lerD.
   {
     erewrite Advantage_par.

From 1f67d41546a97d6d966cd10d9784c4fb00710781 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 16 Jun 2025 16:08:45 +0200
Subject: [PATCH 6/7] More fixes

---
 theories/Crypt/package/pkg_advantage.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index 1a8d94d9..a66dcde2 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -739,4 +739,7 @@ Corollary Advantage_common_par0 :
     ((AdvantageE (A false ∘ K false) (A true ∘ K true) (Adv ∘ par (ID EA) (B true ∘ K true)) <= 0)%R) ->
     ((AdvantageE (B false ∘ K false) (B true ∘ K true) (Adv ∘ par (A false ∘ K false) (ID EB)) <= 0)%R) ->
     ((AdvantageE (par (A false) (B false) ∘ K false) (par (A true) (B true) ∘ K true) Adv <= 0)%R).
-Proof. intros. rewrite <- (GRing.add0r 0%R). now rewrite Advantage_common_par. Qed.
+Proof. intros.
+  first [rewrite <- (GRing.add0r 0%R) | rewrite <- (GRing.add0r (@GRing.zero R))].
+  now rewrite Advantage_common_par.
+Qed.

From b1fbf291d161a61d9a413e6ec6745acdde8f6b0e Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Thu, 6 Nov 2025 16:35:12 +0100
Subject: [PATCH 7/7] Adapt to nominal changes

---
 theories/Crypt/package/pkg_advantage.v   | 11 +++++++++--
 theories/Crypt/package/pkg_composition.v |  4 ++--
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index a66dcde2..230ef3fc 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -297,6 +297,13 @@ Qed.
 Lemma par_emptyR : forall G, par G emptym = G.
 Proof. now setoid_rewrite unionm0. Qed.
 
+Lemma par_emptyR' : forall G, par G (ID emptym) = G.
+Proof.
+  cbn.
+  replace ((ID_raw emptym)) with (emptym : raw_package) by now apply eq_fmap.
+  now setoid_rewrite unionm0.
+Qed.
+
 Lemma Advantage_par_emptyR :
   ∀ G₀ G₁ A,
   AdvantageE (par G₀ emptym) (par G₁ emptym) A = AdvantageE G₀ G₁ A.
@@ -327,8 +334,8 @@ Proof.
     2: fmap_solve.
     rewrite link_id // id_link //.
   }
-  replace (ID Game_import) with (emptym : raw_package) by now apply eq_fmap.
-  rewrite -Advantage_link !Advantage_par_emptyR //.
+  rewrite -Advantage_link.
+  rewrite !par_emptyR' //.
 Qed.
 
 Lemma Advantage_sym :
diff --git a/theories/Crypt/package/pkg_composition.v b/theories/Crypt/package/pkg_composition.v
index f5182a82..7c39df55 100644
--- a/theories/Crypt/package/pkg_composition.v
+++ b/theories/Crypt/package/pkg_composition.v
@@ -390,7 +390,7 @@ Proof.
   erewrite code_link_par_left ; [ reflexivity |  | apply H1 ].
   eapply valid_injectMap.
   1: apply H.
-  apply (valid_imports LA IA EA A H0 n (S1; T1; f1) x).
+  apply (@valid_imports LA IA EA A H0 n (S1; T1; f1) x).
   apply e.
 Qed.
 
@@ -415,7 +415,7 @@ Proof.
   erewrite code_link_par_right ; [ reflexivity | assumption |  | apply H2 ].
   eapply valid_injectMap.
   1: apply H.
-  apply (valid_imports LA IA EA A H1 n (S1; T1; f1) x).
+  apply (@valid_imports LA IA EA A H1 n (S1; T1; f1) x).
   apply e.
 Qed.