[formal-spec] forecast-compliance-fixtures/README.md — Formal model & test suite — 2026-07-29

[github-actions]

Caution

agentic threat detected
Threat detection flagged this output in warn mode. Manual review is REQUIRED before any follow-up automation.

Details

The threat detection engine failed to produce results.

Review the workflow run logs for details.

Summary

This spec documents the fixture files used to bootstrap Section 12 compliance tests for the Forecast Monte Carlo engine (pkg/cli/forecast_montecarlo_test.go, pkg/cli/forecast_test.go). The fixtures represent RunSummary JSON snapshots (run_summary_minimal.json, plus additional zero-ET, failed-run, and high-ET variants) that drive Bernoulli success-rate sampling and bootstrap Effective Token (ET) resampling in the Monte Carlo forecaster. This run formalizes the implicit schema and invariants of these fixtures and their consumers (RunSummary, WorkflowRun, TokenUsageSummary) as testable predicates, and derives a Go testify suite encoding them.

Specification

• File: specs/forecast-compliance-fixtures/README.md
• Focus area: Forecast Monte Carlo compliance fixtures (RunSummary schema, T-FC-022/031-040, T-ET-006)
• Formal notation used: Z3 / TLA+ / F* (mixed, illustrative)

Formal Model

Predicates and invariants (illustrative notation)

-- P1 (Z3, SMT-LIB): Bernoulli success predicate
-- Source: "conclusion: success — the run is counted as successful in Bernoulli sampling"
(assert (=> (= run.conclusion "success") (= bernoulli_success 1)))
(assert (=> (not (= run.conclusion "success")) (= bernoulli_success 0)))

-- P2 (Z3): ET non-negativity invariant
-- Source: "total_effective_tokens: 5400 — the ET observation used in bootstrap resampling"
(assert (>= token_usage_summary.total_effective_tokens 0))

-- P3 (Z3): Zero-ET fixture models missing artifact (T-FC-022)
-- Source: "run_summary_zero_et.json — Run with missing/zero ET (artifact not downloaded)"
(assert (=> zero_et_fixture (= token_usage_summary.total_effective_tokens 0)))

-- P4 (Z3): High-ET overflow boundary (T-ET-006)
-- Source: "run_summary_high_et.json — Run with very high ET (>= 1,000,000) for overflow checks"
(assert (=> high_et_fixture (>= token_usage_summary.total_effective_tokens 1000000)))

-- P5 (TLA+): Duration derivation from timestamps
-- Source: "run.updated_at and run.run_started_at — used to compute duration_seconds"
DurationSeconds == (UpdatedAt - RunStartedAt) \div Second
Invariant_DurationNonNegative == DurationSeconds >= 0

-- P6 (TLA+): Failed-run conclusion sampling (T-FC-035)
-- Source: "run_summary_failed.json — Run with conclusion: failure for Bernoulli sampling"
Invariant_FailedFixtureConclusion ==
    failedFixture => run.conclusion = "failure"

-- P7 (F*): RunSummary schema field presence contract
-- Source: "The run_summary_minimal.json fixture follows the RunSummary struct... Key fields used by the forecast command"
val validRunSummary : rs:RunSummary -> Tot bool
let validRunSummary rs =
  rs.run.conclusion <> "" &&
  rs.run_id >= 0L &&
  rs.token_usage_summary.total_effective_tokens >= 0

-- P8 (F*): Cache-hit determinism (fixture as cached run summary)
-- Source: "Use this fixture as the baseline for Monte Carlo engine compliance tests... by loading it as a cached run summary"
val cachedSummaryStable : rs:RunSummary -> Lemma
  (requires validRunSummary rs)
  (ensures  parseJSON (serializeJSON rs) == rs)

-- P9 (Z3): Timestamp ordering invariant
-- Source: implied by "duration_seconds" computation from created_at/run_started_at/updated_at
(assert (<= run.run_started_at run.updated_at))

-- P10 (TLA+): Monte Carlo input completeness invariant
-- Source: "Use this fixture as the baseline for Monte Carlo engine compliance tests (T-FC-031 through T-FC-040)"
Invariant_MonteCarloInputComplete ==
    /\ run.conclusion \in {"success", "failure"}
    /\ token_usage_summary.total_effective_tokens >= 0
    /\ run.run_started_at # NULL /\ run.updated_at # NULL

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1 Bernoulli success predicate	TestBernoulliSuccessFromConclusion	Verifies success conclusion maps to Bernoulli success=1, others to 0
P2 ET non-negativity	TestEffectiveTokensNonNegative	Verifies TotalEffectiveTokens in fixture is never negative
P3 Zero-ET fixture models missing artifact	TestZeroETFixtureIndicatesMissingArtifact	Validates run_summary_zero_et.json has ET == 0 (T-FC-022)
P4 High-ET overflow boundary	TestHighETFixtureExceedsOverflowThreshold	Validates run_summary_high_et.json has ET >= 1,000,000 (T-ET-006)
P5 Duration derivation non-negative	TestDurationSecondsNonNegative	Computes duration from RunStartedAt/UpdatedAt and checks it's >= 0
P6 Failed-run conclusion sampling	TestFailedFixtureHasFailureConclusion	Validates run_summary_failed.json has conclusion == "failure" (T-FC-035)
P7 RunSummary schema field presence	TestRunSummarySchemaFieldsPresent	Checks required fields (RunID, Conclusion, TotalEffectiveTokens) are populated in minimal fixture
P8 Cache-hit determinism	TestRunSummaryRoundTripSerialization	Marshals/unmarshals RunSummary and asserts equality (stub JSON round-trip)
P9 Timestamp ordering	TestRunStartedBeforeOrEqualUpdated	Asserts RunStartedAt <= UpdatedAt on minimal fixture
P10 Monte Carlo input completeness	TestMonteCarloInputFixtureCompleteness	Table-driven check across all four fixtures that required MC inputs are present and well-formed

Generated Test Suite

📄 `pkg/cli/forecast_fixtures_formal_test.go`

// forecast_fixtures_formal_test.go
//
// Formal predicate coverage derived from:
//   specs/forecast-compliance-fixtures/README.md
//
// Encodes the following formal predicates (see issue for full illustrative
// TLA+ / Z3 / F* notation):
//   P1  Bernoulli success predicate (conclusion -> success indicator)
//   P2  ET non-negativity invariant
//   P3  Zero-ET fixture models missing artifact (T-FC-022)
//   P4  High-ET overflow boundary (T-ET-006)
//   P5  Duration derivation from timestamps is non-negative
//   P6  Failed-run fixture conclusion sampling (T-FC-035)
//   P7  RunSummary schema field presence contract
//   P8  Cache-hit determinism (JSON round-trip stability)
//   P9  Timestamp ordering invariant (RunStartedAt <= UpdatedAt)
//   P10 Monte Carlo input completeness invariant across fixtures
package cli_test

import (
	"encoding/json"
	"os"
	"path/filepath"
	"testing"
	"time"

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

// minimalRunSummary is a stub — replace with real cli.RunSummary import if
// exported, or reuse the existing package-level struct from pkg/cli/logs_models.go.
// stub — replace with real implementation
type minimalWorkflowRun struct {
	Conclusion   string    `json:"conclusion"`
	CreatedAt    time.Time `json:"created_at"`
	UpdatedAt    time.Time `json:"updated_at"`
	RunStartedAt time.Time `json:"run_started_at"`
}

// stub — replace with real implementation
type minimalTokenUsageSummary struct {
	TotalEffectiveTokens int64 `json:"total_effective_tokens"`
}

// stub — replace with real implementation
type minimalRunSummary struct {
	CLIVersion       string                   `json:"cli_version"`
	RunID            int64                    `json:"run_id"`
	Run              minimalWorkflowRun       `json:"run"`
	TokenUsageSummary minimalTokenUsageSummary `json:"token_usage_summary"`
}

// loadFixtureRunSummary loads a fixture file from
// specs/forecast-compliance-fixtures/ into the minimal stub struct.
func loadFixtureRunSummary(t *testing.T, name string) minimalRunSummary {
	t.Helper()
	path := filepath.Join("..", "..", "specs", "forecast-compliance-fixtures", name)
	data, err := os.ReadFile(path)
	require.NoError(t, err, "fixture file %s should be readable", name)

	var rs minimalRunSummary
	require.NoError(t, json.Unmarshal(data, &rs), "fixture %s should be valid JSON matching RunSummary schema", name)
	return rs
}

// bernoulliSuccess implements P1: maps a conclusion string to a Bernoulli
// success indicator (1 for success, 0 otherwise).
func bernoulliSuccess(conclusion string) int {
	if conclusion == "success" {
		return 1
	}
	return 0
}

// TestBernoulliSuccessFromConclusion encodes P1.
func TestBernoulliSuccessFromConclusion(t *testing.T) {
	tests := []struct {
		name       string
		conclusion string
		want       int
	}{
		{"success maps to 1", "success", 1},
		{"failure maps to 0", "failure", 0},
		{"cancelled maps to 0", "cancelled", 0},
		{"empty conclusion maps to 0", "", 0},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			got := bernoulliSuccess(tt.conclusion)
			assert.Equal(t, tt.want, got, "bernoulliSuccess(%q) should equal %d per P1", tt.conclusion, tt.want)
		})
	}
}

// TestEffectiveTokensNonNegative encodes P2 using the minimal fixture.
func TestEffectiveTokensNonNegative(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_minimal.json")
	assert.GreaterOrEqual(t, rs.TokenUsageSummary.TotalEffectiveTokens, int64(0),
		"total_effective_tokens must never be negative per P2")
}

// TestZeroETFixtureIndicatesMissingArtifact encodes P3 (T-FC-022).
// Edge case: fixture representing a run whose token artifact was never downloaded.
func TestZeroETFixtureIndicatesMissingArtifact(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_zero_et.json")
	assert.Zero(t, rs.TokenUsageSummary.TotalEffectiveTokens,
		"run_summary_zero_et.json must have total_effective_tokens == 0 per P3/T-FC-022")
}

// TestHighETFixtureExceedsOverflowThreshold encodes P4 (T-ET-006).
// Edge case: extremely large ET value used to probe overflow handling.
func TestHighETFixtureExceedsOverflowThreshold(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_high_et.json")
	assert.GreaterOrEqual(t, rs.TokenUsageSummary.TotalEffectiveTokens, int64(1_000_000),
		"run_summary_high_et.json must have total_effective_tokens >= 1,000,000 per P4/T-ET-006")
}

// TestDurationSecondsNonNegative encodes P5.
func TestDurationSecondsNonNegative(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_minimal.json")
	duration := rs.Run.UpdatedAt.Sub(rs.Run.RunStartedAt)
	assert.GreaterOrEqual(t, duration.Seconds(), 0.0,
		"duration computed from run_started_at/updated_at must be non-negative per P5")
}

// TestFailedFixtureHasFailureConclusion encodes P6 (T-FC-035).
// Edge case: fixture representing a failed workflow run.
func TestFailedFixtureHasFailureConclusion(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_failed.json")
	assert.Equal(t, "failure", rs.Run.Conclusion,
		"run_summary_failed.json must have conclusion == \"failure\" per P6/T-FC-035")
}

// TestRunSummarySchemaFieldsPresent encodes P7.
func TestRunSummarySchemaFieldsPresent(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_minimal.json")
	require.NotEmpty(t, rs.Run.Conclusion, "run.conclusion must be present per P7 schema contract")
	require.NotZero(t, rs.RunID, "run_id must be present and non-zero per P7 schema contract")
	assert.GreaterOrEqual(t, rs.TokenUsageSummary.TotalEffectiveTokens, int64(0),
		"token_usage_summary.total_effective_tokens must be present per P7 schema contract")
}

// TestRunSummaryRoundTripSerialization encodes P8: JSON round-trip stability
// for a cached run summary.
func TestRunSummaryRoundTripSerialization(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_minimal.json")

	data, err := json.Marshal(rs)
	require.NoError(t, err, "marshaling RunSummary must not error per P8 cache determinism")

	var roundTripped minimalRunSummary
	require.NoError(t, json.Unmarshal(data, &roundTripped), "unmarshaling serialized RunSummary must not error per P8")

	assert.Equal(t, rs, roundTripped, "round-tripped RunSummary must equal original per P8 cache-hit determinism")
}

// TestRunStartedBeforeOrEqualUpdated encodes P9.
func TestRunStartedBeforeOrEqualUpdated(t *testing.T) {
	rs := loadFixtureRunSummary(t, "run_summary_minimal.json")
	assert.True(t, !rs.Run.RunStartedAt.After(rs.Run.UpdatedAt),
		"run_started_at must be <= updated_at per P9 timestamp ordering invariant")
}

// TestMonteCarloInputFixtureCompleteness encodes P10 across all known fixtures.
func TestMonteCarloInputFixtureCompleteness(t *testing.T) {
	fixtures := []string{
		"run_summary_minimal.json",
		"run_summary_zero_et.json",
		"run_summary_failed.json",
		"run_summary_high_et.json",
	}
	for _, name := range fixtures {
		t.Run(name, func(t *testing.T) {
			path := filepath.Join("..", "..", "specs", "forecast-compliance-fixtures", name)
			if _, err := os.Stat(path); os.IsNotExist(err) {
				t.Skipf("fixture %s not yet materialized on disk (only run_summary_minimal.json is committed today) — P10 requires it for full Monte Carlo compliance", name)
				return
			}
			rs := loadFixtureRunSummary(t, name)
			assert.Contains(t, []string{"success", "failure"}, rs.Run.Conclusion,
				"conclusion must be success or failure per P10 Monte Carlo input completeness")
			assert.GreaterOrEqual(t, rs.TokenUsageSummary.TotalEffectiveTokens, int64(0),
				"total_effective_tokens must be non-negative per P10")
			assert.False(t, rs.Run.RunStartedAt.IsZero(), "run_started_at must be set per P10")
			assert.False(t, rs.Run.UpdatedAt.IsZero(), "updated_at must be set per P10")
		})
	}
}

Usage

1. Copy the test file to pkg/cli/forecast_fixtures_formal_test.go.
2. Replace the minimalWorkflowRun / minimalTokenUsageSummary / minimalRunSummary stub structs with the real cli.WorkflowRun / cli.TokenUsageSummary / cli.RunSummary types from pkg/cli/logs_models.go (test currently lives in package cli_test, so unexported fields may need an internal test file in package cli instead).
3. Note: only run_summary_minimal.json is confirmed to exist on disk today; run_summary_zero_et.json, run_summary_failed.json, and run_summary_high_et.json are documented in the README's "Available Additional Fixtures" table but may not yet be materialized — TestMonteCarloInputFixtureCompleteness skips gracefully if a fixture file is missing, but TestZeroETFixtureIndicatesMissingArtifact, TestFailedFixtureHasFailureConclusion, and TestHighETFixtureExceedsOverflowThreshold will need those fixture files created first (per the README's "Adding New Fixtures" guidance).
4. Run: go test ./pkg/cli/... -run Formal

Context

• Spec processed: specs/forecast-compliance-fixtures/README.md
• Formal notation: TLA+ / Z3 / F* (mixed, illustrative)
• Run: https://github.com/github/gh-aw/actions/runs/30468452952

Generated by 🔬 Daily Formal Spec Verifier · aut00 · 30.8 AIC · ⊞ 9.9K · ◷

• expires on Aug 5, 2026, 8:03 AM UTC-08:00