Monogate Electronics Lab
EML Intro: Your First Guard Kernel
You built the Reflex Lab 01 circuit. Now write the guard in EML, compile it toward C for the ESP32, and watch your own clamp event appear in the visualizer.
Section 1
What just happened in your circuit
The potentiometer sends pot_raw. Firmware maps it into requested_output. The guard kernel clamps it to safe_output. The LED and buzzer reflect the safe output, not the raw request.
In the visualizer, the important fields are pot_raw, requested_output, safe_output, and guard_action.
Section 2
The guard kernel in plain math
mathsafe(request, limit) = if request > limit then limit else requestThe domain is limit > 0. The guarantee is safe output <= limit. The proof obligation is the exact thing a reviewer would ask: show that the clamped path never returns a value above the limit.
Section 3
Writing the guard in EML
Save this file beside the Reflex Guard lesson files.
emlmodule threshold_reflex;
fn guard(request: Real, limit: Real) -> Real
requires (limit > 0.0)
ensures (return <= limit)
{
let clamped = request - (request - limit);
if request > limit { limit } else { request }
}requires and ensures are not comments. They become obligations that MachLib/Lean can close later.
Section 4
Compiling to C for the ESP32
basheml-compile threshold_reflex_v0.eml --target c --profile esp32c#include <assert.h>
double threshold_reflex_guard(double request, double limit) {
assert(limit > 0.0);
if (request > limit) {
return limit;
}
return request;
}cpp#include "threshold_reflex_v0.h"
void loop() {
int raw = analogRead(34);
double pot_raw = raw / 4095.0;
double requested_output = pot_raw;
double safe_output = threshold_reflex_guard(requested_output, 0.85);
const char* guard_action =
requested_output > safe_output ? "clamp_to_safe_output" : "pass_through";
Serial.printf(
"{\"pot_raw\":%.3f,\"requested_output\":%.3f,\"safe_output\":%.3f,\"guard_action\":\"%s\"}\n",
pot_raw,
requested_output,
safe_output,
guard_action
);
}The current hand-written firmware reference remains in kernels/threshold_reflex_v0/esp32/threshold_reflex_v0. Generated C should match the same guard boundary and serial fields.
Section 5
The proof obligation
basheml-compile threshold_reflex_v0.eml --target leanleandef guard (request limit : Real) : Real :=
if request > limit then limit else request
theorem guard_output_bounded
(request limit : Real)
(h_limit : limit > 0.0) :
guard request limit <= limit := by
unfold guard
by_cases h : request > limit
. simp [h]
. simp [h]
exact le_of_not_gt hIf your generated Lean contains sorry, that means the proof is still open. The important win is that the compiler named the exact property to prove.
Section 6
Watching it in the visualizer
json{
"pot_raw": 0.97,
"requested_output": 1.00,
"safe_output": 0.85,
"guard_action": "clamp_to_safe_output"
}When guard_action becomes clamp_to_safe_output, the dashboard logs the event, flashes the panel, and plays the sound. The loop is now visible: EML source, generated firmware shape, ESP32 serial frame, visualizer event.
Section 7