Repository navigation
Enforcement rosters: ScopeRoster/SubjectRoster split, QualifiedName structural subjects + last dsl stragglers (E0 PR-0b) - #6256
Merged
Conversation
…r (QualifiedName, structural ==) + last dsl stragglers (E0 / PR-0b)
The fired subject_roster_string_dissolution_trigger (vocab.dag), executed:
SubjectRoster carried BOTH filesystem scope roots and declaration names as one
List<String> - a state-space conflation with two different comparison
semantics (path-literal vs segment-structural) in one representation.
- vocab.dag: SubjectRoster.entries -> List<QualifiedName> (v2.std.qualified_name
authority; compared via structural ==, qualified_name_eq); new ScopeRoster
{ roots: List<String> } for tree roots; ScopeNarrowed.missing -> ScopeRoster;
scope_roster_covers/subject_roster_covers now two fns with the right
semantics each; trigger row deleted, split note left on the carrier.
- standing_intent: desired_scope -> ScopeRoster; required_subjects grounds
v1.compiler.infer.build_type_env via qualified_name_from_dotted_string.
- contract/receipts/gate/enforcement_live: claimed_scope -> ScopeRoster;
discovered_fn_subjects converts at the decl_facts boundary (subject_qn_of,
same single pass, linear); self_application_for now reads facts directly
(String prefix pre-conversion, fn-like only - TypeItem no longer counts
toward self-application, a small honesty gain).
- NEW RED control: permuted_segment_subject_does_not_cover - a QualifiedName
with the same segments in a different order must NOT satisfy the subjects
leg (the discriminator List<String> equality could not express).
- self_application_liveness_discriminates gains a TypeItem-prefix control
(kind filter proven, not just prefix).
- dsl stragglers renamed (operator ask): phase_profile_proof_plan.dag
dsl/tools -> dag/tools AND phase_profile_claim_executor.rs --source-root
dsl -> dag. The Rust consumer test was failing on main since #6165
(source root does not exist: dsl); it now PASSES by execution - the only
.rs change is that one literal.
Receipts by execution (2026-07-05): 11/11 gate_test (incl. new permuted
control), 10/10 enforcement_live witnesses; enrolled pair 40s/39s (QualifiedName
interning over 14,283 facts is in the noise); pinned 3-red/3-green verdict
unchanged (representation-only, zero leg flips - as planned);
phase_profile_claim_executor 1 passed.
Typechecker note: QualifiedName alias vs FreeMonoid<Symbol> does not unify in
an if-branch JOIN (nominal expectation flows from a record-field into fold
init while the then-branch expands structurally) - worked around by hoisting
the fold out of the record construction; assignment-position coercion is fine.
Same #5552 alias-instantiation residue family.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
This was referenced Jul 5, 2026
briansrls
pushed a commit
that referenced
this pull request
Jul 5, 2026
…over QualifiedName subjects
briansrls
added a commit
that referenced
this pull request
Jul 5, 2026
Pick up main floor/CI fixes while keeping P3+P5 review fixes; restores emit optimizations from prior merge path for floor budget.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
PR-0b of the approved enforcement route (follows #6238): executes the fired
subject_roster_string_dissolution_trigger, and un-conflates the carrier it lived on.SubjectRostercarried filesystem scope roots and declaration names as oneList<String>: two facts with different comparison semantics (path-literal vs segment-structural) in one representation. Now:ScopeRoster { roots: List<String> }(scope) andSubjectRoster { entries: List<QualifiedName> }(subjects,v2.std.qualified_nameauthority, structural==).ScopeNarrowed.missing,claimed_scope,desired_scope→ScopeRoster;required_subjects/discovered_subjects→ QualifiedName, grounded viaqualified_name_from_dotted_string(required_subjectsnow groundsv1.compiler.infer.build_type_envas a real name, not a string).permuted_segment_subject_does_not_cover: same segments, different order must NOT satisfy the subjects leg. Plus a TypeItem-prefix control on self-application (kind filter proven;self_application_fornow reads facts directly — a type sharing the lens's module prefix no longer counts as self-application, a small honesty gain).dslstragglers renamed (operator ask):phase_profile_proof_plan.dagdsl/tools→dag/toolsandphase_profile_claim_executor.rs--source-root dsl→dag. The Rust consumer test had been failing on main since rename dsl -> dag #6165 (source root does not exist: dsl) — it now passes by execution; that one literal is the only.rschange.Receipts (by execution, 2026-07-05, incl. after merging main + rebuilt binary)
gate_test(incl. the new permuted control), 10/10enforcement_livewitnesses; enrolled pair 40s/39s — QualifiedName interning over 14,283 facts is in the noise.phase_profile_claim_executor: 1 passed (spawns claim_executor over the repointed plan — both stragglers proven by one execution).QualifiedNamealias vsFreeMonoid<Symbol>fails to unify in an if-branch join (nominal field expectation flows into foldinitwhile the then-branch expands structurally; De-fork grounding keystone: fix v2 generic type-alias instantiation so FreeMonoid aliases resolve - brief in docs plans dsl-v2-defork-audit section 3b #5552 alias-residue family) — worked around by hoisting the fold out of the record construction; assignment-position coercion works. Noted in the commit for the de-fork lane.CI note: the
cicheck will show the known dark-CI cancel in batch-1 (compile-clean wall), as on every recent main run; the receipts above are the executable evidence.🤖 Generated with Claude Code