From da1f3046b4edeb84b2e0ba07d2354e2f2133df09 Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Mon, 4 May 2026 13:51:42 -0600 Subject: [PATCH] docs(readme): qualify the no-unsafe claim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit After Opt #2 (get_unchecked for codegen table indexing), the macro emits ~6 unsafe blocks per chart (in apply_path, do_terminate, follow_defaults, and step's __DISPATCH lookup). Each is a bounded get_unchecked into a codegen-owned static table whose `idx < len` invariant holds by construction (state ids are produced by codegen itself, not user input). User code remains unsafe-free. Update both bullets: - "no Mutex, no unsafe" → "no Mutex, no unsafe in your code" (in the during/split-borrow context) - "No heap, no unsafe, no dynamic dispatch" → drop the unsafe exception with an honest one-sentence note about where it lives and why. --- README.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index ed89b8f..dd09b01 100644 --- a/README.md +++ b/README.md @@ -155,7 +155,7 @@ For nested-state hierarchies, `emit(...)`, `terminate`, and async fn that runs while a state is active and is dropped when you leave. Multiple durings on the active path race concurrently and split-borrow disjoint context fields — no `RefCell`, no `Mutex`, - no `unsafe`. + no `unsafe` in your code. - **`m.run().await` is the whole task.** It races durings, the event channel, and timer deadlines, and parks the executor between them. No manual loop, no busy-waits, no `Send` headaches under @@ -171,9 +171,11 @@ For nested-state hierarchies, `emit(...)`, `terminate`, and input produces a byte-identical journal. The runtime's event queue and timer table are formally verified — Creusot + Why3 + alt-ergo + z3 discharge the proofs (`just verify`). -- **No heap, no `unsafe`, no dynamic dispatch.** Pure monomorphized - code. `no_std` clean by default. Designed to fit on a Cortex-M0+ - under embassy. +- **No heap, no dynamic dispatch.** Pure monomorphized code. + `no_std` clean by default. Designed to fit on a Cortex-M0+ under + embassy. The macro emits a small amount of `unsafe` (bounded + `get_unchecked` indexing into codegen-emitted tables whose layout + guarantees `idx < len` by construction); your code is `unsafe`-free. ## How a chart behaves — the rules