fix: extract inclusive for-loop ranges with their final iteration

[asterite]

Hi! I'm continuing the work in noir-lang/sha256#59 and I found that inclusive ranges (..=) didn't work well in Lampe, so this is a PR to fix that.

Below is the description that Claude created for the PR.

Problem

The extractor ignores the inclusive flag on HirForStatement (and the monomorphized ast::For), so a Noir loop

for i in start..=end { ... }

is emitted as the half-open Lean loop for i in start .. end, silently dropping the final iteration for every inclusive loop.

This makes the Lean model diverge from the program's real semantics in both directions:

• If the dropped iteration performs an assert, the model is weaker than the circuit, so correctness specs against a reference become unprovable — and one could wrongly conclude a circuit under-constrains a value.
• If the dropped iteration mutates state, the model computes a different value than the real program, so theorems proven about the model don't transfer to the circuit.

We found this while formally verifying noir-lang/sha256: its build_msg_block uses for k in msg_start..=msg_end, where the final iteration carries the assert_eq constraining the last word of the message block. In the extracted model that word was never constrained, making the block-correctness spec unprovable.

Fix

When fors.inclusive is set, emit end + 1 (an add of the numeric literal 1 at the loop-index type) as the loop's upper bound. This mirrors the rewrite Noir's own SSA generation performs for constant bounds below the type's maximum (see codegen_for in noirc_evaluator/src/ssa/ssa_gen/mod.rs).

Known caveat: end at the type's maximum

When end is the maximum value of the index type, end + 1 overflows; the Lampe model treats that as failure, whereas the real program iterates up to and including end (Noir generates a break-based loop for that case rather than computing end + 1). So for that corner the model considers executions failing that really succeed, and STHoare triples about them hold vacuously.

Modelling this faithfully would require either an inclusive-loop primitive in the Omni semantics or desugaring to an exclusive loop plus a guarded trailing iteration (if start ≤ end { body(end) }), both of which are heavier changes with proof-ergonomics implications. Given the status quo drops an iteration from every inclusive loop, this PR takes the simple fix and documents the divergence at the emission site — happy to follow up with the faithful treatment if you have a preference between the two.

Testing

• Added inclusive_range.nr to ExtractionTests with its extracted golden showing the end + 1 bound.
• Downstream validation: with this fix, noir-lang/sha256's build_msg_block spec (including the final word's constraint) is fully provable against the extraction; without it, it is not.

🤖 Generated with Claude Code