U64 restoring division: 64 iterations, each shifting the next dividend bit
into the partial remainder and subtracting the divisor when it fits. The
remainder is always < divisor, so 2r+1 can exceed 64 bits only when the
remainder's high bit was set; that bit is the carry out of the shift and
means the divisor fits (2r >= 2^64 > divisor), and the wrapped subtraction
still yields the exact new remainder (the true value is < 2^64).
1205def stdU64DivisionStep =
1206 (lambda unrestricted divisor : (family ModelWord64) .
1207 (lambda unrestricted state : (family StdU64DivisionState) .
1208 (eliminate
1209 StdU64DivisionState
1210 (lambda unrestricted current : (family StdU64DivisionState) . (family StdU64DivisionState))
1211 state
1212 (branch
1213 StdU64DivisionStateOf
1214 remainder
1215 quotient
1216 dividend
1217 .
1218 (app
1219 (lambda unrestricted shifted : (family ModelWord64) .
1220 (app
1221 (lambda unrestricted shiftedQuotient : (family ModelWord64) .
1222 (app
1223 (lambda unrestricted shiftedDividend : (family ModelWord64) .
1224 (nat-eliminate
1225 (lambda unrestricted current : Nat . (family StdU64DivisionState))
1226 (constructor
1227 StdU64DivisionState
1228 StdU64DivisionStateOf
1229 shifted
1230 shiftedQuotient
1231 shiftedDividend)
1232 (lambda unrestricted predecessor : Nat .
1233 (lambda unrestricted induction : (family StdU64DivisionState) .
1234 (constructor
1235 StdU64DivisionState
1236 StdU64DivisionStateOf
1237 (modelWord64Subtract shifted divisor)
1238 (modelWord64Add shiftedQuotient modelWord64One)
1239 shiftedDividend)))
1240 (modelWord64FlagOr
1241 (modelWord64HighBit remainder)
1242 (modelWord64FlagNot (modelWord64LessThan shifted divisor)))))
1243 (modelWord64ShiftLeftOne dividend)))
1244 (modelWord64ShiftLeftOne quotient)))
1245 (modelWord64Add
1246 (modelWord64ShiftLeftOne remainder)
1247 (modelWord64Select (modelWord64HighBit dividend) modelWord64One modelWord64Zero)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.