Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
8882562
WIP: Float de-fork (binary64 in extdeps, kernel type denotation)
Sep 28, 2026
64b8081
kernel_type_denotation: one KernelTypeName carrier, admitted only via…
Sep 28, 2026
59d8efb
Split KernelTypeName into leaf std.kernel_type_name (keeps IEEE model…
Sep 28, 2026
15f9e25
ieee_754_2019: cite helper takes NonEmptyStr (literals checked at cal…
Sep 28, 2026
5180d42
defork census: Float resolution cites #12547
Sep 28, 2026
f99d503
rust primitives: drop unimported 'any' (UnimportedBareProvider); fold…
Sep 28, 2026
4ebb3c4
RustFloatBinding holds the KernelTypeName admission; denotation looku…
Sep 28, 2026
42f2322
Regenerate stage0 gunbc_rust_source_type_bindings.rs (std.float Float…
Sep 28, 2026
9aaeb66
Regenerate dag-v2-defork-audit projection (Float resolved, #12547)
Sep 28, 2026
c3f44b2
WIP: native coproduct variant lowering (sources; mirrors regenerated …
Sep 28, 2026
3b1eecb
WIP: kernel arm holds std.kernel_type_name KernelTypeName
Sep 28, 2026
486a84b
stage0 regen: native coproduct variant lowering + std.kernel_type_nam…
Sep 28, 2026
c63819e
stage0 regen after restack onto #12547 head
Sep 28, 2026
331e5f9
Wrapper-ness decided in the same branch as the parent label (review 7…
Sep 28, 2026
2e9c573
Interpreter: std.types Bool arms realize as host bool from the same i…
gunbai-bot[bot] Oct 2, 2026
e4efafc
Merge origin/main into bool-variant-lowering
Oct 2, 2026
6b25196
Merge: union the std_kernel_type_name partition row with main's clock…
Oct 2, 2026
def1adc
Merge: three-way merge of hand-authored v1_interpreter.rs and compile…
Oct 2, 2026
bb5f229
census_heads: carry VariantPattern parent_identity through the occurr…
Oct 2, 2026
dbca6a2
Regenerate stage0 mirrors to the fixed point after merging main (clai…
Oct 2, 2026
02faba9
infer_semantics_witness: pre-inference VariantPattern fixtures carry …
Oct 2, 2026
1a6df4a
Merge origin/main (with #12980) into bool-variant-lowering
Oct 2, 2026
0c0a5ee
Regenerate stage0 mirrors to the fixed point after merging main (roun…
Oct 2, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion dag/extdeps/languages/rust/representation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module extdeps.languages.rust.representation

import std.types { List, String, Bool, NonEmptyStr }
import std.coercion { TypeCheckpoint }
import std.target_representation { RepresentationSpelling, SourceTypeTargetBinding }
import std.target_representation { RepresentationSpelling, SourceTypeTargetBinding, RepresentationValue }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }

Expand Down Expand Up @@ -113,3 +113,11 @@ fn rust_exact_type_checkpoint(binding: SourceTypeTargetBinding<RustRepresentatio
Absent => none
}
}

// THE VALUES A REPRESENTATION HAS, spelled, where a source coproduct's arms realize onto them. Target
// facts only, naming no source declaration: the Rust Reference (types, "Boolean type") gives `bool`
// exactly two values, `true` and `false`. Which source arm means which value is the corpus's fact
// (gunbc.rust_source_type_bindings rust_source_variant_value_rows).
data rust_bool_true_value: RepresentationValue<RustRepresentation> = RepresentationValue { representation: RustBool, value_spelling: "true" as NonEmptyStr }
data rust_bool_false_value: RepresentationValue<RustRepresentation> = RepresentationValue { representation: RustBool, value_spelling: "false" as NonEmptyStr }
data rust_representation_values: List<RepresentationValue<RustRepresentation>> = [rust_bool_true_value, rust_bool_false_value]
2 changes: 2 additions & 0 deletions dag/gunbc/observation_ci_render.dag
Original file line number Diff line number Diff line change
Expand Up @@ -932,6 +932,7 @@ type CiWitnessRuntimeCause
| WitnessCauseTypeError
| WitnessCauseCrossRepresentationEquality
| WitnessCauseStringRealizationStraddle
| WitnessCauseVariantRealizationRefused
| WitnessCausePoolRootContributesNothing
| WitnessCausePatternMatchFailure
| WitnessCauseDivisionByZero
Expand Down Expand Up @@ -961,6 +962,7 @@ fn ci_witness_runtime_cause_token(cause: CiWitnessRuntimeCause) -> String {
WitnessCauseTypeError => "type-error"
WitnessCauseCrossRepresentationEquality => "cross-representation-equality"
WitnessCauseStringRealizationStraddle => "string-realization-straddle"
WitnessCauseVariantRealizationRefused => "variant-realization-refused"
WitnessCausePoolRootContributesNothing => "pool-root-contributes-nothing"
WitnessCausePatternMatchFailure => "pattern-match-failure"
WitnessCauseDivisionByZero => "division-by-zero"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -298,6 +298,8 @@ data accepted_source_emits_uncompilable_target: RecurringFailureMode = Recurring
"OCCURRENCE, 2026-09-24 (wise-hawk-615, routed from stern-raven-24's native App Attest row gunbc#12251, whose emitted crate refused at rustc with 45 errors in three emitter classes and one runtime-library gap). Each was worked to its earliest unjustified boundary (DESIGN section 6b) rather than at the call site. (C) STRING ORDERING: `a < b` over Timestamp, an alias of String (extdeps.standards.rfc_5280 x509_validity_at, gunbc.auth.approval_capability utc_instant_before). Timestamp comparison needed no new typed ordering: the interpreter already orders Strings byte-lexicographically, so the defect was the emitter's. The boundary was the operand classifier v1.compiler.emit_rust rust_operand_realization_of_type, which filed the corpus String as OperandIdentityUnavailable although the type renderer realizes it as the host text carrier by is_host_text_carrier_type; ordering then refused by operator class while `==` on the same operand passed. Repair: std.operator_realization HostRealizationReason gains HostTextCarrier and the classifier reads the renderer's own predicate, so both answer one question once; is_string_comparison admits the four ordering operators through the same host-string seam as equality, and an ordering over an OPTIONAL String refuses at emission (the interpreter has no Null-vs-Str ordering; Option's None-first order would be fabricated). (A) PRESENT BINDING: `match opt { null => a o => b }` bound the whole Option in emitted code (E0308, E0609) while v1.compiler.infer narrows `o` to the present value. ALL THREE match renderings now read the checker's optional_scrutinee_binding_is_present over match_unguarded_absent_arm_index and emit `Some(o)` in exactly that arm, never re-deriving the narrowing: emit_typed_match_arm_strs for ordinary matches, and emit_typed_tco_match_arm for matches inside the tail-call lowering, which the native App Attest run surfaced separately (extdeps.standards.rfc_5280 read_extensions_list, the one error left after the first renderer was repaired); and emit_typed_match's String-literal re-emission (needs_string_from), where a review of this PR found the decision dropped -- there a string-literal arm over an optional scrutinee also emits `Some(ref __s)`, since a literal matches only a present value. (D) OCTETS: std.bytes bytes_octets and utf8_encode_bytes were interpreter-intercepted builtins whose .dag bodies were placeholders -- `[pure_dag_seam_unreachable()]`, a one-element list of `1 / 0`, and `s as Bytes`, a cast no Rust row realizes and which emitted a runtime panic. Both are now declared HostRealizedSeams (self-call bodies, std.primitive_projection rows, std.primitive_identity declarations with SourcePreservingOrder traversal facts, extdeps.languages.rust.emit rt_function_registry rows, v1.runtime_rust bodies); bytes_octets is typed List<Int> under the bounded_natural_arithmetic_evaluated_as_unbounded_int ruling, since UInt8 has no emitted realization that holds an octet and bytes_qualified_octets is the one boundary observing the range. Two further links surfaced by execution: a REALIZED seam's self-call was lowered by the name-keyed tail-call rewrite into a non-terminating loop (rust_host_seam_is_realized now exempts it, see host_seam_self_call_diverges_when_its_arm_is_absent), and rustc's deny-by-default unconditional_panic refused every crate reaching std.bytes because of pure_dag_seam_unreachable's constant `1 / 0`. The first cut relaxed that lint for all generated code; review 71098 refused it as widening a real check to admit one placeholder, and the placeholder was the earlier link: pure_dag_seam_unreachable is now a rostered HostRealizedSeam too, refusing in the interpreter with a typed error naming the seam and panicking by name in v1_rt, so the lint stays on. EVIDENCE: the fixture test.fixture.emitted_interpreted_parity.string_order_octets_present_binding exits 0 interpreted and requires the thirteen-field line `T F T F T 6 2962370309 97 0 989 ex none q` -- fields 1-5 string ordering, 6-7 octets, 8-9 the ordinary-match present binding, 10 the tail-call-match present binding, 11-13 the String-literal re-emission -- with a RED control that exits 1 printing the observed line; its emitted crate builds and runs to the same line. The enrolled claim module test.claim.emitter_string_order_present_binding_witness_test carries the emission half: host-string ordering over an alias, the named refusal for an ordering over a String? (which inference admits today, so the arm is reachable), and the present binding in all three match renderings. The integration consumer is `gunbc test //gunbc/instruments:native-app-attest` on gunbc#12251. RUNG unchanged at mitigatable for the class: required CI still neither emits-and-compiles a fixture closure nor executes integration targets, which is this row's existing trigger.",
"OCCURRENCE, 2026-09-25 (loyal-boar-23, found by swift-bat-511 on native App Attest P2b): CALLING A LOCALLY BOUND FUNCTION VALUE. extdeps.apple.app_attest first_assertion_refusal folded a List<fn() -> AssertionRefusal?> and called the lambda-bound element `r()`; gunbc#12251 rewrote that one fold as a named AssertionStep sum, leaving the idiom refused everywhere else. The brief placed the defect in emit_rust's callee resolution; re-deriving the chain (DESIGN 6b) placed it three links earlier and found two more downstream. (1) INFERENCE, the earliest unjustified boundary: v1.compiler.infer child_type_node, the total read of a child position's type, returned a child's inferred slot whenever it had one, and an Arrow type node carries its RETURN type there (make_callable_type) -- so the element of List<fn(Int) -> Int> was Int, a lambda parameter bound under it was not callable, and the call refused as \"function 'r' not found in scope\" in `gunbc run` as well as in emission. An Arrow child is now its own type -- landed independently by gunbc#12295 (receipted on arity_proxy_for_callability_misroutes_a_found_local) while this change was in review; this change consumes it rather than restating it. (2) INFERENCE, the list literal: a lambda's typed node carries its BODY type, and a list literal took its first element's type, so [fn() { none }] against List<fn() -> Int?> was typed List<T>; where the declared element is an arrow and any element is a lambda the declared arrow is the element type, every element still judged against it. (3) EMISSION, two value positions of a lambda: a lambda literal in a list was a bare closure (E0308, every closure its own type), and is now the arrow carrier through the record-field row (rust_callable_field_value_wrap) bound at the rendered arrow by a typed let, not an `as` cast, which cuts the expectation typing Some(7) as Option<i32> (E0271); a let-bound lambda was `|x|` with no call site to type x from (E0282 at x.clone()) and is now emitted with typed parameters through emit_typed_collection_lambda, staying a bare closure so it still enters an impl Fn parameter. The call sites themselves (r(), f(v), g(v)) needed no change. EVIDENCE: test.fixture.emitted_interpreted_parity local_callable_value_calls exits 0 interpreted and its emitted crate, driven by a two-line harness over its library, prints the same line `6 8 6 7 9 0` with main returning ExitSuccess; with the expected line mutated both sides refuse (interpreter exit 1, emitted main ExitFailure carrying the observed line); on the pre-fix seed the fixture refuses at resolve. test.claim.local_callable_value_call_witness_test carries three inference controls (fold, unary fold and map lambda parameters over callable elements) and two emission controls (the list-literal carrier and the typed let), all five FAIL on the pre-fix seed and PASS here. RESIDUE, stated: an UNANNOTATED let-bound lambda (`let h = fn(x) { x * 2 }`) has no parameter type a Rust closure can be written at and still emits `|x: _|`-equivalent (E0282); a non-lambda element (a let-bound closure variable) in a List<fn..> keeps its bare rendering. RUNG unchanged at mitigatable: required CI still neither emits-and-compiles a fixture closure nor runs its crate, which is this row's existing trigger.",
"OCCURRENCE, 2026-09-24 (lively-koi-275, gunbc#12208 MQ-1): A FIELD BOUND UNDER A NESTED VARIANT PATTERN KEEPS ITS BOX. The `diagnostics` field of `v2.std.diagnostic` `Outcome` is a recursive Optional, so `v1.compiler.emit_rust` `needs_box_wrapping` boxes it. At a SINGLE-LEVEL arm `Accepted { value: v, diagnostics: d } =>` the emitter binds the field by `ref` and unboxes it (`let d = diagnostics.as_ref()`). Under a NESTED arm `Present { value: Accepted { value: facts, diagnostics: d } } =>` it bound the Box itself, and passing `d` to `v2.std.diagnostic` `diagnostics_merge` failed rustc with E0308 (expected `Option<Rc<NonEmptyDiagnostics>>`, found `Box<Option<..>>`) in the emitted `v2.compiler.infer`. The `.dag` was accepted with zero diagnostics, and only the non-required emit-build lane (`//gunbc/instruments:self-host`) saw it. The author-side repair split the match into two single-level arms, which the rest of the corpus already does by habit. That habit is an unstated workaround: it explains why the population is small and is not evidence that it is zero. The existing trigger of this row covers it: the emitted carrier comes from the declaration, and nested-pattern binders must go through the same unboxing join as single-level arms.",
"OCCURRENCE, 2026-09-28 (warm-wolf-234, precursor to the Bool de-fork): THE ARMS OF A NATIVELY REALIZED COPRODUCT. std.types Bool = True | False is bound to Rust `bool` by gunbc.rust_source_type_bindings, and `match a { True => b False => False }` over it was accepted at zero blocking diagnostics and emitted `Bool::True` / `Bool::False` against a `bool` -- rustc E0308. The type binding said which carrier Bool realizes as and nothing said which of its values each arm is, so the emitter spelled the arm by its SOURCE name, the one spelling the carrier cannot express. It went unexercised because v2.std.logic's structural Bool answered every True/False in the corpus; retiring that declaration exposed it. REPAIRED AT THE OWNING LINK, not at the two sites that tripped it: std.target_representation SourceVariantTargetValue rows keyed on the parent's identity -- a DeclarationRef, or the kernel type name for the kernel mint every module's `Bool` resolves to, admitted by std.types is_kernel_type (the values themselves are target facts in extdeps.languages.rust.representation) -- that identity read once at inference and carried as VariantParentIdentity on VariantPattern and VariantValueBinding, and the emitter spelling the row's value or refusing located (compile_error!) where the identity is not recovered for an arm some row binds -- never falling back to the spelling. Standing controls: fixtures/fixture_closure_rustc/native_bool_variant_probe.dag (rustc, red before, green after), fixtures/fixture_closure_rustc/local_true_false_coproduct_probe.dag (a module-local coproduct whose arms are spelled True/False keeps its own enum, so the rows are identity-keyed), and test.claim.native_variant_realization_witness_test on the emitted bytes.",
"OCCURRENCE, 2026-09-28 (warm-wolf-234, found while choosing the control above; NOT repaired): A MODULE-LOCAL COPRODUCT SPELLED WITH A KERNEL TYPE NAME. `type Bool = True | False` declared in an ordinary module is accepted at zero blocking diagnostics, but kernel names are never overridden in type position, so every signature renders the kernel `bool` while the arms render the local `enum Bool` -- rustc E0308 on the specimen fixtures/fixture_closure_rustc/local_bool_coproduct_probe.dag, measured on origin/main by `gunbc compile --entry` plus cargo check. Two referents for one spelling in one module is the defect; the earlier boundary is the checker, which should refuse a declaration that shadows a kernel name (or the emitter should keep one referent). Rostered here with its specimen so it is not lost; the variant-realization change deliberately does not touch it."
],


Expand Down
42 changes: 40 additions & 2 deletions dag/gunbc/rust_source_type_bindings.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,15 @@ module gunbc.rust_source_type_bindings

import std.types { List, String, Bool, NonEmptyStr }
import std.decl_ref { DeclarationRef, decl_ref }
import std.kernel_type_name { kernel_type_name, KernelTypeNameAdmitted, NotAKernelTypeName }
import std.target_representation {
SourceTypeTargetBinding, CheckpointRowMigration, CheckpointRowDisposition,
SourceTypeTargetBinding, SourceVariantTargetValue, VariantParentKey, VariantParentDeclaration, VariantParentKernelType, RepresentationValue,
CheckpointRowMigration, CheckpointRowDisposition,
MigratedToExactBinding, ProvenUniqueKernelBinding, StillBareNameDebt
}
import extdeps.languages.rust.representation {
RustRepresentation, RustStdString, RustI64, RustBool, RustUnit, RustVecU8, RustSerdeJsonValue
RustRepresentation, RustStdString, RustI64, RustBool, RustUnit, RustVecU8, RustSerdeJsonValue,
rust_bool_true_value, rust_bool_false_value
}

// THE CORPUS'S HALF OF THE THREE-IDENTITY SPLIT (std.target_representation): which of THIS corpus's
Expand Down Expand Up @@ -63,6 +66,41 @@ data rust_source_type_binding_rows: List<SourceTypeTargetBinding<RustRepresentat
rust_source_binding(module_path: "std.types", decl_name: "Json", representation: RustSerdeJsonValue)
]

// WHICH TARGET VALUE EACH ARM OF A NATIVELY REALIZED COPRODUCT IS (std.target_representation
// SourceVariantTargetValue). Bool = True | False realizes as RustBool, and its two arms are the two
// values extdeps.languages.rust.representation lists for that representation. The arm-to-value
// pairing is stated ONCE, below, and keyed twice, because Bool has two identities that reach the
// emitter: the std.types declaration (bound above, and what a reference inside std.types resolves
// to) and the kernel mint every other module's `Bool` resolves to (the kernel name, admitted by
// std.kernel_type_name kernel_type_name -- the same two routes the type level carries as the exact row above and
// the ProvenUniqueKernelBinding verdict below). Keyed on identity, so an unrelated coproduct whose
// arms are spelled True/False has no row and renders its own enum.
type BoolArmValue {
variant: NonEmptyStr
value: RepresentationValue<RustRepresentation>
}

data rust_bool_arm_values: List<BoolArmValue> = [
BoolArmValue { variant: "True" as NonEmptyStr, value: rust_bool_true_value },
BoolArmValue { variant: "False" as NonEmptyStr, value: rust_bool_false_value }
]

fn rust_bool_variant_rows(parent: VariantParentKey) -> List<SourceVariantTargetValue<RustRepresentation>> {
rust_bool_arm_values |> map(a => SourceVariantTargetValue { parent: parent, variant: a.variant, value: a.value })
}

fn rust_bool_kernel_variant_rows() -> List<SourceVariantTargetValue<RustRepresentation>> {
match kernel_type_name(name: "Bool") {
KernelTypeNameAdmitted { kernel_name: k } => rust_bool_variant_rows(parent: VariantParentKernelType { kernel_name: k })
NotAKernelTypeName { name: _ } => []
}
}

data rust_source_variant_value_rows: List<SourceVariantTargetValue<RustRepresentation>> = concat(
rust_bool_variant_rows(parent: VariantParentDeclaration { declaration: decl_ref(module_path: "std.types", decl_name: "Bool") }),
rust_bool_kernel_variant_rows()
)

fn rust_bound_declaration_refs() -> List<DeclarationRef> {
rust_source_type_binding_rows |> map(r => r.source)
}
Expand Down
1 change: 1 addition & 0 deletions dag/gunbc/stage0/stage0_crate_partition_generated.dag
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
"extdeps_units_iso_80000_3",
"std_occurrence_identity",
"std_source_annotation",
"std_kernel_type_name",
"std_target_representation",
"std_literal_elaboration",
"std_operator_realization",
Expand Down
Loading