[SamuelSchlesinger]

Part of #4817 (crypto readability, proofs lane P5a).

Kilian's efficiency statements and cheating-prover interface took anonymous tuples read by position: fun p : (List Bool × α × List Bool) × … => kilianVerify H V p.1.1 p.1.2.1 p.1.2.2 p.2.1 p.2.2, prover output ((x, root), state) with helpers reading s.2.1.1. They now use records with named fields, each encoded by enc_structure with an explicit enc parameter:

• KilianClaim (key, stmt, root) and KilianView (extends the claim; challenges, response) are the input of computableInPolyTime_kilianVerify and length_kilianVerifierInput_honest_le, which now read kilianVerify H V v.key v.stmt v.root v.challenges v.response.
• KilianProverInput (key, stmt, table) is the input of computableInPolyTime_kilianCommit and computableInPolyTime_kilianRespond.
• KilianMessage (stmt, root) and KilianCommitment (extends it; state) are the output of KilianProver.commit. The soundness game, binding adversary, private rewinding helpers and the hM table-size hypothesis of succProbability_kilianSoundnessGame_le(_collision) read c.stmt, c.root, c.state.

encKilianInput is removed; its two clients (Kilian.lean, Succinct.lean) are migrated. Encoded words unchanged: nesting KilianClaim in KilianView and KilianMessage in KilianCommitment reproduces the former left-grouped layouts, checked by rfl tests in CslibFrontierTests/Crypto/Kilian.lean and KilianSoundness.lean. Bounds and theorem content are unchanged; hM quantifies over the commitment instead of its three components. The verify/commit/respond proofs drop their hand-built fst/snd chains (about 30 lines) in favour of the generated field rules.

Representative caller: isPPT_kilianBindingAdversary now states the context through KilianCommitment α (p.2.stmt, p.1.2.state); the residual p.1.1.… paths there come from IsPPTOn.bind_with contexts, not from the prover's output.

Not in scope: the PCP soundness predicate (P5b), which #4968 largely covers. #4968 touches nearby lines (hV.2.1, hpcp.2.2.2) in Kilian.lean/Soundness.lean, so whichever lands second needs a small merge.

Validation. Targeted --wfail --iofail build of Kilian, Soundness, Succinct, NP, Micali, MicaliSoundness, CslibFrontierResults and the Kilian/KilianSoundness/KilianSuccinct/Micali/MicaliSoundness tests (13471 jobs); lint on the three changed modules; hygiene; encoding readability and projection chain ratchets (--base origin/main); lint-style; mk_all --check; manual check (errors []).

Manuals. Operator's Manual: protocols-and-privacy.md now names KilianView/encKilianView as the verifier input of computableInPolyTime_kilianVerify. Agent Operator's Manual: no change needed (no workflow or tooling change).

AI disclosure: Jetski worker proofs (session 7134127c), under the #4817 coordinator; agent review only.

[SamuelSchlesinger]

Agent review: APPROVE at d79c958472396d837152f2438ae72026e6d19f57. Reviewer: revb-2 (Jetski session 823e1915-b7be-458e-959e-1b7d8141259d). This is agent review, not human approval.

The records replace the anonymous Kilian tuples without changing what any statement means.

• Same encoded words. KilianView extends KilianClaim encodes the claim as one framed component, and so does KilianCommitment extends KilianMessage for the message. That reproduces the old left-grouped layouts ((k, x, root), ρs, response) and ((x, root), state); KilianProverInput is the old (k, x, table). The new rfl tests in both test files pin all three. So KilianProver.IsPPT.commit, the verify/commit/respond certificates and length_kilianVerifierInput_honest_le (whose right-hand side is unchanged) state the same facts on the same words.
• Equivalent hypotheses. The new hM in both succProbability_kilianSoundnessGame_le variants, ∀ c ∈ support, (V.queryTable c.stmt).length ≤ M, is equivalent to the old ∀ x root state, ((x, root), state) ∈ support → … by structure eta. The game and the binding adversary only swap a destructuring let for field reads.
• Clients. encKilianInput and the tuple-typed commit have no users left beyond the migrated Kilian/Succinct/Soundness files and the test prover. No results entry or guide page names these shapes. NP.lean and Succinct.lean only mention the certificates by name.
• Ratchets and hygiene.
  • Projection chains and encoding readability under Crypto/Computational/Kilian count the same on main and on this head; neither ratchet changes.
  • No expose no-ops and no lines over 100 characters.
  • The head merges cleanly with current main.
• Manuals. The protocols-and-privacy edit names the new verifier input correctly. I agree the Agent Operator's Manual needs nothing.

Optional notes, none blocking:

1. computableInPolyTime_kilianRespond passes encKilianProverInput_{key,stmt,table}_polyTime enc hinput explicitly, while the commit and verify proofs close the same field goals with by fun_prop. Using by fun_prop here would make the three proofs alike, if it closes these goals; I haven't built it.
2. In computableInPolyTime_kilianVerify, hpair looks unused after the migration now that the field goals go through fun_prop. Drop it if the build agrees.
3. projection_chains_baseline.json still lists Kilian/Soundness.lean: 1, but the count is already 0 on main and on this head. This PR touches the module, so --update-baseline could lower the entry here.

#4968 touches adjacent lines, so whichever PR lands second needs a small merge. If that's this one, I'll review the merge delta. I'll queue this head once ci-checks and guide are green and I've read the notices.

[SamuelSchlesinger]

Agent review: APPROVE at 903a395ce (revb-2, session 823e1915-b7be-458e-959e-1b7d8141259d; agent review, not human approval). The delta since d79c958 only removes the unused hpair; nothing else changes. I withdraw note (3): my local baseline was stale, and origin/main has no Kilian/Soundness entry. Note (1) is reasonably declined because a bare fun_prop hits the whnf heartbeat limit. I'll queue this head once ci-checks and guide are green.

[SamuelSchlesinger]

Review follow-up (release holds) at 903a395ce4ee43c02a18c939340f3dc2f3a6fade, from revb-2 (Jetski session 823e1915-b7be-458e-959e-1b7d8141259d). This adds to my earlier approval; it is agent review, not human approval.

Rendered: I inspected p. 468 of cslib-frontier-operators-manual.pdf from Operator's Manual PDFs run 43371588937 (§14.10.3, "Kilian: honest payload and verifier input accounting"): OK. The changed sentence about the KilianView record and encKilianView renders as prose with inline code. There is no raw markdown, broken link or overflow; encKilianView wraps at a line end, as the other long identifiers on that page do. The Agent Operator's Manual doesn't mention the changed API, and the PR changes no workflow or tooling, so no edit is needed there.

Advisory notices (ci-checks run 43371588766):

• No repeated proof blocks in the 37 proofs examined.
• No parallel definitions among the 19 declarations examined.
• No duplicate statements among the 93 theorems examined.
• PR-description names: 2 hits, neither needs action.
  • encKilianInput is removed here, as the description says.
  • encKilianView is generated by enc_structure (Kilian.lean:301) and used in Succinct.lean and the tests. The checker can't see macro-generated names.

The source and API assessment in my approval above is unchanged. No holds remain.