Supervisor integer only

.github/workflows/ci.yml

@@ -70,6 +70,17 @@ jobs:
           fi
           echo "clean"
 
+      - name: Release tool self-tests (SWR-UPD-11, SEC-05)
+        run: |
+          # The tools that sign things carry their own checks and need neither a
+          # board nor ESP-IDF. They are run here because the failure mode is
+          # quiet: a manifest whose signature does not verify, or a bootloader
+          # that overruns the partition table, is discovered on a device that
+          # cannot then be told otherwise.
+          python3 tools/update-manifest.py --self-test
+          python3 tools/secure-boot.py --self-test
+          python3 tools/sbom.py --self-test
+
       - name: SPDX header on every source file (SWR-NFR-18, UR-CON-04)
         run: |
           missing=0
@@ -79,7 +90,7 @@ jobs:
           done < <(git ls-files \
                      '*.cpp' '*.h' '*.md' '*.sdoc' 'CMakeLists.txt' '*/CMakeLists.txt' \
                      'firmware/controller/**/Kconfig*' 'firmware/controller/*.csv' 'firmware/controller/sdkconfig.*' \
-                     'tools/*.sh' '.github/workflows/*.yml' 'strictdoc.toml' \
+                     'tools/*.sh' 'tools/*.py' '.github/workflows/*.yml' 'strictdoc.toml' \
                    | grep -v '^LICENSE' \
                    | grep -vE '^fixture/(board|firmware)/')
             # fixture/board and fixture/firmware are generated verbatim by
@@ -209,7 +220,15 @@ jobs:
             # IDF_TOOLS_PATH is /opt/esp in this image; the script needs it to
             # find the xtensa picolibc headers, and fails loudly without them
             # rather than analysing nothing and calling it clean.
-            cd "$GITHUB_WORKSPACE"
+            #
+            # `cd ../..` rather than `cd "$GITHUB_WORKSPACE"`: that variable is
+            # not exported into this container, so `cd ""` quietly succeeded,
+            # left the shell in firmware/controller and the next line died with
+            # "tools/tidy-target.sh: No such file or directory" (exit 127). The
+            # action runs the command from `path:` above, so two levels up is
+            # the repository root and does not depend on an environment this
+            # container may not carry.
+            cd ../..
             tools/tidy-target.sh
 
   # SWR-TST-19.  The line floor is enforced; measured at 97.5 % on kiln_core when
@@ -448,6 +467,45 @@ jobs:
             build-docs/json
           if-no-files-found: error
 
+  # --- V-model level 5: the unit design, generated from the source -------
+  #
+  # The document is the gate and the gate is doxygen's warnings: an undocumented
+  # parameter or a reference to something that does not exist fails this job.
+  # The coverage number is printed because a clean doxygen run proves only that
+  # the comments which exist are well formed, and says nothing about the ones
+  # that do not (tools/udd-coverage.py has the argument).
+  udd:
+    name: Unit design document (supervisor)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install doxygen
+        run: sudo apt-get update -qq && sudo apt-get install -y -qq doxygen graphviz
+
+      - name: Generate, with documentation warnings as errors
+        run: tools/udd.sh | tee udd.log
+
+      - name: Summarise what the document covers
+        if: always()
+        run: |
+          {
+            echo '### Unit design document'
+            echo
+            echo 'V-model level 5, generated from the supervisor headers.'
+            echo '```'
+            sed -n '/Unit design coverage/,/Tasklist/p' udd.log || true
+            echo '```'
+          } >> "$GITHUB_STEP_SUMMARY"
+
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: unit-design-document
+          path: |
+            firmware/supervisor/build-udd/html/
+            firmware/supervisor/build-udd/doxygen-warnings.txt
+
   # --- architecture 14.6: the target build ------------------------------
   firmware:
     name: Firmware build (esp32s3)
@@ -473,6 +531,12 @@ jobs:
             idf.py build
             idf.py size > build/size.txt
             idf.py size-components > build/size-components.txt
+            # SWR-NFR-28, and it has to run HERE rather than in a step after
+            # this one: the component licences are scanned from the ESP-IDF tree
+            # on disk, and that tree exists only inside this container.
+            python3 ../../tools/sbom.py --build-dir build \
+                                        --image build/safekiln.bin \
+                                        --out-dir build/sbom --format both
 
       # Summarised from a normal step: $GITHUB_STEP_SUMMARY is a path on the
       # runner, and the step above runs in a container that mounts only the
@@ -486,6 +550,21 @@ jobs:
             echo '```'
             cat firmware/controller/build/size.txt
             echo '```'
+            echo
+            echo '### Bill of materials'
+            echo
+            echo 'SWR-NFR-28, CycloneDX and SPDX, generated from the build:'
+            echo '```'
+            # jq rather than a python heredoc: a heredoc body starts at column
+            # zero, which ends the YAML block scalar this step is written in and
+            # makes the whole workflow file invalid.  The same trap the release
+            # notes step documents, found the same way.
+            for f in firmware/controller/build/sbom/*.cdx.json; do
+              [ -e "$f" ] || continue
+              jq -r '"\(.metadata.component.name) \(.metadata.component.version): \(.components|length) components"' "$f"
+              jq -r '.components[] | select(has("licenses") | not) | "  licence unresolved: \(.name)"' "$f"
+            done
+            echo '```'
           } >> "$GITHUB_STEP_SUMMARY"
 
       - uses: actions/upload-artifact@v4
@@ -498,6 +577,7 @@ jobs:
             firmware/controller/build/bootloader/bootloader.bin
             firmware/controller/build/partition_table/partition-table.bin
             firmware/controller/build/flasher_args.json
+            firmware/controller/build/sbom/
             firmware/controller/build/size.txt
             firmware/controller/build/size-components.txt
           if-no-files-found: error
@@ -516,67 +596,24 @@ jobs:
     steps:
       - uses: actions/checkout@v4
 
+      # The command block below is run by the action as bash -c with the
+      # WHOLE block inside single quotes. One apostrophe anywhere in it, in a
+      # comment as readily as in a string, ends that quoting and bash exits 2
+      # on a parse error before any of it runs. That happened, and the symptom
+      # was a job failing with no output at all. So the block is four lines
+      # with no quoting hazard in them, and everything else lives in
+      # tools/qemu-smoke.sh where it can be read, reviewed and run locally.
       - name: Build and run under QEMU
         uses: espressif/esp-idf-ci-action@v1
         with:
           esp_idf_version: ${{ env.IDF_VERSION }}
           target: esp32s3
           path: firmware/controller
           command: |
-            export SDKCONFIG_DEFAULTS="sdkconfig.defaults;sdkconfig.qemu"
             python "$IDF_PATH/tools/idf_tools.py" install qemu-xtensa
             . "$IDF_PATH/export.sh"
-            idf.py build
-            # No monitor: it wants a tty.  Serial goes to stdout, and the
-            # firmware prints a telemetry line a second.
-            timeout --signal=KILL 180 idf.py qemu > qemu.log 2>&1 || true
-            tail -40 qemu.log
-
-      - name: Assert it booted and started firing
-        run: |
-          log=firmware/controller/qemu.log
-          test -s "$log" || { echo "::error::QEMU produced no output"; exit 1; }
-
-          fail=0
-          want() {
-            if grep -qE "$1" "$log"; then
-              echo "ok: $2"
-            else
-              echo "::error::$2 -- expected /$1/ in the QEMU log"
-              fail=1
-            fi
-          }
-
-          # The banner is "Safe Kiln Controller <ver> (<built>, IDF <ver>) on <target>".
-          # This assertion previously looked for 'Safe Kiln Controller starting', which
-          # the firmware has never printed -- so it could only ever have passed
-          # vacuously or failed.  Matched against what main.cpp actually logs.
-          want 'kiln: Safe Kiln Controller .* on esp32s3' 'the composition root ran'
-          want 'SIMULATED PLANT'                 'the simulated plant was bound'
-          want 'started "'                       'a program was accepted and started'
-          want '^\[RUN'                          'the run controller reached Running'
-          want 'HEAT'                            'the safety supervisor granted heat authority'
-
-          # The kiln has to actually get somewhere: a controller that boots and
-          # then sits at ambient would satisfy every check above.  The state is
-          # padded inside its brackets, so strip the whole bracketed field before
-          # reading the temperature rather than counting on where it lands.
-          if ! awk '/^\[/ { gsub(/\[[^]]*\]/, ""); if ($1+0 > 100) found = 1 }
-                    END { exit !found }' "$log"; then
-            echo "::error::the simulated kiln never passed 100 degC"
-            fail=1
-          fi
-
-          # And it has to get there without tripping a rule.  A spurious fault is
-          # the failure mode that matters most: a rule that stops a working kiln
-          # is worse than no rule, because it gets switched off.
-          if grep -qE '^\s+FAULT [0-9]+' "$log"; then
-            echo "::error::a fault latched during an unperturbed firing"
-            grep -E '^\s+FAULT [0-9]+' "$log" | head -5
-            fail=1
-          fi
-
-          exit $fail
+            cd ../..
+            tools/qemu-smoke.sh
 
       - uses: actions/upload-artifact@v4
         if: always()

.github/workflows/release.yml

@@ -25,6 +25,9 @@ permissions:
 
 env:
   IDF_VERSION: v6.0.1
+  # Pinned for the reason ci.yml pins it: StrictDoc validates the requirements
+  # and a new version can change what validates.
+  STRICTDOC_VERSION: 0.30.1
 
 jobs:
   release:
@@ -45,6 +48,11 @@ jobs:
           echo "tag=$tag" >> "$GITHUB_OUTPUT"
           prev="$(git describe --tags --abbrev=0 "${tag}^" 2>/dev/null || true)"
           echo "prev=$prev" >> "$GITHUB_OUTPUT"
+          # The tag's own commit date, as SOURCE_DATE_EPOCH for the SBOM: a
+          # release artefact kept for five years should be byte-identical when
+          # rebuilt from the same tag, and a wall-clock timestamp is the one
+          # thing that would stop it.
+          echo "epoch=$(git log -1 --format=%ct "$tag")" >> "$GITHUB_OUTPUT"
           echo "Building $tag (previous: ${prev:-none})"
 
       # The logic gate first.  A release whose safety rules are untested is not a
@@ -66,9 +74,42 @@ jobs:
             idf.py build
             # One image covering bootloader, partition table and app, so flashing
             # is a single command and cannot be done half way.
-            idf.py merge-bin -o build/safekiln-merged.bin
+            #
+            # -o is relative to the BUILD directory, not to the project, so the
+            # obvious "build/safekiln-merged.bin" asks for build/build/ and the
+            # file the next step copies is not there. Verified by running it.
+            idf.py merge-bin -o safekiln-merged.bin
             idf.py size > build/size.txt
             idf.py size-components > build/size-components.txt
+            # SWR-NFR-28. Inside the container, because the licences are scanned
+            # from the ESP-IDF tree, and --strict because a release is exactly
+            # the case where an unresolved licence or a missing digest must stop
+            # the build rather than ship as a gap nobody reads.
+            export SOURCE_DATE_EPOCH='${{ steps.version.outputs.epoch }}'
+            python3 ../../tools/sbom.py --build-dir build \
+                                        --image build/safekiln.bin \
+                                        --out-dir build/sbom --format both \
+                                        --strict
+
+      # The two documents ship WITH the binary, deliberately. A release is the
+      # moment somebody asks what this firmware is and what was verified about
+      # it, and an answer that lives only in a CI artifact expires in ninety
+      # days. Both are generated from the sources in this tag, so they describe
+      # the image beside them and not whatever main looked like later.
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+
+      - name: Build the requirements documents (StrictDoc)
+        run: |
+          pipx install "strictdoc==${STRICTDOC_VERSION}"
+          strictdoc export . --output-dir build-docs --formats=html,json
+
+      - name: Build the unit design document (Doxygen)
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y -qq doxygen graphviz
+          tools/udd.sh
 
       - name: Assemble the artifacts
         run: |
@@ -91,6 +132,19 @@ jobs:
           cp firmware/controller/build/size-components.txt     "dist/${base}-size-components.txt"
           # The resolved configuration, so the image can be reproduced.
           cp firmware/controller/sdkconfig                     "dist/${base}-sdkconfig"
+          # The bill of materials, in both formats (SWR-NFR-28). It is kept for
+          # the support period, which is why it is a release asset rather than a
+          # CI artifact that expires.
+          cp firmware/controller/build/sbom/*.cdx.json         "dist/${base}.cdx.json"
+          cp firmware/controller/build/sbom/*.spdx.json        "dist/${base}.spdx.json"
+
+          # The documents, zipped because a release asset is a file and both
+          # are trees of HTML. The JSON half of the StrictDoc export goes in
+          # too: it is the machine-readable form of the traceability, which is
+          # what a tool asking "is every SWR- realised" would read.
+          ( cd build-docs && zip -qr "../dist/safekiln-${tag}-requirements.zip" . )
+          ( cd firmware/supervisor/build-udd/html \
+              && zip -qr "../../../../dist/safekiln-${tag}-unit-design.zip" . )
 
           ( cd dist && sha256sum ./* > SHA256SUMS )
           ls -l dist
@@ -151,6 +205,40 @@ jobs:
             echo 'release of `SWA-05` — the central safety property of the design, which'
             echo 'needs real hardware to verify (`SWR-TST-17`, `SYS-SAF-02`).'
             echo
+            echo '## Documents'
+            echo
+            echo 'Both generated from the sources in this tag, so they describe'
+            echo 'the image beside them:'
+            echo
+            echo "- \`${base%-esp32s3-SIMULATED}-requirements.zip\` and the JSON"
+            echo '  beside it: the user, system, software, architecture, safety'
+            echo '  and security documents as StrictDoc renders them, with the'
+            echo '  traceability between them. `strictdoc export` fails on a'
+            echo '  reference to a requirement that does not exist, so this'
+            echo '  building at all is part of what the release asserts.'
+            echo "- \`${base%-esp32s3-SIMULATED}-unit-design.zip\`: V-model level 5"
+            echo '  for the independent safety supervisor, generated from its'
+            echo '  headers. 76 of 76 public functions and constants, each with'
+            echo '  the requirement it implements, its parameter ranges, its'
+            echo '  error behaviour, its design rationale and the test that'
+            echo '  covers it. Documentation warnings are errors, so a gap in it'
+            echo '  fails the build rather than appearing as a blank entry.'
+            echo
+            echo '## Bill of materials'
+            echo
+            echo 'Published with this release in both formats, generated from the'
+            echo 'build rather than maintained by hand (`SWR-NFR-28`): every'
+            echo 'ESP-IDF component actually linked, with the licence its own'
+            echo 'sources declare, and the image digest they belong to.'
+            echo
+            echo '```'
+            for f in dist/*.cdx.json; do
+              [ -e "$f" ] || continue
+              jq -r '"\(.metadata.component.name) \(.metadata.component.version)  \(.components|length) components"' "$f"
+              jq -r '"serial \(.serialNumber)"' "$f"
+            done
+            echo '```'
+            echo
             echo '## Changes'
             echo
             if [ -n "$prev" ]; then

.gitignore

@@ -47,6 +47,25 @@ dependencies.lock
 *_signing_key*
 secure_boot_digest.bin
 
+# Release artefacts from tools/update-manifest.py: a signed manifest and the
+# image it names belong on the update server, not in git. The public half of the
+# signing key is the exception and IS committed, as the generated header the
+# firmware compiles in (SWR-UPD-11); `*.pem` above keeps the private half out.
+dist/
+
+# The generated Unit Design Document (tools/udd.sh). It is generated from the
+# headers on demand and published as a CI artifact; a copy in git would be the
+# second description of the code that generating it exists to avoid.
+firmware/supervisor/build-udd/
+# The QEMU serial capture from tools/qemu-smoke.sh. A CI artifact and a local
+# scratch file; it got committed once because the run leaves it in the firmware
+# directory rather than in a build one.
+firmware/controller/qemu.log
+# And the LaTeX tree doxygen writes when GENERATE_LATEX is on or when it is run
+# with a configuration piped in from somewhere else, which is how a stray copy
+# of one got committed once.
+firmware/supervisor/latex/
+
 # Python bytecode from the tools/ scripts.
 __pycache__/
 *.pyc