`nx_robot_hal.nx` source

1// nx_robot_hal.nx -- SOVEREIGN fail-safe hardware-write DRIVER (the HAL the generated firmware binds
2// to). This is the never-brick-critical rung (#26): the layer that actually writes actuator outputs
3// and reads sensors. NEVER-BRICK BY CONSTRUCTION + proven MECHANICALLY by the gate (not promised):
4//   * every actuator write is CLAMPED to a safe envelope [HW_SAFE_MIN, HW_SAFE_MAX] before it lands
5//     -- no command, however large/negative/malicious, can escape it (defense-in-depth even if the
6//     firmware's own clamp were wrong);
7//   * pins default to SAFE (0 / disabled) on init;
8//   * a WATCHDOG forces an e-stop (all outputs safe) if not kicked;
9//   * E-STOP is latched and zeroes every output;
10//   * sensor readings are range-checked (out-of-range => invalid => firmware goes safe).
11// Backend here is a MOCK device (an i64 register array) so the whole chain is gate-provable WITHOUT
12// real hardware. HONEST: binding these to a real board's MMIO addresses (the actual GPIO/PWM/step
13// registers) is the final step and needs the bench -- but the fail-safe LOGIC is real + proven now.
14// State layout (i64 array hw): hw[0..HW_NP) = actual pin outputs; hw[HW_NP+p] = sensor[p];
15//   hw[2*HW_NP] = watchdog counter; hw[2*HW_NP+1] = estop latch.
16// license_tier: ORIGINAL  expect_exit: 0
17import "nx_syscalls.nx"
18
19const HW_NP:         i64 = 32
20const HW_SAFE_MAX:   i64 = 400      // actuator output ceiling (e.g. step-rate / current cap)
21const HW_SAFE_MIN:   i64 = 0 - 400
22const HW_SENSOR_MIN: i64 = 0
23const HW_SENSOR_MAX: i64 = 4095     // 12-bit ADC
24const HW_WD_LIMIT:   i64 = 100      // watchdog ticks before auto e-stop
25
26// allocate + safe-default a mock device (all outputs 0, estop clear, wd 0)
27func hwd_new() -> *i64 {
28    let hw: *i64 = sys_mmap((2 * HW_NP + 2) * 8) as *i64
29    var i: i64 = 0
30    while i < 2 * HW_NP + 2 { hw[i] = 0; i = i + 1 }
31    return hw
32}
33
34func hwd_init_pin(hw: *i64, pin: i64) -> i64 { hw[pin] = 0; return 0 }   // safe default
35
36// latched e-stop: set the flag AND force every output to safe (0)
37func hwd_estop(hw: *i64) -> i64 {
38    hw[2 * HW_NP + 1] = 1
39    var p: i64 = 0
40    while p < HW_NP { hw[p] = 0; p = p + 1 }
41    return 0
42}
43
44// FAIL-SAFE actuator write: honor e-stop, then CLAMP to the safe envelope BY CONSTRUCTION, then
45// land the value in the mock register. Returns the ACTUAL written value (always in-envelope).
46func hwd_drive(hw: *i64, pin: i64, u: i64) -> i64 {
47    var v: i64 = u
48    if hw[2 * HW_NP + 1] != 0 { v = 0 }          // e-stop latched -> safe
49    if v > HW_SAFE_MAX { v = HW_SAFE_MAX }        // never-brick clamp (high)
50    if v < HW_SAFE_MIN { v = HW_SAFE_MIN }        // never-brick clamp (low)
51    hw[pin] = v
52    return v
53}
54
55// UNSAFE raw write -- models a NON-fail-safe driver; used ONLY by the gate's negative control.
56func hwd_drive_raw(hw: *i64, pin: i64, u: i64) -> i64 { hw[pin] = u; return u }
57
58// read back the actual output that landed on a pin
59func hwd_out(hw: *i64, pin: i64) -> i64 { return hw[pin] }
60
61func hwd_set_sensor(hw: *i64, pin: i64, val: i64) -> i64 { hw[HW_NP + pin] = val; return 0 }
62func hwd_read_sensor(hw: *i64, pin: i64) -> i64 { return hw[HW_NP + pin] }
63
64// range-check a sensor reading: out-of-range => invalid (1) => firmware must go safe
65func hwd_sensor_invalid(s: i64) -> i64 {
66    if s < HW_SENSOR_MIN { return 1 }
67    if s > HW_SENSOR_MAX { return 1 }
68    return 0
69}
70
71// watchdog: kick to reset; tick each loop -- on overrun it auto-e-stops (fail-safe)
72func hwd_wd_kick(hw: *i64) -> i64 { hw[2 * HW_NP] = 0; return 0 }
73func hwd_wd_tick(hw: *i64) -> i64 {
74    hw[2 * HW_NP] = hw[2 * HW_NP] + 1
75    if hw[2 * HW_NP] > HW_WD_LIMIT { hwd_estop(hw) }
76    return 0
77}
78func hwd_estopped(hw: *i64) -> i64 { return hw[2 * HW_NP + 1] }
nx_robot_hal.nx source

`nx_robot_hal.nx` source
