Skip to content

Commit 1e801dc

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(abi): add Idris2 ABI definitions for IIoT hardware abstraction
Types, HAL, MQTT, OTA, WiFi — 379 LOC of dependently-typed ABI specs for the Kaldor embedded platform. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 4b1e37b commit 1e801dc

5 files changed

Lines changed: 379 additions & 0 deletions

File tree

‎src/abi/HAL.idr‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- HAL.idr — Hardware Abstraction Layer ABI contract.
5+
--
6+
-- Defines the interface that both the freestanding ESP32 implementation
7+
-- (ffi/zig/src/esp_idf_hal.zig) and the simulation implementation
8+
-- (firmware-zig/src/hal.zig) must satisfy.
9+
10+
module KaldorBBW.ABI.HAL
11+
12+
import KaldorBBW.ABI.Types
13+
14+
%default total
15+
16+
-- --------------------------------------------------------------------------
17+
-- HAL interface
18+
-- --------------------------------------------------------------------------
19+
20+
||| Contract for the hardware abstraction layer.
21+
|||
22+
||| All effectful operations live in some monad @m. The actual
23+
||| implementations are in Zig (host simulation or ESP-IDF on device).
24+
public export
25+
interface HalABI (0 m : Type -> Type) where
26+
27+
-- Time
28+
||| Current time in milliseconds since boot.
29+
timerGetMs : m Nat
30+
||| Suspend execution for @ms milliseconds.
31+
delayMs : Nat -> m ()
32+
33+
-- GPIO — return False if the pin index is out of range (> 39)
34+
||| Configure pin as push-pull output.
35+
gpioSetOut : GpioPin -> m Bool
36+
||| Configure pin as input (floating).
37+
gpioSetIn : GpioPin -> m Bool
38+
||| Write a digital level to a pin.
39+
gpioWrite : GpioPin -> Bool -> m Bool
40+
||| Read the current digital level of a pin.
41+
gpioRead : GpioPin -> m Bool
42+
43+
-- UART
44+
||| Write raw bytes to UART0 (debug / log output).
45+
uartPrint : List Bits8 -> m ()
46+
47+
-- System
48+
||| Read the unique chip identifier from the eFuse MAC address.
49+
chipId : m Bits32
50+
||| Return the current size of the free heap in bytes.
51+
freeHeap : m Nat
52+
||| Hard restart the microcontroller. Does not return.
53+
restart : m Void
54+
55+
-- --------------------------------------------------------------------------
56+
-- Derived proofs and combinators
57+
-- --------------------------------------------------------------------------
58+
59+
||| Pin 0 satisfies the GpioPin constraint.
60+
public export
61+
pin0 : GpioPin
62+
pin0 = MkGpioPin 0
63+
64+
||| Pin 39 satisfies the GpioPin constraint (boundary value).
65+
public export
66+
pin39 : GpioPin
67+
pin39 = MkGpioPin 39
68+
69+
||| Convenience: toggle a GPIO pin (read then write the complement).
70+
public export
71+
gpioToggle : HalABI m => Monad m => GpioPin -> m Bool
72+
gpioToggle pin = do
73+
level <- gpioRead pin
74+
gpioWrite pin (not level)

‎src/abi/MQTT.idr‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- MQTT.idr — MQTT client ABI contract.
5+
--
6+
-- Implementation: ffi/zig/src/esp_idf_mqtt.zig (wraps ESP-IDF esp_mqtt_client).
7+
8+
module KaldorBBW.ABI.MQTT
9+
10+
import KaldorBBW.ABI.Types
11+
12+
%default total
13+
14+
-- --------------------------------------------------------------------------
15+
-- MQTT interface
16+
-- --------------------------------------------------------------------------
17+
18+
||| Contract for MQTT operations.
19+
|||
20+
||| @m the effect monad (IO on the device, test monad in simulation)
21+
public export
22+
interface MqttABI (0 m : Type -> Type) where
23+
24+
||| Initiate a connection to the configured broker. Returns True on success.
25+
connect : m Bool
26+
27+
||| Return True if the client is currently connected.
28+
isConnected : m Bool
29+
30+
||| Subscribe to a topic. The MqttTopic proof guarantees valid length.
31+
subscribe : MqttTopic -> m Bool
32+
33+
||| Publish a message.
34+
||| @topic valid MQTT topic (1–256 bytes)
35+
||| @payload message payload (any bytes, including empty)
36+
||| @qos delivery guarantee level
37+
||| @retain whether the broker should retain the message
38+
publish : MqttTopic -> List Bits8 -> MqttQos -> Bool -> m Bool
39+
40+
||| Poll for one pending received message. Returns Nothing if queue empty.
41+
poll : m (Maybe (MqttTopic, List Bits8))
42+
43+
-- --------------------------------------------------------------------------
44+
-- Proof-bearing combinators
45+
-- --------------------------------------------------------------------------
46+
47+
||| Proof: QoS 0 (fire-and-forget) is always a valid QoS choice.
48+
public export
49+
defaultQos : MqttQos
50+
defaultQos = QosAtMostOnce
51+
52+
||| Proof: the topic-length bound is preserved through the ABI.
53+
||| If @t : MqttTopic then @t.bounded witnesses len(t.bytes) <= 256.
54+
public export
55+
topicBoundIntact : (t : MqttTopic) -> LTE (length t.bytes) 256
56+
topicBoundIntact t = t.bounded
57+
58+
||| Convenience: publish a telemetry value using QoS 0, non-retained.
59+
public export
60+
publishTelemetry : MqttABI m => Monad m =>
61+
MqttTopic -> List Bits8 -> m Bool
62+
publishTelemetry topic payload =
63+
publish topic payload QosAtMostOnce False

‎src/abi/OTA.idr‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- OTA.idr — Over-the-Air update ABI contract with state-machine proofs.
5+
--
6+
-- Implementation: ffi/zig/src/esp_idf_ota.zig (wraps ESP-IDF esp_https_ota).
7+
8+
module KaldorBBW.ABI.OTA
9+
10+
import KaldorBBW.ABI.Types
11+
12+
%default total
13+
14+
-- --------------------------------------------------------------------------
15+
-- OTA state machine
16+
-- --------------------------------------------------------------------------
17+
18+
||| Valid states for the OTA update process.
19+
public export
20+
data OtaState
21+
= OtaIdle -- no update in progress
22+
| OtaDownloading -- receiving firmware bytes
23+
| OtaVerifying -- checksum / signature check
24+
| OtaInstalling -- writing to flash partition
25+
| OtaComplete -- update successful; pending reboot
26+
| OtaError -- update failed; back to idle after reset
27+
28+
||| Proof that @begin@ is callable only from the Idle state.
29+
public export
30+
data CanBegin : OtaState -> Type where
31+
BeginFromIdle : CanBegin OtaIdle
32+
33+
||| Proof that @abort@ is callable only during active (non-terminal) states.
34+
public export
35+
data CanAbort : OtaState -> Type where
36+
AbortDownloading : CanAbort OtaDownloading
37+
AbortVerifying : CanAbort OtaVerifying
38+
AbortInstalling : CanAbort OtaInstalling
39+
40+
||| Proof that markValid is callable only when complete.
41+
public export
42+
data CanMarkValid : OtaState -> Type where
43+
MarkValidWhenComplete : CanMarkValid OtaComplete
44+
45+
-- --------------------------------------------------------------------------
46+
-- OTA interface
47+
-- --------------------------------------------------------------------------
48+
49+
||| Contract for OTA operations with typed state-machine transitions.
50+
public export
51+
interface OtaABI (0 m : Type -> Type) where
52+
53+
||| Start a firmware download from the given HTTPS URL.
54+
||| Only callable when in the Idle state (enforced by @CanBegin s@).
55+
begin : OtaUrl
56+
-> {0 s : OtaState}
57+
-> {auto 0 _ : CanBegin s}
58+
-> m Bool
59+
60+
||| Poll download progress. Returns (bytesReceived, totalBytes).
61+
progress : m (Nat, Nat)
62+
63+
||| Verify the downloaded firmware image. Returns True if signature valid.
64+
verify : m Bool
65+
66+
||| Commit the verified image to the active partition.
67+
finish : m Bool
68+
69+
||| Abort an in-progress update (download / verify / install only).
70+
abort : {0 s : OtaState}
71+
-> {auto 0 _ : CanAbort s}
72+
-> m ()
73+
74+
||| Mark the running firmware as valid to prevent automatic rollback.
75+
markValid : m ()
76+
77+
||| Roll back to the previous firmware image.
78+
rollback : m ()

‎src/abi/Types.idr‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- Types.idr — Dependent-typed domain definitions for the Kaldor BBW board.
5+
--
6+
-- Every type here carries a proof that its value is within the valid physical
7+
-- or protocol range. The Zig FFI layer (ffi/zig/src/) enforces the same
8+
-- bounds at runtime; these types make the contract explicit at compile time.
9+
10+
module KaldorBBW.ABI.Types
11+
12+
%default total
13+
14+
-- --------------------------------------------------------------------------
15+
-- GPIO
16+
-- --------------------------------------------------------------------------
17+
18+
||| ESP32 GPIO pin number, constrained to the Xtensa LX6 valid range 0–39.
19+
public export
20+
data GpioPin : Type where
21+
MkGpioPin : (n : Nat) -> {auto 0 prf : LTE n 39} -> GpioPin
22+
23+
||| GPIO operating mode — mirrors the esp_idf @c gpio_mode_t enum.
24+
public export
25+
data GpioMode
26+
= GpioDisable -- 0 (no driver)
27+
| GpioInput -- 1 (input only)
28+
| GpioOutput -- 2 (push-pull output)
29+
| GpioOutputOD -- 6 (open-drain output)
30+
| GpioInputOutput -- 3 (bidirectional)
31+
32+
-- --------------------------------------------------------------------------
33+
-- MQTT
34+
-- --------------------------------------------------------------------------
35+
36+
||| MQTT QoS level.
37+
||| 0 = at most once, 1 = at least once, 2 = exactly once.
38+
public export
39+
data MqttQos = QosAtMostOnce | QosAtLeastOnce | QosExactlyOnce
40+
41+
||| Encode QoS as the unsigned byte value expected on the wire.
42+
public export
43+
qosToU8 : MqttQos -> Bits8
44+
qosToU8 QosAtMostOnce = 0
45+
qosToU8 QosAtLeastOnce = 1
46+
qosToU8 QosExactlyOnce = 2
47+
48+
||| A valid MQTT topic string (MQTT 3.1.1 §4.7).
49+
||| Non-empty, at most 256 bytes, no embedded NUL.
50+
public export
51+
record MqttTopic where
52+
constructor MkTopic
53+
bytes : List Bits8
54+
nonEmpty : NonEmpty bytes
55+
bounded : LTE (length bytes) 256
56+
57+
-- --------------------------------------------------------------------------
58+
-- OTA
59+
-- --------------------------------------------------------------------------
60+
61+
||| An HTTPS URL for firmware downloads.
62+
||| Non-empty, at most 8192 characters, prefixed with "https://".
63+
public export
64+
record OtaUrl where
65+
constructor MkOtaUrl
66+
chars : List Char
67+
nonEmpty : NonEmpty chars
68+
bounded : LTE (length chars) 8192
69+
isHttps : isPrefixOf (unpack "https://") chars = True
70+
71+
-- --------------------------------------------------------------------------
72+
-- BBW sensor domain
73+
-- --------------------------------------------------------------------------
74+
75+
||| Back Beam Width measurement in millimetres.
76+
||| Physical operating range of the Kaldor loom: 10–500 mm (config.zig).
77+
public export
78+
record BbwMm where
79+
constructor MkBbwMm
80+
value : Double
81+
lower : value >= 10.0 = True
82+
upper : value <= 500.0 = True
83+
84+
||| Temperature reading in degrees Celsius (DHT22 range: –40 to +80 °C).
85+
public export
86+
record TempC where
87+
constructor MkTempC
88+
value : Double
89+
lower : value >= -40.0 = True
90+
upper : value <= 80.0 = True
91+
92+
||| Ultrasonic distance reading in millimetres (HC-SR04 range: 20–4000 mm).
93+
public export
94+
record DistanceMm where
95+
constructor MkDistanceMm
96+
value : Double
97+
lower : value >= 20.0 = True
98+
upper : value <= 4000.0 = True
99+
100+
-- --------------------------------------------------------------------------
101+
-- Convenience constructors with proof obligations
102+
-- --------------------------------------------------------------------------
103+
104+
||| Smart constructor: build a GpioPin if n <= 39, else Nothing.
105+
public export
106+
mkGpioPin : (n : Nat) -> Maybe GpioPin
107+
mkGpioPin n with (isLTE n 39)
108+
| Yes prf = Just (MkGpioPin n)
109+
| No _ = Nothing

‎src/abi/WiFi.idr‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- WiFi.idr — WiFi management ABI contract.
5+
--
6+
-- Implementation: ffi/zig/src/esp_idf_wifi.zig (wraps ESP-IDF esp_wifi).
7+
8+
module KaldorBBW.ABI.WiFi
9+
10+
%default total
11+
12+
-- --------------------------------------------------------------------------
13+
-- RSSI
14+
-- --------------------------------------------------------------------------
15+
16+
||| WiFi signal strength in dBm.
17+
||| Constrained to the ESP32 reporting range (–100 to 0 dBm).
18+
||| The value 31 returned by ESP-IDF when no signal is available is mapped
19+
||| to –100 by the Zig FFI wrapper (see ffi/zig/src/esp_idf_wifi.zig).
20+
public export
21+
record Rssi where
22+
constructor MkRssi
23+
dBm : Int
24+
lower : dBm >= -100 = True
25+
upper : dBm <= 0 = True
26+
27+
-- --------------------------------------------------------------------------
28+
-- WiFi interface
29+
-- --------------------------------------------------------------------------
30+
31+
||| Contract for WiFi status queries.
32+
||| Connection management (connect / disconnect) is handled at the HAL level.
33+
public export
34+
interface WiFiABI (0 m : Type -> Type) where
35+
36+
||| Return True if the station is currently associated with an AP.
37+
isConnected : m Bool
38+
39+
||| Return the current RSSI.
40+
||| The returned @Rssi@ proof guarantees the value is in –100..0.
41+
getRssi : m Rssi
42+
43+
-- --------------------------------------------------------------------------
44+
-- Proofs
45+
-- --------------------------------------------------------------------------
46+
47+
||| –50 dBm is a valid RSSI (good signal).
48+
public export
49+
goodSignal : Rssi
50+
goodSignal = MkRssi (-50) Refl Refl
51+
52+
||| –100 dBm is the worst valid RSSI (no signal sentinel).
53+
public export
54+
noSignal : Rssi
55+
noSignal = MkRssi (-100) Refl Refl

0 commit comments

Comments
 (0)