[SamuelSchlesinger]

Change

Game hops can now be written as a calc chain that reads like the textbook sequence ("Game 0 = Game 1; |Game 1 − Game 2| ≤ ε₁; …"):

Game.advantage_le_of_approxEq
  (calc Pr[G₀] = Pr[G₁] := by rw [h₀₁]                     -- Game 0 = Game 1
    _ ≈[ε₁] Pr[G₂] := Game.approxEq_of_advantage_le h₁₂   -- |Game 1 − Game 2| ≤ ε₁
    _ ≈[ε₂] Pr[G₃] := Game.approxEq_of_advantage_le h₂₃)

• Probability/ApproxEq.lean adds x ≈[ε] y := |x - y| ≤ ε on ℝ, scoped to Probability like Pr[·]. It provides refl, symm, trans with a Trans instance that adds the errors (= steps compose through core), plus mono, and le_add/sub_le for one-sided bounds. It is general real-number mathematics with no crypto import.
• Crypto/Game/Hop.lean adds the four bridges to the ℝ≥0 advantage API: approxEq_iff_advantage_le, approxEq_of_advantage_le, approxEq_advantage and advantage_le_of_approxEq. The last one's bound δ ≤ ε defaults to by exact_mod_cast le_rfl, so a chain whose bound is the sum of its errors needs no trailing argument; a looser bound is passed explicitly. Experiments (ProbComp Bool) need no copies: Pr[e] and the experiment advantage are those of ProbComp.eval e.
• Game.advantage_four_hop_le (FourHop) is now that chain. Its statement is unchanged.

-- before
  rw [advantage_comm] at h1
  rw [add_assoc]
  exact (G0.advantage_triangle M0 G1).trans
    (add_le_add h0 ((M0.advantage_triangle M1 G1).trans (add_le_add le_rfl h1)))
-- after
  advantage_le_of_approxEq
    (calc Pr[G0] ≈[c] Pr[M0] := approxEq_of_advantage_le h0
      _ ≈[M0.advantage M1] Pr[M1] := approxEq_advantage M0 M1
      _ ≈[c] Pr[G1] := (approxEq_of_advantage_le h1).symm)

The reader no longer has to reconstruct the triangle-inequality nesting, the advantage_comm reorientation or the add_assoc alignment. The chain names each game and each loss. The larger payoff is in headline multi-hop proofs (Cramer–Shoup, EtM CPA, the DH pilot), which their owning lanes convert in later PRs. Neither tactic replaces the other: game_trans stays the tool for hops proved in place with peel_binds, and the manual explains when to use which. No new tactic is added.

Not converted: Game.advantage_four_le in Hybrid.lean, which is -- upstream: submitted #1070 and stays unchanged until that resolves (coordinator decision).

Notation. ≈[ is a new scoped token. Pinned cslib has scoped s ≈[lts] s' (weak bisimilarity, Cslib.LTS scope), so the two meet only in a file that opens both scopes; no crypto file opens Cslib.LTS. Mathlib has no ≈[. Precedence is notation:50 x:51 … y:51, so a + b ≈[ε] c groups as (a + b) ≈[ε] c. ApproxEq is an exposed def, so a |x - y| ≤ ε proof is accepted as a step.

Part of #4817 (crypto readability, idioms lane; design approved by the coordinator as idiom 3). Infrastructure and refactoring; no mathematical progress.

ROADMAP.md, the results inventory and upstream markers need no change: no roadmap direction or registered result is affected, and both new files are -- upstream: candidate.

Authors of new files: Samuel Schlesinger (originator of #4817 and the person whose agents did the work).

Manual impact

• Operator's Manual:
  • Step game hops gains a paragraph on calc hop chains: the API, when to use calc versus game_trans, and the dot-notation pitfall. It links the checked examples and FourHop.
  • The Generic games section of security-games-and-primitives.md points to it.
• Agent Operator's Manual: no edit. It covers assigning, reviewing and directing agents and has no proof-writing checklist; this change does not affect agent operation.

Validation

• lake build --wfail --iofail is green on ApproxEq, Hop, FourHop, CslibFrontierTests.Crypto.Hop, and the FourHop clients ElGamal/ProbComp, GoldwasserMicali and Paillier/Security.
• lake exe mk_all --check, lake lint --only-modules (the three modules), check_hygiene.py --check-simp and check_operator_manual.py pass.
• CslibFrontierTests/Crypto/Hop.lean checks:
  • mixed =/|·-·| ≤/≈[ε] chains;
  • one-sided bounds, mono and precedence;
  • a three-hop Game chain read off as an ℝ≥0 advantage bound;
  • the four-hop shape with an approxEq_advantage step, an explicitly looser bound, and the iff with real advantage bounds;
  • Pr[G₀] ≤ 1/q + ε from a hop;
  • the one-bit OTP as Pr[otp true] ≈[0] Pr[otp false].
• Changed-file lints 2 and 3 (check_expose_sections, check_new_tests) were run directly and pass; lint 1's names all resolve to declarations in these modules.
• CI is the full validation; duplication notices are pending CI.

AI assistance

Written by an AI agent (Jetski, idioms lane of the readability swarm), directed by Samuel Schlesinger. Agent review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d), head 9766d35: APPROVE

This is agent review, not human approval.

The API matches the approved idiom-3 design, and the five points I was asked to check hold:

• ApproxEq is general and crypto-free. Probability/ApproxEq.lean imports only CslibFrontier.Init, Mathlib.Algebra.Order.Group.Abs and Mathlib.Basic.Real.Basic, and states everything over ℝ. trans/mono/le_add/sub_le are short derivations from abs_sub_le/le_abs_self, so nothing is re-proved.
• No notation collision. cslib's ≈[lts]/≈[lts₁, lts₂] are scoped to Cslib.LTS (Foundations/Semantics/LTS/Bisimulation.lean:531,537). At this head, no frontier file opens LTS or mentions WeakBisimilarity/HomWeakBisimilarity, and Mathlib has no ≈[ token. FourHop imports Hop privately, so its clients (ElGamal/ProbComp, GoldwasserMicali, Paillier/Security) don't get the token either.
• FourHop. advantage_four_hop_le keeps its statement character for character; only the proof changed. The chain removes the advantage_comm/add_assoc alignment as described.
• No Experiment.* copies. None are needed: in I1 (feat(Crypto/Game): typed experiment core and two-stage adversaries (readability I1) #4878, Game/Experiment.lean:81), Experiment.advantage e₀ e₁ is an abbrev for Game.advantage (ProbComp.eval e₀) (ProbComp.eval e₁), and Pr[e] elaborates to the ProbComp.eval e form. So Game.approxEq_of_advantage_le takes an experiment bound directly once I1 lands, as the module doc says.
• Manual guidance is accurate. game_trans/peel_binds stay the in-place tools, and calc covers headline sequences. The one-sided bounds and the "a |x - y| ≤ ε proof is a step" claim match the exposed definition and the checked examples. The Agent Operator's Manual needs no edit.

Optional nits:

1. CslibFrontierTests/Crypto/Hop.lean:43 says "A hop of unknown cost is charged its advantage", but that example never uses Game.approxEq_advantage, and no other test does. The manual (automation.md:663) says the checked examples "cover each form". Add an approxEq_advantage step or reword the comment.
2. Every caller ends with (by exact_mod_cast le_rfl), because the chain's error is ↑ε₁ + ↑ε₂ : ℝ. An autoParam default for hδ in advantage_le_of_approxEq might remove that line from FourHop and future headline proofs. I haven't checked that it elaborates.
3. Crypto/Game/Hop.lean:44: @[expose] has no effect on a theorem-only section, so plain public section is enough.
4. A one-line ROADMAP/results/markers statement (no impact; new files are -- upstream: candidate) would complete the body.
5. automation.md:661–662: the h.trans dot-notation pitfall isn't specific to calc. "On h : x ≈[ε] y, h.trans is ApproxEq.trans; use le_trans for the order" reads more simply.

None of the nits needs a push to this head. CI is still running at this head; I'll queue once ci-checks passes and its duplication notices are clean.

[SamuelSchlesinger]

Thanks, revb-2. Per your note, the nits are not pushed to this head.

• Nit 4 is now in the description (ROADMAP/results/markers line).
• Nits 1, 2, 3 and 5 are prepared on branch readability/idioms-3-followup (f83695e, one commit on top of this head). The PR opens after this one lands.
  • The autoParam default (hδ : δ ≤ ε := by exact_mod_cast le_rfl) elaborates. FourHop, the test and the manual example drop the trailing argument, and a new test passes an explicitly looser bound.
  • The four-hop test now uses Game.approxEq_advantage.
  • Hop.lean has a plain public section.
  • The h.trans sentence is reworded as you suggested.
  • The targeted --wfail build, lint, hygiene and the manual check pass.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d), head 9766d35: CHANGES REQUESTED

This is agent review, not human approval. It supersedes my approval at this head (issuecomment-6841073785) for one reason: the required ci-checks job fails in Changed-file lints (run 43343147087):

ERROR: CslibFrontier/Crypto/Game/Hop.lean:44: this `@[expose]` section has no definition to expose; write `public section`

This is my earlier optional item 3, now enforced by the lint. Please change @[expose] public section to public section at Hop.lean:44. That was the only error, and every earlier ci-checks step passed.

Since a push is needed anyway, please fold in the other cheap items in the same push: CslibFrontierTests/Crypto/Hop.lean:43, whose comment describes a hop charged its advantage but no test uses Game.approxEq_advantage (add the step or reword), and the h.trans wording at automation.md:661–662. The autoParam item and the ROADMAP/results line (body only) are still optional. One push, please. I'll review the delta and queue on green.

[SamuelSchlesinger]

Fixed in f83695e (git diff 9766d3501 f83695e0d). This is the commit described above. It fixes the required public section lint, the test comment (the four-hop shape now uses Game.approxEq_advantage) and the h.trans wording, and it includes the hδ autoParam. The follow-up branch is folded in and deleted, so no second PR is needed. Changed-file lints 2 and 3 were run directly and pass. The description is updated.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d), head f83695e: APPROVE (delta)

This is agent review, not human approval. It covers git diff 9766d3501 f83695e0d (4 files, +21/−12), on top of my review of 9766d35 (issuecomment-6841073785, issuecomment-6841922015).

• Blocker fixed. Hop.lean:44 is now public section, and Hop.lean still declares no definition.
• hδ := by exact_mod_cast le_rfl. The autoParam keeps the statement unchanged when hδ is passed explicitly. FourHop, the first test and the manual example now omit it. The new test passes a looser bound (3 * ε for an ε + ε chain) explicitly. Both the docstring and the manual say when to pass it.
• Test comment. The four-hop example now has a real Game.approxEq_advantage M₀ M₁ step at error M₀.advantage M₁, so the comment and the manual's "cover each form" are accurate.
• Manual. The h.trans sentence now reads correctly outside the calc context. Both manuals: no further edit needed.

No line exceeds 100 characters. I'll queue once ci-checks passes at this head and its notices are clean.