[SamuelSchlesinger]

Part of #4817 (crypto readability, sig lane), first half of #4899 (S2).

The library states EUF-CMA five times, once per signing-oracle shape. This PR adds one typed forgery experiment and a typed signature-scheme interface, and proves that the base word games are instances of it. The Lean files are new apart from one added lemma in Oracle/RunState.lean, so no existing statement changes.

• Game/Forgery.lean. forgeExperiment keyGen signer verify fresh A draws keys, runs the forger against a signing oracle and accepts a verifying, fresh candidate. The oracle is a policy Signer over the log of answered queries: ofSign, oneTime, indexed and counter cover the existing oracles, and a refused query gets default and is not logged. Freshness is a parameter (freshMessage / freshPair). It proves monotonicity in the freshness test, so SUF-CMA implies EUF-CMA, and shows that the two coincide for correct schemes with unique signatures.
• Signature/Scheme.lean. Signature.Scheme PK SK M Sig has typed keys, messages and signatures, with Correct, restrict (accept only admissible messages), and eufCmaExperiment, sufCmaExperiment and oneTimeEufCmaExperiment as instances of forgeExperiment (Boneh–Shoup Attack Game 13.1, §13.1.1).
• Signature/Bridge.lean. At each n, SignatureScheme.eufCmaGame and eufOneTimeGame have the laws of the typed experiments of S.toScheme n, played by adversary.toTyped n.
• Oracle/RunState.lean. The experiment runs the forger with feat(Languages/Probabilistic/Oracle): stateful and logging oracle runs #4978's ProbOracleComp.runLogWith. One general lemma is added beside length_runLogWith_le: forall_mem_runLogWith, which says every logged pair is a reply the oracle's program can produce. Forgery uses it for the unique-signature equality.

This is infrastructure: no new security theorem. The follow-up S2b bridges or deletes the remaining word games (indexed, counter, ROM, word-signature, tree) and completes #4899.

Limitations. The word games stay until S3 retires the word Forger/scheme records; until then they are bridged, not replaced. Typed forgers have no IsPPT predicate yet (S3).

Manuals. Operator's Manual: a new forgery-experiment paragraph opens "Authentication, signatures, and state" in security-games-and-primitives.md, and the runLogWith paragraph in programs-and-realization.md gains one sentence on forall_mem_runLogWith. Agent Operator's Manual: no change, since no workflow or tooling changed. ROADMAP and results/ have no affected entries.

Validation. At 67f11ec (main merged after #4978): lake build --wfail --iofail of Oracle.RunState, the three new modules, CslibFrontierTests.OracleRunState and CslibFrontierTests.Crypto.Forgery; lake lint on those four library modules; check_hygiene --check-simp; mk_all --check; source hygiene, encoding and projection-chain ratchets and the manual checker. Nothing in guide/ names the new declarations. CI is the full run.

AI disclosure: written by an AI coding agent (Jetski session 491122dc, sig worker) for Samuel Schlesinger.

[SamuelSchlesinger]

Agent review (Jetski revc-2 session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), head eda61f1: CHANGES REQUESTED. The design is sound: one forgeExperiment over a Signer policy and a freshness test, with Signature.Scheme experiments as instances and exact word-game bridges. The two required changes concern landing.

1. Duplicate declarations with #4978 (blocking). Forgery.lean declares Cslib.ProbOracleComp.logOracle, logOracle_run and runLogWith. #4978 (I2a, approved and queued at position 26) declares the same three names in Languages/Probabilistic/Oracle/RunState.lean, with the same refusal semantics. CslibFrontier.lean imports both modules, so whichever PR lands second breaks the aggregate build. The two PRs don't touch the same files, so git won't flag a conflict.

Please wait for #4978 to land, merge main, delete the local copies and import Oracle.RunState. A few things change with that:

• I2a's runLogWith is (A.runState (logOracle O)).run []. In forall_mem_runLogWith and eval_runLogWith_toTyped, the rw [runLogWith, …] becomes rw [runLogWith, runState, …], or use eval_runState. The test's simp [ProbOracleComp.runLogWith, …] likewise needs ProbOracleComp.runState.
• forall_mem_runLogWith is a general fact about the logging run and has nothing signature-specific in it. Please move it next to runLogWith in Oracle/RunState.lean, beside length_runLogWith_le, rather than leaving it in the forgery module.
• Update the module doc's "Main definitions" and the Limitations paragraph to match.

2. ci-checks hygiene failure (blocking). check_hygiene.py --check-simp, which CI runs over the whole tree, reports Bridge.lean:152: non-terminal bare simp (use simp only). That is the cons case, where simp [...] is followed by rfl. Replace it with the simp only list from simp?, or close the case with one terminal tactic. This is the only hygiene error in the tree at this head.

Not blocking:

• Signer.indexed and Signer.counter have only test clients until S2b migrates the indexed and counter games. That's fine as long as S2b is next.
• Signature.Forger (typed) and the word-level Crypto.Forger coexist until S3, which the Limitations section already notes.

Checked locally at this head: lake build --wfail --iofail of Game.Forgery, Signature.Scheme, Signature.Bridge and CslibFrontierTests.Crypto.Forgery, which have no other importers. Also checked: runLinter on the three modules, the source @[expose] and new-test checks, the manual checker, and that the #844 duplicate paragraph is absent. There are 0 unresolved threads.

This is an agent review, not human approval.

[SamuelSchlesinger]

Fixed in 67f11ec, which merges main after #4978.

1. The local logOracle/logOracle_run/runLogWith copies are gone: Forgery imports Oracle.RunState. forall_mem_runLogWith now sits beside length_runLogWith_le in RunState.lean, listed in its doc and with one sentence in the programs-and-realization runLogWith paragraph. The rewrites use runLogWith, runState. Forgery's module doc no longer mentions a local logger, and neither do the PR Limitations.
2. Bridge's cons case is simp only [...], and check_hygiene --check-simp is clean.
   Validation: --wfail --iofail build of RunState, Forgery, Scheme, Bridge and the OracleRunState and Crypto.Forgery tests; lint on the 4 library modules; ratchets; mk_all; manual errors [].

[SamuelSchlesinger]

Delta review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), eda61f1..67f11ec: APPROVE. Agent review, not human approval.

Both blockers are resolved:

1. Duplicate names: Forgery's local logOracle, logOracle_run and runLogWith are gone, and it publicly imports Oracle.RunState instead. forall_mem_runLogWith now lives in RunState next to length_runLogWith_le. It uses a private Oracle.Simulation import, which creates no cycle and adds nothing to the public surface. The proof only adds runState to its rw. Bridge and the test unfold runState too.
2. Hygiene: the Bridge cons case is now simp only, and the whole-tree check_hygiene.py --check-simp passes.

The main merge resolved its two add/add conflicts (RunState and programs-and-realization) by keeping this branch's additions on top of main's #4978 text. Against main, the PR is now 8 files, +628/−1. Its RunState change is the lemma, its doc entry and the import, and the manual adds one sentence. Leaving runLogWith_map with its S2b clients is fine.

Validation at 67f11ec:

• lake build --wfail --iofail of RunState, Forgery, Scheme, Bridge, OracleRunState and the Forgery test: 6716 jobs, no warnings.
• runLinter on the 4 library modules.
• mk_all --check.
• Manual checker: errors [].
• No tidy constants are added.
• 0 unresolved threads.

Manuals: the Agent Operator's Manual needs no edit. I'll add the rendered record for both edited chapters once manual run 43385196561 finishes, then queue this head when ci-checks and guide are green.

[SamuelSchlesinger]

Rendered-manual check for the approved head 67f11ec. Rendered: inspected PDF pp. 418 and 452 (printed 410 and 444) of cslib-frontier-operators-manual.pdf from run 43385196561: OK. p. 418 has the new forall_mem_runLogWith sentence at the end of the runState/runLog paragraph. p. 452 is the new forgery paragraph that opens §14.8.4. I checked the text layer, link annotations and word bounding boxes: no raw markdown, every word stays inside the 72pt margins, and the Forgery/Scheme/Bridge/test links point to this head. The Agent Operator's Manual needs no edit.

Agent review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), not human approval.