Lemma Statistics

322
Total Lemmas
47
Main Results
275
Helper Lemmas
22
Files
10,609
Lines
bec7c86
Source Commit

Main Results

Theorems and key lemmas (47 total)

▶ dumas2017dual/dsdp/dsdp_correctness.v
2 main
Name Section Lines Signature Meaning
Theorem dsdp_computes_dot_product_benaloh dsdp_computational_benaloh 1 Theorem dsdp_computes_dot_product_benaloh : @alice_result AHE v1 v2 v3 u1 u2 u3 r2 r3 = u1 * v1 + u2 * v2 + u3 * v3. Main theorem: DSDP computes the dot product using Benaloh encryption
Theorem dsdp_computes_dot_product_paillier dsdp_computational_paillier 1 Theorem dsdp_computes_dot_product_paillier : @alice_result AHE v1 v2 v3 u1 u2 u3 r2 r3 = u1 * v1 + u2 * v2 + u3 * v3. Main theorem: DSDP computes the dot product using Paillier encryption
▶ dumas2017dual/dsdp/dsdp_entropy.v
3 main
Name Section Lines Signature Meaning
Theorem dsdp_centropy_uniform dsdp_entropy 22 Theorem dsdp_centropy_uniform : (forall t, (0 < U3 t)%N) -> (forall t, (U3 t < minn p q)%N) -> `H(VarRV | CondRV) = log (m%:R : R). This establishes that Alice learns nothing beyond the constraint.
Theorem dsdp_centropy_uniform_n dsdp_entropy_n 22 Theorem dsdp_centropy_uniform_n : (forall t, (0 < val (u_of_cond (CondRV t) ord_max))%N) -> (forall t, (val (u_of_cond (CondRV t) ord_max) < minn p q)%N) -> `H(VarRV | CondRV) = log ((m ^ n_relay)%:R : R). Main N-party entropy result: H(V_relay | CondRV) = log(m^n_relay) where V_relay are the relay parties' private inputs.
Main V3_determined functional_determination 18 Lemma V3_determined : V3 = compute_v3 `o [% V1, U1, U2, U3, S, V2]. V3 is functionally determined by the other variables via the constraint. Given V1, U1, U2, U3, S, V2, we can compute: V3 = (S - U2*V2 - U1*V1) / U3. This is key for showing H(V2,V3|constraint) = H(V2|constraint). For Z/pqZ (ring, not field), we use: - U3 is a unit because coprime (val U3) m - Division by unit: x / y = x * y^-1 - Inverse property: y^-1 * y = 1 when y is unit
▶ dumas2017dual/dsdp/dsdp_entropy_trace.v
1 main
Name Section Lines Signature Meaning
Theorem dsdp_result_correct dsdp_traces 1 Theorem dsdp_result_correct : v3 * u3 + r3 + (v2 * u2 + r2) - r2 - r3 + u1 * v1 = u1 * v1 + u2 * v2 + u3 * v3. Protocol correctness is now proved algebraically using ring arithmetic. The final result S = v3*u3 + r3 + (v2*u2 + r2) - r2 - r3 + u1*v1 simplifies to u1*v1 + u2*v2 + u3*v3 by ring.
▶ dumas2017dual/dsdp/dsdp_pismc.v
3 main
Name Section Lines Signature Meaning
Theorem dsdp_ideal_senv_zero dsdp_idealized_termination 10 Theorem dsdp_ideal_senv_zero traces : exists aps' : seq (aproc dsdp_dtype data), erase_aprocs aps' = (interp [> dsdp_ideal_saprocs] dsdp_ideal_procs traces).1 /\ aprocs_senv_depth [:: 0; 1; 2] aps' = 0. Main theorem: DSDP (Idealized) session environment converges to empty.
Theorem dsdp_n4_senv_zero dsdp_n4_idealized_duality 10 Theorem dsdp_n4_senv_zero traces : exists aps' : seq (aproc dsdp_dtype data), erase_aprocs aps' = (interp [> dsdp_n4_saprocs] dsdp_n4_procs traces).1 /\ aprocs_senv_depth [:: 0; 1; 2; 3] aps' = 0. 4-party session environment convergence
Theorem dsdp_3party_rsteps dsdp_3party_rsteps 6 Theorem dsdp_3party_rsteps : exists final traces, rsteps procs3 final traces /\ all_terminated (tval final) /\ all_nonfail (tval final). Main theorem: the 3-party protocol admits an rsteps reduction
▶ dumas2017dual/dsdp/dsdp_program.v
2 main
Name Section Lines Signature Meaning
Theorem dsdp_computes_dot_product dsdp 4 Theorem dsdp_computes_dot_product : alice_result = u1 * v1 + u2 * v2 + u3 * v3. Main correctness theorem: Alice computes the dot product
Theorem dsdp_computes_dot_product_n dsdp_n 4 Theorem dsdp_computes_dot_product_n : alice_result_n = \sum_(i < n_relay.+2) u i * v i. N-party correctness: Alice computes the dot product
▶ dumas2017dual/dsdp/dsdp_security.v
20 main
Name Section Lines Signature Meaning
Theorem dsdp_constraint_centropy_eqlogm dsdp_security 13 Theorem dsdp_constraint_centropy_eqlogm : `H(VarRV | CondRV) = log (m%:R : R). Core entropy bound: H((V2,V3) | constraint view) = log(m). Instantiates the general DSDP entropy analysis with security hypotheses. Shows Alice learns exactly log(m) bits about Bob/Charlie's joint input, not the full log(m^2) bits - proving entropic security.
Theorem dsdp_entropic_security dsdp_security 17 Theorem dsdp_entropic_security : `H(V2 | AliceView) = log (m%:R : R) /\ `H(V2 | AliceView) > 0. DSDP entropic security: H(V2 | AliceView) = log(m) = H(V2) > 0. Since log(m) is the maximum entropy for V2 over Z/pqZ, this means Alice's view is statistically independent of V2: individual secrets enjoy perfect privacy in the sense of Dodis-Smith entropic security.
Main ConstUS_discloses_V2 malicious_adversary_case_analysis 5 Lemma ConstUS_discloses_V2 : US = ConstUS -> Dotp2_rv VS US = V2. If an active adversary controls Alice, force `us` always output `(1, 0)`, then the key privacy premise `v2 _|_ dotp2_rv us vs` is impossible. In contrast, if Alice is an fair player, the probability that `us` outputs that specific value `(1, 0)` is 1/m^2. Finally, if Bob enforce ZPK check to abort the protocol when that value is generated, `v2 _|_ dotp2_rv us vs` is guaranteed, and the protocol is secure with that mitigation ("security with abort") \cite[\S5.2]{dumas2017dual}. Therefore, here we examine the compromised case: `us = (1, 0) -> ~ v2 _|_ dotp2_rv us vs` and the secure case: `us != (1, 0) -> v2 _|_ dotp2_rv us vs`.
Theorem US_compromised_leaks_V2 malicious_adversary_case_analysis 37 Theorem US_compromised_leaks_V2 : US = ConstUS -> ~ `H(V2 | AliceView ) = `H `p_V2. This theorem shows that if an active adversary controls Alice, it can set U1 and U2 as a special combination (1, 0), which allows revealing `V2` from the result that Alice receives. \cite[\S5.2]{dumas2017dual}.
Theorem BobView_indep_V1_proven bob_security_independence 11 Theorem BobView_indep_V1_proven : P |= BobView _|_ V1. Main theorem: BobView is independent of V1
Theorem BobView_indep_V3_proven bob_security_independence 11 Theorem BobView_indep_V3_proven : P |= BobView _|_ V3. Main theorem: BobView is independent of V3
Theorem bob_privacy_V1_alt bob_security 3 Theorem bob_privacy_V1_alt : `H(V1 | BobView) = `H `p_ V1. Bob cannot learn V1 - complete privacy. Alternative formulation: H(V1 | BobView) = H(V1) This directly expresses that conditioning on BobView reveals nothing about V1, i.e., observing Bob's view does not reduce uncertainty about Alice's private input V1. Mathematical reasoning: - BobView _|_ V1 (independence hypothesis) - By definition of independence: observing BobView gives no information about V1 - Therefore: H(V1 | BobView) = H(V1)
Theorem bob_privacy_V1 bob_security 10 Theorem bob_privacy_V1 : `H(V1 | BobView) = log (m%:R : R) /\ `H(V1 | BobView) > 0. Bob cannot learn V1 - complete privacy (concrete entropy value)
Theorem bob_privacy_V3_alt bob_security 3 Theorem bob_privacy_V3_alt : `H(V3 | BobView) = `H `p_ V3. Bob cannot learn V3 - complete privacy. Alternative formulation: H(V3 | BobView) = H(V3) This directly expresses that conditioning on BobView reveals nothing about V3, i.e., observing Bob's view does not reduce uncertainty about Charlie's private input V3. Mathematical reasoning: - BobView _|_ V3 (independence hypothesis) - By definition of independence: observing BobView gives no information about V3 - Therefore: H(V3 | BobView) = H(V3)
Theorem bob_privacy_V3 bob_security 10 Theorem bob_privacy_V3 : `H(V3 | BobView) = log (m%:R : R) /\ `H(V3 | BobView) > 0. Bob cannot learn V3 - complete privacy (concrete entropy value)
Theorem CharlieView_indep_V2_proven charlie_security_independence 18 Theorem CharlieView_indep_V2_proven : P |= CharlieView _|_ V2. Main theorem: CharlieView is independent of V2
Main D3_indep_V1 charlie_security_independence 24 Lemma D3_indep_V1 : P |= D3 _|_ V1. Main lemma: D3 is independent of V1
Theorem CharlieView_indep_V1_proven charlie_security_independence 11 Theorem CharlieView_indep_V1_proven : P |= CharlieView _|_ V1. Main theorem: CharlieView is independent of V1
Theorem charlie_privacy_V1_alt charlie_security 3 Theorem charlie_privacy_V1_alt : `H(V1 | CharlieView) = `H `p_ V1. Charlie cannot learn V1 - complete privacy. Alternative formulation: H(V1 | CharlieView) = H(V1) This directly expresses that conditioning on CharlieView reveals nothing about V1, i.e., observing Charlie's view does not reduce uncertainty about Alice's private input V1. Mathematical reasoning: - CharlieView _|_ V1 (independence hypothesis) - By definition of independence: observing CharlieView gives no information about V1 - Therefore: H(V1 | CharlieView) = H(V1)
Theorem charlie_privacy_V1 charlie_security 10 Theorem charlie_privacy_V1 : `H(V1 | CharlieView) = log (m%:R : R) /\ `H(V1 | CharlieView) > 0. Charlie cannot learn V1 - complete privacy (concrete entropy value)
Theorem charlie_privacy_V2_alt charlie_security 3 Theorem charlie_privacy_V2_alt : `H(V2 | CharlieView) = `H `p_ V2. Charlie cannot learn V2 - complete privacy. Alternative formulation: H(V2 | CharlieView) = H(V2) This directly expresses that conditioning on CharlieView reveals nothing about V2, i.e., observing Charlie's view does not reduce uncertainty about Bob's private input V2. Mathematical reasoning: - CharlieView _|_ V2 (independence hypothesis) - By definition of independence: observing CharlieView gives no information about V2 - Therefore: H(V2 | CharlieView) = H(V2) This is more fundamental than stating H(V2|CharlieView) = log(m), as it captures the independence relationship directly.
Theorem charlie_privacy_V2 charlie_security 10 Theorem charlie_privacy_V2 : `H(V2 | CharlieView) = log (m%:R : R) /\ `H(V2 | CharlieView) > 0. Charlie cannot learn V2 - complete privacy (concrete entropy value)
Theorem enc_ce_contract_ind enc_contraction_n 4 Theorem enc_ce_contract_ind {C : finType} (Z : {RV P -> C}) (target : R) {A : finType} (View : {RV P -> A}) : enc_contractible Z target View -> `H(Z | View) = target. Contraction theorem: if a view is enc_contractible, its conditional entropy equals the target
Theorem dsdp_entropic_security_n_eq dsdp_security_n 1 Theorem dsdp_entropic_security_n_eq : `H(VarRV | AliceView) = log ((m ^ n_relay)%:R : R). Core N-party entropic security: entropy value
Theorem dsdp_entropic_security_n dsdp_security_n 9 Theorem dsdp_entropic_security_n : (0 < n_relay)%N -> `H(VarRV | AliceView) = log ((m ^ n_relay)%:R : R) /\ `H(VarRV | AliceView) > 0. Core N-party entropic security: entropy is positive when n_relay > 0
▶ dumas2017dual/entropy_fiber/entropy_fiber.v
4 main
Name Section Lines Signature Meaning
Main centropy1_uniform_over_set general_pointwise_entropy 22 Lemma centropy1_uniform_over_set (S : {set DomainT}) (c : CodomainT) : `Pr[Y = c] != 0 -> (forall x, x \in S -> `Pr[X = x | Y = c] = #|S|%:R^-1) -> (forall x, x \notin S -> `Pr[X = x | Y = c] = 0) -> (0 < #|S|)%N -> `H[X | Y = c] = log (#|S|%:R : R). General pointwise conditional entropy when distribution is uniform over a set. KEY: This does NOT require Y = f `o X - works for any relationship between X and Y, making it applicable to DSDP and other protocols where the conditioning variable is not simply a function of the variable of interest. Usage: When X is uniformly distributed over set S given Y = c, and has zero probability outside S, the conditional entropy equals log(|S|).
Main centropy1_as_sum fiber_entropy 8 Lemma centropy1_as_sum (c : CodomainT) : `Pr[Y = c] != 0 -> `H[X | Y = c] = - \sum_(x : DomainT) `Pr[X = x | Y = c] * log (`Pr[X = x | Y = c]). Conditional entropy expanded as negative sum of p*log(p) over domain.
Main centropy1_uniform_fiber fiber_entropy 6 Lemma centropy1_uniform_fiber (c : CodomainT) : `Pr[Y = c] != 0 -> let fiber_c := fiber f c in (forall x, x \in fiber_c -> `Pr[X = x | Y = c] = #|fiber_c|%:R ^-1) -> (forall x, x \notin fiber_c -> `Pr[X = x | Y = c] = 0) -> (0 < #|fiber_c|)%N -> `H[X | Y = c] = log (#|fiber_c|%:R : R). If X is uniform over fiber(c) given Y=c, then H(X|Y=c) = log|fiber(c)|. Key lemma for computing conditional entropy via fiber cardinality.
Main centropy_determined_contract functional_determinacy 17 Lemma centropy_determined_contract : `H([% X, Y] | Cond) = `H(X | Cond). Main result: auxiliary variable adds no entropy
▶ dumas2017dual/entropy_fiber/entropy_fiber_zpq.v
1 main
Name Section Lines Signature Meaning
Main cPr_uniform_fiber conditional_probability 39 Lemma cPr_uniform_fiber (cond : CondT) (v : msg * msg) : `Pr[CondRV = cond] != 0 -> v \in fiber cond -> `Pr[VarRV = v | CondRV = cond] = #|fiber cond|%:R^-1. * Uniform conditional probability over fiber. Pr[VarRV = v | CondRV = cond] = |fiber(cond)|^-1 When: 1. VarRV is uniform over msg × msg 2. VarRV is independent of InputRV 3. The conditioning event has positive probability 4. v is in the fiber of cond This is the key lemma for deriving entropy bounds in protocols where the constraint creates a fiber structure.
▶ dumas2017dual/entropy_fiber/linear_fiber_zpq.v
2 main
Name Section Lines Signature Meaning
Main linear_fiber_2d_card fiber_2d 21 Lemma linear_fiber_2d_card (u2 u3 target : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> #|linear_fiber_2d u2 u3 target| = m. Main result: 2D fiber cardinality = m via CRT
Main linear_fiber_nd_card fiber_nd 15 Lemma linear_fiber_nd_card (u : 'I_n.+1 -> msg) (target : msg) : (0 < val (u ord_max))%N -> (val (u ord_max) < minn p q)%N -> #|linear_fiber_nd u target| = (m ^ n)%N. Main result: N-dimensional fiber cardinality = m^n
▶ dumas2017dual/lib/extra_algebra.v
1 main
Name Section Lines Signature Meaning
Main coprime_Zp_unit Zp_unit_extra 6 Lemma coprime_Zp_unit (m : nat) (x : 'Z_m) : (1 < m)%N -> coprime x m -> x \is a GRing.unit. Key lemma from MathComp: unitZpE (x%:R : 'Z_m) \is a GRing.unit = coprime m x (when 1 < m) For x : 'Z_m, we have x = (nat_of_ord x)%:R, so we can apply unitZpE directly.
▶ dumas2017dual/lib/extra_entropy.v
3 main
Name Section Lines Signature Meaning
Main cinde_centropy_eq cinde_centropy_eq 13 Lemma cinde_centropy_eq : P |= X _|_ Y | Z -> `H(Y | [% X, Z]) = `H(Y | Z). Main result: conditional independence implies conditional entropy equality
Main zero_centropy_eq_deterministic1 zero_centropy_eq_point_mass 64 Lemma zero_centropy_eq_deterministic1 (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) : `H(Z | Y) = 0 <-> (forall y, `Pr[Y = y] != 0 -> exists z, `Pr[Z = z | Y = y] = 1). Main lemma 1: conditional entropy is zero iff Z is a function of Y
Main zero_centropy_eq_deterministic zero_centropy_eq_point_mass 29 Lemma zero_centropy_eq_deterministic (V W T: finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) : `H(Z | Y) = 0 <-> (forall y, `Pr[Y = y] != 0 -> exists! z, `Pr[Z = z | Y = y] = 1). Main lemma: conditional entropy zero means Z is a unique function of Y
▶ dumas2017dual/lib/rouche_capelli.v
4 main
Name Section Lines Signature Meaning
Main card_vspace finvect_lemmas 1 Lemma card_vspace (K : finFieldType) (fvT : finVectType K) (U : {vspace fvT}) : #|U| = (#| {:K} | ^ (\dim U))%N. Cardinality of a vector subspace: |U| = |K|^dim(U). Fundamental result: a d-dimensional subspace over finite field K has |K|^d elements. This is the key formula for counting solutions to linear systems.
Main mxrank_sub_eqmx RoucheCapelliTheorems 3 Lemma mxrank_sub_eqmx m n p (A : 'M[R]_(m,n)) (B : 'M[R]_(p,n)) : \rank A = \rank B -> (A <= B)%MS -> (A == B)%MS. Equal rank + submx implies equivalence: if rank(A) = rank(B) and A ≤ B, then A ≡ B. Key lemma for establishing row space equality.
Main count_affine_solutions_explicit affine_solution_counting 6 Lemma count_affine_solutions_explicit (x0 : 'rV[K]_m) : x0 *m A = b -> #|affine_solutions| = (#|{:K}| ^ (m - \rank A))%N. Explicit affine solution count: |{x | xA = b}| = |K|^(m - rank(A)). Combines count_affine_solutions with count_kernel_vectors. This is the main Rouché-Capelli counting formula for row systems.
Main count_affine_solutions_explicit_col affine_solultion_counting_col 6 Lemma count_affine_solutions_explicit_col (v0 : 'cV[K]_n) : A *m v0 = b -> #|affine_solutions_col| = (#|{:K}| ^ (n - \rank A))%N. Explicit affine count (column version): |{v | Av = b}| = |K|^(n - rank(A)). Main Rouché-Capelli formula for Av = b systems. Used in DSDP fiber counting where constraints are expressed as column multiplication.
▶ homomorphic_encryption/paillier1999/paillier_enc.v
1 main
Name Section Lines Signature Meaning
Main paillier_dec_correct paillier_params 10 Lemma paillier_dec_correct (m : 'Z_n) (r : {unit 'Z_n2}) : paillier_dec lambda (paillier_enc m r) = Some m. Decryption with the canonical key recovers the original message

Helper Lemmas

Supporting lemmas and utilities (275 total)

▶ dumas2017dual/dsdp/dsdp_correctness.v
3 helper
Name Section Lines Signature Meaning
Helper dsdp_ok dsdp_computational 1 Lemma dsdp_ok : dsdp 15 = ([:: Finish; Finish; Finish], [:: [:: d (v3 * u3 + r3 + (v2 * u2 + r2) - r2 - r3 + u1 * v1); e (v3 * u3 + r3 + (v2 * u2 + r2)); e v3; e v2; d r3; d r2; d u3; d u2; d u1; d v1; k dk_a]; [:: e (v3 * u3 + r3); e (v2 * u2 + r2); d v2; k dk_b]; [:: e (v3 * u3 + r3 + (v2 * u2 + r2)); d v3; k dk_c] ]). Protocol execution result: running dsdp for 15 steps produces the expected final state with all parties finished and their respective traces. In the idealized scheme, enc(pk, m, r) = m, so ciphertexts are just messages.
Helper dsdp_traces_ok dsdp_computational 1 Lemma dsdp_traces_ok : dsdp_traces = [tuple [bseq d (v3 * u3 + r3 + (v2 * u2 + r2) - r2 - r3 + u1 * v1); e (v3 * u3 + r3 + (v2 * u2 + r2)); e v3; e v2; d r3; d r2; d u3; d u2; d u1; d v1; k dk_a]; [bseq e (v3 * u3 + r3); e (v2 * u2 + r2); d v2; k dk_b]; [bseq e (v3 * u3 + r3 + (v2 * u2 + r2)); d v3; k dk_c]]. Trace structure: each party's trace contains their view of the protocol.
Helper dsdp_is_correct dsdp_computational 1 Lemma dsdp_is_correct: is_dsdp dsdp_traces. Protocol correctness: the final result S satisfies S = u1*v1 + u2*v2 + u3*v3.
▶ dumas2017dual/dsdp/dsdp_entropy.v
11 helper
Name Section Lines Signature Meaning
Helper dsdp_fiber_card dsdp_entropy 5 Lemma dsdp_fiber_card (u1 u2 u3 v1 s : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> #|dsdp_fiber u1 u2 u3 v1 s| = m. Fiber cardinality for full constraint
Helper Pr_dsdp_nosol_eq0 dsdp_entropy 17 Lemma Pr_dsdp_nosol_eq0 (u1 u2 u3 v1 s : msg) (v2 v3 : msg) : `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> (v2, v3) \notin dsdp_fiber u1 u2 u3 v1 s -> `Pr[ VarRV = (v2, v3) | CondRV = (v1, u1, u2, u3, s) ] = 0. Non-solutions have zero probability
Helper Pr_dsdp_sol_uniform dsdp_entropy 15 Lemma Pr_dsdp_sol_uniform (u1 u2 u3 v1 s : msg) (v2 v3 : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> (v2, v3) \in dsdp_fiber u1 u2 u3 v1 s -> `Pr[ VarRV = (v2, v3) | CondRV = (v1, u1, u2, u3, s) ] = m%:R^-1. Solutions have uniform probability. Instantiates cPr_uniform_fiber from entropy_fiber_zpq.v with DSDP structure.
Helper dsdp_centropy1_uniform dsdp_entropy 20 Lemma dsdp_centropy1_uniform (v1 u1 u2 u3 s : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> `Pr[CondRV = (v1, u1, u2, u3, s)] != 0 -> `H[ VarRV | CondRV = (v1, u1, u2, u3, s) ] = log (m%:R : R). Helper: Each conditioning value gives entropy log(m). Uses centropy1_uniform_over_set directly with DSDP-specific probability lemmas.
Helper dsdp_var_entropy dsdp_var_entropy 5 Lemma dsdp_var_entropy : `p_VarRV = fdist_uniform card_msg_pair -> `H `p_VarRV = log (m%:R * m%:R : R). Unconditional entropy of private inputs (V2, V3) when uniformly distributed. Since V2, V3 are private inputs from Bob and Charlie respectively, assuming uniform distribution gives H(V2,V3) = log(m²) = 2*log(m). Combined with the conditional entropy result H(V2,V3 | view) = log(m), this shows DSDP leaks log(m) bits but preserves log(m) bits of entropy. The security argument (joint_centropy_reduction at end of file) shows that H(V2,V3 | AliceView) = H(V2 | AliceView), i.e., knowing V3 given the constraint adds no information beyond knowing V2.
Helper dsdp_fiber_card_n dsdp_entropy_n 9 Lemma dsdp_fiber_card_n (v0 u0 s : msg) (u_rel : {ffun 'I_n_relay.+1 -> msg}) : (0 < val (u_rel ord_max))%N -> (val (u_rel ord_max) < minn p q)%N -> #|dsdp_fiber_fn_n (v0, u0, u_rel, s)| = (m ^ n_relay)%N. Fiber cardinality for N-party
Helper dsdp_centropy1_uniform_n dsdp_entropy_n 29 Lemma dsdp_centropy1_uniform_n (v0 u0 s : msg) (u_rel : {ffun 'I_n_relay.+1 -> msg}) : (0 < val (u_rel ord_max))%N -> (val (u_rel ord_max) < minn p q)%N -> `Pr[CondRV = (v0, u0, u_rel, s)] != 0 -> `H[ VarRV | CondRV = (v0, u0, u_rel, s) ] = log ((m ^ n_relay)%:R : R). Per-conditioning-value entropy
Helper U3_nonzero functional_determination 11 Lemma U3_nonzero : forall t, U3 t != 0. If U3 gives zero, the adversary is not semi-honest, there fore this constraint fits the security model assumption.
Helper V3_determined_centropy_v2 functional_determination 14 Lemma V3_determined_centropy_v2 : `H([% V2, V3] | [% V1, U1, U2, U3, S]) = `H(V2 | [% V1, U1, U2, U3, S]). * * Fundamental Principle of Constraint-Based Security When an auxiliary variable is functionally determined by a secret and a constraint, the joint entropy equals the secret's entropy alone. This formalizes the principle that "knowing possible solution pairs gives exactly the same information as knowing the constraint on the secret." This principle underlies many MPC protocols where: - [V2] is the secret to protect - [V3] is an auxiliary/helper variable - [S, U2, U3] form a constraint linking them - Given constraint, [v3] is determined by [V2] (or vice versa)
Helper alice_view_to_cond semi_honest_case_analysis 74 Lemma alice_view_to_cond (A : finType) (Xvar : {RV P -> A}) : (P |= [% Dk_a, R2, R3] _|_ Xvar | [% V1, U1, U2, U3, S]) -> `H(Xvar | AliceView) = `H(Xvar | [% V1, U1, U2, U3, S]). Generic helper: Strip encryptions from AliceView and apply conditional independence. Given: X is conditionally independent of [Dk_a, R2, R3] given CondRV Proves: H(X | AliceView) = H(X | CondRV) This is reused in dsdp_security.v for the entropic security proof.
Helper joint_centropy_reduction semi_honest_case_analysis 5 Lemma joint_centropy_reduction : `H([% V2, V3] | AliceView ) = `H(V2 | AliceView). Joint conditional entropy reduction: H(V2,V3 | AliceView) = H(V2 | AliceView). V3 adds no additional entropy because it is functionally determined by V2 and the constraint. Used in the entropic security proof (dsdp_security.v).
▶ dumas2017dual/dsdp/dsdp_entropy_trace.v
1 helper
Name Section Lines Signature Meaning
Helper dsdp_algebraic_correctness trace_entropy_analysis 5 Lemma dsdp_algebraic_correctness : forall t, S t = (U1 \* V1 \+ U2 \* V2 \+ U3 \* V3) t. The protocol correctness theorem: the sum S equals the dot product. This is proved algebraically without depending on trace structure.
▶ dumas2017dual/dsdp/dsdp_interface.v
4 helper
Name Section Lines Signature Meaning
Helper dsdp_dtype_eqP Top-level 5 Lemma dsdp_dtype_eqP : Equality.axiom dsdp_dtype_eqb.
Helper std_from_enc_e Standard_Interface_Properties 1 Lemma std_from_enc_e (x : cipher AHE) : di_from_enc DI (di_e DI x) = Some x.
Helper std_from_enc_d Standard_Interface_Properties 1 Lemma std_from_enc_d (x : plain AHE) : di_from_enc DI (di_d DI x) = None.
Helper std_from_enc_k Standard_Interface_Properties 1 Lemma std_from_enc_k (x : priv_key AHE) : di_from_enc DI (di_priv_key DI x) = None.
▶ dumas2017dual/dsdp/dsdp_pismc.v
50 helper
Name Section Lines Signature Meaning
Helper alice_cross_eq smc_dsdp_program 4 Lemma alice_cross_eq dk' v1' u1' u2' u3' r2' r3' ra1' ra2' : erase (palice dk' v1' u1' u2' u3' r2' r3' ra1' ra2') = erase (palice_orig dk' v1' u1' u2' u3' r2' r3' ra1' ra2'). Cross-equality proofs on erased processes (proc, not sproc). The sproc types differ in session env indices, but erased procs are equal when pn maps parties to the expected concrete indices.
Helper bob_cross_eq smc_dsdp_program 4 Lemma bob_cross_eq dk' v2' rb1' rb2' : erase (pbob dk' v2' rb1' rb2') = erase (pbob_orig dk' v2' rb1' rb2').
Helper charlie_cross_eq smc_dsdp_program 4 Lemma charlie_cross_eq dk' v3' rc1' rc2' : erase (pcharlie dk' v3' rc1' rc2') = erase (pcharlie_orig dk' v3' rc1' rc2').
Helper alice_bob_dual smc_dsdp_program 3 Lemma alice_bob_dual : channels_dual aproc_alice aproc_bob. Three-party duality verification
Helper alice_charlie_dual smc_dsdp_program 3 Lemma alice_charlie_dual : channels_dual aproc_alice aproc_charlie.
Helper bob_charlie_dual smc_dsdp_program 3 Lemma bob_charlie_dual : channels_dual aproc_bob aproc_charlie.
Helper pbob_is_first smc_dsdp_program 1 Lemma pbob_is_first dk' v2' rb1' rb2' : pbob dk' v2' rb1' rb2' = DParty_first bob_idx charlie_idx dk' v2' rb1' rb2'. Cross-equality: existing 3-party definitions are instances of templates
Helper pcharlie_is_last smc_dsdp_program 1 Lemma pcharlie_is_last dk' v3' rc1' rc2' : pcharlie dk' v3' rc1' rc2' = DParty_last charlie_idx bob_idx dk' v3' rc1' rc2'.
Helper alice_bob_tmpl_dual smc_dsdp_program 1 Lemma alice_bob_tmpl_dual : channels_dual aproc_alice aproc_bob_tmpl.
Helper alice_charlie_tmpl_dual smc_dsdp_program 1 Lemma alice_charlie_tmpl_dual : channels_dual aproc_alice aproc_charlie_tmpl.
Helper bob_charlie_tmpl_dual smc_dsdp_program 1 Lemma bob_charlie_tmpl_dual : channels_dual aproc_bob_tmpl aproc_charlie_tmpl.
Helper dsdp_max_fuel_ok smc_dsdp_program 1 Lemma dsdp_max_fuel_ok : [> dsdp_saprocs] = 27. Fuel bound computed from program structure: - palice: 15 (7*Init + 2*Recv_enc + 2*Send + Recv_dec + Ret=2) - pbob: 7 (2*Init + Send + Recv_dec + Recv_enc + Send + Finish=1) - pcharlie: 6 (2*Init + Send + Recv_dec + Send + Finish=1) Total: 15 + 7 + 6 = 28, but actually computed as 27
Helper dsdp_ideal_max_fuel_ok dsdp_idealized_termination 1 Lemma dsdp_ideal_max_fuel_ok : [> dsdp_ideal_saprocs] = 27. Fuel bound
Helper dsdp_ideal_terminates dsdp_idealized_termination 1 Lemma dsdp_ideal_terminates traces : all_terminated (interp [> dsdp_ideal_saprocs] dsdp_ideal_procs traces).1. DSDP (Idealized): after interpretation, all processes are terminal.
Helper dsdp_ideal_no_fail dsdp_idealized_termination 1 Lemma dsdp_ideal_no_fail traces : all_nonfail (interp [> dsdp_ideal_saprocs] dsdp_ideal_procs traces).1. DSDP (Idealized): after interpretation, no process is Fail.
Helper alice_first_dual_n4 dsdp_n4_idealized_duality 1 Lemma alice_first_dual_n4 : channels_dual ap_alice_n4 ap_first_n4. 4-party duality verification: all 6 pairs
Helper alice_inter_dual_n4 dsdp_n4_idealized_duality 1 Lemma alice_inter_dual_n4 : channels_dual ap_alice_n4 ap_inter_n4.
Helper alice_last_dual_n4 dsdp_n4_idealized_duality 1 Lemma alice_last_dual_n4 : channels_dual ap_alice_n4 ap_last_n4.
Helper first_inter_dual_n4 dsdp_n4_idealized_duality 1 Lemma first_inter_dual_n4 : channels_dual ap_first_n4 ap_inter_n4.
Helper first_last_dual_n4 dsdp_n4_idealized_duality 1 Lemma first_last_dual_n4 : channels_dual ap_first_n4 ap_last_n4.
Helper inter_last_dual_n4 dsdp_n4_idealized_duality 1 Lemma inter_last_dual_n4 : channels_dual ap_inter_n4 ap_last_n4.
Helper dsdp_n4_builder_correct dsdp_n4_idealized_duality 1 Lemma dsdp_n4_builder_correct : @dsdp_n_procs AHE ek4 2 [:: @Ordinal 3 0 isT; @Ordinal 3 1 isT; @Ordinal 3 2 isT] dk0 v0 u4 r4_3 rand4_3 dk_relay_4 v_relay_4 r1_relay_4 r2_relay_4 = erase_aprocs [aprocs palice_4; pfirst_4; pinter_4; plast_4].
Helper dsdp_n4_max_fuel_ok dsdp_n4_idealized_duality 1 Lemma dsdp_n4_max_fuel_ok : [> dsdp_n4_saprocs] = 31.
Helper dsdp_n4_terminates dsdp_n4_idealized_duality 1 Lemma dsdp_n4_terminates traces : all_terminated (interp [> dsdp_n4_saprocs] dsdp_n4_procs traces).1. 4-party termination: after interpretation, all processes are terminal
Helper dsdp_n4_no_fail dsdp_n4_idealized_duality 1 Lemma dsdp_n4_no_fail traces : all_nonfail (interp [> dsdp_n4_saprocs] dsdp_n4_procs traces).1. 4-party no-fail: after interpretation, no process is Fail
Helper alice_first_dual_n5 dsdp_n5_idealized_duality 1 Lemma alice_first_dual_n5 : channels_dual ap_alice_n5 ap_first_n5. 5-party duality: all 10 pairs
Helper alice_inter2_dual_n5 dsdp_n5_idealized_duality 1 Lemma alice_inter2_dual_n5 : channels_dual ap_alice_n5 ap_inter2_n5.
Helper alice_inter3_dual_n5 dsdp_n5_idealized_duality 1 Lemma alice_inter3_dual_n5 : channels_dual ap_alice_n5 ap_inter3_n5.
Helper alice_last_dual_n5 dsdp_n5_idealized_duality 1 Lemma alice_last_dual_n5 : channels_dual ap_alice_n5 ap_last_n5.
Helper first_inter2_dual_n5 dsdp_n5_idealized_duality 1 Lemma first_inter2_dual_n5 : channels_dual ap_first_n5 ap_inter2_n5.
Helper first_inter3_dual_n5 dsdp_n5_idealized_duality 1 Lemma first_inter3_dual_n5 : channels_dual ap_first_n5 ap_inter3_n5.
Helper first_last_dual_n5 dsdp_n5_idealized_duality 1 Lemma first_last_dual_n5 : channels_dual ap_first_n5 ap_last_n5.
Helper inter2_inter3_dual_n5 dsdp_n5_idealized_duality 1 Lemma inter2_inter3_dual_n5 : channels_dual ap_inter2_n5 ap_inter3_n5.
Helper inter2_last_dual_n5 dsdp_n5_idealized_duality 1 Lemma inter2_last_dual_n5 : channels_dual ap_inter2_n5 ap_last_n5.
Helper inter3_last_dual_n5 dsdp_n5_idealized_duality 1 Lemma inter3_last_dual_n5 : channels_dual ap_inter3_n5 ap_last_n5.
Helper dsdp_n5_terminates dsdp_n5_idealized_duality 1 Lemma dsdp_n5_terminates traces : all_terminated (interp [> dsdp_n5_saprocs] dsdp_n5_procs traces).1.
Helper dsdp_n5_no_fail dsdp_n5_idealized_duality 1 Lemma dsdp_n5_no_fail traces : all_nonfail (interp [> dsdp_n5_saprocs] dsdp_n5_procs traces).1.
Helper size_dsdp_n_procs dsdp_n_rsteps 1 Lemma size_dsdp_n_procs relays dk0 v0 u0 r0 rand_a dk_relay v_relay r1_relay r2_relay : size (@dsdp_n_procs AHE ek n_relay relays dk0 v0 u0 r0 rand_a dk_relay v_relay r1_relay r2_relay) = (size relays).+1. * ** Size of dsdp_n_procs
Helper palice_n_erase dsdp_n_rsteps 16 Lemma palice_n_erase relays dk' v0' u' r' rand_a' : erase (@palice_n AHE ek n_relay relays dk' v0' u' r' rand_a') = pInit (priv_key dk') (pInit (d v0') (foldr (fun (fi : 'I_n_relay.+1 * nat) (cont : proc data) => alice_erase_body u' r' rand_a' fi.1 fi.2 cont) (alice_erase_tail dk' v0' u' r') (zip relays (iota 0 (size relays))))). Alice's erased program decomposes via erase_sproc_iter
Helper DParty_first_erase dsdp_n_rsteps 10 Lemma DParty_first_erase self downstream dk' v' r1' r2' : erase (@DParty_first AHE ek self downstream dk' v' r1' r2') = pInit (priv_key dk') (pInit (d v') (pSend alice_idx (e (enc (ek self) v' r1')) (pRecv alice_idx (fun d0 : data => match std_from_enc (AHE:=AHE) d0 with | Some enc0 => match dec dk' enc0 with | Some m0 => pRecv alice_idx (fun d1 : data => match std_from_enc (AHE:=AHE) d1 with | Some enc1 => pSend downstream (e (Emul enc1 (enc (ek downstream) m0 r2'))) Finish | None => Fail end) | None => Fail end | None => Fail First relay: Init dk; Init v; Send E(v) to Alice; Recv dec from Alice; Recv enc from Alice; Send product to downstream
Helper DParty_last_erase dsdp_n_rsteps 7 Lemma DParty_last_erase self upstream dk' v' r1' r2' : erase (@DParty_last AHE ek self upstream dk' v' r1' r2') = pInit (priv_key dk') (pInit (d v') (pSend alice_idx (e (enc (ek self) v' r1')) (pRecv upstream (fun d0 : data => match std_from_enc (AHE:=AHE) d0 with | Some enc0 => match dec dk' enc0 with | Some m0 => pSend alice_idx (e (enc (ek alice_idx) m0 r2')) Finish | None => Fail end | None => Fail end)))). Last relay: Init dk; Init v; Send E(v) to Alice; Recv dec from upstream; Send re-encrypted to Alice
Helper DParty_intermediate_erase dsdp_n_rsteps 10 Lemma DParty_intermediate_erase self alice_src upstream downstream dk' v' r1' r2' : erase (@DParty_intermediate AHE ek self alice_src upstream downstream dk' v' r1' r2') = pInit (priv_key dk') (pInit (d v') (pSend alice_src (e (enc (ek self) v' r1')) (pRecv alice_src (fun d0 : data => match std_from_enc (AHE:=AHE) d0 with | Some enc0 => pRecv upstream (fun d1 : data => match std_from_enc (AHE:=AHE) d1 with | Some enc1 => match dec dk' enc1 with | Some m0 => pSend downstream (e (Emul enc0 (enc (ek downstream) m0 r2'))) Finish | None => Fail end | None => Fail end) | None => Fail Intermediate relay: Init dk; Init v; Send E(v) to Alice; Recv enc from Alice; Recv dec from upstream; Send product to downstream
Helper size_interp1 interp_sound_section 5 Lemma size_interp1 ps h : size (interp1 ps h) = size ps.
Helper step_proc_trace_indep interp_sound_section 5 Lemma step_proc_trace_indep (ps : seq (proc data)) tr1 tr2 i : (smc_interpreter.step ps tr1 i).1.1 = (smc_interpreter.step ps tr2 i).1.1. The process component of step is independent of the trace argument.
Helper step_progress_trace_indep interp_sound_section 5 Lemma step_progress_trace_indep (ps : seq (proc data)) tr1 tr2 i : (smc_interpreter.step ps tr1 i).2 = (smc_interpreter.step ps tr2 i).2. The progress flag of step is independent of the trace argument.
Helper interp1E interp_sound_section 14 Lemma interp1E h ps traces : size traces = size ps -> interp1 ps h = (interp h ps traces).1. interp1 computes the same processes as interp
Helper step_iota_enum interp_sound_section 1 Lemma step_iota_enum n (ps : seq (proc data)) : [seq smc_interpreter.step ps nil i | i <- iota 0 n] = [seq smc_interpreter.step ps nil (val i) | i <- enum 'I_n]. step_sound gives rsteps using tuples; we need to connect that to the seq-level interp1 which uses iota. These two lemmas bridge the iota/enum gap.
Helper interp_sound interp_sound_section 16 Lemma interp_sound n h (ps : n.-tuple (proc data)) : exists (final : n.-tuple (proc data)) tr, rsteps ps final tr /\ tval final = interp1 (tval ps) h. Interpreter soundness: h rounds of interp produce an rsteps proof
Helper dsdp_3party_terminates dsdp_3party_rsteps 1 Lemma dsdp_3party_terminates traces : all_terminated (interp 27 procs traces).1. The protocol terminates: we can check this via the interpreter
Helper dsdp_3party_no_fail dsdp_3party_rsteps 1 Lemma dsdp_3party_no_fail traces : all_nonfail (interp 27 procs traces).1.
▶ dumas2017dual/dsdp/dsdp_program.v
3 helper
Name Section Lines Signature Meaning
Helper alice_a2_value dsdp 6 Lemma alice_a2_value : exists rr, alice_a2 = E bob (v2 * u2 + r2) rr. Lemma: alice_a2 encrypts v2*u2 + r2
Helper alice_a3_value dsdp 6 Lemma alice_a3_value : exists rr, alice_a3 = E charlie (v3 * u3 + r3) rr. Lemma: alice_a3 encrypts v3*u3 + r3
Helper bob_combined_value dsdp 7 Lemma bob_combined_value : exists rr, bob_combined alice_a3 = E charlie (v3 * u3 + r3 + d2_value) rr. Lemma: Bob's combined ciphertext encrypts the sum
▶ dumas2017dual/dsdp/dsdp_security.v
26 helper
Name Section Lines Signature Meaning
Helper V3_determined_centropy_v2_local dsdp_security 15 Lemma V3_determined_centropy_v2_local : `H([% V2, V3] | CondRV) = `H(V2 | CondRV). V3 is determined by V2 and CondRV, so joint entropy equals single. Uses chain rule and the fact that V3 = compute_v3(CondRV, V2). Follows exact pattern from dsdp_entropy.v V3_determined_centropy_v2.
Helper S_E dotp2 5 Lemma S_E : S = Dotp2_rv VS US \+ VU1. S expressed as dot product: S = (V2,V3)·(U2,U3) + V1*U1. This is the DSDP constraint s = u2*v2 + u3*v3 + u1*v1 in RV form.
Helper U3_R3_indep_V1 bob_security_independence 12 Lemma U3_R3_indep_V1 : P |= [%U3, R3] _|_ V1. Extract U3 _|_ V1 and R3 _|_ V1 from alice_V1_indep_randoms
Helper VU3_indep_V1 bob_security_independence 8 Lemma VU3_indep_V1 : P |= VU3 _|_ V1. VU3 = V3*U3 is independent of V1
Helper VU3R_indep_V1 bob_security_independence 15 Lemma VU3R_indep_V1 : P |= VU3R _|_ V1. VU3R = V3*U3 + R3 is independent of V1
Helper E_charlie_vur3_indep_V1 bob_security_independence 4 Lemma E_charlie_vur3_indep_V1 : P |= E_charlie_vur3 _|_ V1. E_charlie_vur3 is independent of V1 because VU3R is
Helper E_bob_d2_indep_V1 bob_security_independence 4 Lemma E_bob_d2_indep_V1 : P |= E_bob_d2 _|_ V1. E_bob_d2 is independent of V1 because D2 is
Helper D2_indep_V3 bob_security_independence 16 Lemma D2_indep_V3 : P |= D2 _|_ V3. D2 = VU2 + R2 is independent of V3 by one-time-pad masking
Helper E_bob_d2_indep_V3 bob_security_independence 4 Lemma E_bob_d2_indep_V3 : P |= E_bob_d2 _|_ V3. E_bob_d2 is independent of V3 because D2 is
Helper D2_indep_V2 charlie_security_independence 21 Lemma D2_indep_V2 : P |= D2 _|_ V2. D2 = VU2 + R2 is independent of V2 by one-time-pad masking. Mathematical reasoning (using lemma_3_5' from smc_proba.v): Theorem (One-Time Pad Independence): If Z is uniform over a finite group G and Z _|_ [%X, Y], then (X + Z) _|_ Y. Application to D2: - X = VU2 = V2 * U2 (the value to be masked) - Z = R2 (the uniform random mask) - Y = V2 (what we want to prove independence from) - X + Z = D2 = VU2 + R2 The hypothesis R2_indep_VU2_V2 states R2 _|_ [%VU2, V2]. Since R2 is uniform (from dsdp_random_inputs.pR2_unif), by lemma_3_5', we get D2 = VU2 + R2 _|_ V2. Technical note: Full mechanized proof requires careful handling of realType parameter alignment with the smc_proba.lemma_3_5' signature.
Helper D2_indep_VU3R_V2 charlie_security_independence 16 Lemma D2_indep_VU3R_V2 : P |= D2 _|_ [%VU3R, V2]. Intermediate lemma: D2 is independent of [%VU3R, V2] This follows from lemma_3_5' applied to D2 = VU2 + R2
Helper D3_indep_V2 charlie_security_independence 25 Lemma D3_indep_V2 : P |= D3 _|_ V2. D3 = VU3R + D2 is independent of V2. Since D2 is uniform and D2 _|_ [%VU3R, V2], by lemma_3_5', VU3R + D2 = D3 _|_ V2.
Helper E_charlie_d3_indep_V2 charlie_security_independence 4 Lemma E_charlie_d3_indep_V2 : P |= E_charlie_d3 _|_ V2. E_charlie_d3 is independent of V2 because D3 is independent of V2 and encryption is a deterministic function of D3.
Helper V2V3_indep_V1 charlie_security_independence 23 Lemma V2V3_indep_V1 : P |= [%V2, V3] _|_ V1. Helper: Extract [%V2, V3] _|_ V1 from alice_indep
Helper V1_indep_U2U3R2R3 charlie_security_independence 15 Lemma V1_indep_U2U3R2R3 : P |= V1 _|_ [%U2, U3, R2, R3]. Helper: Extract V1 _|_ [%U2, U3, R2, R3] from alice_V1_indep_randoms
Helper alice_indep_no_Dka charlie_security_independence 10 Lemma alice_indep_no_Dka : P |= [%V1, dsdp_entropy.U1 inputs, U2, U3, R2, R3] _|_ [%V2, V3]. Helper: Remove first element from 7-tuple using projection
Helper alice_indep_no_Dka_U1 charlie_security_independence 10 Lemma alice_indep_no_Dka_U1 : P |= [%V1, U2, U3, R2, R3] _|_ [%V2, V3]. Helper: Remove U1 from 6-tuple using projection
Helper V2V3_indep_V1_randoms charlie_security_independence 4 Lemma V2V3_indep_V1_randoms : P |= [%V2, V3] _|_ [%V1, U2, U3, R2, R3]. Helper: [%V2, V3] _|_ [%V1, U2, U3, R2, R3] from alice_indep
Helper V2V3_indep_V1_randoms_structured charlie_security_independence 21 Lemma V2V3_indep_V1_randoms_structured : P |= [%V2, V3] _|_ [%V1, [%U2, U3, R2, R3]]. This is the structure needed for mixing_rule
Helper E_charlie_d3_indep_V1 charlie_security_independence 4 Lemma E_charlie_d3_indep_V1 : P |= E_charlie_d3 _|_ V1. E_charlie_d3 is independent of V1 because D3 is independent of V1
Helper relay_otp_indep relay_security_n 11 Lemma relay_otp_indep : P |= D_i _|_ Y. Core one-time-pad lemma: D_i = VU_i + R_i is independent of Y
Helper relay_enc_otp_indep relay_security_n 4 Lemma relay_enc_otp_indep (party : party_id) : P |= (E' party `o D_i) _|_ Y. Encryption of D_i is independent of Y
Helper relay_privacy_from_indep relay_security_n 1 Lemma relay_privacy_from_indep {A : finType} (View : {RV P -> A}) (V_target : {RV P -> msg}) (pV_unif : `p_ V_target = fdist_uniform card_msg) (View_indep : P |= View _|_ V_target) : `H(V_target | View) = `H `p_ V_target. Generic relay privacy theorem: If RelayView _|_ V_target, then H(V_target | RelayView) = H(V_target)
Helper relay_privacy_logm relay_security_n 10 Lemma relay_privacy_logm {A : finType} (View : {RV P -> A}) (V_target : {RV P -> msg}) (pV_unif : `p_ V_target = fdist_uniform card_msg) (View_indep : P |= View _|_ V_target) : `H(V_target | View) = log (m%:R : R) /\ `H(V_target | View) > 0. Concrete privacy: H(V_target | View) = log(m) > 0
Helper dotp_n_e1 malicious_n 7 Lemma dotp_n_e1 (v : {ffun 'I_n_relay.+1 -> msg}) : dotp_n ConstUS_n v = v ord0. e_1 . v = v_1: the first basis vector extracts the first component
Helper ConstUS_n_discloses_V1 malicious_n 6 Lemma ConstUS_n_discloses_V1 (US VS : {RV P -> {ffun 'I_n_relay.+1 -> msg}}) : US = (fun _ => ConstUS_n) -> Dotp_n_rv US VS = (fun t => VS t ord0). If Alice sets US = e_1, she can extract V_1
▶ dumas2017dual/dsdp/dsdp_syntax_demo.v
13 helper
Name Section Lines Signature Meaning
Helper test_init_space_eq tests 1 Lemma test_init_space_eq : test_init_space = PInit v1 (PInit v2 (PInit v3 PFinish)). test_init_space should desugar to nested Init
Helper test_init_tuple_eq tests 1 Lemma test_init_tuple_eq : test_init_tuple = test_init_space. test_init_tuple should desugar to same as test_init_space
Helper test_init_chained_eq tests 1 Lemma test_init_chained_eq : test_init_chained = test_init_space. test_init_chained same as test_init_space
Helper test_recv_lambda_eq tests 1 Lemma test_recv_lambda_eq : test_recv_lambda = PRecv 0 (fun x => PRet x). test_recv_lambda should desugar to Recv with fun
Helper test_recv_dec_eq recv_dec_enc_tests 1 Lemma test_recv_dec_eq : test_recv_dec = PRecv 0 (fun x => match decrypt dk x with Some v => PRet v | None => PFail end). * Verify the desugaring is correct
Helper test_recv_enc_eq recv_dec_enc_tests 1 Lemma test_recv_enc_eq : test_recv_enc = PRecv 0 (fun x => PRet x).
Helper test_key_wrapper_eq wrapper_tests 1 Lemma test_key_wrapper_eq : test_key_wrapper = PInit (k_wrap dk) PFinish. * Verify desugaring
Helper test_data_wrapper_eq wrapper_tests 1 Lemma test_data_wrapper_eq : test_data_wrapper = PInit (d_wrap v1) PFinish.
Helper test_enc_wrapper_eq wrapper_tests 1 Lemma test_enc_wrapper_eq : test_enc_wrapper = PInit (e_wrap a) PFinish.
Helper partyA_structure two_party_example 1 Lemma partyA_structure : partyA = PInit secret (PSend 1 secret (PRecv 1 (fun response => PRet response))). Verify structure
Helper partyB_structure two_party_example 1 Lemma partyB_structure : partyB = PRecv 0 (fun x => PSend 0 x PFinish).
Helper unicode_ascii_eq unicode_vs_ascii 1 Lemma unicode_ascii_eq : example_unicode = example_ascii. Both versions produce identical terms
Helper mixed_eq unicode_vs_ascii 1 Lemma mixed_eq : example_mixed = example_unicode. Mixed usage also produces the same term
▶ dumas2017dual/entropy_fiber/entropy_fiber.v
10 helper
Name Section Lines Signature Meaning
Helper mem_image_set abstract_fibers 1 Lemma mem_image_set c : (c \in image_set) = [exists x, f x == c]. Alternative characterization: c is in image iff fiber is non-empty
Helper fiber_non_empty_image abstract_fibers 6 Lemma fiber_non_empty_image c : (c \in image_set) = (fiber c != set0). c is in the image of f iff its fiber (preimage) is non-empty
Helper mem_fiber abstract_fibers 1 Lemma mem_fiber x c : (x \in fiber c) = (f x == c). Membership in fiber
Helper nmem_fiber abstract_fibers 1 Lemma nmem_fiber x c : (x \notin fiber c) = (f x != c). Values outside fiber have f(x) ≠ c
Helper fiberC_cond_Pr0 fiber_entropy 11 Lemma fiberC_cond_Pr0 (c : CodomainT) (x : DomainT) : `Pr[Y = c] != 0 -> x \notin fiber f c -> `Pr[X = x | Y = c] = 0. Helper: values outside the fiber have zero conditional probability
Helper entropy_uniform_set fiber_entropy 6 Lemma entropy_uniform_set (S : {set DomainT}) (n : nat) : #|S| = n -> (0 < n)%N -> (- \sum_(x in S) n%:R^-1 * log (n%:R^-1 : R)) = log (n%:R : R). * Entropy unfolded: sum of uniform probabilities equals log |S|.
Helper entropy_fdist_uniform_set fiber_entropy 15 Lemma entropy_fdist_uniform_set (S : {set DomainT}) (n : nat) : #|S| = n -> (0 < n)%N -> exists (P : R.-fdist DomainT), (forall x, x \in S -> P x = n%:R^-1) -> (forall x, x \notin S -> P x = 0) -> `H P = log (n%:R : R). Note: although this is the same as the lemma above, it is difficult to use this version in the following `centropy1_uniform_fiber` proof. So both versions are kept.
Helper centropy_constant_fibers constant_fiber_size 26 Lemma centropy_constant_fibers (fiber_card : nat) : (forall c, c \in image_set f -> #|fiber f c| = fiber_card) -> (0 < fiber_card)%N -> `H(X | Y) = log (fiber_card%:R : R). Then overall conditional entropy is constant
Helper fiberC_jcond_Pr0 conditional_entropy_with_functional_constraint 14 Lemma fiberC_jcond_Pr0 (y : YT) (z : ZT) (x : XT) : `Pr[[% Y, Z] = (y, z)] != 0 -> g x y != z -> `Pr[X = x | [% Y, Z] = (y, z)] = 0. Helper: values outside the fiber have zero conditional probability
Helper centropy_jcond_determined_fibers conditional_entropy_with_functional_constraint 50 Lemma centropy_jcond_determined_fibers (fiber_card : nat) : (forall y z, `Pr[[% Y, Z] = (y, z)] != 0 -> #|[set x' | g x' y == z]| = fiber_card) -> (0 < fiber_card)%N -> `H(X | [% Y, Z]) = log (fiber_card%:R : R). When fibers have constant cardinality and X is uniform over each fiber, the conditional entropy is log(fiber_card). Joint conditioning version.
▶ dumas2017dual/entropy_fiber/entropy_fiber_zpq.v
7 helper
Name Section Lines Signature Meaning
Helper joint_factors_by_indeE fiber_entropy 8 Lemma joint_factors_by_indeE (input : InputT) (var : msg * msg) : `Pr[[%VarRV, InputRV] = (var, input)] = `Pr[VarRV = var] * `Pr[InputRV = input]. Joint probability factors by independence
Helper uniform_VarRV_probE fiber_entropy 4 Lemma uniform_VarRV_probE (var : msg * msg) : `Pr[VarRV = var] = (m ^ 2)%:R^-1 :> R. Uniform VarRV gives probability (m²)^-1
Helper Pr_cond_fiber_marginE marginal_probability 34 Lemma Pr_cond_fiber_marginE (cond : CondT) : `Pr[InputRV = proj_input cond] != 0 -> `Pr[CondRV = cond] = #|fiber cond|%:R * (m ^ 2)%:R^-1 * `Pr[InputRV = proj_input cond]. * Marginal probability over fiber. Pr[CondRV = cond] = |fiber(cond)| × (m²)^-1 × Pr[InputRV = proj_input(cond)] This expresses the marginal probability of the conditioning event as a product of: 1. The fiber cardinality (number of solutions) 2. The uniform probability (m²)^-1 for each solution 3. The probability of the input values
Helper gen_joint_factors_by_indeE fiber_entropy_gen 8 Lemma gen_joint_factors_by_indeE (input : InputT) (var : VarT) : `Pr[[%VarRV, InputRV] = (var, input)] = `Pr[VarRV = var] * `Pr[InputRV = input]. Joint probability factors by independence
Helper gen_uniform_VarRV_probE fiber_entropy_gen 4 Lemma gen_uniform_VarRV_probE (var : VarT) : `Pr[VarRV = var] = K%:R^-1 :> R. Uniform VarRV gives probability K^-1
Helper gen_Pr_cond_fiber_marginE gen_marginal_probability 34 Lemma gen_Pr_cond_fiber_marginE (cond : CondT) : `Pr[InputRV = proj_input cond] != 0 -> `Pr[CondRV = cond] = #|fiber cond|%:R * K%:R^-1 * `Pr[InputRV = proj_input cond].
Helper gen_cPr_uniform_fiber gen_conditional_probability 36 Lemma gen_cPr_uniform_fiber (cond : CondT) (v : VarT) : `Pr[CondRV = cond] != 0 -> v \in fiber cond -> `Pr[VarRV = v | CondRV = cond] = #|fiber cond|%:R^-1.
▶ dumas2017dual/entropy_fiber/linear_fiber_zpq.v
33 helper
Name Section Lines Signature Meaning
Helper proj_Fp_add fiber_2d 4 Lemma proj_Fp_add (x y : msg) : proj_Fp (x + y) = (proj_Fp x + proj_Fp y).
Helper proj_Fp_mul fiber_2d 4 Lemma proj_Fp_mul (x y : msg) : proj_Fp (x * y) = (proj_Fp x * proj_Fp y).
Helper proj_Fq_add fiber_2d 4 Lemma proj_Fq_add (x y : msg) : proj_Fq (x + y) = (proj_Fq x + proj_Fq y).
Helper proj_Fq_mul fiber_2d 4 Lemma proj_Fq_mul (x y : msg) : proj_Fq (x * y) = (proj_Fq x * proj_Fq y).
Helper fiber_Fp_card fiber_2d 1 Lemma fiber_Fp_card (u2 u3 target : 'F_p) : u3 != 0 -> #|fiber_Fp u2 u3 target| = p.
Helper fiber_Fq_card fiber_2d 1 Lemma fiber_Fq_card (u2 u3 target : 'F_q) : u3 != 0 -> #|fiber_Fq u2 u3 target| = q.
Helper val_Fp_lt_p fiber_2d 1 Lemma val_Fp_lt_p (x : 'F_p) : (val x < p)%N.
Helper val_Fq_lt_q fiber_2d 1 Lemma val_Fq_lt_q (x : 'F_q) : (val x < q)%N.
Helper val_msg_lt_m fiber_2d 1 Lemma val_msg_lt_m (x : msg) : (val x < m)%N.
Helper chinese_proj_p fiber_2d 1 Lemma chinese_proj_p (vp vq : nat) : (vp < p)%N -> (chinese p q vp vq %% p = vp)%N.
Helper chinese_proj_q fiber_2d 1 Lemma chinese_proj_q (vp vq : nat) : (vq < q)%N -> (chinese p q vp vq %% q = vq)%N.
Helper proj_Fp_crt fiber_2d 5 Lemma proj_Fp_crt (xp : 'F_p) (xq : 'F_q) : proj_Fp (crt_elem xp xq) = xp. Projection-reconstruction round-trips
Helper proj_Fq_crt fiber_2d 5 Lemma proj_Fq_crt (xp : 'F_p) (xq : 'F_q) : proj_Fq (crt_elem xp xq) = xq.
Helper crt_proj_id fiber_2d 5 Lemma crt_proj_id (x : msg) : crt_elem (proj_Fp x) (proj_Fq x) = x.
Helper chinese_mod_inj_p fiber_2d 12 Lemma chinese_mod_inj_p (xp xp' : 'F_p) (xq xq' : 'F_q) : chinese p q (val xp) (val xq) = chinese p q (val xp') (val xq') %[mod m] -> xp = xp'. CRT component extraction from modular equality
Helper chinese_mod_inj_q fiber_2d 12 Lemma chinese_mod_inj_q (xp xp' : 'F_p) (xq xq' : 'F_q) : chinese p q (val xp) (val xq) = chinese p q (val xp') (val xq') %[mod m] -> xq = xq'.
Helper crt_pair_inj fiber_2d 13 Lemma crt_pair_inj (pp pp' : 'F_p * 'F_p) (qq qq' : 'F_q * 'F_q) : crt_pair pp qq = crt_pair pp' qq' -> pp = pp' /\ qq = qq'. crt_pair is injective
Helper constraint_proj fiber_2d 5 Lemma constraint_proj (u2 u3 target : msg) (vv : msg * msg) : u2 * vv.1 + u3 * vv.2 = target -> (proj_Fp u2 * proj_Fp vv.1 + proj_Fp u3 * proj_Fp vv.2 = proj_Fp target) /\ (proj_Fq u2 * proj_Fq vv.1 + proj_Fq u3 * proj_Fq vv.2 = proj_Fq target). Constraint correspondence between Z_m and field components
Helper constraint_crt fiber_2d 11 Lemma constraint_crt (u2 u3 target : msg) (pp : 'F_p * 'F_p) (qq : 'F_q * 'F_q) : proj_Fp u2 * pp.1 + proj_Fp u3 * pp.2 = proj_Fp target -> proj_Fq u2 * qq.1 + proj_Fq u3 * qq.2 = proj_Fq target -> u2 * (crt_pair pp qq).1 + u3 * (crt_pair pp qq).2 = target.
Helper proj_Fp_neq0 fiber_2d 5 Lemma proj_Fp_neq0 (u3 : msg) : (0 < u3)%N -> (val u3 < p)%N -> proj_Fp u3 != 0%R. Nonzero projection helpers
Helper proj_Fq_neq0 fiber_2d 5 Lemma proj_Fq_neq0 (u3 : msg) : (0 < u3)%N -> (val u3 < q)%N -> proj_Fq u3 != 0%R.
Helper crt_proj_pair_inj fiber_2d 10 Lemma crt_proj_pair_inj : injective crt_proj_pair.
Helper crt_proj_pair_fiber fiber_2d 6 Lemma crt_proj_pair_fiber (u2 u3 target : msg) (vv : msg * msg) : vv \in linear_fiber_2d u2 u3 target -> crt_proj_pair vv \in setX (fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target)) (fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq target)).
Helper crt_pair_fiber fiber_2d 3 Lemma crt_pair_fiber (u2 u3 target : msg) (pp : 'F_p * 'F_p) (qq : 'F_q * 'F_q) : pp \in fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target) -> qq \in fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq target) -> crt_pair pp qq \in linear_fiber_2d u2 u3 target.
Helper crt_proj_pair_surj fiber_2d 6 Lemma crt_proj_pair_surj (u2 u3 target : msg) (ppqq : ('F_p * 'F_p) * ('F_q * 'F_q)) : ppqq \in setX (fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target)) (fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq target)) -> exists vv, vv \in linear_fiber_2d u2 u3 target /\ crt_proj_pair vv = ppqq.
Helper lt_minpq_coprime fiber_nd 14 Lemma lt_minpq_coprime (a : msg) : (0 < val a)%N -> (val a < minn p q)%N -> coprime (val a) m. 0 < u < min(p,q) implies u is coprime to m = p*q
Helper coprime_unitZm fiber_nd 4 Lemma coprime_unitZm (a : msg) : coprime (val a) m -> a \is a GRing.unit. coprime to m implies unit in Z_m
Helper widen_lift_ord_max fiber_nd 1 Lemma widen_lift_ord_max (i : 'I_n) : widen_ord (leqnSn n) i = lift ord_max i :> 'I_n.+1. Reindex sum: split at ord_max and reindex rest via lift
Helper sum_split_last fiber_nd 4 Lemma sum_split_last (F : 'I_n.+1 -> msg) : \sum_(i < n.+1) F i = F ord_max + \sum_(j < n) F (lift ord_max j).
Helper extend_in_fiber fiber_nd 8 Lemma extend_in_fiber (u : 'I_n.+1 -> msg) (target : msg) (w : {ffun 'I_n -> msg}) : u ord_max \is a GRing.unit -> extend_to_fiber u target w \in linear_fiber_nd u target. extend_to_fiber produces a fiber element
Helper project_extend_id fiber_nd 4 Lemma project_extend_id (u : 'I_n.+1 -> msg) (target : msg) (w : {ffun 'I_n -> msg}) : project_fiber (extend_to_fiber u target w) = w. project then extend is identity
Helper extend_project_id fiber_nd 20 Lemma extend_project_id (u : 'I_n.+1 -> msg) (target : msg) (v : {ffun 'I_n.+1 -> msg}) : u ord_max \is a GRing.unit -> v \in linear_fiber_nd u target -> extend_to_fiber u target (project_fiber v) = v. extend then project is identity for fiber elements
Helper extend_fiber_inj fiber_nd 3 Lemma extend_fiber_inj (u : 'I_n.+1 -> msg) (target : msg) : injective (extend_to_fiber u target). extend_to_fiber is injective
▶ dumas2017dual/lib/extra_algebra.v
7 helper
Name Section Lines Signature Meaning
Helper logr_eq1 log_extra 10 Lemma logr_eq1 (x : R) : 0 < x -> (log x = 0) <-> (x = 1). log x = 0 iff x = 1 (for positive x). This is fundamental for entropy calculations where log(prob) = 0 implies the probability is 1 (certainty).
Helper bigD1_filter bigop_extra 6 Lemma bigD1_filter {R : Type} {op : SemiGroup.com_law R} {idx : R} {I : eqType} (r : seq I) (j : I) (P : pred I) (F : I -> R) : j \in r -> P j -> uniq r -> \big[op/idx]_(i <- [seq x <- r | P x]) F i = op (F j) (\big[op/idx]_(i <- [seq x <- r | P x] | i != j) F i). Extract a term from a filtered big operation: if j is in r and satisfies P, we can factor out F(j) from the sum/product over filtered elements. Useful for manipulating sums over constrained index sets.
Helper bigD1_seq_cond bigop_extra 10 Lemma bigD1_seq_cond {R : Type} {op : SemiGroup.com_law R} {idx : R} {I : eqType} (r : seq I) (j : I) (P : pred I) (F : I -> R) : j \in r -> P j -> uniq r -> \big[op/idx]_(i <- r | P i) F i = op (F j) (\big[op/idx]_(i <- r | P i && (i != j)) F i). Extract a term from a conditional big operation over a sequence. Similar to bigD1 but for conditional sums: factors out F(j) when j satisfies P, leaving the rest with an additional (i != j) condition.
Helper Zp_unit_coprime Zp_unit_extra 6 Lemma Zp_unit_coprime (m : nat) (x : 'Z_m) : (1 < m)%N -> x \is a GRing.unit -> coprime x m. Uses unitZpE in reverse: (x%:R) \is a GRing.unit = coprime m x
Helper Zp_unitP Zp_unit_extra 4 Lemma Zp_unitP (m : nat) (x : 'Z_m) : (1 < m)%N -> (x \is a GRing.unit) = coprime x m. Equivalence form: unit status iff coprime (when m > 1)
Helper Zp_Fp_card_eq Zp_Fp_equivalence 5 Lemma Zp_Fp_card_eq (m_minus_2 : nat) : let m := m_minus_2.+2 in prime m -> #|'Z_m| = #|'F_m|. When m is prime, 'Z_m and 'F_m have the same cardinality
Helper entropy_formula_same Zp_Fp_equivalence 1 Lemma entropy_formula_same (m : nat) : (1 < m)%N -> log (m%:R : R) = log (m%:R : R). Reflexivity lemma for entropy formulas over Z_m. This trivial lemma serves as a proof obligation discharge when showing that entropy calculations over different representations (e.g., 'Z_m vs 'F_m when m is prime) yield identical results.
▶ dumas2017dual/lib/extra_entropy.v
9 helper
Name Section Lines Signature Meaning
Helper entropy_sum_split entropy_sum 9 Lemma entropy_sum_split (A : finType) (S : pred A) (p : R) (pmf : A -> R) : (forall a, S a -> pmf a = p) -> (forall a, ~~ S a -> pmf a = 0) -> (- \sum_(a : A) pmf a * log (pmf a)) = (- \sum_(a : A | S a) p * log p). Entropy sum over a subset with uniform probability
Helper cinde_cond_mutual_info0 cinde_cond_mutual_info0 40 Lemma cinde_cond_mutual_info0 : P |= X _|_ Y | Z -> cond_mutual_info `p_[% X, Y, Z] = 0. Conditional independence implies zero conditional mutual information: If X ⊥ Y | Z, then I(X;Y|Z) = 0. This is the information-theoretic characterization of conditional independence.
Helper zero_entropy_eq_point_mass1 zero_entropy_eq_point_mass 72 Lemma zero_entropy_eq_point_mass1 (V: finType) (Z : {RV P -> V}) : `H `p_Z = 0 <-> exists z, `Pr[Z = z] = 1. Zero entropy characterizes point mass distributions: H(Z) = 0 iff there exists z with Pr[Z = z] = 1. This is the deterministic case - no uncertainty means one certain outcome.
Helper zero_entropy_eq_point_mass zero_entropy_eq_point_mass 20 Lemma zero_entropy_eq_point_mass (V: finType) (Z : {RV P -> V}) : `H `p_Z = 0 <-> exists! z, `Pr[Z = z] = 1. Unique point mass characterization: H(Z) = 0 iff there exists UNIQUE z with Pr[Z = z] = 1. Strengthens zero_entropy_eq_point_mass1 with uniqueness.
Helper centropy_term_deterministic zero_centropy_eq_point_mass 28 Lemma centropy_term_deterministic (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) : `Pr[Y = y] != 0 -> (exists z, `Pr[Z = z | Y = y] = 1) -> `p_Y y * centropy1 `p_[% Z, Y] y = 0. Helper: if the conditional distribution Pr[Z | Y = y] is deterministic (i.e., there exists z with Pr[Z = z | Y = y] = 1), then the corresponding term in the conditional entropy sum is zero.
Helper jfdist_cond_entropy_zero zero_centropy_eq_point_mass 15 Lemma jfdist_cond_entropy_zero (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (Hy_marginal : (`p_[% Y, Z])`1 y != 0) (Hy_centropy_zero : - (\sum_(b in W) \Pr_`p_[% Z, Y][[set b] | [set y]] * log \Pr_`p_[% Z, Y][[set b] | [set y]]) = 0) : let cond_dist := jfdist_cond0 `p_[% Y, Z] y Hy_marginal in `H cond_dist = 0. Helper: Conditional distribution has zero entropy when centropy1 is zero
Helper point_mass_to_cond_prob zero_centropy_eq_point_mass 6 Lemma point_mass_to_cond_prob (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (z : W) (Hy_marginal : (`p_[% Y, Z])`1 y != 0) (Hz : (jfdist_cond0 `p_[% Y, Z] y Hy_marginal) z = 1) : `Pr[Z = z | Y = y] = 1. Helper: Point mass in conditional distribution implies conditional probability = 1
Helper zero_centropy1_point_mass zero_centropy_eq_point_mass 25 Lemma zero_centropy1_point_mass (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (HPrYeq0 : `Pr[Y = y] != 0) (Hy_centropy_zero : - (\sum_(b in W) \Pr_`p_[% Z, Y][[set b] | [set y]] * log \Pr_`p_[% Z, Y][[set b] | [set y]]) = 0) : exists z : W, `Pr[Z = z | Y = y] = 1. Helper: If the conditional entropy at y equals zero (as a Prop equality = 0) then there exists z with Pr[Z = z | Y = y] = 1.
Helper inde_cond_entropy inde_entropy_lemmas 7 Lemma inde_cond_entropy (U A B : finType) (P : R.-fdist U) (View : {RV P -> A}) (X : {RV P -> B}) : P |= View _|_ X -> `H(X | View) = `H `p_ X. Independence implies conditional entropy equals unconditional: H(X|V) = H(X)
▶ dumas2017dual/lib/extra_proba.v
17 helper
Name Section Lines Signature Meaning
Helper pair_notin_fin_img_fst proba_extra 17 Lemma pair_notin_fin_img_fst (T A B : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (a : A) (b : B) : a \notin fin_img X -> (a, b) \notin fin_img [% X, Y]. If a is not in the image of X, then (a, b) cannot be in the joint image. This is used to show that pairs outside the support have zero probability.
Helper sum_cPr_eq proba_extra 19 Lemma sum_cPr_eq (T A B : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (y : B) : `Pr[Y = y] != 0 -> \sum_(a in A) `Pr[X = a | Y = y] = 1. Conditional probabilities sum to 1: Σ_a Pr[X = a | Y = y] = 1. This is the law of total probability for conditional distributions, essential for showing that conditional distributions are valid fdists.
Helper cPr_eq_notin_fin_img proba_extra 9 Lemma cPr_eq_notin_fin_img (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (z : W) : z \notin fin_img Z -> `Pr[Z = z | Y = y] = 0. Helper lemma: if z is not in the image of Z, then conditional probability is 0
Helper cPr_eq_two_ones_absurd proba_extra 18 Lemma cPr_eq_two_ones_absurd (V W T : finType) (P : R.-fdist T) (Y : {RV P -> V}) (Z : {RV P -> W}) (y : V) (z z' : W) : `Pr[Y = y] != 0 -> z != z' -> `Pr[Z = z | Y = y] = 1 -> `Pr[Z = z' | Y = y] = 1 -> False. Helper: If two different values both have conditional probability 1, contradiction
Helper jfdist_cond_cPr_eq proba_extra 15 Lemma jfdist_cond_cPr_eq {T TX TY : finType} (P : R.-fdist T) (X : {RV P -> TX}) (Y : {RV P -> TY}) (x : TX) (y : TY) : `Pr[X = x] != 0 -> `p_[% X, Y]`(|x) y = `Pr[Y = y | X = x]. Conditional fdist equals conditional probability
Helper cond_prob_zero_outside_constraint proba_extra 12 Lemma cond_prob_zero_outside_constraint {T TX TY : finType} (P : R.-fdist T) (X : {RV P -> TX}) (Y : {RV P -> TY}) (constraint : TX -> TY -> bool) : (forall t, constraint (X t) (Y t)) -> forall x y, `Pr[X = x] != 0 -> ~~ constraint x y -> `Pr[Y = y | X = x] = 0. If Y must satisfy a property determined by X, then conditional probability is zero outside that property
Helper PrX_fstRV proba_extra 17 Lemma PrX_fstRV (A B T : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (x : A) : \sum_(y : B) `Pr[[% X, Y] = (x, y)] = `Pr[X = x]. Marginalization: summing joint probabilities over Y yields marginal of X. Σ_y Pr[(X,Y) = (x,y)] = Pr[X = x]. Fundamental for deriving marginals.
Helper jproduct_ruleRV proba_extra 10 Lemma jproduct_ruleRV (A B T : finType) (P : R.-fdist T) (X : {RV P -> A}) (Y : {RV P -> B}) (x : A) (y : B) : `Pr[[% X, Y] = (x, y)] = `Pr[Y = y] * `Pr[X = x | Y = y]. Joint probability product rule: Pr[(X,Y) = (x,y)] = Pr[Y=y] * Pr[X=x|Y=y]. This is Bayes' theorem in product form, fundamental for decomposing joint distributions into marginal × conditional.
Helper fdist_proj23_RV3 perm_extra 3 Lemma fdist_proj23_RV3 (TA TB TC : finType) (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}) : fdist_proj23 `p_[% X, Y, Z] = `p_[% Y, Z]. Projection of triple (X,Y,Z) onto (Y,Z) gives the joint distribution of (Y,Z). This connects fdist_proj23 with the random variable notation.
Helper pfwd1_pair4_swap34 perm_extra 4 Lemma pfwd1_pair4_swap34 (TA TB TC TD : finType) (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}) (W : {RV P -> TD}) a b c d : `Pr[ [% X, Y, Z, W] = (a, b, c, d) ] = `Pr[ [% X, Y, W, Z] = (a, b, d, c) ]. Swap 3rd and 4th components in 4-tuple probability: Pr[(X,Y,Z,W)=(a,b,c,d)] = Pr[(X,Y,W,Z)=(a,b,d,c)]. Used for reordering conditioning variables.
Helper pfwd1_nested3_AC perm_extra 6 Lemma pfwd1_nested3_AC (TA TB TC TD : finType) (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}) (W : {RV P -> TD}) a b c d : `Pr[ [% X, [% Y, Z, W]] = (a, (b, c, d)) ] = `Pr[ [% X, [% Y, W, Z]] = (a, (b, d, c)) ]. Swap components in nested triple: (a,(b,c,d)) ↔ (a,(b,d,c)). Relates different nestings of tuple probabilities.
Helper pfwd1_pair4_mid_A perm_extra 5 Lemma pfwd1_pair4_mid_A (TA TB TC TD : finType) (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}) (W : {RV P -> TD}) a b c d : `Pr[ [% X, Y, Z, W] = (a, b, c, d) ] = `Pr[ [% X, [% Y, Z], W] = (a, (b, c), d) ]. Associativity for 4-tuple: (a,b,c,d) ↔ (a,(b,c),d). Shows that flat 4-tuples equal nested representations.
Helper centropyAC perm_extra 12 Lemma centropyAC (A B C D : finType) (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}) : `H(X | [% Y, Z, W]) = `H(X | [% Y, W, Z]). Conditional entropy is invariant under swapping last two conditioning vars: H(X | Y,Z,W) = H(X | Y,W,Z). Commutativity for conditioning tuple tail.
Helper centropyA perm_extra 22 Lemma centropyA (A B C D : finType) (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}) : `H(X | [% Y, [% Z, W]]) = `H(X | [% Y, Z, W]). Associativity for conditional entropy: H(X | (Y,(Z,W))) = H(X | Y,Z,W). Flattens nested conditioning tuples.
Helper centropyA_middle perm_extra 24 Lemma centropyA_middle {A B C D E : finType} (X : {RV P -> A}) (W : {RV P -> B}) (V : {RV P -> C}) (Z : {RV P -> D}) (Y : {RV P -> E}) : `H(X | [% W, [% V, Z], Y]) = `H(X | [% W, V, Z, Y]). Flatten nested pair in middle position: H(X | W,(V,Z),Y) = H(X | W,V,Z,Y). Associativity when the nested pair is in the middle of the conditioning.
Helper centropy4_swap_2_4 perm_extra 12 Lemma centropy4_swap_2_4 (A B C D E : finType) (X : {RV P -> A}) (W : {RV P -> B}) (Y : {RV P -> C}) (Z : {RV P -> D}) (V : {RV P -> E}) : `H(X | [% W, Y, Z, V]) = `H(X | [% W, V, Z, Y]). Swap 2nd and 4th positions in 4-variable conditioning: H(X | W,Y,Z,V) = H(X | W,V,Z,Y). Used for reordering Alice's view components.
Helper marginal_swap_YZ perm_extra 4 Lemma marginal_swap_YZ (V W : finType) (Y : {RV P -> V}) (Z : {RV P -> W}) : forall y : V, (`p_[% Z, Y])`2 y = (`p_[% Y, Z])`1 y. Marginal equivalence under swap: the 2nd marginal of (Z,Y) equals the 1st marginal of (Y,Z). Both give the distribution of Y.
▶ dumas2017dual/lib/rouche_capelli.v
26 helper
Name Section Lines Signature Meaning
Helper card_lker_lfun finvect_lemmas 1 Lemma card_lker_lfun (K : fieldType) (aT : finVectType K) (rT : vectType K) (f : {linear aT -> rT}) : #|lker (linfun f)| = #|[set x : aT | f x == 0]|. Kernel cardinality equals the set of zeros: |ker(f)| = |{x | f(x) = 0}|. Connects the linear algebra kernel with the set-theoretic preimage of 0.
Helper diffvv vector_ext 1 Lemma diffvv {K : fieldType} {vT : vectType K} (U : {vspace vT}) : (U :\: U = 0)%VS. Self-difference is zero: U \ U = 0. Trivial but useful for simplification.
Helper limg_lker vector_ext 1 Lemma limg_lker {K : fieldType} {aT rT : vectType K} (f : 'Hom(aT, rT)) : (f @: lker f = 0)%VS. Image of kernel is zero: f(ker(f)) = 0. By definition of kernel.
Helper HomK vector_ext 1 Lemma HomK {R : nzRingType} {vT wT : vectType R} (A : 'M_(dim vT, dim wT)) : f2mx (Hom A) = A. Matrix representation of Hom: f2mx(Hom(A)) = A. Coercion identity.
Helper rouche1 RoucheCapelliTheorems 8 Lemma rouche1 m n (A : 'M[R]_(m,n)) (B : 'rV_n) : (exists x, x *m A = B) <-> (\rank A = \rank (col_mx A B)). Rouché-Capelli Theorem (Part 1): System xA = B has a solution iff rank(A) = rank([A; B]). The augmented matrix has same rank as coefficient matrix.
Helper rouche2 RoucheCapelliTheorems 10 Lemma rouche2 m n (A : 'M[R]_(m,n)) (B : 'rV_n) : \rank A = \rank (col_mx A B) -> \rank A = m -> exists! x, x *m A = B. Rouché-Capelli Theorem (Part 2): If system is consistent and rank = #rows, then the solution is unique. Full rank means trivial kernel.
Helper exists_nonzero_kernel RoucheCapelliTheorems 6 Lemma exists_nonzero_kernel m n (A : 'M[R]_(m, n)) : (\rank A < m)%N -> exists y : 'rV_m, y *m A = 0 /\ y != 0. Rank-deficient matrices have nontrivial kernels: if rank(A) < m, there exists nonzero y with yA = 0. Foundation for solution counting.
Helper kernel_membership RoucheCapelliTheorems 4 Lemma kernel_membership m n p (A : 'M[R]_(m, n)) (X : 'M[R]_(n, p)) : A *m X = 0 -> (X^T <= kermx A^T)%MS. Solutions to AX = 0 lie in the kernel: if AX = 0, then X^T ≤ ker(A^T). Transposes relate left/right multiplication to kernel membership.
Helper kernel_coeff_exists RoucheCapelliTheorems 6 Lemma kernel_coeff_exists m n p (A : 'M[R]_(m, n)) (X : 'M[R]_(n, p)) : A *m X = 0 -> exists P : 'M[R]_(p, n), X^T = P *m kermx A^T. Kernel coefficient existence: if AX = 0, then X^T can be written as P * ker(A^T) for some P. Explicit decomposition in kernel basis.
Helper sub_coker_colspan FiniteSolutionCounting 8 Lemma sub_coker_colspan m n (A : 'M[K]_(m, n)) : forall x : 'cV[K]_n, x \in colspan (cokermx A) -> A *m x == 0. Vectors in cokernel column span are in kernel: if x ∈ colspan(coker A), then Ax = 0. Connects cokernel with null space.
Helper submx_castmx FiniteSolutionCounting 7 Lemma submx_castmx m1 m2 n (A : 'M[K]_(m1, n)) (B : 'M[K]_(m2, n)) e : (A <= B)%MS -> @submx.body K m1 m2 n A (castmx e B). Submatrix relation preserved under dimension cast: A ≤ B implies A ≤ cast(B). Technical lemma for handling dimension changes in matrix row spaces.
Helper castmx_mul_row FiniteSolutionCounting 4 Lemma castmx_mul_row m n p q (e_m : m = p) (e_n : n = q) (w : 'rV[K]_m) (M : 'M[K]_(m, n)) : castmx (erefl, e_m) w *m castmx (e_m, e_n) M = castmx (erefl, e_n) (w *m M). Lemma for casting matrix multiplication with row vectors
Helper card_lker_mxof card_lker 7 Lemma card_lker_mxof : #|(lker f)| = #|[set x : 'rV[K]_(\dim {:aT}) | x *m (mxof e e' f) == 0]|. Kernel cardinality via matrix representation: |ker(f)| = |{x | x·M = 0}| where M is the matrix of f w.r.t. bases e, e'. Bridges abstract linear maps to concrete matrix equations for counting.
Helper dim_rV counting 1 Lemma dim_rV p : \dim {:'rV[K]_p} = p. Dimension of row vector space: dim('rV_p) = p. Standard identity.
Helper card_lker_Hom counting 8 Lemma card_lker_Hom : #|lker (Hom A)| = #|[set x : 'rV[K]_m | x *m A == 0]|. Kernel cardinality for Hom functor: |ker(Hom(A))| = |{x | xA = 0}|. Specializes card_lker_mxof to the standard matrix-to-linear-map coercion.
Helper cancel_row_free counting 8 Lemma cancel_row_free p q (g : {linear 'rV[K]_p -> 'rV[K]_q}) (h : {linear 'rV[K]_q -> 'rV[K]_p}) : cancel g h -> row_free (lin1_mx g). Cancellation implies row freedom: if g has a left inverse h, then the matrix representation of g has full row rank (row_free).
Helper row_free_tr counting 1 Lemma row_free_tr p q (M : 'M[K]_(p,q)) : p = q -> row_free M^T = row_free M. Row freedom is transpose-invariant for square matrices: row_free(M^T) = row_free(M) when p = q.
Helper count_kernel_vectors counting 3 Lemma count_kernel_vectors : #| [set x : 'rV[K]_m | x *m A == 0] | = (#| {:K} | ^ (m - \rank A))%N. Kernel cardinality formula: |ker(A)| = |K|^(m - rank(A)). The kernel is a subspace of dimension (m - rank(A)), hence has this many elements. This is the core counting result for linear systems.
Helper affine_eq_translate_kernel affine_solution_counting 17 Lemma affine_eq_translate_kernel (x0 : 'rV[K]_m) : x0 *m A = b -> affine_solutions = [set x0 + k | k in kernel_solutions]. Given a particular solution, affine set = particular + kernel
Helper card_translate affine_solution_counting 5 Lemma card_translate (S : {set 'rV[K]_m}) (v : 'rV[K]_m) : #|[set v + s | s in S]| = #|S|. Translation preserves cardinality: |v + S| = |S|. Adding a constant vector v to all elements is a bijection.
Helper count_affine_solutions affine_solution_counting 5 Lemma count_affine_solutions (x0 : 'rV[K]_m) : x0 *m A = b -> #|affine_solutions| = #|kernel_solutions|. Affine solutions = kernel cardinality: |{x | xA = b}| = |ker(A)|. Since affine_solutions = x₀ + ker(A), cardinality equals kernel size.
Helper affine_eq_translate_kernel_col affine_solultion_counting_col 16 Lemma affine_eq_translate_kernel_col (v0 : 'cV[K]_n) : A *m v0 = b -> affine_solutions_col = [set v0 + k | k in kernel_solutions_col]. Given a particular solution, affine set = particular + kernel
Helper card_translate_col affine_solultion_counting_col 5 Lemma card_translate_col (S : {set 'cV[K]_n}) (v : 'cV[K]_n) : #|[set v + s | s in S]| = #|S|. Translation preserves cardinality (column version): |v + S| = |S|. Same as card_translate but for column vectors.
Helper count_affine_solutions_col affine_solultion_counting_col 5 Lemma count_affine_solutions_col (v0 : 'cV[K]_n) : A *m v0 = b -> #|affine_solutions_col| = #|kernel_solutions_col|. Affine = kernel cardinality (column version): |{v | Av = b}| = |ker(A)|. Column version of count_affine_solutions for Av = b systems.
Helper count_kernel_vectors_col affine_solultion_counting_col 16 Lemma count_kernel_vectors_col : #|[set v : 'cV[K]_n | A *m v == 0]| = (#|{:K}| ^ (n - \rank A))%N. Kernel cardinality (column version): |{v | Av = 0}| = |K|^(n - rank(A)). Proved by transposing to row form and applying count_kernel_vectors. Needed because Coq treats 'cV and 'rV as distinct types.
Helper count_affine_solutions_rank1 FiniteSolutionCounting 106 Lemma count_affine_solutions_rank1 (x y z : K) : y != 0 -> #|[set p : K * K | x * p.1 + y * p.2 == z]| = #|K|. 2D linear constraint cardinality: |{(a,b) | x*a + y*b = z}| = |K| when y ≠ 0. Special case for rank-1 systems: one equation in two unknowns has |K| solutions. Used directly in DSDP's constrained_pairs_card and dotp2_solutions. Proof converts the pair constraint to column form and applies the general theory.
▶ homomorphic_encryption/benaloh1994/benaloh_ahe.v
6 helper
Name Section Lines Signature Meaning
Helper dec_correct_mixin benaloh_instance 5 Lemma dec_correct_mixin (dk : BenalohPrivKey n r) (u : {unit 'Z_n}) (m : 'Z_r) : dec_for_mixin dk (enc_for_mixin (pub_of_priv dk) m u) = Some m.
Helper Emul_addM benaloh_instance 6 Lemma Emul_addM : forall (k : BenalohPubKey n r), {morph E[k] : mr1 mr2 / mr1 {[ +%R ; *r ]} mr2 >-> Emul mr1 mr2}.
Helper Epow_scalarM benaloh_instance 8 Lemma Epow_scalarM : forall (k : BenalohPubKey n r) (j : 'Z_r), {morph E[k] : mr / mr {< *%R ; ^r >} j >-> Epow mr j}.
Helper benaloh_Emul_assoc benaloh_instance 1 Lemma benaloh_Emul_assoc : associative Emul.
Helper benaloh_Emul_comm benaloh_instance 1 Lemma benaloh_Emul_comm : commutative Emul.
Helper benaloh_Emul_id benaloh_instance 7 Lemma benaloh_Emul_id : forall k : pub_key BT, left_id (ahe_enc.enc_curry BT k (0, benaloh_rand_id)) (@Emul).
▶ homomorphic_encryption/benaloh1994/benaloh_enc.v
14 helper
Name Section Lines Signature Meaning
Helper Zp_add_eqmod Top-level 10 Lemma Zp_add_eqmod (r : nat) (r_gt1 : (1 < r)%N) (m1 m2 : 'Z_r) : (m1 : nat) + m2 = (m1 + m2)%R %[mod r]. Helper: nat addition of Z_r elements equals Z_r addition mod r
Helper Zp_mulrn_nat Top-level 6 Lemma Zp_mulrn_nat (r : nat) (r_gt1 : (1 < r)%N) (m : 'Z_r) (k : nat) : ((m *+ k)%R : nat) = (((m : nat) * k) %% (Zp_trunc r).+2)%N. Helper: (m *+ k : 'Z_r) as nat equals (m * k) %% (Zp_trunc r).+2
Helper Zp_mulrn_eqmod Top-level 9 Lemma Zp_mulrn_eqmod (r : nat) (r_gt1 : (1 < r)%N) (m1 : 'Z_r) (m2 : nat) : (m1 : nat) * m2 = (m1 *+ m2)%R %[mod r]. Helper: nat mult of Z_r element by nat equals Z_r scalar mult mod r
Helper val_unit_exp BenalohEuler 1 Lemma val_unit_exp (u : {unit 'Z_n}) k : val (u ^+ k)%g = (val u) ^+ k. Helper: val of group exponent = ring exponent of val
Helper euler_unit BenalohEuler 5 Lemma euler_unit (x : {unit 'Z_n}) : (val x) ^+ phi_n = 1. Euler's theorem: any unit raised to phi(n) equals 1
Helper expr_modr BenalohEuler 4 Lemma expr_modr (k : nat) : (val y) ^+ k = (val y) ^+ (k %% r)%N. Exponentiation of y depends only on exponent mod r
Helper Zp_val_ltn BenalohEuler 7 Lemma Zp_val_ltn (x : 'Z_r) : ((x : nat) < r)%N. Helper: 'Z_r elements as nats are bounded by r
Helper enc_mul_dist BenalohEuler 11 Lemma enc_mul_dist : forall (m1 m2 : 'Z_r) (u1 u2 : {unit 'Z_n}), benaloh_enc m1 u1 * benaloh_enc m2 u2 = benaloh_enc (m1 + m2) (u1 * u2). Encryption multiplication distributes as addition on messages
Helper enc_exp_dist BenalohEuler 13 Lemma enc_exp_dist : forall (m1 : 'Z_r) (m2 : nat) (u : {unit 'Z_n}), (benaloh_enc m1 u) ^+ m2 = benaloh_enc (m1 *+ m2) (u ^+ m2). Encryption exponentiation distributes as scalar multiplication
Helper alpha_phi BenalohEuler 1 Lemma alpha_phi : (alpha * r = phi_n)%N. alpha * r = phi_n (alpha is well-defined)
Helper rth_powers_vanish BenalohEuler 4 Lemma rth_powers_vanish (u : {unit 'Z_n}) : (val u) ^+ r ^+ alpha = 1. r-th powers vanish when raised to alpha (subgroup structure)
Helper ciphertext_to_alpha BenalohEuler 6 Lemma ciphertext_to_alpha (m : 'Z_r) (u : {unit 'Z_n}) : (benaloh_enc m u) ^+ alpha = (val y) ^+ (alpha * m). Raising ciphertext to alpha strips randomness
Helper decryption_unique BenalohEuler 4 Lemma decryption_unique (m1 m2 : 'Z_r) (u1 u2 : {unit 'Z_n}) : (benaloh_enc m1 u1) ^+ alpha = (benaloh_enc m2 u2) ^+ alpha -> m1 = m2. Distinct messages give distinct alpha-powers (unique decryption)
Helper benaloh_dec_correct BenalohEuler 12 Lemma benaloh_dec_correct (m : 'Z_r) (u : {unit 'Z_n}) : benaloh_dec alpha (benaloh_enc m u) = Some m. Decryption with alpha recovers the original message
▶ homomorphic_encryption/homomorphic_encryption.v
7 helper
Name Section Lines Signature Meaning
Helper party_id_eqP party_id_def 5 Lemma party_id_eqP : Equality.axiom party_id_eqb.
Helper party_id_natK party_id_def 1 Lemma party_id_natK : cancel party_id_to_nat nat_to_party_id.
Helper party_id_enumP party_id_def 1 Lemma party_id_enumP : Finite.axiom party_id_enum.
Helper card_party_key party_key_types 6 Lemma card_party_key : #|{:p.-key k T}| = #|T|.
Helper card_enc_for enc_types 6 Lemma card_enc_for : #|{:p.-enc T}| = #|T|.
Helper card_enc_for enc_types 1 Lemma card_enc_for' : forall (n : nat), #|T| = n.+1 -> #|{:p.-enc T}| = n.+1.
Helper E_enc_ce_contract enc_lemmas 25 Lemma E_enc_ce_contract (A B C : finType) (p : party_id) (X : {RV P -> A})(E : {RV P -> p.-enc B})(Z : {RV P -> C})(n : nat): #|B| = n.+1 -> (forall x e, `Pr[ [%X, E] = (x, e)] != 0) -> `H(Z | [%X, E]) = `H(Z | X). "Ciphertext conditioning contract": if `E` is a fresh encryption value (uniform over `p.-enc B` and independent from everything else), then conditioning on `E` does not change the conditional entropy of `Z` given `X`. The hypothesis `(forall x e, Pr[[X,E]=(x,e)] != 0)` is a technical condition to make all the conditional probabilities `Pr[ Z=c | [X,E]=(x,e) ]` well-defined in the cpr/centropy lemmas used below.
▶ homomorphic_encryption/idealized/idealized_ahe.v
6 helper
Name Section Lines Signature Meaning
Helper idealized_dec_correct Idealized_AHE 1 Lemma idealized_dec_correct : forall (dk : msgT) (r m : msgT), idealized_dec dk (idealized_enc (idealized_pub_of_priv dk) m r) = Some m. Decryption correctness - straightforward computation
Helper idealized_Emul_addM Idealized_AHE 4 Lemma idealized_Emul_addM : forall (k : pub_key IT), {morph enc_curry IT k : mr1 mr2 / mr_bop IT +%R idealized_rand_mul mr1 mr2 >-> idealized_Emul mr1 mr2}.
Helper idealized_Epow_scalarM Idealized_AHE 5 Lemma idealized_Epow_scalarM : forall (k : pub_key IT) (j : plain IT), {morph enc_curry IT k : mr / mr_bop_rplain IT *%R idealized_rand_pow mr j >-> idealized_Epow mr j}.
Helper idealized_Emul_assoc Idealized_AHE 1 Lemma idealized_Emul_assoc : associative idealized_Emul.
Helper idealized_Emul_comm Idealized_AHE 1 Lemma idealized_Emul_comm : commutative idealized_Emul.
Helper idealized_Emul_id Idealized_AHE 4 Lemma idealized_Emul_id : forall k : pub_key IT, left_id (enc_curry IT k (0, idealized_rand_id)) idealized_Emul.
▶ homomorphic_encryption/key_type.v
3 helper
Name Section Lines Signature Meaning
Helper key_type_eqP key_type_def 5 Lemma key_type_eqP : Equality.axiom key_type_eqb.
Helper key_type_natK key_type_def 1 Lemma key_type_natK : cancel key_type_to_nat nat_to_key_type.
Helper key_type_enumP key_type_def 1 Lemma key_type_enumP : Finite.axiom key_type_enum.
▶ homomorphic_encryption/paillier1999/paillier_ahe.v
6 helper
Name Section Lines Signature Meaning
Helper paillier_dec_correct_mixin paillier_instance 5 Lemma paillier_dec_correct_mixin (dk : PaillierPrivKey n) (u : {unit 'Z_n2}) (m : 'Z_n) : paillier_dec_for_mixin dk (paillier_enc_for_mixin (pub_of_priv dk) m u) = Some m.
Helper paillier_Emul_addM paillier_instance 6 Lemma paillier_Emul_addM : forall (k : pub_key PaillierHETypes), {morph enc_curry PaillierHETypes k : mr1 mr2 / mr_bop PaillierHETypes +%R paillier_rand_mul mr1 mr2 >-> paillier_Emul mr1 mr2}.
Helper paillier_Epow_scalarM paillier_instance 8 Lemma paillier_Epow_scalarM : forall (k : pub_key PaillierHETypes) (j : plain PaillierHETypes), {morph enc_curry PaillierHETypes k : mr / mr_bop_rplain PaillierHETypes *%R paillier_rand_pow mr j >-> paillier_Epow mr j}.
Helper paillier_Emul_assoc paillier_instance 1 Lemma paillier_Emul_assoc : associative paillier_Emul.
Helper paillier_Emul_comm paillier_instance 1 Lemma paillier_Emul_comm : commutative paillier_Emul.
Helper paillier_Emul_id paillier_instance 7 Lemma paillier_Emul_id : forall k : pub_key PT, left_id (enc_curry PT k (0, paillier_rand_id)) paillier_Emul.
▶ homomorphic_encryption/paillier1999/paillier_enc.v
13 helper
Name Section Lines Signature Meaning
Helper Zp_add_eqmod Top-level 10 Lemma Zp_add_eqmod (n : nat) (n_gt1 : (1 < n)%N) (m1 m2 : 'Z_n) : (m1 : nat) + m2 = (m1 + m2)%R %[mod n]. Helper: nat addition of Z_n elements equals Z_n addition mod n
Helper Zp_mulrn_nat Top-level 6 Lemma Zp_mulrn_nat (n : nat) (n_gt1 : (1 < n)%N) (m : 'Z_n) (k : nat) : ((m *+ k)%R : nat) = (((m : nat) * k) %% (Zp_trunc n).+2)%N. Helper: (m *+ k : 'Z_n) as nat equals (m * k) %% (Zp_trunc n).+2
Helper Zp_mulrn_eqmod Top-level 9 Lemma Zp_mulrn_eqmod (n : nat) (n_gt1 : (1 < n)%N) (m1 : 'Z_n) (m2 : nat) : (m1 : nat) * m2 = (m1 *+ m2)%R %[mod n]. Helper: nat mult of Z_n element by nat equals Z_n scalar mult mod n
Helper val_unit_exp Top-level 1 Lemma val_unit_exp (n : nat) (u : {unit 'Z_(n ^ 2)}) k : val (u ^+ k)%g = (val u) ^+ k.
Helper val_unit_mul Top-level 1 Lemma val_unit_mul (n : nat) (u v : {unit 'Z_(n ^ 2)}) : val (u * v)%g = val u * val v.
Helper n2_gt1 paillier_params 4 Lemma n2_gt1 : (1 < n2)%N. n^2 > 1 follows from n > 1
Helper expr_modn paillier_params 3 Lemma expr_modn (k : nat) : g ^+ k = g ^+ (k %% n)%N. Exponentiation of g depends only on exponent mod n
Helper enc_mul_dist paillier_params 8 Lemma enc_mul_dist : forall (m1 m2 : 'Z_n) (r1 r2 : {unit 'Z_n2}), paillier_enc m1 r1 * paillier_enc m2 r2 = paillier_enc (m1 + m2) (r1 * r2)%g. Encryption multiplication distributes as addition on messages
Helper enc_exp_dist paillier_params 9 Lemma enc_exp_dist : forall (m1 : 'Z_n) (m2 : nat) (r : {unit 'Z_n2}), (paillier_enc m1 r) ^+ m2 = paillier_enc (m1 *+ m2) (r ^+ m2)%g. Encryption exponentiation distributes as scalar multiplication
Helper euler_unit paillier_params 5 Lemma euler_unit (x : {unit 'Z_n2}) : (val x) ^+ phi_n2 = 1. Euler's theorem: any unit raised to phi(n^2) equals 1
Helper nth_powers_vanish paillier_params 4 Lemma nth_powers_vanish (r : {unit 'Z_n2}) : (val r) ^+ n ^+ lambda = 1. n-th powers vanish when raised to lambda (subgroup structure)
Helper ciphertext_to_lambda paillier_params 6 Lemma ciphertext_to_lambda (m : 'Z_n) (r : {unit 'Z_n2}) : (paillier_enc m r) ^+ lambda = g ^+ (lambda * m). Raising ciphertext to lambda strips randomness
Helper decryption_unique paillier_params 4 Lemma decryption_unique (m1 m2 : 'Z_n) (r1 r2 : {unit 'Z_n2}) : (paillier_enc m1 r1) ^+ lambda = (paillier_enc m2 r2) ^+ lambda -> m1 = m2. Distinct messages give distinct lambda-powers (unique decryption)