WHIR verifier protocol audit + VM/arena memory safety

[XC0R]

Summary

• WHIR verifier audit: 12 tests validating verify.rs against ACFY24 (eprint 2024/1586) Construction 5.1 and Theorem 5.2. Each test cites the specific paper section it validates.
• Arena OOB hardening ([H-3] Unchecked arena index enables out-of-bounds reads #170): bounds-check get_node before read_unaligned, assert alloc_node index fits u32. 5 tests.
• Address overflow hardening ([M-4] Unchecked fp+offset overflow enables wrong memory access #176): checked_add in MemOrConstant, MemOrFpOrConstant, Deref instruction, and hint execution (6 sites). New AddressOverflow error variant. 10 tests.

Verifier audit coverage

Test	Paper reference
completeness_simple_evaluation_constraint	Construction 5.1 completeness
completeness_multiple_evaluation_constraints	§5.2 Construction 5.5 (batching)
soundness_wrong_evaluation_rejected	Theorem 5.2 (soundness)
error_budget_johnson_bound_parameters	Theorem 5.2 error bounds
expand_from_univariate_matches_pow_definition	§3 pow(x, m) notation
folding_definition_consistency	§4.3 Definition 4.14
univariate_horner_matches_multilinear_on_evals_to_coeffs_output	evals_to_coeffs bit-reversal convention
folded_domain_generator_order	Construction 5.1 step 2d
combination_weights_start_from_one	Convention vs Construction 5.1 step 2e
sumcheck_degree_correct_for_eq_weight	Construction 5.1 degree d = max{d*, 3}
security_assumptions_distance_parameters	§6.2 (UD/JB/CB δ)
ood_error_formula_matches_lemma_4_25	Lemma 4.25 (OOD error)

The proximity gap computation (JohnsonBound) was also verified term-by-term against BCSS25 Theorem 1.5 (eprint 2025/2055, equation 1).

Address overflow scope

checked_add applied at every site where bytecode/hint-derived offsets compute memory addresses:

• MemOrConstant::read_value, memory_address
• MemOrFpOrConstant::read_value (MemoryAfterFp + FpRelative), memory_address
• Instruction::Deref — both fp + shift_0 and ptr + shift_1
• Hint::RequestMemory, Inverse, DerefHint, HintWitness (Inline + Indirect)

Closes #170, closes #176.