#!/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'