diff --git a/dag/gunbc/floor/floor_call_site_demand_seed_growth.dag b/dag/gunbc/floor/floor_call_site_demand_seed_growth.dag index 15aeb7e69d0..e8ce1598c37 100644 --- a/dag/gunbc/floor/floor_call_site_demand_seed_growth.dag +++ b/dag/gunbc/floor/floor_call_site_demand_seed_growth.dag @@ -53,9 +53,11 @@ data floor_call_site_demand_seed_growth_justification: SeedGrowthJustification = DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_NET_ONLY_SITES", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_STORE_DECLINES", field: WholeDeclaration }, DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "cross_claim_store_declines", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "note_cross_claim_store_outcome", field: WholeDeclaration } + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "note_cross_claim_store_outcome", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run.claim_call_site_demand", decl_name: "ConsumerRead", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.cli_run.claim_call_site_demand", decl_name: "ConsumerReadCause", field: WholeDeclaration } ], - reason: "WHAT THIS REPLACES, and why the change is a deletion first. Cross-claim pure-share admission was a hand-authored roster of 575 warm and 5 claim-forced qualified spellings in v2.workflow.floor_pure_producer_share, a second authority over a fact the demand graph carries (DESIGN section 3). Any witness module whose claims re-ran a module-constant producer had to be hand-restructured or hand-rostered before it fit its enrolment margin (gunbc#13030 C3; gunbc#12506 the live case). The roster, its pending-candidate shape, its two collision walls and the seed's plain warm loop (warm_cross_claim_pure_producer, PureProducerWarmRefusal) are deleted in the same change, and admission is now v2.workflow.floor_pure_producer_share derive_cross_claim_share over this observer's rows.\n\nWHY RUST IS STILL NEEDED, and it is one fact: no .dag carrier yet hands the floor PER-CLAIM CALL-SITE DEMAND IDENTITY -- the call sites a planned claim reaches, each with its callee declaration and the canonical preimage of its argument row. DESIGN section 3b's keys row lists demand identity as a declared frontier of demand-engine M1.b, and the floor does not give .dag the claim bodies as values; deriving them in .dag would re-parse and resolve the closure in the interpreter per run. So the seed observes, as one realization of the .dag row type CallSiteDemandObservation, and the operator ruling for this lane (sharp-raven-357, 2026-10-02) admits it on exactly that condition.\n\nWHAT IS NOT GROWN: no admission policy. The seed counts distinct planned claims per identity -- a fact across the claim-frame boundary only it can see -- and decides nothing: the two-claim threshold, the identity grade, and the refused and carried-input exclusions are the .dag fold's, and the seed refuses if the fold's partition does not reconcile with the observed closed rows. No widening: a call whose callee is unresolved or effectful, or whose argument row is not closed, is counted under its CallSiteDemandCause and never admitted. No warm: an admitted site fills on the first planned claim that evaluates it (its wall is excused from the claim's wall deadline only in proportion to the evaluator steps it has performed, at the declared ceiling floor_cross_claim_fill_wall_per_step_ceiling, under the preparation wall safety limit as the outer hard cap, so a stalled fill and a runaway one both still interrupt, naming the producer, its steps and its wall; the declared cost floor is applied to the fill's own steps at retention), netted from that claim's clocks and eval steps through the existing CrossClaimFillGuard, so a statically reached site no claim evaluates costs nothing (which also discharges gunbc#13030 C3 part 1: nothing outside the planned claims' reach is filled). No new correctness dependence: the tier still keys every store on the evaluated argument values and verifies the stored preimage before any serve, so a misjudged site costs a missed share or a wasted store, never a wrong value.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program, and the required floor gates every v2 change. Seed growth here is realization only -- the observer, the site-gated admission set and its check, and the install -- which is the condition the ruling set.\n\nREDS ENROLLED: claim_call_site_demand tests a_constant_reached_by_two_claims_counts_two_and_a_private_one_counts_one (the discriminating pair, with a claim calling the shared helper twice still counting once), an_unplanned_claim_contributes_no_demand, a_parameter_bound_argument_is_counted_open and an_effectful_callee_is_counted_under_its_cause; v1_interpreter a_derived_producer_is_admitted_only_at_its_admitted_sites (the pair varies only the call site, with an ungated control), a_derived_fill_below_the_cost_floor_is_declined_and_one_above_is_stored (the pair varies only the floor) and a_stalled_in_flight_fill_is_excused_nothing_and_a_working_one_by_its_steps (the stalled control); the decision's REDs are .dag, in v2.test.floor.pure_producer_share_refusal.\n\nTHE SINGLE-CLAIM FILL DEBT JOIN (sharp-raven-357 ruling A, 2026-10-03): v2.workflow.floor_pure_producer_share floor_single_claim_fill_debt is a monotone debt set of claims whose own fixture fill is netted from their budget, each admission reported with basis SingleClaimFillDebt naming the claim. The .dag fold decides which one-claim identities are admitted on a member's behalf; derive_and_install_cross_claim_share realizes the identity join -- a PLANNED active member with no admitted fixture identity refuses SingleClaimFillDebtStale -- and adds no declaration for it. The decision's REDs are .dag (an_active_debt_members_fixture_is_admitted_and_names_its_claim against its retired and non-member controls).\n\nNET-ONLY SITES AND THE DECLINE REPORT: a single-claim fill debt site is netted from its one claim and its value is NOT retained (publish_cross_claim_fill, CROSS_CLAIM_NET_ONLY_SITES), because retaining values only one claim ever demands exhausted the tier byte budget on floor probe 37142207751 and left the declined fills on their claims; and every store the tier declines is reported per producer and cause ([cross-claim-share-store-declined], [cross-claim-share-tier]). RED: a_net_only_fill_is_netted_without_retaining_its_value.\n\nTHE UNATTRIBUTED HITS ARE NAMED BY KEY (sharp-raven-357's condition): the shared-fill ledger's unattributed_hits aggregate is now also rendered one line per (frame, phase, cache, key) through gunbc.observation_ci_render ci_shared_fill_unattributed_text and its seed mirror render_shared_fill_unattributed_text_mirror, so whether preparation reads a producer is answerable by identity. REDs: shared_fill a_hit_with_no_recorded_fill_is_counted_never_dropped (in-claim frame) and a_hit_outside_the_fold_is_named_by_key_and_frame; .dag w_shared_fill_unattributed_line_names_frame_phase_and_key.", + reason: "WHAT THIS REPLACES, and why the change is a deletion first. Cross-claim pure-share admission was a hand-authored roster of 575 warm and 5 claim-forced qualified spellings in v2.workflow.floor_pure_producer_share, a second authority over a fact the demand graph carries (DESIGN section 3). Any witness module whose claims re-ran a module-constant producer had to be hand-restructured or hand-rostered before it fit its enrolment margin (gunbc#13030 C3; gunbc#12506 the live case). The roster, its pending-candidate shape, its two collision walls and the seed's plain warm loop (warm_cross_claim_pure_producer, PureProducerWarmRefusal) are deleted in the same change, and admission is now v2.workflow.floor_pure_producer_share derive_cross_claim_share over this observer's rows.\n\nWHY RUST IS STILL NEEDED, and it is one fact: no .dag carrier yet hands the floor PER-CLAIM CALL-SITE DEMAND IDENTITY -- the call sites a planned claim reaches, each with its callee declaration and the canonical preimage of its argument row. DESIGN section 3b's keys row lists demand identity as a declared frontier of demand-engine M1.b, and the floor does not give .dag the claim bodies as values; deriving them in .dag would re-parse and resolve the closure in the interpreter per run. So the seed observes, as one realization of the .dag row type CallSiteDemandObservation, and the operator ruling for this lane (sharp-raven-357, 2026-10-02) admits it on exactly that condition.\n\nWHAT IS NOT GROWN: no admission policy. The seed counts distinct planned claims per identity -- a fact across the claim-frame boundary only it can see -- and decides nothing: the two-claim threshold, the identity grade, and the refused and carried-input exclusions are the .dag fold's, and the seed refuses if the fold's partition does not reconcile with the observed closed rows. No widening: a call whose callee is unresolved or effectful, or whose argument row is not closed, is counted under its CallSiteDemandCause and never admitted. No warm: an admitted site fills on the first planned claim that evaluates it (its wall is excused from the claim's wall deadline only in proportion to the evaluator steps it has performed, at the declared ceiling floor_cross_claim_fill_wall_per_step_ceiling, under the preparation wall safety limit as the outer hard cap, so a stalled fill and a runaway one both still interrupt, naming the producer, its steps and its wall; the declared cost floor is applied to the fill's own steps at retention), netted from that claim's clocks and eval steps through the existing CrossClaimFillGuard, so a statically reached site no claim evaluates costs nothing (which also discharges gunbc#13030 C3 part 1: nothing outside the planned claims' reach is filled). No new correctness dependence: the tier still keys every store on the evaluated argument values and verifies the stored preimage before any serve, so a misjudged site costs a missed share or a wasted store, never a wrong value.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program, and the required floor gates every v2 change. Seed growth here is realization only -- the observer, the site-gated admission set and its check, and the install -- which is the condition the ruling set.\n\nREDS ENROLLED: claim_call_site_demand tests a_constant_reached_by_two_claims_counts_two_and_a_private_one_counts_one (the discriminating pair, with a claim calling the shared helper twice still counting once), an_unplanned_claim_contributes_no_demand, a_parameter_bound_argument_is_counted_open and an_effectful_callee_is_counted_under_its_cause; v1_interpreter a_derived_producer_is_admitted_only_at_its_admitted_sites (the pair varies only the call site, with an ungated control), a_derived_fill_below_the_cost_floor_is_declined_and_one_above_is_stored (the pair varies only the floor) and a_stalled_in_flight_fill_is_excused_nothing_and_a_working_one_by_its_steps (the stalled control); the decision's REDs are .dag, in v2.test.floor.pure_producer_share_refusal.\n\nTHE SINGLE-CLAIM FILL DEBT JOIN (sharp-raven-357 ruling A, 2026-10-03): v2.workflow.floor_pure_producer_share floor_single_claim_fill_debt is a monotone debt set of claims whose own fixture fill is netted from their budget, each admission reported with basis SingleClaimFillDebt naming the claim. The .dag fold decides which one-claim identities are admitted on a member's behalf; derive_and_install_cross_claim_share realizes the identity join -- a PLANNED active member with no admitted fixture identity refuses SingleClaimFillDebtStale -- and adds no declaration for it. The decision's REDs are .dag (an_active_debt_members_fixture_is_admitted_and_names_its_claim against its retired and non-member controls).\n\nNET-ONLY SITES AND THE DECLINE REPORT: a single-claim fill debt site is netted from its one claim and its value is NOT retained (publish_cross_claim_fill, CROSS_CLAIM_NET_ONLY_SITES), because retaining values only one claim ever demands exhausted the tier byte budget on floor probe 37142207751 and left the declined fills on their claims; and every store the tier declines is reported per producer and cause ([cross-claim-share-store-declined], [cross-claim-share-tier]). RED: a_net_only_fill_is_netted_without_retaining_its_value.\n\nTHE UNATTRIBUTED HITS ARE NAMED BY KEY (sharp-raven-357's condition): the shared-fill ledger's unattributed_hits aggregate is now also rendered one line per (frame, phase, cache, key) through gunbc.observation_ci_render ci_shared_fill_unattributed_text and its seed mirror render_shared_fill_unattributed_text_mirror, so whether preparation reads a producer is answerable by identity. REDs: shared_fill a_hit_with_no_recorded_fill_is_counted_never_dropped (in-claim frame) and a_hit_outside_the_fold_is_named_by_key_and_frame; .dag w_shared_fill_unattributed_line_names_frame_phase_and_key.\n\nTHE CONSUMER-READ FACT (bundle refusal, follow-up to gunbc#13043): the observer also reports, per distinct (claim, read), what the expression consuming a closed call site reads off its result -- the field projected immediately off the call, the whole value, or ConsumerReadUnobserved with its ConsumerReadCause when a projection's field name cannot be read -- as one realization of the .dag ClaimConsumerRead / ConsumerRead row types (ConsumerRead here). It decides nothing: the bundle refusal (BundleOfDisjointProjections, ConsumerReadUnknown) is derive_cross_claim_share's, and an unreadable read is declined there, never widened to the whole value. Same reason Rust is needed as the call sites themselves: the claim bodies are not .dag values. RED: claim_call_site_demand each_claims_immediate_projection_is_reported_once_and_a_bare_use_reads_the_whole; the decision's REDs are .dag (two_claims_reading_disjoint_projections_are_declined_as_a_bundle against its same-field and mixed controls).", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, trigger: "Delete the observer (claim_call_site_demand and derive_and_install_cross_claim_share's observation half) when per-claim call-site demand identity is available to .dag: demand-engine M1.b's demand-identity carrier produces CallSiteDemandObservation rows for the planned claims, so the derivation reads them from a modeled carrier and no host walk remains. The site-gated admission set and its check retire with the cross-claim tier itself (gunbc.cross_claim_pure_share_seed_growth's trigger), not with this one.", current_boundary: "v1_compiler.cli_run.required_floor_runner planned claims -> v1_compiler.cli_run.claim_call_site_demand CallSiteDemandObserver observe -> v2.workflow.floor_pure_producer_share floor_cross_claim_share_derivation -> v1_compiler.cli_run derive_and_install_cross_claim_share -> v1_compiler.v1_interpreter install_cross_claim_derived_share / cross_claim_site_admitted -> [floor-phase] phase=cross-claim-share-derivation and [cross-claim-share-admitted] lines" diff --git a/dag/test/claim/namespace_xl2_rehearsal_census_witness_test.dag b/dag/test/claim/namespace_xl2_rehearsal_census_witness_test.dag index 2a9b194987a..7ccc9f66722 100644 --- a/dag/test/claim/namespace_xl2_rehearsal_census_witness_test.dag +++ b/dag/test/claim/namespace_xl2_rehearsal_census_witness_test.dag @@ -90,43 +90,57 @@ fn xl2_unstripped(sources: List) -> Xl2Strip { } } -type Xl2ControlRuns { - cut: Xl2RehearsalRun - two: Xl2RehearsalRun - pre_cut: Xl2RehearsalRun - duplicated: Xl2RehearsalRun - nesting: Xl2RehearsalRun -} - -// ONE NULLARY PRODUCER, WARM, FOR ALL FIVE RUNS (v2.workflow.floor_pure_producer_share carries its -// row): each run is a front end plus its resolves, more than one claim's budget, and the first cut -// of this file paid two of them inside claims and was refused over budget on the floor. -fn xl2_control_runs() -> Xl2ControlRuns { - let provider = xl2_control_source(path: "dag/xl2_control_provider.dag", content: xl2_provider_control_source) - let residual = xl2_control_source(path: "dag/xl2_control_residual.dag", content: xl2_residual_control_source) - let clean = xl2_control_source(path: "dag/xl2_control_clean.dag", content: xl2_clean_control_source) - Xl2ControlRuns { - cut: xl2_control_rehearse(strip: xl2_strip_members(sources: [provider, residual, clean])), - two: xl2_control_rehearse(strip: xl2_strip_members(sources: [ - provider, - xl2_control_source(path: "dag/xl2_control_two.dag", content: xl2_two_failure_control_source) - ])), - pre_cut: xl2_control_rehearse(strip: xl2_unstripped(sources: [provider, residual])), - duplicated: xl2_control_rehearse(strip: xl2_strip_members(sources: [ - xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_residual_control_source), - xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_clean_control_source), - clean - ])), - nesting: xl2_control_rehearse(strip: xl2_strip_members(sources: [ - provider, - xl2_control_source(path: "dag/xl2_control_nested.dag", content: xl2_nested_control_source) - ])) - } +// ONE NULLARY PRODUCER PER RUN, each a front end plus its resolves. They were one record whose +// claims each read a different field, which the derived share now declines as a bundle +// (v2.workflow.floor_pure_producer_share BundleOfDisjointProjections): sharing it netted every +// claim's own run out of that claim's budget. Now `xl2_cut_run` is the one value four claims +// demand, shared by demand; each other run is its one claim's own fixture, carried as that claim's +// floor_single_claim_fill_debt membership rather than hidden inside a shared record. +fn xl2_provider_fixture() -> FixtureSource { + xl2_control_source(path: "dag/xl2_control_provider.dag", content: xl2_provider_control_source) +} + +fn xl2_residual_fixture() -> FixtureSource { + xl2_control_source(path: "dag/xl2_control_residual.dag", content: xl2_residual_control_source) +} + +fn xl2_clean_fixture() -> FixtureSource { + xl2_control_source(path: "dag/xl2_control_clean.dag", content: xl2_clean_control_source) +} + +fn xl2_cut_run() -> Xl2RehearsalRun { + xl2_control_rehearse(strip: xl2_strip_members(sources: [xl2_provider_fixture(), xl2_residual_fixture(), xl2_clean_fixture()])) +} + +fn xl2_two_run() -> Xl2RehearsalRun { + xl2_control_rehearse(strip: xl2_strip_members(sources: [ + xl2_provider_fixture(), + xl2_control_source(path: "dag/xl2_control_two.dag", content: xl2_two_failure_control_source) + ])) +} + +fn xl2_pre_cut_run() -> Xl2RehearsalRun { + xl2_control_rehearse(strip: xl2_unstripped(sources: [xl2_provider_fixture(), xl2_residual_fixture()])) +} + +fn xl2_duplicated_run() -> Xl2RehearsalRun { + xl2_control_rehearse(strip: xl2_strip_members(sources: [ + xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_residual_control_source), + xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_clean_control_source), + xl2_clean_fixture() + ])) +} + +fn xl2_nesting_run() -> Xl2RehearsalRun { + xl2_control_rehearse(strip: xl2_strip_members(sources: [ + xl2_provider_fixture(), + xl2_control_source(path: "dag/xl2_control_nested.dag", content: xl2_nested_control_source) + ])) } // RED CONTROL: the residual module yields exactly one failure chain, and it is that module's. test fn xl2_residual_control_is_reported_holds() -> Bool { - match xl2_control_runs().cut { + match xl2_cut_run() { Xl2RehearsalObserved { residual: residual } => count(residual) == 1 && all(residual, r => r.module == "v2.xl2_control_residual") _ => false @@ -135,7 +149,7 @@ test fn xl2_residual_control_is_reported_holds() -> Bool { // GREEN CONTROL: the provider and the clean module both resolved, and neither contributed a row. test fn xl2_clean_control_resolves_holds() -> Bool { - match xl2_control_runs().cut { + match xl2_cut_run() { Xl2RehearsalObserved { residual: residual, resolved_module_count: n } => n == 2 && !any(residual, r => r.module == "v2.xl2_control_clean" || r.module == "v2.xl2_control_provider") _ => false @@ -145,7 +159,7 @@ test fn xl2_clean_control_resolves_holds() -> Bool { // THE CUT IS WHAT MADE THE RED: the residual module unstripped, beside its provider, resolves on the // same route, so the row above is the strip's residual and not a defect in the specimen. test fn xl2_residual_control_resolves_before_the_cut_holds() -> Bool { - match xl2_control_runs().pre_cut { + match xl2_pre_cut_run() { Xl2RehearsalObserved { residual: residual, resolved_module_count: n } => count(residual) == 0 && n == 2 _ => false } @@ -156,7 +170,7 @@ test fn xl2_residual_control_resolves_before_the_cut_holds() -> Bool { // it. The previous cut raised an abandonment scope for every refused module, which would have kept // the rehearsal incomplete for a reason P4 has since discharged. test fn xl2_control_completeness_is_refused_holds() -> Bool { - match xl2_control_runs().cut { + match xl2_cut_run() { Xl2RehearsalObserved { completeness: Xl2CensusCompletenessRefused { first: Xl2PrerequisiteOutstanding { prerequisite: _ }, rest: rest } } => count(rest) + 1 == count(xl2_prerequisites_outstanding()) && all(rest, r => match r { @@ -184,7 +198,7 @@ fn xl2_first_and_last_chains_differ(residual: List) -> Bool { // TWO INDEPENDENT FAILURES IN ONE MODULE: exactly two rows, both that module's, carrying DIFFERENT // chains, and the module's complete observation raises no scope. test fn xl2_two_failures_in_one_module_are_two_rows_holds() -> Bool { - match xl2_control_runs().two { + match xl2_two_run() { Xl2RehearsalObserved { residual: residual, completeness: Xl2CensusCompletenessRefused { first: _, rest: rest } } => count(residual) == 2 && all(residual, r => r.module == "v2.xl2_control_two") @@ -201,7 +215,7 @@ test fn xl2_two_failures_in_one_module_are_two_rows_holds() -> Bool { // native requalification walls and the uncounted kernel-canonical class, and neither is among its // completeness refusals (the refusal type cannot carry them). test fn xl2_control_names_the_native_requalification_walls_holds() -> Bool { - match xl2_control_runs().cut { + match xl2_cut_run() { Xl2RehearsalObserved { native_requalification: walls, excluded: excluded } => count(walls) == 2 && count(excluded) == 2 && any(excluded, e => e == Xl2KernelCanonicalReferencesUncounted) @@ -214,7 +228,7 @@ test fn xl2_control_names_the_native_requalification_walls_holds() -> Bool { // beside the clean specimen at its own path. Neither shared member enters the ingest, so no row is // emitted, only the uniquely-pathed module resolves, and the path is reported once as unobserved. test fn xl2_duplicated_path_is_withheld_not_chosen_holds() -> Bool { - match xl2_control_runs().duplicated { + match xl2_duplicated_run() { Xl2RehearsalObserved { residual: residual, resolved_module_count: n, completeness: Xl2CensusCompletenessRefused { first: _, rest: rest } } => count(residual) == 0 && n == 1 && count(filter(rest, c => match c { @@ -230,7 +244,7 @@ test fn xl2_duplicated_path_is_withheld_not_chosen_holds() -> Bool { // and only the provider resolves. Before the 2026-10-04 ruling this specimen resolved and was // carried as an uncounted excluded population; that arm dissolved by its own stated condition. test fn xl2_nested_reference_is_residual_after_the_strip_holds() -> Bool { - match xl2_control_runs().nesting { + match xl2_nesting_run() { Xl2RehearsalObserved { residual: residual, resolved_module_count: n } => count(residual) == 1 && n == 1 && all(residual, r => r.module == "v2.xl2_control_provider.nested") _ => false diff --git a/src/v1/stage0/src/cli_run/claim_call_site_demand.rs b/src/v1/stage0/src/cli_run/claim_call_site_demand.rs index a0720f966f1..4141237e156 100644 --- a/src/v1/stage0/src/cli_run/claim_call_site_demand.rs +++ b/src/v1/stage0/src/cli_run/claim_call_site_demand.rs @@ -75,6 +75,8 @@ pub(crate) enum CallSiteDemandRow { /// How many of `claims` this run plans. planned_claims: u64, sites: Vec, + /// Each distinct (claim, read) pair over this identity's sites, claims as in `claims`. + reads: Vec<(String, ConsumerRead)>, }, Unadmissible { cause: CallSiteDemandCause, @@ -90,14 +92,93 @@ pub(crate) fn site_key_of(node: &Node) -> SiteKey { (node.span.file.to_string(), node.span.start, node.span.end) } +/// Immediate projection (or typed Unread) for each call that is a field-access base. +/// A field access whose base is not a readable call still marks every call child `Unread` +/// (`ProjectionBaseUnreadable`) so the call cannot later default to `WholeValue`. +pub(crate) fn immediate_consumer_projections( + nodes: &[Rc], + source_indices: Rc, +) -> HashMap { + let mut projections: HashMap = HashMap::new(); + for n in nodes { + if !matches!(n.expr_data.as_ref(), ExprData::ExprFieldAccess { .. }) { + continue; + } + let unread_call_children = |projections: &mut HashMap| { + for child in n.children.iter() { + if matches!(child.expr_data.as_ref(), ExprData::ExprCall { .. }) { + projections.insert( + site_key_of(child), + ConsumerRead::Unread(ConsumerReadCause::ProjectionBaseUnreadable), + ); + } + } + }; + let Ok(base) = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + crate::v1_std_core::field_access_base(n.clone()) + })) else { + unread_call_children(&mut projections); + continue; + }; + if !matches!(base.expr_data.as_ref(), ExprData::ExprCall { .. }) { + unread_call_children(&mut projections); + continue; + } + let field = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { + crate::v1_std_core::field_access_field_at(n.clone(), source_indices.clone()) + })); + let read = match field { + Err(_) => ConsumerRead::Unread(ConsumerReadCause::ProjectionFieldNameUnreadable), + Ok(f) if f.is_empty() => { + ConsumerRead::Unread(ConsumerReadCause::ProjectionFieldNameEmpty) + } + Ok(f) => ConsumerRead::ProjectedField(f), + }; + projections.insert(site_key_of(&base), read); + } + projections +} + pub(crate) fn render_site(site: &SiteKey) -> String { format!("{}:{}-{}", site.0, site.1, site.2) } +/// The `.dag` `ConsumerRead`: what the expression consuming a call site's result reads off it. +/// Only the IMMEDIATE projection is observed (`f(x).field`); any other consumer reads the whole +/// value. A projection whose field name cannot be read is `Unread` with its `.dag` +/// `ConsumerReadCause` -- `ConsumerReadUnobserved { cause }` -- never a guessed grain. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub(crate) enum ConsumerRead { + WholeValue, + ProjectedField(String), + Unread(ConsumerReadCause), +} + +/// The `.dag` `ConsumerReadCause` arms. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub(crate) enum ConsumerReadCause { + ProjectionFieldNameUnreadable, + ProjectionFieldNameEmpty, + ProjectionBaseUnreadable, + ShareMapLookupUnreadable, +} + +impl ConsumerReadCause { + pub(crate) fn variant(self) -> &'static str { + match self { + ConsumerReadCause::ProjectionFieldNameUnreadable => "ProjectionFieldNameUnreadable", + ConsumerReadCause::ProjectionFieldNameEmpty => "ProjectionFieldNameEmpty", + ConsumerReadCause::ProjectionBaseUnreadable => "ProjectionBaseUnreadable", + ConsumerReadCause::ShareMapLookupUnreadable => "ShareMapLookupUnreadable", + } + } +} + enum SiteFact { Closed { producer: String, preimage: String, + read: ConsumerRead, }, Unadmissible(CallSiteDemandCause), /// An unadmissible site whose callee IS known, kept by producer so a reader can disposition @@ -132,6 +213,8 @@ struct IdentityCell { /// How many of them are planned (index below the planned count). planned: u64, sites: BTreeSet, + /// (claim index, read), each pair once. + reads: BTreeSet<(usize, ConsumerRead)>, } impl<'a> CallSiteDemandObserver<'a> { @@ -192,9 +275,17 @@ impl<'a> CallSiteDemandObserver<'a> { } for (site, fact) in &facts.sites { let cell = match fact { - SiteFact::Closed { producer, preimage } => closed - .entry((producer.clone(), preimage.clone())) - .or_default(), + SiteFact::Closed { + producer, + preimage, + read, + } => { + let cell = closed + .entry((producer.clone(), preimage.clone())) + .or_default(); + cell.reads.insert((index, read.clone())); + cell + } SiteFact::Unadmissible(cause) => open.entry(*cause).or_default(), SiteFact::UnadmissibleOf { producer, cause } => { let by = open_by_producer @@ -233,6 +324,13 @@ impl<'a> CallSiteDemandObserver<'a> { .collect(), planned_claims: cell.planned, sites: cell.sites.iter().map(render_site).collect(), + reads: cell + .reads + .iter() + .map(|(i, read)| { + (format!("{}.{}", claims[*i].0, claims[*i].1), read.clone()) + }) + .collect(), }, ) .collect(); @@ -386,6 +484,8 @@ impl<'a> CallSiteDemandObserver<'a> { } nodes.push(n); } + // Immediate projection, or Unread when the base cannot be read as a call. + let projections = immediate_consumer_projections(&nodes, self.source_indices.clone()); let mut reads: BTreeSet<(String, String)> = BTreeSet::new(); let mut sites: Vec<(SiteKey, SiteFact)> = Vec::new(); for n in &nodes { @@ -395,7 +495,11 @@ impl<'a> CallSiteDemandObserver<'a> { // becomes that site's typed, counted cause. let read = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| { let target = self.call_target(module, n); - let fact = self.site_fact(module, n, target.clone(), &binders); + let read = projections + .get(&site_key_of(n)) + .cloned() + .unwrap_or(ConsumerRead::WholeValue); + let fact = self.site_fact(module, n, target.clone(), &binders, read); (target.ok(), fact) })); let (target, fact) = match read { @@ -441,6 +545,7 @@ impl<'a> CallSiteDemandObserver<'a> { call: &Rc, target: Result<(String, String), CallSiteDemandCause>, binders: &HashSet, + read: ConsumerRead, ) -> SiteFact { let target = match target { Ok(t) => t, @@ -460,6 +565,7 @@ impl<'a> CallSiteDemandObserver<'a> { Some(preimage) => SiteFact::Closed { producer: format!("{}.{}", target.0, target.1), preimage, + read, }, None => SiteFact::UnadmissibleOf { producer: format!("{}.{}", target.0, target.1), @@ -723,4 +829,100 @@ mod tests { ); assert!(closed_claims(&rows, "fixture.n7.reads", "").is_none()); } + // THE PROJECTION FACT: the bundle shape of #13113 in miniature. Two claims read different + // fields projected immediately off one closed call, a third reads one of them, and a fourth + // consumes the whole value; each (claim, read) pair is reported once, so the fold can tell a + // bundle of disjoint slices from one shared value. + const BUNDLE: &str = "module fixture.n7\n\ + type Pair {\n a: Bool\n b: Bool\n}\n\ + fn verdicts() -> Pair { Pair { a: true, b: false } }\n\ + fn claim_a() -> Bool { verdicts().a }\n\ + fn claim_b() -> Bool { verdicts().b }\n\ + fn claim_a_again() -> Bool { verdicts().a && verdicts().a }\n\ + fn claim_whole() -> Bool { verdicts() == verdicts() }\n"; + + fn reads_of(rows: &[CallSiteDemandRow], producer: &str) -> Vec<(String, ConsumerRead)> { + rows.iter() + .find_map(|r| match r { + CallSiteDemandRow::Closed { + producer: p, reads, .. + } if p == producer => Some(reads.clone()), + _ => None, + }) + .unwrap_or_default() + } + + #[test] + fn each_claims_immediate_projection_is_reported_once_and_a_bare_use_reads_the_whole() { + let rows = observe_source( + BUNDLE, + &["claim_a", "claim_b", "claim_a_again", "claim_whole"], + ); + let reads = reads_of(&rows, "fixture.n7.verdicts"); + let field = |f: &str| ConsumerRead::ProjectedField(f.to_string()); + assert_eq!( + reads, + vec![ + ("fixture.n7.claim_a".to_string(), field("a")), + ("fixture.n7.claim_b".to_string(), field("b")), + ("fixture.n7.claim_a_again".to_string(), field("a")), + ( + "fixture.n7.claim_whole".to_string(), + ConsumerRead::WholeValue + ), + ], + "{rows:?}" + ); + } + + // review 77161: a field access whose first child is not the call still has a call child; + // that call is Unread(ProjectionBaseUnreadable), never WholeValue via unwrap_or. + #[test] + fn an_unreadable_field_access_base_marks_the_call_child_unread() { + use crate::std_types::SourceSpan; + use crate::v1_std_core::{ + make_expr_error_node, make_expr_node, ExprErrorKind, NodeOccurrenceIdentity, + }; + let span = |start: i64, end: i64| { + Rc::new(SourceSpan { + file: "probe.dag".to_string(), + start, + end, + }) + }; + let err = make_expr_error_node( + Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), + ExprErrorKind::InternalExprError, + "missing base".to_string(), + span(1, 2), + ); + let call = make_expr_node( + Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), + Rc::new(ExprData::ExprCall { + call_semantics: None, + descent_evidence: None, + }), + crate::v1_std_core::empty_node_list(), + None, + span(10, 20), + ); + let access = make_expr_node( + Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), + Rc::new(ExprData::ExprFieldAccess { summary: None }), + Rc::new(vec![err, call.clone()].into()), + None, + span(1, 30), + ); + let projections = + immediate_consumer_projections(&[access, call.clone()], Rc::new(im::HashMap::new())); + let read = projections + .get(&site_key_of(&call)) + .cloned() + .unwrap_or(ConsumerRead::WholeValue); + assert_eq!( + read, + ConsumerRead::Unread(ConsumerReadCause::ProjectionBaseUnreadable), + "{projections:?}" + ); + } } diff --git a/src/v1/stage0/src/cli_run/required_floor_runner.rs b/src/v1/stage0/src/cli_run/required_floor_runner.rs index adaff4c89c9..fbb984f78aa 100644 --- a/src/v1/stage0/src/cli_run/required_floor_runner.rs +++ b/src/v1/stage0/src/cli_run/required_floor_runner.rs @@ -6841,7 +6841,7 @@ pub(crate) fn derive_and_install_cross_claim_share( in_flight_wall_cap_ms: u64, ) -> Result<(), String> { use super::claim_call_site_demand::{ - CallSiteDemandObserver, CallSiteDemandRow, CLOSED_ARGUMENT_NORMALIZER, + CallSiteDemandObserver, CallSiteDemandRow, ConsumerRead, CLOSED_ARGUMENT_NORMALIZER, }; use v1_interpreter::Value; const MODULE: &str = "v2.workflow.floor_pure_producer_share"; @@ -6912,6 +6912,7 @@ pub(crate) fn derive_and_install_cross_claim_share( claims, planned_claims, sites, + reads, } => Value::Variant { type_name: sym("CallSiteDemandObservation"), variant_name: sym("ClosedCallSiteDemand"), @@ -6938,6 +6939,44 @@ pub(crate) fn derive_and_install_cross_claim_share( sym("sites"), list_value_from_vec(sites.iter().map(str_value).collect()), ), + ( + sym("reads"), + list_value_from_vec( + reads + .iter() + .map(|(claim, read)| { + let read = match read { + ConsumerRead::WholeValue => { + unit("ConsumerRead", "WholeValue") + } + ConsumerRead::ProjectedField(field) => Value::Variant { + type_name: sym("ConsumerRead"), + variant_name: sym("ProjectedField"), + fields: std::rc::Rc::new(vec![( + sym("field"), + str_value(field), + )]), + }, + ConsumerRead::Unread(cause) => Value::Variant { + type_name: sym("ConsumerRead"), + variant_name: sym("ConsumerReadUnobserved"), + fields: std::rc::Rc::new(vec![( + sym("cause"), + unit("ConsumerReadCause", cause.variant()), + )]), + }, + }; + Value::Record { + type_name: sym("ClaimConsumerRead"), + fields: std::rc::Rc::new(vec![ + (sym("claim"), str_value(claim)), + (sym("read"), read), + ]), + } + }) + .collect(), + ), + ), ]), }, CallSiteDemandRow::Unadmissible { @@ -7104,15 +7143,39 @@ pub(crate) fn derive_and_install_cross_claim_share( }; *decline_counts.entry(variant_of(r, "decline")?).or_default() += 1; // EVERY decline is printed, single-claim ones included, so each producer's disposition is - // readable by identity from the run's own log. - { - eprintln!( - "[cross-claim-share-declined] producer={} decline={} argument_preimage={}", - text_of(r, "producer")?, - variant_of(r, "decline")?, - text_of(r, "argument_preimage")? - ); - } + // readable by identity from the run's own log. A bundle names the slices only one claim + // reads, and an unreadable consumer names its cause. + let detail = match ctx.field(r, "decline") { + Some(Value::Variant { + variant_name, + fields: d, + .. + }) => match ctx.resolve(*variant_name).as_str() { + "BundleOfDisjointProjections" => { + let slices = ctx + .field(d, "sole_projections") + .and_then(|v| v1_interpreter::list_value_items(ctx, v)) + .ok_or_else(|| malformed("a bundle decline has no `sole_projections`"))?; + let mut names = Vec::new(); + for s in &slices { + let Value::Str(s) = s else { + return Err(malformed("a sole projection is not a String")); + }; + names.push(s.to_string()); + } + format!(" sole_projections=[{}]", names.join(",")) + } + "ConsumerReadUnknown" => format!(" cause={}", variant_of(d, "cause")?), + _ => String::new(), + }, + _ => return Err(malformed("a declined row has no `decline` variant")), + }; + eprintln!( + "[cross-claim-share-declined] producer={} decline={}{detail} argument_preimage={}", + text_of(r, "producer")?, + variant_of(r, "decline")?, + text_of(r, "argument_preimage")? + ); } let mut unadmissible_rendered = Vec::new(); for row in &unadmissible { diff --git a/src/v2/test/claim/body_lowering/fold_operand_structure_test.dag b/src/v2/test/claim/body_lowering/fold_operand_structure_test.dag index b30a1d89b28..ea2dcb7bafd 100644 --- a/src/v2/test/claim/body_lowering/fold_operand_structure_test.dag +++ b/src/v2/test/claim/body_lowering/fold_operand_structure_test.dag @@ -208,56 +208,42 @@ fn fos_decision_holds(parsed: Optional) -> Bool { } } -// ONE PARSE PER SOURCE, EVERY VERDICT READ OFF IT. Each claim below inspects one Bool of this value, -// and each would otherwise pay its own tokenize, parse and lowering -- the ingest the claims are not -// about. The producer is shared by v2.workflow.floor_pure_producer_share -// derive_cross_claim_share, like v2.test.claim.fold_lowering flp_outcomes; the value is -// six Bools, so it reifies portably. -type FosOutcomes { - and_reader_over_loop: Bool - and_walker_over_loop: Bool - call_reader_over_loop: Bool - call_walker_over_loop: Bool - and_decision_holds: Bool - call_decision_holds: Bool +// ONE PARSE PER SOURCE, read WHOLE by each of its three claims, so the derived cross-claim share +// (v2.workflow.floor_pure_producer_share derive_cross_claim_share) fills it once; each claim then +// computes its OWN verdict over it. The six verdicts were once one record whose claims each read a +// different field: a bundle the share declines (BundleOfDisjointProjections), since sharing it +// netted each claim's own route and decision out of its budget. +fn fos_and_parsed() -> Optional { + fos_parsed(source: fos_and_fold_source) } -fn fos_outcomes() -> FosOutcomes { - let and_parsed = fos_parsed(source: fos_and_fold_source) - let call_parsed = fos_parsed(source: fos_call_fold_source) - FosOutcomes { - and_reader_over_loop: fos_and_over_loop(v: fos_route_value(parsed: and_parsed, route: FosValueReader)), - and_walker_over_loop: fos_and_over_loop(v: fos_route_value(parsed: and_parsed, route: FosBodyWalker)), - call_reader_over_loop: fos_call_over_loop(v: fos_route_value(parsed: call_parsed, route: FosValueReader)), - call_walker_over_loop: fos_call_over_loop(v: fos_route_value(parsed: call_parsed, route: FosBodyWalker)), - and_decision_holds: fos_decision_holds(parsed: and_parsed), - call_decision_holds: fos_decision_holds(parsed: call_parsed) - } +fn fos_call_parsed() -> Optional { + fos_parsed(source: fos_call_fold_source) } // POSITIVE CONTROLS: `fos_t && fold(..)` is Transform(&&, fos_t, Loop) and `fos_h(a: fold(..), b: fos_s)` // is Transform(fos_h, Loop, fos_s), on the value-reader and the body-walker route. test fn an_operand_beside_a_fold_lowers_as_the_operator_over_the_loop() -> Bool { - fos_outcomes().and_reader_over_loop + fos_and_over_loop(v: fos_route_value(parsed: fos_and_parsed(), route: FosValueReader)) } test fn the_body_walker_lowers_an_operand_beside_a_fold_as_the_operator_over_the_loop() -> Bool { - fos_outcomes().and_walker_over_loop + fos_and_over_loop(v: fos_route_value(parsed: fos_and_parsed(), route: FosBodyWalker)) } test fn a_call_with_a_fold_argument_lowers_as_the_call_over_the_loop() -> Bool { - fos_outcomes().call_reader_over_loop + fos_call_over_loop(v: fos_route_value(parsed: fos_call_parsed(), route: FosValueReader)) } test fn the_body_walker_lowers_a_call_with_a_fold_argument_as_the_call_over_the_loop() -> Bool { - fos_outcomes().call_walker_over_loop + fos_call_over_loop(v: fos_route_value(parsed: fos_call_parsed(), route: FosBodyWalker)) } // THE DISCRIMINATING RED: re-adding the descent answers Present at an identity-less encloser. test fn no_identity_less_node_answers_an_enclosed_fold_beside_an_operator() -> Bool { - fos_outcomes().and_decision_holds + fos_decision_holds(parsed: fos_and_parsed()) } test fn no_identity_less_node_answers_an_enclosed_fold_argument() -> Bool { - fos_outcomes().call_decision_holds + fos_decision_holds(parsed: fos_call_parsed()) } diff --git a/src/v2/test/claim/body_type_annotation_refusal_test.dag b/src/v2/test/claim/body_type_annotation_refusal_test.dag index eee270f1a82..5b65c1ef931 100644 --- a/src/v2/test/claim/body_type_annotation_refusal_test.dag +++ b/src/v2/test/claim/body_type_annotation_refusal_test.dag @@ -107,7 +107,7 @@ fn btar_resolve_refused_at_authored_q(o: Outcome) -> Bool { } test fn btar_fn_literal_return_annotation_reaches_resolve() -> Bool { - btar_fn_literal_outcomes().annotated_reaches_resolve + btar_resolve_refused_at_authored_q(o: btar_fn_literal_annotated()) } // (4) The unannotated let-bound literal is not erased: it lowers whole (gunbc#12210), its parameter @@ -121,22 +121,7 @@ fn btar_plain_literal_not_erased(o: Outcome) -> Bool { } test fn btar_unannotated_fn_literal_is_not_erased() -> Bool { - btar_fn_literal_outcomes().plain_not_erased -} - -// ONE WARM PRODUCER FOR THE TWO FN-LITERAL VERDICTS (3) and (4): each once paid its own front end. -// Shared by v2.workflow.floor_pure_producer_share derive_cross_claim_share; the -// claims only read their Bool. -type BtarFnLiteralOutcomes { - annotated_reaches_resolve: Bool - plain_not_erased: Bool -} - -fn btar_fn_literal_outcomes() -> BtarFnLiteralOutcomes { - BtarFnLiteralOutcomes { - annotated_reaches_resolve: btar_resolve_refused_at_authored_q(o: btar_fn_literal_annotated()), - plain_not_erased: btar_plain_literal_not_erased(o: btar_fn_literal_plain()) - } + btar_plain_literal_not_erased(o: btar_fn_literal_plain()) } // (5) A fn literal in an if arm is not erased either: the first-atom operand fallback no longer diff --git a/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag b/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag index dae2c75a68b..a123a758a94 100644 --- a/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag +++ b/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag @@ -61,26 +61,34 @@ fn fmi_reason(o: Outcome) -> Symbol { } } -// EACH FIXTURE PROGRAM IS ASSEMBLED ONCE, by a NULLARY producer the derived cross-claim share -// (v2.workflow.floor_pure_producer_share derive_cross_claim_share) admits where two or more declared -// claims read it; the claims read the decided, -// portable value. The record fold's one assembly serves three claims, including the supplied-tree control (3). -type FmiRecordFoldReading { - no_projection_refusal: Bool - base_is_lexical_reference: Bool - authored_member_formal_reason: Symbol -} - -fn fmi_record_fold_reading() -> FmiRecordFoldReading { - match fmi_assemble(src: fmi_record_fold) { - Rejected { diagnostics: d } => - FmiRecordFoldReading { no_projection_refusal: false, base_is_lexical_reference: false, authored_member_formal_reason: diagnostics_fatal_reason(d: d) } - Accepted { value: tree, diagnostics: _ } => - FmiRecordFoldReading { - no_projection_refusal: fmi_no_projection_refusal(o: fmi_infer_tree(tree: tree)), - base_is_lexical_reference: fmi_base_is_lexical_reference(tree: tree), - authored_member_formal_reason: fmi_reason(o: fmi_infer_with_member_formal_authored(tree: tree)) - } +// THE RECORD FOLD IS ASSEMBLED ONCE, by a NULLARY producer all three claims read WHOLE, so the +// derived cross-claim share (v2.workflow.floor_pure_producer_share derive_cross_claim_share) fills it +// once; each claim computes its OWN verdict over it, including the supplied-tree control (3). The +// three verdicts were once one record whose claims each read a different field: a bundle the share +// declines (BundleOfDisjointProjections), since sharing it netted each claim's own verdict out of +// its budget. An assembly that refuses answers each verdict as the record did. +fn fmi_record_fold_assembled() -> Outcome { + fmi_assemble(src: fmi_record_fold) +} + +fn fmi_record_fold_no_projection_refusal(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: tree, diagnostics: _ } => fmi_no_projection_refusal(o: fmi_infer_tree(tree: tree)) + } +} + +fn fmi_record_fold_base_is_lexical_reference(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: tree, diagnostics: _ } => fmi_base_is_lexical_reference(tree: tree) + } +} + +fn fmi_record_fold_authored_member_formal_reason(o: Outcome) -> Symbol { + match o { + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) + Accepted { value: tree, diagnostics: _ } => fmi_reason(o: fmi_infer_with_member_formal_authored(tree: tree)) } } @@ -89,7 +97,7 @@ fn fmi_sum_fold_reason() -> Symbol { fmi_reason(o: fmi_infer(src: fmi_sum_fold)) fn fmi_body_not_carrier_reason() -> Symbol { fmi_reason(o: fmi_infer(src: fmi_body_not_carrier_fold)) } test fn fmi_fold_member_projects_a_declared_field() -> Bool { - fmi_record_fold_reading().no_projection_refusal + fmi_record_fold_no_projection_refusal(o: fmi_record_fold_assembled()) } fn fmi_no_projection_refusal(o: Outcome) -> Bool { @@ -110,7 +118,7 @@ fn fmi_has_reason(o: Outcome, reason: Symbol) -> Bool { // recorded and infer can type it. RED ON THE BASE: the base was the bare canonical atom `e`, which nothing // typed, so the projection landed in the non-refusing ReceiverTypeUnderived arm. test fn fmi_lambda_binder_projection_base_is_a_lexical_reference() -> Bool { - fmi_record_fold_reading().base_is_lexical_reference + fmi_record_fold_base_is_lexical_reference(o: fmi_record_fold_assembled()) } fn fmi_base_is_lexical_reference(tree: ResolvedTree) -> Bool { @@ -133,7 +141,7 @@ test fn fmi_fold_member_undeclared_field_refuses() -> Bool { // (3) A STEP FORMAL INCOMPATIBLE WITH THE DOMAIN ELEMENT REFUSES. test fn fmi_fold_member_incompatible_formal_refuses() -> Bool { - fmi_record_fold_reading().authored_member_formal_reason == ^application_argument_does_not_inhabit + fmi_record_fold_authored_member_formal_reason(o: fmi_record_fold_assembled()) == ^application_argument_does_not_inhabit } // (3) IS SUPPLIED AT THE RESOLVE -> INFER BOUNDARY, because its red is not authorable in source: a typed diff --git a/src/v2/test/claim/field_projection/field_projection_stages_test.dag b/src/v2/test/claim/field_projection/field_projection_stages_test.dag index 821afe59906..8752abcbfab 100644 --- a/src/v2/test/claim/field_projection/field_projection_stages_test.dag +++ b/src/v2/test/claim/field_projection/field_projection_stages_test.dag @@ -287,7 +287,47 @@ fn fps_supplied_reading_with(records: List, unavailable: List FpsReading { fps_reading_of(o: fps_no_projection_source()) } +// ONE VERDICT PER CLAIM where only that claim reads it, computed over the shared fixture source. A +// reading's field that one claim alone reads is that claim's own stage, not a value another claim +// demands: shared inside the reading it is a bundle slice the derived share declines +// (BundleOfDisjointProjections), so such a claim computes its own stage over the source producer, +// which every claim over that fixture still reads whole. +fn fps_resolves_of(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => true + } +} + +fn fps_carries_projection_of(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: resolved, diagnostics: _ } => fps_carries_projection(root: resolved.root) + } +} + +fn fps_infers_of(o: Outcome) -> Bool { + match o { + Rejected { diagnostics: _ } => false + Accepted { value: resolved, diagnostics: _ } => + match infer(tree: resolved) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => true + } + } +} + +fn fps_projection_grounded_of(o: Outcome) -> Optional { + match o { + Rejected { diagnostics: _ } => optional_absent() + Accepted { value: resolved, diagnostics: _ } => + match infer(tree: resolved) { + Rejected { diagnostics: _ } => optional_absent() + Accepted { value: tree, diagnostics: _ } => fps_grounding_of(facts: fps_projection_facts_in(inferred: tree)) + } + } +} + fn fps_valid_field_reading() -> FpsReading { fps_reading_of(o: fps_valid_field_source()) } fn fps_absent_field_reading() -> FpsReading { fps_supplied_reading(records: [fps_box(fields: [fps_field(name: ^tree, type_node: fps_int(n: 41))])], receiver: fps_box_ref(), codomain: fps_int(n: 2), field: ^absent_field) @@ -296,11 +336,11 @@ fn fps_absent_field_reading() -> FpsReading { // THE FIXTURE'S POSITIVE CONTROL: the receiver alone reaches resolve and infer, so a red below is // about the projection and not about the parameter, the record declaration or the assembly. test fn fps_the_receiver_without_a_projection_resolves_holds() -> Bool { - fps_no_projection_reading().resolves + fps_resolves_of(o: fps_no_projection_source()) } test fn fps_the_receiver_without_a_projection_infers_holds() -> Bool { - fps_no_projection_reading().infers + fps_infers_of(o: fps_no_projection_source()) } test fn fps_a_valid_field_projection_resolves_holds() -> Bool { @@ -308,7 +348,7 @@ test fn fps_a_valid_field_projection_resolves_holds() -> Bool { } test fn fps_a_valid_field_projection_infers_holds() -> Bool { - fps_valid_field_reading().infers + fps_infers_of(o: fps_valid_field_source()) } // AN ABSENT FIELD MUST NOT BE ADMITTED. Asserted as a refusal at whatever stage currently refuses it, @@ -625,10 +665,9 @@ fn fps_match_binder_source(field: String) -> Outcome { // RESOLVE REACHES THE MATCH BINDER'S PROJECTION: the head is bound on the chain and the whole path names // no declaration, so resolve commits the projection shape exactly as it does for a parameter receiver. -fn fps_match_binder_reading() -> FpsReading { fps_reading_of(o: fps_match_binder_source(field: "tree")) } test fn fps_a_match_binder_receiver_resolves_holds() -> Bool { - fps_match_binder_reading().resolves + fps_resolves_of(o: fps_match_binder_source(field: "tree")) } // A MATCH-ARM BINDER AS A RECEIVER IS NOT YET TYPED, AND THIS ROW PINS EXACTLY HOW. It is the population of @@ -652,7 +691,7 @@ test fn fps_a_match_binder_receiver_resolves_holds() -> Bool { // projection_grounded is Present only on exactly that route (resolved, inferred, the projection node found // in the inferred tree, its facts present), so Absent -- any refusal, a missing node, missing facts -- reds it. test fn fps_a_match_binder_receiver_is_not_yet_typed_holds() -> Bool { - match fps_match_binder_reading().projection_grounded { + match fps_projection_grounded_of(o: fps_match_binder_source(field: "tree")) { Absent => false Present { value: derived } => !derived } @@ -661,7 +700,7 @@ test fn fps_a_match_binder_receiver_is_not_yet_typed_holds() -> Bool { // THE PROJECTION NODE IS THERE, IN THE RESOLVED TREE, so the row above is about a receiver whose projection // resolve really built, read independently of infer. test fn fps_a_match_binder_projection_is_in_the_resolved_tree_holds() -> Bool { - fps_match_binder_reading().resolved_carries_projection + fps_carries_projection_of(o: fps_match_binder_source(field: "tree")) } diff --git a/src/v2/test/claim/floor/pure_producer_share_refusal_test.dag b/src/v2/test/claim/floor/pure_producer_share_refusal_test.dag index bba1a9ef7e0..146140d38ac 100644 --- a/src/v2/test/claim/floor/pure_producer_share_refusal_test.dag +++ b/src/v2/test/claim/floor/pure_producer_share_refusal_test.dag @@ -14,7 +14,10 @@ import v2.workflow.floor_pure_producer_share { CallSiteDemandCause, ArgumentNotClosedConstant, CalleeDeclaresEffects, CrossClaimShareDerivation, DeclinedShareRow, ShareDerivationDecline, DemandedByOneClaim, ReachedByNoPlannedClaim, IdentityGradeNotShareable, RefusedByMeasurement, CarriedInputProducer, - LadderOwesNoCarry, + LadderOwesNoCarry, BundleOfDisjointProjections, ConsumerReadUnknown, + ClaimConsumerRead, ConsumerRead, WholeValue, ProjectedField, ConsumerReadUnobserved, + ConsumerReadCause, ProjectionFieldNameUnreadable, ProjectionFieldNameEmpty, ProjectionBaseUnreadable, ShareMapLookupUnreadable, + share_map_lookup_causes, ShareBasis, SharedByDeclaredDemand, SingleClaimFillDebt, SingleClaimFillDebtModule, SingleClaimFillDebtClaim, ActiveFillDebt, RetiredFillDebt, RestructuredPerWitnessRule, fill_debt_active_claims, @@ -25,8 +28,9 @@ import v2.workflow.floor_pure_producer_share { } import std.computation_identity { ComputationIdentity, NormalizedIdentical, IdentityUnknown, MissingConcept } import std.types { List } -import v2.std.algebra { list_map } +import v2.std.algebra { any, list_map } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.diagnostic { outcome_rejected, module_unavailable_diagnostic } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -67,6 +71,11 @@ fn probe_claim_names(claims: Int) -> List { } } +// Every claim reads the whole value: the shape of one shared computed value. +fn whole_reads(claims: List) -> List { + list_map(xs: claims, f: fn(c) { ClaimConsumerRead { claim: c, read: WholeValue } }) +} + fn probe_closed(producer: String, claims: Int) -> CallSiteDemandObservation { ClosedCallSiteDemand { producer: producer, @@ -74,7 +83,8 @@ fn probe_closed(producer: String, claims: Int) -> CallSiteDemandObservation { identity: probe_identity(), claims: probe_claim_names(claims: claims), planned_claims: 1, - sites: ["v2/test/probe.dag:10-40"] + sites: ["v2/test/probe.dag:10-40"], + reads: whole_reads(claims: probe_claim_names(claims: claims)) } } @@ -105,7 +115,8 @@ fn probe_single_claim(producer: String, claim: String) -> CallSiteDemandObservat identity: probe_identity(), claims: [claim], planned_claims: 1, - sites: ["v2/test/debt.dag:10-40"] + sites: ["v2/test/debt.dag:10-40"], + reads: whole_reads(claims: [claim]) } } @@ -128,6 +139,8 @@ fn decline_tag(decline: ShareDerivationDecline) -> String { RefusedByMeasurement => "RefusedByMeasurement" CarriedInputProducer => "CarriedInputProducer" LadderOwesNoCarry { verdict: _ } => "LadderOwesNoCarry" + BundleOfDisjointProjections { sole_projections: _ } => "BundleOfDisjointProjections" + ConsumerReadUnknown { cause: _ } => "ConsumerReadUnknown" } } @@ -170,7 +183,8 @@ test fn declared_demand_no_planned_claim_reaches_is_declined_and_named() -> Bool identity: probe_identity(), claims: probe_claim_names(claims: 4), planned_claims: 0, - sites: ["v2/test/probe.dag:70-80"] + sites: ["v2/test/probe.dag:70-80"], + reads: whole_reads(claims: probe_claim_names(claims: 4)) } ]) (length(xs: d.admitted) == 0) @@ -208,7 +222,8 @@ test fn a_shared_identity_is_based_on_demand_not_debt() -> Bool { identity: probe_identity(), claims: ["v2.test.debt.owes_its_fixture", "v2.test.debt.another"], planned_claims: 2, - sites: ["v2/test/debt.dag:50-60"] + sites: ["v2/test/debt.dag:50-60"], + reads: whole_reads(claims: ["v2.test.debt.owes_its_fixture", "v2.test.debt.another"]) } ]) (length(xs: d.admitted) == 1) @@ -247,7 +262,8 @@ test fn an_identity_of_unknown_grade_is_declined() -> Bool { identity: IdentityUnknown { cause: MissingConcept { detail: "authored fixture" } }, claims: probe_claim_names(claims: 3), planned_claims: 3, - sites: ["v2/test/probe.dag:50-60"] + sites: ["v2/test/probe.dag:50-60"], + reads: whole_reads(claims: probe_claim_names(claims: 3)) } ]) (length(xs: d.admitted) == 0) @@ -353,3 +369,110 @@ test fn a_superseded_row_does_not_transfer_to_other_producers() -> Bool { verdict: SupersededBySingleAuthorityRepair { repaired_by: "an authored fixture" } ) == false } + +// ── THE BUNDLE REFUSAL ──────────────────────────────────────────────────────────────────── +// One closed identity, two declared claims, varied ONLY in what each claim reads off the value. +// The shape is #13113's `trt_verdicts` in miniature: one record of distinct verdicts, each claim +// projecting its own field. A fold without the refusal admits all four; a fold refusing every +// projection reds the same-field and mixed controls. +fn probe_reads(producer: String, reads: List) -> CallSiteDemandObservation { + ClosedCallSiteDemand { + producer: producer, + argument_preimage: "()", + identity: probe_identity(), + claims: probe_claim_names(claims: 2), + planned_claims: 2, + sites: ["v2/test/bundle.dag:10-40", "v2/test/bundle.dag:50-80"], + reads: reads + } +} + +fn reads_of(first: ConsumerRead, second: ConsumerRead) -> List { + [ + ClaimConsumerRead { claim: "v2.test.probe.claim_1", read: first }, + ClaimConsumerRead { claim: "v2.test.probe.claim_2", read: second } + ] +} + +fn sole_projections_named(d: CrossClaimShareDerivation, fields: List) -> Bool { + any(xs: d.declined, predicate: fn(row) { + match row.decline { + BundleOfDisjointProjections { sole_projections: s } => + (length(xs: s) == length(xs: fields)) + && (length(xs: filter(xs: fields, predicate: fn(f) { any(xs: s, predicate: fn(x) { x == f }) })) == length(xs: fields)) + _ => false + } + }) +} + +test fn two_claims_reading_the_same_projection_are_admitted() -> Bool { + let d = probe_derive(observations: [probe_reads(producer: "v2.probe.bundle.same_field", reads: reads_of(first: ProjectedField { field: "bare_body" }, second: ProjectedField { field: "bare_body" }))]) + (length(xs: d.admitted) == 1) && (length(xs: d.declined) == 0) +} + +test fn two_claims_reading_disjoint_projections_are_declined_as_a_bundle() -> Bool { + let d = probe_derive(observations: [probe_reads(producer: "v2.probe.bundle.trt_verdicts", reads: reads_of(first: ProjectedField { field: "bare_body" }, second: ProjectedField { field: "minus_body" }))]) + (length(xs: d.admitted) == 0) + && declined_as(d: d, producer: "v2.probe.bundle.trt_verdicts", decline: BundleOfDisjointProjections { sole_projections: [] }) + && sole_projections_named(d: d, fields: ["bare_body", "minus_body"]) +} + +// THE MIXED CASE, DECIDED: a whole-value reader demands every field, so the projecting claim's +// slice is demanded twice and the identity is one shared value: admitted. +test fn a_whole_value_reader_beside_a_projecting_one_is_admitted() -> Bool { + let d = probe_derive(observations: [probe_reads(producer: "v2.probe.bundle.mixed", reads: reads_of(first: WholeValue, second: ProjectedField { field: "bind_body" }))]) + (length(xs: d.admitted) == 1) && (length(xs: d.declined) == 0) +} + +// A slice only one claim reads is declined even when another slice is shared: the shared field +// is not named, the private one is. +test fn a_private_slice_beside_a_shared_one_is_declined_naming_only_the_private_slice() -> Bool { + let d = probe_derive(observations: [ + ClosedCallSiteDemand { + producer: "v2.probe.bundle.partly_shared", + argument_preimage: "()", + identity: probe_identity(), + claims: probe_claim_names(claims: 3), + planned_claims: 3, + sites: ["v2/test/bundle.dag:90-99"], + reads: [ + ClaimConsumerRead { claim: "v2.test.probe.claim_1", read: ProjectedField { field: "x" } }, + ClaimConsumerRead { claim: "v2.test.probe.claim_2", read: ProjectedField { field: "x" } }, + ClaimConsumerRead { claim: "v2.test.probe.claim_3", read: ProjectedField { field: "y" } } + ] + } + ]) + (length(xs: d.admitted) == 0) && sole_projections_named(d: d, fields: ["y"]) +} + +// NEVER WIDEN: a consumer whose projection the observer could not read is declined with the +// cause, never judged as the whole value. +test fn an_unreadable_consumer_is_declined_with_its_cause() -> Bool { + let d = probe_derive(observations: [probe_reads(producer: "v2.probe.bundle.unread", reads: reads_of(first: WholeValue, second: ConsumerReadUnobserved { cause: ProjectionFieldNameUnreadable }))]) + (length(xs: d.admitted) == 0) + && declined_as(d: d, producer: "v2.probe.bundle.unread", decline: ConsumerReadUnknown { cause: ProjectionFieldNameUnreadable }) + && cross_claim_share_derivation_reconciles(observations: [probe_reads(producer: "v2.probe.bundle.unread", reads: reads_of(first: WholeValue, second: ConsumerReadUnobserved { cause: ProjectionFieldNameUnreadable }))], derivation: d) +} + +// review 77161: a refused map lookup is ShareMapLookupUnreadable, never a miss that drops the +// field from the count and admits a bundle. The A/B case (each claim a private projection, both +// lookups refused) is declined with that cause, not admitted. +test fn a_rejected_share_map_lookup_is_unread_not_a_miss() -> Bool { + let causes = share_map_lookup_causes(o: outcome_rejected(d: module_unavailable_diagnostic(reason: ^share_map_lookup_unreadable, module_file: ^probe))) + (length(xs: causes) == 1) + && any(xs: causes, predicate: fn(c) { + match c { + ShareMapLookupUnreadable => true + ProjectionFieldNameUnreadable => false + ProjectionFieldNameEmpty => false + ProjectionBaseUnreadable => false + } + }) +} + +test fn two_claims_with_unreadable_projection_lookups_are_declined_not_admitted() -> Bool { + let reads = reads_of(first: ConsumerReadUnobserved { cause: ShareMapLookupUnreadable }, second: ConsumerReadUnobserved { cause: ShareMapLookupUnreadable }) + let d = probe_derive(observations: [probe_reads(producer: "v2.probe.bundle.rejected_lookups", reads: reads)]) + (length(xs: d.admitted) == 0) + && declined_as(d: d, producer: "v2.probe.bundle.rejected_lookups", decline: ConsumerReadUnknown { cause: ShareMapLookupUnreadable }) +} diff --git a/src/v2/test/claim/value_base_projection_test.dag b/src/v2/test/claim/value_base_projection_test.dag index 069dae0bd13..cca1cb7d40b 100644 --- a/src/v2/test/claim/value_base_projection_test.dag +++ b/src/v2/test/claim/value_base_projection_test.dag @@ -44,28 +44,21 @@ fn vbp_has_value_projection_of(o: Outcome, field: Symbol) -> Bool } } -// EACH FIXTURE PROGRAM IS ASSEMBLED ONCE, by a NULLARY producer the derived cross-claim share -// (v2.workflow.floor_pure_producer_share derive_cross_claim_share) admits where two or more declared -// claims read it: source assembly is the real -// route this file must exercise (the producer IS that route), and it dominates every claim, so it is filled -// once by the first claim that reads it (netted from that claim) and every later claim reads the DECIDED, -// portable value. Claims over one program share -// its producer. -type VbpCallProjectionReading { - keeps_field: Bool - base_resolved_exactly: Bool - accepted_through_the_frontier: Bool +// THE FIXTURE PROGRAM IS ASSEMBLED ONCE, by a NULLARY producer every claim over it reads WHOLE: +// source assembly is the real route this file must exercise (the producer IS that route) and it +// dominates every claim, so the derived cross-claim share (v2.workflow.floor_pure_producer_share +// derive_cross_claim_share) fills it once and every later claim reads the decided value. Each +// claim then computes its OWN verdict over it. The three verdicts were once one record whose +// claims each read a different field; that is a bundle the share declines +// (BundleOfDisjointProjections), because sharing it netted each claim's own verdict out of its budget. +fn vbp_call_projection_assembled() -> Outcome { + tpb_assemble(src: vbp_call_projection) } -fn vbp_call_projection_reading() -> VbpCallProjectionReading { - let assembled = tpb_assemble(src: vbp_call_projection) - VbpCallProjectionReading { - keeps_field: vbp_has_value_projection_of(o: assembled, field: ^reason), - base_resolved_exactly: vbp_base_resolved_exactly(o: assembled), - accepted_through_the_frontier: match vbp_infer_assembled(o: assembled) { - Accepted { value: _, diagnostics: d } => diagnostics_has_reason(d: d, reason: ^infer_grounding_not_derived) - Rejected { diagnostics: _ } => false - } +fn vbp_call_projection_accepted_through_the_frontier(o: Outcome) -> Bool { + match vbp_infer_assembled(o: o) { + Accepted { value: _, diagnostics: d } => diagnostics_has_reason(d: d, reason: ^infer_grounding_not_derived) + Rejected { diagnostics: _ } => false } } @@ -120,7 +113,7 @@ fn vbp_undeclared_field_is_carried() -> Bool { // (1) A VALUE-BASE PROJECTION RESOLVES ITS BASE AND KEEPS ITS FIELD. test fn vbp_value_base_projection_keeps_its_field() -> Bool { - vbp_call_projection_reading().keeps_field + vbp_has_value_projection_of(o: vbp_call_projection_assembled(), field: ^reason) } // (2) A BOUND NAME SPELLED LIKE THE FIELD IS NOT CAPTURED AS THE FIELD: `reason` is also a parameter of r, @@ -143,7 +136,7 @@ fn vbp_infer_assembled(o: Outcome) -> Outcome { // (1b) THE BASE IS RESOLVED EXACTLY: the call's operator is the declaration reference p.mk and its argument the // parameter reference p.r.x. RED under the mutation that keeps the field but leaves the base verbatim. test fn vbp_value_base_is_resolved_exactly() -> Bool { - vbp_call_projection_reading().base_resolved_exactly + vbp_base_resolved_exactly(o: vbp_call_projection_assembled()) } // (3) THE PROJECTION IS ACCEPTED THROUGH THE FRONTIER, NOT JUDGED: `mk(x: x)` has no derived result type in v2 @@ -151,7 +144,7 @@ test fn vbp_value_base_is_resolved_exactly() -> Bool { // checked against D here -- the program is accepted with the infer_grounding_not_derived frontier entry carried // on the direct infer outcome. This claims only that; it does not claim infer judges the field. test fn vbp_call_result_projection_is_accepted_through_the_frontier() -> Bool { - vbp_call_projection_reading().accepted_through_the_frontier + vbp_call_projection_accepted_through_the_frontier(o: vbp_call_projection_assembled()) } // (4) THE RESIDUE IS CARRIED, NOT ADMITTED: an undeclared field off a call result is accepted only because diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 5a618632a1c..91297b747bc 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -1,6 +1,6 @@ module v2.workflow.floor_pure_producer_share -import std.types { List } +import std.types { List, Map } import std.computation_identity { ComputationIdentity, identity_permits_share } import std.cache_interface { ByteCapacity, CapacityBounded, ExactLimit, ProviderRetention, ReleasedAtProviderScopeExit, @@ -17,6 +17,9 @@ import std.materialization_ladder { import std.measure { Millisecond, Nanosecond, byte_size, millisecond_count, nanosecond, nanosecond_count } import v2.workflow.required_floor { required_floor_new_witness_envelope_ms } import v2.std.algebra { any, list_flat_map, list_map } +import v2.std.collection { empty_map, map_get, map_insert } +import v2.std.diagnostic { Accepted, Rejected, Outcome } +import std.optional { Absent, Present, Optional } // THE CROSS-CLAIM PURE-PRODUCER SHARE -- which pure computations the required floor may fill // once and serve to every planned claim that demands them. @@ -100,6 +103,39 @@ type CallSiteDemandCause | ArgumentNotClosedConstant | CallShapeUnread +// WHAT A DEMANDING CLAIM READS OFF THE VALUE, observed at the call site: the seed reports, for each +// site of a closed identity, the field projected IMMEDIATELY off the call (`f(x).field`) or, when +// the call's result is consumed any other way (bound, passed, compared, returned), the WHOLE value. +// A projected access the observer could not read is its own typed fact, never guessed at a grain. +// +// THE GRAIN'S LIMIT, stated so it is not read as more: a result bound by `let` and projected later +// reads as `WholeValue`, because the observer does not follow binders. That can only admit a share +// the projection rule would decline at a finer grain -- never one the fold without this rule would +// have declined -- so it is a missed refusal with a located population, not a widening; its +// next-rung trigger is the dependency read +// set of demand-engine M1 (docs/plans/demand-engine-program.md), which carries every projection a +// consumer reads off a value rather than only the immediate one. +// ProjectionFieldNameUnreadable -- the call is a field access's base, and reading the field's +// name failed: a projection of unknown grain. +// ProjectionFieldNameEmpty -- the call is a field access's base, and the field's name +// reads empty. +type ConsumerReadCause + = ProjectionFieldNameUnreadable + | ProjectionFieldNameEmpty + | ProjectionBaseUnreadable + | ShareMapLookupUnreadable + +type ConsumerRead + = WholeValue + | ProjectedField { field: String } + | ConsumerReadUnobserved { cause: ConsumerReadCause } + +// One distinct (claim, read) pair; the seed emits each pair once however many sites repeat it. +type ClaimConsumerRead { + claim: String + read: ConsumerRead +} + // `producer` is the callee's qualified declaration; `argument_preimage` the canonical normalized // argument row; `claims` the DISTINCT claims DECLARED in the prepared subject whose reach contains // a site of this identity (each becomes one ladder demand at its claim frame); `planned_claims` @@ -123,6 +159,7 @@ type CallSiteDemandObservation claims: List planned_claims: Int sites: List + reads: List } | UnadmissibleCallSiteDemand { cause: CallSiteDemandCause @@ -231,6 +268,8 @@ type ShareDerivationDecline | RefusedByMeasurement | CarriedInputProducer | LadderOwesNoCarry { verdict: LadderVerdict } + | BundleOfDisjointProjections { sole_projections: List } + | ConsumerReadUnknown { cause: ConsumerReadCause } type DeclinedShareRow { producer: String @@ -280,10 +319,14 @@ fn closed_demand_decline( planned_claims: Int, refused_names: List, carried_names: List, - debt: List + debt: List, + reads: List ) -> List { + let bundle = bundle_decline(claims: claims, reads: reads) if identity_permits_share(ci: identity) == false { [IdentityGradeNotShareable] + } else if length(xs: bundle) > 0 { + bundle } else if planned_claims == 0 { [ReachedByNoPlannedClaim] } else if any(xs: refused_names, predicate: fn(r) { r == producer }) { @@ -300,6 +343,178 @@ fn closed_demand_decline( } } +// THE BUNDLE REFUSAL (follow-up to #13043, flag by stern-bear-500). It is judged BEFORE the planned +// reach because being a bundle is a fact about the identity's declared demand, not about which +// claims one run plans: every bundle in the declared subject is named on every run, so the floor +// log is the population. It applies only to identities two or more claims demand -- one claim +// reading one field of its own fixture is a single recompute (or a named fill debt), not a bundle. Two or more declared claims +// demanding one closed identity owe a carry only if they demand the SAME computed value. A +// producer that bundles distinct work into one record, each claim reading its own field, is not +// one shared value: admitting it nets every claim's own slice out of that claim's budget, which is +// DESIGN section 5's cost externalization performed by authoring pattern. So a claim demands a +// projection when it reads that field off the call or reads the whole value (the whole value +// contains every field), and the identity is admitted only when EVERY projected field is demanded +// by at least two declared claims. Decided explicitly for the mixed case: a whole-value reader +// beside a projecting one is admitted, because the projected slice is genuinely demanded twice -- +// once as itself, once inside the whole. A field only one claim demands is that claim's own work, +// and the row is declined naming each such field. Only one claim per identity reads the fold's +// sole projections, so the seed's per-(claim, read) dedupe makes the list duplicate-free. +fn read_unobserved_cause(read: ConsumerRead) -> List { + match read { + WholeValue => [] + ProjectedField { field: _ } => [] + ConsumerReadUnobserved { cause: k } => [k] + } +} + +// An unreadable consumer stops the decision: a projection the observer could not see might be a +// bundle slice, so the row is declined with the cause rather than judged at a guessed grain. +fn unobserved_read_causes(reads: List) -> List { + list_flat_map(xs: reads, f: fn(r) { read_unobserved_cause(read: r.read) }) +} + +// LINEAR IN THE READS (review 75571: DESIGN section 6, a quadratic fold is always fixed). Three +// passes: the whole-value readers as a set, then per field the projecting claims that are NOT +// whole-value readers, then each projected field whose demand -- whole readers plus those +// projecting claims -- is exactly one. The seed emits each (claim, read) once, so a field's +// projecting rows are distinct claims and a sole field appears once. +// +// A refused map lookup is NEVER a count and NEVER a miss (review 77161, DESIGN section 5: +// a failure arm refuses, never widens). `share_map_lookup_causes` is the one match: Rejected +// is ShareMapLookupUnreadable, Absent is a miss, Present is a hit. Count arithmetic runs +// only after every lookup on the pass is Accepted. +fn whole_value_readers(reads: List) -> Map { + reads |> fold(init: empty_map(), f: fn(acc, r) { + match r.read { + WholeValue => map_insert(acc, r.claim, true) + ProjectedField { field: _ } => acc + ConsumerReadUnobserved { cause: _ } => acc + } + }) +} + +fn share_map_lookup_causes(o: Outcome>) -> List { + match o { + Rejected { diagnostics: _ } => [ShareMapLookupUnreadable] + Accepted { value: _, diagnostics: _ } => [] + } +} + +fn reads_whole_value(wholes: Map, claim: String) -> Bool { + let o = map_get(wholes, claim) + if length(xs: share_map_lookup_causes(o: o)) > 0 { + false + } else { + match o { + Accepted { value: Present { value: _ }, diagnostics: _ } => true + Accepted { value: Absent, diagnostics: _ } => false + Rejected { diagnostics: _ } => false + } + } +} + +fn projection_count(counts: Map, field: String) -> Int { + let o = map_get(counts, field) + if length(xs: share_map_lookup_causes(o: o)) > 0 { + 0 + } else { + match o { + Accepted { value: Present { value: n }, diagnostics: _ } => n + Accepted { value: Absent, diagnostics: _ } => 0 + Rejected { diagnostics: _ } => 0 + } + } +} + +type ShareCountState { + counts: Map + unread: List +} + +fn add_projection_count(state: ShareCountState, wholes: Map, claim: String, field: String) -> ShareCountState { + let whole_o = map_get(wholes, claim) + let whole_unread = share_map_lookup_causes(o: whole_o) + if length(xs: whole_unread) > 0 { + ShareCountState { counts: state.counts, unread: concat(state.unread, whole_unread) } + } else if reads_whole_value(wholes: wholes, claim: claim) { + state + } else { + let count_o = map_get(state.counts, field) + let count_unread = share_map_lookup_causes(o: count_o) + if length(xs: count_unread) > 0 { + ShareCountState { counts: state.counts, unread: concat(state.unread, count_unread) } + } else { + ShareCountState { + counts: map_insert(state.counts, field, projection_count(counts: state.counts, field: field) + 1), + unread: state.unread + } + } + } +} + +fn share_count_state(reads: List) -> ShareCountState { + let wholes = whole_value_readers(reads: reads) + reads |> fold(init: ShareCountState { counts: empty_map(), unread: [] }, f: fn(acc, r) { + match r.read { + ProjectedField { field: f } => + add_projection_count(state: acc, wholes: wholes, claim: r.claim, field: f) + WholeValue => acc + ConsumerReadUnobserved { cause: _ } => acc + } + }) +} + +fn sole_projections_from_state(reads: List, counts: Map) -> List { + let whole_count = length(xs: filter(xs: reads, predicate: fn(r) { + match r.read { + WholeValue => true + ProjectedField { field: _ } => false + ConsumerReadUnobserved { cause: _ } => false + } + })) + list_flat_map(xs: reads, f: fn(r) { + match r.read { + ProjectedField { field: f } => + let count_o = map_get(counts, f) + let unread = share_map_lookup_causes(o: count_o) + if length(xs: unread) > 0 { + [] + } else if whole_count + projection_count(counts: counts, field: f) == 1 { + [f] + } else { + [] + } + WholeValue => [] + ConsumerReadUnobserved { cause: _ } => [] + } + }) +} + +// The bundle verdict for one identity, computed ONCE and read by both the guard and the decline +// row. Empty unless two or more declared claims demand the identity. +fn bundle_decline(claims: List, reads: List) -> List { + if length(xs: claims) < 2 { + [] + } else { + let unobserved = unobserved_read_causes(reads: reads) + if length(xs: unobserved) > 0 { + list_map(xs: unobserved, f: fn(k) { ConsumerReadUnknown { cause: k } }) + } else { + let state = share_count_state(reads: reads) + if length(xs: state.unread) > 0 { + list_map(xs: state.unread, f: fn(k) { ConsumerReadUnknown { cause: k } }) + } else { + let sole = sole_projections_from_state(reads: reads, counts: state.counts) + if length(xs: sole) > 0 { + [BundleOfDisjointProjections { sole_projections: sole }] + } else { + [] + } + } + } + } +} + // The identity's sole demanding claim, when there is exactly one and it is an ACTIVE debt member; // empty otherwise. A list so the caller reads "none" without an optional. fn sole_active_debt_claim(claims: List, debt: List) -> List { @@ -326,8 +541,8 @@ fn derived_share_rows_for( debt: List ) -> List { match observation { - ClosedCallSiteDemand { producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, sites: s } => - if length(xs: closed_demand_decline(producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, refused_names: refused_names, carried_names: carried_names, debt: debt)) == 0 { + ClosedCallSiteDemand { producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, sites: s, reads: rs } => + if length(xs: closed_demand_decline(producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, refused_names: refused_names, carried_names: carried_names, debt: debt, reads: rs)) == 0 { [DerivedShareRow { producer: p, argument_preimage: a, identity: share_ladder_identity(producer: p, argument_preimage: a), basis: share_basis_of(claims: c, debt: debt), claims: length(xs: c), sites: s }] } else { [] @@ -343,9 +558,9 @@ fn declined_share_rows_for( debt: List ) -> List { match observation { - ClosedCallSiteDemand { producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, sites: _ } => + ClosedCallSiteDemand { producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, sites: _, reads: rs } => list_map( - xs: closed_demand_decline(producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, refused_names: refused_names, carried_names: carried_names, debt: debt), + xs: closed_demand_decline(producer: p, argument_preimage: a, identity: i, claims: c, planned_claims: n, refused_names: refused_names, carried_names: carried_names, debt: debt, reads: rs), f: fn(d) { DeclinedShareRow { producer: p, argument_preimage: a, decline: d } } ) UnadmissibleCallSiteDemand { cause: _, claims: _, sites: _ } => [] @@ -354,7 +569,7 @@ fn declined_share_rows_for( fn unadmissible_counts_for(observation: CallSiteDemandObservation) -> List { match observation { - ClosedCallSiteDemand { producer: _, argument_preimage: _, identity: _, claims: _, planned_claims: _, sites: _ } => [] + ClosedCallSiteDemand { producer: _, argument_preimage: _, identity: _, claims: _, planned_claims: _, sites: _, reads: _ } => [] UnadmissibleCallSiteDemand { cause: k, claims: c, sites: n } => [UnadmissibleDemandCount { cause: k, claims: c, sites: n }] } @@ -464,7 +679,7 @@ fn floor_cross_claim_share_derivation( fn closed_observation_count(observations: List) -> Int { length(xs: filter(xs: observations, predicate: fn(o) { match o { - ClosedCallSiteDemand { producer: _, argument_preimage: _, identity: _, claims: _, planned_claims: _, sites: _ } => true + ClosedCallSiteDemand { producer: _, argument_preimage: _, identity: _, claims: _, planned_claims: _, sites: _, reads: _ } => true UnadmissibleCallSiteDemand { cause: _, claims: _, sites: _ } => false } })) @@ -584,6 +799,22 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // Twelve more were added from probe 37238532455, for the sixteen rows gunbc#13187 added to the hand // roster (v2.test.claim.compiler.generic_formal_instantiation): all twelve claims of the module. // Re-derive with that probe; do not extend by hand. +// +// THE xl2 MEMBERS (test.claim.namespace_xl2_rehearsal_census) were the bundle `xl2_control_runs`, +// declined as BundleOfDisjointProjections on floor run 37194676016: each reads its own rehearsal +// run, a front end plus resolves that exceeds a new-witness budget, and the rehearsal itself is the +// claims' subject, so supplying its output would leave them asserting nothing. Un-bundled into one +// producer per run; the shared `xl2_cut_run` is demanded by four claims and is not debt. +// +// THE BUNDLE-DISPOSITION MEMBERS (the fold_operand_structure, body_type_annotation_refusal, +// infer_fold_member_instance, field_projection_stages and value_base_projection claims named +// beside this note's floor runs) read one field each of the bundles fos_outcomes, +// btar_fn_literal_outcomes, fmi_record_fold_reading, fps_match_binder_reading and +// vbp_call_projection_reading, declined as BundleOfDisjointProjections on floor run 37200031313. +// Un-bundled, each fixture's assembly or parse is one producer every claim over it reads whole and +// is SHARED; what remains over the new-witness budget on floor run 37207183924 is each claim's OWN +// stage (its route, infer or front end), which the bundle had been netting from the claim silently. +// That transfer is named here per claim instead. // gunbc#13207 (XL-2 collection concat): its ONE real-path inhabitance claim, kept per the DESIGN section 3 // witness rule (every other claim in the module supplies its input; sharp-raven-357 approved this member). // Measured on that PR's floor run 37238836376: 902,997 eval steps against the 72,300 new-witness budget -- the @@ -591,10 +822,26 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame). data floor_single_claim_fill_debt: List = [ + SingleClaimFillDebtModule { + module: "v2.test.claim.body_lowering.fold_operand_structure", + claims: [ + SingleClaimFillDebtClaim { claim: "a_call_with_a_fold_argument_lowers_as_the_call_over_the_loop", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "the_body_walker_lowers_a_call_with_a_fold_argument_as_the_call_over_the_loop", standing: ActiveFillDebt } + ] + }, + SingleClaimFillDebtModule { + module: "test.claim.namespace_xl2_rehearsal_census", + claims: [ + SingleClaimFillDebtClaim { claim: "xl2_residual_control_resolves_before_the_cut_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "xl2_two_failures_in_one_module_are_two_rows_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "xl2_duplicated_path_is_withheld_not_chosen_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "xl2_nested_reference_is_residual_after_the_strip_holds", standing: ActiveFillDebt } + ] + }, SingleClaimFillDebtModule { module: "v2.test.claim.compiler.collection_concat_realization", claims: [ - SingleClaimFillDebtClaim { claim: "cca_route_runs_on_the_real_path", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "cca_route_runs_on_the_real_path", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { @@ -677,7 +924,9 @@ data floor_single_claim_fill_debt: List = [ claims: [ SingleClaimFillDebtClaim { claim: "fmi_fold_member_undeclared_field_refuses", standing: ActiveFillDebt }, SingleClaimFillDebtClaim { claim: "fmi_fold_over_records_is_accepted", standing: ActiveFillDebt }, - SingleClaimFillDebtClaim { claim: "fmi_fold_step_body_not_the_carrier_refuses", standing: ActiveFillDebt } + SingleClaimFillDebtClaim { claim: "fmi_fold_step_body_not_the_carrier_refuses", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "fmi_fold_member_incompatible_formal_refuses", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "fmi_fold_member_projects_a_declared_field", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { @@ -853,7 +1102,9 @@ data floor_single_claim_fill_debt: List = [ claims: [ SingleClaimFillDebtClaim { claim: "btar_if_arm_fn_literal_is_not_erased", standing: ActiveFillDebt }, SingleClaimFillDebtClaim { claim: "btar_let_annotation_refuses", standing: ActiveFillDebt }, - SingleClaimFillDebtClaim { claim: "btar_unannotated_let_accepts", standing: ActiveFillDebt } + SingleClaimFillDebtClaim { claim: "btar_unannotated_let_accepts", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "btar_fn_literal_return_annotation_reaches_resolve", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "btar_unannotated_fn_literal_is_not_erased", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { @@ -871,7 +1122,7 @@ data floor_single_claim_fill_debt: List = [ module: "v2.test.claim.coercion.identity_cast_emission_route", claims: [ SingleClaimFillDebtClaim { claim: "a_cast_with_no_witness_refuses_before_realization_holds", standing: ActiveFillDebt }, - SingleClaimFillDebtClaim { claim: "an_admitted_identity_cast_emits_through_the_closure_route_holds", standing: RetiredFillDebt { disposition: BecameSharedByDemand } } + SingleClaimFillDebtClaim { claim: "an_admitted_identity_cast_emits_through_the_closure_route_holds", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { @@ -965,7 +1216,8 @@ data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtClaim { claim: "fps_an_absent_field_does_not_infer_holds", standing: RetiredFillDebt { disposition: RestructuredPerWitnessRule } }, SingleClaimFillDebtClaim { claim: "fps_an_unresolvable_provider_leaves_its_declaration_unavailable_holds", standing: RetiredFillDebt { disposition: RestructuredPerWitnessRule } }, SingleClaimFillDebtClaim { claim: "fps_the_int_field_grounds_as_an_int_parameter_does_holds", standing: RetiredFillDebt { disposition: RestructuredPerWitnessRule } }, - SingleClaimFillDebtClaim { claim: "fps_two_fields_of_different_types_ground_differently_holds", standing: RetiredFillDebt { disposition: RestructuredPerWitnessRule } } + SingleClaimFillDebtClaim { claim: "fps_two_fields_of_different_types_ground_differently_holds", standing: RetiredFillDebt { disposition: RestructuredPerWitnessRule } }, + SingleClaimFillDebtClaim { claim: "fps_a_match_binder_receiver_is_not_yet_typed_holds", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { @@ -1255,7 +1507,8 @@ data floor_single_claim_fill_debt: List = [ module: "v2.test.claim.value_base_projection", claims: [ SingleClaimFillDebtClaim { claim: "vbp_a_param_spelled_like_the_field_is_not_captured", standing: ActiveFillDebt }, - SingleClaimFillDebtClaim { claim: "vbp_undeclared_field_off_a_call_result_is_carried_on_the_direct_infer_outcome", standing: ActiveFillDebt } + SingleClaimFillDebtClaim { claim: "vbp_undeclared_field_off_a_call_result_is_carried_on_the_direct_infer_outcome", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "vbp_call_result_projection_is_accepted_through_the_frontier", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule {