refactor(ir): calc lowering moves to lower.ToCalc, the runtime holds a program.Calc

docs/project/spec-compliance/02-detailed-semantic-compliance-map/07-constraint.md

@@ -33,5 +33,5 @@
 | The conditions of a nested constraint (`assert constraint [name] { <expr> }`) are the conditions of the member stating it | `parser/behavior.go` `tryParseNestedConstraint`, `condition.go` `appendConditions` | `parser/behavior_require_member_test.go:TestConstraintMemberNestedBody` | ✅ Faithful |
 | `this` inside an asserted constraint or requirement usage an object's type declares names that object (`Occurrences::Occurrence::this`: the context occurrence, overridden for the owned performances of an object), so a usage typed by a constraint def binds the def's context parameter with `in ref :>> context = this;` and validating the object evaluates the def's result over it; checked about no object (`-constraint` without a subject), the usage reads the type's declared defaults and `this` denotes an exemplar of the type made for the check and abandoned with it | `resolve/this_context.go` `Resolver.ThisContext`, `isBehaviorUsageKind`; `runtime/eval.go` `EvalContext.thisValue`; `runtime/exemplar.go` `Context.exemplarOf` | conformance `instance_validate_constraint_def_context`; `runtime/exemplar_test.go` `TestConstraintAboutNoObjectReadsThisAsExemplar` | ✅ Faithful |
 | A constraint body that declares parameters (`constraint c { in x : Real; assert x >= 0; }`) states conditions like any other, including conditions that start with a keyword (`assert true`, `assert not false`, `assume null != x`, `assert if …`); a condition missing its expression is a diagnostic | `parser/behavior.go` `atConstraintCondition`, `parser/behavior.go` `exprStartKeywords` | `parse/constraint_parameterised_conditions.golden`, `parser/constraint_condition_test.go`, `parser/negative_test.go:constraint_params_assert_no_condition` | ✅ Faithful |
-| A constraint carrying no condition has no value (`ErrNoValue`), neither a verdict nor a vacuous pass: a constraint is a `BooleanEvaluation` whose `result : Boolean[1]` only its body expression binds (KerML 1.1 Beta 2 §7.4.8.2; SysML v2.1 Beta 2 §7.20.2), so with no body nothing binds it — the same unbound-result case a calc with no result expression is, and "no conditions" is not a notion the specification has. The cause stays as the detail (`constraint empty: no value: the constraint declares no condition`; a `return r;` the body never binds carries the calc's hint instead), on every surface that reports a check (REPL, LSP, gRPC `VerifyConstraint`/`VerifyRequirement`, MCP, the solver and `smt` engine, the validation report), and a model-level read of such a constraint's value is undetermined, as any unbound result is. A requirement carrying none is judged by the Requirement rule below instead | `errors.go` `ErrNoValue`, `condition.go` `evaluateConditions`, `conditionCheck.noResultValue`, `conditionCheck.isRequirementCheck`, `invoke_calc.go` `unboundResultHint`, `context.go` `EvaluateConstraintOn`; `solve/translate.go` `requirementSubject`, `Subject.noResultValue`, `unboundConstraintResult` | conformance `condition_less_constraint_def`, `condition_less_constraint_usage`, `read_return_parameters` (`cnegNoCondition`); `runtime/robustness_condition_less_check_test.go`, `runtime/constraint_test.go:TestConstraintWithoutConditionsIsNotAVerdict`, `runtime/owned_constraint_value_test.go:TestOwnedConstraintValueIsNotACondition`, `runtime/robustness_vacuous_requirement_test.go`; `solve/translate_test.go:TestNoConditions`, `solve/asserted_vacuous_test.go` | ✅ Faithful |
+| A constraint carrying no condition has no value (`ErrNoValue`), neither a verdict nor a vacuous pass: a constraint is a `BooleanEvaluation` whose `result : Boolean[1]` only its body expression binds (KerML 1.1 Beta 2 §7.4.8.2; SysML v2.1 Beta 2 §7.20.2), so with no body nothing binds it — the same unbound-result case a calc with no result expression is, and "no conditions" is not a notion the specification has. The cause stays as the detail (`constraint empty: no value: the constraint declares no condition`; a `return r;` the body never binds carries the calc's hint instead), on every surface that reports a check (REPL, LSP, gRPC `VerifyConstraint`/`VerifyRequirement`, MCP, the solver and `smt` engine, the validation report), and a model-level read of such a constraint's value is undetermined, as any unbound result is. A requirement carrying none is judged by the Requirement rule below instead | `errors.go` `ErrNoValue`, `condition.go` `evaluateConditions`, `conditionCheck.noResultValue`, `conditionCheck.isRequirementCheck`, `lower/calc.go` `UnboundResultHint`, `context.go` `EvaluateConstraintOn`; `solve/translate.go` `requirementSubject`, `Subject.noResultValue`, `unboundConstraintResult` | conformance `condition_less_constraint_def`, `condition_less_constraint_usage`, `read_return_parameters` (`cnegNoCondition`); `runtime/robustness_condition_less_check_test.go`, `runtime/constraint_test.go:TestConstraintWithoutConditionsIsNotAVerdict`, `runtime/owned_constraint_value_test.go:TestOwnedConstraintValueIsNotACondition`, `runtime/robustness_vacuous_requirement_test.go`; `solve/translate_test.go:TestNoConditions`, `solve/asserted_vacuous_test.go` | ✅ Faithful |
 | A constraint body's statements (`assign`, `if`, `while`/`loop`/`for` — SysML v2 7.20, whose constraint body is a `CalculationBody`) are steps of one Boolean performance, performed before its conditions are evaluated in the state they left, the ones no `then` between them orders unordered (the library leaves them so; see the unordered-statement row of the action map, which states how `explore`, `-engine check`, replay and seeded runs reach each order); locals live in a fresh frame per check, a body-local `attribute` declared with them is a local too, the constraint's own parameters are copied into the frame so a write binds the copy alone, and `SysML v2 §7.17.9`'s implicit target is the performance itself — so `assign n := …` for a name it holds no feature for (`errConstraintExternalAssignment`) and every effect reaching outside it (a chained or qualified write, `send`, `perform`, `terminate` — `errConstraintEffect`) are refused, as are the stated successions `first`/`fork`/`join`/`merge`/`decide`/`done` and a `then` reaching outside the body (`errStatementNotExecutable`; a `then` between two of the body's own statements orders them), a steps-only body (`ErrNoValue`: nothing binds its result), and a case's own steps, which are its procedure and are not refused | `lower/constraint_body.go` `ConstraintStep`, `condition.go` `appendConditions`/`appendMemberConditions`/`appendOwnedConditions`/`evaluateStepsConditions`/`conditionHoldsAt`, `constraint_statements.go` `constraintStmtHost`/`runConstraintSteps`, `analysis.go` `CaseConditionsOf`, `solve/translate.go` `translator.condition` | `runtime/constraint_test.go:TestConstraintBodyStepsRun`/`TestConstraintBodyPerformIsRefused`/`TestConstraintBodyActionFlowIsRefused`/`TestConstraintBodySuccessionIsRefused`, `runtime/robustness_constraint_body_steps_test.go:TestRuntimeRobustnessConstraintBodySteps`, conformance `constraint_body_steps` + four `constraint_body_steps_*_rejected`, `solve/translate_test.go:TestBodyStatementRefuses`/`TestPerformedActionRefuses`/`TestActionFlowRefuses`, `solve/objective_test.go:TestCaseStepsAreNotBodyStatements` | ⚠️ Approximate (`declared` and `reverse` run the steps in declaration order, a tool-defined linearization, while `explore`, `-engine check`, replay and seeded runs reach every order the library admits; effects outside the performance and stated successions other than `then` between the body's own steps are refused rather than performed) |