P5b: Verification part 2 — INV-FUNC-001 reachability, P5 gate evidence

core/domain/verification.py

@@ -119,6 +119,17 @@ class VerificationReason(StrEnum):
     CONSISTENCY_FINDING = "consistency.finding"
     VERIFIER_NOT_AVAILABLE = "verifier.not_available"
     VERIFIER_ERROR = "verifier.error"
+    # INV-FUNC-001 (C-151, C-153)
+    PARAMETERS_INVALID = "parameters.invalid"
+    ENDPOINT_ABSENT = "endpoint.absent"
+    PORT_MISMATCH = "port.mismatch"
+    VPC_MISMATCH = "vpc.mismatch"
+    PATH_MISSING = "path.missing"
+    COVERAGE_PARTIAL = "coverage.partial"
+    ROUTE_UNSUPPORTED = "route.unsupported"
+    INTERFACE_UNSUPPORTED = "interface.unsupported"
+    VALUE_UNSUPPORTED = "value.unsupported"
+    MODEL_UNSUPPORTED = "model.unsupported"
 
 
 # --- helpers --------------------------------------------------------------------------------------

core/verification/__init__.py

@@ -4,12 +4,14 @@
 sufficiency and freshness, aggregation), registry-v1.0 §2-§5 (the predicates).
 Built in P5a (C-144 to C-150): the structural and consistency gate, the security predicates
 (INV-SEC-001, INV-SEC-002, INV-SEC-003), baseline verification of created resources and the engine.
-INV-FUNC-001 is built in P5b; until then it is UNSUPPORTED ``verifier.not_available``, never PASS.
+INV-FUNC-001 (reachability) is built in P5b (C-151 to C-154); a verifier pair that the dispatch
+table does not have is UNSUPPORTED ``verifier.not_available``, never PASS.
 
     values, views    the verifier's own reader of the stored security view (C-112, C-149)
     cidr, ports      interval-union coverage and the port logic of registry §2.5, §3.3
     retention        RETAINED-INLINE: the parent counterpart, through the identity report
     public_ingress   PIP(22) and PIP(5432)          rds_public_flag   INV-SEC-003
+    reachability     INV-FUNC-001, REACH(S, D, 5432)    func_view         its reader of the inputs
     structural       the mandatory STRUCTURAL and CONSISTENCY items (closed finding codes)
     baseline         the RESOURCE items P4 emits for created resources
     dispatch         the table from a definition's verifier id and version to a function

core/verification/baseline.py

@@ -9,8 +9,9 @@
   groups. The restriction only narrows what is reported; it never turns another group's FAIL into a
   PASS, which the invariant items still carry.
 * A created ``aws_db_instance`` runs INV-SEC-003 for that instance.
-* A created resource of a relevant-unsupported type (registry §2.7, the security-group list) is
-  UNSUPPORTED, even as a placeholder (R5).
+* A created resource of a relevant-unsupported type (registry §2.7: the 26 types of
+  INV-FUNC-001, which contain the three of the security list; C-154) is UNSUPPORTED, even as a
+  placeholder (R5).
 * A created placeholder (an unknown ``count`` or ``for_each``) is UNKNOWN.
 * Any other type is PASS with ``applicable = false`` and the assumption that the registry declares
   no baseline predicate for it. **This is a modelling assumption, not a proof** (C-148, flagged for
@@ -29,11 +30,12 @@
 from typing import Any, Final
 
 from core.domain.enums import ResourceSupport, VerificationResult
+from core.domain.registry_v1 import FUNC_RELEVANT_UNSUPPORTED
 from core.domain.resource import Resource
 from core.domain.verification import VerificationReason
 from core.verification.inputs import VerificationInputs
 from core.verification.outcome import CLAUSE_IPV4, CLAUSE_IPV6, combine
-from core.verification.public_ingress import RELEVANT_UNSUPPORTED, GroupStatus, analyse
+from core.verification.public_ingress import GroupStatus, analyse
 from core.verification.rds_public_flag import DB_INSTANCE_TYPE, instance_state
 from core.verification.views import (
     SECURITY_GROUP_RULE_TYPE,
@@ -146,7 +148,7 @@ def verify_baseline(address: str, inputs: VerificationInputs) -> BaselineOutcome
         return BaselineOutcome(
             S, R.INVARIANT_UNKNOWN, _base(resource), (), True, *BASELINE_VERIFIER
         )
-    if kind in RELEVANT_UNSUPPORTED:
+    if kind in FUNC_RELEVANT_UNSUPPORTED:
         return BaselineOutcome(S, R.TYPE_RELEVANT_UNSUPPORTED, _base(resource), (), True, *ids)
     if resource.support_status is ResourceSupport.UNKNOWN:
         return BaselineOutcome(U, R.RESOURCE_INDETERMINATE, _base(resource), (), True, *ids)

core/verification/cidr.py

@@ -69,3 +69,18 @@ def covers(cidrs: Iterable[str], target: str) -> bool:
         if cursor > wanted.last:
             return True
     return cursor > wanted.last
+
+
+def overlaps(cidrs: Iterable[str], target: str) -> bool:
+    """Whether some member shares at least one address with ``target`` (registry §6.4 row 8: a CIDR
+    that overlaps the target without covering it covers it "partly").
+
+    Same rules as ``covers``: one address family, an invalid member is an error, never ignored."""
+    wanted = parse_network(target)
+    found = False
+    for text in cidrs:
+        member = parse_network(text)
+        if member.version != wanted.version:
+            raise CidrError("an overlap question mixes IPv4 and IPv6")
+        found = found or (member.first <= wanted.last and member.last >= wanted.first)
+    return found

core/verification/dispatch.py

@@ -3,8 +3,8 @@
 The definition of an invariant names its verifier (``verifier_id``, ``verifier_version``, registry
 §10) and its parameters (``predicate.parameters``). The table maps that pair to a function
 ``(definition, inputs) -> PredicateOutcome``. A pair the table does not have is not an error of the
-engine: the item is UNSUPPORTED ``verifier.not_available``, never PASS. INV-FUNC-001 is such a pair
-until P5b adds its verifier.
+engine: the item is UNSUPPORTED ``verifier.not_available``, never PASS (P5a had no entry for
+INV-FUNC-001, so that was its answer; P5b registers ``dail.verify.reachability_cfg``).
 
 The table is data so that a test can inject a verifier that raises, or one that returns something
 that is not an outcome, and watch the engine fail closed.
@@ -23,13 +23,14 @@
 from core.verification.outcome import PredicateOutcome
 from core.verification.public_ingress import evaluate_public_ingress
 from core.verification.rds_public_flag import evaluate_rds_public_flag
+from core.verification.reachability import evaluate_reachability
 
 Verifier = Callable[[Invariant, VerificationInputs], PredicateOutcome]
 VerifierTable = Mapping[tuple[str, str], Verifier]
 
 PUBLIC_INGRESS: Final = ("dail.verify.public_ingress", "1")
 RDS_PUBLIC_FLAG: Final = ("dail.verify.rds_public_flag", "1")
-REACHABILITY_CFG: Final = ("dail.verify.reachability_cfg", "1")  # P5b; not in the table yet
+REACHABILITY_CFG: Final = ("dail.verify.reachability_cfg", "1")
 
 
 def _port(definition: Invariant) -> int:
@@ -59,5 +60,6 @@ def rds_public_flag(_definition: Invariant, inputs: VerificationInputs) -> Predi
     {
         PUBLIC_INGRESS: public_ingress,
         RDS_PUBLIC_FLAG: rds_public_flag,
+        REACHABILITY_CFG: evaluate_reachability,
     }
 )

core/verification/engine.py

@@ -15,8 +15,9 @@
 * Malformed inputs (``VerificationInputError``) stop the run before any item runs.
 * A construction status that is not OK makes every invariant and baseline item UNSUPPORTED
   ``construction.invalid``; no predicate runs (registry §2.8).
-* An invariant the definitions do not have is UNSUPPORTED ``invariant.unknown``; a verifier the
-  table does not have (INV-FUNC-001 until P5b) is UNSUPPORTED ``verifier.not_available``.
+* An invariant the definitions do not have is UNSUPPORTED ``invariant.unknown``; a verifier pair
+  the table does not have is UNSUPPORTED ``verifier.not_available`` (the table of P5b has the three
+  registry verifiers).
 
 ``verifier_invocations`` counts verifier executions: the predicates, the baseline checks and the two
 gates, including executions that raised. Items answered without running a verifier are not counted.