nx_batt_recondition_test.nx source

1import "nx_gate_gn.nx" 2// nx_batt_recondition_test.nx -- gate for R2. Proves: each verdict drives the right staged restore; rejects/retires 3// are NEVER charged; an over-rate or over-voltage plan is REFUSED by the spine (never-ignite enforced in the 4// WORKFLOW, not just the primitive); the refusal IS the spine's refusal (delegation proven); and the full R1->R2 5// chain works (triage -> recondition). expect_exit: 0 6import "nx_syscalls.nx" 7import "nx_intent.nx" 8import "nx_battery_safety.nx" 9import "nx_batt_intake.nx" 10import "nx_batt_recondition.nx" 11 12func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 13// safe envelope: 2A charge, 5A discharge, 60C, 3.0-4.2V 14func mk_env() -> *NxBatterySafetyEnvelope { return nx_battery_safety_envelope_new(1, 2000, 5000, 60000, 3000, 4200) } 15func mk_log() -> *NxBatteryCommandLog { return nx_battery_command_log_new(16) } 16func mk_spec() -> *IntakeSpec { 17 let s: *IntakeSpec = (sys_mmap(128)) as *IntakeSpec 18 s.unsafe_cell_floor_mv = 2000; s.healthy_cell_min_mv = 3000; s.healthy_cell_max_mv = 4250 19 s.soh_retire_permille = 700; s.max_imbalance_mv = 100; s.max_ir_mohm = 150 20 s.temp_min_mc = 0; s.temp_max_mc = 45000; s.recell_max_bad = 3 21 return s 22} 23func mk_pack() -> *PackState { 24 let p: *PackState = (sys_mmap(128)) as *PackState 25 p.n_cells = 10; p.min_cell_mv = 3700; p.max_cell_mv = 3720; p.n_bad_cells = 0 26 p.rated_capacity_mah = 2500; p.measured_capacity_mah = 2400; p.max_ir_mohm = 40 27 p.pack_temp_mc = 25000; p.terminal_mv = 37000; p.swollen = 0 28 return p 29} 30 31func main() -> i64 { 32 var pass: i64=0; var fail: i64=0 33 let st: *i64 = sys_mmap(8) as *i64 34 gp("=== nx_batt_recondition_test: R2 staged restore, every step routed through the never-ignite spine ===\n" as *u8) 35 36 // T1 RECONDITION safe -> RESTORED, 4 steps 37 let r1: i64 = nx_recondition_run(NX_BI_RECONDITION, mk_env(), mk_log(), 1500, 3700, 1000, st) 38 gp(" T1 RECONDITION safe -> verdict " as *u8); gn(r1); gp(" steps " as *u8); gn(st[0]); gp(" (exp 0 / 4)\n" as *u8) 39 if r1==NX_RW_DONE_RESTORED { if st[0]==4 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 40 41 // T2 BMS_RESET safe -> RESTORED, 1 step 42 let r2: i64 = nx_recondition_run(NX_BI_BMS_RESET, mk_env(), mk_log(), 800, 3700, 1000, st) 43 gp(" T2 BMS_RESET safe -> verdict " as *u8); gn(r2); gp(" steps " as *u8); gn(st[0]); gp(" (exp 0 / 1)\n" as *u8) 44 if r2==NX_RW_DONE_RESTORED { if st[0]==1 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 45 46 // T3 RECELL safe -> RESTORED, 6 steps 47 let r3: i64 = nx_recondition_run(NX_BI_RECELL, mk_env(), mk_log(), 1500, 3700, 1000, st) 48 gp(" T3 RECELL safe -> verdict " as *u8); gn(r3); gp(" steps " as *u8); gn(st[0]); gp(" (exp 0 / 6)\n" as *u8) 49 if r3==NX_RW_DONE_RESTORED { if st[0]==6 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 50 51 // T4 UNSAFE_REJECT -> RETIRED, NEVER charged (0 steps) -- the key safety proof 52 let r4: i64 = nx_recondition_run(NX_BI_UNSAFE_REJECT, mk_env(), mk_log(), 1500, 3700, 1000, st) 53 gp(" T4 UNSAFE_REJECT -> verdict " as *u8); gn(r4); gp(" steps " as *u8); gn(st[0]); gp(" (exp 1 / 0 = retired, never charged)\n" as *u8) 54 if r4==NX_RW_DONE_RETIRED { if st[0]==0 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 55 56 // T5 RETIRE_RECYCLE -> RETIRED, 0 steps 57 let r5: i64 = nx_recondition_run(NX_BI_RETIRE_RECYCLE, mk_env(), mk_log(), 1500, 3700, 1000, st) 58 gp(" T5 RETIRE_RECYCLE -> verdict " as *u8); gn(r5); gp(" steps " as *u8); gn(st[0]); gp(" (exp 1 / 0)\n" as *u8) 59 if r5==NX_RW_DONE_RETIRED { if st[0]==0 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 60 61 // T6 PASS_HEALTHY -> RESTORED, 0 steps 62 let r6: i64 = nx_recondition_run(NX_BI_PASS_HEALTHY, mk_env(), mk_log(), 1500, 3700, 1000, st) 63 gp(" T6 PASS_HEALTHY -> verdict " as *u8); gn(r6); gp(" steps " as *u8); gn(st[0]); gp(" (exp 0 / 0)\n" as *u8) 64 if r6==NX_RW_DONE_RESTORED { if st[0]==0 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 65 66 // T7 NEVER-IGNITE: RECONDITION but charge 3000mA > 2000 ceiling -> REFUSED_UNSAFE, 0 steps completed 67 let r7: i64 = nx_recondition_run(NX_BI_RECONDITION, mk_env(), mk_log(), 3000, 3700, 1000, st) 68 gp(" T7 over-rate charge -> verdict " as *u8); gn(r7); gp(" steps " as *u8); gn(st[0]); gp(" (exp 2 / 0 = refused at the wall)\n" as *u8) 69 if r7==NX_RW_REFUSED_UNSAFE { if st[0]==0 { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 70 71 // T8 voltage wall: RECONDITION at 4500mV > 4200 -> REFUSED_UNSAFE 72 let r8: i64 = nx_recondition_run(NX_BI_RECONDITION, mk_env(), mk_log(), 1500, 4500, 1000, st) 73 gp(" T8 over-voltage -> verdict " as *u8); gn(r8); gp(" (exp 2 REFUSED_UNSAFE)\n" as *u8) 74 if r8==NX_RW_REFUSED_UNSAFE { pass=pass+1 } else { fail=fail+1 } 75 76 // T9 composition/delegation: the spine refuses the over-rate directly, and the workflow's refusal IS that refusal 77 let direct: i64 = nx_battery_validate_command(mk_env(), NX_INTENT_DEFENSIVE, NX_BC_CHARGE, 3000, 3700, mk_log(), 1000) 78 gp(" T9 delegate: spine direct=" as *u8); gn(direct); gp(" (exp " as *u8); gn(NX_BS_REFUSED_RATE_CEILING); gp("), workflow=" as *u8); gn(r7); gp("\n" as *u8) 79 if direct==NX_BS_REFUSED_RATE_CEILING { if r7==NX_RW_REFUSED_UNSAFE { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } 80 81 // T10 FULL R1->R2 CHAIN: a swollen pack triages UNSAFE -> reconditions to RETIRED (never charged); 82 // a healthy-imbalanced pack triages RECONDITION -> reconditions to RESTORED. 83 let spec: *IntakeSpec = mk_spec() 84 let bad: *PackState = mk_pack(); bad.swollen = 1 85 let vbad: i64 = nx_batt_triage(bad, spec) 86 let rbad: i64 = nx_recondition_run(vbad, mk_env(), mk_log(), 1500, 3700, 1000, st) 87 let imb: *PackState = mk_pack(); imb.min_cell_mv = 3500; imb.max_cell_mv = 3750 88 let vimb: i64 = nx_batt_triage(imb, spec) 89 let rimb: i64 = nx_recondition_run(vimb, mk_env(), mk_log(), 1500, 3700, 1000, st) 90 gp(" T10 chain: swollen triage=" as *u8); gn(vbad); gp("->recon=" as *u8); gn(rbad); gp("(retire) ; imbalance triage=" as *u8); gn(vimb); gp("->recon=" as *u8); gn(rimb); gp("(restore)\n" as *u8) 91 if vbad==NX_BI_UNSAFE_REJECT { if rbad==NX_RW_DONE_RETIRED { if vimb==NX_BI_RECONDITION { if rimb==NX_RW_DONE_RESTORED { pass=pass+1 } else { fail=fail+1 } } else { fail=fail+1 } } else { fail=fail+1 } } else { fail=fail+1 } 92 93 // LIAR-KILL: same RECONDITION verdict, safe vs over-rate -> verdict MUST flip RESTORED->REFUSED 94 let la: i64 = nx_recondition_run(NX_BI_RECONDITION, mk_env(), mk_log(), 1500, 3700, 1000, st) 95 let lb: i64 = nx_recondition_run(NX_BI_RECONDITION, mk_env(), mk_log(), 9000, 3700, 1000, st) 96 gp(" LIAR safe=" as *u8); gn(la); gp(" over-rate=" as *u8); gn(lb); gp(" (must be 0 then 2)\n" as *u8) 97 if la==NX_RW_DONE_RESTORED { if lb==NX_RW_REFUSED_UNSAFE { pass=pass+1 } else { fail=fail+1; gp(" FAIL liar\n" as *u8) } } else { fail=fail+1; gp(" FAIL liar-base\n" as *u8) } 98 99 gp("BATT-RECONDITION pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail) 100 if fail==0 { gp(" verdict=GREEN (staged restore + rejects-never-charged + over-rate/voltage refused by the spine + R1->R2 chain)\n" as *u8); sys_exit(0); return 0 } 101 gp(" verdict=RED\n" as *u8); sys_exit(1); return 1 102}