"""Synthetic S-FTL-inspired representation accounting, not an FTL simulator.""" from hashlib import sha256 import json from pathlib import Path import sys def integer(value, minimum=0): if type(value) is not int or value < minimum: raise ValueError("expected an integer >= " + str(minimum)) return value def mapping(values): values = tuple(values) if not values: raise ValueError("empty translation page") for value in values: integer(value) if len(set(values)) != len(values): raise ValueError("live logical pages must map to distinct physical pages") return values def encode(values, labels=None): """One bit without labels; two bits with explicit base/local labels.""" values = mapping(values) two_bit = labels is not None labels = tuple(labels) if two_bit else (0,) * len(values) if len(labels) != len(values): raise ValueError("label count mismatch") if any(type(label) is not int or label not in (0, 1) for label in labels): raise ValueError("labels must be integer 0 or 1") heads, symbols, anchors = [], [], {} for i, (ppn, label) in enumerate(zip(values, labels)): if not two_bit: head = i == 0 or ppn != values[i - 1] + 1 else: anchor = anchors.get(label) # Only the base track can bridge an intervening local patch. head = (anchor is None or ppn != anchor[1] + i - anchor[0] or (label == 1 and (i == 0 or labels[i - 1] != 1))) if head: heads.append([i, ppn]) anchors[label] = (i, ppn) symbols.append(2 * int(head) + label if two_bit else int(head)) return {"bits_per_entry": 2 if two_bit else 1, "symbols": symbols, "heads": heads} def decode(encoded): bits = encoded["bits_per_entry"] if type(bits) is not int or bits not in (1, 2): raise ValueError("unsupported bitmap width") symbols, heads = encoded["symbols"], encoded["heads"] if not symbols: raise ValueError("empty bitmap") if any(type(s) is not int or s < 0 or s >= 2 ** bits for s in symbols): raise ValueError("invalid bitmap symbol") expected = [i for i, s in enumerate(symbols) if s >> (bits - 1)] if any(not isinstance(h, list) or len(h) != 2 for h in heads): raise ValueError("invalid head") for i, value in heads: integer(i) integer(value) if [h[0] for h in heads] != expected: raise ValueError("head positions do not match bitmap") positions, anchors, values = dict(heads), {}, [] previous_label = None for i, symbol in enumerate(symbols): label = symbol & 1 if bits == 2 else 0 is_head = bool(symbol >> (bits - 1)) if is_head: anchors[label] = (i, positions[i]) elif label not in anchors or (bits == 2 and label == 1 and previous_label != 1): raise ValueError("continuation without a valid head") start, ppn = anchors[label] # Logical distance includes positions occupied by the other track. values.append(ppn + i - start) previous_label = label return list(mapping(values)) def payload_bytes(encoded, ppn_bytes=4): """Bitmap plus packed head PPNs; excludes all other controller metadata.""" integer(ppn_bytes, 1) values = decode(encoded) if max(values) >= 256 ** ppn_bytes: raise ValueError("PPN does not fit the selected width") bitmap = (len(values) * encoded["bits_per_entry"] + 7) // 8 return bitmap + len(encoded["heads"]) * ppn_bytes def choose_form(current, bitmap_bytes, flat_bytes): if current not in ("flat", "bitmap"): raise ValueError("unknown representation") integer(bitmap_bytes) integer(flat_bytes, 1) if current == "flat" and 5 * bitmap_bytes < 4 * flat_bytes: return "bitmap" if current == "bitmap" and 10 * bitmap_bytes > 9 * flat_bytes: return "flat" return current def witness(name, values, labels): one, two = encode(values), encode(values, labels) if decode(one) != list(values) or decode(two) != list(values): raise RuntimeError("lossless round trip failed") return {"id": name, "mapping_ppn": list(values), "labels": list(labels), "one_bit": one, "two_bit": two, "one_bit_payload_bytes": payload_bytes(one), "two_bit_payload_bytes": payload_bytes(two), "flat_ppn_bytes": 4 * len(values)} def experiment(): rows = [ witness("contiguous", list(range(100, 108)), [0] * 8), witness("one_interior_patch", [100, 101, 102, 900, 901, 105, 106, 107], [0, 0, 0, 1, 1, 0, 0, 0]), witness("logical_order_without_physical_adjacency", list(range(100, 180, 10)), [0] * 8), witness("two_local_runs", [100, 900, 901, 103, 904, 905, 106, 107], [0, 1, 1, 0, 1, 1, 0, 0]), ] for patches in (0, 1, 16, 17): values, labels = list(range(10000, 10512)), [0] * 512 for k in range(patches): position = 2 + 4 * k values[position], labels[position] = 20000 + 4 * k, 1 rows.append(witness("512_entries_" + str(patches) + "_patches", values, labels)) return {"schema_version": 1, "evidence_class": "synthetic-representation-accounting", "model_sha256": sha256(Path(__file__).read_bytes()).hexdigest(), "assumptions": { "ppn_bytes": 4, "bitmap_packing": "byte-rounded", "head_payload": "PPNs only, in bitmap order", "excluded": ["directory", "allocation headers", "pointers", "alignment", "dirty state", "replacement metadata", "flash IO", "CPU time"], "labels": "supplied witness inputs, not a general label-selection policy", "claim": "lossless address reconstruction and idealized payload counts only"}, "cases": rows, "hysteresis": [ {"current": form, "bitmap_bytes": b, "flat_bytes": 100, "next": choose_form(form, b, 100)} for form in ("flat", "bitmap") for b in (79, 80, 85, 90, 91)]} if __name__ == "__main__": result = json.dumps(experiment(), indent=2) + "\n" if len(sys.argv) == 2 and sys.argv[1] == "--check": if json.loads(Path(__file__).with_name("results.json").read_text()) != json.loads(result): raise SystemExit("results.json is stale") print("results.json matches the canonical model") elif len(sys.argv) == 2 and sys.argv[1] == "--write": Path(__file__).with_name("results.json").write_text(result) elif len(sys.argv) == 1: print(result, end="") else: raise SystemExit("usage: model.py [--write|--check]")