Skip to content
Merged
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
709 changes: 11 additions & 698 deletions dag/gunbc/guarantee_stall.dag

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module gunbc.guarantee_stall.algebra_operation_associativity_undeclarable_stall

import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed }
import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, UncountedNotEnumerable }

data algebra_operation_associativity_undeclarable_stall: GuaranteeStall = GuaranteeStall {
subject: "no declared operation in the tree can be said to be associative",
current: OutsideTheLadder,
ceiling: StructurallyGuaranteed,
blocker: AwaitsOneGrounding { grounding: "std.algebra's Semigroup<T> carries the law its name asserts, so that it is distinguishable from Magma<T>" },
population: UncountedNotEnumerable { reason: "every n-ary application of a binary operation in the corpus depends on associativity and none of them can say so. concat alone is roughly 1200 free-call sites above binary across 64 measured arities, but the class is not concat: it is every operation whose surface arity exceeds its declared arity, and nothing enumerates those because nothing can currently ask the question." },
next_rung_trigger: "associativity of a declared operation is expressible and checkable -- SUFFICIENT FOR n-ary application of a binary operation declared associative to fold to nested binary application, which is what gunbc.rung_drop concat_binary_signature_exempt_from_arg_binding waits on. Magma<T> is { op: fn(T, T) -> T } and Semigroup<T> is { op: fn(T, T) -> T }: structurally identical, differing by a blank line where the law would sit, so the type whose ENTIRE content is the associativity law carries no law. This is a DESIGN section 5 wall-after-grounding rather than a ratchet -- associativity of a DECLARED operation is a modeled fact, not an undecidable property of an arbitrary function."
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
module gunbc.guarantee_stall.authority_target_same_expression_equivalence_stall

import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, UncountedNotEnumerable }

// ONE EXPRESSION, TWO EVALUATORS -- AND WHY THIS IS A STALL RATHER THAN A DROP, which is the whole
// reason it is in this carrier. Nothing ever required this comparison, so no rung was lowered and
// there is no previous rung to restore; a `RungDrop` row would make the declared-drop ledger report
// a newly discovered gap as a regression, which is the rung inflation section 4b(1) forbids applied
// to the compiler's own self-description. It was drafted as a drop on gunbc#10154 and moved here
// (codex review 59064) rather than kept with a disclaimer, because a row denying the meaning of the
// carrier it sits in is a meaning fork, not a caveat.
//
// WHY IT IS NOT `gunbc.recurring_failure_mode` `realization_arms_diverge_on_whether_the_program_refuses`,
// stated with a specimen on each side because the question a reader actually has is which row owns a
// given specimen. The two subjects CROSS. IN THIS ROW AND NOT IN THAT ONE: .dag evaluates both
// operands of a conjunction and emitted Rust short-circuits, so where the right operand is total the
// two arms agree on every answer and differ only in WHAT RAN -- no refusal fires, so there is no
// refusal divergence for that row to see and every result-comparison oracle is green through it. IN
// THAT ROW AND NOT IN THIS ONE: a divergence between two realization arms NEITHER of which is the
// authority, which is not an authority-versus-target relation at all. Neither contains the other.
//
// THE CEILING IS 2 AND NOT HIGHER BECAUSE THIS ROW OWNS DETECTION, NOT CONSTRUCTION. Making the
// divergence unwritable -- evaluation order modeled as a property of a connective and consulted by
// both realizations -- is that failure-mode row's trigger. This row is the executed check over
// whatever construction does not yet cover, which is the order section 5 states, so the two coexist.
//
// THE POPULATION IS HONESTLY UNCOUNTABLE AND A GREP UNDERSTATES IT BY CONSTRUCTION: the interpreter
// is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the
// refusal while authoring and rewrote it. The surviving matches are the cases that do NOT carry the
// consequence, so a low count is not evidence the class is small.
data authority_target_same_expression_equivalence_stall: GuaranteeStall = GuaranteeStall {
subject: "one expression evaluated by the .dag authority and by the emitted target is never compared by execution, so the two may agree on the returned value and differ on which subexpressions ran",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: UncountedNotEnumerable { reason: "the affected population is every expression whose two realizations could diverge, and it is survivorship-filtered: the interpreter is the stricter arm, so sites where the divergence carried a consequence were rewritten while authoring and only the harmless matches survive to be grepped" },
next_rung_trigger: "a lane that runs ONE expression through BOTH realizations and refuses a divergence, sufficient for an emission differing from its authority in value OR in what it evaluates being caught, demonstrated by a red on a fixture where the two agree on the returned value and differ on which subexpressions ran; the fixture is already executed and dated on gunbc#10139, so what is owed is enrolment and not a harness, and enrolling behavioral_differential discharges the seed-Rust versus emitted-Rust axis ONLY and does not touch this row"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module gunbc.guarantee_stall.builtin_parameter_name_forked_across_hand_authored_sites_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data builtin_parameter_name_forked_across_hand_authored_sites_stall: GuaranteeStall = GuaranteeStall {
subject: "a builtin parameter's name is authored independently in two more places than its declaration",
current: OutsideTheLadder,
ceiling: StructurallyImpossible,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "src/v1/stage0/src/v1_interpreter.rs expect_int/expect_value_str diagnostic literals (\"substring start\", \"substring end\", \"char_at pos\")", tail: Cons { head: "src/v1/runtime_rust.dag emitted Rust signatures for 47 of the 132 registry builtins", tail: Empty } } },
next_rung_trigger: "a builtin parameter's name is DERIVED from the declared BuiltinParam at both sites -- the interpreter's diagnostic text and the emitted runtime's signature -- rather than authored as a literal in either. ONE trigger, not two: the capability is identical for both sites and splitting it would let each look closable while the capability that closes them stayed dead."
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module gunbc.guarantee_stall.deployed_repository_empty_root_bootstrap_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

// THIS IS A PRE-EXISTING CAPABILITY GAP, NOT A RUNG LOWERED BY THE CUT-OVER. The legacy transport
// did put HEAD/objects/refs beside working bytes in an empty directory, but omitted the index and
// therefore could not produce the consistent repository state this deployment claims. Calling that
// a bootstrap would count mutation as success and repeat the exact conflation RLM-2c removes.
// Git-native convergence now refuses the unobservable pre-state through
// ConvergencePreStateUnobservable, and placement carries that located cause to the outer deploy in
// its durable receipt. The refusal is evidence of the gap; it is not the missing capability.
// THE POPULATION IS ONE PRODUCTION SUBJECT, NOT A SNAPSHOT OF AN OPEN SET. There is one production
// constructor, deployment_spec_srv1, and the realization binding is global rather than a field a
// future spec can silently choose. Any later production spec therefore inherits GitNativeConvergence;
// at a fresh root it reaches the same typed ConvergencePreStateUnobservable wall and cannot proceed.
// The boundary is the refusal construction, not a hand-maintained roster count.
data deployed_repository_empty_root_bootstrap_stall: GuaranteeStall = GuaranteeStall {
subject: "an empty deployed repository root cannot be brought to one consistent candidate revision by live deploy",
current: OutsideTheLadder,
ceiling: StructurallyGuaranteed,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "gunbc.live_deploy.spec deployment_spec_srv1 at a fresh repository root", tail: Empty {} } },
next_rung_trigger: "a modeled Git-native bootstrap sufficient to initialize an empty deployed repository from the admitted runner checkout at the exact candidate, with HEAD, index and tracked worktree read back as that one revision before any later deployment member runs; copying any .git path as files, relaxing ConvergencePreStateUnobservable, or merely creating an empty git directory does not satisfy the capability"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module gunbc.guarantee_stall.doc_graph_dangling_link_population_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data doc_graph_dangling_link_population_stall: GuaranteeStall = GuaranteeStall {
subject: "the derived documentation graph contains dangling links",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } },
next_rung_trigger: "the derived dangling-link identity population is empty and every enrolled projection reports NowPassing"
}
14 changes: 14 additions & 0 deletions dag/gunbc/guarantee_stall/doc_graph_orphan_population_stall.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module gunbc.guarantee_stall.doc_graph_orphan_population_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data doc_graph_orphan_population_stall: GuaranteeStall = GuaranteeStall {
subject: "the derived documentation graph contains orphan documents",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } },
next_rung_trigger: "the derived orphan-document identity population is empty and every enrolled projection reports NowPassing"
}
14 changes: 14 additions & 0 deletions dag/gunbc/guarantee_stall/enforcement_live_closure_gate_stall.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module gunbc.guarantee_stall.enforcement_live_closure_gate_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data enforcement_live_closure_gate_stall: GuaranteeStall = GuaranteeStall {
subject: "the live enforcement closure and its question-zero gate are non-green",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_closure_question_zero_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_module_gate_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.question_zero_verdict_live_holds", tail: Empty {} } } } },
next_rung_trigger: "the live closure question returns zero and both gate projections report true"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module gunbc.guarantee_stall.external_model_scope_live_cover_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data external_model_scope_live_cover_stall: GuaranteeStall = GuaranteeStall {
subject: "the live external-model scope cover does not cover the extdeps tree",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "test.claim.external_model_scope_live_cover_witness.frontier_cover_of_live_extdeps_tree_holds", tail: Empty {} } },
next_rung_trigger: "node://adhoc-89fcf94a-bdd lands: the live extdeps-tree cover is exact and its routed witness returns true"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module gunbc.guarantee_stall.generated_artifact_registry_membership_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { MechanicallyPreventable, StructurallyGuaranteed }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

// THE GENERATED-ARTIFACT REGISTRY IS GUARDED INDIRECTLY, AND THIS ROW EXISTS BECAUSE THE MUTATION
// WAS RUN RATHER THAN REASONED ABOUT. Deleting a member from generated_artifact_registry and
// running the gate produced EXACTLY ONE finding, and it was `.gitattributes` drift -- the
// merge-driver enrollment projection enumerates registry members, so dropping one changes its
// bytes. Nothing said what an author would actually want said: that a COMMITTED file at a
// generated location is now adjudicated by nobody. The wall is real and it is one step removed
// from its subject, so an artifact excluded from the .gitattributes projection for any reason
// would leave the registry silently. Current rung is the honest one for a guard that holds by
// side effect; the trigger names the direct capability, a census joining committed files at
// generated-artifact locations back to registry membership, because a guard that answers about
// enrollment bytes is not the guard that answers about orphaned artifacts.
data generated_artifact_registry_membership_stall: GuaranteeStall = GuaranteeStall {
subject: "a committed generated artifact leaves generated_artifact_registry and stops being adjudicated",
current: MechanicallyPreventable,
ceiling: StructurallyGuaranteed,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "gunbc.generated_artifact generated_artifact_registry", tail: Cons { head: "gunbc.generated_artifact_merge_driver", tail: Empty {} } } },
next_rung_trigger: "a census that enumerates committed files at every artifact_location and refuses one with no generated_artifact_registry member, so registry departure is refused by its own subject rather than by .gitattributes drift"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
module gunbc.guarantee_stall.gitattributes_committed_emit_drift_stall

import v2.std.algebra { Cons, Empty }
import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

// REQUIRED-FLOOR RUN 32942047138 first executed this ReadsLiveTree carrier after #9284 landed.
// The direct byte-equality witness and its aggregate both returned false: one underlying fact,
// namely that the committed .gitattributes no longer equals its emitting authority. This is real
// generated-artifact drift, not a stale expectation. The floor cut's generated-artifact drift
// gates are currently absent, so nothing refused the authority/artifact disagreement when it was
// introduced; this bounded row keeps the two projections attached to the one repair obligation.
data gitattributes_committed_emit_drift_stall: GuaranteeStall = GuaranteeStall {
subject: "the committed .gitattributes differs from the bytes derived by its emitting authority",
current: OutsideTheLadder,
ceiling: MechanicallyPreventable,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation { members: Cons { head: "test.claim.gitattributes_emit_witness.witness_committed_matches_emit_holds", tail: Cons { head: "test.claim.gitattributes_emit_witness.witness_holds", tail: Empty {} } } },
next_rung_trigger: "node://adhoc-16f7520a-85f lands: identify the authority edit that introduced the drift, regenerate .gitattributes from that authority, and restore a required generated-artifact drift gate so later authority/artifact disagreement refuses"
}
21 changes: 21 additions & 0 deletions dag/gunbc/guarantee_stall/heterogeneous_child_list_stall.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
module gunbc.guarantee_stall.heterogeneous_child_list_stall

import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible }
import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation }

data heterogeneous_child_list_stall: GuaranteeStall = GuaranteeStall {
subject: "a type's child list may hold BOTH a type node and a field node, and v1.04_types child_type_node tells them apart by whether `inferred` is populated -- a stamp v1.02_parse field_to_child_node writes at PARSE TIME as Resolved, before any resolution has run. A child list that mixes the two kinds makes that accessor return the FIELD node where its caller expects the TYPE, with no diagnostic",
current: OutsideTheLadder,
ceiling: StructurallyImpossible,
blocker: ClimbableButUnbuilt,
population: BoundedPopulation {
members: [
"v1.02_parse variant_to_child_node",
"v1.02_parse outputs_to_inferred",
"v1.02_parse parse_type_after_kw",
"v1.02_parse parse_type_body_from_prefix",
"v1.02_parse parse_type_expr"
]
},
next_rung_trigger: "v1.04_types child_type_node no longer INFERS SHAPE FROM PROVENANCE -- it discriminates a type child from a field child by something that states the kind, rather than by whether a derived-data slot happens to be occupied. The trigger is that CAPABILITY and not any artifact that would contribute to one: a tag added while the accessor still reads `inferred`-presence satisfies an artifact and leaves the hazard exactly where it is, which is the direction DESIGN section 4b(3) says this machinery structurally cannot see. Emptying the slot BEFORE that lands is the failure this row exists to prevent, not the repair -- it would silently reclassify every field child into the wrong arm at once"
}
Loading
Loading