Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

76 changes: 6 additions & 70 deletions dag/gunbc/floor_non_verdict_classification.dag
Original file line number Diff line number Diff line change
Expand Up @@ -75,81 +75,17 @@ data gating_answer_note: String = "DOES known_red_runtime_errored GATE, AND SHOU

data closure_dependent_evidence: String = "PASSES under a narrow claim_batch --hermetic closure; produces no verdict on the floor's whole-corpus subject"

data closure_dependent_rows: List<ClassifiedNonVerdictRow> = [
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "comment_only_drift_is_one_change_not_remove_add"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "reconcile_would_teardown_only_if_ownership_claimed_it"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_and_srv4_disagree_on_convergence"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_reconcile_adds_exactly_the_missing_fleet_key"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv3_reconcile_refuses_both_unowned_keys_never_teardown"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.srv3_subsumption", function: "srv4_reconcile_is_converged_empty_plan"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "v2.test.claim.staging", function: "cached_stage_hit_skips_stage"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: "PASSES narrow; on the floor throws `cannot access field 'raw' on Int` -- an error text shared with nothing else in the population and a cause shared with the eight rows above it"
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "v2.test.claim.staging", function: "cached_stage_miss_runs_stage"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: closure_dependent_evidence
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "v2.test.emit.produced_decl_support_preserved", function: "produced_decl_support_survives_augmentation"),
cause: ClosureDependentResolution,
standing: AssertsARedThatDoesNotExist,
measured_evidence: "PASSES narrow; on the floor throws `call contract mismatch calling 'render': missing required argument 'proto'`. Its `render` is PATTERN-BOUND out of ProducedDeclWired and std.layout declares a free `fn render(doc, proto)`, so this row is the shadowing class in its loud, different-arity face"
}
]
data closure_dependent_repaid_note: String = "EMPTY, AND THAT IS A REPAYMENT RECEIPT AND A MEASURED JOIN RATHER THAN A MISSING MEASUREMENT. This list held NINE ClosureDependentResolution / AssertsARedThatDoesNotExist rows -- six test.claim.srv3_subsumption, two v2.test.claim.staging, and v2.test.emit.produced_decl_support_preserved. All nine now ANSWER and PASS on the required floor, so they left this carrier and left floor_expected_red in the same change. THE JOIN THIS CARRIER DECLARED AS INFERENCE IS NOW MEASURED, and that is the substantive result rather than the bookkeeping: unjoined_inference_note stated that closure-dependence was measured for these rows, that the local-binding-shadow defect was measured on its own grid, and that the claim THESE NINE lose their verdict TO THAT DEFECT was inference with no colliding name identified for the six srv3 rows or the two staging rows. It named its own instrument -- fix the resolver and re-run, at which point recovery measures the join and non-recovery isolates a second cause. The resolver is fixed (a lexical binding holding a named top-level function now shadows the free function sharing its spelling; the gate named Value::Closure only and so missed Value::Fn) and ALL NINE RECOVERED. Non-recovery would have isolated a second cause; there is none. The one row that already carried a named colliding symbol, produced_decl_support_preserved, is the confirmation rather than the whole result: its `render` is pattern-bound out of ProducedDeclWired against std.layout's free `fn render(doc, proto)`, the loud different-arity face, and it recovered alongside the eight whose colliding name was never identified. The list stays declared rather than deleted because the CAUSE remains constructible -- a lexical binding holding a NON-CALLABLE value still falls through to a same-named free function, enrolled as its own expected-red row with a census-then-widen trigger -- and an emptied arm with its reason recorded is a different fact from an arm that never existed."

data closure_dependent_rows: List<ClassifiedNonVerdictRow> = []

data closure_independent_repaid_note: String = "EMPTY, AND THAT IS A REPAYMENT RECEIPT RATHER THAN A MISSING MEASUREMENT. This list held the four v2.test.manual.bootstrap_footprint_anchor identities, the only ClosureIndependent / HonestDebtWithStatedTrigger rows in the population. Their cause was a Symbol-declared field holding Int code points: semantic_decl_string_to_bundle_node folded a String into character atoms carrying raw code points, and canonical_hash_of_connective routed that field into content_hash_atom -> atom_identity_hash, which requires a string, so the hash threw before any assertion ran. Repaired at the PRODUCER by giving character atoms a string identity through from_code_point, with code_point as its inverse on the two decoders. All four now ANSWER: three PASS and bootstrap_footprint_canonical_holds FAILS honestly, so the four left this roster and the three passing ones left floor_expected_red in the same change. The list stays declared rather than deleted because the CAUSE remains constructible -- nothing prevents another producer putting a non-Symbol into Atom.identity -- and an emptied arm with its reason recorded is a different fact from an arm that never existed."

data closure_independent_rows: List<ClassifiedNonVerdictRow> = []

data unmeasured_rows: List<ClassifiedNonVerdictRow> = [
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.host_phase_status", function: "witness_reconcile_covers_upsert_teardown_and_noop"),
cause: Unmeasured { obstacle: host_phase_unmeasured_note },
standing: StandingUnmeasured,
measured_evidence: "no small-closure arm exists: claim_batch refuses the narrow run with `no declaration named host_phase_reconcile in this execution's loaded index`"
},
ClassifiedNonVerdictRow {
identity: non_verdict_row_identity(module_path: "test.claim.host_phase_status", function: "witness_remaining_work_counts_every_unfinished_cell"),
cause: Unmeasured { obstacle: host_phase_unmeasured_note },
standing: StandingUnmeasured,
measured_evidence: "no small-closure arm exists: claim_batch refuses the narrow run with `no declaration named fleet_subsumption_enrollments in this execution's loaded index`"
}
]
data unmeasured_repaid_note: String = "EMPTY, AND IT WAS REPAID WITHOUT EVER BEING MEASURED, which is a different receipt from the two above and is worth keeping distinct. This list held the two test.claim.host_phase_status identities. They were classified StandingUnmeasured on an honest obstacle: their witness carries ONE import and resolves everything else from the pool, so no narrow closure can even resolve them and there was no small-closure arm to compare against -- host_phase_unmeasured_note records that, and records the refusal to assign them the neighbouring cause merely because they shared an error message. THAT RESTRAINT WAS CORRECT AND IT WAS ALSO NOT NEEDED IN THE END: both now ANSWER and PASS on the required floor after the local-binding-shadow repair, alongside the nine rows that WERE measured as closure-dependent. So the shared cause was real; what was missing was an instrument able to show it, and the repair supplied one that the A/B could not. This is NOT a retroactive classification -- the rows are gone and nothing here claims they were ClosureDependentResolution -- it is the weaker and true statement that a repair aimed elsewhere recovered them too. The list stays declared because the obstacle remains constructible: a witness resolving from the pool rather than from declared imports still has no narrow arm."

data unmeasured_rows: List<ClassifiedNonVerdictRow> = []

data no_classified_non_verdict_rows: List<ClassifiedNonVerdictRow> = []

Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1048,6 +1048,15 @@ fn v1_interpreter_authored_roster_arms() -> List<InterpreterPrimitiveDispatchArm
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.compile_dag_multi_module_fixture" },
form: FreeCall,
authored_spelling: "compile_dag_multi_module_fixture",
realization_module: "v1_interpreter",
dispatch_symbol: "eval_builtin_inner",
dispatch_emit_site: EvalBuiltinInnerSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "free_call.observe_declared_import_closure_symbol_binding" },
form: FreeCall,
Expand Down
30 changes: 22 additions & 8 deletions dag/test/claim/floor_non_verdict_classification_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -38,15 +38,29 @@ test fn every_classified_non_verdict_row_carries_measured_evidence() -> Bool {
every_row_carries_measured_evidence()
}

// THE INHABITANCE ROW IS DELETED BECAUSE ITS POPULATION IS REPAID, NOT TO MAKE A TEST AGREE WITH
// BEHAVIOUR. It asserted `stale_enrolment_count() > 0 && unmeasured_count() > 0` -- that neither
// class was empty and neither had swallowed the other -- and it was the right assertion while the
// carrier held a live debt population. Every row is now gone: the nine ClosureDependentResolution
// rows and the two StandingUnmeasured rows all ANSWER and PASS on the required floor after the
// local-binding-shadow repair, and the four ClosureIndependent rows were repaid earlier at their
// own producer. A row asserting that a repaid population is non-empty is not evidence that
// anything works; it is an assertion that the debt must continue to exist, which would make the
// carrier unable to reach the empty terminal state its own header declares.
//
// THE DISTINCTION THIS TURNS ON, stated because the two moves look identical in a diff: editing a
// witness so it agrees with current behaviour is a claim about the world and is forbidden;
// deleting a witness whose SUBJECT no longer exists is dissolution. Nothing here weakens a
// judgment about the classification carrier -- the join, the uniqueness, the evidence-present and
// the exact-partition rows in this file are untouched and still gate, and they are what red if a
// row is added or removed anywhere. What is deleted is a claim about the population's SIZE, which is
// exactly the shape this file already removed once when `row_count() == 15` was found to be a
// change detector.
//
// IT COMES BACK WITH THE DEBT. The carrier keeps both arms declared with their repayment receipts
// precisely because the causes remain constructible; the day a row is authored into either, this
// assertion is the one to restore, and the receipts name what would put it there.
test fn standing_partition_is_exact_over_the_population() -> Bool {
(stale_enrolment_count() + honest_debt_count() + unmeasured_count())
== classified_non_verdict_row_count()
}

// The result this carrier exists to make unmissable, stated as a partition property rather than
// a literal: SOME rows assert a red that does not exist and SOME were never measured, so neither
// class is empty and neither has swallowed the other. How many are in each is a measurement the
// carrier's rows carry; asserting it here would re-mint the change detector removed above.
test fn both_the_stale_and_the_unmeasured_classes_are_inhabited() -> Bool {
stale_enrolment_count() > 0 && unmeasured_count() > 0
}
Loading
Loading