BUILDS / ENFORCER / V1
enforcer
Holds a supply's output under the limits in lab/limits.toml, below any agent. It measures the output itself, sends the supply only setpoints within the limits, and drives a switch that is open unless it holds it closed. A comparator opens the switch by itself if the supply rises past its threshold, whatever the firmware does.
Parts
| QTY | PART | FORM | |
|---|---|---|---|
| 1 | RP2350 | board with the Pico 2 pinout | authorized sellers only |
| 1 | INA239 | VSSOP-10 on an adapter board | authorized sellers only |
| 1 | TLV3011B | SOT-23-6 on an adapter board | authorized sellers only |
| 1 | AO3401A | SOT-23 on an adapter board | authorized sellers only |
| 1 | AO3400A | SOT-23 on an adapter board | authorized sellers only |
| 1 | resistor, 0.1 Ohm, 1 %, 0.25 W, the shunt | ||
| 1 | resistor, 18.2 kOhm, 0.1 % | ||
| 1 | resistor, 10 kOhm, 0.1 % | ||
| 1 | resistor, 100 kOhm, 1 % | ||
| 1 | resistor, 4.7 kOhm, 1 % | ||
| 1 | resistor, 1 kOhm, 1 % | ||
| 2 | capacitor, 100 nF, ceramic | ||
| 1 | push button, momentary, normally open | ||
| 1 | perfboard, 0.1 inch pitch | ||
| 1 | wire, 22 AWG, solid |
Used in
Pins
| PIN | BOARD PIN | NET | |
|---|---|---|---|
| GP4 | 6 | UART1 TX, to the DPS5005's serial RX | required |
| GP5 | 7 | UART1 RX, from the DPS5005's serial TX | required |
| GP16 | 21 | SPI0 RX, from the INA239's MISO | required |
| GP17 | 22 | SPI0 CSn, to the INA239's CS | required |
| GP18 | 24 | SPI0 SCK, to the INA239's SCLK | required |
| GP19 | 25 | SPI0 TX, to the INA239's MOSI | required |
| GP20 | 26 | EN, through 1 kOhm: high closes the switch | required |
| GP22 | 29 | the button, to GND; pulled up by the RP2350 | required |
| 3V3(OUT) | 36 | 3V3, powering the INA239 and the TLV3011B | required |
| GND | 38 | GND | required |
Walkthrough
At your own risk: not certified or calibrated test equipment. Legal
Build the circuit above on perfboard, with no firmware on the Pico and nothing connected to OUT+.
With the Pico unplugged, set the DPS5005 to 3.3 V (builds/supply) and measure OUT+.
EXPECT0 V: nothing pulls the switch's gate down.
AGENTSSetting the DPS5005 is a hardware action: within lab/limits.toml, and logged.
Plug the Pico into the lab computer while holding BOOTSEL, so no firmware runs, and measure OUT+ again.
EXPECT0 V: GP20 is not driven, and 4.7 kOhm holds EN low.
Still in BOOTSEL, jumper the GP20 end of the 1 kOhm resistor to 3V3, and measure OUT+.
EXPECTOUT+ follows SUPPLY, less at most the switch's drop.
With the jumper in place and nothing connected to OUT+, raise the DPS5005 in 10 mV steps from 3.3 V until OUT+ falls to 0 V, and note SUPPLY at that step.
EXPECTSUPPLY between 3.386 V and 3.617 V (the claim hardware-cut).
AGENTSSetting the supply above lab/limits.toml's 3.4 V needs a person's approval in the session (CLAUDE.md), with nothing on OUT+. Log every setpoint, and record the result as a measurement record citing those entries.
Lower the DPS5005 to 3.3 V, then remove the jumper.
EXPECTOUT+ returns once SUPPLY falls back below the cut, and falls to 0 V when the jumper comes out.
Claims
| CLAIM | SIMULATION | ON THE BENCH |
|---|---|---|
| Its limit logic sends the DPS5005 a setpoint and current limit only when both are within [supply.dps]'s, as asked, and refuses any others rather than clamping them | checked tentzhen-enforcer nothing_above_the_limits_reaches_the_dps; Kani 0.67.0; one input from any state | unknown |
| An input its limit logic refuses changes nothing | checked tentzhen-enforcer a_refused_input_changes_nothing; Kani 0.67.0; one input from any state | unknown |
| Its limit logic opens the switch at a reading above [supply]'s ceilings, a failed read, or a tick with no reading since the tick before, in any state | checked tentzhen-enforcer a_bad_reading_or_a_silent_tick_trips_the_output_at_once; Kani 0.67.0; one input from any state | unknown |
| Its limit logic closes the switch only on the host's On, from off, once a setpoint has been sent | checked tentzhen-enforcer the_output_turns_on_only_by_on_from_off_with_a_setpoint; Kani 0.67.0; one input from any state | unknown |
| In its limit logic a trip ends only by the button or, under reenable = "agent", the host's clear, and either leaves the switch open | checked tentzhen-enforcer only_the_button_or_an_agent_s_clear_ends_a_trip; Kani 0.67.0; one input from any state | unknown |
| Whatever the firmware does, the switch opens when SUPPLY rises past a threshold between 3.386 V and 3.617 V, set by a divider of 18200 Ω over 10000 Ω in resistors within 0.001 of their value, in a room within 10 K of 25 degrees C | tested tentzhen-records the_enforcer_s_numbers_follow_from_its_parts | trusted maker-datasheets |
| It reads SUPPLY within 0.00997 V at 3.4 V, and the current within 0.00226 A at 0.2 A, up to 0.4096 A, through a 0.1 Ω shunt within 0.01 of its value | tested tentzhen-records the_enforcer_s_numbers_follow_from_its_parts | trusted maker-datasheets |
| Its switch blocks up to 30 V, above what [supply.upstream] feeds the DPS5005 | tested tentzhen-records the_enforcer_s_numbers_follow_from_its_parts | trusted maker-datasheets |
| Its switch closes with less than 0.085 Ω only while SUPPLY is at least 2.5 V; below that it may not close fully | unknown | trusted maker-datasheets |
| With GP20 not driven, 4700 Ω from EN to ground holds the switch open, and GP20's pad sees ground through it and the series resistor, within what erratum E9 needs | tested tentzhen-records the_enforcer_s_numbers_follow_from_its_parts | trusted silicon |
| GP20 at 3.3 V holds EN at 2.72 V, at least the AO3400A's specified drive, and the comparator pulls EN to at most 0.2 V, below its lowest threshold | tested tentzhen-records the_enforcer_s_numbers_follow_from_its_parts | trusted maker-datasheets |
| Only the enforcer's own setpoint commands reach the DPS5005's serial port: nothing from the host passes through | unknown | unknown |