# Phase 1 Generated Composition Evidence

This evidence is executable and repository-owned. The
`internal/compositionacceptance` tests run every read-only command below with
`GOWORK=off`, `GOPROXY=off`, `GOFLAGS=-mod=vendor`, and
`GOTOOLCHAIN=local`; they parse or assert the stable output rather than storing
machine-specific absolute paths.

The proof is pinned to Spice core
`v0.1.0-preview.1.0.20260806200749-524424a04df0` and toolchain
`v0.1.0-preview.1.0.20260806203056-d0b9ac086bd6`; the latter passed its own
full verification in 422.9 seconds at 85.1% coverage before this consumer was
vendored. On the final Windows/amd64 edit loop before repository verification,
`make fast` passed in 26.2 seconds and `make check` passed in 28.4 seconds.

| Contract | Exact command | Asserted evidence |
| --- | --- | --- |
| Authorized SDK tools | `go tool github.com/spice-framework/toolchain/cmd/spice annotations doctor ./internal/compositionfixture` | `9 descriptor(s), 2 tool(s)` and no stderr |
| Bean metadata | `go tool github.com/spice-framework/toolchain/cmd/spice beans --explain --format=json ./internal/compositionfixture` | normal `alpha`/`beta`, primary `beta`, fallback `fallback`, and canonical `read`/`write` beans |
| Modulith structure | `go tool github.com/spice-framework/toolchain/cmd/spice modules --format=json ./...` | the single `github.com/spice-framework/spice-agent` root, named interfaces, no cycles, and no unassigned packages |
| Source navigation | `go tool github.com/spice-framework/toolchain/cmd/spice generated --source <manifest-source> --line <manifest-line> --target compositionproof --format json` | source-to-generated `provider-construction` mapping |
| Reverse navigation | `go tool github.com/spice-framework/toolchain/cmd/spice generated --generated <manifest-output> --line <manifest-line> --target compositionproof --format json` | generated-to-source mapping to the exact factory |
| Focused module tests | `go tool github.com/spice-framework/toolchain/cmd/spice test --module=github.com/spice-framework/spice-agent --count=1 --run=GeneratedComposition ./...` | ordinary Go tests pass for the one-module graph |
| Freshness | `go tool github.com/spice-framework/toolchain/cmd/spice generate --check --target CompositionProof . ./internal/compositionfixture` | generation is current |
| Bounded diff | `go tool github.com/spice-framework/toolchain/cmd/spice generate --diff --target CompositionProof . ./internal/compositionfixture` | generation is current with no diff |

The ownership test copies only the required module, self-authorized annotation
tool, vendored toolchain, fixture source, generated target, and manifest to a
temporary directory. Two generations are byte-identical. After a generated
provider file is modified, generation reports that the owned file changed after
the manifest and preserves the edited bytes.

The generated application tests prove:

- the normal primary `beta` provider replaces the fallback and resolves two
  normal candidates without runtime lookup;
- exact aliases of `model.Provider`, `tool.Tool`, and
  `stage.Stage[string, string]` compile through the generated graph;
- stages execute in order `trim`, then `suffix`;
- a fallback-only stage is selected, while a normal stage replaces the
  competing fallback for a second narrow stage interface;
- aliases select the `read` tool while `map[string]tool.Tool` contains only
  canonical `read` and `write` entries;
- full cleanup/error factories register immediately and stop in reverse
  `write`, `read` order;
- a later factory failure rolls back the already-constructed `read` cleanup;
- a typed `bean.Replace` override changes the selected provider for one
  generated application without a global container; and
- generated source uses direct constructor calls and contains no reflection,
  service locator, extension registry, or compiled runtime graph.

The isolated negative fixtures run through `spice verify`. Ambiguous exact
interface providers report the same ordered diagnostic over three runs.
Standalone `@Tool`, `@ModelProvider`, and `@Stage` factories with basic results
are rejected by their official handlers using compiler-owned canonical result
facts. A separate ordinary `@Bean` with a concrete tool implementation is not
implicitly assignable to `tool.Tool`; the graph fails at the exact interface
injection boundary.