EML Intro: Your First Guard Kernel

mathsafe(request, limit) = min(request, limit)

emlmodule threshold_reflex;

@verify(lean, theorem = "guard_output_bounded")
@target(fpga, clock_mhz = 100)
fn reflex_guard(request: Real, limit: Real) -> Real
    requires (limit > 0.0)
    ensures (result <= limit)
{
    min(request, limit)
}

basheml-compile threshold_reflex_v0.eml --target c -o threshold_reflex_v0.c

c#include "libmonogate.h"
#include <stdint.h>
#include <math.h>

/* UNFUSED BY DEFAULT. `a + b * c` in EML is an add of a ROUNDED product; the fused operation is
 * written `fma(a, b, c)` and is emitted as a call to `fma`, which still contracts. GCC contracts
 * `a + b*c` into one fused multiply-add at -O2 and above [...], which would change this
 * artifact's last bits. The pragma below turns that off for THIS FILE ONLY [...]
 * THIS OVERRIDES -ffast-math, ON PURPOSE. [... rationale trimmed ...] */
#if defined(__clang__)
#pragma STDC FP_CONTRACT OFF
#elif defined(__GNUC__)
#pragma GCC push_options
#pragma GCC optimize("fp-contract=off")
#else
#pragma STDC FP_CONTRACT OFF
#endif
#include <stdio.h>
#include <stdlib.h>

/* Contract checks. NOT assert(): -DNDEBUG would delete them, and a release
 * build that silently drops every `requires` and `ensures` is exactly the
 * obligation attenuation this compiler exists to report. */
#define EML_CONTRACT(cond, msg) \
    do { if (!(cond)) { \
        fprintf(stderr, "EML contract violated: %s\n", (msg)); \
        abort(); } } while (0)

static inline double eml_builtin_min(double a, double b) { return isnan(a) ? a : isnan(b) ? b : a == b ? (signbit(a) ? a : b) : fmin(a, b); }

/*
 * reflex_guard
 * Pfaffian chain count (eml-cost pfaffian_r): 0     Cost class: p0-d1-w0-c0
 * EML depth:   1  Symbolic band: LOW (from pfaffian_r only)
 * Numerical:   cancellation exposure NONE  (no mixed-sign subtraction)
 * Dynamics:    0 osc, 0 decay  (predicted_r=0)
 * source obligations for reflex_guard: {O1}
 *   O1 [b0f58e3d87b2] -> PRESERVED (equivalent)  EML_CONTRACT before return; survives -DNDEBUG
 *        build: unconditional -- EML_CONTRACT is a self-contained if/abort, NOT assert(), so -DNDEBUG cannot delete it
 * FPGA est:   1 MAC, 0 exp, 0 ln, 0 trig -> 2 cy @ 32-bit
 */
double reflex_guard(double request, double limit) {
    EML_CONTRACT(((limit > 0.0)), "reflex_guard: requires ((limit > 0.0))");
    double result = eml_builtin_min(request, limit);
    EML_CONTRACT(((result <= limit)), "reflex_guard: ensures violated: (result <= limit)");
    return result;
}

#if !defined(__clang__) && defined(__GNUC__)
#pragma GCC pop_options  /* end of the unfused region: see the note at the top of this file */
#endif

cpp// threshold_reflex_v0.c, libmonogate.h and libmonogate.c sit beside this sketch.
extern "C" double reflex_guard(double request, double limit);

void loop() {
    int raw = analogRead(34);
    double pot_raw = raw / 4095.0;
    double requested_output = pot_raw;
    double safe_output = 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
    );
}

basheml-compile threshold_reflex_v0.eml --target lean -o threshold_reflex_v0.lean

leanimport MachLib.EML
import MachLib.Trig
import MachLib.Forge
import MachLib.Linarith
import MachLib.FixedPoint
import MachLib.SignTactic
import MachLib.Decimal

set_option maxHeartbeats 1000000
set_option autoImplicit false
set_option linter.unusedSimpArgs false

open MachLib
open MachLib.Real

noncomputable def reflex_guard (request : Real) (limit : Real) : Real :=
  (min request limit)

theorem guard_output_bounded (request : Real) (limit : Real)
    (h1 : (limit > (0 : Real))) :
    ((reflex_guard request limit) <= limit) := by
  unfold reflex_guard
  try mach_split_hyps
  try dsimp only
  all_goals
    (try simp only [add_zero, zero_add, mul_zero, zero_mul, mul_one_ax, one_mul_thm, div_one_eq, ofSci_zero]) <;>
      first
      | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
      | (apply clamp_le_hi <;> (first | assumption | mach_positivity))
      -- ... 14 more tactics, tried in order ...
      | sorry  -- out of reach; left for the prover

bashgit clone https://github.com/agent-maestro/machlib
cd machlib/foundations
lake build          # needs elan; about ten minutes the first time
echo '#print axioms guard_output_bounded' >> /path/to/threshold_reflex_v0.lean
lake env lean /path/to/threshold_reflex_v0.lean

output'guard_output_bounded' depends on axioms: [propext, Classical.choice, Real,
 Quot.sound, leR, le_iff_lt_or_eq, ltR, zeroR]

json{
  "pot_raw": 0.97,
  "requested_output": 1.00,
  "safe_output": 0.85,
  "guard_action": "clamp_to_safe_output"
}

basheml-compile threshold_reflex_v0.eml --target verilog -o threshold_reflex_v0.v
compile error (emission gate): function(s) failed to emit, so the output is a comment rather than a datapath:
[('reflex_guard', "unsupported construct: 'no hardware realization for min(...), called from
this kernel(...). Every call needs a resolved module and a resolved latency before any RTL is
written: a guessed latency latches a register before its operand exists, which synthesises and
computes nothing.'")]

eml@verify(lean, theorem = "guard_output_bounded")
@target(fpga, clock_mhz = 100)
fn reflex_guard(request: Real, limit: Real) -> Real
    requires (limit > 0.0)
    ensures (result <= limit)
{
    clamp(request, 0.0, limit)
}