feat(csharp): link a property/field read to the member it reads

[brobl2008]

The gap

The member-call resolver (#1609) binds recv.Method() to the receiver's declared type. A
member used as a value is not an invocation, so no branch ever saw one:

var items = ctx.Items;   // no edge at all

A property was therefore reachable only from its own declaration. "Which methods read this
member" had no answer, and a type exposed purely through properties looked unused.

The change

The extractor records a property/field read on a simple or this receiver, and extract()
resolves it through the same path a member call takes: the receiver's declared type, resolved
with the existing namespace/using/alias scoping, then the member looked up on that type or its
resolvable bases.

Every refusal the call path already makes is inherited — an untypable receiver, an ambiguous
type name, an unresolved base in the chain, or a member the type does not declare all yield
nothing rather than a guess. There are tests for each.

The edge is references[member_access], never calls. Reading a property is not an
invocation, and conflating them would corrupt call-graph queries. A member access that is an
invocation's function is skipped so ctx.Save() stays a single call edge; the receiver of a
chained call is not skipped, because ctx.Items.Any() genuinely reads Items first.

Two notes for review

Entries ride raw_calls rather than a channel of their own. A caller_nid is rewritten by
four separate id passes in extract() — merge-away, prefix remap, symbol remap, collision
disambiguation. A parallel list has to repeat all four, and the day one is missed the result is
edges whose source is not a node: silent, and visible only as a query that quietly returns
nothing. That is not hypothetical — it happened during development, which is why there is an
explicit no-dangling-endpoints test. No callee is set and member_read marks these entries,
so every existing raw_calls consumer (all of which require callee or is_member_call)
ignores them.

Properties are indexed separately from methods rather than folded into method_index, so a
call can never resolve to a property, nor a read to a method.

Tests

Twelve new tests: the basic read, two properties on one type not cross-attributing, a scalar
property, the member winning over a same-named type, a chained call still recording the read, a
method call not being recorded as a read, an unknown member, an untyped receiver, an
inherited property through a base, this.Member, the relation/context being
references[member_access], and no dangling endpoints.

Full suite: 24 → 25 failures, +12 passing. The single differing failure is
test_labeling.py::test_label_communities_batches_when_over_batch_size, which is
order-dependent on pristine source — on an unmodified tree, its file as a whole passes (35
tests) but that one test selected by itself fails. It exercises a synthetic graph with a
monkeypatched LLM and touches no C# extraction. Reproduction on a clean checkout:

pytest tests/test_labeling.py                                              # 35 passed
pytest tests/test_labeling.py::test_label_communities_batches_when_over_batch_size   # fails

Worth flagging separately; I have not touched it here.

[graphify-labs]

Graphify reviewed this change.

Worth a look — the grounded gate found no coupling regressions or blocking issues, but 2 advisory finding(s) below merit a look before merge.

Formal verification. 1 change(s) tested, no difference found (not proven).

---

Graphify review — findings

Adds C# member-access read edges: reading a property or field on a typed receiver (ctx.Items, this.Member) now links the accessing method to the declaration via a references[member_access] edge, so "which methods read this member" is answerable instead of the member being reachable only from its own declaration. The extractor records such reads on raw_calls (marked member_read, no callee) when a member-access node isn't itself an invocation target, and _resolve_csharp_member_calls resolves the receiver's declared type through the existing namespace/using/alias scoping and looks the member up on the type or its resolvable base chain via a new member_index/_member_on_type_or_bases. Ambiguous or untypable receivers, and the receiver of a chained call, are handled deliberately — no edge on ambiguity, and ctx.Items.Any() still records the Items read while ctx.Save() stays a call, not both.

Worth a look

• C# member-read index can resolve reads to methods — graphify/extract.py:3404 · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
• C# member-write expressions are emitted as member reads — graphify/extractors/engine.py:5682 · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review

Analysis details — impact, health, verification

Impact & health

Graphify review

Impact — 1889 functions depend on the 438 functions this change touches.

Health — this change adds coupling hotspots:

• new: extract() — 492 callers, 42 callees
• new: _rebuild_code() — 98 callers, 50 callees
• new: _extract_generic() — 18 callers, 24 callees
• new: extract_xaml() — 19 callers, 17 callees
• new: dispatch_command() — 2 callers, 122 callees
• new: extract_objc() — 27 callers, 9 callees
• new: extract_js() — 80 callers, 3 callees
• new: _get_extractor() — 26 callers, 6 callees
• …and 33 more — each is listed as a finding

Verification — 1889 functions in the blast radius were not formally verified this run (proofs are advisory here).

Gate & verification

graphify gate

PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.

Advisory (not blocking):

• verification_scope: 1738 function(s) in the blast radius were not formally verified this run

Formal verification

Could not verify: Could not verify \_infer\_merge\_root.

The verifier did not have enough to check \_infer\_merge\_root, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `graph_path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify prefix\_graph\_for\_global.

The verifier did not have enough to check prefix\_graph\_for\_global, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 115 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous

Could not verify: Could not verify dispatch\_command.

The verifier did not have enough to check dispatch\_command, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly SystemExit — names the real obstacle, not a sampling gap)

Could not verify: Could not verify \_is\_ignored.

The verifier did not have enough to check \_is\_ignored, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

No difference found (not proven): No behavior difference found in \_match\_anchored\_ignore\_pattern (not a proof).

The verifier ran both versions of \_match\_anchored\_ignore\_pattern on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

Could not verify: Could not verify detect.

The verifier did not have enough to check detect, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_resolve\_csharp\_member\_calls.

The verifier did not have enough to check \_resolve\_csharp\_member\_calls, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: non-vacuity: domain too small (only 1 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous

Could not verify: Could not verify \_csharp\_extra\_walk.

The verifier did not have enough to check \_csharp\_extra\_walk, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 200 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify \_extract\_generic.

The verifier did not have enough to check \_extract\_generic, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_js\_extra\_walk.

The verifier did not have enough to check \_js\_extra\_walk, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 200 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify \_ts\_extra\_walk.

The verifier did not have enough to check \_ts\_extra\_walk, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 200 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify introspect\_postgres.

The verifier did not have enough to check introspect\_postgres, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 24 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly ProgrammingError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify \_resolve\_source\_path.

The verifier did not have enough to check \_resolve\_source\_path, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `graph_path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify resolve\_ruby\_member\_calls.

The verifier did not have enough to check resolve\_ruby\_member\_calls, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: non-vacuity: domain too small (only 1 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous

Could not verify: Could not verify \_\_init\_\_.

The verifier did not have enough to check \_\_init\_\_, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify on\_any\_event.

The verifier did not have enough to check on\_any\_event, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: method — first parameter is `self`, which needs a constructed instance (not synthesizable)

Could not verify: Could not verify watch.

The verifier did not have enough to check watch, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `watch_path` is annotated `Path` — outside the synthesizable primitive/collection set

· 41 more finding(s) on lines outside this diff (see the check run).