diff --git a/.github/workflows/rivet-v-closure.yml b/.github/workflows/rivet-v-closure.yml new file mode 100644 index 00000000..28ee007b --- /dev/null +++ b/.github/workflows/rivet-v-closure.yml @@ -0,0 +1,43 @@ +# Traceability-completeness gate (v0.6.0 / D3). +# +# The release-completeness gate asks "does every approved/implemented artifact have its +# V closed?" — a question that is only answerable if requirement statuses track their +# verification artifacts. They drifted: 16 requirements carried a `verified` VER-* while +# still reading `implemented`/`proposed` themselves (the verified driver suite, gpio, +# timer, the syscall seam, I-ISO, tri-track). The gate misreported them as not-done — it +# erred safe, but it lied, and nothing stopped it recurring. This gate is that stop. +name: rivet V-closure + +on: + push: + branches: [main] + paths: + - "artifacts/**" + - "tools/check-v-closure.py" + - ".github/workflows/rivet-v-closure.yml" + pull_request: + branches: [main] + paths: + - "artifacts/**" + - "tools/check-v-closure.py" + - ".github/workflows/rivet-v-closure.yml" + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.head_ref || github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +jobs: + v-closure: + name: "no requirement lags its closed V" + runs-on: ubuntu-22.04 + timeout-minutes: 10 + steps: + - uses: actions/checkout@v7 + - uses: actions/setup-python@v6 + with: + python-version: "3.12" + - name: Traceability-completeness gate + run: python3 tools/check-v-closure.py diff --git a/artifacts/gust_dma_model.yaml b/artifacts/gust_dma_model.yaml index c96787d8..1f63cb1c 100644 --- a/artifacts/gust_dma_model.yaml +++ b/artifacts/gust_dma_model.yaml @@ -99,7 +99,7 @@ artifacts: - id: REQ-DMA-ASYNC-001 type: sw-req title: "DMA completion is a kiln waitable; no host Future crosses the wasm boundary" - status: proposed + status: verified release: v0.2.1 description: > A transfer SHALL resolve via the existing split-phase pattern: the completion diff --git a/artifacts/gust_os_executor.yaml b/artifacts/gust_os_executor.yaml index c808a580..85708644 100644 --- a/artifacts/gust_os_executor.yaml +++ b/artifacts/gust_os_executor.yaml @@ -11,7 +11,7 @@ artifacts: - id: REQ-OS-EXEC-001 type: sw-req title: "gust:os cooperative async executor (v1, static single-partition)" - status: implemented + status: verified release: v0.4.0 description: > The gust:os inner async layer SHALL schedule a static set of up to diff --git a/artifacts/gust_os_roadmap.yaml b/artifacts/gust_os_roadmap.yaml index 2cda7ea1..1b426a7e 100644 --- a/artifacts/gust_os_roadmap.yaml +++ b/artifacts/gust_os_roadmap.yaml @@ -29,7 +29,7 @@ artifacts: - id: REQ-DRV-GPIO-001 type: sw-req title: "GPIO is a verified thin-seam driver — pin logic in wasm, TCB = mmio only" - status: proposed + status: verified release: v0.3.0 description: > Digital I/O (pin mode, read, write, toggle, and the port-bank bit math) SHALL @@ -50,7 +50,7 @@ artifacts: - id: REQ-DRV-TIMER-001 type: sw-req title: "Hardware timer is a verified thin-seam driver; the tick source becomes a capability" - status: proposed + status: verified release: v0.3.0 description: > A general-purpose hardware timer (compare/period/prescaler programming and the @@ -70,7 +70,7 @@ artifacts: - id: REQ-DRV-SPI-001 type: sw-req title: "SPI is a verified thin-seam driver, DMA-capable via the own handoff" - status: implemented + status: verified release: v0.3.0 description: > SPI master (mode/clock config, the transfer state machine, and CS framing) @@ -96,7 +96,7 @@ artifacts: - id: REQ-DRV-BREADTH-001 type: sw-req title: "The seam generalizes: a multi-driver node composes within the SRAM/TCB budget" - status: implemented + status: verified release: v0.3.0 description: > A single per-node image composing GPIO + timer + SPI + UART drivers SHALL fit @@ -117,7 +117,7 @@ artifacts: - id: REQ-DRV-WDG-001 type: sw-req title: "IWDG watchdog is a verified thin-seam driver — the software cannot-un-start hardware backstop" - status: implemented + status: verified release: v0.3.0 description: > The STM32F1 independent watchdog (IWDG) key-sequence lifecycle — 0x5555 unlock, @@ -339,7 +339,7 @@ artifacts: - id: REQ-OS-SYSCALL-001 type: sw-req title: "gust:os — a typed capability world is the OS ABI (not ad-hoc imports)" - status: implemented + status: verified release: v0.4.0 description: > The OS surface an app sees SHALL be a single WIT world `gust:os` exposing @@ -490,7 +490,7 @@ artifacts: - id: REQ-DRV-ADC-001 type: sw-req title: "ADC is a verified thin-seam driver — read-after-EOC exactly-once analog input" - status: implemented + status: verified release: v0.3.0 description: > The STM32F1 ADC single-conversion path — the SMPR sample-time and SQR @@ -561,7 +561,7 @@ artifacts: - id: REQ-DRV-DAC-001 type: sw-req title: "DAC is a verified thin-seam driver — glitch-free, trigger-gated analog output" - status: implemented + status: verified release: v0.3.0 description: > The STM32F1 software-triggered DAC path — CR channel/trigger configuration @@ -630,7 +630,7 @@ artifacts: - id: REQ-DRV-PWM-001 type: sw-req title: "PWM actuator output is a verified thin-seam driver — duty can never exceed the period, and the failsafe is total and latching" - status: implemented + status: verified release: v0.3.0 description: > The STM32 advanced-timer PWM output path — CCMR1 PWM-mode-1 + output-preload @@ -700,7 +700,7 @@ artifacts: - id: REQ-DRV-I2C-001 type: sw-req title: "I2C is a verified thin-seam master driver — ACK-all-but-last cannot hang the bus" - status: implemented + status: verified release: v0.3.0 description: > The STM32F1 I2C master path — CR2 FREQ + CCR divisor + TRISE timing configuration @@ -770,7 +770,7 @@ artifacts: - id: REQ-DRV-CAN-001 type: sw-req title: "CAN (bxCAN) is a verified thin-seam driver — config-only-in-init, no stale bit rate on the bus" - status: implemented + status: verified release: v0.3.0 description: > The STM32F1 bxCAN master path — the INRQ→INAK init handshake, the BTR @@ -843,7 +843,7 @@ artifacts: - id: REQ-DRV-DMA-001 type: sw-req title: "DMA-as-own ownership driver is CLOSED — demonstrated on-target + register-effect content-gated" - status: implemented + status: verified release: v0.3.0 description: > The dma-own driver (REQ-DMA-OWN-001: a DMA transfer modeled as a Component-Model diff --git a/artifacts/gust_safety_release_line.yaml b/artifacts/gust_safety_release_line.yaml index 54a10d7b..1e7504af 100644 --- a/artifacts/gust_safety_release_line.yaml +++ b/artifacts/gust_safety_release_line.yaml @@ -125,7 +125,7 @@ artifacts: - id: REQ-OS-ISO-001 type: sw-req title: "I-ISO: the hardware memory-protection boundary is the SOLE isolation root of trust (the keystone)" - status: implemented + status: verified release: v0.5.0 description: > This is the release-line KEYSTONE (invariant I-ISO): the target's @@ -622,7 +622,7 @@ artifacts: - id: REQ-OS-TRITRACK-001 type: sw-req title: "T1: at least one load-bearing theorem discharged on all three tracks — Verus + Rocq + Kani" - status: implemented + status: verified release: v0.8.0 description: > Cross-cutting track T1. gust's tri-track claim ("Verus + Rocq + diff --git a/tools/check-v-closure.py b/tools/check-v-closure.py new file mode 100755 index 00000000..a9601534 --- /dev/null +++ b/tools/check-v-closure.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Traceability-completeness gate: a requirement whose V is closed must say so. + +v0.6.0 / D3. The release-completeness gate asks "does every approved/implemented +artifact have its V closed?". That question is only answerable if requirement statuses +track their verification artifacts. They drifted: 12 requirements carried a `verified` +`VER-*` while still reading `implemented`/`proposed` themselves — the whole verified +driver suite, gpio, timer, and the syscall seam. The gate misreported them as not-done. +It erred safe, but it lied, and nothing stopped it recurring. + +This check fails when a requirement's matching verification artifact is `verified` but +the requirement itself is not. Pairing is by id: `REQ-FOO-001` <-> `VER-FOO-001`. + + python3 tools/check-v-closure.py # gate (exit 1 on drift) + python3 tools/check-v-closure.py --list # show every REQ/VER pair + status +""" +import glob +import re +import sys + +REQ_RE = re.compile(r"- id: ([A-Z][A-Z0-9-]+)\n(?:.*\n)*?\s+status: (\w+)") + + +def load_statuses(root="artifacts"): + """id -> status, across every artifact file.""" + status = {} + for path in sorted(glob.glob(f"{root}/*.yaml")): + text = open(path).read() + for match in REQ_RE.finditer(text): + status[match.group(1)] = match.group(2) + return status + + +def pairs(status): + """(req_id, ver_id, req_status, ver_status) for every REQ-* with a matching VER-*.""" + out = [] + for req_id, req_status in sorted(status.items()): + if not req_id.startswith("REQ-"): + continue + ver_id = "VER-" + req_id[len("REQ-"):] + if ver_id in status: + out.append((req_id, ver_id, req_status, status[ver_id])) + return out + + +def main(): + status = load_statuses() + listed = pairs(status) + + if "--list" in sys.argv: + for req_id, ver_id, req_status, ver_status in listed: + print(f"{req_status:12} {req_id:26} <- {ver_status:12} {ver_id}") + return 0 + + # The drift: V closed, requirement not. + drift = [p for p in listed if p[3] == "verified" and p[2] != "verified"] + if drift: + print("Traceability drift — requirement status lags its closed V:\n") + for req_id, ver_id, req_status, _ in drift: + print(f" {req_id:26} is '{req_status}' but {ver_id} is 'verified'") + print( + f"\n{len(drift)} requirement(s) whose V is closed still read as not-done, so the\n" + "release-completeness gate misreports them. Promote each to 'verified' (or, if the\n" + "V should not have been closed, fix the VER artifact instead)." + ) + return 1 + + print(f"V-closure traceability: OK — {len(listed)} REQ/VER pairs, no requirement lags its closed V.") + return 0 + + +if __name__ == "__main__": + sys.exit(main())