From 2d06ab1c5a71bc0bfac6dc09613e07e64be01708 Mon Sep 17 00:00:00 2001 From: Ary Borenszweig Date: Mon, 27 Jul 2026 18:44:35 -0300 Subject: [PATCH] fix: extract inclusive for-loop ranges with their final iteration MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The extractor ignored the `inclusive` flag on `HirForStatement`, so a Noir loop `for i in start..=end` was emitted as the half-open Lean loop `for i in start .. end`, silently dropping the final iteration. Any assert or state mutation in that iteration was absent from the model, making it diverge from the program's real semantics (found while verifying noir-lang/sha256, where the dropped iteration carried the assert constraining the last word of a message block). Emit `end + 1` as the upper bound when the range is inclusive, mirroring the rewrite Noir's own SSA generation performs for constant bounds. When `end` is the maximum value of the index type this add overflows and the model treats the execution as failing, whereas the real program iterates through `end` — modelling that corner faithfully would need an inclusive-loop primitive in the semantics; the divergence is documented at the emission site. Co-Authored-By: Claude Fable 5 --- src/lean/generator.rs | 39 ++++++++++++++++++- .../ExtractionTests-0.0.0/Extracted.lean | 2 + .../Extracted/InclusiveRange.lean | 21 ++++++++++ .../ExtractionTests/src/inclusive_range.nr | 9 +++++ testing/ExtractionTests/src/lib.nr | 1 + 5 files changed, 71 insertions(+), 1 deletion(-) create mode 100644 testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean create mode 100644 testing/ExtractionTests/src/inclusive_range.nr diff --git a/src/lean/generator.rs b/src/lean/generator.rs index 3a38bf85..f6d44c72 100644 --- a/src/lean/generator.rs +++ b/src/lean/generator.rs @@ -3252,7 +3252,44 @@ impl LeanGenerator<'_, '_, '_> { sanitize_variable_name(self.context.def_interner.definition_name(fors.identifier.id)); let start_range = Box::new(self.generate_expr(fors.start_range, out)); - let end_range = Box::new(self.generate_expr(fors.end_range, out)); + let end_range = self.generate_expr(fors.end_range, out); + // Noir's `start..=end` ranges are inclusive, while the Lean loop is + // half-open, so an inclusive upper bound becomes `end + 1`. 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`). + // + // Note: when `end` is the maximum value of the index type, `end + 1` + // overflows, which the Lampe model treats as failure, whereas the real + // program iterates up to and including `end` (Noir generates a + // `break`-based loop for that case). Modelling that faithfully would + // require an inclusive-loop primitive in the Lean semantics; until + // then this diverges for that corner case. + let end_range = if fors.inclusive { + let bound_ty_noir = self.resolve_bound_type(fors.end_range); + let bound_type = self.generate_lean_type_value(&bound_ty_noir, None); + let builtin_ty = self + .unfold_alias(bound_ty_noir) + .try_into() + .ok() + .expect("Inclusive for-loop bound is not a builtin integer type"); + let builtin_name = + builtin::try_infix_into_builtin_name(BinaryOpKind::Add, builtin_ty, builtin_ty) + .expect("Inclusive for-loop bound type does not support addition"); + let one = Expression::Literal(Literal::Numeric(NumericLiteral { + value: "1".to_string(), + typ: bound_type.clone(), + })); + let add_target = Expression::builtin_call_ref(builtin_name.as_str(), &bound_type); + Expression::Call(Call { + function: Box::new(add_target), + params: vec![end_range, one], + return_type: bound_type, + }) + } else { + end_range + }; + let end_range = Box::new(end_range); let mut body_prologue = vec![]; let body = self.generate_expr(fors.block, &mut body_prologue); let body = Box::new(wrap_in_block_if_needed(body_prologue, body)); diff --git a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean index 5fa7f832..db3cf17b 100644 --- a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean +++ b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean @@ -11,6 +11,7 @@ import «ExtractionTests-0.0.0».Extracted.Experiments import «ExtractionTests-0.0.0».Extracted.FieldGenerics import «ExtractionTests-0.0.0».Extracted.GeneratedTypes import «ExtractionTests-0.0.0».Extracted.ImplTraitReturn +import «ExtractionTests-0.0.0».Extracted.InclusiveRange import «ExtractionTests-0.0.0».Extracted.Lib import «ExtractionTests-0.0.0».Extracted.MultipleGenerics import «ExtractionTests-0.0.0».Extracted.NestedMemberAccess @@ -39,6 +40,7 @@ def env := AliasMemberAccess.env ++ Experiments.env ++ FieldGenerics.env ++ ImplTraitReturn.env + ++ InclusiveRange.env ++ Lib.env ++ MultipleGenerics.env ++ NestedMemberAccess.env diff --git a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean new file mode 100644 index 00000000..1642930e --- /dev/null +++ b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean @@ -0,0 +1,21 @@ +-- Generated by lampe + +import «ExtractionTests-0.0.0».Extracted.GeneratedTypes +import Lampe + +open Lampe + +set_option linter.unusedVariables false + +noir_def «ExtractionTests-0.0.0»::inclusive_range::sum_inclusive<>(n: u32) -> u32 := { + let sum = (#_ref returning & u32)((0: u32)); + for i in (0: u32) .. (#_uAdd returning u32)(n, (1: u32)) do { + sum = (#_uAdd returning u32)((#_readRef returning u32)(sum), i); + #_skip + }; + (#_readRef returning u32)(sum) +} + +def «ExtractionTests-0.0.0».InclusiveRange.env : Env := Env.mk + [«ExtractionTests-0.0.0::inclusive_range::sum_inclusive»] + [] diff --git a/testing/ExtractionTests/src/inclusive_range.nr b/testing/ExtractionTests/src/inclusive_range.nr new file mode 100644 index 00000000..b259ccb9 --- /dev/null +++ b/testing/ExtractionTests/src/inclusive_range.nr @@ -0,0 +1,9 @@ +// Inclusive ranges (`start..=end`) must extract to a loop that includes the +// final iteration (regression test for the extractor dropping it). +pub fn sum_inclusive(n: u32) -> u32 { + let mut sum = 0; + for i in 0..=n { + sum = sum + i; + } + sum +} diff --git a/testing/ExtractionTests/src/lib.nr b/testing/ExtractionTests/src/lib.nr index fb5b1572..8bcdde61 100644 --- a/testing/ExtractionTests/src/lib.nr +++ b/testing/ExtractionTests/src/lib.nr @@ -15,6 +15,7 @@ mod reserved_keywords; mod shadow_mut; mod unit_return; mod bool_neq; +mod inclusive_range; mod ref_member_access; mod array_as_vector; mod impl_trait_return;