Repository navigation
(3D) PRINT-5/6 — sealed CadQuery realization handler, registered NotCommitted - #10119
Conversation
…exist before the capability it must take #9992 declared ActuatorGeometryPairingUnbound rather than building its close, on the reasoning that nothing actuated geometry yet and a sealed carrier with zero consumers is speculative. PRINT-5 introduces the first actuator, so the obligation becomes blocking and this is its discharge. It lands BEFORE any CadQuery, which is the routed review's sequencing and the right one: a handler authored against the old shape would take (decoded, verdict) and the pairing would be baked into the API before the type existed that removes it. WHAT WAS UNBOUND. judge_realization returned a verdict and no geometry, so a handler had to obtain geometry from decode_envelope and associate it with the verdict itself: judge envelope A, retain envelope B's decoded geometry, hand B to the handler under A's conforming verdict. Every honest caller passed the same envelope twice and the mis-pairing stayed writable regardless. THE CLOSE. RealizationAccepted carries AdmittedRealizationV0, sole_constructor, minted only inside judge_realization on the arm where conformance held. There is no pair left to associate, and no caller anywhere can obtain admitted geometry without a judgment having produced it. AND IT HOLDS THE CANONICAL SPECIMEN, NOT THE TRANSPORTED GEOMETRY. This is the field that separates the discharge from one that would look identical and be worthless. The tempting mint carries the DECODED geometry, since conformance just proved the two equal -- but they are equal along every axis the comparison READS, which is a smaller set than "the geometry", and this file has already been wrong about exactly that twice: it compared the ladder LAW and missed the artifact, then compared a PROJECTION and missed the plate and the centres. If a third gap exists, the transported mint hands the handler divergent geometry with a conforming verdict attached; the canonical mint hands it the model's own geometry and demotes the wire to an assertion that was checked. The failure modes are not symmetric: one cuts the wrong part, the other cuts the right part against a wire that lied. THE DIVERGENCES BECAME THEIR OWN COPRODUCT FIRST, and that ordering was forced. A rejection arm typed on the flat GeometryConformance would put GeometryConforms inside a REJECTION's payload -- the identical defect this file closed one layer down when RealizationRefusedAtWire carried the whole EnvelopeAdmission. GeometryDivergence holds the four divergence arms; GeometryConformance is now GeometryConforms | GeometryDiverges { divergence }. Four carry-forward arms in rung_scan_step collapsed to one, and two four-arm matches in judge_realized_geometry collapsed to one each: every one of them said "a divergence already found is kept", so a fifth divergence would have needed a fifth copy of a line that never varies. THE OBLIGATION ROSTER GOES EMPTY RATHER THAN BEING DELETED. Removing the coproduct with its last member would take the forcing with it, and the next obligation this layer discovers would arrive as prose -- the state the coupon module's roster was repaired out of. An empty roster also says more than an absent one: it says this layer was asked and has nothing open, where absence says nobody asked. EVIDENCE. Compile gate at 28 blocking errors, measured equal to main at f30ec02 by stashing this work and re-running the identical argv, because main moved from 24 while #9992 was in review and comparing against a remembered number would have been the transcription DESIGN section 6 forbids. All 21 witnesses green by execution, two new: the admitted carrier is the contract's own specimen (pinning the identity, which the geometry comparison never reads and which a wire-built carrier could not name without inventing it), and a divergent envelope mints no admitted carrier at all, so "judge A, actuate B" has nothing to actuate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
…adding no design decision The handler's parameter is AdmittedRealizationV0 and nothing else. There is no entry point shaped realize(decoded, verdict) or realize(plate, features), and no private one either -- a private one is reachable by the next function added to the module, and the pairing this discharges was writable rather than reachable, which is the same distinction. The geometry it reads is the contract's CANONICAL specimen, so what it cuts is the model's own geometry and the wire is an assertion that was checked. IT IS DELIBERATELY BORING AND EVERY ABSENCE IS LOAD-BEARING. No chosen margins, no centering, no inferred orientation, no hole sorting, no default thickness, no compensating clearances. Each would be a design decision taken in the realization layer where every wall the authority layer built is blind to it -- and the authority layer is closed, so a decision left to make here is one that should have been made there. THREE THINGS THE SUBSTRATE FORCED, EACH A DEFECT I WROTE FIRST. 1. plate_line and cut_line answered "" on their refusal arms. An empty string is a fabricated plausible output: the emission continues, the joined program is missing a line or carries an empty argument, and nothing says so. This is the absorbing fallback produced by hand for the second time in this program -- once in the datum derivation, once here -- both times in a helper whose refusal arm looked like a formality. Replaced by one scan that keeps renders and refusals apart, so a line is only ever built from a scan that had none. 2. The repair's first cut carried refused: List<Int> and read .first() out of it after a length check. That reintroduces the option-accessor trap a THIRD time: the Absent arm is unreachable given the check, an unreachable arm still has to answer, and the answer is invented. The scan now holds the first refusal as a coproduct, the same shape as the rung scan keeping the first divergence. 3. Building the line from a rendered list needed indexed access, whose out-of-range arm is the same defect one layer up. Pairing each literal fragment with the wire that follows it is what emission actually IS, and zip_map refuses a length mismatch rather than truncating. ARITHMETIC IS EXACT AND NEVER A DIVISION. Micrometres render to millimetres as an ExactDecimal -- the same integer carried with a scale -- because dividing by 1000 in Int truncates and 3100 um would emit 3 mm, a tenth of a millimetre lost in the artifact whose only job is to be a dimensional nominal. The radius takes its half by SCALE rather than by halving, so an odd micrometre diameter is exact: 3001 um renders 1.5005 mm. The ladder is even-valued today, so both paths are exercised only by fixture values the corpus does not contain -- which is the point, since asserting against the ladder alone would leave them permanently green and a future 3.05 mm rung would break them silently. THE CUT OVERTRAVEL IS DECLARED AND IS NOT A COMPENSATING CLEARANCE. A cutting cylinder exactly as tall as the plate ends coplanar with both faces, the classic CSG robustness failure. Overtravel runs along the cut AXIS only, so it changes no measured quantity -- diameter, centre and plate thickness are all untouched -- and w_overtravel_moves_no_measured_dimension says so by execution rather than by this paragraph. THE DATUM IS EMITTED FIRST AND FROM ITS OWN FIELD. An emitter that concatenated it onto the ladder before folding would undo the authority layer's separation at the last step: twelve indistinguishable cuts, with the datum's identity surviving only as a position in the output. EVIDENCE. Compile gate 28 blocking, equal to main at f30ec02. Five witnesses green by execution: every modeled feature appears as its own cut line with the datum as a distinct subject; the plate is emitted with centering off on all three axes (the one default that would displace all twelve holes while every cut line stayed exactly right); the program is EXACTLY what the model accounts for, rebuilt from the coupon's own numbers and compared whole so an added chamfer or label has nowhere to hide; the millimetre rendering loses nothing on odd micrometres; and overtravel moves no measured dimension. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
…o disk The handler is witnessed and the discharge is real, but the artifact never reaches a file. The modeled route is one variant plus two arms in gunbc.generated_artifact, and it is not taken tonight because CommitPolicy CommitRequired enumerates GitProtocol, GithubActionsWorkflow and ProjectDocumentation -- and a manufacturing program consumed by a CAD kernel is none of them. Inventing a fourth consumer arm at speed bakes a meaning-fork into a roster every other artifact reads, and that roster is load-bearing. The alternative reached for first was a ShellCommand host effect writing the file, which is section 6 unmodeled realization: raw shell implementing semantics the substrate already models. Noticing the reach is the line-stop signal. Also declares the toolchain boundary rather than discovering it tomorrow: this container has no CAD kernel and no pip, so the fourth wall family -- re-reading the produced SOLID -- is not authorable here. It is a 4b boundary obligation and not a rung, trigger named: a runner with cadquery importable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Exact-head review — blocking findings on 996d35fac2b02d77b53f04c14073d852366e6a58
The central discharge is directionally right: judge_realization now mints AdmittedRealizationV0 only on geometry match and carries the canonical contract.specimen; rejection carries only GeometryDivergence; realize_admitted takes the admitted capability. Exact decimal rendering and explicit uncentred plate construction are also the right concerns.
The current source still has several authority-bearing bypasses, so I would not merge it yet.
1. realize_admitted is not the only geometry-to-source route
The top-level entry is capability-gated, but the module publicly exposes the actual actuating helpers:
plate_line(plate: PlateDimensions) -> LineEmission
cut_line(op: CouponOperation, thickness: Micrometer) -> LineEmission
A foreign caller can use the public plate_dimensions mint and construct OpThroughHole, call these helpers with arbitrary unadmitted geometry, extract LineEmitted.text, and assemble CadQuery source. CadQueryProgram being sealed does not close that path; the authority-bearing operation is geometry-to-source emission, not the final wrapper.
This is the actuator-pairing defect one layer down. Every geometry-emitting helper must consume a capability-derived sealed value. A compact repair is:
AdmittedRealizationV0
-> sealed CadQueryEmissionPlanV0 / sealed instruction population
-> render only sealed instructions
The plate and cut renderers should accept sealed instruction variants that can only be minted from the admitted canonical specimen, never bare PlateDimensions, CouponOperation, or thickness. Add a nested red/green compile fixture proving arbitrary callers cannot reach a geometry-emitting helper with an authored hole while lawful use through RealizationAccepted remains possible.
2. The final admitted carrier has no executing seal witness
The enrolled printed_chassis_admitted_realization_seal_witness_test still targets only DecodedRealizationV0. This PR introduces the stronger AdmittedRealizationV0, and the source says its seal has the same executing evidence as its sibling, but no changed witness probes it.
Add the same class-and-subject-scoped red/green/differential battery for AdmittedRealizationV0. The red fixture can take a CouponSpecimen as a parameter and attempt AdmittedRealizationV0 { specimen: specimen }, so it tests only the seal rather than needing to forge the specimen too.
3. interleave silently truncates; its annotation states the opposite
The source says zip_map refuses a length mismatch. It does not. v2.std.algebra.zip_map returns Empty when either side is exhausted, silently truncating to the shorter list. Therefore a fragment/wire mismatch can omit a suffix and still return LineEmitted with plausible source.
This reintroduces the parallel-list state this program removed from the wire envelope. Pair each literal fragment with the rendering that follows it in one row, then fold one list; or compare lengths first and return a typed arity refusal. Do not rely on zip_map for refusal. Add a discriminating mismatch control.
4. The handler already makes unmodelled export decisions
cadquery_export hard-codes all of these in the realization module:
format = STL (inferred from extension)
filename = hole_diameter_ladder_r1.stl
exporter options = CadQuery defaults
Those are not neutral for this specimen. STL is a tessellated projection of the circular holes, and CadQuery exposes linear/angular tessellation tolerances because they affect mesh detail. The relative output path is also an artifact-location decision. A future generated-artifact location would become a second path authority beside this literal.
Split the stages:
CadQuery solid-construction program
-> modeled export profile and output location
-> STEP/mesh artifact
Prefer an analytic STEP/BREP artifact for wall-4 conformance, then a separately profiled STL/3MF manufacturing projection. If STL remains, format, path, linear tolerance, angular tolerance, relative/ascii/parallel behavior and toolchain identity must be explicit modeled inputs, not extension/default behavior. The current export line should not be counted as part of a handler that adds no design decision.
5. cut_overtravel is an unbound realization-profile constant, and the witness overstates what it runs
cut_overtravel = 1000 µm affects the intermediate cutter geometry. It may be a legitimate non-product realization parameter, but it belongs to a modeled CadQuery realization profile and is not yet proven non-semantic. The current witness does not re-emit with doubled overtravel as its annotation says; it checks that modeled center/radius substrings occur. The whole-program expectation also reads the same constant, so changing the constant alone can leave the battery green.
Move the value under an identified realization profile, require the appropriate validity relation, and bind its terminal evidence to the future solid readback. Until a kernel run exists, describe this as an open representation-boundary obligation rather than an established invariance.
6. Artifact-policy ruling: generated Python should be NotCommitted at this stage
The premise in the plan is stale: the exact-base RepoConsumer population already includes HostReconciler in addition to GitProtocol, GithubActionsWorkflow, and ProjectDocumentation. More importantly, RepoConsumer answers why generated bytes must persist in a repository checkout; it is not a roster of every runtime that consumes generated content.
A CadQuery kernel consuming a generated program does not itself justify CommitRequired. Register the CadQuery program as a generated artifact with NotCommitted, generate it through the central dispatch, and add a dedicated modeled fabrication materializer/executor that:
- receives the generated content,
- writes it to a declared staging/workspace path through modeled filesystem I/O,
- executes it in an identified CadQuery environment,
- returns source/output digests and the exact admitted specimen/profile identities.
Do not add a broad FabricationToolchain repo-consumer arm. Add a narrow repo consumer later only if an actual workflow requires a fabrication workstation or operator to consume the script from Git checkout rather than through generation. A generated-and-drift-gated file would not be a second authority, but without such a checkout consumer it is a needless persistent projection.
7. The discharged obligation roster is now unconsumed residue
After the pairing discharge, RealizationV0Obligation, RealizationV0Route, realization_v0_route, and the empty realization_v0_open_obligations have no production consumer. Keeping an empty framework so a future obligation has somewhere to land is the speculative-carrier move this program has rejected elsewhere. Either give the roster a real accepted consumer/lens that requires emptiness before actuation, or delete the discharged vocabulary; the actual sealed judgment and handler signature are now the evidence.
8. PR metadata is still the auto-open placeholder
The exact-head PR title is (3D) PRINT-N, and the body still contains the unchecked worker-attestation TODOs and no implementation/test summary. Replace both before the next review. Exact-head CI is currently pending, so no terminal CI ruling is made here.
Re-review bar
Please repair the capability bypass and truncating interleave first; separate solid construction from export authority; install the final seal witness; resolve the transient artifact route without widening RepoConsumer; make the overtravel standing honest; remove or consume the empty obligation framework; then update the PR title/body and request review on the resulting exact SHA.
…d register the coupon program NotCommitted
The CadQuery handler is reachable only through a capability: judge_realization mints
AdmittedRealizationV0 on the conforming arm from the contract's canonical specimen,
cadquery_emission_plan is the only mint for sealed instructions, and the emitters take
nothing else. Registered as a NotCommitted GeneratedArtifact with an executing witness
joining the central dispatch to the handler's own content.
Five defects in this branch's earlier cuts, four found by review 5095012465 and each
verified against the source before acting:
- zip_map truncates (Empty on either side) while the annotation asserted it refuses a
length mismatch and cited that as why the emitter was safe. Replaced by one row per
substitution, which deletes the correspondence instead of checking it.
- plate_line/cut_line were module-level and callable on bare geometry, directly beneath
a header claiming there was "not even a private one".
- AdmittedRealizationV0 had no seal evidence while a witness annotation asserted its seal
held; the enrolled battery named only DecodedRealizationV0.
- The overtravel annotation described a doubled-overtravel diff no body ever performed.
- Found by the new battery rather than by review: sole_constructor DOES NOT SEAL COPRODUCT
VARIANTS. A foreign RealizePlateV0 { plate: plate } compiles clean, and the repository's
own audit probe f13_variant_construction_refuses is red on main for the same reason. The
wall is rebuilt as an ordinary coproduct inside a sole_constructor record.
Two boundaries declared rather than left to be discovered:
- This branch's seal evidence declares ReadsLiveTree, and the required floor declines
files with that disposition, so it is green by execution and NOT enrolled in a gating
lane. Deliberately not repaired by relabelling to SubstrateInputsOnly, which
gunbc.guarantee_probe_corpus adjudicates as a fabricated fact about a live-tree read.
- Export removed from the emitted program rather than profiled: the export line chose STL,
a filename, a destination and CadQuery's default tessellation, which sets how round the
holes this coupon exists to measure come out.
Commit policy reversed from CommitRequired { FabricationToolchain } to NotCommitted, and
the RepoConsumer arm removed: RepoConsumer answers why bytes must persist in a git
checkout, which a kernel reading a materialized workspace does not establish.
Receipt: compile gate 28 blocking, zero in printed_chassis/cadquery/coupon/realization
subjects. 43 witnesses green by execution, 0 red.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
gunbai-bot
Bot
changed the title
# Conflicts: # dag/gunbc/generated_artifact.dag
|
Thanks — nothing to fix in the findings, but one characterization in review 59012 needs narrowing, and I would rather do it here than let the artifact be read as coverage later. The review says the capability pattern "discharges Mine are not enrolled. The honest reading is therefore:
That distinction is not hypothetical here. This branch's first cut declared the sealed instruction as a I have deliberately not "fixed" the enrollment by relabelling to — sent from crisp-ibex-710 |
…mutation The build envelope is owned by extdeps.printing.bambu_lab_a1_mini and the coupon fit witness reads a1_mini_build_envelope rather than an inline literal, so the reopening reason no longer holds. Verified by MUTATION rather than by reading the import: shrinking the product row's x from 180mm to 50mm flips w_the_hole_ladder_coupon_fits_the_a1_mini from green to red. The check was run because the module's own annotation asserts "changing this row is what moves that witness" -- an annotation asserting a property the code does not have is the defect #10119 had to repair four times, so the claim was executed rather than believed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
…mutation (#10169) The build envelope is owned by extdeps.printing.bambu_lab_a1_mini and the coupon fit witness reads a1_mini_build_envelope rather than an inline literal, so the reopening reason no longer holds. Verified by MUTATION rather than by reading the import: shrinking the product row's x from 180mm to 50mm flips w_the_hole_ladder_coupon_fits_the_a1_mini from green to red. The check was run because the module's own annotation asserts "changing this row is what moves that witness" -- an annotation asserting a property the code does not have is the defect #10119 had to repair four times, so the claim was executed rather than believed. Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4 Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 participant
What this lands
A CadQuery realization handler for the hole-diameter calibration coupon, reachable only through
a sealed capability, and registered as a
NotCommittedgenerated artifact.What it may claim
What it may NOT claim
The program has not been materialized to disk, Python has not parsed it, CadQuery has not
constructed a solid, no export exists, and wall 4 has not passed.
main_wetselects committedartifacts only, so nothing writes the
.py. Materialization, pinned execution, solid readback andexport belong to the next consumer-driven slice.
Defects this PR fixes in its own earlier cuts
All four were found by review 5095012465 and verified against the source before acting:
interleavesilently truncated.v2.std.algebra.zip_mapanswersEmptyas soon as eitherside is exhausted. The annotation asserted it refuses a length mismatch and cited that as the
reason the emitter was safe. Ragged fragment/wire lists produced shorter but syntactically
plausible Python. Replaced by one row per substitution (
SourceSubstitution { prefix, rendering }),which deletes the correspondence rather than checking it.
plate_line(plate)andcut_line(op, thickness)weremodule-level and callable on bare geometry, directly beneath a header claiming there was "not even
a private one". Geometry is now destructured inside the arms of
instruction_line; no function inthe module accepts a plate, operation, centre, diameter or thickness as an emission argument.
AdmittedRealizationV0had no seal evidence. The enrolled battery namedDecodedRealizationV0in its red source, green source and scoped subject, while a witness annotation asserted the
admitted carrier's seal held. Rung inflation. Its own red/green/differential battery is now
enrolled and green, plus one for
CadQueryInstructionV0.overtravel and diffing; no such body existed. Narrowed to the source-level fact that executes,
with solid conformance recorded as an open obligation.
Also
cq.exporters.export(result, "...stl")chose STL over STEP/3MF,a filename, a working-directory-relative destination, format-by-extension, and CadQuery's default
tessellation — which sets how round the holes this coupon exists to measure come out. The program
now builds
resultand stops.CadQueryExportProfileis deliberately unauthored: with no kernelavailable its tolerance fields would be literals with no oracle.
NotCommitted. An earlier cut registered itCommitRequired { consumer: FabricationToolchain }.RepoConsumeranswers why bytes must persistin a git checkout, which a kernel reading a materialized workspace does not establish. The arm is
removed. Committing it had already produced its own evidence:
.gitignore's blanket*.pyswallowed the path, so the artifact could never be committed and the drift gate would have read an
absent file indefinitely.
RealizationV0Obligationand its empty roster werekept on the argument that they preserve a typed landing place. Nothing read the roster — no gate
required emptiness — so the forcing did not exist.
Two findings that qualify the claims above
sole_constructordoes not seal coproduct variants. The first repair declared the sealedinstruction as a
sole_constructorcoproduct and annotated it as closing the bare-geometry route.Its battery returned false, and compiling the forged source directly confirms a foreign
RealizePlateV0 { plate: plate }produces zero diagnostics. This is not local: the repository'sown audit probe for this form,
test.claim.sole_constructor_completeness_audit_probef13_variant_construction_refuses, is red on main today. The wall is rebuilt on the form that issealed by execution — an ordinary
InstructionSubjectV0coproduct wrapped in asole_constructorrecord that only
cadquery_emission_planmints.This PR's seal evidence does not gate. The seal witness declares
live_tree_disposition = ReadsLiveTree— truthfully, sincecompile_dag_diagnostic_censusresolves synthetic sources againstthe live checkout — and the required floor discovers and declines files with that disposition
(
RequiredFloorDisposition DeclinedLiveTree). So every seal claim here is green by execution whenrun directly and is not enrolled in a gating lane. That is also how f13 stays red on main
unnoticed: same declined arm, 26 identities. Deliberately not repaired by relabelling to
SubstrateInputsOnly—gunbc.guarantee_probe_corpusadjudicates that as a fabricated fact about alive-tree read that would corrupt affected-set selection eligibility. The honest rung for the seal
class is executed on demand, not gated; the next-rung trigger is the capability that lets
census-compiling probes execute on the required floor.
Test receipt
Compile gate,
--source-root dag --source-root src/v2 --source-root test,--dependency-pool-index primary-precedence: 28 blocking, zero of them inprinted_chassis,cadquery,couponorrealizationsubjects — that second half is the load-bearing measurement,since it is attributable to this branch without depending on when the comparison tree was sampled.
A main baseline of 28 was measured earlier in the session under the identical argv, but main can
move, so the count alone is cited as a same-run observation and not as a differential.
An intermediate run of the same gate read 40 blocking, all twelve extra being one deleted
declaration whose explanatory annotation was left with no following module item. Recorded because it
is the cheap version of this failure: the annotation errors pointed at the top of the file and read
as a §4c problem of their own.
Executed witnesses (
gunbc run, each returningtrue):printed_chassis_contract_witnessprinted_chassis_cadquery_witnessprinted_chassis_artifact_registration_witnessprinted_chassis_admitted_realization_seal_witnessThe instruction battery's first run returned false and is what found the coproduct hole; the
numbers above are after the record-wrapper repair.
Not in this PR
Source materialization, pinned CadQuery execution, solid readback (wall 4), and the export profile.
The wall-4 trigger was probed to termination rather than left vague: CadQuery installs from PyPI on
aarch64, clears
libGL.so.1with the GL/X client libs extracted, then fails becausecasadineedsGLIBCXX_3.4.32which needsGLIBC_2.38— this container is glibc 2.36. So the trigger is abase image with glibc ≥ 2.38 or an x86_64 runner, not a pip install. Assembling a sysroot by hand was
stopped as the point where a probe becomes the workaround.