code wiki / _hdl_build / nx_batt_intake_test.nx
nx_batt_intake_test.nx source
↩ module page · 109 lines · 5152 B
1import "nx_gate_gn.nx"
2// nx_batt_intake_test.nx -- gate for R1 pack triage. One KAT per verdict branch + bad-arg + a LIAR-KILL (the
3// safety screen must be load-bearing: the same pack flips PASS->REJECT when swollen) + a COMPOSITION PROOF (the
4// triage's SoH equals the nx_consumable kernel's remaining_permille = real reuse, not asserted). expect_exit: 0
5import "nx_syscalls.nx"
6import "nx_batt_intake.nx"
7import "nx_consumable.nx"
8
9func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10
11func mk_spec() -> *IntakeSpec {
12 let s: *IntakeSpec = (sys_mmap(128)) as *IntakeSpec
13 s.unsafe_cell_floor_mv = 2000
14 s.healthy_cell_min_mv = 3000
15 s.healthy_cell_max_mv = 4250
16 s.soh_retire_permille = 700
17 s.max_imbalance_mv = 100
18 s.max_ir_mohm = 150
19 s.temp_min_mc = 0
20 s.temp_max_mc = 45000
21 s.recell_max_bad = 3
22 return s
23}
24
25func mk_healthy() -> *PackState {
26 let p: *PackState = (sys_mmap(128)) as *PackState
27 p.n_cells = 10
28 p.min_cell_mv = 3700
29 p.max_cell_mv = 3720
30 p.n_bad_cells = 0
31 p.rated_capacity_mah = 2500
32 p.measured_capacity_mah = 2400
33 p.max_ir_mohm = 40
34 p.pack_temp_mc = 25000
35 p.terminal_mv = 37000
36 p.swollen = 0
37 return p
38}
39
40func main() -> i64 {
41 var pass: i64=0; var fail: i64=0
42 let spec: *IntakeSpec = mk_spec()
43 gp("=== nx_batt_intake_test: R1 pack triage (safety-first, data-driven) ===\n" as *u8)
44
45 let p1: *PackState = mk_healthy(); p1.swollen = 1
46 let v1: i64 = nx_batt_triage(p1, spec)
47 gp(" KAT1 swollen -> " as *u8); gn(v1); gp(" exp 0 UNSAFE-REJECT\n" as *u8)
48 if v1==NX_BI_UNSAFE_REJECT { pass=pass+1 } else { fail=fail+1 }
49
50 let p2: *PackState = mk_healthy(); p2.min_cell_mv = 1500
51 let v2: i64 = nx_batt_triage(p2, spec)
52 gp(" KAT2 cell<floor -> " as *u8); gn(v2); gp(" exp 0 UNSAFE-REJECT\n" as *u8)
53 if v2==NX_BI_UNSAFE_REJECT { pass=pass+1 } else { fail=fail+1 }
54
55 let p3: *PackState = mk_healthy(); p3.measured_capacity_mah = 1500
56 let v3: i64 = nx_batt_triage(p3, spec)
57 gp(" KAT3 SoH600 no-bad -> " as *u8); gn(v3); gp(" exp 1 RETIRE-RECYCLE\n" as *u8)
58 if v3==NX_BI_RETIRE_RECYCLE { pass=pass+1 } else { fail=fail+1 }
59
60 let p4: *PackState = mk_healthy(); p4.n_bad_cells = 2
61 let v4: i64 = nx_batt_triage(p4, spec)
62 gp(" KAT4 2 bad cells -> " as *u8); gn(v4); gp(" exp 2 RE-CELL\n" as *u8)
63 if v4==NX_BI_RECELL { pass=pass+1 } else { fail=fail+1 }
64
65 let p5: *PackState = mk_healthy(); p5.terminal_mv = 0
66 let v5: i64 = nx_batt_triage(p5, spec)
67 gp(" KAT5 terminal 0V -> " as *u8); gn(v5); gp(" exp 3 BMS-RESET\n" as *u8)
68 if v5==NX_BI_BMS_RESET { pass=pass+1 } else { fail=fail+1 }
69
70 let p6: *PackState = mk_healthy(); p6.min_cell_mv = 3500; p6.max_cell_mv = 3750
71 let v6: i64 = nx_batt_triage(p6, spec)
72 gp(" KAT6 imbalance 250 -> " as *u8); gn(v6); gp(" exp 4 RECONDITION\n" as *u8)
73 if v6==NX_BI_RECONDITION { pass=pass+1 } else { fail=fail+1 }
74
75 let p7: *PackState = mk_healthy()
76 let v7: i64 = nx_batt_triage(p7, spec)
77 gp(" KAT7 healthy -> " as *u8); gn(v7); gp(" exp 5 PASS-HEALTHY\n" as *u8)
78 if v7==NX_BI_PASS_HEALTHY { pass=pass+1 } else { fail=fail+1 }
79
80 let p8: *PackState = mk_healthy(); p8.rated_capacity_mah = 0
81 let v8: i64 = nx_batt_triage(p8, spec)
82 gp(" KAT8 rated=0 -> " as *u8); gn(v8); gp(" exp 6 BAD-ARG\n" as *u8)
83 if v8==NX_BI_BAD_ARG { pass=pass+1 } else { fail=fail+1 }
84
85 // LIAR-KILL: same pack, swollen flipped -> verdict MUST change PASS(5)->REJECT(0).
86 let p9: *PackState = mk_healthy()
87 let v9a: i64 = nx_batt_triage(p9, spec)
88 p9.swollen = 1
89 let v9b: i64 = nx_batt_triage(p9, spec)
90 gp(" LIAR healthy=" as *u8); gn(v9a); gp(" swollen=" as *u8); gn(v9b); gp(" (must be 5 then 0)\n" as *u8)
91 if v9a==NX_BI_PASS_HEALTHY { if v9b==NX_BI_UNSAFE_REJECT { pass=pass+1 } else { fail=fail+1; gp(" FAIL liar\n" as *u8) } } else { fail=fail+1; gp(" FAIL liar-base\n" as *u8) }
92
93 // COMPOSITION PROOF: triage SoH == nx_consumable kernel SoH (real reuse-consistency).
94 let px: *PackState = mk_healthy(); px.measured_capacity_mah = 1800
95 let soh_lib: i64 = nx_bi_soh_permille(px)
96 let cs: *ConsSpec = (sys_mmap(64)) as *ConsSpec
97 cs.rated_life = px.rated_capacity_mah; cs.soon_permille = 0; cs.overdue_permille = 1000
98 let ce: *ConsEff = (sys_mmap(64)) as *ConsEff
99 let dummy: *i64 = (sys_mmap(8)) as *i64
100 var lost: i64 = px.rated_capacity_mah - px.measured_capacity_mah
101 if lost < 0 { lost = 0 }
102 nx_cons_analyze(dummy, dummy, 0, lost, cs, ce)
103 gp(" COMPOSE soh_lib=" as *u8); gn(soh_lib); gp(" soh_consumable=" as *u8); gn(ce.remaining_permille); gp(" (must match)\n" as *u8)
104 if soh_lib==ce.remaining_permille { pass=pass+1 } else { fail=fail+1; gp(" FAIL compose-mismatch\n" as *u8) }
105
106 gp("BATT-INTAKE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail)
107 if fail==0 { gp(" verdict=GREEN (every triage branch + bad-arg + liar-kill + nx_consumable composition proven)\n" as *u8); sys_exit(0); return 0 }
108 gp(" verdict=RED\n" as *u8); sys_exit(1); return 1
109}