Add complete system qualification evidence

tests/qualification/check-requirements.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT="$(cd "$(dirname "$0")/../.." && pwd)"
+MATRIX="$ROOT/tests/qualification/requirements.tsv"
+TLC_EVIDENCE="$ROOT/tests/qualification/tlc-evidence.tsv"
+ARCHITECTURE="$ROOT/docs/spec/architecture.md"
+
+expected="$(
+  {
+    rg -o 'FR-[0-9]+' "$ARCHITECTURE"
+    printf '%s\n' \
+      NFR-Reliability \
+      NFR-Observability \
+      NFR-Scalability \
+      NFR-Performance \
+      NFR-Security \
+      NFR-Deployment
+  } | sort -Vu
+)"
+actual="$(cut -f1 "$MATRIX" | sort -Vu)"
+if [[ "$actual" != "$expected" ]]; then
+  diff -u <(printf '%s\n' "$expected") <(printf '%s\n' "$actual")
+  exit 1
+fi
+
+while IFS=$'\t' read -r requirement path symbol; do
+  [[ -n "$requirement" && -n "$path" && -n "$symbol" ]]
+  [[ -f "$ROOT/$path" ]]
+  rg --fixed-strings --quiet "$symbol" "$ROOT/$path"
+done < "$MATRIX"
+
+model_commit="$(cut -f4 "$TLC_EVIDENCE" | sort -u)"
+test "$(printf '%s\n' "$model_commit" | wc -l)" = 1
+git -C "$ROOT" cat-file -e "$model_commit^{commit}"
+git -C "$ROOT" diff --quiet "$model_commit" -- docs/protocol
+
+configs="$(find "$ROOT/docs/protocol" -maxdepth 1 -name '*.cfg' -printf '%f\n' | sort)"
+evidence_configs="$(cut -f1 "$TLC_EVIDENCE" | sort)"
+test "$configs" = "$evidence_configs"
+
+tla_sha256="$(sha256sum "$ROOT/docs/protocol/Remora.tla" | cut -d ' ' -f1)"
+while IFS=$'\t' read -r config config_sha256 evidence_tla_sha256 commit spec generated distinct depth completion; do
+  test "$(sha256sum "$ROOT/docs/protocol/$config" | cut -d ' ' -f1)" = "$config_sha256"
+  test "$evidence_tla_sha256" = "$tla_sha256"
+  test "$commit" = "$model_commit"
+  test "$(awk '/^SPECIFICATION / { print $2 }' "$ROOT/docs/protocol/$config")" = "$spec"
+  [[ "$generated" =~ ^[1-9][0-9]*$ ]]
+  [[ "$distinct" =~ ^[1-9][0-9]*$ ]]
+  [[ "$depth" =~ ^[1-9][0-9]*$ ]]
+  test "$completion" = "Model checking completed. No error has been found."
+done < "$TLC_EVIDENCE"
+
+printf 'requirement trace and complete TLC evidence binding passed\n'