sair-modmul-carrysave

Carry-save Montgomery modular multiplication (SAIR Modular Arithmetic Challenge)

A learned model that computes (a * b) mod p for prime moduli from 2 bits up to 2048 bits. Every operand-dependent state transition in the inference path is produced by trained weights; re-randomizing any single cell breaks the pipeline while the surrounding loop is untouched. Every learned cell is enumeration-certified exact over its complete finite input alphabet. The exact setup arithmetic that remains, and where it runs, is itemized under Compliance.

Total size: 37,767 parameters.

Result

Measured by the challenge's own evaluator inside the official sandbox image (python:3.12-slim, CPU torch, --network none --read-only --memory 8g --cpus 4), twice, on 1100 freshly generated problems with a different random seed each time. Both runs:

• overall_accuracy = 1.0
• highest_tier_above_90 = 10 (the maximum the challenge admits)
• Scored tiers 1-10: 100/100 each
• Deterministic: yes; manifest, static check and preprocess-isolation check pass
• Inference wall-clock: 71.2 s and 60.6 s of the 300 s budget, all eleven tiers complete. Model load is a further ~2 s, which the rules budget separately.

Diagnostic tier 0: 70/100, unscored. Tier 0 is pure multiplication, so the generator picks a modulus larger than the square of the widest operand: the Mersenne primes 2^2203-1, 2^4253-1 and 2^9689-1 for its top three sub-levels. Those thirty rows are past this model's declared 2,174-bit capacity and are declined rather than guessed.

How it works

The model learns the Montgomery multiplication automaton in a redundant carry-save representation, where the running product is held as two equal-weight bit vectors (A, B) whose sum is the value. In this basis each Montgomery tick is a strictly local, translation-invariant digit map: two 3:2 compressions, a parity read at position 0, and a right shift. That locality is the whole point. A non-redundant binary scan forces a global carry circuit at every step; carry-save form removes it from the function class, and what is left is a Boolean map over a finite local alphabet.

Components, all learned and all enumeration-certified:

• tick cell (weights/cs_tick.pt, 32,800 params): trained Embedding tables over the exact radius-1 local alphabet (Embedding(2^14, 2) for the state map and Embedding(2^4, 2) for the quotient). Supervised against the closed-form truth table; gradient descent from random initialisation reaches the same exact table. Enumeration over all 16,384 + 16 configurations is a proof of exactness at every width.
• fold cell (weights/cs_exit.pt, 3,394): a learned local carry-save compressor, trained to reproduce (A, B) -> (A xor B, shift(A and B)), iterated to canonicalize a redundant pair to binary. Enumerated over every width-7 window (16,384 configs).
• compare cell (291): an MSB-first three-state comparator producing q = [t >= p]. Full transition table (12) certified; scan checked on 800 pairs.
• subtract-prep cell (1,282): forms the two's-complement carry-save pair for the final conditional subtract. Enumerated over its 8 local inputs.

Two Montgomery passes (MonPro(a, b) then MonPro(t1, R^2 mod p)) give a*b mod p in [0, 2p); the compare, subtract-prep and fold exit canonicalizes to [0, p).

Why the fold chain stops on its carry plane

Each fold step moves every carry up one position, so the chain needs as many steps as the longest carry run in the value it is canonicalizing. After a Montgomery pass that run is short. After the conditional subtract it can span the whole width: subtracting p from t = p + k for small k adds the two's complement of p and produces a carry that crosses the word. The chain exits when the compressor returns an empty carry plane, capped at the width. The exit point depends on the operands; the answer does not, because the compressor is idempotent once no carries remain.

Compliance

The rules prohibit hand-coding the arithmetic and ask instead that the capability reside in the trained parameters. This section states exactly what is exact and what is learned.

Learned (every operand-dependent state transition). Both Montgomery passes including the quotient-bit read, all three fold chains, the comparator, the subtract-prep cell, and the p = 2 path (which reads a trained fold cell's carry rather than performing a bitwise AND). No XOR, AND, addition, shift, comparison or subtraction operator acts on operand state in the forward path, and no predicted tensor becomes a Python integer mid-computation.

Exact arithmetic that remains, and where. Operand reduction a mod p and b mod p (the same operation, in the same place, as the official digit_transformer reference); the Montgomery constant R^2 mod p; the two's complement of p; the p = 2 test; bit packing. The middle two are full-width and are functions of p alone; none of these depends on both operands and none can compute the product.

Structural (architecture, not arithmetic). The two-pass Montgomery schedule, the tick count and width as functions of the modulus bit length, the scan direction, the argmax and broadcast of the quotient bit, the three-state comparator decoding, and the fold chain's carry-plane stopping rule.

Weight-perturbation evidence, the rules' stated operational test. One cell re-initialized at a time, everything else including the loop left alone, seeded explicitly, and scored over three seeds (weight_control2.py, weight_control.json):

The second row set is required. After the second Montgomery pass the value satisfies V2 < p + R2 and V2 = a*b mod p, so V2 is either the reduced answer or the answer plus p, and the second case needs the answer to be smaller than R2. Random operands produce full-width answers, so they never request the conditional subtraction. A control that samples only random rows therefore cannot tell a trained comparator from a randomized one. The invariant across the table: no randomized cell, at any seed, is correct on both row sets, and the trained pipeline is correct on both.

Certification

certificate.json records exhaustive enumeration of every learned cell against its exact local truth table over its complete input alphabet. All four cells certify. The value-level induction that composes them into (a*b) mod p is machine-checked in the accompanying proof assistant development (paper/CarrySaveValueInduction.lean).

Runtime requirements

torch only, plus the Python standard library. There is no numpy import and no other third-party import; the optional modchallenge interface base class is guarded and falls back to object.

Verification

The primary receipt is the challenge's own evaluator run inside the official sandbox image, recorded in verification.json: 1100 freshly generated problems, fixed seeds, --cpus 4, all eleven tiers complete, overall_accuracy = 1.0, highest_tier_above_90 = 10, deterministic, inference 60.6–71.2 s.

harness_check.py ships here and re-runs exactness checks against this artifact directly.

Training

Tick cell: supervised filling of Embedding tables against the closed-form radius-1 truth table of the carry-save Montgomery tick, with a logit margin of 10; gradient descent from random initialisation reaches the same exact table. Exit cells: supervised on their own local transition maps. Full method and the enumeration certificates are in the accompanying paper:

Paper: Locality by Representation: Certified Learned Modular Multiplication at 2048 Bits (Recognition Physics Institute, 2026).