CP-TRANSLATION-SCOPE - A translation works on test inputs; which executions does it preserve?

• Situation: Expressions have been translated to a machine with different arithmetic, and a few successful tests do not settle the permitted input range.
• Question: Under which input conditions does the translated program preserve the required result?
• First useful result or blocker: A source-to-target correspondence with an established input condition, or a concrete mismatch or unresolved condition preventing that claim.
• Start with: CMP.12 - Construct an Interpreter or a Meaning-Preserving Translation. If the correspondence depends on a property of possible executions, use CMP.13 - Construct a Computational Abstraction for the Property Being Asked to obtain that premise.
• Stop or return: Use a sufficient correspondence on its established scope. Changed inputs or machine operations reopen the affected premise. An abstract warning alone is not a demonstrated failing execution.

For example, the source computes (x + 1) * (x - 2) with unbounded integers. The target uses unsigned 8-bit arithmetic, wrapping modulo 256. CMP.12 specifies evaluation and translation: evaluate each operand in order, pop the right operand before the left, and append the expression’s result without changing an existing stack prefix. At x = 5, both executions produce 18. That test does not establish correspondence for other inputs.

Suppose the allowed integers satisfy 2 <= x <= 16. CMP.13 can compute ranges at the expression’s intermediate steps: x + 1 lies in [3,17], x - 2 in [0,14], and their product in [0,238]. These ranges cover every source execution under the stated input condition. No arithmetic intermediate overflows the target range. This discharges the arithmetic premise of CMP.12’s correspondence argument; it does not replace the argument about operand order and preservation of the stack.

Now allow x = 17. The source returns 270 and the target 14. The changed range calculation warns that wrapping is possible; this concrete execution establishes an actual mismatch. Return to CMP.12 to choose wider arithmetic, retain a justified input restriction, or explicitly change the intended arithmetic. Do not “repair” the analyzer by removing a real input. For a different abstract warning, CMP.13 checks the proposed execution against the original computation. If reconstruction establishes that a lost distinction produced an impossible path, refine that distinction; failure to resolve a path is not proof that it is impossible.

The same connection can supply a premise about control, binding, errors or effects, but it needs an abstraction for that property and the actual execution rules. A range argument establishes none of those other properties by itself. The direct patterns give those constructions beyond this arithmetic example.