Skip to content
Closed
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
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module gunbc.recurring_failure_mode.production_actuation_unmodeled_beside_a_modeled_probe

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Refresh the analysis that calls this class unlanded

Landing this module makes existing repository documentation immediately false: docs/plans/microvm-launch-displacement-analysis.md:7 still says this exact class is “PROPOSED, NOT LANDED” and does not resolve, while dag/gunbc/doc_graph_roots.dag:1645 says to add the failure-mode row as the document's third bound work when it lands. Without updating both sites in this change, readers are told the new symbol is absent and changes to its carrier are omitted from the analysis document's dependency binding.

Useful? React with 👍 / 👎.


import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data production_actuation_unmodeled_beside_a_modeled_probe: RecurringFailureMode = RecurringFailureMode {
identity: "production_actuation_unmodeled_beside_a_modeled_probe" as NonEmptyStr,

receipts: [
"**PRODUCTION ACTUATION UNMODELED BESIDE A MODELED PROBE** (INVALID STATE: one effect -- what CAUSES a thing to happen -- has two homes. The install path and a probe of the effect are modeled as ArgvCommand and executed through the modeled transport, so the corpus reads as owning the effect; the path PRODUCTION actually takes is hand-authored outside .dag, and .dag carries RECEIPTS of it after the fact. Both homes are honest on their own. Together they answer one question twice, and the modeled half is the one a reader finds first. ",

"HARM, AND IT IS THE READING KIND RATHER THAN A RUNTIME ONE. A reviewer asking 'is this effect modeled' greps, finds modeled argv and a witness asserting its flags, and concludes yes. The production path is not covered by that witness and cannot be, because the witness ranges over the probe's construction. So every guarantee argued from the modeled half is argued about a route production does not take, and the gap is invisible precisely where the corpus looks strongest. It also compounds: each new model authored against the unconsumed home adds mass to the wrong side, and each receipt authored against the live one adds prose where a fold should be. ",

"SPECIMEN WITH A RECEIPT, gunbc micro-VM runners, 2026-09-08. Mt. Collins runs real GitHub Actions jobs in a per-job micro-VM (#10733, run 34108061111, runner-canary-8). What is modeled: runner_microvm_host_ready firecracker_fetch_commands and firecracker_install_commands, as ArgvCommand lists run through run_shell_commands with LocalExec -- so INSTALL is modeled; and runner_microvm_boot_probe_witness_test, which asserts --no-api and --config-file on a modeled launch argv -- so a boot PROBE launch is modeled. What is NOT modeled is the launch real jobs take: runner_bound_attempt_receipt execution_chain is a List<NonEmptyStr> of prose describing the jailer exec, and the actuation itself is host tooling outside the substrate. ",

"THE PRECISION MATTERS AND THE FIRST STATEMENT OF THIS FINDING FAILED IT. The finding was first reported as 'no argv_command starting firecracker anywhere', which is false and a reviewer would have found the two exceptions immediately, discrediting a real defect. The defensible form names the three states separately: install modeled, probe modeled, production actuation not. A finding that overstates its scope is refuted by its own counterexample and the underlying gap survives unaddressed. ",

"DISTINGUISHING FACTS, because three neighbours are close. It is not `unmodeled realization` alone -- raw shell implementing semantics expressible in .dag -- since here a modeled expression EXISTS and production simply does not route through it; the defect is the fork, not the absence. It is not `parallel_representation_debt` in the ordinary sense of two data shapes for one value, because these two homes differ in KIND: one is a fold that could execute, the other is prose recording that something executed. And it is not the receipt pattern being wrong -- observing a live effect is correct and necessary; what makes this a class is a modeled route sitting BESIDE the observed one while nothing joins them. ",

"RECOGNITION RULE, checkable before the model is authored: for an effect the corpus models, ask which route PRODUCTION takes and name it. If the answer is 'a different one', the model is not coverage of that effect no matter how thorough its witness -- and adding to the model widens the fork. The tell in a diff is a new modeled effect path landing with zero importers while a receipt module for the same effect already carries prose rows. ",

"RUNG FOUND AT: 1 (mitigatable) -- the fork is visible to a reader who asks the recognition question, and nothing structural prevents authoring the second home. CEILING: 3 (structurally guaranteed), because the property is decidable from the module graph: whether an effect declared in .dag has a production consumer at execution is exactly the reachability question the impact-query lens already answers over the Node tree. It is not 4, because the hand-authored route lives outside the substrate and its absence cannot be made unrepresentable by any construction inside it. ",

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Do not attribute execution reachability to the impact query

The cited v2.lens.module_impact_query does not answer whether a declaration has a production consumer “at execution”: its ImpactReading traverses module dependency edges and carries no production-root, test-versus-production, call-site, or executed-path classification. A test-only reference or an otherwise unexecuted importer is therefore reachable in that graph without being the consumer this class requires, so this sentence overstates the existing capability and makes the rung-3 ceiling rationale misleading; the missing production-consumer join named in the next receipt still needs to be treated as missing.

Useful? React with 👍 / 👎.


"COROLLARY ON DETECTING THE FORK'S NEAREST COUSIN, AN APPEND-ONLY CARRIER SILENTLY LOSING ROWS. For any append-only carrier that is still a LIST -- a roster, an admit_callers list -- THE MERGE CHECK IS A COUNT COMPARISON AGAINST THE BASE, NOT A READ OF THE DIFF. A branch that re-applies its own rows onto a moved base renders as REORDERING, which is exactly what a reviewer expects a rebased roster to look like, so a row another lane appended after the branch point disappears with no visual signal. The count raises the alarm and the identity join says which row; neither alone is sufficient, and the diff is blind to both. SURVIVING SPECIMEN: `extdeps.exec.command` `command.dag` at 67 rows on main against 68 on a branch that had added two -- `admit_callers` is still that list. SUPERSEDED FOR ONE CARRIER ONLY: the failure-mode roster at 163 against 173. gunbc#10822 (aac9545a53) deleted the hand-appended `gunbc.recurring_failure_mode.roster` list; membership is now the row DIRECTORY, and there is no list to count. Refreshing that citation as if the roster were still countable would be `a_live_authority_name_carries_a_superseded_claim`. Do not invent a replacement count for the dissolved roster; directory membership is a different subject. ",

"NEXT-RUNG TRIGGER, named as the capability rather than an artifact: A JOIN THAT, FOR EACH DECLARED EFFECT PATH, ANSWERS WHETHER A PRODUCTION CONSUMER REACHES IT AT EXECUTION, and refuses a modeled effect that has none while a receipt module for the same subject exists. It must be SUFFICIENT FOR the general case -- any effect, not a per-module allowlist -- and a census that merely counts unconsumed modules CONTRIBUTES to it without retiring it, because the load-bearing half is the join to the receipt subject, not the count.",
],

evidence: [],
}
Loading