# metaBuilder — Full Documentation ## Manual ### Introduction Nix builders are often ordinary functions that return derivations. That is a useful interface for building, but it hides much of the builder's structure. Which inputs matter, which tools are required, which steps run, what outputs are promised, and what runtime shape the artifact has are all left implicit. metaBuilder makes that structure explicit. A builder is written as typed data, the data is read as a program, and the program can be interpreted several ways. That is the central idea. One build, many views. ## What A Builder Describes A metaBuilder builder describes the parts a build author usually cares about. - parameters that configure the build - source inputs - dependency requirements - tools used by build steps - operations that define the build workflow - declared outputs - evidence about checks or expected behavior - descriptors for artifacts and runtime surfaces Those pieces are written once and reused by the views that validate, explain, debug, and materialize the build. ## One Program Over Fixed Operations The operations are the heart of the builder. They are drawn from a fixed signature with two families. Build-time operations cover reading sources, declaring and running tools, writing files, emitting descriptors, and producing derivations. Runtime operations cover declaring services, protocols, capabilities, and units. Every builder, however domain-specific, produces a program over those same operations, which is why one set of views can interpret all of them. ## Why This Is Different From A Function A function answers one question. Given these arguments, what value is returned. A metaBuilder program answers several questions at once. - Is the build shape valid? - Which tools and dependencies does it require? - What would it do without building anything? - What plan would materialization execute? - How does the builder describe itself? - What artifact or runtime declaration is produced? The build result still matters. metaBuilder adds the surrounding structure that makes the builder easier to inspect and evolve. ## Where Examples Fit The examples are complete tours of concrete builders. - [Node service example](/metaBuilder/examples/node-service) - [C code generation example](/metaBuilder/examples/c-codegen) - [IDL example](/metaBuilder/examples/idl) Read the manual for the model. Read the examples to see the model applied to complete artifacts. ### Getting Started This chapter shows the smallest useful shape. Define a builder spec, turn it into a program, and ask the program for several views. ## Getting metaBuilder As a flake input: ```nix { inputs.metaBuilder.url = "github:kleisli-io/metaBuilder"; outputs = { nixpkgs, metaBuilder, ... }: let pkgs = nixpkgs.legacyPackages.x86_64-linux; mb = metaBuilder.lib.mkMb pkgs; in { # use mb here }; } ``` `mkMb` builds the library against your `pkgs` and supplies the nix-effects library from the flake's own input. Pin your own nix-effects with `inputs.metaBuilder.inputs.nix-effects.follows`. Without flakes, import the source tree with explicit arguments: ```nix let fx = import nix-effects-src { inherit pkgs; lib = pkgs.lib; }; mb = import metaBuilder-src { inherit pkgs fx; lib = pkgs.lib; }; in ... ``` The rest of this chapter assumes `mb` and `pkgs` are in scope. ```nix let schema = mb.operations.localSource { name = "schema.proto"; path = ./schema.proto; }; protoc = mb.operations.tool { name = "protoc"; package = pkgs.protobuf; }; output = mb.operations.output { name = "cpp"; path = "$out/cpp"; format = "tree"; }; spec = { _con = "MetaBuilderSpec"; name = "example-idl"; parameters = [ ]; inputs = [ schema ]; dependencies = [ ]; tools = [ protoc ]; operations = [ (mb.operations.readSource { name = "schema.proto"; source = schema; }) (mb.operations.declareTool { tool = protoc; }) (mb.operations.runTool { name = "generate-cpp"; tool = protoc; args = [ "--cpp_out=$out/cpp" (toString schema.path) ]; }) (mb.operations.transformOutput { inherit output; }) (mb.operations.materializeDerivation { name = "example-idl-generated"; }) ]; outputs = [ output ]; evidence = [ ]; }; program = mb.program.fromSpec spec; in { validation = mb.program.validate.run program; dryRun = mb.program."dry-run".run program; planView = mb.program."plan-view".run program; selfView = mb.program.introspect.run program; materialize = mb.program.materialize.run program; } ``` The same `program` is reused by every view. You do not write one builder for validation, another for documentation, and another for materialization. You write the spec once and choose the view that answers the current question. ## First Checks Start with validation. It returns a record with an `ok` flag and a list of `diagnostics`, and an empty list means the shape is clean. ```nix (mb.program.validate.run program).ok ``` Use dry-run when you want to understand the build without producing an artifact. It returns the ordered `steps` the build would take. ```nix (mb.program."dry-run".run program).steps ``` Use plan-view to inspect the concrete commands and file writes materialization will perform. ```nix (mb.program."plan-view".run program).steps ``` Use materialization when you want the derivation. It returns the derivation together with the declared outputs. ```nix (mb.program.materialize.run program).derivation ``` Use introspect to get every view at once as a single self-report. ```nix mb.program.introspect.run program ``` The important habit is to treat the program as the stable object and choose the view that answers the current question. ### Builder Specs A builder spec is the public shape of a build. It gathers the pieces a builder author wants to make explicit before materialization happens. The base shape is `MetaBuilderSpec`. Every spec is a typed value, and the `_con` field names which description constructor the value inhabits. A spec is checked against its description before it becomes a program, so a missing or wrong-shaped field is reported up front. ```nix { _con = "MetaBuilderSpec"; name = "example"; parameters = [ ]; inputs = [ ]; dependencies = [ ]; tools = [ ]; operations = [ ]; outputs = [ ]; evidence = [ ]; } ``` The fields are populated with smart constructors from `mb.operations`. A smart constructor builds a well-typed value for a field, so you rarely write raw records by hand beyond the top-level spec. ## Name The `name` identifies the build in views and materialized artifacts. Choose a name that describes the artifact rather than the implementation technique. ## Parameters Parameters are the configuration surface. They should represent choices the builder user can understand, such as language target, runtime version, feature flags, artifact kind, or service port. ## Inputs Inputs are source values the build consumes. Naming inputs makes dry-run, dependency, and plan views understandable, because the build is no longer a black box around anonymous paths. ## Dependencies Dependencies describe package requirements that are part of the build design. They give dependency views a place to report what the builder needs. ## Tools Tools describe commands used by operations. A tool is more than a string name. It connects a build step to the package that provides it, so a plan never relies on a command from the user's ambient shell. ## Operations Operations are the workflow. They are the build-time and runtime steps the builder performs, and they are the field the program is sequenced from. Reading inputs, declaring tools, generating files, running commands, emitting descriptors, declaring outputs, declaring runtime structure, and materializing artifacts all appear here as operation values. ## Outputs Outputs are promises about what the build produces. A named output can be shown in documentation, checked in plans, and returned from materialization. ## Evidence Evidence records checks or expected behavior. It is useful when a builder wants to say why an artifact should be trusted, not only how it is built. ### Operations Operations are the steps of a build expressed as data. They keep the build workflow visible to validation, dry-run, plan-view, self-documentation, and materialization. An operation states intent at the builder level. The materialized command is one view of that intent, not the only meaning of the operation. Operations come from a fixed signature with two families. Build-time operations shape the derivation. Runtime operations describe how an artifact runs. A program is a sequence drawn from both families, and every operation is one or the other. ## Build-Time Operations The build-time family covers the work that produces a derivation. - `readSource` names a file or tree the build consumes - `resolveDependency` records a required package - `declareTool` introduces a tool before it is used - `runTool` runs a declared tool with arguments - `writeFile` writes generated content - `copyPath` copies a path into the build - `transformOutput` declares an intended result shape - `validateValue` checks a value during the build - `emitDescriptor` attaches structured metadata - `materializeDerivation` marks where the program becomes a derivation ## Reading Inputs Use source operations to name files or trees the build consumes. ```nix mb.operations.readSource { name = "schema"; source = schemaInput; } ``` The view layer can then report that the build uses `schema` instead of only showing a later command line. ## Declaring And Running Tools Declare a tool before running it, then connect a named step to it. ```nix mb.operations.declareTool { tool = compiler; } mb.operations.runTool { name = "compile"; tool = compiler; args = [ "-c" "$out/generated.c" "-o" "$out/generated.o" ]; } ``` Dependency analysis can show the edge from the tool to the operation, and plan-view can show the concrete command. ## Writing Files Generated files should be explicit where possible. ```nix mb.operations.writeFile { output = configHeader; text = "#define FEATURE 1\n"; } ``` This is useful for builders that generate metadata, config headers, manifests, or service descriptors. ## Emitting Descriptors And Transforming Outputs Descriptors attach structured metadata for downstream tools or documentation to read without parsing shell scripts. Output transformations declare the intended result shape, such as a tree, an archive, an ELF binary, JSON, text, or a header directory. ## Runtime Operations The runtime family describes how an artifact runs rather than how it is built. - `declareCapability` records a lifecycle or query capability - `declareProtocol` records a transport and serialization - `declareService` records a service the artifact provides - `materializeUnit` marks where the program produces a runtime unit A builder that produces a service uses these alongside the build-time operations, so one program describes both the store artifact and the way it should run. ## Materializing Materialization operations mark where the program becomes a concrete result. `materializeDerivation` produces a derivation, and `materializeUnit` produces a runtime unit. They are the boundary between a described build and a build that can be realized. ### Programs And Views A builder spec becomes a program. The program is the reusable value that different views interpret. Common entry points are the following. ```nix mb.program.fromSpec spec mb.program.fromOrnamentedSpec builderType spec mb.program.sequence operations ``` Use `fromSpec` when you already have a base builder spec. Use `fromOrnamentedSpec` when a domain builder extends the base shape. Use `sequence` when the program is already expressed as operations. Each view below is a reading of the same `program`. None of them rebuilds it. ## Validation Validation answers whether the program is structurally acceptable. It returns a record with an `ok` flag and a list of `diagnostics`. ```nix mb.program.validate.run program ``` Use it before relying on any other view. ## Dependency Graph Dependency analysis answers which tools, dependencies, services, and operations are involved. It returns a graph of `nodes` and `edges`. ```nix mb.program.deps.run program ``` This view is useful when a builder grows and you need to see whether it still says what it depends on. ## Dry-Run Dry-run answers what would happen without materializing the artifact. It returns the ordered `steps` of the workflow. ```nix mb.program."dry-run".run program ``` Use it as a fast explanation of the builder's workflow. ## Plan View Plan-view answers what materialization would execute. It returns the typed plan steps and the rendered commands. ```nix mb.program."plan-view".run program ``` Use it when you need to inspect command order, generated file writes, and the shape of the materialization plan. ## Describe Describe answers how the builder program documents itself. It returns a rendered, operation-level explanation of the builder. ```nix mb.program.describe.run program ``` ## Introspect Introspect composes the main views into one self-view, so a single call returns validation, dependencies, dry-run, plan, documentation, and materialization together. ```nix mb.program.introspect.run program ``` Use it when you want the complete one build, many views report. ## Materialize Materialization returns the build artifact. The result carries the `derivation` along with the declared outputs and any runtime declarations. ```nix mb.program.materialize.run program ``` Use materialization only after the views show the build says what you intend. ### Designing Builder Surfaces A good builder surface starts from the domain, not from the generic build machinery. For a service builder, the domain might include runtime, entrypoint, port, health path, and service protocol. For a native code generator, the domain might include schema, compiler, defines, artifact kind, and generated outputs. The public constructor should ask for those domain concepts and lower them into the shared builder program. ## Start From The Artifact Ask what the builder promises to produce. A runnable package, a generated source tree, a static library, a CLI, a service unit, or a descriptor bundle each imply different outputs, operations, tools, and runtime descriptors. The artifact tells you which of those the builder needs. ## Name The Vocabulary Use domain names in the public API and avoid exposing generic mechanics when a domain term is clearer. A service builder should ask for a `port` or a `healthPath` before it asks the user to construct a low-level runtime protocol value. ## Keep The Constructor Small A constructor should accept the smallest set of choices that define the build. Everything derived from those choices should be generated by the builder. This keeps the user-facing API stable while the internal program becomes more capable. ## Lower Into Operations The constructor is responsible for lowering domain choices into operations. That lowering is where tools, generated files, descriptors, output declarations, and materialization steps enter the program. The domain fields capture what the user said, and the operations capture what the build does. ## Expose Standard Views A production builder should expose the same standard views during development. Validation, dependency graph, dry-run, plan-view, describe, introspect, and materialize together become the builder's debugging and documentation surface. ## Use Ornaments For Domain Shape An ornament extends the base builder spec with domain-specific fields. Use one when a builder needs a typed domain shape but should still behave like a normal metaBuilder program. The ornament adds data only. It never extends the operation alphabet, and a typed forget map projects the ornamented builder back to the shared shape while keeping its program intact. That is what lets a domain builder stay fully compatible with every standard view. ### Outputs, Evidence, And Runtime Artifacts Builders need to communicate more than the fact that a derivation exists. A user often needs to know what the artifact contains, how it was checked, and how it should run. metaBuilder gives those concerns explicit places in the build description. ## Outputs Outputs name the results a build promises. A generated source tree, a static library, a CLI binary, a JSON manifest, package metadata, or a service tree are typical examples. An output should have a name, a path, and a format, which lets views explain what the build returns without executing it. ## Descriptors Descriptors are structured metadata. Use them when a builder wants to report facts about the artifact, such as compiler identity, runtime version, protocol, generated files, package manager, or artifact kind. Descriptors are better than conventions hidden in filenames because they are part of the program's data. ## Evidence Evidence records checks or claims about the artifact. A syntax-check command, a smoke-test expectation, a generated-artifact invariant, or a compatibility assertion can each be recorded as evidence. Evidence does not replace tests. It gives the builder a typed place to report why a produced artifact should be trusted. ## Runtime Artifacts Some builders produce things that run as services. For those builders the runtime shape should be explicit, and it is expressed with the runtime operations for services, protocols, lifecycle capabilities, and runtime units. These runtime declarations are kept structure. They survive into the materialized result, so the same builder describes both build-time and runtime behavior and returns both from one program. ### Materialization Model Materialization turns a builder program into an artifact. It is one interpretation of the program, not the whole meaning of the builder. The materialization view is useful because it keeps the executable plan visible before and after a derivation exists. ## Plans A plan is the materializable shape of the program. It records the steps that write files, run tools, transform outputs, and produce final artifacts. Plans let you inspect order and intent before asking Nix to build. Materialization works by walking the program and building up a plan state as it goes. The plan state carries working bookkeeping, such as which tools and services have been declared so far, so that later steps can be checked against earlier ones. ## From Plan State To Build Plan When the walk finishes, the plan state is projected into the final build plan. This projection forgets the working bookkeeping and keeps what the artifact needs, which is the outputs, the derivation, and the runtime declarations the builder promised. The bookkeeping existed only to validate the build as it was assembled. ## Tool References Tool references connect command steps to packages. This matters because a plan should not rely on ambient commands from the user's shell. If a step runs `gcc`, the program should know which package provides `gcc`. ## Generated Commands Plan-view exposes command snippets so users can inspect what materialization will execute. Use this view for debugging. The builder API should still be expressed in domain terms rather than asking users to manage every command directly. ## Derivation Outputs Materialization returns derivations and output declarations. The result should match the outputs the builder promised earlier in the spec. ## Runtime Artifacts When the program declares runtime services or units, materialization carries those declarations alongside the derivation result. A builder can therefore produce both a store artifact and a runtime description from the same program. ### Authoring Production Builders Production builders should grow from a small domain surface into a reliable program, not from a large compatibility wrapper. Start with the artifact, name the domain concepts, then expose the standard views that make the builder inspectable. ## Begin With The Smallest Useful Constructor A first constructor should accept only the choices needed to produce the artifact. More options can be added when the builder has a real domain reason for them. ## Add Typed Configuration Deliberately Typed configuration is valuable when it clarifies the build vocabulary. Avoid adding fields only because an underlying command happens to have many flags. A field earns its place when a view becomes more meaningful for having it. ## Prefer Descriptors Over Hidden Conventions If downstream users need to know something, put it in a descriptor. Do not make them infer important facts from path names or shell snippets. ## Keep Views In The Contract Validation, dependency graph, dry-run, plan-view, describe, introspect, and materialize are not only development helpers. They are part of how users learn and trust the builder, so treat their output as a public contract. ## Test The Views That Matter Tests should pin the views that define the builder's public contract. Useful anchors are that validation succeeds for supported specs, that the dependency graph includes the expected tools and operations, that dry-run explains the intended workflow, that plan-view includes the expected materialization shape, and that materialization produces the promised outputs. ## Avoid Compatibility Before Release Do not add compatibility shims before there is a public compatibility problem. Early builders should be shaped around the model you want users to learn. ## Theory ### Builders As Descriptions The central move in metaBuilder is to treat a builder as a description before it is treated as an executable artifact. A description is typed data. Parameters, sources, dependencies, tools, operations, outputs, evidence, and runtime declarations are all generated datatypes with named constructors and fields. A builder spec is an inhabitant of the base description type, and it is checked against that type before anything is built. A spec that is missing a required field or carries the wrong shape is rejected at description time, not at build time. Because the builder is data, its parts are available to inspect and reinterpret. A description says which parts exist and how they relate without committing to the single thing that could be done with them. That separation is what makes multiple views possible. ## Functions And Descriptions A function gives an answer when it is called. It can hide everything that happened on the way to the answer. A description can be read before any answer is produced. It can be checked, summarized, documented, or interpreted into a build. The description is not less precise than a function. It is precise in a form that supports more than one use. ## Typed All The Way Down The types are not decoration. They are the same descriptions the views read and the same descriptions the documentation and schemas are generated from. A field added to a description becomes visible to validation, to dependency analysis, to the rendered docs, and to materialization at once, because all of them read the one typed source. ## Structure Before Execution When a builder is described structurally, its components become available to generic interpretations. Validation inspects the shape. Dependency analysis inspects tools and operations. Dry-run summarizes intent. Plan-view renders an executable plan. Materialization produces the artifact. The build still happens. metaBuilder adds the structure around it that makes the builder inspectable before it runs. ### Internalized Programs An internalized program is a build workflow represented as a value. The value is not a script and not a derivation. It is typed data that records the steps of a build and the order they run in. This is the object every view shares. Validation, dependency analysis, dry-run, plan-view, documentation, introspection, and materialization are all readings of the same program value. ## Operations As A Signature A program is built from operations, and the operations are not an open-ended set of arbitrary effects. They come from a fixed signature with two families. Build-time operations read sources, declare tools, write files, run commands, emit descriptors, and produce derivations. Runtime operations declare services, protocols, capabilities, and units. The signature is the sum of those two families. Every operation in a program is either a build-time operation or a runtime operation and nothing else. Because the alphabet is fixed and total, a view always knows the full set of cases it must handle, and a builder can never smuggle in an effect the views do not understand. ## Programs Are Free The program is the free sequencing of operations over that signature. Free means the program records only which operations occur and in what order. It does not decide what they mean. Meaning is supplied later by a view. This is why one program supports many readings. The program commits to the build's structure and leaves interpretation open. A function would have collapsed that structure into a single answer the moment it was called. ## Meaning By Interpretation A view gives the program meaning by handling each operation. Validation handles an operation by checking it. Dependency analysis handles it by recording what it mentions. Materialization handles it by turning it into part of a derivation. No view owns the program. Each one walks the same sequence of operations and answers a different question. The final derivation is one such answer, not the whole meaning of the builder. ### Ornaments And Domain Surfaces An ornament enriches a base description with domain-specific structure. For metaBuilder the base description is the shared builder shape. A domain builder adds fields for its own vocabulary while keeping the ability to become an ordinary builder program. A service ornament can add a runtime, a port, and a health path. A code-generator ornament can add a compiler identity, a set of defines, and a generated artifact kind. ## Refining Data, Not Operations An ornament refines the data of a description. It does not change the operation alphabet. The shared signature of build-time and runtime operations stays fixed for every builder, ornamented or not. A domain builder still produces a program over the same operations, so every view that understands the base program understands the ornamented one without modification. This is the discipline that keeps domains from fragmenting the model. New vocabulary enters as new fields, and those fields are lowered into the shared operations by the builder's constructor. The operation alphabet is never extended per domain. ## Preserving The Base Shape The enriched builder still carries the shared pieces. Those pieces are inputs, tools, operations, outputs, and evidence. The common views know how to read exactly those pieces, which is why they keep working across domains. ## Adding Domain Meaning The added fields should be meaningful in the domain. Service protocol, health path, compiler identity, generated artifact kind, and language target are good examples. They let a builder author speak in domain terms without giving up the shared program model. ## Surface And Forgetting The domain surface is what users write. The shared builder shape is what the views understand. Moving between them is a real, typed map called forgetting. It projects an ornamented builder onto the shared shape by dropping the domain-only fields and keeping the shared pieces. Those shared pieces are inputs, tools, operations, outputs, and evidence. Because the operations live in the shared shape, forgetting preserves them. The program you get from a forgotten spec is the same program the ornamented spec describes. Nothing the build needs is lost by speaking in domain terms. This forget map is checked, not informal. The projection is certified to land in the base builder type, so an ornamented builder always forgets to a genuine shared builder. Forgetting recurs later in the pipeline. Materialization carries a working plan state with derived bookkeeping, and the final build plan forgets that bookkeeping while keeping only the outputs and runtime declarations the builder promised. Each stage forgets exactly what the next stage does not need. ### Interpretation And Views A view is an interpretation of a program. The program is a sequence of operations and says nothing about their meaning on its own. A view supplies the meaning by handling each operation as the sequence is walked. Because every view reads the same program over the same fixed operation alphabet, the views agree by construction. They differ only in how each operation is handled, not in which operations exist. ## Validation Validation interprets the program as a shape to check. It walks the operations and collects diagnostics, then reports whether the program is acceptable before any artifact is produced. An empty diagnostic list means the build shape is clean. ## Dependency Graph Dependency analysis interprets the program as a graph of requirements and uses. It records nodes for tools, dependencies, services, and operations, and edges for how they relate, so a grown builder can be checked against what it claims to need. ## Dry-Run Dry-run interprets the program as a user-facing summary. It turns each operation into a short statement of intent and produces the ordered list of steps the build would take, without performing them. ## Plan-View Plan-view interprets the program as an executable plan. It builds the same typed plan that materialization uses and renders the concrete commands and file writes, so command order and shape can be inspected before Nix is asked to build. ## Documentation Documentation interprets the program as an explanation. It reads the operations and the declared outputs and renders a description of how the build presents itself to a user. ## Materialization Materialization interprets the program as an artifact-producing plan. It handles build-time operations into a derivation and runtime operations into runtime declarations, returning the derivation together with the outputs and runtime descriptions the builder promised. ## One Program, Many Answers The views are different, and their agreement comes from sharing one program. The final derivation is one interpretation among several. A builder that reads well under validation, dependency analysis, dry-run, and documentation is a builder whose meaning is understood before it is built. ### Evidence, Descriptors, And Runtime Structure Build systems often treat metadata as something outside the build. metaBuilder treats important metadata as part of the description, because a builder's meaning is not exhausted by its store path. ## Evidence Evidence gives checks and claims a place in the description. A smoke test, an expected behavior, or an invariant can be represented as data that views surface. Evidence does not replace tests. It gives the builder a typed place to say why a produced artifact should be trusted. ## Descriptors Descriptors carry structured facts about an artifact. Compiler identity, runtime version, protocol, generated files, and artifact kind are facts a builder should state directly rather than hide in path names or shell scripts. Because a descriptor is part of the program's data, downstream tools and documentation can read it without parsing conventions. ## Runtime Structure Some artifacts are meant to run. Runtime services, protocols, capabilities, and units describe that operational shape. These come from the runtime half of the operation signature, so a builder declares its runtime structure with the same program it uses to build. The runtime declarations are kept structure, not forgotten bookkeeping. They survive into the materialized result, which is why the same program can produce a store artifact and a runtime description together. ## Why They Belong Together Evidence, descriptors, and runtime declarations all answer questions about the artifact beyond whether it built. They belong in the same descriptive model because users need them to evaluate, compose, and operate builders. ## Examples ### Node service example This tour builds a tiny HTTP service from `server.js`. The point is not to mimic a full Node packaging API; it is to show how a builder can name its domain concepts and then expose several views of the same build. The worked artifact is a runnable package with a copied service source, generated package metadata, a wrapper script, an HTTP service descriptor, a runtime unit declaration, and a materialization plan. ## Start from the artifact The source fixture is one file: `node-service/server.js`. The builder turns that file into a runnable tree: - `bin/node-service-demo` starts the service with Node. - `lib/node-service-demo/server.js` contains the copied source. - `share/node-service-demo/package.json` is generated from the typed builder spec. - the runtime view describes the service as HTTP on port 3000 with a `/health` endpoint. ## Source files These pages are the complete source for the worked example: the builder module plus the files it consumes. - [Node service builder module](/metaBuilder/examples/node-service/source/builder.nix) - Source for the Node service builder constructor and worked demo program. - [server.js](/metaBuilder/examples/node-service/source/server.js) - HTTP service fixture copied into the materialized Node demo package. ## Builder vocabulary `NodeServiceBuilder` ornaments the generic `BuilderSpec` with the fields a service builder cares about: runtime version, entrypoint, package manager, script table, test command, service descriptor, and runtime operations. The constructor keeps the public surface small. ```nix nodeService { name = "node-service-demo"; source = ./node-service/server.js; } ``` ## Program walkthrough The constructor lowers the service spec into an internalized program. The builder-facing operations read the source, declare `node` and `bash`, generate `package.json`, run a syntax check, install the runnable tree, emit metadata, and declare the materialized outputs. The runtime operations are part of the same program. They declare the lifecycle capability set, the HTTP protocol, the concrete service, and the runtime unit. That is why dependency analysis, dry-run output, plan-view output, and self-documentation all see the service shape. ## One build, many views The section below is generated from `mb.program.introspect.run program`. It is not a hand-written summary. It validates the program, extracts the dependency graph, renders dry-run and plan-view output, includes service descriptors, and reports the materialized outputs. The same internalized program is interpreted several ways. ### Validation - result: `ok` ### Dependency Graph - nodes: `5` - edges: `2` - services: `1` - node `tool:node` (tool) package `nodejs` - node `tool:bash` (tool) package `bash-interactive` - node `operation:syntax-check` (operation) via `node` - node `operation:install-service` (operation) via `bash` - node `service:node-service-demo-service` (service) package `nodejs` - edge `tool:node` -> `operation:syntax-check` (uses-tool) - edge `tool:bash` -> `operation:install-service` (uses-tool) ### Dry Run - Builder - source `server.js` - tool `node` - tool `bash` - write `share/node-service-demo/package.json` - run `syntax-check` with `node` - run `install-service` with `bash` - descriptor `node-service-demo-metadata` - transform `service-tree` (tree) - transform `package-json` (json) - materialize `node-service-demo-artifact` with `runCommand` - evidence `self-test` ### Dry Run - Runtime - runtime capability `lifecycle` - runtime protocol `http` - runtime service `node-service-demo-service` - runtime unit `node-service-demo-service` ### Plan View - write `write:share/node-service-demo/package.json` - run `syntax-check` - run `install-service` - `write:share/node-service-demo/package.json`: `mkdir -p "$(dirname "$out/share/node-service-demo/package.json")"` - `syntax-check`: `node --check "$pathMap_85e860eb67550a011692fa61e2a4543318fcdb72bf6de38c7f85842029ee99ae"` - `install-service`: `bash -c 'set -eu` ### Plan Shell Excerpt ```sh pathMap_85e860eb67550a011692fa61e2a4543318fcdb72bf6de38c7f85842029ee99ae= mkdir -p "$(dirname "$out/share/node-service-demo/package.json")" cat > "$out/share/node-service-demo/package.json" <<'METABUILDER_HEREDOC_83625931feff0ed1f14d2f61a28aea1a87b63276765f4ca0cc2bceddf130aeed' {"main":"server.js","name":"node-service-demo","private":true,"scripts":{"start":"node server.js","test":"node --check server.js"},"type":"module","version":"0.1.0"} METABUILDER_HEREDOC_83625931feff0ed1f14d2f61a28aea1a87b63276765f4ca0cc2bceddf130aeed node --check "$pathMap_85e860eb67550a011692fa61e2a4543318fcdb72bf6de38c7f85842029ee99ae" bash -c 'set -eu src="$1" mkdir -p "'"$out"'/bin" "'"$out"'/lib/node-service-demo" "'"$out"'/share/node-service-demo" cp "$src" "'"$out"'/lib/node-service-demo/server.js" ``` ### Runtime Services - service `node-service-demo-service` exposes `http/TCP/JSON PORT:3000`; capabilities `start`, `stop`, `health` ### Descriptors - descriptor `node-service-demo-metadata` (payload keys `entrypoint`, `healthPath`, `kind`, `packageManager`, `port`, `runtimeVersion`) ### Builder Self-Documentation - documented operations: `15` - runtime services: `1` ### Materialized Outputs - service-tree -> $out (tree) - package-json -> share/node-service-demo/package.json (json) ### Materialization - derivation: `node-service-demo-artifact` - outputs: `2` - runtime artifacts: `1` - service `node-service-demo-service` ### Substrates - dockerfile: `supported` - shell: `supported` ### Source files These files are the complete source for Node service example: the builder module plus the fixtures it consumes. - [Node service builder module](/metaBuilder/examples/node-service/source/builder.nix) - Source for the Node service builder constructor and worked demo program. - [server.js](/metaBuilder/examples/node-service/source/server.js) - HTTP service fixture copied into the materialized Node demo package. ### Node service builder module This module defines the `NodeServiceBuilder` ornament, the `nodeService` constructor, the concrete `node-service-demo` spec, and the exported views used by the tour page. Source path: [`examples/node-service/builder.nix`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/node-service/builder.nix). ```nix { mb, fx, lib, pkgs, ... }: let H = fx.types.hoas; G = fx.types.generic; ops = mb.operations; eff = mb.program.eff; NodeServiceBuilder = H.ornament mb.descriptions.BuilderSpec { name = "MetaBuilderNodeService"; constructors.MetaBuilderSpec.fields = [ { insert = "runtimeVersion"; type = H.string; } { insert = "entrypoint"; type = H.string; } { insert = "packageManager"; type = H.string; } { insert = "scripts"; type = H.attrs; } { insert = "testCommand"; type = H.string; } { insert = "service"; type = mb.descriptions.ServiceSpec.T; } { keep = "name"; } { keep = "parameters"; } { keep = "inputs"; } { keep = "dependencies"; } { keep = "tools"; } { keep = "operations"; } { keep = "outputs"; } { keep = "evidence"; } ]; }; nodeService = { name , source , version ? "0.1.0" , runtimePackage ? pkgs.nodejs , runtimeVersion ? runtimePackage.version or "node" , entrypoint ? baseNameOf (toString source) , packageManager ? "npm" , port ? 3000 , healthPath ? "/health" }: let sourceFile = ops.localSource { name = entrypoint; path = source; }; nodeTool = ops.tool { name = "node"; package = runtimePackage; }; bashTool = ops.tool { name = "bash"; package = pkgs.bash; }; lifecycleSet = ops.capabilitySet { categories = [ mb.ornaments.capabilities.builtins.lifecycle ]; }; protocol = ops.protocol { name = "http"; description = "HTTP service protocol"; transport = ops.transports.TCP; serialization = ops.serializations.JSON; defaultPort = port; portEnvVar = "PORT"; capabilities = lifecycleSet; options = { inherit healthPath; }; }; service = ops.service { name = "${name}-service"; description = "Runnable Node service artifact"; package = runtimePackage; capabilities = lifecycleSet; protocols = [ protocol ]; config = [ (ops.param { name = "port"; description = "TCP port for the HTTP server"; type = ops.runtimeTypes.RTInt; required = false; }) (ops.param { name = "healthPath"; description = "HTTP path used for health checks"; type = ops.runtimeTypes.RTString; required = false; }) ]; }; scripts = { start = "node ${entrypoint}"; test = "node --check ${entrypoint}"; }; testCommand = scripts.test; appOutput = ops.output { name = "service-tree"; path = "$out"; format = "tree"; }; packageOutput = ops.output { name = "package-json"; path = "share/${name}/package.json"; format = "json"; }; packageJson = builtins.toJSON { inherit name version; type = "module"; main = entrypoint; private = true; inherit scripts; }; installScript = '' set -eu src="$1" mkdir -p "$out/bin" "$out/lib/${name}" "$out/share/${name}" cp "$src" "$out/lib/${name}/${entrypoint}" cat > "$out/bin/${name}" < { requestsTotal += 1; if (request.url === "/health") { response.writeHead(200, { "content-type": "application/json" }); response.end(JSON.stringify({ ok: true })); return; } if (request.url === "/version") { response.writeHead(200, { "content-type": "application/json" }); response.end(JSON.stringify({ version })); return; } if (request.url === "/metrics") { response.writeHead(200, { "content-type": "text/plain; version=0.0.4" }); response.end( [ "# HELP node_service_requests_total Total HTTP requests handled.", "# TYPE node_service_requests_total counter", `node_service_requests_total ${requestsTotal}`, "# HELP node_service_uptime_seconds Process uptime in seconds.", "# TYPE node_service_uptime_seconds gauge", `node_service_uptime_seconds ${process.uptime()}`, "", ].join("\n"), ); return; } response.writeHead(200, { "content-type": "application/json" }); response.end(JSON.stringify({ service: "node-service-demo" })); }); server.listen(port, "127.0.0.1", () => { console.log(`node-service-demo listening on ${port}`); }); ``` ### C code generation example This tour builds a small native artifact from a message schema. The example is intentionally compact: one schema file, one hand-written `main.c`, generated C sources, a static library, and a CLI that proves the generated library links and runs. The point is to show how a native builder can expose generated files, toolchain steps, descriptors, outputs, and the materialization plan as views of one typed program. ## Start from the artifact The source fixture is `c-codegen/messages.def`, a tiny key/value schema. The builder generates: - `include/config.h` from typed configuration defines. - `include/generated_messages.h` and `generated/generated_messages.c` from the schema. - `lib/libmessages-demo.a` from the generated object. - `bin/messages-demo`, linked against the generated library. - `lib/pkgconfig/messages-demo.pc` as metadata for downstream users. ## Source files These pages are the complete source for the worked example: the builder module plus the files it consumes. - [C codegen builder module](/metaBuilder/examples/c-codegen/source/builder.nix) - Source for the C codegen builder constructor and worked native demo program. - [messages.def](/metaBuilder/examples/c-codegen/source/messages.def) - Schema fixture consumed by the C code generator in the native demo. - [main.c](/metaBuilder/examples/c-codegen/source/main.c) - Small CLI source linked against the generated static library. ## Builder vocabulary `CCodegenBuilder` ornaments `BuilderSpec` with the native-builder fields that matter here: compiler identity, schema input, config defines, and artifact kind. The public constructor keeps the domain surface focused on the source inputs and leaves the internal program to spell out the build mechanics. ```nix cCodegen { name = "messages-demo"; schema = ./c-codegen/messages.def; main = ./c-codegen/main.c; } ``` ## Program walkthrough The constructor lowers the spec into a sequence of operations: read the schema and `main.c`, declare `bash`, `gcc`, and `ar`, write the config header, generate C sources, compile the generated source, archive the static library, link the demo CLI, run a smoke test, emit pkg-config metadata, and declare each output. Because those steps are data, metaBuilder can interpret them without rebuilding the builder by hand. Dependency analysis sees the tool-use edges, dry-run shows the build actions, plan-view exposes the shell plan, and materialization turns the same plan into a derivation. ## One build, many views The section below is generated from `mb.program.introspect.run program`. It is the internalized view of the native build: validation, dependency graph, dry-run, plan-view, descriptors, outputs, and materialization. The same internalized program is interpreted several ways. ### Validation - result: `ok` ### Dependency Graph - nodes: `8` - edges: `5` - services: `0` - node `tool:bash` (tool) package `bash-interactive` - node `tool:gcc` (tool) package `gcc-wrapper` - node `tool:ar` (tool) package `binutils-wrapper` - node `operation:generate-c-sources` (operation) via `bash` - node `operation:compile-generated-object` (operation) via `gcc` - node `operation:archive-library` (operation) via `ar` - node `operation:link-demo-cli` (operation) via `gcc` - node `operation:smoke-test` (operation) via `bash` - edge `tool:bash` -> `operation:generate-c-sources` (uses-tool) - edge `tool:gcc` -> `operation:compile-generated-object` (uses-tool) - edge `tool:ar` -> `operation:archive-library` (uses-tool) - edge `tool:gcc` -> `operation:link-demo-cli` (uses-tool) - edge `tool:bash` -> `operation:smoke-test` (uses-tool) ### Dry Run - Builder - source `messages.def` - source `main.c` - tool `bash` - tool `gcc` - tool `ar` - write `include/config.h` - run `generate-c-sources` with `bash` - run `compile-generated-object` with `gcc` - run `archive-library` with `ar` - run `link-demo-cli` with `gcc` - run `smoke-test` with `bash` - write `lib/pkgconfig/messages-demo.pc` - descriptor `messages-demo-metadata` - transform `cli` (elf) - transform `static-library` (archive) - transform `headers` (directory) - transform `pkg-config` (text) - materialize `messages-demo-artifact` with `runCommand` - evidence `smoke-test` ### Dry Run - Runtime None. ### Plan View - write `write:include/config.h` - run `generate-c-sources` - run `compile-generated-object` - run `archive-library` - run `link-demo-cli` - run `smoke-test` - write `write:lib/pkgconfig/messages-demo.pc` - `write:include/config.h`: `mkdir -p "$(dirname "$out/include/config.h")"` - `generate-c-sources`: `bash -c 'set -eu` - `compile-generated-object`: `gcc -I"$out"/include -c ''"$out"/generated/generated_messages.c -o ''"$out"/generated/generated_messages.o` - `archive-library`: `ar rcs ''"$out"/lib/libmessages-demo.a ''"$out"/generated/generated_messages.o` - `link-demo-cli`: `gcc -I"$out"/include "$pathMap_45f70a987ef70685ad13cc6283095c8504a3d4d95f23567a890bb52427d3338d" ''"$out"/lib/libmessages-demo.a -o ''"$out"/bin/messages-demo` - `smoke-test`: `bash -c 'set -eu` - `write:lib/pkgconfig/messages-demo.pc`: `mkdir -p "$(dirname "$out/lib/pkgconfig/messages-demo.pc")"` ### Plan Shell Excerpt ```sh pathMap_301f316e1baa45459961d7b5c3f4a9881e17adfe67b148a8295231c6d567d78f= pathMap_45f70a987ef70685ad13cc6283095c8504a3d4d95f23567a890bb52427d3338d= mkdir -p "$(dirname "$out/include/config.h")" cat > "$out/include/config.h" <<'METABUILDER_HEREDOC_856398558058b5929d6076680e5c3cd22f31adde4a8117afd770ec6dc55cfd7d' #define DEMO_FEATURE 1 #define MESSAGE_LIMIT 8 METABUILDER_HEREDOC_856398558058b5929d6076680e5c3cd22f31adde4a8117afd770ec6dc55cfd7d bash -c 'set -eu schema="$1" ``` ### Runtime Services None. ### Descriptors - descriptor `messages-demo-metadata` (payload keys `artifactKind`, `compiler`, `configDefines`, `generated`, `kind`) ### Builder Self-Documentation - documented operations: `19` - runtime services: `0` ### Materialized Outputs - cli -> $out/bin/messages-demo (elf) - static-library -> $out/lib/libmessages-demo.a (archive) - headers -> $out/include (directory) - pkg-config -> lib/pkgconfig/messages-demo.pc (text) ### Materialization - derivation: `messages-demo-artifact` - outputs: `4` - runtime artifacts: `0` ### Substrates - dockerfile: `supported` - shell: `supported` ### Source files These files are the complete source for C code generation example: the builder module plus the fixtures it consumes. - [C codegen builder module](/metaBuilder/examples/c-codegen/source/builder.nix) - Source for the C codegen builder constructor and worked native demo program. - [messages.def](/metaBuilder/examples/c-codegen/source/messages.def) - Schema fixture consumed by the C code generator in the native demo. - [main.c](/metaBuilder/examples/c-codegen/source/main.c) - Small CLI source linked against the generated static library. ### C codegen builder module This module defines the `CCodegenBuilder` ornament, the `cCodegen` constructor, the concrete `messages-demo` spec, and the exported views used by the tour page. Source path: [`examples/c-codegen/builder.nix`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/c-codegen/builder.nix). ```nix { mb, fx, lib, pkgs, ... }: let H = fx.types.hoas; G = fx.types.generic; ops = mb.operations; eff = mb.program.eff; CCodegenBuilder = H.ornament mb.descriptions.BuilderSpec { name = "MetaBuilderCCodegen"; constructors.MetaBuilderSpec.fields = [ { insert = "compiler"; type = H.string; } { insert = "schema"; type = H.any; } { insert = "configDefines"; type = H.attrs; } { insert = "artifactKind"; type = H.string; } { keep = "name"; } { keep = "parameters"; } { keep = "inputs"; } { keep = "dependencies"; } { keep = "tools"; } { keep = "operations"; } { keep = "outputs"; } { keep = "evidence"; } ]; }; cCodegen = { name , schema , main , compilerPackage ? pkgs.gcc , binutilsPackage ? pkgs.binutils , compiler ? compilerPackage.pname or "gcc" , configDefines ? { DEMO_FEATURE = 1; MESSAGE_LIMIT = 8; } , artifactKind ? "static-library-with-cli" }: let schemaSource = ops.localSource { name = baseNameOf (toString schema); path = schema; }; mainSource = ops.localSource { name = baseNameOf (toString main); path = main; }; gccTool = ops.tool { name = "gcc"; package = compilerPackage; }; arTool = ops.tool { name = "ar"; package = binutilsPackage; }; bashTool = ops.tool { name = "bash"; package = pkgs.bash; }; cliOutput = ops.output { name = "cli"; path = "$out/bin/${name}"; format = "elf"; }; libraryOutput = ops.output { name = "static-library"; path = "$out/lib/lib${name}.a"; format = "archive"; }; headerOutput = ops.output { name = "headers"; path = "$out/include"; format = "directory"; }; pkgConfigOutput = ops.output { name = "pkg-config"; path = "lib/pkgconfig/${name}.pc"; format = "text"; }; defineLines = lib.concatStringsSep "\n" (lib.mapAttrsToList (key: value: "#define ${key} ${toString value}") configDefines); codegenScript = '' set -eu schema="$1" mkdir -p "$out/generated" "$out/include" "$out/lib" "$out/bin" "$out/share/${name}" "$out/lib/pkgconfig" header="$out/include/generated_messages.h" source="$out/generated/generated_messages.c" printf '%s\n' '#pragma once' '#include "config.h"' > "$header" printf '%s\n' '#include "generated_messages.h"' > "$source" while IFS=: read key text; do if [ -z "$key" ]; then continue fi printf 'const char *message_%s(void);\n' "$key" >> "$header" printf 'const char *message_%s(void) { return "%s"; }\n' "$key" "$text" >> "$source" done < "$schema" ''; smokeScript = '' set -eu mkdir -p "$out/share/${name}" "$out/bin/${name}" > "$out/share/${name}/smoke.txt" ''; packageConfig = '' prefix=$out exec_prefix=$out libdir=$out/lib includedir=$out/include Name: ${name} Description: generated C demo library Version: 0.1.0 Libs: -L$out/lib -l${name} Cflags: -I$out/include ''; operations = [ (eff.builder.readSource { name = schemaSource.name; source = schemaSource; }) (eff.builder.readSource { name = mainSource.name; source = mainSource; }) (eff.builder.declareTool { tool = bashTool; }) (eff.builder.declareTool { tool = gccTool; }) (eff.builder.declareTool { tool = arTool; }) (eff.builder.writeFile { output = ops.output { name = "config-header"; path = "include/config.h"; format = "c-header"; }; text = "${defineLines}\n"; }) (eff.builder.runTool { name = "generate-c-sources"; tool = bashTool; args = [ "-c" codegenScript "generate-c-sources" (toString schema) ]; }) (eff.builder.runTool { name = "compile-generated-object"; tool = gccTool; args = [ "-I$out/include" "-c" "$out/generated/generated_messages.c" "-o" "$out/generated/generated_messages.o" ]; }) (eff.builder.runTool { name = "archive-library"; tool = arTool; args = [ "rcs" "$out/lib/lib${name}.a" "$out/generated/generated_messages.o" ]; }) (eff.builder.runTool { name = "link-demo-cli"; tool = gccTool; args = [ "-I$out/include" (toString main) "$out/lib/lib${name}.a" "-o" "$out/bin/${name}" ]; }) (eff.builder.runTool { name = "smoke-test"; tool = bashTool; args = [ "-c" smokeScript "smoke-test" ]; }) (eff.builder.writeFile { output = pkgConfigOutput; text = packageConfig; }) (eff.builder.emitDescriptor { descriptor = ops.descriptor { name = "${name}-metadata"; payload = { kind = "c-codegen"; inherit artifactKind compiler configDefines; generated = [ "include/generated_messages.h" "generated/generated_messages.c" "lib/lib${name}.a" "bin/${name}" ]; }; }; }) (eff.builder.transformOutput { output = cliOutput; }) (eff.builder.transformOutput { output = libraryOutput; }) (eff.builder.transformOutput { output = headerOutput; }) (eff.builder.transformOutput { output = pkgConfigOutput; }) (eff.builder.materializeDerivation { name = "${name}-artifact"; builder = "runCommand"; }) ]; in { _con = "MetaBuilderSpec"; inherit name compiler schema configDefines artifactKind operations; parameters = [ (ops.parameter { name = "artifactKind"; value = artifactKind; }) ]; inputs = [ schemaSource mainSource ]; dependencies = [ ]; tools = [ bashTool gccTool arTool ]; outputs = [ cliOutput libraryOutput headerOutput pkgConfigOutput ]; evidence = [ (ops.evidence { name = "smoke-test"; payload = { command = "$out/bin/${name}"; expectedOutput = "hello from generated C"; }; }) ]; }; spec = cCodegen { name = "messages-demo"; schema = ./messages.def; main = ./main.c; }; program = mb.program.fromOrnamentedSpec CCodegenBuilder.T spec; shellScript = mb.program.backends.shell.run program; value = { builder = { inherit CCodegenBuilder cCodegen; descriptor = G.derive.deriveDescriptor CCodegenBuilder; schema = G.derive.deriveSchema CCodegenBuilder; }; inherit spec program; validation = mb.program.validate.run program; deps = mb.program.deps.run program; dryRun = mb.program."dry-run".run program; planView = mb.program."plan-view".run program; docs = mb.program.describe.run program; selfView = mb.program.introspect.run program; materialize = mb.program.materialize.run program; materializeShell = shellScript; materializeShellCheck = mb.program.backends.shell.shellcheckFor shellScript; # node-service is excluded: its launcher embeds /nix/store paths. materializeShellEquality = mb.program.backends.shell.executionCheckFor program; materializeDockerfile = mb.program.backends.dockerfile.run program; planExport = mb.program."plan-export".json program; }; in { scope = { inherit CCodegenBuilder cCodegen spec program value; }; } ``` ### messages.def This schema is the generator input. The build plan reads each `key:value` row and emits declarations plus C functions returning the configured text. Source path: [`examples/c-codegen/messages.def`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/c-codegen/messages.def). ```text hello:hello from generated C health:ok ``` ### main.c This hand-written CLI proves the generated header and static library can be consumed by ordinary C code. Source path: [`examples/c-codegen/main.c`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/c-codegen/main.c). ```c #include #include "config.h" #include "generated_messages.h" int main(void) { printf("%s\n", message_hello()); return DEMO_FEATURE ? 0 : 1; } ``` ### 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. ### Source files These files are the complete source for Bridge example: the builder module plus the fixtures it consumes. - [Bridge proof module](/metaBuilder/examples/bridge/source/bridge.nix) - Source for the kernel-checked bridge theorem set. ### Bridge proof module This module checks the bridge theorems and exposes their normal forms. Source path: [`examples/bridge.nix`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/bridge.nix). ```nix { lib, self, mb, fx, ... }: let H = fx.types.hoas; V = fx.types.generic.value; G = fx.types.generic; v = fx.types.verified; E = fx.tc.eval; C = fx.tc.conv; node = self.node-service.value; c = self.c-codegen.value; oci = self."oci-image".value; idl = self.idl.value; NodeBuilder = node.builder.NodeServiceBuilder; CBuilder = c.builder.CCodegenBuilder; OciBuilder = oci.builder.OciImageBuilder; IdlBuilder = idl.builder.IdlBuilder; CodeGenBuilder = mb.ornaments."code-gen".CodeGenBuilder; BuilderSpec = mb.descriptions.BuilderSpec; nodeSpecH = V.review NodeBuilder.T node.spec; cSpecH = V.review CBuilder.T c.spec; ociSpecH = V.review OciBuilder.T oci.spec; idlSpecH = V.review IdlBuilder.T idl.spec; nodeBaseSpec = G.ornaments.forget NodeBuilder node.spec; cBaseSpec = G.ornaments.forget CBuilder c.spec; ociBaseSpec = G.ornaments.forget OciBuilder oci.spec; nodeBaseSpecH = V.review BuilderSpec.T nodeBaseSpec; cBaseSpecH = V.review BuilderSpec.T cBaseSpec; ociBaseSpecH = V.review BuilderSpec.T ociBaseSpec; # IdlBuilder ornaments CodeGenBuilder, which ornaments BuilderSpec, so # reaching the common base takes two forget steps. idlCgSpec = G.ornaments.forget IdlBuilder idl.spec; idlBaseSpec = G.ornaments.forget CodeGenBuilder idlCgSpec; idlCgSpecH = V.review CodeGenBuilder.T idlCgSpec; idlBaseSpecH = V.review BuilderSpec.T idlBaseSpec; # forget keeps `operations` and `evidence` — everything compileSpec # reads — so compiling the forgotten base spec rebuilds the same # program as the ornamented spec: compilation factors through forget. nodeBaseProgram = mb.program.fromSpec nodeBaseSpec; cBaseProgram = mb.program.fromSpec cBaseSpec; ociBaseProgram = mb.program.fromSpec ociBaseSpec; idlBaseProgram = mb.program.fromSpec idlBaseSpec; # The compiled effect lists (operations + lowered evidence): the same # input the live interpreters fold, so the kernel fold and the drift # check exercise every constructor the live path sees. nodeCompiledOps = mb.program.compileSpec BuilderSpec.T nodeBaseSpec; cCompiledOps = mb.program.compileSpec BuilderSpec.T cBaseSpec; ociCompiledOps = mb.program.compileSpec BuilderSpec.T ociBaseSpec; idlCompiledOps = mb.program.compileSpec BuilderSpec.T idlBaseSpec; # The canonical program for each example, recomputed from its spec. nodeFromSpec = mb.program.fromOrnamentedSpec NodeBuilder.T node.spec; cFromSpec = mb.program.fromOrnamentedSpec CBuilder.T c.spec; ociFromSpec = mb.program.fromOrnamentedSpec OciBuilder.T oci.spec; idlFromSpec = mb.program.fromOrnamentedSpec IdlBuilder.T idl.spec; evalHoas = term: E.eval [ ] (H.elab term); phrase = text: math: { inherit text math; }; term = text: math: value: { inherit text math value; }; # heavy: the check normalizes large concrete terms (minutes of kernel # evaluation); its test lands in the heavy suite instead of the default. kernelCheck = { name, statement, type, proof, heavy ? false }: let result = H.checkHoas type.value proof.value; in { inherit name heavy; statement = statement.text; statementMath = statement.math; type = type.text; typeMath = type.math; proof = proof.text; proofMath = proof.math; kind = "kernel-check"; ok = !(result ? error); resultTag = result.tag or "error"; # Lazy: reading statement fields must not force the kernel check. error = result.error or null; }; kernelConversion = { name, statement, type, proof, lhs, rhs }: let ok = C.conv 0 (evalHoas lhs) (evalHoas rhs); in { inherit name ok; statement = statement.text; statementMath = statement.math; type = type.text; typeMath = type.math; proof = proof.text; proofMath = proof.math; kind = "kernel-conversion"; resultTag = if ok then "definitional-equality" else "mismatch"; }; builderEffSum = H.sum mb.descriptions.BuilderOp.T mb.descriptions.RuntimeOp.T; noError = result: !(result ? error); # The renderer ρ : BuildPlanStep → String as a kernel term. opaqueLam carries # the live renderStep as an unverified trust boundary; String is axiomatised so # ρ never reduces. Structural step-fold coherence only needs both folds to apply # this same ρ, so the renderer body stays opaque. rhoTy = H.forall "_" mb.descriptions.BuildPlanStep.T (_: H.string); rho = H.opaqueLam mb.program.materialize.renderStep rhoTy; rhoCheck = let typeChecks = noError (H.checkHoas rhoTy rho); in { inherit typeChecks; ok = typeChecks; }; # `mb.descriptions.BuildPlanStep.T` is the kernel step carrier directly # (descriptions.nix). Steps are born finalized: runStep's tool is # FinalizedToolSpec (all-string fields). The remaining opaque leaves — # SourceSpec.T's `any`, env's `attrs` — are axiomatised kernel primitives, # so the structural step-fold threads eliminator-bound payloads through it # with no fabricated literals. This gate confirms the carrier forms and its # emitting constructors inhabit with payloads threaded as bound variables # (exactly matFoldK's usage), and the param-instantiated # `args : listOf string` field checks. planStep = let BPS = mb.descriptions.BuildPlanStep; FinalizedToolSpec = mb.descriptions.FinalizedToolSpec; SourceSpec = mb.descriptions.SourceSpec; app3 = f: a: b: c: H.app (H.app (H.app f a) b) c; app4 = f: a: b: c: d: H.app (H.app (H.app (H.app f a) b) c) d; typeForms = noError (H.checkHoas (H.u 0) BPS.T); # The threading case matFoldK's runTool branch produces: name/tool/args/env # all arrive as bound variables at the constructor's field types. runThreadTy = H.forall "name" H.string (_: H.forall "tool" FinalizedToolSpec.T (_: H.forall "args" (H.listOf H.string) (_: H.forall "env" H.attrs (_: BPS.T)))); runThreadTm = H.lam "name" H.string (name: H.lam "tool" FinalizedToolSpec.T (tool: H.lam "args" (H.listOf H.string) (args: H.lam "env" H.attrs (env: app4 BPS.runStep name tool args env)))); runStepThreads = noError (H.checkHoas runThreadTy runThreadTm); # The param-instantiated literal: args built as a `cons` literal checked # against `listOf string` (the ann-strip target), tool/env threaded as vars. runLitTy = H.forall "tool" FinalizedToolSpec.T (_: H.forall "env" H.attrs (_: BPS.T)); runLitTm = H.lam "tool" FinalizedToolSpec.T (tool: H.lam "env" H.attrs (env: app4 BPS.runStep (H.stringLit "n") tool (H.cons (H.stringLit "a") H.nil) env)); runStepLitArgs = noError (H.checkHoas runLitTy runLitTm); writeStepInhabits = noError (H.checkHoas BPS.T (app3 BPS.writeStep (H.stringLit "w") (H.stringLit "/out/f") (H.stringLit "txt"))); # copyStep threads source : SourceSpec.T as a bound variable. copyTy = H.forall "source" SourceSpec.T (_: BPS.T); copyTm = H.lam "source" SourceSpec.T (source: app3 BPS.copyStep (H.stringLit "c") source (H.stringLit "/out/d")); copyStepThreads = noError (H.checkHoas copyTy copyTm); in { inherit typeForms runStepThreads runStepLitArgs writeStepInhabits copyStepThreads; ok = typeForms && runStepThreads && runStepLitArgs && writeStepInhabits && copyStepThreads; }; # matFoldK : listOf BuilderEff → listOf BuildPlanStep — the kernel # internalisation of materialize's step emission. v.matchSum splits the # sum-injected ops; v.matchData runs the per-op BuilderOp/RuntimeOp # eliminators, consing each emitted step into the fold accumulator. matFold = let BPS = mb.descriptions.BuildPlanStep; BOp = mb.descriptions.BuilderOp; ROp = mb.descriptions.RuntimeOp; OutputSpec = mb.descriptions.OutputSpec; ToolSpec = mb.descriptions.ToolSpec; FinalizedToolSpec = mb.descriptions.FinalizedToolSpec; stepsTy = H.listOf BPS.T; app2 = f: a: b: H.app (H.app f a) b; app3 = f: a: b: c: H.app (H.app (H.app f a) b) c; app4 = f: a: b: c: d: H.app (H.app (H.app (H.app f a) b) c) d; outName = output: v.field OutputSpec.T "name" output; outPath = output: v.field OutputSpec.T "path" output; # materialize finalizes the tool at emission (finalizeTool : ToolSpec → # FinalizedToolSpec); its package projection forces a live derivation — # a trust boundary the kernel cannot compute. The internalised emitter # threads the ρ-visible `name` through both string fields; `package` is # trust-boundary payload, reattached from the live step at the render # comparison (renderableStep). finalizeK = H.ann (H.lam "tool" ToolSpec.T (tool: app2 FinalizedToolSpec.MetaBuilderFinalizedTool (v.field ToolSpec.T "name" tool) (v.field ToolSpec.T "name" tool))) (H.forall "_" ToolSpec.T (_: FinalizedToolSpec.T)); # Per-op emitter, fold-fused: each branch conses its step into `ih` # or passes `ih` through. matchData ann-wraps every body at stepsTy. matStepF = op: ih: v.matchSum BOp.T ROp.T stepsTy op { left = bop: v.matchData BOp stepsTy bop { readSource = name: source: ih; resolveDependency = dependency: ih; declareTool = tool: ih; runTool = name: tool: args: env: H.cons (app4 BPS.runStep name (H.app finalizeK tool) args env) ih; writeFile = output: text: H.cons (app3 BPS.writeStep (outName output) (outPath output) text) ih; copyPath = source: output: H.cons (app3 BPS.copyStep (outName output) source (outPath output)) ih; transformOutput = output: ih; validateValue = validation: ih; emitDescriptor = descriptor: ih; materializeDerivation = name: builder: ih; declareEvidence = evidence: ih; }; right = rop: v.matchData ROp stepsTy rop { declareCapability = category: ih; declareProtocol = protocol: ih; declareService = service: ih; materializeUnit = name: ih; }; }; foldTy = H.forall "_" (H.listOf builderEffSum) (_: stepsTy); matFoldK = H.ann (H.lam "p" (H.listOf builderEffSum) (p: v.fold builderEffSum stepsTy H.nil (H.lam "op" builderEffSum (op: H.lam "ih" stepsTy (ih: matStepF op ih))) p)) foldTy; nodeOpsH = V.review (H.listOf builderEffSum) nodeCompiledOps; cOpsH = V.review (H.listOf builderEffSum) cCompiledOps; # The catamorphism across the Pi extraction boundary: a Nix function # that elaborates its argument (raw operations, no prior review), # runs the verified closure, and extracts the step list back. matFoldX = fx.tc.elaborate.verifyAndExtract foldTy matFoldK; # Tag projection: the ρ-invisible structural skeleton of a step list. # The two interpreters differ on payloads (materialize synthesises a # name dry-run drops), so the honest agreement is at the tag level. StepTag = H.datatype "MetaBuilderStepTag" [ (H.con "RunT" [ ]) (H.con "WriteT" [ ]) (H.con "CopyT" [ ]) (H.con "MkdirT" [ ]) ]; tagsTy = H.listOf StepTag.T; # tagOf : BuildPlanStep → StepTag. tagOf = H.lam "s" BPS.T (s: v.matchData BPS StepTag.T s { runStep = name: tool: args: env: StepTag.RunT; writeStep = name: path: text: StepTag.WriteT; copyStep = name: source: path: StepTag.CopyT; mkdirStep = path: StepTag.MkdirT; }); tagFoldTy = H.forall "_" (H.listOf builderEffSum) (_: tagsTy); # matTagFoldK = tagSeq ∘ matFoldK — the tag projection of the real # step catamorphism (mapped over its output, no refold). matTagFoldK = H.ann (H.lam "p" (H.listOf builderEffSum) (p: v.map BPS.T StepTag.T tagOf (H.app matFoldK p))) tagFoldTy; # dryTagFoldK internalises dry-run's tag-all + the dryRunStepCons # filter+rename to {run,write,copy}: a fold-fused emitter consing one # tag per emitting op, passing ih through otherwise. dryTagStepF = op: ih: v.matchSum BOp.T ROp.T tagsTy op { left = bop: v.matchData BOp tagsTy bop { readSource = name: source: ih; resolveDependency = dependency: ih; declareTool = tool: ih; runTool = name: tool: args: env: H.cons StepTag.RunT ih; writeFile = output: text: H.cons StepTag.WriteT ih; copyPath = source: output: H.cons StepTag.CopyT ih; transformOutput = output: ih; validateValue = validation: ih; emitDescriptor = descriptor: ih; materializeDerivation = name: builder: ih; declareEvidence = evidence: ih; }; right = rop: v.matchData ROp tagsTy rop { declareCapability = category: ih; declareProtocol = protocol: ih; declareService = service: ih; materializeUnit = name: ih; }; }; dryTagFoldK = H.ann (H.lam "p" (H.listOf builderEffSum) (p: v.fold builderEffSum tagsTy H.nil (H.lam "op" builderEffSum (op: H.lam "ih" tagsTy (ih: dryTagStepF op ih))) p)) tagFoldTy; tagConName = builtins.listToAttrs (lib.imap0 (i: c: { name = "con${toString i}"; value = c.name; }) (fx.tc.generic.datatype.datatypeInfo StepTag).constructors); extractTags = foldK: ops: map (s: tagConName.${s._con}) (fx.tc.elaborate.verifyAndExtract tagsTy (H.app foldK ops)); matTagCons = extractTags matTagFoldK; dryTagCons = extractTags dryTagFoldK; # ∀p structural agreement of the two tag folds, proved in the kernel: # map/fold fusion by induction on p. Under the induction binder the # cons head is neutral, so each step case-splits it (sumElim, then # elimData on the op payload) to expose a canonical constructor and # let ι-reduction fire through both folds. Emitting ops discharge by # J-congruence on the tag cons; the others pass the induction # hypothesis through unchanged; nil is refl. # # Construction constraints (each load-bearing): # - The folds are let_-bound once and every motive references the # bound variables: eliminator wrappers ann-wrap each branch body # against a meta-level copy of the motive, so embedding the fold # terms directly multiplies them per branch and exhausts memory. # - The congruence step is a raw J with the function application # already reduced in the motive; H.cong's motive embeds an # unannotated meta-lam that does not elaborate in this position. # - cons literals are ann'd: polymorphic-constructor implicits do # not solve in type position. # - Injections use the explicit forms at levelZero to match sumElim's # internal construction (opt-in internal surface). inlOp = b: H._internal._indexed.inlAtExplicit H.levelZero BOp.T ROp.T b; inrOp = r: H._internal._indexed.inrAtExplicit H.levelZero BOp.T ROp.T r; consEff = h: t: H.ann (H.cons h t) (H.listOf builderEffSum); consTags = h: t: H.ann (H.cons h t) tagsTy; agreeAtF = matF: dryF: q: H.eq tagsTy (H.app matF q) (H.app dryF q); stepCongF = matF: dryF: t: ih: tag: H.j tagsTy (H.app matF t) (H.lam "w" tagsTy (w: H.lam "_p" (H.eq tagsTy (H.app matF t) w) (_: H.eq tagsTy (consTags tag (H.app matF t)) (consTags tag w)))) H.refl (H.app dryF t) ih; elimBopF = matF: dryF: t: ih: bop: v.elimData 0 BOp (H.lam "b" BOp.T (b: agreeAtF matF dryF (consEff (inlOp b) t))) bop { readSource = name: source: ih; resolveDependency = dependency: ih; declareTool = tool: ih; runTool = name: tool: args: env: stepCongF matF dryF t ih StepTag.RunT; writeFile = output: text: stepCongF matF dryF t ih StepTag.WriteT; copyPath = source: output: stepCongF matF dryF t ih StepTag.CopyT; transformOutput = output: ih; validateValue = validation: ih; emitDescriptor = descriptor: ih; materializeDerivation = name: builder: ih; declareEvidence = evidence: ih; }; elimRopF = matF: dryF: t: ih: rop: v.elimData 0 ROp (H.lam "r" ROp.T (r: agreeAtF matF dryF (consEff (inrOp r) t))) rop { declareCapability = category: ih; declareProtocol = protocol: ih; declareService = service: ih; materializeUnit = name: ih; }; sumSplitF = matF: dryF: t: ih: h: H.sumElim 0 BOp.T ROp.T (H.lam "hh" builderEffSum (hh: agreeAtF matF dryF (consEff hh t))) (H.lam "bop" BOp.T (bop: elimBopF matF dryF t ih bop)) (H.lam "rop" ROp.T (rop: elimRopF matF dryF t ih rop)) h; tagAgreeTy = H.forall "p" (H.listOf builderEffSum) (p: H.eq tagsTy (H.app matTagFoldK p) (H.app dryTagFoldK p)); tagAgreeProof = H.let_ "matF" tagFoldTy matTagFoldK (matF: H.let_ "dryF" tagFoldTy dryTagFoldK (dryF: H.lam "p" (H.listOf builderEffSum) (p: H.listElim 0 builderEffSum (H.lam "q" (H.listOf builderEffSum) (q: agreeAtF matF dryF q)) H.refl (H.lam "h" builderEffSum (h: H.lam "t" (H.listOf builderEffSum) (t: H.lam "ih" (agreeAtF matF dryF t) (ih: sumSplitF matF dryF t ih h)))) p))); in { inherit matFoldK foldTy nodeOpsH cOpsH matFoldX; inherit StepTag tagFoldTy matTagFoldK dryTagFoldK matTagCons dryTagCons; inherit tagAgreeTy tagAgreeProof; typeChecks = noError (H.checkHoas foldTy matFoldK); }; # ρ across the extraction boundary: the opaque lambda gives back the # Nix function it carries — the live renderer itself. Rendering both # sides of the drift check through rhoX keeps the renderer single. rhoX = fx.tc.elaborate.verifyAndExtract rhoTy rho; # Extracted datatype values are positionally named (con / _field); # rename through datatype metadata to declared constructor/field names. # Field values stay lazy, so opaque payloads are renamed without force. renameByDatatype = dt: s: let ctors = (fx.tc.generic.datatype.datatypeInfo dt).constructors; byCon = builtins.listToAttrs (lib.imap0 (i: ctor: { name = "con${toString i}"; value = ctor; }) ctors); ctor = byCon.${s._con}; in { _con = ctor.name; } // builtins.listToAttrs (lib.imap0 (i: f: { name = f.name; value = s."_field${toString i}"; }) ctor.fields); # Rebuild a renderable step from an extracted one. env (attrs) and the # source payload are axiomatised-opaque in the kernel — extraction cannot # carry them, so they reattach from the live step (the designed trust # boundary). Every ρ-visible representable field (tool.name, args, path, # text) comes from the extracted step. renderableStep = live: s: let named = renameByDatatype mb.descriptions.BuildPlanStep s; in if named._con == "runStep" then named // { tool = renameByDatatype mb.descriptions.FinalizedToolSpec named.tool; env = live.env; } else if named._con == "copyStep" then named // { source = live.source; } else named; extractedNodeSteps = matFold.matFoldX nodeCompiledOps; extractedCSteps = matFold.matFoldX cCompiledOps; extractedOciSteps = matFold.matFoldX ociCompiledOps; extractedIdlSteps = matFold.matFoldX idlCompiledOps; extractedStepCons = map (s: (renameByDatatype mb.descriptions.BuildPlanStep s)._con); # The extraction drift-check: matFoldK crosses the Pi extraction boundary # as a runnable Nix function, consumes the live operations directly, and # must reproduce live materialize — same constructor sequence (which pins # the length, so the zipped render comparison cannot truncate away extra # steps) and same rendered commands through ρ. Both sides render through # rhoX, and rhoIsLiveRenderer pins rhoX to the live renderer, so renderer # drift is excluded; what remains is genuine fold drift. Step names are # ρ-invisible and differ by design; env/source reattach (renderableStep). # # Coverage split: the constructor-sequence facets cover all four shipped # examples; the rendered-command facets apply only to node and c, the # examples that render shells. extractionCheck = let renderLive = map mb.program.materialize.renderStep; renderX = xs: lives: lib.zipListsWith (s: live: rhoX (renderableStep live s)) xs lives; checks = { nodeNonEmpty = builtins.length extractedNodeSteps > 0; ociNonEmpty = builtins.length extractedOciSteps > 0; idlNonEmpty = builtins.length extractedIdlSteps > 0; hasRunStep = builtins.elem "runStep" (extractedStepCons (extractedNodeSteps ++ extractedCSteps)); nodeCons = extractedStepCons extractedNodeSteps == materializeStepCons node.materialize; cCons = extractedStepCons extractedCSteps == materializeStepCons c.materialize; ociCons = extractedStepCons extractedOciSteps == materializeStepCons oci.materialize; idlCons = extractedStepCons extractedIdlSteps == materializeStepCons idl.materialize; nodeRender = renderX extractedNodeSteps node.materialize.plan.steps == renderLive node.materialize.plan.steps; cRender = renderX extractedCSteps c.materialize.plan.steps == renderLive c.materialize.plan.steps; rhoIsLiveRenderer = let s = builtins.head node.materialize.plan.steps; in rhoX s == mb.program.materialize.renderStep s; }; in checks // { ok = builtins.all (n: checks.${n}) (builtins.attrNames checks); }; nodeTools = map (tool: tool.name) node.spec.tools; cTools = map (tool: tool.name) c.spec.tools; sharedTools = lib.intersectLists nodeTools cTools; nodeOutputs = map (output: output.format) node.spec.outputs; cOutputs = map (output: output.format) c.spec.outputs; sharedOutputFormats = lib.intersectLists nodeOutputs cOutputs; stringList = H.listOf H.string; nodeToolsH = V.review stringList nodeTools; cToolsH = V.review stringList cTools; sharedToolsH = V.review stringList sharedTools; nodeOutputsH = V.review stringList nodeOutputs; cOutputsH = V.review stringList cOutputs; sharedOutputFormatsH = V.review stringList sharedOutputFormats; intersectByKernel = left: right: v.filter H.string (v.fn "candidate" H.string (candidate: v.strElem candidate right)) left; builderSpecFields = map (field: field.name) ((builtins.head (G.derive.deriveDescriptor BuilderSpec).constructors).fields); # dry-run tags every op; materialize records a step only for # runTool/writeFile/copyPath. Filtering dry-run to those kinds and renaming # reproduces materialize's step constructors in order. stepKindToCon = { run = "runStep"; write = "writeStep"; copy = "copyStep"; }; dryRunStepCons = dry: map (s: stepKindToCon.${s.kind}) (builtins.filter (s: stepKindToCon ? ${s.kind}) dry.steps); materializeStepCons = mat: map (s: s._con) mat.plan.steps; stepConToTag = { runStep = "RunT"; writeStep = "WriteT"; copyStep = "CopyT"; mkdirStep = "MkdirT"; }; theoremList = [ (kernelCheck { name = "node-spec-inhabits-node-ornament"; statement = phrase "node.spec : NodeServiceBuilder.T" "\\mathsf{node.spec} : \\mathsf{NodeServiceBuilder.T}"; type = term "NodeServiceBuilder.T" "\\mathsf{NodeServiceBuilder.T}" NodeBuilder.T; proof = term "V.review NodeServiceBuilder.T node.spec" "\\mathsf{review}_{\\mathsf{NodeServiceBuilder.T}}(\\mathsf{node.spec})" nodeSpecH; }) (kernelCheck { name = "c-spec-inhabits-c-ornament"; statement = phrase "c.spec : CCodegenBuilder.T" "\\mathsf{c.spec} : \\mathsf{CCodegenBuilder.T}"; type = term "CCodegenBuilder.T" "\\mathsf{CCodegenBuilder.T}" CBuilder.T; proof = term "V.review CCodegenBuilder.T c.spec" "\\mathsf{review}_{\\mathsf{CCodegenBuilder.T}}(\\mathsf{c.spec})" cSpecH; }) (kernelCheck { name = "node-forget-has-builder-spec-codomain"; statement = phrase "forget_Node : NodeServiceBuilder.T -> BuilderSpec.T" "\\mathsf{forget}_{Node} : \\mathsf{NodeServiceBuilder.T} \\to \\mathsf{BuilderSpec.T}"; type = term "Pi(spec : NodeServiceBuilder.T). BuilderSpec.T" "\\Pi(\\mathsf{spec} : \\mathsf{NodeServiceBuilder.T}).\\, \\mathsf{BuilderSpec.T}" (H.forall "spec" NodeBuilder.T (_: BuilderSpec.T)); proof = term "G.ornaments.forgetHoas NodeServiceBuilder" "\\mathsf{forgetHoas}(\\mathsf{NodeServiceBuilder})" (G.ornaments.forgetHoas NodeBuilder); }) (kernelCheck { name = "c-forget-has-builder-spec-codomain"; statement = phrase "forget_C : CCodegenBuilder.T -> BuilderSpec.T" "\\mathsf{forget}_{C} : \\mathsf{CCodegenBuilder.T} \\to \\mathsf{BuilderSpec.T}"; type = term "Pi(spec : CCodegenBuilder.T). BuilderSpec.T" "\\Pi(\\mathsf{spec} : \\mathsf{CCodegenBuilder.T}).\\, \\mathsf{BuilderSpec.T}" (H.forall "spec" CBuilder.T (_: BuilderSpec.T)); proof = term "G.ornaments.forgetHoas CCodegenBuilder" "\\mathsf{forgetHoas}(\\mathsf{CCodegenBuilder})" (G.ornaments.forgetHoas CBuilder); }) (kernelCheck { name = "node-forget-computes-base-builder-spec"; statement = phrase "forget_Node node.spec = node.baseSpec : BuilderSpec.T" "\\mathsf{forget}_{Node}(\\mathsf{node.spec}) = \\mathsf{node.baseSpec} : \\mathsf{BuilderSpec.T}"; type = term "Eq BuilderSpec.T (forget_Node node.spec) node.baseSpec" "\\operatorname{Eq}_{\\mathsf{BuilderSpec.T}}(\\mathsf{forget}_{Node}(\\mathsf{node.spec}), \\mathsf{node.baseSpec})" (H.eq BuilderSpec.T (G.ornaments.forget NodeBuilder nodeSpecH) nodeBaseSpecH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelCheck { name = "c-forget-computes-base-builder-spec"; statement = phrase "forget_C c.spec = c.baseSpec : BuilderSpec.T" "\\mathsf{forget}_{C}(\\mathsf{c.spec}) = \\mathsf{c.baseSpec} : \\mathsf{BuilderSpec.T}"; type = term "Eq BuilderSpec.T (forget_C c.spec) c.baseSpec" "\\operatorname{Eq}_{\\mathsf{BuilderSpec.T}}(\\mathsf{forget}_{C}(\\mathsf{c.spec}), \\mathsf{c.baseSpec})" (H.eq BuilderSpec.T (G.ornaments.forget CBuilder cSpecH) cBaseSpecH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelConversion { name = "node-program-compilation-factors-through-forget"; statement = phrase "node.program = fromSpec (forget_Node node.spec)" "\\mathsf{program}_{Node} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{Node}(\\mathsf{node.spec})\\big)"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Node} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{Node}(\\mathsf{node.spec})\\big)"; proof = phrase "C.conv 0 (evalHoas node.program) (evalHoas (fromSpec (forget_Node node.spec)))" "\\operatorname{conv}\\big(\\mathsf{program}_{Node},\\ \\mathsf{fromSpec}(\\mathsf{forget}_{Node}(\\mathsf{node.spec}))\\big)"; lhs = node.program; rhs = nodeBaseProgram; }) (kernelConversion { name = "c-program-compilation-factors-through-forget"; statement = phrase "c.program = fromSpec (forget_C c.spec)" "\\mathsf{program}_{C} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{C}(\\mathsf{c.spec})\\big)"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{C} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{C}(\\mathsf{c.spec})\\big)"; proof = phrase "C.conv 0 (evalHoas c.program) (evalHoas (fromSpec (forget_C c.spec)))" "\\operatorname{conv}\\big(\\mathsf{program}_{C},\\ \\mathsf{fromSpec}(\\mathsf{forget}_{C}(\\mathsf{c.spec}))\\big)"; lhs = c.program; rhs = cBaseProgram; }) (kernelConversion { name = "node-program-is-from-ornamented-spec-no-bypass"; statement = phrase "node.program = fromOrnamentedSpec NodeServiceBuilder.T node.spec" "\\mathsf{program}_{Node} \\equiv \\mathsf{fromSpec}(\\mathsf{NodeServiceBuilder.T},\\ \\mathsf{node.spec})"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Node} \\equiv \\mathsf{fromSpec}(\\mathsf{NodeServiceBuilder.T},\\ \\mathsf{node.spec})"; proof = phrase "C.conv 0 (evalHoas node.program) (evalHoas (fromOrnamentedSpec NodeServiceBuilder.T node.spec))" "\\operatorname{conv}\\big(\\mathsf{program}_{Node},\\ \\mathsf{fromSpec}(\\mathsf{NodeServiceBuilder.T},\\ \\mathsf{node.spec})\\big)"; lhs = node.program; rhs = nodeFromSpec; }) (kernelConversion { name = "c-program-is-from-ornamented-spec-no-bypass"; statement = phrase "c.program = fromOrnamentedSpec CCodegenBuilder.T c.spec" "\\mathsf{program}_{C} \\equiv \\mathsf{fromSpec}(\\mathsf{CCodegenBuilder.T},\\ \\mathsf{c.spec})"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{C} \\equiv \\mathsf{fromSpec}(\\mathsf{CCodegenBuilder.T},\\ \\mathsf{c.spec})"; proof = phrase "C.conv 0 (evalHoas c.program) (evalHoas (fromOrnamentedSpec CCodegenBuilder.T c.spec))" "\\operatorname{conv}\\big(\\mathsf{program}_{C},\\ \\mathsf{fromSpec}(\\mathsf{CCodegenBuilder.T},\\ \\mathsf{c.spec})\\big)"; lhs = c.program; rhs = cFromSpec; }) (kernelCheck { name = "oci-spec-inhabits-oci-ornament"; statement = phrase "oci.spec : OciImageBuilder.T" "\\mathsf{oci.spec} : \\mathsf{OciImageBuilder.T}"; type = term "OciImageBuilder.T" "\\mathsf{OciImageBuilder.T}" OciBuilder.T; proof = term "V.review OciImageBuilder.T oci.spec" "\\mathsf{review}_{\\mathsf{OciImageBuilder.T}}(\\mathsf{oci.spec})" ociSpecH; }) (kernelCheck { name = "oci-forget-has-builder-spec-codomain"; statement = phrase "forget_Oci : OciImageBuilder.T -> BuilderSpec.T" "\\mathsf{forget}_{Oci} : \\mathsf{OciImageBuilder.T} \\to \\mathsf{BuilderSpec.T}"; type = term "Pi(spec : OciImageBuilder.T). BuilderSpec.T" "\\Pi(\\mathsf{spec} : \\mathsf{OciImageBuilder.T}).\\, \\mathsf{BuilderSpec.T}" (H.forall "spec" OciBuilder.T (_: BuilderSpec.T)); proof = term "G.ornaments.forgetHoas OciImageBuilder" "\\mathsf{forgetHoas}(\\mathsf{OciImageBuilder})" (G.ornaments.forgetHoas OciBuilder); }) (kernelCheck { name = "oci-forget-computes-base-builder-spec"; statement = phrase "forget_Oci oci.spec = oci.baseSpec : BuilderSpec.T" "\\mathsf{forget}_{Oci}(\\mathsf{oci.spec}) = \\mathsf{oci.baseSpec} : \\mathsf{BuilderSpec.T}"; type = term "Eq BuilderSpec.T (forget_Oci oci.spec) oci.baseSpec" "\\operatorname{Eq}_{\\mathsf{BuilderSpec.T}}(\\mathsf{forget}_{Oci}(\\mathsf{oci.spec}), \\mathsf{oci.baseSpec})" (H.eq BuilderSpec.T (G.ornaments.forget OciBuilder ociSpecH) ociBaseSpecH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelConversion { name = "oci-program-compilation-factors-through-forget"; statement = phrase "oci.program = fromSpec (forget_Oci oci.spec)" "\\mathsf{program}_{Oci} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{Oci}(\\mathsf{oci.spec})\\big)"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Oci} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{Oci}(\\mathsf{oci.spec})\\big)"; proof = phrase "C.conv 0 (evalHoas oci.program) (evalHoas (fromSpec (forget_Oci oci.spec)))" "\\operatorname{conv}\\big(\\mathsf{program}_{Oci},\\ \\mathsf{fromSpec}(\\mathsf{forget}_{Oci}(\\mathsf{oci.spec}))\\big)"; lhs = oci.program; rhs = ociBaseProgram; }) (kernelConversion { name = "oci-program-is-from-ornamented-spec-no-bypass"; statement = phrase "oci.program = fromOrnamentedSpec OciImageBuilder.T oci.spec" "\\mathsf{program}_{Oci} \\equiv \\mathsf{fromSpec}(\\mathsf{OciImageBuilder.T},\\ \\mathsf{oci.spec})"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Oci} \\equiv \\mathsf{fromSpec}(\\mathsf{OciImageBuilder.T},\\ \\mathsf{oci.spec})"; proof = phrase "C.conv 0 (evalHoas oci.program) (evalHoas (fromOrnamentedSpec OciImageBuilder.T oci.spec))" "\\operatorname{conv}\\big(\\mathsf{program}_{Oci},\\ \\mathsf{fromSpec}(\\mathsf{OciImageBuilder.T},\\ \\mathsf{oci.spec})\\big)"; lhs = oci.program; rhs = ociFromSpec; }) (kernelCheck { name = "idl-spec-inhabits-idl-ornament"; statement = phrase "idl.spec : IdlBuilder.T" "\\mathsf{idl.spec} : \\mathsf{IdlBuilder.T}"; type = term "IdlBuilder.T" "\\mathsf{IdlBuilder.T}" IdlBuilder.T; proof = term "V.review IdlBuilder.T idl.spec" "\\mathsf{review}_{\\mathsf{IdlBuilder.T}}(\\mathsf{idl.spec})" idlSpecH; }) (kernelCheck { name = "idl-forget-has-code-gen-codomain"; statement = phrase "forget_Idl : IdlBuilder.T -> CodeGenBuilder.T" "\\mathsf{forget}_{Idl} : \\mathsf{IdlBuilder.T} \\to \\mathsf{CodeGenBuilder.T}"; type = term "Pi(spec : IdlBuilder.T). CodeGenBuilder.T" "\\Pi(\\mathsf{spec} : \\mathsf{IdlBuilder.T}).\\, \\mathsf{CodeGenBuilder.T}" (H.forall "spec" IdlBuilder.T (_: CodeGenBuilder.T)); proof = term "G.ornaments.forgetHoas IdlBuilder" "\\mathsf{forgetHoas}(\\mathsf{IdlBuilder})" (G.ornaments.forgetHoas IdlBuilder); }) (kernelCheck { name = "idl-composite-forget-has-builder-spec-codomain"; statement = phrase "forget_CG . forget_Idl : IdlBuilder.T -> BuilderSpec.T" "\\mathsf{forget}_{CG} \\circ \\mathsf{forget}_{Idl} : \\mathsf{IdlBuilder.T} \\to \\mathsf{BuilderSpec.T}"; type = term "Pi(spec : IdlBuilder.T). BuilderSpec.T" "\\Pi(\\mathsf{spec} : \\mathsf{IdlBuilder.T}).\\, \\mathsf{BuilderSpec.T}" (H.forall "spec" IdlBuilder.T (_: BuilderSpec.T)); proof = term "lam spec. forgetHoas CodeGenBuilder (forgetHoas IdlBuilder spec)" "\\lambda \\mathsf{spec}.\\, \\mathsf{forgetHoas}(\\mathsf{CodeGenBuilder})\\,(\\mathsf{forgetHoas}(\\mathsf{IdlBuilder})\\,\\mathsf{spec})" (H.lam "spec" IdlBuilder.T (s: H.app (G.ornaments.forgetHoas CodeGenBuilder) (H.app (G.ornaments.forgetHoas IdlBuilder) s))); }) (kernelCheck { name = "idl-forget-computes-code-gen-spec"; statement = phrase "forget_Idl idl.spec = idl.cgSpec : CodeGenBuilder.T" "\\mathsf{forget}_{Idl}(\\mathsf{idl.spec}) = \\mathsf{idl.cgSpec} : \\mathsf{CodeGenBuilder.T}"; type = term "Eq CodeGenBuilder.T (forget_Idl idl.spec) idl.cgSpec" "\\operatorname{Eq}_{\\mathsf{CodeGenBuilder.T}}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec}), \\mathsf{idl.cgSpec})" (H.eq CodeGenBuilder.T (G.ornaments.forget IdlBuilder idlSpecH) idlCgSpecH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelCheck { name = "idl-forget-computes-base-builder-spec"; statement = phrase "forget_CG (forget_Idl idl.spec) = idl.baseSpec : BuilderSpec.T" "\\mathsf{forget}_{CG}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec})) = \\mathsf{idl.baseSpec} : \\mathsf{BuilderSpec.T}"; type = term "Eq BuilderSpec.T (forget_CG (forget_Idl idl.spec)) idl.baseSpec" "\\operatorname{Eq}_{\\mathsf{BuilderSpec.T}}(\\mathsf{forget}_{CG}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec})), \\mathsf{idl.baseSpec})" (H.eq BuilderSpec.T (G.ornaments.forget CodeGenBuilder (G.ornaments.forget IdlBuilder idlSpecH)) idlBaseSpecH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelConversion { name = "idl-program-compilation-factors-through-forget"; statement = phrase "idl.program = fromSpec (forget_CG (forget_Idl idl.spec))" "\\mathsf{program}_{Idl} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{CG}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec}))\\big)"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Idl} \\equiv \\mathsf{fromSpec}\\big(\\mathsf{forget}_{CG}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec}))\\big)"; proof = phrase "C.conv 0 (evalHoas idl.program) (evalHoas (fromSpec (forget_CG (forget_Idl idl.spec))))" "\\operatorname{conv}\\big(\\mathsf{program}_{Idl},\\ \\mathsf{fromSpec}(\\mathsf{forget}_{CG}(\\mathsf{forget}_{Idl}(\\mathsf{idl.spec})))\\big)"; lhs = idl.program; rhs = idlBaseProgram; }) (kernelConversion { name = "idl-program-is-from-ornamented-spec-no-bypass"; statement = phrase "idl.program = fromOrnamentedSpec IdlBuilder.T idl.spec" "\\mathsf{program}_{Idl} \\equiv \\mathsf{fromSpec}(\\mathsf{IdlBuilder.T},\\ \\mathsf{idl.spec})"; type = phrase "Definitional equality of Free(BuilderEff) programs" "\\mathsf{program}_{Idl} \\equiv \\mathsf{fromSpec}(\\mathsf{IdlBuilder.T},\\ \\mathsf{idl.spec})"; proof = phrase "C.conv 0 (evalHoas idl.program) (evalHoas (fromOrnamentedSpec IdlBuilder.T idl.spec))" "\\operatorname{conv}\\big(\\mathsf{program}_{Idl},\\ \\mathsf{fromSpec}(\\mathsf{IdlBuilder.T},\\ \\mathsf{idl.spec})\\big)"; lhs = idl.program; rhs = idlFromSpec; }) (kernelConversion { name = "builder-effect-language-is-builder-plus-runtime"; statement = phrase "BuilderEff == BuilderOp + RuntimeOp" "\\mathsf{BuilderEff} \\equiv \\mathsf{BuilderOp.T} + \\mathsf{RuntimeOp.T}"; type = phrase "Definitional equality judgment" "\\mathsf{BuilderEff} \\equiv \\mathsf{BuilderOp.T} + \\mathsf{RuntimeOp.T}"; proof = phrase "C.conv 0 (evalHoas mb.program.BuilderEff) (evalHoas (H.sum BuilderOp.T RuntimeOp.T))" "\\operatorname{conv}(\\mathsf{BuilderEff}, \\mathsf{BuilderOp.T} + \\mathsf{RuntimeOp.T})"; lhs = mb.program.BuilderEff; rhs = builderEffSum; }) (kernelCheck { name = "shared-tools-normalize-from-actual-tool-lists"; statement = phrase "filter (member c.tools) node.tools = sharedTools" "\\operatorname{filter}(\\lambda x.\\, x \\in \\mathsf{c.tools})(\\mathsf{node.tools}) = \\mathsf{sharedTools}"; type = term "Eq (List String) (filter (member c.tools) node.tools) sharedTools" "\\operatorname{Eq}_{\\operatorname{List}(\\mathsf{String})}(\\operatorname{filter}(\\lambda x.\\, x \\in \\mathsf{c.tools})(\\mathsf{node.tools}), \\mathsf{sharedTools})" (H.eq stringList (intersectByKernel nodeToolsH cToolsH) sharedToolsH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelCheck { name = "shared-output-formats-normalize-from-actual-output-lists"; statement = phrase "filter (member c.outputFormats) node.outputFormats = sharedOutputFormats" "\\operatorname{filter}(\\lambda x.\\, x \\in \\mathsf{c.outputFormats})(\\mathsf{node.outputFormats}) = \\mathsf{sharedOutputFormats}"; type = term "Eq (List String) (filter (member c.outputFormats) node.outputFormats) sharedOutputFormats" "\\operatorname{Eq}_{\\operatorname{List}(\\mathsf{String})}(\\operatorname{filter}(\\lambda x.\\, x \\in \\mathsf{c.outputFormats})(\\mathsf{node.outputFormats}), \\mathsf{sharedOutputFormats})" (H.eq stringList (intersectByKernel nodeOutputsH cOutputsH) sharedOutputFormatsH); proof = term "H.refl" "\\mathsf{refl}" H.refl; }) (kernelCheck { name = "matfoldk-internalizes-materialize-step-emission"; statement = phrase "matFoldK : listOf BuilderEff → listOf BuildPlanStep" "\\mathsf{matFoldK} : \\operatorname{List}(\\mathsf{BuilderEff}) \\to \\operatorname{List}(\\mathsf{BuildPlanStep})"; type = term "H.forall _ (listOf BuilderEff) (_: listOf BuildPlanStep.T)" "\\Pi(\\_ : \\operatorname{List}(\\mathsf{BuilderEff})).\\, \\operatorname{List}(\\mathsf{BuildPlanStep})" matFold.foldTy; proof = term "v.fold over v.matchSum → v.matchData per-op step emitters" "\\operatorname{fold}(\\operatorname{matchSum}\\,(\\operatorname{matchData}\\,\\mathsf{BuilderOp})\\,(\\operatorname{matchData}\\,\\mathsf{RuntimeOp}))" matFold.matFoldK; }) (kernelCheck { name = "mattagfoldk-projects-step-fold-to-tags"; statement = phrase "matTagFoldK : listOf BuilderEff → listOf StepTag" "\\mathsf{matTagFoldK} : \\operatorname{List}(\\mathsf{BuilderEff}) \\to \\operatorname{List}(\\mathsf{StepTag})"; type = term "H.forall _ (listOf BuilderEff) (_: listOf StepTag.T)" "\\Pi(\\_ : \\operatorname{List}(\\mathsf{BuilderEff})).\\, \\operatorname{List}(\\mathsf{StepTag})" matFold.tagFoldTy; proof = term "v.map tagOf ∘ matFoldK" "\\operatorname{map}\\,\\mathsf{tagOf} \\circ \\mathsf{matFoldK}" matFold.matTagFoldK; }) (kernelCheck { name = "drytagfoldk-internalizes-dryrun-tag-emission"; statement = phrase "dryTagFoldK : listOf BuilderEff → listOf StepTag" "\\mathsf{dryTagFoldK} : \\operatorname{List}(\\mathsf{BuilderEff}) \\to \\operatorname{List}(\\mathsf{StepTag})"; type = term "H.forall _ (listOf BuilderEff) (_: listOf StepTag.T)" "\\Pi(\\_ : \\operatorname{List}(\\mathsf{BuilderEff})).\\, \\operatorname{List}(\\mathsf{StepTag})" matFold.tagFoldTy; proof = term "v.fold over per-op {run,write,copy} tag emitters" "\\operatorname{fold}(\\operatorname{matchSum}\\,(\\operatorname{matchData}\\,\\mathsf{BuilderOp}\\to\\mathsf{StepTag}))" matFold.dryTagFoldK; }) (kernelCheck { name = "mattagfoldk-agrees-with-drytagfoldk-forall-p"; heavy = true; statement = phrase "∀p. matTagFoldK p = dryTagFoldK p : listOf StepTag" "\\forall p.\\ \\mathsf{matTagFoldK}\\,p = \\mathsf{dryTagFoldK}\\,p : \\operatorname{List}(\\mathsf{StepTag})"; type = term "∀p:listOf BuilderEff. Eq (listOf StepTag) (matTagFoldK p) (dryTagFoldK p)" "\\Pi(p:\\operatorname{List}(\\mathsf{BuilderEff})).\\,\\operatorname{Eq}(\\mathsf{matTagFoldK}\\,p,\\ \\mathsf{dryTagFoldK}\\,p)" matFold.tagAgreeTy; proof = term "listElim induction; cons-head case-split; J-congruence on emitting ctors, ih on the rest" "\\mathsf{listElim}\\,(\\mathsf{sumElim}\\,(\\mathsf{elimData}\\,\\mathsf{J}/\\mathsf{ih}))" matFold.tagAgreeProof; }) ]; normalForms = { inherit builderSpecFields sharedTools sharedOutputFormats; node = { name = node.spec.name; baseName = nodeBaseSpec.name; tools = nodeTools; outputFormats = nodeOutputs; baseFields = builtins.attrNames nodeBaseSpec; }; c = { name = c.spec.name; baseName = cBaseSpec.name; tools = cTools; outputFormats = cOutputs; baseFields = builtins.attrNames cBaseSpec; }; }; value = { inherit theoremList normalForms planStep rhoCheck extractionCheck; }; in { scope.bridgeModel = { inherit value; # One test per theorem: streaming results, failures name the theorem. tests = builtins.listToAttrs (map (theorem: { name = "${lib.optionalString (theorem.heavy or false) "heavy-"}bridge-theorem-${theorem.name}"; value = { expr = theorem.ok; expected = true; }; }) theoremList) // { "bridge-base-field-normal-forms-match-builder-spec" = { expr = let expected = builtins.sort builtins.lessThan ([ "_con" ] ++ builderSpecFields); in value.normalForms.node.baseFields == expected && value.normalForms.c.baseFields == expected; expected = true; }; "bridge-shared-tools-are-derived-from-actual-specs" = { expr = value.normalForms.sharedTools == lib.intersectLists nodeTools cTools; expected = true; }; "bridge-shared-output-formats-are-derived-from-actual-specs" = { expr = value.normalForms.sharedOutputFormats == lib.intersectLists nodeOutputs cOutputs; expected = true; }; "bridge-examples-build-operations-without-bypass" = { expr = builtins.all (src: !lib.hasInfix "operations ++" src) [ (builtins.readFile ./node-service/builder.nix) (builtins.readFile ./c-codegen/builder.nix) (builtins.readFile ./oci-image/builder.nix) (builtins.readFile ./idl/builder.nix) ]; expected = true; }; # dry-run is a separately written fold that never calls materialize, so # agreement of their step constructors is genuine cross-interpreter # content a refactor can break. Non-vacuity guards against empty steps. "bridge-dry-run-and-materialize-step-constructors-agree" = { expr = { nodeNonEmpty = builtins.length node.materialize.plan.steps > 0; cNonEmpty = builtins.length c.materialize.plan.steps > 0; nodeCons = dryRunStepCons node.dryRun == materializeStepCons node.materialize; cCons = dryRunStepCons c.dryRun == materializeStepCons c.materialize; }; expected = { nodeNonEmpty = true; cNonEmpty = true; nodeCons = true; cCons = true; }; }; # The tag projection of matFoldK agrees with the dry-run tag fold on # both examples (structural agreement), and both reproduce the tags of # live materialize's emitted step constructors. The kernel theorem # mattagfoldk-agrees-with-drytagfoldk-forall-p proves the agreement # ∀p; this gates the two concrete instances. heavy: each fold # application runs verifyAndExtract (typecheck + kernel normalization) # over a full example op list. "heavy-bridge-matfoldk-tag-fold-agrees-with-dryrun" = { expr = let toTags = mat: map (con: stepConToTag.${con}) (materializeStepCons mat); in { nodeNonEmpty = builtins.length (matFold.matTagCons matFold.nodeOpsH) > 0; nodeAgree = matFold.matTagCons matFold.nodeOpsH == matFold.dryTagCons matFold.nodeOpsH; cAgree = matFold.matTagCons matFold.cOpsH == matFold.dryTagCons matFold.cOpsH; nodeFaithful = matFold.matTagCons matFold.nodeOpsH == toTags node.materialize; cFaithful = matFold.matTagCons matFold.cOpsH == toTags c.materialize; }; expected = { nodeNonEmpty = true; nodeAgree = true; cAgree = true; nodeFaithful = true; cFaithful = true; }; }; # BuildPlanStep.T is the kernel carrier for the structural step-fold, # reused directly from descriptions.nix. This gates that the carrier forms # (BuildPlanStep.T : U0) and that its emitting constructors inhabit with # payloads threaded as eliminator-bound variables — exactly matFoldK's # usage — plus the param-instantiated args : listOf string field. "bridge-buildplanstep-carrier-inhabits-under-threading" = { expr = value.planStep; expected = { typeForms = true; runStepThreads = true; runStepLitArgs = true; writeStepInhabits = true; copyStepThreads = true; ok = true; }; }; # ρ is the renderer the coherence theorem applies to both step-folds. It # wraps the live renderStep as an opaque kernel lambda; this gates that it # checks against its declared type BuildPlanStep → String. "bridge-rho-renderer-typechecks-against-buildplanstep-to-string" = { expr = value.rhoCheck; expected = { typeChecks = true; ok = true; }; }; } # One test per extraction drift-check facet; see extractionCheck. // builtins.listToAttrs (map (facet: { name = "bridge-extraction-${facet}"; value = { expr = value.extractionCheck.${facet}; expected = true; }; }) [ "nodeNonEmpty" "ociNonEmpty" "idlNonEmpty" "hasRunStep" "nodeCons" "cCons" "ociCons" "idlCons" "nodeRender" "cRender" "rhoIsLiveRenderer" ]); }; } ``` ### IDL example This tour shows the built-in IDL ornament. It starts from a protobuf-style builder spec and asks for generated outputs in two languages. The example is smaller than the Node and C tours because the builder vocabulary already lives in `mb.ornaments.idl`; the useful part is seeing how that ornament still produces the same internalized program views. ## Start from the artifact The IDL builder describes a generated artifact named `example-idl-generated`. The spec declares protobuf as the IDL format and asks for C++ and Java outputs. Materialization records both output trees in the build plan. ## Source files These pages are the complete source for the worked example: the builder module plus the files it consumes. - [IDL builder module](/metaBuilder/examples/idl/source/builder.nix) - Source for the built-in IDL ornament demo and its worked program. - [schema.proto](/metaBuilder/examples/idl/source/schema.proto) - Small protobuf schema fixture consumed by the IDL demo. ## Builder vocabulary `mb.ornaments.idl.fromProtobuf` is the public constructor. It produces an `IdlBuilder` value with IDL format, proto sources, language targets, generated outputs, and tool-backed operations. ```nix mb.ornaments.idl.fromProtobuf { name = "example-idl"; protos = [ ./idl/schema.proto ]; languages = [ "cpp" "java" ]; } ``` ## Program walkthrough The ornament lowers the IDL spec into a program that declares the protobuf tool, runs one generation step per language, and materializes the generated output tree. The same program can be validated, rendered as a dry-run, shown as a shell plan, documented, and materialized. ## One build, many views The section below is generated from `mb.program.introspect.run program`. It shows the same interpretation surface as the greenfield examples, but for a built-in ornament. The same internalized program is interpreted several ways. ### Validation - result: `ok` ### Dependency Graph - nodes: `3` - edges: `2` - services: `0` - node `tool:protoc` (tool) package `protobuf` - node `operation:protoc-cpp-schema.proto` (operation) via `protoc` - node `operation:protoc-java-schema.proto` (operation) via `protoc` - edge `tool:protoc` -> `operation:protoc-cpp-schema.proto` (uses-tool) - edge `tool:protoc` -> `operation:protoc-java-schema.proto` (uses-tool) ### Dry Run - Builder - source `schema.proto` - tool `protoc` - run `protoc-cpp-schema.proto` with `protoc` - run `protoc-java-schema.proto` with `protoc` - transform `cpp` (tree) - transform `java` (tree) - descriptor `example-idl-idl` - materialize `example-idl-generated` with `runCommand` ### Dry Run - Runtime None. ### Plan View - run `protoc-cpp-schema.proto` - run `protoc-java-schema.proto` - `protoc-cpp-schema.proto`: `protoc '--cpp_out='"$out"/cpp "$pathMap_57a673735cdae15dcb45e8e52911d34adcbe149b4a6d67b6eea62b6804511ed4"` - `protoc-java-schema.proto`: `protoc '--java_out='"$out"/java "$pathMap_57a673735cdae15dcb45e8e52911d34adcbe149b4a6d67b6eea62b6804511ed4"` ### Plan Shell Excerpt ```sh pathMap_57a673735cdae15dcb45e8e52911d34adcbe149b4a6d67b6eea62b6804511ed4= protoc '--cpp_out='"$out"/cpp "$pathMap_57a673735cdae15dcb45e8e52911d34adcbe149b4a6d67b6eea62b6804511ed4" protoc '--java_out='"$out"/java "$pathMap_57a673735cdae15dcb45e8e52911d34adcbe149b4a6d67b6eea62b6804511ed4" ``` ### Runtime Services None. ### Descriptors - descriptor `example-idl-idl` (payload keys `format`, `kind`, `languages`, `sources`) ### Builder Self-Documentation - documented operations: `8` - runtime services: `0` ### Materialized Outputs - cpp -> $out/cpp (tree) - java -> $out/java (tree) ### Materialization - derivation: `example-idl-generated` - outputs: `2` - runtime artifacts: `0` ### Substrates - dockerfile: `supported` - shell: `supported` ### Source files These files are the complete source for IDL example: the builder module plus the fixtures it consumes. - [IDL builder module](/metaBuilder/examples/idl/source/builder.nix) - Source for the built-in IDL ornament demo and its worked program. - [schema.proto](/metaBuilder/examples/idl/source/schema.proto) - Small protobuf schema fixture consumed by the IDL demo. ### IDL builder module This module constructs the `example-idl` spec with `mb.ornaments.idl.fromProtobuf`, then exposes the same interpreter views used by the tour page. Source path: [`examples/idl/builder.nix`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/idl/builder.nix). ```nix { mb, ... }: let idl = mb.ornaments.idl; spec = idl.fromProtobuf { name = "example-idl"; protos = [ ./schema.proto ]; languages = [ "cpp" "java" ]; }; program = mb.program.fromOrnamentedSpec idl.IdlBuilder.T spec; value = { builder = { inherit (idl) IdlBuilder fromProtobuf descriptor schema; }; inherit spec program; # Verdict only: the validated program value is already in scope. validation = { inherit (mb.program.validate.run program) ok diagnostics; }; deps = mb.program.deps.run program; dryRun = mb.program."dry-run".run program; planView = mb.program."plan-view".run program; docs = mb.program.describe.run program; selfView = mb.program.introspect.run program; materialize = mb.program.materialize.run program; schemas = mb.reference.schemas; datatypes = mb.reference.datatypes; }; in { scope = { inherit spec program value; }; } ``` ### schema.proto This schema is the source artifact consumed by the IDL builder. The builder asks for C++ and Java generated views from the same input. Source path: [`examples/idl/schema.proto`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/idl/schema.proto). ```protobuf syntax = "proto3"; package metabuilder.example; message Greeting { string text = 1; string language = 2; } service GreetingService { rpc SayHello (Greeting) returns (Greeting); } ``` ### OCI image example This tour builds a runnable OCI image layout from one static busybox layer. The builder vocabulary lives in the `oci-image` ornament; this example only supplies the image fields and shows the resulting views. The worked artifact is a spec-conformant OCI layout (`oci-layout`, `index.json`, `blobs/sha256/*`) plus an `image.oci.tar` archive of the layout, all assembled at build time with the digests computed in the build sandbox. ## Start from the artifact The payload is `pkgsStatic.busybox` — a single musl-static layer with no runtime closure. The build produces: - `oci-layout` and `index.json`, the layout entry points. - `blobs/sha256/` for the layer tar, the image config, and the manifest — each blob named by its own sha256. - `image.oci.tar`, a deterministic tar of the layout for transports that want a single file. ## Source files These pages are the complete source for the worked example: the builder module plus the files it consumes. - [OCI image example module](/metaBuilder/examples/oci-image/source/builder.nix) - Source for the worked busybox image spec and the exported views. ## Builder vocabulary `OciImageBuilder` ornaments the generic `BuilderSpec` with the image fields (layers, entrypoint, cmd, env, exposedPorts, labels, architecture, os). The `ociImage` constructor compiles those fields into the assembly program, so the example stays at the domain surface. ```nix ociImage { name = "busybox-shell"; layers = [ { name = "busybox"; source = pkgs.pkgsStatic.busybox; } ]; entrypoint = [ "/bin/sh" ]; } ``` ## Program walkthrough The constructor lowers the image spec into named steps in digest-chain order: assemble the layer rootfs, tar it deterministically, render the config (embedding layer diff_ids), render the manifest (embedding config and layer digests and sizes), write the index last, re-hash every blob against its filename, clean the scratch directory, and archive the layout. Because the steps are data, every fold renders them by name: dependency analysis, dry-run, plan-view, and self-documentation all show the same assembly. The smoke-test evidence travels with the spec and renders under the documentation's Evidence section. ## One build, many views The section below is generated from `mb.program.introspect.run program`. It is the internalized view of the image build: validation, dependency graph, dry-run, plan-view, descriptors, outputs, and materialization. The same internalized program is interpreted several ways. ### Validation - result: `ok` ### Dependency Graph - nodes: `11` - edges: `8` - services: `0` - node `tool:bash` (tool) package `bash-interactive` - node `tool:tar` (tool) package `gnutar` - node `tool:coreutils` (tool) package `coreutils` - node `operation:assemble-rootfs-busybox` (operation) via `bash` - node `operation:tar-layer-busybox` (operation) via `bash` - node `operation:write-config` (operation) via `bash` - node `operation:write-manifest` (operation) via `bash` - node `operation:write-index` (operation) via `bash` - node `operation:verify-blobs` (operation) via `bash` - node `operation:clean-scratch` (operation) via `bash` - node `operation:archive-layout` (operation) via `bash` - edge `tool:bash` -> `operation:assemble-rootfs-busybox` (uses-tool) - edge `tool:bash` -> `operation:tar-layer-busybox` (uses-tool) - edge `tool:bash` -> `operation:write-config` (uses-tool) - edge `tool:bash` -> `operation:write-manifest` (uses-tool) - edge `tool:bash` -> `operation:write-index` (uses-tool) - edge `tool:bash` -> `operation:verify-blobs` (uses-tool) - edge `tool:bash` -> `operation:clean-scratch` (uses-tool) - edge `tool:bash` -> `operation:archive-layout` (uses-tool) ### Dry Run - Builder - tool `bash` - tool `tar` - tool `coreutils` - write `oci-layout` - run `assemble-rootfs-busybox` with `bash` - run `tar-layer-busybox` with `bash` - run `write-config` with `bash` - run `write-manifest` with `bash` - run `write-index` with `bash` - run `verify-blobs` with `bash` - run `clean-scratch` with `bash` - run `archive-layout` with `bash` - descriptor `busybox-shell-oci-image` - transform `oci-layout` (json) - transform `index` (json) - transform `blobs` (tree) - transform `oci-archive` (tar) - materialize `busybox-shell-oci-image` with `runCommand` - evidence `smoke-test` ### Dry Run - Runtime None. ### Plan View - write `write:oci-layout` - run `assemble-rootfs-busybox` - run `tar-layer-busybox` - run `write-config` - run `write-manifest` - run `write-index` - run `verify-blobs` - run `clean-scratch` - run `archive-layout` - `write:oci-layout`: `mkdir -p "$(dirname "$out/oci-layout")"` - `assemble-rootfs-busybox`: `bash -c 'set -euo pipefail` - `tar-layer-busybox`: `bash -c 'set -euo pipefail` - `write-config`: `bash -c 'set -euo pipefail` - `write-manifest`: `bash -c 'set -euo pipefail` - `write-index`: `bash -c 'set -euo pipefail` - `verify-blobs`: `bash -c 'set -euo pipefail` - `clean-scratch`: `bash -c 'set -euo pipefail` - `archive-layout`: `bash -c 'set -euo pipefail` ### Plan Shell Excerpt ```sh mkdir -p "$(dirname "$out/oci-layout")" cat > "$out/oci-layout" <<'METABUILDER_HEREDOC_18f0797eab35a4597c1e9624aa4f15fd91f6254e5538c1e0d193b2a95dd4acc6' {"imageLayoutVersion":"1.0.0"} METABUILDER_HEREDOC_18f0797eab35a4597c1e9624aa4f15fd91f6254e5538c1e0d193b2a95dd4acc6 bash -c 'set -euo pipefail mkdir -p "'"$out"'/.scratch/rootfs-busybox" cp -a "$1"/. "'"$out"'/.scratch/rootfs-busybox/" chmod -R u+w "'"$out"'/.scratch/rootfs-busybox" ' assemble-rootfs-busybox /nix/store/mm0g0g122n6pi28759dkkx8cfb2724by-busybox-static-x86_64-unknown-linux-musl-1.37.0 bash -c 'set -euo pipefail ``` ### Runtime Services None. ### Descriptors - descriptor `busybox-shell-oci-image` (payload keys `architecture`, `entrypoint`, `exposedPorts`, `kind`, `labels`, `os`) ### Builder Self-Documentation - documented operations: `19` - runtime services: `0` ### Materialized Outputs - oci-layout -> oci-layout (json) - index -> $out/index.json (json) - blobs -> $out/blobs (tree) - oci-archive -> $out/image.oci.tar (tar) ### Materialization - derivation: `busybox-shell-oci-image` - outputs: `4` - runtime artifacts: `0` ### Substrates - dockerfile: `supported` - shell: `supported` ### Source files These files are the complete source for OCI image example: the builder module plus the fixtures it consumes. - [OCI image example module](/metaBuilder/examples/oci-image/source/builder.nix) - Source for the worked busybox image spec and the exported views. ### OCI image example module This module instantiates the `oci-image` ornament's `ociImage` constructor with a static busybox layer and exports the views used by the tour page. Source path: [`examples/oci-image/builder.nix`](https://github.com/kleisli-io/metaBuilder/blob/main/examples/oci-image/builder.nix). ```nix { mb, pkgs, ... }: let ops = mb.operations; oci = mb.ornaments."oci-image"; spec = oci.ociImage { name = "busybox-shell"; layers = [ { name = "busybox"; source = pkgs.pkgsStatic.busybox; } ]; entrypoint = [ "/bin/sh" ]; evidence = [ (ops.evidence { name = "smoke-test"; payload = { command = "/bin/sh -c 'echo oci-smoke-ok'"; expectedOutput = "oci-smoke-ok"; }; }) ]; }; program = mb.program.fromOrnamentedSpec oci.OciImageBuilder.T spec; value = { builder = { inherit (oci) OciImageBuilder ociImage descriptor schema; }; inherit spec program; validation = mb.program.validate.run program; deps = mb.program.deps.run program; dryRun = mb.program."dry-run".run program; planView = mb.program."plan-view".run program; docs = mb.program.describe.run program; selfView = mb.program.introspect.run program; materialize = mb.program.materialize.run program; }; in { scope = { inherit spec program value; }; } ``` ## API Reference ### Core API #### Descriptions `BuilderSpec` and `BuilderOp` are generated datatypes. They are the typed backing for validation, schemas, docs, dependency views, and program interpretation. Domain datatypes keep payloads typed before programs interpret them: sources, dependencies, tools, outputs, evidence, validations, descriptors, and parameters. #### Operations Constructors build typed operation records. Execution is handled by the internalized `mb.program` desc-interp signature. ### Program #### Validate Validation interpreter for typed builder programs. #### Deps Dependency graph interpreter for typed builder programs. #### Dry-run Dry-run interpreter for typed builder programs. #### Plan-view Returns a diagnostic view of a builder program: the typed plan fields, each step with its rendered shell command, runtime artifact summaries, and the combined shell transcript. No derivation is produced. #### Describe Builds a documentation model from the builder's own operation program. This is distinct from `mkDocsContent`, which documents metaBuilder's public API. #### Introspect `introspect.run program` returns every standard view of one builder program — validation, dependencies, dry-run, plan, documentation, materialization, substrate support — plus a rendered markdown summary. #### Materialize Builds typed `BuildPlan` step records, validates tool and service declarations, renders shell commands, and produces a `runCommand` derivation for the finalized plan. `runState` exposes the typed pre-finalize plan state that `plan-export` serializes. #### Backends Backends translate a validated `BuildPlan` into an artifact for another build substrate. Unlike the program interpreters they do not fold over the operation alphabet — they consume the plan that `materialize` produces, so the interpreter coverage grid does not apply. Each backend declares the plans it cannot honor through `unsupportedReasons`; nothing is miscompiled silently. ## `dockerfile` _dockerfile backend: emits a Dockerfile from a substrate-neutral BuildPlan._ Translates a validated `BuildPlan` into a Dockerfile over a parameterizable base image: tool preflight by name, local inputs copied from the build context, and one RUN per rendered step. Plans it cannot honor are rejected with explicit reasons. ## `shell` _shell backend: emits a standalone bash script from a substrate-neutral BuildPlan._ Translates a validated `BuildPlan` into a standalone bash script: tool preflight by name, pathMap exports, library-path export, and the rendered step commands. Plans it cannot honor are rejected with explicit reasons. #### Former `mkBuilderKind { name, base, builderOps, runtimeOps, stateSpec }` derives the operation coproduct surface (`Eff`, `Resp`, `reviewOp`, `opNames`, `injectorsWith`, `dispatch`) and the state ornament (`State`, `forget`, `forgetWith`) from one argument tuple, so the op side and the state side cannot drift. The derived `forget` is op-blind: it never depends on the operation datatypes, so it is operations-preserving by construction. #### Plan-export Serializes a builder program's pre-finalize plan state: `export` yields a JSON-safe attrset with the `BuildPlan` fields, `json` the corresponding string. Live derivations never appear in the output — boxed derivation fields are omitted, and bare boxed positions show as `null`. ### Reference #### Schemas Exposes generated schemas for builder and runtime datatypes without interpreting a program. #### Datatypes Exposes datatype descriptors used by the docs content generator and schema derivation. Rendered project documentation is produced by `mb.mkDocsContent`. ### Ornaments #### Project-builder `ProjectBuilder` ornaments `BuilderSpec` with a single `langName` field, marking a spec as belonging to a language-specific project. Downstream ornaments (`implementations`, `vendoring`, `testing`) refine `ProjectBuilder` further; `dependencies` ornaments `BuilderSpec` directly since it is language-agnostic. #### Dependencies Two surfaces live on this ornament: a **typed-shape** layer (constructors + dispatcher + spec ctor) and a **resolver eliminators** layer (uniform resolution + the resolved-deps marker). ## Typed-shape layer A `DependencyShape` selects the resolution strategy by constructor: - `Uniform { langName }` — single-typed, identical treatment across all packages. - `Partitioned { langName; pathField }` — custom-vs-bundled split driven by a sentinel path field. - `MultiTyped { types : list DependencyType }` — N-type mix; each `DependencyType` declares its own transitive / toposort flags. `matchShape { uniform = …; partitioned = …; multiTyped = …; } shape` is the typed dispatcher: constructor-driven pattern match over the three modes. `define { dependencyShape; … }` produces a `DependenciesBuilder` spec; consumers fold the spec into the surrounding builder pipeline downstream. ## Resolver eliminators `resolveUniform { langName; deps }` walks the transitive closure of `deps` via the `${langName}Deps` field on each package, then toposorts so dependencies precede dependents. Throws on cycles. `markResolved deps` wraps an already-resolved list in a sentinel-tagged record. `isResolved x` answers the marker check; `unwrapDeps x` extracts the list (or returns plain inputs as-is). Together they centralise the inline `if ? __resolvedDeps then .deps else x` pattern that legacy consumers spelled at every call site. #### Implementations Two complementary surfaces live on this ornament: a **typed-spec** layer and a **consumer-coordination** layer. ## Typed-spec layer A `define` call describes a project that supports multiple interchangeable implementations under a single `langName`. Each `ImplementationDescriptor` carries a `name` and an open `capabilities` attrset for impl-specific metadata (e.g. invocation flags, version range, supported targets). `select spec implName` returns the descriptor or throws if absent. `available spec excluded` filters out broken/excluded impls. `perImpl spec f` evaluates `f` against each impl and returns the results keyed by impl name — the typed analog of dynamic `.${implName}` projections. ## Consumer-coordination layer `defineSystem { langName; implementations; defaultImpl; makeOverridable; allowUserExtensions ? false }` returns `{ impls; withExtras; filterByName }` (plus `extend` when extensions are allowed). The `implementations` argument is an attrset (`{ impl-a = {...}; impl-b = {...}; ... }`) so consumers can produce the coordination record without re-shaping input. `withExtras builderFunction args` projects per-impl variants under `result.${implName}` attributes, injects `passthru.repl` when an impl exposes `replWith`, and populates `passthru.meta.ci.targets` with the implementations minus the current one and `brokenOn`. `filterByName impl xs` resolves implementation-specific sources/dependencies — plain values pass through; non-derivation attrsets are treated as per-impl selectors with optional `default`. `makeBuilder { implsSystem; createPublicAPI; baseToolEnv }` recursively wraps a `createPublicAPI` projection with `extend` and `withTools` so downstream consumers receive the full builder surface (not just an impls-system) after extension or tool augmentation. Cross-ornament dependency on `mb.ornaments.toolEnv`. #### ToolEnv Typed tool-environment vocabulary. The underlying `ToolEnvSpec` lives in `mb.descriptions` and carries only a `tools : [ToolSpec]` list — no bash-string fragments leak into the spec. - **Smart constructors**: - `toolEnv.define { tools }` proxies to `mb.operations.toolEnv` (eager structural validation). - `toolEnv.create { name = package; ... }` builds the spec from a `{ name = package | null; }` attrset (legacy ergonomic shape; `null` entries are dropped). - `toolEnv.empty` is the zero element. - `toolEnv.merge a b` combines two environments; tool name collisions resolve B-wins. - **Eliminators** (pure functions of the typed spec): - `toolInputs : ToolEnvSpec → [Derivation]` — deduplicated package list for `nativeBuildInputs`. - `toolBinPath : ToolEnvSpec → String` — `lib.makeBinPath` view. - `toExportSnippet : ToolEnvSpec → String` — heredoc-style `export PATH=...` snippet (empty for empty envs). - `toInlineSnippet : ToolEnvSpec → String` — indented variant. - `toWrapPrefix : ToolEnvSpec → String` — `wrapProgram --prefix` fragment. - `toolPackages : ToolEnvSpec → { name = Derivation; }` — legacy-shaped attrset view, useful for `passthru` round-trip. - `isEmpty : ToolEnvSpec → Bool`. The spec is the single source of truth; every derived view comes from an eliminator. Shell snippets live in eliminator outputs, not in spec fields. #### Testing A `TestSuite` is a typed list of named `TestCase` records. Each case carries an opaque `body` — the framework stops typing at the case boundary so consumers can stash pure-Nix booleans, derivation builders, or arbitrary runner specs. `runPure suite` evaluates every case whose body is a boolean and reports per-case `PASS` / `FAIL` / `SKIP` / `ERROR` classification plus a `passed` / `failed` / `skipped` tally and an `allPass` flag. Non-boolean bodies are skipped — that path is for derivation-driven or runner-driven tests handled downstream. #### Vendoring `mkContract { required; optional; description; }` builds a typed `VendoringContract` declaring the structural requirements a vendored package must satisfy. `defaultContract` is the framework's standard contract (`name`, `deps` required; `version`, `path`, source/registry markers optional). `checkRequired contract metadata` returns the list of contract- required fields missing from `metadata` (empty list ⇒ valid). `define { langName; contract; … }` produces a typed `VendoringBuilder` spec for downstream composition. #### Code-gen `CodeGenBuilder` refines `BuilderSpec` with `generator` and `languages` so multi-language generators (protoc, openapi-generator, graphql-codegen) carry their target metadata in the type. The `codeGen` smart constructor expands a single config record into a fully-typed spec: per-language outputs, read-source / declare-tool / resolve-dependency / run-tool / transform-output / emit-descriptor / materialize-derivation operations. #### Idl `IdlBuilder` refines `CodeGenBuilder` with `idlFormat` and `idlSource`, encoding "this generator is driven by an IDL document" in the type. `fromProtobuf { name; protos; languages; options?; languageConfigs?; }` builds a fully-typed `IdlBuilder` spec for `protoc`. The default language config covers the standard protoc backends; pass `languageConfigs` to override or extend. #### Capabilities Typed capability vocabulary built on the `runtime.*` effect algebra. The underlying datatypes (`CapabilitySchema`, `CapabilityCategory`, `CapabilitySet`) live in `mb.descriptions`; this ornament adds three things consumers actually reach for: - **Smart constructors** as terse aliases: `capabilities.capability { name; description?; params?; returns?; }` `capabilities.category { name; description?; capabilities?; }` `capabilities.set { categories?; custom?; }` - **Built-in categories** as typed values addressable as `capabilities.builtins.{lifecycle,crud,streaming}`. Each is a fully-typed `CapabilityCategory`. Consumer extension goes through `H.ornament` on the closed kernel sum, not through string-keyed attrset merge. - **Schema eliminator** `schema : CapabilitySchema → AttrSet` produces a JSON-Schema-shaped attrset suitable for MCP/API tooling. `setSchemas : CapabilitySet → AttrSet` flattens an entire set, attaching a `category` tag to each entry. #### Protocol Typed communication protocols over the closed kernel sums `Transport` (TCP/Unix/Stdio) and `Serialization` (JSON/Protobuf/Sexp/MsgPack). Both sums are defined in `mb.descriptions` and re-exported here as `protocol.Transport` / `protocol.Serialization`. - **Smart constructor** `protocol.define { name; description?; transport; serialization; defaultPort?; portEnvVar?; capabilities; options?; }` proxies to `mb.operations.protocol` (eager structural validation against `ProtocolSpec.T`). - **Built-in protocols** as typed values addressable as `protocol.builtins.{rpc,jsonRpc,dbus,grpc}`. Each carries a `CapabilitySet` drawn from `capabilities.builtins`. - **`satisfies : ProtocolSpec → CapabilitySet → Bool`** is the capability cross-check (proxy to `mb.descriptions.runtime.protocolSatisfies`). Consumer extension is through `H.ornament` on the kernel sums. There is no `withTransports`/`withSerializations`/`withProtocols` surface — extension via string-keyed attrset merge was a legacy idiom and is intentionally absent. #### Service `define { name; description?; package; capabilities; protocols?; config?; }` builds a typed `ServiceSpec` and attaches an `operations` field holding the runtime-op program that materializes the service: ``` declareCapability(c1) … declareCapability(cN) # one per category declareProtocol(p1) … declareProtocol(pM) # one per protocol declareService(svc) materializeUnit(svc.name) ``` The eager compatibility check fires inside the underlying `mb.operations.service` smart constructor — invalid services cannot be constructed. `compatibility` and `descriptor` are re-exported from `mb.descriptions.runtime` for consumer convenience. `program` is a shortcut: pass either a service value or the arguments to `define`, and receive an internalized builder program. #### ReplServer Typed REPL-server vocabulary built on the locked runtime.* algebra. - **Smart constructor** `replServer.define { protocol; mode; registration?; port?; portEnvVar?; interface?; lifecycle?; enable?; shortLivedFlags?; extra?; }` proxies to `mb.operations.replServer`. Port and `portEnvVar` default from the protocol's `defaultPort`/`portEnvVar`. Registration defaults from `mode` via the inference rule `Foreground → ServiceSpec`, `Background → XDG`. Lifecycle defaults to `LongRunning`. - **Closed-sum re-exports** for consumer ergonomics: `Mode = Foreground | Background`, `Registration = XDG | Global | ServiceSpec | None`, `Lifecycle = LongRunning | OneShot`. - **Built-in protocols** as typed `ProtocolSpec` values: `protocols.{swank,nrepl,dap}`. Each carries a baseline `CapabilitySet` of `lifecycle` only; consumers extend via `capabilitySet { categories = [...] }`. The legacy string-keyed taxonomy (`universal`/`common`/`discovery`/...) is intentionally absent. Registration backend names map to runtime conventions: `XDG` → `$XDG_RUNTIME_DIR/repl//.json`, `Global` → `$XDG_RUNTIME_DIR/repl//shared/.json`, `ServiceSpec` → discovery via NixOS configuration, `None` → no automatic registration. #### Sandbox Typed declarative sandbox profile. The profile is the single source of truth; four enforcement backends — bubblewrap, Landlock, seccomp BPF, and systemd hardening — consume the same declaration and produce backend-specific configuration. Three-layer defense: 1. **bwrap**: mount namespace, PID namespace, seccomp stage-1. 2. **Landlock**: path-based filesystem access (applied from inside the process post-init). 3. **seccomp stage-2**: self-applied filter blocking `execve` post-init when the profile is sealed. - **Smart constructor** `sandbox.define { readOnlyPaths?; readWritePaths?; tmpfs?; listenTcp?; connectTcp?; display?; stdio?; unixSockets?; allowExecve?; allowFork?; lifecycle?; daemonMode?; dns?; sourceAccess?; sourceWritePaths?; coordinationWritePaths?; storeAccess?; }` proxies to `mb.operations.sandboxProfile` (eager structural validation against `SandboxProfile.T`). - **Built-in profiles** as typed `SandboxProfile` values: `profiles.sealed` (the empty default), `profiles.effectful` (sealed + execve + fork). Anything host- or workload-specific composes downstream. - **Eliminators**: - `toBwrap : SandboxProfile → [String]` — bubblewrap argument list. DNS handling routes through `profile.dns` when present. - `toLandlock : SandboxProfile → LandlockProfile` — path-list + port-list view. - `toSeccomp : SandboxProfile → SeccompStage → Thunk Derivation` — BPF filter; stage `Bwrap` includes `processExec`, stage `Self` respects `allowExecve`. - `toSystemd : SandboxProfile → SystemdHardening` — directives suitable for `systemd.services..serviceConfig`. - **Closed-sum re-exports**: `SeccompStage = Bwrap | Self`, `Lifecycle = LongRunning | OneShot`. - **Combinators** in `sandbox.combinators`: `compose`, base profiles (`sealed`/`effectful`), network (`listen`/`connectTo`), filesystem (`readonly`/`readwrite`), execution (`allowExec`/`allowFork`), lifecycle (`daemon`), and a `defer` meta-combinator for two-pass composition. Each carries `{ sig; doc; impl }` metadata. - **Seccomp compiler**: `syscallSets` exposes 12 generic syscall categories. `mkFilter`/`mkAllowlist`/`flattenPolicy` compose them into BPF filters via the bundled `gen-seccomp-bpf` tool. The compiler is a standalone C program (single source file) that reads a newline-separated allowlist and emits a BPF blob. #### Transform `transform` builds a typed `BuilderSpec` for a sequential transformation pipeline. Each `step` is a `{ name; tool; args ? []; env ? {}; }` record carrying a tool (raw or pre-constructed via `mb.operations.tool`). Tools are deduplicated and emitted as `declareTool` operations; steps become `runTool` operations; the `outputs` list expands to `transformOutput` operations. The constructor wraps the `transform-output` effect of the new framework — no new effect tags are introduced. #### Oci-image `OciImageBuilder` refines `BuilderSpec` with image metadata (layers, entrypoint, cmd, env, exposedPorts, labels, architecture, os) so OCI images carry their runtime contract in the type. The `ociImage` smart constructor compiles a single config record into a typed spec whose operations assemble a spec-conformant OCI image layout (`oci-layout`, `index.json`, `blobs/sha256/*`) entirely at build time: per-layer rootfs assembly and deterministic tar, then config/manifest/index rendering in digest-chain order, a blob self-check, scratch cleanup, and an `image.oci.tar` archive of the layout — each as a named step so every fold renders the assembly legibly. ### Library Helpers #### Tool-env `create { tools = [...] }` builds a typed `ToolEnvSpec` from a list of raw `{ name; package }` records; each is wrapped via `mb.operations.tool` so `package` is carried as a typed `Thunk Derivation`. `merge a b` composes two envs — `b` overrides any `a` tool whose `name` matches. `empty` is the identity. #### Toolchain `select` resolves an implementation from prioritized hint evaluators and returns a typed `ToolchainSelection`. An explicit override short-circuits the hint pipeline. `mkManifest` builds a typed `ToolchainManifest` whose `matrix` maps each spec name to its sanitized, default-applied field set. Builder-specific extension fields pass through unchanged. #### Passthru `create` builds a typed `PassthruSpec` from `{ langName; baseName; baseDeps; extensions ? {} }`. The spec is the canonical structured representation of language-tagged package metadata. Hash stability invariant: a `PassthruSpec` depends only on its constructor arguments. Two `create` calls with equal inputs produce equal specs; no ambient state, no derivation references at the spec level. #### Bundled `create` builds a typed `BundledSpec` from `{ langName; packageName; extraAttrs ? {} }`. The typed record's constructor tag (`_con = "MetaBuilderBundled"`) is the discriminator that distinguishes bundled descriptors from anything else; callers can check membership via `isBundled`. #### Dashboard `mkMetrics` produces a typed `sanitize` projection that pulls `lockHash` and `toolchainSpec` out of raw lock-file metrics, filters the toolchain spec by an optional whitelist of fields, and returns a flattened attr-set of the remaining metric fields. `mkWorkspaceSummary` produces a typed `summarize` that walks a workspace member map, sanitizes each member, discovers the first non-null `lockHash`, optionally collects stats, and returns the summary record. #### ContentAddress `contentAddress drv` returns `drv` with floating content-addressing: its output store path is the realised NAR content hash, not the input hash. ```nix final = contentAddress wrappedPackage; ``` Wins over input-addressed caching: early cutoff (unchanged output stops a rebuild cascade) and cross-machine sharing (a realisation built on one machine substitutes on another, given nix >= 2.35 + harmonia >= 3.1.0). Only wrap byte-reproducible derivations (`nix build --rebuild`). A non-reproducible CA drv flaps its output hash and mismatches across machines. Per-derivation opt-in; never `contentAddressedByDefault`. ## Additional pages (including unstable internal surfaces) ### Examples metaBuilder examples are builder definitions with source fixtures, self-documentation, tests, materialization plans, and generated artifacts. - [Node service example](/metaBuilder/examples/node-service) - Guided Node service builder tour: runnable package, HTTP service descriptor, runtime unit, dependency graph, and materialization plan. - [C code generation example](/metaBuilder/examples/c-codegen) - Guided C codegen builder tour: schema input, generated C sources, static library, CLI, descriptors, dependency graph, and materialization plan. - [Bridge example](/metaBuilder/examples/bridge) - Relates the shipped builder kinds — Node service, C code generation, OCI image, and IDL — through kernel-checked ornament, effect, and list-computation theorems. - [IDL example](/metaBuilder/examples/idl) - IDL example: multi-language protobuf code generation via the IdlBuilder ornament and internalized program interpreters. - [OCI image example](/metaBuilder/examples/oci-image) - Guided OCI image builder tour: busybox layer, digest-chain assembly steps, image descriptor, smoke-test evidence, and materialization plan. ### Manual metaBuilder is a library for writing builders as typed descriptions. A builder names the structure of a build. That structure includes inputs, tools, operations, outputs, runtime shape, and evidence, so the same build can be validated, inspected, explained, and materialized. Use this manual when you want to design or consume a metaBuilder builder. It keeps the focus on the public model. You will see which values you write, which views you ask for, and how those views make a builder easier to understand. ## Path Through The Manual Start with [Introduction](/metaBuilder/manual/introduction) for the overall model. Then read [Getting Started](/metaBuilder/manual/getting-started) for the smallest complete flow. The middle chapters explain the reusable pieces. - [Builder Specs](/metaBuilder/manual/builder-specs) - [Operations](/metaBuilder/manual/operations) - [Programs And Views](/metaBuilder/manual/programs-and-views) - [Designing Builder Surfaces](/metaBuilder/manual/designing-builder-surfaces) The final chapters explain how to return useful artifacts and grow a small builder into a production builder. - [Outputs, Evidence, And Runtime Artifacts](/metaBuilder/manual/outputs-evidence-runtime) - [Materialization Model](/metaBuilder/manual/materialization-model) - [Authoring Production Builders](/metaBuilder/manual/authoring-production-builders) For complete guided examples, read the examples section after the manual. ### Theory The theory section explains the ideas behind metaBuilder. It is a companion to the manual and not a prerequisite for using the library. The practical claim is short. A build can be written as typed data, that data can be read as a program, and the program can be interpreted in more than one way. The theory chapters make each part of that claim precise. A builder is a typed description rather than a function. The description becomes a program over a fixed signature of build-time and runtime operations. Domain builders refine the description with extra data through ornaments, and a typed forget map projects them back to the shared shape without losing the program. Every view is an interpretation of that one program. - [Builders As Descriptions](/metaBuilder/theory/builders-as-descriptions) - [Internalized Programs](/metaBuilder/theory/internalized-programs) - [Ornaments And Domain Surfaces](/metaBuilder/theory/ornaments-and-domain-surfaces) - [Interpretation And Views](/metaBuilder/theory/interpretation-and-views) - [Evidence, Descriptors, And Runtime Structure](/metaBuilder/theory/evidence-descriptors-runtime) Read this section when you want to understand why metaBuilder can support one build with many views.