Generated architecture proof

Contract

internal/architectureproof is an application-owned Spice graph. It blank imports the OpenAI and coding-tool auto-configuration packages, contributes a normal model.Provider, and consumes the generated canonical map[string]tool.Tool. It contains no runtime registry, reflection-based lookup, package scan, or hidden dependency construction.

The dispatcher, stage.StaticToolPlanSource, unavailable interaction broker, execution-plan metadata, and kernel engine are separate generated beans. The tool source is the trusted owner of a source-guaranteed immutable generation: new runs lease its current generation, snapshot recovery must request that exact generation, and every terminal or rollback path releases its lease. The plan metadata lists every executable provider, kernel/dispatch stage, broker, and static tool with the selected module version. This proof intentionally has no observer or dispatcher-decorator bean, so it does not invent placeholder identities for absent behavior.

The generated graph supplies a machine-independent semantic SnapshotCompatibilityIdentity. At run start the kernel combines it with the sorted compiled identities, exact static tool-plan ID, and immutable tool definition fingerprints. Acceptance asserts all four values rather than trusting configuration text alone.

The provider uses openaiprovider.New with an instance-owned HTTP client. Its local TLS fixture emits a Responses function call for read; the generated graph dispatches the real bounded coding tool; the kernel appends the result; and a second Responses request emits the final text. The fixture records only safe Boolean/protocol facts. The test credential is a fixed non-secret value and never enters an event, generated file, manifest, or retained request body. An independent generated-application run holds the real provider request open, cancels the caller-owned context, and requires exactly one model, turn, and run terminal outcome while the server observes request cancellation.

Generated evidence

• .spice/architectureproof.manifest.json owns every output and maps provider construction back to application or starter source.
• internal/spicegen/architectureproof/spice_providers_gen.go contains direct constructor calls, the literal named tool map, and direct plan-source, metadata, broker, and engine construction.
• spice beans --explain reports the OpenAI starter default as replaced and the read, replace, and shell defaults as selected.
• spice generate --check and spice generate --diff both require the committed output to be byte-current.
• Acceptance scans emitted event payloads, generated providers, and the ownership manifest for the fixture credential.

Verification

make fast runs the generated workflow and remains targeted below 30 seconds on a warm development machine. make check adds formatting, module/vendor, and vet checks. make verify additionally runs lint, nil safety, security, shuffled/race tests, handwritten coverage, and vendor-offline build/test. The canonical generated package is compiled and executed but excluded from the handwritten statement-coverage denominator.

This proof intentionally does not implement the daemon or TUI. It freezes the cross-repository static-composition seam those applications will consume.