Repository navigation
Integrate the demand engine into the production native driver - #12401
Merged
Merged
Conversation
… uses The contract/persistence split lands first because the engine imports std.judgment_contract for DemandIdentity and demand_identity_canonical, so the lower authority has to exist before the engine group can qualify on its own. judgment_contract declares JudgmentContract.demand_nature: DemandNature and did not import it. std.materialization_ladder is that type's single authority and does not import this module, so the edge is acyclic and the repair is to consume it rather than restate it. The defect survived the originating lane because that lane never compiled this module as its own entry closure; compiled as one at the integration base it is a hard diagnostic. All five encoding and decoding bodies -- length_prefixed_encode, length_prefixed_decode, demand_identity_canonical, demand_identity_decode, string_from_code_points -- are byte-identical to the versions they moved from, so the canonical identity format is preserved by construction rather than by inspection. Nat crossings, checked at the boundary rather than by spelling: count and length are builtin methods typed through v1.compiler.infer_method's registry from the algebra templates, every one of which declares return_type std.nat.Nat, so the v2.std.algebra.length wrapper returning Int is not on this path. Eight sites cross into to_string, into a comparison against a parse_int result, and into take and skip which declare Int. The front end accepts all eight at the integration base, so no widening is authored: a cast nobody needs would lose the nonnegativity the contract carries. Compiled at base 4039815 -- judgment_contract exit=0, 0 blocking errors; materialization_provider exit=0, 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ve claim demand_engine imports std.judgment_contract for DemandIdentity and demand_identity_canonical, so it follows the contract split rather than leading it. Carried with its direct claims only. native_demand_schedule_test is held back deliberately. Compiled as its own entry closure at the integration base it refuses on twelve names it expects from v2.compiler.compile -- NativeDemandPlan, NativeDemandValue, the four native_demand_* identity and plan functions, the three NativeCost arms, native_demand_cost_class and the two observation functions. Those names arrive with the production consumer, so the claim belongs to that group; landing it here would have put a red in the tree with no authority able to green it. The Nat question is answered differently here than in the contract group and the difference is the evidence. All five sites call length as a FREE function -- length(xs: e.entries) -- which resolves to v2.std.algebra length returning Int, not the builtin method whose algebra template declares std.nat.Nat. So the refinement does not reach this module's arithmetic, established from the call form and the declarer rather than from the name. Compiled at base 4039815: demand_engine exit=0, demand_engine_test exit=0, 0 blocking errors each. Direct claims executed, 15 requested and 15 reported, exit=0, no absent results. The negative paths are inside that population rather than beside it: a refused prerequisite blocks its dependent, a fresh effect is never attached, a cycle is reported as a cycle, a missing edge is reported, and no seat leaves a demand ready. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t it denied Three authorities, one capability. v1.compiler.infer_method declares the observed_monotonic_nanos signature, extdeps.languages.rust.emit bridges it into the emitted registry, and v1.compiler.runtime_rust carries the body as its own rt_realization_measurement fragment rather than lines inside an unrelated block. The signature repair is a seed defect independent of the demand program. The row read `params: []` while every call site passed a label and the interpreter accepted it, so the interpreter admitted an argument its own signature denied and no emitted body could have been written against the declaration. The label is never identity material and is never hashed; it exists so pure-call memoization cannot collapse two readings around one subject into one, which would report every measured span as zero. trace_mark beside it already declared its label, so this row now matches the shape its neighbour had. Why the body had to exist: a modeled operation, an interpreter implementation and an emitted-runtime realization are three capabilities, and the builtin was registered for the interpreter only. A fold reading the clock therefore typechecked, ran under `gunbc run`, and panicked in the emitted binary -- which is where the native route actually executes. std.primitive_identity rosters five derived surfaces and a runtime body surface is not among them, which is how a registry row with no body passed every rostered check. Excluded from this group deliberately: the 05_emit_rust.dag hunk in the originating commit is entirely the emitted_closure_crate_name and seed_host_crate_name consolidation, with nothing clock-related in it. That naming work is handled through #12358 and is not replayed here. Compiled at base 4039815, each as its own entry closure: 04_method exit=0, runtime_rust exit=0, rust/emit exit=0, 0 blocking errors each. The emitted realization is NOT yet qualified by this commit. The built binary renders runtime text from the stage0 mirror, not from this .dag, so the specimen that proves the emitted clock executes requires the regenerated mirror and a rebuilt binary. That is the next step, and it is a precondition of the production consumer rather than of this carry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Regenerated rather than carried: the originating lane's mirror commit is a generated projection, and installing its bytes would have shipped a mirror produced by a different authority set than the one integrated here. The affected output population is DERIVED and it is three, not the four the assessment listed as candidates. required-regen planned 161, executed 161 and adjudicated 161, and reported drift in exactly extdeps_languages_rust_emit.rs, v1_compiler_infer_method.rs and v1_compiler_runtime_rust.rs -- one per carried authority. v1_compiler_emit_rust.rs is absent from that set because the 05_emit_rust.dag naming hunk was excluded, which is the difference between a candidate list and a roster. Each mirror carries its authority's change and nothing else: the emitted runtime registry gains the observed_monotonic_nanos bridge row, the builtin signature's empty params becomes the declared label, and the runtime source gains rt_realization_measurement. declared_divergent=1 [main.rs] is pre-existing and is not from this change. This makes the emitted realization exist in a binary for the first time; that binary's specimen is the next step and no claim about the emitted clock is made by this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ays put Carried from the originating lane because #12355 was CLOSED WITHOUT MERGE, so this is neither a dependency already in the tree nor a delivered fix to preserve. It is independent of demand scheduling and lands as its own change rather than inside the production-consumer group. A missing grammar row is not a shape error and this arm reported it as one. The row match produces a precise translate_grammar_relation_row_not_found when the target's grammar renders no row for a relation; the fallback discarded it and then refused from translate_type_expression_project, so a target missing a row for a MODULE MEMBER surfaced as translate_arrow_body_not_a_type_expression -- a cause about the node's shape rather than the target's coverage. DESIGN section 5 requires a failure arm to refuse with a located typed cause, not substitute a different one, and the substitution mis-located real work. THE FATAL IS DELIBERATELY UNCHANGED. translate_arrow_body_not_a_type_expression is the discriminating red of a rostered class at rung 1, closure_emit_renders_an_arrow_without_its_body, asserted BY NAME in v2.test.emit.closure_emit_arrow_body_refusal and pinned by //gunbc/instruments:v2-native-cli. Promoting the row cause to fatal would have retired that evidence while looking like a diagnostic improvement. The row cause is therefore appended FIRST and the shape cause LAST, because diagnostics_fatal selects the last diagnostic -- so the fatal is byte-for-byte the cause it was, and the only change is that the row cause is carried as context instead of dropped. Merged rather than applied: main moved this file +167/-20 since the originating merge base and the conflict was positional. Main's side added translate_module_not_a_type_expression_diagnostic and translate_first_module_body_optional, which translate_type_expression_tree now CALLS, so both sides are load-bearing and both are kept. Nothing of main's was dropped to make room for the carried comment. Compiled at base 4039815 as its own entry closure: exit=0, 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…doing it The production cut. 00_compile.dag carries the demand consumer and its observation folds, 05_emit_rust.dag switches the rendered main onto native_demand_schedule_universe, and native_demand_schedule_test joins its authority at last. WHERE THE CUT ACTUALLY IS, because the file sizes read the other way round. 00_compile.dag is +1047/-0 and nothing was deleted from it, which looks exactly like a handler landing beside the implementation it was supposed to displace. It is not: the route lives in the emitter's rendered-main TEXT, where native_demand_schedule_universe is called from two string literals, and 05_emit_rust.dag is +86/-97 -- a net deletion, the displaced scheduler and its observation leaving the rendered main. A reader checking only the consumer module would conclude the opposite, so the arithmetic is stated here. Carried from three emitter commits and NOT a fourth. The naming consolidation in 1de2805 is excluded, so `let crate_name = if has_pipeline { "v1_compiler" } else { "v1_compiled" }` stands byte-for-byte as main has it and nothing of #12358's subject is replayed. Main's own changes to 00_compile are preserved rather than overwritten: the gunbc.native_frontier_ratchet import, and main's move of list_append and list_snoc_item from v2.std.algebra to std.algebra. Compiled at base 4039815, each as its own entry closure: 00_compile exit=0, native_demand_schedule_test exit=0, 05_emit_rust exit=0, 0 blocking errors each. Claims executed, 14 requested and 14 reported, exit=0, no absent results. The negative paths are inside that population: a reversed elapsed reading is invalid rather than zero, an invalid or unclassified reading makes the observation INCOMPLETE rather than silently totalling, a blocked demand contributes no transition, a kind outside the contracts is counted rather than dropped, and rendering the receipt moves no total. What this commit does NOT establish: the emitted route. 05_emit_rust.dag changed, so v1_compiler_emit_rust.rs is now stale and the binary still renders the old main. Regenerating that mirror and requalifying against the production consumer is the next step. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ched main One mirror, derived rather than listed. required-regen planned 161, executed 161 and adjudicated 161, and reported drift in exactly v1_compiler_emit_rust.rs -- the single authority the production cut changed. The three mirrors installed for the clock group came back clean, which is the evidence that they installed correctly rather than merely that nothing complained. The mirror now renders native_demand_schedule_universe, so a binary built from this tree emits a main that schedules through the engine. Before this commit the switched route existed only in .dag and every built binary still rendered the displaced scheduler. declared_divergent=1 [main.rs] is pre-existing and not from this change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Checkpoint native-execution qualification in progress at The emitted production closure builds successfully (cargo exit 0). Four native controls pass (exit 0): ordered actual primitive readings; independently bounded clock progress; reversed elapsed versus unknown classification; and real production scheduler execution compared against direct scheduling using identical semantic authorities/context/input. The scheduler control observes one true result, one false result, and one located malformed-input refusal. Six transitions produce three complete result rows. The blocked eval demand does not execute. Transition identity uniqueness, valid elapsed observations, exhaustive classification, and exact correspondence with settled executions are all asserted. The production executable also returns those same three complete identity-keyed rows in both arms. Both process exits are 1 because the fixture deliberately contains false/refused results; neither is reported as a passing test population. Discriminating clock red: in an isolated copy of the emitted crate, replace only the actual The selected seven are running from a The following native controls are reviewable qualification artifacts, not claimed as automatically enrolled CI controls. They run against the emitted crate through ordinary cargo integration tests. Implementation ownership/enrollment remains with the active integration author. Executed native controls//! Execute against the emitted v2.compiler.compile crate, never the seed interpreter.
use std::{
collections::BTreeMap,
rc::Rc,
time::{Duration, Instant},
};
use v1_compiled::{
std_cache_identity::parse_source_artifact_kind,
std_judgment_contract::DemandIdentity,
v1_rt,
v2_compiler_compile::*,
v2_compiler_native_test_vocabulary::NativeTestVerdict,
v2_std_demand_engine::{demand_engine_entry, demand_identity_key, DemandState},
};
#[test]
fn emitted_clock_readings_are_ordered() {
let mut previous = v1_rt::observed_monotonic_nanos("ordered".into());
for _ in 0..1024 {
let next = v1_rt::observed_monotonic_nanos("ordered".into());
assert!(
next >= previous,
"emitted clock reversed: {previous} -> {next}"
);
previous = next;
}
}
#[test]
fn emitted_clock_makes_progress_with_an_independent_deadline() {
let deadline = Instant::now() + Duration::from_secs(1);
let first = v1_rt::observed_monotonic_nanos("progress".into());
loop {
let next = v1_rt::observed_monotonic_nanos("progress".into());
assert!(next >= first, "emitted clock reversed");
if next > first {
break;
}
assert!(Instant::now() < deadline, "emitted clock made no progress");
std::thread::yield_now();
}
}
#[test]
fn reversed_elapsed_and_unknown_class_remain_distinct() {
let compiler = native_demand_tested_tree_input("qualification".into());
let plan = native_demand_plan(Rc::new(im::vector![]), compiler.clone());
let initial = native_demand_run_empty(plan);
let known = native_demand_resolve_identity("qualification".into(), compiler);
let invalid = elapsed_observation(9, 4);
assert!(matches!(
&*invalid,
ElapsedObservation::ElapsedObservationInvalid {
start: 9,
finish: 4
}
));
let run = |identity, elapsed| {
Rc::new(NativeDemandRun {
engine: initial.engine.clone(),
rows: initial.rows.clone(),
transitions: Rc::new(im::vector![Rc::new(NativeDemandTransition {
identity,
elapsed
})]),
})
};
let reversed = run(known.clone(), invalid);
let r = native_demand_observation_rollup(reversed.clone());
assert_eq!((r.classified, r.unclassified, r.invalid_elapsed), (1, 0, 1));
assert!(!native_demand_observation_complete(reversed));
let unknown = Rc::new(DemandIdentity {
kind: parse_source_artifact_kind(),
..(*known).clone()
});
let unclassified = run(unknown, elapsed_observation(4, 9));
let r = native_demand_observation_rollup(unclassified.clone());
assert_eq!((r.classified, r.unclassified, r.invalid_elapsed), (0, 1, 0));
assert!(!native_demand_observation_complete(unclassified));
}
fn source(
path: &str,
text: &str,
) -> Rc<v1_compiled::v2_compiler_source_authority::DagSourceReadWitness> {
use v1_compiled::{
extdeps_communication_medium::{DecodeFidelity, Medium},
v2_compiler_source_authority::{source_root_for_storage_path, DagSourceReadWitness},
v2_std_artifact::{Artifact, ArtifactKind},
};
Rc::new(DagSourceReadWitness {
source: Rc::new(Medium {
carried: text.into(),
fidelity: DecodeFidelity::Lossless,
_phantom: std::marker::PhantomData,
}),
artifact: Rc::new(Artifact {
kind: ArtifactKind::SourceFile,
id: path.into(),
file_path: path.into(),
}),
compilation_unit: path.into(),
source_root: source_root_for_storage_path(path.into()),
})
}
#[test]
fn production_scheduler_executes_and_matches_direct_authorities() {
use v1_compiled::v2_std_diagnostic::Outcome;
let ingest = Rc::new(im::vector![
source(
"positive.dag",
"module qualification.positive\nfn yes() -> Bool { true }\nfn no() -> Bool { false }\n"
),
source("broken.dag", "module qualification.broken\n@\n")
]);
let context = match &*native_test_context_from_ingest(ingest) {
Outcome::Accepted { value, .. } => value.clone(),
Outcome::Rejected { diagnostics } => panic!("context: {diagnostics:?}"),
};
let modules = Rc::new(im::vector![
Rc::new(NativeLaneUniverseModule {
module: "qualification.positive".into(),
path: "positive.dag".into(),
declarations: Rc::new(im::vector!["yes".into(), "no".into()]),
}),
Rc::new(NativeLaneUniverseModule {
module: "qualification.broken".into(),
path: "broken.dag".into(),
declarations: Rc::new(im::vector!["blocked".into()]),
})
]);
let index = native_lane_file_refusal_index(context.file_refusals.clone());
let compiler = native_demand_tested_tree_input("qualification".into());
let run = native_demand_schedule_universe(
modules.clone(),
context.clone(),
index.clone(),
compiler.clone(),
);
let mut direct = Vec::new();
for entry in modules.iter() {
match &*native_lane_module_resolution(context.clone(), index.clone(), entry.clone()) {
NativeLaneModuleResolution::NativeLaneModuleContextRowsDecided { rows }
| NativeLaneModuleResolution::NativeLaneModuleResolveRowsDecided { rows } => {
direct.extend(rows.iter().cloned())
}
NativeLaneModuleResolution::NativeLaneModuleResolved { resolved } => {
match &*native_lane_module_inference(entry.clone(), resolved.clone()) {
NativeLaneModulePreparation::NativeLaneModuleRowsDecided { rows } => {
direct.extend(rows.iter().cloned())
}
NativeLaneModulePreparation::NativeLaneModulePrepared { prepared } => {
for declaration in entry.declarations.iter() {
direct.push(native_lane_identity_row(
prepared.clone(),
entry.module.clone(),
declaration.clone(),
));
}
}
}
}
}
}
let keyed = |rows: Vec<Rc<NativeRouteMemberRow>>| -> BTreeMap<String, serde_json::Value> {
let mut by_identity = BTreeMap::new();
for row in rows {
let value = serde_json::to_value(row).unwrap();
let key = value["identity"].to_string();
assert!(
by_identity.insert(key, value).is_none(),
"duplicate result identity"
);
}
by_identity
};
assert_eq!(keyed(direct), keyed(run.rows.iter().cloned().collect()));
assert!(
run.rows
.iter()
.any(|r| matches!(&*r.verdict, NativeTestVerdict::NativeTestPassed)),
"positive demand never executed"
);
assert!(
run.rows
.iter()
.any(|r| matches!(&*r.verdict, NativeTestVerdict::NativeTestReturnedFalse)),
"negative demand never executed"
);
let blocked =
native_demand_eval_identity("qualification.broken".into(), "blocked".into(), compiler);
assert!(matches!(
&*demand_engine_entry(run.engine.clone(), blocked.clone())
.unwrap()
.state,
DemandState::DemandBlocked { .. }
));
let mut keys = std::collections::BTreeSet::new();
for transition in run.transitions.iter() {
let key = demand_identity_key(transition.identity.clone());
assert_ne!(key, demand_identity_key(blocked.clone()));
assert!(keys.insert(key), "duplicate transition");
assert!(elapsed_is_valid(transition.elapsed.clone()));
assert_ne!(
native_demand_cost_class(transition.identity.clone()),
NativeDemandCostClass::NativeCostUnclassified
);
}
let completed: std::collections::BTreeSet<_> = run.engine.completion_order.iter()
.map(|id| demand_identity_key(id.clone())).collect();
assert_eq!(completed, keys, "executed settlements and observations differ");
assert_eq!(run.engine.completion_order.len(), run.transitions.len());
for entry in run.engine.entries.iter() {
let observed = keys.contains(&demand_identity_key(entry.identity.clone()));
match &*entry.state {
DemandState::DemandAvailable { .. } | DemandState::DemandRefused => assert!(observed),
DemandState::DemandBlocked { .. } => assert!(!observed),
_ => panic!("scheduler left a demand unsettled"),
}
}
assert!(native_demand_observation_complete(run.clone()));
assert_eq!(
native_demand_observation_rollup(run.clone()).classified as usize,
run.transitions.len()
);
eprintln!(
"engine transitions={} rows={}",
run.transitions.len(),
run.rows.len()
);
}Reproduction and scopeNative demand execution controlsThese controls run against the emitted Save the control source from the review comment as gunbc compile --source-root dag --source-root src/v2 --source-root src/v1 \
--entry src/v2/compiler/00_compile.dag --output-dir /tmp/native-demand
mkdir -p /tmp/native-demand/tests
cp /tmp/native-demand-controls.rs /tmp/native-demand/tests/controls.rs
timeout 300 cargo test --manifest-path /tmp/native-demand/Cargo.toml \
--test controls --jobs 1 -- --test-threads=1 --nocaptureThe progress test has a separate host The scheduler comparison supplies one shared context, module population, compiler identity, These are operator-invoked emitted qualification controls, not a newly required CI phase. Source identities (sorted relative path, NUL, SHA-256, newline manifest): {
"checkpoint": {
"files": 6931,
"sha256": "f979b3da896391b9b5ac5e417fd7b1d8be2c37bf6ff7d5e12559e7b406ca5f9b"
},
"small": {
"files": 3,
"sha256": "8293ff643271bcce9ed638710b04d69151927a679861991c0b85a6e815970872"
},
"emitted": {
"files": 207,
"sha256": "73174ff912c2bdda12cacd758a145886221b6efb69626cf49e1b18b8a5137d41"
}
} |
Contributor
Author
Native execution qualification: checkpoint 44419a1The checkpoint remains published at Results
Controlled comparisonBoth release arms link the same emitted library and Cargo dependency graph. Source authorities, runtime capabilities, filesystem acquisition, roots, selection, working directory, and input bytes are identical. The direct executable substitutes only the previous scheduling block and its imports into the treatment main; equality of all other main bytes is checked. Durations are not compared. The filesystem PR has not been mixed into one arm. Sources are a A first live-checkout attempt was cancelled after concurrent author edits appeared. A debug direct attempt and an earlier release attempt were superseded before sealing the final controlled comparison. Those partial runs are not used as equivalence evidence. The active implementation owner's files have not been changed or committed by this qualification session. Reviewable controls and reproduction are in the earlier comment. Their execution is established; automatic CI enrollment is not claimed. Reconciliation and any successor receipt remain separate from this fixed checkpoint. Payload lifetime/residency remains unqualified, and seats remain one. Exact native executions and executable identities[
{
"command": [
"timeout",
"900",
"systemd-run",
"--user",
"--scope",
"-p",
"MemoryMax=16G",
"--quiet",
"--",
"/tmp/demand-native-qualification/engine/target/release/v1_compiled",
"adjudicate",
"/tmp/demand-native-qualification/release-small-engine-facts.tsv",
"//v2/test/qualification/...",
"/tmp/demand-native-qualification/small"
],
"cwd": "/tmp/demand-native-qualification/checkpoint",
"exit": 1,
"executable_sha256": "666633a5805f902ea6248148e47513383e9bad28b5205962c3f5663386d0179b",
"source_head": "44419a1ef94f2d284c7178f2439d033e679ff05f",
"pattern": "//v2/test/qualification/...",
"roots": [
"/tmp/demand-native-qualification/small"
]
},
{
"command": [
"timeout",
"900",
"systemd-run",
"--user",
"--scope",
"-p",
"MemoryMax=16G",
"--quiet",
"--",
"/tmp/demand-native-qualification/engine/target/release/direct",
"adjudicate",
"/tmp/demand-native-qualification/release-small-direct-facts.tsv",
"//v2/test/qualification/...",
"/tmp/demand-native-qualification/small"
],
"cwd": "/tmp/demand-native-qualification/checkpoint",
"exit": 1,
"executable_sha256": "333e782c379b6578c9364f8beb82c654653f2648ea0ed5eb521352f33f41773f",
"source_head": "44419a1ef94f2d284c7178f2439d033e679ff05f",
"pattern": "//v2/test/qualification/...",
"roots": [
"/tmp/demand-native-qualification/small"
]
},
{
"command": [
"timeout",
"900",
"systemd-run",
"--user",
"--scope",
"-p",
"MemoryMax=16G",
"--quiet",
"--",
"/tmp/demand-native-qualification/engine/target/release/v1_compiled",
"adjudicate",
"/tmp/demand-native-qualification/release-seven-engine-facts.tsv",
"//v2/test/parse/expression_bodied_fn_decl_parse:all",
"/tmp/demand-native-qualification/checkpoint/dag",
"/tmp/demand-native-qualification/checkpoint/src/v2"
],
"cwd": "/tmp/demand-native-qualification/checkpoint",
"exit": 1,
"executable_sha256": "666633a5805f902ea6248148e47513383e9bad28b5205962c3f5663386d0179b",
"source_head": "44419a1ef94f2d284c7178f2439d033e679ff05f",
"pattern": "//v2/test/parse/expression_bodied_fn_decl_parse:all",
"roots": [
"/tmp/demand-native-qualification/checkpoint/dag",
"/tmp/demand-native-qualification/checkpoint/src/v2"
]
},
{
"command": [
"timeout",
"900",
"systemd-run",
"--user",
"--scope",
"-p",
"MemoryMax=16G",
"--quiet",
"--",
"/tmp/demand-native-qualification/engine/target/release/direct",
"adjudicate",
"/tmp/demand-native-qualification/release-seven-direct-facts.tsv",
"//v2/test/parse/expression_bodied_fn_decl_parse:all",
"/tmp/demand-native-qualification/checkpoint/dag",
"/tmp/demand-native-qualification/checkpoint/src/v2"
],
"cwd": "/tmp/demand-native-qualification/checkpoint",
"exit": 1,
"executable_sha256": "333e782c379b6578c9364f8beb82c654653f2648ea0ed5eb521352f33f41773f",
"source_head": "44419a1ef94f2d284c7178f2439d033e679ff05f",
"pattern": "//v2/test/parse/expression_bodied_fn_decl_parse:all",
"roots": [
"/tmp/demand-native-qualification/checkpoint/dag",
"/tmp/demand-native-qualification/checkpoint/src/v2"
]
}
]Complete selected-seven rows[
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "expression_bodied_fn_decl_parses_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "expression_bodied_literal_fn_decl_parses_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "braced_fn_decl_still_parses_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "braced_fn_decl_survives_normalize_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "empty_eq_fn_decl_refuses_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "expression_bodied_fn_decl_survives_normalize_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
},
{
"identity": {
"module": "v2.test.parse.expression_bodied_fn_decl_parse",
"declaration": "expression_bodied_literal_fn_decl_survives_normalize_holds"
},
"verdict": {
"_variant": "NativeTestRefused",
"stage": {
"_variant": "NativeTestStageContext"
},
"diagnostics": {
"head": {
"reason": "body_lowering_reason_match_arm_navigation_refused",
"at": {
"_variant": "Textual",
"file": "/tmp/demand-native-qualification/checkpoint/src/v2/test/claim/parse/expression_bodied_fn_decl_parse_test.dag",
"extent": {
"_variant": "WholeFile"
}
},
"correction": {
"_variant": "Unavailable",
"reason": {
"_variant": "UserInputBoundary"
}
}
},
"tail": []
}
}
}
]Source and emitted-artifact identities{
"checkpoint": {
"files": 6931,
"sha256": "f979b3da896391b9b5ac5e417fd7b1d8be2c37bf6ff7d5e12559e7b406ca5f9b"
},
"small": {
"files": 3,
"sha256": "8293ff643271bcce9ed638710b04d69151927a679861991c0b85a6e815970872"
},
"emitted": {
"files": 207,
"sha256": "73174ff912c2bdda12cacd758a145886221b6efb69626cf49e1b18b8a5137d41"
}
}Additional SHA-256 identities:
Build and clock-control commandsExecuted from timeout 900 systemd-run --user --scope -p MemoryMax=16G --quiet -- env RUSTC=/home/briansrls/.rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/rustc /home/briansrls/.local/bin/cargo build --release --manifest-path /tmp/demand-native-qualification/engine/Cargo.toml --jobs 1
# exit 0
timeout 300 systemd-run --user --scope -p MemoryMax=16G --quiet -- env RUSTC=/home/briansrls/.rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/rustc /home/briansrls/.local/bin/cargo test --release --manifest-path /tmp/demand-native-qualification/engine/Cargo.toml --test controls --jobs 1 -- --test-threads=1 --nocapture
# exit 0: four passed
timeout 600 systemd-run --user --scope -p MemoryMax=16G --quiet -- env RUSTC=/home/briansrls/.rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/rustc /home/briansrls/.local/bin/cargo test --manifest-path /tmp/demand-native-qualification/clock-zero/Cargo.toml --test controls --jobs 1 emitted_clock_makes_progress_with_an_independent_deadline -- --exact --nocapture
# exit 101: intended constant-zero red, failure within 1.00 secondsClock-control provenance: comparing both candidate source trees (Cargo manifest/lock, Rust modules and test source) leaves exactly one difference,
|
…fact
THE HOLE, stated as measured rather than as a worry. elapsed_observation admits
finish == start as ElapsedObserved { nanos: 0 }, so a realization whose body
returns a constant zero leaves every transition CLASSIFIED and VALIDLY OBSERVED:
unclassified is 0, invalid_elapsed is 0, classified equals the transition count,
and native_demand_observation_complete answers TRUE over totals that are entirely
zero. The emitted-body membership phase cannot see it either -- that check
establishes a bridge HAS a body, never that the body measures anything. Two
different predicates, one shared blind spot.
Three of the four distinctions already held and are unchanged: a reversed reading
is ElapsedObservationInvalid rather than zero, invalid_elapsed is counted
SEPARATELY from unclassified, and both already break completeness. The missing one
was progress.
native_demand_observation_progressed asks progress AT THE RUN, not per transition.
One fast transition may honestly observe a zero span on a coarse clock, so a
per-transition rule would refuse real work; a run that executed transitions and
accumulated no span at all is a clock that is not running. An empty run is
vacuously progressed, so the predicate reports no defect where there was no work.
DELIBERATELY NOT FOLDED INTO completeness. Completeness answers whether every
admitted transition reached a cost class; progress answers whether the realization
underneath produced a measurement. Fusing them would make one counter answer two
questions and would silently change what every existing consumer of `complete`
asserts.
The rendered main CONSUMES it fail-closed: a run whose clock never advanced
refuses with a located cause naming the transition count, rather than reporting
its zeros as an observation. Reporting them would be a fabricated measurement
presented as a reading, which DESIGN section 5 forbids outright. So the predicate
has a production consumer and is not a declaration only witnesses read.
THE READINGS IN THE CLAIMS ARE SUPPLIED, NOT CLOCKED. The subject is the
observation fold, so reading the real clock would assert something about the
host's timer instead -- and could not author the constant-zero case at all, since
a working clock refuses to produce it. Supplying them is also what bounds the
control: there is no timer to wait on, so a broken clock cannot hang its own test.
Compiled at base 4039815: 00_compile exit=0, native_demand_schedule_test
exit=0, 05_emit_rust exit=0, 0 blocking errors each.
Claims executed, 18 requested and 18 reported, exit=0, no absent results. The four
added controls discriminate in both directions: the dead-clock case would fail if
progress were always true (it asserts complete AND not progressed over the same
run), and the positive control would fail if progress were always false.
NOT established by this commit: the refusal in a binary. 05_emit_rust.dag changed,
so v1_compiler_emit_rust.rs is stale again and every built binary still renders a
main without the refusal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…binary One mirror again, derived not listed: required-regen planned 161, executed 161, adjudicated 161, drift in exactly v1_compiler_emit_rust.rs -- the single authority the progress control changed. The four previously installed mirrors came back clean. The mirror now carries native_demand_observation_progressed, so a binary built from this tree renders a main that refuses a run whose clock never advanced. Before this commit the refusal existed only in .dag and every built binary would have reported the zeros. declared_divergent=1 [main.rs] is pre-existing and not from this change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
#12391's modeled filesystem acquisition is on main, so the two changes that touch the emitted driver area meet here rather than racing: modeled acquisition plus modeled demand scheduling and observation. A merge commit rather than a rebase, so the published checkpoint 44419a1 and every head the receipt cites stay reachable and unrewritten. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> # Conflicts: # src/v1/stage0/src/v1_compiler_emit_rust.rs
briansrls
marked this pull request as ready for review
September 27, 2026 15:49
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 915912979e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| " // a different offer to the same drain and changes nothing else.", "\n", | ||
| " let schedule_plan_started = Instant::now();", "\n", | ||
| " let tested_tree_input = native_demand_tested_tree_input(head.clone().unwrap_or_default());", "\n", | ||
| " prepare_total_nanos += span_nanos(schedule_plan_started);", "\n", |
There was a problem hiding this comment.
The schedule_plan_started span is closed before native_demand_schedule_universe is called, even though that function constructs the entire demand plan and drains it. The per-demand spans also exclude ready-queue selection, binding lookup, settlement, readiness recomputation, and row collection, so all of that newly introduced scheduler work falls into the parent residual. For sufficiently large selected universes, this can exceed the fixed 50 ms remainder tolerance and make an otherwise valid production adjudication exit with NativeDriverCostRemainderExceedsTolerance; the scheduler/plan overhead needs an exclusive measurement rather than being left unattributed.
Useful? React with 👍 / 👎.
Contributor
Author
There was a problem hiding this comment.
Fixed at cf82073563e, and you were right that this needed an exclusive measurement rather than being left unattributed.
std.compiler_entry gains ExclusiveDemandScheduling. Because the driver's match over that key is exhaustive with no wildcard, adding the row forced the driver to say what measures it — which is why that match was written without one.
The measurement is taken inside the engine, where the work happens, through the same clock seam the demand's own window uses:
| span | site |
|---|---|
| plan construction | native_demand_schedule_universe |
| ready selection | native_demand_drain, around native_demand_next |
| binding lookup | native_demand_step, before the demand window opens |
| settlement + row collection | native_demand_step, after it closes |
Disjoint from the demand's own window by construction — that window is exactly started..finished around native_demand_execute, and none of these crosses it. The driver reports a reading.
A first attempt was wrong in a way worth recording: it timed the whole native_demand_schedule_universe call and subtracted prepare+eval. That is a residual wearing a row's clothes — it overlaps the spans it subtracts, and worse it absorbs any other unattributed phase into "scheduling", so the remainder could no longer discover a second missing row. A row defined as a residual cannot be the thing that proves the residual is small.
Controls (test.claim.native_driver_cost_partition, 14/14):
- the row is a member of
NativeDriverExclusiveRows— the sum fixture carries a distinct non-zero for it, with the asserted sum and the reconciling parent moved by the same delta so the residual under test is unchanged; an_over_attribution_routed_through_demand_scheduling_is_the_same_refusal— every other row well inside the parent, the total pushed past it through this one, so it fails exactly when this row is dropped from the fold;- the pre-existing tolerance and over-attribution rows still hold, and invalid clock observations still make the observation incomplete.
Adding the key correctly broke nine matches in that witness, since they are over the key type.
| Absent => PreparationNotApplicable | ||
| Present { value: entry } => | ||
| match entry.state { | ||
| DemandRefused => PreparationRefused |
There was a problem hiding this comment.
When resolution returns NativeLaneModuleContextRowsDecided or NativeLaneModuleResolveRowsDecided, its resolve transition is already classified as PreparationRefused; the dependent infer demand is then admitted, settles as DemandRefused, and this unconditional arm classifies that second transition as another refusal. Consequently the emitted prepare_refused telemetry reports 2 for each module that fails during resolution instead of the previous module-level count of 1, skewing the native cost receipt.
Useful? React with 👍 / 👎.
Contributor
Author
There was a problem hiding this comment.
Fixed at cf82073563e. Your reading was exact: the resolve transition carries the decided rows as its value and is a real preparation refusal, then the dependent infer demand settles DemandRefused with no value — it never executed, so there was nothing it refused — and the blanket arm counted it again.
Preparation standing is now decided once per module at the infer demand. There is exactly one infer demand per module (native_demand_plan binds one per entry), so the count cannot scale with declarations. Resolve and eval transitions contribute nothing.
DemandRefused arising from a failed resolution is still counted as refused, which I want to be explicit about: the module's preparation did not succeed, and that is what the old module-level prepare_refused meant.
A second attempt was wrong and is worth recording, because it looked like a fix: it corrected the total by excluding the infer settlement instead. That is the wrong half to drop — it left the count on a per-transition basis rather than per-module, and it reported a resolution failure as something other than a refused preparation, i.e. it changed what the receipt's number means to make an arithmetic problem go away. The intermediate PreparationUnrun standing that served it is deleted.
Four controls (v2.test.demand_engine.native_demand_schedule, 22/22), one per way a module reaches that boundary:
| control | asserts |
|---|---|
a_resolution_failure_is_one_refused_preparation |
refused = 1, ok = 0 — this pair summed to 2 before |
a_resolve_transition_alone_contributes_no_preparation_count |
refused = 0, ok = 0 |
eval_transitions_do_not_move_the_preparation_counts |
counts unmoved across any number of evals |
preparation_counts_do_not_scale_with_declarations |
same module, same single outcome, one test or many |
The last is the load-bearing one: a per-transition count scales with declarations and a per-module count does not, so it is what would have caught the original shape.
…refused REQUIRED-FLOOR REFUSAL cause=UnimportedBareProvider on dag/std/judgment_contract.dag#skip, provider src/v2/std/algebra.dag: the file declares imports, so its bare channel is off and `skip` is never pulled for it. Same class as the DemandNature repair in 3e0a494 and it hid for the same reason: my entry-closure compile passed, because `skip` RESOLVES. The unimported-bare-provider gate is a separate wall from resolution, and only the required floor runs it -- so compiling the module as its own closure could not have caught this, and did not. Only `skip` is flagged of the six bare names the carried decoder uses, and the distinction is checked rather than assumed: skip is declared as fn skip<T> in v2.std.algebra with no builtin registry row, so it is a genuine provider reference. take and fold resolve as algebra METHOD TEMPLATES, count and length through the builtin registry, and join is a free primitive. Importing those would be the concat mistake from earlier in this lane, where naming a free primitive in an import broke resolve across every consumer. The import names the same function that already resolved: fn skip<T>(xs: FreeMonoid<T>, n: Int) against `cs |> skip(n: hash_at + 1)`, where the pipe supplies xs and n is an Int. Verified: judgment_contract compiles exit=0 with 0 blocking errors, and the 48 contract claims re-run 48 requested / 48 reported / 48 PASS, exit=0 -- so the import is a hygiene repair and not a behaviour change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This was referenced Sep 28, 2026
Closed
Demand-engine integration: original seven-demand author owns delivery; management coordinates
#12363
Open
…iled module counts once
P1 -- THE SCHEDULER'S OWN WORK WAS UNATTRIBUTED, AND THAT IS A CORRECTNESS DEFECT.
`schedule_plan_started` opened, covered only native_demand_tested_tree_input, and
CLOSED BEFORE native_demand_schedule_universe ran -- so plan construction, ready-queue
selection, binding lookup, settlement, readiness recomputation and row collection all
fell into the parent residual. The partition's tolerance arm is a fixed 50ms, so a large
enough selected universe makes an otherwise VALID adjudication exit
NativeDriverCostRemainderExceedsTolerance: a fail-closed refusal fired by correct input,
which is the wrong direction of wrong.
The repair uses the mechanism already built for it. std.compiler_entry gains
ExclusiveDemandScheduling, and because the driver's match over that key is exhaustive
WITH NO WILDCARD, adding the row FORCED the driver to say what measures it -- which is
the reason that match was written without a wildcard.
demand_scheduling_nanos = span(whole scheduling call)
- (engine's prepare nanos + engine's eval nanos)
TWO THINGS DELIBERATE HERE. Adding the span to ExclusivePrepare was the one-line edit and
it would DOUBLE-COUNT: the engine already reports its own prepare nanos and the driver
already adds them, so that would trip the OVER-attribution arm instead of the tolerance
one. And the subtraction SATURATES -- these are unsigned, the engine's attributed sum can
exceed the enclosing wall span when the two clocks disagree at the margin, and a plain
subtraction would wrap to an enormous positive and report it as scheduler cost.
P2 -- A MODULE THAT FAILED AT RESOLVE WAS COUNTED TWICE. Its resolve transition carries
the decided rows as its VALUE and is a real preparation refusal; the dependent infer
demand is then admitted and settles DemandRefused WITHOUT a value -- it never executed,
so there is nothing it refused -- and the blanket arm counted it again. prepare_refused
reported 2 for one failing module where the module-level count before the engine was 1.
NativePreparationStanding gains PreparationUnrun for that case, with its own
prepare_unrun total exported and serialized beside prepare_refused. It gets a counter
rather than folding into NotApplicable because "admitted and never executed" is worth
reading: a population where it is large is one mostly blocked behind earlier failures,
and nothing else in the receipt would show that.
THE LIMIT, STATED RATHER THAN IMPLIED. This reads the settled state and not a cause, so a
demand that genuinely refused on its OWN execution without producing rows also lands in
Unrun. The engine already distinguishes DemandRefused from DemandBlocked { cause }
(v2.std.demand_engine), and settling such a dependent as Blocked is the sharper repair --
that belongs to the engine's settlement, not to this rollup, and until it lands the number
is visible here rather than hidden inside the refusal count.
THE ROW KEY'S OWN CONSEQUENCE, HANDLED. std.compiler_entry's header records that its
roster is a hand-authored list whose hole is caught by a witness, and that the witness only
catches it while every key carries a DISTINCT NON-ZERO fixture value. Adding a variant
therefore broke nine matches in
test.claim.native_driver_cost_partition_witness (correctly -- they are over the key TYPE),
and the new row gets a distinct non-zero in the sum fixture with the asserted sum and the
reconciling parent both moved by the same delta, so the residual under test is unchanged.
It also gets the discriminating probe that file keeps per added row: every other row well
inside the parent, the total pushed past it through this one, so the probe fails exactly
when this row is dropped from the fold.
Green: 14/14 in the partition witness, including the new probe. gunbc rebuilt clean;
00_compile and 05_emit_rust compile with no blocking errors.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… counts per module I HAD BOTH OF THESE WRONG, IN THE TWO SPECIFIC WAYS THE RULING NAMES. P1, WRONG THE FIRST TIME: I timed the whole native_demand_schedule_universe call and subtracted the engine's prepare and eval. That is a RESIDUAL WEARING A ROW'S CLOTHES. It overlaps the semantic spans it subtracts, and worse, it ABSORBS any other unattributed phase into "scheduling" -- so the partition's remainder could no longer discover a second missing row. A row defined as a residual cannot be the thing that proves the residual is small, which is the same absorbing arm DESIGN section 5 forbids. NOW MEASURED WHERE THE WORK HAPPENS, inside the engine, through the same clock seam the demand's own window already uses: plan construction native_demand_schedule_universe ready selection native_demand_drain, around native_demand_next binding lookup native_demand_step, before the demand window opens settlement + row collect native_demand_step, after the demand window closes `NativeDemandRun.scheduling_nanos` accumulates those spans and the driver REPORTS the reading. They are disjoint from the demand's own span by construction: that span is exactly started..finished around native_demand_execute, and none of the above crosses it. The driver's own input construction keeps its narrow span charged to prepare, as before the engine landed -- it runs before any demand and is not the scheduler's bookkeeping. An invalid or reversed reading contributes nothing rather than a fabricated figure, and invalid_elapsed still counts those separately, so the total stays a sum of readings actually taken. P2, WRONG TWICE: the first version counted every transition whose standing read Refused, so a module failing at resolve was counted on the resolve transition AND again when its infer demand settled DemandRefused -- 2 where the module-level count was 1. My second version fixed the total by excluding the infer settlement instead, and that is the WRONG HALF to drop: it left the count per-transition rather than per-module, and it reported a resolution failure as something other than a refused preparation, which changes what the receipt's number MEANS in order to make an arithmetic problem go away. Preparation standing is now decided ONCE PER MODULE AT THE INFER DEMAND -- there is exactly one infer demand per module, so the count cannot scale with declarations. Prepared is ok; RowsDecided is refused; DemandRefused because resolution failed is STILL refused, because the module's preparation did not succeed and that is what the old count meant. Resolve and eval transitions contribute nothing. PreparationUnrun and prepare_unrun are deleted -- they existed only to serve the wrong assignment. FOUR DIRECT CONTROLS, one per way a module reaches that boundary: a resolution failure is one refused preparation; a resolve transition alone contributes nothing; any number of evals leaves the counts unmoved; and the counts do not scale with the declaration count -- the last being the one that would have caught the original per-transition shape. The scheduling_nanos field correctly broke all eight NativeDemandRun literals in the schedule test, which is the construction-site census working as intended. Green: 22/22 native demand schedule claims, including the four new ones. 00_compile compiles with 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…of asserting it THE COST SHAPE IS NO LONGER AN UNVERIFIED NOTE. It is two numbers from a control, and they say half the law holds and half does not. WHAT THE LAW CLAIMS: "a completion re-evaluates its DIRECT dependents" -- settling a demand with one dependent among N unrelated ones costs one derivation, not N. The module's own header admitted the check could not see the other half, in its own words: the counter "counts DERIVATIONS, not entries visited", and "locating the dependents is a scan of the relation list". So a whole-population scan and a targeted update reached identical states AND identical counts, and the existing claim passed either way. WHAT IS FIXED: relations are now indexed by direction. demand_engine_relate -- the single site a relation enters -- maintains dependents_of and prerequisites_of, and the two readers consult the index instead of filtering the whole relation population. After this, no reader walks the relation list at all; `.relations` survives only as the authority it always was, plus a length in one fuel bound. These are NOT a second authority. Nothing writes the index that does not write the list in the same call, no reader asks the index a question the list would answer differently, and there is no second writer to drift from. What it removes is a scan, not a fact. WHAT IS NOT FIXED, MEASURED AND ENROLLED: settle still walks the entire entry population TWICE -- once to update the settled entry, once to recompute its dependents' readiness. The new control settles a one-dependent demand in a 5-demand graph and in a 45-demand graph and reports: derivations identical the relation scan is gone entries_walked 10 vs 90 the population walk is not The claim asserts what the engine does TODAY, so it is green by execution and inverts the moment the store becomes keyed. Writing it as the desired property would have landed a red and specified the same thing. WHAT REMAINS IS MECHANICAL AND NAMED. With a persistent LIST, updating one entry is inherently a walk, so locality requires entries keyed by identity plus a separate order list for the whole-population passes the law does NOT claim are local -- seal, reevaluate and the ready-queue build. Nine internal sites and one external length(). AND THE CONSEQUENCE FOR LANDING, STATED PLAINLY: until that control inverts, the production cut is not landable. Its central claim is that a completion costs its out-degree and not the graph, and at the entries grain the implementation does not hold that. The fallback of splitting the cut and landing only the engine/contract/clock foundations is now a live option, since the defect is quantified rather than suspected. I stopped short of the store swap deliberately. It is nine sites in a load-bearing module at the end of a long session, and rushing exactly this kind of edit is what silently deleted a Node-typed argument earlier today. The measurement is committed so the next pass starts from a number. Green: 16/16 demand engine claims including the new control; 22/22 native demand schedule; 14/14 cost partition. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
THE LOCALITY CLAIM HOLDS AT THE ENTRIES GRAIN. The control that was enrolled as the defect now asserts the property and passes: settling a demand with ONE dependent costs the same in a 5-demand graph and in a 45-demand graph, on both counters. before derivations 1 vs 1 entries_walked 10 vs 90 after derivations 1 vs 1 entries_walked 2 vs 2 WHAT CHANGED. `entries` is keyed by identity and `entry_order` carries the insertion order separately, so settlement is a lookup and an insert instead of a rewrite of the population. demand_engine_settle now touches the settled entry and, through the keyed reverse-adjacency index, exactly its direct dependents -- which is the entire content of the law it claims. THE WHOLE-POPULATION PASSES THAT REMAIN ARE THE ONES THE LAW DOES NOT CLAIM ARE LOCAL: seal validates every demand once, reevaluate recomputes every readiness. Both now route through one named helper, demand_engine_entries_mapped, so a THIRD such pass cannot appear inside a function that is supposed to be local without a reader seeing the name. A GENERIC EROSION THIS HIT, AND IT IS THE SAME ONE AS THE FIELD-PROJECTION LANE'S. map_lookup answers Optional<V> over the map's own value generic, and a value destructured straight out of it does not carry DemandEntry<V> through a FIELD READ -- eight errors, all "no field 'identity' on type 'V'". Naming a typed parameter restores it, so every entry rewrite goes through demand_entry_with_state, demand_entry_produced or demand_entry_attached rather than reading fields off a lookup result inline. STILL OUTSTANDING IN THIS FILE, and it is the other half of the cost gate: demand_engine_next rebuilds the ready queue by filtering AND sorting the whole population on every admission, and demand_engine_in_flight filters it again. Keyed entries do not touch that. The next pass maintains the ready set incrementally in canonical order so admitting an already-ready demand is a head read, with its own counter -- because counting only readiness derivations is what hid the entry scans in the first place. Green: 16/16 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…n it proves THREE INVARIANTS MADE EXECUTABLE, because splitting a store from its order buys locality and owes agreement. Two representations of one population can disagree, and a keyed store with a stale order list would answer settlement correctly while every whole-population pass -- seal, reevaluate, receipts -- silently skipped or double-counted a demand. the order resolves entirely in the keyed store no pass reads a dropped key the order names each demand once seal cannot derive one demand twice settlement leaves the order unchanged a completion changes STATE, not membership The third is the value-level shadow of settlement being local: the population a demand belongs to is not a function of what settled. THE FIFTH INVARIANT IS ABSENT AND ITS ABSENCE IS DECLARED. "No operational function traverses entry_order" is a property of the SOURCE, not of any value a claim can read -- the traversals live in demand_engine_entries_mapped and demand_engine_all_entries, and nothing in .dag can see that a third has not appeared elsewhere. Calling the shadow structural would be rung inflation (DESIGN section 4b(1)), so it is recorded as diligence at the same grain as std.compiler_entry's hand-authored row roster, with the same next-rung trigger: a lens over this module's own call graph. AND A PRECISION CORRECTION TO MY OWN CLAIM, which I had overstated. What the counter establishes is that settlement visits the settled entry and its direct dependents and NOTHING ELSE -- the semantic full-population scan is gone. It does NOT establish constant-time operations: a keyed persistent map may carry population-dependent internal cost such as tree depth, and an ordered ready set may carry logarithmic insertion. "Costs its out-degree, not the graph" is sound as a statement about GRAPH WORK; "O(out-degree) wall time" claims more than this evidence supports, and the carrier's header now says so rather than leaving the stronger reading available. Green: 19/19 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… admission THE OTHER HALF OF THE COST GATE. demand_engine_next answered one question -- which identity is canonically first -- by filtering every entry and SORTING the survivors, on every admission, and demand_engine_in_flight filtered the population again beside it. Neither cost a readiness derivation, so both were invisible to the only counter the engine had: exactly the way the entry scans hid. demand_engine_ready_queue returns the maintained order demand_engine_in_flight returns the maintained count demand_engine_next reads the head MAINTENANCE IS LOCAL, AT THE ONE SITE STATE CHANGES. Settlement syncs the settled identity's membership from its new state and then its DIRECT dependents' -- the fold is over the out-degree, so the unrelated population is not consulted here either. The order is keyed on the demand identity and never on arrival, because two runs of one closure must admit in one order and an order depending on which prerequisite settled last would make the completion receipt unreproducible. Seal and reevaluate rebuild both facts from the states they just decided, through one named republish function so a local function cannot reach for a full rebuild by accident. A FINDING ABOUT THE SCAN THAT WAS THERE: demand_engine_in_flight filtered every entry for DemandRunning, and NOTHING IN THIS CORPUS SETS THAT STATE. No producer transitions a demand to running, so that walk computed a constant zero on every admission. It is still derived from state rather than hardcoded -- returning 0 with a comment would be correct today and a fail-open the moment a producer appears, admitting past the seat count because the count was a literal -- so the delta is taken where state changes and tracks a producer that does not exist yet. A COUNTER I WROTE AND DELETED. I first added ready_inspected to make the admission claim observable, then found demand_engine_next returns an admission and not an engine, so no caller could ever read it: a field nothing writes, which is the dangling declaration DESIGN section 3c forbids. The admission cost claim is structural instead -- one inspection of a maintained head, by construction -- and what the counter was a proxy for is asserted directly and is the sharper property: THE MAINTAINED ORDER EQUALS WHAT A FULL REBUILD WOULD PRODUCE, across a seal and three settlements including a refusal, in a 45-demand graph. Drift there would admit a stale identity or skip a ready one while every count looked fine. FIVE STRUCTURAL REDS BESIDE IT: in-flight standing is population-independent and zero; the canonical head survives an unrelated completion; a settled demand leaves the order; a refused prerequisite never admits its dependent; a duplicated dependency cannot duplicate a ready identity. Green: 25/25 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…control that can fail THE REVIEW IS RIGHT AND THE CATCH IS SHARP: DemandRunning is a variant NOTHING IN THIS CORPUS PRODUCES, which is the same unconsumed declaration (DESIGN section 3c) as the inspection counter deleted from this module one commit ago. It got a quiet pass because it sits inside a coproduct rather than standing alone as a field. AND MY CONTROL WAS WORSE THAN USELESS THERE. "The in-flight count is population-independent and zero" cannot fail if the running path breaks, because no producer reaches that path -- so it looked like a guard over the in-flight delta while guarding nothing. A check that cannot go red is a decoration (DESIGN section 4b), and this one was positioned to be cited as coverage. THE FRONTIER IS NOW DECLARED WITH ITS PRODUCER AND TRIGGER, not merely noted. The seat vocabulary is real and consumed -- demand_lease_admits asks the caller's offer whether an admitted demand obtains a lease -- but admission does not RECORD that a demand went in flight, because demand_engine_next answers a DemandAdmission and not an engine, so nothing it wrote could reach a caller. The producer is therefore the admission path returning the engine it changed, which is the SAME structural gap that made the inspection counter unreadable: one missing return, two dangling declarations. Trigger: multi-seat realization -- with one seat the driver executes immediately after admission and no demand is ever observably in flight. AND THE DELTA NOW HAS A ROW THAT DISCRIMINATES. DemandRunning cannot be reached by RUNNING the engine, but it can be SUPPLIED -- demand_engine_settle takes any state, which is the boundary this claim sits at (DESIGN section 3's witness rule). Entering running raises the count, entering it twice does not double-count, and leaving it for a settled state lowers it again. PROVEN DISCRIMINATING BY MUTATION, because a passing claim establishes nothing until it can fail: with demand_in_flight_delta stubbed to return 0, the population row still PASSES and only the new row goes RED. That is the exact split the review predicted. A third row beside it: a running demand is not in the ready order, so a seat held is not also a seat offered. Green: 27/27 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
demand engine 27/27
native schedule 22/22
cost partition 14/14
TWO MERGE CONSEQUENCES FIXED, neither caused by this lane's changes and both found only by running
the sets at THIS head rather than trusting the earlier greens.
Main tightened the unimported-bare-provider rule, so dag/test/claim/native_driver_cost_partition_-
witness now needs `import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }` -- it
declares imports, so its bare channel is off and the pair no longer resolves through the census.
The file had passed 14/14 before the merge on exactly the same content.
And fixing the import made its DEBT ROW stale, which the rule then refused in the other direction:
the roster carried (file, SubstrateInputsOnly) as ActiveDebt, and a pair the file no longer needs
must be retired rather than left owed. Its standing moves ActiveDebt -> Retired { cause:
ImportsFixed }, which is the one transition that roster admits, and the cause is true: the imports
were fixed in this change.
Worth recording that the rule caught BOTH directions. A missing import refused at the file, and a
discharged debt left in place refused as RosterStale -- so neither the fix nor its bookkeeping could
be half-done silently.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… moved authorities THE TRANSLATE FALLBACK IS REMOVED, and the deciding fact is one I did not have when I argued to keep it: this exact repair already had its own PR, #12355. It was HELD because none of its tests observed the preserved diagnostic chain; its author then tried to construct a discriminating red, found the double-failure arm UNREACHABLE on that base, and recommended closing rather than landing unwitnessed defensive code. #12355 closed unmerged. So it was never a 36-line judgment call. The qualitative test is whether the changed arm has a reachable consumer and a mutation-sensitive control, and it demonstrably has neither -- which is the same standard this session has been applying to everything else: a check that cannot go red is a decoration. I argued to retain code I WROTE on a size argument, which is the bias worth recording beside the revert. It is a v2 module, so no seed mirror had to be re-derived and no "translate-removed-but-mirror-stale" head was possible. Restore it only when current main supplies a concrete double-failure specimen whose complete diagnostic chain changes when the repair is removed. THE MIRROR FIXED POINT IS REACHED AND VERIFIED, not assumed. Pass one drifted exactly one mirror -- v1_compiler_emit_rust.rs, from the P1 redo -- which was installed and rebuilt. Pass two reports first_generation_equal=true and exits 0, and both mirrors were hashed before it ran and verified byte-identical after. That is the boundary stated as "the second pass writes zero bytes", checked rather than inferred from an exit code. THE MOVED-AUTHORITY CENSUS, because line counts show the DIRECTION of an extraction and not semantic uniqueness. "materialization_provider shrank and judgment_contract is absent on main" establishes that declarations moved; it does not establish that each now has one home. Measured: 31 authorities declared in judgment_contract each has EXACTLY ONE declaration corpus-wide (dag, src/v1, src/v2) NONE is also declared in materialization_provider the provider CONSUMES them through import std.judgment_contract So the survivorship row reads: moved authorities have one declaration each; the persistence provider consumes them and no longer defines them. And the conclusion is narrowed to what the evidence supports -- no supersession or duplicate authority was found in the retained demand-engine groups; generated mirrors are re-derived; the unrelated translate fallback was removed -- rather than the broader "nothing is duplicated" that asked line totals to prove semantic uniqueness. Green at the fixed-point head: 27/27 demand engine, 22/22 native schedule, 14/14 cost partition. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
Head
|
| demand engine | 27/27 |
| native schedule | 22/22 |
| cost partition | 14/14 |
| roster judgment | passes in claim_batch's preamble — the check that refused locally before |
| mirror fixed point | first_generation_equal=true, zero writes, hashes verified |
This is a second push where the boundary said exactly one. The alternative was leaving a knowingly-red head on the PR. Recording the reason rather than leaving an unexplained extra head.
Still owed and not claimed at this head: native execution, emitted closure build under -D warnings, direct-vs-engine row equality, a production-sized scheduling-cost receipt inside tolerance, and a one-seat RSS receipt. Seats stay at one.
🤖 Generated with Claude Code
…compiles
THE GENERATED LANE FAILED ON A TEST TARGET I NEVER COMPILED. Adding
ExclusiveDemandScheduling to the row key left two non-exhaustive matches in
src/v1/tests/src/native_driver_cost_refusal_test.rs:
error[E0004]: non-exhaustive patterns:
NativeDriverExclusiveRowKey::ExclusiveDemandScheduling not covered
I HAVE A NOTE ABOUT EXACTLY THIS AND STILL DID NOT RUN THE COMMAND. `cargo build --bin gunbc`
does not compile src/v1/tests, so every local build I ran was blind to it. CLAUDE.md names the
command that is not: `cargo clippy --all-targets -- -D warnings` is "the only command that
compiles the integration-test and example targets, so a red there is invisible to every other
step". The pre-push hook runs cargo fmt, not clippy, so nothing local objected either.
WHAT THE EXHAUSTIVE MATCH DID RIGHT. This is the same construction that forced the driver to
measure the row: a match over the key TYPE with no wildcard refuses to compile until its author
decides what the new row means there. It caught the test targets too -- it just caught them in CI
because that is the only place they were built. The row key's own header in std.compiler_entry
says a wildcard would answer zero for a span nobody wired up; the same reasoning is why these two
fixtures had to say 0 explicitly rather than inherit it.
Verified with the CI command this time, not a --bin build: cargo clippy --all-targets -D warnings
finishes clean.
ALSO CONFIRMED FROM THAT RUN: floor PASSED at 43m9s, so the monotone-roster merge was the right
repair, and the regen phases report first_generation_equal=true and fixed_point_equal=true in CI --
the mirror fixed point I verified locally by hashing holds on the runner as well.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The emitted closure refused to compile where the interpreter had accepted the same source:
error[E0308]: length(run.engine.clone().entries.clone())
expected Rc<im::Vector<_>>, found Rc<im::HashMap<Rc<DemandIdentity>, Rc<DemandEntry<..>>>>
`entries` is keyed by identity now and `entry_order` is the population's enumeration, so three
sites counting the store as a list were wrong: native_demand_run_demand_count in 00_compile, and
two assertions in the engine's own claim file. All three typechecked in .dag -- FreeMonoid is
loose enough interpreted -- and only the emit route caught them, which is the rostered class
accepted_source_emits_uncompilable_target.
Worth recording that the interpreted claims could NOT have caught this: 27/27 passed over the same
source. emit-build is a non-required detector lane and its own log says a red there is a real
finding, most likely the author's. It was.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rivation The two conflicted paths are GENERATED mirrors, which are never hand-merged: main's side is taken so the tree builds, and the regen re-derives them from the merged .dag authorities. That is the same sequence this lane used before -- --theirs, build, regen, install, confirm a zero-write second pass -- and not a content decision about either file.
The merge took main's side for two GENERATED mirrors so the tree would build, and the regen then re-derived both from the merged .dag. This commits that re-derivation: without it the branch carries main's mirrors against this lane's emitter source, which is exactly the drift the generated lane refuses. Caught by reading git status before claiming the push was complete -- the candidates had been installed into the worktree and rebuilt against, but never committed, so the head pushed a moment ago carried main's mirrors. Verified after: regen pass two reports first_generation_equal=true and rewrites no mirror, with every hash checked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 30, 2026
…demand engine as its own demand kind NativeOccurrenceCensusSubject depends on the module's resolve demand; its identity is the census artifact kind over the module digest plus the compiler (what the resolved tree it reads depends on); no cache or provider; observation only; scheduled and refused through the engine's existing arms. Its cost is the engine-attributed ExclusiveOccurrenceCensus row, beside main's ExclusiveDemandScheduling. Demand-engine change approved by neat-boar-16 in the absence of #12401's owner (operator lane). Generated stage0 mirror to be regenerated. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 30, 2026
…he xl2 census fold Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Sep 30, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Integrate the demand engine into the production native driver.
Head
cf82073563e. Reconciled against main, both review defects repaired, engine locality fixed and measured, generated mirrors at a verified fixed point. The September 27 checkpoint is preserved in a collapsed section at the bottom and in two tags; it is historical evidence and does not qualify this head.The two review defects
P1 — the scheduler's own work was unattributed, and that was a correctness defect.
schedule_plan_startedopened, covered onlynative_demand_tested_tree_input, and closed beforenative_demand_schedule_universeran — so plan construction, ready selection, binding lookup, settlement, readiness recomputation and row collection all fell into the parent residual. The tolerance arm is a fixed 50 ms, so a large enough universe made an otherwise valid adjudication exitNativeDriverCostRemainderExceedsTolerance: a fail-closed refusal fired by correct input.std.compiler_entrygainsExclusiveDemandScheduling, and because the driver's match over that key is exhaustive with no wildcard, adding the row forced the driver to say what measures it — which is why that match was written without one.The measurement is taken where the work happens, inside the engine, through the same clock seam the demand's own window uses:
native_demand_schedule_universenative_demand_drain, aroundnative_demand_nextnative_demand_step, before the demand window opensnative_demand_step, after it closesA first attempt at this was wrong and is recorded because the failure mode is reusable: it timed the whole scheduling call and subtracted prepare+eval. That is a residual wearing a row's clothes — it overlaps the spans it subtracts and absorbs any other unattributed phase, so the remainder could no longer discover a second missing row. A row defined as a residual cannot be the thing that proves the residual is small.
P2 — a module failing at resolve was counted twice. Its resolve transition carries the decided rows as its value (a real refusal); the dependent infer demand then settles
DemandRefusedwith no value — it never executed — and the blanket arm counted it again.prepare_refusedreported 2 where the module-level count was 1.Preparation standing is now decided once per module at the infer demand. There is exactly one infer demand per module, so the count cannot scale with declarations.
DemandRefusedfrom a failed resolution is still refused, because the module's preparation did not succeed and that is what the old count meant.Also wrong once: a second attempt fixed the total by dropping the infer settlement instead — the wrong half. It left the count per-transition rather than per-module, and renamed a resolution failure to something other than a refused preparation to make arithmetic work.
Four controls, one per way a module reaches that boundary. The load-bearing one: counts do not scale with the declaration count, which is what would have caught the original shape.
The engine's cost shape
The law is "a completion re-evaluates its DIRECT dependents." The module's own header admitted the check could not see the other half — it "counts DERIVATIONS, not entries visited", and "locating the dependents is a scan of the relation list". So a whole-population scan and a targeted update reached identical states and identical counts.
Same out-degree, 5-demand graph versus 45.
demand_engine_relate— the single site a relation enters — maintainsdependents_ofandprerequisites_of. No reader walks the relation list any more.entriesis keyed by identity;entry_ordercarries insertion order separately. Settlement is a lookup and an insert instead of a population rewrite.demand_engine_nextreads the head of a maintained canonical order;in_flightis a maintained count. Both were whole-population filters, andnextalso sorted the survivors on every admission.Whole-population passes that remain are the ones the law does not claim are local — seal and reevaluate — and both route through one named helper so a third cannot hide inside a supposedly-local function.
The claim is at the entry-visitation grain, not wall time. What the counter establishes is that settlement visits the settled entry and its direct dependents and nothing else. It does not establish constant-time operations: a keyed persistent map may carry tree-depth cost and an ordered set logarithmic insertion. "Costs its out-degree, not the graph" is sound about graph work; "O(out-degree) wall time" would claim more than the evidence supports.
Two findings worth keeping
demand_engine_in_flightfiltered the whole population for a state nothing produces. No producer in this corpus setsDemandRunning, so that walk computed a constant zero on every admission. It is still derived from state rather than hardcoded — a literal would be correct today and a fail-open the moment a producer lands.DemandRunningis therefore a declared frontier, with its producer named: the admission path returning the engine it changed, which cannot exist becausedemand_engine_nextanswers aDemandAdmissionand not an engine. That is the same structural gap that made an inspection counter unreadable — one missing return, two dangling declarations. Trigger: multi-seat realization.A counter I wrote and deleted.
ready_inspectedwas added to make the admission claim observable, then removed:nextreturns an admission, so no caller could read it — a field nothing writes, which §3c forbids. What it was a proxy for is asserted directly and is sharper: the maintained ready order equals what a full rebuild would produce, across a seal and three settlements including a refusal, in a 45-demand graph. Drift there would admit a stale identity while every count looked fine.Survivorship against main
.dagfold read the clock undergunbc runand panicked in the emitted binaryExclusiveDemandSchedulingThe moved-authority census: 31 authorities in
judgment_contract, each with exactly one declaration corpus-wide, none also declared inmaterialization_provider, which imports them.No supersession or duplicate authority was found in the retained demand-engine groups; generated mirrors are re-derived; the unrelated translate fallback was removed.
The translate fallback was dropped, and not because it was small. This exact repair already had its own PR, #12355, held because none of its tests observed the preserved diagnostic chain — its author then found the double-failure arm unreachable on that base and recommended closing rather than landing unwitnessed defensive code. It closed unmerged. Restore it only when main supplies a concrete double-failure specimen whose complete diagnostic chain changes when the repair is removed.
Evidence at this head
first_generation_equal=true, exit 0, both mirrors hashed before and verified byte-identical afterTwo merge consequences were found only by re-running at this head: main tightened the unimported-bare-provider rule, so the partition witness needed an explicit
v2.std.live_treeimport, and fixing that import made its debt row stale, which the rule then refused in the other direction asRosterStale. Both directions caught — neither the fix nor its bookkeeping could be half-done silently.Still owed before merge, and not claimed here: native execution, emitted closure build under
-D warnings, direct-scheduler versus engine-scheduler row equality, a production-sized scheduling-cost receipt inside tolerance, and a one-seat RSS receipt. Seats stay at one; multi-seat, materialization consumption and payload lifetime remain out of scope.Historical heads:
checkpoint/12401-pre-reconciliation,checkpoint/12401-native-qualification.Historical: the September 27 checkpoint body (superseded)
Publish the production demand-scheduler integration checkpoint
44419a1ef94before native execution qualification. Base remains40398151be49. No rebase has been performed.The original host-local receipt is preserved unchanged (SHA-256
66296268c591e6108bd4da371c58640e5ce467e4cd61813a2002e388416bbea6). Its publication status is superseded: this exact head is now pushed. Its “semantic equality” section establishes emitted-source preservation for the compared subjects, not integrated scheduling equivalence. Clock labels are metadata/prophylaxis on the measured routes, not an established anti-memoization mechanism. Native execution qualification is now published in the checkpoint receipt: real positive/negative native execution and exact direct/engine result equality, while all seven retain their located Context refusals. Seats remain one; no payload-lifetime advance is claimed.Original checkpoint receipt (historical wording preserved)
Demand-engine integration receipt
integration base: 4039815 (main when the branch was cut; PINNED, not chased)
integrated head: 44419a1 (branch lane/demand-integration, 7 commits)
published: origin/lane/demand-integration at 44419a1 (identical to local; not rebased).
Groups, in dependency order
Compiles, each module as its own entry closure at the base
judgment_contract 0 | materialization_provider 0 | demand_engine 0 | demand_engine_test 0
04_method 0 | runtime_rust 0 | rust/emit 0 | 06_translate 0
00_compile 0 | native_demand_schedule_test 0 | 05_emit_rust 0
All exit=0, 0 blocking errors.
Claims, executed: 77 requested, 77 reported, 0 absent
materialization_provider_witness_test 48/48 PASS exit=0
demand_engine_test 15/15 PASS exit=0
native_demand_schedule_test 14/14 PASS exit=0
Negative paths are INSIDE that population, not beside it: a reversed elapsed reading
is invalid rather than zero; an invalid or unclassified reading makes the observation
INCOMPLETE rather than silently totalling; a blocked demand contributes no transition;
a refused prerequisite blocks its dependent; a fresh effect is never attached; a kind
outside the contracts is counted rather than dropped; rendering the receipt moves no total.
Identity encoding: PRESERVED
All five moved bodies -- length_prefixed_encode/_decode, demand_identity_canonical/_decode,
string_from_code_points -- are byte-identical to the versions in main's
materialization_provider, so the format is preserved by construction. Confirmed by
execution: demand_canonical_encoding_is_injective_and_c1_lossy_collapses PASS,
8945 eval steps, subject db6a37d1d8939ed4.
Nat boundary: no widening authored
count/length in METHOD position type through v1.compiler.infer_method's builtin registry
from the algebra templates, every one of which declares return_type std.nat.Nat. So
v2.std.algebra.length -> Int is not on that path. Eight sites in the contract group cross
into to_string, into a comparison against a parse_int result, and into take/skip which
declare Int; the front end accepts all eight, so nothing was cast -- a widening nobody
needs would discard the nonnegativity the contract carries. The engine's five sites are
the opposite case: they call length as a FREE function, which genuinely returns Int.
Established from call form and declarer, never from the spelling.
Emitted-source preservation holds for the compared subjects
This establishes EMITTED-SOURCE PRESERVATION for these two subjects, and NOT execution
equivalence on the integrated native route, which remains unqualified.
Control = base binary, treatment = integrated binary, identical source subject.
src/v2/compiler/03_resolve.dag 115/116 files byte-identical
src/v2/cli/compile_cli.dag 179/180 files byte-identical
The single differing file in each is v1_rt.rs: 26 diff lines, ALL additions, ZERO
deletions, every one the clock body. Nothing else moved.
Route switch: proved in emitted bytes
Neither comparison above exercises it -- main.rs is byte-identical in both, because the
engine call is in emit_source_root_eval_driver_main_rs while 03_resolve renders a library
stub and compile_cli renders NativeCliDriver. The subject that shows it is the 00_compile
closure, which declares compiler_pipeline_entry = SourceRootEvalDriver.
treatment main.rs calls native_demand_schedule_universe (1004 lines)
control main.rs does not; it runs the per-module loop (1015 lines)
Removed from the rendered main:
for entry in universe.modules.iter()(1 -> 0) and itsper-module
[native-prepare-split]telemetry (1 -> 0). That establishes REMOVAL OF THATINSTRUMENTATION SITE. It does NOT establish that the replacement observation accounts for
every executed demand -- that needs execution, not a source diff.
prepare_total_nanos goes 1 -> 2 and that is NOT a surviving scheduler: one site times the
plan construction the engine introduces, charged honestly to prepare, and the other takes
the engine's rollup native_demand_prepare_nanos(run).max(0) instead of accumulating inside
a loop. prepare_samples survives for the same reason -- the samples come from
native_demand_prepare_samples(run). The .max(0) is the caller-side saturating obligation
the runtime body's own contract states.
Emitted clock: qualified by execution
Regenerated mirror installed, binary rebuilt, specimen fold emitted to Rust, built and RUN:
emitted_clock_monotone=true, emitted_clock_span_nanos=80, exit 0. This is the first
evidence the clock works on the route the native compiler uses; the class is green under
gunbc runand panics in the emitted binary, so interpreted execution establishes nothingabout it. Specimen sources kept out of the repo at
~/.claude/jobs/4f204954/tmp/specimen-src/ (an untracked .dag under the tree has broken
local builds before).
Retained obligations -- NOT discharged by this integration
ways: same-label spans are nonzero in the emitted route (240 distinct vs 80 same), and
the interpreted claim same_label_span_is_zero_under_the_interpreter FAILED, so nothing
on either reachable route memoizes these calls. The comment is a purpose statement and
remains true as one; it discharges no evidence obligation and its same-label arm is not
a discriminating red.
bridge HAS a body; a body returning a constant zero would pass it and fail the specimen.
Different properties. Enrolling a behavioural instrument is a roster decision, named here
rather than taken.
observation, and production consumption of admitted materialization decisions all remain
open. Seats stay at 1: nothing here measures an incremental per-seat working set, and a
small one-seat RSS reading would not qualify the lifetime model.
Landing boundary
Main has moved past 4039815. Reconcile there and decide which evidence needs renewal;
the semantic-equality and route-switch receipts above are properties of THIS candidate.
Per-claim outcomes, retained beside the counts
materialization_provider_witness_test (48 requested / 48 reported, exit=0)
PASS request_kinds_ground_on_cache_identity_rows
PASS request_key_is_deterministic
PASS declared_input_identity_is_in_the_key
PASS request_kind_is_in_the_key
PASS complete_verified_artifact_serves_as_hit
PASS absent_probe_is_a_miss
PASS red_kind_mismatch_refuses_even_on_matching_key_and_content
PASS red_declared_input_miss_stale_artifact_refuses_as_wrong_artifact
PASS red_wrong_content_refuses_never_hits
PASS red_sha256_at_fnv1a64_seam_refuses_without_alias
PASS stored_disk_probe_admitted_fnv_parts_refuse_unqualified_persisted_format
PASS incomplete_v1_shape_artifact_refuses_naming_the_diagnostic_union
PASS admission_within_budget_is_admitted_without_eviction
PASS admission_over_budget_evicts_least_recent_and_counts_it
PASS admission_of_oversized_artifact_is_budget_exhausted
PASS red_admission_derives_completeness_from_request_v1_shape_refused
PASS red_admission_kind_mismatch_is_refused
PASS red_admission_stale_key_is_refused_as_wrong_artifact
PASS red_admission_wrong_content_is_refused
PASS red_forged_output_roster_refuses_as_wrong_content_on_serve
PASS red_forged_output_roster_refuses_as_wrong_content_on_admit
PASS carried_roster_is_the_content_digest_preimage
PASS understated_bytes_alone_hold_every_part_digest_fixed
PASS red_understated_bytes_are_inside_the_authenticated_preimage
PASS red_understated_bytes_alone_are_refused_wrong_content_not_admitted
PASS artifact_size_is_the_carried_parts_fold
PASS red_understating_the_size_lands_on_wrong_content_not_a_budget_bypass
PASS typecheck_request_key_is_the_existing_typed_module_key_authority
PASS red_typecheck_key_tracks_the_authority_when_an_import_changes
PASS complete_artifact_reaches_its_union_through_a_required_field
PASS v1_incompleteness_is_a_named_variant_not_a_missing_list_element
PASS completeness_holds_when_all_required_outputs_are_carried
PASS consumer_target_frontier_names_seven_caches_with_typed_binds
PASS served_hit_carries_a_derived_structural_grade
PASS red_identity_cannot_be_asserted_only_derived
PASS incomplete_artifact_derives_unknown_identity
PASS six_judgment_contracts_join_the_cache_identity_kinds
PASS provider_serve_completeness_reads_the_judgment_contract
PASS parse_and_typecheck_store_addresses_are_preimage_verified_fnv_buckets
PASS admitted_store_address_carries_the_request_bucket_digest_and_preimage
PASS persist_sha1_bucket_is_typed_family_refused
PASS in_process_probe_same_bucket_foreign_identity_is_not_a_hit
PASS in_process_fnv_producer_observation_is_declared_frontier
PASS demand_canonical_encoding_is_injective_and_c1_lossy_collapses
PASS structural_fingerprint_refuses_as_cross_run_store_key
PASS evaluation_result_binding_same_eval_different_content_is_conflict
PASS evaluation_result_binding_same_preimage_different_bucket_is_unverifiable
PASS two_parses_occurrence_qualification_is_an_explicit_frontier
demand_engine_test (15 requested / 15 reported, exit=0)
PASS diamond_join_waits_for_both_prerequisites_holds
PASS independent_peer_does_not_delay_a_dependent_holds
PASS refused_prerequisite_blocks_its_dependent_holds
PASS cycle_is_reported_as_a_cycle_holds
PASS missing_edge_is_reported_holds
PASS share_admitted_demand_is_produced_once_holds
PASS fresh_effect_is_never_attached_holds
PASS no_seat_leaves_the_demand_ready_holds
PASS ready_queue_order_is_canonical_holds
PASS undemanded_judgment_is_outside_the_closure_holds
PASS branch_selector_demands_exactly_one_arm_holds
PASS completion_order_records_what_settled_holds
PASS a_completion_costs_its_out_degree_not_the_graph_holds
PASS sealing_derives_readiness_once_per_demand_holds
PASS a_sealed_cycle_verdict_survives_unrelated_completions_holds
native_demand_schedule_test (14 requested / 14 reported, exit=0)
PASS a_module_derives_one_demand_per_stage_and_one_per_declaration_holds
PASS only_resolve_is_ready_before_anything_settles_holds
PASS a_refused_inference_blocks_every_identity_on_the_named_prerequisite_holds
PASS one_declaration_name_in_two_modules_is_two_demands_holds
PASS the_two_module_stages_are_distinct_demands_holds
PASS the_compiler_input_is_part_of_the_demand_identity_holds
PASS a_demand_kind_outside_the_contracts_is_counted_not_dropped_holds
PASS resolve_and_infer_are_prepare_and_eval_is_eval_holds
PASS cost_class_follows_the_kind_not_the_subject_holds
PASS a_blocked_demand_contributes_no_transition_holds
PASS rendering_the_receipt_does_not_move_any_total_holds
PASS an_unclassified_transition_makes_the_observation_incomplete_holds
PASS a_reversed_elapsed_reading_is_invalid_not_zero_holds
PASS an_invalid_elapsed_reading_makes_the_observation_incomplete_holds
the clock label probe, recorded because one arm FAILED by design
FAIL same_label_span_is_zero_under_the_interpreter (span was NOT zero -- no collapse)
PASS distinct_label_span_is_nonzero_under_the_interpreter
emitted route: distinct_label_span=240 same_label_span=80 monotone=true exit=0
Reading: the label is METADATA / PROPHYLAXIS on both measured routes, NOT an
established anti-memoization mechanism.
Individual claim outcomes retained from the original logs
w3.log
SHA-256
6eb85d0283645a184683ac5cb281567355589f57ff5e58a6d43c8fa01e41c46be_run.log
SHA-256
5b38e02620b37afea6be1f1a17c5491f9cf5bdb6643611d47addc255b11f4610n_run.log
SHA-256
c701837d4d1d1bc1c9e90ed875db0eac1230f23dfeb2ac66aad7e04c82766f72Retained emitted artifact identities
Each tree digest below hashes sorted relative file paths, a NUL, file SHA-256, and newline for every emitted source/manifest file. These identify the retained bytes; they do not upgrade source comparisons into execution evidence.
ab_control:ced24b9511c5c1f6b04efb1ddf0dde2cc7f8b827faffbb6f60f1daf1f056e80fab_treat:b55261547e918447582ed3770449f210e69688cb6fda323d9aaa959ed05e512ccli_control:b0974fc772e0613627d5baf5ef0123f81231cbed8a77438b3386ef71281e634acli_treat:af89cc4fa97c7136572cfb0bd80ad69d200e8ed5bc7d8f096b26e4643628a925main_control:3db88dba142ba65313ead6b2b3a4619ef43f9069b8016138a4132a4fec61de2bmain_treat:73174ff912c2bdda12cacd758a145886221b6efb69626cf49e1b18b8a5137d41Recovered original commands
Recovered from the authoring transcript; historical reported exits remain zero. These are commands that produced the retained evidence, not new executions.
🤖 Generated with Claude Code