spec: Leverage NEG in DVRM

[erik-3milabs]

Use NEG in DVRM to optimize computing the absolute values abs_r and abs_d.
Applying this technique allows abs_r and abs_d to be stored in DWordWLs rather than DWordHLs, saving four columns on the chip.

[greptile-apps]

Greptile Overview

Greptile Summary

This PR optimizes the DVRM chip by replacing the SUB template with the NEG template for computing absolute values of r and d, achieving a 4-column reduction in the chip's size.

Key Changes

• Changed representation: abs_r and abs_d changed from DWordHL (4 Half limbs) to DWordWL (2 Word limbs)
• Replaced constraints:
  • When negative: Use NEG template instead of SUB template
  • When non-negative: Copy only 2 Word limbs instead of 4 Half limbs, with appropriate casting from DWordHL to DWordWL
• Removed range checks: The IS_HALF range check constraints for abs_r and abs_d are no longer needed since the NEG template doesn't require range checking on its output
• Updated LT interaction: No longer needs to cast abs_r and abs_d since they're already in DWordWL format

Correctness

The changes are mathematically sound and consistent with:

• The NEG template signature (input: DWordHL, output: DWordWL)
• The LT interaction signature (expects DWordWL inputs)
• The property that NEG produces valid DWordWL outputs without requiring explicit range checks

This optimization directly builds on the NEG template introduced in PR #270.

Confidence Score: 5/5

• This PR is safe to merge with no identified risks
• The changes are a straightforward optimization that correctly applies the NEG template. All type signatures match, iteration bounds are correctly updated to match the new DWordWL representation, and the removed range check constraints are justified by NEG's design. The changes are well-documented and mathematically sound.
• No files require special attention

Important Files Changed

Filename	Overview
spec/src/dvrm.toml	Replaced SUB template with NEG template for computing absolute values, changing abs_r and abs_d from DWordHL to DWordWL representation, removing range check constraints, and updating iteration bounds to match new representation
spec/dvrm.typ	Removed outdated documentation reference to range check constraints that are no longer needed with the NEG template

Sequence Diagram

sequenceDiagram
    participant DVRM as DVRM Chip
    participant NEG as NEG Template
    participant LT as LT Lookup
    
    Note over DVRM: Input: r, d (DWordHL)
    Note over DVRM: sign_r, sign_d (Bit)
    
    alt sign_r == 1
        DVRM->>NEG: "Compute abs_r from r"
        NEG-->>DVRM: "abs_r (DWordWL, 2 limbs)"
    else sign_r == 0
        Note over DVRM: Copy r to abs_r (2 limbs)
    end
    
    alt sign_d == 1
        DVRM->>NEG: "Compute abs_d from d"
        NEG-->>DVRM: "abs_d (DWordWL, 2 limbs)"
    else sign_d == 0
        Note over DVRM: Copy d to abs_d (2 limbs)
    end
    
    DVRM->>LT: "Verify abs_r < abs_d"
    LT-->>DVRM: "Return verification result"
    
    Note over DVRM,LT: Optimization: 4 columns saved<br/>by using DWordWL instead of DWordHL

Loading