diff --git a/THEORY.md b/THEORY.md index 1d4e83b..c4c3ce9 100644 --- a/THEORY.md +++ b/THEORY.md @@ -337,23 +337,23 @@ extension are in [Examples](src/Examples/README.md). [Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L126 [RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L158 [Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L211 -[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L309 -[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L344 -[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L486 -[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L529 -[RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L543 -[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L762 -[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L880 +[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L311 +[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L362 +[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L504 +[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L547 +[RandomSystem.GameEquivalent]: src/RandomSystems/Game/MBO.lean#L561 +[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L780 +[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: src/RandomSystems/Game/MBO.lean#L898 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L464 -[Interface]: src/RandomSystems/Typed/Interface.lean#L47 -[TypedSystem]: src/RandomSystems/Typed/Interface.lean#L115 -[TypedConverter]: src/RandomSystems/Typed/Interface.lean#L150 -[TypedConverter.comp]: src/RandomSystems/Typed/Interface.lean#L157 -[TypedConverter.id]: src/RandomSystems/Typed/Interface.lean#L162 -[TypedConverter.attach]: src/RandomSystems/Typed/Interface.lean#L213 +[Interface]: src/RandomSystems/Typed/Interface.lean#L40 +[TypedSystem]: src/RandomSystems/Typed/Interface.lean#L136 +[TypedConverter]: src/RandomSystems/Typed/Interface.lean#L175 +[TypedConverter.comp]: src/RandomSystems/Typed/Interface.lean#L182 +[TypedConverter.id]: src/RandomSystems/Typed/Interface.lean#L187 +[TypedConverter.attach]: src/RandomSystems/Typed/Interface.lean#L240 [Interface.tensor]: src/RandomSystems/Typed/Parallel.lean#L89 [TypedSystem.parallel]: src/RandomSystems/Typed/Parallel.lean#L157 [TypedConverter.parallel]: src/RandomSystems/Typed/Parallel.lean#L214 @@ -390,6 +390,6 @@ extension are in [Examples](src/Examples/README.md). [SymmetricEncryption.encryptions]: src/Commons/Definitions/Encryption.lean#L106 [AE.INDCCA]: src/Commons/Definitions/AEAD.lean#L232 [correctedChain]: src/Examples/AuthenticatedEncryption/Security.lean#L137 -[collision_mass_le]: src/Examples/AuthenticatedEncryption/Collision.lean#L64 +[collision_mass_le]: src/Examples/AuthenticatedEncryption/Collision.lean#L65 [exists_pair_one_sub_supAgreement_le]: src/Probability/MultiCoupling.lean#L620 [not_supAgreement_disagreement_le_every_pair]: src/Probability/MultiCoupling.lean#L782 diff --git a/src/ConstructiveCryptography/DSL/GRAMMAR.md b/src/ConstructiveCryptography/DSL/GRAMMAR.md index 59f4b82..62d334b 100644 --- a/src/ConstructiveCryptography/DSL/GRAMMAR.md +++ b/src/ConstructiveCryptography/DSL/GRAMMAR.md @@ -463,10 +463,10 @@ before/after proofs, expression guards, negative tests and exact rewrite traces [Program]: ../../RandomSystems/Converter/Program.lean#L49 [Program.PortPreserving]: ../../RandomSystems/Converter/Program.lean#L127 [automatonSystem_eq_of_bisim]: ../../RandomSystems/System/Automaton.lean#L93 -[Interface.queryBudget]: ../../RandomSystems/Typed/Interface.lean#L70 -[Interface.portBudget]: ../../RandomSystems/Typed/Interface.lean#L97 +[Interface.queryBudget]: ../../RandomSystems/Typed/Interface.lean#L64 +[Interface.portBudget]: ../../RandomSystems/Typed/Interface.lean#L94 [TypedSystem.source]: ../../RandomSystems/Typed/Source.lean#L55 -[TypedSystem.ofAutomaton]: ../../RandomSystems/Typed/Automaton.lean#L55 +[TypedSystem.ofAutomaton]: ../../RandomSystems/Typed/Automaton.lean#L77 [TypedConverter.rightContext]: ../../RandomSystems/Typed/Context.lean#L113 [TypedConverter.filter]: ../../RandomSystems/Typed/Filter.lean#L64 [TypedConverter.ofProgram]: ../../RandomSystems/Typed/DSL/Converters.lean#L46 @@ -485,12 +485,12 @@ before/after proofs, expression guards, negative tests and exact rewrite traces [elabExactDecls]: Elaborator.lean#L826 [elabFilter]: Elaborator.lean#L1139 [sourcesAt]: Elaborator.lean#L730 -[MemorylessSource]: ../../Commons/Definitions/Ideal.lean#L321 -[MemorylessSource.memoryless_eq]: ../../Commons/Definitions/Ideal.lean#L328 +[MemorylessSource]: ../../Commons/Definitions/Ideal.lean#L363 +[MemorylessSource.memoryless_eq]: ../../Commons/Definitions/Ideal.lean#L370 [WriteThrough]: ../../Examples/DSL/Components.lean#L108 [cc_normalize]: ../Tactics/Basic.lean#L34 [cc_nonexpand]: ../Tactics/Categorical.lean#L171 -[cc_nonexpand-interfaces]: ../Notation.lean#L167 +[cc_nonexpand-interfaces]: ../Notation.lean#L176 [cc_triangle]: ../Tactics/Categorical.lean#L160 [cc_construct]: ../Tactics/Categorical.lean#L47 [cc_calc]: ../Tactics/Substitution.lean#L105 diff --git a/src/ConstructiveCryptography/README.md b/src/ConstructiveCryptography/README.md index 9d44e01..4113b2d 100644 --- a/src/ConstructiveCryptography/README.md +++ b/src/ConstructiveCryptography/README.md @@ -549,10 +549,10 @@ compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness [substitutionRelaxation_idem]: Substitution/Relaxation.lean#L287 [Implication.exists_serial_simulators]: Substitution/Construction.lean#L73 [Constructs.derivable_serial_simulators]: Substitution/Construction.lean#L158 -[Domain.Distinguisher.advantage_le_winProbability]: ../RandomSystems/Game/MBO.lean#L762 +[Domain.Distinguisher.advantage_le_winProbability]: ../RandomSystems/Game/MBO.lean#L780 [Domain.Distinguisher.exists_absorbRight]: ../RandomSystems/Distance/Distinguisher.lean#L334 [Domain.SolverBehavior.absorb]: ../RandomSystems/Game/MBOAttachment.lean#L2217 -[Interface]: ../RandomSystems/Typed/Interface.lean#L47 +[Interface]: ../RandomSystems/Typed/Interface.lean#L40 [Interface.associator]: Instances/Monoidal.lean#L56 [Interface.associator_naturality]: Instances/Monoidal.lean#L96 [Interface.distinguishers]: Instances/Algebra.lean#L183 @@ -590,21 +590,21 @@ compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness [PDCBehavior.liftMBO_comp]: ../RandomSystems/Game/MBOAttachment.lean#L1524 [PDCBehavior.liftMBO_id]: ../RandomSystems/Game/MBOAttachment.lean#L504 [PDCBehavior.tensor_id]: ../RandomSystems/Converter/ConverterTensor.lean#L709 -[RandomSystem.ConditionallyEquivalent]: ../RandomSystems/Game/MBO.lean#L529 -[RandomSystem.MonotoneMBO]: ../RandomSystems/Game/MBO.lean#L309 +[RandomSystem.ConditionallyEquivalent]: ../RandomSystems/Game/MBO.lean#L547 +[RandomSystem.MonotoneMBO]: ../RandomSystems/Game/MBO.lean#L311 [RandomSystem.parallel]: ../RandomSystems/Cumulative/CumulativeOperations.lean#L136 -[RandomSystem.visible]: ../RandomSystems/Game/MBO.lean#L344 +[RandomSystem.visible]: ../RandomSystems/Game/MBO.lean#L362 [RandomSystem.visible_attach_liftMBO]: ../RandomSystems/Game/MBOAttachment.lean#L628 -[TypedConverter]: ../RandomSystems/Typed/Interface.lean#L150 -[TypedConverter.attach]: ../RandomSystems/Typed/Interface.lean#L213 +[TypedConverter]: ../RandomSystems/Typed/Interface.lean#L175 +[TypedConverter.attach]: ../RandomSystems/Typed/Interface.lean#L240 [TypedConverter.attachGame]: ../RandomSystems/Typed/Game.lean#L49 -[TypedConverter.comp]: ../RandomSystems/Typed/Interface.lean#L157 +[TypedConverter.comp]: ../RandomSystems/Typed/Interface.lean#L182 [TypedConverter.comp_associator]: ../RandomSystems/Typed/ConverterCoherence.lean#L162 [TypedConverter.comp_leftUnitor]: ../RandomSystems/Typed/ConverterCoherence.lean#L199 [TypedConverter.comp_rightUnitor]: ../RandomSystems/Typed/ConverterCoherence.lean#L228 -[TypedConverter.comp_smul]: ../RandomSystems/Typed/Interface.lean#L233 -[TypedConverter.id]: ../RandomSystems/Typed/Interface.lean#L162 -[TypedConverter.identity_attach]: ../RandomSystems/Typed/Interface.lean#L227 +[TypedConverter.comp_smul]: ../RandomSystems/Typed/Interface.lean#L261 +[TypedConverter.id]: ../RandomSystems/Typed/Interface.lean#L187 +[TypedConverter.identity_attach]: ../RandomSystems/Typed/Interface.lean#L255 [TypedConverter.parallel]: ../RandomSystems/Typed/Parallel.lean#L214 [TypedConverter.parallel_attach]: ../RandomSystems/Typed/ParallelAttachment.lean#L27 [TypedConverter.parallel_rename]: ../RandomSystems/Typed/TensorRename.lean#L132 @@ -614,7 +614,7 @@ compose [9, Definition 2.4.3 and Theorem 2.4.4]: a witness [TypedConverter.rename_refl]: ../RandomSystems/Typed/Relabel.lean#L71 [TypedGame]: ../RandomSystems/Typed/Game.lean#L46 [TypedGame.visible]: ../RandomSystems/Typed/Game.lean#L90 -[TypedSystem]: ../RandomSystems/Typed/Interface.lean#L115 +[TypedSystem]: ../RandomSystems/Typed/Interface.lean#L136 [TypedSystem.dummy]: ../RandomSystems/Typed/SystemCoherence.lean#L101 [TypedSystem.parallel]: ../RandomSystems/Typed/Parallel.lean#L157 [TypedSystem.parallel_assoc_mass]: ../RandomSystems/Typed/SystemCoherence.lean#L89 diff --git a/src/Examples/README.md b/src/Examples/README.md index 1526be1..eab835b 100644 --- a/src/Examples/README.md +++ b/src/Examples/README.md @@ -114,7 +114,7 @@ exercised in [Usability][ExUse]. [cca_bisim]: AuthenticatedEncryption/Oracle.lean#L194 [aeIdeal_bisim]: AuthenticatedEncryption/Oracle.lean#L247 [encryptionReal_bisim]: AuthenticatedEncryption/Oracle.lean#L377 -[hybrid_ideal_distance_le]: AuthenticatedEncryption/Collision.lean#L533 +[hybrid_ideal_distance_le]: AuthenticatedEncryption/Collision.lean#L521 [correctedChain]: AuthenticatedEncryption/Security.lean#L137 [correctedChain_cca]: AuthenticatedEncryption/Security.lean#L156 [correctedChain_ptxt]: AuthenticatedEncryption/Security.lean#L161 diff --git a/src/RandomSystems/Distance/README.md b/src/RandomSystems/Distance/README.md index ba4e982..e26ac1c 100644 --- a/src/RandomSystems/Distance/README.md +++ b/src/RandomSystems/Distance/README.md @@ -236,6 +236,6 @@ Games build on this bound: see [Game](../Game/README.md#identical-until-bad). [RandomSystem.sLaw_restrict]: Restriction.lean#L104 [RandomSystem.transcriptDistance_restrict_le]: Restriction.lean#L136 [RandomSystem.transcriptDistance_le_add_of_ratio_on_good]: HCoefficient.lean#L44 -[transcriptCost]: UntilBad.lean#L42 -[RandomSystem.one_sub_le_sum_tSupp]: UntilBad.lean#L69 -[RandomSystem.transcriptDistance_le_of_transcriptCost_le]: UntilBad.lean#L150 +[transcriptCost]: UntilBad.lean#L44 +[RandomSystem.one_sub_le_sum_tSupp]: UntilBad.lean#L99 +[RandomSystem.transcriptDistance_le_of_transcriptCost_le]: UntilBad.lean#L180 diff --git a/src/RandomSystems/Game/README.md b/src/RandomSystems/Game/README.md index 1bbfcd7..49a4cd4 100644 --- a/src/RandomSystems/Game/README.md +++ b/src/RandomSystems/Game/README.md @@ -131,20 +131,20 @@ between original and replacement messages. -[RandomSystem.MonotoneMBO]: MBO.lean#L309 -[RandomSystem.visible]: MBO.lean#L344 -[DDE.blindMBO]: MBO.lean#L414 -[RandomSystem.winProbability]: MBO.lean#L486 -[RandomSystem.ConditionallyEquivalent]: MBO.lean#L529 -[RandomSystem.GameEquivalent]: MBO.lean#L543 -[Domain.Distinguisher.advantage_le_winProbability]: MBO.lean#L762 -[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: MBO.lean#L866 -[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: MBO.lean#L880 -[Domain.Distinguisher.winProbability_le_of_unsetProbability]: MBO.lean#L957 -[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: MBO.lean#L982 -[Domain.Distinguisher.winProbability_le_of_transcriptCost_le]: UntilBad.lean#L152 -[RandomSystem.GameEquivalent.transcriptDistance_visible_le]: UntilBad.lean#L181 -[PDG.gameEquivalent_behavior_of_isCoupling]: UntilBad.lean#L213 +[RandomSystem.MonotoneMBO]: MBO.lean#L311 +[RandomSystem.visible]: MBO.lean#L362 +[DDE.blindMBO]: MBO.lean#L432 +[RandomSystem.winProbability]: MBO.lean#L504 +[RandomSystem.ConditionallyEquivalent]: MBO.lean#L547 +[RandomSystem.GameEquivalent]: MBO.lean#L561 +[Domain.Distinguisher.advantage_le_winProbability]: MBO.lean#L780 +[Domain.Distinguisher.winProbability_eq_of_gameEquivalent]: MBO.lean#L884 +[Domain.Distinguisher.advantage_le_winProbability_of_gameEquivalent]: MBO.lean#L898 +[Domain.Distinguisher.winProbability_le_of_unsetProbability]: MBO.lean#L975 +[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: MBO.lean#L1000 +[Domain.Distinguisher.winProbability_le_of_transcriptCost_le]: UntilBad.lean#L144 +[RandomSystem.GameEquivalent.transcriptDistance_visible_le]: UntilBad.lean#L173 +[PDG.gameEquivalent_behavior_of_isCoupling]: UntilBad.lean#L205 [PDCBehavior.liftMBO]: MBOAttachment.lean#L464 [PDCBehavior.liftMBO_id]: MBOAttachment.lean#L504 [PDCBehavior.liftMBO_comp]: MBOAttachment.lean#L1524 diff --git a/src/RandomSystems/Typed/README.md b/src/RandomSystems/Typed/README.md index e2f5f10..728e780 100644 --- a/src/RandomSystems/Typed/README.md +++ b/src/RandomSystems/Typed/README.md @@ -235,20 +235,20 @@ typed system sampling the ideal function, under the fixed-query factorization. -[Interface]: Interface.lean#L47 -[Interface.queryBudget]: Interface.lean#L70 -[Interface.portBudget]: Interface.lean#L97 +[Interface]: Interface.lean#L40 +[Interface.queryBudget]: Interface.lean#L64 +[Interface.portBudget]: Interface.lean#L94 [restrict]: ../System/Basic.lean#L798 -[TypedSystem]: Interface.lean#L115 +[TypedSystem]: Interface.lean#L136 [RandomSystem.RepliesAtQueriedInterface]: ../Cumulative/Cumulative.lean#L74 -[TypedConverter]: Interface.lean#L150 -[TypedConverter.ofDDC]: Interface.lean#L166 -[TypedConverter.comp]: Interface.lean#L157 -[TypedConverter.id]: Interface.lean#L162 -[TypedConverter.attach]: Interface.lean#L213 -[TypedConverter.identity_attach]: Interface.lean#L227 -[TypedConverter.comp_smul]: Interface.lean#L233 -[TypedConverter.ofDDC_eq_comp]: Interface.lean#L195 +[TypedConverter]: Interface.lean#L175 +[TypedConverter.ofDDC]: Interface.lean#L191 +[TypedConverter.comp]: Interface.lean#L182 +[TypedConverter.id]: Interface.lean#L187 +[TypedConverter.attach]: Interface.lean#L240 +[TypedConverter.identity_attach]: Interface.lean#L255 +[TypedConverter.comp_smul]: Interface.lean#L261 +[TypedConverter.ofDDC_eq_comp]: Interface.lean#L214 [Interface.tensor]: Parallel.lean#L89 [TypedSystem.parallel]: Parallel.lean#L157 [TypedConverter.parallel]: Parallel.lean#L214 @@ -290,9 +290,9 @@ typed system sampling the ideal function, under the fixed-query factorization. [TypedConverter.attach_rightContext]: Context.lean#L126 [TypedConverter.attach_leftContext]: Context.lean#L131 [TypedSystem.source]: Source.lean#L55 -[TypedSystem.ofAutomaton]: Automaton.lean#L55 -[TypedSystem.ofAutomaton_map_congr]: Automaton.lean#L76 -[TypedSystem.parallel_ofAutomaton]: Automaton.lean#L100 +[TypedSystem.ofAutomaton]: Automaton.lean#L77 +[TypedSystem.ofAutomaton_map_congr]: Automaton.lean#L98 +[TypedSystem.parallel_ofAutomaton]: Automaton.lean#L122 [TypedSystem.ofProbAutomaton]: ProbAutomaton.lean [TypedSystem.ofProbAutomaton_eq_of_simulation]: ProbAutomaton.lean [TypedSystem.ofProbAutomaton_ofDeterministic]: ProbAutomaton.lean