diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index caeda1c..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..858f44f --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,71 @@ +== Contributing + +Thank you for your interest in contributing! We follow a "`Dual-Track`" +architecture where human-readable documentation lives in the root and +machine-readable policies live in `+.machine_readable/+`. + +=== How to Contribute + +We welcome contributions in many forms: + +* *Code:* Improving the core stack or extensions +* *Documentation:* Enhancing docs or AI manifests +* *Testing:* Adding property-based tests or formal proofs +* *Bug reports:* Filing clear, reproducible issues + +=== Getting Started + +[arabic] +. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present) +to understand the repository structure. +. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your +tools. +. *Task Runner:* Use `+just+` to see available commands +(`+just --list+`). + +=== Development Workflow + +==== Branch Naming + +.... +docs/short-description # Documentation +test/what-added # Test additions +feat/short-description # New features +fix/issue-number-description # Bug fixes +refactor/what-changed # Code improvements +security/what-fixed # Security fixes +.... + +==== Commit Messages + +We follow https://www.conventionalcommits.org/[Conventional Commits]: + +.... +(): + +[optional body] + +[optional footer] +.... + +Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`, +`+chore+`, `+security+` + +=== Reporting Bugs + +Before reporting: 1. Search existing issues 2. Check if it’s already +fixed in `+main+` + +When reporting, include: - Clear, descriptive title - Environment +details (OS, versions, toolchain) - Steps to reproduce - Expected vs +actual behaviour + +=== Code of Conduct + +All contributors are expected to adhere to our +link:CODE_OF_CONDUCT.md[Code of Conduct]. + +=== License + +By contributing, you agree that your contributions will be licensed +under the same license as the project (see LICENSE). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 80ecdac..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,66 +0,0 @@ - -# Contributing - -Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`. - -## How to Contribute - -We welcome contributions in many forms: - -- **Code:** Improving the core stack or extensions -- **Documentation:** Enhancing docs or AI manifests -- **Testing:** Adding property-based tests or formal proofs -- **Bug reports:** Filing clear, reproducible issues - -## Getting Started - -1. **Read the AI Manifest:** Start with `0-AI-MANIFEST.a2ml` (if present) to understand the repository structure. -2. **Environment:** Use `nix develop` or `direnv allow` to set up your tools. -3. **Task Runner:** Use `just` to see available commands (`just --list`). - -## Development Workflow - -### Branch Naming - -``` -docs/short-description # Documentation -test/what-added # Test additions -feat/short-description # New features -fix/issue-number-description # Bug fixes -refactor/what-changed # Code improvements -security/what-fixed # Security fixes -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): - -``` -(): - -[optional body] - -[optional footer] -``` - -Types: `feat`, `fix`, `docs`, `test`, `refactor`, `ci`, `chore`, `security` - -## Reporting Bugs - -Before reporting: -1. Search existing issues -2. Check if it's already fixed in `main` - -When reporting, include: -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour - -## Code of Conduct - -All contributors are expected to adhere to our [Code of Conduct](CODE_OF_CONDUCT.md). - -## License - -By contributing, you agree that your contributions will be licensed under the same license as the project (see [LICENSE](LICENSE)). diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..fd9be30 --- /dev/null +++ b/README.adoc @@ -0,0 +1,167 @@ +== What Is This? + +Lustreiser generates *formally verified real-time embedded code* via +https://en.wikipedia.org/wiki/Lustre_(programming_language)[Lustre], the +synchronous dataflow language created by Caspi, Pilaud, Halbwachs, and +Plaice at Grenoble. Lustre is the academic foundation of +https://www.ansys.com/products/embedded-software/ansys-scade-suite[SCADE], +the industrial toolchain used in flight control, nuclear reactor +protection, and automotive powertrain systems. + +*Lustreiser analyses your control logic, extracts dataflow patterns, +generates Lustre nodes with clock calculus, and compiles them to +deterministic C for embedded targets.* Every execution cycle is provably +bounded — no jitter, no surprises, no missed deadlines. + +Part of the https://github.com/hyperpolymath/iseriser[-iser family] of +acceleration frameworks. + +== Key Value + +* *Provably bounded execution time* — Idris2 dependent types prove that +every cycle completes within its deadline via WCET (worst-case execution +time) analysis +* *Deterministic output* — no heap allocation, no recursion, no +unbounded loops in generated C; identical inputs always produce +identical outputs at identical times +* *Safety-standard compliance* — generated code targets DO-178C +(avionics), IEC 61508 (industrial safety), and ISO 26262 (automotive +functional safety) +* *Synchronous hypothesis* — all computations complete before the next +clock tick, enforced by clock calculus and timing proofs + +== Lustre Primer + +Lustre is a *synchronous dataflow language*. Programs are _nodes_ that +transform _streams_ of values at each clock tick. + +[source,lustre] +---- +-- A simple counter that resets when `reset` is true +node counter(reset: bool) returns (count: int); +let + count = if reset then 0 + else (0 -> pre(count) + 1); +tel +---- + +Core operators: + +[width="100%",cols="50%,50%",options="header",] +|=== +|`+pre(x)+` |Previous value of stream `+x+` (one tick delay) +|`+x+` `+→+` `+y+` |`+x+` on first tick, `+y+` thereafter +(initialisation, "`followed-by`") + +|`+x+` `+fby+` `+y+` |Equivalent to `+x+` `+→+` `+pre(y)+` (followed-by +shorthand) + +|`+when+` |Sample a stream on a slower clock (clock calculus +downsampling) + +|`+merge+` |Combine streams from different clocks back to a base clock +|=== + +*Clock calculus* ensures that every stream expression has a well-defined +sampling rate. Lustreiser generates clock annotations and verifies them +against the Idris2 ABI timing proofs. + +== How It Works + +Describe your real-time control system in `+lustreiser.toml+`. +Lustreiser: + +[arabic] +. *Analyses control flow* — parses your manifest to extract dataflow +topology, timing requirements, and I/O declarations +. *Generates Lustre nodes* — produces `+.lus+` files with correct clock +annotations, `+pre+`/`+fby+` temporal operators, and `+when+`/`+merge+` +clock calculus expressions +. *Proves timing bounds* — the Idris2 ABI layer formally verifies that +worst-case execution time (WCET) for every node fits within the declared +clock period +. *Compiles to deterministic C* — the Lustre compiler produces C code +with no `+malloc+`, no recursion, no unbounded loops, and statically +allocated buffers — suitable for bare-metal embedded targets +. *Bridges via Zig FFI* — the generated C is wrapped in a Zig FFI layer +for integration with Rust, Idris2, and other -iser components + +== Architecture + +Follows the hyperpolymath -iser pattern: + +.... +lustreiser.toml ← user describes control system + │ + ▼ +┌─────────────────────┐ +│ Rust CLI │ Parse manifest, validate topology +│ src/main.rs │ +└────────┬────────────┘ + │ + ▼ +┌─────────────────────┐ +│ Control Flow │ Extract dataflow graph, identify +│ Analysis │ nodes, clocks, temporal operators +└────────┬────────────┘ + │ + ▼ +┌─────────────────────┐ +│ Idris2 ABI │ Prove timing bounds (WCET), +│ src/interface/abi/ │ verify clock calculus, validate +│ │ stream buffer layouts +└────────┬────────────┘ + │ + ▼ +┌─────────────────────┐ +│ Lustre Codegen │ Generate .lus files with clock +│ src/codegen/ │ annotations, pre/fby/when/merge +└────────┬────────────┘ + │ + ▼ +┌─────────────────────┐ +│ C Compilation │ Lustre → deterministic C +│ (no malloc, no │ (static buffers, bounded loops) +│ recursion) │ +└────────┬────────────┘ + │ + ▼ +┌─────────────────────┐ +│ Zig FFI Bridge │ C-ABI wrapper for integration +│ src/interface/ffi/ │ with Rust and -iser ecosystem +└─────────────────────┘ +.... + +== Use Cases + +* *Flight control systems* — attitude controllers, autopilot mode logic, +sensor fusion with guaranteed response times (DO-178C Level A) +* *Engine management units* — fuel injection timing, ignition +scheduling, emission control loops (ISO 26262 ASIL D) +* *Nuclear reactor protection* — rod insertion logic, coolant +monitoring, trip systems (IEC 61508 SIL 3/4) +* *PLC programming* — replacing ladder logic with formally verified +synchronous controllers for industrial automation +* *Sensor fusion* — combining accelerometer, gyroscope, and magnetometer +streams with proven latency bounds +* *Robotic actuator control* — servo loops, trajectory planning with +hard real-time constraints + +== Build + +[source,bash] +---- +cargo build --release +cargo test +---- + +== Status + +*Codebase in progress.* Architecture defined, CLI scaffolded, RSR +template complete. Codegen stubs in place — Lustre node generation, +clock calculus, and WCET analysis are the next implementation targets. +See `+ROADMAP.adoc+` for the full phased plan. + +== License + +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/README.md b/README.md deleted file mode 100644 index 305cd45..0000000 --- a/README.md +++ /dev/null @@ -1,171 +0,0 @@ - - -# What Is This? - -Lustreiser generates **formally verified real-time embedded code** via -[Lustre](https://en.wikipedia.org/wiki/Lustre_(programming_language)), -the synchronous dataflow language created by Caspi, Pilaud, Halbwachs, -and Plaice at Grenoble. Lustre is the academic foundation of -[SCADE](https://www.ansys.com/products/embedded-software/ansys-scade-suite), -the industrial toolchain used in flight control, nuclear reactor -protection, and automotive powertrain systems. - -**Lustreiser analyses your control logic, extracts dataflow patterns, -generates Lustre nodes with clock calculus, and compiles them to -deterministic C for embedded targets.** Every execution cycle is -provably bounded — no jitter, no surprises, no missed deadlines. - -Part of the [-iser family](https://github.com/hyperpolymath/iseriser) of -acceleration frameworks. - -# Key Value - -- **Provably bounded execution time** — Idris2 dependent types prove - that every cycle completes within its deadline via WCET (worst-case - execution time) analysis - -- **Deterministic output** — no heap allocation, no recursion, no - unbounded loops in generated C; identical inputs always produce - identical outputs at identical times - -- **Safety-standard compliance** — generated code targets DO-178C - (avionics), IEC 61508 (industrial safety), and ISO 26262 (automotive - functional safety) - -- **Synchronous hypothesis** — all computations complete before the next - clock tick, enforced by clock calculus and timing proofs - -# Lustre Primer - -Lustre is a **synchronous dataflow language**. Programs are *nodes* that -transform *streams* of values at each clock tick. - -```lustre --- A simple counter that resets when `reset` is true -node counter(reset: bool) returns (count: int); -let - count = if reset then 0 - else (0 -> pre(count) + 1); -tel -``` - -Core operators: - -| `pre(x)` | Previous value of stream `x` (one tick delay) | -|----|----| -| `x` `→` `y` | `x` on first tick, `y` thereafter (initialisation, "followed-by") | -| `x` `fby` `y` | Equivalent to `x` `→` `pre(y)` (followed-by shorthand) | -| `when` | Sample a stream on a slower clock (clock calculus downsampling) | -| `merge` | Combine streams from different clocks back to a base clock | - -**Clock calculus** ensures that every stream expression has a -well-defined sampling rate. Lustreiser generates clock annotations and -verifies them against the Idris2 ABI timing proofs. - -# How It Works - -Describe your real-time control system in `lustreiser.toml`. Lustreiser: - -1. **Analyses control flow** — parses your manifest to extract dataflow - topology, timing requirements, and I/O declarations - -2. **Generates Lustre nodes** — produces `.lus` files with correct - clock annotations, `pre`/`fby` temporal operators, and - `when`/`merge` clock calculus expressions - -3. **Proves timing bounds** — the Idris2 ABI layer formally verifies - that worst-case execution time (WCET) for every node fits within the - declared clock period - -4. **Compiles to deterministic C** — the Lustre compiler produces C - code with no `malloc`, no recursion, no unbounded loops, and - statically allocated buffers — suitable for bare-metal embedded - targets - -5. **Bridges via Zig FFI** — the generated C is wrapped in a Zig FFI - layer for integration with Rust, Idris2, and other -iser components - -# Architecture - -Follows the hyperpolymath -iser pattern: - - lustreiser.toml ← user describes control system - │ - ▼ - ┌─────────────────────┐ - │ Rust CLI │ Parse manifest, validate topology - │ src/main.rs │ - └────────┬────────────┘ - │ - ▼ - ┌─────────────────────┐ - │ Control Flow │ Extract dataflow graph, identify - │ Analysis │ nodes, clocks, temporal operators - └────────┬────────────┘ - │ - ▼ - ┌─────────────────────┐ - │ Idris2 ABI │ Prove timing bounds (WCET), - │ src/interface/abi/ │ verify clock calculus, validate - │ │ stream buffer layouts - └────────┬────────────┘ - │ - ▼ - ┌─────────────────────┐ - │ Lustre Codegen │ Generate .lus files with clock - │ src/codegen/ │ annotations, pre/fby/when/merge - └────────┬────────────┘ - │ - ▼ - ┌─────────────────────┐ - │ C Compilation │ Lustre → deterministic C - │ (no malloc, no │ (static buffers, bounded loops) - │ recursion) │ - └────────┬────────────┘ - │ - ▼ - ┌─────────────────────┐ - │ Zig FFI Bridge │ C-ABI wrapper for integration - │ src/interface/ffi/ │ with Rust and -iser ecosystem - └─────────────────────┘ - -# Use Cases - -- **Flight control systems** — attitude controllers, autopilot mode - logic, sensor fusion with guaranteed response times (DO-178C Level A) - -- **Engine management units** — fuel injection timing, ignition - scheduling, emission control loops (ISO 26262 ASIL D) - -- **Nuclear reactor protection** — rod insertion logic, coolant - monitoring, trip systems (IEC 61508 SIL 3/4) - -- **PLC programming** — replacing ladder logic with formally verified - synchronous controllers for industrial automation - -- **Sensor fusion** — combining accelerometer, gyroscope, and - magnetometer streams with proven latency bounds - -- **Robotic actuator control** — servo loops, trajectory planning with - hard real-time constraints - -# Build - -```bash -cargo build --release -cargo test -``` - -# Status - -**Codebase in progress.** Architecture defined, CLI scaffolded, RSR -template complete. Codegen stubs in place — Lustre node generation, -clock calculus, and WCET analysis are the next implementation targets. -See `ROADMAP.adoc` for the full phased plan. - -# License - -SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/SECURITY.md b/SECURITY.adoc similarity index 58% rename from SECURITY.md rename to SECURITY.adoc index 61ae898..1fae521 100644 --- a/SECURITY.md +++ b/SECURITY.adoc @@ -1,21 +1,24 @@ -# Security Policy +== Security Policy -## Supported Versions +=== Supported Versions -| Version | Supported | -|---------|-----------| -| 0.1.x | ✅ | +[cols=",",options="header",] +|=== +|Version |Supported +|0.1.x |✅ +|=== -## Reporting a Vulnerability +=== Reporting a Vulnerability Please report security vulnerabilities to: j.d.a.jewell@open.ac.uk Do NOT open a public issue for security vulnerabilities. -## Response Time +=== Response Time -We aim to respond within 48 hours and provide a fix within 7 days for critical issues. +We aim to respond within 48 hours and provide a fix within 7 days for +critical issues. -## Scope +=== Scope This policy covers the lustreiser CLI tool and its generated artifacts. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..43b4acb --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,30 @@ +== TEST-NEEDS.md — lustreiser + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current Test State + +[cols=",,",options="header",] +|=== +|Category |Count |Notes +|Test files |2 |Current state +|=== + +=== What’s Covered + +* [x] 2 existing test file(s) +* [x] Rust integration tests + +=== Still Missing (for CRG B+) + +* [ ] Zig FFI tests (if applicable) +* [ ] CI/CD test automation +* [ ] Property-based tests +* [ ] Edge case coverage + +=== Run Tests + +[source,bash] +---- +cargo test --all +---- diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 44811c6..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,27 +0,0 @@ -# TEST-NEEDS.md — lustreiser - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current Test State - -| Category | Count | Notes | -|----------|-------|-------| -| Test files | 2 | Current state | - -## What's Covered - -- [x] 2 existing test file(s) -- [x] Rust integration tests - -## Still Missing (for CRG B+) - -- [ ] Zig FFI tests (if applicable) -- [ ] CI/CD test automation -- [ ] Property-based tests -- [ ] Edge case coverage - -## Run Tests - -```bash -cargo test --all -``` diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 68% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index ea356a8..c958ff0 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,14 +1,19 @@ - - -# TOPOLOGY.md — lustreiser +== TOPOLOGY.md — lustreiser -## Purpose +=== Purpose -lustreiser generates verified real-time embedded code via Lustre. Lustre (Caspi and Halbwachs, Grenoble) is a synchronous dataflow language used in safety-critical domains including avionics (SCADE), nuclear control, and automotive systems. lustreiser reads control logic descriptions from a `lustreiser.toml` manifest and generates deterministic, bounded-execution-time C code via Lustre intermediate representation. It targets embedded systems engineers who need provably correct, race-free real-time control logic without writing Lustre directly. +lustreiser generates verified real-time embedded code via Lustre. Lustre +(Caspi and Halbwachs, Grenoble) is a synchronous dataflow language used +in safety-critical domains including avionics (SCADE), nuclear control, +and automotive systems. lustreiser reads control logic descriptions from +a `+lustreiser.toml+` manifest and generates deterministic, +bounded-execution-time C code via Lustre intermediate representation. It +targets embedded systems engineers who need provably correct, race-free +real-time control logic without writing Lustre directly. -## Module Map +=== Module Map -``` +.... lustreiser/ ├── src/ │ ├── main.rs # CLI entry point (clap): init, validate, generate, build, run, info @@ -20,11 +25,11 @@ lustreiser/ ├── verification/ # Proof harnesses ├── container/ # Stapeln container ecosystem └── .machine_readable/ # A2ML metadata -``` +.... -## Data Flow +=== Data Flow -``` +.... lustreiser.toml manifest │ ┌────▼────┐ @@ -43,4 +48,4 @@ lustreiser.toml manifest ┌────▼────┐ │ Lustre │ synchronous compiler → bounded-time C for embedded target └─────────┘ -``` +.... diff --git a/docs/architecture/TOPOLOGY.md b/docs/architecture/TOPOLOGY.adoc similarity index 67% rename from docs/architecture/TOPOLOGY.md rename to docs/architecture/TOPOLOGY.adoc index a61547c..824fe20 100644 --- a/docs/architecture/TOPOLOGY.md +++ b/docs/architecture/TOPOLOGY.adoc @@ -1,18 +1,16 @@ - - +== Topology: lustreiser -# Topology: lustreiser +=== Overview -## Overview +Lustreiser generates formally verified real-time embedded code via +Lustre, the synchronous dataflow language. It analyses control logic, +extracts dataflow patterns, generates Lustre nodes with clock calculus, +compiles to deterministic C for embedded targets, and proves timing +bounds via Idris2 dependent types. -Lustreiser generates formally verified real-time embedded code via Lustre, the -synchronous dataflow language. It analyses control logic, extracts dataflow -patterns, generates Lustre nodes with clock calculus, compiles to deterministic -C for embedded targets, and proves timing bounds via Idris2 dependent types. +=== Module Map -## Module Map - -``` +.... lustreiser/ ├── src/ │ ├── main.rs # CLI entry point (clap subcommands) @@ -42,11 +40,11 @@ lustreiser/ └── generated/lustreiser/ # Generated output directory ├── *.lus # Generated Lustre source files └── *.c # Generated deterministic C code -``` +.... -## Data Flow +=== Data Flow -``` +.... ┌──────────────────┐ │ lustreiser.toml │ User-authored manifest │ (TOML) │ describing control system @@ -98,49 +96,86 @@ lustreiser/ │ Output │ for DO-178C, IEC 61508, │ │ ISO 26262 targets └──────────────────┘ -``` - -## Key Types (Idris2 ABI) - -| Type | Module | Purpose | -|------|--------|---------| -| `LustreNode` | Types.idr | A computation unit with I/O streams, clock, and WCET | -| `Clock` | Types.idr | Sampling rate (period + phase in microseconds) | -| `DataflowStream` | Types.idr | Typed stream sampled on a specific clock | -| `TemporalOperator` | Types.idr | Pre, Fby, When, Merge — state and clock operators | -| `WCET` | Types.idr | Proof that a node meets its timing deadline | -| `CompositionSafe` | Types.idr | Proof that composing two nodes preserves bounds | -| `SafetyLevel` | Types.idr | DAL_A, SIL_4, ASIL_D certification tags | -| `StreamBuffer` | Layout.idr | Memory layout for a stream's history buffer | -| `NodeLayout` | Layout.idr | Complete memory layout for a node's state | -| `FitsInRAM` | Layout.idr | Proof that all nodes fit in available static RAM | - -## Zig FFI Functions - -| Function | Purpose | -|----------|---------| -| `lustreiser_init` | Create compilation context (1kHz base clock default) | -| `lustreiser_free` | Destroy context and release resources | -| `lustreiser_compile_nodes` | Parse manifest, generate Lustre nodes | -| `lustreiser_lustre_to_c` | Compile .lus to deterministic C | -| `lustreiser_analyse_wcet` | Compute worst-case execution time (microseconds) | -| `lustreiser_verify_deadline` | Check WCET < clock period | -| `lustreiser_validate_clocks` | Verify clock calculus consistency | -| `lustreiser_get_clock_tree` | Serialise clock hierarchy | -| `lustreiser_calc_memory_budget` | Total static memory for all buffers | -| `lustreiser_check_memory_fit` | Verify budget fits in target RAM | - -## Safety Standards Mapping - -| Standard | Domain | Lustreiser Relevance | -|----------|--------|---------------------| -| DO-178C Level A | Avionics (catastrophic failure) | Flight control, autopilot, sensor fusion | -| IEC 61508 SIL 3/4 | Industrial (nuclear, chemical) | Reactor protection, trip systems | -| ISO 26262 ASIL D | Automotive (life-threatening) | Engine management, braking, steering | - -## Dependencies - -- **Rust** (cargo): CLI, manifest parsing, orchestration -- **Idris2**: Formal proofs of timing bounds and memory layout -- **Zig**: C-ABI bridge, embedded cross-compilation -- **Lustre**: Generated synchronous dataflow code (not a build dependency — generated) +.... + +=== Key Types (Idris2 ABI) + +[width="100%",cols="27%,34%,39%",options="header",] +|=== +|Type |Module |Purpose +|`+LustreNode+` |Types.idr |A computation unit with I/O streams, clock, +and WCET + +|`+Clock+` |Types.idr |Sampling rate (period + phase in microseconds) + +|`+DataflowStream+` |Types.idr |Typed stream sampled on a specific clock + +|`+TemporalOperator+` |Types.idr |Pre, Fby, When, Merge — state and +clock operators + +|`+WCET+` |Types.idr |Proof that a node meets its timing deadline + +|`+CompositionSafe+` |Types.idr |Proof that composing two nodes +preserves bounds + +|`+SafetyLevel+` |Types.idr |DAL_A, SIL_4, ASIL_D certification tags + +|`+StreamBuffer+` |Layout.idr |Memory layout for a stream’s history +buffer + +|`+NodeLayout+` |Layout.idr |Complete memory layout for a node’s state + +|`+FitsInRAM+` |Layout.idr |Proof that all nodes fit in available static +RAM +|=== + +=== Zig FFI Functions + +[width="100%",cols="53%,47%",options="header",] +|=== +|Function |Purpose +|`+lustreiser_init+` |Create compilation context (1kHz base clock +default) + +|`+lustreiser_free+` |Destroy context and release resources + +|`+lustreiser_compile_nodes+` |Parse manifest, generate Lustre nodes + +|`+lustreiser_lustre_to_c+` |Compile .lus to deterministic C + +|`+lustreiser_analyse_wcet+` |Compute worst-case execution time +(microseconds) + +|`+lustreiser_verify_deadline+` |Check WCET < clock period + +|`+lustreiser_validate_clocks+` |Verify clock calculus consistency + +|`+lustreiser_get_clock_tree+` |Serialise clock hierarchy + +|`+lustreiser_calc_memory_budget+` |Total static memory for all buffers + +|`+lustreiser_check_memory_fit+` |Verify budget fits in target RAM +|=== + +=== Safety Standards Mapping + +[width="100%",cols="27%,20%,53%",options="header",] +|=== +|Standard |Domain |Lustreiser Relevance +|DO-178C Level A |Avionics (catastrophic failure) |Flight control, +autopilot, sensor fusion + +|IEC 61508 SIL 3/4 |Industrial (nuclear, chemical) |Reactor protection, +trip systems + +|ISO 26262 ASIL D |Automotive (life-threatening) |Engine management, +braking, steering +|=== + +=== Dependencies + +* *Rust* (cargo): CLI, manifest parsing, orchestration +* *Idris2*: Formal proofs of timing bounds and memory layout +* *Zig*: C-ABI bridge, embedded cross-compilation +* *Lustre*: Generated synchronous dataflow code (not a build dependency +— generated) diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..d1c4ae0 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — lustreiser (Developer) + +=== What is lustreiser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 3a48bd5..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — lustreiser (Developer) - -## What is lustreiser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..93238ef --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — lustreiser (User) + +=== What is lustreiser? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 528c0a1..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — lustreiser (User) - -## What is lustreiser? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture