diff --git a/_CoqProject b/_CoqProject index 1caabc13..303b43bd 100644 --- a/_CoqProject +++ b/_CoqProject @@ -94,5 +94,9 @@ toy_examples/expected_value_variance.v toy_examples/expected_value_variance_ordn.v toy_examples/expected_value_variance_tuple.v toy_examples/conditional_entropy.v +smc/smc_proba.v +smc/smc_entropy.v +smc/smc_interpreter.v +smc/smc_tactics.v -R . infotheo diff --git a/changelog.txt b/changelog.txt index c688fe5a..b927e215 100644 --- a/changelog.txt +++ b/changelog.txt @@ -27,6 +27,18 @@ from 0.6.0 to 0.6.1 compatibility release +------------------- +from 0.6.1 to 0.7.0 +------------------- + +Port to MathComp 2 + +------------------- +from 0.6.0 to 0.6.1 +------------------- + +compatibility release + ------------------- from 0.5.2 to 0.6.0 ------------------- diff --git a/information_theory/entropy.v b/information_theory/entropy.v index 78c6bfab..84b716fa 100644 --- a/information_theory/entropy.v +++ b/information_theory/entropy.v @@ -187,6 +187,25 @@ rewrite -(pair_bigA _ (fun a1 a2 => P (a1, a2) * log (P (a1, a2)))) /=. by rewrite exchange_big pair_big; apply eq_bigr => -[a b] _; rewrite fdistXE. Qed. +Variables (C: finType) (P' : {fdist A * B * C}). + +About fdistA. + +Lemma joint_entropyA : `H P' = `H (fdistA P'). +Proof. +congr (- _) => /=. +rewrite (eq_bigr (fun a => P' (a.1.1, a.1.2, a.2) * log (P' (a.1.1, a.1.2, a.2)))); last by case => -[]. +rewrite -(pair_bigA _ (fun a1 a2 => P' (a1.1, a1.2, a2) * log (P' (a1.1, a1.2, a2)))) /=. +rewrite -(pair_bigA _ (fun a1 a2 => \sum_j P' (a1, a2, j) * log (P' (a1, a2, j)))) /=. +rewrite [RHS](eq_bigr (fun a => fdistA P' (a.1, (a.2.1, a.2.2)) * log (fdistA P' (a.1, (a.2.1, a.2.2))))); last by case => i []. +rewrite -(pair_bigA _ (fun a1 a2 => fdistA P' (a1, (a2.1, a2.2)) * log (fdistA P' (a1, (a2.1, a2.2))))) /=. +apply: eq_bigr => i _. +rewrite -(pair_bigA _ (fun a1 a2 => fdistA P' (i, (a1, a2)) * log (fdistA P' (i, (a1, a2))))) /=. +apply: eq_bigr => j _. +apply: eq_bigr => k _. +rewrite fdistAE //. +Qed. + End joint_entropy. Lemma entropy_rV (A : finType) n (P : {fdist 'rV[A]_n.+1}) : diff --git a/probability/proba.v b/probability/proba.v index 70f9b18e..17b8e81a 100644 --- a/probability/proba.v +++ b/probability/proba.v @@ -514,7 +514,7 @@ Local Notation "{ 'RV' P -> V }" := (RV_of P (Phant _) (Phant V)). Definition ambient_dist (P : {fdist U}) (X : {RV P -> T}) : {fdist U} := P. End random_variable. -Notation "{ 'RV' P -> T }" := (RV_of P (Phant _) (Phant T)) : proba_scope. +Notation "{ 'RV' P -> T }" := (@RV _ T%type P ) : proba_scope. Section random_variable_eqType. Variables (U : finType) (A : eqType) (P : R.-fdist U). @@ -1822,6 +1822,16 @@ End conditionnally_independent_discrete_random_variables. Notation "P |= X _|_ Y | Z" := (@cinde_rv _ P _ _ _ X Y Z) : proba_scope. Notation "X _|_ Y | Z" := (cinde_rv X Y Z) : proba_scope. +Section conditionnally_independent_discrete_random_variables_extra. + +Variables (U: finType) (P : R.-fdist U) (A B C: finType). +Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}). + +Lemma cinde_rv_sym : X _|_ Y | Z -> Y _|_ X | Z. +Proof. move=>H a b c. by rewrite mulRC cpr_eq_pairC. Qed. + +End conditionnally_independent_discrete_random_variables_extra. + Section independent_rv. Variables (A : finType) (P : R.-fdist A) (TA TB : eqType). Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). @@ -2231,3 +2241,99 @@ rewrite big_ord_recr /=. Abort. End prob_chain_rule. + + + +Section more_rv_lemmas. +Variables (U : finType) (P : R.-fdist U). +Variables (TA TB TC UA UB UC : eqType) (f : TA -> UA) (g : TB -> UB) (h: TC -> UC). +Variables (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}). + +Local Notation "f × g" := + (fun xy => (f xy.1, g xy.2)) (at level 10). + +Lemma comp_RV2_ACA : RV2 (f `o X) (g `o Y) = f × g `o RV2 X Y. +Proof. by []. Qed. + +Lemma comp_RV3_ACA : [%h `o Z, [% (f `o X), (g `o Y)]] = h × (f × g) `o [%Z, [%X, Y]]. +Proof. by []. Qed. +End more_rv_lemmas. + +Section more_preimset. +Variables (aT1 aT2 aT3 rT1 rT2 rT3: finType). +Variables (f : aT1 -> rT1) (g : aT2 -> rT2) (h : aT3 -> rT3). +Variables (A : {set rT1}) (B : {set rT2}) (C : {set rT3}). + +Local Notation "f × g" := + (fun xy => (f xy.1, g xy.2)) (at level 10). + +Lemma preimsetX : + f × g @^-1: (A `* B) = f @^-1: A `* g @^-1: B. +Proof. by apply/setP=> -[] a b /=; rewrite !inE. Qed. + +Lemma preimsetX2 : + h × (f × g) @^-1: (C `* (A `* B)) = h @^-1: C `* (f @^-1: A `* g @^-1: B). +Proof. by apply/setP=> -[] a b /=; rewrite !inE. Qed. + +Lemma in_preimset x (Y : {set rT1}) : (x \in f @^-1: Y) = (f x \in Y). +Proof. by rewrite !inE. Qed. +Lemma in_preimset1 x y : (x \in f @^-1: [set y]) = (f x == y). +Proof. by rewrite !inE. Qed. +End more_preimset. + + +Section more_pr_lemmas. +Variables (U : finType) (P : R.-fdist U). +Variables (TA UA : finType) (f : TA -> UA) (X : {RV P -> TA}). + +Lemma pr_in_comp' E : + `Pr[ (f `o X) \in E ] = `Pr[ X \in f @^-1: E ]. +Proof. +rewrite !pr_inE' /Pr. +rewrite partition_big_preimset /=. +apply: eq_bigr=> i iE. +under [RHS]eq_bigr=> j ?. + rewrite fdistmapE -ssrR.sumRE. + under eq_bigl do rewrite /= inE /=. + over. +under eq_bigl do rewrite -in_preimset1. +rewrite -partition_big_preimset /= fdistmapE -ssrR.sumRE. +apply: eq_bigl=> j. +by rewrite !inE. +Qed. +End more_pr_lemmas. + + +Section more_fdist. +Lemma fdistmapE' (R : realType) (A B : finType) (g : A -> B) + (p : fdist R A) (b : B): + fdistmap g p b = (\sum_(a in g @^-1: [set b]) p a)%mcR. +Proof. by rewrite fdistmapE; apply: eq_bigl=> ?; rewrite !inE. Qed. +End more_fdist. + + +Section more_inde_rv. +Variables (A : finType) (P : R.-fdist A) (TA TB : finType). +Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). + +Definition inde_rv_ev := + forall E F, + `Pr[ [% X, Y] \in E `* F] = `Pr[ X \in E ] * `Pr[ Y \in F ]. + +Lemma inde_rv_events' : inde_rv X Y <-> inde_rv_ev. +Proof. +split=> H; last by move=> *; rewrite -!pr_eq_set1 -H setX1. +move=> E F; rewrite !pr_inE'. +rewrite [LHS]/Pr; under eq_bigr=> *. + rewrite fdistmapE. + under eq_bigl do rewrite !inE /=. + over. +rewrite [in RHS]/Pr big_distrl /=. +under [RHS]eq_bigr=> i ?. + rewrite big_distrr /=. + under eq_bigr do rewrite -!pr_eqE' -H pr_eqE'. + over. +rewrite -big_setX; apply: eq_bigr=> *. +by rewrite fdistmapE. +Qed. +End more_inde_rv. diff --git a/smc/smc_entropy.v b/smc/smc_entropy.v new file mode 100644 index 00000000..134e725f --- /dev/null +++ b/smc/smc_entropy.v @@ -0,0 +1,1420 @@ +From HB Require Import structures. +Require Import Reals. +From mathcomp Require Import all_ssreflect all_algebra fingroup finalg matrix. +From mathcomp Require Import Rstruct ring. +Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist. +Require Import proba jfdist_cond entropy graphoid smc_proba. + +Import GRing.Theory. +Import Num.Theory. + +(************************************************************************************) +(* SMC Proofs in entroy *) +(* *) +(* From: Information-theoretically Secure Number-product Protocol *) +(* SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine *) +(* Learning and Cybernetics. IEEE, 2007. p. 3006-3011. *) +(* *) +(* *) +(* | Definitions | | Meaning |*) +(* |-------------------|----|------------------------------------------------------|*) +(* | x \*d y | == | dot product of two random vectors. |*) +(* | scalar_product | == | The deterministic version of |*) +(* | | | SMC scalar product protocol as a function. |*) +(* | is_scalar_product | == | The correctness of the SMC scalar product results |*) +(* |-------------------------------------------------------------------------------|*) +(* *) +(* *) +(* Lemmas: *) +(* pi2_bob_is_leakage_free_proof == the proof shows that Bob's knowledge of *) +(* Alice's secret input x1 does not increase *) +(* by accessing random variables received *) +(* during the protocols execution *) +(* pi2_alice_is_leakage_free_proof == the proof shows that Alice's knowledge of *) +(* Bob's secret input x2 does not increase *) +(* by accessing random variables received *) +(* during the protocols execution *) +(* cpr_cond_entropy == given a conditional probability removal *) +(* lemma P( X | (Y, Z))->P( X | Y ), shows that*) +(* with some conditions met, there exists a *) +(* conditional entropy removal lemma *) +(* H( X | (Y, Z))->H( X | Y ) *) +(* *) +(************************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. + +Local Open Scope reals_ext_scope. +Local Open Scope proba_scope. +Local Open Scope fdist_scope. +Local Open Scope chap2_scope. +Local Open Scope entropy_scope. +Local Open Scope vec_ext_scope. + +Reserved Notation "u *d w" (at level 40). +Reserved Notation "u \*d w" (at level 40). + +Module smc_entropy_proofs. + +Section extra_ring. + +Variable V : zmodType. +Implicit Types x y : V. + +End extra_ring. + + +Section extra_pr. + +Variables (T TX TY: finType)(TX': finZmodType). +Variable P : R.-fdist T. +Variable n : nat. + +Lemma pr_eq_diag U (X : {RV P -> U}) (x : U) : + `Pr[ [% X, X] = (x, x) ] = `Pr[ X = x ]. +Proof. +by rewrite !pr_eqE /Pr; apply: eq_bigl=> a; rewrite !inE xpair_eqE andbb. +(* After unfolding Pr use eq_bigl to focus on the preim and pred, + use inE to keep only the pred and as booleaning expression, + use xpair_eqE to separate the RV2 to two conditions, + and show LHS and RHS will be only true. +*) +Qed. + +Lemma cpr_eq_id U (X : {RV P -> U}) (x : U) : + `Pr[ X = x ] != 0 -> `Pr[ X = x | X = x ] = 1. +Proof. by move=> ?; rewrite cpr_eqE pr_eq_diag divRR. Qed. + +End extra_pr. + +Section extra_pr2. + +Variables (T TX TY TZ: finType). +Variable P : R.-fdist T. + +Lemma fst_RV2_neq0 (X : {RV P -> TX}) (Y : {RV P -> TY}) x y: + `Pr[[%X, Y] = (x, y)] != 0 -> `Pr[ X = x] != 0. +Proof. +apply: contra => /eqP /pr_eq_domin_RV2 H. +by apply/eqP. +Qed. + +Lemma cpr_RV2_sym (X : {RV P -> TX}) (Y : {RV P -> TY}) (Z : {RV P -> TZ}) x y z: + `Pr[ X = x | [% Y, Z] = (y, z) ] = `Pr[ X = x | [% Z, Y] = (z, y) ]. +Proof. +rewrite !cpr_eqE. +rewrite !coqRE. +rewrite [X in (_ / X)]pr_eq_pairC. +congr (_/_). +rewrite pr_eq_pairC. +rewrite [RHS]pr_eq_pairC. +rewrite !pr_eqE. +congr (Pr P _). +apply/setP => t. +rewrite !inE. +rewrite !xpair_eqE. +by rewrite [X in X && _]Bool.andb_comm. +Qed. + +End extra_pr2. + +Section entropy_with_indeRV. + +Variables (T TX TY TZ: finType). +Variable P : R.-fdist T. + +Lemma inde_rv_alt (X : {RV P -> TX}) (Y : {RV P -> TY}): + inde_rv X Y <-> forall x y,`p_ [%X, Y] (x, y) = `p_ X x * `p_ Y y. +Proof. +rewrite /inde_rv. +split => H x y. +by rewrite -!pr_eqE'. +by rewrite !pr_eqE'. +Qed. + +Lemma joint_entropy_indeRV (X : {RV P -> TX}) (Y : {RV P -> TY}): + inde_rv X Y -> joint_entropy `p_[%X, Y] = `H (`p_X) + `H (`p_Y). +Proof. +rewrite /joint_entropy. +rewrite /entropy. +rewrite !coqRE. +transitivity (- (\sum_(a in TX) \sum_(b in TY) `p_ [% X, Y] (a, b) * log (`p_ X a * `p_ Y b))). + congr (- _). + rewrite pair_big /=. + apply eq_bigr => -[a b] _ /=. + congr (_ * log _). + rewrite coqRE. + by apply inde_rv_alt. (* cannot `apply: ` but can `apply `*) +transitivity ( + - (\sum_(a in TX) \sum_(b in TY) `p_ [%X, Y] (a, b) * log (`p_ X a)) + - (\sum_(a in TX) \sum_(b in TY) `p_ [%X, Y] (a, b) * log (`p_ Y b))). + rewrite -[RHS]oppRB. + congr (- _). + rewrite -addR_opp. + rewrite oppRK. + rewrite -big_split /=. (* merge two \sum_a...\sum_a in RHS so we can apply eq_bigr*) + apply eq_bigr => a _. + rewrite -big_split /=. + apply eq_bigr => b _. + have [->|H0] := eqVneq (`p_ [%X, Y](a, b)) 0. + rewrite !mul0r. + by rewrite add0R. + rewrite mulRC. + rewrite logM //. (* from log (x*y) to log x + log y *) + - by rewrite [LHS]mulRDr. + - rewrite -pr_eqE'. + rewrite pr_eqE Pr_gt0P -pr_eqE. + move: H0. + rewrite -pr_eqE' pr_eq_pairC coqRE. + exact: fst_RV2_neq0. + - rewrite -pr_eqE'. + rewrite pr_eqE Pr_gt0P -pr_eqE. + move: H0. + rewrite -pr_eqE' coqRE. + exact: fst_RV2_neq0. +(* From \sum_a \sum_b `p_ [%X, Y](a, b) to \sum_a `p_ X a*) +under eq_bigr do rewrite -big_distrl -fdist_fstE fst_RV2 /=. +congr (- _ - _). +rewrite exchange_big /=. +apply: eq_bigr => i _. +by rewrite -big_distrl -fdist_sndE snd_RV2 /=. +Qed. + +End entropy_with_indeRV. + + +Section joint_entropyA. + +Variables (A B C: finType) (P : {fdist A * B * C}). + +Lemma joint_entropyA : `H P = `H (fdistA P). +Proof. +congr (- _) => /=. +rewrite (eq_bigr (fun a => P (a.1.1, a.1.2, a.2) * log (P (a.1.1, a.1.2, a.2)))); last by case => -[]. +rewrite -(pair_bigA _ (fun a1 a2 => P (a1.1, a1.2, a2) * log (P (a1.1, a1.2, a2)))) /=. +rewrite -(pair_bigA _ (fun a1 a2 => \sum_j P (a1, a2, j) * log (P (a1, a2, j)))) /=. +rewrite [RHS](eq_bigr (fun a => fdistA P (a.1, (a.2.1, a.2.2)) * log (fdistA P (a.1, (a.2.1, a.2.2))))); last by case => i []. +rewrite -(pair_bigA _ (fun a1 a2 => fdistA P (a1, (a2.1, a2.2)) * log (fdistA P (a1, (a2.1, a2.2))))) /=. +apply: eq_bigr => i _. +rewrite -(pair_bigA _ (fun a1 a2 => fdistA P (i, (a1, a2)) * log (fdistA P (i, (a1, a2))))) /=. +apply: eq_bigr => j _. +apply: eq_bigr => k _. +rewrite fdistAE //. +Qed. + +End joint_entropyA. + +Section pr_entropy. + + +Variables (T TY1 TY2: finType) (TY3: finZmodType) (P : R.-fdist T). +Variable n : nat. +Notation p := n.+2. +Variables (Y1: {RV P -> TY1}) (Y2: {RV P -> TY2}) (Y3: {RV P -> TY3}). + +Hypothesis card_Y3 : #|TY3| = n.+1. +Hypothesis pY3_unif : `p_ Y3 = fdist_uniform card_Y3. +Hypothesis Y2Y3indep : P|= Y2 _|_ Y3. + +Lemma cpr_cond_entropy1_RV y2 y3: + (forall y1 , + `Pr[ Y1 = y1 | Y2 = y2 ] = `Pr[ Y1 = y1 | [%Y2, Y3] = (y2, y3) ]) -> + cond_entropy1_RV Y2 Y1 y2 = cond_entropy1_RV [% Y2, Y3] Y1 (y2, y3). +Proof. +move => H. +case /boolP : ((`p_ [% Y2, Y1])`1 y2 == 0) => Hy2. + rewrite /cond_entropy1_RV. + rewrite /entropy. + congr -%R. + apply:eq_bigr => a _. + (*rewrite jfdist_condE. -- it brings `(fdistmap [% Y2, Y3, Y3] P)`1 (v1, v2) != 0%coqR` so we cannot use it*) + rewrite /jfdist_cond. + have Hy3: ((`p_ [% Y2, Y3, Y1])`1 (y2, y3) == 0). + rewrite fst_RV2. + apply/eqP. + move:(@Pr_domin_setX TY2 TY3 (`p_ [%Y2, Y3]) [set y2] [set y3]). + rewrite !Pr_set1. + rewrite setX1. + rewrite !Pr_set1. + rewrite fst_RV2. + apply. + rewrite fst_RV2 in Hy2. + exact/eqP. + destruct (boolP _). + exfalso. + by rewrite Hy2 in i. + destruct (boolP _). + exfalso. + by rewrite Hy3 in i0. + by rewrite !fdist_uniformE. + +rewrite cond_entropy1_RVE //. +rewrite cond_entropy1_RVE; last first. + rewrite fst_RV2. + rewrite fst_RV2 in Hy2. + rewrite -pr_eqE'. + rewrite Y2Y3indep. + rewrite !pr_eqE'. + rewrite mulR_neq0'. + rewrite Hy2 /=. + rewrite pY3_unif. + rewrite fdist_uniformE /=. + rewrite card_Y3. + rewrite invr_eq0. + by rewrite pnatr_eq0. + +rewrite /cond_entropy1. +rewrite /entropy. +congr -%R. +apply:eq_bigr => a _. +have -> // : \Pr_`p_ [% Y1, Y2][[set a] | [set y2]] = \Pr_`p_ [% Y1, [%Y2, Y3]][[set a] | [set (y2, y3)]]. +rewrite !jPr_Pr. +by rewrite !cpr_eq_set1. +Qed. + +Hypothesis Hy2y3 : forall y1 y2 y3, `Pr[[%Y2, Y3] = (y2, y3)] != 0 -> + `Pr[ Y1 = y1 | [%Y2, Y3] = (y2, y3) ] = `Pr[ Y1 = y1 | Y2 = y2 ]. + +Lemma Pr_neq0_cond_removal : forall y1 y2 y3, `Pr[Y3 = y3] != 0 -> + `Pr[ Y1 = y1 | [%Y2, Y3] = (y2, y3) ] = `Pr[ Y1 = y1 | Y2 = y2 ]. +Proof. +move => y1 y2 y3 Hy3neq0. +have [Hy2|Hy2] := eqVneq `Pr[Y2 = y2] 0. + rewrite !cpr_eqE Y2Y3indep. + by rewrite Hy2 mul0R !Rdiv_0_r. +apply: Hy2y3. +by rewrite Y2Y3indep mulf_eq0 negb_or Hy2. +Qed. + +Lemma snd_extra_indep y2 y3 : + (`p_ [% Y1, [% Y2, Y3]])`2 (y2, y3) = (`p_ [% Y1, Y2])`2 y2 * `p_Y3 y3. +Proof. +rewrite !fdist_sndE big_distrl /=. +apply eq_bigr => y1 _. +have [Hy3|Hy3] := eqVneq `Pr[Y3 = y3] 0. + rewrite -!pr_eqE' Hy3 mulr0 pr_eq_pairC pr_eq_domin_RV2 //. + by rewrite pr_eq_pairC pr_eq_domin_RV2. +have := Pr_neq0_cond_removal y1 y2 Hy3. +rewrite !cpr_eqE Y2Y3indep -!pr_eqE' !coqRE. +have [Hy2 _|Hy2] := eqVneq `Pr[Y2 = y2] 0. + rewrite [in RHS]pr_eq_pairC [in LHS]pr_eq_pairC -pr_eq_pairA. + by rewrite !(pr_eq_domin_RV2 _ _ Hy2) mul0r. +move/(f_equal (fun x => x * (`Pr[Y2 = y2] * `Pr[Y3 = y3]))). +rewrite -[in LHS]mulrA mulVf //; last by rewrite mulf_eq0 negb_or Hy2. +rewrite mulrA -(mulrA _ _^-1). (* Coq identify the A / B is ^-1.*) +by rewrite mulVf // !mulr1. +Qed. + +End pr_entropy. + +Section cpr_cond_entropy_proof. + +Variables (T TY1 TY2 : finType)(TY3 : finZmodType)(P : R.-fdist T). +Variables (Y1 : {RV (P) -> (TY1)})(Y2 : {RV (P) -> (TY2)})(Y3 : {RV (P) -> (TY3)}). + +Lemma cpr_cond_entropy (n: nat)(card_TY3 : #|TY3| = n.+1): + `p_ Y3 = fdist_uniform card_TY3 -> + P |= Y2 _|_ Y3 -> + (forall (y1 : TY1) (y2 : TY2) (y3 : TY3), + `Pr[ [% Y2, Y3] = (y2, y3) ] != 0 -> + `Pr[ Y1 = y1 | [% Y2, Y3] = (y2, y3) ] = + `Pr[ Y1 = y1 | Y2 = y2 ] + ) -> + `H( Y1 | [% Y2, Y3]) = `H( Y1 | Y2). +Proof. +move => Hunif Hinde Hremoval. +rewrite /cond_entropy /=. +under eq_bigl do rewrite inE /=. +set f : TY2 -> TY3 -> R := fun y2 y3 => + (`p_[% Y1, Y2])`2 y2 * `p_Y3 y3 * cond_entropy1 `p_ [% Y1, Y2] y2. +transitivity (\sum_a f a.1 a.2). + apply eq_bigr => a _. + rewrite /f {1 2}(surjective_pairing a) /=. + have [Ha|Ha] := eqVneq ((`p_ [% Y1, Y2])`2 a.1 * `p_Y3 a.2) 0. + by rewrite Ha snd_extra_indep // Ha !coqRE !mul0r. + rewrite snd_extra_indep // -[in LHS]cond_entropy1_RVE; last first. + by rewrite -fdistX2 fdistX_RV2 snd_extra_indep. + have [Hy3|Hy3] := eqVneq `Pr[Y3 = a.2] 0. + rewrite -pr_eqE' in Ha. + by rewrite Hy3 mulr0 eqxx in Ha. + have H' := fun w => Pr_neq0_cond_removal Hinde Hremoval w a.1 Hy3. + rewrite -(cpr_cond_entropy1_RV Hunif Hinde) //. + rewrite cond_entropy1_RVE ?coqRE //. + by apply: contra Ha; rewrite mulf_eq0 -fdistX1 fdistX_RV2 => ->. +rewrite -pair_bigA /=. +apply: eq_bigr => y2 _. +by rewrite /f -big_distrl -big_distrr /= FDist.f1 mulr1 coqRE. +Qed. + + +End cpr_cond_entropy_proof. + +Section lemma_3_8_prep. + +Variables (T TX TY TZ: finType). +Variable P : R.-fdist T. +Variables (X : {RV P -> TX}) (Y : {RV P -> TY}) (f : TY -> TZ). +Let Z := f `o Y. + +Section lemma_3_8_proof. +Variables (y : TY) (z : TZ). + +Lemma pr_eq_ZY_Y : + `Pr[ [% Z, Y] = (f y, y) ] = `Pr[ Y = y ]. +Proof. +rewrite !pr_eqE. +congr (Pr P _). +apply/setP => t. +rewrite !inE. +rewrite xpair_eqE. +apply andb_idl => /eqP <- //. +Qed. + +Hypothesis pr_Y_neq0 : `Pr[ Y = y ] != 0. +(* TODO tried to define it as `Pr[ Y = y ] > 0 and then use `Rlt_not_eq` in the proof, + but this hypothesis would be wrapped by `is_true` that `Rlt_not_eq` cannot be applied directly. +*) + +(* H(f(Y)|X,Y) = H(f(Y)|Y) = 0 *) +(* Meaning: f(Y) is completely determined by Y. + (Because `f` only has one input which is Y). + + And because it is completely determined by Y, + `(X, Y)` won't increase the uncertanty. +*) +(* + Search (`Pr[ _ = _ ])(`p_ _ _). +*) +Lemma fun_cond_entropy_eq0_RV : + cond_entropy1_RV Y Z y = 0. +Proof. +(* If `Pr[Y = y] = 0, it makes the \Pr_QP[[set b] | [set a]] zero because the condition will be never true; need to do this before the cond_entropy1RVE *) +(* +have [H|] := eqVneq (`Pr[ Y = y]) 0. + rewrite /cond_entropy1_RV. + rewrite /entropy. + under eq_bigr => a _ . + rewrite (_ : jfdist_cond _ _ _ = 0). + rewrite mul0R. + over. + rewrite /jfdist_cond. +*) +rewrite cond_entropy1_RVE; last by rewrite fst_RV2 -pr_eqE'. +rewrite /cond_entropy1. +rewrite big1 -1?oppr0 // => i _. +have [<-|] := eqVneq (f y) i. + set pZY := (X in (X * log X)%coqR). + have HpZY: pZY = 1. + rewrite /pZY. + rewrite jPr_Pr. + rewrite cpr_eq_set1. + rewrite cpr_eqE. + rewrite coqRE. + rewrite pr_eq_ZY_Y //=. + by rewrite divff //=. + rewrite HpZY. + rewrite log1. + by rewrite mulR0. +move => Hfy_neq_i. +rewrite jPr_Pr. +rewrite cpr_eq_set1. +rewrite /Z. +(* Try to state that because `f y != i`, `Pr[ (f `o Y) = i | Y = y ] = 0 *) +have ->: `Pr[ (f `o Y) = i | Y = y ] = 0. + rewrite cpr_eqE. + rewrite pr_eqE. + rewrite (_: finset _ = set0). + by rewrite Pr_set0 div0R. + apply/setP => t. + rewrite !inE. + rewrite xpair_eqE. + rewrite /comp_RV. + apply/negbTE /negP => /andP [] /[swap] /eqP ->. + by apply/negP. +by rewrite mul0R. +Qed. + +End lemma_3_8_proof. + +Lemma fun_cond_entropy_ZY_eq0: + `H( Z | Y) = 0. +Proof. +rewrite /cond_entropy. +rewrite big1 // => i _. +rewrite snd_RV2. +have [->|Hi] := eqVneq (`p_ Y i) 0. + by rewrite mul0R. +rewrite -cond_entropy1_RVE ?fst_RV2 //. +by rewrite fun_cond_entropy_eq0_RV ?mulR0 // pr_eqE'. +Qed. + +End lemma_3_8_prep. + +Section fun_cond_entropy_proof. + +Variables (T TX TY TZ: finType). +Variable P : R.-fdist T. +Variables (X : {RV P -> TX}) (Y : {RV P -> TY}) (f : TY -> TZ). +Let Z := f `o Y. + +Local Open Scope ring_scope. +Variable (P': R.-fdist (TX * TY * TZ)). + +Lemma fun_cond_removal : + `H(X|[% Y, Z]) = `H(X| Y ). +Proof. +transitivity (joint_entropy `p_[%Y, Z, X] - entropy `p_[%Y, Z]). (* joint PQ = H P + cond QP*) + apply/eqP. + rewrite eq_sym. + rewrite subr_eq. + rewrite addrC. + apply/eqP. + have -> // : `p_[%X, [%Y, Z]] = fdistX `p_[%[%Y, Z], X]. + by rewrite fdistX_RV2. + have -> // : `p_[%Y, Z] = (`p_ [%[%Y, Z], X])`1. + by rewrite fst_RV2. + rewrite -coqRE. + by rewrite -chain_rule. +transitivity (joint_entropy `p_[%[%X, Y], Z] - entropy `p_[%Y, Z]). (* H(Y,f(Y),X) -> H(X,Y,f(Y))*) + rewrite joint_entropyC. + rewrite /joint_entropy. + rewrite joint_entropyA. + by rewrite fdistX_RV2 fdistA_RV3 . +transitivity (joint_entropy `p_[%X,Y] + cond_entropy `p_[%Z, [%X, Y]] - entropy `p_Y - cond_entropy `p_[%Z, Y]). + rewrite [in LHS]chain_rule. + rewrite !coqRE. + rewrite fdistX_RV2. + rewrite fst_RV2. + rewrite -![in RHS]addrA. + rewrite [RHS]addrCA. + rewrite [RHS]addrC. + rewrite [LHS]addrAC. + congr (_ + _ + _). + rewrite -opprD. + congr (-_). + have -> // : `p_[%Z, Y] = fdistX `p_[%Y, Z]. + by rewrite fdistX_RV2. + have -> // : `p_Y = (`p_[%Y, Z])`1. + by rewrite fst_RV2. + exact:chain_rule. +transitivity (joint_entropy `p_[%X, Y] - entropy `p_Y). + rewrite [LHS]addrAC. + have -> // : cond_entropy `p_[%Z, Y] = 0. + exact:fun_cond_entropy_ZY_eq0. + have -> // : cond_entropy `p_[%Z, [%X, Y]] = 0. + rewrite /Z. + have -> // : f `o Y = (f \o snd) `o [%X, Y]. + by apply/boolp.funext => x //=. + exact:fun_cond_entropy_ZY_eq0. + by rewrite addrK. +rewrite joint_entropyC fdistX_RV2. +rewrite -/(joint_entropy `p_ [%Y, X]). +rewrite chain_rule coqRE. +rewrite fst_RV2 fdistX_RV2. +rewrite addrAC. +by rewrite subrr add0r. +Qed. + +End fun_cond_entropy_proof. + +Section cinde_rv_comp_removal. + +Variables (T: finType)(TX TY TZ TO: finType)(x: TX)(y: TY)(z: TZ). +Variables (P: R.-fdist T)(X: {RV P -> TX})(Y: {RV P -> TY})(Z: {RV P -> TZ})(O: {RV P -> TO}). +Variables (fy: TO -> TY)(fz: TO -> TZ). + +Hypothesis XYZ_cinde: X _|_ (fy `o O) | (fz `o O). +Hypothesis YZneq0: `Pr[ [% fy `o O, fz `o O] = (y, z) ] != 0. + +Lemma cinde_rv_comp_removal: + `Pr[ X = x | (fz `o O) = z ] = `Pr[ X = x | [% fy `o O, fz `o O ] = (y, z) ]. +Proof. +have H:=cinde_alt x (b:=y) (c:=z) XYZ_cinde YZneq0. +symmetry in H. +apply H. +Qed. + +End cinde_rv_comp_removal. + +Section inde_ex. + +Variables (A: finType)(m n: nat)(P : R.-fdist A). +Variables (TX1 TX2 TX3 : finType). +Variables (s1 : {RV P -> TX1}) (s2 : {RV P -> TX2}) (r: {RV P -> TX3}). +Variable (op: TX1 -> TX2 -> TX3). + +Let rv_op (rv1:{RV P -> TX1})(rv2:{RV P -> TX2}) : {RV P -> TX3} := + fun p => op (rv1 p)(rv2 p). + +Hypothesis s1_s2_indep : P|= s1 _|_ s2. +Hypothesis s1s2_r_indep : P|= [%s1, s2] _|_ r. + +Lemma pr_eqM x : `Pr[ (rv_op s1 s2) = x ] = \sum_(a<-fin_img s1) (\sum_(b<-fin_img s2|op a b == x) `Pr[ s1 = a ] * `Pr[ s2 = b]). +Proof. +rewrite -[LHS]pr_eq_set1. +rewrite (reasoning_by_cases _ s1). +apply eq_bigr => a _. +rewrite (reasoning_by_cases _ s2). +rewrite [RHS]big_mkcond /=. +apply eq_bigr => b _. +case: ifPn. + move/eqP => <-. + rewrite -coqRE. + rewrite -s1_s2_indep. + rewrite setX1 setX1. + rewrite pr_eq_set1. + pose f (p:TX1 * TX2) := (op p.1 p.2, p.1, p.2). + have f_inj : injective f. + by move => [x1 x2] [? ?] [] _ -> -> /=. + by rewrite (pr_eq_comp _ _ f_inj ). +move => Hneq. +rewrite setX1 setX1. +rewrite pr_eq_set1. +rewrite pr_eqE. +apply/Pr_set0P. +move => a'. +rewrite !inE /=. +move/eqP => []. +move => Heq1 Heq2 Heq3. +by rewrite -Heq3 -Heq2 -Heq1 eqxx in Hneq. +Qed. + +Lemma pr_eqM2 x y : `Pr[ [%(rv_op s1 s2), r] = (x, y) ] = \sum_(a<-fin_img s1) (\sum_(b<-fin_img s2|op a b == x) `Pr[ s1 = a ] * `Pr[ s2 = b ] * `Pr[ r = y ]). +Proof. +rewrite -[LHS]pr_eq_set1. +rewrite (reasoning_by_cases _ s1). +apply eq_bigr => a _. +rewrite (reasoning_by_cases _ s2). +rewrite [RHS]big_mkcond /=. +apply eq_bigr => b _. +case: ifPn. + move/eqP => <-. + rewrite -coqRE. + rewrite -coqRE. + rewrite -s1_s2_indep -s1s2_r_indep. + rewrite setX1 setX1. + rewrite pr_eq_set1. + pose f (p:TX1 * TX2 * TX3) := (op p.1.1 p.1.2, p.2, p.1.1, p.1.2). + have f_inj : injective f. + by move => [[x1 x2] ?] [[? ?] ?] [] _ -> -> -> /=. + by rewrite (pr_eq_comp _ _ f_inj ). +move => Hneq. +rewrite setX1 setX1. +rewrite pr_eq_set1. +rewrite pr_eqE. +apply/Pr_set0P. +move => a'. +rewrite !inE /=. +move/eqP => []. +move => Heq1 _ Heq2 Heq3. +by rewrite -Heq3 -Heq2 -Heq1 eqxx in Hneq. +Qed. + +Lemma s1Ms2_r_indep : P|= (rv_op s1 s2) _|_ r. +Proof. +rewrite /inde_rv. +move => x y. +rewrite pr_eqM pr_eqM2. +rewrite big_distrl /=. +apply eq_bigr => a _. +rewrite big_distrl /=. +apply eq_bigr => b _. +by rewrite coqRE. +Qed. + +(* TODO: addition lemma; actually we didn't use anything about mul above (any binop works) *) +(* reasoning_by_cases depends on another lemma that is not general before (2024/12/05) -- these proof are not trivial actually. *) + +End inde_ex. + +Arguments s1Ms2_r_indep [_ _ _ _ _] s1 s2 r. + + +Section neg_RV_lemmas. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX : #|TX| = m.+2. + +Lemma sub_RV_eq (U : finZmodType) (X Y : {RV P -> U}): + X \- Y = X \+ neg_RV Y. +Proof. +apply: boolp.funext=> i. +rewrite /neg_RV . +rewrite /=. (* from null_fun to 0 *) +by rewrite sub0r. +Qed. + +Lemma neg_RV_dist_eq (X : {RV P -> TX}): + `p_ X = fdist_uniform card_TX -> + `p_ X = `p_ (neg_RV X). +Proof. +rewrite /dist_of_RV=> Hunif. +apply/val_inj/ffunP => x /=. (* these two steps eq to apply: fdist_ext.*) +rewrite [RHS](_: _ = fdistmap X P (-x)). + by rewrite !Hunif !fdist_uniformE. +rewrite /fdistmap !fdistbindE. +apply: eq_bigr=> a ?. +by rewrite /neg_RV !fdist1E /= sub0r eqr_oppLR. +Qed. + +Lemma neg_RV_inde_eq (U : finType)(V : finZmodType)(X : {RV P -> U})(Y : {RV P -> V}): + P |= X _|_ Y -> + P |= X _|_ neg_RV Y. +Proof. +move => H. +have ->: X = idfun `o X by []. +have ->: neg_RV Y = (fun y: V => 0 - y ) `o Y. + exact: boolp.funext => ? //=. +apply: inde_rv_comp. +exact: H. +Qed. + +End neg_RV_lemmas. + +Section dotproduct. + +Variable TX : ringType. +Variable n : nat. +Variable T : finType. + +Definition dotproduct (a b:'rV[TX]_n) := (a *m b^T)``_ord0. + +Definition dotproduct_rv (P: R.-fdist T) (A B: {RV P -> 'rV[TX]_n}) : {RV P -> TX} := + fun p => dotproduct (A p) (B p). + +End dotproduct. + +Notation "u *d w" := (dotproduct u w). +Notation "u \*d w" := (dotproduct_rv u w). + +Arguments dotproduct {TX n}. + +Section unif_lemmas. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Variables (s1 s2: {RV P -> 'rV[TX]_n})(r: {RV P -> TX}). +Hypothesis card_TX : #|TX| = m.+2. +Hypothesis pr_unif: `p_ r = fdist_uniform card_TX. +Hypothesis s1_s2_indep : P|= s1 _|_ s2. +Hypothesis s1s2_r_indep : P|= [%s1, s2] _|_ r. + +Lemma ps1_dot_s2_r_unif: + @dist_of_RV T P TX (s1 \*d s2 \- r) = fdist_uniform card_TX. +Proof. +have ->: s1 \*d s2 \- r = s1 \*d s2 \+ (neg_RV r). + by apply: boolp.funext=> ?; rewrite /neg_RV /= sub0r. +have Hnegr1unif: `p_ (neg_RV r) = fdist_uniform card_TX. + have Ha := neg_RV_dist_eq pr_unif. + symmetry in Ha. + rewrite Ha. + by rewrite pr_unif. +apply: add_RV_unif; first by rewrite -neg_RV_dist_eq. +apply: s1Ms2_r_indep; first by []. +exact: neg_RV_inde_eq. +Qed. + +End unif_lemmas. + +Section pi2. + + +Section scalar_product_def. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. + +Definition SMC := 'rV[TX]_n -> 'rV[TX]_n -> (TX * TX). + +Definition is_scalar_product (sp: SMC) := + forall (xa xb: 'rV[TX]_n), + (sp xa xb).1 + (sp xa xb).2 = xa *d xb. + +Definition step_eqn2_ya : ('rV[TX]_n * 'rV[TX]_n * TX * 'rV[TX]_n * TX) -> TX := fun z => + let '(xa, sa, ra, xb', t) := z in t - (xb' *d sa) + ra. + +Definition step_eqn3_t_with_offset : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> TX := fun z => + let '(xa, xb, sa, sb, ra, rb) := z in (xa + sa) *d xb + rb. + +Definition scalar_product (sa sb: 'rV[TX]_n)(ra yb: TX)(xa xb: 'rV[TX]_n): (TX * TX) := + let xa' := xa + sa in (* Alice -> Bob *) + let xb' := xb + sb in (* Bob -> Alice *) + let rb := sa *d sb - ra in (* Commodity -> Bob *) + let t_with_offset := step_eqn3_t_with_offset (xa, xb, sa, sb, ra, rb) in + let t := t_with_offset - yb in (* Bob -> Alice *) + let ya := step_eqn2_ya (xa, sa, ra, xb', t) in + (ya, yb). + +Lemma dot_productC (aa bb : 'rV[TX]_n) : aa *d bb = bb *d aa. +Proof. +rewrite /dotproduct. +rewrite !mxE. +apply: eq_bigr=> *. +by rewrite !mxE mulrC. +Qed. + +Lemma dot_productDr (aa bb cc : 'rV[TX]_n) : + aa *d (bb + cc) = aa *d bb + aa *d cc. +Proof. +rewrite /dotproduct !mxE. +rewrite -big_split /=. +apply: eq_bigr=> *. +by rewrite !mxE mulrDr. +Qed. + +(* xb *d (xa + sa) + (sa *d sb - ra) - yb - (xb + sb) *d sa + ra + yb = xa *d xb *) +Lemma scalar_product_correct (sa sb: 'rV[TX]_n)(ra yb: TX) : + is_scalar_product (scalar_product sa sb ra yb). +Proof. +move=>/=xa xb/=. +rewrite (dot_productC (xa+sa) xb). +rewrite !dot_productDr. +rewrite dot_productC. +rewrite (dot_productC xb sa). +rewrite (dot_productC (xb+sb) sa). +rewrite dot_productDr. +ring. +Qed. +(*rewrite (@GRing.add R).[AC(2*2)(1*4*(3*2))].*) + +End scalar_product_def. + +Section eqn2_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Variables (r1 r2 y2: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let x2' := x2 \+ s2. +Let t := x1' \*d x2 \+ r2 \- y2. +Let y1 := t \- x2' \*d s1 \+ r1. +Hypothesis card_TX : #|TX| = m.+2. + +Let f: ('rV[TX]_n * 'rV[TX]_n * TX * 'rV[TX]_n * TX) -> TX := fun z => + let '(xa, sa, ra, xb', t) := z in t - (xb' *d sa) + ra. + +Let y1_fcomp : + y1 = f `o [%x1, s1, r1, x2', t]. +Proof. by apply boolp.funext. Qed. + +Lemma eqn2_proof: + `H(x2|[%[%x1, s1, r1, x2', t], y1]) = `H(x2|[%x1, s1, r1, x2', t]). +Proof. rewrite y1_fcomp. exact: fun_cond_removal. Qed. + +End eqn2_proof. + +Section eqn3_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. + +Variables (r1 r2 y2: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let x2' := x2 \+ s2. +Let t := x1' \*d x2 \+ r2 \- y2. +Let y1 := t \- x2' \*d s1 \+ r1. + +(* Selected variables from scalar-product only for eqn3. + Each equation has a such "focus" from all variables in the scalar-product. +*) +Let O := [%x1, x2, s1, s2, r1, r2]. + +(* f1 `o X in mc_removal_pr must be x2 in eq3 *) +Let f1 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> 'rV[TX]_n := fun z => + let '(x1, x2, s1, s2, r1, r2) := z in x2. + +(* f2 `o X in mc_removal_pr must be (x1, s1, r1, x2 + s2) in eq3 *) +Let f2 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> ('rV[TX]_n * 'rV[TX]_n * TX * 'rV[TX]_n) := fun z => + let '(x1, x2, s1, s2, r1, r2) := z in (x1, s1, r1, x2 + s2). + +Definition fm : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> TX := fun z => + let '(xa, xb, sa, sb, ra, rb) := z in (xa + sa) *d xb + rb. + +(* in mc_removal_pr they are named as Y1 Y2 Ym but we already have Y so renaming them. *) +Let Z := neg_RV y2. +Let W1 := f1 `o O. (* x2; It is okay in Alice's view has it because only used in condition. *) +Let W2 := f2 `o O. (* [%x1, s1, r1, x2']; cannot have x2, s2, r2 here otherwise Alice knows the secret*) +Let Wm := fm `o O. (* t-(neg_RV y2); t before it addes (neg_RV y2) in WmZ*) +Let WmZ := Wm `+ neg_RV y2. (* t *) + +Let eq_W1_RV: + f1 `o O = x2. +Proof. by apply boolp.funext. Qed. + +Let eq_W2_RV: + f2 `o O = [%x1, s1, r1, x2']. +Proof. by apply boolp.funext. Qed. + +Let eq_Wm_RV: + fm `o O = (x1 \+ s1) \*d x2 \+ r2. +Proof. by apply boolp.funext => a . Qed. + +Let eq_WmZ_RV: + fm `o O `+ (neg_RV y2) = t. +Proof. +rewrite /t /add_RV /neg_RV eq_Wm_RV /x1' /=. +apply boolp.funext => a /=. +rewrite sub0r. +by []. +Qed. + +(* Because y2 is generated by Bob -- not related to any other variables. *) +Hypothesis Z_O_indep : inde_rv Z O. +Hypothesis pZ_unif : `p_ Z = fdist_uniform card_TX. (* Assumption in the paper. *) + +Let Z_OO_indep: + P |= Z _|_ [% O, O]. +Proof. +have ->: [%O, O] = (fun o => (o, o)) `o O by []. +have ->: Z = idfun `o Z by []. +exact: inde_rv_comp. +Qed. + +Let Z_WmW2_indep: + P |= Z _|_ [%Wm, W2]. +Proof. +rewrite /Wm /W2. +rewrite (_:Z = idfun `o Z) //. +apply: inde_RV2_comp. +exact: Z_OO_indep. +Qed. + +Let Z_W2_indep: + P |= Z _|_ W2. +Proof. +rewrite (_:Z = idfun `o Z) //. +apply: inde_rv_comp. +by exact: Z_O_indep. +Qed. + +Let Z_Wm_indep: + P |= Z _|_ Wm. +Proof. +rewrite /Wm. +rewrite (_:Z = idfun `o Z) //. +apply: inde_rv_comp. +by exact: Z_O_indep. +Qed. + +Let W2_WmZ_indep : + P |= W2 _|_ WmZ. +Proof. +rewrite cinde_rv_unit. +apply:cinde_rv_sym. +rewrite -cinde_rv_unit. +rewrite /inde_rv. +rewrite /WmZ. +move => x y. +have H := lemma_3_5' pZ_unif Z_WmW2_indep x y. +apply H. +Qed. + +Let pWmZ_unif: + `p_ (Wm `+ neg_RV y2) = fdist_uniform card_TX. +Proof. +have H_ZWM := Z_Wm_indep. +rewrite inde_rv_sym in H_ZWM. +have H := add_RV_unif Wm Z card_TX pZ_unif H_ZWM. +by exact H. +Qed. + + +Lemma eqn3_proof: + `H(x2|[%x1, s1, r1, x2', t]) = `H(x2|[%x1, s1, r1, x2']). +Proof. +rewrite -eq_W1_RV -eq_W2_RV -eq_WmZ_RV eq_Wm_RV. +have Ha := cpr_cond_entropy pWmZ_unif W2_WmZ_indep. +apply Ha => w w2 wmz Hneq0. +by have := mc_removal_pr f1 Z_O_indep pZ_unif w Hneq0. +Qed. + +End eqn3_proof. + +Section eqn4_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. +Hypothesis card_rVTX : #|'rV[TX]_n| = (m.+2 ^ n)%nat.-1.+1. +(* Coq cannot unify `(m.+2^n)%nat.-1.+1` in the definition of fdist_uniform and `(m.+2^n)%nat`, + so we cannot assume `(m.+2^n)%nat` here. + + Check fdist_uniform (n:=(m.+2^n)%nat.-1) card_rVTX. +*) + +Variables (r1: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x2' := x2 \+ s2. + +Let eqn4 := `H(x2|[%x1, s1, r1, x2']) = `H(x2|[%x1, s1, r1]). + +Let O := [%x1, s1, r1, x2]. +Let Z := s2. +Hypothesis pZ_unif : `p_ Z = fdist_uniform card_rVTX. (* Assumption in the paper. *) + +Let W1 := snd `o O. (* x2 *) +Let W2 := fst `o O. (* [%x1, s1, r1] *) +Let Wm := snd `o O. (* x2 *) +Let WmZ := Wm `+ s2. (* x2' = x2 + s2 *) + +Variable Z_O_indep : inde_rv Z O. + +Let Z_OO_indep: + P |= Z _|_ [% O, O]. +Proof. +have ->: [%O, O] = (fun o => (o, o)) `o O by []. +have ->: Z = idfun `o Z by []. +exact: inde_rv_comp. +Qed. + +Let Z_WmW2_indep: + P |= Z _|_ [%Wm, W2]. +Proof. +rewrite /Wm /W2. +rewrite (_:Z = idfun `o Z) //. +apply: inde_RV2_comp. +exact: Z_OO_indep. +Qed. + +Let Z_Wm_indep: + P |= Z _|_ Wm. +Proof. +rewrite /Wm. +rewrite (_:Z = idfun `o Z) //. (* id vs. idfun*) +apply: inde_rv_comp. +by exact: Z_O_indep. +Qed. + +Let pWmZ_unif: + (@dist_of_RV T P 'rV[TX]_n WmZ) = fdist_uniform card_rVTX. +Proof. +rewrite /WmZ. +have H_ZWM := Z_Wm_indep. +rewrite inde_rv_sym in H_ZWM. +have H := add_RV_unif Wm Z card_rVTX pZ_unif H_ZWM. +by exact H. +Qed. + +Let W2_WmZ_indep : + P |= W2 _|_ WmZ. +Proof. +rewrite cinde_rv_unit. +apply:cinde_rv_sym. +rewrite -cinde_rv_unit. +rewrite /inde_rv. +rewrite /WmZ. +move => x y. +have H := (@lemma_3_5' _ _ 'rV[TX]_n P (m.+2 ^ n)%nat.-1 Wm Z W2 card_rVTX pZ_unif Z_WmW2_indep x y). +apply H. +Qed. + +Lemma eqn4_proof: eqn4. +Proof. +rewrite /eqn4. +have Ha := cpr_cond_entropy pWmZ_unif W2_WmZ_indep _. +apply Ha => w w2 wmz Hneq0. +simpl in *. +by have := mc_removal_pr snd Z_O_indep pZ_unif w Hneq0. +Qed. + +End eqn4_proof. + +Section eqn4_1_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. +Variables (r1: {RV P -> TX})(x1 x2 s1: {RV P -> 'rV[TX]_n}). +Hypothesis x2_indep : P |= [% x1, s1, r1] _|_ x2. + +Lemma eqn_4_1_proof: + `H(x2|[%x1, s1, r1]) = entropy `p_ x2. +Proof. +transitivity (joint_entropy `p_ [%x1, s1, r1, x2] - `H `p_ [%x1, s1, r1]). + apply/eqP. + rewrite eq_sym subr_eq addrC. + apply/eqP. + have -> : `p_[%x2, [%x1, s1, r1]] = fdistX `p_[%x1, s1, r1, x2]. + by rewrite fdistX_RV2. + by rewrite chain_rule fst_RV2. +rewrite joint_entropy_indeRV. + by rewrite addrAC subrr add0r. +by exact: x2_indep. +Qed. + +End eqn4_1_proof. + +Section pi2_alice_is_leakage_free_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX : #|TX| = m.+2. +Hypothesis card_rVTX : #|'rV[TX]_n| = (m.+2 ^ n)%nat.-1.+1. + +Variables (r1 y2: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let x2' := x2 \+ s2. +Let r2 := s1 \*d s2 \- r1. +Let t := x1' \*d x2 \+ r2 \- y2. +Let y1 := t \- x2' \*d s1 \+ r1. +Let AliceView := [%x1, s1, r1, x2', t, y1]. + +Hypothesis y2_x1x2s1s2r1_eqn3_indep : P |= y2 _|_ [%x1, x2, s1, s2, r1]. +Hypothesis s2_x1s1r1x2_eqn4_indep : P |= s2 _|_ [%x1, s1, r1, x2]. +Hypothesis x1s2r1_x2_indep: P |= [% x1, s1, r1] _|_ x2. +Hypothesis neg_py2_unif : `p_ (neg_RV y2) = fdist_uniform card_TX. +Hypothesis ps2_unif : `p_ s2 = fdist_uniform card_rVTX. + +Let negy2_x1x2s1s2r1r2_eqn3_indep : + P |= neg_RV y2 _|_ [%x1, x2, s1, s2, r1, r2]. +Proof. +pose f (a: ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX) ) := let '(x1, x2, s1, s2, r1) := a in (a, s1 *d s2 - r1). +by move/(inde_rv_comp (fun (a : TX) => 0 - a) f):y2_x1x2s1s2r1_eqn3_indep. +Qed. + +Lemma pi2_alice_is_leakage_free_proof: + `H( x2 | AliceView) = `H `p_x2. +Proof. +transitivity (`H( x2 | [% x1, s1, r1, x2', t])). + by rewrite eqn2_proof. +transitivity (`H( x2 | [% x1, s1, r1, x2'])). + by rewrite (eqn3_proof negy2_x1x2s1s2r1r2_eqn3_indep neg_py2_unif). +transitivity (`H( x2 | [% x1, s1, r1])). + by rewrite (eqn4_proof ps2_unif s2_x1s1r1x2_eqn4_indep). +rewrite eqn_4_1_proof //. +Qed. + +End pi2_alice_is_leakage_free_proof. + +Section eqn6_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. + +Variables (r1 y2: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let r2 := s1 \*d s2 \- r1. + +Let O := [%x1, x2, s1, s2, r2, y2]. + +Let f1 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> 'rV[TX]_n := fun z => + let '(x1, _, _, _, _, _) := z in x1. + +Let f2 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX) := fun z => + let '(x1, x2, s1, s2, r2, y2) := z in (x2, s2, x1 + s1, r2). + +Let fm : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX * TX) -> TX := fun z => + let '(_, _, _, _, _, y2) := z in y2. + +Let W1 := f1 `o O. (* x1; It is okay in Bob's view has it because only used in condition. *) +Let W2 := f2 `o O. (* [%x2, s2, x1', r2]; cannot have x1, s1 here otherwise Bob knows the secret*) +Let Wm := fm `o O. (* y2 *) + +Let eq_W1_RV: + f1 `o O = x1. +Proof. by apply boolp.funext. Qed. + +Let eq_W2_RV: + f2 `o O = [%x2, s2, x1', r2]. +Proof. by apply boolp.funext. Qed. + +Let eq_Wm_RV: + fm `o O = y2. +Proof. by apply boolp.funext. Qed. + +(* Because y2 (Wm) is generated by Bob; not related to x2, s2, x1, s1, r2 at all*) +Hypothesis W2_Wm_indep: P|= W2 _|_ Wm. +(* Because x1 (W1) is from Alice and y2 (Wm) is from Bob *) +Hypothesis W1_Wm_indep: P|= W1 _|_ Wm. + +(* Because y2 (Wm) is generated by Bob; not related to x2, s2, x1, s1, r2 at all*) +Hypothesis W1W2_Wm_indep: P|= [%W1, W2] _|_ Wm. +(* TODO: deduce other indeps from this one. *) + +(* In the paper, y2 (Wm) is uniform distributed*) +Hypothesis pWm_unif: `p_ Wm = fdist_uniform card_TX. + +Let W1WmW2_cinde : W1 _|_ Wm | W2. +Proof. +apply: inde_RV2_cinde. by exact: W1W2_Wm_indep. +Qed. + +Lemma eqn6_proof: + `H(x1|[%[%x2, s2, x1', r2], y2]) = `H(x1|[%x2, s2, x1', r2]). +Proof. +rewrite -eq_W1_RV -eq_W2_RV -eq_Wm_RV. +have Ha := cpr_cond_entropy pWm_unif W2_Wm_indep _. +apply Ha => w w2 wm Hneq0. +simpl in *. +rewrite pr_eq_pairC in Hneq0. +have Hb:=(@cinde_alt _ _ _ _ _ W1 Wm W2 w wm w2 W1WmW2_cinde Hneq0). +rewrite -/W1. +rewrite cpr_RV2_sym. +exact: Hb. +Qed. + +End eqn6_proof. + +Section eqn7_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. + +Variables (r1: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let r2 := s1 \*d s2 \- r1. + +Let O := [%x1, x2, s1, s2, r2]. + +Let f1 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX) -> 'rV[TX]_n := fun z => + let '(x1, x2, s1, s2, r2) := z in x1. + +Let f2 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX) -> ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n) := fun z => + let '(x1, x2, s1, s2, r2) := z in (x2, s2, x1 + s1). + +Let fm : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * TX) -> TX := fun z => + let '(x1, x2, s1, s2, r2) := z in r2. + +Let W1 := f1 `o O. (* x1; It is okay in Bob's view has it because only used in condition. *) +Let W2 := f2 `o O. (* [%x2, s2, x1']; cannot have x1, s1 here otherwise Bob knows the secret*) +Let Wm := fm `o O. (* r2 *) + +Let eq_W1_RV: + f1 `o O = x1. +Proof. by apply boolp.funext. Qed. + +Let eq_W2_RV: + f2 `o O = [%x2, s2, x1']. +Proof. by apply boolp.funext. Qed. + +Let eq_Wm_RV: + fm `o O = r2. +Proof. by apply boolp.funext. Qed. + +Hypothesis W2_Wm_indep: P|= W2 _|_ Wm. +Hypothesis W1W2_Wm_indep : P|= [%W1, W2] _|_ Wm. + +(* In the paper, r2 (Wm) is uniform distributed*) +Hypothesis pWm_unif: `p_ Wm = fdist_uniform card_TX. + +Let W1WmW2_cinde : W1 _|_ Wm | W2. +Proof. apply: inde_RV2_cinde. by exact: W1W2_Wm_indep. +Qed. + +Lemma eqn7_proof: + `H(x1|[%[%x2, s2, x1'], r2]) = `H(x1|[%x2, s2, x1']). +Proof. +rewrite -eq_W1_RV -eq_W2_RV -eq_Wm_RV. +have Ha := cpr_cond_entropy pWm_unif W2_Wm_indep _. +apply Ha => w w2 wm Hneq0. +simpl in *. +rewrite pr_eq_pairC in Hneq0. +have Hb:=(@cinde_alt _ _ _ _ _ W1 Wm W2 w wm w2 W1WmW2_cinde Hneq0). +rewrite -/W1. +rewrite cpr_RV2_sym. +apply Hb. +Qed. + +(* Although in the paper eqn_7 needs Theorem 3.7 to prove, + it actually only needs cinde_alt. Because r2 is not Wm+Z but just Wm. +*) +End eqn7_proof. + +Section eqn8_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. +Hypothesis card_rVTX: #|'rV[TX]_n| = (m.+2 ^ n)%nat.-1.+1. + +Variables (x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. + +Let O := [%x1, x2, s1, s2]. + +(* f1 `o X in mc_removal_pr must be x1 in eqn8 *) +Let f1 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n) -> 'rV[TX]_n := fun z => + let '(x1, x2, s1, s2) := z in x1. + +(* f2 `o X in mc_removal_pr must be (x2, s2) in eqn8 *) +Let f2 : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n) -> ('rV[TX]_n * 'rV[TX]_n) := fun z => + let '(x1, x2, s1, s2) := z in (x2, s2). + +(* (fm `o X)+Z in mc_removal_pr must be x1 in eqn8 *) +Let fm : ('rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n * 'rV[TX]_n) -> 'rV[TX]_n := fun z => + let '(x1, x2, s1, s2) := z in x1. + +Let Z := s1. +Hypothesis pZ_unif : `p_ Z = fdist_uniform card_rVTX. + +Let W1 := f1 `o O. (* x1 *) +Let W2 := f2 `o O. (* [%x2, s2] *) +Let Wm := fm `o O. (* x1 *) +Let WmZ := fm `o O `+ s1. (* must be x1': x1' = x1 + s1 *) + +Let eq_W1_RV: + f1 `o O = x1. +Proof. by apply boolp.funext. Qed. + +Let eq_W2_RV: + f2 `o O = [%x2, s2]. +Proof. by apply boolp.funext. Qed. + +Let eq_Wm_RV: + fm `o O = x1. +Proof. by apply boolp.funext. Qed. + +Let eq_WmZ_RV: + fm `o O `+ s1 = x1'. +Proof. by rewrite /add_RV /neg_RV eq_Wm_RV /x1' //=. Qed. + +Hypothesis Z_O_indep : inde_rv Z O. + +(* Because s1 and x1 are generated by different participants *) +Hypothesis Z_WmZ_indep: P |= Z _|_ WmZ. + +(* Because [%x2, s2] and x1 are generated by different participants *) +Hypothesis W2_WmZ_indep: P |= W2 _|_ WmZ. + +Let pWmZ_unif : + `p_ WmZ = fdist_uniform card_rVTX. +Proof. +apply: add_RV_unif; last first. + rewrite (_:s1 = idfun `o s1) //. + apply: inde_rv_comp. + rewrite inde_rv_sym. + exact: Z_O_indep. +exact: pZ_unif. +Qed. + +Lemma eqn8_proof: + `H(x1|[%[%x2, s2], x1']) = `H(x1|[%x2, s2]). +Proof. +rewrite -eq_W1_RV -eq_W2_RV -eq_WmZ_RV. +rewrite -/W1 -/W2 -/WmZ. +have Ha := cpr_cond_entropy pWmZ_unif W2_WmZ_indep _. +apply: Ha => w w2 wm Hneq0. +rewrite -/W1. +by have := (mc_removal_pr f1 Z_O_indep pZ_unif w Hneq0). +Qed. + +End eqn8_proof. + +Section eqn8_1_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. +Hypothesis card_rVTX: #|'rV[TX]_n| = m.+2. + +Variables (x1 x2 s2: {RV P -> 'rV[TX]_n}). + +Hypothesis x2s2_x1_indep : P |= [% x2, s2] _|_ x1. + +Lemma eqn_8_1_proof: + `H(x1|[%x2, s2]) = entropy `p_ x1. +Proof. +transitivity (joint_entropy `p_ [%x2, s2, x1] - entropy `p_ [%x2, s2]). + apply/eqP. + rewrite eq_sym subr_eq addrC. + apply/eqP. + have -> : `p_ [%x1, [%x2, s2]] = fdistX `p_ [%[%x2, s2], x1]. + by rewrite fdistX_RV2. + by rewrite chain_rule fst_RV2. +rewrite joint_entropy_indeRV. + by rewrite addrAC subrr add0r. +by exact: x2s2_x1_indep. +Qed. + +End eqn8_1_proof. + +Section pi2_bob_view_is_leakage_free_proof. + +Variables (T: finType)(m n: nat)(P : R.-fdist T). +Let TX := [the finComRingType of 'I_m.+2]. +Hypothesis card_TX: #|TX| = m.+2. +Hypothesis card_rVTX: #|'rV[TX]_n| = (m.+2 ^ n)%nat.-1.+1. +Variables (r1 y2: {RV P -> TX})(x1 x2 s1 s2: {RV P -> 'rV[TX]_n}). +Let x1' := x1 \+ s1. +Let r2 := s1 \*d s2 \- r1. + +(* Hypothese from the paper. *) +Hypothesis x2s2_x1'_indep : P |= [% x2, s2] _|_ x1'. +Hypothesis x2s2x1'r2_y2_eqn6_indep : P |= [%x2, s2, x1', r2] _|_ y2. +Hypothesis x1x2s2x1'r2_y2_eqn6_indep : P |= [%x1, [%x2, s2, x1', r2]] _|_ y2. +Hypothesis x2_s2_x1'_r2_eqn7_indep : P |= [%x2, s2, x1'] _|_ r2. +Hypothesis x1x2_s2_x1'_r2_eqn7_indep : P |= [%x1, [%x2, s2, x1']] _|_ r2. +(* TODO: Reduce: longer one can imply others *) +Hypothesis s1_x1x2s1s2_eqn8_indep : P |= s1 _|_ [%x1, x2, s1, s2]. +Hypothesis x2s2_x1_indep : P |= [% x2, s2] _|_ x1. + +Hypothesis s1s2_r1_indep : P|= [%s1, s2] _|_ r1. +Hypothesis s1_s2_indep : P|= s1 _|_ s2. +Hypothesis pr1_unif : `p_ r1 = fdist_uniform card_TX. +Hypothesis py2_unif : `p_ y2 = fdist_uniform card_TX. +Hypothesis ps1_unif : `p_ s1 = fdist_uniform card_rVTX. + +Let pr2_unif := ps1_dot_s2_r_unif pr1_unif s1_s2_indep s1s2_r1_indep. +Let BobView := [%x2, s2, x1', r2, y2]. + +Lemma pi2_bob_is_leakage_free_proof: + `H( x1 | BobView) = `H `p_ x1. +Proof. +transitivity (`H( x1 | [% x2, s2, x1', r2])). + by rewrite (eqn6_proof x2s2x1'r2_y2_eqn6_indep x1x2s2x1'r2_y2_eqn6_indep py2_unif). +transitivity (`H(x1|[%x2, s2, x1'])). + by rewrite (eqn7_proof x2_s2_x1'_r2_eqn7_indep x1x2_s2_x1'_r2_eqn7_indep pr2_unif). +transitivity (`H(x1|[%x2, s2])). + by rewrite (eqn8_proof ps1_unif s1_x1x2s1s2_eqn8_indep). +by rewrite eqn_8_1_proof //. +Qed. + +End pi2_bob_view_is_leakage_free_proof. + +End pi2. + +(* TODO: Using graphoid for combinations of independ random variables. *) +Section mutual_indep. + +(* Pairwise independence: Any collection of mutually independent random variables is pairwise independent + +(But pairwise independence does not imply mutual independence. + +How to express "a collection of any types of mutual independent random variables"? +RV2 is a collection. But it is not a sequence so cannot be used to generate arbitrary pairs of RVs. +Should RV2 supports to be traversed as a sequence?? +*) + +Variables (A: finType)(m n: nat)(P : R.-fdist A). +Variables (TX VX: finType). +Variables (x1 x2 s1 s2 r1 y2: {RV P -> TX}). + +Hypothesis Hinde : {homo nth x1 [:: x1; x2; s1; s2] : i j / i < j >-> inde_rv i j}%nat. + +Lemma x1_x2_inde: + P|= x1 _|_ x2. +Proof. +have H := @Hinde 0 1. +apply H. +rewrite //. +Qed. + +Hypothesis Hinde_all : forall i j, P|= nth x1 [:: x1; x2; s1; s2] i _|_ nth r1 [:: r1; y2] j. + +Lemma x1_r1_inde: + P|= x1 _|_ r1. +Proof. +have H := @Hinde_all 0 0. +apply H. +Qed. + +End mutual_indep. + +End smc_entropy_proofs. diff --git a/smc/smc_interpreter.v b/smc/smc_interpreter.v new file mode 100644 index 00000000..59e6aa85 --- /dev/null +++ b/smc/smc_interpreter.v @@ -0,0 +1,584 @@ +From HB Require Import structures. +Require Import Reals. +From mathcomp Require Import all_ssreflect all_algebra fingroup finalg matrix Rstruct ring. +Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist. +Require Import proba jfdist_cond entropy graphoid smc_proba smc_entropy smc_tactics. + +Import GRing.Theory. +Import Num.Theory. +Module scp := smc_entropy.smc_entropy_proofs. + +(******************************************************************************) +(* *) +(* Interpreter for Secure Multiparty Protocols *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. +Local Open Scope reals_ext_scope. +Local Open Scope proba_scope. +Local Open Scope fdist_scope. +Local Open Scope chap2_scope. +Local Open Scope entropy_scope. +Local Open Scope vec_ext_scope. + +Reserved Notation "u *d w" (at level 40). +Reserved Notation "u \*d w" (at level 40). + +Section interp. +Variable data : Type. +Inductive proc : Type := + | Init : data -> proc -> proc + | Send : nat -> data -> proc -> proc + | Recv : nat -> (data -> proc) -> proc + | Ret : data -> proc + | Finish : proc + | Fail : proc. + +Definition step (A : Type) (ps : seq proc) (trace : seq data) + (yes no : proc * seq data -> A) (i : nat) : A := + let ps := nth Fail ps in + let p := ps i in + let nop := no (p, trace) in + match p with + | Recv frm f => + if ps frm is Send dst v _ then + if dst == i then yes (f v, v::trace) else nop + else nop + | Send dst w next => + if ps dst is Recv frm _ then + if frm == i then yes (next, trace) else nop + else nop + | Init d next => + yes (next, d::trace) + | Ret d => + yes (Finish, d :: trace) + | Finish | Fail => + nop + end. + +Fixpoint interp h (ps : seq proc) (traces : seq (seq data)) := + if h is h.+1 then + if has (fun i => step ps [::] (fun=>true) (fun=>false) i) + (iota 0 (size ps)) then + let ps_trs' := [seq step ps (nth [::] traces i) idfun idfun i + | i <- iota 0 (size ps)] in + let ps' := unzip1 ps_trs' in + let trs' := unzip2 ps_trs' in + interp h ps' trs' + else (ps, traces) + else (ps, traces). + +Definition run_interp h procs := interp h procs (nseq (size procs) [::]). +End interp. + +Arguments Finish {data}. +Arguments Fail {data}. + +Section traces. +Variable data : eqType. +Local Open Scope nat_scope. + +Lemma size_traces h (procs : seq (proc data)) : + forall s, s \in (run_interp h procs).2 -> size s <= h. +Proof. +clear. +pose k := h. +rewrite -{2}/k /run_interp. +set traces := nseq _ _ => /=. +have Htr : {in traces, forall s, size s <= k - h}. + move=> s. by rewrite mem_nseq => /andP[] _ /eqP ->. +have : h <= k by []. +elim: h k procs traces Htr => [| h IH] k procs traces Htr hk //=. + move=> s /Htr. by rewrite subn0. +move=> s. +case: ifP => H; last by move/Htr/leq_trans; apply; rewrite leq_subr. +move/IH; apply; last by apply/ltnW. +move=> /= {}s. +rewrite /unzip2 -map_comp. +case/mapP => i. +rewrite mem_iota add0n /step => /andP[] _ Hi /=. +have Hsz : size (nth [::] traces i) < k - h. + case/boolP: (i < size traces) => Hi'. + apply/(leq_ltn_trans (Htr _ _)). + by rewrite mem_nth. + by rewrite subnS prednK // leq_subRL // ?addn1 // ltnW. + rewrite nth_default. by rewrite leq_subRL ?addn1 // ltnW. + by rewrite leqNgt. +case: nth => /=[d p|n d p|n p|d||] -> //=; try exact/ltnW. +- case: nth => /=[{}d {}p|n1 {}d {}p| n1 _|{}d||] /=; try exact/ltnW. + case: ifP => _ /=; exact/ltnW. +- case: nth => /=[{}d p1|n1 {}d p1| n1 p1|{}d||] /=; try exact/ltnW. + case: ifP => _ //=; exact/ltnW. +Qed. + +Lemma size_interp h (procs : seq (proc data)) (traces : seq (seq data)) : + size procs = size traces -> + size (interp h procs traces).1 = size procs /\ + size (interp h procs traces).2 = size procs. +Proof. +elim: h procs traces => // h IH procs traces Hsz /=. +case: ifP => _ //. +rewrite /unzip1 /unzip2 -!map_comp. +set map1 := map _ _. +set map2 := map _ _. +case: (IH map1 map2). + by rewrite !size_map. +move=> -> ->. +by rewrite !size_map size_iota. +Qed. + +Lemma size_traces_nth h (procs : seq (proc data)) (i : 'I_(size procs)) : + (size (nth [::] (run_interp h procs).2 i) <= h)%N. +Proof. +by apply/size_traces/mem_nth; rewrite (size_interp _ _).2 // size_nseq. +Qed. + +Definition interp_traces h procs : (size procs).-tuple (h.-bseq data) := + [tuple Bseq (size_traces_nth h i) | i < size procs]. + +Lemma interp_traces_ok h procs : + map val (interp_traces h procs) = (run_interp h procs).2. +Proof. +apply (eq_from_nth (x0:=[::])). + rewrite size_map /= size_map size_enum_ord. + by rewrite (size_interp _ _).2 ?size_nseq. +move=> i Hi. +rewrite size_map in Hi. +rewrite (nth_map [bseq]) // /interp_traces. +rewrite size_tuple in Hi. +by rewrite (_ : i = Ordinal Hi) // nth_mktuple. +Qed. +End traces. + +Section scalar_product. +Variable m : nat. +Variable TX : finComRingType. +Variable VX : lmodType TX. (* vector is not ringType (mul)*) +Variable dotproduct : VX -> VX -> TX. +Notation "u *d w" := (dotproduct u w). + +Definition alice : nat := 0. +Definition bob : nat := 1. +Definition coserv : nat := 2. + +Definition data := (TX + VX)%type. +Definition one x : data := inl x. +Definition vec x : data := inr x. + +Definition Recv_one frm f : proc data := + Recv frm (fun x => if x is inl v then f v else Fail). +Definition Recv_vec frm f : proc data := + Recv frm (fun x => if x is inr v then f v else Fail). + +Definition pcoserv (sa sb: VX) (ra : TX) : proc data := + Init (vec sa) ( + Init (vec sb) ( + Init (one ra) ( + Send alice (vec sa) ( + Send alice (one ra) ( + Send bob (vec sb) ( + Send bob (one (sa *d sb - ra)) Finish)))))). + +Definition palice (xa : VX) : proc data := + Init (vec xa) ( + Recv_vec coserv (fun sa => + Recv_one coserv (fun ra => + Send bob (vec (xa + sa)) ( + Recv_vec bob (fun xb' => + Recv_one bob (fun t => + Ret (one (t - (xb' *d sa) + ra)))))))). + +Definition pbob (xb : VX) (yb : TX) : proc data := + Init (vec xb) ( + Init (one yb) ( + Recv_vec coserv (fun sb => + Recv_one coserv (fun rb => + Recv_vec alice (fun xa' => + let t := xa' *d xb + rb - yb in + Send alice (vec (xb + sb)) + (Send alice (one t) (Ret (one yb)))))))). + +Variables (sa sb: VX) (ra yb: TX) (xa xb: VX). +Definition smc_scalar_product h := + (interp h [:: palice xa; pbob xb yb; pcoserv sa sb ra] [::[::];[::];[::]]). + +Goal (smc_scalar_product 11).2 = ([::]). +cbv -[GRing.add GRing.opp GRing.Ring.sort (*Equality.eqtype_hasDecEq_mixin*) ]. +Undo 1. +rewrite /smc_scalar_product. +rewrite (lock (11 : nat)) /=. +rewrite -lock (lock (10 : nat)) /=. +rewrite -lock (lock (9 : nat)) /=. +rewrite -lock (lock (8 : nat)) /=. +rewrite -lock (lock (7 : nat)) /=. +rewrite -lock (lock (6 : nat)) /=. +rewrite -lock (lock (5 : nat)) /=. +rewrite -lock (lock (4 : nat)) /=. +rewrite -lock (lock (3 : nat)) /=. +rewrite -lock (lock (2 : nat)) /=. +rewrite -lock (lock (1 : nat)) /=. +rewrite -lock (lock (0 : nat)) /=. +Abort. + +Let xa' := xa + sa. +Let xb' := xb + sb. +Let rb := sa *d sb - ra. +Let t := xa' *d xb + rb - yb. +Let ya := t - xb' *d sa + ra. + +Lemma smc_scalar_product_ok : + smc_scalar_product 11 = + ([:: Finish; Finish; Finish], + [:: [:: one ya; + one t; + vec xb'; + one ra; + vec sa; + vec xa]; + [:: one yb; + vec xa'; + one rb; + vec sb; + one yb; + vec xb]; + [:: one ra; + vec sb; + vec sa] + ]). +Proof. reflexivity. Qed. + +Definition smc_scalar_product_traces := + interp_traces 11 [:: palice xa; pbob xb yb; pcoserv sa sb ra]. + +Lemma smc_scalar_product_traces_ok : + smc_scalar_product_traces = + [tuple + [bseq one ya; one t; vec xb'; one ra; vec sa; vec xa]; + [bseq one yb; vec xa'; one rb; vec sb; one yb; vec xb]; + [bseq one ra; vec sb; vec sa]]. +Proof. by apply/val_inj/(inj_map val_inj); rewrite interp_traces_ok. Qed. + +Definition smc_scalar_product_tracesT := 11.-bseq data. + +Definition smc_scalar_product_party_tracesT := + 3.-tuple smc_scalar_product_tracesT. + +Definition is_scalar_product (trs: smc_scalar_product_party_tracesT) := + let '(ya, xa) := + if tnth trs 0 is Bseq [:: inl ya; _; _; _; _; inr xa] _ then (ya, xa) + else (0,0) in + let '(yb, xb) := + if tnth trs 1 is Bseq [:: inl yb; _; _; _; _; inr xb] _ then (yb, xb) + else (0,0) in + xa *d xb = ya + yb. + +End scalar_product. + +Section pi2. + +Section information_leakage_proof. + +Variable n m : nat. +Variable T : finType. +Variable P : R.-fdist T. +Let TX := [the finComRingType of 'I_m.+2]. +Let VX := 'rV[TX]_n. + +Lemma card_TX : #|TX| = m.+2. +Proof. by rewrite card_ord. Qed. + +Let q := (m.+2 ^ n)%nat.-1. +Lemma card_VX : #|VX| = q.+1. +Proof. +rewrite prednK. + by rewrite /VX card_mx card_TX mul1n. +by rewrite expn_gt0. +Qed. + +Notation "u *d w" := (scp.dotproduct u w). +Notation "u \*d w" := (scp.dotproduct_rv u w). + +Lemma smc_scalar_product_is_correct sa sb ra yb xa xb : + is_scalar_product scp.dotproduct ( + @smc_scalar_product_traces TX VX scp.dotproduct sa sb ra yb xa xb). +Proof. +rewrite smc_scalar_product_traces_ok /is_scalar_product /=. +symmetry. +rewrite (scp.dot_productC (xa+sa) xb). +rewrite !scp.dot_productDr. +rewrite scp.dot_productC. +rewrite (scp.dot_productC xb sa). +rewrite (scp.dot_productC (xb+sb) sa). +rewrite scp.dot_productDr. +(* Weird: without making it as a lemma, the ring tactic fails. *) +have // ->: xa *d xb + sa *d xb + (sa *d sb - ra) - yb - (sa *d xb + sa *d sb) + ra + yb = xa *d xb. + by ring. +Qed. + +Definition scalar_product_uncurry (o: VX * VX * TX * TX * VX * VX) + : smc_scalar_product_party_tracesT VX := + let '(sa, sb, ra, yb, xa, xb) := o in + (smc_scalar_product_traces scp.dotproduct sa sb ra yb xa xb). + +Record scalar_product_random_inputs := + ScalarProductRandomInputs { + x1 : {RV P -> VX}; + x2 : {RV P -> VX}; + s1 : {RV P -> VX}; + s2 : {RV P -> VX}; + r1 : {RV P -> TX}; + y2 : {RV P -> TX}; + + (* TODO: prove others via these basic hypotheses + x1_indep : P |= x1 _|_ [%x2, s1, s2, r1, y2]; + x2_indep : P |= x2 _|_ [%x1, s1, s2, r1, y2]; + *) + + x2s2x1s1r1_y2_indep : P |= [% x2, s2, x1, s1, r1] _|_ y2; + x1s1r1_x2_indep : P |= [%x1, s1, r1] _|_ x2; + s1_s2_indep : P |= s1 _|_ s2; + s1s2_r1_indep : P |= [% s1, s2] _|_ r1; + x2_indep : P |= [% x1, s1, r1] _|_ x2; + y2_x1x2s1s2r1_indep : P |= y2 _|_ [% x1, x2, s1, s2, r1]; + s1_x1x2s1s2_indep : P |= s1 _|_ [% x1, x2, s1, s2]; + s2_x1s1r1x2_indep : P |= s2 _|_ [% x1, s1, r1, x2]; + x2s2_x1s1_indep : P |= [%x2, s2] _|_ [%x1, s1]; + x1_s1_indep : P |= x1 _|_ s1; + s1_x1x2s2_indep : P |= s1 _|_ [%x1, [%x2, s2]]; + s1x2x1x2_r1_indep : P |= [% s1, s2, x1, x2] _|_ r1; + x2s2_x1_indep : P |= [%x2, s2] _|_ x1; + + neg_py2_unif : `p_ (neg_RV y2) = fdist_uniform card_TX; + + ps1_unif : `p_ s1 = fdist_uniform card_VX; + ps2_unif : `p_ s2 = fdist_uniform card_VX; + py2_unif : `p_ y2 = fdist_uniform card_TX; + pr1_unif : `p_ r1 = fdist_uniform card_TX; + }. + +Variable inputs: scalar_product_random_inputs. + +Definition scalar_product_RV (inputs : scalar_product_random_inputs) : + {RV P -> smc_scalar_product_party_tracesT VX} := + scalar_product_uncurry `o + [%s1 inputs, s2 inputs, r1 inputs, y2 inputs, x1 inputs, x2 inputs]. + +Let alice_traces : RV (smc_scalar_product_tracesT VX) P := + (fun t => tnth t 0) `o scalar_product_RV inputs. + +Let bob_traces : RV (smc_scalar_product_tracesT VX) P := + (fun t => tnth t 1) `o scalar_product_RV inputs. + +Definition scalar_product_is_leakage_free := + `H(x2 inputs | alice_traces) = `H `p_ (x2 inputs) /\ + `H(x1 inputs | bob_traces) = `H `p_ (x1 inputs). + +Let x1 := x1 inputs. +Let s1 := s1 inputs. +Let r1 := r1 inputs. +Let x2 := x2 inputs. +Let s2 := s2 inputs. +Let y2 := y2 inputs. +Let x1' : {RV P -> VX} := x1 \+ s1. +Let x2' : {RV P -> VX} := x2 \+ s2. +Let r2 : {RV P -> TX} := (s1 \*d s2) \- r1. +Let t : {RV P -> TX} := x1' \*d x2 \+ r2 \- y2. +Let y1 : {RV P -> TX} := t \- (x2' \*d s1) \+ r1. +Let data := (sum TX VX). +Let one x : data := inl x. +Let vec x : data := inr x. + +Lemma cond_entropyC (A B C : finType) + (X: {RV P -> A}) (Y: {RV P -> B}) (Z: {RV P -> C}) : + `H(X | [% Y, Z]) = `H(X | [% Z, Y]). +Proof. +rewrite /cond_entropy /=. +rewrite (reindex (fun p : C * B => (p.2, p.1))) /=; last first. + by exists (fun p : B * C => (p.2, p.1)) => -[b c]. +apply: eq_bigr => -[c b] _ /=. +rewrite !snd_RV2 -!pr_eqE' pr_eq_pairC. +congr (_ * _). +rewrite /cond_entropy1; congr (- _). +rewrite /jcPr !snd_RV2. +apply: eq_bigr => a _. +by rewrite !setX1 !Pr_set1 -!pr_eqE' !pr_eq_pairA pr_eq_pairAC (pr_eq_pairC Z). +Qed. + +Let alice_traces_from_view xs : 11.-bseq _ := + let '(x1, s1, r1, x2', t, y1) := xs in + [bseq one y1; one t; vec x2'; one r1; vec s1; vec x1]. + +Lemma alice_traces_ok : + alice_traces = alice_traces_from_view `o [%x1, s1, r1, x2', t, y1]. +Proof. +apply: boolp.funext => x /=. +rewrite /alice_traces /scalar_product_RV /comp_RV /=. +by rewrite smc_scalar_product_traces_ok. +Qed. + +Lemma alice_traces_entropy : + `H(x2 | alice_traces) = `H(x2 | [%x1, s1, r1, x2', t, y1]). +Proof. +transitivity (`H(x2 | [% alice_traces, [%x1, s1, r1, x2', t, y1]])). + pose f (xs : smc_scalar_product_tracesT VX) := + if xs is Bseq [:: inl y1; inl t; inr x2'; + inl r1; inr s1; inr x1] _ + then (x1, s1, r1, x2', t, y1) + else (0, 0, 0, 0, 0, 0). + have fK : cancel alice_traces_from_view f by move=> [] [] [] [] []. + have -> : [% x1, s1, r1, x2', t, y1] = f `o alice_traces. + by apply: boolp.funext => x /=; rewrite alice_traces_ok /comp_RV fK. + by rewrite scp.fun_cond_removal. +by rewrite alice_traces_ok cond_entropyC scp.fun_cond_removal. +Qed. + +Let bob_traces_from_view xs : 11.-bseq _ := + let '(x2, s2, x1', r2, y2) := xs in + [:: one y2; vec x1'; one r2; vec s2; one y2; vec x2]. + +Lemma bob_traces_ok : + bob_traces = bob_traces_from_view `o [%x2, s2, x1', r2, y2]. +Proof. +apply: boolp.funext => x /=. +rewrite /bob_traces /scalar_product_RV /comp_RV /=. +by rewrite smc_scalar_product_traces_ok. +Qed. + +Lemma bob_traces_entropy : + `H(x1 | bob_traces) = `H(x1 | [%x2, s2, x1', r2, y2]). +Proof. +transitivity (`H(x1 | [% bob_traces, [%x2, s2, x1', r2, y2]])). + pose f (xs : 11.-bseq data) := + if xs is Bseq [:: inl y2; inr x1'; inl r2; + inr s2; inl _; inr x2] _ + then (x2, s2, x1', r2, y2) + else (0, 0, 0, 0, 0). + have fK : cancel bob_traces_from_view f by move=> [] [] [] [] []. + have -> : [%x2, s2, x1', r2, y2] = f `o bob_traces. + by apply: boolp.funext => x; rewrite bob_traces_ok /comp_RV fK. + by rewrite scp.fun_cond_removal. +by rewrite bob_traces_ok cond_entropyC scp.fun_cond_removal. +Qed. + +Let pnegy2_unif : + `p_ (neg_RV y2) = fdist_uniform card_TX. +Proof. rewrite -(scp.neg_RV_dist_eq (py2_unif inputs)). +exact: (py2_unif inputs). Qed. + +Let x2s2_x1'_indepP : + P |= [% x2, s2] _|_ x1'. +Proof. +have px1_s1_unif: `p_ (x1 \+ s1 : {RV P -> _}) = fdist_uniform card_VX. + rewrite -(add_RV_unif x1 s1) ?ps1_unif //. + exact: x1_s1_indep. +have H:= @lemma_3_5' T (VX * VX)%type VX P q x1 s1 [%x2, s2] card_VX (ps1_unif inputs) (s1_x1x2s2_indep inputs). +rewrite inde_rv_sym in H. +exact: H. +Qed. + +Let x2s2x1s1r2_y2_indep : + P |= [% x2, s2, x1, s1, r1] _|_ y2 -> + P |= [% x2, s2, x1, s1, r2] _|_ y2. +Proof. +pose f := fun (vs : (VX * VX * VX * VX * TX)) => + let '(xb, sb, xa, sa, ra) := vs in (xb, sb, xa, sa, sa *d sb - ra). +pose g := fun (ws : TX) => ws. (* because idfun causes error. *) +by apply_inde_rv_comp f g. +Qed. + +Let x2s2x1'r2_y2_indep : + P |= [% x2, s2, x1, s1, r2] _|_ y2 -> + P |= [% x2, s2, x1', r2] _|_ y2. +Proof. +pose f := fun (vs : (VX * VX * VX * VX * TX)) => + let '(xb, sb, xa, sa, rb) := vs in (xb, sb, xa + sa, rb). +pose g := fun (ws : TX) => ws. +by apply_inde_rv_comp f g. +Qed. + +Let x2s2x1'r2_y2_indepP := + x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)). + +Let x1x2s2x1'r2_y2_indep : + P |= [% x2, s2, x1, s1, r2] _|_ y2 -> + P |= [% x1, [%x2, s2, x1', r2]] _|_ y2. +Proof. +rewrite /x1'. +pose f := fun (vs : (VX * VX * VX * VX * TX)) => + let '(xb, sb, xa, sa, rb) := vs in (xa, (xb, sb, xa + sa, rb)). +pose g := fun (ws : TX) => ws. +by apply_inde_rv_comp f g. +Qed. + +Let x1x2s2x1'r2_y2_indepP := + x1x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)). + +Let x1x2s2x1'_r2_indep : + P |= [% x1, [% x2, s2, x1']] _|_ r2. +Proof. +rewrite inde_rv_sym /r2 scp.sub_RV_eq. +apply: (lemma_3_5' (card_TZ:=card_TX)). + by rewrite -(scp.neg_RV_dist_eq (card_TX:=card_TX)) pr1_unif. +rewrite inde_rv_sym. +apply: scp.neg_RV_inde_eq. +pose f := fun (vs: (VX * VX * VX * VX)) => + let '(sa, sb, xa, xb) := vs in (sa *d sb, (xa, (xb, sb, xa + sa))). +pose g := fun (ws : TX) => ws. +have := s1x2x1x2_r1_indep inputs. +by apply_inde_rv_comp f g. +Qed. + +Let x2s2x1'_r2_indep : + P |= [% x2, s2, x1'] _|_ r2. +Proof. +have := x1x2s2x1'_r2_indep. +pose f := fun (vs: (VX * (VX * VX * VX))) => + let '(xa, (xb, sb, xa')) := vs in (xb, sb, xa'). +pose g := fun (ws : TX) => ws. +by apply_inde_rv_comp f g. +Qed. + +(* Use all hypotheses of the secret inputs and random variables, + and all technical lemmas about intermediate results, + to prove information leakage free equations in Sec.[III.C]{Shen2007} + + H(x2 | VIEW_1^{\pi_2}) = H(x2) ... Alice obtain no new knowledge about `x2` from the protocol + H(x1 | VIEW_2^{\pi_2}) = H(x1) ... Bob obtain no new knowledge about `x1` from the protocol + + *) + +Let proof_alice := scp.pi2_alice_is_leakage_free_proof + (y2_x1x2s1s2r1_indep inputs) + (s2_x1s1r1x2_indep inputs) + (x1s1r1_x2_indep inputs) pnegy2_unif (ps2_unif inputs). + +Check proof_alice. + +Let proof_bob := scp.pi2_bob_is_leakage_free_proof + (card_TX:=card_TX)(card_rVTX:=card_VX)(r1:=r1)(y2:=y2) + x2s2_x1'_indepP x2s2x1'r2_y2_indepP x1x2s2x1'r2_y2_indepP + x2s2x1'_r2_indep x1x2s2x1'_r2_indep + (s1_x1x2s1s2_indep inputs) (x2s2_x1_indep inputs) (s1s2_r1_indep inputs) + (s1_s2_indep inputs) + (pr1_unif inputs) (py2_unif inputs) (ps1_unif inputs). + +Check proof_bob. + +Theorem scalar_product_is_leakage_freeP : + scalar_product_is_leakage_free. +Proof. +split. + rewrite alice_traces_entropy. + exact: proof_alice. +rewrite bob_traces_entropy. +exact: proof_bob. +Qed. + +End information_leakage_proof. + +End pi2. diff --git a/smc/smc_interpreter_mkBind.v b/smc/smc_interpreter_mkBind.v new file mode 100644 index 00000000..d507b3a1 --- /dev/null +++ b/smc/smc_interpreter_mkBind.v @@ -0,0 +1,154 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra fingroup finalg matrix. +Require Import Reals. +From mathcomp Require Import Rstruct ring. +Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext. +Require Import fdist proba jfdist_cond entropy smc graphoid. + +Import GRing.Theory. +Import Num.Theory. + +(******************************************************************************) +(* *) +(* Interpreter for Secure Multiparty Protocols *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. +Local Open Scope vec_ext_scope. + +Reserved Notation "u *d w" (at level 40). +Reserved Notation "u \*d w" (at level 40). + +Section interp. +Variable data : eqType. +Inductive proc : Type -> Type := + | Send : nat -> data -> proc unit + | Recv : nat -> proc data + | Ret A : A -> proc A + | Bind A B : proc A -> (A -> proc B) -> proc B + | Fail A : proc A. + +Arguments Fail {A}. + +Fixpoint mkBind A (p : proc A) : proc A := + match p in proc B return B = A -> proc A with + | Send n v => fun H => eq_rect _ proc (Bind (Send n v) (@Ret _)) _ H + | Recv n => fun H => eq_rect _ proc (Bind (Recv n) (@Ret _)) _ H + | Bind C _ m g => fun H0 => + if m is Bind _ _ _ _ then + match mkBind m in proc D return (D = C) -> proc A with + | Bind _ _ m f => fun H => + eq_rect _ proc + (Bind m (fun x => Bind (eq_rect _ proc (f x) _ H) g)) _ H0 + | m' => fun H => eq_rect _ proc (Bind m' g) _ H0 + end erefl + else p + | p => fun H => p + end erefl. + +Fixpoint interp h (ps : seq (proc data)) : seq (proc data) := + if h is h.+1 then + let step A (yes : proc data -> A) (no : proc data -> A) i := + let p := nth Fail ps i in + match mkBind p in proc C return (C = data) -> A with + | Bind _ B (Send dst _) next => fun H => + if mkBind (nth Fail ps dst) is Bind _ _ (Recv frm) _ then + if frm == i then yes (eq_rect B proc (next tt) _ H) else no p + else no p + | Bind _ B (Ret _ v) f => fun H => yes (eq_rect _ proc (f v) _ H) + | _ => fun _ => no + (match mkBind p in proc A return (A = data) -> proc data with + | Bind _ B (Recv frm) f => fun H => + if mkBind (nth Fail ps frm) is Bind _ _ (Send dst v) _ then + if dst == i then eq_rect B proc (f v) _ H else p + else p + | _ => fun H => p end erefl) + end erefl + in + if has (step bool (fun=>true) (fun=>false)) (iota 0 (size ps)) then + let ps' := map (step (proc data) idfun idfun) (iota 0 (size ps)) + in interp h ps' + else + ps + else ps. + +End interp. + +Arguments Fail {data A}. +Arguments Ret {data A}. +Arguments Recv {data}. +Arguments Send {data}. + +Notation "m >>= f" := (Bind m f) (at level 49). +Notation "'do' x <- m ; e" := (Bind m (fun x => e)) + (at level 60, x name, m at level 200, e at level 60, only parsing). +Notation "'do' x : T <- m ; e" := (Bind m (fun x : T => e)) + (at level 60, x name, m at level 200, e at level 60, only parsing). +Notation "m >> f" := (Bind m (fun _ => f)) (at level 49). + +Section scalar_product. +Variable TX VX : ringType. +Variable dotproduct : VX -> VX -> TX. +Notation "u *d w" := (dotproduct u w). + +Definition alice : nat := 0. +Definition bob : nat := 1. +Definition coserv : nat := 2. +Definition data := option (TX + VX). +Definition one x : data := Some (inl x). +Definition vec x : data := Some (inr x). +Notation proc := (proc data). +Definition Recv_one frm : proc TX := + Recv frm >>= fun x => if x is Some (inl v) then Ret v else Fail. +Definition Recv_vec frm : proc VX := + Recv frm >>= fun x => if x is Some (inr v) then Ret v else Fail. + +Definition palice (xa : VX) : proc data := + do sa <- Recv_vec coserv; + do ra <- Recv_one coserv; + Send bob (vec (xa + sa)) >> + do xb' <- Recv_vec bob; + do t <- Recv_one bob; + Ret (one (t - (xb' *d sa) + ra)). +Definition pbob (xb : VX) : proc data := + do sb <- Recv_vec coserv; + do yb <- Recv_one coserv; + do rb <- Recv_one coserv; + do xa' <- Recv_vec alice; + let t := xa' *d xb + rb - yb in + Send alice (vec (xb + sb)) >> Send alice (one t) >> Ret (one yb). +Definition pcoserv (sa sb: VX) (ra yb: TX) : proc data := + Send alice (vec sa) >> + Send alice (one ra) >> + Send bob (vec sb) >> + Send bob (one yb) >> + Send bob (one (sa *d sb - ra)) >> Ret None. + +Variables (sa sb: VX) (ra yb: TX) (xa xb: VX). +Definition scalar_product h := + interp h [:: palice xa; pbob xb; pcoserv sa sb ra yb]. + +Goal scalar_product 16 = [:: Fail; Fail; Fail]. +cbv -[GRing.add GRing.opp]. +rewrite /scalar_product. +rewrite (lock (14 : nat)) /=. +rewrite -lock (lock (12 : nat)) /=. +rewrite -lock (lock (10 : nat)) /=. +rewrite -lock (lock (8 : nat)) /=. +rewrite -lock (lock (6 : nat)) /=. +rewrite -lock (lock (4 : nat)) /=. +rewrite -lock (lock (2 : nat)) /=. +rewrite -lock /=. +Abort. + +Lemma scalar_product_ok : + scalar_product 16 = + [:: Ret (one ((xa + sa) *d xb + (sa *d sb - ra) - yb - (xb + sb) *d sa + ra)); + Ret (one yb); Ret None]. +Proof. reflexivity. Qed. +End scalar_product. diff --git a/smc/smc_party_indep.v b/smc/smc_party_indep.v new file mode 100644 index 00000000..a314ea15 --- /dev/null +++ b/smc/smc_party_indep.v @@ -0,0 +1,171 @@ +From HB Require Import structures. +Require Import Reals. +From mathcomp Require Import all_ssreflect all_algebra fingroup Rstruct ring boolp classical_sets. +Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist. +Require Import proba jfdist_cond entropy graphoid smc_proba smc_entropy smc_tactics. + +Import GRing.Theory. +Import Num.Theory. + +(******************************************************************************) +(* *) +(* Party, RNG and independence experiments for Secure Multiparty Protocols *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. +Local Open Scope reals_ext_scope. +Local Open Scope proba_scope. +Local Open Scope fdist_scope. +Local Open Scope chap2_scope. +Local Open Scope entropy_scope. +Local Open Scope vec_ext_scope. + +Section party. + +Inductive party := Alice | Bob | Coserv. + +Definition party_eqb_subproof (p1 p2: party) : { p1 = p2 } + { p1 <> p2 }. +Proof. decide equality. Defined. + +Definition party_eqb (p1 p2: party) : bool := + if party_eqb_subproof p1 p2 then true else false. + +Print Module Equality. + +Lemma party_eqP : Equality.axiom party_eqb. +Proof. +move=> p1 p2. +rewrite /party_eqb. +by case: party_eqb_subproof => /= H;constructor. +Qed. + +HB.instance Definition _ := hasDecEq.Build party party_eqP. + +Definition party_to_nat (a : party) : nat := + match a with Alice => 0 | Bob => 1 | Coserv => 2 end. + +Definition nat_to_party (a : nat) : party := + match a with 0 => Alice | 1 => Bob | _ => Coserv end. + +Lemma party_natK : cancel party_to_nat nat_to_party. +Proof. by case. Qed. + +HB.instance Definition _ : isCountable party := CanIsCountable party_natK. + +Definition party_enum := [:: Alice; Bob; Coserv]. + +Lemma party_enumP : Finite.axiom party_enum. +Proof. by case. Qed. + +HB.instance Definition _ := isFinite.Build party party_enumP. + +End party. + +Section indep. + +(* Memo: use this to contain related expressions *) +Inductive AliceVar := X1. +Inductive BobVar := X2 | Y2. +Inductive CoservVar := S1 | S2 | R1. (* Once one RV is generated, RGN changes so they are mutual indep *) + +(* uniform distribution: + + TX : 1,2,3,.....N + ([Alice: 100%, Bob: 0%, Coserv: 0%], 1) (Alice, 2) ..... (Alice, N) + + r1 + y1 = (uniform dist; by lemma) + + r1 : 1,2,3,..... N + y1 : 1,2,3...... M + + r1 + y1: ( + +---- Convex algebra + (party1 * party2 * party3 * {RV P -> TX}) + + (1, 0, 0, x1) + (0.5, 0.5, 0, x1 + y2 * y2 * s1) + + can be embeded into Euclidean space. + +---- Union semi-lattice + + ({RV P -> TX} * seq bool) + + (x1, 1, 0, 0...) + (x1 + y2, 1, 1, 0...) + (s1, 0, 0, 1...) + (x1 + y2 * s1 + s2, 1, 1, 1...) + + cannot be naturally embeded into Euclidean space. + cosever: a collection of countable parties, so the vector become inf. + or because protocol must stop, so the vector is finite. +---- + + Variables (x : {RV P -> VX})(x_ : (party * party * party)). + + The set of tuples should form as a partial function whose type would be: + f: {RV P -> TX} -> (A, B, C) + + (there are inf many RVs; + initially we have values for primitive RVs like x1, s1 and so on; + x1 maps to a specific tuple like (1, 0, 0) and so on for s1...; + we can gradullay add such mapping to functions. + ) + + f_x1 union f_x2 .... and then the final function knows more and more + mappings of tuples. + + Extensive function: function can accept parties one by one. + +---- + + (1, 0, 0, x1) --> x1 + +*) + + +Variable T : finType. +Variable P : R.-fdist T. +Variable TX : finComRingType. +Variable VX : lmodType TX. + +(* TODO: TX VX type issue (sum type?) *) + +HB.instance Definition _ := gen_eqMixin {RV P -> VX}. +HB.instance Definition _ := gen_choiceMixin {RV P -> VX}. + +From mathcomp Require Import finmap. + +Variables (x1 : {RV P -> VX})(x2 : {RV P -> VX}). + +Definition partymap := {fset ({RV P -> VX} * seq bool)%type}. + +Print cid. +Print constructive_indefinite_description. +About sigW. + +Hypothesis inde_between_parties : forall (f : partymap) (a b : {RV P -> VX}) (pa pb : seq bool), + (a, pa) \in f -> (b, pb) \in f -> foldr andb true (map (uncurry andb) (zip pa pb)) = false -> inde_rv a b. +Arguments inde_between_parties f [a b]. + +Local Open Scope fset_scope. + +Definition px1 : seq bool := [::true]. +Definition px2 : seq bool := [::false; true]. +Definition partymap_a : partymap := [fset (x1, px1); (x2, px2)]. + +Goal P |= x1 _|_ x2. +Proof. +apply: (inde_between_parties partymap_a px1 px2) => //. + by rewrite !inE eqxx. +by rewrite !inE eqxx orbT. +Qed. + +End indep. + diff --git a/smc/smc_proba.v b/smc/smc_proba.v new file mode 100644 index 00000000..25d2445f --- /dev/null +++ b/smc/smc_proba.v @@ -0,0 +1,418 @@ +(* infotheo: information theory and error-correcting codes in Coq *) +(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) + +From mathcomp Require Import all_ssreflect ssralg finalg ssrnum matrix. +From mathcomp Require Import reals Rstruct zmodp ring lra. +Require Import Reals. + +Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist. +Require Import proba jfdist_cond graphoid. + +Import GRing.Theory. +Import Num.Theory. + +(************************************************************************************) +(* SMC "Useful Tools" probability lemmas *) +(* *) +(* From: Information-theoretically Secure Number-product Protocol, *) +(* Sec. III.B "Useful Tools" *) +(* SHEN, Chih-Hao, et al. In: 2007 International Conference on Machine *) +(* Learning and Cybernetics. IEEE, 2007. p. 3006-3011. *) +(* *) +(************************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. + +Local Open Scope reals_ext_scope. +Local Open Scope proba_scope. +Local Open Scope fdist_scope. + +Section more_independent_rv_lemmas. + +Variables (A : finType) (P : R.-fdist A) (TA TB TC TD : finType). +Variables (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}). +Variables (UA UB UC: finType) (f : TA -> UA) (g : TB -> UB) (h : TC -> UC). + +Local Notation "f × g" := + (fun xy => (f xy.1, g xy.2)) (at level 10). + + +Lemma RV2_indeC : + P |= [% X, X] _|_ [% Z, Y] -> + P |= [% X, Y] _|_ [% X, Z]. +Proof. +rewrite /inde_rv => H [x1 y] [x2 z]. +rewrite coqRE. +rewrite [LHS]pr_eq_pairAC. +rewrite -[LHS]pr_eq_pairA. +have H1 := H (x1, x2) (z, y). +rewrite coqRE in H1. +rewrite -[LHS]pr_eq_pairA in H1. +Abort. + +(* Information-Theoretically Secure Number Protocol*) +(* Lemma 3.1 *) +Lemma inde_rv_comp (UB' TB' : finType) (g' : TB' -> UB')(Y' : {RV P -> TB'}): P|= X _|_ Y' -> P|= (f `o X) _|_ (g' `o Y'). +Proof. +move/inde_rv_events'. +rewrite /inde_rv_ev. +move=> H i j. +rewrite -[LHS]pr_eq_set1. +rewrite comp_RV2_ACA /=. +rewrite pr_in_comp'. +rewrite -setX1. +rewrite preimsetX. +rewrite H. (* second to third line in the pencil-paper proof *) +rewrite -!pr_in_comp'. +by rewrite !pr_eq_set1. +Qed. + +Lemma inde_RV2_comp : P|= X _|_ [% Y, Z] -> P|= (f `o X) _|_ [% (g `o Y), (h `o Z)]. +Proof. +pose gh := (fun '(y, z) => (g y, h z)). +have ->: [% g `o Y, h `o Z] = gh `o [%Y, Z] by []. +apply inde_rv_comp. +Qed. + +(* Lemma 3.2 *) +Lemma RV2_inde_rv_snd : P |= [% X, Y] _|_ Z -> P |= Y _|_ Z. +Proof. +move/inde_rv_events'. +move=> H y z. +rewrite -[LHS]pr_eq_set1 pr_inE'. +rewrite -(snd_RV2 X [% Y, Z]) Pr_fdist_snd. +rewrite -pr_inE'. +rewrite setTE -setX1. +rewrite pr_in_pairA. +rewrite H. +by rewrite -setTE pr_inE' -Pr_fdist_snd snd_RV2 -pr_inE' !pr_eq_set1. +Qed. + + +Lemma cpr_prd_unit_RV : X _|_ Y | [% unit_RV P, Z] -> X _|_ Y | Z. +Proof. +move=>H a b c. +have:=H a b (tt,c). +Undo 2. +move=> + a /[swap] b c. +Undo 1. +move=> + a b c => /(_ a b (tt,c)). +rewrite 3!cPr_eq_def. +have->: finset (preim [% unit_RV P, Z] (pred1 (tt, c))) = finset (preim Z (pred1 c)). + apply /setP => x. + by rewrite !inE. +by rewrite -!cPr_eq_def. +Qed. + +(* Lemma 3.3 *) +Lemma inde_RV2_cinde : P |= [% X, Z] _|_ Y -> X _|_ Y | Z. +Proof. +move/cinde_rv_unit /cinde_rv_sym. +move/weak_union /cinde_rv_sym. +by apply cpr_prd_unit_RV. +Qed. + +Lemma cpr_eqE_mul a b : + `Pr[ X = a | Y = b ] * `Pr[Y = b] = `Pr[ [% X, Y] = (a, b) ]. +Proof. +rewrite cpr_eqE. +rewrite !coqRE. +rewrite -!mulrA. +have [|?] := eqVneq `Pr[ Y = b ] 0. + move=>Y0. + rewrite Y0. + rewrite !mulr0. + rewrite pr_eq_pairC. + by rewrite pr_eq_domin_RV2. +rewrite mulVr //. +by rewrite mulr1. +Qed. + +Lemma inde_rv_cprP : P |= X _|_ Y <-> forall x y, `Pr[ Y = y ] != 0 -> `Pr[ X = x | Y = y] = `Pr[ X = x]. +Proof. +rewrite /inde_rv. +split. + move => H x y Hy. + move/(_ x y):H. (* bring back H and apply it with x and y*) + rewrite -cpr_eqE_mul. + rewrite coqRE. + by apply /mulIf. +move => H x y0. +rewrite -cpr_eqE_mul. +case /boolP: (`Pr[ Y = y0 ] == 0) => Hy. + rewrite (eqP Hy). + by rewrite mulR0 mulr0. +by rewrite H. +Qed. + + +End more_independent_rv_lemmas. + +Section XY. + +Variables (A : finType) (P : R.-fdist A) (TA TB: finType). +Variables (X : {RV P -> TA}) (Y : {RV P -> TB}). + +Lemma inde_rv_sym: P|= X _|_ Y <-> P|= Y _|_ X. +Proof. by split => /cinde_rv_unit/cinde_rv_sym/cinde_rv_unit. Qed. + +End XY. + +Section XYZ. + +Variables (A : finType) (P : R.-fdist A) (TA TB TC: finType). +Variables (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}). + +Lemma inde_RV2_sym : P|=[%X, Y] _|_ Z <-> P|=[%Y, X] _|_ Z. +Proof. by split => /cinde_rv_unit/cinde_rv_sym/cinde_drv_2C/cinde_rv_sym/cinde_rv_unit. Qed. + +End XYZ. + +Section lemma_3_4. + +Variables (T : finType) (A: finZmodType). +Variable P : R.-fdist T. +Variable n : nat. +Variables (X Y : {RV P -> A}). + +(* How to express "the distribution of random variable Y is uniform distribution" as a prop. *) +Hypothesis card_A : #|A| = n.+1. +Variable pY_unif : `p_ Y = fdist_uniform card_A. +Variable XY_indep : P |= X _|_ Y. + +(* Add two random variables = add results from two functions. *) +(* We use this because add_RV is in coqR *) +Definition add_RV : {RV P -> A} := X \+ Y. +Definition sub_RV : {RV P -> A} := X \- Y. +Definition neg_RV : {RV P -> A} := \0 \- X. + +Lemma add_RV_mul i : `p_ add_RV i = (\sum_(k <- fin_img X) `Pr[ X = k ] * `Pr[ Y = (i - k)%mcR ]). +Proof. +transitivity (`Pr[add_RV \in [set i]]). + by rewrite pr_inE' /Pr big_set1. +rewrite (reasoning_by_cases _ X). +transitivity (\sum_(k <- fin_img X) `Pr[ [% X, Y] \in ([set k] `* [set i-k]%mcR) ]). + apply eq_bigr=> k _. + rewrite !pr_eq_setE. + rewrite /Pr. + apply: eq_bigl. + move=>r /=. + rewrite !inE /=. + rewrite /add_RV. + rewrite andbC; apply: andb_id2l. + rewrite /=. + move /eqP ->. + rewrite [RHS]eq_sym. + by rewrite subr_eq addrC eq_sym. +under eq_bigr do rewrite setX1 pr_eq_set1 -cpr_eqE_mul. +under eq_bigr=> k _. + (* Similar to `have->:`, set the wanted form *) + rewrite (_ : _ * _ = `Pr[ X = k ] * `Pr[ Y = (i - k)%mcR ] ); last first. + rewrite cpr_eqE. (* To remove the form of conditional probability *) + rewrite XY_indep. (* So we can split it from `Pr [% X, Y] to `Pr X and `Pr Y*) + rewrite !coqRE. (* Because / and * are in stdlib, not in mathcomp *) + rewrite -!mulrA. + (* case analysis on (`Pr[ Y = (i - k)%mcR ] == 0) *) + have [|H] := eqVneq `Pr[ Y = (i - k)%mcR ] 0. + - by move->; rewrite !mulr0. + - by rewrite mulVr ?mulr1 //. + over. +under eq_bigr=> k _. + rewrite [X in _ * X]pr_eqE' /=. + rewrite -cpr_eq_unit_RV. + over. +done. +Qed. + +(* Lemma 3.4 *) +Lemma add_RV_unif : `p_ add_RV = fdist_uniform card_A . +Proof. +apply: fdist_ext=> /= i. +rewrite fdist_uniformE /=. +rewrite add_RV_mul. +under eq_bigr=> k _. + rewrite [X in _ * X]pr_eqE' pY_unif fdist_uniformE /=. + rewrite -cpr_eq_unit_RV. + over. +rewrite -big_distrl /=. (* Pull the const part `Pr[ Y = (i - k) ] from the \sum_k *) +by rewrite cPr_1 ?mul1r // pr_eq_unit oner_neq0. +Qed. + +End lemma_3_4. + +Global Arguments add_RV_unif [T A P n]. + +Notation "X `+ Y" := (add_RV X Y) : proba_scope. + +Section fdist_cond_prop. +Variables T TX TY TZ : finType. +Variables (P : R.-fdist T) (y : TY). +Variables (X : {RV P -> TX}) (Y : {RV P -> TY}) (Z : {RV P -> TZ}). + +Let E := finset (Y @^-1 y). +Hypothesis E0 : Pr P E != 0. + +Variable (X': {RV (fdist_cond E0) -> TX}). +Hypothesis EX' : X' = X :> (T -> TX). + +Lemma Pr_fdist_cond_RV x : `Pr[ X' = x ] = `Pr[ X = x | Y = y ]. +Proof. by rewrite pr_eqE Pr_fdist_cond cPr_eq_def EX'. Qed. + +Hypothesis Z_XY_indep : inde_rv Z [%X, Y]. + +Lemma fdist_cond_indep : fdist_cond E0 |= X _|_ Z. +Proof. +move: Z_XY_indep => /cinde_rv_unit /weak_union. +rewrite /cinde_rv /= => H. +move => /= x z. +rewrite mulRC pr_eq_pairC. +have := H z x (tt,y). +rewrite !pr_eqE !Pr_fdist_cond !cPr_eq_def. +have -> // : finset (preim [% unit_RV P, Y] (pred1 (tt, y))) = E. +by apply/setP => e; rewrite !inE. +Qed. +End fdist_cond_prop. + +Section lemma_3_5. + +Variable (T TY: finType) (TZ: finZmodType). +Variable P : R.-fdist T. +Variable n : nat. + +Variables (X Z: {RV P -> TZ}) (Y : {RV P -> TY} ). +Let XZ : {RV P -> TZ} := X `+ Z. + +Hypothesis card_TZ : #|TZ| = n.+1. +Hypothesis pZ_unif : `p_ Z = fdist_uniform card_TZ. + +Variable Z_XY_indep : inde_rv Z [%X, Y]. + +Let Z_X_indep : inde_rv Z X. +Proof. exact/cinde_rv_unit/decomposition/cinde_rv_unit/Z_XY_indep. Qed. +Let Z_Y_indep : inde_rv Z Y. +Proof. exact/cinde_rv_unit/decomposition/cinde_drv_2C/cinde_rv_unit/Z_XY_indep. +Qed. + + +Section iy. +Variables (i : TZ) (y : TY). +Let E := finset (Y @^-1 y). +Hypothesis Y0 : Pr P E != 0. + +Let X': {RV (fdist_cond Y0) -> TZ} := X. +Let Z': {RV (fdist_cond Y0) -> TZ} := Z. +Let XZ': {RV (fdist_cond Y0) -> TZ} := X' `+ Z'. + + +Lemma lemma_3_5 : `Pr[ XZ = i | Y = y] = `Pr[ XZ = i]. (* The paper way to prove P |= X\+Z _|_ Y *) +Proof. +rewrite -(Pr_fdist_cond_RV (X':=XZ')) //. +rewrite pr_eqE' (@add_RV_mul _ _ _ X' Z'); last exact: fdist_cond_indep. +under eq_bigr => k _. + rewrite (Pr_fdist_cond_RV (X:=X)) //. + rewrite (Pr_fdist_cond_RV (X:=Z)) //. + rewrite [X in _ * X]cpr_eqE. + rewrite Z_Y_indep. + rewrite -[(_/_)%coqR]mulRA mulRV; last by rewrite pr_eqE. + rewrite mulR1 [X in _ * X]pr_eqE' pZ_unif fdist_uniformE /=. + over. +rewrite -big_distrl /=. (* Pull the const part `Pr[ Y = (i - k) ] from the \sum_k *) +rewrite /X' cPr_1 ?mul1r //; last by rewrite pr_eqE. +rewrite pr_eqE' (add_RV_unif X Z (card_TZ)) //. +- by rewrite fdist_uniformE. +- rewrite /inde_rv /= => /= x z. + rewrite mulRC pr_eq_pairC. (* Swap X _|_ Z to Z _|_ X so we can apply Z_X_indep *) + exact: Z_X_indep. +Qed. + +End iy. + +Lemma lemma_3_5' : P |= XZ _|_ Y. +Proof. +apply/inde_rv_cprP. +move => /= x y0 Hy. +rewrite lemma_3_5 //. +by rewrite -pr_eqE. +Qed. + +End lemma_3_5. + +Section lemma_3_6. + +Variables (T TY TX : finType)(TZ : finZmodType). +Variable P : R.-fdist T. +Variable n : nat. +Variables (i : TZ) (x1 : TX) (y : TY). +(* X2 means X2 to Xn-1 *) +Variables (X2 : {RV P -> TY}) (X1 : {RV P -> TX}) (Xn Z : {RV P -> TZ}). + +Hypothesis card_TZ : #|TZ| = n.+1. +Variable pZ_unif : `p_ Z = fdist_uniform card_TZ. +Variable Z_Xs_indep : inde_rv Z [%X1, X2, Xn]. +Variable Z_X1X2_indep : inde_rv Z [%X1, X2]. +Let XnZ := Xn `+ Z. + +Hypothesis X0 : `Pr[ [% XnZ, X2] = (i, y) ] != 0. + +Lemma lemma_3_6 : `Pr[ X1 = x1 | [% X2, XnZ] = (y , i)] = `Pr[ X1 = x1 | X2 = y]. +Proof. +have:= inde_RV2_cinde (X:=X1) (Z:=X2) (Y:=XnZ). +move => H. +rewrite cpr_eq_pairCr. +apply: cinde_alt. +rewrite (inde_RV2_sym X1 X2 XnZ) in H. +apply: H. +rewrite inde_RV2_sym. +rewrite inde_rv_sym. +have:= (@lemma_3_5' _ _ TZ P n Xn Z [% X1, X2] card_TZ pZ_unif). +apply. +apply/cinde_rv_unit. +apply: cinde_drv_2C. +by apply/cinde_rv_unit. +exact: X0. +Qed. + +End lemma_3_6. + +Section theorem_3_7. + +Variables (T TX TY1 TY2: finType)(TZ: finZmodType). +Variable P : R.-fdist T. +Variable n : nat. +Variables (X: {RV P -> TX}) (Z : {RV P -> TZ}). +Variables (f1 : TX -> TY1) (f2 : TX -> TY2) (fm : TX -> TZ). + +Variable Z_X_indep : inde_rv Z X. + +Let Y1 := f1 `o X. +Let Y2 := f2 `o X. (* y2...ym-1*) +Let Ym := fm `o X. +Let YmZ := Ym `+ Z. +Let f x := (f1 x, f2 x, fm x). +Let Y := f `o X. + +Hypothesis card_TZ : #|TZ| = n.+1. +Variable pZ_unif : `p_ Z = fdist_uniform card_TZ. + +(* Theorem 3.7: masked_condition_removal *) +Theorem mc_removal_pr y1 y2 ymz: + `Pr[ [% Y2, Ym `+ Z] = (y2, ymz) ] != 0 -> + `Pr[Y1 = y1|[%Y2, YmZ] = (y2, ymz)] = `Pr[Y1 = y1 | Y2 = y2]. +Proof. +have H:= (@lemma_3_6 _ _ _ TZ _ n ymz y1 y2 Y2 Y1 Ym Z card_TZ). +rewrite pr_eq_pairC in H. +apply H. +apply: pZ_unif. +rewrite (_:[%_ , _] = Y) //. +rewrite (_:Z = idfun `o Z) //. (* id vs. idfun*) +exact: inde_rv_comp. +Qed. + +(*TODO: the Entropy part needs to be done in another file, not inside the probability directory. *) + + +End theorem_3_7. diff --git a/smc/smc_tactics.v b/smc/smc_tactics.v new file mode 100644 index 00000000..a5cf12e0 --- /dev/null +++ b/smc/smc_tactics.v @@ -0,0 +1,103 @@ +From Ltac2 Require Import Ltac2. +From Ltac2 Require Option. +From Ltac2 Require Import Message. +From HB Require Import structures. +Require Import Reals. +From mathcomp Require Import all_ssreflect all_algebra fingroup finalg matrix. +From mathcomp Require Import Rstruct ring. +Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist. +Require Import proba jfdist_cond entropy graphoid smc_proba. + +Import GRing.Theory. +Import Num.Theory. +Set Implicit Arguments. +Unset Strict Implicit. +Import Prenex Implicits. + +Local Open Scope ring_scope. +Local Open Scope reals_ext_scope. +Local Open Scope proba_scope. +Local Open Scope fdist_scope. +Local Open Scope chap2_scope. +Local Open Scope entropy_scope. +Local Open Scope vec_ext_scope. + +Ltac2 bar () := let x := '(3+4) in constr:($x + 5). + +Ltac2 show_type () := + (* this is desugared into something more primitive from Pattern *) + match! goal with + | [ |- forall _ : ?e, _ ] => + (*Memo: note how it pattern match the goal and use the symbol inside.*) + Message.print (Message.of_constr e) + end. + +Goal forall (n:nat), n = n. +Proof. + show_type (). +Abort. + + +(* Maybe: Goal is `[% vecRV_a, vecRV_b, oneRV_a, oneRV_b...] _|_ rv` + Define a tactic to automatically generate sub-goals: vec_RV_a _|_ rv , vecRV_b _|_ rv... + Meanwhile, we need a lemma to show that mutual independence implies pairwise independence. + + Not sure if we really need Ltac, though. If we can generate arbitrary sub-goals in other ways? +*) + +Section boole. + +Variables (A: finType)(m n: nat)(P : R.-fdist A). +Variables (TX VX: finType). +Variables (x1 x2 s1 s2: {RV P -> TX})(y1 r1: {RV P -> VX}). + +Inductive boole := fact | lie. + +Ltac2 rec print_list x := match x with +| a :: t => print (of_constr a); print_list t +| [] => () +end. +Ltac2 Notation "ex2" x(list1(constr, ",")) := print_list x. +Goal true. +Proof. +ex2 [%x1, r1, s2]. +ex2 x1, r1, s2. +Abort. +End boole. + + +Ltac RVs_to_tuple vs := + let rec iter vs := + match vs with + | RV2 ?x ?y => + let ires := iter x in + constr: ((ires, y)) + | ?z => z + end in + iter vs. + +Ltac apply_inde_rv_comp f g := + match goal with + | [ |- _ |= ?v1l _|_ ?v1r -> _ |= ?v2l _|_ ?v2r ] => + let H := fresh "H" in + move => H; + (have-> : v2l = f `o v1l by apply: boolp.funext => ? //=); + (have-> : v2r = g `o v1r by apply: boolp.funext => ? //=); + exact: (inde_rv_comp f g H) + | _ => + fail + end. + +(* +Section test. +Variables (A: finType)(m n: nat)(P : R.-fdist A). +Variables (TX VX: finType). +Variables (x1 x2 s1 s2: {RV P -> TX})(y1 r1: {RV P -> VX}). + +Ltac test vs := + let result := RVs_to_tuple vs in + idtac result. + +Eval cbv in ltac: (test [% x1, x2]). +End test. +*)