[formal-spec] compiler-threat-detection-compliance/README.md — Formal model & test suite — 2026-10-15 #69062

(go/redacted):build !integration

// Formal tests for specs/compiler-threat-detection-compliance/README.md
// Encodes: CrosswalkFunctional, CrosswalkInjective, IDFormat, RuleNormDisjoint,
// NormRangeReserved, IdentityPrefix, ShiftedRange, MonotoneCrosswalk,
// UnusedRuleSlot, NoGapInAllocation.

package workflow

import (
	"os"
	"path/filepath"
	"regexp"
	"runtime"
	"sort"
	"strconv"
	"strings"
	"testing"

	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

var (
	crosswalkRowRe = regexp.MustCompile(`^\| (CTR-\d{3}) \| (T-CTR-\d{3}) \|$`)
	normRowRe      = regexp.MustCompile(`^\| (T-CTR-\d{3}) \| .+ \|$`)
	ruleRe         = regexp.MustCompile(`^CTR-\d{3}$`)
	testRe         = regexp.MustCompile(`^T-CTR-\d{3}$`)
)

type crosswalkRow struct{ rule, test string }

func crosswalkNum(t *testing.T, id string) int {
	t.Helper()
	n, err := strconv.Atoi(id[strings.LastIndex(id, "-")+1:])
	require.NoError(t, err, "ID %q should end in a number", id)
	return n
}

func loadCrosswalk(t *testing.T) ([]crosswalkRow, []string) {
	t.Helper()
	_, thisFile, _, ok := runtime.Caller(0)
	require.True(t, ok, "runtime.Caller should succeed")
	data, err := os.ReadFile(filepath.Join(filepath.Dir(thisFile), "..", "..", "specs", "compiler-threat-detection-compliance", "README.md"))
	require.NoError(t, err, "compliance README should be readable")

	var rows []crosswalkRow
	var norms []string
	for _, line := range strings.Split(string(data), "\n") {
		line = strings.TrimSpace(line)
		if m := crosswalkRowRe.FindStringSubmatch(line); m != nil {
			rows = append(rows, crosswalkRow{m[1], m[2]})
		} else if m := normRowRe.FindStringSubmatch(line); m != nil {
			norms = append(norms, m[1])
		}
	}
	require.NotEmpty(t, rows, "crosswalk table should have rows")
	require.NotEmpty(t, norms, "norm tables should have rows")
	return rows, norms
}

func TestFormal_CrosswalkEachRuleHasOneTestID(t *testing.T) {
	rows, _ := loadCrosswalk(t)
	seen := map[string]int{}
	for _, r := range rows {
		seen[r.rule]++
	}
	for rule, n := range seen {
		assert.Equal(t, 1, n, "rule %s should appear exactly once in the crosswalk", rule)
	}
}

func TestFormal_CrosswalkTestIDsUnique(t *testing.T) {
	rows, _ := loadCrosswalk(t)
	seen := map[string]string{}
	for _, r := range rows {
		prev, dup := seen[r.test]
		assert.False(t, dup, "test ID %s is used by both %s and %s", r.test, prev, r.rule)
		seen[r.test] = r.rule
	}
}

func TestFormal_CrosswalkIDFormat(t *testing.T) {
	rows, norms := loadCrosswalk(t)
	for _, r := range rows {
		assert.Regexp(t, ruleRe, r.rule, "rule ID %q should be well formed", r.rule)
		assert.Regexp(t, testRe, r.test, "test ID %q should be well formed", r.test)
	}
	for _, n := range norms {
		assert.Regexp(t, testRe, n, "norm test ID %q should be well formed", n)
	}
}

func TestFormal_RuleTestsDisjointFromNormTests(t *testing.T) {
	rows, norms := loadCrosswalk(t)
	normSet := map[string]bool{}
	for _, n := range norms {
		normSet[n] = true
	}
	for _, r := range rows {
		assert.False(t, normSet[r.test], "rule test %s must not reuse a Section 6 norm test ID", r.test)
	}
}

func TestFormal_NormTestIDRange(t *testing.T) {
	_, norms := loadCrosswalk(t)
	expected := map[int]bool{40: true}
	for i := 24; i <= 38; i++ {
		expected[i] = true
	}
	got := map[int]int{}
	for _, n := range norms {
		got[crosswalkNum(t, n)]++
	}
	for num, count := range got {
		assert.True(t, expected[num], "T-CTR-%03d is not an allowed norm test ID", num)
		assert.Equal(t, 1, count, "T-CTR-%03d should appear once in norm tables", num)
	}
	for num := range expected {
		assert.Contains(t, got, num, "norm test T-CTR-%03d should be listed", num)
	}
}

func TestFormal_CrosswalkKnownMappings(t *testing.T) {
	rows, _ := loadCrosswalk(t)
	m := map[string]string{}
	for _, r := range rows {
		m[r.rule] = r.test
	}
	for i := 1; i <= 23; i++ {
		assert.Equal(t, "T-CTR-"+leftPad3(i), m["CTR-"+leftPad3(i)], "CTR-%03d should map to the identity test ID", i)
	}
	assert.Equal(t, "T-CTR-039", m["CTR-025"], "CTR-025 should map to T-CTR-039")
	for i := 26; i <= 33; i++ {
		assert.Equal(t, "T-CTR-"+leftPad3(i+15), m["CTR-"+leftPad3(i)], "CTR-%03d should map to T-CTR-%03d", i, i+15)
	}
}

func leftPad3(n int) string {
	s := strconv.Itoa(n)
	for len(s) < 3 {
		s = "0" + s
	}
	return s
}

func TestFormal_CrosswalkMonotone(t *testing.T) {
	rows, _ := loadCrosswalk(t)
	sorted := append([]crosswalkRow(nil), rows...)
	sort.Slice(sorted, func(i, j int) bool { return crosswalkNum(t, sorted[i].rule) < crosswalkNum(t, sorted[j].rule) })
	for i := 1; i < len(sorted); i++ {
		assert.Less(t, crosswalkNum(t, sorted[i-1].test), crosswalkNum(t, sorted[i].test),
			"test IDs should increase with rule IDs (%s -> %s)", sorted[i-1].rule, sorted[i].rule)
	}
}

func TestFormal_CTR024AbsentFromCrosswalk(t *testing.T) {
	rows, norms := loadCrosswalk(t)
	for _, r := range rows {
		assert.NotEqual(t, "CTR-024", r.rule, "CTR-024 has no active rule row")
	}
	assert.Contains(t, norms, "T-CTR-024", "T-CTR-024 slot should be held by a norm test")
}

func TestFormal_SharedIDSpaceGapFree(t *testing.T) {
	rows, norms := loadCrosswalk(t)
	used := map[int]bool{}
	max := 0
	for _, r := range rows {
		n := crosswalkNum(t, r.test)
		used[n] = true
		if n > max {
			max = n
		}
	}
	for _, n := range norms {
		num := crosswalkNum(t, n)
		used[num] = true
		if num > max {
			max = num
		}
	}
	for i := 1; i <= max; i++ {
		assert.True(t, used[i], "T-CTR-%03d should be allocated (shared sequence must be gap-free)", i)
	}
}