A041 DuplicateLocalName

CHANGELOG.md

@@ -373,6 +373,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   element has no enclosing variable name and panicked codegen. Distinct from A028
   (whole-array `@`), and also covers a nested-array element such as the outer `@` in
   `[@, [1, 2]]`. The array-element sibling of #225's struct-literal-field fix ([#225])
+- A041 `DuplicateLocalName`: reject duplicate function-local names across disjoint
+  sibling blocks (if/else arms, sequential ifs, non-det blocks) with a two-location
+  diagnostic instead of panicking in codegen ([#217])
 
 ### AST
 
@@ -861,3 +864,4 @@ Initial tagged release.
 [#224]: https://github.com/Inferara/inference/issues/224
 [#225]: https://github.com/Inferara/inference/issues/225
 [#227]: https://github.com/Inferara/inference/issues/227
+[#217]: https://github.com/Inferara/inference/issues/217

core/analysis/README.md

@@ -131,6 +131,14 @@ A037 is the static half of array bounds checking. When the index is a constant i
 
 A compound (struct or array) `@` is lowered by writing into a *named* frame slot, which only a `let`/`const` binding supplies, so `@` of such a type is rejected wherever no slot exists. These complement A014 (array `@` as a function argument) and A027/A028 (whole-binding compound `@`). A scalar or enum `@` is unaffected: the type checker threads it its declared field/element type, so it lowers to a single uzumaki opcode. Array-literal arguments are handled separately by A012, so these rules do not extend to that position.
 
+### Duplicate Local Names (errors)
+
+| ID | Struct | Severity | What it checks |
+|----|--------|----------|----------------|
+| A041 | `DuplicateLocalName` | error | a function-local name (`let`/`const`) declared more than once per function body; well-typed across disjoint sibling blocks but collides in the flat WebAssembly local namespace — rename or hoist a single declaration |
+
+A041 rejects a function-local name introduced more than once in a single function body, even when the two declarations sit in disjoint sibling blocks (`if`/`else` arms, sequential `if`s, `loop` bodies, or non-deterministic blocks) and are individually well-typed — the type checker's scope-based shadowing check never flags them, since sibling scopes never coexist. The conflict surfaces one phase later: `core/wasm-codegen` flattens every body local into a single name-keyed WebAssembly local namespace, so two sibling declarations of the same name would otherwise collide. This is a simplicity and auditability rule, not a proof-soundness requirement — the Rocq translation addresses locals by numeric index, so the flat namespace exists only to preserve a 1:1 mapping between source name, WASM local, and proof index for humans reading traces and proofs. The diagnostic cites both declaration sites and suggests renaming one of them or hoisting a single declaration above the blocks.
+
 ## Diagnostic Output Format
 
 ```
@@ -231,6 +239,7 @@ Test files are organized by rule group:
 | `rules_a038.rs` | A038 (uzumaki on compound struct field) |
 | `rules_a039.rs` | A039 (struct uzumaki passed as function argument) |
 | `rules_a040.rs` | A040 (uzumaki as compound element of an array literal) |
+| `rules_a041.rs` | A041 (duplicate function-local name across sibling blocks) |
 | `walker_tests.rs` | `walk_function_bodies`, `WalkContext` depth tracking |
 
 ## Dependencies

core/analysis/src/errors.rs

@@ -209,6 +209,13 @@ pub enum AnalysisDiagnostic {
         length: u32,
         location: Location,
     },
+
+    #[error("local `{name}` is already declared in this function (first declaration at {first_location}); each local name is introduced once per function body — rename one of them or hoist a single declaration above the blocks")]
+    DuplicateLocalName {
+        name: String,
+        location: Location,
+        first_location: Location,
+    },
 }
 
 impl AnalysisDiagnostic {
@@ -252,7 +259,8 @@ impl AnalysisDiagnostic {
             | AnalysisDiagnostic::VisibilityInsideSpec { location, .. }
             | AnalysisDiagnostic::RecursionDetected { location, .. }
             | AnalysisDiagnostic::StackDepthExceeded { location, .. }
-            | AnalysisDiagnostic::ArrayIndexConstOutOfBounds { location, .. } => location,
+            | AnalysisDiagnostic::ArrayIndexConstOutOfBounds { location, .. }
+            | AnalysisDiagnostic::DuplicateLocalName { location, .. } => location,
         }
     }
 
@@ -300,6 +308,7 @@ impl AnalysisDiagnostic {
             AnalysisDiagnostic::UzumakiOnCompoundField { .. } => "A038",
             AnalysisDiagnostic::StructUzumakiAsArgument { .. } => "A039",
             AnalysisDiagnostic::UzumakiOnCompoundArrayElement { .. } => "A040",
+            AnalysisDiagnostic::DuplicateLocalName { .. } => "A041",
         }
     }
 }
@@ -1197,6 +1206,41 @@ mod tests {
         assert_eq!(err.rule_id(), "A040");
     }
 
+    #[test]
+    fn display_duplicate_local_name() {
+        let first_location = Location {
+            offset_start: 0,
+            offset_end: 5,
+            start_line: 2,
+            start_column: 9,
+            end_line: 2,
+            end_column: 14,
+        };
+        let err = AnalysisDiagnostic::DuplicateLocalName {
+            name: "x".to_string(),
+            location: test_location(),
+            first_location,
+        };
+        let text = err.to_string();
+        assert!(
+            text.contains("local `x` is already declared"),
+            "A041 diagnostic must name the duplicated local, got: {text}"
+        );
+        assert!(
+            text.contains("first declaration at 2:9"),
+            "A041 diagnostic must cite the first declaration's location, got: {text}"
+        );
+        assert!(
+            text.contains("rename one of them or hoist"),
+            "A041 diagnostic must give the rename-or-hoist guidance, got: {text}"
+        );
+        assert!(
+            !text.contains("shadow"),
+            "A041 diagnostic must not use shadowing terminology, got: {text}"
+        );
+        assert_eq!(err.rule_id(), "A041");
+    }
+
     #[test]
     fn partial_eq_for_diagnostic() {
         let a = AnalysisDiagnostic::BreakOutsideLoop {

core/analysis/src/lib.rs

@@ -85,6 +85,15 @@
 //!   `c < 0` or `c >= length`. This is a compile-time check with zero runtime
 //!   cost; dynamic (non-literal) indices are out of scope for this rule.
 //!
+//! ### Duplicate Local Names (A041)
+//!
+//! - A041: A function-local name (`let` or `const`) may be declared at most once
+//!   per function body. Reusing a name across disjoint sibling blocks is well
+//!   typed but collides in the flat WebAssembly local namespace, so it is
+//!   rejected with a rename-or-hoist hint. This is a simplicity and auditability
+//!   rule — it preserves a 1:1 source-name to local to proof-index mapping per
+//!   function — not a proof-soundness requirement.
+//!
 //! ## Pipeline Position
 //!
 //! ```text
@@ -198,6 +207,7 @@ mod tests {
             AnalysisDiagnostic::UzumakiOnCompoundField { field: "i".to_string(), ty: "Inner".to_string(), location: dummy_location() },
             AnalysisDiagnostic::StructUzumakiAsArgument { location: dummy_location() },
             AnalysisDiagnostic::UzumakiOnCompoundArrayElement { ty: "Point".to_string(), location: dummy_location() },
+            AnalysisDiagnostic::DuplicateLocalName { name: "x".to_string(), location: dummy_location(), first_location: dummy_location() },
         ];
 
         let rules = rules::all_rules();

core/analysis/src/rules/duplicate_local_name.rs

@@ -0,0 +1,107 @@
+//! A041: A function-local name is declared at most once per function body.
+//!
+//! Every `let` and `const` binding in a function body shares a single flat
+//! namespace. Two declarations of the same name — even in disjoint sibling
+//! blocks that never coexist at runtime (the two arms of an `if`, two
+//! sequential `if`s, a loop body and a later block, or two non-deterministic
+//! blocks) — are rejected here.
+//!
+//! The type checker treats each lexical block as its own scope, so reusing a
+//! name across sibling blocks is *not* shadowing and it is accepted there. Code
+//! generation, however, flattens every body local into one name-keyed map (one
+//! WebAssembly local per source name), where a repeated name would collide.
+//! This rule enforces the flat-namespace contract as a diagnostic instead of a
+//! codegen crash.
+//!
+//! The rationale is simplicity and auditability, **not** proof soundness: the
+//! Rocq backend addresses locals by numeric index and is unaffected by names,
+//! so either policy yields a sound proof term. What a single flat namespace
+//! buys is a 1:1 source-name to WebAssembly-local to proof-index mapping per
+//! function, which keeps proofs and traces legible to a human reading them.
+//! See issue #217.
+//!
+//! ## Invariant
+//!
+//! A041 must flag *exactly* the body-local duplicates that would trip the
+//! defense-in-depth collision asserts in wasm-codegen's `pre_scan_locals`. The
+//! two walks must agree: if they diverge, either a panic leaks through (A041
+//! misses a duplicate) or legal code is rejected (A041 over-flags). To hold
+//! that agreement, the descent here mirrors `pre_scan_locals`' pre-order DFS —
+//! it recurses through `Stmt::Block`, both arms of `Stmt::If`, and `Stmt::Loop`
+//! bodies, treating `VarDef`/`ConstDef` as leaves. Non-deterministic blocks
+//! (`forall`/`exists`/`unique`/`assume`) surface as `Stmt::Block` carrying a
+//! kind and are descended unconditionally, exactly as codegen descends them.
+//!
+//! Parameters are out of scope: a body local that reuses a parameter name is
+//! already rejected by the type checker (`VariableShadowed`, since parameters
+//! sit in an enclosing scope), and analysis only runs on type-checked programs.
+//! The accumulator is therefore a flat per-body map with no scope tree — it
+//! makes no ancestor/sibling distinction because the type checker has already
+//! removed every ancestor collision.
+
+use inference_ast::arena::AstArena;
+use inference_ast::ids::{IdentId, StmtId};
+use inference_ast::nodes::{Def, Location, Stmt};
+use rustc_hash::FxHashMap;
+
+use crate::{
+    errors::{AnalysisDiagnostic, LabeledDiagnostic},
+    walker,
+};
+
+crate::rule! {
+    /// A function-local name may be declared at most once per function body.
+    #[id = "A041"]
+    #[name = "Duplicate local name"]
+    #[severity = error]
+    pub struct DuplicateLocalName;
+    fn check(ctx: &TypedContext) -> Vec<LabeledDiagnostic> {
+        let mut errors = Vec::new();
+        let arena = ctx.arena();
+        for source_file in ctx.source_files() {
+            let module_path = &source_file.module_path;
+            walker::for_each_function_body(arena, &source_file.defs, &mut |body_id| {
+                // Fresh per body: names in different functions never interact.
+                let mut first_seen: FxHashMap<String, Location> = FxHashMap::default();
+                walker::walk_block_stmts(arena, body_id, &mut |stmt_id| {
+                    let Some((name_id, location)) = local_declaration(arena, stmt_id) else {
+                        return;
+                    };
+                    let name = arena[name_id].name.clone();
+                    if let Some(&first_location) = first_seen.get(&name) {
+                        errors.push(LabeledDiagnostic::new(
+                            module_path.clone(),
+                            AnalysisDiagnostic::DuplicateLocalName {
+                                name,
+                                location,
+                                first_location,
+                            },
+                        ));
+                    } else {
+                        first_seen.insert(name, location);
+                    }
+                });
+            });
+        }
+        errors
+    }
+}
+
+/// The declared name and the statement's own location for a `let` or `const`
+/// statement, or `None` for any other statement.
+///
+/// Both arms cite `arena[stmt_id].location` so the caret points at the whole
+/// statement uniformly — for a `ConstDef` this is the statement's location, not
+/// the inner `Def::Constant` node's.
+#[must_use = "the extracted declaration drives duplicate detection"]
+fn local_declaration(arena: &AstArena, stmt_id: StmtId) -> Option<(IdentId, Location)> {
+    let location = arena[stmt_id].location;
+    match &arena[stmt_id].kind {
+        Stmt::VarDef { name, .. } => Some((*name, location)),
+        Stmt::ConstDef(def_id) => match &arena[*def_id].kind {
+            Def::Constant { name, .. } => Some((*name, location)),
+            _ => None,
+        },
+        _ => None,
+    }
+}

core/analysis/src/rules/mod.rs

@@ -10,6 +10,7 @@ pub mod compound_literal_position;
 pub mod compound_return_call_assignment;
 pub mod compound_return_call_position;
 pub mod dead_code;
+pub mod duplicate_local_name;
 pub mod empty_enum_definition;
 pub mod empty_struct_definition;
 pub mod extern_function_call;
@@ -48,6 +49,7 @@ use compound_literal_position::CompoundLiteralPosition;
 use compound_return_call_assignment::CompoundReturnCallAssignment;
 use compound_return_call_position::CompoundReturnCallPosition;
 use dead_code::DeadCode;
+use duplicate_local_name::DuplicateLocalName;
 use empty_enum_definition::EmptyEnumDefinition;
 use empty_struct_definition::EmptyStructDefinition;
 use extern_function_call::ExternFunctionCall;
@@ -120,5 +122,6 @@ pub fn all_rules() -> &'static [&'static dyn crate::rule::Rule] {
         &UzumakiOnCompoundField,
         &StructUzumakiAsArgument,
         &UzumakiOnCompoundArrayElement,
+        &DuplicateLocalName,
     ]
 }

core/wasm-codegen/docs/local-variables-lowering.md

@@ -80,7 +80,9 @@ The pre-scan intentionally flattens all nested scopes into a single WASM local p
 local declared inside a `forall { }` block, an `if` arm, an `else` arm, or a `loop` body
 shares the same pool as one declared at the top of the function. This is consistent with
 how WebAssembly defines locals: they are function-scoped, not block-scoped. The Inference
-type-checker is responsible for enforcing lexical scoping rules at the language level.
+type-checker enforces lexical scoping for nested (ancestor) shadowing; analysis rule A041
+additionally rejects a name declared more than once across disjoint sibling blocks, since
+such names are individually well-typed but would otherwise collide in this flat pool.
 
 ## Supported Initializer Expression Kinds
 

core/wasm-codegen/src/compiler.rs

@@ -1366,7 +1366,8 @@ impl Compiler {
                         assert!(
                             prev.is_none(),
                             "local `{const_name}` collides with an existing entry in locals_map; \
-                             the type-checker should have rejected shadowing",
+                             analysis rule A041 rejects duplicate function-local names before codegen \
+                             (each name maps to exactly one WebAssembly local)",
                         );
                         *local_idx += 1;
                     }
@@ -1386,7 +1387,8 @@ impl Compiler {
                     assert!(
                         prev.is_none(),
                         "local `{var_name}` collides with an existing entry in locals_map; \
-                         the type-checker should have rejected shadowing",
+                         analysis rule A041 rejects duplicate function-local names before codegen \
+                         (each name maps to exactly one WebAssembly local)",
                     );
                     *local_idx += 1;
                 }
@@ -1682,7 +1684,13 @@ impl Compiler {
                     element_layout,
                 };
                 let binding_name = arena[name_id].name.clone();
-                array_offsets.insert(binding_name, slot);
+                let prev = array_offsets.insert(binding_name.clone(), slot);
+                assert!(
+                    prev.is_none(),
+                    "array local `{binding_name}` collides with an existing frame slot; \
+                     analysis rule A041 rejects duplicate function-local names before codegen \
+                     (each name maps to exactly one frame slot)",
+                );
                 *current_offset = aligned_offset.checked_add(byte_count).expect(
                     "Frame offset overflow: total array allocation exceeds u32::MAX",
                 );
@@ -1719,7 +1727,13 @@ impl Compiler {
                             fields: field_slots,
                         };
                         let binding_name = arena[name_id].name.clone();
-                        struct_offsets.insert(binding_name, slot);
+                        let prev = struct_offsets.insert(binding_name.clone(), slot);
+                        assert!(
+                            prev.is_none(),
+                            "struct local `{binding_name}` collides with an existing frame slot; \
+                             analysis rule A041 rejects duplicate function-local names before codegen \
+                             (each name maps to exactly one frame slot)",
+                        );
                         *current_offset = aligned_offset.checked_add(total_size).expect(
                             "Frame offset overflow: struct allocation exceeds u32::MAX",
                         );

tests/src/analysis/mod.rs

@@ -16,4 +16,5 @@ mod rules_a037;
 mod rules_a038;
 mod rules_a039;
 mod rules_a040;
+mod rules_a041;
 mod walker_tests;