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
21 changes: 21 additions & 0 deletions dag/gunbc/executor_schedule_retention.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
module gunbc.executor_schedule_retention

data schedule_retention_policy_note: String = "The v1 claim executor holds the WHOLE batch schedule before it runs a witness, so per-module retention is EXACT, not heuristic: each module's retained typed state (typed-module result, normalize/ownership diagnostic memos, parse-body entry in the process-shared MultiEntryIndex) is refcounted by the number of remaining scheduled entries whose closure reaches it, and dropped the moment that count hits zero. Derived from declared inputs (the schedule x the module-graph closure); no threshold, no recency heuristic, no GC. DESIGN grounding: S2 (drop dead weight is the master move), S4 (a heuristic is never necessary in a closed system - the schedule exists, so retention is computed not guessed), S5 (fail-closed). Authority: this carrier; the Rust realization in cli_run.rs mirrors each fact below and schedule_retention_policy_matches_modeled_authority reds on drift - the extdeps.realization.resolved_graph SizeBounded-cap lockstep pattern applied to a policy. Dissolution trigger: the cross-entry typed-module-memo ladder SpacePacked eviction (PR-beta), the same trigger floor_drain_retention_test.dag's Never/ScopeExit note carries."

data schedule_retention_tunable_count: Int = 0

data schedule_retention_tunable_count_note: String = "Zero by construction: the retention rule is the schedule's remaining demand, full stop - no threshold, no recency, no confidence dial. Mirrored by SCHEDULE_RETENTION_TUNABLE_COUNT in cli_run.rs; a nonzero here (a smuggled heuristic - S5's confidence-threshold tell) must move BOTH surfaces and face review."

data schedule_retention_grain_is_per_module: Bool = true

data schedule_retention_heads_stay_resident: Bool = true

data schedule_retention_heads_note: String = "Heads (the whole-pool parse snapshot and the bare/qualified census layers) are NOT per-module state and are never evicted - the #6848 bare-name census requires the whole-pool heads resident for the run's lifetime (heads-only parse #6956/#6972 precedent). Held by construction: only per-module cache keys are recorded for eviction."

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_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."
22 changes: 22 additions & 0 deletions dag/test/claim/executor_schedule_retention_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module test.claim.executor_schedule_retention

import gunbc.executor_schedule_retention {
schedule_retention_tunable_count,
schedule_retention_grain_is_per_module,
schedule_retention_heads_stay_resident,
schedule_retention_retain_on_unknown,
schedule_retention_underflow_refuses,
}

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."

test fn schedule_retention_exposes_no_tunables() -> Bool {
schedule_retention_tunable_count == 0
}

test fn schedule_retention_policy_is_fail_closed() -> Bool {
schedule_retention_grain_is_per_module
&& schedule_retention_heads_stay_resident
&& schedule_retention_retain_on_unknown
&& schedule_retention_underflow_refuses
}
3 changes: 2 additions & 1 deletion docs/probes/witness_entry_eligibility_census.tsv
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# witness_entry_eligibility_census stamp=2026-07-23T19:48Z grain=entry_closure roots=witness_layer_roots(test.dag with test fn/data)
# witness_entry_eligibility_census stamp=2026-07-24T00:55Z grain=entry_closure roots=witness_layer_roots(test.dag with test fn/data)
entry module_path subject_module subject_decl disposition retained_or_ineligible_reason first_error_class execution_leg
dag/test/claim/accelerator_demo_execution_witness_test.dag test.claim.accelerator_demo_execution_witness test.claim.accelerator_demo_execution_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/accelerator_demo_gpu_witness_test.dag test.claim.accelerator_demo_gpu_witness test.claim.accelerator_demo_gpu_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
Expand Down Expand Up @@ -99,6 +99,7 @@ dag/test/claim/emit_host_gate_verdicts_test.dag test.claim.emit_host_gate_verdic
dag/test/claim/emit_host_gate_witness_test.dag test.claim.emit_host_gate_witness test.claim.emit_host_gate_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/emit_host_typed_smoke_test.dag test.claim.emit_host_typed_smoke_test test.claim.emit_host_typed_smoke_test witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/exec_arg_limit_witness_test.dag test.claim.exec_arg_limit_witness test.claim.exec_arg_limit_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/executor_schedule_retention_test.dag test.claim.executor_schedule_retention test.claim.executor_schedule_retention witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/extdeps_anemia_grounding_witness_test.dag test.claim.extdeps_anemia_grounding_witness test.claim.extdeps_anemia_grounding_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/extdeps_dpkg_witness_test.dag test.claim.extdeps_dpkg_witness test.claim.extdeps_dpkg_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
dag/test/claim/extdeps_git_diff_name_status_witness_test.dag test.claim.extdeps_git_diff_name_status_witness test.claim.extdeps_git_diff_name_status_witness witness_entry InterpretedRetained BulkFlipPendingCensusIncomplete CensusPending InterpretedLeg
Expand Down
4 changes: 2 additions & 2 deletions docs/probes/witness_entry_eligibility_histogram.txt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# witness_entry_eligibility_histogram stamp=2026-07-23T19:48Z total_entries=880
# witness_entry_eligibility_histogram stamp=2026-07-24T00:55Z total_entries=881
disposition reason count
InterpretedRetained BulkFlipPendingCensusIncomplete 700
InterpretedRetained BulkFlipPendingCensusIncomplete 701
EmitIneligible OfflineLocalRecipe 82
EmitIneligible LongLaneScheduled 64
InterpretedRetained EmitOnDemandFamilyGrain 26
Expand Down
Loading
Loading