[SamuelSchlesinger]

Change

This adds one library-wide convention for writing probabilities in statements, plus textbook notation for uniform sampling. SPDZ is the first client.

Statement convention (documented in the Operator's Manual, design approved for #4817):

• A named advantage is ℝ≥0, defined through Experiment.advantage/Experiment.succProbability (I1) or the Game API.
• Every other probability in a public statement is Pr[e] : ℝ: one-sided bounds, exact values, hop differences and biases. Statements stop writing (ProbComp.eval e true).toReal, ℝ≥0∞ masses or Game.succProbability (ProbComp.eval e).
• An exact hop that is a distribution equality stays one.
• ℝ≥0∞ stays inside PMF algebra.

$ᵗ α (in Notation.lean, scoped with Pr[·]) is notation for exactly ProbComp.uniform α, following VCVio. It adds no constant (#guard_expr … =ₛ ProbComp.uniform …), so eval_uniform, pmf_norm and every other lemma apply unchanged. Goals print ProbComp.uniform α as $ᵗ α, including inside do blocks.

SPDZ (representative client):

-- before
theorem toReal_eval_macCheckSoundnessGame_le … :
    ((ProbComp.eval (macCheckSoundnessGame p T err deltaShift)) true).toReal ≤ 2 / (p : ℝ)
theorem succProbability_macCheckSoundnessGame_le … :   -- the same fact in a third spelling
    (Game.succProbability (ProbComp.eval (macCheckSoundnessGame p T err deltaShift)) : ℝ) ≤
      2 / (p : ℝ)
-- after
theorem probability_macCheckSoundnessGame_le … :
    Pr[macCheckSoundnessGame p T err deltaShift] ≤ 2 / p

• toReal_eval_linearCombZeroGame_le → probability_linearCombZeroGame_le : Pr[…] ≤ 1 / p.
• The duplicate succProbability_macCheckSoundnessGame_le is deleted.
• The three game bodies sample with let α ← $ᵗ ZMod p.
• The eval_*_le ℝ≥0∞ forms stay, because the adaptive-adversary proof consumes them inside PMF algebra.
• The test states its conjunct with Pr[·].

There is no library sweep. Lanes adopt Pr/$ᵗ in PRs cut after this one lands, and a tooling ratchet then stops new old-style statements.

Depends on I1 #4878, which has landed. The manual names I1's Experiment.coe_advantage/coe_succProbability. The PR is retargeted to main and merges main at fc1080c. The only conflict was the security-games experiment paragraph: it takes main's text and re-appends this PR's sentence.

Part of #4817 (crypto readability, idioms lane; idioms 1 and 2 of the approved design, folded together per the coordinator). Infrastructure, documentation and a client refactor; no mathematical progress.

Manual impact

• Operator's Manual:
  • new section State a probability and sample uniformly, with the convention, $ᵗ, and links to SPDZ and the checked examples;
  • a sentence in the experiment paragraph of security-games-and-primitives.md;
  • the SPDZ paragraph of protocols-and-privacy.md names the renamed lemma.
• Agent Operator's Manual: no edit. It covers assigning, reviewing and directing agents and has no statement-writing checklist; this change does not affect agent operation.

Validation

• lake build --wfail --iofail is green on Notation, CslibFrontierTests.ProbabilityNotation, SPDZ, CslibFrontierTests.Crypto.SPDZ, Experiment and CslibFrontierTests.Crypto.Experiment.
• lake exe mk_all --check, lake lint --only-modules (Notation, SPDZ), check_hygiene.py --check-simp and check_operator_manual.py pass.
• ProbabilityNotation.lean gains $ᵗ checks:
  • #guard_expr syntactic identity;
  • #guard_msgs printing ($ᵗ Fin 3, a do block, <$>, a parenthesized product);
  • f $ x still parses;
  • rw [eval_uniform] and plain simp work on a $ᵗ block.
• Notation.lean has about 145 transitive importers; CI rebuilds them and 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-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 7c007b0: APPROVE

Checked against the agreed design (Pr convention rules 1–4 and the scoped $ᵗ sampling notation):

• $ᵗ is scoped notation:max "$ᵗ " α:lead => Cslib.ProbComp.uniform α in Cslib.Probability, so it shares the Pr scope and introduces no constant. The tests cover #guard_expr against ProbComp.uniform, printing inside do, next to <$> and on products, parsing next to $ application, and eval_uniform/simp seeing through it.
• SPDZ: probability_linearCombZeroGame_le (≤ 1 / p) and probability_macCheckSoundnessGame_le (≤ 2 / p) keep their proofs and elaborate to the former .toReal statements. All four sampling games now read let alpha ← $ᵗ ZMod p / let e ← $ᵗ (Fin T → ZMod p). Nothing still refers to the removed succProbability_macCheckSoundnessGame_le or the old toReal_eval_* names.
• Manuals: the convention text matches rules 1–4, including the distribution-equality exception. The Experiment.coe_succProbability/coe_advantage it cites exist on the base. The PR body records the AOM assessment.

Optional nit, not blocking: the test file opens Cslib Probability at the top, so nothing checks that ProbComp.uniform (Fin 3) prints as itself outside the scope, even though the module doc promises it. A short section before the open with /-- info: ProbComp.uniform (Fin 3) : ProbComp (Fin 3) -/ #guard_msgs in #check ProbComp.uniform (Fin 3) would pin that down.

Not queued: this targets readability/infra-i1-experiment. I will queue once #4878 lands, this PR is retargeted to main, and CI passes on the resulting head.

This is agent review, not human approval.

[SamuelSchlesinger]

Added the negative scope test in caf8441. In a namespace that opens only Cslib, #check ProbComp.uniform (Fin 3) prints ProbComp.uniform (Fin 3). Test-only delta: git diff 7c007b08a caf844136.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head caf8441: APPROVE (delta 7c007b0..caf8441). The delta is test-only and adds the negative scope test. The open Cslib Probability at line 13 is scoped to namespace CslibFrontierTests.ProbabilityNotation, and the new Unscoped namespace opens only Cslib. So the #guard_msgs really checks that ProbComp.uniform (Fin 3) prints as itself outside the scope. Still not queued: it waits for #4878 to land and the retarget to main.

This is agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head fc1080c: APPROVE (main merge after #4878)

git show --remerge-diff shows one hand-resolved hunk, in the security-games experiment paragraph. Against origin/main, the merged manual differs only by this PR's own Pr[e]/$ᵗ sentence, the same text as at caf8441. The PR diff against main is still the 7 files, +122/−34, that I approved, and the Lean sources match caf8441. There are 0 unresolved threads. I'll queue once ci-checks and guide are green on this head.

This is agent review, not human approval.

[SamuelSchlesinger]

Rendered-manual check (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head fc1080c. This adds to my approval and leaves the queued head unchanged.

Rendered: inspected pp. 55–56, 425 and 484 of cslib-frontier-operators-manual.pdf from run 43375960011: OK.

• pp. 55–56 hold the new section 6.27, "State a probability and sample uniformly". Its bullets, the $ᵗ paragraph and the probability_macCheckSoundnessGame_le example render as prose and code with no raw markdown. Long identifiers wrap inside the text block, as elsewhere in the manual, and no line passes the right margin (text ends at x ≤ 543 of 612 pt). Notation.lean, SPDZ.lean and "checked examples" link to the files at this head. The section is in the table of contents (p. 3).
• p. 425: the new Experiment sentence renders, and its "State a probability and sample uniformly" cross-reference goes to p. 55.
• p. 484: the SPDZ list shows probability_macCheckSoundnessGame_le (Pr[macCheckSoundnessGame p T err deltaShift] ≤ 2 / p) inline, with no overflow.

I checked the pages through poppler text, word boxes and link extraction (pdftotext -layout/-bbox-layout, pdftohtml -xml), not by eye.

Agent Operator's Manual: no edit needed. It is built from manual/AGENT_OPERATORS.md, which this PR doesn't touch, and the change is about statement notation, not agent workflow.