fix: address 4-reviewer findings + add dev/prod variants with bazel rustc profile

Reviewer fixes
--------------
- INLINE-STORAGE de-greenwashed: surface test removed, verified-by emptied;
  verify gate now reports MISSING (not falsely PASSED) for the no-runtime-
  allocation requirement that needs witness instrumentation we don't wire.
- DR-KVS-BACKEND-CHOICE rewritten: matches the actual vendored impl
  (json_backend.rs with Adler32 + fs::rename snapshot rotation), not the
  fabricated RocksDB ADR that contradicted the code.
- DR-KVS-INLINE-STORAGE-GAP added: records the three honest response
  options (witness wiring / heapless / spec downgrade) so the gap has
  an audit trail.
- 9 upstream miri_test targets restored via tools/miri.sh + `make miri`
  (cargo-miri wrapper — public rules_rust 0.70 has no miri_test rule;
  eclipse-score uses a private 0.68.2-score fork).
- verify.py: mutable-default-arg fixed (_LIST_CACHE module-level dict);
  bazel build errors no longer swallowed by capture_output=True.
- README: explicit that C++ has the same gap (kvs.cpp:24 carries an
  open `// TODO String Handling in set_value TBD`); :status: valid in
  sphinx-needs framing clarified as "approved-for-design" not
  "must-be-implemented"; 6-of-35 comp-req scope rationale recorded.

Variants model
--------------
- variants/feature-model.yaml + bindings.yaml declare two deployment
  contexts: `dev` (engineering iteration) and `prod` (release-mode
  safety builds).
- Each variant binds three axes by name: (a) KvsBuilder runtime dials
  (KvsDefaults/KvsLoad/snapshot_max_count), (b) bazel --config= profile
  in /.bazelrc, (c) audit scope (out-of-scope-for: list).
- /.bazelrc adds --config=dev (fastbuild) and --config=prod (compilation_
  mode=opt + lto=fat + codegen-units=1 + overflow-checks=on + strip=
  symbols + embed-bitcode=yes). panic=abort lives in a separate
  --config=prod_ship for the shipping binary (Rust's #[test] harness
  needs unwinding outside nightly's -Zpanic_abort_tests).
- Makefile threads VARIANT= through `make verify` and `make bazel`.
- README + variants/README explain the design and why a variant model
  is needed: upstream eclipse-score rust_kvs has NO cargo features in
  the core library, so variants ride on builder dials + bazel rustc-
  flag profiles + audit scope, not --features.

Gate output (variant=dev, default):  3 PASSED, 2 FAILED, 0 MISSING
Gate output (variant=prod):          3 PASSED, 2 FAILED, 1 MISSING

The 2 FAILED are the confirmed-real upstream falsifications of
comp_req__kvs__key_naming and comp_req__kvs__key_length; the MISSING
under prod is INLINE-STORAGE (out-of-scope for dev).

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

Author: avrabe

.bazelrc

@@ -0,0 +1,62 @@
+# example-kvs bazel configuration.
+#
+# Two named build profiles, bound to the variant model in variants/:
+#
+#   --config=dev   — fastbuild, ASAN-friendly, default rustc flags.
+#                    Mirrors the `dev` variant in variants/bindings.yaml.
+#                    Use for engineering iteration.
+#
+#   --config=prod  — release-mode + LTO + single codegen-unit + panic=abort.
+#                    Mirrors the `prod` variant in variants/bindings.yaml.
+#                    These flags are the minimum that an ASIL-B safety case
+#                    typically asks for on Rust builds:
+#                       lto=fat            single translation unit at link time
+#                       codegen-units=1    deterministic, no parallelization noise
+#                       panic=abort        no unwinding (smaller, FuSa-compatible,
+#                                          eliminates the cleanup-path surface)
+#                       opt-level=3        max speed (default for compilation_mode=opt)
+#                       overflow-checks=on intentional — ASIL-B forbids silent UB on
+#                                          integer overflow; cost is a few % in tight
+#                                          loops, acceptable for safety builds
+#                       strip=symbols      smaller binary, debuginfo lives in a
+#                                          separate file (split-debuginfo in CI)
+#
+# `make verify VARIANT=prod` passes `--config=prod` through; same for `make bazel`.
+
+# ── default settings ─────────────────────────────────────────────────
+build --java_language_version=17
+test --test_output=errors
+
+# ── --config=dev (engineering builds) ────────────────────────────────
+build:dev --compilation_mode=fastbuild
+
+# ── --config=prod (safety flags compatible with bazel test) ──────────
+# Used for `make verify VARIANT=prod` and any test-time invocation.
+# panic=abort is INTENTIONALLY OMITTED here: Rust's #[test] harness
+# requires unwinding to report failures and is incompatible with
+# panic=abort outside nightly's -Zpanic_abort_tests. panic=abort lives
+# in --config=prod_ship below for the actually-deployed binary.
+build:prod --compilation_mode=opt
+build:prod --@rules_rust//rust/settings:extra_rustc_flag=-Cembed-bitcode=yes
+build:prod --@rules_rust//rust/settings:extra_rustc_flag=-Clto=fat
+build:prod --@rules_rust//rust/settings:extra_rustc_flag=-Ccodegen-units=1
+build:prod --@rules_rust//rust/settings:extra_rustc_flag=-Coverflow-checks=on
+build:prod --@rules_rust//rust/settings:extra_rustc_flag=-Cstrip=symbols
+# Mirror codegen-units=1 on exec-target crates (proc-macros,
+# build-scripts) so the prod toolchain composes cleanly.
+build:prod --@rules_rust//rust/settings:extra_exec_rustc_flag=-Ccodegen-units=1
+
+# ── --config=prod_ship (the actually-deployed binary only) ───────────
+# Extends --config=prod with panic=abort. Use for `bazel build` of
+# shipping binaries, NEVER for `bazel test`. The deployed ASIL-B
+# Rust binary should not carry the unwinding machinery — smaller
+# code size, no cleanup-path semantics for the assessor to argue
+# about.
+#
+# Typical use:
+#   bazel build --config=prod_ship //:kvs_component
+build:prod_ship --config=prod
+build:prod_ship --@rules_rust//rust/settings:extra_rustc_flag=-Cpanic=abort
+
+# Per-user overrides (gitignored)
+try-import %workspace%/user.bazelrc

Makefile

@@ -8,20 +8,30 @@ SIGIL   ?= sigil
 PYTHON  ?= python3
 SCHEMAS := vendor/rivet-schemas
 
-.PHONY: all validate aadl wit verify attest clean
+.PHONY: all validate aadl wit verify attest miri clean
+
+# ── miri UB-check (vendored rust_kvs, per-module — matches upstream) ─
+# Mirrors the intent of eclipse-score's nine `miri_test` BUILD targets
+# (which live in their custom rules_rust fork). See tools/miri.sh.
+miri:
+	@tools/miri.sh $(MODULE)
 
 # Default: run all checks that work without external dependencies
 # (rivet, the verification gate, and the Bazel WASM-component build).
 # aadl/wit/attest are optional — they require spar / sigil installed.
 all: validate verify bazel
 
 # ── Bazel: real WASM-component build (AADL → WIT → bindgen → component) ─
+# Picks the bazel config from the active variant; see /.bazelrc.
+# `make bazel`              uses dev (fastbuild)
+# `make bazel VARIANT=prod` uses prod (release-mode + LTO + safety flags)
+BAZEL := $(if $(shell command -v bazelisk),bazelisk,bazel)
 bazel:
-	@command -v bazelisk >/dev/null 2>&1 || command -v bazel >/dev/null 2>&1 || { \
+	@command -v $(BAZEL) >/dev/null 2>&1 || { \
 	    echo "bazel(isk) not in PATH — skipping WASM-component build"; \
 	    exit 0; }
-	@$(if $(shell command -v bazelisk),bazelisk,bazel) build //...
-	@$(if $(shell command -v bazelisk),bazelisk,bazel) test  //...
+	@$(BAZEL) build --config=$(VARIANT) //...
+	@$(BAZEL) test  --config=$(VARIANT) //...
 
 # ── rivet typed-artifact validation (always runs) ───────────────────
 validate:
@@ -48,8 +58,13 @@ wit:
 # comp-req with status:approved, finds tests by name convention,
 # reports PASSED / FAILED / MISSING per artifact. Exits 1 if any
 # FAILED or MISSING.
+#
+# Variant selection: `make verify VARIANT=prod` overrides the default
+# `dev` variant. See variants/bindings.yaml for what each variant
+# scopes in or out.
+VARIANT ?= dev
 verify:
-	@$(PYTHON) tools/verify.py --artifacts artifacts
+	@$(PYTHON) tools/verify.py --artifacts artifacts --variant $(VARIANT)
 
 # ── sigil-signed release manifest (optional) ────────────────────────
 attest:

README.md

@@ -32,25 +32,33 @@ This repo:
    `verified-by:` evidence list — there is no stubbing. Each artifact's
    bucket reflects what the real bazel test invocation reported.
 
-## Finding: two upstream comp-reqs are unverified and unenforced
+## Finding: two upstream comp-reqs are unverified and unenforced (both Rust and C++)
 
 Running the gate against the vendored eclipse-score `rust_kvs` surfaces
 a clean-room-verified gap. Two component requirements documented in
 [`persistency/score/kvs/docs/requirements/index.rst`](https://github.com/eclipse-score/persistency/blob/main/score/kvs/docs/requirements/index.rst)
-are accepted (`:status: valid`) but their declared behavior is not
-implemented and not tested:
+are accepted (`:status: valid`) but their declared behavior is neither
+implemented nor tested in *either* language binding:
 
-| Upstream comp-req | RST text (verbatim) | What the impl does |
+| Upstream comp-req | RST text (verbatim) | What both impls do |
 |---|---|---|
-| `comp_req__kvs__key_naming` | "shall accept keys that consist solely of alphanumeric characters, underscores, or dashes" | `Kvs::set_value("with space", _)` returns `Ok(())`. Same for keys containing `.`, `/`, or any other character. |
-| `comp_req__kvs__key_length` | "shall limit the maximum length of a key to 32 bytes" | `Kvs::set_value(&"a".repeat(33), _)` returns `Ok(())`. No length check exists. |
+| `comp_req__kvs__key_naming` | "shall accept keys that consist solely of alphanumeric characters, underscores, or dashes" | `Kvs::set_value("with space", _)` returns `Ok(())` in Rust (`kvs.rs:238`) and the C++ `set_value` (`src/cpp/src/kvs.cpp:24` carries an open `// TODO String Handling in set_value TBD`). Same for `.`, `/`, or any other character. |
+| `comp_req__kvs__key_length` | "shall limit the maximum length of a key to 32 bytes" | `Kvs::set_value(&"a".repeat(33), _)` returns `Ok(())`. No length constant exists in either codebase. |
 
 Verified independently (clean-room search across both Rust and C++
-codebases under eclipse-score): there is no `validate_key` / `check_key`
-function anywhere, no length constant, no test case directive
-(`.. test_case::`) tied to either comp-req, no documentation note saying
-"validation happens at the IPC boundary." Both Rust `set_value` and the
-C++ `set_value` accept any input.
+codebases under eclipse-score): no `validate_key` / `check_key` /
+length-constant symbol exists, no `.. test_case::` directive in
+`score/kvs/docs/` references either comp-req ID, no documentation
+note saying "validation happens at the IPC boundary."
+
+**Context on `:status: valid`.** In the sphinx-needs workflow
+eclipse-score uses, `:status: valid` means "approved for design" —
+not "must be implemented by release X." SCORE is pre-1.0 and this
+state is normal for early-stage projects. The finding's value is not
+"eclipse-score is broken" but "an artifact-driven gate makes the
+spec/impl delta a CI signal, where a coverage dashboard hides it as
+a wedge." The eclipse-score project itself is healthy and well-run;
+the methodology is the lesson.
 
 **The gate calls this out by going RED.** Current `make verify` output:
 
@@ -60,17 +68,24 @@ BUCKET    ID                            EVIDENCE
 PASSED    COMP-REQ-KVS-KEY-ENCODING     1 test(s) all green
 PASSED    COMP-REQ-KVS-VALUE-CHECKSUM   5 test(s) all green
 PASSED    COMP-REQ-KVS-ATOMIC-STORE     5 test(s) all green
-PASSED    COMP-REQ-KVS-INLINE-STORAGE   1 test(s) all green
 FAILED    COMP-REQ-KVS-KEY-NAMING       3 test(s) failed:
                                           - test_..._space_rejected
                                           - test_..._dot_rejected
                                           - test_..._slash_rejected
 FAILED    COMP-REQ-KVS-KEY-LENGTH       1 test(s) failed:
                                           - test_..._32_byte_cap_enforced
+MISSING   COMP-REQ-KVS-INLINE-STORAGE   verified-by is absent or empty
 ─────────────────────────────────────────────────────────────────────
-4 PASSED, 2 FAILED, 0 MISSING
+3 PASSED, 2 FAILED, 1 MISSING
 ```
 
+INLINE-STORAGE is MISSING (not PASSED) on purpose: the spec asks for
+"no runtime heap allocation," upstream uses HashMap + Arc<Mutex> which
+do allocate, and a genuine verifying test requires witness
+allocator-guard instrumentation that this example does not wire.
+DR-KVS-INLINE-STORAGE-GAP records the three response options
+(witness wiring / heapless replacement / spec downgrade).
+
 The surface tests at [`tests/surface/surface_tests.rs`](tests/surface/surface_tests.rs)
 assert exactly what the upstream RST says — no pulseengine-side
 embellishment. CI is intentionally red on this finding.
@@ -173,15 +188,41 @@ example-kvs/
 └── README                           # you are here
 ```
 
+## Variants (dev vs prod)
+
+Two named deployment contexts are declared in [`variants/`](variants/);
+each binds together three axes — KvsBuilder runtime dials, the bazel
+`--config=` profile (`/.bazelrc`), and which comp-reqs the verify
+gate enforces:
+
+| Variant | KvsBuilder dials | bazel profile | Audit scope |
+|---|---|---|---|
+| `dev` (default) | `Defaults::Ignored`, `Load::Ignored`, snapshot=1 | `--config=dev` (fastbuild) | excludes COMP-REQ-KVS-INLINE-STORAGE |
+| `prod` | `Defaults::Required`, `Load::Required`, snapshot=10 | `--config=prod` (compilation_mode=opt + `lto=fat` + `codegen-units=1` + `panic=abort` + `overflow-checks=on` + `strip=symbols`) | full comp-req set |
+
+Select via `VARIANT=…` on any make target:
+
+```sh
+make verify VARIANT=dev      # default
+make verify VARIANT=prod     # full enforcement
+make bazel  VARIANT=prod     # release-mode + LTO + safety rustc flags
+```
+
+Upstream eclipse-score `rust_kvs` has **no cargo features** in the
+core library, so the variant model rides on builder-time dials +
+bazel rustc-flag profiles, not `--features`. See
+[`variants/README.md`](variants/README.md) for the design rationale.
+
 ## Run it
 
 ```sh
-make validate    # rivet validate against the typed schema
-make verify      # artifact-driven verification gate (needs bazel installed)
-make bazel       # bazel build + bazel test //... (the WASM chain)
-make aadl        # spar validates the AADL package (requires spar)
-make wit         # spar AADL → WIT round-trip check (requires spar)
-make attest      # sigil-signed release manifest (requires sigil)
+make validate                       # rivet validate against the typed schema
+make verify [VARIANT=dev|prod]      # artifact-driven verification gate
+make bazel  [VARIANT=dev|prod]      # bazel build + bazel test //...
+make miri   [MODULE=<module>]       # cargo-miri UB check (matches upstream's miri_test intent)
+make aadl                           # spar validates the AADL package (requires spar)
+make wit                            # spar AADL → WIT round-trip check (requires spar)
+make attest                         # sigil-signed release manifest (requires sigil)
 ```
 
 Test the vendored upstream crate directly with cargo:
@@ -205,6 +246,16 @@ bazel test //tests/surface:surface_tests
   workstream — see the
   [playground-eclipse-score](https://github.com/pulseengine/playground-eclipse-score)
   workspace for that.
+- **Not a full mirror of eclipse-score's persistency comp-req set.**
+  Upstream `score/kvs/docs/requirements/index.rst` declares 35
+  comp-reqs; this example carries 6 of them. The selection is a
+  representative slice covering one functional-positive
+  (KEY-ENCODING), one functional-positive-impl-matches-spec
+  (VALUE-CHECKSUM), one durability (ATOMIC-STORE), one
+  non-functional with a real gap (INLINE-STORAGE), and the two that
+  surfaced the finding (KEY-NAMING, KEY-LENGTH). A safety case would
+  need to cover the other 29 explicitly; this example is a
+  methodology demonstrator, not a coverage substitute.
 - **Not endorsed by the Eclipse Foundation or eclipse-score
   maintainers.** This is a pulseengine demonstration that vendors
   upstream Apache-2.0 sources; issues belong here, eclipse-score's

artifacts/requirements.yaml

@@ -268,13 +268,14 @@ artifacts:
       safety-level: ASIL_B
       security: "NO"
       verification-criteria: >
-        Documented gap — the upstream implementation uses HashMap and
-        Arc on the hot path; no allocator guard is wired. A real check
-        requires witness allocator instrumentation. The current
-        surface test PASSES (no guard fires) but the gap is recorded
-        here so future witness wiring closes it.
-      verified-by:
-        - "//tests/surface:surface_tests:test_comp_req_kvs_inline_storage_no_runtime_alloc_documented_gap"
+        No verifying test exists. The upstream implementation uses
+        std::collections::HashMap and Arc<Mutex> on the hot path —
+        both allocate. A real check requires witness allocator
+        instrumentation (witness::no_alloc_guard) which is not wired
+        in this example. The verify gate intentionally reports this
+        comp-req as MISSING (not PASSED) to make the gap auditable.
+        See DR-KVS-INLINE-STORAGE-GAP for the response options.
+      verified-by: []
     tags: [persistency, kvs, memory]
     links:
       - type: satisfies

artifacts/safety-and-decisions.yaml

@@ -65,43 +65,63 @@ artifacts:
 
   - id: DR-KVS-BACKEND-CHOICE
     type: decision-record
-    title: Choose RocksDB over LevelDB for the KVS backend
+    title: JSON file backend with snapshot rotation (no WAL backend)
     status: approved
-    description: Selection of the durable storage backend.
+    description: Selection of the durable storage backend that ships today.
     fields:
       rationale: >
-        RocksDB ships ASIL-relevant write-ahead-logging defaults and
-        has an active maintenance line; LevelDB upstream activity has
-        stalled.
+        Vendored eclipse-score rust_kvs uses a single backend
+        (json_backend.rs:401) that writes (key, value) as a tinyjson
+        document, computes an Adler32 checksum stored in a sibling
+        .hash file, and achieves atomic replace via fs::rename
+        snapshot rotation (json_backend.rs:216-254). Adler32 is the
+        upstream's checksum-of-record despite the comp_req text
+        saying "CRC32C" — that is itself a spec/impl gap.
       alternatives: >
-        LevelDB (rejected: stalled upstream), bespoke append-only log
-        (rejected: re-implements WAL crash-safety).
+        RocksDB or LevelDB or a bespoke write-ahead log were
+        considered upstream but not implemented. The KvsBackend
+        trait (kvs_backend.rs:45) exposes an extension point; only
+        JsonBackend implements it.
       consequences: >
-        Increases binary size by ~1.8 MB; adds a C++ dependency we
-        must track in the SBOM.
+        Atomicity guarantee is bounded by the POSIX fs::rename
+        atomicity (kvs_backend::test_flush_ok and the snapshot_*
+        tests cover the rotation path). Snapshot count caps at
+        json_backend's snapshot_max_count (default 3, runtime-
+        configurable via JsonBackendBuilder::snapshot_max_count).
+        No durability guarantee beyond what the filesystem provides.
     tags: [persistency, kvs, decision]
     links:
       - type: satisfies
         target: COMP-REQ-KVS-ATOMIC-STORE
       - type: belongs-to
         target: COMP-KVS
 
-  - id: DR-KVS-INLINE-STORAGE-FIRST
+  - id: DR-KVS-INLINE-STORAGE-GAP
     type: decision-record
-    title: Inline storage path is the only ASIL-B path
+    title: Inline-storage requirement is unmet by the current backend
     status: approved
-    description: Storage strategy for ASIL-B builds.
+    description: Tracking the gap between the spec and the impl.
     fields:
       rationale: >
-        Heap-storage variant uses dynamic allocation on the hot path,
-        which violates FEAT-REQ-PERSIST-NO-RUNTIME-ALLOC. Inline
-        storage path is the only one certified.
+        COMP-REQ-KVS-INLINE-STORAGE says "no heap allocation on the
+        hot path." Vendored rust_kvs uses std::collections::HashMap
+        for the in-memory store (kvs.rs) and Arc<Mutex<KvsData>> per
+        method (kvs.rs:38-44, etc.) — both allocate. There is no
+        allocator-tripwire in the build, and the surface test for
+        this comp-req is documented as a gap, not real verification.
       alternatives: >
-        Allow heap variant in ASIL-B (rejected: violates no-alloc),
-        ship both with cfg flag (rejected: doubles MC/DC scope).
+        (a) wire witness::no_alloc_guard around set_value/get_value
+        and have it panic on any allocator call — requires the
+        witness toolchain be present; (b) replace HashMap with a
+        bounded inline structure (heapless::IndexMap or a custom
+        slab) — requires an upstream fork; (c) downgrade COMP-REQ-
+        KVS-INLINE-STORAGE to draft and document that ASIL-B inline
+        storage is out of scope for this baseline.
       consequences: >
-        Capacity is fixed at component init; reconfigurations require
-        re-flashing. Acceptable for the target ECU.
+        Until (a), (b), or (c) lands, the comp-req's verified-by:
+        list is intentionally empty and the verify gate buckets the
+        artifact as MISSING — not falsely PASSED. The gap is
+        recorded; the audit trail does not lie.
     tags: [persistency, kvs, decision, memory]
     links:
       - type: satisfies