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

### Summary

This formalizes the `specs/otel-observability-spec.md` (v0.4.0) OpenTelemetry Observability Specification for `gh-aw`. The spec defines the `observability.otlp` configuration surface, endpoint/header normalization, direct/collector export modes, W3C trace-context propagation, resource identity, span/metric/log contracts, and security/cardinality controls. This run extends the existing formalization (`otel_observability_formal_test.go`, 15 predicates) with 6 additional predicates (P16–P21) covering resource-attribute secret-reference rejection, attribute/resource-attribute independence, merge precedence semantics, and two forward-looking stub predicates for metric cardinality bounds and instrumentation scope naming that have no concrete implementation yet.

### Specification

- **File**: `specs/otel-observability-spec.md`
- **Focus area**: OTLP configuration validation, attribute/resource-attribute handling, metric cardinality, instrumentation scope naming
- **Formal notation used**: TLA+ / Z3-style guard conjunction / F* pre-post contracts

### Formal Model

<details>
<summary><b>Predicates and invariants (illustrative notation)</b></summary>

**P16 — SecretRefResourceAttributeRejected** (§5.3, §8)
> Source: "Headers MUST be classified as secrets..." / "observability.otlp.resource-attributes.%s must not reference secrets.* or vars.*"

```
∀ (key, value) ∈ resource_attributes(workflow):
    SecretRefPattern.matches(value) ⟹ ValidateResourceAttributes(workflow) = Err(msg)
```
F*-style contract:
```fstar
val validateOTLPResourceAttributes: workflow:WorkflowData -> Pure (result unit)
  (requires True)
  (ensures fun r -> (exists k v. resourceAttrs workflow k v /\ isSecretRef v) ==> isErr r)
```

**P17 — CustomAttributesResourceAttributesIndependent** (§8.1)
> Source: "Stable resource attributes include..." vs custom span `attributes`; the two fields are parsed from disjoint frontmatter keys (`attributes` vs `resource-attributes`).

```
collectOTLPCustomAttributes(fm) ∩ collectOTLPResourceAttributes(fm) semantics ⟹
    ∀ fm: customAttrs(fm) = extract(fm, "attributes") ∧
          resourceAttrs(fm) = extract(fm, "resource-attributes") ∧
          customAttrs(fm) ≠ resourceAttrs(fm) when contents differ
```

**P18 — MergePrecedenceBaseWinsOverOverride** (§5.3, layered config semantics)
> Source: "Top-level `headers` MUST apply only to the string endpoint form. Object and array forms MUST use per-entry headers." — generalized as a base/override precedence invariant used by `mergeOTLPStringMaps`.

```
∀ k ∈ dom(base) ∩ dom(override): merge(base, override)[k] = base[k]
∀ k ∈ dom(base) \ dom(override): merge(base, override)[k] = base[k]
∀ k ∈ dom(override) \ dom(base): merge(base, override)[k] = override[k]
```

**P19 — MergeOfEmptyMapsYieldsNil** (defensive allocation invariant)
```
base = ∅ ∧ override = ∅ ⟹ merge(base, override) = nil
```

**P20 — MetricResourceCardinalityBound** (§8.3) — *stub, no concrete implementation yet*
> Source: "Workflow run IDs, job run IDs, trace IDs, span IDs, commit SHAs, pull-request or issue numbers, actor IDs, item URLs, and conversation IDs MUST NOT be metric resource attributes or metric dimensions by default."

```
∀ d ∈ HighCardinalityDimensions: IsAllowedByDefault(d) = false
∀ d ∈ BoundedCardinalityDimensions: IsAllowedByDefault(d) = true
HighCardinalityDimensions = {run.id, job.run.id, trace.id, span.id, commit.sha,
                              pull_request.id, issue.id, actor.id, item.url, conversation.id}
```

**P21 — InstrumentationScopeNaming** (§8.4) — *stub, no concrete implementation yet*
> Source: "Telemetry emitted by the core runtime MUST use instrumentation scope name `gh-aw`... Gateway telemetry SHOULD use a gateway-specific scope such as `gh-aw-mcpg`."

```
CoreScope = "gh-aw"
GatewayScope = "gh-aw-mcpg"
CoreScope ≠ GatewayScope
```

</details>

### Behavioral Coverage Map

| Predicate / Invariant | Test Function | Description |
|---|---|---|
| `SecretRefResourceAttributeRejected` (P16) | `TestFormal_SecretRefResourceAttributeRejected` | Rejects `resource-attributes` values referencing `secrets.*`/`vars.*`; accepts literals and nil workflow data |
| `CustomAttributesResourceAttributesIndependent` (P17) | `TestFormal_CustomAttributesResourceAttributesIndependent` | Confirms `attributes` and `resource-attributes` are parsed and stored independently |
| `MergePrecedenceBaseWinsOverOverride` (P18) | `TestFormal_MergePrecedenceBaseWinsOverOverride` | Verifies base-map values win on key collision; disjoint keys are unioned |
| `MergeOfEmptyMapsYieldsNil` (P19) | `TestFormal_MergeOfEmptyMapsYieldsNil` | Confirms merging nil/empty maps yields nil, not an empty allocated map |
| `MetricResourceCardinalityBound` (P20) | `TestFormal_MetricResourceCardinalityBound` | Ensures high-cardinality identifiers are excluded from default metric dimensions; bounded ones are allowed (stub interface) |
| `InstrumentationScopeNaming` (P21) | `TestFormal_InstrumentationScopeNaming` | Confirms core scope is `gh-aw`, gateway scope is `gh-aw-mcpg`, and the two remain distinct (stub interface) |

### Generated Test Suite

<details>
<summary><b>📄 <code>pkg/workflow/otel_observability_formal_v2_test.go</code></b></summary>

```go
package workflow

// This file formalizes additional predicates from
// specs/otel-observability-spec.md (v0.4.0) that are not yet covered by
// otel_observability_formal_test.go. It complements that file rather than
// duplicating its predicates.
//
// Formal predicates encoded here (see issue body for full TLA+/Z3/F* notation):
//   P16 SecretRefResourceAttributeRejected  (§5.3 / §8: resource-attributes MUST NOT reference secrets/vars)
//   P17 CustomAttributesResourceAttributesIndependent (§8.1: attributes and resource-attributes are distinct maps)
//   P18 MergePrecedenceBaseWinsOverOverride (§5.3-adjacent merge semantics used for header/attribute layering)
//   P19 MergeOfEmptyMapsYieldsNil (defensive merge invariant: no spurious allocation)
//   P20 MetricResourceCardinalityBound (§8.3: run/job/trace/span/commit/actor/item IDs MUST NOT be metric dimensions by default) — stub, no concrete implementation exists yet
//   P21 InstrumentationScopeNaming (§8.4: core scope MUST be "gh-aw"; gateway scope SHOULD be "gh-aw-mcpg") — stub, no concrete implementation exists yet

import (
	"testing"

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

// TestFormal_SecretRefResourceAttributeRejected encodes P16: §8/§5 requires that
// observability.otlp.resource-attributes values MUST NOT reference secrets.* or
// vars.* because resource attributes are exported to tracing backends and are
// not treated as secret values.
func TestFormal_SecretRefResourceAttributeRejected(t *testing.T) {
	tests := []struct {
		name      string
		workflow  *WorkflowData
		expectErr bool
	}{
		{
			name: "secrets reference is rejected",
			workflow: &WorkflowData{
				RawFrontmatter: map[string]any{
					"observability": map[string]any{
						"otlp": map[string]any{
							"resource-attributes": map[string]any{
								"team": "${{ secrets.TEAM_NAME }}",
							},
						},
					},
				},
			},
			expectErr: true,
		},
		{
			name: "vars reference is rejected",
			workflow: &WorkflowData{
				RawFrontmatter: map[string]any{
					"observability": map[string]any{
						"otlp": map[string]any{
							"resource-attributes": map[string]any{
								"env": "${{ vars.DEPLOY_ENV }}",
							},
						},
					},
				},
			},
			expectErr: true,
		},
		{
			name: "plain literal value is accepted",
			workflow: &WorkflowData{
				RawFrontmatter: map[string]any{
					"observability": map[string]any{
						"otlp": map[string]any{
							"resource-attributes": map[string]any{
								"team": "platform-eng",
							},
						},
					},
				},
			},
			expectErr: false,
		},
		{
			name:      "nil workflow data produces no error",
			workflow:  nil,
			expectErr: false,
		},
	}

	for _, tc := range tests {
		t.Run(tc.name, func(t *testing.T) {
			err := validateOTLPResourceAttributes(tc.workflow)
			if tc.expectErr {
				require.Error(t, err, "resource-attributes referencing secrets/vars MUST be rejected per §8/§5.3")
				assert.Contains(t, err.Error(), "must not reference secrets.* or vars.*",
					"error message must explain why the value is disallowed")
			} else {
				assert.NoError(t, err, "literal resource-attribute values or nil workflow data MUST NOT produce an error")
			}
		})
	}
}

// TestFormal_CustomAttributesResourceAttributesIndependent encodes P17: §8.1
// requires that `observability.otlp.attributes` (span/custom attributes) and
// `observability.otlp.resource-attributes` (resource identity) are collected
// independently and MUST NOT be conflated.
func TestFormal_CustomAttributesResourceAttributesIndependent(t *testing.T) {
	frontmatter := map[string]any{
		"observability": map[string]any{
			"otlp": map[string]any{
				"attributes": map[string]any{
					"session.id": "abc123",
				},
				"resource-attributes": map[string]any{
					"deployment.environment.name": "prod",
				},
			},
		},
	}

	customAttrs := collectOTLPCustomAttributes(frontmatter)
	resourceAttrs := collectOTLPResourceAttributes(frontmatter)

	require.NotNil(t, customAttrs, "custom attributes map must be collected when present")
	require.NotNil(t, resourceAttrs, "resource attributes map must be collected when present")
	assert.Equal(t, map[string]string{"session.id": "abc123"}, customAttrs,
		"custom attributes MUST only contain the `attributes` field contents")
	assert.Equal(t, map[string]string{"deployment.environment.name": "prod"}, resourceAttrs,
		"resource attributes MUST only contain the `resource-attributes` field contents")
	assert.NotEqual(t, customAttrs, resourceAttrs, "the two attribute maps MUST remain independent")
}

// TestFormal_MergePrecedenceBaseWinsOverOverride encodes P18: the layered
// attribute/header merge helper used across the OTLP configuration pipeline
// MUST let the more specific ("base") map win over the less specific
// ("override") map on key collision, matching the documented per-entry vs
// top-level precedence rules in §5.3.
func TestFormal_MergePrecedenceBaseWinsOverOverride(t *testing.T) {
	tests := []struct {
		name     string
		base     map[string]string
		override map[string]string
		want     map[string]string
	}{
		{
			name:     "base value wins on key collision",
			base:     map[string]string{"k": "base-value", "only-base": "b"},
			override: map[string]string{"k": "override-value", "only-override": "o"},
			want:     map[string]string{"k": "base-value", "only-base": "b", "only-override": "o"},
		},
		{
			name:     "disjoint keys are unioned",
			base:     map[string]string{"a": "1"},
			override: map[string]string{"b": "2"},
			want:     map[string]string{"a": "1", "b": "2"},
		},
	}

	for _, tc := range tests {
		t.Run(tc.name, func(t *testing.T) {
			got := mergeOTLPStringMaps(tc.base, tc.override)
			assert.Equal(t, tc.want, got, "base map values MUST take precedence over override map values on key collision")
		})
	}
}

// TestFormal_MergeOfEmptyMapsYieldsNil encodes P19: merging two empty (or nil)
// maps MUST return nil rather than an allocated empty map, so downstream code
// that checks len(...) == 0 or nil-ness behaves consistently.
func TestFormal_MergeOfEmptyMapsYieldsNil(t *testing.T) {
	assert.Nil(t, mergeOTLPStringMaps(nil, nil), "merging two nil maps MUST yield nil")
	assert.Nil(t, mergeOTLPStringMaps(map[string]string{}, nil), "merging an empty map and nil MUST yield nil")
	assert.Nil(t, mergeOTLPStringMaps(nil, map[string]string{}), "merging nil and an empty map MUST yield nil")
}

// metricAttributeRegistry is a stub — replace with real implementation.
// It represents the set of dimensions a conforming metric provider is
// permitted to attach by default, per §8.3.
type metricAttributeRegistry struct {
	forbiddenByDefault map[string]bool
}

// stub — replace with real implementation.
func newMetricAttributeRegistry() *metricAttributeRegistry {
	return &metricAttributeRegistry{
		forbiddenByDefault: map[string]bool{
			"gh-aw.run.id":        true,
			"github.run_id":       true,
			"trace_id":            true,
			"span_id":             true,
			"commit.sha":          true,
			"pull_request.id":     true,
			"issue.id":            true,
			"actor.id":            true,
			"item.url":            true,
			"conversation.id":     true,
			"gh-aw.workflow.name": false,
			"service.name":        false,
		},
	}
}

// stub — replace with real implementation.
func (r *metricAttributeRegistry) isAllowedByDefault(dimension string) bool {
	forbidden, known := r.forbiddenByDefault[dimension]
	if !known {
		// Unknown dimensions are conservatively allowed in this stub; a real
		// implementation MUST classify every emitted dimension explicitly.
		return true
	}
	return !forbidden
}

// TestFormal_MetricResourceCardinalityBound encodes P20 (§8.3): a metric
// provider MUST NOT attach unique run, job, trace, span, commit, actor, item,
// or conversation identifiers as metric dimensions by default. No concrete
// gh-aw metrics-cardinality-filter implementation currently exists in
// pkg/workflow, so this test exercises a minimal stub interface that captures
// the required behavior; it should be replaced with the real filter once
// implemented.
func TestFormal_MetricResourceCardinalityBound(t *testing.T) {
	registry := newMetricAttributeRegistry()

	highCardinality := []string{
		"gh-aw.run.id", "github.run_id", "trace_id", "span_id",
		"commit.sha", "pull_request.id", "issue.id", "actor.id",
		"item.url", "conversation.id",
	}
	for _, dim := range highCardinality {
		assert.False(t, registry.isAllowedByDefault(dim),
			"high-cardinality dimension %q MUST NOT be a default metric attribute per §8.3", dim)
	}

	boundedCardinality := []string{"gh-aw.workflow.name", "service.name"}
	for _, dim := range boundedCardinality {
		assert.True(t, registry.isAllowedByDefault(dim),
			"bounded-cardinality dimension %q MAY be a default metric attribute", dim)
	}
}

// instrumentationScopeResolver is a stub — replace with real implementation.
// §8.4 requires scope name "gh-aw" for core runtime telemetry and a
// gateway-specific scope such as "gh-aw-mcpg" for gateway telemetry.
type instrumentationScopeResolver struct{}

// stub — replace with real implementation.
func (instrumentationScopeResolver) coreScopeName() string { return "gh-aw" }

// stub — replace with real implementation.
func (instrumentationScopeResolver) gatewayScopeName() string { return "gh-aw-mcpg" }

// TestFormal_InstrumentationScopeNaming encodes P21 (§8.4): core runtime
// telemetry MUST use instrumentation scope "gh-aw"; gateway telemetry SHOULD
// use a gateway-specific scope such as "gh-aw-mcpg". No concrete scope-naming
// implementation currently exists in pkg/workflow, so this test exercises a
// minimal stub interface capturing the required naming contract.
func TestFormal_InstrumentationScopeNaming(t *testing.T) {
	resolver := instrumentationScopeResolver{}

	assert.Equal(t, "gh-aw", resolver.coreScopeName(),
		"core runtime instrumentation scope MUST be named \"gh-aw\" per §8.4")
	assert.Equal(t, "gh-aw-mcpg", resolver.gatewayScopeName(),
		"gateway instrumentation scope SHOULD be named \"gh-aw-mcpg\" per §8.4")
	assert.NotEqual(t, resolver.coreScopeName(), resolver.gatewayScopeName(),
		"core and gateway scopes MUST remain distinct to avoid conflating telemetry sources")
}
```

</details>

### Usage

1. Copy the test file to the appropriate package directory (`pkg/workflow/`).
2. Replace the `metricAttributeRegistry` and `instrumentationScopeResolver` stub interfaces (P20, P21) with real implementations once a metrics-cardinality filter and instrumentation-scope resolver exist in `pkg/workflow`.
3. Run: `go test ./pkg/workflow/... -run Formal`

### Context

- Spec processed: `specs/otel-observability-spec.md`
- Formal notation: TLA+ / Z3-style guard conjunction / F*
- Complements existing coverage in `pkg/workflow/otel_observability_formal_test.go` (15 predicates, P1–P15)
- Run: https://github.com/github/gh-aw/actions/runs/30754988230







> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> 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:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "proxy.golang.org"
> ```
>
> See [Network Configuration](https://github.github.com/gh-aw/reference/network/) for more information.
>
> </details>


> Generated by [🔬 Daily Formal Spec Verifier](https://github.com/github/gh-aw/actions/runs/30754988230) · auto · 83.2 AIC · ⌖ 6.12 AIC · ⊞ 10K · [◷](https://github.com/search?q=repo%3Agithub%2Fgh-aw+is%3Aissue+%22gh-aw-workflow-call-id%3A+github%2Fgh-aw%2Fdaily-formal-spec-verifier%22&type=issues)
> - [x] expires  on Aug 9, 2026, 7:52 AM UTC-08:00

Predicate / Invariant	Test Function	Description
`SecretRefResourceAttributeRejected` (P16)	`TestFormal_SecretRefResourceAttributeRejected`	Rejects `resource-attributes` values referencing `secrets.`/`vars.`; accepts literals and nil workflow data
`CustomAttributesResourceAttributesIndependent` (P17)	`TestFormal_CustomAttributesResourceAttributesIndependent`	Confirms `attributes` and `resource-attributes` are parsed and stored independently
`MergePrecedenceBaseWinsOverOverride` (P18)	`TestFormal_MergePrecedenceBaseWinsOverOverride`	Verifies base-map values win on key collision; disjoint keys are unioned
`MergeOfEmptyMapsYieldsNil` (P19)	`TestFormal_MergeOfEmptyMapsYieldsNil`	Confirms merging nil/empty maps yields nil, not an empty allocated map
`MetricResourceCardinalityBound` (P20)	`TestFormal_MetricResourceCardinalityBound`	Ensures high-cardinality identifiers are excluded from default metric dimensions; bounded ones are allowed (stub interface)
`InstrumentationScopeNaming` (P21)	`TestFormal_InstrumentationScopeNaming`	Confirms core scope is `gh-aw`, gateway scope is `gh-aw-mcpg`, and the two remain distinct (stub interface)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[formal-spec] otel-observability-spec.md — Formal model & test suite — 2026-08-02 #49807

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Uh oh!

[formal-spec] otel-observability-spec.md — Formal model & test suite — 2026-08-02 #49807

Description

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions