sots-re/verify/results/shim/bu/claimcheck.py
alex 696935ea2a lane BU: H1 confirmed - the fleet-visit order is ascending fleet->Location, and the two-file outcome set is the two orderings of two heap pointers
Three fresh processes on ad-turn27 with the seeds pinned, hooking the two
single-caller per-element callees of the assignment walk.

  * ascending fleet->Location: 6 of 6 multi-element sequences
  * ascending element address (the committed prediction P3): 0 of 6
  * ascending fleet id / systemId / minimum ship id: 0 of 6 each

Three processes gave three different orders of the same six fleets, and every
difference is a pair whose Location addresses exchanged relative order. Runs 1
and 2 wrote byte-identical autosaves and still visited differently. Run 3
flipped the branch and its two Location addresses flipped with it: it is
byte-identical to lane BP's run B, runs 1 and 2 to BP's A and L.

So P3 is falsified as written and its hypothesis class, H1, is confirmed with
a sharper key. H1b is excluded on this path.

Second finding the static read had missed: the fleets already carry their new
ids when the walk first touches them, so the mint is upstream in the gather.
That moves the engine's canonicalisation point by one level.

rule 26(d) and rule 19 are both met by measurement rather than argument: an
instrumented pinned run reproduced an unpinned natural run byte for byte,
twice.
2026-09-09 03:38:22 -04:00

18 lines
1 KiB
Python

import re,sys
EL=re.compile(r"^aivisit claim call=(\d+) idx=(\d+) elem=(\S+) fid=(\d+) nships=(\d+) loc=(\S+) agent=(\S+) ships=\[([^\]]*)\]")
def nd(v): return all(v[i]<=v[i+1] for i in range(len(v)-1))
for path,label in zip(sys.argv[1::2],sys.argv[2::2]):
seqs={}
for ln in open(path):
m=EL.match(ln)
if m: seqs.setdefault(int(m.group(1)),[]).append((int(m.group(3),16),int(m.group(6),16),int(m.group(4)),[int(x) for x in m.group(8).split()]))
print(f"### {label} ({path})")
t=l=e=f=0
for c,rows in sorted(seqs.items()):
if len(rows)<2: continue
t+=1
L=nd([r[1] for r in rows]); E=nd([r[0] for r in rows]); F=nd([r[2] for r in rows])
l+=L; e+=E; f+=F
print(f" call={c} n={len(rows)} loc_asc={L} elem_asc={E} fid_asc={F}")
for r in rows: print(f" elem=0x{r[0]:08x} loc=0x{r[1]:08x} fid={r[2]:5d} ships={r[3][:3]}")
print(f" -> claim sequences with >1 element: {t} loc-ordered {l}/{t} elem-ordered {e}/{t} id-ordered {f}/{t}\n")