File size: 4,337 Bytes
3579fb4 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 | """The recipe codec on every short string and at every boundary of the format.
Checked for both encoders: the round trip, the length bound of the completeness
lemma, and that the reserved tag 128 is never emitted. The boundaries covered
are the 127-byte literal cap and the run lengths that map to the extreme repeat
tags, together with exhaustive coverage at small lengths.
"""
import itertools
import json
import os
import random
import sys
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from selfrep import describe, describe_literal, decode
REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
def runs_path(name: str) -> str:
d = os.path.join(REPO, "paper", "runs")
os.makedirs(d, exist_ok=True)
return os.path.join(d, name)
def bound(n: int) -> int:
return n + -(-n // 127) + 1
def tags(tape: bytes):
i, out = 0, []
while True:
t = tape[i]
out.append(t)
i += 1
if t == 0:
return out
i += t if t <= 127 else 1
class Audit:
def __init__(self):
self.n = 0
self.roundtrip = []
self.overlong = []
self.not_tight = []
self.tag128 = []
def check(self, b: bytes) -> None:
self.n += 1
for enc in (describe, describe_literal):
r = enc(b)
if decode(r) != b:
self.roundtrip.append((enc.__name__, len(b)))
if len(r) > bound(len(b)):
self.overlong.append((enc.__name__, len(b), len(r)))
if len(describe_literal(b)) != bound(len(b)):
self.not_tight.append(len(b))
if 128 in tags(describe(b)):
self.tag128.append(len(b))
@property
def ok(self) -> bool:
return not (self.roundtrip or self.overlong or self.not_tight or self.tag128)
def main() -> int:
a = Audit()
for n in range(0, 15):
for t in itertools.product((0, 1), repeat=n):
a.check(bytes(t))
binary = a.n
for n in range(0, 10):
for t in itertools.product((0, 1, 2), repeat=n):
a.check(bytes(t))
ternary = a.n - binary
print(f" exhaustive: {binary:,} binary strings to length 14, "
f"{ternary:,} ternary to length 9")
edges = (list(range(0, 12))
+ [126, 127, 128, 129, 130, 251, 252, 253, 254, 255, 256, 257,
380, 381, 382, 508, 509, 510])
before = a.n
for L in edges:
a.check(bytes([0x41]) * L)
a.check(bytes([0x00]) * L)
a.check(bytes([0xFF]) * L)
a.check(bytes(range(256))[:L] if L <= 256 else bytes(range(256)) * (L // 256))
a.check(bytes([0x41] * L + [0x42]))
a.check(bytes([0x42] + [0x41] * L))
a.check(bytes([0x41] * L + [0x42] * L))
a.check(bytes(([0x41] * 4 + [0x42]) * max(1, L)))
a.check(bytes(([0x41] * 3 + [0x42]) * max(1, L)))
print(f" boundaries: {a.n - before:,} strings straddling the literal cap, "
f"the extreme repeat tags, and the run/literal transitions")
rng = random.Random(11)
before = a.n
for _ in range(4000):
n = rng.randrange(0, 900)
alpha = rng.choice([2, 3, 7, 256])
a.check(bytes(rng.randrange(alpha) for _ in range(n)))
for _ in range(1500):
n = rng.randrange(0, 900)
out = bytearray()
while len(out) < n:
out += bytes([rng.randrange(256)]) * rng.choice([1, 2, 3, 4, 5, 126, 127, 128, 253])
a.check(bytes(out[:n]))
print(f" random and run-structured: {a.n - before:,} strings")
print(f" total {a.n:,}: round-trip exact, neither encoder exceeds "
f"|f| + ceil(|f|/127) + 1, the literal encoder attains it, "
f"tag 128 never emitted: {'yes' if a.ok else 'NO'}")
if not a.ok:
print(" roundtrip:", a.roundtrip[:5])
print(" overlong:", a.overlong[:5])
print(" not tight:", a.not_tight[:5])
print(" tag128:", a.tag128[:5])
json.dump({"strings": a.n, "roundtrip_failures": len(a.roundtrip),
"bound_failures": len(a.overlong),
"literal_not_tight": len(a.not_tight),
"tag128_emitted": len(a.tag128)},
open(runs_path("paper_codec.json"), "w"), indent=1)
return 0 if a.ok else 1
if __name__ == "__main__":
sys.exit(main())
|