fix(soundness): range-check HintsTable init limbs (#999)

[spherel]

Problem

HintsTable is the only RAM table with prover-witnessed (non-zero) init
values — it holds the guest's private hint inputs.
DynVolatileRamTableInitConfig::construct_circuit created those init-value
limbs as raw WitIns with no range check, so a malicious prover could
supply non-canonical limbs (>= 2^16).

The load path reads memory via UInt::new_unchecked (e.g. LW in
load_v2.rs) and forwards the limbs to the destination register
unconstrained, so a non-canonical hint word would propagate into the
computation. This is an under-constraint soundness bug: a crafted proof
using out-of-range hint limbs would verify.

Design Rationale

Bind every non-zero-init limb to LIMB_BITS (u16) in construct_circuit,
making each reconstructed hint word a canonical u32 — the same range
discipline every other prover-supplied word in the system already follows.
The fix is on the constraint side (the load-bearing surface for soundness);
per-row addresses are already formula-bound structural witins and the table
base (hint_start_addr) is already range-checked by the verifier's
validate_mem_state, so this closes the one remaining unconstrained axis (the
init value limbs).

A range check is a looking lookup, which the default
TableCircuit::build_gkr_iop_circuit does not wire for table circuits, so the
fix needs three coordinated touches (below). For zero-init tables (heap,
stack) the looking lengths are 0, so all wiring stays byte-for-byte
identical to the current behaviour.

Change Highlights

• ceno_zkvm/tables/ram/ram_impl.rs — range-check every non-zero-init
  limb (assert_ux::<LIMB_BITS>) in construct_circuit; thread an optional
  LkMultiplicity through assign_instances / assign_instances_dynamic so
  the per-limb u16 lookups are recorded. Adds the range check on hint table #999 soundness regression
  test.
• ceno_zkvm/tables/ram/ram_circuit.rs — DynVolatileRamCircuit
  overrides build_gkr_iop_circuit to size the r/w/lk/zero out-eval
  groups with looking + table lengths; adds
  assign_instances_with_lk_multiplicities.
• ceno_zkvm/structs.rs — new ZKVMWitnesses::assign_table_circuit_with_lk
  (mirrors assign_shared_circuit) to fold a table circuit's own lookup
  multiplicity into lk_mlts before finalize.
• ceno_zkvm/instructions/riscv/rv32im/mmu.rs — route HintsInitCircuit
  through assign_table_circuit_with_lk; HeapInitCircuit stays on the plain
  path (zero-init, no lookups).
• ceno_zkvm/e2e.rs — move the dynamic-init-table assignment before
  finalize_lk_multiplicities so the hint range-check lookups land in
  combined_lk_mlt, matching the existing pre-finalize ShardRam ordering
  (main + GPU-debug-compare paths).

Rebased onto current master; merged with #1350's dynamic-init padding guard
so the u16 multiplicity is recorded only for real rows
(i < num_instances && let Some(rec) = rec_opt), consistent with the prefix
selector that gates the range-check constraints.

Benchmark / Performance Impact

Not benchmarked — the change adds only O(hint_words) u16 range-lookups
during witness generation and leaves the verifier's structural shape
unchanged (zero-init tables produce identical circuits). Prover impact is
negligible relative to the per-shard logup it already performs.

Testing

cargo check --workspace --all-targets
cargo make clippy                       # -D warnings
cargo test -p ceno_zkvm tables::ram::ram_impl   # incl. new #999 regression

• New soundness regression test_hint_init_rejects_non_canonical_limb:
  honest (canonical) limbs satisfy every range lookup; forcing any single init
  limb to 2^LIMB_BITS makes the init_v_limb_{i}_in_u16 lookup fall outside
  the u16 table and MockProver rejects the witness. The test fails if the
  range check is removed.
• Real (non-mock) prove + verify of fibonacci with hints, single shard and
  61-shard — the global logup balances including the hint circuit's
  range-check records (a dropped lookup would unbalance the recorded
  multiplicity).
• Integration e2e suite (mirror of .github/workflows/integration.yml); the
  fibonacci --hints MOCK path is confirmed passing on this branch.

Risks and Rollout

• Soundness: strictly tightening — adds a constraint, removes an
  under-constraint. No verifier semantic-contract change.
• Compatibility: zero-init tables (heap/stack) are wired identically; only
  HintsTable gains the lk group.
• Rollback: revert the commit; no migrations or persisted state.

Follow-ups (optional)

• None required for soundness. (Optional defense-in-depth, separate from this
  PR: make the u32 arithmetic in the verifier's validate_mem_state
  hint/heap bound explicit via checked_add/checked_mul.)

Copilot Reviewer Directive (keep this section)

When Copilot reviews this PR, apply .github/copilot-instructions.md strictly.

[hero78119]

LGTM!