Rounding after every rescale is the range-relation bottleneck — and range relations are what zkGPT's whole optimization effort attacks.

• Each quantized product must be rescaled and rounded, and every rounding is a range relation. zkGPT states plainly that range relations are its dominant cost — more expensive than arithmetic relations — so requantization is where the prover time concentrates, as it does for DeepProve (27%).
• Constraint fusion is the direct attack: merge adjacent rounding constraints so several rescales share one range relation, cutting the count without changing precision. This is the same idea as DeepProve's delayed requantization, done at the constraint level rather than the field level.
• Lasso proves the range relations; the rescale itself is a fixed-point multiply-and-shift with the rounded result supplied as advice.

The paper describes an explicit two-case (in-range/out-of-range) construction with an InRange product. The code has neither: clamping is folded into the Requantise table, and the in/out-of-range distinction is carried by how many high-order zeroing chunks the decomposition needs.

More than 50% of the prover cost comes from activation functions, Softmax, and requantization, with the latter being the most expensive component overall, accounting for 27% of total prover time. Consequently, optimizing any of these components would yield substantial improvements in overall prover performance.

DeepProve · §5

Requantizing incurs accuracy loss and thus avoiding it increases the accuracy. This strategy is even more effective when using a large field 𝔽 during proving.

DeepProve · Appendix C

• The core op is four steps: multiply by the fixed-point multiplier, add the rounding constant, right-shift, then a Requantise table lookup that clamps internally. There is no separate clamp gadget and no InRange product — input.clamp(min,max) is baked into the table's definition.
• The paper's "two cases" appear only as a table-set choice. RequantCtx::lookup_tables picks by the number of high-order zeroing chunks: 0 → [ShiftCheck, Requantise]; 1 → add SignedZeroCheck; more → add ZeroCheck too. The out-of-range machinery is those extra 16-bit chunk tables, not a branch in the protocol.
• The wide accumulator is decomposed into a shifted part (the right-shift bits, range-checked), the value chunk (hits the Requantise table), and zeroing chunks (high bits forced to zero). The verifier never gets an oracle for the pre-shift value.
• Delayed requantization. An $N\times M$ by $M\times P$ integer matmul produces at most $2q + \log_2 M + 1$ bits. If that still fits the field and the next lookup's domain, skip the requant. A bigger field buys accuracy, not just speed.

        // Apply the fixed point multiplication, rounding and right shift
        let rescaled_input = input
            .mul_scalar(self.fixed_point_multiplier())
            .add_scalar(self.rounding_constant())
            .bitwise_right_shift_scalar(self.right_shift() as Element);
        // Perform the lookup, the table will handle clamping internally
        table.lookup_tensor(rescaled_input)

        match chunking_info.number_of_zeroing_chunks() {
            0 => vec![Table::new_shift_check(), Table::new_requantise()],
            1 => vec![
                Table::new_shift_check(),
                Table::new_requantise(),
                Table::new_signed_zero_check(),
            ],
            _ => vec![
                Table::new_shift_check(),
                Table::new_requantise(),
                Table::new_zero_check(),
                Table::new_signed_zero_check(),
            ],
        }

No requantization protocol. Division is an ONNX op proven with a non-deterministic advice value.

• The execution trace records, for non-deterministic operations such as division, an advice value — the prover supplies the quotient and the relation is checked. That is the entire mechanism.
• Nothing is said about when rescaling must fire, how overflow is prevented across a deep transformer, how table domains stay addressable, or what the accumulated rounding error does to accuracy.
• Because Jolt Atlas is lookup-native over a large field, the pressure is different: the binding constraint is lookup table domain size, which is attacked by prefix-suffix decomposition and teleportation rather than by shrinking values back down.
• The "advice value" is more structured than the paper lets on. The fused-rebase seam supplies rescaled = acc >> S (ClampAcc) and remainder R (RescaleRemainder) as advice, forces R ∈ [0,2^S) by an identity range check, and proves acc = rescaled·2^S + R inside the operator's own sumcheck — no separate Div node. It is the single most reused gadget in the codebase (Einsum / Mul / Square / Cube / MeanOfSquares).

Requantization exists here, and it is a first-class building block: PosTrunc / Trunc, table-lookup truncation protocols that fire after every fixed-point multiplication.

• After each fixed-point multiply the scale doubles and must be shifted back down. Hao et al. give this its own protocol pair -- PosTrunc (positive inputs) and Trunc (signed) -- built from the same digit-decomposition-plus-lookup machinery as everything else.
• It is used inside the higher functions rather than as a separate layer: the exponential protocol, for instance, multiplies the per-digit lookups together and calls PosTrunc after each product to hold the scale.
• Cost tracks the truncation bitlength, and nothing else. The paper isolates this cleanly: varying the scale changes the runtime of PosTrunc and Trunc and of essentially nothing else in the building-block table.
• This is the same operator that costs DeepProve the largest single share of its prover, reached from a different substrate -- and, as there, it is discharged by decomposing a wide value into narrow chunks and looking the chunks up.