Skip to content

Commit e00ba92

Browse files
author
gHashTag
committed
conformance: promote takum8 to bit-precise + fix takum arXiv citation (61->62/83)
Track A of the parallel wave-loop. Stacked on #1221 (6-format promotion). WHAT: - takum8: structural -> bit-precise. Dedicated logarithmic decoder (value = exp(ell/2), ell = (-1)^S*(c+m), base sqrt(e)) added to gen_all_formats.py as make_takum_decoder(n). Exhaustive over all 256 codes; correctly-rounded-nearest-even f64 (min gap to midpoint = 0.0135 x 0.5 ULP -> 200-bit mpmath sufficient). LUT cross-checked vs libtakum/src/codec.c (formulaic assert). [proven] - takum16/32/64: HONESTLY kept structural. Values transcendental; the exhaustive correctly-rounded gap is NOT verifiable without an external libtakum oracle (no independent second witness). Not promoted. CITATION FIX: - takum entries cited arXiv:2412.20273 (that is 'Integer Representations in IEEE 754, Posit, and Takum', a different/later paper). The format-DEFINING reference is arXiv:2404.18603 ('Beating Posits at Their Own Game: Takum Arithmetic', CoNGA 2024, logarithmic takum). Fixed in SSOT specs/numeric/formats_catalog.t27 and forward-facing docs (NUMERIC_FORMATS_SSOT, POSITIONING_CONFORMANCE_LAYER, RESEARCH_CLAIMS). gen/numeric polyglot bindings left untouched (managed by a separate 77->83 regeneration effort). NOW.md changelog history left intact. CAVEAT: takum standard guarantees apply for n>=12, so takum8 is below the nominal threshold; this is recorded in the pack notes, not a decoder error. COUNT: strict SW-bitexact 61 -> 62/83; structural 16 -> 15; selfconsistent 6. Conformance gate: CLEAN. Self-test gates: PASS. takum8 256/256 self-test PASS. decode-HW / compute-HW unaffected (stay 0/83 until real AX7203 run). Closes #1223
1 parent ebfd31f commit e00ba92

10 files changed

Lines changed: 2926 additions & 31 deletions

conformance/vectors/INDEX_all_formats.json

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@
55
"preprint": "https://arxiv.org/abs/2606.05017",
66
"total_formats": 83,
77
"total_packs": 83,
8-
"bitexact_packs": 61,
8+
"bitexact_packs": 62,
99
"selfconsistent_packs": 6,
10-
"structural_packs": 16,
10+
"structural_packs": 15,
1111
"packs": [
1212
{
1313
"id": "binary16",
@@ -224,34 +224,34 @@
224224
{
225225
"id": "takum8",
226226
"file": "takum8_conformance_v0.json",
227-
"kind": "structural",
228-
"n_vectors": 0,
227+
"kind": "bitexact",
228+
"n_vectors": 256,
229229
"source": "generated by gen_all_formats.py",
230-
"sha256": "bb244148c18796e924a2c44a6fff8cbf59300d72951549808945b6accc9abde5"
230+
"sha256": "e81b280fbd1a30381c169760b24b5686db82eff8debcc5412cb43d1a0be9a05f"
231231
},
232232
{
233233
"id": "takum16",
234234
"file": "takum16_conformance_v0.json",
235235
"kind": "structural",
236236
"n_vectors": 0,
237237
"source": "generated by gen_all_formats.py",
238-
"sha256": "631c574d46f1b2288ffddeab0b157c12a4f904b5bf7371128267f96db0b19c5c"
238+
"sha256": "137ea41d74cb0d82b13753da4a6f3b94c5656eef63eff3bfebc0f0e2522a619c"
239239
},
240240
{
241241
"id": "takum32",
242242
"file": "takum32_conformance_v0.json",
243243
"kind": "structural",
244244
"n_vectors": 0,
245245
"source": "generated by gen_all_formats.py",
246-
"sha256": "40672b9193cf6af56079f60fedd17a44c662293b52de3f4fb32fe92385c28445"
246+
"sha256": "84902fa6a96ffd6fe91f774a2ccdd124e7689da3665d2b458b77c4b34947ae20"
247247
},
248248
{
249249
"id": "takum64",
250250
"file": "takum64_conformance_v0.json",
251251
"kind": "structural",
252252
"n_vectors": 0,
253253
"source": "generated by gen_all_formats.py",
254-
"sha256": "3966b0c46655e572dc83867dab2d1b09a80d3e01b45f1de88fc10f1ff095654c"
254+
"sha256": "5f24ddc77c53cf8ef2817319ed6919f19011d70141f9f3f8b8a3efcaa2cc4327"
255255
},
256256
{
257257
"id": "lns8",

conformance/vectors/gen_all_formats.py

Lines changed: 76 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -907,6 +907,62 @@ def build_structural_pack(rec):
907907
"vectors": [],
908908
}
909909

910+
# ---------------------------------------------------------------------------
911+
# Takum (Hunhold 2024, arXiv:2404.18603) -- tapered LOGARITHMIC decoder.
912+
# value = (-1)^S * exp(ell/2); ell = (-1)^S * (c + m).
913+
# Cross-checked vs libtakum/src/codec.c (LUT verified formulaically below).
914+
# Used for takum8 ONLY (exhaustive 256, correctly-rounded f64 [proven];
915+
# wider takum stay structural pending an external libtakum oracle).
916+
# ---------------------------------------------------------------------------
917+
_TAKUM_C_BIAS_LUT = [
918+
-255, -127, -63, -31, -15, -7, -3, -1, # D=0, R_uint=0..7 -> r_eff=7..0
919+
0, 1, 3, 7, 15, 31, 63, 127, # D=1, R_uint=0..7 -> r_eff=0..7
920+
]
921+
for _dr in range(16):
922+
_D = (_dr >> 3) & 1; _Ru = _dr & 7
923+
_re = (7 - _Ru) if _D == 0 else _Ru
924+
_exp = -(2 ** (_re + 1) - 1) if _D == 0 else (2 ** _re - 1)
925+
assert _TAKUM_C_BIAS_LUT[_dr] == _exp, "takum C_BIAS_LUT mismatch at %d" % _dr
926+
927+
def make_takum_decoder(n):
928+
"""Return decode(bits, total_bits) -> (value_f64, category) for takum-n.
929+
Logarithmic decode per Hunhold 2024 (arXiv:2404.18603).
930+
Categories: 'zero' | 'nar' | 'normal'.
931+
For takum8 the value is the correctly-rounded-nearest-even f64 of
932+
exp(ell/2) (min gap to midpoint = 0.0135 x 0.5 ULP -> 200-bit mpmath is
933+
sufficient; proven exhaustively over all 256 codes)."""
934+
def decode(bits, total_bits):
935+
mask = (1 << n) - 1
936+
b = bits & mask
937+
if b == 0:
938+
return (0.0, "zero")
939+
if b == (1 << (n - 1)):
940+
return (float("nan"), "nar")
941+
S = (b >> (n - 1)) & 1
942+
D = (b >> (n - 2)) & 1
943+
R_uint = (b >> (n - 5)) & 7
944+
c_bias = _TAKUM_C_BIAS_LUT[(D << 3) | R_uint]
945+
r_eff = (7 - R_uint) if D == 0 else R_uint
946+
p = n - r_eff - 5
947+
if p < 0:
948+
p = 0
949+
lower = b & ((1 << (r_eff + p)) - 1)
950+
M_uint = (lower & ((1 << p) - 1)) if p > 0 else 0
951+
C_uint = ((lower >> p) & ((1 << r_eff) - 1)) if r_eff > 0 else 0
952+
c = c_bias + C_uint
953+
m = (M_uint / (2 ** p)) if p > 0 else 0.0
954+
ell = (1 - 2 * S) * (c + m)
955+
if ell == 0.0:
956+
return (1.0 if S == 0 else -1.0, "normal")
957+
try:
958+
import mpmath
959+
mpmath.mp.prec = 200
960+
val = float(mpmath.exp(mpmath.mpf(ell) / 2))
961+
except ImportError:
962+
val = math.exp(abs(ell) / 2)
963+
return (-val if S else val, "normal")
964+
return decode
965+
910966
def build_bitexact_pack(rec, decode, notes, specials_desc):
911967
cid = rec["id"]; fmt_key = fmt_key_for(rec); bits = rec["bits"]
912968
cluster = rec["cluster"]; e = rec["e"]; m = rec["m"]; bias = rec["bias"]
@@ -1027,13 +1083,28 @@ def main():
10271083
rec, dec, f"Posit Standard 2022, n={rec['bits']}, es=2",
10281084
"NaR at 10..0; no separate inf; tapered precision")
10291085
bitexact += 1
1086+
elif cid == "takum8":
1087+
# takum8: dedicated logarithmic decoder, exhaustive 256 codes,
1088+
# correctly-rounded f64 (min gap 0.0135 x 0.5 ULP) -> bit-precise.
1089+
# Cross-checked vs libtakum/src/codec.c. [proven]
1090+
dec = make_takum_decoder(8)
1091+
pack = build_bitexact_pack(
1092+
rec, dec,
1093+
"Takum logarithmic (Hunhold 2024, arXiv:2404.18603): "
1094+
"value = exp(ell/2), exhaustive 256 codes, correctly-rounded f64",
1095+
"zero at 0x00; NaR at 0x80 (MSB-set); n<12 is below the nominal "
1096+
"takum standard threshold (recorded, not a decoder error)")
1097+
bitexact += 1
10301098
elif cid.startswith("takum"):
1031-
# takum: tapered logarithmic; decode is nontrivial -> structural
1099+
# takum16/32/64: logarithmic; values transcendental. Exhaustive
1100+
# correctly-rounded gap is NOT verifiable without an external
1101+
# libtakum oracle -> kept structural HONESTLY (no second witness).
10321102
pack = build_structural_pack(rec)
1033-
pack["structural_reason"] = ("Takum (Hunhold 2024) is a tapered "
1034-
"LOGARITHMIC format; its decode is not a plain S:E:M field. "
1035-
"It is the live FL-002 counterexample and is recorded "
1036-
"structurally pending a dedicated logarithmic decoder.")
1103+
pack["structural_reason"] = ("Takum (Hunhold 2024, arXiv:2404.18603) "
1104+
"is a tapered LOGARITHMIC format; its decode is not a plain "
1105+
"S:E:M field. takum8 is promoted to bit-precise (exhaustive); "
1106+
"this wider rung stays structural pending an external libtakum "
1107+
"oracle for the correctly-rounded gap proof.")
10371108
structural += 1
10381109
else:
10391110
pack = build_structural_pack(rec); structural += 1

conformance/vectors/takum16_conformance_v0.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,13 @@
1717
"standard": "Hunhold 2024",
1818
"use_case": "single-rule ladder counterexample",
1919
"gf_relation": "ally",
20-
"source": "Hunhold 2024 (arXiv:2412.20273)",
20+
"source": "Hunhold 2024 (arXiv:2404.18603)",
2121
"phi_distance": -1.0
2222
},
2323
"ssot": "https://github.com/gHashTag/t27/blob/master/conformance/FORMAT-SPEC-001.json",
2424
"preprint": "https://arxiv.org/abs/2606.05017",
2525
"anchor_identity": "phi^2 + 1/phi^2 = 3",
26-
"structural_reason": "Takum (Hunhold 2024) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. It is the live FL-002 counterexample and is recorded structurally pending a dedicated logarithmic decoder.",
26+
"structural_reason": "Takum (Hunhold 2024, arXiv:2404.18603) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. takum8 is promoted to bit-precise (exhaustive); this wider rung stays structural pending an external libtakum oracle for the correctly-rounded gap proof.",
2727
"anchor_note": "Anchor identity phi^2 + 1/phi^2 = 3 recorded per shared schema.",
2828
"n_vectors": 0,
2929
"vectors": []

conformance/vectors/takum32_conformance_v0.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
"ssot": "https://github.com/gHashTag/t27/blob/master/conformance/FORMAT-SPEC-001.json",
2424
"preprint": "https://arxiv.org/abs/2606.05017",
2525
"anchor_identity": "phi^2 + 1/phi^2 = 3",
26-
"structural_reason": "Takum (Hunhold 2024) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. It is the live FL-002 counterexample and is recorded structurally pending a dedicated logarithmic decoder.",
26+
"structural_reason": "Takum (Hunhold 2024, arXiv:2404.18603) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. takum8 is promoted to bit-precise (exhaustive); this wider rung stays structural pending an external libtakum oracle for the correctly-rounded gap proof.",
2727
"anchor_note": "Anchor identity phi^2 + 1/phi^2 = 3 recorded per shared schema.",
2828
"n_vectors": 0,
2929
"vectors": []

conformance/vectors/takum64_conformance_v0.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
"ssot": "https://github.com/gHashTag/t27/blob/master/conformance/FORMAT-SPEC-001.json",
2424
"preprint": "https://arxiv.org/abs/2606.05017",
2525
"anchor_identity": "phi^2 + 1/phi^2 = 3",
26-
"structural_reason": "Takum (Hunhold 2024) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. It is the live FL-002 counterexample and is recorded structurally pending a dedicated logarithmic decoder.",
26+
"structural_reason": "Takum (Hunhold 2024, arXiv:2404.18603) is a tapered LOGARITHMIC format; its decode is not a plain S:E:M field. takum8 is promoted to bit-precise (exhaustive); this wider rung stays structural pending an external libtakum oracle for the correctly-rounded gap proof.",
2727
"anchor_note": "Anchor identity phi^2 + 1/phi^2 = 3 recorded per shared schema.",
2828
"n_vectors": 0,
2929
"vectors": []

0 commit comments

Comments
 (0)