Skip to content
Closed
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
6 changes: 3 additions & 3 deletions dag/gunbc/floor/floor_cost_debt_edit_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@ import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the changed-cost-debt-witness ceiling the required floor applies at
// claim build (operator ruling, 2026-09-19). The modeled authority is
// v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceiling_at_base; the declaration below
// v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceilings_at_base; the declaration below
// is its seed-side reader at the claim-build boundary, not a second policy.
data floor_cost_debt_edit_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.cli_run.required_floor_runner", decl_name: "cost_debt_changed_witness_ceiling", field: WholeDeclaration }
],
reason: "WHY RUST IS STILL NEEDED: the required floor builds its claims in the seed, and the eval-step budget of a claim is fixed when v1_compiler.cli_run.required_floor_runner run_required_floor constructs it. The .dag decides everything about a changed cost-debt witness -- it shows the base declaration, tokenizes base and head, decides pure conjunct removal, selects the tier, derives the budget and names the edit's label. The seed item does the two reads the fold cannot perform from that loop: it hands over the head file's bytes and the comparison base the floor already resolved, then decodes the returned record (label, removed_conjuncts, budget) into the claim. It adds no policy: no tier choice, no label wording and no budget figure lives in it.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program. The required floor guards that program, and this change implements an operator ruling on its cost rule. It adds no language behavior, compatibility route, seed feature or emitted surface, and no flag: the tier is decided from the witness's tokens, never from anything an author writes.\n\nHAND-ITEM DELTA: +1, the reader above. The budget branch it feeds sits inside run_required_floor, which already existed.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete the seed declaration when the self-emitted claim executor builds the required floor's claim roster and selects each claim's eval-step budget by calling v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceiling_at_base (and v2.workflow.required_floor claim_eval_step_budget_for_identity) directly, so no hand-written reader decodes the ceiling record. NOT retired by the cost-debt roster reaching zero: an empty roster still needs its changed rows judged by this rule when one is touched.",
current_boundary: "v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceiling_at_base -> v1_compiler.cli_run.required_floor_runner cost_debt_changed_witness_ceiling -> v1_compiler.cli_run.required_floor_runner run_required_floor -> v1_compiler.cli_run.required_floor_runner RequiredFloorClaim"
trigger: "Delete the seed declaration when the self-emitted claim executor builds the required floor's claim roster and selects each claim's eval-step budget by calling v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceilings_at_base (and v2.workflow.required_floor claim_eval_step_budget_for_identity) directly, so no hand-written reader decodes the ceiling record. NOT retired by the cost-debt roster reaching zero: an empty roster still needs its changed rows judged by this rule when one is touched.",
current_boundary: "v2.workflow.floor_cost_debt_edit cost_debt_changed_witness_ceilings_at_base -> v1_compiler.cli_run.required_floor_runner cost_debt_changed_witness_ceilings -> v1_compiler.cli_run.required_floor_runner run_required_floor -> v1_compiler.cli_run.required_floor_runner RequiredFloorClaim"
}
187 changes: 136 additions & 51 deletions src/v1/stage0/src/cli_run/required_floor_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -809,20 +809,21 @@ pub(crate) fn floor_git_diff_name_status_range() -> Result<(Vec<String>, HashSet
}
}

/// The ceiling a CHANGED cost-debt witness is judged against, read from
/// `v2.workflow.floor_cost_debt_edit` `cost_debt_changed_witness_ceiling_at_base` (operator ruling,
/// 2026-09-19). The `.dag` shows the base, tokenizes both declarations, decides whether the edit
/// The ceilings the CHANGED cost-debt witnesses of ONE FILE are judged against, read from
/// `v2.workflow.floor_cost_debt_edit` `cost_debt_changed_witness_ceilings_at_base` (operator ruling,
/// 2026-09-19; one call per file, operator ruling 2026-10-01). The `.dag` shows the base, lexes the
/// base and head files once each, selects every function's declaration from those two streams, decides whether each edit
/// is a pure conjunct removal and selects the tier and its budget. THE HOST'S SHARE ENDS AT TWO
/// READS the fold cannot perform from here: the head file's bytes, and which comparison base the
/// floor already resolved -- plus the floor's own discovered test-fn identities, which the model
/// resolves a removed call against. Returns the model's edit label (for the receipt) and the budget in steps.
pub(crate) fn cost_debt_changed_witness_ceiling(
pub(crate) fn cost_debt_changed_witness_ceilings(
base: &str,
rel_path: &str,
function: &str,
functions: &[String],
head_source: &str,
test_fn_identities: &[String],
) -> Result<(String, u64), String> {
) -> Result<Vec<(String, u64)>, String> {
use v1_interpreter::Value;
let roots = default_source_roots();
let entry = "src/v2/workflow/floor_cost_debt_edit.dag";
Expand All @@ -832,7 +833,10 @@ pub(crate) fn cost_debt_changed_witness_ceiling(
let args = [
(Some("base".to_string()), str_value(base)),
(Some("path".to_string()), str_value(rel_path)),
(Some("function".to_string()), str_value(function)),
(
Some("functions".to_string()),
list_value_from_vec(functions.iter().map(str_value).collect()),
),
(Some("head_source".to_string()), str_value(head_source)),
(
Some("test_fn_identities".to_string()),
Expand All @@ -841,35 +845,65 @@ pub(crate) fn cost_debt_changed_witness_ceiling(
];
let result = v1_interpreter::run_in_context_with_args(
&ctx,
"cost_debt_changed_witness_ceiling_at_base",
"cost_debt_changed_witness_ceilings_at_base",
&args,
false,
)
.map_err(|e| format!("cost_debt_changed_witness_ceiling_at_base: {e}"))?;
let Value::Record { fields, .. } = &result else {
.map_err(|e| format!("cost_debt_changed_witness_ceilings_at_base: {e}"))?;
let rows = match &result {
Value::List(items) => items.iter().cloned().collect::<Vec<_>>(),
other => {
return Err(format!(
"cost_debt_changed_witness_ceilings_at_base returned `{}`, expected a List of \
CostDebtChangedWitnessCeiling",
ctx.format_value(other)
))
}
};
if rows.len() != functions.len() {
return Err(format!(
"cost_debt_changed_witness_ceiling_at_base returned `{}`, expected \
CostDebtChangedWitnessCeiling",
ctx.format_value(&result)
"cost_debt_changed_witness_ceilings_at_base returned {} ceiling(s) for {} function(s); \
the result is aligned with its input or it is not a decision",
rows.len(),
functions.len()
));
};
// THE LABEL IS THE MODEL'S (`cost_debt_edit_label`); the host prints it and mints no wording.
let edit = match ctx.field(fields, "label") {
Some(Value::Str(label)) => label.to_string(),
_ => return Err("CostDebtChangedWitnessCeiling carries no `label` String".to_string()),
};
let budget = match ctx.field(fields, "budget") {
Some(Value::Record {
fields: measure, ..
}) => match ctx.field(measure, "count") {
Some(Value::Int(n)) if *n > 0 => *n as u64,
_ => {
return Err("CostDebtChangedWitnessCeiling.budget has no positive count".to_string())
}
},
_ => return Err("CostDebtChangedWitnessCeiling carries no budget Measure".to_string()),
};
Ok((edit, budget))
}
rows.iter()
.map(|row| {
let Value::Record { fields, .. } = row else {
return Err(format!(
"ceiling row `{}` is not a CostDebtChangedWitnessCeiling",
ctx.format_value(row)
));
};
// THE LABEL IS THE MODEL'S (`cost_debt_edit_label`); the host prints it and mints no wording.
let edit = match ctx.field(fields, "label") {
Some(Value::Str(label)) => label.to_string(),
_ => {
return Err(
"CostDebtChangedWitnessCeiling carries no `label` String".to_string()
)
}
};
let budget = match ctx.field(fields, "budget") {
Some(Value::Record {
fields: measure, ..
}) => match ctx.field(measure, "count") {
Some(Value::Int(n)) if *n > 0 => *n as u64,
_ => {
return Err("CostDebtChangedWitnessCeiling.budget has no positive count"
.to_string())
}
},
_ => {
return Err(
"CostDebtChangedWitnessCeiling carries no budget Measure".to_string()
)
}
};
Ok((edit, budget))
})
.collect()
}

/// Names of `test fn` / `test data` declarations at the resolved diff base, per path.
Expand Down Expand Up @@ -8718,6 +8752,10 @@ pub fn run_required_floor(
} else {
Vec::new()
};
// The control for the one-judgment-per-file rule: judgments (each lexing base and head once)
// must equal changed files, not changed identities.
let mut cost_debt_edit_files_judged = 0usize;
let mut cost_debt_edit_identities_judged = 0usize;
for file in files {
let matched_prefix = long_home_prefixes
.iter()
Expand All @@ -8731,6 +8769,57 @@ pub fn run_required_floor(
let inside_required_gate = required_gate_admits(&file.module_path);
let path_is_long = is_long_home_path(&file.path);
let storage_agreement = long_home_storage_agreement(path_is_long, long_home);
// ONE JUDGMENT PER CHANGED FILE (operator ruling 2026-10-01). The edit judgment lexes the
// base and head files; called once per identity it lexed each file once per changed
// cost-debt witness in it, and on a 125 KB witness file two such witnesses held site
// projection past the 90-minute cap (run 36856989404). Every changed cost-debt witness of
// this file that reaches the budget arm below is judged in one call, against two lexes.
let file_cost_debt_functions: Vec<String> =
if prepared_module_paths.contains(&file.module_path) {
file.functions
.iter()
.filter(|function| {
let identity = format!("{}.{}", file.module_path, function);
changed_witness_set.contains(&identity)
&& cost_debt_roster.contains(&identity)
&& !corpus_census.contains_key(&identity)
&& !grandfathered_roster.contains(&identity)
})
.cloned()
.collect()
} else {
Vec::new()
};
let file_cost_debt_ceilings: HashMap<String, (String, u64)> = if file_cost_debt_functions
.is_empty()
{
HashMap::new()
} else {
let base = floor_diff_comparison_readout()?.base().to_string();
let rel_path = normalize_repo_path(&workspace_relative_repo_path(&file.path));
let head_source = std::fs::read_to_string(&file.path)
.map_err(|e| format!("changed cost-debt witness file {}: read: {e}", file.path))?;
let ceilings = cost_debt_changed_witness_ceilings(
&base,
&rel_path,
&file_cost_debt_functions,
&head_source,
&discovered_test_fn_identities,
)
.map_err(|e| {
format!(
"REQUIRED-FLOOR REFUSAL cause=CostDebtEditUnobserved file={} — {e}",
file.path
)
})?;
cost_debt_edit_files_judged += 1;
cost_debt_edit_identities_judged += file_cost_debt_functions.len();
file_cost_debt_functions
.iter()
.cloned()
.zip(ceilings)
.collect()
};
for function in &file.functions {
let identity = format!("{}.{}", file.module_path, function);
// ONE SITE PER QUALIFIED IDENTITY, REFUSED OVER THE WHOLE OFFERED POPULATION.
Expand Down Expand Up @@ -8861,26 +8950,17 @@ pub fn run_required_floor(
grandfathered_eval_step_budget
} else if cost_debt_roster.contains(&identity) {
let base = floor_diff_comparison_readout()?.base().to_string();
let rel_path = normalize_repo_path(&workspace_relative_repo_path(&file.path));
let head_source = std::fs::read_to_string(&file.path).map_err(|e| {
format!(
"changed cost-debt witness {identity}: read {}: {e}",
file.path
)
})?;
let (edit, budget) = cost_debt_changed_witness_ceiling(
&base,
&rel_path,
function,
&head_source,
&discovered_test_fn_identities,
)
.map_err(|e| {
format!(
"REQUIRED-FLOOR REFUSAL cause=CostDebtEditUnobserved \
identity={identity} — {e}"
)
})?;
let (edit, budget) = file_cost_debt_ceilings
.get(function)
.cloned()
.ok_or_else(|| {
format!(
"REQUIRED-FLOOR REFUSAL cause=CostDebtEditUnobserved \
identity={identity} — the per-file judgment of {} did not \
cover this changed cost-debt witness",
file.path
)
})?;
eprintln!(
"[floor-cost-debt-edit] identity={identity} base={base} edit={edit} \
eval_step_budget={budget}"
Expand Down Expand Up @@ -9183,6 +9263,11 @@ pub fn run_required_floor(
RequiredFloorDisposition::DeclinedDiscoveryExcluded { .. }
)
});
eprintln!(
"[floor-cost-debt-edit] judgments={cost_debt_edit_files_judged} \
changed_identities={cost_debt_edit_identities_judged} -- one judgment (two lexes) per \
changed file, never per identity"
);
eprintln!(
"[floor-phase] phase=site-projection state=completed wall_ms={} declared={} sites={} \
files={} claims={} declined_long={} declined_fixture={} declined_outside_gate={} \
Expand Down
42 changes: 42 additions & 0 deletions src/v2/test/floor_cost_debt_edit_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import v2.workflow.floor_cost_debt_edit {
cost_debt_edit_cause_label,
CostDebtChangedWitnessCeiling,
cost_debt_edit_from_sources,
cost_debt_edits_from_sources,
cost_debt_changed_witness_ceiling,
}
import v2.workflow.required_floor {
Expand All @@ -15,6 +16,7 @@ import v2.workflow.required_floor {
ClaimEvalStepStanding, EvalStepsWithinBudget, EvalStepsOverBudget, EvalStepsOverBudgetUnderDeclaredDrop,
claim_eval_step_standing,
}
import v2.std.algebra { list_head, HeadFound, HeadAbsent, list_tail, TailFound, TailAbsent, length }
import v2.std.logic { Bool }
import v2.std.integer { Int }
import v2.std.text { String }
Expand Down Expand Up @@ -222,3 +224,43 @@ test fn cost_debt_edit_witness_absent_at_base_is_rejudged() -> Bool {
let edit = decide(base: src_other_witness_only(), head: src_one_conjunct(), function: "w")
edit_rejudged_for(edit: edit, cause: WitnessNotDeclaredAtBase {}) && rejudged_and_refused(edit: edit)
}

// ONE LEX PAIR, MANY FUNCTIONS, ANSWERS ALIGNED (operator ruling 2026-10-01). The floor judges every
// changed cost-debt witness of a file in one call so the file is lexed twice in all, not twice per
// witness; the per-file form must still answer each function as its own decision, in input order.
// Three functions, three different arms: a pure removal, a rejudged edit, and a name absent at base.
fn src_two_witnesses_base() -> String { src(body: "test fn w() -> Bool { a() && t() } test fn v() -> Bool { a(x: 1) }") }
fn src_two_witnesses_head() -> String { src(body: "test fn w() -> Bool { a() } test fn v() -> Bool { a(x: 2) }") }

test fn one_lex_pair_judges_each_function_of_the_file_in_order() -> Bool {
let edits = cost_debt_edits_from_sources(
base_source: src_two_witnesses_base(),
head_source: src_two_witnesses_head(),
functions: ["w", "v", "z"],
test_fn_identities: fixture_test_fns()
)
match list_head(xs: edits) {
HeadAbsent => false
HeadFound { value: first } =>
edit_is_pure_removal_of(edit: first, expected: 1)
&& match list_tail(xs: edits) {
TailAbsent => false
TailFound { tail: rest } =>
match list_head(xs: rest) {
HeadAbsent => false
HeadFound { value: second } =>
edit_rejudged_for(edit: second, cause: EditIsNotAConjunctRemoval {})
&& match list_tail(xs: rest) {
TailAbsent => false
TailFound { tail: last } =>
match list_head(xs: last) {
HeadAbsent => false
HeadFound { value: third } =>
edit_rejudged_for(edit: third, cause: WitnessNotDeclaredAtBase {})
&& length(last) == 1
}
}
}
}
}
}
Loading