diff --git a/.gitattributes b/.gitattributes index c20789b93cc..9081cb07316 100644 --- a/.gitattributes +++ b/.gitattributes @@ -68,7 +68,6 @@ src/v1/stage0/src/recorded_fixture.rs !merge src/v1/stage0/src/required_regen_host.rs !merge src/v1/stage0/src/resolved_graph_cache.rs !merge src/v1/stage0/src/shared_typecheck_store.rs !merge -src/v1/stage0/src/std_lens_verdict.rs !merge src/v1/stage0/src/target_invocation_host.rs !merge src/v1/stage0/src/usv_pilot_v2_std_algebra.rs !merge src/v1/stage0/src/usv_pilot_v2_std_collection.rs !merge diff --git a/dag/gunbc/roster_registry.dag b/dag/gunbc/roster_registry.dag index 0541a1f8edd..ba58c245a19 100644 --- a/dag/gunbc/roster_registry.dag +++ b/dag/gunbc/roster_registry.dag @@ -252,7 +252,7 @@ data roster_registry: List = [ roster: roster_decl(module_path: "gunbc.stage0_rust_source_lifecycle_scaffold", decl_name: "rust_source_lifecycle_residue_rows"), unit_kind: "tracked .rs path outside derived authority joins (file-grain residue)", membership: DeclaredFrontier { - reason: "file-grain paths tracked on disk that no authority join classifies yet — bootstrap copies, hand-retained harness kernels, module_path_index files, frontier layout lag, and authority contradictions (stage0_core lib.rs vs partition rows); each row carries reason and dissolve_on. Cargo [[bin]] paths are host-derived (gunbc.stage0_cargo_manifest), not residue rows", + reason: "file-grain paths tracked on disk that no authority join classifies yet — bootstrap copies, hand-retained harness kernels, module_path_index files, and frontier layout lag; each row carries reason and dissolve_on. Cargo [[bin]] paths are host-derived (gunbc.stage0_cargo_manifest), not residue rows", dissolution: unbound_dissolution(description: "per row: the path derives from the observed generated population (gunbc.stage0_rust_source_lifecycle_scaffold derived_generated_stage0_repo_paths), hand_maintained_stage0_filenames, stage0_cargo_bin_paths_observed (PR B host boundary), or stage0_partition_crate_rows and the row deletes; roster-wide, rust_source_host_observation_note host boundary supplies path evidence and promotes the scaffold to ZeroHandMaintainedRust acceptance (V1FinishLine, dag/gunbc/v1/v1_deletion_plan.dag)") } }, diff --git a/dag/gunbc/stage0/stage0_crate_layout_generated.dag b/dag/gunbc/stage0/stage0_crate_layout_generated.dag index b027c88e31e..5ac17ebe49c 100644 --- a/dag/gunbc/stage0/stage0_crate_layout_generated.dag +++ b/dag/gunbc/stage0/stage0_crate_layout_generated.dag @@ -53,7 +53,6 @@ data generated_stage0_filenames: List = [ "derived_realization_schedule.rs", "memory_governor.rs", "namespace_wave_admission.rs", - "std_lens_verdict.rs", "v2_compiler_body_producer.rs", "v2_compiler_normalize.rs", "v2_compiler_target_carriers.rs", diff --git a/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag b/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag index 336040d8df1..51821a0c03f 100644 --- a/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag +++ b/dag/gunbc/stage0/stage0_rust_source_lifecycle_scaffold.dag @@ -529,10 +529,6 @@ data residue_module_path_index_reason: String = "hand_maintained_stage0_dirs lis data residue_module_path_index_dissolution: DissolutionCondition = unbound_dissolution(description: "dissolve-on: module_path_index/*.rs paths derive from hand_maintained_stage0_dirs + host census, or the directory dissolves into generated emit") -data residue_stage0_core_lib_reason: String = "src/v1/stage0_core/src/lib.rs exists on disk but is absent from stage0_partition_crate_rows — authority contradiction surfaced for operator resolution" - -data residue_stage0_core_lib_dissolution: DissolutionCondition = unbound_dissolution(description: "dissolve-on: stage0_partition_crate_rows enrolls src/v1/stage0_core OR the crate deletes") - fn residue_row(path: String, reason: String, dissolution: DissolutionCondition) -> RustSourceLifecycleRow { RustSourceLifecycleRow { path: path, @@ -563,11 +559,6 @@ data rust_source_lifecycle_residue_rows: List = [ path: "src/v1/stage0/src/module_path_index/parsed_dag_file.rs", reason: residue_module_path_index_reason, dissolution: residue_module_path_index_dissolution - ), - residue_row( - path: "src/v1/stage0_core/src/lib.rs", - reason: residue_stage0_core_lib_reason, - dissolution: residue_stage0_core_lib_dissolution ) ] @@ -855,5 +846,3 @@ fn stage0_rust_lifecycle_scaffold_mechanical_checks_holds() -> Bool { data unclassified_axis_rung_note: String = "RUNG DROP, DECLARED (2026-08-20). SUBJECT: the unclassified axis -- count_tracked_unclassified here, and unclassified_paths in gunbc.stage0_rust_lifecycle_totality, which answer the same question over the same two authorities. DECLARED RUNG: mitigatable. It is NOT mechanically preventable, and it was reported as though it were by carriers that derive the axis correctly while nothing executing can make it fire.\n\nMEASURED AT 026a709a71636d60df325f9183b78febff22901d, by execution, both directions. LIVE: current_stage0_rust_source_observation() through lifecycle_totality_receipt gives tracked=270, generated=126, disposition=7, stale=0, UNCLASSIFIED=137, paths enumerated. HERMETIC: the same predicate over lifecycle_totality_witness_observation(extra_paths: []) gives ZERO. The predicate is not wrong; the subject is. That constructor sets tracked := classified ++ extra_paths, so unclassified_paths is IDENTICALLY extra_paths -- confirmed by planting a path that does not exist on disk and getting back exactly it. A hermetic witness of this carrier can only discover what its author already typed into the call.\n\nTHE LIVE ARM DOES NOT RESCUE IT, FOR TWO REASONS THAT ARE INDEPENDENT OF EACH OTHER. First, it executes nowhere: both files reaching it declare ReadsLiveTree, which the required floor declines, and their exclusion rows name bin_witness_wet_entries as their real executing consumer -- a roster of 94 rows across 38 entry files whose consumer, the ci.yml wet job, was deleted at 611fd02770. Second, and worse, the live witnesses would not detect the frontier even when run: measured under claim_batch --wet at this ref, all three PASS at 137 unclassified. One accepted DerivedUnclassifiedTracked with a positive count OR CargoTargetMissingLifecycleDisposition OR ManifestStateScaffoldOk -- three mutually contradictory states, so it was green at 137 and would have been green at 0. The other asserted only that two Bools are false, which any refusal satisfies, including a git outage. Both disjunctions are repaired in this change; that repair removes a fabricated green and does NOT change the rung, because the witnesses still execute nowhere.\n\nWHAT THIS CHANGE ACTUALLY BUYS, stated narrowly so it is not mistaken for the climb: DerivedUnclassifiedTracked now has a discriminating RED that runs on the required floor. It had none. count_newly_unclassified_tracked is checked first and is the narrower predicate, so every pre-existing constructor reached the newly arm and the standing arm was unreachable by any executing input -- including from a witness named for the unclassified axis that asserted the newly arm and passed. That is one arm of one carrier made falsifiable. The AXIS is still measured over a manufactured subject.\n\nCEILING AND WHY: mechanically preventable is not the ceiling and structural impossibility is. Classification is decidable and fully modeled -- a tracked path either is or is not a member of two closed authorities -- so the reachable end state is that an unclassified file cannot be WRITTEN, not that a check finds it. That is section 4b's construction rung and it is a property of the file, not of two lists that can both omit it.\n\nNEXT-RUNG TRIGGER, and it is deliberately not a wall: an executing consumer for the live observation. Not a restored wet lane by itself -- ReadsLiveTree declines these files from the floor independently, so a wet lane alone leaves them off. Until some executing path reaches the real tracked population, a construction wall over the live arm would be a SECOND unexecuted artifact sitting at exactly this rung while looking like a climb, which is the rung inflation 4b names as worse than sitting low. The 137 is a decision about what this repository intends to classify and is routed to the operator as a discovery rather than landed as a refusal.\n\nRESTORATION: this row is rewritten as an ordinary description -- not amended -- when the axis has an executing consumer over the live population, at which point the honest rung can be re-measured instead of re-argued." data unclassified_axis_rung_restoration: DissolutionCondition = unbound_dissolution(description: "dissolve-on: the unclassified axis acquires an executing consumer over the LIVE tracked population (not a manufactured observation), at which point unclassified_axis_rung_note is rewritten in one pass and this row deletes with it") - -data rust_source_lifecycle_partition_contradiction_note: String = "OPEN: src/v1/stage0_core/src/lib.rs is tracked on disk but stage0_partition_crate_rows has no src/v1/stage0_core row. Residue row surfaces the contradiction; operator resolves via partition row or crate deletion." diff --git a/dag/gunbc/v1/v1_consumer_census.dag b/dag/gunbc/v1/v1_consumer_census.dag index 9d635182e7d..14618c65e5a 100644 --- a/dag/gunbc/v1/v1_consumer_census.dag +++ b/dag/gunbc/v1/v1_consumer_census.dag @@ -302,6 +302,8 @@ fn v1cc_boundary(consumer: DeclarationRef, authority: DeclarationRef, dispositio BoundaryConsumer { consumer: consumer, consumed_old_authority: authority, disposition: disposition } } +data stage0_core_deletion_search_receipt: String = "SEARCH RECEIPT (2026-08-30): searched the workspace member declarations and every tracked Cargo.toml for a stage0_core member or path dependency; searched workflow, emission and tooling sources for stage0_core; and checked both the authored partition authority v2.workflow.rust_crate_partition and its gunbc.stage0_crate_partition_generated projection. No builder or owner names src/v1/stage0_core. The only hits outside the orphan directory were this retirement receipt and the lifecycle residue contradiction whose own dissolution condition selected crate deletion. Therefore the directory deletes; it is not enrolled or frozen." + fn tsv_row(path_decl: String) -> V1ConsumerRow { { boundary: v1cc_boundary( @@ -430,7 +432,7 @@ data v1_static_consumers: List = [ }, { boundary: v1cc_boundary( - consumer: decl_ref(module_path: "gunbc.stage0_rust_source_lifecycle_scaffold", decl_name: "residue_stage0_core_lib_dissolution"), + consumer: decl_ref(module_path: "gunbc.v1_consumer_census", decl_name: "stage0_core_deletion_search_receipt"), authority: stage0_partition_rows, disposition: retired(reason: "an ALREADY-DECLARED open authority contradiction, not a discovery of this census: src/v1/stage0_core/src/lib.rs is tracked on disk, absent from the partition rows and absent from the workspace member list, and the residue row's dissolution reads 'stage0_partition_crate_rows enrolls src/v1/stage0_core OR the crate deletes'. XL-5 satisfies the second arm. Recorded so the transaction is known to DISCHARGE that row rather than orphan it"), ), diff --git a/src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs b/src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs index 3d6b9a08e0b..762600c798a 100644 --- a/src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs +++ b/src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs @@ -19,7 +19,6 @@ pub const HAND_MAINTAINED_STAGE0_FILES: &[&str] = &[ "derived_realization_schedule.rs", "memory_governor.rs", "namespace_wave_admission.rs", - "std_lens_verdict.rs", "v2_compiler_body_producer.rs", "v2_compiler_normalize.rs", "v2_compiler_target_carriers.rs", diff --git a/src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs b/src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs index ec40b68ee58..30997088281 100644 --- a/src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs +++ b/src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs @@ -39,7 +39,7 @@ pub fn generated_pub_mod_basenames() -> Rc> { pub fn generated_stage0_filenames() -> Rc> { thread_local! { static CACHED: Rc> = { - Rc::new(vec!["v1_interpreter.rs".to_string(), "bounded_shell_host_drain.rs".to_string(), "cli_run.rs".to_string(), "codex_app_server_stdio_session.rs".to_string(), "coproduct_reflection.rs".to_string(), "data_initializer_identity.rs".to_string(), "declaration_index.rs".to_string(), "resolved_graph_cache.rs".to_string(), "shared_typecheck_store.rs".to_string(), "recorded_fixture.rs".to_string(), "phase_profile.rs".to_string(), "pre_push.rs".to_string(), "census_exclude_derive.rs".to_string(), "derived_realization_schedule.rs".to_string(), "memory_governor.rs".to_string(), "namespace_wave_admission.rs".to_string(), "std_lens_verdict.rs".to_string(), "v2_compiler_body_producer.rs".to_string(), "v2_compiler_normalize.rs".to_string(), "v2_compiler_target_carriers.rs".to_string(), "v2_compiler_discovery_enumeration.rs".to_string(), "v2_compiler_parse_engine_hooks.rs".to_string(), "v2_compiler_use_site_verdict.rs".to_string(), "cssl_seed_linked_closure_assembly.rs".to_string(), "required_regen_host.rs".to_string(), "target_invocation_host.rs".to_string(), "behavioral_receipt_host.rs".to_string(), "partition_crate_boundary_host.rs".to_string(), "generated_artifact_boundary_host.rs".to_string(), "emitted_closure_compile_host.rs".to_string(), "v2_compiler_compile.rs".to_string(), "v2_compiler_program_assembly.rs".to_string(), "v2_compiler_source_authority.rs".to_string(), "usv_pilot_v2_std_algebra.rs".to_string(), "usv_pilot_v2_std_collection.rs".to_string(), "usv_pilot_v2_std_node.rs".to_string(), "v2_compiler_resolve.rs".to_string(), "v2_compiler_program_partition.rs".to_string(), "v2_compiler_tokenize.rs".to_string(), "v2_compiler_infer.rs".to_string(), "bootstrap_stage0_crate_layout_generated.rs".to_string(), "v1_interpreter_dispatch_generated.rs".to_string(), "main.rs".to_string()]) + Rc::new(vec!["v1_interpreter.rs".to_string(), "bounded_shell_host_drain.rs".to_string(), "cli_run.rs".to_string(), "codex_app_server_stdio_session.rs".to_string(), "coproduct_reflection.rs".to_string(), "data_initializer_identity.rs".to_string(), "declaration_index.rs".to_string(), "resolved_graph_cache.rs".to_string(), "shared_typecheck_store.rs".to_string(), "recorded_fixture.rs".to_string(), "phase_profile.rs".to_string(), "pre_push.rs".to_string(), "census_exclude_derive.rs".to_string(), "derived_realization_schedule.rs".to_string(), "memory_governor.rs".to_string(), "namespace_wave_admission.rs".to_string(), "v2_compiler_body_producer.rs".to_string(), "v2_compiler_normalize.rs".to_string(), "v2_compiler_target_carriers.rs".to_string(), "v2_compiler_discovery_enumeration.rs".to_string(), "v2_compiler_parse_engine_hooks.rs".to_string(), "v2_compiler_use_site_verdict.rs".to_string(), "cssl_seed_linked_closure_assembly.rs".to_string(), "required_regen_host.rs".to_string(), "target_invocation_host.rs".to_string(), "behavioral_receipt_host.rs".to_string(), "partition_crate_boundary_host.rs".to_string(), "generated_artifact_boundary_host.rs".to_string(), "emitted_closure_compile_host.rs".to_string(), "v2_compiler_compile.rs".to_string(), "v2_compiler_program_assembly.rs".to_string(), "v2_compiler_source_authority.rs".to_string(), "usv_pilot_v2_std_algebra.rs".to_string(), "usv_pilot_v2_std_collection.rs".to_string(), "usv_pilot_v2_std_node.rs".to_string(), "v2_compiler_resolve.rs".to_string(), "v2_compiler_program_partition.rs".to_string(), "v2_compiler_tokenize.rs".to_string(), "v2_compiler_infer.rs".to_string(), "bootstrap_stage0_crate_layout_generated.rs".to_string(), "v1_interpreter_dispatch_generated.rs".to_string(), "main.rs".to_string()]) }; } CACHED.with(|c: &Rc>| c.clone()) diff --git a/src/v1/stage0/src/std_lens_verdict.rs b/src/v1/stage0/src/std_lens_verdict.rs deleted file mode 100644 index f2b8f13fabc..00000000000 --- a/src/v1/stage0/src/std_lens_verdict.rs +++ /dev/null @@ -1,63 +0,0 @@ -// Generated by v1 compiler -- do not edit. -// Source module: std.lens_verdict - -use self::LensVerdict::*; -use self::LensVerdictLocus::*; -use crate::v1_rt; -use crate::v1_rt::{VecCompat, VecJoin}; -use crate::NonEmptyBTreeSet; -use crate::NonEmptyVec; -use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; -use std::rc::Rc; - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -#[serde(tag = "_variant")] -pub enum LensVerdictLocus { - ModuleWholeFile { module_name: String }, -} -impl LensVerdictLocus { - pub fn module_name(&self) -> String { - match self { - LensVerdictLocus::ModuleWholeFile { - module_name: __val, .. - } => __val.clone(), - } - } -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct LensVerdictDiagnostic { - pub reason: String, - pub at: Rc, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -#[serde(tag = "_variant")] -pub enum LensVerdict { - Holds, - Violation { - diagnostic: Rc, - }, - NotApplicable { - diagnostic: Rc, - }, - Unrealized { - diagnostic: Rc, - }, -} -impl LensVerdict { - pub fn diagnostic(&self) -> Rc { - match self { - LensVerdict::Holds => panic!("no diagnostic on unit variant"), - LensVerdict::Violation { - diagnostic: __val, .. - } => __val.clone(), - LensVerdict::NotApplicable { - diagnostic: __val, .. - } => __val.clone(), - LensVerdict::Unrealized { - diagnostic: __val, .. - } => __val.clone(), - } - } -} diff --git a/src/v1/stage0_core/Cargo.toml b/src/v1/stage0_core/Cargo.toml deleted file mode 100644 index c9f345c5f8c..00000000000 --- a/src/v1/stage0_core/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -[package] -name = "v1-stage0-core" -version = "0.1.0" -edition = "2021" -[features] -default = [] -text_lookup_work_counter = [] - - -[dependencies] -stacker = "0.1" -im = { version = "15.1", features = ["serde"] } -serde = { version = "1", features = ["derive", "rc"] } -serde_json = "1" -unicode-ident = "1" -unicode-properties = { version = "0.1", features = ["emoji"] } diff --git a/src/v1/stage0_core/src/lib.rs b/src/v1/stage0_core/src/lib.rs deleted file mode 100644 index 6030db108ef..00000000000 --- a/src/v1/stage0_core/src/lib.rs +++ /dev/null @@ -1,175 +0,0 @@ -//! Generated by regen_stage0 -- do not edit. -//! -//! Crate boundary for generated v2 stage0 core authorities. -//! -//! The module bodies remain generated into `src/v1/stage0/src`. This crate -//! exposes the lower std/runtime/artifact/language/infer support surface -//! without copying generated module bodies. The root `NonEmpty*` wrappers are -//! mirrored from the stage0 lib root because generated modules address them as -//! `crate::NonEmptyVec` and `crate::NonEmptyBTreeSet`. - -#![allow( - unused_imports, - unused_variables, - unused_mut, - unused_parens, - dead_code, - unreachable_patterns, - non_shorthand_field_patterns, - suspicious_double_ref_op, - clippy::all -)] - -#[path = "../../stage0/src/extdeps_external_authority.rs"] -pub mod extdeps_external_authority; -#[path = "../../stage0/src/extdeps_languages_dag_emit.rs"] -pub mod extdeps_languages_dag_emit; -#[path = "../../stage0/src/extdeps_languages_dag_syntax.rs"] -pub mod extdeps_languages_dag_syntax; -#[path = "../../stage0/src/extdeps_languages_dag_types.rs"] -pub mod extdeps_languages_dag_types; -#[path = "../../stage0/src/extdeps_languages_go_emit.rs"] -pub mod extdeps_languages_go_emit; -#[path = "../../stage0/src/extdeps_languages_go_syntax.rs"] -pub mod extdeps_languages_go_syntax; -#[path = "../../stage0/src/extdeps_languages_go_types.rs"] -pub mod extdeps_languages_go_types; -#[path = "../../stage0/src/extdeps_languages_python_emit.rs"] -pub mod extdeps_languages_python_emit; -#[path = "../../stage0/src/extdeps_languages_python_syntax.rs"] -pub mod extdeps_languages_python_syntax; -#[path = "../../stage0/src/extdeps_languages_python_types.rs"] -pub mod extdeps_languages_python_types; -#[path = "../../stage0/src/extdeps_languages_rust_emit.rs"] -pub mod extdeps_languages_rust_emit; -#[path = "../../stage0/src/extdeps_languages_rust_syntax.rs"] -pub mod extdeps_languages_rust_syntax; -#[path = "../../stage0/src/extdeps_languages_rust_types.rs"] -pub mod extdeps_languages_rust_types; -#[path = "../../stage0/src/extdeps_uri.rs"] -pub mod extdeps_uri; -#[path = "../../stage0/src/std_algebra.rs"] -pub mod std_algebra; -#[path = "../../stage0/src/std_coercion.rs"] -pub mod std_coercion; -#[path = "../../stage0/src/std_computation.rs"] -pub mod std_computation; -#[path = "../../stage0/src/std_content_hash.rs"] -pub mod std_content_hash; -#[path = "../../stage0/src/std_decl_ref.rs"] -pub mod std_decl_ref; -#[path = "../../stage0/src/std_roster_frontier.rs"] -pub mod std_roster_frontier; -#[path = "../../stage0/src/std_disposition.rs"] -pub mod std_disposition; -#[path = "../../stage0/src/std_effects.rs"] -pub mod std_effects; -#[path = "../../stage0/src/std_emit_model.rs"] -pub mod std_emit_model; -#[path = "../../stage0/src/std_error_primitives.rs"] -pub mod std_error_primitives; -#[path = "../../stage0/src/std_execution_mode.rs"] -pub mod std_execution_mode; -#[path = "../../stage0/src/std_graph.rs"] -pub mod std_graph; -#[path = "../../stage0/src/std_induction.rs"] -pub mod std_induction; -#[path = "../../stage0/src/std_interface_summary.rs"] -pub mod std_interface_summary; -#[path = "../../stage0/src/std_iteration.rs"] -pub mod std_iteration; -#[path = "../../stage0/src/std_lens_verdict.rs"] -pub mod std_lens_verdict; -#[path = "../../stage0/src/std_magnitude.rs"] -pub mod std_magnitude; -#[path = "../../stage0/src/std_measure.rs"] -pub mod std_measure; -#[path = "../../stage0/src/std_nat.rs"] -pub mod std_nat; -#[path = "../../stage0/src/std_node.rs"] -pub mod std_node; -#[path = "../../stage0/src/std_pareto.rs"] -pub mod std_pareto; -#[path = "../../stage0/src/std_realization_schedule.rs"] -pub mod std_realization_schedule; -#[path = "../../stage0/src/std_syntax.rs"] -pub mod std_syntax; -#[path = "../../stage0/src/std_termination.rs"] -pub mod std_termination; -#[path = "../../stage0/src/std_types.rs"] -pub mod std_types; -#[path = "../../stage0/src/v1_compiler_artifact.rs"] -pub mod v1_compiler_artifact; -#[path = "../../stage0/src/v1_compiler_infer_emit_info.rs"] -pub mod v1_compiler_infer_emit_info; -#[path = "../../stage0/src/v1_compiler_infer_env.rs"] -pub mod v1_compiler_infer_env; -#[path = "../../stage0/src/v1_compiler_infer_items.rs"] -pub mod v1_compiler_infer_items; -#[path = "../../stage0/src/v1_compiler_infer_service.rs"] -pub mod v1_compiler_infer_service; -#[path = "../../stage0/src/v1_compiler_infer_sigs.rs"] -pub mod v1_compiler_infer_sigs; -#[path = "../../stage0/src/v1_compiler_infer_types.rs"] -pub mod v1_compiler_infer_types; -#[path = "../../stage0/src/v1_compiler_languages.rs"] -pub mod v1_compiler_languages; -#[path = "../../stage0/src/v1_rt.rs"] -pub mod v1_rt; -#[path = "../../stage0/src/v1_std_core.rs"] -pub mod v1_std_core; - -pub struct NonEmptyVec(Vec); - -impl std::fmt::Debug for NonEmptyVec { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - f.debug_tuple("NonEmptyVec").field(&self.0).finish() - } -} - -impl Clone for NonEmptyVec { - fn clone(&self) -> Self { - Self(self.0.clone()) - } -} - -impl PartialEq for NonEmptyVec { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } -} - -impl NonEmptyVec { - pub fn new(items: Vec) -> Result { - if items.is_empty() { - Err("NonEmptyVec requires at least one element") - } else { - Ok(Self(items)) - } - } - - pub fn into_vec(self) -> Vec { - self.0 - } -} - -#[derive(Debug, Clone, PartialEq)] -pub struct NonEmptyBTreeSet(std::collections::BTreeSet); - -impl NonEmptyBTreeSet { - pub fn new(items: std::collections::BTreeSet) -> Result { - if items.is_empty() { - Err("NonEmptyBTreeSet requires at least one element") - } else { - Ok(Self(items)) - } - } - - pub fn as_set(&self) -> &std::collections::BTreeSet { - &self.0 - } - - pub fn into_set(self) -> std::collections::BTreeSet { - self.0 - } -} diff --git a/src/v2/compiler/self_host/seed_retention_frontier.dag b/src/v2/compiler/self_host/seed_retention_frontier.dag index a7e17694c7b..761260c4c39 100644 --- a/src/v2/compiler/self_host/seed_retention_frontier.dag +++ b/src/v2/compiler/self_host/seed_retention_frontier.dag @@ -130,7 +130,6 @@ data seed_retention_frontier_roster: List = [ retained_reason_undeclared(path: "src/census_exclude_derive.rs", cause: SeedRetainedIntrinsicSource), retained_reason_undeclared(path: "src/derived_realization_schedule.rs", cause: SeedRetainedIntrinsicSource), retained_reason_undeclared(path: "src/memory_governor.rs", cause: SeedRetainedIntrinsicSource), - retained_reason_undeclared(path: "src/std_lens_verdict.rs", cause: SeedRetainedIntrinsicSource), retained_reason_undeclared(path: "src/v2_compiler_body_producer.rs", cause: SeedRetainedIntrinsicSource), retained_reason_undeclared(path: "src/v2_compiler_normalize.rs", cause: SeedRetainedIntrinsicSource), retained_reason_undeclared(path: "src/v2_compiler_target_carriers.rs", cause: SeedRetainedIntrinsicSource), diff --git a/src/v2/compiler/self_host/stage0_crate_layout.dag b/src/v2/compiler/self_host/stage0_crate_layout.dag index 8f9bbe78e5a..1803069534f 100644 --- a/src/v2/compiler/self_host/stage0_crate_layout.dag +++ b/src/v2/compiler/self_host/stage0_crate_layout.dag @@ -84,7 +84,6 @@ data seed_retained_intrinsic_registrations: List Bool { - generated_stage0_filenames |> any(f => f == join([basename, ".rs"], "")) +fn stage0_file_is_seed_retained(basename: String, filenames: List) -> Bool { + filenames |> any(f => f == join([basename, ".rs"], "")) } -fn stage0_file_has_pub_mod(basename: String) -> Bool { - generated_pub_mod_basenames |> any(b => b == basename) +fn stage0_file_has_pub_mod(basename: String, pub_mod_basenames: List) -> Bool { + pub_mod_basenames |> any(b => b == basename) } // A rostered module is admissible when the crate-layout authority does not register it as a // seed-retained file at all (it is emitter-produced, and stage0 lib.rs declares the emitted // population), or registers it AND declares a pub mod for it. The refused state is the third // combination, and it is returned by name rather than counted so the failure locates itself. -fn roster_entry_violates_pub_mod_join(basename: String) -> Bool { - stage0_file_is_seed_retained(basename: basename) && !stage0_file_has_pub_mod(basename: basename) +fn roster_entry_violates_pub_mod_join( + basename: String, + filenames: List, + pub_mod_basenames: List +) -> Bool { + stage0_file_is_seed_retained(basename: basename, filenames: filenames) + && !stage0_file_has_pub_mod(basename: basename, pub_mod_basenames: pub_mod_basenames) } -fn roster_pub_mod_violations(rows: List) -> List { +fn roster_pub_mod_violations( + rows: List, + filenames: List, + pub_mod_basenames: List +) -> List { rows |> fold(init: [], f: (acc, row) => acc |> concat( - row.modules |> filter(m => roster_entry_violates_pub_mod_join(basename: m)) + row.modules |> filter(m => roster_entry_violates_pub_mod_join( + basename: m, + filenames: filenames, + pub_mod_basenames: pub_mod_basenames + )) )) } test fn w_live_partition_roster_declares_no_undeclared_module() -> Bool { - roster_pub_mod_violations(rows: generated_partition_crate_rows) |> count == 0 + roster_pub_mod_violations( + rows: generated_partition_crate_rows, + filenames: generated_stage0_filenames, + pub_mod_basenames: generated_pub_mod_basenames + ) |> count == 0 } -// THE DISCRIMINATING RED, made green as an assertion that the detector fires. std_lens_verdict -// is cited because it is a REAL registration in the layout authority carrying has_pub_mod -// false -- a made-up name would test nothing, since the join's whole subject is agreement with -// that authority. This witness reds if the detector stops firing, and it reds if the layout -// authority ever grows a pub mod for that file, which is the honest coupling: the fixture's -// meaning depends on the same fact the live assertion does. +// THE DISCRIMINATING RED, made green as an assertion that the detector fires. The fixture +// preserves the exact formerly-live contradiction after its production rows dissolve: one +// filename registration for std_lens_verdict.rs, no matching pub mod, and one partition row +// naming the basename. It supplies both sides of the layout join explicitly because borrowing +// the accepted generated population made the RED disappear when the dead registration was +// correctly deleted. This witness reds if the detector stops firing; the live assertion above +// independently stays bound to the generated authorities. fn violating_fixture_row() -> GeneratedPartitionCrateRow { GeneratedPartitionCrateRow { package_name: "fixture-violating-crate", @@ -98,7 +116,11 @@ fn violating_fixture_row() -> GeneratedPartitionCrateRow { } test fn w_fixture_roster_naming_an_undeclared_module_is_refused() -> Bool { - let violations = roster_pub_mod_violations(rows: [violating_fixture_row()]) + let violations = roster_pub_mod_violations( + rows: [violating_fixture_row()], + filenames: ["std_types.rs", "std_lens_verdict.rs"], + pub_mod_basenames: ["std_types"] + ) (violations |> count == 1) && (violations |> any(v => v == "std_lens_verdict")) } @@ -117,5 +139,9 @@ fn clean_fixture_row() -> GeneratedPartitionCrateRow { } test fn w_fixture_roster_of_emitted_modules_is_admitted() -> Bool { - roster_pub_mod_violations(rows: [clean_fixture_row()]) |> count == 0 + roster_pub_mod_violations( + rows: [clean_fixture_row()], + filenames: generated_stage0_filenames, + pub_mod_basenames: generated_pub_mod_basenames + ) |> count == 0 }