Clearly define integer/float overflow and conversion rules

spec/05-types.md

@@ -55,7 +55,7 @@ There is one integer type, `int`, for which the name integer is a synonym.
 This type is binary, signed, and uses twos-complement representation for
 negative values. The range of values that can be stored is
 implementation-defined; however, the range [-2147483648, 2147483647],
-must be supported.
+must be supported. This range must be finite.
 
 Certain operations on integer values produce a mathematical result that
 cannot be represented as an integer. Examples include the following:
@@ -64,16 +64,8 @@ cannot be represented as an integer. Examples include the following:
 -   Applying the unary minus to the smallest value.
 -   Multiplying, adding, or subtracting two values.
 
-In such cases, the resulting type and value is implementation-defined,
-but must be one of the following:
-
--   The computation is done as though the types of the values were `float`
-    with the result having that type.
--   The result type is int and the value reflects wrap-around (for
-    example adding 1 to the largest value results in the smallest value).
--   The computation is done as though the type had some unspecified,
-    arithmetic-like object type with the result being mathematically
-    correct.
+In such cases, the computation is done as though the types of the values were
+`float` with the result having that type.
 
 The constants `PHP_INT_SIZE` (§[[6.3](06-constants.md#core-predefined-constants)](#core-predefined-constants)) and `PHP_INT_MAX` (§[[6.3](06-constants.md#core-predefined-constants)](#core-predefined-constants)) define certain
 characteristics about type `int`.

spec/08-conversions.md

@@ -40,8 +40,22 @@ result value is 0; otherwise, the result value is 1.
 
 If the source type is `float`, for the values `INF`, `-INF`, and `NAN`, the
 result value is implementation-defined. For all other values, if the
-precision can be preserved, the fractional part is rounded towards zero
-and the result is well defined; otherwise, the result is undefined.
+precision can be preserved (that is, the float is within the range of an
+integer), the fractional part is rounded towards zero. If the precision cannot
+be preserved, the following conversion algorithm is used:
+
+ 1. The floating point remainder (wherein the remainder has the same sign as the
+    dividend) of dividing the float by 2 to the power of the number of bits in
+    an integer (for example, 32), rounded towards zero, is taken.
+ 2. If the remainder is less than zero, it is rounded towards
+    infinity and 2 to the power of the number of bits is added.
+ 3. This result is then converted to an unsigned integer, then converted to a
+    signed integer by treating the unsigned integer as a two's complement
+    representation of the signed integer.
+
+Implementations may implement this conversion differently (for example, on some
+architectures there may be hardware support for this specific conversion mode)
+so long as the result is the same.
 
 If the source value is `NULL`, the result value is 0.