Added exact lemma for parameteriezed global hybrids.#992
Added exact lemma for parameteriezed global hybrids.#992alleystoughton wants to merge 1 commit intomainfrom
Conversation
fdupress
left a comment
fdupress
left a comment
There was a problem hiding this comment.
Looks good to me. Minor comment on what I think belongs in statements and what I think should be hidden in proofs.
|
|
||
| module Hybrid : HYBRID = { | ||
| proc main(i : int) : bool = { | ||
| proc main(y : unit, i : int) : bool = { |
There was a problem hiding this comment.
Perhaps it would be better to keep this as it was, and use transitivity or proc change in the proofs (as opposed to in the definition and statements) to catch the mismatch? This is not blocking merge; just thinking of the "exemplary" quality of examples. (And yes, we should also revisit older examples, that are only exemplary in that they could be done at the time.)
There was a problem hiding this comment.
Thanks, but Hybrid is part of the proof. The concluding lemma doesn't mention it.
lemma GReal_GIdeal &m :
`|Pr[GReal.main() @ &m : res] - Pr[GIdeal.main() @ &m : res]| <=
(m - 1)%r * (1%r / (2 ^ n)%r)
So I think it's simpler to use the dummy argument.
There was a problem hiding this comment.
There is a proof step I want to improve, but should I merge when ready?
Added global hybrid lemma for hybrids parameterized by oracles that gives an equality, not just an upper bound. Updated the DDH global hybrid example to use it. Idea based on the Nominal-SSProve paper "Mechanizing Nested Hybrid Arguments", https://eprint.iacr.org/2025/1122.
alleystoughton
force-pushed
the
new-global-hybrid-lemma
branch
from
33a2845 to
b74d6cb
Compare
2 participants
Added global hybrid lemma for hybrids parameterized by oracles that gives
an equality, not just an upper bound. Updated the DDH global hybrid example
to use it. Idea based on the Nominal-SSProve paper "Mechanizing Nested Hybrid
Arguments", https://eprint.iacr.org/2025/1122.