# Bridge example


The shipped builder kinds are related by proof objects checked through
the nix-effects kernel. For each of the four example builders — Node
service, C code generation, OCI image, and IDL — the bridge proves how
the ornament refines its base, how its forget map computes, and how
program compilation factors through forget. It also pins the shared
effect language, internalizes the materialize and dry-run step folds,
and proves their tag agreement for every program.

## What is proven

The bridge relates all four example builders — Node service, C code
generation, OCI image, and IDL — through the common `BuilderSpec`
surface and the shared builder effect language. Each kind carries
the same theorem family: ornament membership, forget codomain and
computation, and program compilation factoring through forget with
no bypass. The IDL theorems track the two-level forget through
`CodeGenBuilder` down to `BuilderSpec`. The final group internalizes
the materialize and dry-run step folds and proves they agree on
step tags for every program; the Node and C builders additionally
carry intersection theorems over their actual tool and
output-format lists.

### `node-spec-inhabits-node-ornament`

$$
\mathsf{node.spec} : \mathsf{NodeServiceBuilder.T}
$$

- Type: $\mathsf{NodeServiceBuilder.T}$
- Proof: $\mathsf{review}_{\mathsf{NodeServiceBuilder.T}}(\mathsf{node.spec})$
- Kernel result: `desc-con`


### `c-spec-inhabits-c-ornament`

$$
\mathsf{c.spec} : \mathsf{CCodegenBuilder.T}
$$

- Type: $\mathsf{CCodegenBuilder.T}$
- Proof: $\mathsf{review}_{\mathsf{CCodegenBuilder.T}}(\mathsf{c.spec})$
- Kernel result: `desc-con`


### `node-forget-has-builder-spec-codomain`

$$
\mathsf{forget}_{Node} : \mathsf{NodeServiceBuilder.T} \to \mathsf{BuilderSpec.T}
$$

- Type: $\Pi(\mathsf{spec} : \mathsf{NodeServiceBuilder.T}).\, \mathsf{BuilderSpec.T}$
- Proof: $\mathsf{forgetHoas}(\mathsf{NodeServiceBuilder})$
- Kernel result: `ann`


### `c-forget-has-builder-spec-codomain`

$$
\mathsf{forget}_{C} : \mathsf{CCodegenBuilder.T} \to \mathsf{BuilderSpec.T}
$$

- Type: $\Pi(\mathsf{spec} : \mathsf{CCodegenBuilder.T}).\, \mathsf{BuilderSpec.T}$
- Proof: $\mathsf{forgetHoas}(\mathsf{CCodegenBuilder})$
- Kernel result: `ann`


### `node-forget-computes-base-builder-spec`

$$
\mathsf{forget}_{Node}(\mathsf{node.spec}) = \mathsf{node.baseSpec} : \mathsf{BuilderSpec.T}
$$

- Type: $\operatorname{Eq}_{\mathsf{BuilderSpec.T}}(\mathsf{forget}_{Node}(\mathsf{node.spec}), \mathsf{node.baseSpec})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `c-forget-computes-base-builder-spec`

$$
\mathsf{forget}_{C}(\mathsf{c.spec}) = \mathsf{c.baseSpec} : \mathsf{BuilderSpec.T}
$$

- Type: $\operatorname{Eq}_{\mathsf{BuilderSpec.T}}(\mathsf{forget}_{C}(\mathsf{c.spec}), \mathsf{c.baseSpec})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `node-program-compilation-factors-through-forget`

$$
\mathsf{program}_{Node} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{Node}(\mathsf{node.spec})\big)
$$

- Type: $\mathsf{program}_{Node} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{Node}(\mathsf{node.spec})\big)$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Node},\ \mathsf{fromSpec}(\mathsf{forget}_{Node}(\mathsf{node.spec}))\big)$
- Kernel result: `definitional-equality`


### `c-program-compilation-factors-through-forget`

$$
\mathsf{program}_{C} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{C}(\mathsf{c.spec})\big)
$$

- Type: $\mathsf{program}_{C} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{C}(\mathsf{c.spec})\big)$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{C},\ \mathsf{fromSpec}(\mathsf{forget}_{C}(\mathsf{c.spec}))\big)$
- Kernel result: `definitional-equality`


### `node-program-is-from-ornamented-spec-no-bypass`

$$
\mathsf{program}_{Node} \equiv \mathsf{fromSpec}(\mathsf{NodeServiceBuilder.T},\ \mathsf{node.spec})
$$

- Type: $\mathsf{program}_{Node} \equiv \mathsf{fromSpec}(\mathsf{NodeServiceBuilder.T},\ \mathsf{node.spec})$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Node},\ \mathsf{fromSpec}(\mathsf{NodeServiceBuilder.T},\ \mathsf{node.spec})\big)$
- Kernel result: `definitional-equality`


### `c-program-is-from-ornamented-spec-no-bypass`

$$
\mathsf{program}_{C} \equiv \mathsf{fromSpec}(\mathsf{CCodegenBuilder.T},\ \mathsf{c.spec})
$$

- Type: $\mathsf{program}_{C} \equiv \mathsf{fromSpec}(\mathsf{CCodegenBuilder.T},\ \mathsf{c.spec})$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{C},\ \mathsf{fromSpec}(\mathsf{CCodegenBuilder.T},\ \mathsf{c.spec})\big)$
- Kernel result: `definitional-equality`


### `oci-spec-inhabits-oci-ornament`

$$
\mathsf{oci.spec} : \mathsf{OciImageBuilder.T}
$$

- Type: $\mathsf{OciImageBuilder.T}$
- Proof: $\mathsf{review}_{\mathsf{OciImageBuilder.T}}(\mathsf{oci.spec})$
- Kernel result: `desc-con`


### `oci-forget-has-builder-spec-codomain`

$$
\mathsf{forget}_{Oci} : \mathsf{OciImageBuilder.T} \to \mathsf{BuilderSpec.T}
$$

- Type: $\Pi(\mathsf{spec} : \mathsf{OciImageBuilder.T}).\, \mathsf{BuilderSpec.T}$
- Proof: $\mathsf{forgetHoas}(\mathsf{OciImageBuilder})$
- Kernel result: `ann`


### `oci-forget-computes-base-builder-spec`

$$
\mathsf{forget}_{Oci}(\mathsf{oci.spec}) = \mathsf{oci.baseSpec} : \mathsf{BuilderSpec.T}
$$

- Type: $\operatorname{Eq}_{\mathsf{BuilderSpec.T}}(\mathsf{forget}_{Oci}(\mathsf{oci.spec}), \mathsf{oci.baseSpec})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `oci-program-compilation-factors-through-forget`

$$
\mathsf{program}_{Oci} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{Oci}(\mathsf{oci.spec})\big)
$$

- Type: $\mathsf{program}_{Oci} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{Oci}(\mathsf{oci.spec})\big)$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Oci},\ \mathsf{fromSpec}(\mathsf{forget}_{Oci}(\mathsf{oci.spec}))\big)$
- Kernel result: `definitional-equality`


### `oci-program-is-from-ornamented-spec-no-bypass`

$$
\mathsf{program}_{Oci} \equiv \mathsf{fromSpec}(\mathsf{OciImageBuilder.T},\ \mathsf{oci.spec})
$$

- Type: $\mathsf{program}_{Oci} \equiv \mathsf{fromSpec}(\mathsf{OciImageBuilder.T},\ \mathsf{oci.spec})$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Oci},\ \mathsf{fromSpec}(\mathsf{OciImageBuilder.T},\ \mathsf{oci.spec})\big)$
- Kernel result: `definitional-equality`


### `idl-spec-inhabits-idl-ornament`

$$
\mathsf{idl.spec} : \mathsf{IdlBuilder.T}
$$

- Type: $\mathsf{IdlBuilder.T}$
- Proof: $\mathsf{review}_{\mathsf{IdlBuilder.T}}(\mathsf{idl.spec})$
- Kernel result: `desc-con`


### `idl-forget-has-code-gen-codomain`

$$
\mathsf{forget}_{Idl} : \mathsf{IdlBuilder.T} \to \mathsf{CodeGenBuilder.T}
$$

- Type: $\Pi(\mathsf{spec} : \mathsf{IdlBuilder.T}).\, \mathsf{CodeGenBuilder.T}$
- Proof: $\mathsf{forgetHoas}(\mathsf{IdlBuilder})$
- Kernel result: `ann`


### `idl-composite-forget-has-builder-spec-codomain`

$$
\mathsf{forget}_{CG} \circ \mathsf{forget}_{Idl} : \mathsf{IdlBuilder.T} \to \mathsf{BuilderSpec.T}
$$

- Type: $\Pi(\mathsf{spec} : \mathsf{IdlBuilder.T}).\, \mathsf{BuilderSpec.T}$
- Proof: $\lambda \mathsf{spec}.\, \mathsf{forgetHoas}(\mathsf{CodeGenBuilder})\,(\mathsf{forgetHoas}(\mathsf{IdlBuilder})\,\mathsf{spec})$
- Kernel result: `lam`


### `idl-forget-computes-code-gen-spec`

$$
\mathsf{forget}_{Idl}(\mathsf{idl.spec}) = \mathsf{idl.cgSpec} : \mathsf{CodeGenBuilder.T}
$$

- Type: $\operatorname{Eq}_{\mathsf{CodeGenBuilder.T}}(\mathsf{forget}_{Idl}(\mathsf{idl.spec}), \mathsf{idl.cgSpec})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `idl-forget-computes-base-builder-spec`

$$
\mathsf{forget}_{CG}(\mathsf{forget}_{Idl}(\mathsf{idl.spec})) = \mathsf{idl.baseSpec} : \mathsf{BuilderSpec.T}
$$

- Type: $\operatorname{Eq}_{\mathsf{BuilderSpec.T}}(\mathsf{forget}_{CG}(\mathsf{forget}_{Idl}(\mathsf{idl.spec})), \mathsf{idl.baseSpec})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `idl-program-compilation-factors-through-forget`

$$
\mathsf{program}_{Idl} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{CG}(\mathsf{forget}_{Idl}(\mathsf{idl.spec}))\big)
$$

- Type: $\mathsf{program}_{Idl} \equiv \mathsf{fromSpec}\big(\mathsf{forget}_{CG}(\mathsf{forget}_{Idl}(\mathsf{idl.spec}))\big)$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Idl},\ \mathsf{fromSpec}(\mathsf{forget}_{CG}(\mathsf{forget}_{Idl}(\mathsf{idl.spec})))\big)$
- Kernel result: `definitional-equality`


### `idl-program-is-from-ornamented-spec-no-bypass`

$$
\mathsf{program}_{Idl} \equiv \mathsf{fromSpec}(\mathsf{IdlBuilder.T},\ \mathsf{idl.spec})
$$

- Type: $\mathsf{program}_{Idl} \equiv \mathsf{fromSpec}(\mathsf{IdlBuilder.T},\ \mathsf{idl.spec})$
- Proof: $\operatorname{conv}\big(\mathsf{program}_{Idl},\ \mathsf{fromSpec}(\mathsf{IdlBuilder.T},\ \mathsf{idl.spec})\big)$
- Kernel result: `definitional-equality`


### `builder-effect-language-is-builder-plus-runtime`

$$
\mathsf{BuilderEff} \equiv \mathsf{BuilderOp.T} + \mathsf{RuntimeOp.T}
$$

- Type: $\mathsf{BuilderEff} \equiv \mathsf{BuilderOp.T} + \mathsf{RuntimeOp.T}$
- Proof: $\operatorname{conv}(\mathsf{BuilderEff}, \mathsf{BuilderOp.T} + \mathsf{RuntimeOp.T})$
- Kernel result: `definitional-equality`


### `shared-tools-normalize-from-actual-tool-lists`

$$
\operatorname{filter}(\lambda x.\, x \in \mathsf{c.tools})(\mathsf{node.tools}) = \mathsf{sharedTools}
$$

- Type: $\operatorname{Eq}_{\operatorname{List}(\mathsf{String})}(\operatorname{filter}(\lambda x.\, x \in \mathsf{c.tools})(\mathsf{node.tools}), \mathsf{sharedTools})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `shared-output-formats-normalize-from-actual-output-lists`

$$
\operatorname{filter}(\lambda x.\, x \in \mathsf{c.outputFormats})(\mathsf{node.outputFormats}) = \mathsf{sharedOutputFormats}
$$

- Type: $\operatorname{Eq}_{\operatorname{List}(\mathsf{String})}(\operatorname{filter}(\lambda x.\, x \in \mathsf{c.outputFormats})(\mathsf{node.outputFormats}), \mathsf{sharedOutputFormats})$
- Proof: $\mathsf{refl}$
- Kernel result: `desc-con`


### `matfoldk-internalizes-materialize-step-emission`

$$
\mathsf{matFoldK} : \operatorname{List}(\mathsf{BuilderEff}) \to \operatorname{List}(\mathsf{BuildPlanStep})
$$

- Type: $\Pi(\_ : \operatorname{List}(\mathsf{BuilderEff})).\, \operatorname{List}(\mathsf{BuildPlanStep})$
- Proof: $\operatorname{fold}(\operatorname{matchSum}\,(\operatorname{matchData}\,\mathsf{BuilderOp})\,(\operatorname{matchData}\,\mathsf{RuntimeOp}))$
- Kernel result: `ann`


### `mattagfoldk-projects-step-fold-to-tags`

$$
\mathsf{matTagFoldK} : \operatorname{List}(\mathsf{BuilderEff}) \to \operatorname{List}(\mathsf{StepTag})
$$

- Type: $\Pi(\_ : \operatorname{List}(\mathsf{BuilderEff})).\, \operatorname{List}(\mathsf{StepTag})$
- Proof: $\operatorname{map}\,\mathsf{tagOf} \circ \mathsf{matFoldK}$
- Kernel result: `ann`


### `drytagfoldk-internalizes-dryrun-tag-emission`

$$
\mathsf{dryTagFoldK} : \operatorname{List}(\mathsf{BuilderEff}) \to \operatorname{List}(\mathsf{StepTag})
$$

- Type: $\Pi(\_ : \operatorname{List}(\mathsf{BuilderEff})).\, \operatorname{List}(\mathsf{StepTag})$
- Proof: $\operatorname{fold}(\operatorname{matchSum}\,(\operatorname{matchData}\,\mathsf{BuilderOp}\to\mathsf{StepTag}))$
- Kernel result: `ann`


### `mattagfoldk-agrees-with-drytagfoldk-forall-p`

$$
\forall p.\ \mathsf{matTagFoldK}\,p = \mathsf{dryTagFoldK}\,p : \operatorname{List}(\mathsf{StepTag})
$$

- Type: $\Pi(p:\operatorname{List}(\mathsf{BuilderEff})).\,\operatorname{Eq}(\mathsf{matTagFoldK}\,p,\ \mathsf{dryTagFoldK}\,p)$
- Proof: $\mathsf{listElim}\,(\mathsf{sumElim}\,(\mathsf{elimData}\,\mathsf{J}/\mathsf{ih}))$
- Kernel result: `skipped` (long normalization; verified in the heavy test suite)

## Source files

These pages are the complete source for the worked example: the builder module plus the files it consumes.

- [Bridge proof module](/metaBuilder/examples/bridge/source/bridge.nix) - Source for the kernel-checked bridge theorem set.

## Normal forms

The list-intersection theorems run over the Node and C builders'
actual lists. The bridge derives these values from the loaded
builder specs:

- BuilderSpec fields: `name`, `parameters`, `inputs`, `dependencies`, `tools`, `operations`, `outputs`, `evidence`
- Node base name: `node-service-demo`
- C base name: `messages-demo`
- Node tools: `node`, `bash`
- C tools: `bash`, `gcc`, `ar`
- Shared tools: `bash`
- Node output formats: `tree`, `json`
- C output formats: `elf`, `archive`, `directory`, `text`
- Shared output formats: `[]`

## Proof boundary

The checked bridge covers the relationships currently resident in the
kernel: ornament membership, forget maps, the common effect carrier,
derived list computations over strings, and the internalized
materialize and dry-run tag folds together with their agreement
theorem. The self-views remain documentation views over the
resulting builder programs; they consume these facts but are not
themselves proof terms.