feat(ProgramLogic): eRHL program logic, TV distance, Fiat-Shamir, and ElGamal IND-CPA#116

Merged

quangvdao merged 15 commits intomasterfrom

quang/more-program-logic

Mar 7, 2026

Commits on Mar 5, 2026

feat: rename SigmaAlg to SigmaProtocol, add game_rule simp set, extend program logic tactics
quangvdao
committed

Commits on Mar 6, 2026

feat(ElGamal): prove Part A sorry's — all-random hybrid distributional equivalence
quangvdao
committed
feat(ProgramLogic): prove wp_uniformSample, relTriple_uniformSample_bij, tvDist_simulateQ bound
quangvdao
committed
feat: generalize QueryBound, prove Schnorr security, add eRHL bridges and OptimalCoupling
quangvdao
committed
feat(ElGamal): add hstart chain + main IND-CPA theorem (4 sorry's remain)
quangvdao
committed
chore: remove unused [DecidableEq β] from tvDist_map_le lemmas
quangvdao
committed
feat(ElGamal): finish hybrid-to-real IND-CPA bridge
quangvdao
committed
feat(ToMathlib): prove optimal coupling existence
quangvdao
committed
feat(ProgramLogic): finish quantitative bridge lemmas
quangvdao
committed

Commits on Mar 7, 2026