float add: full IEEE subnormal support (subnormal operands and gradual-underflow results) via effective exponent, implicit-bit selection, and a clamped normalize shift; oracle validated bit-exact against numpy float32/float16

src/build.py

@@ -1097,9 +1097,9 @@ def add_float_add(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, opposite-sign infinities -> NaN, exact
-    cancellation -> +0), flush-to-zero for subnormal operands and results,
-    round-to-nearest-even for the mantissa. A zero operand passes the other
-    operand through verbatim.
+    cancellation -> +0), subnormal operands and gradual-underflow subnormal
+    results, round-to-nearest-even for the mantissa. A zero operand passes the
+    other operand through verbatim.
 
     Datapath: payload comparison picks the larger-magnitude operand, swap
     muxes route it to L; the smaller mantissa is aligned right through a
@@ -1132,6 +1132,13 @@ def add_float_add(tensors: Dict[str, torch.Tensor], family: str,
         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])
+        # True zero is exp==0 AND frac==0; a subnormal (exp==0, frac!=0) is a
+        # nonzero datapath operand, not a zero.
+        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])
+        # Effective exponent LSB for subnormals: a subnormal (exp==0) acts at
+        # the smallest normal exponent (biased 1), so force the LSB when exp==0.
+        add_gate(tensors, f"{prefix}.{op}.eexp_lsb", [1.0, 1.0], [-1.0])
 
     # Payload magnitude comparison (chooses the larger-magnitude operand).
     add_bit_cascade_compare(
@@ -1148,7 +1155,7 @@ def add_float_add(tensors: Dict[str, torch.Tensor], family: str,
     # Swap muxes: sel = pl.lt (a smaller in magnitude -> L = b).
     add_gate(tensors, f"{prefix}.swap.not_sel", [-1.0], [0.0])
     for name, width in (("sign_l", 1), ("exp_l", E), ("exp_s", E),
-                        ("mant_l", F), ("mant_s", F)):
+                        ("mant_l", F), ("mant_s", F), ("impl_l", 1), ("impl_s", 1)):
         for k in range(width):
             g = f"{prefix}.swap.{name}.bit{k}" if width > 1 else f"{prefix}.swap.{name}"
             add_gate(tensors, f"{g}.and_a", [1.0, 1.0], [-2.0])
@@ -1248,6 +1255,20 @@ def add_float_add(tensors: Dict[str, torch.Tensor], family: str,
         add_gate(tensors, f"{prefix}.exp_round.bit{k}.xor.layer2", [1.0, 1.0], [-2.0])
         add_gate(tensors, f"{prefix}.exp_round.bit{k}.carry", [1.0, 1.0], [-2.0])
 
+    # Gradual underflow. exp_r <= 0 (pre-round) means the result is subnormal:
+    # clamp the normalize shift to exp_L so it stays denormalized, and clamp the
+    # exponent field to 0. The datapath's normal path then emits the subnormal.
+    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])       # OR(sign, zero)
+    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])   # AND(exp_r, not_uf)
+    for bbit in range(nlz_bits):                                          # nsh = min(nlz, exp_L)
+        add_gate(tensors, f"{prefix}.nsh.bit{bbit}.not_sel", [-1.0], [0.0])
+        add_gate(tensors, f"{prefix}.nsh.bit{bbit}.and_a", [1.0, 1.0], [-2.0])
+        add_gate(tensors, f"{prefix}.nsh.bit{bbit}.and_b", [1.0, 1.0], [-2.0])
+        add_gate(tensors, f"{prefix}.nsh.bit{bbit}.or", [1.0, 1.0], [-1.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])
@@ -1269,7 +1290,7 @@ def add_float_add(tensors: Dict[str, torch.Tensor], family: str,
     add_gate(tensors, f"{prefix}.sel.a_zero_pass", [1.0, 1.0, 1.0, 1.0], [-4.0])
     add_gate(tensors, f"{prefix}.sel.b_zero_pass", [1.0, 1.0, 1.0, 1.0], [-4.0])
     add_gate(tensors, f"{prefix}.sel.dp_reach", [1.0, 1.0, 1.0, 1.0], [-4.0])
-    add_gate(tensors, f"{prefix}.sel.dp_zero_c", [1.0, 1.0], [-1.0])
+    add_gate(tensors, f"{prefix}.sel.dp_zero_c", [1.0], [-1.0])   # true-zero result only
     add_gate(tensors, f"{prefix}.sel.not_dp_zero_c", [-1.0], [0.0])
     add_gate(tensors, f"{prefix}.sel.not_ovf", [-1.0], [0.0])
     add_gate(tensors, f"{prefix}.sel.dp_zero", [1.0, 1.0], [-2.0])
@@ -3444,14 +3465,14 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
     # bit F+2 implicit 1.
     def l_ext(k: int) -> int:
         if k == F + 2:
-            return one
+            return R("swap.impl_l.or")          # implicit bit: 1 normal, 0 subnormal
         if 2 <= k <= F + 1:
             return mant_l(k - 2)
         return zero
 
     def s_frame_in(k: int) -> int:
         if k == F + 2:
-            return one
+            return R("swap.impl_s.or")
         if 2 <= k <= F + 1:
             return mant_s(k - 2)
         return zero
@@ -3489,11 +3510,17 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         "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")],
+        "a.eexp_lsb": [a(E), R("a.exp_zero")],
+        "a.is_zero": [R("a.exp_zero"), R("a.frac_zero")],
+        "a.nonzero": [R("a.is_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.eexp_lsb": [b(E), R("b.exp_zero")],
+        "b.is_zero": [R("b.exp_zero"), R("b.frac_zero")],
+        "b.nonzero": [R("b.is_zero")],
         "swap.not_sel": [R("pl.lt")],
         "align.not_sat": [R("align.sat")],
         "align.sticky_final": [R(f"align.s{num_stages - 1}.sticky"), R("align.sat")],
@@ -3506,6 +3533,9 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         "round.tail": [shifted(1), shifted(0), R("align.sticky_final")],
         "round.rsl": [R("round.tail"), trunc(0)],
         "round.up": [shifted(2), R("round.rsl")],
+        "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")],
         "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")],
@@ -3520,14 +3550,14 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         "sel.not_inf_ops": [R("sel.inf_ops")],
         "sel.inf_operand": [R("sel.not_nan"), R("sel.inf_ops")],
         "sel.both_zero": [R("sel.not_nan"), R("sel.not_inf_ops"),
-                          R("a.exp_zero"), R("b.exp_zero")],
+                          R("a.is_zero"), R("b.is_zero")],
         "sel.a_zero_pass": [R("sel.not_nan"), R("sel.not_inf_ops"),
-                            R("a.exp_zero"), R("b.exp_nzero")],
+                            R("a.is_zero"), R("b.nonzero")],
         "sel.b_zero_pass": [R("sel.not_nan"), R("sel.not_inf_ops"),
-                            R("b.exp_zero"), R("a.exp_nzero")],
+                            R("b.is_zero"), R("a.nonzero")],
         "sel.dp_reach": [R("sel.not_nan"), R("sel.not_inf_ops"),
-                         R("a.exp_nzero"), R("b.exp_nzero")],
-        "sel.dp_zero_c": [R("lzc.not_nz"), R("exp_r.underflow")],
+                         R("a.nonzero"), R("b.nonzero")],
+        "sel.dp_zero_c": [R("lzc.not_nz")],
         "sel.not_dp_zero_c": [R("sel.dp_zero_c")],
         "sel.not_ovf": [R("exp_r.overflow")],
         "sel.dp_zero": [R("sel.dp_reach"), R("sel.dp_zero_c")],
@@ -3585,7 +3615,7 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         return [R("pl.le.not_gt")]
 
     # Swap muxes: sel = pl.lt; L side takes b when sel, S side takes a.
-    m = re.match(r"^swap\.(sign_l|exp_l|exp_s|mant_l|mant_s)(?:\.bit(\d+))?\.(and_a|and_b|or)$", suffix)
+    m = re.match(r"^swap\.(sign_l|exp_l|exp_s|mant_l|mant_s|impl_l|impl_s)(?:\.bit(\d+))?\.(and_a|and_b|or)$", suffix)
     if m:
         name = m.group(1)
         k = int(m.group(2)) if m.group(2) is not None else 0
@@ -3594,7 +3624,11 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         if name == "sign_l":
             a_side, b_side = a(0), b(0)
         elif name in ("exp_l", "exp_s"):
-            a_side, b_side = a(E - k), b(E - k)
+            # LSB carries the subnormal correction (effective exponent >= 1).
+            a_side, b_side = ((R("a.eexp_lsb"), R("b.eexp_lsb")) if k == 0
+                             else (a(E - k), b(E - k)))
+        elif name in ("impl_l", "impl_s"):
+            a_side, b_side = R("a.exp_nzero"), R("b.exp_nzero")
         else:
             a_side, b_side = a(W - 1 - k), b(W - 1 - k)
         l_side = name.endswith("_l") or name == "sign_l"
@@ -3702,7 +3736,7 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
         bbit = int(m.group(1))
         k = int(m.group(2))
         kind = m.group(3)
-        sel = R(f"lzc.nlz.bit{bbit}")
+        sel = R(f"nsh.bit{bbit}.or")       # clamped shift = min(nlz, exp_L)
 
         def nin(kk: int) -> int:
             if kk < 0 or kk >= RES:
@@ -3737,7 +3771,7 @@ def infer_float_add_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}")          # exp_r clamped to 0 when subnormal
         if rest == "xor.layer1.or" or rest == "xor.layer1.nand":
             return [e_bit, cin]
         if rest == "xor.layer2":
@@ -3749,6 +3783,23 @@ def infer_float_add_inputs(gate: str, reg: SignalRegistry, family: str,
     if m:
         return [R(f"lzc.nlz.bit{int(m.group(1))}")]
 
+    m = re.match(r"^exprc\.bit(\d+)$", suffix)          # exp_r clamped to 0 on underflow
+    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"^nsh\.bit(\d+)\.(not_sel|and_a|and_b|or)$", suffix)   # min(nlz, exp_L)
+    if m:
+        bbit = int(m.group(1))
+        kind = m.group(2)
+        if kind == "not_sel":
+            return [R("er.underflow")]
+        if kind == "and_a":
+            return [R(f"lzc.nlz.bit{bbit}"), R(f"nsh.bit{bbit}.not_sel")]
+        if kind == "and_b":
+            return [exp_l(bbit), R("er.underflow")]
+        return [R(f"nsh.bit{bbit}.and_a"), R(f"nsh.bit{bbit}.and_b")]
+
     m = re.match(r"^exp_s1\.fa(\d+)\.(.+)$", suffix)
     if m:
         k = int(m.group(1))

src/eval.py

@@ -780,8 +780,9 @@ def float_div_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:
 def float_add_oracle(aw: int, bw: int, exp_bits: int, frac_bits: int) -> int:
     """Expected sum word under the documented contract: exact IEEE specials
     (NaN, infinities, opposite-sign infinities -> NaN, signed zeros, exact
-    cancellation -> +0), flush-to-zero subnormals (a zero operand passes the
-    other through verbatim), round-to-nearest-even mantissa."""
+    cancellation -> +0), subnormal operands and gradual-underflow subnormal
+    results, round-to-nearest-even mantissa. A zero operand passes the other
+    through verbatim. Pure integer arithmetic, so exact."""
     E, F = exp_bits, frac_bits
     emax = (1 << E) - 1
     fmask = (1 << F) - 1
@@ -792,59 +793,72 @@ def float_add_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
     if a_nan or b_nan or (a_inf and b_inf and sa != sb):
         return qnan
     if a_inf or b_inf:
         s = sa if a_inf else sb
         return (s << (E + F)) | (emax << F)
+    a_zero = ea == 0 and fa == 0                 # true zero, not subnormal
+    b_zero = eb == 0 and fb == 0
     if a_zero and b_zero:
         return (sa & sb) << (E + F)
     if a_zero:
         return bw
     if b_zero:
         return aw
-    Ma, Mb = (1 << F) | fa, (1 << F) | fb
-    pla, plb = (ea << F) | fa, (eb << F) | fb
+    Ma = ((1 << F) if ea else 0) | fa            # implicit bit = (exp != 0)
+    Mb = ((1 << F) if eb else 0) | fb
+    eea = ea if ea else 1                         # effective (denormal) exponent
+    eeb = eb if eb else 1
+    pla = (eea << (F + 1)) | Ma
+    plb = (eeb << (F + 1)) | Mb
     if pla >= plb:
-        sL, ML, eL, MS, eS = sa, Ma, ea, Mb, eb
+        sL, ML, eL, MS, eS = sa, Ma, eea, Mb, eeb
     else:
-        sL, ML, eL, MS, eS = sb, Mb, eb, Ma, ea
+        sL, ML, eL, MS, eS = sb, Mb, eeb, Ma, eea
     d = eL - eS
-    # Exact fixed-point value with G extra low bits below the mantissa LSB,
-    # so guard/round/sticky are all recoverable for round-to-nearest-even.
+    # Exact fixed-point value with G extra low bits below the mantissa LSB.
     G = F + 4
     total = (ML << (d + G)) + (MS << G) if sa == sb else (ML << (d + G)) - (MS << G)
     if total == 0:
         return 0  # exact cancellation -> +0
     t = total.bit_length() - 1
-    # Normalize so the leading 1 sits at bit position (F + G); the mantissa
-    # is the top F+1 bits, then guard/round/sticky below.
     exp_r = eS + (t - G) - F
-    lead = F + G
-    if t >= lead:
-        sh = t - lead
-        mant_ext = total >> sh
-        sticky_low = 1 if (total & ((1 << sh) - 1)) else 0
+    if exp_r >= 1:
+        lead = F + G
+        if t >= lead:
+            sh = t - lead
+            mant_ext = total >> sh
+            sticky_low = 1 if (total & ((1 << sh) - 1)) else 0
+        else:
+            mant_ext = total << (lead - t)
+            sticky_low = 0
+        frac = (mant_ext >> G) & fmask
+        guard = (mant_ext >> (G - 1)) & 1
+        below = (mant_ext & ((1 << (G - 1)) - 1)) or sticky_low
+        if guard and ((frac & 1) or below):      # round-to-nearest-even
+            frac += 1
+            if frac > fmask:
+                frac = 0
+                exp_r += 1
+        if exp_r >= emax:
+            return (sL << (E + F)) | (emax << F)
+        return (sL << (E + F)) | (exp_r << F) | frac
+    # subnormal result: gradual underflow to exponent field 0
+    rshift = G + 1 - eS
+    if rshift <= 0:
+        sig = total << (-rshift)
     else:
-        mant_ext = total << (lead - t)
-        sticky_low = 0
-    frac = (mant_ext >> G) & fmask
-    guard = (mant_ext >> (G - 1)) & 1
-    below = (mant_ext & ((1 << (G - 1)) - 1)) or sticky_low
-    if guard and ((frac & 1) or below):     # round-to-nearest-even
-        frac += 1
-        if frac > fmask:
-            frac = 0
-            exp_r += 1
-    inf_w = (sL << (E + F)) | (emax << F)
-    zero_w = sL << (E + F)
-    if exp_r >= emax:
-        return inf_w
-    if exp_r <= 0:
-        return zero_w
-    return (sL << (E + F)) | (exp_r << F) | frac
+        sig = total >> rshift
+        guard = (total >> (rshift - 1)) & 1
+        sticky = 1 if (total & ((1 << (rshift - 1)) - 1)) else 0
+        if guard and ((sig & 1) or sticky):
+            sig += 1
+    if sig == 0:
+        return sL << (E + F)
+    if sig >= (1 << F):                           # rounded up to smallest normal
+        return (sL << (E + F)) | (1 << F)
+    return (sL << (E + F)) | sig
 
 
 # =============================================================================