diff --git a/examples/pulseengine-fixvec/Makefile b/examples/pulseengine-fixvec/Makefile new file mode 100644 index 0000000..c176649 --- /dev/null +++ b/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 diff --git a/examples/pulseengine-fixvec/README.md b/examples/pulseengine-fixvec/README.md new file mode 100644 index 0000000..a41c8a9 --- /dev/null +++ b/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; + ... + } + +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. diff --git a/examples/pulseengine-fixvec/arch/fixvec.aadl b/examples/pulseengine-fixvec/arch/fixvec.aadl new file mode 100644 index 0000000..b2089bc --- /dev/null +++ b/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). A heap-storage variant would + -- be a sibling .heap implementation here. + properties + ARP4761::Implementation_Strategy => "inline_storage"; + end FixVecComponent.inline; + +end FixVec; diff --git a/examples/pulseengine-fixvec/arch/fixvec.wit b/examples/pulseengine-fixvec/arch/fixvec.wit new file mode 100644 index 0000000..41eafa0 --- /dev/null +++ b/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; + + /// 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; + + /// 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; +} + +/// The world the FixVec component exports. +world fixvec-component { + export fix-vec; +} diff --git a/examples/pulseengine-fixvec/artifacts/fixvec.yaml b/examples/pulseengine-fixvec/artifacts/fixvec.yaml new file mode 100644 index 0000000..377a7bc --- /dev/null +++ b/examples/pulseengine-fixvec/artifacts/fixvec.yaml @@ -0,0 +1,169 @@ +# FixVec interface — pulseengine treatment of the eclipse-score +# `logic_arc_int__b_r__fixvec` + 5× `logic_arc_int_op__cont__fixvec_*` +# need declarations. +# +# Hand-authored for this worked example. A real converter would emit +# this shape from the eclipse RST automatically (TYPE_MAP already +# covers logic_arc_int / logic_arc_int_op via the playground's +# tools/score_import.py). + +artifacts: + + # ── The interface itself ─────────────────────────────────────────── + - id: LOGIC-ARC-INT-FIXVEC + type: logic-arc-int + title: Fixed-Capacity Vector + status: approved + description: > + A fixed-capacity vector with inline storage. Provides the + classical vector operations bounded by a compile-time CAPACITY. + Equivalent to eclipse-score's logic_arc_int__b_r__fixvec. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + + # ── The five operations ──────────────────────────────────────────── + # Each maps to one eclipse logic_arc_int_op need. The + # `belongs-to → LOGIC-ARC-INT-FIXVEC` link is the rivet equivalent + # of eclipse's `:included_by:` back-reference. + + - id: LOGIC-ARC-INT-OP-FIXVEC-PUSH + type: logic-arc-int + title: Push + status: approved + description: > + Append an element. Fails with InsufficientCapacity if the + vector is full. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + links: + - type: belongs-to + target: LOGIC-ARC-INT-FIXVEC + + - id: LOGIC-ARC-INT-OP-FIXVEC-POP + type: logic-arc-int + title: Pop + status: approved + description: > + Remove and return the last element, or None if the vector is empty. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + links: + - type: belongs-to + target: LOGIC-ARC-INT-FIXVEC + + - id: LOGIC-ARC-INT-OP-FIXVEC-CLEAR + type: logic-arc-int + title: Clear + status: approved + description: Remove all elements; reset length to zero. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + links: + - type: belongs-to + target: LOGIC-ARC-INT-FIXVEC + + - id: LOGIC-ARC-INT-OP-FIXVEC-INDEX + type: logic-arc-int + title: Index + status: approved + description: > + Random access to the i-th element. Bounds-checked; panics on + out-of-bounds in std, returns Option in no-std variants. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + links: + - type: belongs-to + target: LOGIC-ARC-INT-FIXVEC + + - id: LOGIC-ARC-INT-OP-FIXVEC-ITERATE + type: logic-arc-int + title: Iterate + status: approved + description: Borrow the contents as a slice; iterator protocol. + fields: + safety-level: ASIL_B + security: "YES" + tags: [baselibs-rust, containers, fixvec] + links: + - type: belongs-to + target: LOGIC-ARC-INT-FIXVEC + + # ── The architectural component that ships the interface ─────────── + # Eclipse: comp_arc_sta__baselibs_rust__containers_rust + # Pulseengine: a `comp` artifact with `provides:` link to the interface. + + - id: COMP-BASELIBS-CONTAINERS-RUST + type: comp + title: Rust Containers + status: approved + description: > + Component providing the inline / heap-storage vector + implementations. Equivalent to eclipse's + comp_arc_sta__baselibs_rust__containers_rust. + fields: + safety-level: ASIL_B + security: "YES" + component-type: library + tags: [baselibs-rust, containers] + links: + - type: provides + target: LOGIC-ARC-INT-FIXVEC + + # ── Detailed design — bridges the interface to the implementation ── + # The score schema enforces `sw-unit → dd-sta → comp-req` rather than + # `sw-unit → interface` directly. This is the realistic eclipse + # pattern: detailed design (dd_sta) sits between the architecture + # interface and the implementing source file. + + - id: DD-STA-FIXVEC-INLINE + type: dd-sta + title: InlineVec detailed design + status: approved + description: > + Static design: `#[repr(transparent)] struct InlineVec` + wrapping a `GenericVec>`. Backs the FixVec + interface with inline (no-heap) storage. CAPACITY must be in + [1, u32::MAX]. + fields: + safety-level: ASIL_B + view-type: class-diagram + tags: [baselibs-rust, containers, design] + links: + - type: belongs-to + target: COMP-BASELIBS-CONTAINERS-RUST + + # ── Cited source: the actual Rust implementation file ────────────── + # This is the pulseengine equivalent of eclipse's `source_code_link` + # field but explicit and content-hashed. In a real build, the + # `wit-bindgen` step would generate a trait against arch/fixvec.wit + # and the Rust impl would implement that trait — making the + # interface-to-implementation link binary, not documentary. + + - id: SRC-INLINEVEC-RS + type: sw-unit + title: InlineVec implementation + status: approved + description: > + Hand-written Rust implementation of the FixVec interface using + inline storage. Lives in the upstream baselibs_rust repo at + score/baselibs_rust/src/containers/inline/vec.rs. + fields: + safety-level: ASIL_B + source-file: "upstream/eclipse-score-baselibs_rust/src/containers/inline/vec.rs" + language: rust + tags: [baselibs-rust, containers, impl] + links: + - type: implements + target: DD-STA-FIXVEC-INLINE + - type: belongs-to + target: COMP-BASELIBS-CONTAINERS-RUST diff --git a/examples/pulseengine-fixvec/rivet.yaml b/examples/pulseengine-fixvec/rivet.yaml new file mode 100644 index 0000000..623c923 --- /dev/null +++ b/examples/pulseengine-fixvec/rivet.yaml @@ -0,0 +1,17 @@ +# Worked example — eclipse-score FixVec interface in rivet typed YAML. +# +# Self-contained rivet project. The artifacts under `artifacts/` are +# the pulseengine equivalent of the typed needs eclipse-score declares +# at upstream/baselibs_rust/docs/baselibs_rust/containers_rust/architecture/index.rst. +# +# Run from this directory: +# rivet --schemas ../../vendor/rivet-schemas validate +project: + name: pulseengine-fixvec + version: "0.1.0" + schemas: + - common + - score +sources: + - path: artifacts + format: generic-yaml