nx_alu_divider_proof_test.nx

nx_alu_divider_proof_test.nx -- the divider's PROOF step (theory -> PROOF -> raced). Not randomized: a machine-checked INDUCTIVE proof, width-independent. THEORY (cited): restoring division is a digit recurrence -- Parhami; H&P. PROOF (here): correctness of the W-stage divider follows by INDUCTION on stages from the per-stage INVARIANT. Inductive step (one radix-2 stage): given 0 <= rem < b (hypothesis) and an input bit in {0,1}, rem_in = 2*rem + bit (so 0 <= rem_in < 2b) ge = (rem_in >=u b) (LTU, magnitude-correct for ALL b) rem' = ge ? rem_in - b : rem_in qbit = ge CLAIM: 0 <= rem' < b AND rem' = rem_in mod b AND qbit = rem_in div b. This claim uses only compare/subtract/select, which are MAGNITUDE-CLEAN for any b (LTU/SUB/MUX), so the step is b-INDEPENDENT in argument; we MACHINE-CHECK it EXHAUSTIVELY over the step's full local space for every b in [1, 512] (all rem in [0,b), both bits). Base case rem=0 holds; the step preserves the invariant; therefore by induction the W-stage divider is correct AT ANY WIDTH -- the verified-coverage the incumbent (Yosys/ABC $div, structural-LEC-only) does NOT give. This is k-induction over the recurrence, done with no SAT solver. Known answer (FAIL LOUD): "262656 262656 " (steps proven / total). exit 0 iff equal.