example: FixVec — pulseengine treatment of eclipse's logic_arc_int

examples/pulseengine-fixvec/Makefile

@@ -0,0 +1,33 @@
+# Worked example — eclipse-score FixVec interface, pulseengine treatment.
+#
+#   make validate   rivet validates the typed artifacts (always available)
+#   make aadl       spar validates the AADL package (requires spar in PATH)
+#   make wit        spar emits WIT from AADL and diffs against arch/fixvec.wit
+
+RIVET ?= rivet
+SPAR  ?= spar
+SCHEMAS := ../../vendor/rivet-schemas
+
+.PHONY: all validate aadl wit clean
+
+all: validate
+
+validate:
+	@$(RIVET) --schemas $(SCHEMAS) validate
+
+aadl:
+	@command -v $(SPAR) >/dev/null 2>&1 || { \
+	    echo "spar not in PATH — install from https://github.com/pulseengine/spar"; \
+	    exit 0; }
+	@$(SPAR) validate arch/fixvec.aadl
+
+wit:
+	@command -v $(SPAR) >/dev/null 2>&1 || { \
+	    echo "spar not in PATH — skipping AADL→WIT round-trip check"; \
+	    exit 0; }
+	@$(SPAR) emit --format wit arch/fixvec.aadl > /tmp/fixvec.spar.wit
+	@diff -u arch/fixvec.wit /tmp/fixvec.spar.wit \
+	    && echo "AADL → WIT round-trip matches arch/fixvec.wit"
+
+clean:
+	@rm -f /tmp/fixvec.spar.wit

examples/pulseengine-fixvec/README.md

@@ -0,0 +1,141 @@
+# Worked example — eclipse-score `FixVec` interface, pulseengine treatment
+
+Eclipse-score declares the `FixVec` interface as a sphinx-needs typed-graph
+of documents: one `logic_arc_int` + five `logic_arc_int_op` operations,
+linked into a `comp_arc_sta` component. The actual Rust implementation
+lives separately in `baselibs_rust/src/containers/inline/vec.rs` —
+hand-written, with no automated connection to the interface need.
+
+This directory shows what that same interface looks like when expressed
+in the **pulseengine stack** (rivet typed artifacts + spar AADL + WIT
+binary contract + Rust component). The goal is concrete demonstration,
+not advocacy: every file here is the equivalent of something eclipse
+already has, just expressed in a different vocabulary.
+
+## What's the same
+
+The data is the same. Five operations on a fixed-capacity vector:
+push, pop, clear, index, iterate. Safety classification ASIL_B,
+security YES. Both stacks model these as typed entities in a graph.
+
+## What's different
+
+The pulseengine treatment goes one step further: the AADL package
+emits a WIT (WebAssembly Interface Type) file that is **link-time
+enforced** by the Rust component. If the Rust implementation's
+signature drifts from the declared interface, the build fails. In
+eclipse's stack, the interface need and the source code are two
+hand-maintained artifacts with no mechanical link — a developer can
+rename `fn push` and the interface document stays unchanged.
+
+This is the central operational difference: eclipse models the
+interface as a *specification* (a document), pulseengine models it
+as a *contract* (a binary obligation).
+
+## Files
+
+| File | What | Eclipse equivalent |
+|---|---|---|
+| `artifacts/fixvec.yaml` | rivet typed artifacts for the interface + 5 ops + safety classification | `logic_arc_int__b_r__fixvec` + 5× `logic_arc_int_op__cont__fixvec_*` need declarations in `baselibs_rust/docs/baselibs_rust/containers_rust/architecture/index.rst` |
+| `arch/fixvec.aadl` | spar AADL package modelling the interface as a typed AADL `feature` with provider/consumer ports and ASIL property | None — eclipse has no architecture-model file; `draw_interface` walks the need-graph at sphinx-build time to produce a PlantUML diagram |
+| `arch/fixvec.wit` | WIT file `spar` emits from the AADL — the binary contract | None — eclipse's interface stops at the rendered diagram |
+| `rivet.yaml` | rivet project: declares schemas + sources + the cross-link namespace | per-repo eclipse `conf.py` plus the metamodel imported via `score_sphinx_bundle` |
+| `Makefile` | `make validate` — rivet validates the typed artifacts and (when spar is installed) checks AADL→WIT consistency | `bazel run //:docs_check` — sphinx validates the need graph |
+
+## Traceability — the same artifact, three forms
+
+```
+                           Eclipse                               Pulseengine
+                          ─────────                             ─────────────
+
+interface declaration      .. logic_arc_int:: Fixed-Capacity     artifacts/fixvec.yaml
+                           Vector                                   id: LOGIC-ARC-INT-FIXVEC
+                              :id: logic_arc_int__b_r__fixvec       type: logic-arc-int
+                              :safety: ASIL_B                       fields:
+                              :security: YES                          safety-level: ASIL_B
+                                                                      security: "YES"
+
+per-operation declaration  .. logic_arc_int_op:: Push             artifacts/fixvec.yaml
+                              :id: ...__fixvec_push                  id: LOGIC-ARC-INT-OP-FIXVEC-PUSH
+                              :included_by:                          type: logic-arc-int
+                                logic_arc_int__b_r__fixvec           links:
+                                                                       - type: belongs-to
+                                                                         target: LOGIC-ARC-INT-FIXVEC
+
+architecture model        none (graph IS the model)              arch/fixvec.aadl
+                                                                    package FixVec public
+                                                                      feature group FixVecOps
+                                                                        push: provides subprogram
+                                                                        ...
+                                                                      properties
+                                                                        ARP4761::SafetyLevel => ASIL_B;
+
+binary contract            none                                  arch/fixvec.wit
+                                                                    interface fix-vec {
+                                                                      push: func(item: u32)
+                                                                          -> result<_, vec-err>;
+                                                                      pop:  func() -> option<u32>;
+                                                                      ...
+                                                                    }
+
+implementation             baselibs_rust/src/containers/          src/lib.rs (sketch — same
+                           inline/vec.rs                           shape as eclipse's vec.rs,
+                              fn push(...) -> Result<...>          but link-time-checked
+                              fn pop(...) -> Option<...>           against arch/fixvec.wit)
+                              ...                                  via wit-bindgen
+```
+
+## Run the validation
+
+```sh
+# rivet validates the typed artifacts
+rivet --schemas ../../vendor/rivet-schemas validate
+
+# spar validates the AADL package (optional — requires spar installed)
+spar validate arch/fixvec.aadl
+
+# wit-bindgen verifies AADL→WIT consistency (optional)
+spar emit --format wit arch/fixvec.aadl | diff - arch/fixvec.wit
+```
+
+When all three pass, the interface specification (rivet artifact) +
+the architectural model (AADL) + the binary contract (WIT) are
+provably aligned. Adding the Rust implementation behind a
+`wit-bindgen`-generated trait gates the build on the same alignment.
+
+## Why this is more than eclipse's `draw_interface`
+
+Eclipse's `score_draw_uml_funcs.draw_interface` walks the typed need
+graph and renders a PlantUML diagram. The diagram is the deliverable.
+
+Pulseengine's spar + WIT does the same diagram render (spar can emit
+PlantUML / Mermaid from the AADL model), **plus** generates the WIT
+contract, **plus** has analysis passes for scheduling / latency /
+ARINC 653 partitioning / EMV2 fault trees that ask
+property-of-the-architecture questions the eclipse stack can only
+ask via prose review.
+
+The diagram is the same; the *gate* around the diagram is different.
+
+## What this is *not*
+
+- Not a working AADL build — `arch/fixvec.aadl` is a hand-written
+  example. To compile it into a real WIT contract you need spar
+  installed (see [`pulseengine/spar`](https://github.com/pulseengine/spar)).
+- Not a complete Rust component — `arch/fixvec.wit` is the
+  intended contract shape; the Rust implementation that links against
+  it would live in a separate project (this example is about the
+  modelling layer, not the runtime).
+- Not a translation tool — the example was written by hand to
+  illustrate the equivalence. A real `tools/score_to_spar.py`
+  converter is future work; see the `kvs` full-stack example
+  (planned) for the next step.
+
+## What this *is*
+
+Concrete answer to the question: *"if I took one piece of eclipse-
+score's work and expressed it the way pulseengine does, what would
+that look like?"* This: same interface, same operations, same safety
+classification — plus an enforceable architectural model and a binary
+contract the implementation has to honour. One worked example, one
+page, real eclipse content as the input.

examples/pulseengine-fixvec/arch/fixvec.aadl

@@ -0,0 +1,119 @@
+-- spar-flavoured AADL package modelling the FixVec interface.
+--
+-- This is the pulseengine equivalent of eclipse-score's logic_arc_int +
+-- 5 logic_arc_int_op need declarations. Where eclipse stops at "the
+-- typed need graph IS the interface", spar's AADL layer adds:
+--   - typed feature-group with provides/requires direction
+--   - subprogram signatures (typed in/out parameters)
+--   - ARP4761 / ISO 26262 properties bound to the architecture element
+--   - emission to WIT (see ../arch/fixvec.wit) and to Rust traits via
+--     wit-bindgen
+--
+-- This file is hand-authored for the worked example. A real
+-- score-to-aadl converter would emit this shape from the eclipse
+-- typed-need graph.
+--
+-- Validate:  spar validate arch/fixvec.aadl   (when spar is installed)
+
+package FixVec
+public
+  with ARP4761;
+  with Data_Model;
+
+  -- ── The interface: a feature group with 5 typed subprograms ──────
+  --
+  -- Equivalent to eclipse's:
+  --   .. logic_arc_int:: Fixed-Capacity Vector
+  --      :id: logic_arc_int__b_r__fixvec
+  --   + the 5 .. logic_arc_int_op:: children linked via :included_by:
+  feature group FixVecOps
+
+    features
+
+      -- Push: append element. Fails on full.
+      -- Equivalent to logic_arc_int_op__cont__fixvec_push.
+      push : provides subprogram access PushFn;
+
+      -- Pop: remove and return last, or None on empty.
+      pop : provides subprogram access PopFn;
+
+      -- Clear: reset length to zero.
+      clear : provides subprogram access ClearFn;
+
+      -- Index: random access; bounds-checked.
+      index : provides subprogram access IndexFn;
+
+      -- Iterate: borrow contents as slice; iterator protocol.
+      iterate : provides subprogram access IterateFn;
+
+    properties
+      -- ASIL_B classification on the interface as a whole.
+      -- Eclipse encodes the same as `:safety: ASIL_B` on each need.
+      ARP4761::Development_Assurance_Level => ASIL_B;
+      -- Security classification (ISO/SAE 21434).
+      ARP4761::Security_Level => YES;
+  end FixVecOps;
+
+  -- ── The five subprogram signatures ──────────────────────────────
+  --
+  -- This is where the pulseengine stack diverges from eclipse:
+  -- spar emits a typed signature per operation, which becomes the
+  -- WIT contract (see arch/fixvec.wit) which becomes a Rust trait
+  -- via wit-bindgen which is link-time-checked at build.
+  --
+  -- Eclipse stops at "the operation is documented"; pulseengine
+  -- continues to "the operation has a binary contract".
+
+  subprogram PushFn
+    features
+      item       : in parameter Base_Types::Unsigned_32;
+      result     : out parameter Base_Types::Boolean;  -- ok/err
+    properties
+      Data_Model::Base_Type => (classifier (Base_Types::Unsigned_32));
+  end PushFn;
+
+  subprogram PopFn
+    features
+      result     : out parameter Base_Types::Unsigned_32;
+      has_value  : out parameter Base_Types::Boolean;  -- None encoding
+  end PopFn;
+
+  subprogram ClearFn
+    -- no parameters, no return
+  end ClearFn;
+
+  subprogram IndexFn
+    features
+      idx        : in parameter Base_Types::Unsigned_32;
+      result     : out parameter Base_Types::Unsigned_32;
+      has_value  : out parameter Base_Types::Boolean;
+  end IndexFn;
+
+  subprogram IterateFn
+    features
+      callback   : in parameter Base_Types::Unsigned_32;  -- function ptr abstraction
+    -- spar materialises the iterator into a callback-based contract
+    -- so it survives the WIT boundary (WASM components don't have
+    -- native iterator protocols).
+  end IterateFn;
+
+  -- ── The component that ships the interface ──────────────────────
+  -- Equivalent to eclipse's comp_arc_sta__baselibs_rust__containers_rust.
+
+  system FixVecComponent
+    features
+      ops : provides feature group FixVecOps;
+    properties
+      ARP4761::Development_Assurance_Level => ASIL_B;
+      ARP4761::Security_Level => YES;
+  end FixVecComponent;
+
+  system implementation FixVecComponent.inline
+    -- Inline-storage variant. Eclipse's FixVec is the inline variant
+    -- (storage: Inline<T, CAPACITY>). A heap-storage variant would
+    -- be a sibling .heap implementation here.
+    properties
+      ARP4761::Implementation_Strategy => "inline_storage";
+  end FixVecComponent.inline;
+
+end FixVec;

examples/pulseengine-fixvec/arch/fixvec.wit

@@ -0,0 +1,58 @@
+// WIT (WebAssembly Interface Type) — the binary contract spar emits
+// from arch/fixvec.aadl.
+//
+// This is the file that makes the pulseengine treatment more than
+// eclipse's "interface as documentation". The Rust implementation
+// of FixVec is required to satisfy this contract at link time —
+// wit-bindgen generates a trait, the impl provides it, the WASM
+// component link step fails if the signature drifts.
+//
+// In eclipse's setup, the equivalent step doesn't exist: the
+// interface need (logic_arc_int__b_r__fixvec + 5 ops) and the Rust
+// implementation (vec.rs::fn push) are two hand-maintained
+// artifacts; a developer can rename `fn push` and the interface
+// need stays unchanged, with nothing complaining.
+
+package pulseengine:fixvec@0.1.0;
+
+/// The fixed-capacity vector interface, as a binary contract.
+///
+/// Lifted from eclipse-score's logic_arc_int__b_r__fixvec, which
+/// declares the same 5 operations at the spec level but doesn't
+/// bind them to typed signatures.
+interface fix-vec {
+    /// Errors that the FixVec operations can return.
+    variant vec-err {
+        /// The vector is full and cannot accept more elements.
+        insufficient-capacity,
+        /// Index is out of bounds for the current vector length.
+        out-of-bounds,
+    }
+
+    /// Append an element. Fails with insufficient-capacity if full.
+    /// Eclipse equivalent: logic_arc_int_op__cont__fixvec_push
+    push: func(item: u32) -> result<_, vec-err>;
+
+    /// Remove and return the last element, or none if empty.
+    /// Eclipse equivalent: logic_arc_int_op__cont__fixvec_pop
+    pop: func() -> option<u32>;
+
+    /// Remove all elements; reset length to zero.
+    /// Eclipse equivalent: logic_arc_int_op__cont__fixvec_clear
+    clear: func();
+
+    /// Random access to the i-th element.
+    /// Eclipse equivalent: logic_arc_int_op__cont__fixvec_index
+    index: func(idx: u32) -> result<u32, vec-err>;
+
+    /// Borrow the contents as a slice (length + pointer in the
+    /// WASM-component ABI). Iterator protocol is provided by the
+    /// host-side wrapper around this primitive.
+    /// Eclipse equivalent: logic_arc_int_op__cont__fixvec_iterate
+    iterate: func() -> list<u32>;
+}
+
+/// The world the FixVec component exports.
+world fixvec-component {
+    export fix-vec;
+}