nx_robot_hal_gate.nx source
↩ module page · 131 lines · 5514 B
1// nx_robot_hal_gate.nx -- R-ROBO-5 GATE: the fail-safe hardware-write driver, never-brick PROVEN
2// MECHANICALLY (the proof #26 demands -- not a promise). VERIFIES:
3// (1) safe-default on init (all outputs 0);
4// (2) clamp HIGH: a huge command lands as exactly HW_SAFE_MAX;
5// (3) clamp LOW: a hugely-negative command lands as exactly HW_SAFE_MIN;
6// (4) pass-through: an in-envelope command lands unchanged;
7// (5) EXHAUSTIVE never-brick: sweep commands incl. extremes (+/-1e9) -- the actual written value is
8// ALWAYS within [HW_SAFE_MIN, HW_SAFE_MAX] (0 escapes -> the mechanical never-brick proof);
9// (6) e-stop latches and forces every output safe (0), and stays safe after;
10// (7) watchdog overrun auto-e-stops (fail-safe on a stalled loop);
11// (8) sensor range-check flags out-of-range readings invalid;
12// (9) NEGATIVE CONTROL: the raw (non-fail-safe) write path DOES escape the envelope -- proving the
13// clamp is what provides the guarantee.
14// 100% sovereign, integer-only. license_tier: ORIGINAL expect_exit: 0
15import "nx_syscalls.nx"
16import "nx_robot_hal.nx"
17
18func sw(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
19func sn(v: i64) -> i64 {
20 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 }
21 var m: i64 = v
22 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
23 let d: *u8 = sys_mmap(24); var k: i64 = 0
24 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
25 let o: *u8 = sys_mmap(24); var i: i64 = 0
26 while i < k { o[i] = d[k - 1 - i]; i = i + 1 }
27 sys_write(1, o, k); return 0
28}
29func check(name: *u8, cond: i64, tot: *i64) -> i64 {
30 if cond == 1 { sw(" ok " as *u8); tot[0] = tot[0] + 1 }
31 else { sw(" FAIL " as *u8); tot[1] = tot[1] + 1 }
32 sw(name); sw("\n" as *u8)
33 return 0
34}
35
36func main() -> i64 {
37 let tot: *i64 = sys_mmap(16) as *i64
38 tot[0] = 0; tot[1] = 0
39 sw("=== nx_robot_hal_gate R-ROBO-5 -- fail-safe hardware-write driver (never-brick PROVEN) ===\n" as *u8)
40
41 let hw: *i64 = hwd_new()
42
43 // (1) safe-default on init
44 var ok1: i64 = 1
45 var p: i64 = 0
46 while p < 32 { if hwd_out(hw, p) != 0 { ok1 = 0 } p = p + 1 }
47 check("safe-default on init: all outputs 0" as *u8, ok1, tot)
48
49 // (2) clamp high
50 let vh: i64 = hwd_drive(hw, 5, 100000)
51 sw(" drive(5, 100000) landed " as *u8); sn(vh); sw(" (SAFE_MAX=400)\n" as *u8)
52 var ok2: i64 = 0
53 if vh == 400 { if hwd_out(hw, 5) == 400 { ok2 = 1 } }
54 check("clamp HIGH: huge command lands as HW_SAFE_MAX (400)" as *u8, ok2, tot)
55
56 // (3) clamp low
57 let vl: i64 = hwd_drive(hw, 6, 0 - 100000)
58 sw(" drive(6, -100000) landed " as *u8); sn(vl); sw(" (SAFE_MIN=-400)\n" as *u8)
59 var ok3: i64 = 0
60 if vl == (0 - 400) { ok3 = 1 }
61 check("clamp LOW: hugely-negative command lands as HW_SAFE_MIN (-400)" as *u8, ok3, tot)
62
63 // (4) pass-through in-envelope
64 let vp: i64 = hwd_drive(hw, 7, 250)
65 var ok4: i64 = 0
66 if vp == 250 { ok4 = 1 }
67 check("pass-through: in-envelope command (250) lands unchanged" as *u8, ok4, tot)
68
69 // (5) EXHAUSTIVE never-brick sweep -- no command escapes the envelope
70 let hw2: *i64 = hwd_new()
71 var esc: i64 = 0
72 var u: i64 = 0 - 1000
73 while u <= 1000 {
74 let w: i64 = hwd_drive(hw2, 3, u)
75 if w > 400 { esc = 1 }
76 if w < (0 - 400) { esc = 1 }
77 u = u + 1
78 }
79 // plus extreme spot values
80 let e1: i64 = hwd_drive(hw2, 3, 1000000000)
81 let e2: i64 = hwd_drive(hw2, 3, 0 - 1000000000)
82 if e1 > 400 { esc = 1 }
83 if e2 < (0 - 400) { esc = 1 }
84 sw(" swept commands -1000..1000 + /-1e9; envelope escapes=" as *u8); sn(esc); sw("\n" as *u8)
85 var ok5: i64 = 0
86 if esc == 0 { ok5 = 1 }
87 check("EXHAUSTIVE never-brick: NO command escapes [-400,400] (mechanical proof)" as *u8, ok5, tot)
88
89 // (6) e-stop latches + forces safe
90 hwd_drive(hw, 8, 300)
91 hwd_estop(hw)
92 var ok6: i64 = 0
93 if hwd_out(hw, 8) == 0 {
94 let after: i64 = hwd_drive(hw, 8, 300) // estop latched -> still safe
95 if after == 0 { ok6 = 1 }
96 }
97 check("e-stop latches: forces outputs to 0 and stays safe after" as *u8, ok6, tot)
98
99 // (7) watchdog overrun auto-e-stops
100 let hw3: *i64 = hwd_new()
101 var t: i64 = 0
102 while t < 105 { hwd_wd_tick(hw3); t = t + 1 } // exceed HW_WD_LIMIT=100
103 var ok7: i64 = 0
104 if hwd_estopped(hw3) == 1 {
105 let drv: i64 = hwd_drive(hw3, 2, 300) // after watchdog estop -> safe
106 if drv == 0 { ok7 = 1 }
107 }
108 check("watchdog overrun AUTO-e-stops (fail-safe on stalled loop)" as *u8, ok7, tot)
109
110 // (8) sensor range-check
111 var ok8: i64 = 0
112 if hwd_sensor_invalid(2000) == 0 {
113 if hwd_sensor_invalid(0 - 1) == 1 {
114 if hwd_sensor_invalid(5000) == 1 { ok8 = 1 }
115 }
116 }
117 check("sensor range-check: in-range valid, out-of-range flagged invalid" as *u8, ok8, tot)
118
119 // (9) NEGATIVE CONTROL: raw write escapes the envelope
120 let hw4: *i64 = hwd_new()
121 let raw: i64 = hwd_drive_raw(hw4, 1, 100000)
122 sw(" raw write landed " as *u8); sn(hwd_out(hw4, 1)); sw(" (escapes envelope -> unsafe)\n" as *u8)
123 var ok9: i64 = 0
124 if hwd_out(hw4, 1) == 100000 { ok9 = 1 }
125 check("NEG-CONTROL: raw (non-fail-safe) write DOES escape envelope (clamp earns its keep)" as *u8, ok9, tot)
126
127 sw("=== VERDICT pass=" as *u8); sn(tot[0]); sw(" fail=" as *u8); sn(tot[1]); sw(" ===\n" as *u8)
128 if tot[1] == 0 { sys_exit(0) }
129 sys_exit(1)
130 return 1
131}