Repository navigation
Conversation
…pected_red note's producer The add-slice roster note in v2.workflow.floor_expected_red carried a dated receipt (main 3a8344b: infer accepts dag_add_emitted_root; the infer-then-translate composition refuses headed by infer_grounding_not_derived) and named its own next-rung trigger: a .dag entry returning the per-stage verdicts for one root, so the paragraph can name a producer instead of a commit. v2.compiler.self_host.candidate_generation_stage_verdicts is that entry, parameterized over root and target: the receipt's verdict vocabulary (infer_accepted / infer_rejected; candidate_accepted or the rejection head reason) plus the carried-reasons lists -- the half the verdict symbols cannot say, namely that infer accepts while carrying the frontier diagnostic on its accepted path, so the enrolled witness's d == None conjunct fails even where the composition reaches acceptance. v2.test.execution.self_host_candidate_generation_stage_verdicts binds the instrument to the slice's own fixture, with add_slice_stage_verdicts_entry the runnable gunbc run --function form (ExitSuccess only when infer accepts clean and the composition accepts clean). Two witnesses: infer-accepts as a permanent positive control, and the frontier-state pin that is expected to red the day the add-slice stall's trigger lands, flipping to a permanent regression control in the same change that removes the roster row (DESIGN 4b(4)). Measured by execution on this branch: the entry exits 1 printing infer=infer_accepted, infer_carried=[infer_grounding_not_derived x10], composition=infer_grounding_not_derived, composition_carried=[x11] -- the receipt reproduced, with bind_outcome's pending-plus-gate chain counted. Both witnesses PASS; the enrolled semantic witness still fails as enrolled. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…nd-to-end infer gains the declared-inhabitant membership derivation: a node declared in the dag language authority's declared-inhabitants roster derives its grounding by lookup, with the roster as evidence -- the namespacing answer to the atom authority question, at specimen scope. The add slice's ten type-spine nodes (Arrow, Conj, Atom) are all roster members, so: - candidate_generation_translate_self_emit_dag_add_slice_holds passes; its floor_expected_red roster row and per-row note delete per the roster's own stale-quarantine arm - the dag same-language ingest path compiles end-to-end: cross_language_compile accepts, byte-equal to the authority's own serialization, no carried diagnostics - the add-slice stall narrows to its four python/typescript round-trip members; the original trigger's causal clause was refuted by execution and is restated against the grammar parse-product population - the instrument's frontier guard flips to add_slice_composition_accepts_holds (DESIGN 4b(4): frontier guard to permanent regression control) - five manual witnesses flip with it: two root flips rewritten to assert the green state, three transitive conjunctions updated The kinds stay frontier: non-member Arrow/Conj/Atom specimens carry GroundingNotDerived exactly as before, and all fourteen enrolled refusal/acceptance controls pass unchanged. The door's production path still reds inside rust emission, untouched by this rule. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
…joins binding to inhabitant once (#10686) The resolver already binds the surface spelling Int to the canonical binding symbol dag_binding_type_int; what that binding DENOTES is the Int inhabitant declared at dag_declared_inhabitants_core. Every hand-rolled fixture facts lookup re-authored that join (dag_add_canonical_grounding_for, record_construct_canonical_grounding_for). The language authority now declares it once as dag_binding_denotation, and infer_node_facts consumes it: an Atom whose identity is a canonical dag binding with a declared denotation derives with that denotation as its grounding evidence. Direct-rust-door specimen census: 14 underived -> 10 underived (the four dag_binding_type_int atoms derive; grammar-production atoms, algebra atoms, bare operand atoms, and the arrow/conj spine stay on the frontier unchanged). Specimen-scope interim in the same frame as infer_node_declared_in_dag_inhabitants: both delete in favor of consuming resolution output when the resolver hands infer declaration-resolved identities directly (the namespace migration's completed state). Witness: v2.test.execution.dag_binding_denotation — all four Int binding atoms in the door specimen derive with dag_int_inhabitant_node() as structural evidence, and the two bare operand atoms stay GroundingNotDerived (boundary control). Refusal suite 14/14, ingest bridge 7/7, add-slice instruments 2/2 green; every remaining red in the at-risk population reproduces identically on the pre-change tree and is enrolled in floor_expected_red. Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7725725ca6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if infer_node_declared_in_dag_inhabitants(n: n) { | ||
| inferred_facts_from_derived_type( | ||
| node: n, | ||
| derived_type: dag_declared_inhabitants_root(), |
There was a problem hiding this comment.
For every roster match, this records the entire inhabitants roster as the node's derived_type. However, canonical_grounding_from_derived_type stores this value as CanonicalGroundingWitness.structural.evidence, and inferred_facts_resolved_type exposes that field as the node's resolved type; consumers such as eval_runtime_value_acceptance_witness then compare the full roster against the runtime value's actual type and reject with eval_rejected_resolved_type_mismatch. Translation can likewise use this evidence as the replacement node after coercion fails. The membership authority must either yield the member's actual resolved type or be represented separately from type evidence rather than placing the roster in this field.
Useful? React with 👍 / 👎.
| xs: node_subtree_nodes(root: dag_declared_inhabitants_root()), | ||
| predicate: fn(member) { member == n } |
There was a problem hiding this comment.
When inference is run on dag_declared_inhabitants_root() itself, node_subtree_nodes includes the root as its first element, so this predicate incorrectly treats the roster container as one of its declared inhabitants. The subsequent construction passes that same root as both node and derived_type, causing canonical_grounding_from_derived_type to hard-reject it with grounding_evidence_is_source; previously this input remained on the accepted grounding frontier. Traverse only the actual declared-member targets, or otherwise exclude the container root.
Useful? React with 👍 / 👎.
|
Consolidated into #10692 (lane-owner request: one PR for the grounding-frontier push). This commit lands there unchanged as the second commit; CI green on this tree. Closing in favor of the consolidated PR. |
2 participants
Stack note
This branch is stacked on #10670 (the stage-verdicts instrument). Until that merges, this PR's diff includes the instrument commit; the change described below is the second commit only. Based on
mainso the witness floor CI runs against it.What lands
v2.compiler.infergains the declared-inhabitant membership derivation: a node declared in the dag language authority's declared-inhabitants roster (dag_declared_inhabitants_root) derives its grounding by lookup, with the roster as the evidence. This is the namespacing answer to the atom-authority question, at specimen scope — the authority already fixes what its members denote, so infer looks the declaration up rather than inventing it. The add slice's ten type-spine nodes (the add-fnArrow, the int-inhabitantConjs, the inhabitant and surface-spellingAtoms) are all roster members.The kinds stay frontier: a non-member
Arrow/Conj/AtomcarriesGroundingNotDerivedexactly as before.Measured consequences (all executed on this branch)
candidate_generation_translate_self_emit_dag_add_slice_holds— the enrolled expected-red witness — passes. Itsfloor_expected_redroster row and per-row note delete in this change, per the roster's own stale-quarantine arm.infer_acceptedwith zero carried diagnostics andcandidate_acceptedwith none carried; its frontier guard flips toadd_slice_composition_accepts_holds— the DESIGN 4b(4) move from frontier guard to permanent regression control.cross_language_compileover the ingested parse tree accepts,carriedbyte-equal to the target model's own serialization of the same node, no carried diagnostics.manual/witnesses flipped (green before, red after the rule — caught by the flip census, all rewritten per 4b(4) with the flip recorded in comments): two root flips (ingest_identity_coercion_accepts_source_present_in_authored_roster,ingest_cross_language_compile_accepts_holds) and three transitive conjunctions.What did not move (negative controls)
translate_underived_refusal_testpass unchanged — the emptyConj, the bodied arrow, the rust grammar atom, the disj/value specimens all stay underived-and-refused.cross_language_compile_refuses_canonical_underived_holdscontrol).dag_add_emit_round_trip(dag_add_domain_*) are unchanged (verified red on the pre-change tree as well).Census evidence
Every test module referencing
infer_grounding_not_derivedor the touched machinery was run pre- and post-change:infer_self_grounding_wall(12),translate_underived_refusal(14),dag_add_emit_round_trip(6),emit_ingest_grammar_relation_round_trip(1),ingest_bridge(9),cross_language_add_python_to_typescript(4),inhabitant_neutralization(6),inhabitant_neutralization_e2e(6),emit_host_classical_not(14),branch_infer_if_then_else(2),compile_eval_thesis_proof(6), the floor-coherence (5) and stall (11) witnesses, plus the door's production group root.