You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Commit 947d6c3
Browse filesBrowse the repository at this point in the historyBrowse files
P-037 A2.2-4R3: F-CONDITIONAL-RECEIVER repaired; a reduced receiver under ?. binds ordinal 0
A2.2-4's completeness oracle found (formal note §10.6.10,
F-CONDITIONAL-RECEIVER, §10.1 case 1) that the invocation loop read a
reduced extension receiver from a MemberAccessExpressionSyntax only.
`r?.Ext(...)` invokes through a MemberBindingExpressionSyntax, so the
receiver handle was dropped and the call was relevant only if another
argument was a handle: the handle's declared ordinal 0 vanished. Pinned RED
on the hostile case ext-conditional-access.
The repair: for an invocation whose expression is a member binding, the
receiver is the nearest enclosing ConditionalAccessExpressionSyntax's own
expression — a binding is by construction the first operation after its
`?.`, so that expression is what the receiver argument evaluates
(`a?.B?.Ext()` reads the inner binding `.B`, a member, which the walker
already classifies as no handle). The receiver then goes through ValueOf and
the value-flow walker as a member-access receiver does, with one more rule
in the walker: Roslyn binds such a receiver argument to an
IConditionalAccessInstanceOperation placeholder standing for the conditional
access's own operand — the same reference when the call is entered at all (a
null operand skips the call and yields no alternate value) — so the walker
classifies that operand. Nothing else in the binding moves.
Measured on this tree: the 52 census shapes read byte-identical; the probe's
oracle reading is unchanged (RED 1, F-MEMBER); ext-conditional-access reads
green (captured, ordinal 0, var); every other pinned RED stays as pinned
(F-MEMBER, F-VOCAB); the inertness control and the local rehearsal against
the T before-takes are unchanged on both engines. The ledger moves
F-CONDITIONAL-RECEIVER to `closed`, which closes the three case-1 findings;
spec/OwnIR.md §5.2 names the `?.` receiver; §10.6.9 and §10.6.11 record the
landing. Same instrument, no new T/R.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QfeUtLRm6KFRWcTGQZxQQb
Copy file name to clipboardExpand all lines: corpus/p037-hostile/cases/ext-conditional-access.cs
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -1,5 +1,5 @@
1
1
// GENERATED by scripts/p037_hostile_census.py (P-037 A2.2-4 hostile census); do not edit.
2
-
// site form: a reduced extension method invoked through `?.` on the handle; the receiver still binds declared ordinal 0
2
+
// site form: a reduced extension method invoked through `?.` on the handle; the receiver still binds declared ordinal 0 (F-CONDITIONAL-RECEIVER, repaired in A2.2-4R3)
Copy file name to clipboardExpand all lines: corpus/p037-hostile/expected.json
+2-5Lines changed: 2 additions & 5 deletions
Original file line number
Diff line number
Diff line change
@@ -278,11 +278,8 @@
278
278
"explanation": "receiver_not_summary_parameter"
279
279
}
280
280
],
281
-
"red": {
282
-
"occurrence_not_captured": 1
283
-
},
284
-
"finding": "F-CONDITIONAL-RECEIVER",
285
-
"why": "site form: a reduced extension method invoked through `?.` on the handle; the receiver still binds declared ordinal 0"
281
+
"red": {},
282
+
"why": "site form: a reduced extension method invoked through `?.` on the handle; the receiver still binds declared ordinal 0 (F-CONDITIONAL-RECEIVER, repaired in A2.2-4R3)"
Copy file name to clipboardExpand all lines: corpus/p037-relevance/oracle_findings.json
+7-7Lines changed: 7 additions & 7 deletions
Original file line number
Diff line number
Diff line change
@@ -9,13 +9,6 @@
9
9
"status": "open: a census finding; carrying these members in the orphan carrier is a production change to be classified on its own",
10
10
"red": "occurrence_not_captured"
11
11
},
12
-
"F-CONDITIONAL-RECEIVER": {
13
-
"class": "case 1",
14
-
"title": "a reduced extension receiver under `?.` is not bound to ordinal 0",
15
-
"evidence": "The invocation loop reads the receiver only from a MemberAccessExpressionSyntax; `r?.Ext(...)` invokes through a MemberBindingExpressionSyntax and the receiver handle is dropped, so the call is not relevant unless another argument is a handle. Witnessed by the hostile case ext-conditional-access.",
16
-
"status": "open: an implementation defect in the A2 classifier, to be repaired as its own classified change",
17
-
"red": "occurrence_not_captured"
18
-
},
19
12
"F-VOCAB": {
20
13
"class": "case 3",
21
14
"title": "argument shapes the frozen vocabulary has no name for: a tested operand, an interpolation hole, an indexer argument, a constructor-initializer argument",
@@ -47,6 +40,13 @@
47
40
"evidence": "For an expanded params argument the argument operation carries the call's own syntax, so the span-containment match finds nothing and the fallback classifies `model.GetOperation(expression)` of the element alone. A transparent wrapper (parentheses, the null-forgiving `!`) has no operation of its own, so the handle under it is lost and the call is not relevant; a boxing or user-defined element conversion sits on the array element, not on the expression, so a struct handle boxed into `params object[]` or a handle passed through op_Implicit into `params Box[]` yields an opaque-and-relevant slot although nothing of the handle reaches the callee. Witnessed by the hostile cases whose binding is `params` and whose value-flow shape is parens, bang, boxing or user_implicit; casts, `as` and the may-value forms have operations of their own and are classified correctly.",
48
41
"status": "closed: A2.2-4R2. ValueOf classifies an expanded params element from the ParamArray argument's array initializer element (its conversion included) instead of the bare syntax; the affected pairwise cases are designed green by the generic rule.",
"title": "a reduced extension receiver under `?.` is not bound to ordinal 0",
47
+
"evidence": "The invocation loop reads the receiver only from a MemberAccessExpressionSyntax; `r?.Ext(...)` invokes through a MemberBindingExpressionSyntax and the receiver handle is dropped, so the call is not relevant unless another argument is a handle. Witnessed by the hostile case ext-conditional-access.",
48
+
"status": "closed: A2.2-4R3. The invocation loop reads the reduced receiver of an invocation through a MemberBindingExpressionSyntax from the nearest enclosing ConditionalAccessExpressionSyntax's expression; ext-conditional-access is designed green.",
Copy file name to clipboardExpand all lines: docs/notes/p037-formal-kernel.md
+23-2Lines changed: 23 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1171,7 +1171,12 @@ causes of FACT-DIFF. Tracked in #364 with its own acceptance.
1171
1171
classified from the ParamArray argument's array-initializer element, its
1172
1172
element conversion included, so a handle under parentheses or `!` is no
1173
1173
longer lost and a boxed or user-converted element no longer yields a false
1174
-
slot; the affected pairwise cases read green by the generic design;
1174
+
slot; the affected pairwise cases read green by the generic design. R3
1175
+
landed in the commit carrying this line: the reduced receiver of an
1176
+
invocation through a member binding (`r?.Ext(...)`) is read from the
1177
+
enclosing conditional access, so the handle binds declared ordinal 0 there
1178
+
too; `ext-conditional-access` reads green; the three case-1 findings are
1179
+
closed;
1175
1180
-**A2.2-5** mutation campaign: remove the handle, add parentheses, perturb the
1176
1181
binding, distinguish nested calls;
1177
1182
-**A2.2-S** cumulative A2 after-evidence on M1 against the existing R with
@@ -1229,7 +1234,7 @@ does a pinned RED that silently disappears):
1229
1234
| F-MEMBER | 3 | expression-bodied members, struct and record methods, property accessors are outside the legacy admission *and* the orphan carrier (the gates sit inside the class / block-body loop) | probe `Box.op_Implicit`; hostile `member-*`|
1230
1235
| F-SHADOW | 1 | the guarded-fact handle set was keyed by spelling (`handles.Contains(lr.Local.Name)`) and the candidate collector descends into lambdas: a same-spelled non-candidate in a sibling scope, or beside a lambda-local creation, got a false `var` fact. **Repaired in A2.2-4R1** (10.6.11) | hostile `shadow-*`, now green |
1231
1236
| F-PARAMS-ELEMENT | 1 | an expanded params element was classified from its bare syntax: under parentheses or `!` the handle was lost (no operation of its own); under a boxing or user-defined element conversion a false opaque-and-relevant slot was emitted. **Repaired in A2.2-4R2** (10.6.11) | hostile `pw-*-params-*` with parens / bang / boxing / user_implicit, now green |
1232
-
| F-CONDITIONAL-RECEIVER | 1 |`r?.Ext(...)` invokes through a member binding, the receiver is read from `MemberAccessExpressionSyntax` only, and ordinal 0 is dropped| hostile `ext-conditional-access`|
1237
+
| F-CONDITIONAL-RECEIVER | 1 |`r?.Ext(...)` invokes through a member binding, the receiver was read from `MemberAccessExpressionSyntax` only, and ordinal 0 was dropped. **Repaired in A2.2-4R3** (10.6.11) | hostile `ext-conditional-access`, now green|
1233
1238
| F-VOCAB | 3 | four argument shapes the frozen list has no name for: a tested operand, an interpolation hole, an indexer argument, a constructor-initializer argument; production correctly emits nothing, the sentence demands a name | hostile `vocab-*`|
1234
1239
1235
1240
Two rulings the oracle reads into the freeze, recorded here as §10.1 case-4
@@ -1299,3 +1304,19 @@ nested-function gap.
1299
1304
expanded params binding, across site forms and carriers) read green by the
1300
1305
generic design; every other pinned RED stays; inertness and the local
1301
1306
rehearsal unchanged.
1307
+
-**R3, F-CONDITIONAL-RECEIVER.** In the invocation loop the reduced
1308
+
receiver is read from a `MemberAccessExpressionSyntax` as before and, for
1309
+
an invocation whose expression is a `MemberBindingExpressionSyntax`, from
1310
+
the nearest enclosing `ConditionalAccessExpressionSyntax`'s expression: a
1311
+
binding is by construction the first operation after its `?.`, so that
1312
+
expression is the receiver (`a?.B?.Ext()` reads the inner binding `.B`, a
1313
+
member, not a handle). The receiver then goes through `ValueOf` and the
1314
+
walker as a member-access receiver does, with one more rule in the walker:
1315
+
Roslyn binds such a receiver argument to an
1316
+
`IConditionalAccessInstanceOperation` placeholder, which stands for the
1317
+
conditional access's own operand (the same reference when the call is
1318
+
entered at all; a null operand skips the call and yields no alternate
1319
+
value), so the walker classifies that operand. Measured: the 52 shapes
1320
+
and the probe byte-identical; `ext-conditional-access` reads green
1321
+
(captured, ordinal 0, `var`); every other pinned RED stays; inertness and
0 commit comments