nx_isa_loop_sov.nx

nx_isa_loop_sov.nx -- LOOP rung: derive ITERATIVE programs with a BACKWARD branch, run on god. The forward-branch rung (nx_isa_cf_sov) exercised a data-dependent path; this exercises a real LOOP -- a backward JAL (negative, sign-extended imm_j) around a decrementing counter (guaranteed termination). The new hardware path proven: the sim's negative branch/jump immediate. target/derived shape: acc = 0; i = a; while i > 0 { acc = acc + BODY(i,a,b); i = i - 1 } BODY = op2( op1(reg,reg), reg ) over registers {0, i, a, b}, op in {ADD,SUB,MUL}. (1) team COMPOSES a random non-trivial such loop T (non-constant over train, not all-zero), (2) team DERIVES a same-shape G by GA on T's TRAIN examples, (3) ENCODE both to a real RV64 loop (beq exit + backward jal) + run BOTH on rv64im_min_sim over 12 HELD-OUT inputs + verify sim(T)==sim(G). Termination is structural (counter i = a <= 13 decrements to 0), so every candidate halts; the search never hangs. Controls: FAITHFUL (loops with KNOWN closed forms a*a, a(a+1)/2, b*a(a+1)/2 -- correct only if the loop truly iterates a times on the hardware) + NEGATIVE (a perturbed body the differential must catch). license_tier: ORIGINAL