Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion dag/test/claim/legacy_binding_projection_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,13 @@ test fn a_decision_about_a_non_base_occurrence_refuses() -> Bool {
// insertion belongs to the change that does that wiring, not to the change that opened the carrier
// -- and this comment is corrected here rather than left standing, because a refusal justified by a
// reason that has stopped being true is the stale-prose failure inside the honesty argument itself.
test fn a_declared_insertion_refuses_because_no_carrier_can_express_its_cause() -> Bool {
//
// THE FUNCTION NAME CARRIES THE SAME CLAIM AND WAS CORRECTED WITH IT. It read
// `..._because_no_carrier_can_express_its_cause`, which asserts the proposition this block just
// retired. Correcting the annotation and leaving the name would have been the worse half-measure of
// the two: a reader trusts a name without reading the body, so a false name outranks a true comment
// sitting directly above it.
test fn a_declared_insertion_refuses_because_this_projector_is_not_wired_to_the_cause_arm() -> Bool {
match lbp_emit(
expected_base: [10],
decisions: [lbp_carry(base: 10, projected: 11)],
Expand Down
65 changes: 42 additions & 23 deletions src/v2/workflow/legacy_binding_projection.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
module v2.workflow.legacy_binding_projection

import std.types { String, Bool, Int, List, NonEmptyStr }
import std.types { String, Bool, Int, List }
import std.content_hash { Fnv1a64Structural }
import std.dissolution { DissolutionCondition, UnboundDissolution }
import std.dissolution { DissolutionCondition, bound_dissolution }
import std.decl_ref { decl_ref }
import std.occurrence_identity { OccurrenceId, ScopedOccurrenceRef }
import v2.workflow.legacy_binding_observation {
LegacyBindingObservationSubject,
Expand All @@ -24,13 +25,19 @@ import v2.workflow.legacy_binding_delta {
// per-occurrence carry decision into the ProjectionProvenance the delta consumes.
//
// It emits ProjectedFromSource ONLY. ProjectedAsInsertion is not merely unimplemented here, it is
// UNEMITTABLE, and the reason is a property of the substrate rather than of this module:
// `std.occurrence_identity` `NodeOccurrenceIdentity` has two arms, `OccurrenceSynthetic` and
// `OccurrenceMinted`, and neither carries a cause -- `caused_by` appears zero times anywhere in
// `dag/std` or `src/v2/std`. A projector-created node therefore has no representable provenance,
// and the arm it would have to borrow is already the fill value for every non-parser-constructed
// node, so borrowing it would collapse parser-minted, incidentally-synthetic and
// projection-synthesized-with-cause into one symbol.
// UNEMITTABLE BY THIS MODULE, and the reason has MOVED -- it used to be a property of the substrate
// and is now a property of this module's wiring. `std.occurrence_identity` `NodeOccurrenceIdentity`
// once had two arms, `OccurrenceSynthetic` and `OccurrenceMinted`, neither carrying a cause; a
// projector-created node had no representable provenance, and the arm it would have had to borrow is
// already the fill value for every non-parser-constructed node, so borrowing it would have collapsed
// parser-minted, incidentally-synthetic and projection-synthesized-with-cause into one symbol.
//
// gunbc#9359 closed that: `OccurrenceProjected { id, caused_by }` carries the cause, and
// `v2.workflow.legacy_binding_delta` `insertion_provenance_entry` derives the `ProjectedAsInsertion`
// row from it. THE REFUSAL BELOW STAYS ANYWAY, and the distinction is the point -- what this module
// cannot do is no longer EXPRESS an insertion's cause but EMIT one, because nothing here has been
// taught to allocate a projected occurrence and name what caused it. A refusal is honest about a
// capability that is unbuilt; it would be dishonest as a claim that the capability is impossible.
//
// THE COST OF THAT IS A WRONG ANSWER, NOT A MISSING FEATURE, which is the whole reason this module
// refuses instead of improvising. The delta's source-coverage law reads carried sources; an
Expand All @@ -40,11 +47,12 @@ import v2.workflow.legacy_binding_delta {
// dropped occurrence survived. That is exactly the defect a review caught on gunbc#9337, arriving
// through the carrier instead of through the filter.
//
// So insertions are BLOCKED ON A NAMED WORK ITEM (`node://adhoc-e1692c72-f81`: model the third arm
// as a shared-authority algebra decision), and this module's refusal is the honest state until it
// lands. No placeholder cause, no optional field, no convention -- each of those is the fabricated
// cause wearing a different hat, and a fabricated cause is worse than an omitted insertion because
// the omission is countable and the fabrication is not.
// That hazard is why the carrier gained a third ARM rather than an optional field: no placeholder
// cause, no `caused_by: OccurrenceId?` on the minted arm, no convention -- each of those is the
// fabricated cause wearing a different hat, and a fabricated cause is worse than an omitted
// insertion because the omission is countable and the fabrication is not. With the arm landed, the
// remaining work is wiring this projector across it, and until that lands the refusal below is
// still the honest state.
// THE RETIREMENT IS A TYPED CONDITION, NOT A SENTENCE. An earlier revision of this module carried
// the whole thing as `data ...: String`, which is the shape §4c names as modeling debt and which
// #6262/#6424 already swept once: a dissolution condition is machine-consumed, so it belongs in
Expand All @@ -53,18 +61,29 @@ import v2.workflow.legacy_binding_delta {
// a bounded trigger; that is backwards -- naming a trigger is precisely what makes it a fact rather
// than commentary, and therefore precisely what disqualifies the String carrier.
//
// It is UNBOUND rather than bound, and that is forced rather than lazy. The bound form would be
// `DeclarationAppears` over `std.occurrence_identity` `OccurrenceProjected`, and that declaration
// does not exist on this base -- so authoring the citation here would be refused by the citation
// wall as a name that does not resolve, which is the §3 fabricated-citation class the dissolution
// module's own annotation warns about by name. 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.
// IT IS NOW BOUND, AND THIS IS THE CHANGE THAT WAS ENTITLED TO BIND IT. An earlier revision left it
// UNBOUND and said so honestly: the bound form is `DeclarationAppears` over `std.occurrence_identity`
// `OccurrenceProjected`, that declaration did not exist on the base this module was authored against,
// and authoring the citation there would have been refused by the citation wall as a name that does
// not resolve -- the §3 fabricated-citation class the dissolution module's own annotation warns about
// by name. That revision also named its own trigger: the condition binds in the same change that
// rebases this module onto the arm, at which point the ref is verifiable at the moment it is written.
//
// gunbc#9359 is that change. It lands the third arm and rebases this file onto it in one commit, so
// the citation is authored at the first moment it CAN be authored honestly rather than at the first
// moment it is convenient. Leaving it unbound here would have been worse than merely stale: a
// dissolution condition is machine-consumed, so the debt would have reported UNBOUND while its own
// binding declaration sat in the same commit -- a false fact rather than a false comment.
//
// WHAT DID NOT CHANGE: the refusal. `ProjectionInsertionUnrepresentable` still fires, because the
// carrier boundary is closed and the PROJECTOR is not yet wired across it. Binding the dissolution
// records that the blocking declaration now exists; it does not claim this module emits insertions.
//
// The instrument for the claim, rather than a transcription of it: grep `caused_by` across `dag/std`
// and `src/v2/std`, and read `NodeOccurrenceIdentity`'s arms in `std.occurrence_identity`.
data legacy_binding_projection_insertion_dissolution: DissolutionCondition = UnboundDissolution {
description: "ProjectedAsInsertion is unemittable while std.occurrence_identity NodeOccurrenceIdentity carries no arm for a projector-created node's cause. Binds to DeclarationAppears over OccurrenceProjected once that arm lands (gunbc#9359); ProjectionInsertionUnrepresentable then flips to a regression control over the InsertionCauseLost population rather than retiring, because deleting an executed refusal recreates specification-without-execution one rung up." as NonEmptyStr
}
data legacy_binding_projection_insertion_dissolution: DissolutionCondition = bound_dissolution(
ref: decl_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceProjected")
)

// A CARRY DECISION IS PER BASE OCCURRENCE, AND ITS DENOMINATOR IS THE BASE OBSERVATION'S OWN
// EXPECTED POPULATION -- not the projected side, and not the set of decisions this module happened
Expand Down
Loading