Bridge example — metaBuilder

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 - 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.