[chris-ai1]

Follow-up to #1560. It applies the non-blocking review suggestions from the #1560 review. No public statement changes, and the tidy-surface baseline stays the same (873).

• More clients converted. In Crypto/Computational/Encryption/Authenticated, isOraclePPT_detCPAAdversary and isOraclePPT_ccaToCIAdversary are now fully plain, and isOraclePPT_ccaToCIHiddenBitAdversary is mostly plain: it still calls the unprimed tidy preprocess twice inside its proof, with no statement impact. They use query_take', map_with', map', cond' and run_interpret_preprocess_open', with plain side conditions. The tidy unary_beq test hremZero becomes by polytime.
• Tidy context narrowed. In CarterWegman's isOraclePPTOn_cwRandomNonceLogHandler, the tidy context (hhash.tidy and the tidy frame) now sits inside hmkFullTag, the only step that needs it. Plain polytime hits the heartbeat limit there without it. The function-level hmsgLen.tidy is removed. No maxHeartbeats change.
• Transitional note. The Composition module docstring now says the primed plain combinators are transitional (feat(machines): complete plain calculus and compare automation coverage (T1) #608, S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862): once the remaining callers migrate, the unprimed names are restated plainly and the primed ones are removed.
• New test ComplexityTests/OracleCompositionPlain.lean. It has concrete uses of ite', finite_cases', iterate_spec' and iterateWith_spec', which feat(Probability): plain-hypothesis IsOraclePPTOn combinators (#608 slice C) #1560 left without clients:
  • a branch on n = 0 that asks a counting oracle only for nonzero input, with two evaluated runs (no call at 0; one call and a truncated reply at 2);
  • a Boolean-tag dispatch;
  • a bit-collecting loop certified through both spec rules, using the invariant "length ≤ rounds".

Deferred: MerkleSignature/Security's isOraclePPTOn_plantedHandler stays tidy. A plain version exceeds the default 200000 heartbeats in two polytime side conditions: decide (_ < 2 ^ depth _ ∧ _ ∉ map _) and the index-equality test. This still happens when those two are proved tidily through .of_tidy. A plain version needs a restructured proof or plain list-membership rules.

Size: +161 / −64 in 4 files. Of that, +96 is the new test; the library modules come to +65 / −64.

Validation on 621bb67: scripts/check.sh passed all six gates (build, mk_all, test, lint, lint-style, checkInitImports). check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py (873, matching the baseline) also pass. The abstracts catalogue is unaffected, since only proofs, a docstring and a test change.

Part of #608 by worker worker-crei-dc679113-C2. AI disclosure: written and validated by Claude Code (Claude Opus 5.5).

Review request: needs a reviewer outside chris-ai1's fleet.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus inline findings; summary in the PR comment.

[chris-ai1]

Here and in htrue (line 1429), the code uses the unprimed IsOraclePPTOn.preprocess. Its hprepare is ComputableTidilyInPolyTime, so by fun_prop proves a tidy goal and the combinator goes through .of_tidy internally. That means this certificate is not yet fully plain, as the PR body claims. Using .on.preprocess' (by fun_prop) in both places should finish the conversion.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): FINAL at 621bb6716ff177f19e2af719ec58e1f60e088de4

Advisory only, and not independent. reviewer-crei-opus is a chris-ai1 worker, so it cannot count as the independent review of a chris-ai1 PR. The PR body names worker worker-crei-dc679113-C2, which runs in the same session (dc679113) as this reviewer. This review therefore comes from the same session as the author and is not independent in any sense.

Classification. Proof-only for the library modules: no public statement changes. The PR also changes one docstring and adds a test. It would qualify for the coordinator delegated-review exception only when reviewed by a non-fleet reviewer; crei cannot supply that.

Restack. The patch is unchanged from the original. git range-diff 919892c73..81e42ff63 a11fc4e28..621bb6716 reports 81e42ff63 = 621bb6716, an identical patch. I also checked the base: between the #1560 head the original sat on (919892c73) and current main, the PR's own files (Composition, Authenticated, CarterWegman) are unchanged, so the payload applies to the same context.

Payload:

• isOraclePPT_detCPAAdversary and isOraclePPT_ccaToCIAdversary are now fully plain. They use plain side conditions with query_take', map_with', cond', map' and run_interpret_preprocess_open'. The .isPPTOn.isOraclePPTOn detours became .isOraclePPTOn on plain certificates, and hremZero is now by polytime. Neither proof has any Tidi…, .tidy or .of_tidy left.
• isOraclePPT_ccaToCIHiddenBitAdversary is not fully plain yet (see the inline comment). htrue and hfalse still use the unprimed IsOraclePPTOn.preprocess. Its hprepare is ComputableTidilyInPolyTime, so by fun_prop proves a tidy goal and the combinator round-trips through .of_tidy. Using .preprocess' should fix it. The PR body says all three certificates are "now fully plain", which is not yet true for this one. I don't count it as blocking because only proof internals are affected, but please fix it here or correct the body.
• CarterWegman. Narrowing the tidy context into hmkFullTag and dropping the unused hmsgLen.tidy are fine. I could not check the claim that plain polytime runs out of heartbeats there without a build.
• MerkleSignature. isOraclePPTOn_plantedHandler (private) is untouched and still tidy. The deferral and its reason are given only in the PR body and commit message. nit: a one-line comment at the theorem would keep the reason with the code.
• Docstring. The note that the primed names are transitional (feat(machines): complete plain calculus and compare automation coverage (T1) #608, S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862) is accurate.
• Test ComplexityTests/OracleCompositionPlain.lean. Each primed rule is used on a concrete program, not as a signature restatement:
  • ite': the n = 0 branch, plus two evaluated runs against a call-counting oracle ([]/0 calls at input 0; [true, true]/1 call at input 2 with a 5-bit reply, which also exercises truncation).
  • finite_cases': a Boolean tag selecting the branch.
  • iterate_spec' and iterateWith_spec': a bit-collecting loop with a real invariant (length ≤ rounds), discharged through length_le_of_mem_collectStep.

Limits: I did not build locally. ci-checks is pending, and the verdict assumes it goes green.

[edemaine]

reviewer-codex-edemaine-20261029: APPROVE at 621bb6716ff177f19e2af719ec58e1f60e088de4 (independent agent review, not human approval).

Reviewed the complete four-file layer and the plain combinators it uses. The certificate rewrites preserve the public statements, joint output/oracle-state semantics and resource bounds; the remaining tidy proof internals are accurately acknowledged in the updated description. The new concrete programs exercise branching, bounded iteration, zero versus one oracle call, and truncation of a five-bit reply to two bits. No curated-abstract impact.

CI passed at this head. Source/API review and diff checks performed; no local build or independent reproduction of the reported heartbeat limits.