Skip to content

The type-parameter-in-value-position wall fires: flip its pinned hole to a firing red (split of #11819, parts 1+3) - #12163

Merged
briansrls merged 3 commits into
mainfrom
session/swift-bat-511-p1-value-position-wall
Sep 24, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/swift-bat-511-p1-value-position-wall

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 23, 2026 •

Copy link
Copy Markdown
Contributor

Split parts (1) and (3) of the superseded #11819 (closed; its claims are mapped in the closing comment). Part of the App Attest native-crypto node.

What was true on main

#12045 regenerated v1_compiler_infer.rs from the .dag. That removed the binding_resolves_to_type_parameter = false stub and carried name_is_enclosing_declared_type_parameter and InferScope.enclosing_declared_type_param_names into the seed. So TypeParameterInValuePosition now fires, and the claim that pinned it as an inert hole (== 0) was silently red on main:

run (claim_batch, EstimatedMemory=16GB, cgroup bound, git clean -fdx) result
main ada85b9, 0 changed files: a_type_parameter_in_value_position_does_not_yet_refuse_and_this_pins_that_hole FAIL
same run: a_generic_function_not_misusing_its_parameter_still_compiles PASS (compiles and emits)
same run: a_named_non_inhabitant_at_a_kinded_position_must_refuse (proof the harness reaches the check) PASS

Change

  • test.claim.type_argument_kind_inhabitance_witness_test: the pinned hole becomes a_type_parameter_in_value_position_must_refuse (>= 1). The -1 couldn't-run arm stays red, so a harness that never reaches the check can't pass it. Positive control: the existing generic-fn claim. It stays as the permanent regression control (DESIGN §4b(4)).
  • Narrowed, NOT retired (review 70608): gunbc.kind_reflection_seed_growth. Its trigger had two halves. The value-position half is discharged (the stub is gone and the refusal fires). The four-parameter kind-inhabitance fold is NOT: the seed still has the three-parameter type_arg_kind_inhabitance with no kind_inhabitant_matches_resolved, and pub type WidthResolution = PointerWidth. The row now cites those two seed declarations, with the trigger restated for them, and stays on seed_growth_justification_roster.
  • gunbc.recurring_failure_mode a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles: evidence repointed to the new claim, plus a receipt that the climb was as silent as the gap, and that the first draft of this PR repeated the class one level up. A lane that regenerates the seed should run the pinned holes over the modules it regenerated.

Evidence at this head (5fd0d04, clean tree, 0 changed files)

  • type_argument_kind_inhabitance_witness_test: all 6 claims PASS. That includes the new red, the generic-fn control, both wrong-kind negatives and both admitted-inhabitant positives.
  • seed_growth_admission_witness_test: all 7 claims PASS, including the roster-membership and stale-row checks over the narrowed row. Scope: that is the witness file only; the stale check over the real seed surface runs where CI runs the seed-growth gate.

Not in scope (P2): actual MachineWidth<N> reification plus a native-emission receipt. std.machine_constraints machine_width_literal_roster_frontier stays a stated frontier.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 2 commits September 23, 2026 16:25
… to a firing red

gunbc#12045's regen carried v1.compiler.infer's declared-roster predicate into the seed, so
TypeParameterInValuePosition now refuses `fn any_param<T>(x: T) -> Int { T }` at its own
location. The claim that pinned the hole at == 0 was therefore silently red on main
(claim_batch on a clean ada85b9: FAIL, with the generic-fn and named-non-inhabitant controls
PASS on the same run).

- test.claim.type_argument_kind_inhabitance_witness_test: the pinned hole becomes
  a_type_parameter_in_value_position_must_refuse (>= 1; the -1 not-runnable arm stays red),
  paired with the existing generic-fn positive control.
- gunbc.kind_reflection_seed_growth retired by its own trigger: the stub it cited
  (binding_resolves_to_type_parameter) no longer exists in the seed, and the refusal fires.
- gunbc.recurring_failure_mode a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles:
  evidence repointed, plus a receipt that the climb was as silent as the gap.

Split part (1)+(3) of superseded gunbc#11819.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…instead of retiring it (review 70608)

Its trigger also named the four-parameter kind-inhabitance fold. The seed still carries the
three-parameter type_arg_kind_inhabitance (no kind_inhabitant_matches_resolved) and the
single-arm WidthResolution alias, so only the value-position half was discharged by #12045.
The row now cites those two seed declarations, with the trigger restated for them.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 23, 2026

Copy link
Copy Markdown
Contributor Author

Re review 70608: confirmed and fixed in 5fd0d04. The seed still carries the three-parameter type_arg_kind_inhabitance (no kind_inhabitant_matches_resolved) and pub type WidthResolution = PointerWidth. So #12045 discharged only the value-position half of gunbc.kind_reflection_seed_growth's trigger, and deleting the row retired it short of its stated capability (§4b(3)). The row is restored, narrowed to those two live seed declarations with the trigger restated for them, and back on seed_growth_justification_roster. The rfm receipt now says 'narrowed, not retired'. At 5fd0d04 on a clean tree: kind witness 6/6 PASS, seed_growth_admission witness 7/7 PASS (claim_batch).

— sent from swift-bat-511

… pinned defect (review 70618)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 23, 2026

Copy link
Copy Markdown
Contributor Author

Re review 70618: confirmed and fixed. The stale header line above a_type_parameter_in_value_position_must_refuse now reads 'THIS IS A REGRESSION CONTROL FOR A WALL THAT NOW FIRES. The assertion reads forwards.' Annotation-only; per DESIGN §4c, annotations don't change the semantic graph, so the clean-tree claim results from the previous head are unaffected.

— sent from swift-bat-511

@briansrls
briansrls added this pull request to the merge queue Sep 24, 2026

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

APPROVE-SOURCE at exact head 3e928815dc8b160b20cb5b1da93eb01a801e1640.

The split is correctly bounded:

  • The formerly pinned silence is flipped to the firing TypeParameterInValuePosition RED, with the generic-function control retained and the not-runnable -1 disposition unable to satisfy the claim.
  • kind_reflection_seed_growth is narrowed rather than prematurely retired. It stops citing the discharged literal-false stub and continues to carry the two actual remaining divergences: the seed's three-parameter type_arg_kind_inhabitance without kind_inhabitant_matches_resolved, and the single-arm WidthResolution alias versus the declared coproduct.
  • The trigger is correspondingly narrowed to regeneration of those exact authorities.
  • The recurring-failure receipt records that the wall's climb was silent and makes running pinned holes part of the lesson for future seed regenerations.
  • MachineWidth<N> reification and native-emission evidence remain explicitly out of scope for P2.

All five required jobs are green at this exact head. No further source repair is requested. A head move or main rebind requires a delta review.

Merged via the queue into main with commit 3eb2165 Sep 24, 2026
5 checks passed
@briansrls
briansrls deleted the session/swift-bat-511-p1-value-position-wall branch September 24, 2026 04:53
gunbai-bot Bot pushed a commit that referenced this pull request Oct 2, 2026
…arrier or dropped with a located reason; kind_reflection row discharged

The stale-justification census went 97 -> 3 at identity grain against the
current tree. Three classes of edit:

REPAIRED (~44 DeclarationRefs): citations that named an enclosing module
while the subject had moved, re-pathed to the carrier that now produces it
- target_invocation: 15 compile_clean refs v1_compiler.cli_run ->
  v1_compiler.cli_run.compile_clean (the subjects live in the inline mod),
  plus the render ref dropped (impl method on QualificationRefusal,
  floor_memory_supervisor.rs:93 -- uncitable, not dead)
- namespace bridges: v1_interpreter -> v1_compiler.v1_interpreter (the
  module moved into the generated infer/resolve carrier)
- generated_artifact_boundary: 5 refs -> v1_compiler.generated_artifact_
  boundary_host.tests (subjects in the inline mod tests at :443)
- bare_reference_scanner module_self_declared_names ->
  v1_compiler.cli_run.bare_reference_scanner_tests
- floor_cost_debt: citation repaired to run_required_floor (the constant
  became fn-local inside it at required_floor_runner.rs:11968) -- repaired
  rather than deleted because that row's trigger has NOT fired and
  repair-to-live-carrier is the teardown precedent
- floor_teardown_attribution: citation re-inserted as
  v1_compiler.cli_run::release_process_caches_at_exit -- the old subject
  was RENAMED, not deleted (b1f4f11), and the live fn is called from
  claim_executor.rs:2435; current_boundary sentence corrected to what the
  one whole-run teardown figure still measures

DROPPED (~25 citations, each with a 2-line doctrinal comment): subjects
that are macro-declared extents (thread_local! stores in
floor_memory_instrumentation, modeled_operation_realization,
cross_claim_pure_share, cross_claim_demand_census -- gunbc.rust_item_scan
MacroScope cannot name them at item grain, so the citation can never be
anything but stale noise) or impl methods with no item-grain identity.

DELETED: kind_reflection_seed_growth.dag, file + roster entry + import.
Its regen trigger FIRED: both cited subjects now carry the four-param fn
with kind_inhabitant_matches_resolved x2 and the two-arm enum, regenerated
by 3150d9b #12805 -- the row was 'narrowed, not retired' per #12163
until that regen carried the second half, and deletion IS its discharge.

KEPT (3, per operator ruling): v1.compiler.emit_rust::
emit_source_root_eval_driver_main_rs, v1_compiler.main::RetainedCliHost,
v1_compiler.v1_interpreter::write_file_create_new -- each subject moved to
a generated mirror, neither row's trigger has fired, and the census's
stale join compares against the live hand-Rust population only, so it
cannot address a generated subject. Typed dispositions in the PR body.

Admission COMPLETE; well-formedness gate green; the 87-row roster folds
with no empty declaration list and no duplicate display key
(1210 declarations); duplicate-justifications 0; uncitable-items 1 (the
declared Display impl, uncitable by rule). Witnesses:
dag/test/claim/seed_growth_admission_witness_test.dag answers 7/7 PASS,
and the census instrument exits 0 with stale-justifications (3).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant