fdd0b72b7a
The complement to the per-function compare harness. Instead of "did this function's declared outputs match", it asks "is the entire simulation state still identical" -- so no region-declaration mistake can hide from it. Coverage is PROVED, not declared: the digest tree is re-serialised and compared byte-for-byte against the inflated save on every run. When that reconstruction reproduces the stream, the whole file is a function of the digest's inputs. A run that cannot account for the file says so and exits non-zero. This is the direct answer to B4's three hooks that printed "0 diverged" over an empty region set. It localises. The root is the fold of a per-subsystem / per-object tree with named objects, so the known load->re-save delta reports as exactly five leaves -- /Summary/Checksum and four /Sim/players/Player[...]/Status 4->0 -- naming the two Singularity players by id where the raw byte diff could only say "1st of two". One real End Turn reports as 108 fully attributed differences. Float-parity policy is explicit and strict by default (STATE_CHECKSUM.md 3): raw IEEE-754 bits; a `canonical` policy for signed zero and NaN payloads only; and deliberately NO tolerant hashing mode, because quantisation moves the cliff rather than removing it and destroys the roll-up. Tolerance lives in the differ as --ulps, applied after localisation. Corpus census: 0 NaN, 0 -0.0, 0 subnormals across 4,474 float leaves, so the strict default costs nothing today and a test fails the day that changes. Validated on the real saves (verify/results/state-checksum/): 10 files, 4 distinct contents, all STABLE + COVERED; chain record/verify works on the real turn1-3 saves. The VM-driven replay loop is designed (section 5) but UNRUN. Section 3.5 names the one question the host side cannot settle -- whether the turn pipeline depends on x87 intermediate precision -- and the experiment that would: force fpu_cw to 0x027f / 0x127f / 0x137f across End Turn and checksum the three autosaves. Also recorded: Summary.Checksum is NOT a byte sum over the inflated stream nor a sum over the int leaves (both ruled out), so nobody repeats those two. 38 tests; sots-engine untouched, clean_room_check.sh OK.
96 lines
3 KiB
Python
96 lines
3 KiB
Python
#!/usr/bin/env python3
|
|
"""float_census.py -- classify every float leaf in a set of saves.
|
|
|
|
This is the evidence behind the float-parity policy in STATE_CHECKSUM.md: it
|
|
says whether the corpus actually contains the values where a `bits` policy and
|
|
a `canonical` policy disagree (signed zero, NaN payloads), and whether it
|
|
contains the values where an x87 -> SSE port is most likely to drift
|
|
(subnormals, values at the edge of float32 range).
|
|
|
|
uv run python3 float_census.py SAVE...
|
|
"""
|
|
from __future__ import annotations
|
|
|
|
import collections
|
|
import math
|
|
import os
|
|
import struct
|
|
import sys
|
|
|
|
_HERE = os.path.dirname(os.path.abspath(__file__))
|
|
if _HERE not in sys.path:
|
|
sys.path.insert(0, _HERE)
|
|
|
|
import state_checksum as sc # noqa: E402
|
|
|
|
FLT_MIN_NORMAL = 1.1754943508222875e-38
|
|
FLT_MAX = 3.4028234663852886e38
|
|
|
|
|
|
def classify(raw: bytes) -> str:
|
|
(bits,) = struct.unpack("<I", raw)
|
|
(v,) = struct.unpack("<f", raw)
|
|
if bits == 0x80000000:
|
|
return "negative zero"
|
|
if v == 0.0:
|
|
return "positive zero"
|
|
if math.isnan(v):
|
|
return "NaN"
|
|
if math.isinf(v):
|
|
return "infinity"
|
|
if bits == 0x7F7FFFFF:
|
|
return "FLT_MAX (0x7f7fffff)"
|
|
if bits == 0xFF7FFFFF:
|
|
return "-FLT_MAX"
|
|
if abs(v) < FLT_MIN_NORMAL:
|
|
return "subnormal"
|
|
if v == int(v) and abs(v) < 2 ** 24:
|
|
return "exact integer"
|
|
return "ordinary"
|
|
|
|
|
|
def main(argv=None) -> int:
|
|
argv = list(sys.argv[1:] if argv is None else argv)
|
|
if not argv:
|
|
print("usage: float_census.py SAVE...", file=sys.stderr)
|
|
return 2
|
|
seen: set = set()
|
|
total = collections.Counter()
|
|
print("# float census -- classes that separate the 'bits' and 'canonical'")
|
|
print("# policies are: negative zero, NaN. Classes an x87 -> SSE port is")
|
|
print("# most likely to move are: subnormal, and anything near FLT_MAX.")
|
|
print()
|
|
for p in argv:
|
|
with open(p, "rb") as f:
|
|
data = f.read()
|
|
key = hash(data)
|
|
if key in seen:
|
|
continue
|
|
seen.add(key)
|
|
ck = sc.checksum_bytes(data, path=p, audit=False)
|
|
c = collections.Counter()
|
|
examples: dict = {}
|
|
for n in ck.root.walk():
|
|
if n.kind != "float":
|
|
continue
|
|
k = classify(n.raw)
|
|
c[k] += 1
|
|
examples.setdefault(k, n.path)
|
|
total += c
|
|
print(f"{os.path.basename(p)}: {sum(c.values())} float leaves")
|
|
for k, v in sorted(c.items(), key=lambda kv: -kv[1]):
|
|
print(f" {v:>6} {k:<24} e.g. {examples[k]}")
|
|
print()
|
|
print("all distinct saves combined:")
|
|
for k, v in sorted(total.items(), key=lambda kv: -kv[1]):
|
|
print(f" {v:>6} {k}")
|
|
print()
|
|
risky = total["negative zero"] + total["NaN"]
|
|
print(f"'canonical' would change {risky} leaf/leaves across the corpus "
|
|
f"({'a no-op today' if risky == 0 else 'NOT a no-op'}).")
|
|
print(f"subnormals: {total['subnormal']} (each one is an x87/SSE parity risk)")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|