Repository navigation
Deliver a sliced project to a LAN printer, refusing wherever it could have guessed - #10574
Merged
Merged
Conversation
…cked
I asserted for hours that no CadQuery kernel could exist in this container and
escalated a host decision to install one. I had never tried. The claim rested
entirely on apt needing root -- true -- which I generalized from ONE package
manager to the whole environment, and then routed around by sideloading .deb
files and pointing LD_LIBRARY_PATH at them. That is the workaround arm DESIGN
section 5 names: the obstacle was a dependency-manager CHOICE, and going around
it hid exactly the choice that needed making.
conda-forge via micromamba resolves libGL.so.1 and libX11.so.6 into a
user-owned prefix with no privilege at all. cadquery 2.8.0 imports and runs.
extdeps.package_managers.conda_forge carries that reasoning and the one solve
that provisions the prefix; extdeps.package_managers.pip makes the version
mandatory in the builder signature so no caller can land an unpinned install;
extdeps.opencascade.ocp owns the kernel as its own versioned subject, separate
from extdeps.cadquery, per the external-upstream-decomposition rule.
product.printed_chassis.cad_toolchain joins them and mints an execution plan
ONLY on the Ready arm, so holding a plan is holding proof the toolchain was
judged rather than assumed. An empty observation list refuses as Unobserved
rather than passing vacuously.
product.printed_chassis.export_profile discharges the obligation
cadquery_realization.dag filed with the trigger "a runner with cadquery
importable". That trigger has fired, so the profile is authored against
measurement instead of the seven blind literals the obligation existed to
avoid.
THREE ERRORS THE MEASUREMENT PASSED THROUGH, all of which read as evidence:
- The first tolerance study measured nothing. OCC caches a triangulation on
the shape, so five tolerances re-exported the SAME mesh and the facet count
sat at 1196 across all five. I was about to report that the linear
tolerance does not matter. Rebuilding per setting flips it to 12612. The
control that would not move WAS the finding.
- The deviations were RADIUS deviations reported under a diameter's name -- a
factor of two, in the flattering direction, on the one quantity the coupon
exists to resolve. The instrument string now records which quantity is
meant so the conflation cannot be re-entered silently.
- A 4.4 mm measurement was labelled a coupon ladder rung. The ladder runs
3.00 to 4.00 mm; 4.4 mm is the fan mount's fastener hole. Attaching the
coupon's rung spacing to it was the wrong-denominator error a second time,
wearing a subject name instead of a bare number.
Observation and requirement are separately authored and joined by subject at
adjudication, so a measurement can never carry its own pass criterion. Both fan
features land DistinctionUndeclared -- the fit the fastener hole owes an M4 and
the clearance the bore owes a fan body are unmeasured, and they refuse rather
than borrow the coupon's number.
Deliberately NOT done: retyping angularTolerance into a gunbc angle.
std.measure declines to mint a radian carrier on purpose, since a turn divides
exactly into degrees and arcseconds and a radian does not. The knob stays an
opaque upstream parameter and the safety comes from measured deviation.
std.measure gains a Nanometer carrier because the deviations are genuinely
sub-micrometre, and rounding them into micrometres would report zero -- the
safest possible value -- for exactly the cases whose margin is being claimed.
Only the widening conversion is offered; a floored chord error is an error
bound that flatters itself.
Six witnesses, all green by execution, including a 5000/5001 nanometre boundary
pair so the criterion cannot be satisfied by a constructor that always answers
"within", and a mis-join arm so a bookkeeping error is never attributed to the
mesh.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
Review findings on the parent commit, both fixed rather than annotated away:
- StlExportKnobs carried the linear tolerance as a String. Upstream documents
it in millimetres and this substrate carries lengths, so spelling it as text
merged the quantity with its realization. It is now a Micrometer, rendered
at the emit boundary as <count>e-3 -- exact, because a micrometre is exactly
one thousandth of a millimetre, and it avoids zero-padding a fractional
field where a padding bug silently changes the tolerance rather than failing
to parse. The ANGULAR knob stays text: std.measure declines to mint a radian
carrier on purpose, and that rationale never covered the linear one.
- chord_error_safety_factor was a bare 20 governing which observations refuse.
It is now a policy row with an external referent: the gaugemaker's rule, that
an instrument resolves about ten times finer than the tolerance it judges.
This repository doubles it, and the reason is falsifiable rather than
cautious -- the rule is stated for RANDOM error that partially cancels, and
an inscribed polygon undersizes every time, so the bias never averages out
and does not earn that cancellation.
THE SLICER, WHICH IS THE LAST STEP BETWEEN A VERIFIED MESH AND PLASTIC.
Debian bookworm main carries prusa-slicer, cura-engine and slic3r for arm64,
any of them one apt transaction away. None can drive the machines this
repository owns: gunbc.fleet_printer_access models Bambu Lab printers in LAN
Mode with MQTT control and an FTPS file channel, and that firmware consumes a
sliced Bambu project. Installing the convenient dependency would have produced a
toolchain that runs end to end and emits an artifact the printer rejects.
OrcaSlicer is the correct tool and publishes an aarch64 AppImage. It does not
run here, and the module says so with the measurement rather than the guess:
the artifact was fetched, extracted, and its symbol versions read directly --
floor GLIBC_2.38 against a host providing 2.36. The asset name says Ubuntu 24.04
and would have suggested 2.39; a build host's glibc is an UPPER BOUND on what a
binary may reference, never the floor it requires, so inferring from the
filename errs toward refusing hosts that work. extdeps.gnu.libc exists because a
target triple does not carry this fact, and it now carries the ordering needed
to decide it -- structured, with the string spelling DERIVED from it, so the
module's existing refusal to mint a second naming scheme still holds.
product.printed_chassis.slicing_toolchain judges the host against that floor and
mints a SlicePlan only on the runnable arm. An unobserved host refuses rather
than being assumed compatible, because the alternative buys a dynamic-linker
error at the moment of use instead of a decision at the point of decision. This
is DESIGN section 4b's boundary column: an external fact, observed and refused,
never fabricated around. The route around it -- unpacking the AppImage and
supplying newer symbols by hand -- is named in the module precisely because this
product's history already contains that move once, against the CAD kernel, and
it was rejected.
Five witnesses, green by execution. Four are paired so none is satisfiable by a
judgement that answers one way: 2.37 must refuse AND 2.38 must run, so an
off-by-one in the direction that refuses a working host is caught; a higher
major with a lower minor must still satisfy, which fails if the comparison packs
the pair into one number or reads the minor alone; and the plan must not be
minted while the floor is unmet AND must be minted when it is met.
The fifth asserts that THIS container fails the floor. It goes red when the
execution environment is fixed, which is correct: it is the declared refusal's
own regression control, and its flip is the signal to retire the refusal rather
than to edit the expectation.
REGENERATED std_measure.rs, which the parent commit drifted. The Nanometer
carrier changed std.measure without its stage0 mirror being regenerated, and the
build lane caught it. Worth recording where the recipe is, because the obvious
one is wrong: gunbc run --entry generated_artifact_gate --function main_wet does
NOT cover this population, and a whole-corpus gunbc compile refuses to write at
all while the tree carries blocking errors outside the required closure. The
mirror is produced by the build lane itself -- claim_executor --required-ci
--required-lane build -- which leaves the regenerated bytes at
target/stage0-regen-candidate. Verified by content: seventeen lines, exactly the
Nanometer type and its three functions. cargo clippy --all-targets is clean.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
Five review blockers, all real, all in the enclosing evidence and admission boundaries rather than in the arithmetic they guard. THE DENOMINATOR. admit_export_profile and judge_cad_toolchain judged whatever evidence a caller handed in, so "every standing I was given passed" was returned as "the profile is safe". A caller holding one green coupon standing and omitting both fan features received an admission. judge_cad_toolchain refused only the EMPTY observation list, so one present SONAME with the second silently omitted produced Ready -- nothing absent, nothing unobserved, among what was supplied. A short list does not look short. The worst part is that this module's own witness was EXHIBITING the hole. It removed the undeclared feature from the ARGUMENT, watched the call flip to admitted, and I read that as proof the refusal worked. Removal from the evidence was indistinguishable from removal from the intended subject. Both now judge against a DECLARED ROSTER, walked by identity, with coverage as an identity join rather than a count -- missing, foreign and duplicated as separate arms because they have separate remedies -- proven before any geometry or verdict folds. The replacement witnesses vary the ROSTER against fixed evidence, so what changes between the paired calls is the declared population. THE SEALS. CadQueryExecutionPlan and SlicePlan were minted from public coproduct arms, so any module could construct the green arm itself and hand it to the sanctioned mint. A seal proves WHO MAY MINT, never that the value handed in was earned -- the same class already met on zero-width this session and not generalized. Both now mint from a carrier only the judge produces. THE UNADJUDICATED REQUIREMENT. cad_toolchain declared pinned cadquery and cadquery-ocp, and a command to install them, then judged the toolchain on system libraries alone. A host with both SONAMEs and no importable CadQuery minted an execution plan. A requirement no observation can contradict is documentation sitting inside a gate. THE EVIDENCE BINDING. ChordObservation now carries the profile it was measured under and the admission DERIVES the profile from the standings rather than taking free knobs, so measure-under-P1-then-admit-P2 refuses. The OCC triangulation cache is why that is not hypothetical. RELATIVE DEFLECTION, which went further than the review or I expected. cq.exporters.export takes NO `relative` parameter -- I began emitting one on the review's wording and checked the signature first, which would otherwise have been a TypeError on every part. It forwards positionally to Shape.exportStl and lets relative default to True, so the linear tolerance was a FRACTION OF SHAPE SIZE while this model types it as a Micrometer. Model and emission disagreed about what the number meant. So the earlier claim that the linear knob was inert was false: it is inert only under the relative interpretation nothing had declared. Measured at one micrometre, diameter undersize -- relative 932/1243/1368/23622 nm across 3, 4, 4.4 and 76 mm; absolute 932/993/991/998. Under absolute the tolerance bounds the chord error as a length and every feature converges on it regardless of size. Emission moved to result.val().exportStl with tolerance, angularTolerance, ascii, relative and parallel all explicit, verified by executing the exact emitted call: 4852 facets against 520, volume 15466.88 against analytic 15466.88, one solid. THE SLICER, RE-MEASURED TWICE BY EXECUTION. Meeting the ABI floor is NECESSARY AND NOT SUFFICIENT, and the earlier witness asserting 2.38 "runs" overstated its own measurement. A host at 2.39 refused; then the session image moved to Debian 13 and glibc 2.41 and it refused again. HostAbiStanding and OrcaExecutionStanding are now separate and only an attempt reaches ExecutionReady. The witness asserting this container sat below the floor went RED when the image landed, which is what it was written to do. The recorded rows were re-measured; the expectation was not edited to keep them green. The floor itself is now censused across the whole ELF closure -- 150 objects -- not the entry binary, and the aarch64 claim is narrowed to the AppImage route since an aarch64 flatpak exists at v2.3.1. And the module no longer claims slicing is blocked, because it is not: the same artifact runs in a pinned container image whose userspace carries the closure, so on that route the host's C library is not the slicer's dependency at all. Binding a libc floor to a host on account of this product would attach the requirement to the wrong subject. THE CLASS. `docker version` answers about the DEFAULT CONTEXT; I read it as "no container execution route" and escalated a base-image change and a privileged install, neither needed, while a reachable context was listed the whole time. That is the same move as reading apt's need for root as "this environment cannot acquire software". Filed as a CAPABILITY-PROBE FORM on the existing selection_view_read_as_population row rather than as a new class, because the repair is identical: state the population from the subject, not from whichever member was probed first. docs/design-failure-modes.md regenerated. Sixteen witnesses, all green by execution, each paired so none is satisfiable by a judgement that answers one way. Compile clean: 25 blocking errors, all pre-existing on main, none in any file here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two blockers, and both are the same defect wearing different clothes: the conclusion supplied beside the call instead of derived from evidence. THE EXPORT DENOMINATOR WAS STILL CALLER-WRITABLE. admit_export_profile took the roster as a parameter, which moved the writable denominator one argument to the left rather than removing it -- a caller could still name [coupon_top_rung_subject], omit both fan features, and be admitted. It now closes over export_profile_subject_roster and receives standings only. cover_roster stays roster-parametric, because varying the roster against fixed evidence is the entire content of the coverage discriminator; what may not be offered is that knob on the production admission. The positive control was the worse half: a witness asserted that a one-subject roster admits on the measured evidence, which PROVED THE DEFECT rather than pairing the refusal. The population is now held fixed at the authority roster and the EVIDENCE is completed instead. CONSTRUCTOR EXCLUSIVITY IS NOT MINT SOUNDNESS. Sealing a type decides who may mint it; it does not decide what the mint must consume. CadQuery -- CadToolchainReady was a bare public arm, so a foreign module could write it and hand it to the sanctioned mint. It now carries a sole_constructor AdmittedCadToolchain that only judge_cad_toolchain mints, and the plan mint takes that token BY VALUE: there is no arm at that signature for an unjudged toolchain. Slicing -- judge_orca_execution took `started: Bool` beside the call, so the sealed AttemptedExecution was minted on a caller's say-so. It now consumes a ProcessOutcome, and Ready requires a zero exit status from that carrier, so "it started" has no spelling separable from the process being described. WHAT NEITHER REPAIR CLAIMS, annotated in both modules rather than left for the seal to imply: the observations are authored at the boundary. No construction in this graph can witness a Python import or a process. That is DESIGN section 4b's boundary column, deliberately off the ladder -- what the shapes remove is the UNSTRUCTURED assertion, not the boundary. 16 witnesses green by execution. Compile: 25 blocking errors, unchanged and all pre-existing on main, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…e to defend the copy
THE PREMISE OF THE LAST COMMIT WAS FALSE. It said no construction in this
graph can witness a process, and used that to justify a locally declared
ProcessOutcome carrying program, exit status and diagnostic. This repository
already owns that seam: gunbc.command_runner run_shell_command_capture is
effectful, reaches shell.Exec.RunArgv, and returns extdeps.shell.exec
ProcessOutcome -- a coproduct that exists precisely because a free success
flag was rejected as a conclusion rather than an observation.
So the local type was never a boundary obligation. It was a NICKNAME for an
authority one import away, and in a flat namespace a second ProcessOutcome is
worse than redundant. Deleted, not renamed.
AND THE ANNOTATION WAS DOING THE WALL'S WORK. ProcessExited { exit_status: 0 }
was publicly constructible, so the conclusion was still supplied beside the
call -- better typed than `started: Bool`, structurally the same defect -- and
the witness's positive control fabricated exactly that. The tell was that a
paragraph was needed to explain why the seal could be trusted.
attempt_orca_execution is now effectful and reaches a real process. There is
no pure path to AttemptedExecution; a spawn failure refuses before any outcome
exists. The two recorded hosts author ExecutionRefused directly, which is safe
in the direction that matters: a fabricated refusal costs a slice that would
have worked, a fabricated readiness mints a plan from a process that never
ran.
WHAT THIS DELETES AND DOES NOT REPLACE. Three witnesses established the Ready
arm from a fixture-supplied outcome. They are gone. A hermetic evaluation
replays a mock and constructs no argv, so a hermetic positive control could
only assert the mock -- specification without execution, which is what those
witnesses were. The Ready arm now carries NO executed evidence, and the wet
receipt that would restore it is named in the file as the next-rung trigger
rather than left to read as coverage.
CADQUERY: THE NAME NOW SAYS WHAT THE MINT ESTABLISHES. CadToolchainReady ->
CadToolchainRequirementsReportedSatisfied, because the token proves the
declared rosters were exhaustively joined to SUPPLIED observations -- not that
the SONAMEs resolve, not that CadQuery imports. Also deleted a sentence
claiming an instrument field keeps that boundary declared: no such field
exists on either observation type, so it asserted a mechanism that was not
there. The climb -- a real import probe through the same effectful seam -- is
named as the trigger.
13 witnesses green by execution. Compile: 25 blocking errors, unchanged and
all pre-existing on main, none in a changed file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
FOURTH ROUND, SAME CLASS, AND THIS TIME LOAD-BEARING.
attempt_orca_execution executed one ArgvCommand while sealing a SEPARATE
caller-supplied `program`, so a caller could run any zero-exit command and
seal the name "orca-slicer" onto the result. The execution receipt was real;
its SUBJECT could still be substituted after observation.
That is not cosmetic here. admit_slice builds the slice invocation FROM the
sealed program, so the admitted plan would have invoked a binary that was
never the one proven to run. ArgvCommand already carries program
structurally, so the second representation had no reason to exist: the seal
now reads command.program, and there is no second input left to disagree with
the first.
The progression across these rounds, kept because it is the whole lesson:
a Bool says the process ran
-> a structured record says the process ran
-> a real process ran, subject named separately
-> the subject derives from the command that executed
Each step removed one more place the answer could be supplied beside the
evidence.
THE CADQUERY NARROWING WAS HALF-DONE. The standing was renamed to
CadToolchainRequirementsReportedSatisfied while the downstream admission
still read CadQueryExecutionAdmitted, and a stale sentence still claimed that
holding the plan proves the toolchain was judged Ready -- false by the type
the previous commit deliberately introduced. A narrowed rung leaks through
whatever vocabulary downstream keeps the old name, and the reader sees the
name, not the paragraph. The arms are now
CadQueryExecutionRequirementsSatisfied / RequirementsUnmet, named for the
census actually performed.
WHAT THE SEALED ATTEMPT LICENSES is now stated where admit_slice can be read:
that THIS program ran to a zero exit on a host clearing the floor. Not that
the model path exists, not that the profiles resolve, not that the slice is
correct -- the PLA-at-255 incident was exit zero, "Success.", the right preset
name and the wrong temperatures entirely.
13 witnesses green by execution. Compile: 25 blocking errors, unchanged and
all pre-existing on main, none in a changed file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
… host FIFTH ROUND, AND THIS ONE IS NOT THE PREVIOUS DEFECT AGAIN. Deriving the sealed program from the executed command closed subject SUBSTITUTION. It did not close subject KIND: attempt_orca_execution accepted any ArgvCommand, so a caller could run `true` on a host clearing the Orca ABI floor, observe a genuine zero exit, seal program "true", and have admit_slice hand that program to the slice invocation. Nothing was faked anywhere along that path. Generic executability was simply read as ORCA executability. THE REPAIR IS NOT command.program == "orca-slicer". A string compare at the consumer would be a second authority for what counts as this upstream product -- DESIGN section 3 -- and an unreliable one besides: this module's own standing example is an artifact whose FILENAME misstates it, which is why the ABI floor is measured from the ELF closure rather than read off "Ubuntu2404". So extdeps.printing.orca_slicer owns the kind. OrcaExecutable is sealed there, that module mints every invocation over it, and attempt_orca_execution takes the executable and BUILDS the probe itself -- there is no parameter through which a command of another kind can arrive. The probe is --version: the cheapest Orca-shaped command there is, no display needed, and it exits zero only if the runtime closure resolved, which is the fact a would-be slicer actually needs. AND THE SEAL CARRIES THE EXECUTABLE, NOT ITS NAME. Keeping a NonEmptyStr on AttemptedExecution would have dropped the narrowing one function later: admit_slice would hold a program string with no way to know it named an Orca binary, so the kind established at the attempt would be lost exactly where it is spent. The typed executable travels the whole way to the invocation it authorizes. PR body: the prose "Sixteen witnesses" line is corrected to thirteen and now points at the three deletions, which the Verification section already described. 13 witnesses green by execution. Compile: 25 blocking errors, unchanged and all pre-existing on main, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…eted a module FOUR NATIVE-REVIEW FINDINGS (review 60915), each verified against the code before being taken. THE POSITIVE STANDING WAS FORGEABLE, and it is the export-side twin of the class this PR has been chasing on the slicing side for six rounds. Every arm of ChordStanding was a public constructor, so a caller could wrap excessive deviations -- or DistinctionUndeclared requirements -- in WithinRequiredDistinction for all three subjects and be admitted with adjudicate_chord never running. Coverage was an identity join over subjects nothing had judged. The passing arm now carries a sealed ChordJudgment. The failing arms stay public, and the asymmetry is deliberate: an authored REFUSAL costs an export that would have been fine, an authored PASS admits a profile nothing measured. Sealing the arms a caller can only hurt itself with buys nothing and costs every fixture the ability to state a failure directly. The generalization, which is wider than execution seals: ANY POSITIVE STANDING DOWNSTREAM ADMISSION TRUSTS MUST ITSELF BE EARNED. THE COUPON BUDGET COPIED ITS AUTHORITY'S NUMBER and named it in a string. An `authority:` field spelling out where 100 came from reads as a citation and creates no dependency at all -- change the canonical step in coupon hole_ladder_spec and every printed rung moves while the budget silently holds the old value, the string still reading correct. It now consumes ladder_step, and a degenerate ladder makes the requirement UNDECLARED rather than substituting a spacing that does not exist. THE PROFILE CENSUS WAS QUADRATIC. Equality is transitive, so comparing each standing to the first establishes the same predicate in one pass. AND I DESTROYED A MODULE WHILE FIXING THE FOURTH. extdeps/tools/sha256sum.dag ALREADY EXISTED -- four consumers, two operations, and a Sha256VerifyVerdict that separates a digest mismatch from the verification machinery breaking, so a broken mktemp is not reported as a corrupted download. I overwrote it with a shell redirect without checking. 25 blocking errors became 65. What caught it was a CONTROL, not a reading: the compile filter printed nothing, not even the "N blocking error(s)" summary line it always matches. "No matching diagnostic" and "the instrument failed to report" are different states, and only an always-matching line keeps them apart. Restored from HEAD; admit_orca_executable now CONSUMES sha256sum_verify_via_shell rather than a reimplementation of it, which is also the better model -- this module has no reason to know how a digest is taken. THE ORCA MINT, which the native review found independently: sole_constructor answers who may write the literal, and an unrestricted orca_executable(program: NonEmptyStr) handed that answer back to every caller. The mint now consumes a verified digest against the pinned asset. Restricting its CALLERS would only have moved the trust one function outward. 13 witnesses green by execution. Compile: 25 blocking errors, back to baseline after the 26 my own fold-over-Optional introduced, all pre-existing, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…mutable path TWO BLOCKERS AT THE NEXT AUTHORITY BOUNDARY, one of which retracts an approval the reviewer had already given. B12 -- SEALING THE JUDGMENT DID NOT SEAL THE CRITERION. ChordJudgment proves adjudicate_chord RAN. It does not prove the requirement it ran AGAINST was this product's, and ChordRequirement stayed publicly authorable. The positive control demonstrated the hole precisely: it authored a flattering DistinctionDeclared for two subjects production calls UNDECLARED, ran them through the legitimate adjudicator, received genuine sealed passes, and spent them on production admission. Nothing forged, every seal real, criterion caller-selected. That is the same defect a third time, each repair having moved it one argument outward rather than removing it: caller supplies the evidence population -> closed by rostering subjects caller supplies the ROSTER -> closed by closing over it caller supplies already-judged STANDINGS -> closed here admit_export_profile now takes OBSERVATIONS -- measurements, the only thing a caller is entitled to supply -- and joins each to the canonical requirement itself. adjudicate_chord stays public for the discriminator witnesses; what may not happen is its generic result being the production authorization currency. THE POSITIVE CONTROL IS DELETED, NOT REBUILT. Production honestly refuses today because two of three rostered subjects have no measured requirement, so a positive control cannot exist without fabricating policy -- the same fabrication as the three slicing Ready witnesses this PR already deleted. The trigger that would restore it names the measurement, not an artifact. NO CHORD-SPECIFIC COMPILER RED IS OWED, and this is a deliberate non-addition. Once ChordJudgment is sole_constructor the forbidden state is unwritable even from a fixture, and gunbc.model.population already records the canonical cross-module sole_constructor refusal measurement, pointing coverage at gunbc.guarantee_probe_corpus. A second product-specific compile-negative would duplicate substrate coverage while looking like product evidence. B13 -- VERIFIED BYTES BECAME AN UNVERIFIED MUTABLE PATH. The digest mint was correct at mint time and stored only the PATH. Verify the real AppImage, receive the seal, replace the file, and the capability is spent against whatever now occupies it. Adding a digest field beside the program would record what was verified without ensuring those bytes are what later execute. This module insists the 2.38 floor belongs to THIS content rather than to the Orca name, so a seal that decays into a name reintroduces exactly the inheritance it refuses. The two real closures are re-verification at every positive spend, or materialization into an owned content-addressed realization that the probe and the slice both consume. Neither belongs in a PR this size, so THE POSITIVE CAPABILITY IS UNINHABITED: there is no way to obtain an OrcaExecutable, hence no ExecutionReady and no SlicePlan. A coproduct having a Ready arm is not a reason to manufacture a way to reach it. What the direct-host route keeps is what it actually established: a measured ABI floor, and two recorded hosts that cleared it and still refused. 12 witnesses green by execution. Compile: 25 blocking errors, at baseline, all pre-existing, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…0-cad-toolchain # Conflicts: # dag/extdeps/printing/orca_slicer.dag # dag/gunbc/product/printed_chassis/export_profile.dag # dag/test/claim/printed_chassis_export_profile_witness_test.dag # docs/design-failure-modes.md
…copy FOURTH RETRIEVAL MISS, AND THE SHARPEST. std.observation_completeness already owns this exact law, and its own annotation documents the precise hole my version had: a duplicate in the EXPECTED list makes the join MORE permissive, certifying exactness while the roster is malformed. Roster [coupon, coupon, bore] against observations [coupon, bore] returned COMPLETE in the local copy while the fan-hole obligation silently vanished. B12 did not introduce that. It COPIED the module's existing local join to work over observations -- a second local copy of a substrate law, carrying a defect the authority had already closed AND written down. Both local implementations are now deleted rather than consolidated into a third. The authority also checks repeated-expected FIRST, and its reasoning is the part worth keeping: missing and foreign are statements ABOUT a question set and mean nothing when the question set is itself malformed, so reporting "missing" against a broken roster sends a consumer to repair the wrong artifact. TWO POPULATIONS ARE NOW JOINED, NOT ONE, with distinct refusal arms because their remedies differ. Observation coverage asks whether every rostered subject was MEASURED exactly once. Requirement coverage asks whether every rostered subject carries exactly one CANONICAL POLICY. Collapsing them would report an unmeasured feature and an unauthored requirement as one refusal, and different people fix those. AND THE EXACT-ONE LOOKUP IS NOW EARNED. `filter |> first` conflated three authority states: one canonical requirement, none, and TWO OR MORE resolved by list order. The third bites exactly at this module's stated next rung -- append a measured DistinctionDeclared for the fan hole beside the existing DistinctionUndeclared and the new policy is silently ignored; reverse the order and the declared one silently wins while a conflicting row still stands. A missing row was also being manufactured into an authored "undeclared", which refuses in the safe direction while naming the wrong remedy. THE WITNESS WAS BOUND TO A MECHANISM RATHER THAN TO WHAT SHIPS. The foreign-subject discriminator called the local helper directly, so it could have stayed green over that copy after production moved to a different join. It now asserts through production admission, supplying three observations for a three-subject roster with one measured twice and another not at all -- equal cardinality, still refused. Its two standing fixtures are deleted with it. THE REQUIREMENT-POPULATION ARM HAS NO DISCRIMINATING RED, stated in the source rather than left to look covered: both populations it compares are closed over by admission, so its RED is authorable only by editing the canonical rows. Also cleaned the stale orca_slicer sentence that still said "the only mints are in this module" immediately above the section declaring there is no mint -- exactly the overstated-rung prose this series exists to remove. 12 witnesses green by execution. Compile: 25 blocking errors, at baseline, all pre-existing, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…umer THREE SUBJECTS CAN BE MALFORMED, NOT TWO. ObservationRepeatedExpected says THE ROSTER ITSELF asks a question twice; it says nothing about the population being checked against it. Mapping it to ExportProfileRefusedRequirementPopulation sent a reader to repair the requirements when the roster was broken -- the same wrong-remedy error as reporting "missing" against a malformed denominator, which is precisely why the authority checks that arm first. ExportProfileRefusedSubjectRoster now owns it, from EITHER join. THE DEAD-SURFACE SWEEP FOUND UNCONSUMED FACTS, NOT DEAD CODE. exercised_chord_observations -- the recorded 993/991/998 nm rows this module exists for -- had NO CONSUMER once admission moved to taking observations as a parameter. Recorded evidence nothing adjudicates is a ledger, not a fact the graph carries: it can drift from the roster or from the profile it was measured under and nothing refuses. The module now carries its verdict on its own rows, with a witness, and that verdict is UNSETTLED -- the honest state, because two of the three measured features still have no authored requirement. That is the argument for sweeping after any change that moves a function's inputs: the finding was not unused code, it was unused EVIDENCE. Also deleted the four helpers the B12 cut orphaned: standing_subject, standings_share_one_profile, count_observations_for, chord_subject_feature. TWO SELF-INFLICTED ERRORS ON THE WAY HERE, neither committed, both caught by the compile count rather than by reading the diff. An expression placed on the line after `=` in a data declaration took the whole module down into 253 cascading errors from one line. And the orphan-deletion pass backed up to the previous blank line, swallowing chord_subject and chord_subject_eq -- both LIVE -- because they sat adjacent to the dead one with no separator. The orphan census was correct; the excision was not. Both restored verbatim from HEAD. 13 witnesses green by execution. Compile: 25 blocking errors, at baseline, all pre-existing, none in a changed file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
… argv The operator's constraint is that handing over an STL is the manual step to eliminate, so delivery is the work. This models the upload leg: FTPS to the machine's LAN file channel, with the credential reaching curl as a binding rather than an argument. extdeps.ietf.ftps splits the two negotiations, which are different protocols wearing one name -- a client that guesses wrong gets an unhelpful hangup that sends the reader to check the password. RFC 4217 is cited for the EXPLICIT leg only, which is its whole subject; implicit FTPS and port 990 are IANA's registration plus curl's ftps:// behaviour, and citing the RFC for them would attribute to a standards document a fact it does not contain. THE CREDENTIAL BOUNDARY IS THE POINT OF THE CHANGE. A first draft took `credential: Secret` and rendered it into curl's --user. That did not merely resemble a known hazard -- it re-created the class gunbc.credential_argv_exposure exists to RETIRE, on a fleet where that module records the audience as MEASURED rather than assumed (/proc with no hidepid, /proc/PID/cmdline mode 0444, runner slots in the host pid namespace), and where the identical defect had already been found and repaired on the Redfish side by deleting the -u arms. The comment above it argued the parameter was safe because the secret was "never a literal", which is a justification standing beside the thing it was meant to justify. The builder now has no parameter that could carry a secret. gunbc.auth.netrc_binding is a SHARED authority rather than a second copy: the 0600-at-creation O_EXCL write, the shred-before-write rewrite order and the shred-after-use are one fact with one home. bmc_onboard is migrated onto it and its duplicate netrc_content is deleted, its six call sites unchanged; srv3 is repointed. The deletion is the census -- srv3 refused loudly, which is exactly what a real dependent should do. WHAT THE SEALS DO AND DO NOT ESTABLISH, since a wrapper that reads stronger than it is would be worse than none. The payload's bytes are COPIED into an owned realization before they are hashed, and it is the copy that is uploaded: hashing the caller's path and handing curl the same path would prove what was there when sha256sum ran, not what curl later opens, so replacing the file in between would ship different bytes under a receipt naming the old digest. A copy and not a read, because a .3mf is binary and Filesystem.Read carries String content. That narrows the window to a 0700 private directory's lifetime; it does not make mutation unwritable, and content-addressed storage is named as the structural close. NetrcBinding's sole_constructor proves owner-only creation at MINT time and bounds no lifetime -- .dag has no linear or region types -- so it is recorded as mitigation with that missing capability as its next-rung trigger, not as construction. ProjectUploadReceipt is named for what FTPS actually observed. A completed transfer establishes that the server accepted the bytes this invocation was instructed to send, under this remote name; it does NOT establish that the device's storage now holds them, because nothing read anything back. An earlier `delivered: Digest` implied that stronger claim, and MQTT would have spent it as though the remote object were verified. Remote-equals-local needs an independent readback and is a separate climb. Two defects found by EXECUTION rather than by typechecking, both worth recording. The ProcessOutcome match arms invented `exit_code` and `output` fields that do not exist on the output variants, and re-tested `code == 0`, duplicating the ExitZeroSucceeds policy run_shell_command_capture already owns. Those diagnostics land on the TYPE DECLARATION site in extdeps/shell/exec.dag, not on the file holding the bad match -- so a changed-file diagnostic filter is structurally unable to see them, and only a whole-set difference finds them. Compile-clean had reported those files clean. Witness evidence is deliberately NOT claimed here: the witnesses reach evaluation now, but gunbc run refuses a Bool and its refusal prose is not a modeled oracle, so the structured verdict is CI's to give. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Required CI refused at namespace-wave-admission with exactly one unadjudicated
delta:
TargetChanged binding gunbc.srv3_boot_once_cd::srv3_boot_once_cd_resolved
`netrc_content` — base {gunbc.tools.bmc_onboard}
-> head {gunbc.auth.netrc_binding}
That is the wall doing its job rather than an obstacle to route around. The
spelling is identical on both sides while the declaration behind it moved, which
is the meaning-fork shape a leaf key is deliberately NOT invariant under -- the
other four deltas from the same change were auto-classified as
SameDeclarationIdentityRebind or ExplicitlyEvaluatedZeroDelta and needed no row.
The floor itself was green: claims_failed=0, passed=3460.
The row carries its own death. It goes when this PR merges, at which point main
declares netrc_content in gunbc.auth.netrc_binding, base and head bind the
spelling identically, no run can produce the delta, and it reports CONSUMED
rather than stale. The row says to adjudicate that deletion by joining against
main's tree on its own (module, in_declaration, spelling, target) tuple, because
a trigger sentence is not evidence that the trigger fired.
Two notes on how this was landed. The roster is a `.rs` file, so I checked
whether it was generated before hand-editing it -- it is not, and its own seed
growth justification records these rows as DATA consumed by an already-rostered
declaration, dissolving row by row with the transition each names. And the label
is inlined rather than bound to a new const, because that same file tracks a
hand-declaration census and a const would grow it to say something a string
literal already says.
Verified with cargo check -p v1-compiler --bin claim_executor, reading the INNER
exit status: the remote wrapper reports "exited with code 0" while the cargo it
ran exits non-zero, so the first attempt's exit 101 (my own wrong -p) would have
read as success from the wrapper alone.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…ce and cleanup holes Review found four P1 defects in the FTPS lane and one duplicate authority. All are repaired here. I HAD WRITTEN A SECOND ENDPOINT AUTHORITY. main already carries printer_01_lan_endpoint and printer_02_lan_endpoint in gunbc.fleet_intent_network, transcribed from the operator's reservation table on 2026-09-04, with the MAC rows beside them. I authored gunbc.fleet.printer_lan_endpoint an hour earlier saying the same thing, because I searched MY OWN BRANCH -- whose base predates those rows -- rather than the authority surface. The duplicate is deleted and delivery reads main's roster through the topology. THE FREE host PARAMETER WAS A CREDENTIAL EXFILTRATION HOLE, not untidiness. deliver_project_to_printer keyed the Secret Manager locus on `printer` while taking the FTPS endpoint and netrc machine from an independent caller-supplied `host`, so `printer_01 + attacker-host` was spellable: printer-01's access code would be fetched and deliberately sent to a peer the caller chose, with verification disabled so nothing would object. Two facts that must agree were free to disagree. The address now derives from the PhysicalAssetIdentity and there is no host parameter. TWO FIXED PATHS WERE SUBSTITUTION RACES WITH NO ATTACKER IN THEM. The payload realization used one name under the private root and the netrc used a single /tmp path, so two deliveries in one job could overwrite each other between mint and use: place_netrc_binding does remove-then-write, so A's credential can vanish after A minted its binding and before A's curl reads it, and the sealed payload digest can describe bytes a second identification has already replaced -- B13 reopened by ordinary concurrency rather than by an adversary. Each attempt now takes its own mktemp -d. CLEANUP FAILURE WAS ERASED. Both shred results were assigned to `_`, so a completed upload whose credential shred failed still returned ProjectDelivered -- an access code left on disk, reported as a clean delivery. Collapsing it into ProjectDeliveryRefused would be the opposite lie, since the bytes DID arrive and a retry would send them twice. ProjectTransferredCleanupRefused preserves the transfer fact and names the residue, and MQTT must not consume it as readiness. AND srv3 WAS WRITING A BMC CREDENTIAL WORLD-READABLE. srv3_boot_once_cd_resolved consumed netrc_content but wrote it with plain Filesystem.Write, i.e. at the ambient umask -- moving the exposure the Redfish argv repair had just closed from the process table onto the filesystem, for the same unprivileged audience. It now goes through place_netrc_binding, 0600 at creation via O_EXCL. The earlier claim that "BMC is migrated onto the shared binding" was too broad: the bmc_onboard call family had migrated, this writer had not. The wave-admission roster's eight consumed gunbc#10514 rows are deleted, which came due because this change touches the roster. Their trigger was adjudicated rather than assumed: all four spellings are declared in gunbc.auth.gcp_secret_access in this tree, so the transition they name can no longer occur. Compile: 38 blocking, none in any file this branch changes, and no diagnostic anywhere names netrc, a credential, ProcessOutcome, FTPS or curl -- checked that way because a defect of mine previously landed on extdeps/shell/exec.dag, where a changed-file filter could not see it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…dpoint Two more P1s from review, both repaired by narrowing construction rather than adding a check. DELIVERY CANNOT TRUTHFULLY ACCEPT A GENERIC CommandTransport. The payload realization and the netrc are materialized on THIS filesystem, and the SshExec arm only wraps argv for remote execution -- it copies nothing. So a caller passing SshExec would run curl on another machine against paths that exist only in this container: a confusing failure at best, and at worst a read of whatever those paths happen to name over there. The parameter is DELETED rather than validated, because a transport this function cannot honour should not be spellable at its boundary. Hosting delivery on srv2 is a different realization -- fetch the credential there, materialize the project there, execute there -- not this one with a flag changed. THE ENDPOINT LOOKUP WAS filter |> first, which is the shape this lane keeps objecting to elsewhere. It now admits exactly one row that matches the asset AND is a FabricationAppliance AND is Lan. Zero, duplicate and wrong-class refuse distinctly: "no endpoint for this asset" and "an endpoint that is not the file channel" have different remedies, and the second would authenticate an access code to a tailscale or BMC attachment that happens to name the same printer. The access-code locus, the endpoint and the peer-verification exception are now bound to one physical asset the whole way down. Two of the six diagnostics this produced were the substrate refusing correctly. Adding PrinterAddressWrongClass made the call site non-exhaustive until it decided what to do with it, and the locality fold was missing TailscaleOverlay -- exactly the endpoint class that must never receive a credential. On the reachability model, deliberately NOT touched: a census shows ContainerRunner is bound to no execution population anywhere -- it appears only in the enum, the fold, and witnesses calling that fold -- so the standing `false` is model-versus- itself and flipping it to match one measurement would pick a different ungrounded answer. My socket observation (local=172.17.0.17 -> 192.168.1.234:990, routed) is evidence about THIS session realization and is recorded as such. Compile: 38 blocking, none in any file this branch changes, and no diagnostic names netrc, a credential, ProcessOutcome, FTPS, curl, an endpoint, a transport or a locality -- checked that way because a defect of mine previously landed on extdeps/shell/exec.dag where a changed-file filter was blind to it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…ission row THE FIRST WET RUN FOUND BOTH OF THESE, which is the point of having run it. CLEANUP ONLY RAN AFTER A TRANSFER WAS ATTEMPTED, so every earlier refusal stranded the owned copy. Measured, not reasoned: the run stopped at the credential leg and left /tmp/tmp.g22PxY8VJT/project-payload behind, 226915 bytes, one per attempt indefinitely. Every exit path now drops the realization through a single refuse_and_drop helper rather than repeating the call, so an arm added later cannot forget it. The netrc correctly did not leak, because it is placed after the point that refused -- the ordering held, only the payload's did not. THE ADMISSION ROW I ADDED WENT STALE, AND MY OWN LATER FIX IS WHAT STALED IT. The row said `netrc_content` in srv3_boot_once_cd_resolved retargets to gunbc.auth.netrc_binding. Then srv3 moved to place_netrc_binding for the owner-only write, so it no longer calls netrc_content at all and the delta the row describes cannot occur. A row matching no delta is a permission standing over nothing, which is exactly what the wall refuses. Deleted, along with the import that was left behind unused. That makes three refusals from one roster in one session -- delta created, consumed rows due on touch, row gone stale -- all of them the same rule: an entry must correspond to a real current motion. Each time the first instinct was that CI was in the way, and each time CI was reporting something true about the change. Compile: 38 blocking, none in any file this branch changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
deliver_project_to_printer decided whether a printer's access code existed
by reading a roster this repository writes. An empty roster meant "we have
no record", and it was being consumed as "the remote says no" -- a local
declaration wearing an observation's name, writable by any author who
appended a row.
It now asks Secret Manager. gcp.SecretManager.GetSecret was already
declared in extdeps with zero callers; all it lacked was the
outcome: RestOutcome field that stops dispatch_rest raising its 404 as a
rendered TypeError, which is how the wet run of 2026-09-06 received it. It
is the only operation in that service declaring an outcome, and the reason
is asymmetric: for AccessVersion a 404 is a failure and raising loses
nothing, but for GetSecret a 404 is THE ANSWER, so the one arm that must
not throw is the one the question was asked to reach.
Three distinctions the transport would otherwise have collapsed:
A 404 is absence; every other non-success is an unanswered question. A 403
means the caller was not permitted to look, a transport refusal means
nothing was reached. Folding either into absence would report "this printer
has no access code" on the strength of a permissions problem, and the
remedy that follows -- provision one -- would mint a second version over a
code that was there all along.
A present container is not a known version. RestOk routed back through the
roster unmodified answered ProvisionRequired for a secret that demonstrably
exists. That is now PrinterCredentialVersionUnrecorded, and delivery
refuses on it rather than guessing a version or re-provisioning.
The classification is separated from the transport so its RED is
authorable. Inline in the network func, the decision that must not go wrong
could only be exercised by making Secret Manager return a 403 on demand.
Separated, a witness constructs RestStatusRefused { status: 403 } directly:
a positive control on 404 plus a discriminating red across 403, 401, 429,
transport refusal and an undecodable body.
Also, from review: the receipt join consumes secret_ref_secret_resource
rather than re-spelling project+secret equality, with version deliberately
excluded -- desired says pending, and the receipt is the authority that
supplies it. PrinterAccessCodeLocusFound becomes
PrinterAccessCodeDesiredLocusFound, because it answers which secret the
code is SUPPOSED to live in and never whether it is there. Delivery
projects ProjectDeliveryProvisionRequired as its own outcome. The wet-run
actuator reads its payload path from PRINT_N_WET_PAYLOAD and refuses rather
than defaulting; it previously carried one author's scratchpad literal, and
a guessed default there spends an hour of printer time on wrong geometry.
Compile: 38 blocking, equal to the baseline, none in these files.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
gunbai-bot
Bot
changed the title
Three blockers found by review against ee5cd66, repaired together because they are one boundary seen from three sides. B2, the serious one: production walked around its own refusal. observe_printer_secret_container derived the secret name from printer_access_code_desired_ref, which spells an id BY CONVENTION and therefore succeeds for any identity. A printer present in the fabrication topology but absent from printer_access_code_loci had a plausible Secret Manager name synthesized for it and queried. The roster's refusal was correct, had a witness, and had no consumer -- the module even carried a comment asserting unknown printers refuse, which was true of the lookup function and false of the production path. The desired ref now comes OUT of the admitted locus row, so the roster cannot be bypassed by construction rather than by discipline, and the existing unknown-printer red finally tests a function production calls. Receipt resolution takes that same admitted SecretRef instead of independently re-deriving it, so the join and the remote read cannot drift onto different subjects. An undeclared or conflicted locus gets its own arms rather than ObservationRefused: a missing declaration means fix this repository, a failed observation means the problem is out there, and merging them would send an operator to debug Secret Manager for a row nobody wrote. B3: a 404 arriving over a subject-matched provisioning receipt returned ProvisionRequired, identical to a printer that was never onboarded. Those facts differ. A receipt is evidence a write happened and returned an exact version, so a container that is now gone is a CONTRADICTION between a durable receipt and a current observation -- and that is all the new arm asserts, since at project+secret join grain any other explanation would itself imply a defect in the write machinery. The remedy is to investigate, never to provision: ProvisionRequired routes to onboarding, which would have recreated a secret something deleted and destroyed the only signal that a deletion occurred. B1: the witness asserted ref.version == "1" while fleet_secret_ref constructs "pending" -- the exact false materialization claim removed from production earlier in this branch, left standing in the test. It is the sole blocking identity in the floor lane at ee5cd66, so this is corroborated by execution and not only by reading. Repaired by comparing the locus to what the canonical constructor produces rather than copying "pending" in place of "1", which would have relocated the duplicate authority instead of removing it; secret_ref_version_resource is no longer called on a desired ref at all, since rendering a pending ref as a version resource is the confusion the row exists to refuse. Compile: 38 blocking, equal to the baseline, none in these files. The aggregate witness executes and returns true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…ellable
Review found B4: the SecretProvisionReceipt this lane treats as durable
evidence is forgeable. It has no seal, and secret_provision_receipt is a
pure fn taking every argument from its caller, so sealing the type alone
would not fix it either -- the constructor consumes no effect-earned input.
The mint repair needs the provisioning actuator, which does not exist. This
lands the half that does not, and it is the half that makes the actuator's
arrival a one-function change.
The classifier took a whole PrinterCredentialResolution as its record
input, which made ObservationRefused, VersionUnrecorded and
MaterializationVanished syntactically admissible as "what our records
show" -- transitions a record lookup can never legitimately produce, each
forwarded by hand through two separate match arms. A forwarding arm is
exactly where a wrong mapping hides, and there were sixteen of them.
The record answers one question with two answers, so that is now the type:
PrinterMaterializationRecord = NoRecordedMaterialization
| RecordedMaterialization { exact_ref }
materialization_record_for is the single adapter from stored receipts to
that record, and it is the seam B4 will land on. When the actuator becomes
the sole minter of an effect-earned receipt, ONLY THAT FUNCTION CHANGES:
the classifier already speaks in records and the witnesses already author
records, so neither has to move. That is the reason to introduce the narrow
type before the actuator rather than after. Ambiguity now refuses at the
adapter, because "two receipts claim this secret" is a fact about our
records and not about the remote container the classifier reasons over.
The review's sharpest catch was in the red I had just written. It
constructed PrinterCredentialProvisioned { exact: <the DESIRED pending
ref> } -- a value named Provisioned holding something definitionally not an
exact provisioned version. It still discriminated the branching law, but it
only type-checked because the classifier accepted the whole coproduct.
It now authors RecordedMaterialization with a pinned version, which is the
authorable seam by design; what may never be authorable is the
effect-earned receipt that produces one in production.
Also: the MaterializationVanished explanation "or the read is pointed at a
different project than the write was" was removed from the production
module and reported as removed, while the witness comment kept it. One
instance fixed, two existed. Both are gone now, and the arm asserts only
the contradiction it can evidence.
Compile: 38 blocking, equal to the baseline, none in these files. The
aggregate witness executes and returns true.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Review found a binding defect inside secret_provision_receipt: version_resource and version were two independent caller arguments, so a receipt whose action named ".../versions/7" while its identity pinned "12" was spellable, and nothing could detect it. Two fields, one fact, unbound. The fact is the identity Secret Manager returns from the write. AddVersion already answers name: SmResolvedVersionIdentity -- the full projects/P/secrets/S/versions/V -- so the receipt now takes that identity and derives both fields from it. The disagreement has no constructor. sm_resolved_version_id lives beside the decoder in extdeps because that is what makes it total BY CONSTRUCTION rather than by validation: the brand's only mint is decode_sm_resolved_version_identity_wire, whose well-formedness check already requires exactly one "/versions/" with a nonempty slash-free segment after it, so the split cannot fail for a value of this type and the fallback is unreachable rather than lenient. If the brand ever became mintable another way, that function would have to refuse instead -- which is a property of the type, and why the extractor sits next to the thing that enforces it. WHY NOW rather than with the actuator: secret_provision_receipt has ZERO production callers -- three witnesses and nothing else. The signature was free to change today and will not be once a real minter exists. SCOPE, STATED SO THE CLASS IS NOT READ AS CLOSED. This fixes the BINDING between the two fields. It does not make the receipt effect-earned. SecretProvisionReceipt still has no seal and this fn is still pure, so a caller can supply an identity that came from nowhere; the difference is that what it supplies must at least be internally consistent. The remaining half needs the provisioning actuator to be the sole minter, taking the identity from a performed AddVersion response rather than a parameter. A seal added now, with no minter behind it, would make the type unconstructible rather than better guarded, and a seal beside a pure helper kept alive to work around it is the escape hatch. The new red says the same thing in its own comment: it establishes internal consistency and NOTHING about provenance, because a green row there is easy to over-read. Compile: 38 blocking, equal to the baseline, none in the touched modules. Both a_receipt_cannot_pin_a_version_its_resource_does_not_name and fleet_printer_access_witnesses_hold execute and return true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
One conflict, in NAMESPACE_TRANSITION_ADMISSIONS. This branch had emptied the roster to &[] because its own rows were consumed; main had added the twenty-fifth transition for changes of its own. Taking this side would have deleted main's live admission with no conflict to show for it. Resolved to main's file whole, and the reason is a second drop the conflict markers did NOT surface. Auto-merge silently took this branch's deletion of the TWENTY-FOURTH DISSOLUTION doc block: merge-base had it, this branch removed it, main left it untouched, so one-side-changed resolved to the deletion without ever asking. That block records WHY nineteen asset-identity rows went away, which is still true of the merged tree -- this branch had deleted the rows and the account of them together. Nothing on this side was needed in that file: its only content was the empty roster and those removals. Verified by content rather than by a clean exit: the file is byte-identical to origin/main, and the branch's own work is intact across all eight .dag files. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…ders Two review findings, and both falsify a claim made in an earlier commit message on this branch rather than merely improving on it. B6. sm_resolved_version_id was documented as TOTAL BY CONSTRUCTION on the reasoning that SmResolvedVersionIdentity can only be minted by the validating decoder, so the split could not fail and its fallback was unreachable. The type is `NonEmptyStr where brand(...)`, and a brand is a NAME, not a constructor: any module can write `"anything" as SmResolvedVersionIdentity`, and a witness three files away in this same branch already did. The decoder is A minter, never THE minter. So the fallback was reachable and it returned the whole malformed string as the version id -- answering "not-a-version-resource" to the question "which version is this", in the field a credential fetch is later pinned on. That is the fabricated plausible output §5 forbids outright, sitting behind a comment asserting it could not happen. It refuses now, and the refusal propagates: secret_provision_receipt answers SecretProvisionReceiptMint, so a malformed identity mints nothing rather than minting something with a plausible-looking segment in it. The validation the brand does not perform happens at the point of use, and the note says it is validation rather than construction -- the rung climbs when the decoder owns a carrier no other module can spell, at which point the refusal arm becomes unreachable FOR REAL and can be deleted with evidence. The destructive control is enrolled: a_malformed_resolved_identity_mints_no _receipt feeds exactly "not-a-version-resource" and asserts both the projection and the mint refuse. It goes red if any lenient fallback returns. B5. The previous commit claimed materialization_record_for was the single adapter, so that when the actuator becomes sole minter ONE function would change. Three functions read printer_access_code_provision_receipts: that adapter, a separate recorded_materialization_is_ambiguous that filtered and counted the same roster, and an inline filter in the observer building the match count. A claim of single authority is falsified by any second reader, and there were two. Worse, the ambiguity check ran AFTER the token was resolved and AFTER GetSecret was dispatched, so duplicate local receipts plus an unavailable token answered ObservationRefused -- a malformed LOCAL declaration hidden behind an unrelated EXTERNAL failure, which is the exact fault-class collapse the locus admission was repaired to prevent, reappearing one population over. PrinterMaterializationLookup carries the conflict so that PrinterMaterializationRecord can stay exactly two arms, the lookup happens ONCE before anything is dialled, and everything answerable from our own records is answered before the network is touched. Compile: 35 blocking, equal to the merged-tree baseline, none in the touched modules. Both a_malformed_resolved_identity_mints_no_receipt and fleet_printer_access_witnesses_hold execute and return true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…B4 denies Review finding B7, plus the source half of a sync I reported done and had only half done. B7. The destructive witness used SecretProvisionReceiptMint, ReceiptMinted and ReceiptRefusedMalformedIdentity bare, thirteen times, with none of them in its import list. Two failures had to coincide for that to survive. The scripted edit that was supposed to add them silently no-opped -- the import is a multi-line block and the pattern assumed one line, and a replace that matches nothing returns the string unchanged and says so to nobody. Then the flat namespace resolved the three names anyway, because their defining module happened to be in the assembled closure. So compile was clean, both witnesses executed green, and CI was green on four checks over an edit that never happened. The green is not counterevidence here, it is the reason the class is dangerous: accidental coverage is invisible to every execution-based check by construction, and "this consumer owns an explicit binding" is a census claim, not a runtime one. Repair is the binding only; no semantics move. The two stale comments are the same shape one surface over. The PR body was synchronized and the carriers were not, so source contradicted both the body and the implementation: "A PURE FUNCTION OF THE OUTCOME" -- it is a pure function of the outcome AND the record, which is the entire point of the narrowing. "a CONTRADICTION between a durable receipt and a current observation" -- durable asserts exactly the property B4 established this carrier lacks, in the one comment a reader consults to learn what the arm means. It now says recorded materialization, and states why the stronger word was wrong. The third instance the review found, in gunbc.secret_provision, is pre-existing on main from #7972 and outside this branch's hunks; flagged, not edited. WHILE FIXING THAT, THE TWO STANDING CLAIMS WERE ACTUALLY CHECKED rather than asserted a third time. grep for printer_access_code_provision_receipts returns exactly two hits, the declaration and materialization_lookup_for, so the single-reader claim holds -- and that grep is now cited in the note itself, so a reader can refuse the sentence in one command instead of taking the author's word. grep for `as SmResolvedVersionIdentity` returns nine casts across four files, which confirms B6 more strongly than the comment claiming it did. Compile: 35 blocking, equal to the merged-tree baseline, none in the touched modules. Both a_malformed_resolved_identity_mints_no_receipt and fleet_printer_access_witnesses_hold execute and return true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Three findings from the approving review. The first is not a nit. THE SUCCESS ARM WAS FABRICATED FAILURE. printer_delivery_wet_run answered exit_failure with a "DELIVERED remote=..." reason on ProjectDelivered, so a SUCCESSFUL delivery exited non-zero. The reason it happened is visible in the shape: exit_failure is the arm that carries a printable string, and this actuator exists to report which leg answered, so every arm reached for it. §5 forbids fabricated failure in the same breath as fabricated success, and it is worse here than a cosmetic inversion -- anything wiring this into automation reads the exit code and concludes the transfer failed while the file is sitting on the printer. It answers ExitSuccess now, and nothing is lost by dropping the reported name: the remote filename is remote_name_for_digest of the payload content, a pure function of the digest, so it is re-derivable from the payload at any time rather than a fact only that run knew. The refusal arms keep their reasons, because WHICH leg refused and why is exactly what a caller cannot re-derive. IDENTITIES COMPARE AS IDENTITIES. endpoint_names_printer coerced both sides to String and compared the renderings -- an equality on the PROJECTION, not the subject. It holds for any two assets that happen to render alike, and it would start lying silently the moment rendering changed. It now compares directly, which is the same equality gunbc.fleet_printer_access already uses on this type when matching a locus row to its printer. That fix has NO DISCRIMINATING WITNESS AND PROBABLY CANNOT HAVE ONE, stated here rather than papered over: the two spellings diverge only for two DISTINCT identities that render identically, and constructing that pair may not be possible for this type. A row that cannot go red is a decoration §4b calls worse than absent, because it gets cited as coverage. So this is compile-verified and behaviour-preserving, and it removes a class rather than fixing an observed defect. THE BARE Nat PORT IS MARKED, NOT MINTED. A TCP port is 16-bit with a registry behind it; Nat admits 0 and 70000, neither of which any endpoint can hold. A Port coined in extdeps.ietf.ftps would be a second name the moment ssh, http, or the MQTT channel this lane has not built needs one, so the row carries feature:/dissolve-on: naming the shared std carrier instead. NOT EXPANDED ONTO: the same String-coerced equality appears in five other fleet modules (runner_connectivity, shell_transport_observation, revision_acceptance, multi_principal_probe, converge_plan). Those are other lanes' modules and predate this branch, so they are substrate debt; turning them into a blocker here would be the scope creep the previous review declined for pre-existing bare bindings. Flagged, not touched. Compile: 35 blocking, equal to the merged-tree baseline, none in the touched modules. fleet_printer_access_witnesses_hold and w_no_credential_is_ever_spelled_into_the_upload_argv execute and return true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
… is lost"
Three findings, and all three are the same failure wearing different
clothes: a property asserted without running the check that would falsify
it.
B8. The feature:/dissolve-on: marker on the bare Nat port was BORN STALE.
std.types.Port has been `Int where range(min: 1, max: 65535)` all along,
consumed by boot artifact delivery, cli dispatch and three spark serving
modules. The marker advertised a gap that was really an unconsumed
authority, and a trigger already satisfied is worse than no marker at all --
it will be cited as evidence the question was considered.
The route there is the part worth recording. The dashboard review noted in
passing "(no existing Port authority to consume)" and I wrote the marker on
that basis WITHOUT CHECKING. An absence is a census claim, and it is no more
checkable when a reviewer supplies it than when I assert it myself. Now
consumed: Nat admitted 0 and 70000, neither of which any endpoint can hold,
and Port refuses both by construction rather than by annotation.
B9. "Nothing is lost by dropping the reported name" was false, and this
module's own design refutes it. identify_project_payload copies the caller's
file into a PRIVATE OWNED REALIZATION and hashes THAT COPY, precisely
because the caller path is mutable -- so once the realization is removed,
rehashing the original need not reproduce the digest. If the name really
were always re-derivable, the private realization would have been pointless.
I justified a discard with a claim that contradicts the TOCTOU protection
the same lane built.
The honest statement replaces it: this actuator's public result is
ProcessExit ONLY, a successful run deliberately exposes no receipt metadata,
and a caller needing the exact remote name consumes ProjectDelivery and its
ProjectUploadReceipt directly. The refusal arms keep their reasons for a
reason that survives scrutiny -- WHICH leg refused is re-derivable from
nothing, mutable or not.
REQUEST_CHANGES: two `uses net: Network` clauses with no
`std.resources { Network }` import. Both bound, and the sweep covered every
changed file rather than the two named; those two were the only ones.
One correction to that finding, because the difference is the whole
hazard: it is NOT an unresolved symbol at the compiler floor. Both files
compile clean at baseline -- Network resolves through the whole-tree flat
namespace without the import. An unresolved symbol is loud and
self-correcting; accidental resolution is silent and GREEN, which is why
this is the second instance on this branch after the three mint names in
B7, and why CI passing was never evidence either way.
Compile: 35 blocking, equal to the merged-tree baseline, none in the
touched modules. w_the_ftps_port_follows_the_negotiation_in_both_directions
and fleet_printer_access_witnesses_hold execute and return true.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Contributor
|
Both One correction to the finding, because the difference is the whole hazard. It is not an unresolved symbol at the compiler floor. Both files compiled clean at the tree baseline before this fix: The — sent from crisp-ibex-710 |
…ames
B8 moved both of this module's port surfaces from a bare Nat to
std.types.Port -- ftps_default_port's return and FtpsEndpoint.port. That
left `import std.nat { Nat }` with no remaining consumer: the only three
surviving Nat occurrences in the file are inside a section 4c annotation
block, which is annotation-erased and cannot constitute a use.
It is not cosmetic here. An unused import widens the assembled closure,
and a wider closure is what lets an undeclared bare name resolve by
coincidence -- silent and green, which is the class this branch hit twice
already (three mint names in B7, and `Network` in the dashboard finding,
where both files compiled clean at baseline precisely because the flat
namespace resolved the symbol without the import). The missing-import
defect and the unused-import defect are the same failure seen from
opposite sides.
Verified stale rather than assumed stale: at 8cdad79 lines 79 and 136
were real Nat uses, so this edge was made dead by my own repair.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…t read as a clean failure Review 61366 found that the ProcessRefused arm of deliver_project_to_printer computed `credential_shredded` and `realization_removed` and then discarded both. A transfer that failed AND whose credential shred also failed returned a plain ProjectDeliveryRefused -- byte-identical to a refusal that left nothing behind. The access code may still be on disk and nothing in the value says so. This module already carries the argument against exactly that collapse, in the annotation above ProjectDelivery: assigning the shred results to `_` on the SUCCESS path meant an access code left on disk was reported as a clean delivery, which is why ProjectTransferredCleanupRefused exists. The argument simply had not been applied to its mirror -- and the mirror is the likelier case, because a transfer that died mid-flight is a transfer whose cleanup had the least chance to run. ProjectDeliveryRefusedResidueRemains is not a severity label on the refusal. It is a second fact with a different remedy: a plain refusal may be retried, a residue refusal must send someone to look at the disk first. Those must never be one message. The classification is extracted as the pure `refused_delivery` rather than left inline, because inline its discriminating case is reachable only by actually failing a live network transfer -- so no witness could ever exercise it, and the variant would have been a decoration. Split out, both arms are reachable from a fixture with no shell and no network. Evidence, executed, not asserted: a_clean_failed_transfer_is_not_reported_as_leaving_residue returned true a_failed_transfer_whose_shred_also_failed_names_the_residue returned true Same stderr in both, cleanliness the only variable, each arm rejecting the other's answer. And the control that had to fail: replacing `if cleaned` with `if true` -- the exact collapse this prevents -- flipped the second witness to `returned false`. Two greens alone would not have established that the pair discriminates. Every variant named in the new match arms is explicitly imported. Leaving them to the whole-tree flat namespace is the accidental-resolution defect this same PR just repaired twice. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Contributor
|
Review 61366 — taking the ProcessRefused finding, pushed as You were right about the shape and there is a sharper way to say it. This module already carries the argument against exactly this collapse, in the annotation above
One thing I did beyond the finding, because otherwise the variant would have been a decoration. The classification was inline in the effectful Evidence, executed:
Same stderr in both, cleanliness the only variable, each arm explicitly rejecting the other answer. Two greens would not have established that they discriminate, so I ran the control that had to fail: replacing Every variant named in the new match arms is explicitly imported rather than left to the whole-tree flat namespace. That is the accidental-resolution defect this PR repaired twice already, and a test file is not exempt from it. — sent from crisp-ibex-710 |
…y path that can leave it Review 61370 filed two REQUEST_CHANGES items. Both are real; I verified each against the current code before touching it, and the second turned out to have four sites rather than the two cited. RECEIPT IDENTITY COULD CONTRADICT ITSELF secret_provision_receipt built the identity from the INTENT's project and secret but took the version from the RESOLVED resource. An intent for secret A answered with projects/P/secrets/B/versions/9 minted an identity for A/9 while recording B/9 as the action -- every field individually true, the row as a whole a lie, and nothing downstream able to detect it because both halves looked authoritative. sm_resolved_version_secret_resource now projects the secret half of the response the same way the version half was already projected, and a resolved resource naming a different secret than the intent refuses via ReceiptRefusedResolvedSecretDisagreesWithIntent instead of being averaged with it. Only projecting the version is what invited the blend. CLEANUP WAS DISCARDED ON FOUR PATHS, NOT TWO The review cited refuse_and_drop and the wet-run token exit. Grepping the module for the pattern rather than the two names found four: refuse_and_drop let _ = shell.Remove.FileForce PrinterCredentialProvisionRequired let _ = shell.Remove.FileForce the wet-run SuppliedTokenUnavailable exit no removal at all (ProcessRefused, fixed in 525a621 for review 61366) That is the tell that 525a621 patched a site and not a class, so this pass takes the class: `grep -c 'let _ = shell.Remove'` in the module is now 0. Each path names the residue with a variant carrying its own remedy -- ProjectDeliveryUnattemptedResidueRemains and ProjectDeliveryProvisionRequiredResidueRemains, the latter keeping `desired` so the provisioning fact is not lost to report the disk fact. abandon_payload is exported as the bracket for callers that give up before delivery is entered, and returns whether removal succeeded rather than swallowing it. The residue sentence itself has one authority, residue_cause: it appears once in the module where it previously would have been written four times. Evidence, executed, with the control for each new class: a_resolved_resource_for_another_secret_mints_no_receipt true a_resolved_resource_for_the_intended_secret_still_mints true a_malformed_resolved_identity_mints_no_receipt true an_unattempted_delivery_that_cleaned_up_... true an_unattempted_delivery_whose_removal_failed_names_the_residue true a_failed_transfer_whose_shred_also_failed_names_the_residue true Controls: replacing the disagreement guard with `if false` -- exactly the original blend -- flipped the receipt witness to false; `if cleaned` -> `if true` flipped the residue witness to false. Both restores verified byte-identical. The pairs hold every input fixed except the one variable, so a collapse cannot pass by producing a differently-worded message. Adding the mint variant made five existing witness matches non-exhaustive and the compiler refused each by name. That census is the reason the variant is a variant rather than a field. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
Contributor
|
Review 61370 — both items verified against current code and fixed in Receipt identity could contradict itself. Confirmed exactly as described. Cleanup lost on early exits — four sites, not two. You cited
Four instances of one class is the tell that Each path names the residue with a variant carrying its own remedy. Evidence, executed, with a control per new class:
Controls: replacing the disagreement guard with One design note on why these are variants and not a The witness project is read off — sent from crisp-ibex-710 |
…ned payload copy Review 61378 filed two blocking items. Both confirmed against current code, and both are the same class as the previous three rounds -- an effect whose result is bound to `_`, so a failure is spelled identically to a success. A FAILED NETRC WRITE IS NOT EVIDENCE THAT NOTHING WAS WRITTEN WriteOwnerOnly reports only success, so a write that died partway leaves an owner-only file holding a prefix of the netrc -- and the credential is the LAST field on that line, so a truncated one is the likelier shape. The refusal said "no credential was placed", a claim about the disk that the return value could not support. The placement now removes on failure and names the path when removal also fails. Three arms, because the two ways of leaving material behind have different stories: a partial write we could not clean, and a pre-existing file we never owned. That site also held another `let _ = shell.Remove`. IDENTIFICATION REFUSED WHILE HOLDING A COMPLETE COPY The hash-failure arm ran with the whole payload already copied into a private directory and returned a refusal naming neither the copy nor its path, so recovery had nothing to act on; the copy-failure arm could leave a partial destination the same way. Every post-mktemp refusal now routes through one bracket, so a future failure mode cannot reintroduce the leak by returning a refusal. It removes the workspace with RecursiveForce rather than the file alone, because the mktemp directory was leaking per attempt too. THE FIXTURE THAT WOULD HAVE ASSERTED NOTHING The first residue witness pointed at an unremovable path under /proc. `rm -rf` exits 0 on a MISSING path even under an unwritable parent, so that witness would have been permanently green while carrying no information -- and worse than absent, because it would have been cited as coverage. Verified by running the fixture in a shell before trusting it. Making removal genuinely fail needs a chmod-ed parent, which is a witness with effects that can leave that directory behind in CI. So classification is split from effect in both modules and the discriminating input is a Bool. That is the third time in this PR the same split was the answer. Evidence, executed: an_identification_refusal_that_cleaned_up_... true an_identification_refusal_whose_workspace_survived_names_the_path true a_netrc_write_failure_that_cleaned_up_reports_no_credential... true a_netrc_partial_write_that_survived_removal_names_the_path true a_netrc_path_that_was_never_ours_is_not_reported_as_ours true Each pair is its own control: same inputs, one Bool varying, asserting opposite arms and explicitly rejecting each other's, so a classifier that ignored the Bool must flip one of them red. The new variants forced four consumers to declare a position, two of them (bmc_onboard, srv3_boot_once_cd) outside this PR's subject. That census is why these are variants and not a field. SCOPE, STATED RATHER THAN LEFT IMPLICIT: `grep -rn 'let _ = shell\.' dag/` finds 19 further instances of this class outside this PR -- package_delivery 11, provider_wire_evidence 5, merge-admission instruments 3. All five modules in this PR's scope are now 0. The remainder is not fixed here and is not silently dropped either; it needs its own change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…ndary, and make the scheme follow the negotiation Four blocking findings from the side-chat review of 71aa00b. All four verified against the code before being touched; all four were real. 1. A CREDENTIAL-BEARING PATH REACHED A PRINTED DIAGNOSTIC netrc_write_refusal modelled the case where a partial netrc could not be deleted, carried the path as a printable NonEmptyStr, and the delivery layer concatenated it into a refusal cause as "(at <path>)" -- which the wet-run actuator prints. So on precisely the arm where the shred FAILED, a diagnostic named the file still holding a printer access code. The standing rule forbids a path that dereferences to a credential, and the annotation I had written beside it asserted that naming the path "leaks nothing". That claim is now retracted in the source rather than quietly deleted. MY FIRST REPAIR FOR THIS DID NOT HOLD, AND THE CONTROL IS WHAT CAUGHT IT. I sealed the locator as a sole_constructor CredentialResidueLocus on the theory that restricting construction also prevents rendering. A control that cast the sealed value with `as String` and asked whether the result contained the fixture path COMPILED AND ANSWERED TRUE. sole_constructor governs where a value may come FROM, not what a holder may do with it -- a distinction this same file already records for NetrcBinding, and which I then relied on for a property it does not provide. Without that control I would have shipped a "structural" guarantee that was not one. The locator is therefore not carried at all. A value that does not hold the path cannot be made to render it, under any cast, by any consumer. The replacement control now REFUSES at the compiler -- `field 'locus' not found` -- so the bad state is unwritable rather than merely unwritten. The path stays inside netrc_binding, where the placement that created it already has it in scope and is the only authority that could act on it. 2. THE NetrcBinding SEAL WAS BYPASSABLE AT THE BOUNDARY THAT MATTERS upload_command_for and project_upload_command took a bare FilePath, so the seal proved nothing where an authenticated transfer is actually represented: a caller could pass any path and the emitted argv would be identical to the safe one. A witness in this very file did exactly that, supplying a fixture path it had never placed -- the live demonstration that the boundary was open. The PR body meanwhile claimed the builder took a NetrcBinding, which is what kept the gap invisible. Both product-level builders now consume NetrcBinding and project the path internally. curl_ftps_upload_command stays FilePath-parametric on purpose: it is curl syntax, not a place a credential guarantee can live. The witness drops to that helper, because it can no longer forge what production requires. 3. FtpsExplicit WAS MODELLED AND REALIZED AS IMPLICIT ftps_upload_url derived the PORT from the negotiation and then emitted "ftps://" unconditionally. curl reads ftps:// as implicit TLS from the first byte and ftp:// + --ssl-reqd as an explicit upgrade, so a modelled explicit endpoint produced ftps://host:21 -- implicit TLS aimed at the explicit port, the exact mismatch the type's own commentary claims it makes unspellable. The Bambu path is implicit so the wet run never exercised it; the generic authority was false regardless, and a type that is only right on the path someone happened to measure is not an authority. Scheme now derives from negotiation, with a two-scheme witness beside the existing two-port one. 4. THE RESIDUE DISTINCTION WAS ERASED BY THE CONSUMERS THIS PR CHANGED bmc_onboard.write_netrc and srv3_boot_once_cd mapped both refusal arms to the same `false`, in the same change that introduced the second arm -- the caller learned "not written" and could not learn "credential material may still be on disk", which is a different remedy: retry versus clean up first. That is the defect this PR exists to remove, committed one function away from the fix. Both now preserve the fact. bmc_onboard derives its five refusal reasons from one outcome-to-reason function rather than five literals, because a distinction threaded by hand at five sites is a distinction that survives at some of them. Evidence, executed: the_ftps_scheme_follows_the_negotiation_in_both_directions true an_explicit_endpoint_is_never_emitted_as_an_implicit_url true a_netrc_write_failure_that_cleaned_up_reports_no_credential... true a_netrc_partial_write_..._states_the_fact_without_the_path true a_netrc_path_that_was_never_ours_is_not_reported_as_ours true w_the_upload_url_carries_the_derived_name_not_the_local_one true w_no_credential_is_ever_spelled_into_the_upload_argv true Controls: binding a `locus` field from a consumer is refused by the compiler; the earlier seal-based attempt returned true and is why the design changed. One witness was RENAMED rather than left: a_netrc_partial_write_..._names_the_path asserted the property this change removes, so the name would have been false. Also fixes the duplicated comment fragment review 61384 noted, and a repo-wide scan for the same splice artifact found no others. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…air prose, and fix the 4c grain that reddened the floor Three things, one of which is a CI red of my own making. THE FLOOR LANE REFUSED 951eb37, AND IT WAS RIGHT Four annotation lines I added inside the srv3 netrc match are inside a DECLARATION BODY, and 4c models module-item grain only. That is the fourth time this session I have put an annotation inside a body -- previously a service body and a match arm. A match arm is a declaration body; the rule has no in-body form to reach for, and I keep reaching for one. Hoisted above the enclosing declaration, and the note now says why it lives there. A scan of every file this branch touches finds no other instance. THE CONTRADICTORY ENDPOINT WAS STILL SPELLABLE The previous commit made the URL scheme derive from the negotiation, and the type's commentary claimed derivation makes the mismatch impossible. It did not: FtpsEndpoint was an open struct, so FtpsEndpoint { port: 21, negotiation: FtpsImplicit } remained perfectly writable and produced exactly the connection failure the type exists to prevent. A derivation only helps callers who USE it. FtpsEndpoint is now sole_constructor with ftps_endpoint deriving the port from the negotiation, so the pair cannot be authored at all. The control confirms it at the compiler rather than by inspection: authoring that pair in a witness is refused with "sole_constructor type 'FtpsEndpoint' cannot be constructed outside its defining module". That is the invalid state having no constructor, not a check that catches it afterwards. Deliberately NOT closed: a non-standard FTPS port. The protocol permits one and a device may need it. That would be a second, differently-named constructor in the module -- a deliberate act rather than a field nobody noticed was free. PROSE FROM A REPAIR I ABANDONED Three notes still described the sealed-locator design that did not hold -- netrc_binding saying a failed cleanup "names the file", and bmc_onboard and srv3 saying "the locus is sealed". There is no locator and no seal in the final type. Comments asserting a design the code does not have are worse than no comment, because they read as the specification. All three now say what the code does and name the abandoned attempt rather than hiding it. Evidence, executed: an_explicit_endpoint_is_never_emitted_as_an_implicit_url true w_the_ftps_port_follows_the_negotiation_in_both_directions true w_the_upload_url_carries_the_derived_name_not_the_local_one true Control: authoring port=21 with FtpsImplicit is refused by the compiler. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…0-cad-toolchain # Conflicts: # dag/gunbc/srv3/srv3_boot_once_cd.dag
…d already disproved Side-chat review of 05e8f4d plus an audit of my own PR body. None of these are behavioral; all four are text asserting something the code does not do, which is the failure mode that keeps a real gap invisible. THE PR BODY CLAIMED A SIGNATURE THAT NEVER EXISTED It said curl_ftps_upload_command takes a NetrcBinding. It does not and should not -- it is curl syntax, not a place a credential guarantee can live. I fixed the CODE for this in the previous commit and wrote in that commit message that the body was corrected, then never edited the body: the executing half landed, the asserting half did not, and the executing half made it look done. The body now states what is true and says plainly that the old sentence was never true and that the seal WAS genuinely bypassable at upload_command_for until this PR closed it -- because that overclaim is what kept the gap past three reviews. THEN I AUDITED THE POPULATION INSTEAD OF THE INSTANCE Second false claim in one body is a signal, so I extracted all 42 backticked identifiers from it and checked each against the tree. Two more were unciteable: `LocusUndeclared` and `LocusConflicted` exist nowhere -- the variants are PrinterCredentialLocusUndeclared and PrinterCredentialLocusConflicted. Not false, but a reader grepping what the body printed finds nothing, which is what section 3's cite-the-symbol rule forbids. Only unresolved tokens now are two SHAs. A HEADING SURVIVED THE PARAGRAPH IT INTRODUCED netrc_binding still led with "THE RESIDUE LOCATOR IS SEALED" above a paragraph explaining that the seal was abandoned because it did not hold. Replacing the body of a note and leaving its heading is how a note comes to assert the opposite of what follows it. TWO CLAIMS CONTRADICTED BY THIS BRANCH'S OWN MEASUREMENTS printer_project_delivery said the A1 certificate is "self-signed" while extdeps.ietf.ftps -- one import away, on this branch -- records the measured result: a certificate issued by C=CN, O=BBL Technologies Co., Ltd, CN=BBL CA, a vendor chain, explicitly "not a self-signed leaf". That matters because "self-signed" makes disabling verification sound inevitable rather than a declared weakening whose trigger is pinning that CA with --cacert. The same stale claim appeared in a witness note and is corrected there too. It also said the access code "lives only in Secret Manager". At this head neither printer's code has been materialized there, which is exactly why PrinterCredentialProvisionRequired and ProjectDeliveryProvisionRequired exist and why the wet run refuses. Describing the destination state as the current one is how a refusal path starts reading as an edge case rather than where we are. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 6, 2026
…y count Two honest measurements disagree by one: shell-only reads 14, shell-or-Filesystem reads 15. The wider selector is the right one -- the defect is an ignored effect outcome, not a property of which service produced it -- and it is now written out rather than implied by a grep. Membership is rostered by module, enclosing declaration and the arm each sweep follows, because provider_wire_evidence's five members share one declaration and would collapse to one at declaration grain. bmc_onboard write_netrc is named as deliberately out of population rather than silently dropped: #10574 deletes it, so the original 19 was branch-relative. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
…r roster to the fleet, restore a caller I stranded
Review 61400 filed two blocking items; CI independently found a third that is
mine. All three verified against the code before being touched.
CREDENTIAL RESIDUE WAS DISCHARGED BY DELETING THE PAYLOAD
The netrc residue arm routed through refuse_and_drop, which derived cleanliness
from the PAYLOAD removal alone. So a refusal that already knew a credential may
be on disk, whose payload copy happened to delete cleanly, returned an ordinary
ProjectDeliveryUnattempted. The obligation survived in the cause TEXT and was
erased from the TYPE -- worse than losing both, because a consumer matching the
outcome sees a clean refusal while a human reading the message sees a credential
on disk, and only one of those is machine-checkable.
Residue now has two independent sources and cleaning one cannot discharge the
other. The parameter is named `clean` rather than `removed`, because that is
what it had to mean all along.
This is the FIFTH appearance of one class in this PR -- a distinction kept in
prose and dropped from the carrier -- and the SECOND I introduced while fixing
an earlier instance of it.
THE FLEET'S EXCEPTION ROSTER WAS LIVING IN THE PROTOCOL MODEL
extdeps.ietf.ftps enumerated UnverifiablePeerClass, and the note beside it
argued that "adding a new excuse requires editing this module, where it is
reviewable" -- which states the layer inversion out loud without noticing. That
is admission control over which devices a CONSUMER FLEET may waive verification
for, living inside a model of an IETF protocol, and the tell was in the name:
DeviceCertificateSubjectIsSerialNotAddress and its measurement are an
observation of THIS repository's printers. Section 3 is explicit that
observations produced here are receipts in the observing product layer, never
facts owned by the observed upstream.
FtpsPeerVerification and FtpsEndpoint are now parametric over the peer class,
and gunbc.fleet.printer_project_delivery declares its own closed
PrinterUnverifiablePeerClass. The weakening stays non-self-authorising because
the roster is still closed WHERE IT IS DECLARED -- it simply is not declared in
extdeps any more. One shape, N bound reason types. A second fleet with a
different device no longer has to edit a protocol module it does not own.
AND I STRANDED A CALLER IN ANOTHER MODULE
Splitting write_netrc into write_netrc_outcome removed a symbol that
gunbc.tools.bmc_first_contact imports and calls. I had grepped for callers
INSIDE bmc_onboard and stopped there. The namespace-wave-admission phase caught
it exactly: NewUnresolvedness binding bmc_first_contact::bmc_first_contact
`write_netrc` -- base {gunbc.tools.bmc_onboard} -> head {}. Migrated to the new
API rather than restoring the Bool, so first-contact reports the residue fact
too instead of "netrc write failed". Repo-wide sweep for the removed name: 0.
Evidence, executed:
a_credential_residue_survives_a_successful_payload_removal true
a_refusal_with_no_prior_residue_can_still_report_clean true
w_peer_verification_is_waived_only_by_the_enumerated_peer_class true
an_explicit_endpoint_is_never_emitted_as_an_implicit_url true
an_identification_refusal_whose_workspace_survived_names_the_path true
The residue pair holds PAYLOAD REMOVAL FIXED AT SUCCESS and varies only prior
credential residue, because varying the removal would not have caught this: both
arms of the old shape cleaned the payload up.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…g about the collapse The side-chat review caught that my discriminating pair for the credential-residue defect exercised nothing it claimed to. Both witnesses called unattempted_delivery(clean: <literal>) -- the ALREADY-COLLAPSED value. They varied the OUTPUT of the join while asserting a property OF the join, so they would have stayed green if the production expression regressed to `clean: removed`, which is exactly the defect they were written to prevent. Worse, I described that pair in the previous commit message as "holds payload removal fixed at success and varies only prior credential residue". It did neither: it never touched payload removal or residue_already at all. That is the same shape as the /proc fixture earlier in this PR -- evidence whose intended negative could not occur -- and I produced it while fixing an instance of the class it belongs to. The join is now `delivery_is_clean(payload_removed, residue_already)`, a pure two-input function, so a fixture can name "payload removed but credential residue known" directly instead of approximating it one layer down. Both witnesses pass payload_removed: true and vary ONLY residue_already, through that function. Evidence: a_credential_residue_survives_a_successful_payload_removal true a_refusal_with_no_prior_residue_can_still_report_clean true Control, which is the point: regressing the join to `payload_removed` alone -- the exact defect -- flips the first witness to false. The previous pair would have stayed green through that same regression. Restore verified byte-identical. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
…s why I set out to correct container_execution as stale. It was not stale, and the attempt is worth recording because it nearly landed a regression dressed as a fix. The row asserts the session image refuses the slicer with 36 unresolved sonames. A later session (mine) resolved 33 of them from conda-forge, ran the binary, and produced a real slice -- which reads as a falsification. It was not one. The resolver publishes no aarch64 build of libwebkit2gtk-4.1 or libjavascriptcoregtk-4.1 at all, so the residue is not a package nobody had installed yet; it is absent from the channel, and no amount of resolving closes it on this architecture. What made the binary start was a fabricated dependency: empty stub objects carrying the two sonames and none of their symbols. The binary references 99 webkit symbols the stubs do not define, and LD_BIND_NOW aborts on the first of them. The slice completed only because the CLI path never calls into webkit -- a property of the code path taken, not of the environment. That is exactly the hand-assembled toolchain this module's opening annotation already names and rejects, rediscovered as a good idea by the author of the warning. The receipt now carries the non-transience, so the next reader who resolves 33 of 36 does not reach my conclusion. Nothing else changes: both witnesses still assert both recorded hosts refuse and neither yields a plan, and the sealed Ready arm is untouched -- an authored refusal remains safe in the direction an authored value may lie, and Ready remains unauthorable. Verified independently: the pinned container route (print-n/orca:2.4.2 on srv2, the route this module declares sound) slices the same input to BYTE-IDENTICAL toolpaths -- 34,904 motion commands equal, differing only in a generation timestamp and a nondeterministic object id. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs
briansrls
pushed a commit
that referenced
this pull request
Sep 6, 2026
…cope (#10664) * Classify the 19 discarded shell-effect outcomes outside the printer scope 16 of them are lawfully best-effort under one stated discriminator; 3 owe a real distinction and sit in a subsystem with no producer and no consumer. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Record the entry-vs-module map: a cut here reds a witness and shrinks a monotone roster "Dormant at both ends" overstated it. The two Bool entries have no callers; the modules do not. merge_admission_fetch_stall_deadline_seconds is imported by merge_admission_current_context and asserted by an enrolled witness, and read_tested_subject / read_floor_receipt are enumerated sites of the filesystem_io absence-establishment monotone roster, whose rows may leave by deletion. A path-shaped grep and a module-shaped grep answer different questions here; only the second finds importers. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Check all 16 against the mktemp-origin test by construction site, not by name cache_dir is the member whose name asserts a lifetime its construction does not have: both sites are shell.Mktemp.Dir(), so it is per-run and the discriminator holds. Every other binding the sweeps reach is likewise a shell.Mktemp.* call with no other origin and no shadowing. Recorded at the declaration, with the naming defect named separately rather than fixed here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * The population moved 19 -> 15: carry the ref the count was taken against main deleted materialize_spark_serving_ollama_runtime_bundle with the whole spark-serving archive-admission block while this was open, so four members left by deletion of the subject rather than by being consumed -- package_delivery 11 -> 7, the other three modules unchanged at 5 / 2 / 1. The annotation citing that function by name would have described nothing. Every count now names the ref it was measured at, because a bare number cannot tell a real change from a stale citation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * State the selector and identify members by declaration and arm, not by count Two honest measurements disagree by one: shell-only reads 14, shell-or-Filesystem reads 15. The wider selector is the right one -- the defect is an ignored effect outcome, not a property of which service produced it -- and it is now written out rather than implied by a grep. Membership is rostered by module, enclosing declaration and the arm each sweep follows, because provider_wire_evidence's five members share one declaration and would collapse to one at declaration grain. bmc_onboard write_netrc is named as deliberately out of population rather than silently dropped: #10574 deletes it, so the original 19 was branch-relative. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Three sites, two defects, two modules: say which count is which Two independent reviewers summarized the OutcomeSemanticallyRequired class as "two" -- the count of defects and of modules, not of sites. A classification whose thesis is that a count needs its selector, its ref and an identity roster should not leave its own count ambiguous. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Name the instrument: drop the transcribed census totals from all four modules DESIGN §6 -- a measurement is cited by naming the producer that re-derives it, never by copying its numbers into prose. Adding a revision and a selector made the totals attributable without making them re-derivable, and four modules each holding a copy is four ledgers maintained by hand independently of their subjects. The totals are gone; what remains is the SELECTOR (the instrument that re-derives the population at any ref) and the members NAMED by module, declaration and arm. The identity roster also carries what a total never could: main's deletion of materialize_spark_serving_ollama_runtime_bundle retired its members by deletion of the subject, which a count cannot distinguish from a member being consumed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 6, 2026
…cope (#10664) * Classify the 19 discarded shell-effect outcomes outside the printer scope 16 of them are lawfully best-effort under one stated discriminator; 3 owe a real distinction and sit in a subsystem with no producer and no consumer. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Record the entry-vs-module map: a cut here reds a witness and shrinks a monotone roster "Dormant at both ends" overstated it. The two Bool entries have no callers; the modules do not. merge_admission_fetch_stall_deadline_seconds is imported by merge_admission_current_context and asserted by an enrolled witness, and read_tested_subject / read_floor_receipt are enumerated sites of the filesystem_io absence-establishment monotone roster, whose rows may leave by deletion. A path-shaped grep and a module-shaped grep answer different questions here; only the second finds importers. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Check all 16 against the mktemp-origin test by construction site, not by name cache_dir is the member whose name asserts a lifetime its construction does not have: both sites are shell.Mktemp.Dir(), so it is per-run and the discriminator holds. Every other binding the sweeps reach is likewise a shell.Mktemp.* call with no other origin and no shadowing. Recorded at the declaration, with the naming defect named separately rather than fixed here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * The population moved 19 -> 15: carry the ref the count was taken against main deleted materialize_spark_serving_ollama_runtime_bundle with the whole spark-serving archive-admission block while this was open, so four members left by deletion of the subject rather than by being consumed -- package_delivery 11 -> 7, the other three modules unchanged at 5 / 2 / 1. The annotation citing that function by name would have described nothing. Every count now names the ref it was measured at, because a bare number cannot tell a real change from a stale citation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * State the selector and identify members by declaration and arm, not by count Two honest measurements disagree by one: shell-only reads 14, shell-or-Filesystem reads 15. The wider selector is the right one -- the defect is an ignored effect outcome, not a property of which service produced it -- and it is now written out rather than implied by a grep. Membership is rostered by module, enclosing declaration and the arm each sweep follows, because provider_wire_evidence's five members share one declaration and would collapse to one at declaration grain. bmc_onboard write_netrc is named as deliberately out of population rather than silently dropped: #10574 deletes it, so the original 19 was branch-relative. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Three sites, two defects, two modules: say which count is which Two independent reviewers summarized the OutcomeSemanticallyRequired class as "two" -- the count of defects and of modules, not of sites. A classification whose thesis is that a count needs its selector, its ref and an identity roster should not leave its own count ambiguous. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA * Name the instrument: drop the transcribed census totals from all four modules DESIGN §6 -- a measurement is cited by naming the producer that re-derives it, never by copying its numbers into prose. Adding a revision and a selector made the totals attributable without making them re-derivable, and four modules each holding a copy is four ledgers maintained by hand independently of their subjects. The totals are gone; what remains is the SELECTOR (the instrument that re-derives the population at any ref) and the members NAMED by module, declaration and arm. The identity roster also carries what a total never could: main's deletion of materialize_spark_serving_ollama_runtime_bundle retired its members by deletion of the subject, which a count cannot distinguish from a member being consumed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 7, 2026
…LocalRepoWetLane
* Control (b) seed-unavailable behavioral receipt for dag/std/logic.dag
Route the seed-unavailable control (b) onto LocalRepoWetLane per operator
ruling (session bright-ram-778, msg msg_aee406be-d956-48c7-88a6-fed609d5fcc9):
- New transport module (tools.self_host_logic_seed_unavailable_transport):
emit dag/std/logic.dag with the real gunbc binary, compile the emitted
Rust WITHOUT the seed crate (zero-external-dependency crate, self-contained
pure std types), run the witness binary, verify expected constants.
The emitted code from dag/std/logic.dag is self-contained with no external
crate imports beyond std, so the cargo build requires no network access and
the seed crate is absent at link time -- seed linkage is structurally
impossible by construction (DESIGN section 7).
- New witness test (test.claim.self_host_logic_seed_unavailable_witness):
self_host_logic_seed_unavailable_receipt_holds -> Bool.
- Exclusion row in gunbc.ci_layer_roots.witness_exclusion_frontier:
classified as LocalRepoWetLane, excluded from hermetic discovery because
the transport operations have no mock_response.
- Schedule entry in v2.workflow.local_repo_wet_terminal.local_repo_wet_schedule:
enrolled for execution by the required floor's local-repo wet lane.
This control tests whether the emitted candidate depends on the seed crate.
If the emitted code fails to build or run without the seed, that failure IS
the finding -- it would mean the emitted code is not in fact self-contained,
a first-order fact about self-hosting.
This is NOT a substitute for control (a). Control (b) tests seed independence;
control (a) tests whether the comparison discriminates. Neither establishes
the other, and a green (b) does not cover a missing (a).
* Correct control (b): use standard emitted-crate deps but exclude v1-compiler seed; document embedded-source boundary
The parent (bright-ram-778) identified that emit_v2_rt_module unconditionally
emits src/v1_rt.rs into every emitted Rust crate. This file is the v2 runtime
shim -- seed-derived source embedded in the emitted source tree (fourth
seed-dependency mode not denied by crate-absence controls).
Corrections:
- Use standard emitted-crate dependencies (im, serde, stacker, clap, etc.)
which v1_rt.rs requires for its runtime primitives
- Deliberately exclude v1-compiler (the seed crate) -- this is what control (b)
actually tests: the emitted logic builds and runs without the seed library
- Document the boundary: v1_rt.rs IS present (unconditional emitter behavior)
but its functions are NOT CALLED by the emitted logic module (dag/std/logic.dag
is pure type declarations and function definitions, no v1_rt references)
- The control denies execution, linkage, and fallback modes; names embedded
source as the fourth mode with stated boundary
- Update exclusion reason and schedule comments to match
* Enforce v1_rt call-site check in control (b) transport
Per review (bright-ram-778): the embedded-source boundary for the
unconditionally-emitted v1_rt.rs must be ENFORCED BY EXECUTION rather
than narrated in prose. The transport now:
1. Reads the emitted subject module (src/std_logic.rs for dag/std/logic.dag)
2. Checks for v1_rt:: call sites via string_contains
3. Refuses if any are found (typed refusal: subject outside denial scope)
4. Only proceeds to cargo build + witness run if the check passes
The red IS authorable: point this transport at any module that uses
concat/trim/length/rc_empty_map and the v1_rt:: check fires.
Also removed all "dead code elimination" claims from comments per
instruction: the source is embedded either way, elimination is the
optimizer's choice not a structural guarantee.
* Route control (a) onto LocalRepoWetLane alongside control (b)
Rehome self_host_logic_behavioral_witness_test from FalsifierSelfHostWet (dead,
DeclaredCadenceUnrealized) to LocalRepoWetLane (live, same lane as control (b)).
Per operator ruling (bright-ram-778): a control that EXISTS and is PROVEN but
NEVER EXECUTES is the worst of the three states -- worse than absent, because
it gets cited as coverage while carrying no information. DESIGN is explicit that
a tier where the machinery exists but nothing gates on it is itself a lie.
Changes:
- ci_layer_roots.dag: change control (a) exclusion from FalsifierSelfHostWet
to LocalRepoWetLane, preserve the FalsifierSelfHostWet provenance in reason
- local_repo_wet_terminal.dag: add WetScheduledClaim for control (a)
- self_host_logic_behavioral_witness_test.dag: update documentation to reflect
new routing and the separation from control (b)
Both controls now route through the same LocalRepoWetLane lane. The emission
target (dag/std/logic.dag) is shared; each currently does its own emit step.
A future optimization could share the emit and diverge only at cargo build.
This completes the brief's requirement: TWO controls on the existing agreement
corpus, both routed through a live executor.
* Widen v1_rt call-site check to all emitted .rs files (excluding v1_rt.rs)
Replace single-file check (src/std_logic.rs only) with crate-wide check:
enumerate all .rs files via shell.Find.FilesByNameSorted, exclude v1_rt.rs
(which defines the runtime functions), and check every other file for
v1_rt:: call sites. A failed read or any matching file returns false
(fail-closed).
This makes the instrument's population equal to the claim's population:
the control asserts NO emitted file calls into the seed runtime, and the
check covers every emitted .rs file.
* Add fixture test for v1_rt:: call-site check logic
Hermetic fixture that proves the slbu_check_no_v1_rt_calls mechanism
discriminates, without requiring gunbc emit or cargo build:
- GREEN: clean file with no v1_rt:: reference passes
- RED: file containing v1_rt::lookup fails the check (discriminator)
- GREEN: v1_rt.rs file (excluded from check) with v1_rt:: content permitted
These operate on synthetic file contents via Filesystem.Write/Read and
string_contains -- testing the CHECK FUNCTION in isolation.
* Fix receipt defects and §4c annotations on controls (a)/(b)
- Remove unused slbu_scaffold_dissolution_trigger (review 61030 finding 1)
- Delete the unreferenced DissolutionCondition data row and its import
- Fix vacuity in slbu_check_no_v1_rt_calls:
- Check found.success and refuse on failed file enumeration
- Refuse on empty file list (list_length > 0 guard) — no subject to check
- Fix exact-path exclusion: use ends_with(..., '/v1_rt.rs') instead of
string_contains substring match (was matching foo_v1_rt.rs etc.)
- Fix ordering: move scan to AFTER Cargo.toml and main.rs writes, so
what it scans is what cargo builds, not an intermediate tree
- Fix acceptance sentence: remove 'CONSTRUCTION OVER PROSE' and
'ENFORCES by execution' claims — a spelling search is a per-subject
validator, not a construction wall, and cannot carry an enforcement
claim. State what it actually does.
- Hoist 12 §4c grain violations from inline comments between
WetScheduledClaim elements in local_repo_wet_schedule() to a single
standalone // block above the function, joined by symbol identity
rather than adjacency
* Fix subject-presence check and answer ordering question
- Replace the non-emptiness guard with a genuine subject-presence check:
verify that a file ending with '/std_logic.rs' is in the enumeration
(the expected emitted module for dag/std/logic.dag). The name
'subject_present' now matches what the code does.
- Trim comment that claimed 'empty file list' was checked (it was, but
only as a proxy; the real check is now the specific module filename).
* Remove function-body // comments that caused 32 parse FAIL errors
The dag language only admits source annotations at module-item grain.
Comments (//) inside function bodies produce:
'source annotation sits inside a declaration body'
Removed 15 comment lines from self_host_logic_seed_unavailable_transport.dag
and 2 comment lines from the check_fixture_test.dag that were inside
function/test bodies. Essential rationale preserved as module-item
annotations above the function definitions.
* Fix ends_with call syntax: method call, not free function
ends_with is a String method in the dag language, invoked as
f.ends_with(suffix: '/std_logic.rs') not ends_with(s: f, suffix: ...).
The free-function form caused a runtime NoSuchFunction error on the
required-witnesses-floor run at 041a0c2.
No parse FAIL errors remain — confirmed 0 parse errors in the failed
run's logs. The only error was this runtime NoSuchFunction for ends_with.
* Replace ends_with with string_contains for path matching
ends_with is not available as either a free function or a method
on Primitive(String) in the dag runtime resolution context. The
free-function form produced NoSuchFunction, and the method-call
form produced 'no method surface on Primitive(T)'.
Use string_contains with path prefix + exact root match for the
v1_rt.rs exclusion (matching /v1_rt.rs or bare v1_rt.rs), and
string_contains for the subject presence check (std_logic.rs is a
unique enough filename in the emitted crate to avoid false positives).
* Fix cargo build failure: add missing text_lookup_work_counter feature
The emitted v1_rt.rs uses '#[cfg(feature = text_lookup_work_counter)]'.
Without declaring this feature in Cargo.toml, newer rustc emits
'unexpected cfg condition value' errors (under -D warnings configured
by the build environment). The behavioral transport (control a) already
has this fix; the seed-unavailable transport (control b) was missing it.
This caused the cargo build to fail with exit 101 on the floor run,
which was the actual failure behind observed=failed at 047cdae.
* Hoist two irrecoverable facts back as module-item annotations
Re-added two facts that were deleted with the function-body // cleanup
at 041a0c2, now at module-item grain where the grammar admits them:
1. Validator-not-wall claim (above slbu_cargo_toml, attached to the
call-site check): restores the third agreement site saying this is
a per-subject spelling search, not a construction wall. Three sites
now agree again (transport, witness test, ci_layer_roots).
2. Ordering rationale (above slbu_seed_unavailable_receipt): documents
that the scan must run after the writes because this substrate
evaluates let bindings in declaration order (eval_block, not data
dependency), so the ordering is carried by line position. A future
editor who moves the scan above the writes reintroduces the defect.
Also kept the 'NO seed crate dependency' note above slbu_cargo_toml
(the absence of v1-compiler is not visible from the code).
* Fix fixture test: route through real transport function, not a re-implementation
The fixture was re-implementing check_no_v1_rt_calls_in_file inline,
creating a parallel predicate that already diverged (no v1_rt.rs
exclusion). The third test (v1_rt_rs_with_calls_permitted) never
invoked any variant of the check, making it decorative.
Fixed: fixture now imports slbu_check_no_v1_rt_calls from the real
transport and calls it over a synthetic temp directory. Three tests
mirror the three behaviors: clean dir passes, v1_rt:: call in a
non-v1_rt file fails, and v1_rt.rs containing calls still passes
(the exclusion works). All three invoke the real function.
This resolves review 38602 findings 1 and 2.
* Thread writes_ok through slbu_check_no_v1_rt_calls for structural ordering
The ordering between the Cargo.toml/main.rs writes and the v1_rt:: call-site
scan is now enforced by DATA DEPENDENCY rather than by line position: the
scan accepts writes_ok (cargo_toml.success && main_rs.success) as a parameter,
so it cannot be evaluated until both writes have completed. Reordering the
scan above either write would reference an unbound variable — compile-time
refusal.
The ordering comment above fn slbu_seed_unavailable_receipt now names the
structural dependency rather than warning about line order.
Fixture test updated to pass writes_ok: true for all three cases (the
fixture tests the check logic in isolation; the write ordering is a
deployment guarantee tested by the wet lane).
* Honestly document containment-test approximation for unavailable suffix method
The v1_rt.rs exclusion and std_logic.rs subject check use string_contains
rather than ends_with, because ends_with is declared in std.primitives and
handled by the interpreter but not registered in the resolver's method
surface for Primitive(String) — a declared known gap at
v1_compiler_infer.rs:7428 (same class as starts_with on List receivers).
The annotation now says the check is a CONTAINMENT TEST standing in for
a suffix test, and names the gap that would let a tighter rung arrive.
* Fix false positive in v1_rt:: check: exclude use-import lines
The emitted std_logic.rs legitimately imports types from the v1_rt runtime
via 'use crate::v1_rt::{...}'. The previous check flagged ALL occurrences
of v1_rt:: in non-v1_rt files, including these use-import lines.
Changed to per-line check: a line containing v1_rt:: is a violation UNLESS
it is a use-import line (contains 'use crate::v1_rt'). This correctly
passes on the emitted subject module while still catching actual call-site
references like v1_rt::lookup(key).
Also fixed one remaining body-grain // comment in the fixture test that
was missed due to a brace-counting bug in the scanner script.
* Add 4b(3) rung drop row for spelling-search validator
The v1_rt:: call-site check in the seed-unavailable transport is a
per-subject spelling search (string_contains), not a construction wall.
This registers the honest rung: structurally-guaranteed -> mitigatable,
with the restoration trigger being the NEXT-RUNG TRIGGER already stated
in the transport header (emit runtime fragments from modeled source).
Also includes items (1) and (2) from e0b0c22 (fixture now imports
and calls the real transport function, third test invokes the real check)
and the per-line v1_rt:: check fix from 23bc824 (exclude use-import
lines to avoid false positives on legitimate runtime type imports).
* Clarify writes_ok as ordering device, fixture scope note
- writes_ok annotation now states it is an ORDERING DEVICE, not an error
signal; the write failure is separately typed as slb_stage_incomplete
through staged, so the conflation is unreachable on the real path.
- Fixture header notes it passes writes_ok: true and CANNOT detect an
ordering regression — that is deliberate, covered by the wet lane.
* Fix seed-linkage check: search for v1_compiler:: not v1_rt::
The check was looking for the wrong pattern. v1_rt:: appears in every
emitted module as legitimate same-crate runtime shim usage (e.g.,
'use crate::v1_rt::{VecCompat, VecJoin}'). This is infrastructure,
not seed linkage.
The actual seed crate prefix is v1_compiler:: — the same spelling the
behavioral transport uses for its seed leg, and the same crate that is
deliberately absent from Cargo.toml. The manifest half (no v1-compiler
dependency) is the stronger claim — structural rather than a spelling
grep — and the spelling check now searches for the correct namespace.
The per-line complexity (previously needed to exclude use-import lines
from v1_rt:: false positives) is no longer needed because v1_compiler::
has no false positives in emitted modules. The v1_rt.rs exclusion
remains for defense-in-depth (v1_rt.rs may reference v1_compiler in
comments about seed source files).
* Sequence temp-directory cleanup after all operations via dependency token
The cleanup Remove calls could race ahead of the scan, build, and witness
operations on a dataflow-ordered substrate. Fixed by threading a sequencing
token (seq) derived from the receipt verdict through the cleanup: seq is
computed as verdict || !verdict, and the cleanup calls consume seq as an
operand. On any scheduling substrate, cleanup cannot evaluate before
verdict because seq does not exist until verdict is available.
* Register spelling-search rung drop in the rung_drop roster
* chore: regenerate drifted generated artifacts (ci auto-heal)
Ledger-Repair-Judged: docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md self_host_spelling_search_check
* Replace spelling-search rung-drop with guarantee-stall row
The spelling-search check in the seed-unavailable transport was always a
VALIDATOR (per-subject spelling search for v1_compiler:: references), not
a construction wall. It never held the structural rung, so a RUNG DROP
with previous: StructurallyGuaranteed fabricated an event.
WHAT CHANGES:
- DELETE dag/gunbc/rung_drop/self_host_spelling_search_check.dag
- REMOVE SelfHostSpellingSearchCheck arm from LegacyProseIdentity
- REMOVE self_host_spelling_search_check from rung_drop roster
- CREATE dag/gunbc/guarantee_stall/self_host_spelling_search_stall.dag:
GuaranteeStall with current=Mitigatable, ceiling=StructurallyGuaranteed,
blocker=AwaitsOneGrounding, population=BoundedPopulation (2 members)
- ENROLL the new stall in guarantee_stall roster
- NARROW the transport header: the spelling search is a VALIDATOR, not a
construction wall; the structural half is the manifest (v1-compiler
absent from Cargo.toml)
The grep against the actual emitted output confirms zero false positives:
no emitted .rs file contains 'v1_compiler::'. The committed stage0 mirrors
(src/v1/stage0/src/) are a different population (19 hand-authored files)
and are not scanned by the transport.
Carrier: guarantee_stall (correct), not rung_drop (wrong).
* Replace tautology with standard cleanup pattern
The seq = verdict || !verdict tautology was a workaround for ordering
cleanup after verdict evaluation. Replace it with the standard pattern
used by emit_host_transport and other instruments: cleanups are let-bound
in declaration order after verdict, and their results are ANDed into the
receipt expression. This eliminates the constant-folding risk (cleanups
always evaluate because they feed the return value) and the unused-binding
risk (cleanup results are consumed by the && chain).
Also narrow the transport header: the spelling search is a VALIDATOR
not a construction wall; the structural half is the manifest
(v1-compiler absent from Cargo.toml).
Grep against actual emitted output confirms: 0 files contain
'v1_compiler::' (with colons). The committed stage0 mirrors are
a different population and are not scanned by the transport.
* Fix stale comment referencing removed seq tautology
* Add dissolution trigger for hand-authored Cargo.toml
Per review 61218 finding 2: the hand-authored Cargo.toml (literal TOML
concat) is a parallel authority that will drift from the emitter's
dependency list. Adds DISSOLVES WHEN comment tying it to the emitter
producing its own Cargo.toml from the modeled dependency declaration.
Review finding 1 (rung_drop carrier mismatch) is obsolete — the file
was deleted in 715061d, replaced by the guarantee_stall row.
Review finding 3 (string_contains validator pattern) is already
documented as a validator-not-construction wall and carried by the
guarantee_stall row.
* Rename slbu_check_no_v1_rt_calls to slbu_check_no_seed_crate_refs
Per review 61230 nit: the function was named for v1_rt:: but actually
checks for v1_compiler::. Renamed to describe what it does (check for
seed crate references) rather than an obsolete subject.
* Honest cleanup comment: name the lazy-evaluation leak
The previous comment claimed cleanup 'cannot silently leak temp directories'
but under a lazy evaluation model with short-circuit &&, a false verdict
never demands cleanup_out or cleanup_src, leaking the temp directories on
the failure path. The house pattern (every transport in this codebase)
relies on strict let evaluation to guarantee cleanup execution. Naming the
gap honestly rather than asserting a guarantee that depends on the
evaluation model.
* Add exemption note for hand-authored Rust driver source
Per review 61252 finding 2: slbu_driver_main_source is hand-authored Rust
(medium-as-string) without a dissolution trigger. Unlike the Cargo.toml
(which duplicates the emitter's dependency list), the driver source is
a subject-specific behavioral test harness. Exempt because there is no
emitter-produced test driver to drift from — no parallel authority exists.
* chore: regenerate drifted generated artifacts (ci auto-heal)
Ledger-Repair-Judged: docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-rung-drops.md
* Correct cleanup comment: measured facts, not lazy-evaluation caveat
snappy-crane-234 measured: let is eager (unreferenced bindings evaluate)
and && does not short-circuit (both operands always evaluate). Cleanup
always runs. But this is a property of the current interpreter realization,
not a declared substrate guarantee — if && ever gains short-circuit
semantics, cleanup silently stops without any test going red. Filed as
its own 4b subject by snappy-crane-234.
* Tighten cleanup annotation: cite probe names and existing failure-mode
Cite snappy-crane-234 probe names (let_is_eager_when_unused,
and_demands_right_even_when_left_false) rather than transcribing their
conclusion. Replace the speculative caveat about short-circuit semantics
with a one-line cite to the existing failure-mode row
realization_arms_diverge_on_whether_the_program_refuses.
* Fix parse errors: hoist function-body /// comment to module level
The cleanup annotation comment was placed between let-bindings inside the
function body, which the compiler treats as source annotations (module-item
grain only). Moved above the function and merged with the existing module-
level cleanup comment. Also updated to cite snappy-crane-234 probe names
and the existing failure-mode row
realization_arms_diverge_on_whether_the_program_refuses.
* Fix citations in cleanup annotation: probe names, not session id
Cite the probe names (let_is_eager_when_unused,
and_demands_right_even_when_left_false) directly rather than the session
that ran them. Session ids are transient and resolve to nothing. Also fix
the residual citation: the failure-mode row exists in another lane's branch
and may not land before this PR — state as pending rather than as a tree
fact.
* Fix cleanup annotation: drop && clause, cite gunbc#10647
The &&-does-not-short-circuit clause was my framing and did not survive
measurement. Under short-circuit && the cleanup still reaches the
filesystem because effects are let-bound (eager let). The property the
transport stands on is EAGER LET, one axis. Cite the pending PR
(gunbc#10647) for the residual (no declared property guarantees this).
* Add dissolution trigger for hand-authored Rust driver blob
Per review 61312 advisory: the Rust test driver had an exemption note
but no dissolution trigger. DESIGN requires a named trigger even when
the dissolving capability is not yet built. Adds DISSOLVES WHEN the
emitter produces a behavioral witness driver for a modeled subject.
* File guarantee_stall rows for hand-authored Cargo.toml and Rust driver
Both medium-as-string sites in the seed-unavailable transport now have
guarantee_stall rows (current=Mitigatable, ceiling=StructurallyGuaranteed,
blocker=AwaitsOneGrounding, population=BoundedPopulation), matching the
pattern already used for the spelling-search validator. Per DESIGN §4b
meta-obligation 2 ('no untracked stall'): each class below its ceiling
names its next-rung trigger via the roster, not only in prose.
* Fix witness_admission_test: rehomed behavioral witness is now on LocalRepoWetLane
The self_host_logic_behavioral_receipt_holds witness was rehomed from
FalsifierSelfHostWet to LocalRepoWetLane earlier in this PR. The test
that asserts its consumer cadence still expected FalsifierSelfHostWet,
causing Bool(false). Updated to expect LocalRepoWetLane.
* Enroll fixture test on wet lane, add exclusion
The three self_host_logic_seed_unavailable_check_fixture identities were
being discovered by the hermetic floor but have no mock for file operations
(shell.Mktemp.Dir, Filesystem.Write, shell.Remove.RecursiveForce). Route
to the wet lane alongside the main witness, and exclude from hermetic
discovery via the same reason string.
* Contract migration: rename witness_self_host_logic_falsifier_wet_consumer_holds
The test function name carried 'falsifier_wet' after the witness was
rehomed to LocalRepoWetLane — a meaning fork per DESIGN §3. Renamed
to witness_self_host_logic_local_repo_wet_consumer_holds. Added
annotation explaining the rehoming and citing the authority
(ci_layer_roots.dag exclusion row). Single occurrence in tree, rename
is free.
* Enroll seed-unavailable witness in floor_route_gap
The identity executes on the local-repo wet lane (WetScheduledClaim in
local_repo_wet_terminal.dag) and held in the most recent floor run.
This enrollment records only the hermetic unreachability — it is honest
because the identity HAS a real executing route. Follows the precedent
set by the sibling self_host_logic_behavioral_witness which is already
enrolled at line 328.
* Replace bare Cons enrolment with FloorRouteGapExpectation
Migrate from the bare Cons list entry (legacy form) to the
FloorRouteGapExpectation form, which pins the identity, operation
(Parents), and ground (NoMockResponse). Carry annotation stating
enrolment is not the route — the route is the WetScheduledClaim row,
and the identity was enrolled on the wet lane and held.
* Balance the braces that made the whole tree unparseable, so this branch can execute for the first time
Three required-lane runs on this branch failed at "module index refused: 2
unparseable .dag source(s)", which reports standing=measurement_unreached --
the instrument could not be BUILT, so no floor ran, no claims executed, and
heal failed for the same reason rather than for any generated-artifact drift.
Two defects, both purely syntactic:
local_repo_wet_terminal.dag a duplicated "expectation: ExpectedToHold {}"
and its closing brace, left over from an append
floor_route_gap.dag floor_route_gap_expectation_chunk_07 opened 7
braces (fn + 6 Cons) and closed 6
Verified no subject moved: 32 wet-scheduled identities before and after with
none lost, 101 FloorRouteGapExpectation rows unchanged, and every .dag file in
the diff now brace-balanced with depth returning to 0 and never going negative.
The parser's reported location is a character offset, not a line number.
Nothing semantic is touched. The behavioral-witness rehome, the chunk_07 rows
in located/expectation form, and the annotations are all as the lane authored
them, and none of them has executed even once.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
* Model JIT runner minting and join it to the owned-cell binding (#10661)
* Model JIT runner minting and join it to the owned-cell binding
generate-jitconfig is a different endpoint from the registration-token flow
already modeled as RegisterOrganizationRunner, and the difference is the reason
this fleet wants it: a registration token is a shared secret a machine uses to
register itself and then keep durable credentials on disk, while a JIT config is
minted by the caller for one runner identity and makes the runner ephemeral by
construction. It is not a different authority -- GitHub gates both on
organization self-hosted-runners write -- so the new effect arm answers with the
same permission rather than inventing a runner-lane permission beside it.
gunbc.runner_jit_mint joins the two facts that must hold before a credential
exists at all: the fabric cell must be owned, and the App credential must
actually hold that permission. Those are separate authorities, so this module
owns neither. Ownership is checked before the credential, and its witness uses a
fully sufficient credential so only the cell can produce the refusal.
Also retargets two attempt witnesses off bind_microvm_to_cell. Its argument is
sole_constructor, deliberately, so no test outside its module can build one;
exposing a builder would punch exactly the hole the seal exists to close, so the
refusal is exercised at the composable step the binder delegates to.
A 201 with an empty encoded_jit_config refuses rather than yielding an empty
credential -- status-only branching would boot a guest holding an empty drive
that waits out its whole deadline looking healthy.
Nothing calls plan_jit_mint yet; the lifecycle controller is its caller.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
* Witness that members_owned cannot currently refuse
The review accepted this PR's coverage narrowing partly on an annotation I wrote
claiming the ownership join is covered upstream where the snapshot is minted.
That was not true: members_owned had no witness anywhere in the corpus, and
FabricCellMember is an ordinary record, so the sole_constructor seal was never
the reason it went uncovered.
Checking it surfaced the larger fact. fabric_cell_member_ownership derives
ownership by building FabricCellSlotScope from the member's own slot, and
fabric_cell_subject_ownership answers Owned for every slot scope. A member
carries only a slot, so the Ensured arm is unreachable from a member and Absent
is never constructed -- members_owned returns true for every input, and its fold
seeds true so the empty cell reads as owned too.
That matters because a consumer reads it as a safety predicate: runner_jit_mint
refuses to mint a runner credential for a cell that is not owned. The refusal is
real in the arm receiving the Bool; the Bool reaching it cannot presently be
false. What actually rejects a malformed cell today is fabric_cell_shape's
Incomplete arm, which runs before ownership is consulted -- a different
authority than the one the refusal names.
These witnesses pin the current behavior rather than asserting a guarantee, so
the day ownership becomes variable they go RED and the consumer's refusal gets
re-examined instead of silently starting to fire.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
---------
Co-authored-by: Brian Searls <cutencool.work@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Bind two zero-arg stage0 partition helpers as data so each pure value evaluates once (#10530)
* rust_crate_partition_witness: lift stage0 partition derivation from fn to data
The stage0 partition DAG (stage0_module_dag), its resolve+fold receipt
(stage0_partition_receipt_outcome), and the intermediate fold outcome
are frame-invariant computations: their inputs are all pure data or
constant-function return values, and no claim perturbs them.
Previously, every claim that called stage0_partition_receipt_outcome()
re-evaluated the entire module list concatenation, the cross-unit edge
table, and the partition fold. The test module has 4 claims that consume
this value directly (witness_runtime_unit_members_holds,
witness_v1_infer_unit_members_holds, witness_v1_artifact_unit_members_holds,
witness_partition_perturbation_member_coverage_holds) and 2 more that
call it indirectly through stage0_partition_fold_ok and
stage0_partition_r4_valid.
The witness_perturbation test (ForwardSameInSameOut) only checks the
determinism of the member-coverage comparison; it does not perturb the
stage0 data.
DESIGN.md section 2: a cache may discharge unavoidable recurrence but
may never excuse authored duplication. This is a modelling fix (case c),
not a cache — the partition derivation is frame-invariant and should be
declared as data, not recomputed per claim.
Changed:
- stage0_module_dag: fn -> data
- stage0_partition_receipt_outcome: fn -> data
- stage0_partition_r4_valid: reads receipt data, skips partition_fold
- stage0_partition_fold_ok: reads receipt data
- stage0_single_crate_fold_outcome: reads dag data
- All call sites: () removed from data references
* Bind the resolve outcome too: r4_valid was recomputing the demand this change collapses
Review 61406 caught an authored duplication left standing by the previous commit.
stage0_partition_r4_valid called resolve_partition_outcome a second time to pull the
assignment, while matching a receipt whose own definition already embedded that same call --
two demands for one pure fact with a shared-state least common ancestor, which DESIGN
section 2 names as authored duplication rather than a caching opportunity.
It is the same defect this change exists to remove, one declaration away from the fix. So
the resolve becomes its own binding, stage0_resolve_partition_outcome, and both the receipt
and r4_valid read it. resolve_partition_outcome now has exactly one call site.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014qYnzwGtbQqwa7o6wcSoaX
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Classify the 19 discarded shell-effect outcomes outside the printer scope (#10664)
* Classify the 19 discarded shell-effect outcomes outside the printer scope
16 of them are lawfully best-effort under one stated discriminator; 3 owe a
real distinction and sit in a subsystem with no producer and no consumer.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Record the entry-vs-module map: a cut here reds a witness and shrinks a monotone roster
"Dormant at both ends" overstated it. The two Bool entries have no callers; the
modules do not. merge_admission_fetch_stall_deadline_seconds is imported by
merge_admission_current_context and asserted by an enrolled witness, and
read_tested_subject / read_floor_receipt are enumerated sites of the
filesystem_io absence-establishment monotone roster, whose rows may leave by
deletion. A path-shaped grep and a module-shaped grep answer different questions
here; only the second finds importers.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Check all 16 against the mktemp-origin test by construction site, not by name
cache_dir is the member whose name asserts a lifetime its construction does not
have: both sites are shell.Mktemp.Dir(), so it is per-run and the discriminator
holds. Every other binding the sweeps reach is likewise a shell.Mktemp.* call
with no other origin and no shadowing. Recorded at the declaration, with the
naming defect named separately rather than fixed here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* The population moved 19 -> 15: carry the ref the count was taken against
main deleted materialize_spark_serving_ollama_runtime_bundle with the whole
spark-serving archive-admission block while this was open, so four members left
by deletion of the subject rather than by being consumed -- package_delivery
11 -> 7, the other three modules unchanged at 5 / 2 / 1. The annotation citing
that function by name would have described nothing. Every count now names the
ref it was measured at, because a bare number cannot tell a real change from a
stale citation.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* State the selector and identify members by declaration and arm, not by count
Two honest measurements disagree by one: shell-only reads 14, shell-or-Filesystem
reads 15. The wider selector is the right one -- the defect is an ignored effect
outcome, not a property of which service produced it -- and it is now written
out rather than implied by a grep. Membership is rostered by module, enclosing
declaration and the arm each sweep follows, because provider_wire_evidence's
five members share one declaration and would collapse to one at declaration
grain. bmc_onboard write_netrc is named as deliberately out of population rather
than silently dropped: #10574 deletes it, so the original 19 was branch-relative.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Three sites, two defects, two modules: say which count is which
Two independent reviewers summarized the OutcomeSemanticallyRequired class as
"two" -- the count of defects and of modules, not of sites. A classification
whose thesis is that a count needs its selector, its ref and an identity roster
should not leave its own count ambiguous.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Name the instrument: drop the transcribed census totals from all four modules
DESIGN §6 -- a measurement is cited by naming the producer that re-derives it,
never by copying its numbers into prose. Adding a revision and a selector made
the totals attributable without making them re-derivable, and four modules each
holding a copy is four ledgers maintained by hand independently of their
subjects. The totals are gone; what remains is the SELECTOR (the instrument that
re-derives the population at any ref) and the members NAMED by module,
declaration and arm. The identity roster also carries what a total never could:
main's deletion of materialize_spark_serving_ollama_runtime_bundle retired its
members by deletion of the subject, which a count cannot distinguish from a
member being consumed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Review is a function: exclusive criteria mapped to calls, folded to one verdict and one piece of worker feedback (#10665)
* Review is a function: exclusive criteria mapped to calls, folded to one verdict and one piece of worker feedback
gunbc.roadmap.roadmap_review_function writes the review as review(subject) = aggregate(map(criteria,
criterion_review)): ReviewSubject is the one input every criterion sees, criterion_review builds a
criterion's whole call (its brief and verdict path), review_calls is the map over the roster, and
review_aggregate folds the evidence into the belt's reconciliation and the worker's feedback. The belt
now builds each reviewer's brief through criterion_review instead of hand-assembling it.
The criteria roster is proven an exclusive partition (review_criteria_are_exclusive_parts: distinct keys,
distinct grounding propositions) and gains extdeps-placement, grounded on s1.grounding-intersubjective:
does the change carry a fact other parties already agree on without pointing at the shared authority,
or put such a fact in the wrong layer (an upstream fact inside a product module, our policy or
observations inside extdeps, a hub enumerating products).
WorkerFeedback is the recomposition for the person who acts on it: findings regrouped by path in
criteria order, identical rows folded once, a path named by two criteria counted as the residual
(overlap_count), unjudged criteria listed as not reviewed. The reconciliation's failure detail is that
text, so the continuation turn and the board show the worker the same smoothed feedback.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* The review roster is derived from the design argument: each proposition carries its own review reading
gunbc.design_argument rows are now DesignRow { proposition, review? }: the proposition of the serial
argument plus, where it is checkable on one change, the reviewer's question and tells. The section
lists, design_propositions and design_argument are derived from the rows unchanged. gunbc.roadmap
.roadmap_review_criteria no longer authors a roster: review_criteria is flat_map over the rows with a
review reading, keyed by the proposition id minus its section prefix. Adding, changing or retiring a
criterion is one edit to the proposition's row and nothing else (operator: DESIGN criteria flow to
reviews with no dual representation). Witness keys follow the derivation (closed-grounded-substrate,
minimize-redundancy, grounding-intersubjective); the reviewer-spread witness reads the live keys.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* The belt realizes the review plan and judges through its fold: revision-bound calls, exact join, streaming feedback
Review 5125854144 on the first cut: the modeled map and fold sat beside production. Now they are it.
- ReviewPlan { revision, subject, calls }: the revision is the roster's content (any change to a criterion's
key, question or tells moves it); a call carries no verdict path (review_verdict_instruction is the
realization's, appended with the path it mints).
- ReviewObservation is bound to call id, subject id (node@head) and plan revision by the path the belt read it
from; review_join refuses unknown, duplicate, other-subject and other-revision observations by name and
keeps every planned call in the denominator (missing = awaiting). A subset of approvals is Pending, not
Complete.
- The belt builds the plan (belt_review_plan_for_head), realizes plan.calls with revision-keyed artifacts and
units (belt_review_call_key = <revision>-<criterion>), and publication and the workflow review segment
consume review_aggregate's report; belt_review_evidence, review_all_approved and the direct
review_reconcile calls are gone from production. Workflow evidence carries ReviewReport.
- Temporal rule: a head reviewed under an earlier roster is explicitly superseded -- old verdicts are not
this plan's observations, the restart is reported as ReviewPlanSuperseded with the stale count.
- review_criterion_identities_are_unique replaces the exclusivity claim; path grouping is presentation only.
- WorkerFeedback carries the incomplete calls; the text says the report is not complete and names them.
- DesignRow.review is PropositionReviewDisposition: ReviewableOnChange { parts } | NotReviewableOnChange { reason };
each part names its criterion key (extdeps-placement for s1.grounding-intersubjective).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* Operator entries for the review function: review one attempt's head on demand, and read its aggregate report
belt_review_head_for_instance is the one path a head is reviewed through -- the tick after verification
and the operator on demand (belt_review_head_cli) -- and belt_review_report_for_instance the one report
(belt_review_report_cli, JSON with state, detail, approved, incomplete, could_not_judge, overlap and the
worker feedback text). The operator entry does not verify and publishes nothing; publication still gates
on verification and the aggregate. review_report_json is the report's wire.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
* Move the route-gap annotation to the grain §4c admits, and make it describe the six rows it actually covers
Four required-lane runs on this branch have now failed. The first three were an
unparseable tree; this one got past the module index and refused on the
annotation itself:
floor_route_gap.dag:863-865: source annotation sits inside a declaration body.
Only module-item grain is modeled; move it above the declaration it describes.
§4c admits only standalone leading // blocks attached to module-scope
declarations. A row inside a Cons chain in a function body is not a module item,
so a per-row annotation is inadmissible by construction. The content was right
and its placement was not; it moves into the existing block above
floor_route_gap_expectation_chunk_07, where the enrolment-is-not-the-route
sentence already lives.
The same block also asserted "these five route gaps ... all five executing and
holding on that lane" over a chunk that now carries six. That sentence was true
when written and is invalidated by the row added beside it, which is precisely
the failure mode §4c makes undetectable: no Accepted program reads an
annotation, so a stale one never reds and keeps reading plausibly. It now states
the six explicitly and separates their evidence -- the five eval_model probes
were observed by the run that produced their gaps; the sixth is enrolled beside
its own WetScheduledClaim row and is established by whichever run admits it --
and puts the maintenance obligation on whoever adds a seventh.
No row, identity, operation or ground changed: six FloorRouteGapExpectation rows
before and after, and the file's brace delta matches main's.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
* Fix annotation-position parse errors in floor_route_gap chunk_07
Move function-body // comments to module-item grain above the function
declaration. Same class of error as earlier in this PR: source annotations
inside a declaration body are refused (only module-item grain is modeled).
* Fix stall subject: v1_compiler:: not v1_rt::
The stall was created before the search pattern was changed from v1_rt::
to v1_compiler::. Subject string was stale — said v1_rt:: but the check
searches for v1_compiler::.
* fix: brace balance in floor_route_gap.dag (473/473); remove stale falsifier enrollment for behavioral receipt
floor_route_gap.dag:
- Added 3 fixture expectations (seed-unavailable check_fixture identities)
- Added corresponding Cons nesting closures (3 structural opens + 3 closes)
- Updated annotation: chunk carries NINE identities, run 34050705404
- Braces balanced: 473 opens, 473 closes (was 473/472, fixed +1 fn close)
wet_receipt_enrollment.dag:
- Removed self_host_logic_behavioral_receipt_holds from
falsifier_self_host_wet_template_entries (identity migrated to
local_repo_wet_terminal WetScheduledClaim, no longer enumerated in
falsifier roster; §3 smell resolved)
* Fix fixture vacuity: give v1_rt.rs actual v1_compiler:: reference; remove run number from annotation
The fixture directory_with_v1_rt_containing_calls_passes claimed it tested
that a v1_rt.rs with v1_compiler:: in comments passes the check, but the
file content had NO v1_compiler:: at all (unimplemented!() stub). Fix by
adding a prose comment referencing v1_compiler::lookup. The check still
passes because v1_rt.rs is excluded from the scan by name containment.
Also remove the transcribed run number 34050705404 / be79b78 from the
floor_route_gap annotation per section 6 (measurement artifacts do not
belong in authority files).
* Fix comment: local_repo_wet_terminal header says v1_compiler:: not v1_rt::
The schedule header for CONTROL (b) said 'The transport's v1_rt:: call-site
check' but the transport checks for v1_compiler:: (the seed crate namespace).
v1_rt is the runtime shim (emitted unconditionally); v1_compiler is the seed
crate that is deliberately absent. The comment misnames the checked token,
which is a meaning fork (DESIGN §3: one name, two materially different
meanings).
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Brian Searls <cutencool.work@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Model the path that sends a sliced project to a Bambu printer on the LAN, and make every place it could have guessed refuse instead.
What this delivers
A printer file-delivery chain in
.dag— payload identity, endpoint resolution, credential resolution, FTPS upload, cleanup — plus the credential authority it needed and the Secret Manager observation that tells it whether it may proceed at all.It has been run wet against the real machines.
printer-01is at192.168.1.234andprinter-02at192.168.1.235, joined from three agreeing sources (a port scan, the TLS certificate CN, and the operator's DHCP table) rather than trusted from one.The credential boundary
The first draft of the upload passed a
Secretinto curl's--user, re-creating exactly the classgunbc.credential_argv_exposureexists to retire — a roster whose audience is measured, not assumed: on srv1,/prochas nohidepid,cmdlineis mode 0444, and runner slots share the host pid namespace.It is now structurally unspellable at the boundary that represents an authenticated transfer:
upload_command_forandproject_upload_commandtake aNetrcBindingand project the path internally, so a caller cannot supply an arbitrary one.curl_ftps_upload_commandstaysFilePath-parametric on purpose — it is curl syntax, not a place a credential guarantee can live — and no function in the chain has a parameter aSecretcan enter. An earlier version of this sentence said the curl helper itself took aNetrcBinding, which was never true and is exactly the kind of body claim that keeps a real gap invisible: the seal was genuinely bypassable atupload_command_foruntil this PR closed it. The netrc authority lives ingunbc.auth.netrc_binding— one authority, not a copy — and the srv3 BMC bootstrap was migrated onto it, replacing aFilesystem.Writethat placed a credential under the ambient umask.Observation, not declaration
Delivery originally decided whether a printer's access code existed by reading a roster this repository writes. An empty roster meant we have no record, and it was being consumed as the remote says no — a local declaration wearing an observation's name, writable by any author who appended a row.
It now asks Secret Manager.
gcp.SecretManager.GetSecretwas already declared in extdeps with a full response block and zero callers; all it lacked was theoutcome: RestOutcomefield that stopsdispatch_restraising a 404 as a renderedTypeError— which is how the wet run received it. It is the only operation in that service declaring an outcome, and the asymmetry is deliberate: forAccessVersiona 404 is a failure and raising loses nothing a caller could act on, but forGetSecreta 404 is the answer, so the one arm that must not throw is the one the question was asked to reach.The roster's job narrowed to the one question a remote cannot answer: which version, because the version is minted by the write and only the writer can say what it produced.
The roster is an unavoidable input, not a function something else could have called
The observer originally derived the secret name from
printer_access_code_desired_ref, which spells an id by convention and therefore succeeds for any identity. So a printer present in the fabrication topology but absent fromprinter_access_code_locihad a plausible Secret Manager name synthesized for it and queried. The roster's refusal was correct, had a witness, and had no consumer — the module even carried a comment asserting that unknown printers refuse, which was true of the lookup function and false of the production path.The desired ref now comes out of the admitted locus row, so the roster cannot be bypassed by construction rather than by discipline, and the existing unknown-printer red finally tests a function production calls. Receipt resolution consumes that same admitted
SecretRefinstead of independently re-deriving it, so the join and the remote read cannot drift onto different subjects.States that could have collapsed into one
Each was a real arm that had to be split, and each has a witness:
PrinterCredentialLocusUndeclaredPrinterCredentialLocusConflictedPrinterCredentialProvisionRequiredPrinterCredentialMaterializationVanishedPrinterCredentialObservationRefusedPrinterCredentialVersionUnrecordedAn undeclared locus and a failed observation are deliberately not the same arm: one says the fault is in here, the other says it is out there.
Everything answerable from our own records is answered before anything is dialled. An earlier revision checked receipt ambiguity after resolving a token and dispatching
GetSecret, so duplicate local receipts plus an unavailable token answeredPrinterCredentialObservationRefused— a malformed local declaration hidden behind an unrelated external failure, which is the same fault-class collapse one population over. The receipt roster now has exactly one reader,materialization_lookup_for, and it runs first.PrinterMaterializationLookupcarries the conflict case so thatPrinterMaterializationRecordcan stay exactly two arms.Three of these rows were found after the first implementation looked right, two of them by review. All had the same shape — two facts with different remedies collapsed into one arm wearing the wrong one.
Why the classification is separate from the transport
classify_container_observationis a pure function of the outcome and the materialization record; the network function does the read and decides nothing. That split exists so the RED is authorable. Inline, the decision that must not go wrong — 404 becomes absence, 403 must not — could only be exercised by making Secret Manager return a 403 on demand. Separated, a witness constructsRestStatusRefused { status: 403 }directly.Enrolled: a positive control on 404, a discriminating red across 403 / 401 / 429 / transport refusal / undecodable body, one for the present-container case, and one asserting that a 404 arriving over an existing receipt is not read as never-provisioned.
One witness in this file was itself asserting the false claim production had removed —
ref.version == "1"against afleet_secret_refthat constructs"pending". It was the sole blocking identity in the floor lane atee5cd66e80, so that defect is corroborated by execution rather than by reading. It now compares the locus to what the canonical constructor produces, rather than copying"pending"in place of"1", which would have relocated the duplicate authority instead of removing it.What is deliberately not here
AccessVersionis unreachable from a pending locus.PrinterAccessCodeDesiredLocusFoundanswers which secret the code is supposed to live in and never whether it is there — the rename is the point, since the old name was being read as capability.The provisioning actuator is not built:
SECRET-PROVISION-0owns idempotency and performs noCreateSecret/AddVersiontoday,SecretProvisionCredentialcarries only Spark arms so a printer would be misfiled, andDischargedAtis constructed nowhere — verified, not assumed. CORRECTED AFTER A WET RUN ON 2026-09-06 falsified the original sentence here, which read "neither access code has ever been materialized". Both are now materialized:printer-01-lan-access-codeandprinter-02-lan-access-codeexist ingunbai-secretsat version 1, ENABLED, payload SHA-256-verified against the operator's source files. That was done OUT-OF-BAND withcurl, not through any modelled path, so it changes the state without discharging the gap — and the consequence is that the actuator described above still cannot truthfully mint a receipt for version 1, because a receipt is earned from a performedAddVersionresponse and this repository did not perform one. The measured current state is therefore neither the pre-onboarding 404 nor a recorded materialization, but container present, exact version unrecorded: delivery reaches secret resolution and refuses rather than guessing which version holds the code. What remains before a print is version PROVENANCE, not secret availability.A brand is a name, not a constructor
sm_resolved_version_idwas documented as total by construction, on the reasoning thatSmResolvedVersionIdentitycan only be minted by the validating decoder. The type isNonEmptyStr where brand(...), so any module can write"anything" as SmResolvedVersionIdentity—and a witness in this branch did. The "unreachable" fallback was reachable and returned the whole
malformed string as a version id, in the field a credential fetch is later pinned on.
It refuses now, and the refusal propagates:
secret_provision_receiptanswers a mint outcome, so amalformed identity produces no receipt rather than one carrying a plausible-looking segment. The
note says plainly that this is validation and not construction; the rung climbs when the decoder owns
a carrier no other module can spell, at which point the refusal arm becomes unreachable for real.
Rung
Mitigation, and that is the ceiling: whether a secret exists is an external fact observed at a boundary and never becomes construction. What changed is that the boundary is a real read whose refusal arms refuse, instead of a local list whose silence was read as an answer.
Scope of the cleanup class, stated at its accurate strength
Four review rounds found what is one class, not four bugs: an effect whose result is bound to
_,so a failure is spelled identically to a success. It surfaced as a completed upload whose credential
shred failed reported as clean; a failed transfer whose shred also failed reported as an ordinary
refusal;
refuse_and_dropand the provision-required arm dropping payload removals; and netrcpartial writes claiming "no credential was placed" while identification abandoned a complete payload
copy. Each was fixed at the cited site before the pattern was censused, which is why it recurred.
This PR eliminated discarded shell-effect outcomes from the printer-delivery scope. All five
modules it touches are at zero. A whole-tree census found further candidates outside that
scope. A count here needs its SELECTOR and its REVISION, and this one has been stated without both.
Selector:
let _ = shell.<Op>orlet _ = Filesystem.<Op>— an effect whose outcome is bound to_. Under that selector, measured on this branch: 19 at merge-basef1064ea(
package_delivery11,provider_wire_evidence5,merge_admission_walk2,merge_admission_capture1)and 15 on the merged tree, because
mainindependently deleted fourlet _ = shell.Remove.RecursiveForcelines frompackage_delivery.Narrowing the selector to
shell.alone gives 14, and a reviewer measuring that way willlegitimately get a different number. The member that drops is
merge_admission_walk'slet _ = Filesystem.Write(...)— which belongs to the class on the merits, since the defect is anignored effect outcome and not a property of which service produced it. So 14 understates and 15 is
the figure this PR uses.
One more revision detail, because it explains a real discrepancy rather than papering over it: this
branch also removes a
let _ = shell.Remove.FileForcefrombmc_onboardthatmainstill carries.That instance never appeared in the population above, because the original census was taken on this
branch after the netrc migration had already removed it — so "19" was branch-relative from the start,
not a
mainmeasurement.Those candidates are not claimed closed, and not claimed to be defects. They are a syntactic
candidate population that still needs classifying: which members actually owe a semantic distinction,
which are explicitly best-effort, which are false positives of the grep. Mass-replacing
_withnames would create as many unread values as there are members, and fix nothing. They are owned by a separate lane
(
node://adhoc-79d7ea96-82e) rather than left ownerless.None of the four modules sits on this product's causal path — verified against the 182-module
transitive import closure of
printer_delivery_wet_run/printer_project_delivery/netrc_binding, in which none of them appears.What the new witnesses do and do not establish
The residue classifications are split out of their effects so the discriminating input is a
Bool,which is what makes each RED authorable at all — the first fixture attempt pointed at an
"unremovable" path under
/proc, andrm -rfexits 0 on a missing path even under an unwritableparent, so it would have been permanently green while reading as coverage.
That split has a limit worth stating rather than glossing: a pure pair proves the classification
law, not that the effect adapter hands the classifier the right Bool. Those are two questions. The
first is now covered by execution; the second is not, and this PR does not claim it.
No access code value appears in this repository in any form. Codes are referenced by locus only.
🤖 Generated with Claude Code
https://claude.ai/code/session_01XapoExtJQauXkqJCDS9dGs