Repository navigation
mandatory_tag_gate_witness: read Node out of NormalizedTree - #13458
Conversation
…alized.root)
normalize returns a NormalizedTree; the witness built GrainTree{root: Node} from it directly, a compile error on main. Parse-grain claims (8) and 3 normalized-grain rejects pass; mandatory_tag_normalized_grain_clean_accepts is red for a separate reason (see PR).
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…zed rejects vacuous Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…rmalize Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
… supplied tree unresolved) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
APPROVE at exact head 641ccf98697138449bc45a599ff68f8a36ed9948. No blocking finding in this bounded witness-type repair plus failure-mode filing. This is not approval of a repaired mandatory-tag lens or certification of the production compiler's tag enforcement.
The executable change is the correct projection: normalize returns the admitted NormalizedTree carrier, whose root is the Node that GrainTree and the existing lens inspect. normalized_grain_tree now passes normalized.root, not the carrier and not the pre-normalize parse tree. Earlier-stage refusal still makes the witness fail. No assertion, gate, roster or exclusion is weakened.
The new row accurately preserves the important distinction: the reported normalized-grain clean positive is RED, while the missing/misnamed negatives fail to discriminate that blindness. mandatory_tag_scan_decls really does select dag_surface_data_decl; the described surface-versus-lowered-shape mismatch is consistent with that reader. Parse-grain evidence is kept separate from normalized-grain evidence. The long-lane exclusion is explicitly acknowledged, and this PR does not pretend that adding an unenrolled identity to floor_expected_red would establish an executing floor verdict.
The supplied normalized-root / empty-resolution-index probe is explicitly NOT credited as the production compile path. Its rejection of both clean and violating specimens is a loud rejection on that experiment, not proof of production fail-open acceptance. The row leaves the actual resolved/inferred input and the correct repair location unestablished; preserve that uncertainty when the implementation is undertaken.
The ceiling is an attainable normalized-tree admission guarantee, not a rung achieved by this PR. Read the restoration condition as the complete clean/missing/misnamed discriminator over the actual normalized producer. A clean-positive pass alone, a parse-tree substitution, or an always-accept gate would not satisfy the condition that the negatives remain valid for their own reasons. Any claim about production compiler enforcement still needs its own real-path evidence, and the controls remain rather than being deleted on repair.
CI: the exact-SHA query returns workflow 37424836503, completed successfully. All five jobs (generated, floor, emit-build, rust-unit-tests and witnesses) succeeded; all-target lint and stage0 checking are successful steps. This does not imply the excluded long-lane witness ran in the required floor or that its intentional red has gone green. The BuildBuddy probes, historical timings and mutation described in the receipt remain author-run evidence; I did not replay them.
Reviewed the pinned witness, pinned RFM, NormalizedTree carrier, relevant lens/roster source, head DESIGN and CI metadata/steps. No local compiler execution, new census, merge or enqueue. No further code change, new test lane, or expansion into the lens repair is required to land this filing.
Compile fix:
normalizeyields a NormalizedTree; the witness put it inGrainTree { root: Node }. Nownormalized.root.Evidence (claim_batch, ctrl-build --remote): 8 parse-grain claims + normalized missing/misnamed rejects + roster claim PASS. Mutant (
root: parse_root) flipsnormalized_grain_clean_acceptsto PASS, i.e. the repaired value is what that claim reads.Not fixed, found by the probe:
mandatory_tag_normalized_grain_clean_acceptsis RED on the repaired tree. Its gate rejection ismandatory_tag_missing_required_decl(probes for unreadable/not_accepted/type_mismatch/gated all false; normalize itself accepts). So the normalized tree no longer exposes the anchor decl name to the lens. Consequence: the normalized-grainmissing/misnamedrejects pass vacuously (everything is 'missing'). Separate defect in normalize output vs mandatory_tag lens; needs its own item.Don't merge; #13341 re-queues after #13400 and this.
🤖 Generated with Claude Code