Fix fib_iterative programs

[gabrielbosio]

Some fib_iterative programs didn't have the halt instruction which caused verification to fail. This PR adds that instruction to the problematic fib_iterative programs.

[github-actions]

Codex Code Review

Findings

1. Low – Comment/code mismatch can mislead correctness assumptions

   • fib_iterative_500k.s:24
   • fib_iterative_2M.s:24
   • These still say “halt with result in a0”, but a0 is now explicitly set to 0 just before ecall ([line 22] in each file). This can cause incorrect expectations for anyone using these as result-returning samples.

2. Low – Redundant instruction / dead write

   • fib_iterative_250k.s:21
   • fib_iterative_500k.s:21
   • fib_iterative_2M.s:21
   • mv a0, t1 is immediately overwritten by li a0, 0; this is dead code and adds confusion. Either remove the mv, or preserve the computed result in another register if it’s needed for debugging/proof traces.

Security

• No security vulnerabilities identified in this diff.

Performance

• No significant performance issues identified in this diff.

[claude]

Review

The core fix is correct: the prover HALT table enforces x10 (a0) == 0 at halt time, so these three programs were failing verification without the 'li a0, 0' before ecall. Good catch.

Two minor issues left to clean up (inline comments added):

• fib_iterative_500k.s and fib_iterative_2M.s: The 'mv a0, t1' is now a dead instruction (immediately overwritten by 'li a0, 0'), and the ecall comment still says 'halt with result in a0' which is now inaccurate. The 250k file in this PR was updated correctly but the other two were not. Suggestions attached.