Verilog widths: big_frame.t27's 600000- and 1200000-byte frame arrays are exact sizes, not an underflow -- record them in the ledger #8902

Master's Verilog widths (absurd-width ledger) check has been red since #8764 added specs/tri/t27b/conformance/big_frame.t27. Part of the t27b coverage epic (see #8326 and #6063).

What the check reports

Run 38100044010 on master 39d5af3:

scanned 1857 spec(s) with target/release/t27c
      specs/base/ternary_memory.t27: 3801183
      specs/compiler/stdlib.t27: 4198431
  NEW specs/tri/t27b/conformance/big_frame.t27: 4799999,9599999
FAIL: 1 spec(s) newly emit a width that cannot be real.

Why it is not an underflow

tools/check_verilog_widths.py exists to catch range_decl underflows ([4294967295:0]). Its ledger, tools/verilog_width_baseline.txt, already holds two specs whose huge widths are exact arithmetic on what the spec asks for (stdlib.t27, ternary_memory.t27), each with the arithmetic written out.

big_frame.t27 is the same class. It is t27b's frame-size conformance spec (see #8758): its whole point is local arrays of more than 1 MiB on the stack.

• far_ends holds two [600000]u8 arrays: 600000 * 8 = 4,800,000 bits, so [4799999:0].
• deep_big holds one [1200000]u8: 1200000 * 8 = 9,600,000 bits, so [9599999:0].
• The other locals stay below 2^20 bits: Tape is 65536 * 8 + 64 = 524,352 bits, and mid_frames is 80,000 bits. The test body's [1100000]u8 is not emitted, because test blocks have no Verilog form.

The widths match the checker bit for bit. Shrinking the arrays would remove what the spec tests, and excluding conformance specs from the scan would hide the next real underflow in one.

Fix

Add the spec to tools/verilog_width_baseline.txt with the arithmetic, as the two existing lines have it. The checker, its threshold and its scope are unchanged.

Boundary

• tools/verilog_width_baseline.txt

User Scenarios

• Given the Verilog width checker scans all specs, When it encounters specs/tri/t27b/conformance/big_frame.t27, Then it reports widths 4799999 and 9599999 as newly seen and fails the build.
• Given the two large arrays in big_frame.t27 are exact sizes (600000×8 and 1200000×8 bits), When the baseline ledger records their arithmetic, Then the checker treats them as known-good and the build passes.

Requirements

• FR-001: The file tools/verilog_width_baseline.txt MUST contain a line for specs/tri/t27b/conformance/big_frame.t27 with the two widths and their arithmetic (6000008=4799999+1, 12000008=9599999+1).
• FR-002: The checker tools/check_verilog_widths.py MUST continue to use the same threshold and scope; only the baseline is updated.
• FR-003: The existing lines for stdlib.t27 and ternary_memory.t27 MUST remain unchanged.

Success Criteria

• Running tools/check_verilog_widths.py exits 0 with no "NEW" lines for big_frame.t27.
• The file tools/verilog_width_baseline.txt contains exactly one line mentioning specs/tri/t27b/conformance/big_frame.t27 with widths 4799999,9599999 and the arithmetic shown.