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
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ The recursion's payoff is that **language design itself opens up.** It is normal

## Recurring failure modes (instances of §3–§5, kept for pattern-matching)

hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · positional citation (a `file:line` pointer where a symbol was available — see §3).
hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · **empty-observation narrow** (the absorbing fallback's mirror: ⊥-as-answer conflated with ⊥-as-ignorance — an observation that could not express what changed rendered as the verdict "nothing is affected", so the run narrows to nothing instead of widening. Strictly worse than the widen §5 already forbids: a widen is merely expensive, a narrow is silently uncovered. Live specimen: a push whose baseline ref *is* the pushed ref diffs the commit against itself, and the witness floor reported the resulting zero-path observation as "N unaffected (import-closure, skipped without resolve)" — receipt, two main pushes reporting an identical `4118 unaffected` on different commits, a skip count that cannot be a function of the diff. The tell that one observation is wrong rather than three local choices reasonable: its consumers disagree — compile-clean widened to whole-tree, regen gated on the event name, the witness floor skipped) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · positional citation (a `file:line` pointer where a symbol was available — see §3).

## Open threads

Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/design_document.dag
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ fn section_7_blocks() -> List<MarkdownBlock> {
fn failure_modes_blocks() -> List<MarkdownBlock> {
[
h2(text: "Recurring failure modes (instances of §3–§5, kept for pattern-matching)"),
p(text: "hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · positional citation (a `file:line` pointer where a symbol was available — see §3)."),
p(text: "hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · **empty-observation narrow** (the absorbing fallback's mirror: ⊥-as-answer conflated with ⊥-as-ignorance — an observation that could not express what changed rendered as the verdict \"nothing is affected\", so the run narrows to nothing instead of widening. Strictly worse than the widen §5 already forbids: a widen is merely expensive, a narrow is silently uncovered. Live specimen: a push whose baseline ref *is* the pushed ref diffs the commit against itself, and the witness floor reported the resulting zero-path observation as \"N unaffected (import-closure, skipped without resolve)\" — receipt, two main pushes reporting an identical `4118 unaffected` on different commits, a skip count that cannot be a function of the diff. The tell that one observation is wrong rather than three local choices reasonable: its consumers disagree — compile-clean widened to whole-tree, regen gated on the event name, the witness floor skipped) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · positional citation (a `file:line` pointer where a symbol was available — see §3)."),
]
}

Expand Down
8 changes: 8 additions & 0 deletions dag/gunbc/executor_schedule_retention.dag
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,14 @@ data schedule_retention_retain_on_unknown: Bool = true

data schedule_retention_retain_on_unknown_note: String = "When reachability CANNOT be computed for a cached module (a provenance gap), the safe arm is RETAIN - correctness-fail-closed but memory-fail-open - so it is a typed, per-module, COUNTED RetentionUnknown row, never a silent retain-everything (that absorbing fallback is a T-as-ignorance widen whose frequency the corpus would never see, S5)."

data schedule_retention_release_and_eviction_counted_apart: Bool = true

data schedule_retention_release_vs_eviction_note: String = "A module is RELEASED when its retention refcount reaches zero; it is EVICTED only when that release actually dropped recorded cache state. The two are different facts and are counted apart (schedule_releases vs schedule_evictions, released_modules vs evicted_modules). They diverge on every run whose arming reaches modules the run never reconciles - the ordinary case, because arming spans the whole DISCOVERED roster while the affected set resolves a subset. Fusing them overstates the mechanism by that entire population: a live CI receipt read schedule_evictions=2200 against modules_refcounted=2200 and typed_cache_peak=883, i.e. it claimed to have evicted every module it had ever heard of, ~2.5x the modules that were ever cached, and a counter that equals the arm count by construction carries no information at all. Rust lockstep: SCHEDULE_RETENTION_RELEASE_AND_EVICTION_COUNTED_APART in cli_run.rs; discriminating RED: unreconciled_module_releases_without_evicting (an armed-but-never-reconciled module must release without evicting - re-fusing the counters reds it)."

data schedule_retention_entry_line_asserts_execution: Bool = false

data schedule_retention_entry_line_note: String = "The per-entry drain line witnesses ONE fact: the schedule moved PAST that entry, so its per-module state can no longer be read. It asserts nothing about selection or execution - index_arm_schedule_retention walks every DISCOVERED row before any predict-skip, so the line also appears for entries the affected set skipped without ever resolving them. It was formerly spelled entry='...', which two independent readers hours apart took as proof the entry had been scheduled and run, and that misreading cost hours of misdirected diagnosis on a real selection defect. It is now schedule_passed_entry='...' beside an ARMED-line legend, because a label that asserts a fact its mechanism cannot support is a defect of the same family as a wrong number (DESIGN section 5: a diagnostic must be typed and located, and locating it on the wrong subject is not locating it)."

data schedule_retention_underflow_refuses: Bool = true

data schedule_retention_underflow_note: String = "A decrement past zero (a scheduled entry demands state the refcount said was fully consumed) is a schedule-derivation defect and REFUSES, typed and located - the mechanism never serves a wrong verdict against evicted state. Content-key recompute-on-miss is the correctness license; the refusal is the loudness that keeps a derivation bug from hiding."
10 changes: 10 additions & 0 deletions dag/test/claim/executor_schedule_retention_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ import gunbc.executor_schedule_retention {
schedule_retention_heads_stay_resident,
schedule_retention_retain_on_unknown,
schedule_retention_underflow_refuses,
schedule_retention_release_and_eviction_counted_apart,
schedule_retention_entry_line_asserts_execution,
}

data witness_note: String = "In-corpus consumer of the schedule-derived retention policy carrier: asserts the modeled policy facts by execution (green-by-execution). The Rust realization in cli_run.rs mirrors these same facts and a Rust lockstep witness (schedule_retention_policy_matches_modeled_authority) pins the two together, so a policy edit that forgets either side reds."
Expand All @@ -14,6 +16,14 @@ test fn schedule_retention_exposes_no_tunables() -> Bool {
schedule_retention_tunable_count == 0
}

test fn schedule_retention_release_is_not_an_eviction() -> Bool {
schedule_retention_release_and_eviction_counted_apart
}

test fn schedule_retention_drain_line_claims_no_execution() -> Bool {
schedule_retention_entry_line_asserts_execution == false
}

test fn schedule_retention_policy_is_fail_closed() -> Bool {
schedule_retention_grain_is_per_module
&& schedule_retention_heads_stay_resident
Expand Down
Loading
Loading