opt_modred: admit bounded nonlinear slots as opaque digits (-opaque-slots)

[akashlevy]

Problem

A mod-7 checksum spelled as a balanced 8→4→2→1 tree of 6→3 residue LUTs was
left fully serial by opt_modred.

The leaf tables are not linear in the raw bits: a 6→3 table decodes the
canonical digits only, so it answers 0 — not the residue — for the 2^k-1
its own inputs can reach. The proof therefore died at the leaves, even though
the tables above the leaves genuinely do add mod M over whatever the leaves
emit. opt_modadd_tree does not own this shape either, since it is a tree
rather than a serial cascade.

Change

New -opaque-slots (default off). A slot whose own reduction proof failed
is admitted as an opaque k-bit digit once a sweep shows its image misses
2^k-1; the levels above it are then proven linear in those digits and
re-emitted as one end-around-carry carry-save tree.

A leaf is never treated as a residue, only as a bounded unknown digit — that is
what keeps this sound on tables that are merely mod-M-shaped.

Supporting pieces:

• check_linear gains a sweep_max out-parameter and keeps sweeping past a
  mismatch when the cut is cheap enough (-max-bound-bits, default 10 bits),
  purely to get that image bound. bound_memo keeps the tightest bound any cut
  of a node yielded.
• Proof::opaque counts admitted digits through the whole composition.

Guards

• Two opaque digits minimum. One is a serial cascade's own state, where the
  tree merely re-adds the digit the step already produced while the chain stays
  alive to feed the later steps — area for no depth. Measured +9.5 LoL on a
  mod-61 cascade before this guard existed.
• Cell-level region depth is only skipped in favour of the bit-level arrival
  test when the match actually uses opaque digits, since an opaque-slot region
  keeps the leaf tables that the depth above is counted over.

Validation

Consumer-side measurements are in the companion PR. Summary: 3 cases win
(−4.75, −6.25 and −1.50 LoL, each also 10–15% smaller), 1 trades 0.75 LoL for
6.5% area, and 20 of 24 A/B'd designs — barrel shifters, add trees, add chains,
multipliers — are bit-identical.

equiv_opt -assert passes on the three cases where the new path fires and the
design is small enough to prove, including the one whose leaf tables differ
from A % 7 on ~74% of inputs.

Because the flag defaults off, this is a no-op on its own and safe to merge
first: with -opaque-slots absent, every A/B'd case reproduces its baseline
metrics exactly. The behavior change lands atomically in the preqorsor PR.

Made with Cursor

[greptile-apps]

Greptile Summary

The PR adds opt-in support for treating bounded nonlinear reduction slots as opaque digits, enabling higher reduction-tree levels to be rewritten as carry-save trees.

• Exhaustively records output bounds for inexpensive nonlinear cuts.
• Tracks opaque digits through composed proofs and requires at least two before rewriting.
• Adds -opaque-slots and -max-bound-bits, while clamping shift-related bit-count options to valid signed-shift ranges.

Confidence Score: 5/5

The PR appears safe to merge.

No blocking failure remains.

Important Files Changed

Filename	Overview
passes/opt/opt_modred.cc	Adds bounded opaque-slot proof composition, associated profitability guards and options, and correctly clamps the previously unsafe shift-count arguments.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Candidate reduction root] --> B[Build and sweep cut]
    B --> C{Cut linear?}
    C -->|Yes| D[Compose proven slot weights]
    C -->|No, bounded and opaque enabled| E[Record image bound]
    E --> F[Admit slot as opaque digit at upper level]
    D --> G{Profitable rewrite?}
    F --> G
    G -->|Yes| H[Emit carry-save tree and normalize]
    G -->|No| I[Keep original region]

Loading

_{Reviews (2): Last reviewed commit: "opt_modred: keep user-supplied bit count..." | Re-trigger Greptile}

[akashlevy]

@greptileai review

[akashlevy]

The motivating win on qor_compress_mux_path6 (30.75 → 26.00 LoL) already landed as -opaque-digits in #302. The tagram LoL-for-area trade is documented there too. This branch now conflicts on opt_modred.cc and would re-litigate a matcher that already fires.

Companion Preqorsor PR: Silimate/preqorsor#2293 (closing as well).