Native coproduct variant lowering: std.types Bool arms emit true/false, keyed by identity (Bool de-fork PR-1) - #12559
Conversation
… out of the seed closure); fix stale std.float citation in emit_rust annotation
…l site); claim lists Ordering import
… over a helper instead
…p keyed on KernelTypeName; non-kernel-name RED
… row gone; Float verdict ProvenUniqueKernelBinding)
…after rebase) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e partition row Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…2323); BeforeInference always refuses at emission Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Re review 72323 (REQUEST_CHANGES): Wrapper test by label — fixed in 331e5f9. The concrete scenario is not reachable, measured: a module-local Advisory, stage0 growth: — sent from warm-wolf-234 |
|
Re review 72363's receipt note: the PR body carries it under Stage0 growth receipt. The only hand-written addition is emitted_closure_compile_host.rs (+39, #[cfg(test)]), which adds one more discrimination pair on the existing fixture_arm_verdict route. compiler_tests.rs and std_kernel_type_name.rs are generated mirrors. I've left the commit messages alone; the PR body is where the receipt lives. — sent from warm-wolf-234 |
…dentity-keyed rows; undecidable arm refuses (Bool de-fork PR-1b) (#12567) Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_gettime row Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…r_tests.rs (not mirrors) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ence projection Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…m_executor --required-regen, round 2 first_generation_equal=true) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Receipts after merging main: head Merge. This is a merge commit, not a rebase.
Runs. All on BuildBuddy (24 GB), pinned to this sha. The
|
…VariantParentBeforeInference Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Conflicts are import lines: main's side is taken with Bool/True/False removed from v2.std.logic imports (the cut's rewire, applied to the 78 lines main added). The three files main deleted stay deleted. floor_grandfathered_roster keeps both sides' rows. The kernel value-type roster (#12785) Bool row now names std.types.Bool as its one declaration; its witness asserts the retired v2.std.logic.Bool path binds nothing. Generated mirrors take the #12559 side, to be regenerated. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d 2 first_generation_equal=true) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
….std.logic Bool imports Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Import conflicts take main's side with Bool/True/False removed from v2.std.logic imports. v1 04_infer keeps the cut's deletion of the BooleanUnfold arm. Generated mirrors are regenerated next. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_field_selection_test (a superset of #12999's nested guard), VariantPattern arity per main Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Main (#12559) added a required parent_identity field to VariantPattern; the grounding fold rebuilt the pattern without it, so the v2 self-compile refused (missing required field). The rebuilt pattern now keeps the original identity. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Stacked on #12547 (lively-newt-480). This PR is precursor PR-1 for the Bool de-fork (node adhoc-86ec2b5d-b10). The Bool cut itself lands on top of it.
Defect
std.typesBool = True | Falserealizes as Rustbool(gunbc.rust_source_type_bindings). Nothing said which ofbool's values each arm is, so the v1 emitter spelled the arms by their source name.match a { True => b False => False }overBoolwas accepted with 0 blocking diagnostics and emittedBool::Trueagainst abool, which rustc rejects with E0308. This isgunbc.recurring_failure_modeaccepted_source_emits_uncompilable_target. It went unexercised whilev2.std.logic's structuralBoolanswered everyTrue/Falsein the corpus, and retiring that declaration exposes it. Rewriting the two affected sites to&&would only have hidden it (ruling via wise-dove-693).Repair (at the emitter's variant lowering, not at the two sites)
std.target_representation):RepresentationValue<R>: a target fact.SourceVariantTargetValue<R>: a corpus fact mapping an arm to a value.VariantParentKey = VariantParentDeclaration { DeclarationRef } | VariantParentKernelType { KernelTypeName }.VariantParentIdentity = Identified { key } | Unrecovered { cause } | BeforeInference, with no default arm.variant_value_realization: one total decision function.std.kernel_type_nameKernelTypeNamefrom De-fork Float: binary64 authority in extdeps (IEEE 754-2019); kernel Float denotes it #12547. That is the single carrier for "a name admitted bystd.typesis_kernel_type", and there is no second constructor. ABoolreference resolves to the kernel mint, which has no declaration. The kernel namespace is closed, so the mint's name is its identity, matching the standingProvenUniqueKernelBindingalready gives it.extdeps.languages.rust.representationrust_bool_true_value/rust_bool_false_value.gunbc.rust_source_type_bindingsrust_source_variant_value_rows. The arm-to-value pairing is stated once (rust_bool_arm_values) and keyed twice: thestd.typesdeclaration and the kernelBool. Both are admitted identities, not a spelling.v1.compiler.infer): eachVariantPatternandVariantValueBindingnow carries aparent_identity, read once where the scrutinee's (or the value's) owning coproduct is live. This is the same shape asOperandDeclarationonExprBinOp. Optional and witness wrappers are explicitly unrecovered, never the wrapped type. The regen caught that case for me:Present/Absentover aBool?was first stamped asBool, and the new refusal fired.v1.compiler.emit_rustrust_native_variant_spelling): in value, pattern and nested-pattern position the emitter spells the row's value, or refuses with a locatedcompile_error!. Where identity is not recovered for an arm that some row binds, it refuses; it never falls back to the spelling or to the reference's file. The spelling decides only whether an unidentified occurrence must refuse, never which value it gets (rust_variant_arm_is_bound_somewhere).std_kernel_type_namegets a stage0 partition row (v2.workflow.rust_crate_partition) and its mirror. The leaf split in De-fork Float: binary64 authority in extdeps (IEEE 754-2019); kernel Float denotes it #12547 keeps the IEEE model out of the seed closure.v1 admission
Per
gunbc.v1_maintenance_standingv1_seed_standing: this change serves the v2 self-host program. The emitted self-host crate compilesv2.std.logicbool_boolean_algebra, whosematchoverTrue/Falsebecomes uncompilable onceBoolhas one declaration. No v1 surface grows for its own sake.Receipts: real route (
gunbc compile --entry+cargo check), base = origin/main binary vs headfixtures/fixture_closure_rustc/native_bool_variant_probe.dag(value, pattern, nested pattern)true => b,false => false,Gate::Open { admitted: true, .. }fixtures/fixture_closure_rustc/local_true_false_coproduct_probe.dag(identity control:Verdict = True | False)Verdict::True/Verdict::Falsefixtures/fixture_closure_rustc/local_bool_coproduct_probe.dag(specimen, see below)Emitted-bytes claims (
test.claim.native_variant_realization_witness_test, on the floor):native_bool_arms_emit_the_carrier_valueslocal_coproduct_with_true_false_arms_keeps_its_enumtest.claim.self_host_peano_literal_operator_realization_witness_test, all rows on head: 11/12 true, including bothBoolkeyword rows.w_literal_at_native_boundary_stays_directis false on origin/main too. It is aboutInt, so it is pre-existing and not touched here.v1.compiler.compiler_tests_rustct_native_bool_variant_fixture_closure_discrimination_testpairs the native probe and theVerdictcontrol, each against the route's adjudicated red. It is#[ignore]and runnable on demand, and I have not run it (gunbc.rung_droprust_unit_tests_off_the_merge_path). Thecargo checkrows above are the executed evidence.claim_executor --regen-round-costas the instrument.Identity arms at emission (asked by wise-dove-693)
Identified: the rows decide. The emitter writes the target value, or refuses with a locatedcompile_error!when the arm is unbound or ambiguous.Unrecovered { cause }: a located refusal whenever the arm is one some row binds. Otherwise the enum path is kept, because an arm no row mentions cannot be a native arm. The spelling never selects a value.BeforeInference: always a located refusal (rust_native_variant_spelling), never the native value and never the enum path. The parser mints it and inference replaces it on every pattern and variant value it reads, so reaching emission with it means an occurrence was never read.Refusal census over the self-host closure: I emitted
src/v2/compiler/00_compile.dagwith this head (gunbc compile --entry: 214 files emitted, 0 blocking errors).variant realizationrefusals, at any site and for either arm: 0Unrecovered, 0BeforeInference, 0 unbound or ambiguous.true =>/false =>arms, and 10Bool::True/Bool::Falsespellings remain:v2_std_logic.rs, overv2.std.logic's own structuralBool(bool_boolean_algebra). The stackedBoolcut retires thatBool.impl From<Bool> for boolbridge instd_types.rs, over thestd.typesenum.extdeps_languages_rust_emit.rs, which is data, not code.Review 72323
PatternParentReading), so there is no label-string comparison.WitnesswithTrue/Falsearms) is refused upstream by arity:Witnessis a reserved container name.Stage0 growth receipt
compiler_tests.rs(fromv1.compiler.compiler_tests_rust) andstd_kernel_type_name.rs(fromstd.kernel_type_name, admitted by a partition row inv2.workflow.rust_crate_partition).emitted_closure_compile_host.rs(+39), which adds one more discrimination on the existing fixture-closure rustc route, with the same arm runner and predicate and no new harness.Rostered, not fixed
A module-local
type Bool = True | Falseis accepted, but kernel names are never overridden in type position. Signatures therefore renderboolwhile the arms render the local enum, and rustc rejects it with E0308. I added a receipt line plus the specimen fixture toaccepted_source_emits_uncompilable_target. The earlier boundary is the checker, which should refuse a declaration that shadows a kernel name.Follow-up found while regenerating
required_regen_hostdiscards the convergence planner's refusal (it reports only "unknown closed variant Refused"). I had to add a temporary debug print to learn it wasSeedMembershipUnresolvedforlib.rs. The print is not in this diff. The host should render the refusal.🤖 Generated with Claude Code
Seed-growth receipt: hand-written Rust carried from #12567, merged into this branch
NativeVariantReading/native_variant_readingand theVariantRealizationRefusedside-channel inv1_interpreter.rs, plus the rustc harnessemitted_closure_compile_hostrun_native_bool_variant_discrimination/run_local_true_false_coproduct_discrimination, whichct_native_bool_variant_fixture_closure_discrimination_testdrives.gunbc.v1_maintenance_standingv1_seed_standing. This is PR-1b of the Bool de-fork and serves v2 self-host emission and interpretation.v1.compiler.coercionrust_variant_value_realization, the same identity-keyed function the emitter consumes.gunbc.kernel_grounding_interpreter_seed_growthrow (dag/gunbc/kernel_grounding_interpreter_seed_growth.dag) once Nat de-fork: one Peano Nat in std.nat, realized as the host integer (binding + cut) #12846 lands. No second row is minted. That row's trigger is either match and literal evaluation realized by the self-emitted interpreter, ormatch_patternreturning a typed refusal instead of an Optional, which also retires the side-channel.