Call elimination: requires violation diagnostic should point to call site (#741)

Fixes #531

## Problem

During call elimination, the generated asserts for `requires`
preconditions used only the call site metadata (`md`), discarding the
requires clause's own metadata. This meant origin-based labels and the
requires clause's file range were lost, producing generic diagnostic
names like `callElimAssert_requires_0_4` and no link back to the
original requires clause location.

## Fix

In `createAsserts` and `createAssumes`, use
`check.md.setCallSiteFileRange md` instead of `md` alone. This:
- Preserves the requires/ensures clause's metadata (including origin
labels) as the base
- Sets the call site as the primary file range (which was already the
reported location)
- Adds the original clause file range as a related file range for richer
SARIF diagnostics

## Testing

All existing tests pass. The correctness proofs (`CallElimCorrect`)
compile without changes. A SARIF output test verifies that related
locations are emitted correctly.

Author: MikaelMayer

Strata/Transform/CoreTransform.lean

@@ -254,7 +254,10 @@ def createAsserts
     := conds.mapM (fun (l, check) => do
           let newLabel ← genIdent l (fun s => s!"{labelPrefix}{s}")
           -- Non-lifting: the replacement expressions must be closed (no dangling bvars).
-          return Statement.assert newLabel.toPretty (Lambda.LExpr.substFvars check.expr subst) md)
+          -- Use the call site as the primary file range, preserving the requires
+          -- clause location as a related file range for richer diagnostics.
+          let assertMd := check.md.setCallSiteFileRange md
+          return Statement.assert newLabel.toPretty (Lambda.LExpr.substFvars check.expr subst) assertMd)
 
 /-- turns a list of preconditions into assumes with substitution -/
 def createAssumes
@@ -267,7 +270,10 @@ def createAssumes
     conds.mapM (fun (l, check) => do
       let newLabel ← genIdent l (fun s => s!"{labelPrefix}{s}")
       -- Non-lifting: the replacement expressions must be closed (no dangling bvars).
-      return Statement.assume newLabel.toPretty (Lambda.LExpr.substFvars check.expr subst) md)
+      -- Use the call site as the primary file range, preserving the ensures
+      -- clause location as a related file range for richer diagnostics.
+      let assumeMd := check.md.setCallSiteFileRange md
+      return Statement.assume newLabel.toPretty (Lambda.LExpr.substFvars check.expr subst) assumeMd)
 
 /--
 Generate the substitution pairs needed for the body of the procedure

StrataTest/Languages/Python/expected_laurel/test_class_methods.expected

@@ -5,9 +5,9 @@ test_class_methods.py(24, 4): ✅ pass - assert_assert(539)_calls_Any_to_bool_0
 test_class_methods.py(24, 4): ❓ unknown - assert(539)
 test_class_methods.py(28, 4): ✅ pass - assert_assert(654)_calls_Any_to_bool_0
 test_class_methods.py(28, 4): ❓ unknown - assert(654)
-test_class_methods.py(30, 4): ✅ pass - callElimAssert_requires_0_4
-test_class_methods.py(30, 4): ✅ pass - callElimAssert_requires_1_5
-test_class_methods.py(30, 4): ✅ pass - callElimAssert_requires_2_6
+test_class_methods.py(30, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_class_methods.py(30, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_class_methods.py(30, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_methods.py(17, 0): ✅ pass - postcondition
 test_class_methods.py(32, 0): ✅ pass - ite_cond_calls_Any_to_bool_0
 DETAIL: 9 passed, 0 failed, 3 inconclusive

StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected

@@ -3,9 +3,9 @@ test_class_with_methods.py(23, 4): ✅ pass - assert_assert(459)_calls_Any_to_bo
 test_class_with_methods.py(23, 4): ❓ unknown - assert(459)
 test_class_with_methods.py(26, 4): ✅ pass - assert_assert(544)_calls_Any_to_bool_0
 test_class_with_methods.py(26, 4): ❓ unknown - assert(544)
-test_class_with_methods.py(28, 4): ✅ pass - callElimAssert_requires_0_4
-test_class_with_methods.py(28, 4): ✅ pass - callElimAssert_requires_1_5
-test_class_with_methods.py(28, 4): ✅ pass - callElimAssert_requires_2_6
+test_class_with_methods.py(28, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_class_with_methods.py(28, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_class_with_methods.py(28, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_with_methods.py(17, 0): ✅ pass - postcondition
 test_class_with_methods.py(30, 0): ✅ pass - ite_cond_calls_Any_to_bool_0
 DETAIL: 8 passed, 0 failed, 2 inconclusive

StrataTest/Languages/Python/expected_laurel/test_datetime.expected

@@ -1,8 +1,8 @@
-test_datetime.py(13, 0): ✅ pass - callElimAssert_requires_12
-test_datetime.py(14, 0): ✅ pass - callElimAssert_requires_0_4
-test_datetime.py(14, 0): ✅ pass - callElimAssert_requires_1_5
-test_datetime.py(14, 0): ✅ pass - callElimAssert_requires_2_6
-test_datetime.py(14, 0): ✅ pass - callElimAssert_requires_3_7
+test_datetime.py(13, 0): ✅ pass - (Origin_datetime_date_Requires)d_type
+test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)
+test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_type
+test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)days_pos
+test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos
 test_datetime.py(21, 0): ✅ pass - assert_assert(554)_calls_Any_to_bool_0
 test_datetime.py(21, 0): ✅ pass - assert(554)
 test_datetime.py(25, 0): ✅ pass - assert_assert(673)_calls_Any_to_bool_0

StrataTest/Languages/Python/expected_laurel/test_default_params.expected

@@ -2,20 +2,20 @@ unknown location: ✅ pass - (greet ensures) Return type constraint
 test_default_params.py(8, 4): ✅ pass - loop_guard_calls_Any_to_bool_0
 test_default_params.py(8, 4): ✅ pass - loop_guard_end_calls_Any_to_bool_0
 unknown location: ❓ unknown - (power ensures) Return type constraint
-test_default_params.py(14, 4): ✅ pass - callElimAssert_requires_0_21
-test_default_params.py(14, 4): ✅ pass - callElimAssert_requires_1_22
+test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of name
+test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of greeting
 test_default_params.py(15, 4): ✅ pass - assert_assert(325)_calls_Any_to_bool_0
 test_default_params.py(15, 4): ❓ unknown - assert(325)
-test_default_params.py(17, 4): ✅ pass - callElimAssert_requires_0_15
-test_default_params.py(17, 4): ✅ pass - callElimAssert_requires_1_16
+test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of name
+test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of greeting
 test_default_params.py(18, 4): ✅ pass - assert_assert(421)_calls_Any_to_bool_0
 test_default_params.py(18, 4): ❓ unknown - assert(421)
-test_default_params.py(20, 4): ✅ pass - callElimAssert_requires_0_9
-test_default_params.py(20, 4): ✅ pass - callElimAssert_requires_1_10
+test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of base
+test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of exp
 test_default_params.py(21, 4): ✅ pass - assert_assert(501)_calls_Any_to_bool_0
 test_default_params.py(21, 4): ❓ unknown - assert(501)
-test_default_params.py(23, 4): ✅ pass - callElimAssert_requires_0_3
-test_default_params.py(23, 4): ✅ pass - callElimAssert_requires_1_4
+test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of base
+test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of exp
 test_default_params.py(24, 4): ✅ pass - assert_assert(571)_calls_Any_to_bool_0
 test_default_params.py(24, 4): ❓ unknown - assert(571)
 test_default_params.py(26, 0): ✅ pass - ite_cond_calls_Any_to_bool_0

StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected

@@ -5,12 +5,12 @@ unknown location: ✅ pass - (Sum ensures) Return type constraint
 unknown location: ❓ unknown - set_LaurelResult_calls_Any_get_0
 unknown location: ❓ unknown - set_LaurelResult_calls_Any_get_1
 unknown location: ❓ unknown - (List_Dict_index ensures) Return type constraint
-test_func_input_type_constraints.py(15, 0): ✅ pass - callElimAssert_requires_0_17
-test_func_input_type_constraints.py(15, 0): ✅ pass - callElimAssert_requires_1_18
-test_func_input_type_constraints.py(16, 0): ✅ pass - callElimAssert_requires_0_11
-test_func_input_type_constraints.py(16, 0): ✅ pass - callElimAssert_requires_1_12
-test_func_input_type_constraints.py(17, 0): ✅ pass - callElimAssert_requires_0_4
-test_func_input_type_constraints.py(17, 0): ✅ pass - callElimAssert_requires_1_5
-test_func_input_type_constraints.py(17, 0): ✅ pass - callElimAssert_requires_2_6
+test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of x
+test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of y
+test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of x
+test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of y
+test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of l
+test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of i
+test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of s
 DETAIL: 11 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive

StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected

@@ -1,7 +1,7 @@
-test_function_def_calls.py(6, 4): ❓ unknown - callElimAssert_requires_0_4
-test_function_def_calls.py(6, 4): ✅ pass - callElimAssert_requires_1_5
-test_function_def_calls.py(6, 4): ✅ pass - callElimAssert_requires_2_6
-test_function_def_calls.py(9, 4): ✅ pass - callElimAssert_requires_10
+test_function_def_calls.py(6, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_function_def_calls.py(9, 4): ✅ pass - (my_f requires) Type constraint of s
 test_function_def_calls.py(11, 0): ✅ pass - ite_cond_calls_Any_to_bool_0
 DETAIL: 4 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive

StrataTest/Languages/Python/expected_laurel/test_if_elif.expected

@@ -5,16 +5,16 @@ unknown location: ✅ pass - (classify ensures) Return type constraint
 test_if_elif.py(6, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
 unknown location: ✅ pass - (classify ensures) Return type constraint
 unknown location: ✅ pass - (classify ensures) Return type constraint
-test_if_elif.py(12, 4): ✅ pass - callElimAssert_requires_14
+test_if_elif.py(12, 4): ✅ pass - (classify requires) Type constraint of x
 test_if_elif.py(13, 4): ✅ pass - assert_assert(225)_calls_Any_to_bool_0
 test_if_elif.py(13, 4): ❓ unknown - assert(225)
-test_if_elif.py(15, 4): ✅ pass - callElimAssert_requires_10
+test_if_elif.py(15, 4): ✅ pass - (classify requires) Type constraint of x
 test_if_elif.py(16, 4): ✅ pass - assert_assert(302)_calls_Any_to_bool_0
 test_if_elif.py(16, 4): ❓ unknown - assert(302)
-test_if_elif.py(18, 4): ✅ pass - callElimAssert_requires_6
+test_if_elif.py(18, 4): ✅ pass - (classify requires) Type constraint of x
 test_if_elif.py(19, 4): ✅ pass - assert_assert(371)_calls_Any_to_bool_0
 test_if_elif.py(19, 4): ❓ unknown - assert(371)
-test_if_elif.py(21, 4): ✅ pass - callElimAssert_requires_2
+test_if_elif.py(21, 4): ✅ pass - (classify requires) Type constraint of x
 test_if_elif.py(22, 4): ✅ pass - assert_assert(444)_calls_Any_to_bool_0
 test_if_elif.py(22, 4): ❓ unknown - assert(444)
 test_if_elif.py(24, 0): ✅ pass - ite_cond_calls_Any_to_bool_0

StrataTest/Languages/Python/expected_laurel/test_missing_models.expected

@@ -1,7 +1,7 @@
 test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_0
 test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_1
-test_missing_models.py(9, 4): ❓ unknown - callElimAssert_requires_0_22
-test_missing_models.py(9, 4): ✅ pass - callElimAssert_requires_1_23
-test_missing_models.py(9, 4): ✅ pass - callElimAssert_requires_2_24
+test_missing_models.py(9, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 DETAIL: 2 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive

StrataTest/Languages/Python/expected_laurel/test_multi_function.expected

@@ -6,18 +6,18 @@ test_multi_function.py(11, 4): ✅ pass - ite_cond_calls_PNotIn_0
 test_multi_function.py(11, 4): ✅ pass - ite_cond_calls_Any_to_bool_1
 unknown location: ✅ pass - (validate_config ensures) Return type constraint
 unknown location: ✅ pass - (validate_config ensures) Return type constraint
-test_multi_function.py(16, 4): ✅ pass - callElimAssert_requires_0_7
-test_multi_function.py(16, 4): ✅ pass - callElimAssert_requires_1_8
-test_multi_function.py(17, 4): ✅ pass - callElimAssert_requires_2
+test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of name
+test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of value
+test_multi_function.py(17, 4): ✅ pass - (validate_config requires) Type constraint of config
 test_multi_function.py(18, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
 unknown location: ❓ unknown - set_LaurelResult_calls_Any_get_0
-test_multi_function.py(23, 4): ✅ pass - callElimAssert_requires_0_21
-test_multi_function.py(23, 4): ✅ pass - callElimAssert_requires_1_22
+test_multi_function.py(23, 4): ✅ pass - (process_config requires) Type constraint of name
+test_multi_function.py(23, 4): ✅ pass - (process_config requires) Type constraint of value
 test_multi_function.py(24, 4): ✅ pass - assert_assert(651)_calls_Any_to_bool_0
 test_multi_function.py(24, 4): ❓ unknown - assert(651)
-test_multi_function.py(26, 4): ✅ pass - callElimAssert_requires_0_14
-test_multi_function.py(26, 4): ✅ pass - callElimAssert_requires_1_15
-test_multi_function.py(26, 4): ✅ pass - callElimAssert_requires_2_16
+test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_multi_function.py(28, 0): ✅ pass - ite_cond_calls_Any_to_bool_0
 DETAIL: 19 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive