From 3cafed111456aa2f14cbc052dc7d7a9a5aee3abe Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 02:26:18 +0530 Subject: [PATCH 1/3] P5b-fix step 0: record the P5b review result (PHASE_GATES) Co-Authored-By: Claude Sonnet 5.5 --- docs/PHASE_GATES.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/docs/PHASE_GATES.md b/docs/PHASE_GATES.md index efb1ac4..a81bf40 100644 --- a/docs/PHASE_GATES.md +++ b/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 From 8bb5029054c9310fde31f779d354f3fdbc66baf2 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 02:38:44 +0530 Subject: [PATCH 2/3] =?UTF-8?q?P5b-fix=20step=201-2:=20an=20unresolved=20e?= =?UTF-8?q?ntry=20of=20vpc=5Fsecurity=5Fgroup=5Fids=20is=20row=204;=20the?= =?UTF-8?q?=20engine=20is=20compared=20exactly=20(registry=20=C2=A76.3=20E?= =?UTF-8?q?2,=20E3;=20=C2=A76.4=20row=204;=20C-156)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 21 new tests were written and shown failing first (12 of 19 failed on the old code: the reviewer's reproductions on D and on S, a placeholder group, the path not established, the engine casing). The fix adds the side-level unresolved reasons to the row 4 reasons when a side is read, and compares the engine with the exact string "postgres". Two P5b tests asserted the superseded results for an unresolved entry of S (PASS row 6; row 7 with no path); they now assert UNKNOWN, row 4 (C-156 rule 2). Co-Authored-By: Claude Sonnet 5.5 --- core/verification/reachability.py | 6 +- tests/unit/test_reachability_predicate.py | 11 +- .../test_reachability_unresolved_groups.py | 245 ++++++++++++++++++ 3 files changed, 256 insertions(+), 6 deletions(-) create mode 100644 tests/unit/test_reachability_unresolved_groups.py diff --git a/core/verification/reachability.py b/core/verification/reachability.py index 7f7e634..e5b017b 100644 --- a/core/verification/reachability.py +++ b/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 ----------------------------------------------------------------------------- diff --git a/tests/unit/test_reachability_predicate.py b/tests/unit/test_reachability_predicate.py index 8d253fd..032a145 100644 --- a/tests/unit/test_reachability_predicate.py +++ b/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( diff --git a/tests/unit/test_reachability_unresolved_groups.py b/tests/unit/test_reachability_unresolved_groups.py new file mode 100644 index 0000000..ab451b3 --- /dev/null +++ b/tests/unit/test_reachability_unresolved_groups.py @@ -0,0 +1,245 @@ +"""INV-FUNC-001: an unresolved entry of vpc_security_group_ids (P5b-fix step 1; registry §6.3, §6.4; +C-155 item 7, C-156). + +Every expected value is derived by hand from the registry text on the canonical topology (see the +derivation in ``test_reachability_vectors.py``), not from the code under test. + +* E3: "each entry references a configured aws_security_group with a resolved vpc_id". An entry of + ``D.vpc_security_group_ids`` that is unresolved (a variable without a value, or a group whose + ``count`` is unknown) leaves E3 unresolved: row 4, UNKNOWN. Rows 1 to 3 come first, row 2 causes + win over row 4, and row 4 comes before rows 5 to 9, so the result is UNKNOWN whether or not the + path is otherwise established (a path built from the known groups is not a PASS, and a missing + path is not a FAIL). +* The registry says nothing about an unresolved entry of ``S.vpc_security_group_ids``. C-156 reads + it the same way (row 4): whether that group is MIXED or RETAINED-INLINE (row 2) cannot be + checked. C-155 item 13 records that the authors may relax it to PASS in registry v1.1. +* A literal AWS id stays UNSUPPORTED (C-155 item 7), and the engine is compared with the exact + string ``"postgres"`` of E2. +""" + +from __future__ import annotations + +import dataclasses +import unittest + +from core.domain.enums import VerificationResult +from core.domain.jsonvalue import thaw_json +from core.domain.resource import Resource +from core.domain.verification import VerificationReason +from core.verification.outcome import PredicateOutcome +from core.verification.reachability import evaluate_reachability +from tests.func_builders import ( + APP_SGS_LINE, + APP_TO_DB, + DB_SGS_LINE, + IGW_ROUTE, + attribute, + canonical, + edit, + edits, + with_attributes, +) +from tests.reach_builders import definition, evaluate, inputs + +P, F, U, S = ( + VerificationResult.PASS, + VerificationResult.FAIL, + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, +) +R = VerificationReason +VAR = 'variable "u" {}\n' +INTRA_ROUTE = ' route {\n cidr_block = "10.0.2.0/24"\n nat_gateway_id = "nat-1"\n }\n' + +# the group lines, with the text that stands for one more entry in the list +DB_LIST = "[aws_security_group.db.id, {}]" +APP_LIST = "[aws_security_group.app.id, {}]" +PLACEHOLDER = ( + '\nresource "aws_security_group" "extra" {\n count = var.u\n name = "extra"\n' + ' description = "unknown count"\n vpc_id = aws_vpc.main.id\n}\n' +) +RESOLVED = ( + '\nresource "aws_security_group" "extra" {\n name = "extra"\n' + ' description = "an extra group"\n vpc_id = aws_vpc.main.id\n' + " ingress = []\n egress = []\n}\n" +) + + +def sgs(value: str) -> str: + return f" vpc_security_group_ids = {value}\n" + + +def on_db(value: str, text: str | None = None) -> str: + return edit(text or canonical(), DB_SGS_LINE, sgs(value)) + + +def on_app(value: str, text: str | None = None) -> str: + return edit(text or canonical(), APP_SGS_LINE, sgs(value)) + + +class Check(unittest.TestCase): + def check( + self, + outcome: PredicateOutcome, + result: VerificationResult, + row: int, + reason: VerificationReason | None, + ) -> None: + self.assertEqual( + (outcome.result, outcome.observations["row"], outcome.reason), + (result, row, reason), + outcome.observations, + ) + + +class TestUnresolvedEntryOfD(Check): + def test_a_variable_among_the_entries(self) -> None: + text = VAR + on_db(DB_LIST.format("var.u")) + outcome = evaluate(text) + self.check(outcome, U, 4, R.ATTRIBUTE_UNRESOLVED) + self.assertTrue(outcome.observations["unresolved"]) + + def test_a_concat_with_a_variable(self) -> None: + text = VAR + on_db("concat([aws_security_group.db.id], [var.u])") + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_the_whole_list_unresolved_stays_row_four(self) -> None: + self.check(evaluate(VAR + on_db("var.u")), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_a_placeholder_group_among_the_entries(self) -> None: + text = VAR + on_db(DB_LIST.format("aws_security_group.extra[0].id")) + PLACEHOLDER + outcome = evaluate(text) + self.check(outcome, U, 4, R.ATTRIBUTE_UNRESOLVED) + self.assertTrue(outcome.observations["unresolved"]) + + def test_the_path_not_established_is_still_unknown_never_a_fail(self) -> None: + # without the ingress rule row 9 would say FAIL; E3 is unresolved, so row 4 comes first + text = VAR + on_db(DB_LIST.format("var.u"), edit(canonical(), APP_TO_DB, "")) + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_a_resolved_extra_group_changes_nothing(self) -> None: + text = on_db(DB_LIST.format("aws_security_group.extra.id")) + RESOLVED + self.check(evaluate(text), P, 6, None) + + def test_a_literal_group_id_is_unsupported(self) -> None: + text = on_db(DB_LIST.format('"sg-0123456789abcdef0"')) + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + def test_rows_one_to_three_and_row_two_come_before_row_four(self) -> None: + unresolved = VAR + on_db(DB_LIST.format("var.u")) + self.check(evaluate(edit(unresolved, '"postgres"', '"mysql"')), F, 3, R.PORT_MISMATCH) + self.check( + evaluate(edit(unresolved, IGW_ROUTE, IGW_ROUTE + INTRA_ROUTE)), + S, + 2, + R.ROUTE_UNSUPPORTED, + ) + self.check( + evaluate( + unresolved.replace('resource "aws_db_instance" "database"', 'resource "x" "y"') + ), + F, + 1, + R.ENDPOINT_ABSENT, + ) + + def test_row_four_comes_before_rows_five_to_nine(self) -> None: + far = ( + '\nresource "aws_vpc" "other" {\n cidr_block = "10.1.0.0/16"\n}\n' + '\nresource "aws_subnet" "far" {\n vpc_id = aws_vpc.other.id\n' + ' cidr_block = "10.1.1.0/24"\n}\n' + ) + text = edits( + canonical(), + ( + " subnet_id = aws_subnet.app.id\n", + " subnet_id = aws_subnet.far.id\n", + ), + (DB_SGS_LINE, sgs(DB_LIST.format("var.u"))), + ) + self.check(evaluate(VAR + text + far), U, 4, R.ATTRIBUTE_UNRESOLVED) + + +class TestUnresolvedEntryOfS(Check): + """C-156 rule 2: the registry is silent; the conservative reading is row 4.""" + + def test_a_variable_among_the_entries(self) -> None: + outcome = evaluate(VAR + on_app(APP_LIST.format("var.u"))) + self.check(outcome, U, 4, R.ATTRIBUTE_UNRESOLVED) + self.assertTrue(outcome.observations["unresolved"]) + + def test_a_concat_with_a_variable(self) -> None: + text = VAR + on_app("concat([aws_security_group.app.id], [var.u])") + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_the_whole_list_unresolved_stays_row_four(self) -> None: + self.check(evaluate(VAR + on_app("var.u")), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_a_placeholder_group_among_the_entries(self) -> None: + text = VAR + on_app(APP_LIST.format("aws_security_group.extra[0].id")) + PLACEHOLDER + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_the_path_not_established_is_still_unknown_never_a_fail(self) -> None: + text = VAR + on_app(APP_LIST.format("var.u"), edit(canonical(), APP_TO_DB, "")) + self.check(evaluate(text), U, 4, R.ATTRIBUTE_UNRESOLVED) + + def test_a_resolved_extra_group_changes_nothing(self) -> None: + text = on_app(APP_LIST.format("aws_security_group.extra.id")) + RESOLVED + self.check(evaluate(text), P, 6, None) + + def test_a_literal_group_id_is_unsupported(self) -> None: + text = on_app(APP_LIST.format('"sg-0123456789abcdef0"')) + self.check(evaluate(text), S, 2, R.MODEL_UNSUPPORTED) + + +class TestAReferenceToAPlaceholderGroup(Check): + """A reference that names a group of unknown ``count`` cannot come from the text (the evaluator + gives an unknown value for it), so the stored view is damaged by hand: the entry is a ``Ref`` + to the placeholder. E3 is unresolved all the same (row 4).""" + + def check_entry(self, owner: str, own: str) -> None: + base = inputs(VAR + canonical() + PLACEHOLDER) + placeholder = {"$dail": "ref", "address": "aws_security_group.extra", "attribute": "id"} + known = {"$dail": "ref", "address": f"aws_security_group.{own}", "attribute": "id"} + + def damage(resource: Resource) -> Resource: + attributes = thaw_json(resource.attributes) + attributes["vpc_security_group_ids"] = attribute([known, placeholder]) + return with_attributes(resource, attributes) + + found = [damage(r) if r.address == owner else r for r in base.candidate_resources] + given = dataclasses.replace(base, candidate_resources=tuple(found)) + outcome = evaluate_reachability(definition(given), given) + self.check(outcome, U, 4, R.ATTRIBUTE_UNRESOLVED) + self.assertTrue(any("placeholder" in line for line in outcome.observations["unresolved"])) + + def test_an_entry_of_d(self) -> None: + self.check_entry("aws_db_instance.database", "db") + + def test_an_entry_of_s(self) -> None: + self.check_entry("aws_instance.app", "app") + + +class TestTheEngineIsComparedExactly(Check): + """Registry E2: ``engine == "postgres"``, the exact string.""" + + def test_the_exact_string_is_a_pass(self) -> None: + self.check(evaluate(canonical()), P, 6, None) + + def test_another_casing_is_not_postgres(self) -> None: + for spelling in ("Postgres", "POSTGRES", "PostgreS"): + with self.subTest(engine=spelling): + text = edit(canonical(), '"postgres"', f'"{spelling}"') + self.check(evaluate(text), F, 3, R.PORT_MISMATCH) + + def test_a_port_still_wins_over_the_engine(self) -> None: + text = edit( + canonical(), + ' engine = "postgres"', + ' engine = "Postgres"\n port = 5432', + ) + self.check(evaluate(text), P, 6, None) + + +if __name__ == "__main__": + unittest.main() From f807dee064896e1381fbda25cc522a660d0e70d4 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 02:38:44 +0530 Subject: [PATCH 3/3] =?UTF-8?q?P5b-fix=20step=204:=20register=20row=20C-15?= =?UTF-8?q?6=20(Proposed)=20and=20item=2013=20of=20C-155=20(registry=20?= =?UTF-8?q?=C2=A76.3,=20=C2=A76.4;=20C-155,=20C-156)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 5.5 --- docs/DECISIONS_REGISTER.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index ebcd64a..f62079a 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/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:` 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) |