#!/usr/bin/env python3
"""Train an int_synth decoder and emit the committable conformance vector `photo` of
`neural-conformance/`: the integer model (`int_synth.json`), a coded picture
(`latent.bin`, the wire payload), the integer-forward reference RGB (`ref_rgb.bin`) and
`meta.json`. The Rust decoder (`int_synth.rs`) reproduces the reference BIT-EXACTLY on
every machine: the determinism is exact by construction, and this vector shows it on a
model trained in float and quantised after training, not only on seeded weights.
**The pictures are generated here; the tool reads no image file.** The pictures the
decoder is trained on, and the picture the vector codes, are written by `picture()`
below from a seed: 128 × 128 RGB8 dead-leaves pictures. A picture starts as a vertical
gradient between two colours; then 400 discs are painted back to front, each with a
centre uniform over the picture, a radius ⌊32·16 / (16 + u)⌋ (at least 2) for u uniform
in 0..239, a colour each channel of which is uniform in 16..239, and a linear shading
⌊(gx·dx + gy·dy) / 8⌋ for gx, gy uniform in −3..3, where (dx, dy) is the pixel's offset
from the centre; then every sample gets noise uniform in −2..2, and every value is
clamped to 0..255. Every draw is a SplitMix64 counter stream keyed by (seed, stream),
and the generator is integer arithmetic only, so a seed gives the same pictures on
every machine and every Python. The coded picture is stream 0 of the seed and the
training pictures are streams 1 to N: the decoder never sees the picture it codes.
Pipeline (the working recipe; see wai_int_synth_train.py for why training through the
`>> shift` fails): float-train an autoencoder on the training pictures, with torch
seeded from the same seed, deterministic algorithms and a fixed thread count on the
CPU: Adam steps on batches drawn by a generator seeded from the same seed, the learning
rate falling to a tenth for the last quarter of the steps, on the squared error of the
decoder's output before the clamp, so that an output below 0 or above 1 still has a
gradient; then quantise the DECODER after training, with each layer's activation scale
measured on the training pictures (its largest magnitude over 127, and 1/255 at the
output), its shift the largest that keeps its weights within ±127, and its weight scale
the one that makes the shift carry that activation scale exactly, so the integer
pipeline tracks the float one. Encode
the coded picture through the float encoder, quantise the latent to int8, and decode it
through the EXPORTED INTEGER model in numpy, the same i64 arithmetic int_synth.rs runs
(scatter-accumulate, +bias, arithmetic `>> shift`, integer ReLU, clamp to 0..255).
That numpy decode is the reference the Rust decoder must match to max|Δ|=0.
python tools/wai_int_synth_real.py --out
[--seed S] [--pictures N] [--steps K]
python tools/wai_int_synth_real.py --picture-only [--seed S] [--stream K]
python tools/wai_int_synth_real.py --check
Training needs numpy and torch. `--picture-only` writes one generated picture as a
binary PPM, and `--check` regenerates the picture a committed vector codes from the
seed in its `meta.json`, requires the vector's reference decode (`ref_rgb.bin`) to
reconstruct it at the PSNR `meta.json` records, and requires the vector's record in the
corpus's `licences.json` to state the seed and streams `meta.json` records; both need
only the Python standard library. The committed vector's command is in
`neural-conformance/README.md`.
"""
from __future__ import annotations
import argparse
import hashlib
import json
import math
import struct
import sys
from pathlib import Path
SIDE = 128 # the pictures' side; the model's output size
DISCS = 400 # discs per picture
THREADS = 4 # fixed: CPU reductions depend on it
SEED = 20261104 # the committed vector's seed
PICTURES = 512 # training pictures: streams 1 to PICTURES
STEPS, BATCH, LR = 3000, 32, 2e-4
# ---- the generated pictures (integer arithmetic only) --------------------------------
M64 = (1 << 64) - 1
GOLDEN = 0x9E3779B97F4A7C15
def _mix64(x):
"""SplitMix64's finalizer."""
x &= M64
x = ((x ^ (x >> 30)) * 0xBF58476D1CE4E5B9) & M64
x = ((x ^ (x >> 27)) * 0x94D049BB133111EB) & M64
return x ^ (x >> 31)
class Rng:
"""A SplitMix64 stream, keyed by (seed, stream)."""
def __init__(self, seed, stream):
self.s = _mix64(seed * GOLDEN + stream * 0xD1B54A32D192ED03)
def next(self):
self.s = (self.s + GOLDEN) & M64
return _mix64(self.s)
def int(self, lo, hi):
"""Uniform integer in [lo, hi]."""
return lo + self.next() % (hi - lo + 1)
def picture(seed, stream, side=SIDE):
"""One dead-leaves picture as RGB8 bytes: rows top to bottom, pixels left to right,
R, G, B. The module docstring states the formula."""
r = Rng(seed, stream)
top = [r.int(16, 239) for _ in range(3)]
bottom = [r.int(16, 239) for _ in range(3)]
px = bytearray(side * side * 3)
for y in range(side):
row = [(top[c] * (side - 1 - y) + bottom[c] * y) // (side - 1) for c in range(3)]
for x in range(side):
p = (y * side + x) * 3
px[p:p + 3] = bytes(row)
rmax = side // 4
for _ in range(DISCS):
cx, cy = r.int(0, side - 1), r.int(0, side - 1)
rad = max(2, rmax * 16 // (16 + r.int(0, 239)))
base = [r.int(16, 239) for _ in range(3)]
gx, gy = r.int(-3, 3), r.int(-3, 3)
for y in range(max(0, cy - rad), min(side, cy + rad + 1)):
dy = y - cy
for x in range(max(0, cx - rad), min(side, cx + rad + 1)):
dx = x - cx
if dx * dx + dy * dy > rad * rad:
continue
shade = (gx * dx + gy * dy) // 8
p = (y * side + x) * 3
for c in range(3):
px[p + c] = min(255, max(0, base[c] + shade))
for i in range(len(px)):
px[i] = min(255, max(0, px[i] + r.int(-2, 2)))
return bytes(px)
def write_ppm(path, rgb, w, h):
Path(path).write_bytes(b"P6\n%d %d\n255\n" % (w, h) + bytes(rgb))
def psnr_db(a, b):
"""PSNR of two RGB8 buffers, in dB, from their integer sum of squared differences."""
assert len(a) == len(b) and len(a) > 0
sse = sum((x - y) * (x - y) for x, y in zip(a, b))
return 99.0 if sse == 0 else 10 * math.log10(255 * 255 * len(a) / sse)
# ---- the integer forward, byte-for-byte as int_synth.rs runs it ----
def conv_transpose2d_int(inp, layer):
import numpy as np
cin, hin, win = inp.shape
oc, k, s, p, op = layer["out_ch"], layer["k"], layer["stride"], layer["pad"], layer["out_pad"]
hout = (hin - 1) * s + k + op - 2 * p
wout = (win - 1) * s + k + op - 2 * p
W = np.array(layer["weight"], np.int64).reshape(cin, oc, k, k)
out = np.zeros((oc, hout, wout), np.int64)
for ky in range(k):
for kx in range(k):
# contribution of this kernel tap: (oc, hin, win)
contrib = np.einsum("iohw,ihw->ohw", W[:, :, ky, kx][:, :, None, None] + np.zeros((1, 1, hin, win), np.int64), inp)
ys = np.arange(hin) * s + ky - p
xs = np.arange(win) * s + kx - p
ym = (ys >= 0) & (ys < hout)
xm = (xs >= 0) & (xs < wout)
if not ym.any() or not xm.any():
continue
out[np.ix_(np.arange(oc), ys[ym], xs[xm])] += contrib[:, ym][:, :, xm]
b = np.array(layer["bias"], np.int64).reshape(oc, 1, 1)
out = (out + b) >> np.int64(layer["shift"]) # arithmetic shift, matches Rust i64 >>
if layer["relu"]:
out = np.maximum(out, 0)
return out
def decode_int(latent_i8, layers, h, w):
import numpy as np
cur = latent_i8.astype(np.int64)
for l in layers:
cur = conv_transpose2d_int(cur, l)
assert cur.shape[0] == 3 and cur.shape[1] == h and cur.shape[2] == w, cur.shape
return np.clip(cur, 0, 255).astype(np.uint8).transpose(1, 2, 0) # H,W,3
GENERATOR = "tools/wai_int_synth_real.py" # this tool, as a licence record names it
def licence_record_fails(vdir, meta):
"""The vector's record in the corpus's `licences.json` (two directories up) states
the pictures meta.json says the vector was made from: content generated by this
tool, the coded picture `seed S, stream K`, and the training pictures
`seed S, streams A to B` from meta.json's `training_streams`, a range that leaves
out the coded picture's stream."""
fails = []
seed, stream = meta["seed"], meta["stream"]
tr_streams = meta.get("training_streams")
if not (isinstance(tr_streams, list) and len(tr_streams) == 2
and all(isinstance(x, int) for x in tr_streams) and tr_streams[0] <= tr_streams[1]):
return [f"meta.json's training_streams {tr_streams!r} is not [first, last]"]
a, b = tr_streams
if a <= stream <= b:
fails.append(f"meta.json's training streams {a} to {b} include the coded picture's stream {stream}")
try:
records = json.loads((vdir.parent.parent / "licences.json").read_text())["vectors"]
rec = records[vdir.name]
tr = rec["training"]
except (OSError, ValueError, KeyError, TypeError) as e:
return fails + [f"licences.json has no record with a training record for {vdir.name} ({e!r})"]
want = {
"": f"the dead-leaves picture the tool generates from seed {seed}, stream {stream}",
"training ": f"the dead-leaves pictures the tool generates from seed {seed}, streams {a} to {b}",
}
for label, r in (("", rec), ("training ", tr)):
if not isinstance(r, dict):
fails.append(f"licences.json's {label}record for {vdir.name} is not an object")
continue
if r.get("content") != "generated" or r.get("generator") != GENERATOR:
fails.append(f"licences.json's {label}record for {vdir.name} does not say its content is "
f"generated by {GENERATOR}")
if r.get("input") != want[label]:
fails.append(f"licences.json's {label}input for {vdir.name} is {r.get('input')!r}; "
f"meta.json says {want[label]!r}")
return fails
def check(vdir):
"""The committed vector codes the picture its seed generates: its reference decode
(`ref_rgb.bin`, whose SHA-256 is the corpus's digest for the vector in
`sha256.json` two directories up) reconstructs that picture at the PSNR meta.json
records, to two decimals; and the vector's licence record states the pictures
meta.json says it was made from (`licence_record_fails`)."""
vdir = Path(vdir)
meta = json.loads((vdir / "meta.json").read_text())
w, h = meta["width"], meta["height"]
head = (vdir / "latent.bin").read_bytes()[:12]
ph, pw, _c, _s, _r = struct.unpack("= 0 keeps the weights within ±127; clamping them")
shift = 0
sw = sout / (sin * 2 ** shift)
layers.append({
"in_ch": c.in_channels, "out_ch": c.out_channels, "k": 5, "stride": 2, "pad": 2, "out_pad": 1,
"weight": torch.clamp(torch.round(c.weight.detach() / sw), -128, 127).to(torch.int64).reshape(-1).tolist(),
"bias": torch.round(c.bias.detach() / (sw * sin)).to(torch.int64).reshape(-1).tolist(),
"shift": shift, "relu": i < len(dec) - 1,
})
sin = sout
# ---- encode the coded picture → int8 latent → wire payload ----
with torch.no_grad():
lat = (enc(test) * 64.0)[0].numpy() # (C, LS, LS)
lat_i8 = np.clip(np.round(lat / s0), -128, 127).astype(np.int8)
out = Path(args.out)
out.mkdir(parents=True, exist_ok=True)
torch.save({"enc": enc.state_dict(), "dec": dec.state_dict()}, out / "float_model.pt")
(out / "int_synth.json").write_text(json.dumps({"layers": layers}, separators=(",", ":")))
# wire payload: u32 H, u32 W, u16 C, u8 S_log2, u8 reserved, then C*S*S int8
s_log2 = int(round(math.log2(LS)))
payload = struct.pack(" int:
ap = argparse.ArgumentParser(description="Train an int_synth decoder on generated pictures and write the corpus vector.")
ap.add_argument("--out", help="output dir: int_synth.json, latent.bin, ref_rgb.bin and meta.json (the vector), "
"two previews and the float model (float_model.pt)")
ap.add_argument("--seed", type=int, default=SEED)
ap.add_argument("--pictures", type=int, default=PICTURES, help="training pictures: streams 1 to N of the seed")
ap.add_argument("--chans", type=int, nargs="+", default=[96, 72, 48, 24, 3])
ap.add_argument("--latent-side", type=int, default=8)
ap.add_argument("--steps", type=int, default=STEPS, help="Adam steps, each on a batch drawn from the training pictures")
ap.add_argument("--batch", type=int, default=BATCH)
ap.add_argument("--lr", type=float, default=LR)
ap.add_argument("--picture-only", metavar="OUT.ppm", help="write one generated picture and exit")
ap.add_argument("--stream", type=int, default=0, help="with --picture-only: 0 the coded picture, 1 to N the training pictures")
ap.add_argument("--check", metavar="VECTOR_DIR", help="check that a committed vector codes the picture its seed generates")
args = ap.parse_args()
if args.check:
return check(args.check)
if args.picture_only:
write_ppm(args.picture_only, picture(args.seed, args.stream), SIDE, SIDE)
return 0
if not args.out:
ap.error("--out is required unless --picture-only or --check is given")
return train(args)
if __name__ == "__main__":
raise SystemExit(main())