Repository navigation
Measured compile: a unit variant is bound through its parent coproduct (std.measure census 147 -> 0) - #12132
Conversation
…t, so std.measure's phantom type arguments stop reading as missing imports The measure compile_dag_diagnostic_census arms (gunbc.type_ref_hit_ne_bind_measure) charged every bare leaf without a binding of its own to a missing import. A zero-payload variant never has one -- its binding is its declaring coproduct's -- so std.measure's Measure<Memory, One, Nat> produced 147 blocking UnresolvedType rows in a census of a source importing std.measure alone, while the unmeasured resolve admitted the same leaves: two routes of one compiler answering one question opposite ways. type_ref_measure_binding_authority gains the arm the resolver's unit_variant_index already answers (built only from bindings visible to the env); an unobserved index stays strict. Mirror regenerated with --required-regen; only this change's hunk is installed (the candidate also carries 31 files of pre-existing main drift, not taken here). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-206-unit-variant-binding-2
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
SOURCE HOLD at GitHub's current exact head 176d391ee26ca2521464f51ff8a48570666ced32.
(The request named 36529891527…; that is not #12132's head. I bound this review to the current PR head reported by GitHub.)
The diagnosis is correct: the measured compile must not call std.measure's visible zero-payload variants unresolved when the ordinary resolver binds them through their parent coproduct. Keeping the change measurement-only, leaving an unobserved index strict, and regenerating only the corresponding stage0 hunk are the right boundaries. Two source walls remain.
1. An index key is not the same fact as one resolvable visible unit variant
type_ref_unit_variant_parent_is_bound currently returns true for any map_get(env.unit_variant_index, name) hit. The ordinary resolver's canonical lookup_unit_variant_phantom_type is stricter: it sums every contribution and resolves only when the total is exactly one; zero or several refuse. Its source explicitly states that duplicate names within one coproduct and multiple visible variants with the same leaf both refuse.
The index can also retain an outer key with an empty contribution map: unit_variant_index_remove_binding reinserts contributions_without_key(...) even when the last contribution was removed during shadowing. Thus map_get may be Present for total 0 as well as total >1.
This head can therefore suppress the measured UnresolvedType for a leaf the ordinary route does not bind—the same two-route fork the PR is intended to eliminate.
Use one shared cardinality judgment over the index, approximately:
index observed
AND sum(all contribution.count for this leaf) == 1
Prefer moving/exposing that judgment so both lookup_unit_variant_phantom_type and the measurement arm consume the same authority, rather than reimplementing it twice.
Required REDs/controls:
- two visible parent coproducts each declare
Alpha->Alpharemains unbound/charged; - one coproduct contains duplicate zero-payload
Alphaarms -> remains unbound/charged; - shadowing removes the last visible contributor while the outer index key remains -> remains unbound/charged;
- exactly one visible parent contribution -> accepted;
- the existing transitive-only parent control -> still charged.
2. The maintenance receipt incorrectly says there is no public-surface growth
The PR adds a new top-level v1 declaration, type_ref_unit_variant_parent_is_bound, and the generated stage0 mirror exports it as:
pub fn type_ref_unit_variant_parent_is_bound(...)The repository's own v1 maintenance standing records that stage0-added pub fn visibility counts as PublicSurfaceGrowth; that refusal class dominates ordinary purpose-test admission unless an exact exception is authorized. The new admission note nevertheless says “no public surface growth.” That classification is false.
The fastest repair is also the lower-concept shape: this helper has one consumer, so inline the exact-one-contribution fold into the existing type_ref_measure_binding_authority and regenerate the mirror. That removes the new exported declaration entirely. Otherwise the PR needs an explicit exact-subject authorization for the public growth, not a note saying the class does not fire.
After repair, rerun the three unit-variant claims plus the new ambiguity/shadow controls, the 8/8 phantom-marker population, the full 74-file census regression comparison, and exact-head required CI. I found no separate blocker in the measurement-only scope, the main-vs-mirror hunk discipline, or the corrected v1 purpose justification once the public-surface statement is made honest.
…ck for a main-wide measured-compile defect, dissolving on gunbc#12132 The census of the hold-store harness reaches std.measure through cas_slot_keys' std.decimal import (bisected to 9945e92), and the measured compile charges std.measure's own unit variants, passed as phantom type arguments, as missing imports. Enrolled through explicit_witness_admission known_red_probe rather than deleted or loosened; the trigger names the capability #12132 delivers. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ssion recorded as an annotation, not a String row - lookup_unit_variant_phantom_type / UnitVariantPhantomLookup move from v1.compiler.infer_resolve to v1.compiler.infer_env (owner of unit_variant_index); infer_resolve and emit_rust import it from there. - type_ref_measure_binding_authority consumes it inline (no new declaration), so the measure binds exactly what resolve resolves instead of any key present in the index (review: side chat 5289240229). - The v1 purpose-test admission moves from a String data row to a // annotation on the admitted declaration, and states the relocation of the pub set instead of denying growth (review 70469). - Answer controls for two parents, a duplicate arm and a shadow-emptied key, labelled as answer controls: a key-presence mutation leaves them green because the resolver/emitter route refuses first. - Mirrors regenerated with --required-regen and installed by three-way merge against a clean-main candidate (merge-file committed clean mine), so pre-existing main drift is not taken. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
SOURCE HOLD at exact head 757bb621402212be81da216c0648eb46ca0fe15b.
The source construction itself now answers both findings from review 5289240229 correctly:
lookup_unit_variant_phantom_typehas moved tov1.compiler.infer_env, beside theunit_variant_indexit judges, and the resolver, Rust emitter, and measured-compile authority all consume that ONE exact-one judgment. Zero, many, duplicate-arm and unobserved states therefore cannot diverge through a second implementation.- The one-consumer
type_ref_unit_variant_parent_is_bounddeclaration is gone. The maintenance annotation now states the actual public-set relocation instead of denying public-surface movement, and the generated mirrors are limited to the intended three-way-merged hunks. - The six census claims are honest answer controls. I accept that the two-parent, duplicate-arm, and shadow fixtures refuse before the measured binding predicate becomes outcome-determining; labeling them as answer controls rather than pretending the key-presence mutation discriminates them is correct.
One evidence wall remains, because there IS a direct route to the measured predicate with a non-exact-one key.
Exercise type_ref_measure_binding_authority directly through the existing generated-Rust test authority
src/v1/compiler_tests_rust.dag already uses exactly the needed fixture shape: it clones crate::v1_compiler_infer_env::empty_type_env(), authors unit_variant_index, sets unit_variant_index_observed = true, and drives an infer/emit function. Use that existing test authority to call the measured predicate itself:
let mut env_value = (*crate::v1_compiler_infer_env::empty_type_env()).clone();
env_value.str_bindings = empty;
env_value.ancestry_str_bindings = empty;
env_value.unit_variant_index_observed = true;
env_value.unit_variant_index = ...;
let env = Rc::new(env_value);
crate::v1_compiler_infer_env::type_ref_measure_binding_authority(
env,
"Alpha".to_string(),
)With the ordinary binding maps empty, arm 1 cannot intercept the query, so the test reaches the new unit-variant arm directly. Author at least these cases:
- one parent contribution with
count = 1-> true; - two parent contributions, each
count = 1-> false; - one parent contribution with
count = 2-> false; - an outer
Alphakey whose inner contribution map is empty -> false; - optionally, the same one-contribution map with
unit_variant_index_observed = false-> false.
The variant node may be the same harmless node reused by the existing unit-variant emitter fixture; only contribution cardinality is under judgment.
The discriminating mutation is now available: replace the helper call/answer with bare outer-key presence. The many- and empty-key tests must fail while the exact-one positive remains green. This is the specific wall the end-to-end census controls cannot provide, because their resolver/emitter diagnostics dominate first.
Keep the six census claims. Together the two layers establish different facts:
- census claims: the compiler's externally observed answers remain correct;
- direct host test: the measured binding authority itself really consumes exact-one rather than key presence.
This is not a request to invent a production route that reaches an otherwise dominated branch. It uses the repository's existing white-box seed-test boundary for the exact helper this PR relocates and makes load-bearing.
I found no further source blocker in the shared helper placement, resolver/emitter repointing, measurement-only scope, public-surface account, or mirror merge discipline.
Landing also remains contingent on the completed 74-file fixed-vs-base census comparison and exact-head required CI. The PR body is still the pre-repair account (type_ref_unit_variant_parent_is_bound, key-presence semantics, three claims, String admission row); refresh it to the shared exact-one helper, six answer controls, direct discriminating test, and final 74-file receipt.
…ntribution is visible Five generated compiler_tests (src/v1/compiler_tests_rust.dag ct_measure_unit_variant_exact_one_test) call type_ref_measure_binding_authority over an env with EMPTY str_bindings, so only the contribution map decides: one parent once binds; two parents, one parent twice, an emptied outer key, and an unobserved index do not. Mutating the arm to bare key presence fails exactly the two-parent, twice and emptied-key tests. Mirrors: v1_compiler_compiler_tests_rust.rs from the first regen, compiler_tests.rs from the second generation, each installed by three-way merge against a clean-main candidate. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
SOURCE APPROVE at exact head 038e3ac11ddee7f7d29e03b96bfc98e0444f661c, superseding REQUEST_CHANGES review 5290446232.
The requested discriminating boundary is now present and correctly generated.
Direct measured-authority route
ct_measure_unit_variant_exact_one_test generates five Rust tests that call v1_compiler_infer_env::type_ref_measure_binding_authority directly. The helper starts from empty_type_env(), changes only unit_variant_index and unit_variant_index_observed, and therefore leaves str_bindings, ancestry_str_bindings, parents and the symbol index empty. The ordinary-binding arm cannot answer the query; the tests reach the unit-variant branch itself.
The supplied states cover the load-bearing partition:
- one parent with count 1 -> bound;
- two parents with count 1 each -> unbound;
- one parent with count 2 -> unbound;
- an outer key with an empty contribution map -> unbound;
- an otherwise valid contribution under an unobserved index -> unbound.
The reported mutation from the shared exact-one judgment to outer-key presence is genuinely discriminating: the two-parent, count-2 and empty-map tests fail while the exact-one positive and unobserved-index control remain green. This is the white-box complement the prior review required; the six census claims can remain honest answer controls for the externally observed compiler behavior.
Generated-source chain
The delta from 757bb621402 is one commit and exactly three files:
src/v1/compiler_tests_rust.dag, the generator authority;src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs, its first-generation mirror;src/v1/stage0/src/compiler_tests.rs, the second-generation generated test output.
The generated Rust tests match the .dag source in helper shape, five cases and expectations. No production compiler source or previously approved exact-one construction moved in this delta, and no unrelated stage0 drift is present.
I therefore accept the shared-helper placement, resolver/emitter/measure convergence, inlined measure arm, public-surface relocation account, six census controls, and the new direct mutation-tested evidence.
Conditions before landing
This is source approval, contingent on the evidence the author already names:
- Complete the full 74-file fixed-versus-unfixed census sweep on this exact source and report every file. Any pass/fail delta beyond the intended unit-variant false positives needs adjudication rather than being summarized as a count.
- Refresh the PR body: it currently describes the superseded key-presence helper, three-claim evidence set and old mirror story. Record the shared exact-one judgment, six answer controls, five white-box tests, mutation result, full sweep and exact head.
- Require exact-head CI green. At review time clippy is green; compiler, floor and emit-build are running.
No additional source change is required by this review. If the sweep or CI moves the SHA, rebind the approval to the resulting exact head.
briansrls
left a comment
There was a problem hiding this comment.
SOURCE APPROVE at exact head 038e3ac11ddee7f7d29e03b96bfc98e0444f661c, superseding REQUEST_CHANGES review 5290446232.
The requested discriminating white-box boundary is now present and correctly generated.
ct_measure_unit_variant_exact_one_test constructs an otherwise-empty TypeEnv, writes only unit_variant_index, and calls v1_compiler_infer_env::type_ref_measure_binding_authority directly. Because str_bindings and ancestry_str_bindings remain empty, the ordinary binding arm cannot intercept. The five cases cover exactly the judgment at issue:
- one contribution from one parent -> bound;
- one contribution from each of two parents -> unbound;
- count two from one parent -> unbound;
- present outer key with an empty contribution map -> unbound;
- unobserved index -> unbound.
The reported mutation from the shared exact-one judgment to bare outer-key presence is discriminating: it fails the two-parent, count-two, and empty-map tests while preserving the unique positive and unobserved-index control. That closes the evidence gap without inventing a fake census route. The six end-to-end census claims remain useful answer controls beside it.
The source-of-truth/generated relationship also holds: the test is authored in src/v1/compiler_tests_rust.dag; the first-generation v1_compiler_compiler_tests_rust.rs emits it; the second-generation compiler_tests.rs contains the formatted Rust tests. I found no hand-only insertion or new public helper.
No further source finding remains in the shared exact-one helper placement, measured-compile arm, resolver/emitter repointing, v1 admission annotation, or mirror-install method.
This is source approval, not a landing receipt. Before merge, require:
- the complete 74-file fixed-vs-unfixed census sweep on this exact source family, with every divergence accounted for;
- the PR body refreshed from its superseded key-presence/three-control description to the shared exact-one implementation, six answer controls, five direct compiler tests, and full sweep table;
- exact-head required CI on
038e3ac11dd(none was registered when reviewed).
Any source change made while refreshing evidence requires an exact-head rebind.
Census regression sweep at exact head
|
| file | roster | fixed P/F | base P/F | verdict |
|---|---|---|---|---|
dag/gunbc/explicit_witness_admission.dag |
0 | 0/0 | 0/0 | no test fns |
dag/test/claim/admit_callers_roster_integrity_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/algebra_expansion_evidence_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/algebra_receiver_alias_witness_test.dag |
4 | 1/3 | 1/3 | match |
dag/test/claim/algebra_receiver_callable_witness_test.dag |
11 | 5/6 | 5/6 | match |
dag/test/claim/argument_shape_at_a_declared_position_probe_test.dag |
4 | 2/2 | 2/2 | match |
dag/test/claim/arity_zero_import_refusal_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/brand_nominal_identity_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/callable_candidate_ambiguity_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/census_app_acquisition_refusal_probe_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/citation_cause_subject_disjointness_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/compile_accepted_unevaluable_program_control_test.dag |
6 | 3/3 | 3/3 | match |
dag/test/claim/compile_diagnostic_census_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/data_class_refusal_probe_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/declared_type_expected_type_path_witness_test.dag |
19 | 13/6 | 13/6 | match |
dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag |
33 | 32/1 | 32/1 | match |
dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/direct_call_argument_type_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/duplicate_definition_binding_probe_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/duplicate_record_field_refusal_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/effectful_item_kind_collapse_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/emitter_unprojectable_construct_refuse_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/empty_list_element_fabrication_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/fabric/fabric_output_contract_resolution_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/fabric_m0_job_ending_seal_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/fabric_m0_origin_readback_seal_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/file_hold_plan_refusal_probe_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/fleet/fleet_converge_launch_scope_non_interference_test.dag |
5 | 5/0 | 0/0 | TRUNCATED |
dag/test/claim/fleet_observation_seal_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/generic_effectful_declaration_wall_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/generic_lambda_parameter_binding_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/guarantee_floor_class_probe_witness_test.dag |
17 | 14/3 | 14/3 | match |
dag/test/claim/guarantee_probe_corpus_witness_test.dag |
53 | 50/3 | 50/3 | match |
dag/test/claim/import_admission_closure_membership_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/infer_nullary_local_callable_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/infer_record_field_completeness_zero_field_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/infer_record_lit_variant_field_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/inventory_admitted_ledger_seal_livetree_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/lambda_receiver_type_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/long/where_refinement_enforcement_witness_test.dag |
48 | 42/6 | 42/6 | match |
dag/test/claim/machine_intake/no_fallback_plan_ineligibility_wall_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/machine_intake/predictive_claim_construction_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/marker_argument_not_consulted_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/match_exhaustiveness_coproduct_witness_test.dag |
26 | 26/0 | 26/0 | match |
dag/test/claim/namespace_step0_subject_collector_witness_test.dag |
15 | 15/0 | 15/0 | match |
dag/test/claim/operation_admit_callers_inert_witness_test.dag |
2 | 1/1 | 1/1 | match |
dag/test/claim/optional_at_required_position_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/optional_cast_wall_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/payload_arm_excess_field_admission_test.dag |
11 | 4/7 | 4/7 | match |
dag/test/claim/pipeline_transport_emit_rest_shell_witness_test.dag |
25 | 25/0 | 25/0 | match |
dag/test/claim/printed_chassis_admitted_realization_seal_witness_test.dag |
12 | 12/0 | 12/0 | match |
dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/process_lease_plan_is_not_a_refusal_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/qualified_pattern_head_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/record_decl_spelling_identity_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/record_literal_call_arg_handoff_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/refinement_seam_enforcement_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/review_sheet_batch_actuator_witness_test.dag |
28 | 28/0 | 28/0 | match |
dag/test/claim/review_sheet_header_init_refusal_probe_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/review_sheet_header_schema_witness_test.dag |
12 | 12/0 | 12/0 | match |
dag/test/claim/review_sheet_tab_refusal_probe_witness_test.dag |
10 | 10/0 | 10/0 | match |
dag/test/claim/self_host_equality_admission_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/sole_constructor_completeness_audit_probe_test.dag |
26 | 20/6 | 20/6 | match |
dag/test/claim/sole_constructor_type_head_exposure_witness_test.dag |
6 | 5/1 | 5/1 | match |
dag/test/claim/spark/spark_declared_unit_digest_seal_probe_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/test_reference_wall_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/transport_emission_not_modeled_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/transport_field_refusal_witness_test.dag |
13 | 13/0 | 13/0 | match |
dag/test/claim/type_argument_kind_inhabitance_witness_test.dag |
6 | 5/1 | 5/1 | match |
dag/test/claim/type_ref_hit_ne_bind_measure_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/type_reference_resolve_changeover_equivalence_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/unit_variant_binding_authority_witness_test.dag |
6 | 6/0 | -/- | new on branch |
dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/manual/command_runner_local_argv_receipt_test.dag |
6 | 0/6 | 0/6 | match |
dag/test/retirement/model.dag |
0 | 0/0 | 0/0 | no test fns |
src/v1/compiler_tests_rust.dag |
0 | 0/0 | 0/0 | no test fns |
src/v1/tests/claim/bare_variant_reference_occurrence_control_test.dag |
1 | 0/0 | 0/0 | TRUNCATED |
src/v1/tests/claim/type_declaration_occurrence_control_test.dag |
1 | 0/0 | 0/0 | TRUNCATED |
Census regression sweep at exact head
|
| file | roster | fixed P/F | base P/F | verdict |
|---|---|---|---|---|
dag/gunbc/explicit_witness_admission.dag |
0 | 0/0 | 0/0 | no test fns |
dag/test/claim/admit_callers_roster_integrity_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/algebra_expansion_evidence_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/algebra_receiver_alias_witness_test.dag |
4 | 1/3 | 1/3 | match |
dag/test/claim/algebra_receiver_callable_witness_test.dag |
11 | 5/6 | 5/6 | match |
dag/test/claim/argument_shape_at_a_declared_position_probe_test.dag |
4 | 2/2 | 2/2 | match |
dag/test/claim/arity_zero_import_refusal_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/brand_nominal_identity_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/callable_candidate_ambiguity_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/census_app_acquisition_refusal_probe_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/citation_cause_subject_disjointness_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/compile_accepted_unevaluable_program_control_test.dag |
6 | 3/3 | 3/3 | match |
dag/test/claim/compile_diagnostic_census_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/data_class_refusal_probe_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/declared_type_expected_type_path_witness_test.dag |
19 | 13/6 | 13/6 | match |
dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag |
33 | 32/1 | 32/1 | match |
dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/direct_call_argument_type_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/duplicate_definition_binding_probe_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/duplicate_record_field_refusal_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/effectful_item_kind_collapse_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/emitter_unprojectable_construct_refuse_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/empty_list_element_fabrication_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/fabric/fabric_output_contract_resolution_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/fabric_m0_job_ending_seal_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/fabric_m0_origin_readback_seal_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/file_hold_plan_refusal_probe_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/fleet/fleet_converge_launch_scope_non_interference_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/fleet_observation_seal_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/generic_effectful_declaration_wall_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/generic_lambda_parameter_binding_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/guarantee_floor_class_probe_witness_test.dag |
17 | 14/3 | 14/3 | match |
dag/test/claim/guarantee_probe_corpus_witness_test.dag |
53 | 50/3 | 50/3 | match |
dag/test/claim/import_admission_closure_membership_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/infer_nullary_local_callable_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/infer_record_field_completeness_zero_field_witness_test.dag |
5 | 5/0 | 5/0 | match |
dag/test/claim/infer_record_lit_variant_field_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/inventory_admitted_ledger_seal_livetree_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/lambda_receiver_type_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/long/where_refinement_enforcement_witness_test.dag |
48 | 42/6 | 42/6 | match |
dag/test/claim/machine_intake/no_fallback_plan_ineligibility_wall_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/machine_intake/predictive_claim_construction_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/marker_argument_not_consulted_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/match_exhaustiveness_coproduct_witness_test.dag |
26 | 26/0 | 26/0 | match |
dag/test/claim/namespace_step0_subject_collector_witness_test.dag |
15 | 15/0 | 15/0 | match |
dag/test/claim/operation_admit_callers_inert_witness_test.dag |
2 | 1/1 | 1/1 | match |
dag/test/claim/optional_at_required_position_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/optional_cast_wall_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/payload_arm_excess_field_admission_test.dag |
11 | 4/7 | 4/7 | match |
dag/test/claim/pipeline_transport_emit_rest_shell_witness_test.dag |
25 | 25/0 | 25/0 | match |
dag/test/claim/printed_chassis_admitted_realization_seal_witness_test.dag |
12 | 12/0 | 12/0 | match |
dag/test/claim/printed_chassis_manufacturing_manifest_livetree_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/process_lease_plan_is_not_a_refusal_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/qualified_pattern_head_witness_test.dag |
2 | 2/0 | 2/0 | match |
dag/test/claim/record_decl_spelling_identity_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/record_literal_call_arg_handoff_witness_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/refinement_seam_enforcement_witness_test.dag |
7 | 7/0 | 7/0 | match |
dag/test/claim/review_sheet_batch_actuator_witness_test.dag |
28 | 28/0 | 28/0 | match |
dag/test/claim/review_sheet_header_init_refusal_probe_witness_test.dag |
6 | 6/0 | 6/0 | match |
dag/test/claim/review_sheet_header_schema_witness_test.dag |
12 | 12/0 | 12/0 | match |
dag/test/claim/review_sheet_tab_refusal_probe_witness_test.dag |
10 | 10/0 | 10/0 | match |
dag/test/claim/self_host_equality_admission_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/claim/sole_constructor_completeness_audit_probe_test.dag |
26 | 20/6 | 20/6 | match |
dag/test/claim/sole_constructor_type_head_exposure_witness_test.dag |
6 | 5/1 | 5/1 | match |
dag/test/claim/spark/spark_declared_unit_digest_seal_probe_test.dag |
3 | 3/0 | 3/0 | match |
dag/test/claim/test_reference_wall_witness_test.dag |
11 | 11/0 | 11/0 | match |
dag/test/claim/transport_emission_not_modeled_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/transport_field_refusal_witness_test.dag |
13 | 13/0 | 13/0 | match |
dag/test/claim/type_argument_kind_inhabitance_witness_test.dag |
6 | 5/1 | 5/1 | match |
dag/test/claim/type_ref_hit_ne_bind_measure_witness_test.dag |
8 | 8/0 | 8/0 | match |
dag/test/claim/type_reference_resolve_changeover_equivalence_witness_test.dag |
4 | 4/0 | 4/0 | match |
dag/test/claim/unit_variant_binding_authority_witness_test.dag |
6 | 6/0 | -/- | new on branch |
dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag |
9 | 9/0 | 9/0 | match |
dag/test/manual/command_runner_local_argv_receipt_test.dag |
6 | 0/6 | 0/6 | match |
dag/test/retirement/model.dag |
0 | 0/0 | 0/0 | no test fns |
src/v1/compiler_tests_rust.dag |
0 | 0/0 | 0/0 | no test fns |
src/v1/tests/claim/bare_variant_reference_occurrence_control_test.dag |
1 | 1/0 | 1/0 | match |
src/v1/tests/claim/type_declaration_occurrence_control_test.dag |
1 | 1/0 | 1/0 | match |
The merge of main (which carries #12132 and #11985, both touching the emitter) took main's pristine v1_compiler_emit_rust.rs; --required-regen then produced the candidate from the joined 05_emit_rust.dag and only that file was installed. A second regeneration round produced a byte-identical file (per-file fixed point, sha256 6297b8140753fc63). Main's regen round still refuses on #12011's release_locus_seed_constants_generated.rs; that belongs to the mirror-reconciliation lane and nothing is installed for it here. All nine Pkg15 witness arms green on the regenerated mirror. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…(its dissolution, #12132, landed) The #filter bare-provider refusal that hid its verdict was already retired by #12609. On main 785934a the probe PASSES, which its own dissolution names as the row's deletion condition. The nine algebra_receiver probes remain red (re-measured on the same main). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Defect
Two routes of one compiler answered one question in opposite ways. The question: does
std.measure'sMeasure<Memory, One, Nat>resolve, whereMemoryandOneare std.measure's ownQuantityand scale unit variants passed as phantom type arguments?lookup_unit_variant_phantom_typeresolves the leaves.compile_dag_diagnostic_censusarms,gunbc.type_ref_hit_ne_bind_measure): charged every such leaf with a blockingUnresolvedType, becausetype_ref_measure_binding_authorityhad no arm for a zero-payload variant.As a result, a census of a source that imports
std.measureand nothing else reported 147 blocking rows on main. Every census whose closure reaches std.measure read red for a reason that isn't its subject. std.decimal reaches it through std.bytes → std.integer. That's how #12000's stack (cas_slot_keysimporting std.decimal) turnedtest.claim.file_hold_plan_refusal_probe_witness_testthe_harness_runs_and_a_clean_source_over_the_hold_store_is_cleanred. It bisects to 9945e92, and its parent is clean.Which side is right
The measure is wrong. A unit variant has no binding of its own: its binding is its declaring coproduct's. The resolver already owns the judgment of when a bare leaf names exactly one visible unit variant, so the measure must consume that judgment, not restate it.
Change
lookup_unit_variant_phantom_typeandUnitVariantPhantomLookupmove fromv1.compiler.infer_resolvetov1.compiler.infer_env, beside theunit_variant_indexthey judge. The move is needed so the measure can consume them without an import cycle. The resolver and the Rust emitter keep consuming the same function.type_ref_measure_binding_authoritygains an inline arm. A bare leaf is bound ifflookup_unit_variant_phantom_typeanswersUnitVariantPhantomPresent, meaning exactly one visible contribution with count 1. Zero contributions, two parents, one parent declaring it twice, a shadow that empties the key, and an unobserved index all answer unbound. No new pub fn is emitted, so the pub set moves and does not grow. No exemption is added, and the measure is armed exactly as before.type_ref_unit_variant_parent_is_boundis gone. Key presence is not the resolver's contract: the white-box tests below fail under it.gunbc.v1_maintenance_standingv1_seed_standing, instanceDefectRepairDiagnosticsMayMove) is recorded as a//annotation beside the arm it admits (DESIGN §4c). No String data row is added.gunbc.type_ref_hit_ne_bind_measureis updated to the three-arm authority.claim_executor --required-regenand installed only by three-way merge against a clean-main candidate. Main carries about 31 files of pre-existing mirror drift, which this PR does not take.compiler_tests.rsgot its second generation after its generator mirror was installed.Evidence
Census answer controls: six claims in
test.claim.unit_variant_binding_authority_witness_test, all passing on this head (6/6, re-run in the sweep below).a_source_importing_only_std_measure_is_clean_under_the_measured_compile(147 → 0)a_variant_of_an_imported_coproduct_is_bound_as_a_type_argumenta_variant_whose_parent_is_not_bound_is_still_charged_by_the_measurea_variant_declared_by_two_visible_coproducts_is_refused_as_ambiguousa_variant_declared_twice_by_one_coproduct_is_refuseda_variant_whose_only_parent_is_shadowed_is_refusedThe last three are answer controls, not discriminators of the measure: the resolver or emitter refuses those leaves before the measure decides.
Direct discriminating boundary: the white-box test generator
ct_measure_unit_variant_exact_one_test(inv1.compiler.compiler_tests_rust) emits five Rust tests. Each drivestype_ref_measure_binding_authorityover an otherwise-emptyTypeEnv, so only the contribution map decides:All five pass. Replacing the judgment with bare key presence fails exactly the two-parent, count-2 and emptied-key tests. These white-box results and the mutation were run by the previous owner and accepted in review 5291522360; I did not re-run them.
Neighbouring witnesses:
phantom_marker_type_argument_identity_witness_testpasses 8/8, per the previous owner's run (it does not call the census, so it is outside the sweep).Regression sweep: every witness file that calls
compile_dag_diagnostic_censusorcompile_census_probewas run withclaim_batchbuilt from this head and with an unfixedclaim_batchbuilt from the branch's merge-base, 034aef0. The table and verdicts are in the PR comments: no comparable file differs from base, and the one red file fails identically on base.Exact-head CI on
038e3ac11dd: clippy, compiler, emit-build, floor and witnesses all pass.Recorded, not changed
Arm (1) treats a coproduct name reached only transitively as bound: it draws only the advisory
UnlistedImportUse. The variant arm is stricter than that on the same fixture. This is the existing grain of arm (1), and this PR doesn't touch it.🤖 Generated with Claude Code