float div: full IEEE subnormal support (pre-normalize both operands, then right-shift the aligned quotient by max(0,1-er) for gradual underflow); oracle validated bit-exact against numpy; all float variants rebuilt. add/mul/div subnormals now complete.

neural_computer.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:9340602703da2e7563954a45a2febb1d8ed026ac861b493883add2d5311f1f9d
-size 33592582
+oid sha256:c358cad0b5e5fd8cf83720eeb42a399047409d374932a9dc6ec3ebda754933bf
+size 34601074

src/build.py

@@ -1492,19 +1492,16 @@ def add_float_div(tensors: Dict[str, torch.Tensor], family: str,
     Self-contained circuit; external inputs are the raw operand words
     $a[0..W-1] / $b[0..W-1] (MSB-first). Contract: exact IEEE specials
     (NaN, infinities, signed zeros, x/0 -> inf, 0/0 and inf/inf -> NaN),
-    flush-to-zero for subnormal operands and results, round-to-nearest-even
-    for the mantissa.
-
-    Datapath: F+3 restoring-division stages (one quotient bit each; the two
-    extra stages supply the guard bit in either normalize case), a one-bit
-    normalize mux bank keyed on the integer quotient bit, guard/round/sticky
-    extraction with a round-to-nearest-even incrementer on the fraction, two
-    E+2-bit two's-complement exponent chains computing exp_a - exp_b + bias
-    - 1 + q0 plus a rounding-overflow carry, range detectors, and a one-hot
-    specials selection network producing the output word.
-
-    Rounding: round-to-nearest-even (RNE); underflow flushes to zero,
-    specials exact.
+    subnormal operands and gradual-underflow subnormal results,
+    round-to-nearest-even for the mantissa.
+
+    Datapath: each operand mantissa is pre-normalized (a leading-zero count
+    drives a left-barrel so the leading 1 sits at bit F, and na = eexp - lz);
+    F+3 restoring-division stages produce the quotient; a one-bit normalize mux
+    aligns it on the integer quotient bit; two E+2-bit exponent chains give
+    er = na - nb + bias - 1 + q0; the aligned mantissa frame is right-shifted by
+    max(0, 1 - er) to denormalize subnormal quotients; then round-to-nearest-even
+    and a one-hot specials network produce the output word.
     """
     E, F = exp_bits, frac_bits
     prefix = f"{family}.div"
@@ -1516,11 +1513,40 @@ def add_float_div(tensors: Dict[str, torch.Tensor], family: str,
 
     for op in ("a", "b"):
         add_gate(tensors, f"{prefix}.{op}.exp_zero", [-1.0] * E, [0.0])
+        add_gate(tensors, f"{prefix}.{op}.exp_nzero", [1.0] * E, [-1.0])
         add_gate(tensors, f"{prefix}.{op}.exp_max", [1.0] * E, [-float(E)])
         add_gate(tensors, f"{prefix}.{op}.frac_nz", [1.0] * F, [-1.0])
         add_gate(tensors, f"{prefix}.{op}.frac_zero", [-1.0] * F, [0.0])
         add_gate(tensors, f"{prefix}.{op}.is_nan", [1.0, 1.0], [-2.0])
         add_gate(tensors, f"{prefix}.{op}.is_inf", [1.0, 1.0], [-2.0])
+        add_gate(tensors, f"{prefix}.{op}.is_zero", [1.0, 1.0], [-2.0])
+        add_gate(tensors, f"{prefix}.{op}.nonzero", [-1.0], [0.0])
+        add_gate(tensors, f"{prefix}.{op}.eexp_lsb", [1.0, 1.0], [-1.0])
+
+    # Pre-normalize each operand mantissa: a leading-zero count over the F+1-bit
+    # mantissa drives a left-barrel so the leading 1 sits at bit F; na = eexp - lz.
+    ML = F + 1
+    mlzb = 0
+    while (1 << mlzb) <= ML:
+        mlzb += 1
+    for op in ("a", "b"):
+        for pos in range(1, ML):
+            add_gate(tensors, f"{prefix}.{op}.pn.any_higher{pos}", [1.0] * pos, [-1.0])
+            add_gate(tensors, f"{prefix}.{op}.pn.is_highest{pos}.not_higher", [-1.0], [0.0])
+            add_gate(tensors, f"{prefix}.{op}.pn.is_highest{pos}.and", [1.0, 1.0], [-2.0])
+        for bbit in range(mlzb):
+            fan = sum(1 for pos in range(1, ML) if (pos >> bbit) & 1)
+            add_gate(tensors, f"{prefix}.{op}.pn.lz.bit{bbit}", [1.0] * max(1, fan), [-1.0])
+        for bbit in range(mlzb):
+            for k in range(ML):
+                add_gate(tensors, f"{prefix}.{op}.pn.s{bbit}.bit{k}.not_sel", [-1.0], [0.0])
+                add_gate(tensors, f"{prefix}.{op}.pn.s{bbit}.bit{k}.and_a", [1.0, 1.0], [-2.0])
+                add_gate(tensors, f"{prefix}.{op}.pn.s{bbit}.bit{k}.and_b", [1.0, 1.0], [-2.0])
+                add_gate(tensors, f"{prefix}.{op}.pn.s{bbit}.bit{k}.or", [1.0, 1.0], [-1.0])
+        for bbit in range(mlzb):
+            add_gate(tensors, f"{prefix}.{op}.nlz.bit{bbit}", [-1.0], [0.0])
+        for bit in range(E + 2):
+            add_full_adder(tensors, f"{prefix}.{op}.neff.fa{bit}")
 
     # Restoring division stages: per stage a bit-cascade GE comparator, the
     # quotient-bit OR (shifted-out top bit forces GE), a conditional
@@ -1560,7 +1586,44 @@ def add_float_div(tensors: Dict[str, torch.Tensor], family: str,
     add_gate(tensors, f"{prefix}.round.g.or", [1.0, 1.0], [-1.0])
     add_gate(tensors, f"{prefix}.round.rem_nz", [1.0] * (F + 1), [-1.0])
     add_gate(tensors, f"{prefix}.round.q_extra", [1.0, 1.0], [-2.0])
-    add_gate(tensors, f"{prefix}.round.sticky", [1.0, 1.0], [-1.0])
+    add_gate(tensors, f"{prefix}.round.sticky_orig", [1.0, 1.0], [-1.0])   # rem_nz OR q_extra
+
+    # exp_r = na - nb + bias - 1 + q0 (E+2-bit two's complement) using the
+    # pre-normalized effective exponents na = a.neff, nb = b.neff.
+    for bit in range(E + 2):
+        add_gate(tensors, f"{prefix}.exp_nb.bit{bit}", [-1.0], [0.0])       # ~nb
+    for bit in range(E + 2):
+        add_full_adder(tensors, f"{prefix}.exp_s1.fa{bit}")                # na + ~nb + q0
+        add_full_adder(tensors, f"{prefix}.exp_r.fa{bit}")                 # + bias
+
+    # Gradual underflow: right-shift the aligned mantissa frame MF (bit 0 guard,
+    # bits 1..F frac, bit F+1 implicit 1) by rsh = max(0, 1 - er).
+    RBd = 0
+    while (1 << RBd) < (F + 2):
+        RBd += 1
+    add_gate(tensors, f"{prefix}.er.zero", [-1.0] * (E + 2), [0.0])
+    add_gate(tensors, f"{prefix}.er.underflow", [1.0, 1.0], [-1.0])
+    add_gate(tensors, f"{prefix}.er.not_underflow", [-1.0], [0.0])
+    for k in range(E + 2):
+        add_gate(tensors, f"{prefix}.exprc.bit{k}", [1.0, 1.0], [-2.0])     # er clamped >= 0
+        add_gate(tensors, f"{prefix}.ernot.bit{k}", [-1.0], [0.0])          # ~er
+        add_full_adder(tensors, f"{prefix}.subv.fa{k}")                    # 1 - er
+        add_gate(tensors, f"{prefix}.rsh.bit{k}", [1.0, 1.0], [-2.0])       # (1-er) AND underflow
+    add_gate(tensors, f"{prefix}.too_deep", [1.0] * (E + 2 - RBd), [-1.0])
+    add_gate(tensors, f"{prefix}.not_deep", [-1.0], [0.0])
+    for j in range(RBd):
+        add_gate(tensors, f"{prefix}.rbar.s{j}.drop", [1.0] * (1 << j), [-1.0])
+        add_gate(tensors, f"{prefix}.rbar.s{j}.st_and", [1.0, 1.0], [-2.0])
+        add_gate(tensors, f"{prefix}.rbar.s{j}.sticky", [1.0, 1.0], [-1.0])
+        for k in range(F + 2):
+            add_gate(tensors, f"{prefix}.rbar.s{j}.bit{k}.not_sel", [-1.0], [0.0])
+            add_gate(tensors, f"{prefix}.rbar.s{j}.bit{k}.and_a", [1.0, 1.0], [-2.0])
+            add_gate(tensors, f"{prefix}.rbar.s{j}.bit{k}.and_b", [1.0, 1.0], [-2.0])
+            add_gate(tensors, f"{prefix}.rbar.s{j}.bit{k}.or", [1.0, 1.0], [-1.0])
+    for k in range(F):
+        add_gate(tensors, f"{prefix}.sig.bit{k}", [1.0, 1.0], [-2.0])       # shifted[k+1] AND not_deep
+    add_gate(tensors, f"{prefix}.round.guard", [1.0, 1.0], [-2.0])          # shifted[0] AND not_deep
+    add_gate(tensors, f"{prefix}.round.sticky", [1.0, 1.0, 1.0], [-1.0])    # barrel OR orig OR too_deep
     add_gate(tensors, f"{prefix}.round.rsl", [1.0, 1.0], [-1.0])
     add_gate(tensors, f"{prefix}.round.up", [1.0, 1.0], [-2.0])
     for k in range(F):
@@ -1568,24 +1631,12 @@ def add_float_div(tensors: Dict[str, torch.Tensor], family: str,
         add_gate(tensors, f"{prefix}.rnd.bit{k}.xor.layer1.nand", [-1.0, -1.0], [1.0])
         add_gate(tensors, f"{prefix}.rnd.bit{k}.xor.layer2", [1.0, 1.0], [-2.0])
         add_gate(tensors, f"{prefix}.rnd.bit{k}.carry", [1.0, 1.0], [-2.0])
-
-    # exp_r = exp_a - exp_b + bias - 1 + q0 in E+2-bit two's complement:
-    # chain s1 = exp_a + ~exp_b (cin = q0), then exp_r = s1 + bias (cin = 0).
-    for bit in range(E):
-        add_gate(tensors, f"{prefix}.exp_nb.bit{bit}", [-1.0], [0.0])
-    for bit in range(E + 2):
-        add_full_adder(tensors, f"{prefix}.exp_s1.fa{bit}")
-        add_full_adder(tensors, f"{prefix}.exp_r.fa{bit}")
-
-    # exp_final = exp_r + rounding carry-out (E+2-bit incrementer).
     for bit in range(E + 2):
         add_gate(tensors, f"{prefix}.exp_round.bit{bit}.xor.layer1.or", [1.0, 1.0], [-1.0])
         add_gate(tensors, f"{prefix}.exp_round.bit{bit}.xor.layer1.nand", [-1.0, -1.0], [1.0])
         add_gate(tensors, f"{prefix}.exp_round.bit{bit}.xor.layer2", [1.0, 1.0], [-2.0])
         add_gate(tensors, f"{prefix}.exp_round.bit{bit}.carry", [1.0, 1.0], [-2.0])
-
     add_gate(tensors, f"{prefix}.exp_r.zero", [-1.0] * (E + 2), [0.0])
-    add_gate(tensors, f"{prefix}.exp_r.underflow", [1.0, 1.0], [-1.0])
     add_gate(tensors, f"{prefix}.exp_r.not_neg", [-1.0], [0.0])
     add_gate(tensors, f"{prefix}.exp_r.and_low", [1.0] * E, [-float(E)])
     add_gate(tensors, f"{prefix}.exp_r.ge_emax", [1.0, 1.0], [-1.0])
@@ -3304,11 +3355,40 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
     zero = reg.get_id("#0")
     one = reg.get_id("#1")
 
-    def m_a(k: int) -> int:
-        return one if k == F else a(W - 1 - k)
+    ML = F + 1
+    mlzb = 0
+    while (1 << mlzb) <= ML:
+        mlzb += 1
+    RBd = 0
+    while (1 << RBd) < (F + 2):
+        RBd += 1
 
-    def m_b(k: int) -> int:
-        return one if k == F else b(W - 1 - k)
+    def m_raw(op: str, k: int) -> int:               # raw mantissa (implicit = exp!=0)
+        w = a if op == "a" else b
+        return R(f"{op}.exp_nzero") if k == F else w(W - 1 - k)
+
+    def m_a(k: int) -> int:                           # pre-normalized dividend
+        return R(f"a.pn.s{mlzb - 1}.bit{k}.or")
+
+    def m_b(k: int) -> int:                           # pre-normalized divisor
+        return R(f"b.pn.s{mlzb - 1}.bit{k}.or")
+
+    def eexp(op: str, k: int) -> int:
+        w = a if op == "a" else b
+        return R(f"{op}.eexp_lsb") if k == 0 else (w(E - k) if k < E else zero)
+
+    def na(op: str, k: int) -> int:                   # effective exponent na = eexp - lz
+        return R(f"{op}.neff.fa{k}.ha2.sum.layer2") if k < E + 2 else zero
+
+    def MF(k: int) -> int:                            # aligned mantissa frame
+        if k == 0:
+            return R("round.g.or")                     # guard
+        if k <= F:
+            return R(f"norm.bit{k - 1}.or")            # frac[k-1]
+        return one                                     # implicit
+
+    def shifted(k: int) -> int:                       # frame right-shifted by rsh
+        return R(f"rbar.s{RBd - 1}.bit{k}.or")
 
     def rem_prev(stage: int, k: int) -> int:
         return R(f"mant_div.stage{stage - 1}.mux.bit{k}.or")
@@ -3337,16 +3417,24 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
         "sign_xor.layer1.or": [a(0), b(0)],
         "sign_xor.layer1.nand": [a(0), b(0)],
         "sign_xor.layer2": [R("sign_xor.layer1.or"), R("sign_xor.layer1.nand")],
-        "a.exp_zero": exp_a_field, "a.exp_max": exp_a_field,
+        "a.exp_zero": exp_a_field, "a.exp_nzero": exp_a_field, "a.exp_max": exp_a_field,
         "a.frac_nz": frac_a_field, "a.frac_zero": frac_a_field,
         "a.is_nan": [R("a.exp_max"), R("a.frac_nz")],
         "a.is_inf": [R("a.exp_max"), R("a.frac_zero")],
-        "b.exp_zero": exp_b_field, "b.exp_max": exp_b_field,
+        "a.is_zero": [R("a.exp_zero"), R("a.frac_zero")], "a.nonzero": [R("a.is_zero")],
+        "a.eexp_lsb": [a(E), R("a.exp_zero")],
+        "b.exp_zero": exp_b_field, "b.exp_nzero": exp_b_field, "b.exp_max": exp_b_field,
         "b.frac_nz": frac_b_field, "b.frac_zero": frac_b_field,
         "b.is_nan": [R("b.exp_max"), R("b.frac_nz")],
         "b.is_inf": [R("b.exp_max"), R("b.frac_zero")],
+        "b.is_zero": [R("b.exp_zero"), R("b.frac_zero")], "b.nonzero": [R("b.is_zero")],
+        "b.eexp_lsb": [b(E), R("b.exp_zero")],
+        "er.zero": [R(f"exp_r.fa{k}.ha2.sum.layer2") for k in range(E + 2)],
+        "er.underflow": [R(f"exp_r.fa{E + 1}.ha2.sum.layer2"), R("er.zero")],
+        "er.not_underflow": [R("er.underflow")],
+        "too_deep": [R(f"rsh.bit{k}") for k in range(RBd, E + 2)],
+        "not_deep": [R("too_deep")],
         "exp_r.zero": [R(f"exp_round.bit{k}.xor.layer2") for k in range(E + 2)],
-        "exp_r.underflow": [R(f"exp_round.bit{E + 1}.xor.layer2"), R("exp_r.zero")],
         "exp_r.not_neg": [R(f"exp_round.bit{E + 1}.xor.layer2")],
         "exp_r.and_low": [R(f"exp_round.bit{k}.xor.layer2") for k in range(E)],
         "exp_r.ge_emax": [R(f"exp_round.bit{E}.xor.layer2"), R("exp_r.and_low")],
@@ -3357,21 +3445,23 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
         "round.g.or": [R("round.g.and_a"), R("round.g.and_b")],
         "round.rem_nz": [R(f"mant_div.stage{F + 2}.mux.bit{k}.or") for k in range(F + 1)],
         "round.q_extra": [R("mant_div.stage0.q"), R(f"mant_div.stage{F + 2}.q")],
-        "round.sticky": [R("round.rem_nz"), R("round.q_extra")],
-        "round.rsl": [R("round.sticky"), R("norm.bit0.or")],
-        "round.up": [R("round.g.or"), R("round.rsl")],
+        "round.sticky_orig": [R("round.rem_nz"), R("round.q_extra")],
+        "round.guard": [shifted(0), R("not_deep")],
+        "round.sticky": [R(f"rbar.s{RBd - 1}.sticky"), R("round.sticky_orig"), R("too_deep")],
+        "round.rsl": [R("round.sticky"), R("sig.bit0")],
+        "round.up": [R("round.guard"), R("round.rsl")],
         "sel.inputs_nan": [R("a.is_nan"), R("b.is_nan")],
-        "sel.zero_zero": [R("a.exp_zero"), R("b.exp_zero")],
+        "sel.zero_zero": [R("a.is_zero"), R("b.is_zero")],
         "sel.inf_inf": [R("a.is_inf"), R("b.is_inf")],
         "sel.nan_cases": [R("sel.zero_zero"), R("sel.inf_inf")],
         "sel.nan": [R("sel.inputs_nan"), R("sel.nan_cases")],
         "sel.not_nan": [R("sel.nan")],
-        "sel.inf_in": [R("a.is_inf"), R("b.exp_zero")],
-        "sel.zero_in": [R("a.exp_zero"), R("b.is_inf")],
+        "sel.inf_in": [R("a.is_inf"), R("b.is_zero")],
+        "sel.zero_in": [R("a.is_zero"), R("b.is_inf")],
         "sel.inf_or_ovf": [R("sel.inf_in"), R("exp_r.overflow")],
         "sel.not_inf_path": [R("sel.inf_or_ovf")],
         "sel.inf": [R("sel.not_nan"), R("sel.inf_or_ovf")],
-        "sel.zero_or_unf": [R("sel.zero_in"), R("exp_r.underflow")],
+        "sel.zero_or_unf": [R("sel.zero_in"), R("sel.zero_in")],
         "sel.not_zero_unf": [R("sel.zero_or_unf")],
         "sel.zero": [R("sel.not_nan"), R("sel.not_inf_path"), R("sel.zero_or_unf")],
         "sel.norm": [R("sel.not_nan"), R("sel.not_inf_path"), R("sel.not_zero_unf")],
@@ -3380,27 +3470,120 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
     if suffix in table:
         return table[suffix]
 
-    m = re.match(r"^exp_nb\.bit(\d+)$", suffix)
+    m = re.match(r"^([ab])\.pn\.any_higher(\d+)$", suffix)      # pre-normalize: LZC
+    if m:
+        op = m.group(1)
+        pos = int(m.group(2))
+        return [m_raw(op, ML - 1 - t) for t in range(pos)]
+    m = re.match(r"^([ab])\.pn\.is_highest(\d+)\.(not_higher|and)$", suffix)
     if m:
-        return [b(E - int(m.group(1)))]
+        op = m.group(1)
+        pos = int(m.group(2))
+        if m.group(3) == "not_higher":
+            return [R(f"{op}.pn.any_higher{pos}")]
+        return [m_raw(op, ML - 1 - pos), R(f"{op}.pn.is_highest{pos}.not_higher")]
+    m = re.match(r"^([ab])\.pn\.lz\.bit(\d+)$", suffix)
+    if m:
+        op = m.group(1)
+        bbit = int(m.group(2))
+        srcs = [R(f"{op}.pn.is_highest{pos}.and") for pos in range(1, ML) if (pos >> bbit) & 1]
+        return srcs if srcs else [zero]
+    m = re.match(r"^([ab])\.pn\.s(\d+)\.bit(\d+)\.(not_sel|and_a|and_b|or)$", suffix)   # left-barrel
+    if m:
+        op = m.group(1)
+        bbit = int(m.group(2))
+        k = int(m.group(3))
+        kind = m.group(4)
+        sel = R(f"{op}.pn.lz.bit{bbit}")
+
+        def lin(kk: int) -> int:
+            if kk < 0 or kk >= ML:
+                return zero
+            return m_raw(op, kk) if bbit == 0 else R(f"{op}.pn.s{bbit - 1}.bit{kk}.or")
 
-    m = re.match(r"^exp_s1\.fa(\d+)\.(.+)$", suffix)
+        if kind == "not_sel":
+            return [sel]
+        if kind == "and_a":
+            return [lin(k), R(f"{op}.pn.s{bbit}.bit{k}.not_sel")]
+        if kind == "and_b":
+            return [lin(k - (1 << bbit)), sel]
+        return [R(f"{op}.pn.s{bbit}.bit{k}.and_a"), R(f"{op}.pn.s{bbit}.bit{k}.and_b")]
+    m = re.match(r"^([ab])\.nlz\.bit(\d+)$", suffix)
+    if m:
+        return [R(f"{m.group(1)}.pn.lz.bit{int(m.group(2))}")]
+    m = re.match(r"^([ab])\.neff\.fa(\d+)\.(.+)$", suffix)      # na = eexp - lz
+    if m:
+        op = m.group(1)
+        k = int(m.group(2))
+        b_sig = R(f"{op}.nlz.bit{k}") if k < mlzb else one
+        cin = one if k == 0 else R(f"{op}.neff.fa{k - 1}.carry_or")
+        return _fa_member_inputs(m.group(3), f"{prefix}.{op}.neff.fa{k}", eexp(op, k), b_sig, cin, reg)
+
+    m = re.match(r"^exp_nb\.bit(\d+)$", suffix)                 # ~nb
+    if m:
+        return [na("b", int(m.group(1)))]
+    m = re.match(r"^exp_s1\.fa(\d+)\.(.+)$", suffix)            # na + ~nb + q0
     if m:
         k = int(m.group(1))
-        a_sig = a(E - k) if k < E else zero
-        b_sig = R(f"exp_nb.bit{k}") if k < E else one
         cin = q(0) if k == 0 else R(f"exp_s1.fa{k - 1}.carry_or")
         return _fa_member_inputs(m.group(2), f"{prefix}.exp_s1.fa{k}",
-                                 a_sig, b_sig, cin, reg)
-
-    m = re.match(r"^exp_r\.fa(\d+)\.(.+)$", suffix)
+                                 na("a", k), R(f"exp_nb.bit{k}"), cin, reg)
+    m = re.match(r"^exp_r\.fa(\d+)\.(.+)$", suffix)            # + bias
     if m:
         k = int(m.group(1))
         a_sig = R(f"exp_s1.fa{k}.ha2.sum.layer2")
         b_sig = one if (bias >> k) & 1 else zero
         cin = zero if k == 0 else R(f"exp_r.fa{k - 1}.carry_or")
-        return _fa_member_inputs(m.group(2), f"{prefix}.exp_r.fa{k}",
-                                 a_sig, b_sig, cin, reg)
+        return _fa_member_inputs(m.group(2), f"{prefix}.exp_r.fa{k}", a_sig, b_sig, cin, reg)
+    m = re.match(r"^exprc\.bit(\d+)$", suffix)                  # er clamped >= 0
+    if m:
+        k = int(m.group(1))
+        return [R(f"exp_r.fa{k}.ha2.sum.layer2"), R("er.not_underflow")]
+    m = re.match(r"^ernot\.bit(\d+)$", suffix)                  # ~er
+    if m:
+        return [R(f"exp_r.fa{int(m.group(1))}.ha2.sum.layer2")]
+    m = re.match(r"^subv\.fa(\d+)\.(.+)$", suffix)              # 1 - er
+    if m:
+        k = int(m.group(1))
+        a_sig = one if (1 >> k) & 1 else zero
+        cin = one if k == 0 else R(f"subv.fa{k - 1}.carry_or")
+        return _fa_member_inputs(m.group(2), f"{prefix}.subv.fa{k}", a_sig, R(f"ernot.bit{k}"), cin, reg)
+    m = re.match(r"^rsh\.bit(\d+)$", suffix)                    # rsh = (1-er) AND underflow
+    if m:
+        k = int(m.group(1))
+        return [R(f"subv.fa{k}.ha2.sum.layer2"), R("er.underflow")]
+    m = re.match(r"^rbar\.s(\d+)\.(.+)$", suffix)               # right-barrel on MF by rsh
+    if m:
+        j = int(m.group(1))
+        rest = m.group(2)
+        sel = R(f"rsh.bit{j}")
+
+        def rin(k: int) -> int:
+            if k < 0 or k > F + 1:
+                return zero
+            return MF(k) if j == 0 else R(f"rbar.s{j - 1}.bit{k}.or")
+
+        if rest == "drop":
+            return [rin(k) for k in range(1 << j)]
+        if rest == "st_and":
+            return [sel, R(f"rbar.s{j}.drop")]
+        if rest == "sticky":
+            prev = zero if j == 0 else R(f"rbar.s{j - 1}.sticky")
+            return [prev, R(f"rbar.s{j}.st_and")]
+        mm = re.match(r"^bit(\d+)\.(not_sel|and_a|and_b|or)$", rest)
+        if mm:
+            k = int(mm.group(1))
+            kind = mm.group(2)
+            if kind == "not_sel":
+                return [sel]
+            if kind == "and_a":
+                return [rin(k), R(f"rbar.s{j}.bit{k}.not_sel")]
+            if kind == "and_b":
+                return [rin(k + (1 << j)), sel]
+            return [R(f"rbar.s{j}.bit{k}.and_a"), R(f"rbar.s{j}.bit{k}.and_b")]
+    m = re.match(r"^sig\.bit(\d+)$", suffix)                    # mantissa frac bit (masked)
+    if m:
+        return [shifted(int(m.group(1)) + 1), R("not_deep")]
 
     m = re.match(r"^mant_div\.stage(\d+)\.(.+)$", suffix)
     if m:
@@ -3491,7 +3674,7 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
         k = int(m.group(1))
         rest = m.group(2)
         cin = R("round.up") if k == 0 else R(f"rnd.bit{k - 1}.carry")
-        f_bit = R(f"norm.bit{k}.or")
+        f_bit = R(f"sig.bit{k}")
         if rest == "xor.layer1.or" or rest == "xor.layer1.nand":
             return [f_bit, cin]
         if rest == "xor.layer2":
@@ -3504,7 +3687,7 @@ def infer_float_div_inputs(gate: str, reg: SignalRegistry, family: str,
         k = int(m.group(1))
         rest = m.group(2)
         cin = R(f"rnd.bit{F - 1}.carry") if k == 0 else R(f"exp_round.bit{k - 1}.carry")
-        e_bit = R(f"exp_r.fa{k}.ha2.sum.layer2")
+        e_bit = R(f"exprc.bit{k}")
         if rest == "xor.layer1.or" or rest == "xor.layer1.nand":
             return [e_bit, cin]
         if rest == "xor.layer2":

src/eval.py

@@ -754,7 +754,8 @@ def float_mul_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:
 def float_div_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:
     """Expected quotient word under the documented contract: exact IEEE
     specials (NaN, infinities, x/0 -> inf, 0/0 and inf/inf -> NaN, signed
-    zeros), flush-to-zero subnormals, round-to-nearest-even mantissa."""
+    zeros), subnormal operands and gradual-underflow subnormal results,
+    round-to-nearest-even mantissa."""
     E, F = exp_bits, frac_bits
     emax = (1 << E) - 1
     fmask = (1 << F) - 1
@@ -767,35 +768,52 @@ def float_div_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:
     b_nan = eb == emax and fb != 0
     a_inf = ea == emax and fa == 0
     b_inf = eb == emax and fb == 0
-    a_zero = ea == 0  # flush-to-zero
-    b_zero = eb == 0
-    inf_w = (s << (E + F)) | (emax << F)
-    zero_w = s << (E + F)
+    a_zero = ea == 0 and fa == 0
+    b_zero = eb == 0 and fb == 0
     if a_nan or b_nan or (a_zero and b_zero) or (a_inf and b_inf):
         return qnan
     if a_inf or b_zero:
-        return inf_w
+        return (s << (E + F)) | (emax << F)
     if a_zero or b_inf:
-        return zero_w
-    Ma, Mb = (1 << F) | fa, (1 << F) | fb
+        return s << (E + F)
+    Ma = ((1 << F) if ea else 0) | fa
+    Mb = ((1 << F) if eb else 0) | fb
+    eea = ea if ea else 1
+    eeb = eb if eb else 1
+    ta = Ma.bit_length() - 1                       # pre-normalize both mantissas
+    tb = Mb.bit_length() - 1
+    na = eea - (F - ta)
+    nb = eeb - (F - tb)
+    Ma <<= (F - ta)
+    Mb <<= (F - tb)
     q0 = 1 if Ma >= Mb else 0
-    exp_r = ea - eb + bias - 1 + q0
-    num = Ma << (F + 2 - q0)               # implicit 1 + F frac + guard bits
+    er = na - nb + bias - 1 + q0
+    num = Ma << (F + 2 - q0)
     Q = num // Mb
     rem = num % Mb
-    frac = (Q >> 1) & fmask
-    guard = Q & 1
-    sticky = 1 if rem else 0
-    if guard and ((frac & 1) or sticky):   # round-to-nearest-even
-        frac += 1
-        if frac > fmask:
-            frac = 0
-            exp_r += 1
-    if exp_r >= emax:
-        return inf_w
-    if exp_r <= 0:
-        return zero_w
-    return (s << (E + F)) | (exp_r << F) | frac
+    if er >= 1:
+        frac = (Q >> 1) & fmask
+        guard = Q & 1
+        sticky = 1 if rem else 0
+        if guard and ((frac & 1) or sticky):
+            frac += 1
+            if frac > fmask:
+                frac = 0
+                er += 1
+        if er >= emax:
+            return (s << (E + F)) | (emax << F)
+        return (s << (E + F)) | (er << F) | frac
+    rsh = (1 - er) + 1                              # gradual underflow
+    sig = Q >> rsh
+    guard = (Q >> (rsh - 1)) & 1
+    sticky = 1 if ((Q & ((1 << (rsh - 1)) - 1)) or rem) else 0
+    if guard and ((sig & 1) or sticky):
+        sig += 1
+    if sig == 0:
+        return s << (E + F)
+    if sig >= (1 << F):
+        return (s << (E + F)) | (1 << F)
+    return (s << (E + F)) | sig
 
 
 def float_add_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:

variants/neural_alu16.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:802a94ce8fe13fb1a65948d129b1a7ce867854d12a7e6c9ea29ad07cbf80101c
-size 26669131
+oid sha256:5f446db437a0de918305a96edfaa5e43871ccf04d4ff01af6dc4a0b0f5d9b299
+size 27677671

variants/neural_alu32.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:7d356eacda47b4d7854ddf6cf2ef1959099874e2a52f189f3bbf079112a4ce9d
-size 25056244
+oid sha256:d35d7c3801b45c4a34af02097f8e10389cb6eadb88df2962de913db0b455e2f5
+size 26064500

variants/neural_alu8.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:1b20bb8b51f6461b377ef7075d143fc722d373cc1f8a788ed784bbb38926d69d
-size 25056244
+oid sha256:ffcddf4c5081404b7d3010e705c40b13e4058973ea97b57f734e36f522a656ed
+size 26064500

variants/neural_computer16.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:af69d406922aa5bd6951fc26107e926a3952fe6500c9bb8764dc372719dc3015
-size 35185717
+oid sha256:7b945aabc345ec0313643493b2667b5aac4b034ab4aa878ddb89da8d39c1e198
+size 36194449

variants/neural_computer16_reduced.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:c905b9f7dc4777b30c5f48b055ed285b1fc33b12d93a476f7423427b5e815fc1
-size 27374453
+oid sha256:58f883b503cb40a6e9cd3fb0629fcce99de438fa4b52720fcdba12a024dc2ce5
+size 28382973

variants/neural_computer16_registers.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:1efb427160154a95592968ddeb2c9bb9ef52317abc2ac918308a690759fd8c47
-size 26755145
+oid sha256:b9f7ad572ba0136d068bab7edfafe9e2aa383e1a6fe1e1e291fb972cff589c20
+size 27764633

variants/neural_computer16_scratchpad.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:225e933c57d6367695138523e76c069941895ad459621b7d52c8ed25739201a5
-size 26839997
+oid sha256:aa7c9630864d48014acc971035034943d377f959839a889b871263d8af3636eb
+size 27848613

variants/neural_computer16_small.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:9b23b977f92f953d9f85f4aeec991163f325f2e881871ec567c8292a3315122e
-size 26959213
+oid sha256:71ede38e63607b4cda4e366db1bef813a48eb473f13aa0b4c563a72c1b244d94
+size 27967749

variants/neural_computer32.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:9340602703da2e7563954a45a2febb1d8ed026ac861b493883add2d5311f1f9d
-size 33592582
+oid sha256:c358cad0b5e5fd8cf83720eeb42a399047409d374932a9dc6ec3ebda754933bf
+size 34601074

variants/neural_computer32_reduced.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:9fa760a30def5486195c584adc51816bf289496c8d5faaadb728a17bed0201d5
-size 25781462
+oid sha256:7e72369c1d4839e176a28b1cac8d89082698254af54c81af82bc6391f50b1c68
+size 26789662

variants/neural_computer32_registers.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:15bf955559b534d3fd6243b45f89d42ae6d12a8784464536dc08ec745befbc84
-size 25162246
+oid sha256:065f85b710beb30882dc8dc76e0f5b00a50c0cbb7c98bbf786d236be56216678
+size 26170374

variants/neural_computer32_scratchpad.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:495bca1533a313103fb30eaff2400899ccabf4911a4c08543e6d66252febf498
-size 25246246
+oid sha256:ce74d1fb55c4e43902664788da52d612722fef4f434b5c7391a41a469c9106bc
+size 26254306

variants/neural_computer32_small.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:38d52839bac1d351804c76403dc5f51bf9d2bf22eaa5a7d3f8fac25dc9f2a84e
-size 25365434
+oid sha256:74614887741b0aab81644a23aec52b4315cc4cd8661030467b834d9d554c862f
+size 26374348

variants/neural_computer8.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:af719c6b6499b85dba19ba425dcb15c9a06c19f6cbb8ed160bfe78484dea5b1a
-size 33564518
+oid sha256:93aa28025be1610259c6605c0c0b645b26e4d9e4a3ff7482183e7b71c1825585
+size 34572926

variants/neural_computer8_reduced.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:e4a3ffff1d0d89ed5f7b5cb1a5bd21b06a89efa834e5daebe7296f19bd750c44
-size 25752570
+oid sha256:63c11df1459c3ae2f87437528f4af6a1e2b1a39cc4474fa6e800e83922beb8cf
+size 26761486

variants/neural_computer8_registers.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:9287c670af87dc6e7682d670d9d671bcf5d021065c7fdc77a0c3336e8f45ace7
-size 25134066
+oid sha256:1b315ef217223e48cd1967b723ac417da290c27fb86f450496f1fb77eb8270b8
+size 26142278

variants/neural_computer8_scratchpad.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:d468d051f2b58c8b2cfb360be2022a67f344cfc8d3f51fee51dc02ebb3384c7a
-size 25218118
+oid sha256:c493262272216ee4207c76e37dc11a96320828918c352e60f8dedda4513fe9a2
+size 26226042

variants/neural_computer8_small.safetensors

@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:6ec97c8709bfa2f5916849776cf65b2f0dcbd771b45a2c099e39dca7087e8846
-size 25337262
+oid sha256:1ebf7e275a87aa80033af987cede32e85aa35b4bb926d50df334a5e972149812
+size 26345338