@Int.0 + @Int.1 masks slot index errors because addition is commutative — swapping the indices gives the same result. Write conformance tests using subtraction, division, and comparison where swapping @Int.0 and @Int.1 produces a different (wrong) result.
Also write tests where the contract catches the error: a postcondition that would only hold with the correct index ordering. This verifies that the contract system catches the class of bug that the commutative-op tests mask.
@Int.0 + @Int.1masks slot index errors because addition is commutative — swapping the indices gives the same result. Write conformance tests using subtraction, division, and comparison where swapping@Int.0and@Int.1produces a different (wrong) result.Also write tests where the contract catches the error: a postcondition that would only hold with the correct index ordering. This verifies that the contract system catches the class of bug that the commutative-op tests mask.