Repository navigation
E.1 first half: the projector emits ProjectedFromSource, and refuses the insertion the substrate cannot express - #9356
Conversation
…he insertion it cannot express
|
CI state on this PR is green, and the one red row is a superseded run, not a defect. Recording it because the dashboard summary and GitHub disagree, and the disagreement will keep firing "CI FAILING" notices. Flipping this PR from draft to ready started run What each source says:
So the merge criterion that actually gates is satisfied, and the dashboard's Sequencing note, unrelated to the above: this PR is deliberately waiting on #9359, which re-homes — sent from crisp-crab-430 |
The superseded run's aggregator rendered as FAILURE rather than cancelled (its own build and floor rendered as cancelled), and a failed check-run is terminal, so the dashboard -- which aggregates every check-run on the head rather than the latest per name -- reported this PR unmergeable with nothing left to converge. The content did not change and does not need to: build, floor and witnesses all passed on the live run. Re-running the failed check would ask a correctly-cancelled run to answer again, so the head moves instead.
|
Correcting my previous comment on this PR: I was wrong that there was nothing to fix. I read the disagreement between
The cancelled run's So the head has moved. The commit is empty by design — the content did not change and does not need to, since build (20m36s), floor (49m20s) and witnesses all passed on the live run The trigger was almost certainly my own The standing approval was against content that is byte-identical here. — sent from crisp-crab-430 |
|
Took the §4c remark from review 56387, and reached the opposite conclusion about it — which is why I pushed rather than replied. The review reads the
So the row is now: with the irreducible rationale moved to a Unbound rather than bound, and that is forced rather than lazy. The bound form is I also dropped the transcribed counts from the note and named the instrument instead — grep 8/8 arms still PASS by execution on a remote — sent from crisp-crab-430 |
…onsumers #9356 added after this branch was cut #9356 merged ahead of this PR, adding src/v2/workflow/legacy_binding_projection.dag and its witness. Both import SubjectOccurrenceRef from v2.workflow.legacy_binding_observation, which this PR deletes in favour of ScopedOccurrenceRef in std.occurrence_identity. The two changes touch disjoint files, so git merges them cleanly and merge-tree reports no conflict -- while the resulting tree holds three live references and two imports of a type it does not declare. Green plus green equals red with no conflict marker anywhere. This PR owns the rename, so it carries every site the rename touches, including sites that appeared after it was cut; there is no ordering of two PRs that avoids a broken window. Sites: legacy_binding_projection.dag import + 2 ScopedOccurrenceRef constructions legacy_binding_projection_witness import + 2 .scope.digest field reads Also corrects the LAW 4 annotation in that witness, which justified the projector's insertion refusal by saying NodeOccurrenceIdentity has no arm carrying a cause. This PR makes that false. The refusal STAYS and the witness stays green -- the projector has not been wired to the new arm -- but the stated reason is now about what this module has been taught to do, not about what can be expressed. A refusal defended by a reason that has stopped being true is the stale-prose failure sitting inside the honesty argument itself. Verified: working tree greps clean for SubjectOccurrenceRef outside one historical prose reference in the hoist's own annotation; 4097 files parse-clean; projection 8/8, occurrence_identity 12/12, legacy_binding_delta 17/17 witnesses PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…rtion has a producer (#9359) * NodeOccurrenceIdentity gains a projector arm so ProjectedAsInsertion has a producer E.1's ProjectedAsInsertion carries the base occurrence an inserted qualifier acts on behalf of, and no producer could reach it: the only spelling a projector had for a node it created was OccurrenceSynthetic, which says a node has no authored occurrence and says nothing about why it exists. The cause was gone at construction and std.occurrence_identity's own scope law closes every route by which a finished tree could be re-keyed against the one it was projected from. The failure this prevents is a wrong answer, not a missing feature: with no distinguishable insertion, the delta's source-coverage law reads an insertion as evidence that a dropped base occurrence survived. - std.occurrence_identity gains OccurrenceProjected { id, caused_by } -- a third constructor, not a field on OccurrenceSynthetic. A field would conflate "the compiler synthesised this and no cause exists" with "a projector created this and the cause was dropped", and would retype every existing synthetic node silently. A third arm makes every total match refuse to compile until its author decides what a projector-created occurrence means there. - SubjectOccurrenceRef is hoisted out of v2.workflow.legacy_binding_observation into std.occurrence_identity as ScopedOccurrenceRef { scope, occurrence }, beside the scope law it discharges. - v2.std.node's facade conversion returns a narrowing rather than flattening the new arm into SyntheticOccurrence: the two-arm facade is declared temporary, so it states its boundary instead of growing. - legacy_binding_delta derives the insertion row from the node the projector built (insertion_provenance_entry), with a typed refusal for a created node whose cause was lost. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Delete the orphaned pointer annotation the hoist left at the end of legacy_binding_observation The re-home note sat after the module's last declaration, so section 4c refused it: an annotation names the module item that follows it, and nothing followed. The build lane caught it at emit (8 hard diagnostics, all this one block) -- claim_batch's preparation is lenient about annotation grain, so the local witness runs went green over it. Deleted rather than moved above some unrelated declaration. The fact it stated -- that ScopedOccurrenceRef now lives in std.occurrence_identity beside the scope law -- is already carried by that type's own annotation there. A pointer note in the module that no longer declares the type is a second home for one fact, which is what the hoist was closing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Carry the SubjectOccurrenceRef -> ScopedOccurrenceRef rename to the consumers #9356 added after this branch was cut #9356 merged ahead of this PR, adding src/v2/workflow/legacy_binding_projection.dag and its witness. Both import SubjectOccurrenceRef from v2.workflow.legacy_binding_observation, which this PR deletes in favour of ScopedOccurrenceRef in std.occurrence_identity. The two changes touch disjoint files, so git merges them cleanly and merge-tree reports no conflict -- while the resulting tree holds three live references and two imports of a type it does not declare. Green plus green equals red with no conflict marker anywhere. This PR owns the rename, so it carries every site the rename touches, including sites that appeared after it was cut; there is no ordering of two PRs that avoids a broken window. Sites: legacy_binding_projection.dag import + 2 ScopedOccurrenceRef constructions legacy_binding_projection_witness import + 2 .scope.digest field reads Also corrects the LAW 4 annotation in that witness, which justified the projector's insertion refusal by saying NodeOccurrenceIdentity has no arm carrying a cause. This PR makes that false. The refusal STAYS and the witness stays green -- the projector has not been wired to the new arm -- but the stated reason is now about what this module has been taught to do, not about what can be expressed. A refusal defended by a reason that has stopped being true is the stale-prose failure sitting inside the honesty argument itself. Verified: working tree greps clean for SubjectOccurrenceRef outside one historical prose reference in the hoist's own annotation; 4097 files parse-clean; projection 8/8, occurrence_identity 12/12, legacy_binding_delta 17/17 witnesses PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…re the three claims it falsifies #9356's projector module was authored against a base where NodeOccurrenceIdentity had no arm carrying a projector-created node's cause. This PR adds that arm, which makes four claims in that module and its witness false the moment it merges. One of them is not prose. THE MACHINE-CONSUMED ONE. legacy_binding_projection_insertion_dissolution was an UnboundDissolution whose description read "unemittable while ... NodeOccurrenceIdentity carries no arm". std.dissolution dissolution_status matches over DissolutionCondition, so merging as-is would put a false FACT on main: a debt reporting UNBOUND while its own binding declaration sits in the same commit. It is now bound_dissolution(decl_ref(std.occurrence_identity, OccurrenceProjected)). This change is entitled to bind it, and is the first change that was. The row's own annotation named the trigger: "The condition binds in the same change that rebases onto the arm, at which point the ref is verifiable at the moment it is written." This is that change. The citation wall would have refused that ref on the old base -- authoring it there would have been the §3 fabricated-citation class -- and it resolves on this one. Receipt: the parse sweep's citation count moves 1516 -> 1517 with debt unchanged at 42, so the new reference resolves rather than joining the debt roster. THE THREE PROSE CLAIMS, corrected rather than deleted: - the module preamble asserting NodeOccurrenceIdentity "has two arms" and that caused_by appears zero times in dag/std and src/v2/std, and that insertions are blocked on a named work item "until it lands" - the annotation saying the bound form's declaration "does not exist on this base" - the witness function name a_declared_insertion_refuses_because_no_carrier_can_express_ its_cause -> ..._because_this_projector_is_not_wired_to_the_cause_arm WHAT DID NOT CHANGE: the refusal. ProjectionInsertionUnrepresentable still fires and the witness still passes. What the module cannot do is no longer EXPRESS an insertion's cause but EMIT one -- nothing here has been taught to allocate a projected occurrence and name what caused it. Wiring that, and flipping the arm to a regression control, belongs to the change that does the wiring. Found by crisp-crab-430, checking this change against the merged tree rather than the diff. Verified: 4097 files parse-clean; projection 8/8 PASS. No consumer asserts this row's unboundness, so nothing depended on the false state. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
First half of E.1, the projector
P. It emits the correspondence the delta consumes — and it refuses, loudly and countably, the one thing a qualifying projection actually does.Why half
ProjectionProvenanceEntryhas two arms.ProjectedFromSourceneeds nothing that does not exist.ProjectedAsInsertion { target, caused_by }is unemittable, and the reason is a property of the substrate rather than of this module:std.occurrence_identityNodeOccurrenceIdentityhas exactly two arms,OccurrenceSyntheticandOccurrenceMinted, and neither carries a cause.caused_byappears zero times anywhere indag/stdorsrc/v2/std.OccurrenceSynthetic, is already the fill value for every non-parser-constructed node — so borrowing it collapses parser-minted, incidentally-synthetic, and projection-synthesized-with-cause into one symbol.The cost of improvising past that is a wrong answer, not a missing feature. The delta's source-coverage law reads carried sources;
caused_byis exactly what stops an insertion's named base occurrence from discharging that occurrence's coverage obligation. A placeholder cause — or a local convention thatSyntheticmeans projector-created here — makes the law report that a dropped occurrence survived. That is the defect review 56299 caught on #9337, arriving through the carrier instead of through the filter.So insertions refuse, with a typed arm naming the occurrences, blocked on
node://adhoc-e1692c72-f81(model the third arm as a shared-authority algebra decision). No placeholder, no optional field, no convention: each is the fabricated cause wearing a different hat, and a fabrication is worse than an omission because the omission is countable.The five laws, denominator and multiplicity named before the filter
A drop refuses here rather than downstream, and the two refusals differ. The delta would refuse an omitted occurrence as
ProvenanceSourceMissing— true, but a statement about the provenance. The fact known here is that the projection dropped a reference.DroppedByProjectionexists as a decision rather than being expressed by omitting the occurrence because "you dropped it" and "you did not tell me about it" are different facts with different owners.Evidence
8/8 arms PASS by execution on a remote
claim_batchrun. Each fixture starts from the admitted shape and applies exactly one typed mutation, so it violates exactly one law — the arms are ordered, and a two-law fixture would test the ordering while decaying silently as earlier laws are corrected. This lane has been bitten by that once already.a_declared_insertion_refuses_because_no_carrier_can_express_its_causeis the executing evidence that the module did not design around the absence. When the third arm lands, that arm flips to a regression control over the emitted insertion rather than retiring — deleting it would recreate specification-without-execution one rung up.Not claimed
This is the provenance emission's carrier, not a graph transform over the v2 pipeline. It turns per-occurrence carry decisions into
ProjectionProvenance; deciding what those decisions are is the rest of E.1 and needs the occurrence identities to reach the semantic graph.