[SamuelSchlesinger]

Change

Step 3 of #814, part 2 of 2, stacked on #2201 (review and merge that first; this PR's diff is against its branch). This finishes the migration of the Crypto clients and deletes the last specialized copies of the generic OracleComp semantics:

• ProbOracleComp.handler, the transitional abbreviation left by part 1, is deleted. Its 227 remaining Crypto uses become OracleComp.sumHandler.
• ProbOracleComp.eq_of_mem_support_pure and ProbOracleComp.mem_support_map are deleted. Their clients use the generic OracleComp.eq_of_mem_supportWith_pure and OracleComp.mem_supportWith_map_iff.

The change is a mechanical rename across 21 Crypto modules (Signature, MerkleSignature, IndexedSignature, MAC, EncryptThenMAC, the PRF and GGM families, Cramer–Shoup, GMW, UntilBad, OneWay/MCSP), with the three proof adjustments below. Statement meaning is unchanged, because OracleComp.sumHandler is defined by the same two cases as the deleted handler.

After this PR, ProbOracleComp has no semantics of its own. Its handlers are OracleComp.sumHandler, its run and acceptance probability are instances of OracleComp.runWith, and its support is OracleComp.support.

Validation

Hosted CI runs the six gates. Locally, lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts and lake exe lint-style pass on top of part 1, as do check_hygiene.py --check-simp, check_tidy_surface.py and check_changed_files.py --base origin/main.

Elaboration time of the hot modules this PR touches. I timed lake env lean (wall / user seconds) with LEAN_NUM_THREADS=4 on a shared machine at load 15–25, so differences within about ±10% are noise:

Module	main	this PR	user time
Computational.MAC	20.5 / 35.0	20.1 / 34.9	0%
Encryption.EncryptThenMAC	10.1 / 45.9	10.5 / 47.2	+3%
IndexedSignature.Counter (3 runs)	19.6 / 23.5	20.0 / 24.2	+3%
Computational.Signature	8.5 / 10.6	8.7 / 10.9	+3%
Computational.CramerShoup (1 run)	9.1 / 21.4	9.1 / 21.3	0%
MerkleSignature.Security (1 run)	5.6 / 10.2	5.7 / 10.3	+1%
PseudorandomFunction.Coins	4.6 / 4.7	4.6 / 4.6	−1%

Unless marked, each figure is the mean of two interleaved runs in a checkout of main and of this branch. Part 1's table covers CarterWegman, Authenticated, CCA and the Naor–Reingold modules, which are unchanged here.

Three proofs needed more than the rename, and their statements are unchanged:

• Game/UntilBad: rw [OracleComp.sumHandler] left an unassigned instance at one site, so that site uses OracleComp.sumHandler_inr.
• MerkleSignature/Security and two sites in EncryptThenMAC: rw [ProbOracleComp.support_sample] failed after mem_supportWith_map_iff, which states membership in supportWith (fun _ => Set.univ) rather than the reducible support. Those sites use simp only instead.

AI assistance

Claude Code (Opus), as worker-claude-015dlg8k-oraclesem for coordinator-claude-015dlg8k.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author review of a9abceab3e53e0dca12310e08f6cce352a0c1323, covering the complete own layer over #2201's c419ef98f8ab9f99fc4556cf985eb8e1a008c8bc and reusing that layer's semantic review.

This layer completes the migration: the handler abbreviation and two specialized support wrappers are deleted, with no retired qualified names remaining in maintained Lean clients, tests, abstracts or guide. Eighteen files are exact generic-name substitutions; I inspected the remaining deletions and all proof adjustments. The support-map substitutions retain the same witnesses, the sample-support simplifications preserve the signature/tag length arguments, and sumHandler_inr preserves the finder oracle's reply and state update. Games, security assumptions, encodings, independent resource bounds and abstract statements are unchanged.

The combined revision is alias-free. The migration-completeness request on #2201's current head remains open: integrate this complete migration as one change rather than landing its transitional parent alone.

Hygiene/simp, whitespace, canonical aggregate, import-cycle and retired-name checks pass. The author reports strict library/test/abstract builds. At my single CI inspection, title passed and library CI and Guide were running. No reviewer Lean build or timing rerun. Agent review, not human approval; required final validation remains before integration.

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): this is a Claude-fleet PR, stacked on #2201. It migrates the remaining 21 Crypto modules and deletes the transitional facade, with statements unchanged. Please review at a9abceab3e53e0dca12310e08f6cce352a0c1323, after #2201: reviewer-codex-edemaine (@edemaine) or the Codex reviewers above.