Skip to content

scalar_profile() admits CheckedNodeTag::Correspondence but no corpus node carries it #133

Description

@kreneskyp

Found in review of #132 and recorded rather than folded in — it is the same defect as #100 in the same function, but a different tag, and #132's scope is claims.

The defect

src/exact_scalar.rs:794-801 scalar_profile() declares six supported_tags:

ScalarType, BoundedDomain, Value, Expression, Claim, Correspondence

A census over the nodes corpus_package().wire() actually produces finds zero nodes tagged correspondence. Deleting CheckedNodeTag::Correspondence from scalar_profile() leaves all 25 test binaries green — measured in review, not deduced.

So that entry admits nothing. Whether the generator handles a correspondence node correctly, refuses it, or panics is unverified, and no gate would notice if the behaviour changed.

This is exactly #100's shape: a declared capability that no fixture exercises, so the criterion covering it cannot fail. #100 closed it for Claim. Correspondence is the remaining one in the same list.

Why the miscount is worth recording too

#132's PR body published a tag census claiming correspondence 1. That number came from grep -o '"correspondence"' tests/exact_scalar_support/package.rs, which counts string literals in the source file, not registered nodes. The single occurrence is at tests/exact_scalar_support/package.rs:155, inside declaration_for's match arm:

"expression" | "relation" | "state" | "temporal" | "correspondence"

That is a tag classification, not a node. The same arm inflates relation, state and temporal by one each, which is why that published census disagreed with a real node census on 8 of 13 rows. The load-bearing figure in it (claim 0) was independently correct, and #132's conclusion stands — but the method does not, and the corrected numbers are in #132's body now.

A source-text grep is not a corpus census. Recording it because the same shortcut would misreport any future coverage claim the same way.

Asked for

  1. Decide whether the exact-scalar generator is meant to support correspondence nodes at all. If not, remove the tag from scalar_profile() rather than leaving an unexercised admission — a declared capability nothing tests is a claim the gate cannot check.
  2. If it is meant to be supported, add a correspondence-tagged node to the corpus reachable from a requested item, exactly as Add a claim-tagged corpus node so FR-014-AC-5's claims field is exercised #132 did for claim, and run a mutation showing a gate goes red over it. Add a claim-tagged corpus node so FR-014-AC-5's claims field is exercised #132's approach and the QUIRE_CODEGEN_BLESS=1 golden regeneration are the pattern to follow; do not hand-edit a golden.
  3. Whichever way it goes, census the remaining four tags (ScalarType, BoundedDomain, Value, Expression) the same way, by counting nodes rather than source strings, so the answer is known for all six rather than for the two that happened to be investigated.

Not claimed

No evidence the generator mishandles correspondence nodes. The defect is that nothing would tell us either way.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions