[formal-spec] otel-observability-spec.md — Formal model & test suite — 2026-06-27

[github-actions]

Summary

specs/otel-observability-spec.md v0.4.0 defines the compatibility-first OpenTelemetry observability contract for gh-aw: OTLP endpoint normalization, header secrecy, Sentry rewriting, if-missing policy, service-name formation, domain extraction, local mirror invariants, and fan-out ordering. This formalization derives 15 predicates (TLA+, Z3/SMT-LIB, F*) and maps each to a Go testify unit test in pkg/workflow/.

Specification

• File: specs/otel-observability-spec.md
• Focus area: observability.otlp compiler + runtime contract, Levels 1 & 2 (§2.3)
• Formal notation used: TLA+ / Z3-SMT-LIB / F* (mixed, illustrative)

Formal Model

Predicates and invariants (illustrative notation)

P1  EndpointFormNormalization  [TLA+]
  ∀ e ∈ NormalizeEndpoint(ep): e.url ≠ ""  — §5.2 entries with empty URL discarded

P2  HeaderMapDeterminism  [Z3]
  serialize(m) = join(",", [k+"="+m[k] | k ← sortedKeys(m)])  — §5.3 ascending sort

P3  SentryAuthHeaderRewrite  [F*]
  isSentry(ep) ∧ toLower(name)="authorization" ==> result="x-sentry-auth"  — §5.4

P4  IfMissingPolicyValidation  [TLA+]
  NormalizeIfMissing(v) ∈ {"error","warn","ignore",""} ∧ invalid → ""  — §5.5

P5  ServiceNameFormation  [F*]
  otelServiceName(w): s = "gh-aw" ∨ hasPrefix(s,"gh-aw.")  — §6.1

P6  StaticDomainExtraction  [Z3]
  isExpression(ep) ∨ ep="" → ExtractDomain(ep)=""  — §5.7

P7  ExpressionNoAllowlistEntry  [TLA+]
  ∀ ep: isExpression(ep) → ExtractDomain(ep)=""  — §5.7

P8  TopLevelHeadersStringFormOnly  [TLA+]
  form ∈ {object,array} → topLevelHeaders ignored  — §5.3

P9  FanOutPreservesOrder  [TLA+]
  ∀ i: entries[i].url = declared[i]  — §16.3 declaration order preserved

P10 MirrorPathConstant  [Z3]
  localMirrorPath = "/tmp/gh-aw/otel.jsonl"  — §14.1 stable Level 2

P11 EmptyURLEntryDiscarded  [TLA+]
  ∀ e ∈ entries: e.url ≠ ""  — §5.2 empty URL → discarded

P12 NonSentryHeaderPreservation  [F*]
  ¬isSentry(ep) → normalize(h,ep)=h  — §5.4 no rewrite outside Sentry

P13 NilHeadersNormalize  [F*]
  normalize(nil,_)="" ∧ normalize("",_)="" ∧ normalize({},_)=""  — edge case

P14 InvalidIfMissingIsDefault  [Z3]
  v∉IfMissingPolicy → NormalizeIfMissing(v)=""  — §5.5 error default

P15 AbsentObservabilityNoRemoteExport  [TLA+]
  ¬HasKey(fm,"observability") → NormalizeEndpoint(fm)=<<>>  — §5.1

Behavioral Coverage Map

Predicate	Test Function	Description
P1 EndpointFormNormalization	TestFormal_EndpointFormNormalization	string/object/array → ordered list; empty/absent → empty
P2 HeaderMapDeterminism	TestFormal_HeaderMapDeterminism	Map headers sorted ascending, deterministic over 10 runs
P3 SentryAuthHeaderRewrite	TestFormal_SentryAuthHeaderRewrite	Authorization→x-sentry-auth on Sentry; preserved elsewhere
P4 IfMissingPolicyValidation	TestFormal_IfMissingPolicyValidation	error/warn/ignore accepted (case-insensitive); others → ""
P5 ServiceNameFormation	TestFormal_ServiceNameFormation	"gh-aw" or "gh-aw.<sanitized-id>"; WorkflowID > Name
P6 StaticDomainExtraction	TestFormal_StaticDomainExtraction	Static URLs → hostname; expressions/empty → ""
P7 ExpressionNoAllowlistEntry	TestFormal_ExpressionProducesNoAllowlistEntry	${{ ... }} → empty domain (no allowlist entry)
P8 TopLevelHeadersStringFormOnly	TestFormal_TopLevelHeadersApplyToStringFormOnly	Top-level headers only for string form; object/array immune
P9 FanOutPreservesOrder	TestFormal_FanOutPreservesDeclarationOrder	3-endpoint fan-out in declaration order
P10 MirrorPathConstant	TestFormal_MirrorPathConstant	/tmp/gh-aw/otel.jsonl stable Level 2 constant
P11 EmptyURLEntryDiscarded	TestFormal_EmptyURLEntriesDiscarded	Empty-URL entries discarded; valid entries kept
P12 NonSentryHeaderPreservation	TestFormal_StringHeaderFormPreservedForNonSentry	String headers unchanged for non-Sentry endpoints
P13 NilHeadersNormalize	TestFormal_NilAndEmptyHeadersYieldEmptyString	nil/""/{} → "" without panic
P14 InvalidIfMissingIsDefault	TestFormal_InvalidIfMissingFallsBackToDefault	fail/silent/skip/abort → "" (error default)
P15 AbsentObservabilityNoExport	TestFormal_AbsentObservabilityProducesNoEndpoints	nil/absent observability → no endpoints

Generated Test Suite

📄 `pkg/workflow/otel_observability_formal_test.go` (key tests — full file in repo)

(go/redacted):build !integration

// Formal test suite for specs/otel-observability-spec.md v0.4.0.
// Notation: TLA+/Z3/F* (illustrative). Predicates P1–P15 listed in file header.
// Run: go test ./pkg/workflow/... -run Formal

package workflow

import (
	"encoding/json"
	"strings"
	"testing"

	"github.com/github/gh-aw/pkg/constants"
	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// P4 — §5.5 if-missing policy accepts exactly error/warn/ignore; invalid → "".
func TestFormal_IfMissingPolicyValidation(t *testing.T) {
	cases := []struct{ in, want string }{
		{"error", "error"}, {"warn", "warn"}, {"ignore", "ignore"},
		{"Error", "error"}, {"WARN", "warn"}, {"  warn  ", "warn"},
		{"", ""}, {"fail", ""}, {"silent", ""}, {"skip", ""},
	}
	for _, c := range cases {
		t.Run("mode="+c.in, func(t *testing.T) {
			assert.Equal(t, c.want, normalizeOTLPIfMissingMode(c.in),
				"P4: if-missing %q must normalize to %q", c.in, c.want)
		})
	}
}

// P3 — §5.4 Authorization → x-sentry-auth on Sentry endpoints only.
func TestFormal_SentryAuthHeaderRewrite(t *testing.T) {
	tests := []struct {
		name, ep, wantContain, wantMissing string
		headers                            any
	}{
		{"sentry HTTPS rewrites", "https://ingest.sentry.io/123",
			map[string]any{"Authorization": "Sentry key=abc"},
			"x-sentry-auth=", "Authorization="},
		{"non-sentry preserves", "(traces.datadog.com/redacted)",
			map[string]any{"Authorization": "Bearer tok"},
			"Authorization=", "x-sentry-auth="},
		{"well-known sentry secret rewrites",
			"${{ secrets." + constants.OTELSentryEndpointSecretName + " }}",
			map[string]any{"Authorization": "Sentry key=xyz"},
			"x-sentry-auth=", "Authorization="},
	}
	for _, tt := range tests {
		t.Run(tt.name, func(t *testing.T) {
			r := normalizeOTLPHeadersForEndpoint(tt.headers, tt.ep)
			assert.Contains(t, r, tt.wantContain, "P3: %q", tt.ep)
			assert.NotContains(t, r, tt.wantMissing, "P3: %q", tt.ep)
		})
	}
}

// P10 — §14.1 stable Level 2 mirror path contract.
func TestFormal_MirrorPathConstant(t *testing.T) {
	assert.Equal(t, "/tmp/gh-aw/otel.jsonl",
		constants.TmpGhAwDir+"/"+constants.OtelJsonlFilename,
		"P10: mirror path must be /tmp/gh-aw/otel.jsonl per spec §14.1")
}

// P9 — §16.3 / §6.4 fan-out preserves declaration order.
func TestFormal_FanOutPreservesDeclarationOrder(t *testing.T) {
	declared := []string{"(primary.example.com/redacted)", "(secondary.example.com/redacted)", "(tertiary.example.com/redacted)"}
	eps := make([]any, len(declared))
	for i, u := range declared {
		eps[i] = map[string]any{"url": u}
	}
	entries := collectAllOTLPEndpoints(map[string]any{"observability": map[string]any{"otlp": map[string]any{"endpoint": eps}}})
	require.Len(t, entries, len(declared), "P9: all declared endpoints must be preserved")
	for i, e := range entries {
		assert.Equal(t, declared[i], e.URL, "P9: endpoint %d must match declaration order", i)
	}
}

// Encoding — §6.1 GH_AW_OTLP_ENDPOINTS must be valid compact JSON array.
func TestFormal_EndpointEncoding(t *testing.T) {
	assert.Empty(t, encodeOTLPEndpoints(nil), "empty endpoints → empty string")
	entries := []otlpEndpointEntry{{URL: "(p.example.com/redacted)", Headers: "K=V"}, {URL: "(b.example.com/redacted)"}}
	raw := encodeOTLPEndpoints(entries)
	var dec []map[string]any
	require.NoError(t, json.Unmarshal([]byte(raw), &dec))
	require.Len(t, dec, 2)
	assert.Equal(t, "(p.example.com/redacted)", dec[0]["url"])
	_, hasH := dec[1]["headers"]
	assert.False(t, hasH, "headers omitted when empty")
}

Usage

1. Full test file: pkg/workflow/otel_observability_formal_test.go (committed in this run).
2. Run: go test ./pkg/workflow/... -run Formal

Context

• Spec processed: specs/otel-observability-spec.md
• Formal notation: TLA+ / Z3-SMT-LIB / F*
• Levels covered: Level 1 & 2 (§2.3) — 15 predicates, 17 test functions
• Implementation map: §17.3 → pkg/workflow/observability_otlp.go
• Run: https://github.com/github/gh-aw/actions/runs/28294045363

Warning

Firewall blocked 1 domain

The following domain was blocked by the firewall during workflow execution:

• proxy.golang.org

To allow these domains, add them to the network.allowed list in your workflow frontmatter:

network:
  allowed:
    - defaults
    - "proxy.golang.org"

See Network Configuration for more information.

Generated by 🔬 Daily Formal Spec Verifier · 297.9 AIC · ⌖ 19.3 AIC · ⊞ 6.9K · ◷

• expires on Jul 4, 2026, 8:12 AM UTC-08:00