#!/usr/bin/env python3
"""Read exported native netlist; do not trust generator contract as reference."""
import hashlib,json,pathlib,xml.etree.ElementTree as E,itertools,argparse
P=pathlib.Path(__file__).resolve().parent

def verify(root):
 ns={n.get('name'):{(x.get('ref'),x.get('pin')) for x in n.findall('node')} for n in root.findall('nets/net')}
 pin_to_net={p:n for n,ps in ns.items() for p in ps}
 def net(ref,pin): return pin_to_net.get((ref,str(pin)))
 def eq(ref,pin,name):assert net(ref,pin)=='/'+name,(ref,pin,net(ref,pin),name)
 # Datasheet pins encoded independently of connection-contract.json.
 quad_channels=[(4,5,2),(6,7,1),(8,9,14),(10,11,13)] # IN-, IN+, OUT
 for ref,phase_ch in [('U2',[(0,'A','lo'),(1,'A','hi'),(2,'B','lo'),(3,'B','hi')]),('U3',[(0,'C','lo'),(1,'C','hi')])]:
  eq(ref,3,'DRV_AVDD');eq(ref,12,'GND')
  for ch,phase,side in phase_ch:
   minus,plus,out=quad_channels[ch]
   eq(ref,minus,'WIN_LO' if side=='lo' else 'ADC_I'+phase)
   eq(ref,plus,'ADC_I'+phase if side=='lo' else 'WIN_HI')
   eq(ref,out,'CUT_FAULT_N')
 for minus,plus,out in quad_channels[2:]:
  eq('U3',minus,'DRV_AVDD');eq('U3',plus,'GND');assert net('U3',out).startswith('unconnected-') and ns[net('U3',out)]=={('U3',str(out))}
 for ref in ['U8','U9']:
  eq(ref,1,'GND');eq(ref,2,'CUT_FAULT_N');eq(ref,3,'CTRL_3V3' if ref=='U8' else 'DRV_AVDD')
 for r,p,n in [('U4',1,'CUT_FAULT_N'),('U4',6,'CUT_CLEAR_N'),('U4',3,'ARM_RC'),('U4',4,'ARM_CLK'),('U4',5,'CTRL_3V3'),('U4',2,'GND'),('U5',1,'ARM_CLK'),('U5',2,'RUN_NOT'),('U5',6,'CUT_CLEAR_N'),('U5',7,'CTRL_3V3'),('U5',5,'CUT_PERMIT'),('U5',8,'CTRL_3V3'),('U5',4,'GND'),('U6',1,'RUN_BUF'),('U6',2,'CUT_PERMIT'),('U6',4,'DRV_RUN_GATED'),('U7',2,'RUN_BUF'),('U7',4,'RUN_NOT'),('U10',2,'DRV_RUN_REQ'),('U10',4,'RUN_BUF')]:eq(r,p,n)
 assert ns['/DRV_RUN_GATED']=={('U6','4'),('R5','1')}
 assert ns['/DRV_RUN_REQ']=={('J1','10'),('J4','1'),('R20','1'),('U10','2')}
 assert ns['/ARM_CLK']=={('U4','4'),('U5','1')}
 assert ns['/CUT_CLEAR_N']=={('U4','6'),('U5','6')}
 assert ns['/CUT_PERMIT']=={('U5','5'),('U6','2')}
 assert ns['/Q1_GATE']=={('Q1','1'),('R5','2'),('R6','1')}
 assert ns['/DRV_OFF']=={('U1','21'),('Q1','3'),('R15','2')}
 for r,p,n in [('R16',1,'DRV_AVDD'),('R16',2,'WIN_HI'),('R17',1,'WIN_HI'),('R17',2,'WIN_LO'),('R18',1,'WIN_LO'),('R18',2,'GND'),('R19',1,'CTRL_3V3'),('R19',2,'CUT_FAULT_N'),('R20',1,'DRV_RUN_REQ'),('R20',2,'GND'),('R21',1,'ARM_RAW'),('R21',2,'ARM_RC'),('R22',1,'ARM_RC'),('R22',2,'GND'),('J5',1,'CTRL_3V3'),('J5',2,'ARM_RAW')]:eq(r,p,n)
 for i,u in enumerate(['U2','U3','U4','U5','U6','U7','U8','U9','U10']):
  eq('C'+str(22+i),1,'DRV_AVDD' if u in ['U2','U3','U9'] else 'CTRL_3V3');eq('C'+str(22+i),2,'GND')
 values={c.get('ref'):c.findtext('value') for c in root.findall('components/comp')}
 assert [values[r] for r in ['R16','R17','R18']]==['14.0k 1%','10.7k 1%','14.0k 1%']
 assert values['R2']=='0R' and values['R3']=='10k 1%'
 assert next(c for c in root.findall('components/comp') if c.get('ref')=='R3').find("property[@name='dnp']") is not None
 assert all(values[r]=='TLV803EA29DBZR' for r in ['U8','U9'])
 assert all(values[r]=='TLV9024PWR' for r in ['U2','U3'])
 return ns

def logical_cases():
 # Event model assumes stable digital values at CLK and a valid CLEAR pulse.
 # Analog timing/metastability/slow rails are explicitly outside this model.
 traces=[]
 for source in ['A_lo','A_hi','B_lo','B_hi','C_lo','C_hi','CTRL_UV','AVDD_UV']:
  q=0
  def event(clear,clock,run):
   nonlocal q
   if not clear:q=0
   elif clock:q=1-run
   return q, q & run
  assert event(0,0,0)==(0,0) # power reset
  assert event(1,0,1)==(0,0) # RUN alone never arms
  assert event(1,1,1)==(0,0) # ARM with stable RUN high rejected
  assert event(1,1,0)==(1,0) # manual arm with RUN low
  assert event(1,0,1)==(1,1) # requested drive
  assert event(0,1,1)==(0,0) # clear dominates clock, even hung RUN
  assert event(1,0,1)==(0,0) # fault withdrawn cannot restart
  assert event(1,1,1)==(0,0) # repeated ARM still cannot restart hung RUN
  assert event(1,1,0)==(1,0)
  assert event(1,0,1)==(1,1)
  traces.append(source)
 return traces

def main():
 root=E.parse(P/'netlist-A85.xml').getroot(); ns=verify(root)
 # Mutation checks must reject a J4 bypass, a missing phase-C fault output,
 # an incorrectly swapped supervisor ground/reset and a wrong latch clear.
 mutations=[]
 for ref,pin,bad in [('J4','1','/DRV_RUN_GATED'),('U3','2','/GND'),('U9','2','/GND'),('U5','6','/CTRL_3V3')]:
  copy=E.fromstring(E.tostring(root));node=None
  for n in copy.findall('nets/net'):
   for x in list(n.findall('node')):
    if x.get('ref')==ref and x.get('pin')==pin:node=x;n.remove(x)
  assert node is not None
  target=next(n for n in copy.findall('nets/net') if n.get('name')==bad);target.append(node)
  try:verify(copy)
  except AssertionError:mutations.append(ref+'.'+pin)
  else:raise AssertionError('unsafe mutation accepted')
 erc=(P/'ERC_A85.rpt').read_text();assert '** ERC messages: 0  Errors 0  Warnings 0' in erc
 result={'status':'A85_NATIVE_NETLIST_AND_DIGITAL_LOGIC_PASS_NOT_HARDWARE','checked_nets':len(ns),'fault_sequences':logical_cases(),'unsafe_mutations_rejected':mutations,'native_ERC_zero':True,'pcb_updated':False,'independent_CPU_cutoff_schematic_connected':True,'independent_sensor_fault_coverage':False,'physical_delay_qualified':False,'manufacturing_release':False,'motor_run_permission':False,'source_sha256':{x.name:hashlib.sha256(x.read_bytes()).hexdigest() for x in [P/'drill_motor_a85_cutoff.kicad_sch',P/'Project.kicad_sym',P/'netlist-A85.xml']}}
 (P/'verification-A85.json').write_text(json.dumps(result,indent=2)+'\n');print(json.dumps(result))
if __name__=='__main__':main()
