Skip to content

Bounds in ℝ≥0 #25

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MarcIlunga merged 1 commit into from
Oct 13, 2026
Merged

Bounds in ℝ≥0 #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,11 @@ globally; use `letI` or a wrapper carrier.
- New and changed code passes Mathlib's standard linter set:
`lake env lean -Dweak.linter.mathlibStandardSet=true <file>` reports nothing. The set is not
yet enabled in the lakefile, because older code does not pass it.
- Security bounds are stated in `ℝ≥0`, as `Δ R S ≤ (b : ℝ≥0)`; the coercion to `ℝ≥0∞` is
additive and order-preserving, so `push_cast` moves it. `ENNReal.ofReal` appears only where
the distances are defined from real probabilities (`transcriptDistance`, the advantages,
`advantageDistance`) and in the lemmas that bridge to them (`transcriptDistance_le`,
`transcriptDistance_le_of_advantage_le`).

## Naming and ownership

Expand Down
82 changes: 41 additions & 41 deletions THEORY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -871,30 +871,30 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
[Program.inline]: src/RandomSystems/Converter/ProgramAttachment.lean#L258
[Program.combine]: src/RandomSystems/Converter/ProgramAttachment.lean#L429
[Program.trim_apply_ofProgramOn_automaton]: src/RandomSystems/Converter/ProgramAttachment.lean#L609
[RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L225
[Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L162
[Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L168
[RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L228
[Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L165
[Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L171
[IsDDD]: src/RandomSystems/System/InterfaceSystem.lean#L968
[RandomSystem.decisionProbability]: src/RandomSystems/Distance/Decision.lean#L247
[Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L121
[Domain.Distinguisher.probability]: src/RandomSystems/Distance/Distinguisher.lean#L125
[Domain.Distinguisher.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L131
[advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L140
[advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L142
[advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L145
[RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L153
[advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L182
[Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L193
[DistinguisherBehavior.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L204
[DistinguisherBehavior.advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L214
[DistinguisherBehavior.advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L216
[DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L219
[DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L224
[RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L232
[DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L277
[DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L290
[Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L251
[Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L316
[RandomSystem.decisionProbability]: src/RandomSystems/Distance/Decision.lean#L262
[Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L122
[Domain.Distinguisher.probability]: src/RandomSystems/Distance/Distinguisher.lean#L126
[Domain.Distinguisher.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L132
[advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L141
[advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L143
[advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L146
[RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L154
[advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L196
[Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L207
[DistinguisherBehavior.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L218
[DistinguisherBehavior.advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L228
[DistinguisherBehavior.advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L230
[DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L233
[DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L238
[RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L246
[DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L291
[DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L304
[Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L265
[Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L330
[absorbAll]: src/RandomSystems/Distance/Absorption.lean#L42
[RandomSystem.restrict]: src/RandomSystems/Distance/Restriction.lean#L59
[RandomSystem.restrict_restrict]: src/RandomSystems/Distance/Restriction.lean#L67
Expand All @@ -904,14 +904,14 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
[DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50
[PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54
[PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37
[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L289
[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L298
[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L391
[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L461
[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L504
[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L758
[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L837
[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L862
[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L290
[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L299
[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L392
[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L462
[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L505
[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L759
[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L838
[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L863
[PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455
[PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495
[PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515
Expand Down Expand Up @@ -958,10 +958,10 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
[Interface.Resource.ofFunction]: src/ConstructiveCryptography/Functional.lean#L56
[Interface.Resource.ofConditional]: src/ConstructiveCryptography/Functional.lean#L38
[Interface.Resource.sample]: src/ConstructiveCryptography/Functional.lean#L176
[Interface.withMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L51
[Interface.Game]: src/ConstructiveCryptography/InterfaceGame.lean#L62
[Interface.liftMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L65
[Interface.Game.visible]: src/ConstructiveCryptography/InterfaceGame.lean#L83
[Interface.withMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L52
[Interface.Game]: src/ConstructiveCryptography/InterfaceGame.lean#L63
[Interface.liftMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L66
[Interface.Game.visible]: src/ConstructiveCryptography/InterfaceGame.lean#L84
[Interface.Game.ofPDG]: src/ConstructiveCryptography/PresentedGame.lean#L54
[Interface.Game.visible_ofPDG]: src/ConstructiveCryptography/PresentedGame.lean#L64
[Interface.Game.conditionallyEquivalent_ofPDG_iff]: src/ConstructiveCryptography/PresentedGame.lean#L74
Expand Down Expand Up @@ -1033,12 +1033,12 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X
[Games.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L93
[DistinctionGames.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L148
[Games.absorb_comp]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L101
[Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L99
[Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L149
[Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L210
[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L88
[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L93
[Interface.win_le]: src/ConstructiveCryptography/InterfaceGame.lean#L194
[Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L100
[Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L150
[Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L211
[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L89
[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L94
[Interface.win_le]: src/ConstructiveCryptography/InterfaceGame.lean#L195

<!-- Declarations: §4 -->

Expand Down
5 changes: 3 additions & 2 deletions src/ConstructiveCryptography/InterfaceGame.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ probability that its MBO is set on fixed queries (CR18, Theorem 4.17), through
namespace SystemAlgebra.Interface

open CategoryTheory ConstructiveCryptography
open scoped NNReal

/-- The interface of `A` with the MBO: its replies carry the MBO. -/
abbrev withMBO (A : Interface) : Interface where
Expand Down Expand Up @@ -208,9 +209,9 @@ Theorem 4.17): a game on an interface conditionally equivalent to a resource `T`
unset with probability at least `1 - ε` on the queries of each transcript of `T`, has its
visible resource within `ε` of `T`. -/
theorem dist_visible_le {A : Interface} {G : Game A} {T : Resource A}
(hc : DistinctionGames.ConditionallyEquivalent G T) {ε : ℝ}
(hc : DistinctionGames.ConditionallyEquivalent G T) {ε : ℝ≥0}
(hε : ∀ h, T.1 h ≠ 0 → 1 - ε ≤ G.1.1.unsetProbability (h.map Prod.fst)) :
CryptographicAlgebra.distance (DistinctionGames.visible G) T ≤ ENNReal.ofReal ε := by
CryptographicAlgebra.distance (DistinctionGames.visible G) T ≤ ε := by
-- The distance of `CompatiblePseudoMetric` (its field `fibreMetric`) on interfaces is the
-- systems-level transcript distance of the random systems.
rw [cc_distance_eq]
Expand Down
10 changes: 5 additions & 5 deletions src/ConstructiveCryptography/PresentedGame.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ the ideal answers.
namespace SystemAlgebra

open Probability ConstructiveCryptography
open scoped SystemAlgebra
open scoped SystemAlgebra NNReal

namespace Interface

Expand Down Expand Up @@ -88,9 +88,9 @@ every admitted query sequence, then `R` and `S` are at most `ε` apart. -/
theorem game_dist_le {A : Interface}
{G : PDG (Σ i, A.X i) (Σ i, A.Y i) A.inputDomain} {hG : G.isProbDist} {R S : Resource A}
(visible : R.1 = PDS.behavior G.underlying (PDG.underlying_probability hG))
(equiv : Game.ofPDG G hG visible |≡ S) {ε : ℝ}
(equiv : Game.ofPDG G hG visible |≡ S) {ε : ℝ≥0}
(hbad : ∀ xs, xs = [] ∨ A.domain xs → G.badProbability xs ≤ ε) :
Δ R S ≤ ENNReal.ofReal ε := by
Δ R S ≤ ε := by
-- Δ(R, S) = Δ((ofPDG G)⁻, S) (`R` is the visible resource of the presented game)
-- ≤ ε (`ofPDG G |≡ S`, MBO unset with probability ≥ 1 - ε)
--
Expand Down Expand Up @@ -220,9 +220,9 @@ theorem game_dist_ofSingleFunction_le {I K X Y : Type}
{P : Distribution K} [Distribution.IsProbability P] {f : K → X → Y} {bad : K → MC X}
{R S : Resource ⟨I, fun _ => X, fun _ => Y, D, hD, bound, hb⟩}
(equiv : Game.ofSingleFunction D hD bound hb P f bad |≡ S)
(visible : R = Resource.sample P (fun k => Resource.ofFunction (fun _ => f k))) {ε : ℝ}
(visible : R = Resource.sample P (fun k => Resource.ofFunction (fun _ => f k))) {ε : ℝ≥0}
(hbad : ∀ xs, xs = [] ∨ D xs → P.mass (fun k => (bad k).1 (xs.map Sigma.snd)) ≤ ε) :
Δ R S ≤ ENNReal.ofReal ε := by
Δ R S ≤ ε := by
-- `R` is the resource sampling the function.
subst visible
-- The distance bound for a presented game: `R` is presented by the visible systems of the
Expand Down
6 changes: 3 additions & 3 deletions src/Examples/AuthenticatedEncryption/Collision.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ replacement message, in either order.

open SystemAlgebra SystemAlgebra.DSL SystemAlgebra.Interface Probability
open Commons
open scoped SystemAlgebra
open scoped SystemAlgebra NNReal

namespace AuthenticatedEncryption

Expand Down Expand Up @@ -538,7 +538,7 @@ theorem collisionGame_badProbability_le (xs : List (Σ i, (AE.perPort M C q).X i
theorem hybrid_ideal_distance_le :
Δ (Hybrid scheme q) (AE.Ideal.perPort M C (budget := q) • Encryption.Real.perPort scheme :
Interface.Resource (AE.perPort M C q)) ≤
ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) :=
((q .enc) ^ 2 / Fintype.card M : ℝ≥0) :=
-- The distinguisher D on the left queries either system at the ports `enc` (sends `m`,
-- receives `c`) and `dec` (sends `c`, receives `m` or ⊥), at most `q p` times at port `p`;
-- replies return along the same wires.
Expand All @@ -561,7 +561,7 @@ theorem hybrid_ideal_distance_le :
-- Δ(Hybrid, ρ^ae(E_k)) ≤ sup_xs Pr[collision on xs] (game_dist_le; xs empty or admitted)
-- ≤ q_e² / |M| (collisionGame_badProbability_le)
game_dist_le (hybrid_visible scheme q) (collisionGame_conditionallyEquivalent scheme q)
(collisionGame_badProbability_le scheme q)
fun xs hxs => by push_cast; exact collisionGame_badProbability_le scheme q xs hxs

end Game

Expand Down
10 changes: 5 additions & 5 deletions src/Examples/AuthenticatedEncryption/Security.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ open CategoryTheory
open Commons
open ConstructiveCryptography ConstructiveCryptography.CryptographicAlgebra
open SystemAlgebra SystemAlgebra.Interface
open scoped SystemAlgebra
open scoped SystemAlgebra NNReal

namespace AuthenticatedEncryption

Expand All @@ -60,7 +60,7 @@ theorem ae_of_ind_cca_int_ptxt [AdmissibleDistinguishers]
AE.Secure scheme fun D =>
εptxt D + εcca (absorb ρ^ptxt D) + εptxt (absorb (ρ^ptxt ≫ ρ^cca) D) +
εcca (absorb (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt) D) +
ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) := by
((q .enc) ^ 2 / Fintype.card M : ℝ≥0) := by
cc_calc mixed (distinguisherAdvantage AdmissibleDistinguishers.admissible) using
(fun D _ R S => distinguisherAdvantage_le_distance _ D R S)
⟦E_k, D_k⟧ ≃[εptxt] ρ^ptxt • ⟦E_k, D_k⟧ := ptxt
Expand All @@ -71,7 +71,7 @@ theorem ae_of_ind_cca_int_ptxt [AdmissibleDistinguishers]
_ ≃[εcca ∘ absorb (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt)]
ρ^ptxt • ρ^cca • ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ :=
AdmissibleDistinguishers.substitutesWithin_context (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt) cca
_ ≈[ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M)] ⟦E$_k, D^⊥⟧ :=
_ ≈[((q .enc) ^ 2 / Fintype.card M : ℝ≥0)] ⟦E$_k, D^⊥⟧ :=
hybrid_ideal_distance_le scheme q

/-- The two assumptions of the implication. -/
Expand Down Expand Up @@ -124,7 +124,7 @@ theorem real_ideal_distance_le :
Δ ⟦E_k, D_k⟧ ⟦E$_k, D^⊥⟧ ≤
Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧) + Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧) +
Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧) + Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧) +
ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) := by
((q .enc) ^ 2 / Fintype.card M : ℝ≥0) := by
cc_calc statistical
⟦E_k, D_k⟧ ≈[Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧)] ρ^ptxt • ⟦E_k, D_k⟧ := le_rfl
_ ≈[Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧)] ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ :=
Expand All @@ -134,7 +134,7 @@ theorem real_ideal_distance_le :
_ ≈[Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧)] ρ^ptxt • ρ^cca • ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ :=
((distance_attach_le _ _ _).trans (distance_attach_le _ _ _)).trans
(distance_attach_le _ _ _)
_ ≈[ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M)] ⟦E$_k, D^⊥⟧ :=
_ ≈[((q .enc) ^ 2 / Fintype.card M : ℝ≥0)] ⟦E$_k, D^⊥⟧ :=
hybrid_ideal_distance_le scheme q

end AuthenticatedEncryption
19 changes: 17 additions & 2 deletions src/RandomSystems/Distance/Decision.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ a sample.

## Main results

* `RandomSystem.transcriptDistance_le`: a bound in `ℝ≥0` on the transcript laws under every
environment bounds the transcript distance
* `RandomSystem.decisionProbability_envProbe`: an environment followed by an event test
decides `1` with the probability of the event
* `RandomSystem.decisionProbability_gap_le`: decision gaps are at most the transcript
Expand All @@ -36,6 +38,7 @@ a sample.
namespace SystemAlgebra

open Classical Probability
open scoped NNReal

theorem Cons.queries_eq {A B : Type} {e : List B →. A} {h : List (A × B)}
(hc : Cons e h) : h.map Prod.fst = qsOf e (h.map Prod.snd) := by
Expand Down Expand Up @@ -232,11 +235,23 @@ theorem statDist_le_transcriptDistance {E : DDE (Σ i, X i) (Σ i, Y i)} {n :
ENNReal.ofReal (statDist (R.sLaw E.1 n) (S.sLaw E.1 n)) ≤ R.transcriptDistance S :=
le_iSup_of_le E (le_iSup_of_le n (le_iSup_of_le hn (le_iSup_of_le hc le_rfl)))

/-- **A bound on the transcript laws bounds the transcript distance**: if under every compatible
query-bounded environment the statistical distance of the transcript laws is at most `b`, the
transcript distance is at most `b`. -/
theorem transcriptDistance_le {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} {b : ℝ≥0}
(h : ∀ (E : DDE (Σ i, X i) (Σ i, Y i)) (n : ℕ), QueryBounded n E → 𝒟.Compatible E →
statDist (R.sLaw E.1 n) (S.sLaw E.1 n) ≤ b) :
R.transcriptDistance S ≤ b :=
iSup_le fun E => iSup_le fun n => iSup_le fun hn => iSup_le fun hc => by
-- The real bound `b` read in `ℝ≥0∞` is `b` itself.
rw [← ENNReal.ofReal_coe_nnreal]
exact ENNReal.ofReal_le_ofReal (h E n hn hc)

theorem transcriptDistance_le_one {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟}
(hR : R.RepliesAtQueriedInterface) (hS : S.RepliesAtQueriedInterface) :
R.transcriptDistance S ≤ 1 := by
refine iSup_le fun E => iSup_le fun n => iSup_le fun _ => iSup_le fun hc => ?_
apply ENNReal.ofReal_le_one.mpr
rw [← ENNReal.coe_one]
refine transcriptDistance_le fun E n _ hc => ?_
have hr := R.sLaw_isProbDist (hc R hR) n
have hs := S.sLaw_isProbDist (hc S hS) n
exact (statDist_le_weight hr.1 hs.1).trans_eq hr.2
Expand Down
14 changes: 14 additions & 0 deletions src/RandomSystems/Distance/Distinguisher.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ serial composition is absorbing its PDCs in turn.
namespace SystemAlgebra

open Classical Probability
open scoped NNReal

section Attachment

Expand Down Expand Up @@ -178,6 +179,19 @@ theorem RandomSystem.transcriptDistance_eq_iSup {𝒟 : Domain (Σ i, X i) (Σ i
_ = R.transcriptDistance S := ENNReal.ofReal_toReal
(ne_top_of_le_ne_top ENNReal.one_ne_top (transcriptDistance_le_one hR hS))

/-- **A bound on every advantage bounds the transcript distance**: if every probabilistic
distinguisher's advantage is at most `b`, the transcript distance is at most `b`. -/
theorem RandomSystem.transcriptDistance_le_of_advantage_le {𝒟 : Domain (Σ i, X i) (Σ i, Y i)}
{R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟}
(hR : R.RepliesAtQueriedInterface) (hS : S.RepliesAtQueriedInterface) {b : ℝ≥0}
(h : ∀ P : 𝒟.Distinguisher, |P.probability R - P.probability S| ≤ b) :
R.transcriptDistance S ≤ b := by
-- The transcript distance is the largest advantage; each is at most `b`.
rw [RandomSystem.transcriptDistance_eq_iSup hR hS]
refine iSup_le fun P => ?_
rw [Domain.Distinguisher.advantage, ← ENNReal.ofReal_coe_nnreal]
exact ENNReal.ofReal_le_ofReal (h P)

/-- The advantage of a probabilistic distinguisher is at most the transcript distance. -/
theorem Domain.Distinguisher.advantage_le_transcriptDistance {𝒟 : Domain (Σ i, X i) (Σ i, Y i)}
(P : 𝒟.Distinguisher) {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟}
Expand Down
Loading
Loading