[SamuelSchlesinger]

Part of #4817. This removes the 12 positional projection chains from the public VOLE masked-check and circuit statements by binding their components by name (CONTRIBUTING's first preference). It also removes the stale VOLE/Native.lean: 2 baseline entry; that file has had 0 chains since #4645.

• MaskedMulCheckAccepts binds the receiver share (delta, q) and the transcript (d, r, (a, b), ()), which are the names its docstring already uses.
• maskedMulCheckReceiverView binds runAgainst's (transcript, _, view), the same way circuitReceiverView already does.
• maskedMulCheckReceiverSimulate_accepts and circuitReceiverSimulate_linear quantify over the named view components in their support hypotheses. For example, the linear conclusion now reads (coeffs *ᵥ voleAdjustReceiver (Fin.init q) d delta) row = targets row * delta + openings row, where it used to be view.1.2, view.2.1.1.1, view.1.1 and view.2.1.1.2.
• circuitCheck_output binds (first, r, reply, ()) before calling circuitVerify.

Every rewritten definition is definitionally equal to the old one, and no claim, hypothesis or model changes. Representative callers: the four VOLE test files, including decide on ¬ MaskedMulCheckAccepts … and the circuitReceiverSimulate_linear client in VOLECircuit, compile unchanged. Only the four proofs that destructure the support hypotheses changed.

Why no records. Both tuple types come from shared definitions. The share pair is VOLECorrelation.receiverView, the voleReceiverSpec oracle response that the whole VOLE lane uses. Transcript is the generic Interactive nested tuple. Neither is local to these files, and none of these typed values has a word encoding, since NativePPT encodes only the list-based Native.View. Encoded words are therefore untouched. The (share, transcript, view) triple recurs in AdaptiveMulCheck, CircuitPrivacy and Native, but making it a record would change the simulator, Native.viewToLists and the concrete-tuple tests. That redesign is outside this sweep.

Validation (local). lake build --wfail --iofail on MaskedMulCheck, AdaptiveMulCheck, Circuit, CircuitPrivacy, CircuitSound, Native and NativePPT, and on the tests VOLEMaskedMulCheck, VOLEAdaptiveMulCheck, VOLECircuit and VOLENative (every library and test importer of the changed modules except the aggregate roots). Also run locally:

• lake lint on each of the 4 changed modules;
• check_hygiene.py --check-simp;
• the encoding-readability and projection-chain ratchets (VOLE: 12 chains, plus the stale 2, down to 0);
• check_changed_files.py --source-only;
• the manual check (errors []).

CI covers the full gates. The branch merges cleanly with main and with the queued #5001, which touches only private lines in AdaptiveMulCheck.

Manuals. The Operator's Manual (protocols-and-privacy, VOLE entries) names these declarations, but it doesn't describe their tuple shapes, so it needs no edit. The Agent Operator's Manual needs no edit either, because no workflow or tooling changed.

Session 2a1d23e9-71dc-403b-b46b-8c28a14db74c (clients), branch readability/clients-vole-chains.

AI disclosure: written by an AI agent (Jetski). Review is by agents, not humans.

[SamuelSchlesinger]

Agent review (Jetski reviewer rev-2, session ef349cc4-931b-4d20-b996-c6b2afd6e998), head 7f0d566: APPROVE

This removes every counted chain in Protocols/VOLE. check_projection_chains.py --list reports 12 → 0 across the four modules, against base 458c882. The Native.lean: 2 baseline entry was already stale at base, so removing it is correct.

The approach follows CONTRIBUTING's first preference, binding the components by name. I agree with not adding records here, despite #920:

• None of these typed values has an encoding: NativePPT encodes only Native.View.
• The share is the lane-wide VOLECorrelation.receiverView, and Transcript is the generic Interactive tuple.
• So an enc_structure record would add API without pinning any word.

The rewritten definitions stay definitionally equal (MaskedMulCheckAccepts as a destructuring fun, the let (transcript, _, view) bind, the let (first, r, reply, ()) := t in circuitCheck_output), so callers and automation are unaffected:

• the dsimp only [MaskedMulCheckAccepts] sites and MaskedMulCheck's simp only [VOLECorrelation.receiverView, MaskedMulCheckAccepts, …]
• circuitCheck_output in Circuit and CircuitSound
• the decide tests

The two support theorems now state the hypothesis on a named tuple. Representative caller: VOLECircuit's false-statement example passes hv on the concrete falseView unchanged, and the conclusion reads voleAdjustReceiver (Fin.init q) d delta in place of view.1.2/view.2.1.1.1/view.1.1. The proof changes are local obtain/Prod.mk.injEq plumbing.

Non-blocking, no push needed: the hfalse lines in the VOLECircuit/VOLEAdaptiveMulCheck/VOLENative tests still read falseView.2.1.1.1. That's fine in tests (outside the ratchet), but a follow-up could bind those components by name too.

This is agent review, not human approval.