P5b-fix: an unresolved security-group entry must not give PASS (INV-FUNC-001)

core/verification/reachability.py

@@ -479,7 +479,9 @@ def _side(self, fact: Fact, owner: str) -> _Sides:
         if fact.state == UNKNOWN_STATE:
             run.unresolved.append(f"{owner}: vpc_security_group_ids {fact.reason}")
             return _Sides()
-        return run.groups_of(fact, f"{owner}.vpc_security_group_ids")
+        side = run.groups_of(fact, f"{owner}.vpc_security_group_ids")
+        run.unresolved.extend(side.unresolved)  # E3: every entry must be resolved (C-156)
+        return side
 
     def _subnet(self, inst: Any) -> None:
         run = self.run
@@ -679,7 +681,7 @@ def check_listener(self) -> None:
         engine = db.engine
         if engine.state == UNKNOWN_STATE:
             run.unresolved.append(f"{db.address}: engine {engine.reason}")
-        elif engine.state == KNOWN and str(engine.value).lower() != "postgres":
+        elif engine.state == KNOWN and engine.value != "postgres":  # E2: the exact string
             raise run.stop(F, 3, R.PORT_MISMATCH, f"{db.address}.engine is {engine.value}")
 
     # --- rows 6 to 9 -----------------------------------------------------------------------------

docs/DECISIONS_REGISTER.md

@@ -166,4 +166,5 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec
 | C-152 | P5b: endpoint resolution across moves, and indeterminate endpoints | The bindings `S` and `D` are addresses of the **trusted** state (registry §6.1). A baseline resolves a binding by address in the candidate; an address that no candidate resource has is absent (row 1, FAIL, `endpoint.absent`). A candidate with a parent resolves it through the identity report (registry §2.3, moves followed): the match whose `trusted_resource_ref` is the binding; UNCHANGED, MODIFIED and REPLACED give the candidate resource of the match; **DELETED is absent** (row 1); **UNCERTAIN, a placeholder (unknown `count` or `for_each`, support status UNKNOWN) and a resource that is itself UNSUPPORTED are indeterminate**: UNKNOWN (row 4), never FAIL, never PASS. **Registry reading, flagged:** registry §2.4 would call an UNSUPPORTED endpoint resource UNSUPPORTED rather than UNKNOWN; the work package says UNKNOWN and both are lack of proof, so the work package is followed and the question goes to the reviewer. A candidate that has a parent but no identity report, or a report with no match for the binding while the parent has the resource, is UNSUPPORTED `identity.missing` (as in P5a). A binding that the parent does not have either is UNSUPPORTED `parameters.invalid` (the definitions and the trusted state disagree). **A created endpoint** (the candidate creates the resource at another address and the old one is DELETED) is FAIL by row 1: no heuristic match is made; only a `moved` block or an identity match ties a new address to the trusted one. The observation `endpoints` records, per binding, the trusted address, the match change type and the candidate address. | Proposed (P5b) |
 | C-153 | P5b: rows 1 to 9 and the definitions they need | The rows of registry §6.4 are evaluated in order and the first that applies returns. Row 2 collects every cause it can evaluate, reports all of them in the observation `row2_causes` and names the reason by the first in this fixed order: relevant-unsupported type, M3 route, `propagating_vgws`, interface block, name-based `security_groups`, no `vpc_security_group_ids` or no `subnet_id`, MIXED, RETAINED-INLINE, `unresolved` direction form (C-120(c)), unsupported value or rule, other. **Definitions** (each with the registry text it makes precise): `SG(S)` and `SG(D)` are the groups that the `vpc_security_group_ids` of `S` and `D` reference; `src_sg(r)` is `source_security_groups` of the stored rule view (a reference gives the address of the group; a literal AWS id gives `EXTERNAL:<id>` and matches no configured group), so "src_sg(r) contains a group in SG(D)" is a non-empty intersection of addresses; `self(r)` is the stored `self` flag and E6 needs `h in SG(S)`; the CIDR clauses use `cidr.covers` on the IPv4 sources of **one** determinate rule that permits TCP/5432 (`ports.permits_tcp`): E5 and E6 say "exists r with ... v4(r) covers" and `v4(r)` is the CIDR list of a single rule, so two rules with half of the range each do not cover it (no pooling across rules; a test pins this); **"partly covers"** (row 8) is `cidr.overlaps`: the IPv4 sources of a determinate rule that permits TCP/5432 intersect the target, and (E5 or E6 failing) no rule covers it (interval arithmetic, no enumeration); `ADDR(S)` is `private_ip/32` if it resolves to an IPv4 address, else the `cidr_block` of the subnet of `S`; an unresolved subnet CIDR makes the clause unresolved. **"An indeterminate rule could satisfy" E5 or E6** (row 7): a rule of the side (an egress rule of a group in `SG(S)` for E5, an ingress rule of a group in `SG(D)` for E6, a rule with direction `None` for either, a rule of an `UNRESOLVED:*` pseudo-group, a rule resource that is an UNKNOWN placeholder) that is not determinate, is not unsupported, **could permit TCP/5432** (`ports.may_permit_tcp`, so an unresolved protocol or port counts) **and whose satisfying side could match**: its group sources are unresolved or could be the other side's groups, its IPv4 sources are unresolved, include a prefix list, or cover or partly cover the target, or (E6) its `self` is unresolved. **Counted:** an indeterminate rule with a resolved satisfying source and an unresolved port or protocol is counted (UNKNOWN), because the rule could supply the permission; this is the safe direction and it is the mirror of the gap of C-150 (where SEC `possible` text drops such a rule and can give PASS); here dropping it could give an unsound FAIL, so it is not dropped. When both E5 and E6 fail, row 7 applies if either failing condition could be satisfied by an indeterminate rule (registry text: "it"; the more cautious reading), then row 8. **Where the registry is silent (R5), UNSUPPORTED and listed as a spec gap:** a `vpc_id` of a group in `SG(D)`, of `S`'s subnet or of a route table that is a literal id rather than a reference to a configured `aws_vpc` (the VPC CIDR is then unknown); a literal AWS id in `vpc_security_group_ids`; `D` with neither `port` nor `engine`; a route table whose `vpc_id` is unresolved and that has an M3 candidate route or `propagating_vgws` (it may be the VPC of `D`); an unresolved or unsupported route destination or target in a route table of `VPC(D)`, a dynamic route expansion that cannot be fixed, an unsupported value of a field the path reads, an invalid `private_ip`. **Unresolved values (row 4):** an unresolved `vpc_security_group_ids`, group `vpc_id`, `subnet_id`, subnet `vpc_id` or an unresolved `D.port` (**gap:** registry row 4 names E3 and E4 but not E2; an unresolved E2 cannot be PASS, so it is UNKNOWN). **M3:** a route of a route table of `VPC(D)` whose IPv4 `cidr_block` lies inside the CIDR of that VPC and whose target is not `local` (`gateway_id = "local"` and no other target); IPv6-only routes are not read (M5); a route wider than the VPC CIDR never applies. Rows 3 and 5 FAIL only on resolved values. | Proposed (P5b) |
 | C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys (present on every path): `row`, `reason`, `detail`, `endpoints`, `port`, `unresolved` (why row 4 applies), `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) |
-| C-155 | P5b: cases that registry §6 does not decide, settled conservatively here, for registry v1.1 | Implementing INV-FUNC-001 exactly as §6.3 and §6.4 left these open; each was settled by the work package's rule R5 (UNSUPPORTED, or the cautious reading) and is listed in C-152 and C-153. The authors should confirm or amend them together with C-150 in registry v1.1 (a new file under C-85, with the version bump of the invariants whose results change). **(1) Row 4 and E2.** Row 4 names E3 and E4 but not E2; an unresolved `D.port`, or an unresolved `D.engine` when there is no port, is UNKNOWN here (row 4), because an unresolved E2 cannot be a PASS and no other row fits. **(2) Row 7, "it".** When both E5 and E6 fail and an indeterminate rule could satisfy only one of them, row 7 is UNKNOWN here (the more cautious reading; the precise reading would be FAIL, since both are needed). **(3) "Could satisfy".** An indeterminate rule with a resolved satisfying side beside an unresolved port or protocol counts as one that could satisfy (UNKNOWN), unlike the SEC `possible` text of C-150, which drops it. **(4) Row 2 and an UNSUPPORTED endpoint resource.** The work package says UNKNOWN (C-152); §2.4 would call it UNSUPPORTED. **(5) Rules of unknown direction.** A rule resource whose `type` is unresolved counts as a rule of every direction: it can satisfy E5 or E6 (row 7) and makes a group that declares an explicit empty list MIXED (row 2). **(6) A pseudo-group with an unresolved target.** Its rules are determinate but may belong to a group of `SG(S)` or `SG(D)`; they count for row 7. **(7) Literal ids.** A literal AWS id as a `vpc_id`, as an entry of `vpc_security_group_ids` or as a `subnet_id` is UNSUPPORTED (the VPC CIDR or the rules of that group are not known). **(8) M1.** Groups of `D` in two VPCs, and `D` with neither `port` nor `engine`, are UNSUPPORTED. **(9) M3.** A route table whose `vpc_id` cannot be fixed, a placeholder route table, a route whose destination or target cannot be fixed, a prefix-list destination and a dynamic route expansion that cannot be fixed make the result UNSUPPORTED when they could belong to `VPC(D)`; an IPv6-only route is not read (M5); a route with no target is treated as non-local. **(10) E5 and E6 per rule.** `v4(r)` is the CIDR list of one rule, so two rules with half of the range each do not cover it; the registry text does not say that explicitly. **(11) `src_sg` of an egress rule** is read as the group named in `security_groups` or `source_security_group_id` of that egress rule (a destination group), as AWS does. **(12) `ADDR(S)`** with an unresolved `private_ip` falls back to the subnet CIDR, and an unresolved subnet CIDR leaves E6 undecidable by a CIDR (row 7). | Open (found 29 Oct 2026; P5b) |
+| C-155 | P5b: cases that registry §6 does not decide, settled conservatively here, for registry v1.1 | Implementing INV-FUNC-001 exactly as §6.3 and §6.4 left these open; each was settled by the work package's rule R5 (UNSUPPORTED, or the cautious reading) and is listed in C-152 and C-153. The authors should confirm or amend them together with C-150 in registry v1.1 (a new file under C-85, with the version bump of the invariants whose results change). **(1) Row 4 and E2.** Row 4 names E3 and E4 but not E2; an unresolved `D.port`, or an unresolved `D.engine` when there is no port, is UNKNOWN here (row 4), because an unresolved E2 cannot be a PASS and no other row fits. **(2) Row 7, "it".** When both E5 and E6 fail and an indeterminate rule could satisfy only one of them, row 7 is UNKNOWN here (the more cautious reading; the precise reading would be FAIL, since both are needed). **(3) "Could satisfy".** An indeterminate rule with a resolved satisfying side beside an unresolved port or protocol counts as one that could satisfy (UNKNOWN), unlike the SEC `possible` text of C-150, which drops it. **(4) Row 2 and an UNSUPPORTED endpoint resource.** The work package says UNKNOWN (C-152); §2.4 would call it UNSUPPORTED. **(5) Rules of unknown direction.** A rule resource whose `type` is unresolved counts as a rule of every direction: it can satisfy E5 or E6 (row 7) and makes a group that declares an explicit empty list MIXED (row 2). **(6) A pseudo-group with an unresolved target.** Its rules are determinate but may belong to a group of `SG(S)` or `SG(D)`; they count for row 7. **(7) Literal ids.** A literal AWS id as a `vpc_id`, as an entry of `vpc_security_group_ids` or as a `subnet_id` is UNSUPPORTED (the VPC CIDR or the rules of that group are not known). **(8) M1.** Groups of `D` in two VPCs, and `D` with neither `port` nor `engine`, are UNSUPPORTED. **(9) M3.** A route table whose `vpc_id` cannot be fixed, a placeholder route table, a route whose destination or target cannot be fixed, a prefix-list destination and a dynamic route expansion that cannot be fixed make the result UNSUPPORTED when they could belong to `VPC(D)`; an IPv6-only route is not read (M5); a route with no target is treated as non-local. **(10) E5 and E6 per rule.** `v4(r)` is the CIDR list of one rule, so two rules with half of the range each do not cover it; the registry text does not say that explicitly. **(11) `src_sg` of an egress rule** is read as the group named in `security_groups` or `source_security_group_id` of that egress rule (a destination group), as AWS does. **(12) `ADDR(S)`** with an unresolved `private_ip` falls back to the subnet CIDR, and an unresolved subnet CIDR leaves E6 undecidable by a CIDR (row 7). **(13) An unresolved entry of `SG(S)`** (`S.vpc_security_group_ids`) is UNKNOWN (row 4) here (C-156); an extra allow-only group cannot remove permission, so the authors may relax it to PASS in registry v1.1 when the known groups are enough, once MIXED and RETAINED-INLINE can be checked for it. | Open (found 29 Oct 2026; P5b) |
+| C-156 | P5b-fix: an unresolved entry of `vpc_security_group_ids` is row 4; the engine is compared exactly | Registry §6.3 E3: each entry of `D.vpc_security_group_ids` references a configured aws_security_group with a resolved `vpc_id`; §6.4 row 4: when E3 or E4 needs an unresolved value the result is UNKNOWN. P5b let an unresolved entry (a variable, a `concat` with a variable, a group of unknown `count`) reach row 6 and give PASS when the known groups established the path (found by the external review of PR #22). **(1)** An entry of `D.vpc_security_group_ids` that is unresolved, or that references a placeholder group, is added to the row 4 reasons when the side is read, so row 4 (UNKNOWN, `attribute.unresolved`) applies after rows 1 to 3 and any row 2 cause, and before rows 5 to 9; the path is neither a PASS nor a FAIL then. **(2)** The same for `S.vpc_security_group_ids`; the registry is silent, see C-155 item 13. **(3)** The row 7 use of the unresolved entries of the side is unchanged; row 4 now returns first, so it is not reached for them. **(4)** A literal id stays UNSUPPORTED (C-155 item 7). **(5)** E2 compares `engine` with the exact string `postgres`, as the registry writes it; `Postgres` or `POSTGRES` without a port is row 3 (FAIL) (before, the comparison ignored case). Open question for the authors: the provider may accept other spellings of the engine name; no behaviour beyond the exact comparison. **(6)** Two P5b tests asserted the superseded results (an unresolved entry of `S` with the path established: PASS, row 6; with no path: row 7); they now assert UNKNOWN, row 4, and were changed in the commit that changes the code. | Proposed (P5b-fix) |

docs/PHASE_GATES.md

@@ -138,6 +138,21 @@ with C-143 option B before D4. C-148 NOT_APPLICABLE question goes to the authors
 Proposed; C-149, C-150 Open. C-120(c) verified in source; probe in the P5 gate.
 ```
 
+## P5b — Verification, part 2 (INV-FUNC-001)
+
+```text
+P5 gate: NOT PASSED YET (external review, 29 Oct 2026; PR #22 at 20def0d, merged before the verdict,
+C-28 process lapse recorded a fifth time). Suite passes on Python 3.12 and 3.13 (skipped=1); black,
+ruff and mypy clean. Carry-forward 1 of the P5a verdict is closed: the three covers() mutants are
+killed by the new boundary tests. About 100 reviewer probes of INV-FUNC-001 and 7 mutations of the
+reviewer's own were all as the registry says, except one soundness defect: an unresolved entry in
+vpc_security_group_ids (for example [aws_security_group.db.id, var.u]) gives PASS when the path
+is otherwise established, although E3 requires every entry to be resolved and row 4 gives UNKNOWN.
+Fix package: P5b-fix (feature/p5b-fix). The P5 gate and milestone M2 are decided after it.
+Carry-forward: C-150 and C-155 for registry v1.1 before D4; index_rules placeholder hazard with
+C-143 option B before D4; C-148 NOT_APPLICABLE question goes to the authors.
+```
+
 ## P5b–P10 — NOT STARTED
 
 ## Temporary exceptions

tests/unit/test_reachability_predicate.py

@@ -778,21 +778,24 @@ def test_row_seven_a_prefix_list(self) -> None:
             evaluate(swap_ingress('  prefix_list_ids = ["pl-1"]\n')), U, 7, R.RULE_INDETERMINATE
         )
 
-    def test_row_seven_an_unresolved_group_of_the_source(self) -> None:
+    def test_an_unresolved_group_of_the_source_with_no_path_is_row_four(self) -> None:
+        # P5b-fix (C-156): E3 comes first, so row 4 and not row 7 (was row 7 in P5b)
         text = VAR + edits(
             canonical(),
             (APP_TO_DB, ""),
             (APP_SGS_LINE, "  vpc_security_group_ids      = [aws_security_group.app.id, var.u]\n"),
         )
-        self.check(evaluate(text), U, 7, R.ATTRIBUTE_UNRESOLVED)
+        self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED)
 
-    def test_an_unresolved_group_does_not_spoil_a_pass_that_already_holds(self) -> None:
+    def test_an_unresolved_group_of_the_source_is_not_a_pass_even_when_the_path_holds(self) -> None:
+        # P5b-fix (C-156): superseded the P5b test that expected PASS, row 6; an unresolved entry
+        # leaves the check of the groups of S undecided (MIXED and RETAINED-INLINE), so row 4
         text = VAR + edit(
             canonical(),
             APP_SGS_LINE,
             "  vpc_security_group_ids      = [aws_security_group.app.id, var.u]\n",
         )
-        self.check(evaluate(text), P, 6, None)
+        self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED)
 
     def test_row_seven_comes_before_row_eight(self) -> None:
         both = ingress_5432("narrow", '  cidr_blocks = ["10.0.1.0/25"]\n') + ingress_5432(