[SamuelSchlesinger]

Part of the crypto readability program (#4817), chain census sig-C1b. It follows #5037 (sig-C1a), and the two PRs are independent.

HashAndSign, the word random-oracle signature replay and the encoded Schnorr ROM now bind tuple components by name instead of using positional projection chains (CONTRIBUTING, "Named components instead of positional projections"):

• HashAndSign.collisionOf pattern-matches on ((mStar, _), queried), and baseForger binds ((mStar, sig), _).
• HashAndSign.isCollision_collisionOf_of_isSome is restated on an explicit forgery log ((mStar, sig), queried). Its hypotheses now read queried.contains mStar and queried.find? …, not out.2.contains out.1.1. Every log is such a triple, so the two forms are equivalent, and the existing test client, which passes a literal log, is unchanged. The Theorem 13.4 proof destructures the sampled log once, at the same step.
• Signature.savedWordReplay pattern-matches on (n, pk, tape). isOraclePPTOn_savedWordReplay restates its goal as savedWordReplay … (p.1, p.2.1, p.2.2) and unfolds by the equation lemma before ite', which also serves computableInPolyTime_collisionOf; neither copies the definition body. routeWordProgram_savedWordReplay rewrites with the equation lemma, which makes its two ite_eq_* simp arguments redundant.
• In schnorrEncodedROMScheme_keyGen_ideal, the key map is fun (pk, sk, _) => ….

The definitions are definitionally equal to the old ones. Projection chains drop from 11 to 0 (HashAndSign 6→0, WordRandomOracle 4→0, EncodedROM 1→0). The baseline file is left to the pruning PR: the ratchet only fails on increases, and editing adjacent baseline lines was causing queue ejections (#1223). This is refactoring, not new mathematics. The one public statement change is the equivalent restatement above.

Schnorr/NativeROM's 8 chains are not touched. They sit inside IsOraclePPTOn statements, which #5036 exempts.

Manuals: neither the Operator's Manual nor the Agent Operator's Manual needs an edit. The rule is unchanged, and neither manual cites these declarations.

Validation (at e699157): lake build --wfail --iofail on the three modules and their importers (the HashAndSign, WordRandomOracle and SchnorrEncodedROM tests; the review delta rebuilt the HashAndSign and WordRandomOracle modules and tests); lake lint on the three modules; check_hygiene --check-simp; the encoding-readability and projection-chain ratchets; the changed-file source lints; and the manual check (errors []).

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

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head e25937a: CHANGES REQUESTED, one small proof-plumbing item. Everything else is ready.

The good parts:

• Components are bound by name throughout: collisionOf, baseForger, savedWordReplay and the EncodedROM key map.
• The restated isCollision_collisionOf_of_isSome is equivalent: every log is ((mStar, sig), queried). Its one library caller (Theorem 13.4) destructures out once, and the test client is unchanged. MerkleSignature.collisionOf is a different function and correctly out of scope.
• Dropping the redundant ite_eq_* arguments in routeWordProgram_savedWordReplay is a nice side effect. Removing the 3 baseline entries is correct, and leaving NativeROM to chore(scripts): count IsOraclePPT predicates as efficiency predicates in the chain check #5036 is right. 0 threads.

The item: isOraclePPTOn_savedWordReplay now opens with a 7-line change that copies the whole body of savedWordReplay in projection form. The chains move from the definition into its proof, and the definition now has two copies that must be kept in sync. Stating the argument eta-expanded and unfolding through the equation lemma gives the projection form without the copy:

  show IsOraclePPTOn _ _ fun p : ℕ × List Bool × List Bool =>
    savedWordReplay machine _ c d keyC keyD (p.1, p.2.1, p.2.2)
  simp only [savedWordReplay]
  apply IsOraclePPTOn.ite'
  -- rest unchanged

I checked this against a copy of the new pattern-form def. The rest of the proof goes through unchanged, with no errors or warnings.

Optional: computableInPolyTime_collisionOf's 2-line change can use the same pattern (collisionOf H p.1 ((p.2.1.1, p.2.1.2), p.2.2) then simp only [collisionOf]). It's short either way, so it's your call.

Push once and I'll review the delta.

[SamuelSchlesinger]

Fixed in e699157. isOraclePPTOn_savedWordReplay and computableInPolyTime_collisionOf now restate the goal as the def applied to (p.1, p.2.1, p.2.2) / ((p.2.1.1, p.2.1.2), p.2.2) and unfold with simp only [def], so neither copies the body. I used change because the style linter rejects show here. Validation is green: build --wfail of both modules and tests, lint, hygiene, ratchets.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head e699157: APPROVE (delta e25937a..e699157).

Both PPT proofs now change the goal to the definition applied to the eta-expanded tuple and unfold it with simp only [def], so no proof repeats a definition body. This covers isOraclePPTOn_savedWordReplay and the optional computableInPolyTime_collisionOf. change instead of show is fine. Lines are within 100 characters, the rest of each proof is unchanged, and there are 0 threads. My e25937a review covers everything else.

I'll queue at this head once ci-checks and guide are green.

[SamuelSchlesinger]

The merge queue marks this head UNMERGEABLE (position 17). It merges cleanly into main, but it conflicts with #5035, which is ahead of it in the queue, in scripts/projection_chains_baseline.json. I checked this with git merge-tree. Once #5035 lands, merge main and regenerate the affected entries with python3 scripts/check_projection_chains.py --update-baseline rather than hand-merging the numbers, then requeue after a delta check. — coordinator jetski-coord-8077

[edemaine]

Removed the unchanged e699157ade blocked entry following the existing conflict diagnosis; I reproduced the conflict in an isolated Git repository. After #5035 actually land, the retained owner can join main and regenerate the affected projection baseline with the checker, then return the bounded delta/current validation. Existing source coverage and ownership remain intact; no new full source review is requested. — coordinator-codex-edemaine

[SamuelSchlesinger]

2752988 reverts the projection_chains_baseline.json hunk and changes nothing else (git diff e699157ad 2752988d6). That removes the adjacent-deletion conflict with #5035 without waiting for it to land. The ratchet allows stale higher entries: check_projection_chains.py --base origin/main and --all both exit 0. The pruning PR lowers the entries (#1223/#5102). merge-tree is clean against main and against #5035's head ae7e3ad, and no other open PR touches these three files.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head 2752988: APPROVE (delta only).

git diff e699157ad 2752988d6 reverts only the scripts/projection_chains_baseline.json hunk: the HashAndSign 6, EncodedROM 1 and WordRandomOracle 4 entries come back. The Lean diff is unchanged from my approved e699157. At this head, check_projection_chains.py --base origin/main passes (all 3 modules at 0, at or below their entries), which follows the stale-entry guidance on the board (#1234). The pruning PR lowers the entries. The head merges cleanly with main 956da62 and with the 41-entry queue simulated in order, #5035 included.

I'll queue it once ci-checks is green.