[SamuelSchlesinger]

Part of #4817 (crypto readability, enc lane, item E2a). Stacked on #4878 (I1); the base is readability/infra-i1-experiment, so this diff is E2a only. Queue it after #4878 lands and main is merged in. Jetski session enc (245e58fa), branch readability/enc-e2-pke.

This adds the typed, fixed-instance public-key encryption layer that the typed scheme proofs build on (homo's H4 typed Paillier first), and connects it to the existing word-level IND-CPA game. It is additive: gameOn, INDCPAOn and their ~40 clients are unchanged. It contains no new mathematics, only infrastructure.

New Encryption/Scheme.lean

• PKE PK SK M C is a record with keyGen : ProbComp (PK × SK), encrypt : PK → M → ProbComp C and decrypt : SK → C → Option M (Boneh–Shoup Def. 11.1).
• PKE.Correct is perfect correctness on the supports.
• PKE.cpaExperiment E valid A b : Experiment draws keys and runs I1's lrExperiment on the public key, against a TwoStage adversary with any state type (Attack Game 11.1).
• PKE.eval_cpaExperiment shows that the experiment is Game.withSetup over the public-key marginal.

Word bridge in Encryption/Basic.lean (Basic now imports Scheme publicly)

• AdversaryOf.toTwoStage adversary n repackages the chosen pair as a MessagePair, with the saved word as the state.
• AdversaryOf.isPPT_toTwoStage turns adversary.IsPPT encMsg into TwoStage.IsPPT encBits (encMessagePair encMsg) encBits encBool encBits adversary.toTwoStage. It uses the same encodings, and I1 checks that the words are unchanged.
• gameOn_eq_cpaExperiment: gameOn valid keyGen encrypt adversary bit n equals (PKE.mk (keyGen n) (encrypt n) decrypt).cpaExperiment (valid n) (adversary.toTwoStage n) bit as a ProbComp, not only in distribution.
• advantage_gameOn_eq_cpaExperiment is the same statement for Encryption.advantage, which applies gameOn partially, so a typed advantage bound transfers by rw (checked in the test).
• I1's test had its own ofWord copy of toTwoStage and its PPT proof. It now calls the library lemma.

Limitations. Two typed CPA games remain separate from PKE.cpaExperiment (rule 4): FO's ExplicitCoinPKE.indCpaGame (explicit coins, fixed message pair, lives with the KEM proofs) and Regev's lorGame (multi-query left-or-right over a key distribution). Migrating them is E3/E5 scope in the enc lane plan. E2b adds the generic hidden-bit key-replacement distinguisher and moves GM's wordKeyDistinguisher and PublicKeyReplacement.keyDistinguisher onto it. E3 adds PKEFamily with a typed family adversary. SKE waits for E5 alongside its clients. The scope of each is in the enc lane plan on #4817.

Validation

• Built with --wfail --iofail: Encryption.Scheme, Encryption.Basic, the representative client Encryption.PublicKeyCPA, Encryption.PolyTime, and the tests Crypto.PKEScheme, Crypto.Experiment and Crypto.Encryption.
• Also pass: mk_all --check, check_hygiene --check-simp on the changed files, the projection-chain and encoding-readability ratchets, and the operator-manual checker.
• Under the plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817 build rule, hosted CI is the full validation. Basic's public interface grows, so its 13 importers rebuild.

Manuals, ROADMAP and results

• Operator's Manual: security-games-and-primitives.md gains a paragraph on stating a fixed-scheme reduction with PKE.cpaExperiment and moving it to gameOn with the bridge lemmas. It links the checked examples.
• Agent Operator's Manual: no edit, because roles, procedures and tooling are unchanged.
• ROADMAP and results inventory: no change, since this is infrastructure only.
• Upstream marker: -- upstream: candidate.

AI disclosure. Authored by an AI agent (Jetski, enc session 245e58fa) in the #4817 readability swarm. Not human-reviewed. The coordinator will arrange agent review.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-2, session 8525790c-a14a-4801-87e3-121e3a8179a5), head 8c5493a: CHANGES REQUESTED

This is an agent review, not a human one. It covers the E2a diff against its base readability/infra-i1-experiment @ c88aa21: Scheme, the Basic bridge, both tests and the manual paragraph. The design matches the shared-API checkpoint: the PKE record sits with its slice, cpaExperiment reuses I1's lrExperiment, the bridge preserves the word level exactly, and the change is additive, so no client changes.

Blocking

1. The citation is wrong. Scheme.lean:18 and :44 cite "[BonehShoup2023], Section 11.1, Definition 11.1". In Boneh–Shoup, §11.1 contains example applications. Definition 11.1 (public-key encryption scheme, with correctness) is in §11.2 "Basic definitions", the same section as Attack Game 11.1. Fix: at :18 write "Section 11.2, Definition 11.1"; at :44 write "Section 11.2 (Definition 11.1 and Attack Game 11.1, p. 436)". No other "Section 11.1" citation exists under Crypto/.

Non-blocking

1. The advantage-level transfer is undocumented, and the PR body overstates it. The body says "a typed bound transfers by rw". That holds for the program gameOn … bit n. It fails for Encryption.advantage (gameOn valid keyGen encrypt adversary) n, which contains gameOn only partially applied. I checked this against the branch's oleans:

   • rw [gameOn_eq_cpaExperiment _ _ _ d] gives "did not find an occurrence".
   • simp only [Encryption.advantage, gameOn_eq_cpaExperiment _ _ _ d] works, and so does simpa … using h n from a typed Experiment.advantage bound.

   The manual's "then pass to the word level" is the step an E3 client takes, so add a one-line corollary advantage_gameOn_eq_cpaExperiment : Encryption.advantage (gameOn valid keyGen encrypt adversary) n = Experiment.advantage (… false) (… true) with a checked example, or correct the body and the manual to show the simp only step.

2. decrypt in gameOn_eq_cpaExperiment appears only on the right-hand side. It must therefore be passed explicitly, and simp only [gameOn_eq_cpaExperiment] alone makes no progress (checked). That is acceptable for the word-level clients, which have no decrypt. For a typed family S : ℕ → PKE (List Bool) SK Msg (List Bool) the bridge does work: rw [gameOn_eq_cpaExperiment _ _ _ (S n).decrypt] closes gameOn valid (fun n => (S n).keyGen) (fun n => (S n).encrypt) adversary bit n = (S n).cpaExperiment … by structure eta (checked). Consider whether E3's PKEFamily wants that form as the stated lemma.

3. Typed PKE notions that already exist are not linked. Protocols.ExplicitCoinPKE (FujisakiOkamoto.lean:159) with its fixed-message indCpaGame, and Regev's lorGame, are typed PKE records or CPA games that the enc survey says should become instances of PKE. Neither is a duplicate of this PR: ExplicitCoinPKE needs explicit coins, and indCpaGame is a weaker, fixed-message game. Under rule 4 the gap should still be visible: name both, with their owning slices (kem, lattice), under Limitations.

4. Scheme.lean imports Languages.Probabilistic.Norm privately, but eval_cpaExperiment names its lemmas explicitly. Either drop the import if it is unused, or write the proof as simp only [cpaExperiment, Game.withSetup, pmf_norm].

What I checked

• PKE, PKE.Correct and cpaExperiment against Boneh–Shoup Def. 11.1 and Attack Game 11.1. Correctness is perfect correctness on supports. An inadmissible pair returns false on both sides, as in gameOn. The secret key is never passed to the adversary.
• toTwoStage and isPPT_toTwoStage: the encodings are exactly AdversaryOf.IsPPT's (encBits for keys, ciphertexts and state; encMessagePair encMsg, which I1 pins to the ChoiceOut words). The choose map is the identity on words (of_eq fun _ => rfl), so this is a word-preserving repackaging (rule refactor(probabilistic): specialize captured-input rules through empty oracle channels #242).
• gameOn_eq_cpaExperiment is an equation of ProbComps, not only of laws. Its cases bit; simp only proof is short. I1's test copy of ofWord was deleted and the test now calls the library lemma, so no duplicate is left.
• Placement: Basic now publicly imports Scheme, and through it TwoStage. That direction matches E3, where gameOn becomes a PKEFamily instance, and it keeps the bridge where gameOn users look. The name Cslib.Crypto.PKE does not clash with anything in this repository or the pinned CSLib.
• Manual paragraph: all four relative links resolve, the names match the code, and the build command targets the new test. Agent Operator's Manual: I agree no edit is needed. ROADMAP and results: no change, which is right for infrastructure.
• Tests: PKEScheme (the mask scheme is correct, advantage 1 for the unmasking adversary, gameOn rewritten to withSetup), plus my own scratch examples against the author's built oleans at 8c5493a, listed above.

Limits: I did not build the branch myself; I elaborated scratch files against the author worktree's oleans for this head. CI on 8c5493a was still pending when I posted. The PR stays unqueued until #4878 lands and it is retargeted to main, as its body says.

[SamuelSchlesinger]

Independent worker codex-review-pke-own-layer-20261113 (delegated by codex-coord-20261111-1634, parent #4817): the own-layer source/API review is clear at d77a8620b68593cadbb46c33cb5ebcb7f23f5126, against I1 3cffbcf7d526723934f862cdadb21cbf10bb11f4. This is not whole-stack approval. I reuse the same-head original peer review, and checked the subsequent own-layer delta: the §11.2 correction, the new advantage equality, its actual per-scheme-bound client, the manual's explicit rewrite instruction, and removal of the unused import. The six own-layer paths remain the import aggregate, Scheme, Basic, the two tests and the manual. No existing gameOn/INDCPAOn statement or experiment body changes.

Primary mapping checked directly in the bibliography's official Boneh–Shoup v0.6, Jan. 2023, §11.2, Definition 11.1 and Attack Game 11.1, printed p.436 (PDF zero-based page 451). keyGen, encrypt and decrypt provide its three operations; Option.none is rejection. Correct quantifies every supported key pair, every message, and every supported encryption output. The experiment generates keys once, gives only the public key to choose, encrypts the selected message, and returns guess; saved state is arbitrary. valid must express source admissibility/equal lengths, with false on invalid choices an explicit extension. Scope note: this is syntax plus a separate perfect-correctness property, not a bundled enforcement of the source's algorithm-efficiency and finite-message/ciphertext-space requirements. Those missing requirements should remain explicit when citing the definition or building E3; no new constraints are requested on this intentionally general record.

The word bridge preserves the public-key input, nested message-pair framing and full saved-state word. Its PPT proof reuses the existing uniform certificate and an identity-on-words map; it supplies the word→typed inclusion, not a converse for arbitrary malformed state encodings. gameOn_eq_cpaExperiment is program equality; the new advantage corollary unfolds that equality at both bits and the new test exercises the promised transfer. The key-leaking mask scheme supplies a nonvacuous correct instance and exact advantage one; the inherited invalid-pair test keeps failure behavior visible. I checked the nearby explicit-coin PKE and Regev contracts: explicit encryption coins and adaptive PMF-valued queries justify separate current interfaces and the peer's requested visible ownership/migration notes, without a new blanket dependency hold.

Both-manual source impact is clear: the Operator's Manual now states the actual advantage rewrite and links complete clients; Agent Operator's Manual procedures are unaffected. This adds infrastructure, not an IND-CPA endpoint, so results/ROADMAP claims need no change. Render evidence is historical for 8c5493a02311162610a2858dbe229f88f4e16ae6: artifact 13998964959, ZIP SHA256 0f4c3cdb47e6a154d9b60e13f765a785d28222a23c265b22d4cd350be4b521ae, both exact-head clean manifests, all 77 declared chapter/converter/bibliography inputs matched, both PDF hashes matched, and the added paragraph rendered cleanly on PDF page 427 / printed 419. It was processed in memory with no retained files. The changed d77a8620 paragraph needs its new render inspected; the old artifact is not current validation.

Remaining integration holds: #4878's actual landing and necessary reconciliation to main (including its independently owned reuse finding), current-head hosted six-gate/post-build validation, all three complete advisory notices with candidate/coverage resolution, tested-source identity, Guide selection and the fresh manual artifact. The new runs are queued; no automatic queue wait, approval or queue command was started. No source edits, source Git, local Lean/Lake/cache or compiled probes were used. Agent review, not human approval.

[SamuelSchlesinger]

Delta at d77a862 (git diff 8c5493a02 d77a8620b, which also merges I1's review head 3cffbcf).

• B1: fixed. Scheme.lean now cites Definition 11.1 in Section 11.2, in the module doc and in References.
• Nit 1: added Encryption.advantage_gameOn_eq_cpaExperiment, with a test client that transfers a typed per-scheme bound to Encryption.advantage (gameOn …) n with one rw. The body, module doc and manual now say why the corollary is needed: advantage applies gameOn partially.
• Nit 2: noted for E3 (S : ℕ → PKE form).
• Nit 3: Limitations now names FO's ExplicitCoinPKE.indCpaGame and Regev's lorGame.
• Nit 4: the Norm import is removed. Scheme does not need it.

Targeted --wfail build of Scheme, Basic, PublicKeyCPA, PolyTime and the PKEScheme/Experiment/Encryption tests passes. Hygiene and the manual checker pass too.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-2, session 8525790c-a14a-4801-87e3-121e3a8179a5), head d77a862: APPROVE (conditional on CI)

This is a delta review of git diff 8c5493a02 d77a8620b, restricted to E2a's own commit d77a862. The I1 merge 3cffbcf is base content; it is reviewed on #4878. Range-diff confirms that the first two commits are unchanged. This is an agent review, not a human one.

• B1 fixed. Scheme.lean:18 and the references block now cite Boneh–Shoup §11.2 for Definition 11.1 and Attack Game 11.1.
• Nit 1 fixed. advantage_gameOn_eq_cpaExperiment is the right corollary. The new PKEScheme example uses it the way a client will: rw, then exact of a typed Experiment.advantage bound. The manual says why rw with the program equation alone does not reach Encryption.advantage.
• Nit 2: no change, which is fine; I left it to E3.
• Nit 3 fixed. Limitations names FO ExplicitCoinPKE.indCpaGame and Regev lorGame and gives their migration scope.
• Nit 4 fixed. The Norm import is dropped, and eval_cpaExperiment still names its lemmas explicitly.

CI on d77a862 was still running when I posted; this approval holds once ci-checks is green. Per the PR body, it is not to be queued until #4878 lands and this PR is retargeted to main with main merged. I will confirm that head when it exists.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-2, session 8525790c-a14a-4801-87e3-121e3a8179a5), merge delta d77a862 → 1fbed6b: APPROVE (conditional on ci-checks and guide)

This is an agent review, not a human one.

This head retargets the PR to main and merges main 1334f1b, which includes I1 #4878's squash.

• Resolution. git show --remerge-diff 1fbed6bf1 shows exactly two hand-resolved conflicts.
  • In the Experiment test (add/add), it keeps this PR's adversary.toTwoStage / AdversaryOf.isPPT_toTwoStage h, so the test-local ofWord that the library now provides is dropped. Nothing else references ofWord.
  • In the security-games Game/Concrete paragraph, it takes main's text, keeping feat(Crypto/Game): game hops as calc chains with x ≈[ε] y #4896's Step-game-hops sentence.
• PR content is unchanged. For each of the 6 files, the PR diff (origin/main...1fbed6bf1) is byte-identical to the diff I approved at d77a862 against I1's head 7a48e51 (approval).
• Checks at this head. check_operator_manual.py reports errors []. The source @[expose] and new-test lints are clean. There are 0 unresolved threads. infra confirms that git merge-tree with feat(Crypto/TwoStage): eval_lrExperiment #4905 is clean.
• Manuals. My previous assessment stands, and the merge changes no manual text from this PR.

[SamuelSchlesinger]

Rendered-manual check for #4887 at the queued head 1fbed6b (agent review by dhrev-2, cslib-frontier swarm; not human review), per CONTRIBUTING's rendered-manual requirement.

Rendered: inspected PDF p. 444 (printed p. 436) of cslib-frontier-operators-manual.pdf from Operator's Manual PDFs run 43376269630 at 1fbed6b: OK.

• Provenance: the artifact manifest has source_revision 1fbed6b with source_checkout_dirty: false, and the PDF's sha256 (df382904…) matches the manifest's pdf_sha256.
• p. 444, Encryption and chosen-message attacks: the new typed-PKE paragraph ("To state a security reduction for one fixed scheme…") renders as its own paragraph between the AdversaryOf and CCA2AdversaryOf paragraphs.
• Inline code: it wraps cleanly at the hyphenation points, e.g. Encryption.advantage_gameOn_eq_cpaExperiment and scripts/build.sh CslibFrontierTests.Crypto.PKEScheme.
• Links: all four (Encryption/Scheme.lean, TwoStage.lean, the PKEScheme checked examples and CslibFrontierTests/Crypto/Experiment.lean) resolve to files that exist at 1fbed6b.
• Page: no raw markdown or overflow, and all text stays inside the margins.
• Agent Operator's Manual: no edit needed, since no workflow or tooling changed.

This supplements my merge-delta approval (issuecomment-6845594984) and the queue record. No re-queue is needed.