35.1. The template
The rows below are generated from PropertyKindCalculus.Rubrics.deploymentTemplate. The
author's part column is the one to read while building a document; the sections that
follow argue why each group asks for what it asks. Conformance is declared exactly as for
the model template: declaration sites through the @[rubric …] attribute, section sites
through the document's own tags, and a status computed from the two against each rubric's
evidence kind.
| Requires | The rubric | The author's part |
|---|---|---|---|
What is deployed |
|
|
|
| exposition | What is deployed, and which model boundary each deployed unit realizes | List the deployed units, and name for each the model boundary it realizes |
| exposition | The document states what deploying the model adds, and cites the model document for what the module is | State what deploying the model adds, and cite the model document for what the module is |
The contracts |
|
|
|
| checked | The data contract is declared, compiled in, and validated against a producer's own claims before any payload is decoded | Declare the payload interface, compile it into the executable, and validate it against the producer's own claims before any payload is decoded |
| checked | The platform contract is kind-typed and held to the registration payload, with the discharge relation decided by the kernel | Kind-type the argument plane the scheduler passes, hold it to the registration payload, and let the kernel decide the discharge relation between the two |
| generated | One deployment card per deployed unit, each panel read off a declared object rather than written beside it | Generate one deployment card per deployed unit, each panel read off a declared object rather than written beside it |
Sizing and knobs |
|
|
|
| measured | The run is sized from measured records, not from constants typed by hand | Size the run from measured records, and name the records each size came from |
| measured | Operating points come from a sweep whose own turnover or plateau names them, reported with the dispersion any threshold has to beat | Sweep the parameter, let the machine's own turnover or plateau name the operating point, and report the dispersion any threshold has to beat |
| exposition | Every environment knob a job may set is enumerated with what it decides | Enumerate every environment knob a job may set, with what each one decides |
The platform |
|
|
|
| exposition | The image facts are stated: what ships per unit, the toolchain and architecture spectrum it was built for, and the ABI floor it runs against | State what ships per unit, the toolchain and architecture spectrum it was built for, and the ABI floor it runs against |
| exposition | Registration and version derivation are mechanized, so a deployed version is derived from the artifact rather than asserted beside it | Derive the deployed version from the artifact and mechanize registration, so neither is asserted beside what actually shipped |
| exposition | Backend interchange is stated: what the same source does on each target, and what changes when the target changes | State what the same source does on each target, and what changes when the target does |
Acceptance |
|
|
|
| checked | Acceptance is a gate against the specification the model document proves — run as proof-by-execution, not asserted | Run acceptance as a gate against the specification the model document proves — proof by execution, not an assertion that the two agree |
| measured | Performance claims are a paired A/B in the deployed executable, never a microbenchmark quoted as a prediction | Make every performance claim a paired A/B in the deployed executable, never a microbenchmark quoted as a prediction |
| exposition | Each green signal names which of the changed lines it actually compiled or ran, so a passing pipeline is not quoted as evidence for a path it never touched | Say, for each green signal quoted as evidence, which of the changed lines it actually compiled or ran |
Reproducibility and limits |
|
|
|
| exposition | Failure, checkpoint and resume semantics are stated: what a partially completed job leaves behind, and what resuming it does | State what a partially completed job leaves behind, and what resuming it does with that |
| generated | A reproducibility manifest carries the pins and digests of what actually ran, generated from the artifacts rather than transcribed | Generate the reproducibility manifest from the artifacts — the pins and digests of what actually ran, not of what was intended |
| exposition | What is trusted is stated plainly: the boundaries the verification does not cross, and what a consumer is therefore taking on faith | Name the boundaries this deployment's verification does not cross, and what a consumer is therefore taking on faith |