3.8. Deterministic bounded splitting🔗

Hex.Nat.Squfof.factor searches for a proper divisor of an input below 2^64, using exact arithmetic and no random seed. Its result includes the actual multiplier attempts, recurrence steps, and peak queue length. A reported divisor need not itself be prime; Hex.Nat.Squfof.factor_spec proves that it is strictly between one and the input and divides the input.

The combined forward/reverse budget is visible on a small example:

(some 4451, 1, 25)#eval let r := Hex.Nat.Squfof.factor 22117019
        { multipliers := 1, steps := 25 }
      let d := match r.outcome with
        | .factor d => some d
        | _ => none
      (d, r.attempts, r.steps)

(some 4451, 1, 25)

One fewer step exhausts the selected search. Exhaustion is not a primality verdict:

true#eval (Hex.Nat.Squfof.factor 22117019
  { multipliers := 1, steps := 24 }).outcome == .exhausted

true

Very close factors can give an immediate square form even at 64 bits. This example has factors 4026531853 and 4026532019:

(some 4026531853, 1, 2)#eval let r := Hex.Nat.Squfof.factor 16212959431627901207
        { multipliers := 1, steps := 128 }
      let d := match r.outcome with
        | .factor d => some d
        | _ => none
      (d, r.attempts, r.steps)

(some 4026531853, 1, 2)

This close-factor example does not predict the cost of a general 64-bit composite. Primes, unsuitable forms, and resource exhaustion can produce no factor; inputs at or above 2^64 return unsupported. The complete checked factorization interface offers an explicit SQUFOF policy in the integer-factorization chapter.