claimroutineinferred_dep

Packed shifts match ideal XOR off bad set

Packed cyclic shifts match the ideal XOR outside a bad set
reduces the packed implementation to the ideal XOR
Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

Let S0S_0 be the composition of the packed cyclic shifts implementing the lines of on the segments at j0,…,jf−2j_0,\ldots,j_{f-2}, and let T0T_0 be the ideal permutation that performs the XORs yji←yji⊕xjiy_{j_i}\leftarrow y_{j_i}\oplus x_{j_i} for 0≤i<f−10\le i<f-1 and fixes all other address coordinates. Then S0S_0 and T0T_0 agree at every address outside B\mathcal B, the set of addresses at which some used guard value in yy or zz fails .

In plain English

The composition S0S_0 of packed cyclic shifts that implements the eight packed additions on the segments at j0,…,jf−2j_0,\ldots,j_{f-2} agrees with the ideal permutation T0T_0, which XORs yji←yji⊕xjiy_{j_i}\leftarrow y_{j_i}\oplus x_{j_i} for 0≤i<f−10\le i<f-1, at every address outside the bad set B\mathcal B. Here B\mathcal B is the set of addresses where some used guard value in yy or zz fails the guard-interval condition.

Why it's here

This reduces the packed implementation to the ideal XOR on all but a small set of addresses. Away from B\mathcal B the guard values stay in range, so the eight controlled additions from the previous claim act as a clean conditional parity flip on each segment. The next claims use this to bound ∣B∣|\mathcal B| and to show the cost of implementing the rotations is dominated by the stated time bound.”
Classified routine:
Direct consequence of the preceding claim (eight controlled additions flip parity) applied segmentwise. Away from the bad set no guard value overflows, so the packed cyclic shifts coincide with the ideal XOR permutation; this is bookkeeping.

Uses

claimEight controlled additions flip parity

Used by

claimBad set is small and invariantclaimRotations cost O(V L^τ) via swaps

Sources

PaperOpen
Section
§5.2 Packed changes of selected address bits
Page
—
Label
—
Line
sections/05-layers.tex:292
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Packed cyclic shifts agree with ideal XOR off bad set" rests on claim-lem-packed-selected-bit-rectangle-1