Skip to content
Merged
30 changes: 30 additions & 0 deletions dag/gunbc/v1/v1_maintenance_standing.dag
Original file line number Diff line number Diff line change
Expand Up @@ -577,6 +577,36 @@ data v1_seed_standing: SeedLifecycleStanding = SemanticsFrozen { maintenance: Ma
// KEY CALLS THAT CAN NEVER HIT -- a step whose loop index differs each time -- is a demand-graph
// question under std.materialization_ladder that this change deliberately leaves open.

// THE LIST HALF OF THE SAME KEY DEFECT, ADMITTED ON ITS OWN ROW BECAUSE IT IS A SEPARATE CHANGE TO
// THE SEED (gunbc#12066). THE CHANGE: both `list_push` arms of the interpreter call
// eval_recompute_extend_push_hash, which, when the parent list's content hash is already alive in
// the eval-call memo's identity hash memo, records the pushed list's hash as mix(parent, item).
// No carrier, type or exported item changes; the new function is private to the interpreter.
//
// THE DEFECT, and why it is key derivation rather than admission. The list content hash is a left
// fold mix(h, child) from a fixed seed with no finalizer, so hash(push(xs, x)) == mix(hash(xs),
// hash(x)) exactly. A recursion threading a growing list_push accumulator handed every call a new
// Rc, missed the identity memo, and refolded the whole accumulator: one relation realized at
// per-call O(|xs|). The question the row above leaves open -- should the memo key calls that can
// never hit -- is answered NO CRITERION IS NEEDED: "can never recur" is undecidable, any proxy is a
// heuristic that fails silently in the cost direction (DESIGN section 5), and with the key at
// O(item) an unrecurrable call costs a bounded constant. Per-call RETENTION of stored arguments is
// the residual admission question and stays open; it needs a recurrence census, not a threshold.
//
// THE PURPOSE TEST is satisfied on the row above's argument: the interpreter is the engine the v2
// self-host program runs on, and a recursion threading a list accumulator is its ordinary shape; a
// cost-shape defect fixed under DESIGN section 6's bare-minimum-cost rule regardless of n.
// BehaviorPreservingRedundancyRemoval: every key VALUE is unchanged -- the recorded hash is the
// value the full fold computes -- and memo hits
// still verify arguments by equality, so a key can cost a lookup and never an answer.
// PUBLICSURFACEGROWTH: none; nothing exported is added.
//
// THE CONTROL, VALUE AND ROUTE: interpreter test push_hash_extension_tests
// pushed_list_hash_is_the_full_fold_and_is_demand_gated drives list_push through BOTH production
// arms (eval_builtin, eval_algebra_method_inner) and asserts the extended entry equals the full
// fold; deleting the extension call from either arm turns it red. Unlike the string half's key
// sites, this route is pinned.

data v1_maintenance_typecheck_progress_admission_note: String = "AN ADMISSION UNDER THE 2026-08-20 PURPOSE TEST, recorded in the same PR as the change it admits, because an admission written afterwards is indistinguishable from an author's own classification. THE RULING, verbatim and relayed through the requesting session's parent (snappy-dove-250, import/namespace manager) on 2026-08-25: 'ah yeah - we need to fix the typecheckmoduleresult issue'. There is no PR review or transcript to point at; the relay is the record and this row is the citation, stated plainly rather than dressed up as pointing at a document that does not exist -- the same shape as v1_maintenance_purpose_ruling_note above.\n\nTHE DEFECT, at the grain that makes it a defect rather than an improvement. v1.compiler.infer typecheck_module has an early return: when build_type_env yields error diagnostics it hands back a TypedModule whose items list is EMPTY and never reaches item analysis. The seed therefore renders two different facts as one value -- a module that COMPLETED item checking and legitimately has no items, and a module that was ABANDONED before item checking started. Every downstream reader of TypedModule.items receives the same empty list for both, so a consumer wanting the distinction must infer it from 'items is empty AND there are error diagnostics', and that inference is unreliable in the direction that matters: a module that completed and has item-level errors presents identically. This is the state-space conflation DESIGN names, in the seed, on a carrier read by the whole back end.\n\nWHY THE FIELD LANDS ON TypedModule AND NOT ON TypecheckModuleResult, since the ruling names the result type and the change does not edit it. realize_module destructures the result and inserts only .typed into the module index; a progress field on the result alone would be discarded one line after it was set, which is this same defect one level out. The result type is where the issue was NOTICED; the carrier that survives the destructure is where the fact has to live.\n\nTHE EXHIBITED COST, because a defect with no demonstrated victim is a preference. A demand oracle built in this lane to score resolution producers read TypedModule.items to derive per-module demand, and was found DEAD as a scoring instrument for exactly this reason: an abandoned module reports total_arm1=1, which is indistinguishable from a genuine single-ask module, so the instrument's error is ANTI-CORRELATED with the defect it was built to find -- the modules most likely to abandon are the ones whose demand it most understates. That oracle was discarded rather than repaired, which is the measured price of the conflation and is why this is not speculative hardening.\n\nWHY IT SERVES THE V2 SELF-HOST PROGRAM, which is the whole admission test. The v2 resolution work this lane exists to do reads seed-produced TypedModule values to measure and compare producers. An instrument that cannot tell 'not checked' from 'nothing to check' cannot score a producer, and the program's next steps (one closure authority, exact denotation) are measurement-gated. This repairs the seed's report of its own progress; it adds no language behavior, no compatibility obligation, no escape hatch, and completes no seed feature.\n\nTHE SCOPE LIMIT, stated because this row will be cited and its limit is the part most likely to be dropped in the citing. THE RULING ADMITS THIS CHANGE ONLY. It does NOT settle whether PublicSurfaceGrowth means a NEW EXPORTED DECLARATION or ANY CHANGE TO EXPORTED SURFACE -- this change adds a coproduct and a record field to a type the seed exports, so it sits squarely on that unresolved boundary and was ruled admissible without the boundary being drawn. Nobody may cite this row as the answer to that question. A later proposal that needs the boundary decided must route it for its own ruling; treating this admission as precedent for a general reading of PublicSurfaceGrowth would be the authority-substitution failure DESIGN names -- borrowing one authority's answer to settle a question it never addressed. The five refused classes are untouched and still dominate every admission, including this one."

// gunbc#10727 MERGED WHILE ITS OBJECTION STOOD UNANSWERED, filed as the row below. The mechanical
Expand Down
141 changes: 138 additions & 3 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9125,6 +9125,46 @@ fn eval_recompute_value_hash(
}
}

/// THE PUSH CONSTRUCTOR CARRIES THE LIST KEY FORWARD, because the list content hash is a left
/// fold with no finalizer: `hash(push(xs, x)) == mix(hash(xs), hash(x))` exactly. A recursion that
/// threads a growing `list_push` accumulator hands every call a NEW `Rc`, so the identity memo
/// missed on every step and the key rehashed the whole accumulator: one relation realized at
/// per-call O(size), the same key-derivation defect #12065 closed for strings. The failing link is
/// the key derivation, not memo admission -- once the key is O(item), a call that never recurs
/// costs a bounded constant, so no "can this recur" heuristic is needed to decide admission.
///
/// DEMAND-GATED: it extends only a parent hash that a key derivation already paid for (alive in the
/// memo). An accumulator no call ever keyed is never hashed here, so a program that does not key
/// lists pays nothing. The item is hashed through the same memo the key would use, so the result is
/// the value the full fold would compute; a Closure item bails and the result is simply left
/// unmemoized, to be refused by the ordinary derivation.
fn eval_recompute_extend_push_hash(
ctx: &InterpContext,
parent: &Rc<RrbVector<Value>>,
item: &Value,
pushed: &Value,
) {
let Value::List(child) = pushed else { return };
let Ok(mut memo) = ctx.eval_recompute_hash_memo.try_borrow_mut() else {
return;
};
let parent_h = match memo.get(&(Rc::as_ptr(parent) as usize)) {
Some((w, h)) if w.alive() => *h,
_ => return,
};
let interner = ctx.symbols.borrow();
let Some(item_h) = eval_recompute_value_hash(&mut memo, &interner, item) else {
return;
};
memo.insert(
Rc::as_ptr(child) as usize,
(
CompositeWeak::List(Rc::downgrade(child)),
eval_recompute_mix(parent_h, item_h),
),
);
}

fn eval_recompute_arg_key(
memo: &mut EvalRecomputeHashMemo,
interner: &SymbolInterner,
Expand Down Expand Up @@ -11160,8 +11200,10 @@ macro_rules! v1_algebra_method_arms {
counters.list_push_items_copied += copied;
drop(counters);
let mut result = (*items).clone();
result.push_back(item);
Ok(list_value(result))
result.push_back(item.clone());
let pushed = list_value(result);
eval_recompute_extend_push_hash($ctx, &items, &item, &pushed);
Ok(pushed)
}
None => Err(InterpError::TypeError {
msg: format!("list_push on non-list: {}", $receiver.type_label()),
Expand Down Expand Up @@ -20080,7 +20122,9 @@ macro_rules! v1_builtin_arms {
drop(counters);
let mut result = (*items).clone();
result.push_back((*item).clone());
Ok(Some(list_value(result)))
let pushed = list_value(result);
eval_recompute_extend_push_hash($ctx, &items, item, &pushed);
Ok(Some(pushed))
}
None => Ok(None),
},
Expand Down Expand Up @@ -25626,3 +25670,94 @@ mod the_emitted_listing_producer_refuses_too {
);
}
}

#[cfg(test)]
mod push_hash_extension_tests {
use std::rc::Rc;

use im::{vector as im_vec, HashMap};

use super::*;
use crate::v1_compiler_infer_emit_info::empty_emit_graph_info;
use crate::v1_compiler_infer_items::ResolvedGraph;

fn test_ctx() -> InterpContext {
let graph = ResolvedGraph {
modules: Rc::new(im_vec![]),
item_registry: Rc::new(HashMap::new()),
diagnostics: Rc::new(im_vec![]),
emit_graph_info: empty_emit_graph_info(),
};
InterpContext::new(&graph, Rc::new(HashMap::new()), ExecutionMode::Hermetic)
}

fn full_fold_hash(ctx: &InterpContext, v: &Value) -> u64 {
// A fresh memo: the reference is the whole fold, with nothing served from identity.
let mut fresh = EvalRecomputeHashMemo::default();
eval_recompute_value_hash(&mut fresh, &ctx.symbols.borrow(), v).expect("keyable")
}

/// THROUGH THE PRODUCTION ARMS, never the helper: `i` selects the free-call arm
/// (`eval_builtin`) or the method arm (`eval_algebra_method_inner`), alternating so deleting
/// the extension from EITHER arm turns the test red (DESIGN section 3: deleting the
/// integration must make a control fail).
fn push(ctx: &InterpContext, xs: &Rc<RrbVector<Value>>, item: Value, i: i64) -> Value {
let receiver = Value::List(xs.clone());
if i % 2 == 0 {
eval_builtin("list_push", &[(None, receiver), (None, item)], ctx)
.expect("free list_push evaluates")
.expect("free list_push is a builtin")
} else {
eval_algebra_method_inner("list_push", receiver, &[item], &Env::empty(), ctx)
.expect("method list_push evaluates")
}
}

/// The extended entry must be the value the full fold computes, for scalar and composite
/// items alike -- otherwise two equal accumulators would key apart (or two distinct ones
/// together). And it must be demand-gated: an unkeyed parent is never extended.
#[test]
fn pushed_list_hash_is_the_full_fold_and_is_demand_gated() {
let ctx = test_ctx();
let mut acc = list_value(Vec::<Value>::new());
// Unkeyed parent: no entry may appear for the child.
let Value::List(rc0) = acc.clone() else {
unreachable!()
};
let child = push(&ctx, &rc0, Value::Int(0), 0);
let Value::List(child_rc) = &child else {
unreachable!()
};
assert!(ctx
.eval_recompute_hash_memo
.borrow()
.get(&(Rc::as_ptr(child_rc) as usize))
.is_none());
// Key the root once, then thread the accumulator.
{
let mut m = ctx.eval_recompute_hash_memo.borrow_mut();
eval_recompute_value_hash(&mut m, &ctx.symbols.borrow(), &acc).unwrap();
}
for i in 0..64 {
let Value::List(rc) = acc.clone() else {
unreachable!()
};
let item = if i % 3 == 0 {
list_value(vec![Value::Int(i), str_value(format!("s{i}"))])
} else {
Value::Int(i)
};
acc = push(&ctx, &rc, item, i);
let Value::List(now) = &acc else {
unreachable!()
};
let served = ctx
.eval_recompute_hash_memo
.borrow()
.get(&(Rc::as_ptr(now) as usize))
.map(|(_, h)| *h)
.expect("a keyed lineage is extended on push");
assert_eq!(served, full_fold_hash(&ctx, &acc));
}
}
}
Loading