refactor(Crypto/PRG): allow explicit seed and ideal distributions - #1071
Open
SamuelSchlesinger wants to merge 2 commits into
Open
SamuelSchlesinger wants to merge 2 commits into
SamuelSchlesinger wants to merge 2 commits into
Conversation
SamuelSchlesinger
requested review from
arademaker,
chenson2018,
crei,
fmontesi and
sorrachai
as code owners
October 4, 2026 22:30
SamuelSchlesinger
added this pull request to stack #1064
October 4, 2026 22:31
SamuelSchlesinger
force-pushed
the
samschles/crypto-pr-09-prg-distributions
branch
from
October 4, 2026 23:03
0ef0536 to
f05d7d8
Compare
SamuelSchlesinger
force-pushed
the
samschles/crypto-pr-09-prg-distributions
branch
from
October 4, 2026 23:33
f05d7d8 to
56d36e3
Compare
SamuelSchlesinger
removed this pull request from stack #1064
October 5, 2026 20:06
SamuelSchlesinger
added this pull request to stack #1077
October 5, 2026 20:07
SamuelSchlesinger
force-pushed
the
samschles/crypto-pr-09-prg-distributions
branch
from
October 5, 2026 20:19
56d36e3 to
4872c75
Compare
SamuelSchlesinger
removed this pull request from stack #1077
October 5, 2026 20:20
SamuelSchlesinger
added this pull request to stack #1080
October 5, 2026 20:20
SamuelSchlesinger
removed this pull request from stack #1080
October 5, 2026 20:43
SamuelSchlesinger
added this pull request to stack #1082
October 5, 2026 20:43
Generalizes the PRG experiments from #876 so that the seed and ideal distributions are explicit arguments. They are auto-params defaulting to `PMF.uniformOfFintype _`, so on finite types `G.Secure Admissible ε`, `Family.Secure`, and the existing results keep their meaning without changes at call sites. Computational definitions over infinite sample spaces, such as words, can now reuse these experiments. Advantage and asymptotic security are now expressed through `Game` and `Negligible`. The `[Fintype]` and `[Nonempty]` instances move from the definitions to the results that need them, so callers that pass them explicitly need to drop them. `secure_zero_iff_outputDist_eq_uniform` becomes `secure_zero_iff_outputDist_eq`, which compares with the ideal distribution; a deprecated alias keeps the old name.
SamuelSchlesinger
force-pushed
the
samschles/crypto-pr-09-prg-distributions
branch
from
October 5, 2026 20:56
4872c75 to
058e07b
Compare
SamuelSchlesinger
removed this pull request from stack #1082
October 5, 2026 20:57
SamuelSchlesinger
added this pull request to stack #1084
October 5, 2026 20:57
SamuelSchlesinger
removed this pull request from stack #1084
October 5, 2026 21:02
SamuelSchlesinger
changed the base branch from
samschles/crypto-pr-08-hybrid-arguments
to
main
October 5, 2026 21:02
SamuelSchlesinger
changed the base branch from
main
to
samschles/crypto-pr-08-hybrid-arguments
October 5, 2026 21:03
SamuelSchlesinger
added this pull request to stack #1085
October 5, 2026 21:03
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Generalizes the PRG experiments to accept explicit seed and ideal distributions. Omitted distributions default to uniform sampling on finite types, preserving the experiments of Boneh and Shoup, Attack Game 3.1. Explicit distributions support nonuniform sampling and infinite ambient types.
Reuses
Game.advantageand defines family security throughGame.SecureandGame.SecureWithError. Finite and nonempty instances are needed for uniform defaults and finite counting results; calls passing the old instance arguments explicitly need adjustment.Zero-error security against all tests is characterized by equality with the supplied ideal distribution. Renames
secure_zero_iff_outputDist_eq_uniformtosecure_zero_iff_outputDist_eq, retaining the old name as a deprecated alias.Depends on #1070.
Composed with Claude Code; reviewed and restacked with Codex.