Skip to content
2 changes: 1 addition & 1 deletion dag/gunbc/durable_cas_file_store.dag
Original file line number Diff line number Diff line change
Expand Up @@ -827,7 +827,7 @@ fn cas_name_is_digits(s: String) -> Bool {

// "<key>.<n>" -> key, or none for a name that is not a slot file.
fn cas_key_of_slot_name(name: String) -> NonEmptyStr? {
let parts = name.split(delimiter: ".")
let parts: List<String> = name.split(delimiter: ".")
if count(parts) < 2 { none } else {
let last = match first(skip(parts, count(parts) - 1)) {
Absent => ""
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
module gunbc.recurring_failure_mode.generic_variant_without_expected_type_leaves_a_present_arm_undecided

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data generic_variant_without_expected_type_leaves_a_present_arm_undecided: RecurringFailureMode = RecurringFailureMode {
identity: "generic_variant_without_expected_type_leaves_a_present_arm_undecided" as NonEmptyStr,

receipts: [
"**a generic variant constructed with no expected type leaves a downstream `Present` arm undecided, and the interpreter answered it silently** (INVALID STATE: an accepted program with a `match` whose scrutinee type the checker could not resolve, holding a `Present { value: .. }` arm whose meaning -- does it read an optional's present value? -- is decided from exactly that type).",

"SPECIMEN (gunbc#12386, found by valiant-bat-424, worked around there by hoisting both lambdas into typed top-level fns): observe_numa mapped each numactl CPU record to an ObservationAttempt through a lambda, flat_mapped the refusals out through a second lambda, and matched `first(malformed)`. A malformed record produced one refusal, and the interpreter took the `_` arm, so a malformed section was reported as an ESTABLISHED topology. Minimized to four lines with no map lambda at all: `[No { cause: Bad { .. } }]`, flat_map to its causes, `match first(..) { Present { value: c } => .. _ => .. }` -- count 1, arm Absent. It requires the payload to be itself a variant, which is why the Nat/String two-liner did not reproduce: the interpreter peels a raw non-variant payload without reading the type.",

"THE CHAIN, RE-DERIVED PER DESIGN section 6b AND TRACED BY INSTRUMENTATION RATHER THAN READ. (1) v1.compiler.infer types the record literal of a generic variant with no expected type as the UNINSTANTIATED declaration -- Attempt's Disj body with its fields still typed T and E, so even E is left free although the field value fixes it. (2) A lambda parameter over that element type collapses to the bare T. (3) `[c]` is List<T>, and `first` of it is a CompilerError \"unresolved type\" node, with NO diagnostic. (4) v1.compiler.infer annotate_pattern_parent_enums reads that subject as PatternLookupBlocked and stamps the arm parent_enum none, silently. (5) v1_compiler.interpreter match_pattern peels a raw present payload for `Present` only when parent_enum is Optional, so a variant payload misses and the next arm wins. Typed top-level fns repaired #12386 only because their declared types supplied the expected type at link 1.",

"EARLIEST UNJUSTIFIED LINK: link 1, generic constructor instantiation. Links 3 and 4 are where the checker proceeded on a type it did not have without saying so -- the DESIGN section 5 absorbing fallback -- and link 4 is where that silence becomes a runtime meaning. The repair landed at link 4 as a REFUSAL: v1.compiler.infer PresentArmScrutineeTypeUnresolved refuses, located at the match, a `Present` arm left without a parent over a blocked scrutinee. The reviewed distinction is Present versus Absent: an `Absent` arm matches Null and Optional.Absent without the parent stamp, so its meaning does not rest on the missing type, and it stays admitted. No claim is made here about other variant patterns -- v1_compiler.interpreter match_pattern also special-cases `Holds` on parent_enum Witness, which this row did not audit. The refusal names the remedy the specimen's author reached by hand: give the producing value a declared type.",

"THE RUST EMITTER DIVERGES LOUDLY WHERE THE INTERPRETER DIVERGED SILENTLY -- executed, not read. The red shape (a one-element list of a generic variant built with no expected type, flat_mapped to its causes, `match first(..) { Present { value: c } => .. }`) was emitted to Rust by a compiler WITHOUT this refusal: emission succeeded and rendered the arm as `Some(c)` (v1.compiler.emit_rust keys Present on the variant NAME via is_optional_variant_name, so the missing parent_enum did not reach it), and rustc then refused the crate with E0282 `type annotations needed`, unable to infer the generic parameter T of the uninstantiated constructor -- link 1 of this row, caught by the target's own inference. So before the refusal the two realizations disagreed: the interpreter answered the wrong arm, the emitted route refused to build. The checker refusal now closes both before either runs, and link 1 remains the trigger.",

"EVIDENCE: test.claim.infer_present_arm_unresolved_scrutinee_witness. The red a_present_arm_over_an_unresolved_scrutinee_refuses compiles the minimized shape as fixture source and requires exactly one blocking PresentArmScrutineeTypeUnresolved; the_typed_producer_is_accepted holds the annotated twin by the difference of blocking totals; the_typed_producer_reads_its_variant_payload_as_present EXECUTES the accepted shape and requires the interpreter to take the Present arm and bind the variant payload.",

"RUNG FOUND AT: outside the ladder (silent wrong answer on the interpreter route). RUNG NOW: structurally guaranteed for DIRECT `Present` arms over a PatternLookupBlocked scrutinee -- no Accepted program holds such an arm. Nested field patterns (a `Present` inside another pattern's field binding, annotated against a field subject) are NOT audited by this refusal and are not claimed. CEILING: structurally guaranteed for the whole class, and it is not reached: an unresolved type still flows silently through links 2 and 3 into every consumer that is not a `Present` arm. NEXT-RUNG TRIGGER, NAMED AS A CAPABILITY: generic variant construction instantiates the declaration's type parameters -- binding each one a field value or the expected type determines, unifying the arms of a match or if that construct the same generic type, and refusing, located, a type argument nothing determines -- sufficient for no Accepted expression to carry an uninstantiated declaration parameter as its type. When that capability lands, the invalid-source regression control test.claim.infer_present_arm_unresolved_scrutinee_witness a_present_arm_over_an_unresolved_scrutinee_refuses STAYS ENROLLED (DESIGN section 4b(4)); the refusal it expects may MOVE to the constructor boundary (an undetermined type argument refused where the variant is built), and the control is then re-pointed at that refusal class, never retired.",

"RECOGNITION RULE: when a runtime decision reads a checker ANNOTATION rather than a value, ask what the checker stamps when it could not compute the annotation. If the answer is a default (none, the first arm, the name) and no diagnostic, the realization is answering a question the checker declined -- the tell is a fix that only works when the value has a declared type somewhere upstream.",
],

evidence: [],
}
4 changes: 2 additions & 2 deletions dag/gunbc/spark/native_serving_apply.dag
Original file line number Diff line number Diff line change
Expand Up @@ -792,8 +792,8 @@ fn spark_native_arm_steps_of(launches: List<ArmNodeLaunch>, renders: List<GlmNat
match master_endpoint {
Absent => NativeArmStepsRefused { cause: "the arm's rendezvous endpoint is unknown, so nothing could be verified after a restart" as NonEmptyStr }
Present { value: endpoint } => {
let steps = flat_map(zip_map(a: launches, b: renders, f: fn(l, r) { spark_native_step_of(launch: l, render: r, units: units, profile: profile) }),
o => match o { Absent => [] as List<SparkNativeHostStep> Present { value: v } => [v] })
let per_rank: List<SparkNativeHostStep?> = zip_map(a: launches, b: renders, f: fn(l, r) { spark_native_step_of(launch: l, render: r, units: units, profile: profile) })
let steps = flat_map(per_rank, o => match o { Absent => [] as List<SparkNativeHostStep> Present { value: v } => [v] })
if count(steps) == count(launches) && count(steps) > 0 {
NativeArmSteps { steps: steps, master_endpoint: endpoint }
} else {
Expand Down
15 changes: 9 additions & 6 deletions dag/test/claim/fabric/data_class_admission_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module test.claim.fabric.data_class_admission_witness_test

import std.types { Bool, String, NonEmptyStr, FilePath, List }
import std.nat { Nat }
import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq }
import std.content_hash { ContentHash, as_content_hash_structural, content_hash_atom }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
Expand Down Expand Up @@ -228,13 +229,15 @@ test fn a_personal_identity_handed_to_a_build_output_sink_is_refused_before_the_

// LABEL PRESERVATION AND ERASURE. A projection of a classified value is classified in the same
// category; the erased form keeps the category and the basis and has no payload at all.
fn email_length_of(claims: OidcStandardClaims) -> Nat {
match claims.email {
Present { value: e } => count(e as String)
Absent => 0
}
}

test fn a_projection_of_classified_data_keeps_its_category() -> Bool {
let email_length = classified_map(c: fx_pii(), f: fn(claims) {
match claims.email {
Present { value: e } => count(e as String)
Absent => 0
}
})
let email_length = classified_map(c: fx_pii(), f: fn(claims) { email_length_of(claims: claims) })
declaration_ref_eq(a: classified_category(c: email_length), b: personal_identity_ref())
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
module test.claim.infer_present_arm_unresolved_scrutinee_witness

import gunbc.compile_census_probe { blocking_class_count_for, total_blocking_count_for }
import std.types { Bool, Int, List, String }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

// THE DISCRIMINATING RED FOR gunbc.recurring_failure_mode
// generic_variant_without_expected_type_leaves_a_present_arm_undecided, AND ITS CONTROLS.
//
// The red is the minimized shape of the silent wrong answer found on gunbc#12386: a generic variant
// built with no expected type, flat_mapped through a lambda, and a `Present { value: c }` arm over
// `first` of the result. Before v1.compiler.infer PresentArmScrutineeTypeUnresolved the interpreter
// took the `_` arm for a ONE-element list (measured: count 1, arm Absent). The module sits under the
// test.claim.infer_ prefix the required gate admits, and every fixture is a string handed to a
// nested compile, because an inline red would be refused by the compiler compiling this file.
//
// Fixture type names carry a Probe prefix: bare names resolve by global uniqueness, so `Ok` or
// `Cause` could bind a corpus declaration instead of the fixture's own.
data present_arm_unresolved_red_source: String = "module probe_present_arm_unresolved\ntype ProbeCause = | ProbeBad { detail: String }\ntype ProbeAttempt<T, E> = ProbeKept { observed: T } | ProbeRefused { cause: E }\nfn f() -> String {\n let attempts = [ProbeRefused { cause: ProbeBad { detail: \"x\" } }]\n let causes = flat_map(attempts, a => match a { ProbeRefused { cause: c } => [c] _ => [] })\n match first(causes) { Present { value: c } => \"present\" _ => \"absent\" }\n}\n"

// THE REMEDY THE REFUSAL NAMES, WRITTEN: the same program with the producing let given its declared
// type. This is the positive control, and the difference against the red cancels the live-tree
// baseline the census compiles against.
data present_arm_unresolved_green_source: String = "module probe_present_arm_unresolved_typed\ntype ProbeCause = | ProbeBad { detail: String }\ntype ProbeAttempt<T, E> = ProbeKept { observed: T } | ProbeRefused { cause: E }\nfn f() -> String {\n let attempts: List<ProbeAttempt<Int, ProbeCause>> = [ProbeRefused { cause: ProbeBad { detail: \"x\" } }]\n let causes = flat_map(attempts, a => match a { ProbeRefused { cause: c } => [c] _ => [] })\n match first(causes) { Present { value: c } => \"present\" _ => \"absent\" }\n}\n"

data present_arm_unresolved_class: String = "PresentArmScrutineeTypeUnresolved"

test fn a_present_arm_over_an_unresolved_scrutinee_refuses() -> Bool {
blocking_class_count_for(source: present_arm_unresolved_red_source, wanted_class: present_arm_unresolved_class) == 1
}

test fn the_typed_producer_is_accepted() -> Bool {
blocking_class_count_for(source: present_arm_unresolved_green_source, wanted_class: present_arm_unresolved_class) == 0
&& total_blocking_count_for(source: present_arm_unresolved_red_source) - total_blocking_count_for(source: present_arm_unresolved_green_source) == 1
}

// THE ROUTE, NOT ONLY THE VERDICT (DESIGN section 3, the pairing obligation). The accepted shape is
// executed here by the interpreter and must take the Present arm for a one-element list whose
// element is itself a variant -- the exact payload kind that missed the arm before.
type PresentArmProbeCause = | PresentArmProbeBad { detail: String }
type PresentArmProbeAttempt<T, E> = PresentArmProbeKept { observed: T } | PresentArmProbeRefused { cause: E }

test fn the_typed_producer_reads_its_variant_payload_as_present() -> Bool {
let attempts: List<PresentArmProbeAttempt<Int, PresentArmProbeCause>> = [PresentArmProbeRefused { cause: PresentArmProbeBad { detail: "x" } }]
let causes = flat_map(attempts, a => match a { PresentArmProbeRefused { cause: c } => [c] _ => [] })
match first(causes) { Present { value: PresentArmProbeBad { detail: d } } => d == "x" _ => false }
}
4 changes: 4 additions & 0 deletions src/v1/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -407,6 +407,7 @@ type CompilerDiagnostic
| TestCodeReferenceRowOrphaned { referrer: String, span: SourceSpan }
| MissingField { field: String, type_name: String, span: SourceSpan }
| SiblingOperandEffectOrderUndetermined { construct: String, first_operand: String, second_operand: String, span: SourceSpan }
| PresentArmScrutineeTypeUnresolved { pattern: String, span: SourceSpan }
| NonExhaustiveMatch { missing: List<String>, span: SourceSpan }
| CircularDependency { modules: List<String>, span: SourceSpan }
| DuplicateModule { name: String, span: SourceSpan }
Expand Down Expand Up @@ -635,6 +636,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
TestCodeReferenceRowOrphaned { referrer: _, span: s } => s
MissingField { field: _, type_name: _, span: s } => s
SiblingOperandEffectOrderUndetermined { construct: _, first_operand: _, second_operand: _, span: s } => s
PresentArmScrutineeTypeUnresolved { pattern: _, span: s } => s
NonExhaustiveMatch { missing: _, span: s } => s
CircularDependency { modules: _, span: s } => s
DuplicateModule { name: _, span: s } => s
Expand Down Expand Up @@ -718,6 +720,7 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
TestCodeReferenceBudgetMismatch { referrer: r, declared: d, observed: o, span: _ } => concat("the test-reference debt row for '", r, "' declares ", to_string(value: d), " reference(s) but ", to_string(value: o), " were observed. The count is an equality in both directions: more means new test-code references appeared and must be removed; fewer means debt was paid and the row must be lowered or deleted")
MissingField { field: f, type_name: t, span: _ } => concat("missing required field '", f, "' in literal of type '", t, "'")
SiblingOperandEffectOrderUndetermined { construct: c, first_operand: a, second_operand: b, span: _ } => concat("two sibling operands of '", c, "' each reach a declared effect ('", a, "' and '", b, "'), and nothing in the model orders them: sibling position is not a sequencing authority, and two realizations of this program may run them in opposite orders. Bind them with let, in the order this program needs, before constructing '", c, "'")
PresentArmScrutineeTypeUnresolved { pattern: p, span: _ } => concat("a '", p, "' arm decides from the scrutinee's type whether it reads an optional's present value, and the checker could not resolve that type: the scrutinee's type is unresolved, typically because a generic variant upstream was constructed with no expected type, so its type arguments were never instantiated. Without that type the arm's meaning is undecided, so it refuses rather than guessing. Give the value that produces the scrutinee a declared type (annotate the let, or construct it inside a function whose return type declares it)")
NonExhaustiveMatch { missing: ms, span: _ } => concat("non-exhaustive match: missing variant(s) ", join(ms, separator: ", "))
CircularDependency { modules: ms, span: _ } => concat("circular dependency detected: ", join(ms, separator: " -> "))
DuplicateModule { name: n, span: _ } => concat("duplicate module declaration: '", n, "'")
Expand Down Expand Up @@ -877,6 +880,7 @@ fn diagnostic_disposition(d: CompilerDiagnostic) -> DiagnosticDisposition {
TestCodeReferenceRowOrphaned { referrer: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
MissingField { field: _, type_name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
SiblingOperandEffectOrderUndetermined { construct: _, first_operand: _, second_operand: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
PresentArmScrutineeTypeUnresolved { pattern: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
NonExhaustiveMatch { missing: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
CircularDependency { modules: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
DuplicateModule { name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
Expand Down
Loading