|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +# What Is This? |
| 7 | + |
| 8 | +Lustreiser generates **formally verified real-time embedded code** via |
| 9 | +[Lustre](https://en.wikipedia.org/wiki/Lustre_(programming_language)), |
| 10 | +the synchronous dataflow language created by Caspi, Pilaud, Halbwachs, |
| 11 | +and Plaice at Grenoble. Lustre is the academic foundation of |
| 12 | +[SCADE](https://www.ansys.com/products/embedded-software/ansys-scade-suite), |
| 13 | +the industrial toolchain used in flight control, nuclear reactor |
| 14 | +protection, and automotive powertrain systems. |
| 15 | + |
| 16 | +**Lustreiser analyses your control logic, extracts dataflow patterns, |
| 17 | +generates Lustre nodes with clock calculus, and compiles them to |
| 18 | +deterministic C for embedded targets.** Every execution cycle is |
| 19 | +provably bounded — no jitter, no surprises, no missed deadlines. |
| 20 | + |
| 21 | +Part of the [-iser family](https://github.com/hyperpolymath/iseriser) of |
| 22 | +acceleration frameworks. |
| 23 | + |
| 24 | +# Key Value |
| 25 | + |
| 26 | +- **Provably bounded execution time** — Idris2 dependent types prove |
| 27 | + that every cycle completes within its deadline via WCET (worst-case |
| 28 | + execution time) analysis |
| 29 | + |
| 30 | +- **Deterministic output** — no heap allocation, no recursion, no |
| 31 | + unbounded loops in generated C; identical inputs always produce |
| 32 | + identical outputs at identical times |
| 33 | + |
| 34 | +- **Safety-standard compliance** — generated code targets DO-178C |
| 35 | + (avionics), IEC 61508 (industrial safety), and ISO 26262 (automotive |
| 36 | + functional safety) |
| 37 | + |
| 38 | +- **Synchronous hypothesis** — all computations complete before the next |
| 39 | + clock tick, enforced by clock calculus and timing proofs |
| 40 | + |
| 41 | +# Lustre Primer |
| 42 | + |
| 43 | +Lustre is a **synchronous dataflow language**. Programs are *nodes* that |
| 44 | +transform *streams* of values at each clock tick. |
| 45 | + |
| 46 | +```lustre |
| 47 | +-- A simple counter that resets when `reset` is true |
| 48 | +node counter(reset: bool) returns (count: int); |
| 49 | +let |
| 50 | + count = if reset then 0 |
| 51 | + else (0 -> pre(count) + 1); |
| 52 | +tel |
| 53 | +``` |
| 54 | + |
| 55 | +Core operators: |
| 56 | + |
| 57 | +| `pre(x)` | Previous value of stream `x` (one tick delay) | |
| 58 | +|----|----| |
| 59 | +| `x` `→` `y` | `x` on first tick, `y` thereafter (initialisation, "followed-by") | |
| 60 | +| `x` `fby` `y` | Equivalent to `x` `→` `pre(y)` (followed-by shorthand) | |
| 61 | +| `when` | Sample a stream on a slower clock (clock calculus downsampling) | |
| 62 | +| `merge` | Combine streams from different clocks back to a base clock | |
| 63 | + |
| 64 | +**Clock calculus** ensures that every stream expression has a |
| 65 | +well-defined sampling rate. Lustreiser generates clock annotations and |
| 66 | +verifies them against the Idris2 ABI timing proofs. |
| 67 | + |
| 68 | +# How It Works |
| 69 | + |
| 70 | +Describe your real-time control system in `lustreiser.toml`. Lustreiser: |
| 71 | + |
| 72 | +1. **Analyses control flow** — parses your manifest to extract dataflow |
| 73 | + topology, timing requirements, and I/O declarations |
| 74 | + |
| 75 | +2. **Generates Lustre nodes** — produces `.lus` files with correct |
| 76 | + clock annotations, `pre`/`fby` temporal operators, and |
| 77 | + `when`/`merge` clock calculus expressions |
| 78 | + |
| 79 | +3. **Proves timing bounds** — the Idris2 ABI layer formally verifies |
| 80 | + that worst-case execution time (WCET) for every node fits within the |
| 81 | + declared clock period |
| 82 | + |
| 83 | +4. **Compiles to deterministic C** — the Lustre compiler produces C |
| 84 | + code with no `malloc`, no recursion, no unbounded loops, and |
| 85 | + statically allocated buffers — suitable for bare-metal embedded |
| 86 | + targets |
| 87 | + |
| 88 | +5. **Bridges via Zig FFI** — the generated C is wrapped in a Zig FFI |
| 89 | + layer for integration with Rust, Idris2, and other -iser components |
| 90 | + |
| 91 | +# Architecture |
| 92 | + |
| 93 | +Follows the hyperpolymath -iser pattern: |
| 94 | + |
| 95 | + lustreiser.toml ← user describes control system |
| 96 | + │ |
| 97 | + ▼ |
| 98 | + ┌─────────────────────┐ |
| 99 | + │ Rust CLI │ Parse manifest, validate topology |
| 100 | + │ src/main.rs │ |
| 101 | + └────────┬────────────┘ |
| 102 | + │ |
| 103 | + ▼ |
| 104 | + ┌─────────────────────┐ |
| 105 | + │ Control Flow │ Extract dataflow graph, identify |
| 106 | + │ Analysis │ nodes, clocks, temporal operators |
| 107 | + └────────┬────────────┘ |
| 108 | + │ |
| 109 | + ▼ |
| 110 | + ┌─────────────────────┐ |
| 111 | + │ Idris2 ABI │ Prove timing bounds (WCET), |
| 112 | + │ src/interface/abi/ │ verify clock calculus, validate |
| 113 | + │ │ stream buffer layouts |
| 114 | + └────────┬────────────┘ |
| 115 | + │ |
| 116 | + ▼ |
| 117 | + ┌─────────────────────┐ |
| 118 | + │ Lustre Codegen │ Generate .lus files with clock |
| 119 | + │ src/codegen/ │ annotations, pre/fby/when/merge |
| 120 | + └────────┬────────────┘ |
| 121 | + │ |
| 122 | + ▼ |
| 123 | + ┌─────────────────────┐ |
| 124 | + │ C Compilation │ Lustre → deterministic C |
| 125 | + │ (no malloc, no │ (static buffers, bounded loops) |
| 126 | + │ recursion) │ |
| 127 | + └────────┬────────────┘ |
| 128 | + │ |
| 129 | + ▼ |
| 130 | + ┌─────────────────────┐ |
| 131 | + │ Zig FFI Bridge │ C-ABI wrapper for integration |
| 132 | + │ src/interface/ffi/ │ with Rust and -iser ecosystem |
| 133 | + └─────────────────────┘ |
| 134 | + |
| 135 | +# Use Cases |
| 136 | + |
| 137 | +- **Flight control systems** — attitude controllers, autopilot mode |
| 138 | + logic, sensor fusion with guaranteed response times (DO-178C Level A) |
| 139 | + |
| 140 | +- **Engine management units** — fuel injection timing, ignition |
| 141 | + scheduling, emission control loops (ISO 26262 ASIL D) |
| 142 | + |
| 143 | +- **Nuclear reactor protection** — rod insertion logic, coolant |
| 144 | + monitoring, trip systems (IEC 61508 SIL 3/4) |
| 145 | + |
| 146 | +- **PLC programming** — replacing ladder logic with formally verified |
| 147 | + synchronous controllers for industrial automation |
| 148 | + |
| 149 | +- **Sensor fusion** — combining accelerometer, gyroscope, and |
| 150 | + magnetometer streams with proven latency bounds |
| 151 | + |
| 152 | +- **Robotic actuator control** — servo loops, trajectory planning with |
| 153 | + hard real-time constraints |
| 154 | + |
| 155 | +# Build |
| 156 | + |
| 157 | +```bash |
| 158 | +cargo build --release |
| 159 | +cargo test |
| 160 | +``` |
| 161 | + |
| 162 | +# Status |
| 163 | + |
| 164 | +**Codebase in progress.** Architecture defined, CLI scaffolded, RSR |
| 165 | +template complete. Codegen stubs in place — Lustre node generation, |
| 166 | +clock calculus, and WCET analysis are the next implementation targets. |
| 167 | +See `ROADMAP.adoc` for the full phased plan. |
| 168 | + |
| 169 | +# License |
| 170 | + |
| 171 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
0 commit comments