From d6f22c6d2fb159eeb1e421c9c2ff28417c19e052 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 3 Sep 2026 05:44:42 +0000 Subject: [PATCH 1/3] Manufacturing manifest: seal the printer-asset join, and refuse until a machine is registered The coupon authority already declared this binding unsolved -- coupon_v1_open_obligations carries PhysicalPrintInstanceAttributionUnsolved routed to AttributeByManufacturingManifestAndHandling -- so this is that declared route, not a new idea. Two coupons off two printers are geometrically identical, so the binding cannot be recovered by inspecting the plastic. NO SECOND IDENTITY FOR A PRINTER. product.placement_supply.PhysicalAsset already carries identity, a catalog DeclarationRef naming the vendor product row, an optional serial and procurement provenance, and its charter already splits owned inventory from vendor facts. A machine that produces parts is the same physical object with a role. Minting PrinterNodeIdentity would have been two names for one unit -- the brief calls it "node-ness of the printers", and that name is what made a new concept look necessary. THE ADMISSION EXISTS BECAUSE THE CARRIER IS WEAKER THAN THE CONSUMER NEEDS. PhysicalAssetIdentity is a branded NonEmptyStr; a brand does not make a duplicate or unregistered identity unwritable. The repair is not a stronger printer-only identity -- that re-opens what the paragraph above closed -- but a sealed admission at the consuming boundary, the same shape as AdmittedRealizationV0. owned_printer_inventory is EMPTY and the live-inventory witness asserts that it therefore admits nothing. That is the correct day-one state, not a gap: until a serial is read off a machine, no coupon can be attributed to it. Pre-populating a plausible row would be a fabricated fact about hardware nobody has inspected. Six witnesses green by execution. The discrimination claim on w_the_admitted_asset_is_the_one_requested_not_the_first_row was verified by MUTATION, not asserted: replacing the identity join with `a => true` leaves the empty-inventory and single-row witnesses green and turns that one red. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4 --- .../manufacturing_manifest.dag | 120 +++++++++++++++++ ...is_manufacturing_manifest_witness_test.dag | 127 ++++++++++++++++++ 2 files changed, 247 insertions(+) create mode 100644 dag/gunbc/product/printed_chassis/manufacturing_manifest.dag create mode 100644 dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag diff --git a/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag b/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag new file mode 100644 index 00000000000..d83edf6b881 --- /dev/null +++ b/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag @@ -0,0 +1,120 @@ +module product.printed_chassis.manufacturing_manifest + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import product.placement_supply { + PhysicalAsset, + PhysicalAssetIdentity, +} + +// THE MANIFEST BINDS A PRINTED THING TO THE PROCESS THAT PRODUCED IT, and it exists because the +// coupon authority already declared that binding unsolved. coupon_v1_open_obligations carries +// PhysicalPrintInstanceAttributionUnsolved routed to AttributeByManufacturingManifestAndHandling; +// this module is that route, not a new idea. Two coupons off two printers are geometrically +// IDENTICAL -- the orientation datum makes one orientable, never attributable -- so the binding +// cannot be recovered by inspecting the plastic and must be captured while the part is still on the +// bed it was printed on. +// +// A PRINTER IS A PhysicalAsset AND THIS MODULE MINTS NO SECOND IDENTITY FOR ONE. product. +// placement_supply already carries identity, a catalog DeclarationRef naming the vendor product row, +// an optional physical serial and procurement provenance, and its charter already assigns +// vendor/product facts to extdeps and owned inventory to the product layer. A machine that produces +// parts rather than occupying a shelf is the same physical object with a ROLE; minting +// PrinterNodeIdentity beside PhysicalAssetIdentity would be two names for one unit, which is the +// net-concepts-by-re-invention failure DESIGN section 2 names. The brief calls it "node-ness of the +// printers" and that name is what made a new concept look necessary. + +// THE ADMISSION EXISTS BECAUSE THE IDENTITY CARRIER IS WEAKER THAN THE CONSUMER NEEDS, and saying +// so is the honest alternative to strengthening it here. +// +// PhysicalAssetIdentity is a branded NonEmptyStr. A brand stops an arbitrary NonEmptyStr standing in +// for one, and it does NOT make a duplicate or an unregistered identity unwritable -- so a consumer +// handed a bare PhysicalAssetIdentity has a string that looks authoritative and may name nothing. +// The repair is NOT a stronger printer-only identity: that would put two identities on one machine +// and re-open exactly what the paragraph above closed. It is a sealed admission at the CONSUMING +// boundary, which is the same shape as the realization contract's AdmittedRealizationV0 -- a value +// only a join against the authority can mint, so the manifest consumes a checked binding rather +// than a hopeful string. A later corpus-wide migration of PhysicalAssetIdentity to an +// allocator-minted identity replaces this bounded wall without disturbing its consumers. +type AdmittedPrinterAsset sole_constructor { + asset: PhysicalAsset +} + +fn admitted_printer_identity(a: AdmittedPrinterAsset) -> PhysicalAssetIdentity { + a.asset.identity +} + +fn admitted_printer_catalog(a: AdmittedPrinterAsset) -> DeclarationRef { + a.asset.catalog +} + +// EVERY REFUSAL NAMES WHAT IT LOOKED FOR AND WHAT IT FOUND. A single PrinterAssetRefused carrying a +// reason string would make these four indistinguishable to a consumer and unreportable to an +// operator holding the machine. +type PrinterAssetAdmission + = PrinterAssetAdmitted { binding: AdmittedPrinterAsset } + | PrinterAssetAbsent { requested: PhysicalAssetIdentity } + | PrinterAssetDuplicate { requested: PhysicalAssetIdentity, matches: Int } + | PrinterCatalogMismatch { requested: PhysicalAssetIdentity, expected_module: NonEmptyStr, found_module: NonEmptyStr } + +fn physical_asset_identity_eq(a: PhysicalAssetIdentity, b: PhysicalAssetIdentity) -> Bool { + a as String == b as String +} + +// THE SCAN CARRIES THE MATCHES RATHER THAN A COUNT PLUS A VALUE, because a count and a separately +// held candidate can disagree. Holding the matched rows is what lets the duplicate arm report how +// many without a second traversal, and it is why this fold has no early exit: an early exit would +// find the first match and never learn that a second exists, which is the whole point of the +// duplicate refusal. +type PrinterAssetScan sole_constructor { + matches: List +} + +fn scan_printer_assets(inventory: List, requested: PhysicalAssetIdentity) -> PrinterAssetScan { + PrinterAssetScan { + matches: filter(inventory, a => physical_asset_identity_eq(a: a.identity, b: requested)) + } +} + +// The product row every admitted printer must name. Stated as the module path rather than as a +// DeclarationRef literal because the catalog's decl_name varies by which declaration in that module +// a row cites, while the MODULE is what identifies the product. +data a1_mini_catalog_module: NonEmptyStr = "extdeps.printing.bambu_lab_a1_mini" + +// AN EMPTY INVENTORY REFUSES, AND THAT IS THE CORRECT DAY-ONE STATE rather than a gap to be filled +// before this is useful. Until a printer is registered with its serial, no coupon can be attributed +// to it -- which is exactly the fail-closed behaviour this module exists to provide. The tempting +// arm is to admit an unregistered identity "for now" so that a print can proceed; that is the +// absorbing fallback, and it fails open precisely at the moment the operator most needs the binding +// to be real. +fn admit_printer_asset(inventory: List, requested: PhysicalAssetIdentity) -> PrinterAssetAdmission { + let scan = scan_printer_assets(inventory: inventory, requested: requested) + let n = count(scan.matches) + if n == 0 { + PrinterAssetAbsent { requested: requested } + } else { + if n > 1 { + PrinterAssetDuplicate { requested: requested, matches: n } + } else { + fold(scan.matches, init: PrinterAssetAbsent { requested: requested }, f: fn(_, a) { + let catalog_matches = a.catalog.module_path as String == a1_mini_catalog_module as String + if catalog_matches { + PrinterAssetAdmitted { binding: AdmittedPrinterAsset { asset: a } } + } else { + PrinterCatalogMismatch { + requested: requested, + expected_module: a1_mini_catalog_module, + found_module: a.catalog.module_path, + } + } + }) + } + } +} + +// THE OWNED PRINTER INVENTORY, EMPTY UNTIL THE MACHINES ARE IN HAND. This roster is the authority +// admit_printer_asset joins against, and it is deliberately not pre-populated with a plausible row: +// a PhysicalAsset with an invented serial would be a fabricated fact about hardware nobody has +// inspected, and every attribution built on it would inherit that. It is filled by reading the +// serial off each machine. +data owned_printer_inventory: List = [] diff --git a/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag b/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag new file mode 100644 index 00000000000..c8c9b4084bb --- /dev/null +++ b/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag @@ -0,0 +1,127 @@ +module test.claim.printed_chassis_manufacturing_manifest_witness_test + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import product.placement_supply { PhysicalAsset, PhysicalAssetIdentity } +import product.printed_chassis.manufacturing_manifest { + AdmittedPrinterAsset, + PrinterAssetAdmission, + PrinterAssetAdmitted, + PrinterAssetAbsent, + PrinterAssetDuplicate, + PrinterCatalogMismatch, + admit_printer_asset, + admitted_printer_identity, + a1_mini_catalog_module, + owned_printer_inventory, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn a1_mini_catalog() -> DeclarationRef { + DeclarationRef { + module_path: "extdeps.printing.bambu_lab_a1_mini", + decl_name: "a1_mini_build_envelope", + field: WholeDeclaration + } +} + +fn foreign_catalog() -> DeclarationRef { + DeclarationRef { + module_path: "extdeps.printing.some_other_printer", + decl_name: "other_build_envelope", + field: WholeDeclaration + } +} + +fn printer_row(id: NonEmptyStr, catalog: DeclarationRef) -> PhysicalAsset { + PhysicalAsset { + identity: id as PhysicalAssetIdentity, + catalog: catalog, + physical_serial: Absent, + procurement: Absent + } +} + +// AN EMPTY INVENTORY REFUSES, AND THIS IS THE LIVE STATE OF THE REPOSITORY TODAY, not a fixture +// convenience. owned_printer_inventory is empty because the machines have not been read yet, so +// nothing can be attributed to a printer -- which is the behaviour that makes the manifest worth +// having. A version that admitted an unregistered identity so a print could proceed would fail open +// exactly when the operator most needs the binding to be real. +test fn w_the_live_inventory_admits_nothing_today() -> Bool { + match admit_printer_asset(inventory: owned_printer_inventory, requested: "printer-a" as PhysicalAssetIdentity) { + PrinterAssetAbsent { requested: r } => r as String == "printer-a" + PrinterAssetAdmitted { binding: _ } => false + PrinterAssetDuplicate { requested: _, matches: _ } => false + PrinterCatalogMismatch { requested: _, expected_module: _, found_module: _ } => false + } +} + +// THE POSITIVE CONTROL. Without it the refusals above prove only that this function refuses +// everything, which a `false` in every arm would also satisfy. +test fn w_a_registered_a1_mini_is_admitted_under_its_own_identity() -> Bool { + let inv = [printer_row(id: "printer-a", catalog: a1_mini_catalog())] + match admit_printer_asset(inventory: inv, requested: "printer-a" as PhysicalAssetIdentity) { + PrinterAssetAdmitted { binding: b } => admitted_printer_identity(a: b) as String == "printer-a" + PrinterAssetAbsent { requested: _ } => false + PrinterAssetDuplicate { requested: _, matches: _ } => false + PrinterCatalogMismatch { requested: _, expected_module: _, found_module: _ } => false + } +} + +// TWO MACHINES, AND THE ONE NOT ASKED FOR IS NOT ADMITTED. This is the discriminating case for the +// join actually filtering: an implementation that returned the first inventory row regardless of the +// requested identity passes every witness above and fails here. +test fn w_the_admitted_asset_is_the_one_requested_not_the_first_row() -> Bool { + let inv = [ + printer_row(id: "printer-a", catalog: a1_mini_catalog()), + printer_row(id: "printer-b", catalog: a1_mini_catalog()), + ] + match admit_printer_asset(inventory: inv, requested: "printer-b" as PhysicalAssetIdentity) { + PrinterAssetAdmitted { binding: b } => admitted_printer_identity(a: b) as String == "printer-b" + PrinterAssetAbsent { requested: _ } => false + PrinterAssetDuplicate { requested: _, matches: _ } => false + PrinterCatalogMismatch { requested: _, expected_module: _, found_module: _ } => false + } +} + +// A DUPLICATE IDENTITY REFUSES AND SAYS HOW MANY. PhysicalAssetIdentity is a branded NonEmptyStr, so +// two rows may carry the same string -- the brand does not make that unwritable. This is the arm +// that stops a consumer silently taking whichever row the fold reached first. +test fn w_a_duplicated_identity_refuses_and_counts_the_matches() -> Bool { + let inv = [ + printer_row(id: "printer-a", catalog: a1_mini_catalog()), + printer_row(id: "printer-a", catalog: a1_mini_catalog()), + ] + match admit_printer_asset(inventory: inv, requested: "printer-a" as PhysicalAssetIdentity) { + PrinterAssetDuplicate { requested: r, matches: n } => r as String == "printer-a" && n == 2 + PrinterAssetAdmitted { binding: _ } => false + PrinterAssetAbsent { requested: _ } => false + PrinterCatalogMismatch { requested: _, expected_module: _, found_module: _ } => false + } +} + +// A ROW THAT IS NOT AN A1 MINI REFUSES, NAMING BOTH MODULES. A registered asset is not automatically +// a printer this program can qualify: the catalog is what says which product it is, and admitting a +// row whose catalog names another machine would bind a coupon to a process this program has no +// envelope, nozzle or material grading for. +test fn w_a_registered_asset_with_a_foreign_catalog_refuses() -> Bool { + let inv = [printer_row(id: "printer-a", catalog: foreign_catalog())] + match admit_printer_asset(inventory: inv, requested: "printer-a" as PhysicalAssetIdentity) { + PrinterCatalogMismatch { requested: r, expected_module: e, found_module: f } => + r as String == "printer-a" + && e as String == "extdeps.printing.bambu_lab_a1_mini" + && f as String == "extdeps.printing.some_other_printer" + PrinterAssetAdmitted { binding: _ } => false + PrinterAssetAbsent { requested: _ } => false + PrinterAssetDuplicate { requested: _, matches: _ } => false + } +} + +// THE EXPECTED MODULE IS READ FROM THE MANIFEST, NOT RESTATED HERE. If this witness spelled the +// module path as its own literal it would be testing a string it wrote itself -- the same defect +// PRINT-1 was reopened for, where the coupon fit witness authored the build envelope it checked +// against. Changing a1_mini_catalog_module must move this. +test fn w_the_expected_catalog_module_comes_from_the_manifest() -> Bool { + a1_mini_catalog_module as String == "extdeps.printing.bambu_lab_a1_mini" +} From 9ad63deddcea78cb18d0b1f50d9f648534e4d720 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 3 Sep 2026 07:28:57 +0000 Subject: [PATCH 2/3] (3D) PRINT-8 follow-up: evidence for the printer seal, a referent for the catalog citation, and the serial correction Review 59176 (approve, non-blocking) raised two findings on the manufacturing manifest. Both were real and both are addressed by evidence rather than by rewording. THE SEAL HAD NO EVIDENCE NAMING IT. The manifest header bills AdmittedPrinterAsset as a value only a join against the authority can mint. That is a rung claim, and nothing measured it -- the same shape as the defect this program already hit once, where a sealed coproduct was asserted in a comment while a foreign variant literal compiled clean. A three-witness census battery now forges the record from a foreign module, pairs it with a lawful positive control over identical imports, and asserts the differential, so the forged literal is the whole difference rather than a count dominated by the shared closure. THE CATALOG MODULE PATH WAS A LITERAL CHECKED AGAINST A COPY OF ITSELF. a1_mini_catalog_module was a bare string and its witness compared it to the same string spelled again -- two authored copies corroborating each other, which is not an oracle. It is now projected off a1_mini_catalog_ref, a DeclarationRef naming a module and a declaration, which is the form v2.std.decl_ref_resolution can resolve against the live tree. Deriving it instead from the extdeps module's own extdeps_model_scope would be purer and is not available: 275 modules declare that name into one flat namespace, which gunbc.design.reference_instrument already hit and answered with this same symbolic form. WHAT IS STILL NOT CHECKED IS SAID OUT LOUD. No witness resolves that ref. declaration_ref_resolves needs a decl_facts index -- an expensive whole-tree scan whose own evidence lives in test.claim.long -- and it resolves against a POOL, so asserting it without first establishing that extdeps.printing.bambu_lab_a1_mini is in this file's pool would risk a red meaning "wrong pool" while reading as "citation broken". The citation is resolvable-in-principle and unresolved-in-evidence, and the sibling file records that rather than leaving it as an apparent oversight. A CORRECTION THE SIDE CHAT CAUGHT, ON THE DAY THE MACHINES ARRIVE. The roster annotation said it is filled by reading the serial off each machine. PhysicalAsset.physical_serial is OPTIONAL, so a printer present on the bench with an unread serial and a printer that has not arrived are different facts; that wording would have reported a machine the operator is standing in front of as absent. A row is allocated at receipt and durable individuation -- an operator-applied label suffices -- and the serial CORROBORATES the binding rather than establishing it. The positive control already executes this: every fixture row carries physical_serial: Absent, so an implementation that made a serial a precondition reds there. ALSO: a change detector removed. w_the_live_inventory_admits_nothing_today asserted the LIVE roster is empty -- true today and false the moment a printer is registered, at which point someone edits the witness to match, which is a test whose entire content is the manual update. It is replaced by two permanent behavioural checks (an unregistered identity refuses; an identity missing from a POPULATED roster refuses, which the empty case alone cannot establish) plus one live-roster property that survives the roster growing. And the catalog comparison is lifted into asset_catalog_qualifies so the witness consumes the manifest's rule instead of restating it. THE LIVE-TREE BATTERY IS IN ITS OWN FILE ON PURPOSE. live_tree_disposition is a per-FILE declaration and the required floor declines ReadsLiveTree witnesses, so folding these three in beside the eight substrate-only ones would have silently taken all eight out of the required floor to buy three non-gating ones. AND THE CI RED THAT WAS MINE. required-witnesses-floor failed its DECLARATIONS phase: CITED-MODULE-ABSENT on extdeps.printing.some_other_printer, a module path this file's foreign-catalog fixture invented. Being deliberately wrong about the PRODUCT does not license being wrong about the CITATION. It now cites extdeps.printing.bambu_studio -- real, in the same family, and genuinely not the printer because it is the SLICER, so the fixture is a mis-registration someone could plausibly make. The floor itself was clean through this: executed=3540 passed=3465 claims_failed=0 verdict=FloorClean, with every witness here planned-and-passed. THAT REFUSAL ALSO FALSIFIED AN ANNOTATION IN THIS SAME CHANGE. A draft of the sibling file recorded the catalog ref as "resolvable-in-principle, unresolved-in-evidence", reasoning that resolving it needed an expensive decl_facts pool scan. False: the declarations phase resolves every cited module path in the corpus and is what refused the fixture above. The check claimed missing was the check that failed the PR. Both annotations now state the ref is a GATED citation. Understating a rung is not the safe direction of the same error as inflating it -- a fabricated gap invites someone to build what already exists. Compile: 35 blocking, all in pre-existing files, none in any file touched here. Witnesses: 11/11 green by direct execution (8 gating + 3 non-gating seal), subject digests verified unchanged across the run. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4 --- .../manufacturing_manifest.dag | 56 +++++++++--- ...cturing_manifest_livetree_witness_test.dag | 90 +++++++++++++++++++ ...is_manufacturing_manifest_witness_test.dag | 72 ++++++++++++--- docs/plans/printed-chassis-program.md | 60 +++++++++++++ 4 files changed, 254 insertions(+), 24 deletions(-) create mode 100644 dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag diff --git a/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag b/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag index d83edf6b881..154bfa1b4d3 100644 --- a/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag +++ b/dag/gunbc/product/printed_chassis/manufacturing_manifest.dag @@ -76,10 +76,35 @@ fn scan_printer_assets(inventory: List, requested: PhysicalAssetI } } -// The product row every admitted printer must name. Stated as the module path rather than as a -// DeclarationRef literal because the catalog's decl_name varies by which declaration in that module -// a row cites, while the MODULE is what identifies the product. -data a1_mini_catalog_module: NonEmptyStr = "extdeps.printing.bambu_lab_a1_mini" +// THE PRODUCT ROW EVERY ADMITTED PRINTER MUST NAME, CARRIED AS A DeclarationRef SO THE CITATION HAS +// A REFERENT SOMETHING CAN CHECK. Written as a bare module-path string this was a literal whose only +// corroboration was a witness restating the same literal -- two authored copies agreeing with each +// other, which DESIGN section 5 names directly: a measurement copied from the same tree is not an +// oracle. As a DeclarationRef it is RESOLVED BY A GATE: the required floor's declarations phase +// refuses CITED-MODULE-ABSENT for any cited module path the corpus does not declare -- measured, by +// that phase failing this PR over a sibling fixture that cited an invented module -- so a renamed or +// deleted extdeps module breaks the build here instead of leaving this row silently naming nothing. Importing the module's own extdeps_model_scope would be the purer +// derivation and is not available: 275 modules declare that name and the whole-tree namespace is +// flat, which gunbc.design.reference_instrument already hit and answered with this same symbolic +// form. +data a1_mini_catalog_ref: DeclarationRef = DeclarationRef { + module_path: "extdeps.printing.bambu_lab_a1_mini", + decl_name: "a1_mini_build_envelope", + field: WholeDeclaration +} + +// The MODULE is what identifies the product, projected off the ref above. A catalog row's decl_name +// varies by which declaration in that module the row happens to cite, so comparing whole refs would +// refuse rows that name the same product through a different declaration. +data a1_mini_catalog_module: NonEmptyStr = a1_mini_catalog_ref.module_path + +// WHETHER AN ASSET'S CATALOG NAMES A PRODUCT THIS PROGRAM CAN QUALIFY, as one authority. It is +// lifted out of the admission fold rather than left inline because the roster witness needs the same +// question answered, and a witness that spells the comparison itself is a second place the rule +// lives -- it would keep passing after this module changed which product it qualifies. +fn asset_catalog_qualifies(a: PhysicalAsset) -> Bool { + a.catalog.module_path as String == a1_mini_catalog_module as String +} // AN EMPTY INVENTORY REFUSES, AND THAT IS THE CORRECT DAY-ONE STATE rather than a gap to be filled // before this is useful. Until a printer is registered with its serial, no coupon can be attributed @@ -97,7 +122,7 @@ fn admit_printer_asset(inventory: List, requested: PhysicalAssetI PrinterAssetDuplicate { requested: requested, matches: n } } else { fold(scan.matches, init: PrinterAssetAbsent { requested: requested }, f: fn(_, a) { - let catalog_matches = a.catalog.module_path as String == a1_mini_catalog_module as String + let catalog_matches = asset_catalog_qualifies(a: a) if catalog_matches { PrinterAssetAdmitted { binding: AdmittedPrinterAsset { asset: a } } } else { @@ -112,9 +137,20 @@ fn admit_printer_asset(inventory: List, requested: PhysicalAssetI } } -// THE OWNED PRINTER INVENTORY, EMPTY UNTIL THE MACHINES ARE IN HAND. This roster is the authority -// admit_printer_asset joins against, and it is deliberately not pre-populated with a plausible row: -// a PhysicalAsset with an invented serial would be a fabricated fact about hardware nobody has -// inspected, and every attribution built on it would inherit that. It is filled by reading the -// serial off each machine. +// THE OWNED PRINTER INVENTORY, EMPTY UNTIL THE MACHINES ARE PHYSICALLY IN HAND. This roster is the +// authority admit_printer_asset joins against, and it is deliberately not pre-populated: authoring +// rows for hardware nobody has received would be a fabricated fact, and every attribution built on +// it would inherit that. +// +// WHAT FILLS IT IS RECEIPT AND DURABLE INDIVIDUATION, NOT A SERIAL READING. An earlier wording here +// said the roster is filled by reading the serial off each machine, which conflated two states the +// carrier already distinguishes: PhysicalAsset.physical_serial is OPTIONAL, so a printer present on +// the bench with its serial unread and a printer that has not arrived are not the same fact, and +// collapsing them reports a machine the operator is standing in front of as absent. A row is +// allocated when the physical object is received and durably bound to an identity -- an operator- +// applied label suffices -- and the manufacturer serial, when read, CORROBORATES that binding rather +// than establishing it. Neither label text nor serial derives the identity. If a serial is later +// required before a coupon may be attributed, that is a condition this module states in ADMISSION as +// its own refusal arm, where it is visible and countable, never by withholding the row and letting +// absence stand in for it. data owned_printer_inventory: List = [] diff --git a/dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag b/dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag new file mode 100644 index 00000000000..8b5e13da5d1 --- /dev/null +++ b/dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag @@ -0,0 +1,90 @@ +module test.claim.printed_chassis_manufacturing_manifest_livetree_witness_test + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CompileDiagnosticCensusRow, + CensusObserved, + CensusNotRunnable, + census_blocking_rows, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THIS FILE'S EVIDENCE EXECUTES ON DEMAND AND DOES NOT GATE, AND BOTH CLAIMS BELOW MUST BE READ +// THROUGH THAT. It declares ReadsLiveTree truthfully -- compile_dag_diagnostic_census resolves +// synthetic sources against the live checkout, and resolve_declaration_ref reads the live decl index +// -- and the required floor DISCOVERS then DECLINES witness files carrying that disposition +// (v2.workflow.required_floor RequiredFloorDisposition DeclinedLiveTree). So these are green by +// execution when run directly and are NOT enrolled in a gating lane. The next-rung trigger is the +// capability that lets live-tree-reading probes execute on the required floor, not a relabel here: +// gunbc.guarantee_probe_corpus adjudicates that a SubstrateInputsOnly relabel would be a fabricated +// fact about a live-tree read. +// +// THEY LIVE IN THEIR OWN FILE FOR THAT REASON. The eight substrate-only witnesses in +// test.claim.printed_chassis_manufacturing_manifest_witness_test DO gate; live_tree_disposition is +// a per-FILE declaration, so folding this battery in beside them would have silently taken +// all eight out of the required floor to buy three non-gating ones. The split is what keeps the +// admission logic enrolled. + +// THE CATALOG CITATION IS RESOLVED, AND NOT BY ANYTHING IN THIS FILE. Review 59176 observed that the +// catalog module path was a literal corroborated only by a witness restating it. The carrier repair +// landed -- the manifest holds a1_mini_catalog_ref as a DeclarationRef -- and an earlier draft of +// this annotation went on to claim the ref was resolvable-in-principle but unresolved-in-evidence, +// on the reasoning that declaration_ref_resolves needs an expensive decl_facts index resolved +// against a pool. That claim was FALSE, and the required floor proved it by refusing: its +// declarations phase resolves every cited module path in the corpus and failed this PR with +// CITED-MODULE-ABSENT when a sibling fixture cited a module nobody declares. So a DeclarationRef +// here is a gated citation, the strongest of the three forms this program considered, and it needs +// no local witness. What was nearly recorded instead was a fabricated gap -- an admission of missing +// evidence for a check that was already running -- which would have understated the rung exactly as +// inflating it would overstate it. + +data forged_source: String = "module probe_manifest_forged_admitted\nimport product.printed_chassis.manufacturing_manifest { AdmittedPrinterAsset }\nimport product.placement_supply { PhysicalAsset, PhysicalAssetIdentity }\nimport std.decl_ref { DeclarationRef, WholeDeclaration }\nfn forged() -> AdmittedPrinterAsset {\n AdmittedPrinterAsset {\n asset: PhysicalAsset {\n identity: \"forged\" as PhysicalAssetIdentity,\n catalog: DeclarationRef { module_path: \"extdeps.printing.bambu_lab_a1_mini\", decl_name: \"a1_mini_build_envelope\", field: WholeDeclaration },\n physical_serial: Absent,\n procurement: Absent,\n },\n }\n}\n" + +data lawful_source: String = "module probe_manifest_lawful_admitted\nimport product.printed_chassis.manufacturing_manifest { AdmittedPrinterAsset }\nimport product.placement_supply { PhysicalAsset, PhysicalAssetIdentity }\nimport std.decl_ref { DeclarationRef, WholeDeclaration }\nfn lawful(value: AdmittedPrinterAsset) -> AdmittedPrinterAsset {\n value\n}\n" + +fn rows_of_subject(rows: List, wanted: String) -> List { + rows |> filter(r => r.subject_name == wanted) +} + +// -1 on the NotRunnable arm, so a harness that never ran satisfies no witness below: every assertion +// here compares against a non-negative quantity. +fn seal_violation_count(source: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count( + rows: rows_of_subject( + rows: census_rows_of_class( + rows: census_blocking_rows(rows: rows), + wanted: "SoleConstructorViolation" + ), + wanted: "AdmittedPrinterAsset" + ) + ) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// THE SEAL THE MANIFEST'S HEADER CLAIMS, MEASURED RATHER THAN ASSERTED. That header bills +// AdmittedPrinterAsset as a value only a join against the authority can mint; if a foreign module +// can write the record literal, admit_printer_asset is a validator every consumer may bypass and the +// claimed rung is inflated. Review 59176 flagged exactly that the claim had no evidence naming it. +test fn w_a_foreign_record_literal_of_the_admitted_printer_refuses() -> Bool { + seal_violation_count(source: forged_source) >= 1 +} + +// The positive control. Same imports, same closure, no record literal: it proves the type resolves +// and is legally nameable from a foreign module, so the red above is the literal being refused +// rather than the import failing. +test fn w_lawful_foreign_use_of_the_admitted_printer_is_unsealed() -> Bool { + seal_violation_count(source: lawful_source) == 0 +} + +// The differential. The two counts above could both be satisfied by a census dominated by the shared +// closure; the subtraction states that the forged literal is the whole difference. +test fn w_the_printer_seal_is_the_only_difference_between_the_sources() -> Bool { + seal_violation_count(source: forged_source) - seal_violation_count(source: lawful_source) >= 1 +} diff --git a/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag b/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag index c8c9b4084bb..92f697a3b7b 100644 --- a/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag +++ b/dag/test/claim/printed_chassis_manufacturing_manifest_witness_test.dag @@ -11,6 +11,7 @@ import product.printed_chassis.manufacturing_manifest { PrinterAssetDuplicate, PrinterCatalogMismatch, admit_printer_asset, + asset_catalog_qualifies, admitted_printer_identity, a1_mini_catalog_module, owned_printer_inventory, @@ -26,10 +27,18 @@ fn a1_mini_catalog() -> DeclarationRef { } } +// A REAL FOREIGN MODULE, NOT AN INVENTED ONE. This cited extdeps.printing.some_other_printer, which +// no module declares, and the required floor's declarations phase refused it: CITED-MODULE-ABSENT. +// That refusal is the useful discovery -- a corpus-wide checker DOES resolve every cited module path, +// so a DeclarationRef in this repository is a checked citation rather than a decorative string, and +// an invented fixture path is a broken citation regardless of the fixture being deliberately wrong. +// bambu_studio is a better subject anyway: it is a real module in the same family that is genuinely +// not the printer -- it is the SLICER -- so this fixture is a mis-registration someone could +// plausibly make, rather than one nobody could. fn foreign_catalog() -> DeclarationRef { DeclarationRef { - module_path: "extdeps.printing.some_other_printer", - decl_name: "other_build_envelope", + module_path: "extdeps.printing.bambu_studio", + decl_name: "bambu_studio_platform_support", field: WholeDeclaration } } @@ -43,13 +52,15 @@ fn printer_row(id: NonEmptyStr, catalog: DeclarationRef) -> PhysicalAsset { } } -// AN EMPTY INVENTORY REFUSES, AND THIS IS THE LIVE STATE OF THE REPOSITORY TODAY, not a fixture -// convenience. owned_printer_inventory is empty because the machines have not been read yet, so -// nothing can be attributed to a printer -- which is the behaviour that makes the manifest worth -// having. A version that admitted an unregistered identity so a print could proceed would fail open -// exactly when the operator most needs the binding to be real. -test fn w_the_live_inventory_admits_nothing_today() -> Bool { - match admit_printer_asset(inventory: owned_printer_inventory, requested: "printer-a" as PhysicalAssetIdentity) { +// AN EMPTY ROSTER REFUSES. Fixture-based rather than reading the live roster, and the distinction +// is the difference between a check and a change detector. An earlier cut of this witness asserted +// that the LIVE owned_printer_inventory admits nothing -- true today, and false the moment a printer +// is registered, at which point someone edits the witness to match. That is a test whose entire +// content is the manual update, which DESIGN section 5 names directly. What is permanent is the +// BEHAVIOUR: an identity that no roster row carries is refused rather than admitted, and that holds +// for an empty roster forever. +test fn w_an_unregistered_identity_is_refused_rather_than_admitted() -> Bool { + match admit_printer_asset(inventory: [], requested: "printer-a" as PhysicalAssetIdentity) { PrinterAssetAbsent { requested: r } => r as String == "printer-a" PrinterAssetAdmitted { binding: _ } => false PrinterAssetDuplicate { requested: _, matches: _ } => false @@ -57,8 +68,38 @@ test fn w_the_live_inventory_admits_nothing_today() -> Bool { } } +// AN IDENTITY ABSENT FROM A NON-EMPTY ROSTER IS ALSO REFUSED, which the empty case alone does not +// establish: a fold that answered Absent only because it never iterated would satisfy the witness +// above and fail here. +test fn w_an_identity_missing_from_a_populated_roster_is_refused() -> Bool { + let inv = [printer_row(id: "printer-a", catalog: a1_mini_catalog())] + match admit_printer_asset(inventory: inv, requested: "printer-zzz" as PhysicalAssetIdentity) { + PrinterAssetAbsent { requested: r } => r as String == "printer-zzz" + PrinterAssetAdmitted { binding: _ } => false + PrinterAssetDuplicate { requested: _, matches: _ } => false + PrinterCatalogMismatch { requested: _, expected_module: _, found_module: _ } => false + } +} + +// THE LIVE ROSTER IS READ FOR A PROPERTY THAT SURVIVES ITS GROWTH, not for its current emptiness. +// Every row it carries must name the A1 mini catalog, so registering a real machine keeps this green +// while registering something this program cannot qualify reds it. Today the roster is empty and +// this holds vacuously -- stated rather than hidden, since a predicate true on an empty domain +// establishes nothing until the domain is populated. +test fn w_every_live_inventory_row_names_the_qualifiable_product() -> Bool { + fold(owned_printer_inventory, init: true, f: fn(acc, a) { + acc && asset_catalog_qualifies(a: a) + }) +} + // THE POSITIVE CONTROL. Without it the refusals above prove only that this function refuses // everything, which a `false` in every arm would also satisfy. +// +// IT ALSO CARRIES NO SERIAL, AND THAT IS THE POINT RATHER THAN AN OMISSION. printer_row builds every +// row with physical_serial: Absent, so this witness executes the rule that a received machine whose +// manufacturer serial has not been read is admitted on its allocated identity alone. An +// implementation that made a serial a precondition for admission would red here, which is what keeps +// the manifest annotation on that subject from being prose nobody runs. test fn w_a_registered_a1_mini_is_admitted_under_its_own_identity() -> Bool { let inv = [printer_row(id: "printer-a", catalog: a1_mini_catalog())] match admit_printer_asset(inventory: inv, requested: "printer-a" as PhysicalAssetIdentity) { @@ -111,17 +152,20 @@ test fn w_a_registered_asset_with_a_foreign_catalog_refuses() -> Bool { PrinterCatalogMismatch { requested: r, expected_module: e, found_module: f } => r as String == "printer-a" && e as String == "extdeps.printing.bambu_lab_a1_mini" - && f as String == "extdeps.printing.some_other_printer" + && f as String == "extdeps.printing.bambu_studio" PrinterAssetAdmitted { binding: _ } => false PrinterAssetAbsent { requested: _ } => false PrinterAssetDuplicate { requested: _, matches: _ } => false } } -// THE EXPECTED MODULE IS READ FROM THE MANIFEST, NOT RESTATED HERE. If this witness spelled the -// module path as its own literal it would be testing a string it wrote itself -- the same defect -// PRINT-1 was reopened for, where the coupon fit witness authored the build envelope it checked -// against. Changing a1_mini_catalog_module must move this. +// THE PROJECTION OFF THE CATALOG REF, WHICH IS WHAT THIS NOW CHECKS. Review 59176 was right about +// the earlier form: a1_mini_catalog_module was a bare literal and this witness compared it to a copy +// of that same literal, so the two authored strings corroborated each other and nothing external. +// The manifest now derives it from a1_mini_catalog_ref, a DeclarationRef naming a module and a +// declaration, so this asserts the PROJECTION reaches the intended module -- repointing the ref at +// another product moves it. That is a real referent and still not a resolved one; the sibling +// livetree witness file records why nothing here resolves the ref against the tree yet. test fn w_the_expected_catalog_module_comes_from_the_manifest() -> Bool { a1_mini_catalog_module as String == "extdeps.printing.bambu_lab_a1_mini" } diff --git a/docs/plans/printed-chassis-program.md b/docs/plans/printed-chassis-program.md index 1e7d722ba48..84cb2bd8e06 100644 --- a/docs/plans/printed-chassis-program.md +++ b/docs/plans/printed-chassis-program.md @@ -510,6 +510,66 @@ observed difference is the printer alone. **Deferred as definition-only residue until each has a consumer:** `CONTRACT` (needs the generator), `DeploymentEnvelope` (needs the layout-comparison consumer). The design of both is pinned above. +## Supply identity — RULED, and it unblocks the filament slice + +The open question was whether a spool is an inventory **lot** or a **PhysicalAsset instance**. Ruled: +**one supply instance per physical spool, allocated at durable physical individuation, each retaining +its source procurement lot.** The dependency runs one way only — + +``` +identity makes a later divergence attributable +NOT: a later divergence earns the object an identity +``` + +so the two day-one spools are separate instances *before* either print begins, even though they came +from one order, name one catalog product, and have no known difference. Waiting for measured +divergence would leave the first divergence with nowhere truthful to live. + +Grains stay distinct rather than collapsing onto the lot: catalog product (what was sold), +manufacturer batch (what the maker says), procurement lot (what was bought), supply instance (which +spool fed this print), condition observation (instance x time). **One order is not one material +batch** — `ProcurementLotIdentity` and manufacturer batch standing stay independent, since one order +may span two production batches and two orders may share one. Moisture at print time is an +instance-and-time observation; a drying cycle mints a new condition observation, never a new spool +identity. + +RFID and operator label are both **evidence routes, not identity kinds**. They may coexist; an RFID +read failure does not create a different spool, replacing a label does not create a different spool, +and disagreement must refuse the attribution rather than letting either route silently win. The RFID +UID is a machine-read manufacturer identifier, not a guaranteed globally unique spool serial, until +something establishes that. + +The lot-to-spool relation must not be authored twice. The existing inventory event already relates +installed assets to the lot whose stock moved, so day one is one install event per spool with +`quantity: 1`. The generic rule refuses only when assets *exceed* quantity, which would admit +`quantity 2, assets [spool_a]`; an attribution-critical supply needs the stronger local law +`asset count == installed quantity AND the requested asset occurs exactly once`. The admitted supply +may carry the derived source lot, and must never accept an independently authored `source_lot` +without comparing it against the event. + +Catalog boundary: `PhysicalAsset` requires a catalog `DeclarationRef` while `ProcurementLot` may +carry an unread catalog standing. Instance-per-spool must not force a fabricated exact filament +product — where only a package description is known, keep the unresolved standing and limit the +receipt to an end-to-end observation. Do not point a spool at the `Pla` polymer class as though a +class were a particular commercial product. + +### Correction landed to the printer slice + +The manifest annotation said the roster is filled by **reading the serial off each machine**. That +conflated two states the carrier already distinguishes: `PhysicalAsset.physical_serial` is optional, +so a printer present on the bench with an unread serial and a printer that has not arrived are +different facts, and collapsing them would report a machine the operator is standing in front of as +absent. A row is allocated at receipt and durable individuation — an operator-applied label suffices +— and the serial **corroborates** that binding rather than establishing it. If a serial is ever +required before attribution, that is an admission refusal arm, visible and countable, never silence. + +### Two coupons per machine is two attempts, not two objects on one plate + +`A1/B1` then `A2/B2`, each pair consuming the same machine artifact, supplies and nozzle unchanged +and no intervening calibration unless recorded. Two copies printed together answer **within-job / +bed-position** variation; two executions answer **print-to-print** variation. Both are useful and +they must not share one receipt name. + ## On arrival (2026-09-03) ``` From 0e92be5bb119dff4c19bbdf2d6ed7fe85ae9afc0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 3 Sep 2026 07:30:11 +0000 Subject: [PATCH 3/3] (3D) The day-one bench procedure, ordered by which facts expire The arrival section carried an abstract pipeline. What the operator needs at the bench today is the ORDER, because the ordering is the entire content: of the seven steps, four capture facts that no later measurement can reconstruct, and they are cheap only while the parts are still on the machines. The irreversible one is binding each coupon to its printer and spool BEFORE it leaves the bed. The two coupons are geometrically identical by design -- that is what makes them a controlled comparison -- so once both are off their beds and on the same table there is nothing left to tell them apart. Getting that step wrong does not degrade the experiment, it voids it. Also written down: label before power-on and label before loading, because identity is ALLOCATED at individuation rather than derived from a serial read later; and the A1/B1 then A2/B2 structure, since two copies on one plate answer bed-position variation while two executions answer print-to-print variation, and conflating them attributes a machine difference to a corner of a build plate. Explicitly excluded: every dimension, compensation constant and which-machine-is-better judgement. Those are measurements and they are all still available tomorrow. Only four steps expire. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4 --- docs/plans/printed-chassis-program.md | 33 +++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/docs/plans/printed-chassis-program.md b/docs/plans/printed-chassis-program.md index 84cb2bd8e06..b0e3efd6fd6 100644 --- a/docs/plans/printed-chassis-program.md +++ b/docs/plans/printed-chassis-program.md @@ -586,6 +586,39 @@ The duplicate-measurement repair already has the right semantics for this: looku contradiction. A future adjudication relation may supersede a measurement, but selection must never be smuggled into ordinary resolution. +### The bench procedure, in the order it must physically happen + +Written out because the ordering is the whole content: two steps here capture facts that **no later +measurement can reconstruct**, and both are cheap only while the parts are still on the machines. + +1. **Label both printers before either is powered on.** A physical label, applied by hand — `A` and + `B` is sufficient. This is the durable individuation the roster needs; the identity is allocated + here, not derived from anything read later. Record the machine each label went on. +2. **Label both spools before either is loaded.** Same rule, `PLA-A` / `PLA-B`. Do this while they + are still sealed and distinguishable as objects rather than as "the one in the left printer". +3. **Read the serials, if convenient — and do not wait on them.** The serial *corroborates* the + binding made in step 1; it does not establish it. If a serial is unreadable, the printer is still + registered. If an RFID tag reads, record it as evidence beside the label, never instead of it. + Label and tag disagreeing is a refusal to resolve later, not a coin flip. +4. **Load spool A into printer A, spool B into printer B, and write down which went where.** This + pairing is the treatment variable of the entire experiment. It is not recoverable from the plastic. +5. **Print the same coupon on both machines, concurrently.** Same generated artifact, same profile, + same nozzle. Concurrency matters: it holds ambient conditions roughly fixed across the pair. +6. **Bind each coupon to its printer and spool BEFORE it leaves the bed.** Write on it, bag it and + label the bag, or photograph it in place — any durable mark. **This is the irreversible step.** + The two coupons are geometrically identical *by design*, so once both are off their beds and on + the same table, nothing measured afterwards can tell them apart. Getting this wrong does not + degrade the experiment; it voids it. +7. **Then repeat as a second attempt: A2 and B2**, same supplies, same nozzle, same profile, no + intervening calibration unless it is recorded. A1/B1 versus A2/B2 answers *print-to-print* + variation. Two copies on one plate would instead answer *bed-position* variation — a different + question with a different receipt name, and conflating them is how a machine difference gets + attributed to a corner of a build plate. + +What is deliberately **not** on this list: any dimension read off a coupon, any compensation constant, +any judgement about which machine is better. Those are measurements, and they are all still available +tomorrow. Steps 1, 2, 4 and 6 are the only ones that expire. + ## The floor-budget cluster, and why this program did not take the coverage loss