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
28 changes: 28 additions & 0 deletions dag/gunbc/commit_workflow.dag
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,30 @@ data commit_gate_roster: List<CommitCheckEnrollment> = [
check: CommitSpecGate { gate: SelfHostStalenessGate },
surfaces: [GithubActionsCiRegenJob]
},
CommitCheckEnrollment {
check: CommitWitnessClaim {
entry: "dag/test/claim/commit_witness_claim_roster_witness_test.dag",
check_fns: [
"commit_witness_claim_roster_red_control_holds"
],
kind: CorpusWitnessKind,
span: SpanUndeclared
},
surfaces: [GithubActionsCiJob]
},
CommitCheckEnrollment {
check: CommitWitnessClaim {
entry: "src/v2/lens/non_fold_residue_test.dag",
check_fns: [
"non_fold_residue_no_unrostered_or_stale",
"non_fold_residue_synthetic_unrostered_red_holds",
"non_fold_residue_wildcard_red_fixture_holds"
],
kind: CorpusWitnessKind,
span: SpanUndeclared
},
surfaces: [GithubActionsCiJob]
},
CommitCheckEnrollment {
check: CommitWitnessClaim {
entry: "dag/test/claim/github_merge_state_witness_test.dag",
Expand Down Expand Up @@ -703,6 +727,10 @@ data commit_workflow_ci_floor_gates: List<Gate> = project_ci_floor_gates(roster:

data commit_workflow_local_tidy_checks: List<LocalTidyCheck> = project_local_tidy_checks(roster: commit_gate_roster)

fn ci_floor_commit_witness_claim_schedule() -> List<ScheduleWitnessEntry> {
project_ci_floor_witness_entries(roster: commit_gate_roster)
}

fn realization_artifact_path(surface: CommitWorkflowSurface) -> String {
match surface {
GithubActionsCiJob => artifact_path(a: CiYamlArtifact)
Expand Down
23 changes: 23 additions & 0 deletions dag/test/claim/commit_witness_claim_roster_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
module test.claim.commit_witness_claim_roster_witness

import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
import v2.std.logic { Bool }
import v2.std.text { String }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data synthetic_stale_entry: String = "dag/test/claim/synthetic_missing_roster_witness_test.dag"
data synthetic_stale_fn: String = "this_witness_function_does_not_exist"

data commit_witness_claim_roster_fast_lane_note: String = "PR-time roster detector fast lane (operator brief 2026-07-22, class 3): synthetic stale (entry, check_fn) RED proves the resolvability machinery fires — typed COMMIT_WITNESS_CLAIM_ROSTER_REFUSAL on live defects. Full-corpus roster resolvability receipt moved to dag/test/claim/long/commit_witness_claim_roster_witness_test.dag (~210s eval; exceeds 5s fast-lane budget). Detection-only: never auto-delete enrollments. Dissolve-on: enrollment derived from discovery (module-identity Phase-0 admission invariant)."

fn witness_commit_witness_claim_roster_red_holds() -> Bool {
!commit_witness_claim_pair_resolvable(
entry: synthetic_stale_entry,
function: synthetic_stale_fn
)
}

test fn commit_witness_claim_roster_red_control_holds() -> Bool {
witness_commit_witness_claim_roster_red_holds()
}
20 changes: 20 additions & 0 deletions dag/test/claim/long/commit_witness_claim_roster_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
module test.claim.long.commit_witness_claim_roster_witness

import v2.workflow.commit_witness_claim_roster {
commit_witness_claim_roster_live_unresolvable_count
}
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
import v2.std.logic { Bool }
import v2.std.text { String }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data commit_witness_claim_roster_long_note: String = "Full CommitWitnessClaim roster resolvability receipt exceeds the per-PR 5s fast-lane eval budget (gunbc_ci_fast_lane_rule_note; measured ~210s eval on 2026-07-23). Projects via ci_floor_commit_witness_claim_schedule and resolves every enrolled (entry, check_fn) pair — the #7060 stale-roster class. Fast-lane per-PR coverage: dag/test/claim/commit_witness_claim_roster_witness_test.dag synthetic stale-pair RED only. Excluded from discovery at test/claim/long/ dir grain (gunbc.ci_layer_roots). NOT roster-enrolled on GithubActionsCiJob — dissolve-on: long-lane scheduled falsifier follow-on enrolls this row. Local recipe until then: claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/long/commit_witness_claim_roster_witness_test.dag --function commit_witness_claim_roster_holds."

fn witness_commit_witness_claim_roster_live_holds() -> Bool {
commit_witness_claim_roster_live_unresolvable_count() == 0
}

test fn commit_witness_claim_roster_holds() -> Bool {
witness_commit_witness_claim_roster_live_holds()
}
6 changes: 6 additions & 0 deletions src/v1/04_method.dag
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,12 @@ fn builtin_function_registry() -> Map<String, Node> {
let m = map_insert(m, "non_fold_residue_unrostered_count", int_type)
let m = map_insert(m, "non_fold_residue_stale_roster_count", int_type)
let m = map_insert(m, "non_fold_residue_coproduct_universe_count", int_type)
let m = map_insert(m, "commit_witness_claim_roster_unresolvable_count", int_type)
let m = map_insert(m, "commit_witness_claim_pair_resolvable", bool_type)
let m = map_insert(m, "non_fold_residue_wildcard_red_fixture_holds", bool_type)
let m = map_insert(m, "non_fold_residue_total_fold_green_fixture_holds", bool_type)
let m = map_insert(m, "non_fold_residue_roster_red_fixture_holds", bool_type)
let m = map_insert(m, "non_fold_residue_synthetic_unrostered_red_holds", bool_type)
let m = map_insert(m, "complexity_linearity_syntactic_finding_count", int_type)
let m = map_insert(m, "complexity_linearity_wildcard_facts", list_of_type_variable(id: "complexity_linearity_wildcard_fact_elem"))
let m = map_insert(m, "complexity_linearity_syntactic_site_fired", bool_type)
Expand Down
230 changes: 230 additions & 0 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21508,6 +21508,236 @@ mod pool_heads_oracle_tests {
}
}

// ── CommitWitnessClaim roster resolvability (PR-time detector) ─────────────────────────────────
//
// Every explicit `CommitWitnessClaim` row on the GithubActionsCiJob surface must resolve its
// entry module and name every `check_fn` — the #7060 class (witness moved, roster row stale →
// `no main function found` on every main CI run until #7079). Host-fed; dissolve-on: the
// `.dag` authority evaluates `project_ci_floor_witness_entries` without this re-parse once
// fn-body reflection can read the roster at compile time.

const COMMIT_WORKFLOW_ENTRY: &str = "dag/gunbc/commit_workflow.dag";
const CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN: &str = "ci_floor_commit_witness_claim_schedule";

fn schedule_witness_pairs_from_value(
ctx: &v1_interpreter::InterpContext,
val: &v1_interpreter::Value,
) -> Result<Vec<(String, String)>, String> {
let v1_interpreter::Value::List(items) = val else {
return Err(format!(
"{CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN} did not return a List: {val:?}"
));
};
let mut pairs = Vec::new();
for item in items.iter() {
let v1_interpreter::Value::Record { fields, .. } = item else {
return Err(format!(
"{CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN} element is not a Record: {item:?}"
));
};
let entry = commit_witness_field_str(ctx, fields, "entry")?;
let function = commit_witness_field_str(ctx, fields, "function")?;
pairs.push((entry, function));
}
Ok(pairs)
}

fn commit_witness_field_str(
ctx: &v1_interpreter::InterpContext,
fields: &[(v1_interpreter::Symbol, v1_interpreter::Value)],
name: &str,
) -> Result<String, String> {
match ctx.field(fields, name) {
Some(v1_interpreter::Value::Str(s)) => Ok(s.clone()),
other => Err(format!("{name} not a String: {other:?}")),
}
}

fn ci_floor_commit_witness_claim_pairs() -> Result<Vec<(String, String)>, String> {
let roots = witness_layer_roots();
let index = build_multi_entry_index(&roots);
let (graph, source_indices) = resolve_entry_with_index(&index, COMMIT_WORKFLOW_ENTRY)?;
let ctx = make_eval_context(
&graph,
source_indices,
v1_interpreter::ExecutionMode::Hermetic,
);
let val = v1_interpreter::run_in_context(&ctx, CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN, true)
.map_err(|e| format!("{CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN}: {e}"))?;
schedule_witness_pairs_from_value(&ctx, &val)
}

pub fn commit_witness_claim_pair_resolvable(entry: &str, function: &str) -> bool {
let roots = witness_layer_roots();
let index = build_multi_entry_index(&roots);
let mut entry_cache = std::collections::HashMap::new();
matches!(
commit_witness_claim_pair_resolvability_with_index(
&index,
&roots,
entry,
function,
&mut entry_cache,
),
CommitWitnessClaimPairResolvability::Resolvable
)
}

#[derive(Debug, Clone, PartialEq, Eq)]
enum CommitWitnessClaimPairResolvability {
Resolvable,
EntryMissing { detail: String },
EntryResolveFailed { detail: String },
FunctionNotFound,
}

#[derive(Debug, Clone)]
enum RosterEntryRegistryCache {
EntryMissing { detail: String },
EntryResolveFailed { detail: String },
Functions(std::collections::HashSet<String>),
}

fn roster_entry_registry_cache(
index: &MultiEntryIndex,
roots: &[String],
entry: &str,
) -> RosterEntryRegistryCache {
let entry_path = match resolve_entry_file_under_roots(roots, entry) {
Ok(p) => p,
Err(detail) => {
return RosterEntryRegistryCache::EntryMissing { detail };
}
};
let (graph, source_indices) = match resolve_entry_with_index(index, &entry_path) {
Ok(r) => r,
Err(detail) => {
return RosterEntryRegistryCache::EntryResolveFailed { detail };
}
};
let ctx = make_eval_context(
&graph,
source_indices,
v1_interpreter::ExecutionMode::Hermetic,
);
RosterEntryRegistryCache::Functions(ctx.item_registry.keys().cloned().collect())
}

fn commit_witness_claim_pair_resolvability_with_index(
index: &MultiEntryIndex,
roots: &[String],
entry: &str,
function: &str,
entry_cache: &mut std::collections::HashMap<String, RosterEntryRegistryCache>,
) -> CommitWitnessClaimPairResolvability {
let cached = entry_cache
.entry(entry.to_string())
.or_insert_with(|| roster_entry_registry_cache(index, roots, entry));
match cached {
RosterEntryRegistryCache::EntryMissing { detail } => {
CommitWitnessClaimPairResolvability::EntryMissing {
detail: detail.clone(),
}
}
RosterEntryRegistryCache::EntryResolveFailed { detail } => {
CommitWitnessClaimPairResolvability::EntryResolveFailed {
detail: detail.clone(),
}
}
RosterEntryRegistryCache::Functions(names) => {
if names.contains(function) {
CommitWitnessClaimPairResolvability::Resolvable
} else {
CommitWitnessClaimPairResolvability::FunctionNotFound
}
}
}
}

pub fn commit_witness_claim_roster_defects() -> Vec<(String, String, String)> {
let Ok(pairs) = ci_floor_commit_witness_claim_pairs() else {
return vec![(
"dag/gunbc/commit_workflow.dag".to_string(),
CI_FLOOR_COMMIT_WITNESS_SCHEDULE_FN.to_string(),
"schedule_projection_failed".to_string(),
)];
};
let roots = witness_layer_roots();
let index = build_multi_entry_index(&roots);
let mut entry_cache = std::collections::HashMap::new();
let mut defects = Vec::new();
for (entry, function) in pairs {
let cause = match commit_witness_claim_pair_resolvability_with_index(
&index,
&roots,
&entry,
&function,
&mut entry_cache,
) {
CommitWitnessClaimPairResolvability::Resolvable => continue,
CommitWitnessClaimPairResolvability::EntryMissing { detail } => {
format!("entry_missing:{detail}")
}
CommitWitnessClaimPairResolvability::EntryResolveFailed { detail } => {
format!("entry_resolve_failed:{detail}")
}
CommitWitnessClaimPairResolvability::FunctionNotFound => {
"function_not_found".to_string()
}
};
defects.push((entry, function, cause));
}
defects
}

pub fn commit_witness_claim_roster_unresolvable_count() -> i64 {
let defects = commit_witness_claim_roster_defects();
for (entry, function, cause) in &defects {
eprintln!(
"COMMIT_WITNESS_CLAIM_ROSTER_REFUSAL count={} entry={entry} function={function} cause={cause}",
defects.len()
);
}
defects.len() as i64
}

pub fn commit_witness_claim_roster_holds() -> bool {
commit_witness_claim_roster_unresolvable_count() == 0
}

pub fn non_fold_residue_wildcard_red_fixture_holds() -> bool {
let fixture = vec![(
"m.dag".to_string(),
"module m\ntype Mode = A | B | C\nfn f(x: Mode) -> Bool {\n match x {\n A => true\n _ => false\n }\n}\n"
.to_string(),
)];
nfr_residue_sites(&fixture).contains(&"m.dag::f".to_string())
}

pub fn non_fold_residue_total_fold_green_fixture_holds() -> bool {
let fixture = vec![(
"m.dag".to_string(),
"module m\ntype Mode = A | B | C\nfn f(x: Mode) -> Bool {\n match x {\n A => true\n B => false\n C => false\n }\n}\n"
.to_string(),
)];
!nfr_residue_sites(&fixture).contains(&"m.dag::f".to_string())
}

pub fn non_fold_residue_roster_red_fixture_holds() -> bool {
!non_fold_residue_site_is_rostered("synthetic/unrostered_site.dag::would_fail")
}

pub fn non_fold_residue_synthetic_unrostered_red_holds() -> bool {
let fixture = vec![(
"synthetic_red_fixture.dag".to_string(),
"module synthetic_red_fixture\ntype Mode = A | B | C\nfn f(x: Mode) -> Bool {\n match x {\n A => true\n _ => false\n }\n}\n"
.to_string(),
)];
let sites = nfr_residue_sites(&fixture);
let site = "synthetic_red_fixture.dag::f";
sites.contains(&site.to_string()) && !non_fold_residue_site_is_rostered(site)
}

// ── Non-fold-residue census (DESIGN §6) ──────────────────────────────────────────────────────────
//
// Audits the corpus for `match` expressions whose scrutinee is a function parameter with a declared
Expand Down
30 changes: 30 additions & 0 deletions src/v1/stage0/src/v1_compiler_infer_method.rs
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,36 @@ pub fn builtin_function_registry() -> Rc<HashMap<String, Rc<Node>>> {
"non_fold_residue_coproduct_universe_count".to_string(),
int_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"commit_witness_claim_roster_unresolvable_count".to_string(),
int_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"commit_witness_claim_pair_resolvable".to_string(),
bool_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"non_fold_residue_wildcard_red_fixture_holds".to_string(),
bool_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"non_fold_residue_total_fold_green_fixture_holds".to_string(),
bool_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"non_fold_residue_roster_red_fixture_holds".to_string(),
bool_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"non_fold_residue_synthetic_unrostered_red_holds".to_string(),
bool_type(),
);
let m = v1_rt::rc_map_insert(
m.clone(),
"complexity_linearity_syntactic_finding_count".to_string(),
Expand Down
Loading
Loading