File size: 4,695 Bytes
4a3e194 | 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 | """The device against Definition 2.8 of the paper.
Definition 2.8 specifies one device application on the
post-instruction state (x, tau, h, omega):
(i) if y[c_wr] = 1 then omega' = omega . y[R_out] and x'[R_out] = 0,
otherwise omega' = omega;
(ii) if y[c_rd] = 1 and h < |tau| then x'[R_in] = tau[h], x'[c_eot] = 0,
h' = h + 1; if y[c_rd] = 1 and h = |tau| then x'[c_eot] = 1 and h' = h;
if y[c_rd] = 0 then h' = h;
(iii) if y[c_rw] = 1 then h' = 0;
(iv) finally x'[c_rd] = x'[c_rw] = x'[c_wr] = 0.
The clauses are transcribed here independently of selfrep.Tape and the two are
compared over the whole cross product of request values, head positions and
tapes. The sweep covers non-unit values, so it also decides whether a request
fires on the value 1 alone.
"""
import itertools
import json
import os
import sys
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
from selfrep import Tape, C_WR, C_EOT, C_RW, C_RD, R_IN, R_OUT
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 spec(mem, tau, h, omega):
"""Definition 2.8, clause by clause, on (mem, h, omega)."""
m = list(mem)
w = list(omega)
if m[C_WR] == 1: # (i)
w.append(m[R_OUT])
m[R_OUT] = 0
hp = h
if m[C_RD] == 1: # (ii)
if h < len(tau):
m[R_IN] = tau[h]
m[C_EOT] = 0
hp = h + 1
else:
m[C_EOT] = 1
if m[C_RW] == 1: # (iii)
hp = 0
m[C_WR] = m[C_RD] = m[C_RW] = 0 # (iv)
return m, hp, w
def main() -> int:
tapes = [b"", b"\x07", b"\x01\x02", bytes(range(5)), bytes(range(64))]
vals = (0, 1, 2, 3, 127, 128, 255)
bad, n = [], 0
for tau in tapes:
heads = sorted({0, 1, max(0, len(tau) - 1), len(tau)})
for h in heads:
for wr, rd, rw in itertools.product(vals, repeat=3):
for eot, rin, rout in ((0, 0, 0), (1, 9, 200), (0, 255, 1), (1, 1, 255)):
mem = [0] * 256
mem[C_WR], mem[C_RD], mem[C_RW] = wr, rd, rw
mem[C_EOT], mem[R_IN], mem[R_OUT] = eot, rin, rout
mem[0x10] = 0xAB # an ordinary cell, must not move
want_mem, want_h, want_out = spec(mem, tau, h, b"")
dev = Tape(tau)
dev.h = h
got_mem = list(mem)
dev.apply(got_mem)
n += 1
if (got_mem != want_mem or dev.h != want_h
or bytes(dev.out) != bytes(want_out)):
bad.append({"tau": len(tau), "h": h, "wr": wr, "rd": rd,
"rw": rw, "eot": eot,
"spec": (want_mem[C_EOT], want_mem[R_IN],
want_mem[R_OUT], want_h, list(want_out)),
"impl": (got_mem[C_EOT], got_mem[R_IN],
got_mem[R_OUT], dev.h, list(dev.out))})
print(f" device applications compared: {n:,}")
print(f" implementation agrees with Definition 2.8 on every one: "
f"{'yes' if not bad else f'NO ({len(bad)} disagreements)'}")
for b in bad[:5]:
print(" ", b)
# A request fires on the value 1 and on no other value. The head starts off
# zero so that a rewind is observable; without that a rewind of a head
# already at 0 changes nothing and the test would not see it fire.
fires = []
for cell in (C_WR, C_RD, C_RW):
for v in range(256):
mem = [0] * 256
mem[cell] = v
mem[R_OUT] = 0x5A
dev = Tape(b"\x11\x22")
dev.h = 1
before = (dev.h, len(dev.out))
dev.apply(mem)
acted = (dev.h, len(dev.out)) != before or mem[R_IN] != 0 or mem[C_EOT] != 0
if acted != (v == 1):
fires.append((cell, v, acted))
print(f" each request fires exactly on the value 1, over all 256 cell values: "
f"{'yes' if not fires else f'NO {fires[:5]}'}")
ok = not bad and not fires
json.dump({"applications": n, "disagreements": len(bad),
"value_trigger_failures": len(fires)},
open(runs_path("paper_device.json"), "w"), indent=1)
return 0 if ok else 1
if __name__ == "__main__":
sys.exit(main())
|