docs: bespoke Lustre documentation for all template files

Replace generic -iser template placeholders with Lustre-specific content
across the entire repository. Idris2 ABI now defines LustreNode, Clock,
DataflowStream, TemporalOperator (Pre/Fby/When/Merge), WCET timing proofs,
StreamBuffer/NodeLayout memory proofs, and SafetyLevel certification tags.
Zig FFI implements Lustre compilation, WCET analysis, clock calculus
validation, and memory budget verification. README covers synchronous
dataflow semantics, clock calculus, safety standards (DO-178C, IEC 61508,
ISO 26262), and use cases. ROADMAP defines six phases from scaffold through
SCADE interop. TOPOLOGY.md documents module map and data flow.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,12 +1,12 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# AGENTIC.a2ml — AI agent constraints and capabilities
+# AGENTIC.a2ml — AI agent constraints and capabilities for lustreiser
 # Defines what AI agents can and cannot do in this repository.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [agent-permissions]
 can-edit-source = true
@@ -22,6 +22,17 @@ can-create-files = true
 # - Never use banned languages (TypeScript, Python, Go, etc.)
 # - Never place state files in repository root (must be in .machine_readable/)
 # - Never use AGPL license (use PMPL-1.0-or-later)
+# - Never generate C code with malloc, recursion, or unbounded loops
+# - Never weaken WCET proofs or skip timing verification
+# - Never generate Lustre code with ambiguous clock assignments
+
+[lustre-specific-constraints]
+# Generated C output must be deterministic and certifiable:
+# - No dynamic memory allocation (malloc/calloc/realloc)
+# - No recursion (bounded call depth only)
+# - No unbounded loops (iteration counts known at compile time)
+# - All stream buffers statically allocated
+# - WCET must be proven less than clock period for every node
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -6,14 +6,28 @@
   (version "0.1.0")
   (name "lustreiser")
   (type "tool")
-  (purpose "Generate formally verified real-time embedded code via Lustre")
+  (purpose "Generate formally verified real-time embedded code via Lustre synchronous dataflow")
 
   (position-in-ecosystem
     (family "-iser acceleration frameworks")
     (meta-framework "iseriser")
     (relationship "sibling")
+    (domain "safety-critical real-time embedded systems")
     (top-3 ("typedqliser" "chapeliser" "verisimiser")))
 
+  (target-domain
+    (primary "Avionics flight control (DO-178C)")
+    (secondary "Nuclear reactor protection (IEC 61508)")
+    (tertiary "Automotive powertrain (ISO 26262)")
+    (additional "PLC programming, sensor fusion, robotic actuator control"))
+
+  (lustre-ecosystem
+    (language "Lustre — Caspi, Pilaud, Halbwachs, Plaice (Grenoble, 1987)")
+    (industrial-tool "SCADE Suite (Ansys/Esterel Technologies)")
+    (model-checker "Kind2 (University of Iowa)")
+    (reference-compiler "Lv6 / Lustre V6")
+    (related-language "Esterel — synchronous reactive (events, not dataflow)"))
+
   (related-projects
     (project "iseriser"
       (relationship "meta-framework")
@@ -32,7 +46,7 @@
       (description "Database recovery via constraint propagation"))
     (project "proven"
       (relationship "dependency")
-      (description "Shared Idris2 verified library"))
+      (description "Shared Idris2 verified library — timing proofs reuse proven primitives"))
     (project "typell"
       (relationship "dependency")
-      (description "Type theory engine"))))
+      (description "Type theory engine — used for clock calculus type checking"))))

.machine_readable/6a2/META.a2ml

@@ -4,38 +4,56 @@
 
 (meta
   (version "0.1.0")
-  (last-updated "2026-03-20")
+  (last-updated "2026-03-21")
 
   (architecture-decisions
     (adr "001-iser-pattern"
       (status "accepted")
-      (context "Need to make powerful languages accessible without steep learning curves")
-      (decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW")
-      (consequences "Users write zero target language code; all complexity in the -iser"))
+      (context "Need to make Lustre synchronous dataflow programming accessible without requiring Lustre expertise")
+      (decision "Use manifest-driven code generation: user describes control system in TOML, lustreiser generates Lustre nodes, proves timing bounds, and compiles to deterministic C")
+      (consequences "Users write zero Lustre code; all clock calculus and temporal operators generated automatically"))
 
     (adr "002-abi-ffi-standard"
       (status "accepted")
-      (context "Need verified interop between Rust CLI, target language, and user code")
-      (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge")
-      (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs"))
+      (context "Need verified interop between Rust CLI, Lustre compilation, and embedded C output")
+      (decision "Idris2 ABI for formal timing proofs (WCET bounds, clock calculus soundness), Zig FFI for C-ABI bridge to Lustre compiler")
+      (consequences "Compile-time guarantee that every node meets its deadline; zero runtime overhead from proofs"))
 
-    (adr "003-rsr-template"
+    (adr "003-synchronous-hypothesis"
+      (status "accepted")
+      (context "Lustre assumes all computations complete within one clock tick (synchronous hypothesis)")
+      (decision "Enforce synchronous hypothesis via Idris2 WCET proofs: prove that worst-case execution time is strictly less than clock period for every node")
+      (consequences "Generates only code that provably meets hard real-time deadlines; rejects specifications that cannot be proven safe"))
+
+    (adr "004-deterministic-c-output"
+      (status "accepted")
+      (context "Safety-critical standards (DO-178C, IEC 61508, ISO 26262) require deterministic, bounded-time execution")
+      (decision "Generated C code must use no malloc, no recursion, no unbounded loops, and only statically allocated buffers")
+      (consequences "Output is certifiable for safety-critical deployment; memory footprint is known at compile time"))
+
+    (adr "005-rsr-template"
       (status "accepted")
       (context "Need consistent project structure across 29+ -iser repos")
       (decision "All repos cloned from rsr-template-repo with full CI/CD and governance")
       (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")))
 
   (development-practices
-    (language "Rust" (purpose "CLI and orchestration"))
-    (language "Idris2" (purpose "ABI formal proofs"))
-    (language "Zig" (purpose "FFI C-ABI bridge"))
+    (language "Rust" (purpose "CLI, manifest parsing, orchestration"))
+    (language "Idris2" (purpose "ABI formal proofs — timing bounds, clock calculus, memory layout"))
+    (language "Zig" (purpose "FFI C-ABI bridge — Lustre compilation and timing analysis"))
+    (language "Lustre" (purpose "Generated synchronous dataflow code — nodes, clocks, temporal operators"))
+    (language "C" (purpose "Final embedded output — deterministic, no-malloc, certifiable"))
     (build-tool "cargo")
     (ci "GitHub Actions (17 workflows)"))
 
   (design-rationale
     (principle "Manifest-driven"
       (explanation "User intent captured in TOML; all generation is deterministic and reproducible"))
-    (principle "Formally verified bridges"
-      (explanation "Idris2 dependent types prove interface correctness at compile time"))
+    (principle "Formally verified timing"
+      (explanation "Idris2 dependent types prove WCET < clock period for every generated node"))
+    (principle "Clock calculus soundness"
+      (explanation "Every stream has exactly one clock; when/merge operators are type-checked for consistency"))
     (principle "Zero target language exposure"
-      (explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything"))))
+      (explanation "Users never write Lustre, C, or Zig — the -iser handles everything"))
+    (principle "Safety-certifiable output"
+      (explanation "Generated C code targets DO-178C Level A, IEC 61508 SIL 4, ISO 26262 ASIL D"))))

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,23 +1,27 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# NEUROSYM.a2ml — Neurosymbolic integration metadata
+# NEUROSYM.a2ml — Neurosymbolic integration metadata for lustreiser
 # Configuration for Hypatia scanning and symbolic reasoning.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [hypatia-config]
 scan-enabled = true
-scan-depth = "standard"  # quick | standard | deep
+scan-depth = "deep"  # Deep scanning for safety-critical code
 report-format = "logtalk"
 
 [symbolic-rules]
-# Custom symbolic rules for this project
+# Custom symbolic rules for lustreiser safety invariants:
 # - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" }
+# - { name = "no-malloc-in-generated-c", pattern = "malloc|calloc|realloc", severity = "critical" }
+# - { name = "no-recursion-in-generated-c", pattern = "recursive", severity = "critical" }
+# - { name = "wcet-proof-required", pattern = "MeetsDeadline", severity = "warning" }
+# - { name = "clock-consistency", pattern = "ClockError", severity = "critical" }
 
 [neural-config]
-# Neural pattern detection settings
-# confidence-threshold = 0.85
+# Neural pattern detection for dataflow analysis
+# confidence-threshold = 0.95  # Higher threshold for safety-critical domain
 # model = "hypatia-v2"

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,29 +1,37 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# PLAYBOOK.a2ml — Operational playbook
+# PLAYBOOK.a2ml — Operational playbook for lustreiser
 # Runbooks, incident response, deployment procedures.
 
 [metadata]
 version = "0.1.0"
-last-updated = "{{CURRENT_DATE}}"
+last-updated = "2026-03-21"
 
 [deployment]
-# method = "gitops"  # gitops | manual | ci-triggered
-# target = "container"  # container | binary | library | wasm
+method = "binary"  # CLI binary distributed via cargo install or container
+target = "binary"  # Primary output is a CLI tool; secondary output is generated C code
+
+[embedded-target-deployment]
+# Generated C code deployment to embedded targets:
+# 1. Run `lustreiser generate` to produce .lus and .c files
+# 2. Cross-compile C output for target architecture (ARM Cortex-M, RISC-V)
+# 3. Flash to embedded target
+# 4. Verify timing on hardware matches WCET analysis
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
+# 1. Check .machine_readable/6a2/STATE.a2ml for current status
 # 2. Review recent commits and CI results
-# 3. Run `just validate` to check compliance
+# 3. Run `just validate` to check RSR compliance
 # 4. Run `just security` to audit for vulnerabilities
+# 5. For timing-related issues: re-run WCET analysis with updated code paths
 
 [release-process]
-# 1. Update version in STATE.a2ml, META.a2ml, Justfile
+# 1. Update version in STATE.a2ml, META.a2ml, Cargo.toml, main.zig
 # 2. Run `just release-preflight` (validate + quality + security + maint-hard-pass)
-# 3. Optional local permission hardening: `just perms-snapshot && just perms-lock`
-# 4. Tag and push
-# 5. Restore local permissions if needed: `just perms-restore`
+# 3. Verify all Idris2 timing proofs compile without holes
+# 4. Run integration tests against Zig FFI
+# 5. Tag and push
 # 6. Run `just container-push` if applicable
 
 [maintenance-operations]
@@ -33,3 +41,5 @@ last-updated = "{{CURRENT_DATE}}"
 #   just maint-hard-pass
 # Permission audit:
 #   just perms-audit
+# Timing proof verification:
+#   cd src/interface/abi && idris2 --check Types.idr Layout.idr Foreign.idr

.machine_readable/6a2/STATE.a2ml

@@ -5,31 +5,37 @@
 (state
   (metadata
     (version "0.1.0")
-    (last-updated "2026-03-20")
+    (last-updated "2026-03-21")
     (author "Jonathan D.A. Jewell"))
 
   (project-context
     (name "lustreiser")
-    (description "Generate formally verified real-time embedded code via Lustre")
-    (status "scaffold")
+    (description "Generate formally verified real-time embedded code via Lustre synchronous dataflow")
+    (status "scaffold-documented")
     (priority "—")
-    (ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)"))
+    (ecosystem "-iser family (https://github.com/hyperpolymath/iseriser)")
+    (domain "Safety-critical real-time embedded systems (avionics, nuclear, automotive)")
+    (target-standards "DO-178C, IEC 61508, ISO 26262"))
 
   (current-position
-    (phase "initial-scaffold")
-    (completion-percentage 5)
-    (milestone "Architecture defined, CLI scaffolded, RSR template complete"))
+    (phase "scaffold-with-bespoke-docs")
+    (completion-percentage 10)
+    (milestone "Architecture defined, CLI scaffolded, RSR template complete, bespoke Idris2 ABI types defined"))
 
   (route-to-mvp
-    (step 1 "Replace codegen stubs with target-language-specific generation")
-    (step 2 "Implement Idris2 ABI proofs for core invariants")
-    (step 3 "Build Zig FFI bridge")
-    (step 4 "Integration tests with real-world examples")
-    (step 5 "Documentation and examples"))
+    (step 1 "Implement control flow analysis — parse manifest to extract dataflow topology")
+    (step 2 "Implement Lustre node generation — produce .lus files with clock annotations")
+    (step 3 "Implement clock calculus — when/merge operators, clock consistency checking")
+    (step 4 "Implement WCET analysis — timing bounds for generated C code paths")
+    (step 5 "Write Idris2 proofs for timing bounds (WCET < clock period)")
+    (step 6 "Implement Lustre-to-C compilation backend (no malloc, no recursion)")
+    (step 7 "Integration tests with real embedded targets (ARM Cortex-M, RISC-V)")
+    (step 8 "First working end-to-end example (simple flight controller node)"))
 
   (blockers-and-issues
     (none "Project is in scaffold phase — no blockers yet"))
 
   (critical-next-actions
-    (action "Implement codegen for primary use case")
-    (action "Write first working example end-to-end")))
+    (action "Implement control flow analysis from lustreiser.toml manifest")
+    (action "Generate first .lus file from a simple dataflow specification")
+    (action "Define Lustre-specific manifest schema (nodes, clocks, streams, timing)")))