Repository navigation
A training run's identity must move when its seed does: resolve the manifest, derive the contract, and let derive_work_key stay the only authority - #9574
Conversation
…anifest, derive the contract, and let derive_work_key stay the only authority The resident-model programme compares training runs -- control against candidate, base against adapter -- and every one of those comparisons joins on a Work identity. So the identity has to name ONE computation. Measured on this tree nothing modelled the step between an authored recipe and an exact run, which meant a run's identity could be minted from values the trainer had not yet chosen. THE SHAPE, and each piece exists because the alternative was constructible: The manifest carries no deferral. There is no Auto, Latest, Default or BestAvailable arm, and the zero-invalid axes are PositiveInt rather than Nat while the convention-word axes (numeric format, method, packing, loss mask) are closed enums rather than NonEmptyStr -- `numeric_format: NonEmptyStr` admits "auto" and "default", which is the failure wearing the shape of a value. A caller that has not pinned a coordinate cannot say so in the manifest; its observation is AxisUnresolved and resolve_training refuses, naming a CLOSED axis so a new coordinate cannot be added without failing every exhaustive match over the refusal population. The manifest is a total projection of the evidence, not an argument beside it. An earlier revision took both and sealed the door, which confines WHO may construct and establishes nothing about WHAT IS TRUE of the values -- a manifest naming base B beside evidence attesting base A was constructible and no wall could see it. That is the ceiling this repository already records for sole_constructor, and the repair is derivation rather than a comparison. THE CONTRACT IS DERIVED, AND THIS IS THE ONE THAT WOULD HAVE SHIPPED. resolve_training previously took the WorkContract as an argument. derive_work_key reads ONLY the contract and requirements, so a caller could resolve a manifest pinning seed 7 and pass a contract mentioning nothing about it: two runs differing in seed, optimizer and numeric format would have shared one Work key while producing different weights. The contract now descends from the evidence, over field-tagged length-separated material, with ContentHash coordinates going through serialize_content_hash rather than a bare digest cast so the hash family survives -- a dropped family coordinate is an identity collision, not a formatting detail. derive_work_key remains the sole identity authority and nothing stores its result, so a stored key cannot disagree with the derived one. The admission derives under demand.work.principal, not demand.id.principal. The requester and the accounting scope are different roles that share a representation; deriving under the requester refused every legitimate demand whose work was scoped to an organization, which would have made service accounts and delegated execution unrepresentable. The admission establishes exactly one relation -- this resolution derives the Work this demand NAMES -- and leaves authorization to the grant machinery that owns it. EVIDENCE, all green BY EXECUTION rather than by compiling. Seven witnesses run through the interpreter and return true: a changed seed and a changed base artifact each move the Work key; a changed resolution RECEIPT does not, which is the negative control that stops the projection from hashing provenance instead of the computation; an unresolved coordinate refuses naming SeedAxis; and the cross-principal pair admits a requester asking for work scoped elsewhere while refusing a demand naming a Work this resolution does not derive. The completeness witness is proven to be falsifiable, not merely green: deleting the seed row from the material flips it to false and restoring it flips it back. Without that mutation the control could not be distinguished from one that passes because the key ignores every coordinate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nto a source annotation Review on #9574 flagged training_resolution_excludes_dispatch_note as a `data ...: String` whose sole purpose is commentary, which DESIGN 4c calls misplaced or dead data, and noted it matches the repo-wide `*_note: String` idiom. Both halves are true and the conclusion goes the other way for NEW code. That idiom is a compensating convention the corpus adopted when `//` was a parse error: prose had to be hoisted into a String row to survive at all, and 4c records the cost -- intent became mechanically indistinguishable from program data, and the first cleanup it forced swept 215 dead rows across ~130 files. Annotations parse now, so the reason for the workaround is gone; matching it here would author one more row of the debt that convention exists to explain. The content is unchanged and belongs in an annotation by 4c's own test: it is irreducible rationale about WHY the manifest has its shape -- which coordinates change the promised answer and which are execution policy -- rather than a restatement of what the declaration structurally says, and nothing machine- consumed lives in it. No `Accepted` program could read it either way, so it was never evidence for any claim; as a String it merely looked like it could be. Module now carries zero commentary String rows. Compile unchanged at 0 blocking, and the falsifiable completeness witness still returns true, so the annotation move is inert to the semantic graph exactly as 4c requires. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…oordinate, a bounded dropout, and a method sum that stopped carrying dead parameters Four defects, and the first is in the PR body rather than the code. THE OVERCLAIM. This PR stated that every semantic coordinate reaches the Work key. The suite varied TWO -- seed and base artifact -- and held the other twenty-one fixed in one fixture. The seed mutation proved the SEED control was falsifiable and established nothing about the rest, so the claim was stronger than its executable population. That is the inflation DESIGN 4b rates as worse than sitting low, because an overclaimed wall never ranks for the work that would make it real. Now one perturbation control per coordinate, all twenty three, each moving exactly one field. THE METHOD WAS A SUM WHOSE PARAMETERS WERE A PRODUCT. TrainingMethod carried FullParameter | LowRankAdaptation while target_modules, rank, scaling and dropout stayed UNCONDITIONAL manifest coordinates, so a full-parameter computation carried a LoRA rank its trainer never reads -- and two identical full-parameter runs would derive DIFFERENT Work keys because someone authored rank 16 rather than 32. That is the exact inverse of the collision this module exists to prevent: one computation receiving many identities, because dead fields participate in equality. The arm is deleted rather than fixed in place: the programme is low-rank adaptation, and an arm kept only to anticipate a consumer that does not exist is the carrier-before-consumer scaffold this module otherwise refuses. The honest later shape is a sum OF PRODUCTS. BATCH IDENTITY HAD THREE WRITABLE REPRESENTATIONS AND NO TOPOLOGY. micro_batch, gradient_accumulation and global_batch were stored independently with no worker count anywhere. Under global = micro * accumulation * workers the fixture's 2, 8 and 64 silently asserted four data-parallel workers -- a fact the manifest never carried -- and both (2, 8, 16) and (2, 8, 64) construct, their difference being an OMITTED topology rather than two spellings of one computation. Global batch is now DERIVED from the two independent causes and never stored. Worker count and gradient reduction are semantic rather than placement and belong here when a coordinated multi-host realization exists; this slice admits single-worker only. A DROPOUT RATE IS BOUNDED AND Nat IS NOT. Zero is meaningful so PositiveInt was the wrong narrowing, but Nat admits 1001 and 5000, which are not probabilities. No bounded refinement predicate exists to consume, so the bound is a sealed mint refusing above one thousand, with BOTH boundary admissions asserted beside the refusal so the wall cannot be satisfied by refusing everything. Also: the material annotation said length-separated when the implementation is delimiter-separated over delimiter-free renderings. The encoding is injective either way on this domain, but a mechanism described as one it does not implement is a defect in the description, and it would become a real defect the first time a rendering could contain a delimiter. And the witness still carried its own commentary `data ...: String` row -- the same form rejected in the production module one commit earlier -- now an annotation. EVIDENCE, green by execution: the twenty-three-coordinate control, the receipt negative control, the dropout boundary pair with its refusal, and the derived global batch. THE NEW CONTROL IS PROVEN FALSIFIABLE ON A COORDINATE THE OLD ONE COULD NOT HAVE REACHED: deleting the `packing` row from the identity material flips it to false and restoring it flips it back. A mutation against seed alone would have said nothing about that field, which is precisely why the previous evidence did not support the previous claim. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… picked the winner The readback slice: an independent observation of a training run, kept apart from the runner's own receipt. A trainer that writes "success" has established only that it believed it finished -- not that the artifact still exists and hashes correctly, that no process is still running, or that the receipt belongs to this run rather than another using the same recipe. Convergence that read the receipt would be asking the thing it is checking. The first draft carried one process state, one terminal standing, one output and one effective manifest per run. That was wrong at the grain, and the error was structural rather than a missing case. One demand reaches several execution attempts -- infrastructure retry, capability escalation and requested re-execution are all NEW attempts rather than mutations of an earlier one -- so a singular output field makes two produced artifacts unrepresentable, a singular terminal discards the local failure the moment an escalated attempt succeeds, and a singular effective manifest hides the exact disagreement that axis exists to detect. A carrier admitting one member has selected a winner before the reconciler ever runs. So every axis is TrainingPopulationObservation<T>, and it has no absent arm. A complete read that found nothing is an observed population with zero members; that is a different fact from "nobody ran the observation" and from "the observation ran and could not produce a reading", because empty licenses a conclusion -- restart the run -- that ignorance does not. The two negative arms stay apart because their owners and remedies differ: not-attempted is owed to the scheduling driver and repaired by dispatching an observer; refused is owed to the transport or store and repaired by fixing that path. The refused arm carries its attempt receipt, without which the two would be differently-named strings. Three further corrections. The readback stays generic in P: narrowing to NonEmptyStr would mean product.training can represent readback only for bindings whose principal happens to be a string, which is a binding-level restriction inside a provider-neutral module. The effective manifest carries the typed TrainingResolvedManifest rather than a hash, because the axis exists to answer WHICH coordinate disagreed and a hash answers only same-or-different. The output member carries a Sha256Digest with its producing attempt and materialization evidence, because the model-artifact path needs an exact produced artifact and not an arbitrary structural hash. The top-level subject was not enough on its own. Without a per-axis subject the shape admits a readback whose subject is run A while its checkpoints came from run B and its terminal from run C, and every field typechecks. Raw reads are therefore subject-bound and the binder compares all five against the subject derived from the desired run, refusing on a closed axis coordinate before any axis fact enters the readback. Nine witnesses, all green by execution. One refusal control per axis, reading the axis back out of the refusal so a binder refusing on the wrong axis fails rather than passing as a generic refusal; a positive control, without which an unconditionally-refusing binder would pass every refusal witness. And two controls that an earlier revision of this suite would have missed: it varied only the work identity, so an equality comparing work and ignoring the demand would have passed everything -- the suite would have measured one half of a pair while claiming the pair. The two halves are now separated, each differing in exactly one coordinate. The sole_constructor wall on the subject was confirmed by execution, not asserted: a forged cross-module literal refuses with "cannot be constructed outside its defining module", and the probe was removed after it fired. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Second slice pushed: readback (
|
…eyed projection instead of two folds of the same manifest The effective-manifest axis has to name WHICH coordinate diverged, not merely that something did. The obvious way to build that comparator is to fold the manifest a second time beside training_manifest_material -- and that is a second spelling of the coordinate set, with two failure modes that both compile: a coordinate present in the key fold and absent from the comparator is invisible to the comparison forever, and the two spellings can drift. So the per-coordinate projection is hoisted into a single authority. training_manifest_coordinate_material(m, axis) is where a coordinate's material lives, training_resolution_axes() enumerates the roster once, and training_manifest_material now folds that roster rather than listing the coordinates itself. Any consumer that needs to compare, name or serialize a coordinate reads the same function, so a coordinate cannot enter the work key without being comparable -- the relation is structural rather than maintained by hand. This preserves the material bytes and their order. The regression check that matters is the 23-control work-key witness, which perturbs each coordinate independently and requires the key to move: it still returns true by execution after the refactor. A hand-listed axis roster in a consumer would have been the same defect one level out -- a second, silently narrower roster whose forgotten coordinate is the one that drifts -- which is why the roster is a function rather than a convention. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…an admitted attempt graph, and rootedness as a bounded fixpoint The readback binds each of its five populations to the run's Demand/Work subject, which stops a whole population being filed against the wrong run. It stops nothing about the individual members. Every process, checkpoint, terminal, output and manifest receipt carries a freely supplied execution attempt identity, so a member naming an attempt from another run passes every check the readback can perform: the wrapper is honest, the member is foreign, and a subject comparison cannot see one level down. Reconciliation joins evidence at attempt grain, so it cannot be written correctly until membership is decidable. Membership is therefore decided against an admitted graph and never inferred from a shared materialization path, a similar key, adjacency in time, or the wrapper's own asserted subject. Each of those is a resemblance, and a resemblance admitted as identity is how another run's artifact becomes this run's output. The witness for that is direct: an attempt key under a different principal is not a member. ROOTEDNESS IS A BOUNDED FIXPOINT RATHER THAN A WALK, and the case that forces it passes every local check. Two attempts each naming the other as predecessor are both present, neither predecessor is absent, no work is foreign -- and neither chain ever reaches the demand. A recursive walk over that pair does not terminate. Folding over the attempt list, whose length bounds the longest possible chain, reaches the fixpoint and reports both as unrooted. The same machinery catches the quieter case: a chain whose root is an initial attempt for ANOTHER run's demand, which would otherwise be admitted and then joined as evidence about a run it belongs to only by resemblance. Every way the graph can be wrong is its own named refusal, because the remedies differ -- a foreign work is a routing defect, an absent predecessor is a lost observation, a duplicate identity is a producer emitting twice, an unrooted chain is not an attempt at this run at all. The refusal carries first + more rather than the first defect found: an ordered refusal would hide the second until the first was repaired, so a graph with three problems would take three round trips and the hidden defects would read as new regressions each time. A duplicated identity is reported at EVERY occurrence rather than once per repeated identity. Which occurrence is "the original" is not a fact the graph has -- the members arrive unordered -- so nominating one as legitimate would be the fold inventing a precedence it cannot establish. Nine witnesses, all green by execution, including the positive control without which an admitter that refused everything would satisfy all of them, and the RequestedReexecution case: a rerun roots directly in the demand like an initial attempt and unlike a retry, so a rootedness rule recognizing only InitialAttempt would report every rerun as unrooted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Fourth slice: the admitted attempt graph (
|
…control per axis cannot see two foreign axes at once The readback binder compared its five axis subjects in a nested if-chain and returned on the first mismatch. So a readback whose execution AND outputs both came from another run reported only execution, and the second defect would have surfaced as a fresh regression the moment the first was repaired. This is the same first-wins failure the reconciliation notes in this module reject, committed one layer down by the author who wrote them. WHAT DID NOT CATCH IT IS THE POINT. Nine witnesses passed, including one refusal control per axis, and six approvals read the diff -- one of them crediting the branch with "admission refusals carry every defect", which was true of the attempt graph and false of this binder at that head. The per-axis controls are not weak evidence; they are evidence of a different proposition. Each makes a single axis foreign, so each proves its comparison EXISTS and none can express what happens when two mismatch at once. No amount of that family reaches this bug, which is why the new control is added beside them rather than replacing them: they fail on different bugs. The refusal now carries first + more, making the population non-empty structurally so a refusal holding no mismatch is unrepresentable, and the binder folds all five before deciding. THE NEW CONTROL IS SHOWN TO DISCRIMINATE RATHER THAN ASSERTED TO. Reintroducing first-wins by returning an empty `more` turns it red; restoring the fold turns it green, with the file restored byte-exactly afterwards. A witness that passes against both the fix and the bug would have been decoration, and this repository rates that as worse than absent because it gets cited as coverage. TrainingCheckpointReceipt is renamed TrainingCheckpointObservation in the same change. It records that a checkpoint-like artifact was seen and binds none of optimizer state, scheduler state, RNG state, data-order position, atomic publication standing, or a materialization readback -- so it cannot establish that training could resume from it. Under the old name a later reconciliation arm could reasonably have derived "resume required" from it; the carrier now says what it is, and no arm may until a checkpoint admission lands. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Correction: the readback binder had a first-wins defect, and nine green witnesses plus six approvals did not see itPosting this against my own earlier slice, because the way it was missed is more useful than the fix. The defect. What did not catch it. Nine witnesses passed, including one refusal control per axis. Six approvals read the diff — review 57243 credits the branch with "admission refusals carry every defect", which was true of the attempt graph and false of this binder at that head. The per-axis controls aren't weak evidence; they're evidence of a different proposition. Each makes exactly one axis foreign, so each proves its comparison exists, and none can express two simultaneous mismatches. No number of them reaches this bug. The new control is added beside them rather than replacing them, because the two families fail on different bugs. The fix. The refusal carries The control is shown to discriminate, not asserted to. Reintroducing first-wins by returning an empty Also in this push: PR description updated — it still said "first slice / no readback" while carrying four slices. — sent from zesty-crane-477 |
…e stage ladder that is not yet the wall it looks like The readback's axes are observed separately, so evidence taken at different moments cannot be read as simultaneous state. A process seen running at 09:00 beside a terminal success written at 09:05 is stale-but-previously-true evidence, not a contradiction, and a fold treating the pair as simultaneous would manufacture contradictions out of ordinary staleness. It cuts the other way too: "terminal success and the output population is empty" is a contradiction ONLY when the output enumeration happened after the successful terminal was observable. So a cross-axis temporal conclusion is available only from a producer that establishes read order, and the answer is three-valued. "The relation was not observed" is neither ordered nor unordered: collapsing it into a negative would let a missing sweep read as evidence that two reads were unordered, which a reconciler would take as licence to ignore a conflict it cannot rule out. A cut belonging to another run answers Unobserved for the same reason -- it is well-formed, its sweep really happened, and it orders a different run's reads; borrowing it is authority substitution, where both halves check out and only the relation between them is invented. THE ORDER IS READ OFF THE SEQUENCE THE SWEEP TRAVERSED. An earlier revision of this file carried a hand-written position table beside the stage ladder under an annotation claiming it was derived from it. It was not: it was a second ordering, free to disagree, and the disagreement would have compiled -- the cut establishing one order while every comparison read another. Each stage now appends its own axis, so the ordering is a consequence of which stage functions ran. AND THE LADDER IS NOT THE WALL IT LOOKS LIKE, which is the part worth reading. The stages consume one another's tokens so that skipping one should be unwritable. Measured, it is not: passing a SweepStarted where a TerminalsEnumerated is declared compiles with ZERO blocking diagnostics. The cause is not local to this module. A value of one PARAMETERIZED type is silently accepted where a different parameterized type is declared at a direct-call argument, while the same mismatch on non-generic types refuses with `type mismatch: expected 'Product(Beta)', got 'Product(Alpha)'` and a bare scalar at that same position refuses with `value does not inhabit its declared type at the direct call argument`. The check runs there and does not separate two parameterized node types; different field names do not save it, and it is not the generic callee, since a fully concrete parameter fails identically. The annotation therefore states the rung as MITIGATABLE with its next-rung trigger named, rather than describing the shape as construction-over-validation. The ladder makes the correct order the obvious thing to write and gives the sweep one home; it does not make the wrong order unwritable, and an inflated rung is the thing that stops a class ever ranking for repair. When the direct-call argument judgment separates distinct parameterized types, this ladder becomes a wall with no edit here. Five witnesses, green by execution: no cut answers Unobserved rather than a negative; a completed sweep orders outputs and processes after terminals; the reverse pair reports out-of-order, without which a comparison answering "in order" for everything would pass the positive case and establish nothing; a foreign run's cut orders nothing here while this run's does; and the swept sequence holds every axis exactly once in stage order. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Fifth slice: the temporal observation cut — plus a below-floor compiler defect found while testing my own claimThe sliceThe readback's five axes are observed separately, so evidence taken at different moments cannot be read as simultaneous state. A process seen running at 09:00 beside a terminal success written at 09:05 is stale-but-previously-true evidence, not a contradiction — a fold treating the pair as simultaneous would manufacture contradictions out of ordinary staleness. It cuts the other way too: terminal success and the output population is empty is a contradiction only when the output enumeration happened after the successful terminal was observable. The answer is deliberately three-valued. "The relation was not observed" is neither ordered nor unordered; collapsing it into a negative would let a missing sweep read as evidence that two reads were unordered, which a reconciler would take as licence to ignore a conflict it cannot rule out. A cut belonging to another run answers A defect I introduced and caught in the same fileThe first revision carried a hand-written position table beside the stage ladder, under an annotation claiming it was derived from it. It wasn't — it was a second ordering, free to disagree, and the disagreement would have compiled: the cut establishing one order while every comparison read another. Each stage now appends its own axis, so the ordering is a consequence of which stage functions ran. The finding that is bigger than this PRThe stages consume one another's tokens so that skipping one should be unwritable. I tested it. It isn't. Passing a
The check runs at that position and refuses a scalar; it does not separate two parameterized node types. Different field names don't save it, and it isn't the generic callee — a fully concrete parameter fails identically. Load-bearing consequence beyond this PR: This is below floor per §4b ("values inhabit declared types"). It is not claimed as fixed here and I am not absorbing it into this lane; it needs a compiler owner. Rung, stated honestlyThe annotation says mitigatable, with the next-rung trigger named (the direct-call argument judgment separating distinct parameterized types). The ladder makes the correct order the obvious thing to write and gives the sweep one home; it does not make the wrong order unwritable. Calling it construction-over-validation would be the inflation that stops a class ever ranking for repair — and when that judgment lands, this ladder becomes a wall with no edit here. Five witnesses, green by execution, including the reverse-pair control — without it, a comparison answering "in order" for every pair would pass the positive case and establish nothing. — sent from zesty-crane-477 |
Correction to my previous comment: both of my claims about the compiler finding were wrongTwo things I asserted in the observation-cut comment need retracting, and the second is the dangerous one. 1. "Two causes, only one of which is the brand" — not established. I demonstrated two failing surfaces, not two root causes. The isolating probe:
Applied type arguments are not compared even without refinement, which explains the 2. "Runtime equality over the pair still holds — only the compile-time half is absent." This understated it. The exact standing: What this does and does not change in this PR. The attempt-graph admission stays strong — its fold actually checks work equality, roots, predecessors and cycles, so the executed fold is the evidence rather than the nominal type. Same for the repaired readback binder, which really compares all five subjects. What changes is the classification: possession of a generic sealed carrier is not authorization. A consumer must compare the subject against one derived from the desired run rather than treating possession of a Consequence for the eventual actuation boundary, recorded now so it isn't discovered later: a Routed out of this lane, as it should be: work item — sent from zesty-crane-477 |
…t admission, and the Attempt inert row its own dissolution condition retires Seeing a checkpoint-like artifact establishes that something was written. It does not establish that the thing written is a state training can continue from, and the gap between those two is where the expensive failure lives: a resume from a PARTIALLY published checkpoint takes model weights from step 500 beside an optimizer state from step 400, and the run does not crash. It converges to a different model, slowly, and every downstream comparison then joins on a Work identity describing a computation that never happened. So admission is its own carrier and the observation cannot be widened into it by renaming. What must hold is a CLOSED component roster rather than an ad hoc check, because the failure is per-component: a missing optimizer state and a missing RNG state are both "incomplete", and a check asking "are there components?" passes a checkpoint holding only weights. Each component carries its own digest and its own materialization readback -- one digest over the whole checkpoint makes "which part is missing" unanswerable, and a component recorded without a readback is a claim that bytes exist somewhere, which is exactly the claim a resume is about to bet a run on. Atomic publication is observed rather than assumed, and unobserved is its own arm: a writer that published components one at a time leaves a checkpoint whose parts are individually valid and jointly inconsistent, and "we did not observe the publication standing" is neither "incomplete" nor "atomic" -- collapsing it either blocks a healthy resume or authorizes a torn one. The attempt must be a member of the admitted run graph, without which a checkpoint from another run whose components all read back correctly is admissible: every component honest, the publication genuinely atomic, and the state belonging to a different computation. Manifest agreement moves to resolution.dag beside the coordinate projection, as a POPULATION of differing coordinates rather than a boolean or a first-difference. "The manifests differ" sends a reader to twenty-three coordinates; naming only the first hides the rest until it is fixed. Both are answers a hash could have given, which is the reason this reads the axis-keyed projection: a hash answers same-or-different and can never answer WHICH, and WHICH is the entire purpose of the effective-manifest axis. CI REPAIR IN THE SAME CHANGE, and it is the roster working as designed rather than a collision. The floor's inert-carrier lens went red with exactly one failure more than main, isolated by diffing the failed sets rather than guessed: v2/test/lens_inert_carrier. The roster's Attempt row records a carrier "referenced only by fabric_terminal_contract_witness_test so far", and its dissolution condition reads "a live consumer reads the carrier; the stale-roster check then forces this row's deletion". attempt_graph.dag is production code that reads Attempt, so the row is stale and the row itself says the remedy is deletion. Attempt is the only rostered carrier this lane's production code consumes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…on witnesses, and the one a torn publication would pass The previous commit landed checkpoint admission with no witnesses. A compiling carrier is specification without execution -- the failure this lane keeps naming in other people's work -- so this is the evidence that should have shipped with it. The witness that carries the class is a_checkpoint_holding_only_weights_is_refused_naming_every_ absent_component. A checkpoint holding only model weights is exactly what a torn publication leaves behind, and it is the input a resume must never accept: the run continues with weights from this step beside an optimizer state from an earlier one and DOES NOT CRASH. It converges to a different model. A check asking "are there components?" passes that input, which is why the roster is closed; the witness asserts all four absent components are named AND that model_weights is not reported missing, so it fails in both directions -- if the roster stops being closed, and if the refusal starts over-reporting. The rest, each failing on something the others cannot see: incomplete and unobserved publication do not read as each other, because one says the writer left a torn checkpoint and the other says nobody looked, and their remedies are opposite; a checkpoint whose attempt is outside the admitted run graph is refused even though every component reads back honestly, its publication is genuinely atomic and its manifest agrees -- membership is the only thing separating it from an admissible one; a diverged manifest refuses naming the COORDINATE and reports exactly one, which a hash comparison could never have produced; and all independent defects are reported together, so a checkpoint missing its RNG state AND diverging on gradient accumulation does not take two rounds to learn about, with the second reason reading as a regression introduced by fixing the first. The positive control is what makes every refusal above load-bearing: an admitter that refused everything would satisfy all of them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Sixth slice: checkpoint admission — plus the CI repair, and a gap of my own I'm namingThe CI failure was mine, and the roster told me the remedy
Cause: the inert-carrier roster's A gap I left and then closedThe previous push landed Why admission is a separate carrier from observationSeeing a checkpoint-like artifact establishes that something was written, not that it is a state training can continue from. The gap between those is where the expensive failure lives: a resume from a partially published checkpoint takes model weights from step 500 beside an optimizer state from step 400, and the run does not crash. It converges to a different model, slowly, and every downstream comparison then joins on a Work identity describing a computation that never happened. So: a closed component roster (a check asking "are there components?" passes a checkpoint holding only weights); per-component digest and materialization readback (one digest over the whole checkpoint makes "which part is missing" unanswerable; a component without a readback is a claim that bytes exist somewhere, which is what the resume is about to bet a run on); atomic publication observed, with Six witnesses, all green by executionThe one carrying the class is The others each fail on something the rest cannot see: incomplete vs unobserved publication do not read as each other (one says the writer left a torn checkpoint, the other says nobody looked — opposite remedies); a foreign-run checkpoint is refused even though every component reads back honestly, the publication is genuinely atomic, and the manifest agrees — membership is the only thing separating it from an admissible one; a diverged manifest refuses naming the coordinate and reports exactly one, which a hash comparison could never produce; independent defects are all reported together. And the positive control, without which an admitter that refused everything would satisfy every refusal witness above. Also landed
Still not here: reconciliation and actuation. Per the design ruling, the ordered effect sequence belongs in the Spark realization with non-parameterized outer types (the generic stage ladder cannot be a wall under the routed compiler defect), and wet actuation must not sit behind a generic authorization alone. — sent from zesty-crane-477 |
…evidence composition, and reconciliation at per-attempt grain Reconciliation is a pure fold that draws a conclusion and does nothing; actuation consumes the conclusion. A fold that could also act would decide and do in one step, leaving no representable state in between for anything to disagree with. CONFLICTS ARE A PER-ATTEMPT FACT, AND AN EARLIER ATTEMPT AT THIS MODULE GOT THAT WRONG AT THE GRAIN AND WAS DISCARDED WHOLE. Retry, capability escalation and requested re-execution create NEW attempts rather than mutating an earlier one, so across attempts a failure then a success is the ordinary local-model-to-Opus escalation history this programme exists to record; a terminal beside a later running process is normal continuation; and two attempts producing two digests is two attempts. The real contradictions all live within ONE attempt. Reading any of them at run grain refuses exactly the evidence the escalation model is built to keep, which is why the witnesses come in pairs that are identical one attempt identity apart and must return opposite verdicts. THE HOLE THIS CHANGE CLOSES WAS IN CODE ALREADY PUSHED. The observation cut established that SOME sweep enumerated the axes in order, and the readback carried populations each stamped with the enumeration receipt that produced it -- and nothing related the two. A well-formed, same-subject cut from a DIFFERENT sweep could therefore order populations it never observed: every half honest, the relation between them invented. That is the third instance of one defect this lane has removed -- a manifest accepted beside evidence it could disagree with, a contract accepted beside a manifest it could disagree with, and now a cut accepted beside populations it never saw. Reconciliation taking graph, readback and cut as three independent arguments would have been the fourth. So TrainingRunEvidenceComposition is admitted once, per axis, by receipt equality, and reconciliation consumes only the composition. A cut naming another sweep's receipts is refused per axis with every mismatch retained. A cut covering an axis nobody enumerated gets its own refusal rather than a receipt mismatch, because that is a producer reporting work it did not do. AN EMPTY BLOCKER POPULATION IS NECESSARY AND NOT SUFFICIENT FOR CONVERGENCE. Five successfully enumerated empty populations contain no contradiction anywhere and are plainly not a converged run -- they are a run nobody started. Convergence is therefore reached from POSITIVE evidence, exactly one completion candidate, and the candidate is mintable only downstream of the graph and the cut: without an ordered sweep, an output population read before the terminal is indistinguishable from a finished run whose artifact is missing, and those have opposite remedies. A GUARD REMOVED RATHER THAN SHIPPED. An earlier revision threaded an `ordered` boolean through the cross-axis arms. Once composition became the only door, that boolean could not be false for any admissible input, and a guard whose red is unreachable is a decoration that gets cited as coverage. The requirement did not disappear; it moved to the door. Ten witnesses, all green by execution, including the positive control without which a fold that blocked unconditionally would satisfy every refusal above. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Seventh and eighth slices: evidence composition + reconciliation at per-attempt grainThis completes the observation spine: resolution → readback → attempt graph → observation cut → checkpoint admission → evidence composition → reconciliation. Ten witnesses, all green by execution. The grain, and the version I discardedRetry, capability escalation and requested re-execution create new attempts rather than mutating an earlier one. So across attempts:
The real contradictions all live within one attempt. An earlier draft of this module keyed them at run grain, and I discarded it whole rather than land it — it would have refused exactly the evidence the escalation model is built to keep. The witnesses therefore come in pairs that are identical one attempt identity apart and must return opposite verdicts:
A hole in code I had already pushedThe cut established that some sweep enumerated the axes in order; the readback carried populations each stamped with its enumeration receipt. Nothing related the two. A well-formed, same-subject cut from a different sweep could order populations it never observed — every half honest, the relation between them invented. That is the third instance of one defect this lane has removed: a manifest accepted beside evidence it could disagree with; a contract accepted beside a manifest it could disagree with; now a cut accepted beside populations it never saw. Reconciliation taking graph/readback/cut as three independent arguments would have been the fourth.
Convergence needs positive evidence
A guard removed rather than shippedAn earlier revision threaded an Not hereActuation. Per the design ruling it must not sit behind a generic authorization while the routed compiler defect stands ( — sent from zesty-crane-477 |
Correction: the compiler defect I reported is not a generics defect
What I claimed: distinct parameterized types are silently admitted at a direct-call argument, while "the same mismatch on non-generic types refuses" — with the non-generic case cited as the control proving nominal comparison exists. What is actually true: a non-generic So the class is which producer sees the pair, and it is wider than generics. My four-case matrix was a real measurement that supported a wrong generalisation — the discriminating variable was sitting in the fixtures the whole time and I read it as "generic vs non-generic" because that was the axis I had set out to test. Root-cause count: one. The caution I recorded — two failing surfaces, root-cause count not established — was right, and the Measured after the repair, each fixture its own entry compile, all refusals What does not change for this PR. The consequence I recorded still stands and is if anything broader: possession of a sealed carrier is not authorization, — sent from zesty-crane-477 |
|
Floor red at `c1db6c9` is main's, not this branch's — measured, not inferred. Compared this PR's floor job (run 33182227955) against the latest main floor run (33145062452, `3a8344b5`):
The Not pushing a speculative fix: there is nothing on this branch to repair, and re-running would replay the same main-owned population. |
… the execution claim commits before the trainer starts An attempt must be durably claimed BEFORE a trainer process exists, and the claim is committed by a control-plane transaction rather than by the actuator. The actuator only realizes an already-committed claim, so a controller that dies between commitment and launch leaves a claim that can be resumed rather than a run that gets started twice. THE EXCLUSION KEY IS THE TRANSITION, NOT THE ATTEMPT IDENTITY, and that is the whole content of the module. A uniqueness constraint on the attempt identity excludes nothing: two convergence passes that both read "execution required" choose attempt-A and attempt-B, the identities differ, and both commit. What must be unique is the SEMANTIC TRANSITION -- this demand, this work, this cause -- so the second pass compare-and-sets an occupied slot and receives the first pass's claim instead of minting a rival one. The witness pair is written so this is checked rather than assumed: the race witness asserts one committed attempt, and a separate control asserts the two candidate identities DIFFER while the transition slots are EQUAL. Without that control the race witness is satisfied by any key at all, including the one that does not work. ALREADY-COMMITTED IS A SUCCESS, NOT A REFUSAL. The losing pass observed a real state and lost a compare-and-set; the correct answer is the winner's claim so it can dispatch the SAME occurrence. Returning a refusal would make a benign race look like a defect and invite a retry into a second mint. Snapshot-stale is deliberately NOT folded into it: the ledger moved under the caller, so what the caller believes is unreliable and the remedy is to re-observe, not to proceed with either claim. DISPATCH IS RECORDED ON A COMMITTED CLAIM AND HAS NO OTHER ROUTE. TrainingExecutionClaim is sole_constructor with admit_callers limited to admit_start_claim and record_claim_dispatch, so "dispatched" cannot be asserted about an occurrence that was never durably claimed. The ordering is a property of the constructor surface rather than an invariant someone remembers to preserve. CONTROL STATE IS COMPOSED, NOT SUPPLIED BESIDE THE EVIDENCE. Passing a claim or grant list into reconciliation would have been the FOURTH instance of one defect this lane has removed: a manifest beside evidence it could disagree with, a contract beside a manifest, a cut beside populations it never observed, and now a control record beside a graph it never described. TrainingRunConvergenceInput joins the two admitted compositions on one subject and reconcile_training_run consumes that and nothing else. Reconciliation moved with it. A graph attempt with no execution claim is now TrainingAttemptWithoutExecutionClaim -- a control-state defect, not a reason to launch. It is exactly the state a retrospective writer produces, and answering it with "execution required" is an instruction to start another trainer. ExecutionRequired is correspondingly narrow: a committed undispatched claim is TrainingRunLaunchDispatchRequired and a dispatched one awaiting a process is TrainingRunLaunchPending, because the two carry different instructions -- one needs an actuation, the other needs only an observer. BOTH LAUNCH ARMS CARRY A POPULATION, NOT ONE CLAIM. Two active claims on two lawful transitions are both awaiting their launch, and reporting only the first would send a caller to dispatch one and read the run as handled. That is the first-wins defect this lane already repaired in the readback binder; it was reintroduced here in the first cut and is fixed with its own discriminating control asserting the reported population is 2. One existing witness went red on purpose and is rewritten rather than deleted: no_blockers_over_empty_populations_requires_execution_rather_than_converging asserted execution-required over the ordinary two-attempt fixture, which was true only while the fold could not see what had been claimed. Over that fixture it would now be asserting that a run with two live claims should have a third trainer started, so it is re-authored at the grain the narrowed arm actually means: no attempts, no claims, empty populations. Green by execution: 12 execution-control witnesses and 16 reconciliation witnesses, 0 red. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
1 participant
Why
The resident-model programme compares training runs — control against candidate, base against adapter — and every comparison joins on a Work identity. So that identity must name one computation. Nothing on this tree modelled the step between an authored recipe and an exact run, so a run's identity could be minted from values the trainer had not yet chosen.
Scope (this PR now carries four slices — the description below was written for the first and is kept because each slice's reasoning still stands):
observations → TrainingResolution → ResolvedTrainingWork → TrainingRunDesired, the join key everything else needs.Still not here: reconciliation and actuation. Reconciliation additionally needs a temporal observation cut, without which a fold would manufacture contradictions out of ordinary staleness. Checkpoint evidence is deliberately named
TrainingCheckpointObservation— it records that an artifact was seen and binds none of optimizer/scheduler/RNG/data-order state, so no arm may derive "resume required" from it until a checkpoint admission lands. Production episode initiation stays blocked onowned_host(#9534).See the PR comments for each later slice's reasoning and evidence.
Construction walls
No deferral is writable. No
Auto/Latest/Defaultarm; zero-invalid axes arePositiveInt; convention-word axes are closed enums —numeric_format: NonEmptyStradmits"auto", which is the failure wearing the shape of a value. An unpinned coordinate isAxisUnresolvedand refuses, naming a closed axis, so a new coordinate can't be added without failing every exhaustive match.Dropout is bounded by a sealed mint. Zero is meaningful so
PositiveIntwould be wrong, butNatadmits1001. No bounded refinement predicate exists to consume, so the mint refuses above 1000 — with both boundary admissions asserted beside the refusal, so the wall can't be satisfied by refusing everything.The manifest is a total projection of the evidence, not an argument beside it.
sole_constructorconfines who may construct and establishes nothing about what is true of supplied values — a manifest naming base B beside evidence attesting base A was constructible and no wall could see it.The contract is derived, not accepted.
derive_work_keyreads only contract and requirements, so a caller could resolve a manifest pinning seed 7 and pass a contract mentioning nothing about it: two runs differing in seed, optimizer and numeric format would have shared one Work key while producing different weights. Field-tagged, delimiter-separated over delimiter-free renderings, withserialize_content_hashpreserving the hash family — a dropped family is an identity collision, not a formatting detail.Global batch is derived, never stored.
micro_batch,gradient_accumulationandglobal_batchas three independent coordinates with no worker count meant(2,8,16)and(2,8,64)both construct, their difference an omitted topology fact rather than two spellings of one computation. This slice admits single-worker only; worker count and reduction policy are semantic, not placement, and belong here when a coordinated multi-host realization exists.Low-rank adaptation only. An earlier revision carried
FullParameter | LowRankAdaptationwhile keepingrank/scaling/dropoutunconditional — so a full-parameter run carried a LoRA rank its trainer never reads, and two identical full-parameter runs would derive different keys from an authored rank. That is one computation receiving many identities. The arm is deleted; a full-parameter arm kept only to anticipate a nonexistent consumer is a carrier-before-consumer scaffold. The later shape is a sum of products.Admission derives under
demand.work.principal. Requester and accounting scope are different roles sharing a representation; deriving under the requester refused every demand whose work was scoped to an organization, making service accounts and delegated execution unrepresentable.Evidence — green by execution
micro × accumulationSeedAxisdemand.workrefusedThe control is proven falsifiable on a coordinate a single-field mutation could not reach: deleting the
packingrow from the identity material flips it tofalse; restoring flips it back.Correction to an earlier version of this PR body
It claimed the completeness wall covered every semantic coordinate while the suite varied only two — seed and base artifact — with the other twenty-one fixed in one fixture. The seed mutation proved the seed control falsifiable and established nothing about the rest. The claim was wider than its executable population, which is the inflation DESIGN §4b rates as worse than sitting low. That is what this PR's latest commit repairs.
What this does not do
No production initiation. Training consumes the fabric's standing and models no cost cause of its own —
owned_hostreturns an offer withOperatingCostUnreadand the selection fold owns whether it can be priced, so a training-specific refusal would be a fourth authority for a question three layers already answer.No
TuningReciperecord and noTuningRecipeIdentity: no recipe artifact exists, so an opaque hash would name nothing.