diff --git a/core/domain/identity.py b/core/domain/identity.py index 5780ac6..e496d3a 100644 --- a/core/domain/identity.py +++ b/core/domain/identity.py @@ -19,6 +19,10 @@ | DELETED | set | null | DIFFERENT | null | | UNCERTAIN | either, not both null | | UNCERTAIN | LOW | +``moved`` (C-177, "every resource move counts as a change"): true exactly when both refs are set +and differ, i.e. a ``moved`` block or Terraform's implicit ``count`` move made the pair. A moved +pair is never UNCHANGED. The constructor refuses a flag that disagrees with the refs. + ``IdentityReport`` is frozen. Its ``content_hash`` covers everything except ``report_id`` and ``created_at`` (C-33 helpers), so two runs over the same inputs can be compared by hash; the constructor recomputes it (``HashMismatchError``). It also rejects a summary that is not the one @@ -261,6 +265,7 @@ class IdentityMatch: change_type: ChangeType confidence: IdentityConfidence | None rationale: Mapping[str, Any] + moved: bool = False def __post_init__(self) -> None: trusted = _require_ref(self.trusted_resource_ref, "IdentityMatch.trusted_resource_ref") @@ -272,8 +277,25 @@ def __post_init__(self) -> None: if self.confidence is not None: require_enum(self.confidence, IdentityConfidence, "IdentityMatch.confidence") self._check_combination(trusted, candidate) + self._check_moved(trusted, candidate) object.__setattr__(self, "rationale", self._canonical_rationale(self.rationale)) + def _check_moved(self, trusted: str | None, candidate: str | None) -> None: + """C-177: the flag says exactly whether the pair crosses two addresses, and a pair that a + move made is never UNCHANGED.""" + if not isinstance(self.moved, bool): + raise DomainValidationError("IdentityMatch.moved: must be a boolean") + across = trusted is not None and candidate is not None and trusted != candidate + if self.moved != across: + raise DomainValidationError( + f"IdentityMatch: moved is {self.moved} for refs {trusted!r} and {candidate!r}; it " + "is true exactly for a pair across two addresses (C-177)" + ) + if self.moved and self.change_type is ChangeType.UNCHANGED: + raise DomainValidationError( + "IdentityMatch: a moved pair is never UNCHANGED; every move is a change (C-177)" + ) + def _check_combination(self, trusted: str | None, candidate: str | None) -> None: change = self.change_type status = self.identity_status @@ -344,8 +366,16 @@ def create( change_type: ChangeType, rule: EvidenceType, evidence_ids: Iterable[str], + moved: bool | None = None, ) -> IdentityMatch: - """A match whose status and confidence follow from the change type (C-122).""" + """A match whose status and confidence follow from the change type (C-122). ``moved`` is + derived from the refs when it is not given (C-177); a value that disagrees is refused.""" + if moved is None: + moved = ( + trusted_ref is not None + and candidate_ref is not None + and trusted_ref != candidate_ref + ) if change_type in _PAIR_CHANGES: status, confidence = IdentityStatus.SAME, IdentityConfidence.HIGH elif change_type is ChangeType.UNCERTAIN: @@ -359,6 +389,7 @@ def create( change_type=change_type, confidence=confidence, rationale={"rule": rule.value, "evidence_ids": sorted(set(evidence_ids))}, + moved=moved, ) @property @@ -384,6 +415,7 @@ def to_dict(self) -> dict[str, Any]: "change_type": self.change_type.value, "confidence": None if self.confidence is None else self.confidence.value, "rationale": thaw_json(self.rationale), + "moved": self.moved, } @classmethod @@ -397,6 +429,7 @@ def from_dict(cls, data: Mapping[str, Any]) -> IdentityMatch: "change_type", "confidence", "rationale", + "moved", ), "IdentityMatch", ) @@ -414,6 +447,7 @@ def from_dict(cls, data: Mapping[str, Any]) -> IdentityMatch: else parse_enum(raw_confidence, IdentityConfidence, "IdentityMatch.confidence") ), rationale=fields["rationale"], + moved=fields["moved"], ) diff --git a/core/domain/impact.py b/core/domain/impact.py index b98a55f..dc1d2bd 100644 --- a/core/domain/impact.py +++ b/core/domain/impact.py @@ -166,6 +166,7 @@ class ChangeFlag(StrEnum): UNRESOLVED_CONTENT = "UNRESOLVED_CONTENT" UNSUPPORTED_TYPE = "UNSUPPORTED_TYPE" + MOVED = "MOVED" # a pair that a move made: the change reason "moved" (C-177) # --- helpers -------------------------------------------------------------------------------------- @@ -251,6 +252,14 @@ def __post_init__(self) -> None: flags = tuple(require_enum(f, ChangeFlag, "ChangedResource.flags") for f in self.flags) if list(flags) != sorted(set(flags)): raise DomainValidationError("ChangedResource.flags: must be sorted and unique") + if ChangeFlag.MOVED in flags and ( + self.trusted_ref is None + or self.candidate_ref is None + or self.trusted_ref == self.candidate_ref + ): + raise DomainValidationError( + "ChangedResource.flags: MOVED needs a pair across two addresses (C-177)" + ) object.__setattr__(self, "flags", flags) def refs(self) -> tuple[str, ...]: diff --git a/core/domain/registry_v1_1.py b/core/domain/registry_v1_1.py new file mode 100644 index 0000000..02fb775 --- /dev/null +++ b/core/domain/registry_v1_1.py @@ -0,0 +1,57 @@ +"""The four registry-v1.1 invariants as data (P6d; registry v1.1 §1.4, §3, §4, §10; C-178 to C-181). + +Registry v1.1 changes the ``possible`` clause of §3.3, so INV-SEC-001 and INV-SEC-002 are version 2; +INV-SEC-003 and INV-FUNC-001 are unchanged at version 1. ``registry_v1_1_invariants`` therefore +takes the v1.0 definitions of ``registry_v1`` and: + +* for INV-SEC-001 and INV-SEC-002 sets ``version = 2`` and cites ``registry-v1.1`` in + ``predicate.registry`` and in the description; scope, verifier id and verifier version stay as + they are (registry §10 is unchanged, C-180); +* keeps INV-SEC-003 and INV-FUNC-001 exactly as v1.0 builds them, so their ``definition_hash`` is + the one already stored for that id and version (C-181 (1)). + +``registry_v1`` is not changed: it still builds the v1.0 definitions, which the TerraPreserve v1.0 +labels and the existing fixtures cite. The verifier reads ``predicate.registry`` to choose the +§3.3 clause (``core.verification.dispatch``). + +DAIL stores registry v1.1 as the integer ``invariant_registry_version`` 2 (C-180, the user's +decision of 11 Nov 2026; the field is an integer, C-32): ``REGISTRY_VERSION_V1_1``. +""" + +from __future__ import annotations + +from dataclasses import replace +from datetime import datetime +from typing import Final + +from core.domain.invariant import Invariant +from core.domain.jsonvalue import thaw_json +from core.domain.registry_v1 import REGISTRY_TAG, registry_v1_invariants + +REGISTRY_TAG_V1_0: Final = REGISTRY_TAG +REGISTRY_TAG_V1_1: Final = "registry-v1.1" +REGISTRY_VERSION_V1_0: Final = 1 +REGISTRY_VERSION_V1_1: Final = 2 +# Registry v1.1 §1.4: the invariants whose version changes, and their new version. +_BUMPED: Final = {"INV-SEC-001": 2, "INV-SEC-002": 2} + + +def _bumped(definition: Invariant, version: int) -> Invariant: + predicate = thaw_json(definition.predicate) + predicate["registry"] = REGISTRY_TAG_V1_1 + return replace( + definition, + version=version, + predicate=predicate, + description=definition.description.replace(REGISTRY_TAG_V1_0, REGISTRY_TAG_V1_1), + ) + + +def registry_v1_1_invariants( + now: datetime, *, source: str, destination: str +) -> tuple[Invariant, ...]: + """The four ``registry-v1.1`` invariant definitions, sorted by id (bindings as in v1.0).""" + definitions = registry_v1_invariants(now, source=source, destination=destination) + return tuple( + _bumped(d, _BUMPED[d.invariant_id]) if d.invariant_id in _BUMPED else d for d in definitions + ) diff --git a/core/identity/findings.py b/core/identity/findings.py index ae10f84..8d7f73a 100644 --- a/core/identity/findings.py +++ b/core/identity/findings.py @@ -67,6 +67,16 @@ def match(self) -> IdentityMatch: change_type=self.change, rule=self.rule, evidence_ids=[item.evidence_id for item in self.evidence], + moved=self.moved, + ) + + @property + def moved(self) -> bool: + """A pair across two addresses: only a move can make one (C-177).""" + return ( + self.trusted_ref is not None + and self.candidate_ref is not None + and self.trusted_ref != self.candidate_ref ) diff --git a/core/identity/strategy.py b/core/identity/strategy.py index 627c88e..b7c6e1b 100644 --- a/core/identity/strategy.py +++ b/core/identity/strategy.py @@ -18,6 +18,9 @@ 5. **AMB-1**: unpaired instances of one block that cannot be told apart are all UNCERTAIN. 6. The leftovers: unpaired trusted is DELETED, unpaired candidate CREATED. 7. A pair is UNCHANGED (equal fingerprints) or MODIFIED; **RT-1** may make it REPLACED or UNCERTAIN. + A pair that a move made is never UNCHANGED (C-177, "every resource move counts as a change"): + with equal fingerprints it is MODIFIED, decided by the move evidence, and the match is + ``moved``. ``UNSUPPORTED_TYPE`` and ``UNRESOLVED_CONTENT`` are flags, not identity evidence: they are attached by both strategies, so the two differ only in identity decisions. @@ -411,10 +414,13 @@ def classify(self, trusted: Resource, candidate: Resource) -> Draft: observed = {"trusted": trusted.fingerprint, "candidate": candidate.fingerprint} if trusted.fingerprint == candidate.fingerprint: change, rule = ChangeType.UNCHANGED, EvidenceType.FINGERPRINT_EQUAL + if steps: + # C-177: every resource move counts as a change; the move evidence decides + change, rule = ChangeType.MODIFIED, via.evidence_type fingerprint = self.ev.about( trusted, candidate, - rule, + EvidenceType.FINGERPRINT_EQUAL, EvidenceSource.BOTH, observed, "The canonical content of the paired resources is identical.", diff --git a/core/impact/changes.py b/core/impact/changes.py index 215165c..cd0fd2b 100644 --- a/core/impact/changes.py +++ b/core/impact/changes.py @@ -1,12 +1,13 @@ """The changed set (Doc 08 §6; registry §2.7, §2.9; C-117; C-140 item 1, C-143). Every identity match that is not UNCHANGED is a change source, with its change type and the flags -the identity evidence carries (``UNRESOLVED_CONTENT``, ``UNSUPPORTED_TYPE``). An UNCHANGED match is -**also** a change source when the resource carries unresolved content: equal fingerprints do not -prove an unresolved element unchanged (registry §2.9 treats "unresolved on both sides" as changed; -C-117). Such a source is carried with change type UNCERTAIN and the flag ``UNRESOLVED_CONTENT``, and -the engine uses it only for invariants whose footprint contains the resource. It can only add -UNCERTAIN; it never removes anything. +the identity evidence carries (``UNRESOLVED_CONTENT``, ``UNSUPPORTED_TYPE``). A pair that a move +made is never UNCHANGED (C-177) and carries the flag ``MOVED``, the change reason "moved". An +UNCHANGED match is **also** a change source when the resource carries unresolved content: equal +fingerprints do not prove an unresolved element unchanged (registry §2.9 treats "unresolved on +both sides" as changed; C-117). Such a source is carried with change type UNCERTAIN and the flag +``UNRESOLVED_CONTENT``, and the engine uses it only for invariants whose footprint contains the +resource. It can only add UNCERTAIN; it never removes anything. What counts as unresolved content (C-143, option A): an Unknown or Unsupported canonical value in the resource, a security-group direction in the form ``unresolved``, ``dynamic`` or ``mixed``, @@ -108,6 +109,8 @@ def _flags(identity: IdentityReport, match: IdentityMatch) -> tuple[ChangeFlag, for e in identity.evidence_for(match) if e.evidence_type in _FLAG_OF } + if match.moved: + found.add(ChangeFlag.MOVED) return tuple(sorted(found)) diff --git a/core/impact/engine.py b/core/impact/engine.py index 097c972..575baac 100644 --- a/core/impact/engine.py +++ b/core/impact/engine.py @@ -298,7 +298,8 @@ def _work_item(invariant: Invariant, impacted: ImpactedInvariant) -> Verificatio reason=strongest, scope=tuple(scope or sorted(invariant.scope.resource_types)), required_evidence=( - f"L1 {invariant.verifier_id} {invariant.verifier_version} (registry-v1.0)" + f"L1 {invariant.verifier_id} {invariant.verifier_version} " + f"({invariant.predicate.get('registry', 'registry-v1.0')})" ), priority=WorkPriority.BLOCKING, ) diff --git a/core/verification/dispatch.py b/core/verification/dispatch.py index ea936f4..b4567c6 100644 --- a/core/verification/dispatch.py +++ b/core/verification/dispatch.py @@ -21,7 +21,7 @@ from core.domain.invariant import Invariant from core.verification.inputs import VerificationInputs from core.verification.outcome import PredicateOutcome -from core.verification.public_ingress import evaluate_public_ingress +from core.verification.public_ingress import REGISTRIES, evaluate_public_ingress from core.verification.rds_public_flag import evaluate_rds_public_flag from core.verification.reachability import evaluate_reachability @@ -41,13 +41,23 @@ def _port(definition: Invariant) -> int: return port +def registry_of(definition: Invariant) -> str: + """The registry tag the definition cites (``predicate.registry``); it selects the §3.3 text + of ``PIP(p)`` (C-181 (2)). A tag the verifier does not know raises: VERIFIER_ERROR.""" + registry = definition.predicate.get("registry") + if not isinstance(registry, str) or registry not in REGISTRIES: + raise ValueError(f"{definition.invariant_id}: unknown registry {registry!r}") + return registry + + def public_ingress(definition: Invariant, inputs: VerificationInputs) -> PredicateOutcome: - """INV-SEC-001 and INV-SEC-002: ``PIP(p)`` with ``p`` from the definition.""" + """INV-SEC-001 and INV-SEC-002: ``PIP(p)`` with ``p`` and the registry from the definition.""" return evaluate_public_ingress( _port(definition), inputs.candidate_resources, parent_resources=inputs.parent_resources, identity=inputs.identity, + registry=registry_of(definition), ) diff --git a/core/verification/engine.py b/core/verification/engine.py index b5b0e77..a0d786c 100644 --- a/core/verification/engine.py +++ b/core/verification/engine.py @@ -316,7 +316,8 @@ def _predicate_text(plan: _Plan) -> str: return plan.target_id predicate = plan.definition.predicate parameters = thaw_json(predicate.get("parameters", {})) - return f"registry-v1.0 {predicate.get('section', '')} {canonical_json(parameters)}" + registry = predicate.get("registry", "registry-v1.0") # C-181 (4): the definition's tag + return f"{registry} {predicate.get('section', '')} {canonical_json(parameters)}" def _evidence( diff --git a/core/verification/public_ingress.py b/core/verification/public_ingress.py index d48b4b0..3ae597e 100644 --- a/core/verification/public_ingress.py +++ b/core/verification/public_ingress.py @@ -5,8 +5,14 @@ D(g) = ingress rules of g that are determinate and permit TCP/p IPv4 violates4(g) := the union of their IPv4 sources covers 0.0.0.0/0 IPv6 violates6(g) := the union of their IPv6 sources covers ::/0 - possible4(g) := an indeterminate ingress rule could permit TCP/p and its IPv4 sources are - unresolved or include a prefix list (possible6 likewise for IPv6) + possible4(g) := an indeterminate ingress rule could permit TCP/p and (its IPv4 sources are + unresolved or include a prefix list, or its resolved IPv4 sources together + with those of D(g) cover 0.0.0.0/0) (possible6 likewise for IPv6 and ::/0) + +The last alternative is registry v1.1 (C-178, which closes C-150); INV-SEC-001 and INV-SEC-002 +version 2 cite it. Version 1 cites registry v1.0, which has only the first two alternatives: the +definition's ``predicate.registry`` chooses (``core.verification.dispatch``, C-181 (2)), and the +default is v1.1, the cautious one. Each clause is decided in this order (registry §3.4), per address family: @@ -34,10 +40,9 @@ * An unresolved egress direction matters only through MIXED: with a rule resource targeting the group it cannot be decided and the group is treated as MIXED (UNSUPPORTED). -Registry §3.3 has one consequence the authors should know about (Open row C-150): a rule whose -protocol or port is unresolved but whose IPv4 source is known, such as 0.0.0.0/0, is not -``possible`` by the text, so it gives PASS. It is implemented as written and reported in -``indeterminate_rules``. +Under registry v1.0 a rule whose protocol or port is unresolved but whose IPv4 source is known, +such as 0.0.0.0/0, is not ``possible``, so it gives PASS (C-150); under v1.1 it gives UNKNOWN. In +both it is reported in ``indeterminate_rules``. Standard library and ``core.domain`` only. """ @@ -50,6 +55,7 @@ from core.domain.enums import VerificationResult from core.domain.identity import IdentityReport +from core.domain.registry_v1_1 import REGISTRY_TAG_V1_0, REGISTRY_TAG_V1_1 from core.domain.resource import Resource from core.domain.verification import VerificationReason from core.verification.cidr import IPV4_ANY, IPV6_ANY, covers @@ -78,6 +84,7 @@ "v1: coverage split across groups is not detected (S6)", ) TOLERATED_ASSUMPTION: Final = "tolerated type: aws_db_subnet_group (C-15)" +REGISTRIES: Final = (REGISTRY_TAG_V1_0, REGISTRY_TAG_V1_1) P, F, U, S = ( VerificationResult.PASS, @@ -122,14 +129,26 @@ class Analysis: outcome: PredicateOutcome -def _could_expose(rule: Rule, port: int, family: tuple[str, str, str, str]) -> bool: - """``possible`` for one indeterminate rule and one address family (registry §3.3).""" +def _could_expose( + rule: Rule, + port: int, + family: tuple[str, str, str, str], + decided: Sequence[str], + registry: str, +) -> bool: + """``possible`` for one indeterminate rule and one address family (registry §3.3). + + ``decided`` is the union of the family's sources over ``D(g)``; only v1.1 reads it. + """ if not may_permit_tcp(rule.protocol, rule.from_port, rule.to_port, port): return False - _, _, sources, unresolved = family + _, wanted, sources, unresolved = family if getattr(rule, unresolved) or rule.prefix_list_ids: return True - return rule.direction is None and bool(getattr(rule, sources)) + known = list(getattr(rule, sources)) + if rule.direction is None and known: # C-146 (2): wider than the registry text, kept + return True + return registry == REGISTRY_TAG_V1_1 and covers([*decided, *known], wanted) def _violation( @@ -155,6 +174,7 @@ def _group_status( view: GroupView, port: int, retention: VerificationReason | None, + registry: str, ) -> tuple[GroupStatus, bool]: """The status of one group, and whether it is MIXED.""" ingress_like = (*view.ingress, *view.unresolved_direction) @@ -192,7 +212,7 @@ def _group_status( elif reasons: clauses[name] = S elif blocks_unexpandable or any( - _could_expose(rule, port, family) for rule in indeterminate + _could_expose(rule, port, family, union, registry) for rule in indeterminate ): clauses[name] = U else: @@ -225,8 +245,12 @@ def analyse( *, parent_resources: Iterable[Resource] | None = None, identity: IdentityReport | None = None, + registry: str = REGISTRY_TAG_V1_1, ) -> Analysis: - """Evaluate ``PIP(port)`` for a candidate (``parent_resources`` is ``None`` for a baseline).""" + """Evaluate ``PIP(port)`` for a candidate (``parent_resources`` is ``None`` for a baseline) + under the §3.3 text of ``registry`` (``registry-v1.0`` or ``registry-v1.1``).""" + if registry not in REGISTRIES: + raise ValueError(f"public ingress: unknown registry {registry!r}") candidate = list(resources) config = read_security(candidate) parent = None if parent_resources is None else {r.address: r for r in parent_resources} @@ -245,7 +269,7 @@ def analyse( retention = None if view.forms is not None and view.forms["ingress"] == "absent": retention = ingress_retention(address, parent=parent, identity=identity) - status, mixed = _group_status(address, view, port, retention) + status, mixed = _group_status(address, view, port, retention, registry) statuses[address] = status if mixed: mixed_groups.append(address) @@ -330,12 +354,16 @@ def evaluate_public_ingress( *, parent_resources: Iterable[Resource] | None = None, identity: IdentityReport | None = None, + registry: str = REGISTRY_TAG_V1_1, ) -> PredicateOutcome: - """``PIP(port)``: INV-SEC-001 for 22, INV-SEC-002 for 5432.""" - return analyse(port, resources, parent_resources=parent_resources, identity=identity).outcome + """``PIP(port)``: INV-SEC-001 for 22, INV-SEC-002 for 5432, under ``registry``'s §3.3.""" + return analyse( + port, resources, parent_resources=parent_resources, identity=identity, registry=registry + ).outcome __all__ = [ + "REGISTRIES", "RELEVANT_UNSUPPORTED", "Analysis", "GroupStatus", diff --git a/docs/BUILD_SEQUENCE.md b/docs/BUILD_SEQUENCE.md index edb8d31..baba9c3 100644 --- a/docs/BUILD_SEQUENCE.md +++ b/docs/BUILD_SEQUENCE.md @@ -23,16 +23,19 @@ The build is split into 18 work packages (N-06 in `DECISIONS_REGISTER.md`). Ever | 13 | Nov 4–5 | P6a promotion decision | | 14 | Nov 6–9 | P6b promotion commit (done) | | 14b | Nov 6–9 | P6c orchestrator, baseline flow, fixed-patch loop → P6 gate, M3 | +| 14c | Nov 11–13 | P6d every move is a change (C-177) and invariant registry v1.1 (C-178 to C-181; INV-SEC-001/002 version 2), inserted after P6c and before P7a; ends with a PR for external review, after which the user tags `registry-v1.1` | | 15 | Nov 10–13 | D3 real-world pool | | 16 | Nov 14–20 | D4 scenario generator | | 17 | Nov 21–28 | D5 oracle labels + calibration (free route, N-08) | | 18 | Nov 29–30 | D6 freeze TerraPreserve v1.0 | | 19 | Dec 1–2 | P7a LLM adapter (fake provider, Ollama) | | 20 | Dec 3–6 | P7b patch validation → P7 gate, M4 | -| 21 | Dec 7–11 | P9 AWS integration (free route) → M6 | +| 21 | — | ~~P9 AWS integration (free route) → M6~~ removed by C-71 (advisor, 11 Nov 2026): AWS stays fully offline, no deployment, no AWS account, no live calibration; milestone M6 (AWS Demonstration) is removed | | 22 | Dec 12–14 | P8a experiment harness | | 23 | Dec 15–18 | P8b metrics and reports → P8 gate, M5 | | 24–28 | Dec 19–Jan 2 | P10 hardening, protocol freeze + pilot, LLM patch generation, main run, QA report | | 29 | Jan 3–4 | TerraPreserve v1.1 (real LLM patches) | Critical path: P1a → P6b. + +C-71 (advisor, 11 Nov 2026): the free-of-cost route. LLMs are free open-weight models (local Ollama for wiring checks; free Kaggle or Colab GPUs for the experiment), each pinned by exact digest, quantization, temperature and seed, licence checked; no paid LLM API. AWS stays fully offline, so P9 and M6 are removed. diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index b030bf4..764f4cb 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -82,7 +82,7 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-68 | Evidence subject identity | VERIFICATION evidence carries `invariant_id` and `invariant_version`. Supersession requires equal subject and equal `verifier_id`. Registry §2.10. P5 implements it. | Accepted 4 Oct 2026 (step 4); implementation in P5 | | C-69 | F3/F7 redesign (resolves N-03) | Route edits stay safe cases. F3 unsafe: move EC2 outside a CIDR-based RDS ingress rule, or edit its subnet's CIDR, or move it to a second VPC. F7 unsafe: edit a shared hub security group. The controlled tier records `rds_ingress_mode` (SG_REF or CIDR). The generator never adds non-local routes inside the VPC CIDR. Corrects N-03's premise: the local route cannot be deleted, but its target can be replaced. D0 amendments A1. | Accepted 4 Oct 2026 (step 4); paper text pending advisor | | C-70 | Impact ground truth (resolves N-04) | Computed per (parent, candidate) pair by TerraPreserve tooling. `truth_changed` is the set of invariants whose oracle result differs. `oracle_affected` is the set whose registry footprint changed. Precision and recall are measured against `oracle_affected`; DAIL's recall on `truth_changed` must be 100%. New D6 gate 10: `truth_changed ⊆ oracle_affected`. D0 amendments A2. | Accepted 4 Oct 2026 (step 4); paper text pending advisor | -| C-71 | Free-of-cost dataset route (under N-08) | D0's "$85–325" budget is replaced by USD 0. v1.1 LLM candidates come from local open-weight models through Ollama. Calibration: offline-only baseline recommended, a Free-plan AWS account optional, emulators for deployability smoke tests only. The oracle's plan-JSON input path is to be checked at D1. D0 amendments A3. | **Open**: advisor decision before step 17 (calibration) and step 19 (LLM design) | +| C-71 | Free-of-cost dataset route (under N-08) | D0's "$85–325" budget is replaced by USD 0. v1.1 LLM candidates come from local open-weight models through Ollama. Calibration: offline-only baseline recommended, a Free-plan AWS account optional, emulators for deployability smoke tests only. The oracle's plan-JSON input path is to be checked at D1. D0 amendments A3. **Decision (advisor, 11 Nov 2026): the free-of-cost route is approved.** The experiment uses free open-weight LLMs (local Ollama for wiring checks; free Kaggle or Colab GPUs for the experiment), each pinned by exact digest, quantization, temperature and seed, with its licence checked; no paid LLM API. AWS stays fully offline: no deployment, no AWS account, no calibration against live AWS. P9 and milestone M6 (AWS Demonstration) are removed from the build sequence, and the paper states that the oracle and DAIL are configuration-level only. | Decided (advisor, 11 Nov 2026) | | C-72 | Scenario classes | `gt_class` is unsafe when a step regresses an invariant or the final target FAILs. It is safe when nothing regresses, the final target PASSes and every label is definite. Otherwise it is indeterminate: excluded from the 320, replaced, and counted. New D6 gate 11. D0 amendments A7. | Accepted 4 Oct 2026 (step 4); paper text pending advisor | | C-73 | Checkov `CKV_AWS_24` semantics (D1 item V04) | Verified at Checkov 3.3.30: `CKV_AWS_24` scans inline `ingress` of `aws_security_group`, `aws_security_group_rule` of type ingress and `aws_vpc_security_group_ingress_rule`. It matches the literal `0.0.0.0/0` and the strings `::/0` and `0000:0000:0000:0000:0000:0000:0000:0000/0` (for `aws_vpc_security_group_ingress_rule` the IPv6 `cidr_ipv6` is missed, and so is an `ip_protocol = -1` rule without ports). It ignores the protocol unless it is `-1`, so `udp` or `icmp` on port 22 from `0.0.0.0/0` FAILs; it treats ports 0-0 as all ports; it passes a rule that also lists `prefix_list_ids` or sets `self = true`; in an inline group it stops at the first `self = true` block; it ignores egress; it reports no result for an unresolved variable; it does not union CIDRs. Evidence: [RESOLUTION.md V04](https://github.com/Ayushxsingh100/terrapreserve/blob/ff70de82622b7d275bbf0f2490f0ce521786246e/validation/d1_to_verify/RESOLUTION.md) at terrapreserve `ff70de8`. Affected spec text, left as written: registry §3.7 lines 237-239 (the resource list and "has no IPv6 clause here"); registry §8 vectors S4, S8 and S9 (registry and Checkov disagree: Checkov PASS, FAIL and PASS); D0 amendments A5 line 134 ("differences recorded"). Open question for the authors: which Checkov disagreements are expected documented limitations and which count as findings against Checkov in the paper. | **Open**: authors; recorded 23 Oct 2026 (D1 Prompt C); no semantics changed | | C-74 | Relevant-unsupported type lists: completeness (D1 item V12, heuristic) | A keyword heuristic over the 1,678 resource types of provider 6.53.0 matches 396 types; 25 are supported or already listed, 371 are not listed (126 of them in the core EC2/VPC/RDS name families). Candidates to decide on first: `aws_vpc_security_group_rules_exclusive` (removes unlisted rules), `aws_vpc_security_group_vpc_association`, `aws_vpn_gateway_route_propagation`, `aws_vpc_route_server_propagation` (routes added outside the configuration), `aws_default_subnet` and `aws_default_vpc`, the accepter and options types of the listed peering and transit-gateway attachments. The heuristic is not a proof of relevance or irrelevance. Evidence: [RESOLUTION.md V12](https://github.com/Ayushxsingh100/terrapreserve/blob/ff70de82622b7d275bbf0f2490f0ce521786246e/validation/d1_to_verify/RESOLUTION.md) at terrapreserve `ff70de8`. Affected: registry §2.7 table (lines 136-140) and the marker at line 142, the UNSUPPORTED conditions in §3.4 and §6.4 row 2, §9. Open question: which candidates join which list before the freeze. Nothing was added to the lists. **Decision 24 Oct 2026 (authors):** the candidates were added to registry §2.7 as listed (rules-exclusive to the three security-group lists; the rest to INV-FUNC-001); over-approximation is intentional. | Accepted 24 Oct 2026 (authors, D2 step 6 Package 1) | @@ -140,7 +140,7 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-126 | P3b: RT-1 precisely (implements C-90) | The controlled list is exactly C-90's v1 list: `aws_security_group.name`, read from `Resource.attributes["name"]`. It is a data table (`REPLACE_TRIGGER_FIELDS`), so a later version extends it without a change of the algorithm; this package adds no field. For a **paired** `aws_security_group` with different fingerprints: `name` Known on both sides and unequal gives SAME and **REPLACED** with `REPLACE_TRIGGER_FIELD` (both values observed); `name` unresolved (unknown, unsupported or a reference) on a side, or absent on exactly one side (the provider computes a name when none is set, and an explicit `null` is absent, C-120), with different encodings gives **UNCERTAIN** with `REPLACE_TRIGGER_UNRESOLVED` (Doc 07 §12: "rather than inventing REPLACED"); identical encodings (the same unknown, the same reference, absent on both sides) give no replacement evidence, so MODIFIED. REPLACED is never concluded for an unsupported type. **Known limitation (paper threat to validity):** an argument that Terraform replaces on but that is not in the list is reported MODIFIED. The ForceNew arguments of the other types and the other arguments of `aws_security_group` that are left out are listed as suggestions in the P3b report with citations; changing the list is a register decision. **Authors' decision (28 Oct 2026): Accepted as implemented, including the interpretations listed in the P3b report, section 9.** | Accepted 28 Oct 2026 (authors, P3b decisions) | | C-127 | P3b: identity-strategy seam (C-20, hypothesis H3) | `IdentityStrategy` is a small protocol with two implementations. `EvidenceIdentity` is everything above and the only one production code may use. `AddressOnlyIdentity` is the ablation: pairing by identical address only, no moves, no RT-1, no AMB-1, no implicit moves; equal fingerprint UNCHANGED, different MODIFIED, unpaired CREATED or DELETED. Placeholders are still UNCERTAIN in the ablation, and so are the unpaired instances of an indeterminate block (C-124 rule 3): the ablation removes identity *evidence*, not the rule that unknown is not a pass. **Interpretation (confirmed by the authors, 28 Oct 2026; H3 therefore isolates only moves, RT-1 and AMB-1):** the work package lists only the placeholders as kept; the instances next to a placeholder are kept as well because they are the same rule, and because it says the ablation differs from the full strategy "exactly on moved, replaced and ambiguous cases". The flags `UNSUPPORTED_TYPE` and `UNRESOLVED_CONTENT` are attached by both strategies. `compare` checks that every input resource is in exactly one match whatever the strategy (`IdentityStrategyError`). The strategy is an explicit argument of `compare` with `EvidenceIdentity()` as default; there is **no configuration key and no environment switch**, and every report names its strategy in `algorithm_version` (`dail-identity-1`, `dail-identity-addr-1`). The ablation exists only so that the experiment harness (P8) can run the condition "DAIL minus identity". Whether it changes any result is not known; it is hypothesis H3 until measured. **Authors' decision (28 Oct 2026): Accepted as implemented, including the interpretations listed in the P3b report, section 9.** | Accepted 28 Oct 2026 (authors, P3b decisions) | | C-128 | P3b: an explicit move from a key-less address is refused by the pipeline while Terraform accepts it | Found while testing that a `moved` block removes the ambiguity of C-125. P3a-2 (`core/terraform_model/evaluation.py`, `_moves`) reads a key-less `from` as "the resource is still declared" (`eval.move_from_exists`), so `moved { from = aws_vpc.v to = aws_vpc.v["a"] }` on a resource `v` that now has `for_each` (or `to = aws_vpc.v[1]` with `count`) makes the whole evaluation UNSUPPORTED (checked 28 Oct 2026 with `evaluate_configuration`). Terraform unifies the two endpoints to instance level when either has a key (`internal/addrs/move_endpoint.go` L173-L215, tag `v1.15.8`) and then asks whether the *no-key instance* is still declared (`internal/refactoring/move_validate.go` L99, `moveableObjectExists` L229-L243); with `count` or `for_each` it is not, so the statement is valid. **Effect:** fail-closed (UNSUPPORTED is never a pass), no safety problem, but the move that gives a key to an existing resource cannot reach the identity engine through the pipeline; the engine tests pass that move directly. P3a-2 is merged and outside P3b, so nothing was changed. **Question for the authors:** relax the check for an instance-level statement in a later fix package? **Authors' decision (28 Oct 2026): stays Open as a recorded limitation; it fails closed. Decide before D4 (step 16), because the F5 scenario family (adding `for_each` or `count` with a `moved` block) can produce this form.** | Open (recorded limitation; decide before D4, step 16) | -| C-129 | P3b: a move that changes the instance key is MODIFIED | `logical_identity` holds the instance key (C-113), so the fingerprint of `v["x"]` differs from that of `v["z"]` even when everything else is equal. A pair made by an instance-level `moved` block that changes the key is therefore SAME and MODIFIED, not UNCHANGED (Doc 07 §9 applied to the C-33 fingerprint); a resource-level move keeps every key and can be UNCHANGED. This reports more change than Terraform's no-op move, which is the conservative direction. Test: `test_an_instance_level_move_pairs_exactly_that_instance`. **Question for the authors:** keep it, or leave the key out of the comparison for a pair that a move made? **Authors' decision (28 Oct 2026): accepted as a conservative limitation.** | Accepted 28 Oct 2026 (authors, P3b decisions) as a conservative limitation | +| C-129 | P3b: a move that changes the instance key is MODIFIED | `logical_identity` holds the instance key (C-113), so the fingerprint of `v["x"]` differs from that of `v["z"]` even when everything else is equal. A pair made by an instance-level `moved` block that changes the key is therefore SAME and MODIFIED, not UNCHANGED (Doc 07 §9 applied to the C-33 fingerprint); a resource-level move keeps every key and can be UNCHANGED. This reports more change than Terraform's no-op move, which is the conservative direction. Test: `test_an_instance_level_move_pairs_exactly_that_instance`. **Question for the authors:** keep it, or leave the key out of the comparison for a pair that a move made? **Authors' decision (28 Oct 2026): accepted as a conservative limitation.** **Superseded by C-177 (authors, 31 Oct 2026, paper audit round 3, finding C-01): "Every resource move counts as a change"; the clause "a resource-level move keeps every key and can be UNCHANGED" no longer holds.** | Superseded by C-177 (31 Oct 2026); was Accepted 28 Oct 2026 (authors, P3b decisions) as a conservative limitation | | C-130 | P3b: the v1 controlled list (C-126) against the provider's ForceNew arguments and the fixtures | In provider 6.53.0 more arguments of the supported types are ForceNew than the one in C-90 (list with line numbers in the P3b report, section 8; for `aws_security_group`: `description` L73, `name` L83, `name_prefix` L94, `vpc_id` L115 of `vpc_security_group.go`). Five fixtures contain an `aws_security_group_rule` pair whose changed argument is ForceNew in the provider (`cidr_blocks` L62, `source_security_group_id` L135 of `vpc_security_group_rule.go`): `func_unknown_dependency_unknown_v1`, `ec2_rds_5432_pass_v1`, `sg_private_postgres_pass_v1`, `sg_private_ssh_pass_v1`, `sg_public_postgres_fail_v1`. Their hand-derived `changes` say SAME and MODIFIED, and the engine agrees under the v1 list. If the list grows, those five blocks (and the paper's change-class counts) have to be derived again. This package changes neither the list nor a fixture. **Question for the authors:** is the one-field list final for v1, with this as a threat to validity, or does it grow before the experiments? **Authors' decision (28 Oct 2026): the controlled list stays at the single v1 field (`aws_security_group.name`); the row stays Open as a recorded limitation. Decide before D5 (oracle labels), because the oracle's plan JSON may show replace actions for the five fixtures whose changed argument is ForceNew.** | Open (recorded limitation; decide before D5, oracle labels) | | C-131 | P3c: dependency engine boundary, inputs and NetworkX | `core/dependency` imports only the standard library, `core.domain` and itself (contract rule R15, ADR-005); never `core.terraform_model`, `core.identity`, `core.persistence`, `core.application` or `core.promotion`. **Inputs:** the state's `Resource` tuple, the `Invariant` definitions (`core.domain.invariant`, with `InvariantScope`) and optional `SemanticBinding`s (a frozen dataclass in `core/dependency/invariants.py`: `invariant_id`, `source`, `destination`, `protocol`, `port`; the `S`/`D` bindings of the fixtures' `expected.json`). All resources must carry one non-null `normalization_version` in `Resource.provenance` (the same value), addresses must be unique, `(invariant_id, version)` must be unique and every binding must name a given invariant, else `DependencyInputError` (a `DomainValidationError`). An empty state has no resource to read the version from, so `build_graph` takes an optional keyword `normalization_version` that is required then (and must agree with the resources otherwise). **NetworkX is not used.** The graph is frozen tuples with a plain adjacency index, because (a) Doc 07 §28 needs an ordering controlled end to end, (b) it avoids the first third-party package in `core` (R7, `dev.lock`, `pip-audit`) for a graph of a few hundred nodes, and (c) P3c only constructs the graph and offers a small traversal. **Deviation from the spec's ADR list:** Doc 02 §26 and the README row name NetworkX for ADR-005. The ADR file did not exist (README: "Pending - written in P3c"), so it is written, not rewritten, as "Dependency graph representation; NetworkX deferred", status Proposed. Four texts still named the NetworkX exception when P3c was written: `CLAUDE.md` (Architecture rules), `docs/adr/ADR-002`, the `graph` extra `networkx==3.6.1` in `pyproject.toml`, and the docstring of `core/dependency/__init__.py`. The last was rewritten in P3c; the other three were removed in the P3c-fix housekeeping commit (the extra was declared and never installed, locked or imported, so no lock or pin in use changes). P4 reassesses only if a traversal need appears. **Question for the authors:** accept the deviation, and remove the stale mentions in a housekeeping change? | Proposed (P3c) | | C-132 | P3c: domain types, names and identity (`core/domain/graph.py`) | **`GraphNode`:** `node_id` (`RESOURCE:`, `INVARIANT::`, `SEMANTIC:`), `node_type` (RESOURCE, INVARIANT, SEMANTIC), `ref_id` (the address, the invariant id, or the semantic token), `attributes` (JSON, no floats). Guards tie the three together. **`GraphEdge`:** Doc 05's `edge_type` is the **class** (TERRAFORM_REFERENCE, INFRASTRUCTURE, INVARIANT_SCOPE, INVARIANT_SEMANTIC); the typed relationship of Doc 07 §16 is the new field `relationship`. Closed vocabulary by class: TERRAFORM_REFERENCE has `REFERENCE`; INFRASTRUCTURE has `SUBNET_BELONGS_TO_VPC`, `ROUTE_TABLE_BELONGS_TO_VPC`, `ASSOCIATES_SUBNET`, `ASSOCIATES_ROUTE_TABLE`, `IGW_ATTACHED_TO_VPC`, `INSTANCE_IN_SUBNET`, `INSTANCE_USES_SECURITY_GROUP`, `DB_USES_SECURITY_GROUP`, `RULE_BELONGS_TO_SECURITY_GROUP` and `DB_SUBNET_PLACEMENT` (C-136, not a §16 row); INVARIANT_SCOPE has `SCOPE`; INVARIANT_SEMANTIC has `SOURCE`, `DESTINATION`, `PROTOCOL_PORT` and `BINDING` (added by P3c: the prompt's list has no relationship for the missing-binding edge of C-134; reported, not decided). A relationship outside its class is refused. `edge_key = SHA-256 (core.domain.hashing) of {source_node_id, edge_type, relationship, target_node_id, attributes}` (Doc 07 §22 plus the class); **`edge_key` is the edge's identity**, and Doc 05's UUID `edge_id` (a persistence identifier) is not created because nothing persists graphs. Status is `DependencyStatus` (KNOWN, UNCERTAIN, UNSUPPORTED) and is **not** part of the key. Fields: `edge_key`, `source_node_id`, `target_node_id`, `edge_type`, `relationship`, `status`, `attributes`, `evidence`, `provenance` (non-empty tuple of `Provenance`: the source resource's; for invariant edges a DERIVED one). **`DependencyEvidence`** (Doc 07 §27): `source`, `target` (node ids), `edge_type`, `relationship`, `source_fact`, `target_fact` (short stable text), `derivation_rule` (closed vocabulary, C-133 item 7) and `status`; it must agree with its edge. **`DependencyGraph`:** `graph_id`, `state_id`, `nodes` (sorted by `node_id`), `edges` (sorted by `edge_key`), `graph_version` (= `algorithm_version`), `normalization_version`, `algorithm_version` (`GRAPH_ALGORITHM_VERSION`, `"dail-graph-1"` in P3c, `"dail-graph-2"` since C-136), `created_at`, `graph_hash`. Guards: unique node ids, unique edge keys, every endpoint is a node, resource-class edges start at a RESOURCE node and invariant-class edges at an INVARIANT node, `edge_key` and `graph_hash` recomputed (`HashMismatchError`), frozen, JSON-validated, `to_dict`/`from_dict` round trip. Cycles are allowed by the type. **The graph hash is structural:** it covers `{algorithm_version, normalization_version, nodes, edges}` (an edge as key, endpoints, class, relationship, status, attributes) and excludes `graph_id`, `state_id`, `created_at`, provenance and evidence. **Node attributes are structural only:** a resource node has `{kind, resource_type, support_status}` and nothing else, where `kind` is `resource`, `data`, `module` or `absent`; a security-group-rule resource node also has `{direction, protocol, from_port, to_port, rule_key, determinate, unsupported}` from `security_attributes.rule` (`rule_key` is the P3a canonical text of the equivalence fields, Doc 07 §18; a test checks it against `CanonicalSecurityRule.rule_key()`); a security-group node also has `{inline_forms, inline_rule_keys (sorted), inline_indeterminate}`; an invariant node has `{category, name}`; a semantic node has `{kind}` (`protocol_port`, `unresolved` or `external`). Never the fingerprint and never a raw attribute value, so a tag change or a ForceNew `name` change leaves the hash unchanged. (The prompt lists `unresolved` among the resource `kind` values; unresolved targets are SEMANTIC nodes here, so it is a semantic kind. Reported, not decided.) A `data` or `module` node has `support_status` UNSUPPORTED (not modelled) and an `absent` node UNKNOWN; `resource_type` is read from the address text. Node ids: `SEMANTIC:UNRESOLVED:#`, `SEMANTIC:EXTERNAL:#`, `SEMANTIC:UNRESOLVED:#binding`, `SEMANTIC:/`. | Proposed (P3c) | @@ -161,7 +161,7 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-147 | P5a: the structural and consistency gate | A `STRUCTURAL` item and a `CONSISTENCY` item run on **every** candidate, added by `run_work_set` with reason `MANDATORY_GATE` and priority BLOCKING, whether or not the impact report lists them (Doc 09 §6). Structural checks (Doc 09 §6, §15): the construction status is OK, otherwise the item FAILs with `construction.invalid` and **every invariant item returns UNSUPPORTED** with that reason and none is evaluated (registry §2.8); each resource's `fingerprint` and `canonical_json` recompute; addresses are unique; every `Reference` resolves to a resource of the candidate or is marked UNKNOWN or UNSUPPORTED; the candidate `state_hash` recomputes with the domain's own `resource_set_hash`; a graph, if given, has a node for every resource and recomputes its hash; every invariant a work item names is in the definitions; the parent lineage matches when a parent is given. Consistency checks (Doc 09 §31): the identity report's candidate id and refs exist; the impact report has the same candidate id and parent state id; its `graph_version` equals the graph's algorithm version; every result passed in refers to the same candidate. Each failed check is a recorded finding with a closed code, and any finding fails the item. A work item whose invariant is unknown to the definitions makes the structural item FAIL with `invariant.unknown` and the item itself returns UNSUPPORTED with that reason (never VERIFIER_ERROR, never PASS). **Step 5 details:** `VerificationInputs` also carries `normalization_version` (needed to recompute the state hash of an empty candidate) and `construction_note`. The closed finding codes are `construction.invalid`, `resource.fingerprint_mismatch`, `resource.canonical_json_mismatch`, `resource.duplicate_address`, `reference.unresolved` (a reference marked SUPPORTED whose target is neither an instance address nor the address of a block that has instances), `state.hash_mismatch`, `state.normalization_mixed`, `graph.node_missing`, `graph.hash_mismatch` (the graph does not survive a round trip through its constructor), `lineage.graph_state_mismatch` (**the "parent lineage" check, as read here:** the trusted graph belongs to `parent_state_id` and the candidate graph to `candidate_id`), `work.invariant_unknown`, `work.resource_unknown`, `identity.candidate_mismatch`, `identity.parent_mismatch`, `identity.ref_unknown`, `impact.candidate_mismatch`, `impact.parent_mismatch`, `impact.graph_version_mismatch`, `impact.graph_hash_mismatch` (**added:** the impact report's graph hashes equal those of the graphs given) and `result.candidate_mismatch`. Gate reasons: `construction.invalid`, `structural.finding`, `consistency.finding`; both gates are evidence level L0 and class STRUCTURAL / CONSISTENCY. A construction status of UNSUPPORTED is treated like INVALID. | Proposed (P5a) | | C-148 | P5a: baseline verification and types with no predicate | P4 emits a `RESOURCE` work item (class BASELINE) per CREATED resource. For a created `aws_security_group` or `aws_security_group_rule` the item runs `PIP(22)` and `PIP(5432)` and reports the clauses of the groups that resource contributes to; the item result is the worst of the two, restricted to those groups (the restriction narrows the observations only; it never turns another group's FAIL into PASS, which the invariant items still carry). A created `aws_db_instance`: the SEC-003 flag of that instance. A created resource of a relevant-unsupported type: UNSUPPORTED. A created resource inside an indeterminate (placeholder) block: UNKNOWN. **A created resource of any other type: PASS with `applicable = false`**, and the assumption `registry-v1.0 declares no baseline predicate for ` (Doc 08 §16; registry §2.7: every other unsupported type is declared irrelevant). **This is an explicit modelling assumption that the paper must state, not a proof. Flagged for the authors:** the alternative is a distinct NOT_APPLICABLE outcome that never counts as proof. **Step 5 details:** the verifier of a security-group or rule item is that of INV-SEC-001 in the definitions given, of a database item that of INV-SEC-003, of a not-applicable item the DAIL-internal `dail.verify.baseline` version `1` (not a registry §10 identity); a definition set without the invariant makes the item UNSUPPORTED `invariant.unknown`, never PASS. The relevant-unsupported list used is the security-group list of registry §2.7 (the INV-FUNC-001 list joins in P5b). A placeholder of any type is UNKNOWN with the new reason `resource.indeterminate`; an unreadable (UNSUPPORTED) security group, rule or database is UNSUPPORTED `rule.unsupported`; a work item naming a resource the candidate does not have is UNSUPPORTED `structural.finding` (and a structural finding). Observations: `resource`, `resource_type`, and `groups` and `predicates` (per port, per clause) for groups and rules, or `value` for a database. | Proposed (P5a) | | C-149 | P5a: the stored view does not say which field of a rule is unresolved (R1) | Registry §3.3 makes `possible4(g)` depend on a rule's IPv4 sources being unresolved and `possible6(g)` on its IPv6 sources, apart from the protocol and ports. The stored rule view (`security_attributes`) has `determinate` and `problems` (reason codes such as `variable.no_value`), but a reason does not name the field, and an unresolved list is stored as `[]`. So `func_unknown_dependency_unknown_v1` (an ingress rule on 5432 whose **source group** is unknown, expected clauses PASS and PASS) cannot be told from a rule with an unknown CIDR list by the view alone. **Resolution used:** for an `aws_security_group_rule` the verifier reads the rule's own `attributes` (C-112 encoding, which holds every configured argument) and derives, per field, whether it is unresolved: exact. For inline rules the stored blocks are in `attributes` too, but the view sorts them, so a rule cannot be paired with its block without redoing P3a's canonicalisation; the verifier takes the **union over the indeterminate blocks of one direction** of the family flags (IPv4 list unresolved, IPv6 list unresolved) and gives them to every indeterminate inline rule of that direction. This can only add UNKNOWN (never remove it); it differs from the registry text only for a group with two or more indeterminate inline blocks in one direction that are unresolved in different families, and then only at clause level unless a third block explains the first. No fixture or vector is affected. **Question for the authors:** accept this, or extend the P3a view (a P3a change) to record the unresolved fields per rule? | Open (found 28 Oct 2026; P5a) | -| C-150 | P5a: registry §3.3 drops an indeterminate rule whose sources are known | Registry §3.3 defines `possible4(g)` as an indeterminate rule that could permit TCP/p **and** whose IPv4 sources are unresolved or include a prefix list (`possible6` likewise). A rule whose protocol or port is unresolved but whose IPv4 source is known, for example `from_port = var.p` with `cidr_blocks = ["0.0.0.0/0"]`, is indeterminate, could permit the port, but has resolved sources, so it is not `possible`, is not in `D(g)` (not determinate), and the registry text gives PASS although the rule may open the port to the internet. **Implemented verbatim** (work package: no reinterpretation), pinned by `TestRegistryGap` in `tests/unit/test_verification_public_ingress.py`, and the rule is reported in the observation `indeterminate_rules`. It is the one place where the registry text lets a PASS stand on a rule whose meaning is unresolved, against "uncertainty is never a pass" (CLAUDE.md). The independent oracle follows the same text, so the two would agree and both be unsound for this case. **Proposed amendment, for the authors:** `possible` also when the family's sources are known and non-empty (what C-146 already does for a rule with an unresolved direction); a new registry file and version bump under C-85. **Question: amend, or accept and state as a limitation?** | Open (found 28 Oct 2026; P5a step 4) | +| C-150 | P5a: registry §3.3 drops an indeterminate rule whose sources are known | Registry §3.3 defines `possible4(g)` as an indeterminate rule that could permit TCP/p **and** whose IPv4 sources are unresolved or include a prefix list (`possible6` likewise). A rule whose protocol or port is unresolved but whose IPv4 source is known, for example `from_port = var.p` with `cidr_blocks = ["0.0.0.0/0"]`, is indeterminate, could permit the port, but has resolved sources, so it is not `possible`, is not in `D(g)` (not determinate), and the registry text gives PASS although the rule may open the port to the internet. **Implemented verbatim** (work package: no reinterpretation), pinned by `TestRegistryGap` in `tests/unit/test_verification_public_ingress.py`, and the rule is reported in the observation `indeterminate_rules`. It is the one place where the registry text lets a PASS stand on a rule whose meaning is unresolved, against "uncertainty is never a pass" (CLAUDE.md). The independent oracle follows the same text, so the two would agree and both be unsound for this case. **Proposed amendment, for the authors:** `possible` also when the family's sources are known and non-empty (what C-146 already does for a rule with an unresolved direction); a new registry file and version bump under C-85. **Question: amend, or accept and state as a limitation?** **Decision (authors, 11 Nov 2026, C-150 amended): close the gap now in registry v1.1 instead of stating it as a limitation; implemented by C-178.** | Decided (authors, 11 Nov 2026): see C-178 | | C-151 | P5b: FUNC verifier boundary, entry and parameters | `core/verification/reachability.py` (the predicate) and `core/verification/func_view.py` (the reader of the stored resources) import only the standard library and `core.domain`, like the rest of `core.verification` (contract rule R17, nothing loosened; the self-test now names both modules). The verifier is registered in `dispatch.DEFAULT_VERIFIERS` under `dispatch.REACHABILITY_CFG` = `("dail.verify.reachability_cfg", "1")`, read from the definition, not retyped; a pair that is missing from the table is still UNSUPPORTED `verifier.not_available`. Entry: `evaluate_reachability(definition, inputs) -> PredicateOutcome`. The endpoints are `definition.predicate["parameters"]` = `{S, D, port}`; a definition without text `S` and `D`, with `S == D`, or with `port != 5432` is UNSUPPORTED `parameters.invalid`, never PASS. An endpoint of the wrong type (S not an `aws_instance`, D not an `aws_db_instance`) is UNSUPPORTED `parameters.invalid`. A stored value the reader cannot read raises `ViewError`, which the engine turns into VERIFIER_ERROR; "cannot read" is never "absent". **Shared code:** the MIXED test (registry §2.6) moves from `public_ingress` to `views.group_is_mixed` and RETAINED-INLINE gets a direction parameter (`retention.inline_retention`, with `ingress_retention` as the same call for ingress), so FUNC reads the egress of `SG(S)` and the ingress of `SG(D)` with the one definition; `views.Rule` gains the flags `sources_unresolved` and `self_unresolved` (read like the family flags of C-149); `cidr.py` gains `overlaps`. The SEC results are unchanged and the whole SEC test suite is the check. New reason codes (closed vocabulary): `parameters.invalid`, `endpoint.absent`, `port.mismatch`, `vpc.mismatch`, `path.missing`, `coverage.partial`, `route.unsupported`, `interface.unsupported`, `value.unsupported`, `model.unsupported`. | Proposed (P5b) | | 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) | @@ -188,3 +188,8 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-174 | P6c: fixed patch only, patch text not applied | The patch is a record bound to the parent; `candidate_dir` is the candidate. The orchestrator stores the `Patch` and its hash and checks `patch.parent_state_id` against the candidate's parent; it does not check that the patch text produces the directory. A limit for P7b (patch validation) and P8: a request whose patch and directory disagree is evaluated as the directory says. | Proposed (P6c) | | C-175 | P6c: sole callers of the repository writes (closes the C-168 (b) carry-forward) | R8 is extended to the repository writes: in `core/`, `evidence/`, `llm/` and `scripts/`, `TrustedStateRepository.save_promoted` is called only from `core.promotion.commit` (defined in `core.persistence`) and `save_baseline` only from `core.application.baseline` (defined in `core.persistence`). Tests are not scanned, as for R8. The check (`repository_write_violations` in `tests/contract/test_architecture_boundaries.py`) sees an attribute use and a string given to `getattr`, `hasattr` or `setattr`; its self-test fires for a forbidden caller and for each write named by the other write's permission. Nothing is loosened. | Proposed (P6c) | | C-176 | P6c: baseline evidence carries the state's own hash (the prompt names `to_evidence_submission`) | C-171 says to record the baseline VERIFICATION evidence with `to_evidence_submission(..., parent_state_id=None, state_id=)`. That helper stamps the record with `result.candidate_hash`, the hash of the **resource set** that was verified. Evidence about a state must carry that state's `state_hash` (Doc 11 §8, §44), and P6b's binding check (`carried_problems` for a version-0 parent, `evaluate_proof` condition P6) compares exactly that value when a later candidate carries an unaffected invariant forward from version 0 (INV-SEC-003 in the canonical scenario). Probed during P6c step 3: with the helper's record `evaluate_proof` answers "P6: the evidence state_hash differs from the state", so every carry-forward from a baseline would be refused and every canonical PROMOTE would ESCALATE. **Implemented instead:** `core/application/baseline.py` builds the submission itself, from the same result payload, kind, event name and provenance as the helper, once the state exists; the state hash depends on the invariant statuses and resources but not on evidence ids, and the evidence ids are derived from `baseline_id`, so the order is possible. No change to `core.verification` or `core.domain`. For the authors: either this, or a `state_hash` argument on `to_evidence_submission` (a change to a package that has passed its gate). | Proposed (P6c) | +| C-177 | P6d: every move is a change (supersedes C-129's resource-level clause) | **Authors' decision (31 Oct 2026, paper audit round 3, finding C-01): "Every resource move counts as a change."** A pair made by a `moved` block of the candidate, or by Terraform's implicit `count` move (C-76: `x` to `x[0]` when `count` is added, `x[0]` to `x` when it is removed), is never UNCHANGED, even when the fingerprints are equal. With equal fingerprints it is MODIFIED, the match carries `moved = true`, its deciding rule is the move evidence (`EXPLICIT_MOVE` or `IMPLICIT_COUNT_MOVE`, which names `from`, `to` and the statements applied) and `FINGERPRINT_EQUAL` is still attached. With different fingerprints it is MODIFIED (`moved = true`), or REPLACED / UNCERTAIN exactly as RT-1 decides. No `ChangeType` value is added (Doc 05's enumeration is unchanged): the flag is the field `IdentityMatch.moved`, serialized and required in `from_dict`, and the domain refuses a match whose flag disagrees with its refs (a pair across two addresses must be `moved`, a pair at one address and a one-sided match must not be, and a moved pair cannot be UNCHANGED). Impact treats every such pair as a change source with the flag `ChangeFlag.MOVED` (the reason "moved"); it is never dropped as unchanged. No evidence is carried across a REPLACED pair (unchanged rule; a moved-and-replaced security group is tested). `AddressOnlyIdentity` (C-127, H3) does not follow moves and never sets the flag. Registry text is not changed for this (the work package lists no registry change). Tests: `tests/unit/test_moves_are_changes.py`. | Decided (authors, 31 Oct 2026) | +| C-178 | P6d: registry v1.1 closes C-150; INV-SEC-001 and INV-SEC-002 version 2 | **Authors' decision (11 Nov 2026, C-150 amended): close the gap now, in registry v1.1, instead of stating it as a limitation.** `docs/specs/INVARIANT_REGISTRY_v1.1.md` (a new file, C-85; `INVARIANT_REGISTRY_v1.md` is unchanged) replaces the §3.3 clause by: `possible4(g) := exists indeterminate r in In(g) that could permit TCP/p (its protocol or ports unresolved, or they permit p) and (its IPv4 sources are unresolved or include a prefix list, or its resolved IPv4 sources, together with the union of v4(r') over r' in D(g), cover 0.0.0.0/0). possible6(g) is the same for IPv6 sources and ::/0.` A rule whose port is unresolved but whose source is the whole internet may open the port, and uncertainty is never a pass. INV-SEC-001 and INV-SEC-002 become version 2; their results change only for such rules. INV-SEC-003 and INV-FUNC-001 stay version 1. **C-155 is out of scope:** its conservative readings stay DAIL implementation choices for now and are not written into v1.1; the differences between DAIL and the oracle on those cases will be measured in P8. Evidence for SEC v1 does not satisfy v2 (C-62: equal `invariant_version` required). | Decided (authors, 11 Nov 2026) | +| C-179 | P6d: registry v1.1 §2.9 clarification (from the TerraPreserve oracle work, Open D5-D) | **Authors' decision (10 Nov 2026): wording only, no result changes, no `invariant_version` change.** Registry v1.1 §2.9 adds: "In the footprint comparison, an argument that neither configuration writes compares as absent on both sides and is not changed. The predicates still treat such a value as §2.2 says." and "The parent counterpart's inline-rule form (§3.5, §6.6) is compared through what it decides: whether the group is RETAINED-INLINE in that direction (§2.6). A baseline has no parent, so this is false for every group of a baseline." DAIL's impact analysis is resource-level (C-140) and is not changed by it. | Decided (authors, 10 Nov 2026) | +| C-180 | P6d: how DAIL stores registry 1.1, and the verifier version | The registry file says `invariant_registry_version = 1.1`, but the field is an integer ≥ 1 in `TrustedState`, `PromotionPolicy` and the schema (C-32). **User's decision (11 Nov 2026): keep the integer; DAIL stores registry v1.1 as `2`** (1 = the `registry-v1.0` tag, 2 = `registry-v1.1`; `core.domain.registry_v1_1.REGISTRY_VERSION_V1_1`). Definitions and evidence cite the tag `registry-v1.1`. **User's decision (11 Nov 2026): the verifier version of `dail.verify.public_ingress` stays `"1"`**: registry v1.1 changes exactly what the work package lists and §10 is not among them; v1 and v2 evidence are already told apart by `invariant_version` (C-62). Question for the reviewer: should a later registry bump §10 when a predicate changes? | Decided (user, 11 Nov 2026) | +| C-181 | P6d: implementation readings for registry v1.1 | (1) `core/domain/registry_v1_1.py` is a new module beside `registry_v1.py`, which keeps building the v1.0 definitions unchanged (they are what TerraPreserve v1.0's labels and the existing fixtures cite, and its tests read the v1.0 file). v1.1 takes INV-SEC-001/002 from v1.0, sets `version = 2`, cites `registry-v1.1` in `predicate.registry` and the description; INV-SEC-003 and INV-FUNC-001 are the v1.0 definitions object for object (same `definition_hash`, so a stored definition of the same id and version is not contradicted). (2) The public-ingress verifier reads `predicate.registry` of the definition: `registry-v1.0` evaluates the v1.0 clause, `registry-v1.1` the v1.1 clause, any other tag raises (VERIFIER_ERROR, fail closed). The direct function's default is v1.1 (the conservative one); baseline resource items use it. (3) C-146 (2) is kept: a rule whose direction is unresolved is `possible` for a family when it has any known source of that family (wider than v1.1). (4) The citation `registry-v1.0` that the verification engine and the impact work items wrote for every invariant now comes from the definition's `predicate.registry`. (5) The test pipeline (`tests/promotion_pipeline.py`) takes the definitions and the registry version as keywords; the default stays v1.0, so no passed test changes its inputs. | Proposed (P6d) | diff --git a/docs/PHASE_GATES.md b/docs/PHASE_GATES.md index f7496d8..d98bcba 100644 --- a/docs/PHASE_GATES.md +++ b/docs/PHASE_GATES.md @@ -236,8 +236,58 @@ the stale route). C-176: baseline evidence is built in core.application.baseline to_evidence_submission stamps the resource-set hash, not the state's. Construction failure stores no decision (C-170 (3), for the authors). 18 fixtures have a parent, the prompt said 17. ``` +P6c mini-gate: PASSED. P6 gate: PASSED WITH LIMITS. M3 (Trust Transition Complete): reached for +fixed patches (external review, 29 Oct 2026; PR #26 at d7c0333, merged before the verdict, C-28 +process lapse recorded a ninth time). Suite passes on Python 3.12 and 3.13 (4106 tests); black, ruff +and mypy clean; no passed package, fixture or requirement changed. Reviewer probes: conflicting +reruns refused, emergency switch turns a PROMOTE into an audited ESCALATE with no state change; +6 of 6 reviewer mutations of the orchestrator killed. +Limits: reports are not persisted (P8); fixed patches only, patch text not applied (P7b); one +SQLite file; Step 5 suites written after the code; author's 38 mutations and the C-176 probe not +re-run by the reviewer. +Carry-forward: a second attempt on the same terminal candidate returns the first decision without +deciding (MEDIUM; reject or document in P7/P8); C-173 Proposed until the authors confirm; C-169 Open; +C-170 to C-176 Proposed. + +## P6d — Every move is a change, and invariant registry v1.1 (pending external review) -## P6c–P10 — NOT STARTED +```text +P6d mini-gate: NOT DECIDED. Status written by the P6d author as an input to the external review. +What changed: + Moves (C-177, supersedes C-129's resource-level clause): a pair made by a moved block or by the + implicit count move is never UNCHANGED; with equal fingerprints it is MODIFIED, the match carries + moved = true and the move evidence decides; impact carries it with the flag MOVED. No new + ChangeType. AddressOnlyIdentity (C-127) is unchanged. tests.unit.test_moves_are_changes. + Registry v1.1 (C-178 to C-181): docs/specs/INVARIANT_REGISTRY_v1.1.md, the v1.0 text with the + §3.3 possible clause (C-150 closed), the §2.9 wording and the versions; INVARIANT_REGISTRY_v1.md + unchanged (sha256 pinned by a test). INV-SEC-001/002 version 2, INV-SEC-003 and INV-FUNC-001 + version 1; DAIL stores registry 1.1 as invariant_registry_version 2 (C-180). The verifier reads + the definition's predicate.registry; SEC evidence of version 2 cites registry-v1.1. Version 1 + evidence is not carried forward to version 2 (C-62). tests.unit.test_registry_v1_1, + tests.unit.test_verification_public_ingress.TestRegistryGap. +Equivalence on TerraPreserve v1.0 (read-only; archive sha256 equal to TerraPreserve +docs/D6_FREEZE.md at 8ec1931): indeterminate SEC-001/002 ingress rules that v1.1 makes possible +and v1.0 does not: dev primary 0, dev alternate 0, test primary 0, test alternate 0. +TerraPreserve v1.0 labels are identical under registry v1.0 and v1.1. + How: the test split records no indeterminate SEC ingress rule. The dev split records two + (tp-v1-F3-0278, aws_security_group.ec2_sg.ingress[0] and [1], both value sets, steps 0 and 1, + reason "security-group sources unresolved"); the archive does not record their sources, so the + scenario's Terraform (scenarios/dev/tp-v1-F3-0278, steps 0 and 1) was read, not run (user's + decision, 11 Nov 2026): neither rule has cidr_blocks, ipv6_cidr_blocks or prefix_list_ids, and + the clause records no violation, so neither is possible under v1.1. +Limits: the oracle itself is not changed (TerraPreserve is read only); C-155's readings stay DAIL +choices (P8 measures them); the verifier version stays "1" (C-180, question for the reviewer); +the test pipeline still defaults to the v1.0 definitions, and the canonical scenario is run under +v1.1 by tests.unit.test_registry_v1_1. Carry-forward: C-181 Proposed; the user tags registry-v1.1 +after the verdict and the merge. +``` + +## P7a–P10 — NOT STARTED + +P9 (AWS integration) and milestone M6 (AWS Demonstration) are removed (C-71, Decided by the advisor, +11 Nov 2026): AWS stays fully offline, with no deployment, no AWS account and no calibration against +live AWS; the oracle and DAIL are configuration-level only. The packages after P6c are P6d, P7a, P7b, +P8a, P8b and P10. ## Temporary exceptions diff --git a/docs/SPEC_INDEX.md b/docs/SPEC_INDEX.md index 7661872..88d682f 100644 --- a/docs/SPEC_INDEX.md +++ b/docs/SPEC_INDEX.md @@ -29,7 +29,8 @@ which document to consult for a given decision. - [`BUILD_SEQUENCE.md`](BUILD_SEQUENCE.md) — the 18 work packages and their order. - [`DECISIONS_REGISTER.md`](DECISIONS_REGISTER.md) — recorded conflicts and their resolutions. - [`docs/specs/D0_Dataset_Specification_TerraPreserve_v1.md`](specs/D0_Dataset_Specification_TerraPreserve_v1.md) — the TerraPreserve D0 dataset specification v1.0, the base document of the D0 amendments (added verbatim on 23 Oct 2026; implemented in the TerraPreserve repository). -- [`docs/specs/INVARIANT_REGISTRY_v1.md`](specs/INVARIANT_REGISTRY_v1.md) — the four protected invariants: exact predicates, results, footprints and conformance vectors (C-17). Normative for P4, P5, D4 and D5. +- [`docs/specs/INVARIANT_REGISTRY_v1.md`](specs/INVARIANT_REGISTRY_v1.md) — the four protected invariants: exact predicates, results, footprints and conformance vectors (C-17). Normative for P4, P5, D4 and D5. Frozen as the tag `registry-v1.0`; never edited (C-85). TerraPreserve v1.0's labels cite it. +- [`docs/specs/INVARIANT_REGISTRY_v1.1.md`](specs/INVARIANT_REGISTRY_v1.1.md) — registry v1.1 (P6d; C-178 to C-181): the v1.0 text with the §3.3 `possible` clause (C-150 closed), the §2.9 wording and the versions (INV-SEC-001 and INV-SEC-002 version 2). **For DAIL it takes precedence over v1.0 from P6d on.** v1.0 stays the reference for the evidence and the labels that cite `registry-v1.0`. - [`docs/specs/D0_AMENDMENTS_v1.0.1.md`](specs/D0_AMENDMENTS_v1.0.1.md) — amends TerraPreserve D0 v1.0 (N-03, N-04, N-08; gt_class; canonical topology). ## Precedence diff --git a/docs/specs/INVARIANT_REGISTRY_v1.1.md b/docs/specs/INVARIANT_REGISTRY_v1.1.md new file mode 100644 index 0000000..f9a5df1 --- /dev/null +++ b/docs/specs/INVARIANT_REGISTRY_v1.1.md @@ -0,0 +1,543 @@ +# Invariant Registry Specification v1.1 + +| | | +|---|---| +| **Status** | Normative for DAIL from P6d. **[v1.1]** Supersedes v1.0 (`INVARIANT_REGISTRY_v1.md`, git tag `registry-v1.0`), which is never edited. To be frozen as git tag `registry-v1.1` on the commit that merges this version (C-85). Changes after the tag go in a new file (§1.4). | +| **Register** | Implements C-17. Decisions proposed here are listed in §11 (C-64 onward). Decisions recorded on 24 Oct 2026 (D2 step 6): C-74, C-76, C-77, C-78, C-84, C-85. | +| **Registry version** | **[v1.1]** `invariant_registry_version = 1.1`. INV-SEC-001 and INV-SEC-002 are `version = 2`; INV-SEC-003 and INV-FUNC-001 are `version = 1` (§1.4). | +| **Readers** | DAIL verifiers (P5), DAIL impact analysis (P4), the TerraPreserve generator (D4), the independent oracle (D5, ADR-010), the paper. | + +## Change log (v1.0 to v1.1) + +Each change against v1.0 is marked **[v1.1]** where it is made. Nothing else differs from v1.0. + +- [v1.1] **§3.3 `possible4` and `possible6`** (C-150 closed; register C-178; authors' decision of 11 Nov 2026). An indeterminate rule that could permit TCP/*p* is also *possible* when its resolved sources, together with the union of the sources of `D(g)`, cover the whole address family. A note in §3.3 says why. INV-SEC-001 and INV-SEC-002 become version 2 (§3.1, §4.1); their results change only for such rules. +- [v1.1] **§2.9 clarification** (register C-179; authors' decision of 10 Nov 2026, from the TerraPreserve oracle work, Open D5-D). Two sentences on arguments that neither configuration writes and on the parent counterpart's inline-rule form. Wording only: no result changes and no invariant version changes. +- [v1.1] **§1 versioning.** `invariant_registry_version` is 1.1 (header table, §1.4); §1.4 lists the invariant versions of this registry, with INV-SEC-001 and INV-SEC-002 at version 2; the tag of this version is `registry-v1.1`. + +**Independence rule.** This document must be implementable by someone who has never seen DAIL's code. The TerraPreserve oracle is written only from this document, Terraform semantics and AWS semantics (ADR-010, N-02). Nothing here refers to a DAIL module, class or function. + +**Markers.** +- **[PAPER]** marks a semantic choice the paper must state; show these to the advisor. +- **[DECIDED date, C-NN]** marks an authors' decision on a D1 finding, recorded in the register row named. +- **[TO VERIFY AT D1]** marked a Terraform or AWS behaviour not yet confirmed against the pinned Terraform and AWS provider versions. D1 Prompt C resolved every such marker (23 Oct 2026). Each is now **[VERIFIED AT D1: CONFIRMED or CHANGED (item)]**, or **[OPEN AFTER D1: UNRESOLVED (item)]** when it could not be settled, with a link to the evidence in `RESOLUTION.md` at a pinned TerraPreserve commit (§12). + +**Normative words.** MUST, MUST NOT and MAY are used in the RFC 2119 sense. + +--- + +## 1. Scope and versioning + +1.1 **The four invariants.** The registry defines exactly four protected invariants: INV-SEC-001, INV-SEC-002, INV-SEC-003 and INV-FUNC-001. They are the frozen TerraPreserve v1.0 set (D0 Decision 4). + +1.2 **Evaluation level.** Every invariant is evaluated at **configuration level, evidence level L1** (Doc 09 §10; C-22). L1 means deterministic predicate evaluation over the resolved Terraform configuration. Nothing in this document is a statement about runtime packet delivery (Doc 04 §9). **[PAPER]** + +1.3 **Supported resource types** (Doc 04 §2): `aws_vpc`, `aws_subnet`, `aws_internet_gateway`, `aws_route_table`, `aws_route_table_association`, `aws_security_group`, `aws_security_group_rule`, `aws_instance`, `aws_db_instance`. Every other resource type is *unsupported*. §2.7 says when an unsupported type changes a result. + +1.4 **Versioning rule.** +- Any change to an invariant's predicate, scope, footprint (§2.9) or result conditions creates a new invariant version and increments `invariant_registry_version`. +- A change of wording only, with identical results on every input, creates no new invariant version. After the tag it still needs a new registry file and increments `invariant_registry_version` (C-85). +- The registry is frozen by the tag `registry-v1.0` (C-85). The D0 amendments are frozen separately, before D4 starts. +- **Tagging (C-85).** **[v1.1]** This version is identified by the git tag `registry-v1.1`; v1.0 by `registry-v1.0`. After its tag a registry file is never edited. Any change is a new file (`INVARIANT_REGISTRY_v1.1.md`, and so on) that increments `invariant_registry_version`, and increments `invariant_version` for each invariant whose predicate, scope, footprint or result conditions change (Doc 06 §4.2). A wording-only change still needs a new file but bumps no `invariant_version`. Fixtures, the oracle and evidence cite the tag. +- **Edits before the tag.** C-74, C-76, C-77, C-78 and C-84 changed result conditions before the tag, and every invariant stays at version 1. This is allowed because nothing had consumed version 1 yet: no fixture, oracle label or verification evidence cited its semantics. +- **[v1.1] Versions in this registry.** `invariant_registry_version = 1.1`. + + | Invariant | `invariant_version` | Changed in v1.1 | + |---|---|---| + | INV-SEC-001 | 2 | §3.3 `possible4`/`possible6` (C-178) | + | INV-SEC-002 | 2 | as INV-SEC-001 (§4.2) | + | INV-SEC-003 | 1 | no | + | INV-FUNC-001 | 1 | no | + +--- + +## 2. Common definitions (apply to all four invariants) + +### 2.1 Input + +The input is one Terraform root-module configuration directory together with the scenario's variable values. It is evaluated with the pinned Terraform and AWS provider versions; ADR-013 requires these pins to be identical in both repositories. + +An implementation MAY read HCL directly, or the JSON plan representation (`terraform show -json`). Both MUST yield the resolved values defined in §2.2. The oracle uses a different input path from DAIL (ADR-010). Neither path's convenience may change a result defined here. + +**Parent.** A candidate is evaluated together with its parent: the configuration of the Trusted State it was generated from (ADR-012). A baseline has no parent. The parent is read only by the inline-rule retention rule (§2.6, C-84); every other result definition (§3 to §6) reads the evaluated configuration alone. When TerraPreserve labels a trajectory, the parent of step k is step k − 1, which need not be a Trusted State. + +### 2.2 Resolved values + +An attribute is **resolved** when its value can be determined from the configuration and variable values alone, without provider or AWS knowledge. That covers: +- literals; +- input variables (provided value, else declared default); +- locals; +- functions over resolved values; +- a reference to an argument of another configured resource, where that argument is itself resolved. For example, `aws_subnet.app.cidr_block` resolves to the configured CIDR. + +**Identity references.** A reference to a resource's `id` (for example `aws_security_group.db.id`) is resolved **as a reference**. It identifies the configured resource instance it names, not a concrete AWS ID. + +**External literal IDs.** A literal AWS ID that names no configured resource (for example `"sg-0123abcd"`) is an **external reference**. + +**Unresolved.** Anything else is **unresolved**: data-source attributes, provider-computed attributes that are not set in the configuration, and variables without a value. + +**Modules.** Resources in local child modules (path sources) are evaluated as if inlined, using their full module address. A resource whose instances come from a non-local module source (registry, git, URL) is **unresolved**. + +### 2.3 Resource instances + +**Expansion.** +- A resource with a resolved `count` or `for_each` expands to its instances (`addr[0]`, `addr["key"]`). +- A `dynamic` block with a resolved `for_each` expands to its blocks. +- When expansion is unresolved, the number of instances or blocks is unknown. The resource or block is **indeterminate**. + +**Moves.** +- Explicit `moved` blocks MUST be followed when comparing two configurations. +- Terraform's implicit move when `count` is added to or removed from a single-instance resource MUST be followed too. [VERIFIED AT D1: CONFIRMED (V10): Terraform 1.15.8 moves `x` to `x[0]` when `count` is added and `x[0]` back to `x` when `count` is removed. It does not move implicitly into or out of `for_each`, or between `count` and `for_each`; those need `moved` blocks. [RES V10][d1-res]. New fact recorded as C-76.] +- There is no implicit move into or out of `for_each`, or between `count` and `for_each`. Such a change is a delete and a create unless a `moved` block says otherwise. [DECIDED 24 Oct 2026: C-76. No predicate changes.] + +### 2.4 Result values and combination + +Results are PASS, FAIL, UNKNOWN, UNSUPPORTED and VERIFIER_ERROR, with Doc 09 §4 meanings: +- UNKNOWN means the required facts exist in the supported model but are unresolved. +- UNSUPPORTED means the facts depend on a construct outside the supported model (Doc 04 §17). +- An implementation that throws, times out or produces malformed output MUST return VERIFIER_ERROR for that invariant evaluation (Doc 09 §37). It MUST NOT return any other value. +- UNKNOWN, UNSUPPORTED and VERIFIER_ERROR are never PASS. + +Each invariant section defines how its sub-results combine, because existential and universal predicates combine differently. + +### 2.5 CIDRs and protocols + +**CIDRs.** +- IPv4 and IPv6 CIDRs are parsed strictly. A CIDR that is syntactically invalid, or has host bits set, makes the rule containing it UNSUPPORTED. [VERIFIED AT D1: CONFIRMED (V08): `terraform validate` rejects host-bit and malformed IPv4 and IPv6 CIDRs in `aws_security_group_rule`, in inline `aws_security_group` rules and in `aws_vpc.cidr_block`. [RES V08][d1-res].] +- Order and duplicates inside CIDR lists never matter (Doc 04 §8.1). +- "Covers" means set containment of address ranges. A list of CIDRs covers a range R when the union of the listed ranges contains R. + +**Protocols.** `protocol` is compared case-insensitively. [VERIFIED AT D1: CONFIRMED (V09): upper-case values are accepted; the plan JSON shows the normalised lower-case name (`-1` for all, a name for a protocol number). [RES V09][d1-res]. See C-75.] It canonicalises as: + +| Configured value | Canonical | Ports | +|---|---|---| +| `"-1"`, `"all"` | ALL | every port; `from_port`/`to_port` ignored | +| `"tcp"`, `"6"` | TCP | `[from_port, to_port]`, inclusive | +| `"udp"`, `"17"` | UDP | not TCP | +| `"icmp"`, `"1"` | ICMP | not TCP | +| `"icmpv6"`, `"58"` | ICMPV6 | not TCP | +| any other number | that protocol | not TCP | + +For TCP, `from_port > to_port` makes the rule UNSUPPORTED. + +`permits_tcp(r, p)` is true when protocol(r) = ALL, or when protocol(r) = TCP and `from_port ≤ p ≤ to_port`. + +### 2.6 Canonical security-group rule set + +AWS security groups contain **allow rules only**; there are no deny rules. [VERIFIED AT D1: CONFIRMED (V11): Amazon VPC User Guide, "Security group rules": "You can specify allow rules, but not deny rules." [RES V11][d1-res].] Adding a rule can only widen what a group permits. §3 and §6 depend on this. + +**Rule sets.** For each configured `aws_security_group` instance *g*: +- `In(g)` is *g*'s inline `ingress` blocks, plus every `aws_security_group_rule` with `type = "ingress"` whose `security_group_id` resolves to a reference to *g*. +- `Out(g)` is the same for `egress`. + +**A canonical rule *r*** carries: +- protocol; +- port range; +- `v4(r)` (`cidr_blocks`); +- `v6(r)` (`ipv6_cidr_blocks`); +- `src_sg(r)`: the security-group references in the inline `security_groups`, or in `source_security_group_id`; +- `self(r)`; +- `pl(r)` (`prefix_list_ids`). + +**Indeterminate rules.** A rule is *indeterminate* when: +- its protocol or ports are unresolved; +- any source list is unresolved; +- it has a non-empty `pl(r)` (prefix-list contents are not in the configuration); +- or it comes from an indeterminate resource or block (§2.3). + +**Unresolved targets.** An `aws_security_group_rule` whose `security_group_id` is external or unresolved belongs to a pseudo-group keyed by that value: the literal ID, or `UNRESOLVED:`. + +**MIXED groups.** A group *g* is **MIXED** when it has at least one inline rule block (form *blocks*; ingress or egress) and is also the target of at least one `aws_security_group_rule`. The provider documents that combining the two forms on one group causes conflicting rule management, so the applied rule set is not determined by the configuration. [VERIFIED AT D1: CONFIRMED (X01): provider documentation v6.53.0 (`security_group`, `security_group_rule`): combining inline rules with `aws_security_group_rule` "may cause rule conflicts, perpetual differences, and result in rules being overwritten". [RES X01][d1-res].] + +**Inline-rule forms (C-84).** For each direction (ingress, egress), a configured group *g* uses one of three forms in the configuration: +- *blocks*: one or more inline `ingress` (or `egress`) blocks; +- *explicit empty*: `ingress = []` (or `egress = []`); +- *absent*: the argument is not written. + +The provider processes these arguments in attributes-as-blocks mode. An absent argument leaves the existing rules in place; an explicit empty list removes them (Terraform 1.15.x language documentation, "Attributes as Blocks", ; provider 6.53.0 `security_group` documentation, ; evidence record [RES V12][d1-res]; corroborated by the open provider issue ). So: +- *explicit empty*: *g* has no inline rules in that direction; +- *absent*, and *g* has no parent counterpart (a baseline, or a group the candidate creates): no inline rules, because the group is deployed fresh; +- *absent*, and *g*'s parent counterpart (after following moves, §2.3) used *explicit empty* or was *absent*: no inline rules; +- *absent*, and *g*'s parent counterpart used *blocks*: *g* is **RETAINED-INLINE** in that direction. Its applied rules are the parent's rules, which the configuration no longer shows. §3.4 and §6.4 make results that read that direction UNSUPPORTED. + +When the parent is a Trusted State, it cannot itself be RETAINED-INLINE for a required invariant, because that result would have blocked its promotion. In TerraPreserve trajectories, no generated step is RETAINED-INLINE (D0 amendments A10). In both cases one parent is enough. Rules created outside the configuration are not modelled. **[PAPER]** + +**MIXED, explicit empty (C-84).** A group is also MIXED when it uses *explicit empty* in a direction and is the target of at least one `aws_security_group_rule` of that direction. The explicit empty list tells the group resource to remove rules that the separate resource adds, so the applied rule set is not determined by the configuration (provider 6.53.0 documentation, mixing warning, X01; documentary evidence only, not observed with `apply`). **[PAPER]** + +**Default egress.** When Terraform creates a security group inside a VPC, it removes AWS's default allow-all egress rule. `Out(g)` is therefore exactly what the configuration declares, and may be empty. This comes from the provider's `aws_security_group` documentation (note on egress rules). [VERIFIED AT D1: CONFIRMED (V06): the note is in the v6.53.0 documentation and the create function revokes the default IPv4 and IPv6 egress rules. Documentary evidence only; this cannot be observed without `apply`. [RES V06][d1-res].] + +### 2.7 Unsupported constructs + +A resource type outside §1.3 changes a result only if it appears in the invariant's **relevant-unsupported list**. Every other unsupported type is declared irrelevant to that invariant. This is an explicit modelling assumption, and the paper must state it as a limitation. **[PAPER]** + +| Invariant | Relevant-unsupported types (presence anywhere in the configuration) | +|---|---| +| INV-SEC-001, INV-SEC-002 | `aws_vpc_security_group_ingress_rule`, `aws_default_security_group`, `aws_vpc_security_group_rules_exclusive` | +| INV-SEC-003 | none | +| INV-FUNC-001 | `aws_vpc_security_group_ingress_rule`, `aws_vpc_security_group_egress_rule`, `aws_default_security_group`, `aws_network_interface`, `aws_network_interface_attachment`, `aws_network_interface_sg_attachment`, `aws_network_acl`, `aws_network_acl_rule`, `aws_network_acl_association`, `aws_default_network_acl`, `aws_route`, `aws_default_route_table`, `aws_main_route_table_association`, `aws_vpc_ipv4_cidr_block_association`, `aws_vpc_peering_connection`, `aws_ec2_transit_gateway_vpc_attachment`, `aws_vpc_endpoint`, `aws_vpc_security_group_rules_exclusive`, `aws_vpc_security_group_vpc_association`, `aws_vpn_gateway_route_propagation`, `aws_vpc_route_server_propagation`, `aws_default_subnet`, `aws_default_vpc`, `aws_vpc_peering_connection_accepter`, `aws_vpc_peering_connection_options`, `aws_ec2_transit_gateway_vpc_attachment_accepter` | + +[VERIFIED AT D1: CHANGED (V12, heuristic): the lists are not shown to be complete. A keyword heuristic over the 1,678 resource types of provider 6.53.0 lists candidates the authors must decide on before the freeze, for example `aws_vpc_security_group_rules_exclusive`, `aws_vpc_security_group_vpc_association`, `aws_vpn_gateway_route_propagation`, `aws_vpc_route_server_propagation` and `aws_default_subnet`. [RES V12][d1-res].] [DECIDED 24 Oct 2026, C-74: the candidates were added as shown. The routing and VPC types join INV-FUNC-001 only; `aws_vpc_security_group_rules_exclusive` joins all three security-group lists because it removes rules the configuration does not list. The lists remain a heuristic result, not a proof of completeness. Over-approximation is intentional: UNSUPPORTED never passes.] **[PAPER]** + +**Tolerated type.** `aws_db_subnet_group` is tolerated, not relevant, under C-15 and §6.2. RDS placement is taken from the RDS security groups' VPC, and the subnet group's subnets are not modelled. The evidence MUST record this assumption. + +### 2.8 Configurations with errors + +If the configuration fails `terraform validate` with the pinned versions, every invariant is UNSUPPORTED. A configuration Terraform rejects is outside the model. D0 Gate 2 keeps such configurations out of TerraPreserve; this rule covers LLM candidates. + +### 2.9 Footprint and relevance (used by N-04 impact metrics) + +Two configurations (parent and candidate) are compared instance by instance, after following moves (§2.3), on **resolved** attribute values. + +**Changed elements.** A footprint element is *changed* when any of these holds: +- it is created or deleted; +- its resolved value differs; +- it is resolved on one side and unresolved on the other, or unresolved on both. Unresolved values are treated as changed. + +**[v1.1] Clarification (C-179, wording only).** In the footprint comparison, an argument that neither configuration writes compares as absent on both sides and is not changed. The predicates still treat such a value as §2.2 says. The parent counterpart's inline-rule form (§3.5, §6.6) is compared through what it decides: whether the group is RETAINED-INLINE in that direction (§2.6). A baseline has no parent, so this is false for every group of a baseline. + +**Footprint.** An invariant's **footprint** is the set of elements listed in its section (§3.5, §5.4, §6.6). A change is **relevant** to an invariant when it changes at least one element of that invariant's footprint. + +**Completeness property.** If an invariant's result differs between parent and candidate, at least one footprint element MUST have changed. A counterexample is a registry defect that must be fixed before D6 (Part B, A2). + +### 2.10 Evidence requirements (all invariants) + +Every result MUST produce a Doc 11 §25 `VerificationEvidence` record that carries: +- **subject identity:** `invariant_id` and `invariant_version`. This settles the design question in C-62; P5 implements it; +- `verifier_id` and `verifier_version` (§10); +- `evidence_level = "L1"`; +- the content hash of the evaluated configuration; +- the result, and for INV-SEC-001/002 the result of each clause; +- the observations listed in the invariant's section; +- an `assumptions` list naming every modelling assumption the evaluation relied on (for example `"C-15: RDS VPC from security groups"`, `"default network ACL assumed"`). + +**Supersession.** Evidence for one subject never supersedes evidence for another. Supersession requires equal `invariant_id`, `invariant_version` and `verifier_id` (C-62). + +--- + +## 3. INV-SEC-001: no public ingress to TCP/22 + +3.1 **Identity.** `INV-SEC-001`, version 2. **[v1.1]** (version 1 in registry v1.0; §3.3 changed.) Name: "No public SSH ingress". Category SECURITY. + +3.2 **Statement.** No security group in the configuration admits TCP port 22 from the entire IPv4 internet, or from the entire IPv6 internet. + +3.3 **Predicate.** The predicate is `PIP(22)`, the public-ingress predicate for port *p*, with two clauses: + +``` +For each security group g (configured groups and pseudo-groups): + D(g) = { r in In(g) : r determinate and permits_tcp(r, p) } + IPv4 clause: violates4(g) := union of v4(r) over r in D(g) covers 0.0.0.0/0 + IPv6 clause: violates6(g) := union of v6(r) over r in D(g) covers ::/0 + possible4(g) := exists indeterminate r in In(g) that could permit TCP/p + (its protocol or ports unresolved, or they permit p) and + (its IPv4 sources are unresolved or include a prefix list, + or its resolved IPv4 sources, together with the union of v4(r') + over r' in D(g), cover 0.0.0.0/0). + possible6(g) is the same for IPv6 sources and ::/0. +``` + +**[v1.1] Note on `possible` (C-150, C-178).** In v1.0 an indeterminate rule was *possible* only when its sources were unresolved or included a prefix list. A rule whose protocol or ports are unresolved but whose source is the whole internet, for example `from_port = var.p` with `cidr_blocks = ["0.0.0.0/0"]`, was therefore neither in `D(g)` nor *possible*, and the clause was PASS. Such a rule may open the port to the internet, and uncertainty is never a pass (§2.4), so in v1.1 it is *possible* and the clause is UNKNOWN. Its resolved sources count together with those of `D(g)`, because rules are allow-only (§2.6). A rule whose resolved sources do not cover the address family even with `D(g)` (for example `10.0.0.0/8` alone) is still not *possible*. INV-SEC-001 and INV-SEC-002 are version 2; their results differ from version 1 only for such rules. + +**Scope.** Every configured `aws_security_group` instance, plus every pseudo-group, whether or not any instance or database uses it. **[PAPER]** +- Doc 09 §8 scopes the predicate to rules "relevant to the protected workload". This registry is stricter on purpose. It matches D0's F6 unsafe example (a new SG open on port 22) and Checkov's per-group check. +- Because of this, a change to which security groups an instance uses does not change this invariant's result. + +**What counts as public.** Doc 09 §8 says "0.0.0.0/0 or equivalent public IPv4 scope". This registry makes that precise: +- The source CIDRs of one group's port-*p* rules count as public **when together they cover** `0.0.0.0/0`. A split such as `0.0.0.0/1` plus `128.0.0.0/1` therefore FAILs. **[PAPER]** +- Narrower public ranges (for example a single `/8`) are not violations in v1. +- Coverage split across two different groups is not detected in v1. + +3.4 **Results.** First compute the result of each clause: + +| Condition (evaluated in this order) | Clause result | +|---|---| +| Some group *g* has `violates(g)` (and *g* is not MIXED) | FAIL | +| Some group is MIXED; some group is RETAINED-INLINE in ingress (§2.6, C-84); some ingress rule is UNSUPPORTED (§2.5); or a relevant-unsupported type (§2.7) is present | UNSUPPORTED | +| Some group has `possible(g)` | UNKNOWN | +| Otherwise | PASS | + +A RETAINED-INLINE group is not evaluated by `violates(g)`, because its rules are not known. A RETAINED-INLINE group cannot give FAIL or PASS; another group's violation still gives FAIL. + +Then the invariant result: +- **FAIL** if either clause FAILs, because a single violating rule cannot be undone by other allow-only rules; +- otherwise **UNSUPPORTED**, then **UNKNOWN**, then **PASS**, taking the worst clause in that order; +- **VERIFIER_ERROR** overrides all of the above (§2.4). + +The evidence reports the IPv4 and IPv6 clauses separately (C-13). + +**Observations to record:** +- for each FAIL: the group, the contributing rule addresses, their CIDRs and port ranges; +- the MIXED groups; +- the RETAINED-INLINE groups and their direction (C-84); +- the indeterminate rules, with the reason for each; +- the relevant-unsupported resources found; +- the number of groups evaluated. + +3.5 **Footprint.** +- `aws_security_group`: existence, and every field of each inline `ingress` block (`from_port`, `to_port`, `protocol`, `cidr_blocks`, `ipv6_cidr_blocks`, `prefix_list_ids`, `security_groups`, `self`). Also *whether any inline `egress` block exists*, because it affects MIXED status; the contents of egress blocks are not in the footprint. Also the form (*blocks*, *explicit empty*, *absent*) of each direction, and the parent counterpart's ingress form (C-84). +- `aws_security_group_rule`: existence, and `type`, `from_port`, `to_port`, `protocol`, `cidr_blocks`, `ipv6_cidr_blocks`, `prefix_list_ids`, `source_security_group_id`, `self` and `security_group_id`. +- The existence of each relevant-unsupported type in §2.7. +- **Not in the footprint:** `vpc_id`, `name`, `name_prefix`, `description`, `tags`, egress contents, and any instance or database security-group attachment. + +3.6 **Verifier and evidence.** L1. Verifier `dail.verify.public_ingress`, version `1`, run with parameter `p = 22`. + +3.7 **Checkov (advisory only, C-12).** +- `CKV_AWS_24`, "Ensure no security groups allow ingress from 0.0.0.0:0 to port 22". Checkov's policy index lists it for `aws_security_group` and `aws_security_group_rule`. +- Checkov tests a single rule's CIDR, not the union of a group's rules, and has no IPv6 clause here. Disagreements are therefore expected, are recorded, and never change a result. +- [VERIFIED AT D1: CHANGED (V04): Checkov 3.3.30 also scans `aws_vpc_security_group_ingress_rule`, tests `::/0` (but not for that resource), and ignores the protocol unless it is `-1`. The first bullet (resource list) and the words "has no IPv6 clause here" above are affected; both are left as written. [RES V04][d1-res]. See C-73.] + +--- + +## 4. INV-SEC-002: no public ingress to TCP/5432 + +4.1 **Identity.** `INV-SEC-002`, version 2. **[v1.1]** (version 1 in registry v1.0; §3.3, which §4.2 applies, changed.) Name: "No public PostgreSQL ingress". Category SECURITY. + +4.2 **Statement, predicate, results, footprint and evidence.** Identical to §3.2–§3.6 with `p = 5432`. The scope is every security group, not only the database's (D0 Decision 4). + +4.3 **Why it exists.** It catches the regression D0 Decision 4 describes: a "repair" that restores INV-FUNC-001 by opening 5432 to the internet. + +4.4 **Checkov.** No Checkov policy dedicated to port 5432 was found in the policy listings searched for this draft. [VERIFIED AT D1: CONFIRMED (V02): none; custom predicate only (C-14). No Checkov 3.3.30 check mentions port 5432, and no check distinguishes a public from a private 5432 rule. [RES V02][d1-res].] + +--- + +## 5. INV-SEC-003: RDS instances are not publicly accessible + +5.1 **Identity.** `INV-SEC-003`, version 1. Name: "RDS not publicly accessible". Category SECURITY. + +5.2 **Statement and predicate.** For every configured `aws_db_instance` instance *d*, `publicly_accessible(d)` is false. +- An absent attribute is false. The provider default is `false`; the provider schema and third-party rule documentation agree. [VERIFIED AT D1: CONFIRMED (V05): `Default: false` in the v6.53.0 source; the plan JSON shows `false` for an unset attribute. [RES V05][d1-res]. See C-75.] +- With zero `aws_db_instance` instances the predicate holds vacuously. The evidence records the count, 0. + +5.3 **Results.** + +| Condition (in this order) | Result | +|---|---| +| Some instance has resolved `publicly_accessible = true` | FAIL | +| Some instance has an unresolved `publicly_accessible`, or `aws_db_instance` is indeterminate (§2.3) | UNKNOWN | +| Otherwise | PASS | + +**Observations:** each instance's address and its resolved value (or the reason it is unresolved). + +**Out of scope:** other RDS resource types, such as `aws_rds_cluster_instance`, are not covered by this invariant. + +5.4 **Footprint.** `aws_db_instance` existence, and its `publicly_accessible` attribute. + +5.5 **Verifier and evidence.** L1. Verifier `dail.verify.rds_public_flag`, version `1`. + +5.6 **Checkov (advisory).** +- Candidate: `CKV_AWS_17`. The policy index lists it for `aws_db_instance` as data "not public accessible". +- [VERIFIED AT D1: CONFIRMED (V03): `CKV_AWS_17` inspects `publicly_accessible` and FAILs only on `true`; absent PASSes; an unresolved reference gives no result. It also scans `aws_rds_cluster_instance`. [RES V03][d1-res].] + +--- + +## 6. INV-FUNC-001: EC2 → RDS on TCP/5432 (configuration level) + +6.1 **Identity.** `INV-FUNC-001`, version 1. Name: "Application can reach database on TCP/5432". Category FUNCTIONAL. + +**Binding.** Each scenario binds two **endpoints** by full instance address: +- the source `S`, an `aws_instance`; +- the destination `D`, an `aws_db_instance`. + +For example, `S = aws_instance.app` and `D = aws_db_instance.database`. Endpoints are followed across moves (§2.3). + +**[PAPER]** A PASS means the configuration-level prerequisites hold within this model (Doc 09 §9). It does not mean packets flow at runtime. + +6.2 **Network model** (C-15, made precise): +- **M1, RDS network context.** `VPC(D)` is the VPC that all of `D`'s security groups (`vpc_security_group_ids`) belong to. RDS subnets are not modelled. `aws_db_subnet_group` is tolerated (§2.7). The assumption, recorded in evidence, is that AWS requires the instance's security groups and its subnet group to be in the same VPC. [OPEN AFTER D1: UNRESOLVED (X02): no AWS RDS page read states the requirement, and AWS documents a Security Group VPC Association feature under which a group can serve resources in other VPCs. M1 stays an uncited assumption. [RES X02][d1-res]. See C-77.] [DECIDED 24 Oct 2026, C-77: M1 stays a recorded assumption. `aws_vpc_security_group_vpc_association` is in INV-FUNC-001's relevant-unsupported list (§2.7), so a configuration using that feature is UNSUPPORTED.] **[PAPER]** +- **M2, EC2 placement.** `VPC(S)` is the `vpc_id` of the configured `aws_subnet` that `S.subnet_id` references. +- **M3, intra-VPC routing.** Routing inside a VPC is the VPC **local route**. AWS documents that the local route cannot be deleted, but **its target can be replaced, and more-specific routes can redirect east–west traffic to a middlebox** (network interface, Gateway Load Balancer endpoint or NAT gateway). Such routing is not modelled. Therefore **any route in any `aws_route_table` of `VPC(D)` whose destination is contained in the VPC CIDR and whose target is not `local` makes the result UNSUPPORTED.** Routes whose destination is wider than the VPC CIDR (for example `0.0.0.0/0` to an internet gateway) never apply to intra-VPC traffic, because the most specific route wins. **[PAPER]** +- **M4, network ACLs.** Network ACLs are not modelled. When no NACL-related type from §2.7 is present, every subnet is assumed to use the default network ACL, which AWS documents as allowing all inbound and outbound traffic. That assumption is recorded in evidence. If any NACL-related type is present, the result is UNSUPPORTED (§2.7). +- **M5, statefulness and protocol.** Security groups are stateful, so only `S`'s egress and `D`'s ingress are evaluated. Only IPv4 is modelled for this invariant. + +6.3 **Predicate.** `REACH(S, D, 5432)` holds when all of the following hold: + +``` +E1 S and D both exist in the configuration. +E2 The listener port: D.port, if set, equals 5432; if D.port is absent, D.engine is + "postgres". [VERIFIED AT D1: CONFIRMED (V07): AWS CreateDBInstance documents 5432 for RDS for PostgreSQL. The provider sets no default, so the plan JSON shows an unset `port` as unknown. [RES V07][d1-res]. See C-75.] +E3 D has a non-empty, resolved vpc_security_group_ids. Each entry references a configured + aws_security_group with a resolved vpc_id, and they all share one VPC(D). +E4 S has a resolved subnet_id that references a configured aws_subnet, and VPC(S) = VPC(D). +E5 Some security group of S permits egress to D: + exists g in SG(S), r in Out(g) with permits_tcp(r, 5432) and + (src_sg(r) contains a group in SG(D)) or (v4(r) covers CIDR(VPC(D))) + where SG(S) is S.vpc_security_group_ids. +E6 Some security group of D permits ingress from S: + exists h in SG(D), r in In(h) with permits_tcp(r, 5432) and + (src_sg(r) contains a group in SG(S)) or (self(r) and h is in SG(S)) + or (v4(r) covers ADDR(S)) + where ADDR(S) = S.private_ip/32 if resolved, else the cidr_block of S's subnet. +E7 M3 and M4 hold: no intra-VPC non-local route and no NACL-related type. +``` + +6.4 **Results.** Evaluate in this order. The first row that applies gives the result: + +| # | Condition | Result | +|---|---|---| +| 1 | `S` or `D` is absent (deleted, with no move): the protected endpoint is gone | FAIL | +| 2 | A relevant-unsupported type is present; any route of M3 exists; `S` uses name-based `security_groups`; `D` or `S` has no `vpc_security_group_ids` (default security group not modelled); `S` has no `subnet_id` (default VPC not modelled); any group in `SG(S) ∪ SG(D)` is MIXED; a group in `SG(D)` is RETAINED-INLINE in ingress, or a group in `SG(S)` is RETAINED-INLINE in egress (§2.6, C-84); `S` has a `network_interface` or `primary_network_interface` block (C-78); an `aws_route_table` whose `vpc_id` is `VPC(D)` sets `propagating_vgws` (written in the configuration, even as an empty list) (C-78); or an engine, port or rule value is UNSUPPORTED (§2.5) | UNSUPPORTED | +| 3 | E2 is definitely false: `D.port` resolves to a value other than 5432, or `port` is absent and `D.engine` resolves to an engine other than `postgres` | FAIL | +| 4 | E3 or E4 fails because a needed value is unresolved, or an endpoint is indeterminate | UNKNOWN | +| 5 | E3 holds and `VPC(S) ≠ VPC(D)` | FAIL | +| 6 | E5 and E6 both hold using determinate rules only | PASS | +| 7 | E5 or E6 does not hold with determinate rules, but an indeterminate rule (including one in a pseudo-group whose target is unresolved) could satisfy it | UNKNOWN | +| 8 | E5 or E6 does not hold, and an egress CIDR **partly** covers `CIDR(VPC(D))`, or an ingress CIDR partly covers `ADDR(S)` | UNKNOWN | +| 9 | Otherwise | FAIL | + +**Why rows 7 and 8 return UNKNOWN.** Rules are allow-only (§2.6), so an unresolved rule could only add permission. A FAIL is therefore reported only when no unresolved rule could supply the missing permission. Partial coverage (row 8) cannot be decided because RDS subnets (C-15) and unassigned instance addresses are not modelled. **[PAPER]** + +**Observations to record:** +- the evaluated path: `S`, its subnet, `VPC(S)`, `SG(S)`, the egress rule matched, `SG(D)`, the ingress rule matched, `VPC(D)` and the port; +- for each failing row: the reason; +- for row 2, which RETAINED-INLINE group, network interface block or `propagating_vgws` caused it (C-78, C-84); +- the `assumptions` list (M1, M4, IPv4 only). + +6.5 **Worked cases** (the canonical topology, Doc 04 Appendix B): +- **PASS.** The database group admits TCP/5432 from the app group by reference, and the app group's egress is `-1` to `0.0.0.0/0`. +- **The canonical regression is FAIL.** A candidate removes `app_to_db_5432` while fixing SSH, so row 9 applies. +- **A route edit inside the VPC.** A candidate replaces `0.0.0.0/0 → igw` with nothing. The result is unchanged, because that route is not inside the VPC CIDR (M3). + +6.6 **Footprint**, given the bindings `S` and `D` (both parent and candidate values count): +- `S`: existence, `subnet_id`, `vpc_security_group_ids`, `security_groups`, `private_ip`, `network_interface`, `primary_network_interface` (presence and contents). +- `D`: existence, `vpc_security_group_ids`, `port`, `engine`. +- The `aws_subnet` that `S` references: existence, `vpc_id`, `cidr_block`. +- The `aws_vpc` that `VPC(S)` or `VPC(D)` names: existence, `cidr_block`. +- Each `aws_security_group` in `SG(S) ∪ SG(D)`: existence and `vpc_id`; for `SG(S)`, every field of each egress block; for `SG(D)`, every field of each ingress block; and the presence of inline blocks (MIXED status); the form of each direction of each group in `SG(S) ∪ SG(D)`, and the parent counterpart's egress form for `SG(S)` and ingress form for `SG(D)` (C-84). +- Each `aws_security_group_rule` whose target is in `SG(S) ∪ SG(D)`, or is unresolved: existence and all rule fields (§3.5). +- Each `aws_route_table` whose `vpc_id` is `VPC(D)`: every route whose destination is contained in that VPC's CIDR, plus the existence of such routes, and its `propagating_vgws`. +- The existence of each relevant-unsupported type (§2.7), and `moved` blocks naming `S` or `D`. +- **Not in the footprint:** + - routes whose destination is wider than the VPC CIDR; + - `aws_route_table_association` (no route that could matter depends on it in v1, because M3 checks every route table of the VPC); + - `aws_internet_gateway`; + - `publicly_accessible`; + - instance type, tags and names. + +6.7 **Verifier and evidence.** L1. Verifier `dail.verify.reachability_cfg`, version `1`. + +6.8 **Checkov.** None. This invariant is a custom predicate (D0 Decision 4). + +--- + +## 7. Spec consistency notes (for the register; not part of the predicates) + +7.1 **Doc 04 §7.6** lists `security_group_ids` for `aws_instance`. The provider's VPC-placement argument is `vpc_security_group_ids`; `security_groups` takes names. [VERIFIED AT D1: CONFIRMED (V13): `aws_instance` has no `security_group_ids`; `vpc_security_group_ids` holds IDs and `security_groups` holds names. Doc 04 errata row: C-79. [RES V13][d1-res].] + +7.2 **Doc 04 §7.8** lists `security_group_id(s)` as the SG-to-SG source field of `aws_security_group_rule`. The provider argument is `source_security_group_id`. [VERIFIED AT D1: CONFIRMED (V14): `source_security_group_id` is the source; `security_group_id` is required and names the rule's own group. Doc 04 errata row: C-80. [RES V14][d1-res].] + +7.3 **Doc 09 §8 versus §3.3.** Doc 09 §8 scopes INV-SEC-001 to the protected workload; this registry uses every group (C-64). Doc 08 §14's example path (security-group change → EC2 → invariant) is therefore not relevant to SEC-001 v1. That path only affects DAIL's impact precision, not safety. + +--- + +## 8. Conformance vectors + +Each vector is a minimal configuration difference from the canonical topology. Both DAIL and the oracle MUST reproduce these results. D2 turns them into fixtures. A vector that names a parent is evaluated together with that parent (§2.1, §2.6); every other vector is a baseline with no parent. + +| # | Invariant | Configuration fact | Expected | +|---|---|---|---| +| S1 | SEC-001 | Inline ingress `tcp 22–22` from `0.0.0.0/0` | FAIL (IPv4) | +| S2 | SEC-001 | Separate rule `protocol "-1"`, ports `0–0`, `0.0.0.0/0` | FAIL | +| S3 | SEC-001 | `tcp 0–65535` from `::/0` only | FAIL (IPv6 clause); IPv4 clause PASS | +| S4 | SEC-001 | One rule `tcp 22` from `0.0.0.0/1` and `128.0.0.0/1` | FAIL | +| S5 | SEC-001 | Same group: rule A `tcp 22` from `0.0.0.0/1`; rule B `tcp 20–30` from `128.0.0.0/1` | FAIL | +| S6 | SEC-001 | Group A `tcp 22` from `0.0.0.0/1`; group B `tcp 22` from `128.0.0.0/1` | PASS (documented v1 limitation) | +| S7 | SEC-001 | `tcp 22` from `10.0.0.0/16` | PASS | +| S8 | SEC-001 | `udp 22` from `0.0.0.0/0` | PASS | +| S9 | SEC-001 | `tcp 22` from `var.ssh_cidr`, which has no value | UNKNOWN | +| S10 | SEC-001 | `tcp 22` with `prefix_list_ids` only | UNKNOWN | +| S11 | SEC-001 | Group with inline ingress and also targeted by an `aws_security_group_rule` | UNSUPPORTED | +| S12 | SEC-001 | A group used by nothing has `tcp 22` from `0.0.0.0/0` | FAIL | +| S13 | SEC-001 | Configuration contains `aws_vpc_security_group_ingress_rule`; nothing else violates | UNSUPPORTED | +| S14 | SEC-002 | The application group opens `tcp 5432` to `0.0.0.0/0` | FAIL | +| R1 | SEC-003 | `publicly_accessible` absent | PASS | +| R2 | SEC-003 | `publicly_accessible = true` | FAIL | +| R3 | SEC-003 | `publicly_accessible = var.public`, with no value | UNKNOWN | +| R4 | SEC-003 | No `aws_db_instance` at all | PASS (vacuous; count 0) | +| F1 | FUNC-001 | Canonical: ingress by SG reference, egress `-1` to `0.0.0.0/0` | PASS | +| F2 | FUNC-001 | `app_to_db_5432` removed | FAIL | +| F3 | FUNC-001 | Ingress `tcp 5432` from `10.0.1.0/24` (the app subnet) | PASS | +| F4 | FUNC-001 | As F3, but `S` moved to a subnet `10.0.3.0/24` in the same VPC | FAIL | +| F5 | FUNC-001 | The app group has no egress at all | FAIL | +| F6 | FUNC-001 | App egress only `tcp 5432` to `10.0.2.0/24`, a database subnet | UNKNOWN (row 8) | +| F7 | FUNC-001 | A route table has `10.0.2.0/24 → network_interface_id` | UNSUPPORTED | +| F8 | FUNC-001 | Route `0.0.0.0/0 → igw` removed | PASS | +| F9 | FUNC-001 | Configuration contains `aws_network_acl` | UNSUPPORTED | +| F10 | FUNC-001 | `D` deleted | FAIL | +| F11 | FUNC-001 | `D.port = 3306` | FAIL | +| F12 | FUNC-001 | `D` has no `vpc_security_group_ids` | UNSUPPORTED | +| F13 | FUNC-001 | Ingress from `10.0.1.0/25`, `S.private_ip` unset | UNKNOWN; with `S.private_ip = 10.0.1.10`: PASS | +| F14 | FUNC-001 | `S` moved to a subnet of a second VPC | FAIL | +| F15 | FUNC-001 | `aws_db_subnet_group` present, all else canonical | PASS, with the assumption recorded | +| S15 | SEC-001 | Configuration contains `aws_vpc_security_group_rules_exclusive`; nothing else violates | UNSUPPORTED | +| S16 | SEC-001 | Parent: a group has an inline `ingress` block (no public 22). Candidate: same group, `ingress` argument absent; nothing else violates | UNSUPPORTED (RETAINED-INLINE) | +| S17 | SEC-001 | As S16, but the candidate writes `ingress = []` | PASS | +| S18 | SEC-001 | Baseline: a group with no `ingress` argument and no `aws_security_group_rule` targeting it; nothing else violates | PASS | +| S19 | SEC-001 | A group writes `ingress = []` and is the target of an ingress `aws_security_group_rule`; nothing else violates | UNSUPPORTED (MIXED) | +| S20 | SEC-001 | As S16, and another group has `tcp 22` from `0.0.0.0/0` | FAIL | +| F16 | FUNC-001 | `S` has a `network_interface` block | UNSUPPORTED | +| F17 | FUNC-001 | An `aws_route_table` of `VPC(D)` sets `propagating_vgws` | UNSUPPORTED | +| F18 | FUNC-001 | Configuration contains `aws_vpc_security_group_vpc_association` | UNSUPPORTED | +| F19 | FUNC-001 | Parent: the database group admits TCP/5432 from the app group by an inline `ingress` block. Candidate: that group's `ingress` argument absent | UNSUPPORTED (RETAINED-INLINE) | +| F20 | FUNC-001 | Configuration contains `aws_default_vpc` | UNSUPPORTED | + +--- + +## 9. Footprint summary (input to N-04) + +| Invariant | Footprint (§ reference) | +|---|---| +| INV-SEC-001 | §3.5: SG ingress fields, SG-rule fields, inline-egress presence, inline-rule forms (C-84), relevant-unsupported presence | +| INV-SEC-002 | Same as SEC-001 | +| INV-SEC-003 | §5.4: `aws_db_instance` existence and `publicly_accessible` | +| INV-FUNC-001 | §6.6: endpoints, S's subnet, VPC, SG(S) egress, SG(D) ingress, rules targeting them, inline-rule forms (C-84), intra-VPC routes, S network interfaces and `propagating_vgws` (C-78), relevant-unsupported presence, moves | + +--- + +## 10. Verifier identities + +| Invariant | DAIL verifier ID | Version | Level | +|---|---|---|---| +| INV-SEC-001 | `dail.verify.public_ingress` (p = 22) | 1 | L1 | +| INV-SEC-002 | `dail.verify.public_ingress` (p = 5432) | 1 | L1 | +| INV-SEC-003 | `dail.verify.rds_public_flag` | 1 | L1 | +| INV-FUNC-001 | `dail.verify.reachability_cfg` | 1 | L1 | + +The oracle uses its own IDs under the `tp.oracle.` prefix. Oracle results are L2 (Doc 09 §10) and are research labels only (ADR-010). + +--- + +## 11. Decisions proposed by this document (register rows) + +| Proposed ID | Decision | Marker | +|---|---|---| +| C-64 | The SEC public-ingress semantics: every security group is in scope, attached or not (§3.3). "Equivalent public scope" means a group's port-*p* rule CIDRs together cover `0.0.0.0/0` (or `::/0`). Unresolved rules are handled monotonically (§2.6, §3.4). MIXED groups are UNSUPPORTED. | [PAPER] | +| C-65 | Unsupported-construct policy: closed relevant-unsupported lists per invariant; every other type is declared irrelevant (§2.7). | [PAPER] | +| C-66 | INV-FUNC-001 model under C-15: endpoint binding, with absence giving FAIL; the E1–E7 predicate; partial coverage gives UNKNOWN; non-local intra-VPC routes give UNSUPPORTED; default NACL assumed only when no NACL type is present; IPv4 only (§6). | [PAPER] | +| C-67 | `aws_db_subnet_group` is tolerated under C-15, and the canonical topology includes it with two database subnets in two Availability Zones (Part B, A6). This resolves the plan's open item on RDS subnet placement. | | +| C-68 | Evidence subject identity: VERIFICATION evidence carries `invariant_id` and `invariant_version`, and supersession requires equal subject and verifier (§2.10). This settles C-62's design; P5 implements it. | | +| C-74 | Relevant-unsupported lists: nine candidate types added (`aws_vpc_security_group_rules_exclusive` to all three security-group lists, the routing and VPC types to INV-FUNC-001 only); over-approximation is intentional (§2.7). Accepted 24 Oct 2026. | [PAPER] | +| C-76 | There is no implicit move into or out of `for_each`, or between `count` and `for_each` (§2.3); no predicate change. Accepted 24 Oct 2026. | | +| C-77 | M1 stays a recorded assumption, and `aws_vpc_security_group_vpc_association` joins INV-FUNC-001's relevant-unsupported list (§2.7, §6.2). Accepted 24 Oct 2026. | [PAPER] | +| C-78 | `network_interface` and `primary_network_interface` on `S`, and `propagating_vgws` on route tables of `VPC(D)`, give UNSUPPORTED for INV-FUNC-001 and enter its footprint (§6.4 row 2, §6.6). Accepted 24 Oct 2026. | | +| C-84 | Inline `ingress`/`egress` are attributes-as-blocks: an absent argument keeps the parent's rules (RETAINED-INLINE, UNSUPPORTED), explicit `= []` means no rules, and explicit `= []` plus a separate rule of that direction is MIXED (§2.6, §3.4, §6.4). Accepted 24 Oct 2026. | [PAPER] | +| C-85 | The registry is versioned by the git tag `registry-v1.0`; after the tag every change is a new file that bumps `invariant_registry_version` and each affected `invariant_version` (§1.4). Accepted 24 Oct 2026. | | + +--- + +## 12. Open items + +**Resolved at D1 (23 Oct 2026)** against Terraform 1.15.8, AWS provider 6.53.0 and Checkov 3.3.30. Evidence: [RESOLUTION.md at terrapreserve commit `ff70de82622b7d275bbf0f2490f0ce521786246e`][d1-res]. +- §2.3: implicit moves for `count` and `for_each`. CONFIRMED (V10); new fact C-76. Decided 24 Oct 2026. +- §2.5: host-bit CIDRs rejected (V08, CONFIRMED); upper-case protocols accepted (V09, CONFIRMED); plan-JSON facts C-75. +- §2.6: allow-only (V11), mixing warning (X01) and default-egress removal (V06): all CONFIRMED. +- §2.7: relevant-unsupported lists. CHANGED (V12, heuristic): candidates for the authors, C-74 and C-78. Decided 24 Oct 2026: the candidates were added to the lists (C-74). +- §5.2: `publicly_accessible` defaults to `false`. CONFIRMED (V05). +- §6.2 M1: RDS security groups and subnet group share a VPC. UNRESOLVED (X02); C-77. Decided 24 Oct 2026. +- §6.3 E2: the postgres default port is 5432. CONFIRMED (V07); the plan JSON shows an unset port as unknown (C-75). +- §3.7: Checkov `CKV_AWS_24` semantics. CHANGED (V04); C-73. §4.4: none, custom predicate only. CONFIRMED (V02). §5.6: `CKV_AWS_17`. CONFIRMED (V03). +- §7.1–7.2: Doc 04 field-name errata. CONFIRMED (V13, V14); C-79 and C-80. +- §6.6 and §2.6, attributes outside the footprints (C-78): DECIDED 24 Oct 2026. `network_interface`, `primary_network_interface` and `propagating_vgws` give UNSUPPORTED (§6.4 row 2); inline `ingress`/`egress` retention is C-84 (§2.6). +- Oracle input path (D0 amendments A3.4): an offline plan works (V01, CONFIRMED); C-75 lists what is unknown in the plan JSON. + +**Advisor confirmation** is needed for the [PAPER] items: §1.2, §2.6, §2.7, §3.3, §6.1, §6.2 M1 and M3, and §6.4 rows 7–8. + +[d1-res]: https://github.com/Ayushxsingh100/terrapreserve/blob/ff70de82622b7d275bbf0f2490f0ce521786246e/validation/d1_to_verify/RESOLUTION.md diff --git a/tests/promotion_pipeline.py b/tests/promotion_pipeline.py index b8a3890..22d0269 100644 --- a/tests/promotion_pipeline.py +++ b/tests/promotion_pipeline.py @@ -117,7 +117,12 @@ def parent_statuses(parent: str) -> dict[str, InvariantStatus]: def trusted_from( - parent: str, resources: Any, definitions: list[Invariant], *, state_id: str = PARENT_STATE + parent: str, + resources: Any, + definitions: list[Invariant], + *, + state_id: str = PARENT_STATE, + registry_version: int = 1, ) -> TrustedState: statuses = parent_statuses(parent) proofs = [ @@ -136,7 +141,7 @@ def trusted_from( invariant_proofs=proofs, evidence_refs=sorted({e for p in proofs for e in p.evidence_ids}), normalization_version=NORMALIZATION_VERSION, - invariant_registry_version=1, + invariant_registry_version=registry_version, now=NOW, state_id=state_id, ) @@ -151,13 +156,17 @@ def pipeline( parent_trusted: TrustedState | None = None, sequence: int = 1, patch_n: int = 7, + definitions: list[Invariant] | None = None, + registry_version: int = 1, ) -> PipelineRun: """Everything up to the verification report for one fixture that has a parent. The extra keywords are P6b's (they let a test run a second candidate beside the first, or from a state that a commit made): ``candidate_id``, ``sequence`` and ``patch_n`` name the candidate and its patch, and ``parent_trusted`` replaces the state that is otherwise built from the - parent directory. With none of them the behaviour is that of P6a.""" + parent directory. With none of them the behaviour is that of P6a. P6d adds ``definitions`` + (the registry-v1.0 definitions when not given) and the ``registry_version`` of the state + built from the parent directory.""" data = fixture.data parent = data["parent"] assert parent is not None, data["fixture_id"] @@ -166,9 +175,12 @@ def pipeline( after = normalize_directory(ROOT / data["config"], None, now=NOW) before = normalize_directory(ROOT / parent, None, now=NOW) assert after.resource_set_hash is not None - definitions = list(registry(source, destination).values()) + if definitions is None: + definitions = list(registry(source, destination).values()) semantic = [SemanticBinding("INV-FUNC-001", source, destination, "TCP", 5432)] - trusted = parent_trusted or trusted_from(parent, before.resources, definitions) + trusted = parent_trusted or trusted_from( + parent, before.resources, definitions, registry_version=registry_version + ) parent_id = trusted.state_id before_resources = trusted.resources if parent_trusted else before.resources identity = compare( diff --git a/tests/unit/test_identity_domain.py b/tests/unit/test_identity_domain.py index 202be93..0b65f69 100644 --- a/tests/unit/test_identity_domain.py +++ b/tests/unit/test_identity_domain.py @@ -261,8 +261,10 @@ def build( confidence: str | None, ) -> IdentityMatch: return IdentityMatch( + # one address on both sides: a pair across two addresses is a move (C-177), which this + # table of status and confidence is not about trusted_resource_ref="aws_vpc.a" if trusted else None, - candidate_resource_ref="aws_vpc.b" if candidate else None, + candidate_resource_ref="aws_vpc.a" if candidate else None, identity_status=IdentityStatus(status), change_type=ChangeType(change), confidence=None if confidence is None else IdentityConfidence(confidence), @@ -301,9 +303,9 @@ def test_create_derives_status_and_confidence_from_the_change(self) -> None: } for change, (trusted, candidate, status, confidence) in cases.items(): with self.subTest(change=change): - made = IdentityMatch.create( + made = IdentityMatch.create( # one address: not a move (C-177) trusted_ref="aws_vpc.a" if trusted else None, - candidate_ref="aws_vpc.b" if candidate else None, + candidate_ref="aws_vpc.a" if candidate else None, change_type=change, rule=EvidenceType.EXACT_ADDRESS, evidence_ids=[self.proof.evidence_id], @@ -604,14 +606,14 @@ def test_a_resource_cannot_be_in_two_matches(self) -> None: ( [ match("aws_vpc.a", "aws_vpc.a", ChangeType.UNCHANGED, one), - match("aws_vpc.a", "aws_vpc.b", ChangeType.UNCHANGED, two), + match("aws_vpc.a", "aws_vpc.b", ChangeType.MODIFIED, two), # moved (C-177) ], "trusted", ), ( [ - match("aws_vpc.a", "aws_vpc.b", ChangeType.UNCHANGED, one), - match("aws_vpc.c", "aws_vpc.b", ChangeType.UNCHANGED, two), + match("aws_vpc.a", "aws_vpc.b", ChangeType.MODIFIED, one), # moved (C-177) + match("aws_vpc.c", "aws_vpc.b", ChangeType.MODIFIED, two), ], "candidate", ), diff --git a/tests/unit/test_identity_engine.py b/tests/unit/test_identity_engine.py index 8a2ee2a..4289b0e 100644 --- a/tests/unit/test_identity_engine.py +++ b/tests/unit/test_identity_engine.py @@ -406,9 +406,11 @@ def test_a_resource_level_move_pairs_the_resources(self) -> None: self.assertEqual( (m.trusted_resource_ref, m.candidate_resource_ref), ("aws_vpc.a", "aws_vpc.b") ) + # C-177 (authors, 31 Oct 2026) supersedes C-129: every move is a change, so the pair is + # MODIFIED and moved although the fingerprints are equal (was UNCHANGED) self.assertEqual( - (m.change_type, m.identity_status, m.confidence), - (ChangeType.UNCHANGED, IdentityStatus.SAME, IdentityConfidence.HIGH), + (m.change_type, m.identity_status, m.confidence, m.moved), + (ChangeType.MODIFIED, IdentityStatus.SAME, IdentityConfidence.HIGH, True), ) kinds = {e.evidence_type for e in report.evidence_for(m)} self.assertIn(EvidenceType.EXPLICIT_MOVE, kinds) @@ -429,8 +431,9 @@ def test_a_resource_level_move_carries_every_instance_with_its_key(self) -> None self.assertEqual( changes(report), { - 'aws_vpc.a["x"]->aws_vpc.b["x"]': "UNCHANGED", - 'aws_vpc.a["y"]->aws_vpc.b["y"]': "UNCHANGED", + # C-177 supersedes C-129's "a resource-level move ... can be UNCHANGED" + 'aws_vpc.a["x"]->aws_vpc.b["x"]': "MODIFIED", + 'aws_vpc.a["y"]->aws_vpc.b["y"]': "MODIFIED", }, ) @@ -469,7 +472,8 @@ def test_chained_moves_reach_the_final_address(self) -> None: tf(vpc("a")), tf(vpc("c"), moved("aws_vpc.a", "aws_vpc.b"), moved("aws_vpc.b", "aws_vpc.c")), ) - self.assertEqual(changes(report), {"aws_vpc.a->aws_vpc.c": "UNCHANGED"}) + # C-177: every move is a change (was UNCHANGED under C-129) + self.assertEqual(changes(report), {"aws_vpc.a->aws_vpc.c": "MODIFIED"}) m = report.resource_matches[0] move = next( e for e in report.evidence_for(m) if e.evidence_type is EvidenceType.EXPLICIT_MOVE diff --git a/tests/unit/test_identity_strategy.py b/tests/unit/test_identity_strategy.py index b12dbff..58c410b 100644 --- a/tests/unit/test_identity_strategy.py +++ b/tests/unit/test_identity_strategy.py @@ -170,7 +170,8 @@ def test_it_keeps_the_content_flags(self) -> None: def test_it_differs_on_a_moved_resource(self) -> None: trusted, candidate = tf(vpc("a")), tf(vpc("b"), moved("aws_vpc.a", "aws_vpc.b")) full, ablated = both(trusted, candidate) - self.assertEqual(changes(full), {"aws_vpc.a->aws_vpc.b": "UNCHANGED"}) + # C-177: every move is a change (was UNCHANGED under C-129) + self.assertEqual(changes(full), {"aws_vpc.a->aws_vpc.b": "MODIFIED"}) self.assertEqual(changes(ablated), {"aws_vpc.a->-": "DELETED", "-->aws_vpc.b": "CREATED"}) def test_it_differs_on_an_implicit_count_move(self) -> None: diff --git a/tests/unit/test_moves_are_changes.py b/tests/unit/test_moves_are_changes.py new file mode 100644 index 0000000..ca5b260 --- /dev/null +++ b/tests/unit/test_moves_are_changes.py @@ -0,0 +1,331 @@ +"""Every move is a change (P6d; C-177, which supersedes C-129's resource-level clause; C-76, C-127). + +The rule, quoted from the P6d work package (section 3.1) and the authors' decision of 31 Oct 2026 +(paper audit round 3, finding C-01, "Every resource move counts as a change"): + +1. A pair made by a ``moved`` block of the candidate, or by Terraform's implicit ``count`` move + (C-76: ``x`` <-> ``x[0]``), is never UNCHANGED, even when the fingerprints are equal. With equal + fingerprints it is MODIFIED with ``moved = true`` and evidence that names the move. With + different fingerprints it is MODIFIED (``moved = true``), or REPLACED / UNCERTAIN exactly as + RT-1 decides. +2. No new ``ChangeType`` value; the flag lives on the identity match and its evidence. +3. Impact treats every such pair as a change source with reason "moved"; it is never dropped. +4. No evidence is carried across a REPLACED pair (unchanged rule). +5. ``AddressOnlyIdentity`` (C-127) does not follow moves. + +Expected values come from those sentences. Configurations go through the real pipeline. +""" + +from __future__ import annotations + +import unittest + +from core.domain.enums import ChangeType, ImpactStatus +from core.domain.errors import DomainValidationError +from core.domain.evidence import EvidenceValidity +from core.domain.identity import EvidenceType, IdentityMatch, IdentityReport +from core.domain.impact import ChangedResource, ChangeFlag +from core.identity.strategy import AddressOnlyIdentity +from core.impact.inputs import PriorProof +from tests.identity_builders import compare_texts +from tests.impact_builders import NET, impact_between, impacted + +LF = chr(10) + + +def block(header: str, *lines: str) -> str: + return header + " {" + LF + "".join(f" {line}" + LF for line in lines) + "}" + + +def tf(*blocks: str) -> str: + return LF.join(blocks) + LF + + +def vpc(label: str, *args: str, cidr: str = "10.0.0.0/16") -> str: + return block(f'resource "aws_vpc" "{label}"', *args, f'cidr_block = "{cidr}"') + + +def group(label: str, *args: str, name: str = "g") -> str: + return block(f'resource "aws_security_group" "{label}"', f'name = "{name}"', *args) + + +def moved(source: str, target: str) -> str: + return block("moved", f"from = {source}", f"to = {target}") + + +def pair_of(report: IdentityReport, trusted_ref: str) -> IdentityMatch: + (found,) = (m for m in report.resource_matches if m.trusted_resource_ref == trusted_ref) + return found + + +def kinds(report: IdentityReport, match: IdentityMatch) -> set[EvidenceType]: + return {item.evidence_type for item in report.evidence_for(match)} + + +def move_evidence(report: IdentityReport, match: IdentityMatch) -> dict[str, object]: + (item,) = ( + e + for e in report.evidence_for(match) + if e.evidence_type in (EvidenceType.EXPLICIT_MOVE, EvidenceType.IMPLICIT_COUNT_MOVE) + ) + observed = item.to_dict()["observed_value"] + assert isinstance(observed, dict) + return observed + + +class TestIdentity(unittest.TestCase): + def assert_moved_modified( + self, report: IdentityReport, trusted_ref: str, candidate_ref: str + ) -> IdentityMatch: + match = pair_of(report, trusted_ref) + self.assertEqual(match.candidate_resource_ref, candidate_ref) + self.assertIs(match.change_type, ChangeType.MODIFIED) + self.assertTrue(match.moved) + self.assertTrue(match.to_dict()["moved"]) + return match + + def test_explicit_rename_with_no_other_change(self) -> None: + report = compare_texts(tf(vpc("a")), tf(vpc("b"), moved("aws_vpc.a", "aws_vpc.b"))) + match = self.assert_moved_modified(report, "aws_vpc.a", "aws_vpc.b") + # the fingerprints are equal: the evidence says so, and the move is what decides + self.assertIn(EvidenceType.FINGERPRINT_EQUAL, kinds(report, match)) + self.assertIs(match.rule, EvidenceType.EXPLICIT_MOVE) + evidence = move_evidence(report, match) + self.assertEqual((evidence["from"], evidence["to"]), ("aws_vpc.a", "aws_vpc.b")) + self.assertEqual(evidence["statements"], [["aws_vpc.a", "aws_vpc.b"]]) + self.assertEqual(report.summary["unchanged"], ()) + + def test_adding_count_moves_x_to_x0(self) -> None: + report = compare_texts(tf(vpc("v")), tf(vpc("v", "count = 1"))) + match = self.assert_moved_modified(report, "aws_vpc.v", "aws_vpc.v[0]") + self.assertIn(EvidenceType.IMPLICIT_COUNT_MOVE, kinds(report, match)) + self.assertNotIn(EvidenceType.EXPLICIT_MOVE, kinds(report, match)) + evidence = move_evidence(report, match) + self.assertEqual((evidence["from"], evidence["to"]), ("aws_vpc.v", "aws_vpc.v[0]")) + + def test_removing_count_moves_x0_to_x(self) -> None: + report = compare_texts(tf(vpc("v", "count = 1")), tf(vpc("v"))) + match = self.assert_moved_modified(report, "aws_vpc.v[0]", "aws_vpc.v") + self.assertIn(EvidenceType.IMPLICIT_COUNT_MOVE, kinds(report, match)) + + def test_instance_key_change(self) -> None: + trusted = tf(vpc("v", 'for_each = toset(["x", "y"])')) + candidate = tf( + vpc("v", 'for_each = toset(["z", "y"])'), moved('aws_vpc.v["x"]', 'aws_vpc.v["z"]') + ) + report = compare_texts(trusted, candidate) + self.assert_moved_modified(report, 'aws_vpc.v["x"]', 'aws_vpc.v["z"]') + # the instance nobody moved is still compared on content alone + untouched = pair_of(report, 'aws_vpc.v["y"]') + self.assertIs(untouched.change_type, ChangeType.UNCHANGED) + self.assertFalse(untouched.moved) + + def test_resource_level_move_of_keyed_instances(self) -> None: + each = 'for_each = toset(["x", "y"])' + report = compare_texts( + tf(vpc("a", each)), tf(vpc("b", each), moved("aws_vpc.a", "aws_vpc.b")) + ) + self.assert_moved_modified(report, 'aws_vpc.a["x"]', 'aws_vpc.b["x"]') + self.assert_moved_modified(report, 'aws_vpc.a["y"]', 'aws_vpc.b["y"]') + + def test_chained_move_is_one_pair(self) -> None: + report = compare_texts( + tf(vpc("a")), + tf(vpc("c"), moved("aws_vpc.a", "aws_vpc.b"), moved("aws_vpc.b", "aws_vpc.c")), + ) + self.assertEqual(len(report.resource_matches), 1) + match = self.assert_moved_modified(report, "aws_vpc.a", "aws_vpc.c") + self.assertEqual( + move_evidence(report, match)["statements"], + [["aws_vpc.a", "aws_vpc.b"], ["aws_vpc.b", "aws_vpc.c"]], + ) + + def test_move_plus_an_argument_change(self) -> None: + report = compare_texts( + tf(vpc("a")), + tf(vpc("b", "enable_dns_hostnames = true"), moved("aws_vpc.a", "aws_vpc.b")), + ) + match = self.assert_moved_modified(report, "aws_vpc.a", "aws_vpc.b") + self.assertIn(EvidenceType.FINGERPRINT_DIFFERENT, kinds(report, match)) + self.assertIn(EvidenceType.EXPLICIT_MOVE, kinds(report, match)) + + def test_move_plus_a_security_group_name_change_is_replaced(self) -> None: + report = compare_texts( + tf(group("a", name="one")), + tf(group("b", name="two"), moved("aws_security_group.a", "aws_security_group.b")), + ) + match = pair_of(report, "aws_security_group.a") + self.assertEqual(match.candidate_resource_ref, "aws_security_group.b") + self.assertIs(match.change_type, ChangeType.REPLACED) + self.assertTrue(match.moved) + self.assertIn(EvidenceType.REPLACE_TRIGGER_FIELD, kinds(report, match)) + self.assertIn(EvidenceType.EXPLICIT_MOVE, kinds(report, match)) + + def test_address_only_identity_does_not_follow_moves(self) -> None: + report = compare_texts( + tf(vpc("a")), + tf(vpc("b"), moved("aws_vpc.a", "aws_vpc.b")), + strategy=AddressOnlyIdentity(), + ) + self.assertEqual( + {m.key: m.change_type for m in report.resource_matches}, + {"aws_vpc.a->-": ChangeType.DELETED, "-->aws_vpc.b": ChangeType.CREATED}, + ) + self.assertFalse(any(m.moved for m in report.resource_matches)) + + def test_an_unmoved_equal_pair_is_still_unchanged(self) -> None: + report = compare_texts(tf(vpc("a")), tf(vpc("a"))) + (match,) = report.resource_matches + self.assertIs(match.change_type, ChangeType.UNCHANGED) + self.assertFalse(match.moved) + self.assertFalse(match.to_dict()["moved"]) + + +class TestMatchGuards(unittest.TestCase): + """The domain refuses a match that would hide a move (rule 1), whoever builds it.""" + + EV = "a" * 64 + + def make(self, trusted: str | None, candidate: str | None, change: ChangeType, moved: bool): + rule = EvidenceType.FINGERPRINT_EQUAL + return IdentityMatch.create( + trusted_ref=trusted, + candidate_ref=candidate, + change_type=change, + rule=rule, + evidence_ids=[self.EV], + moved=moved, + ) + + def test_a_moved_pair_cannot_be_unchanged(self) -> None: + with self.assertRaises(DomainValidationError): + self.make("aws_vpc.a", "aws_vpc.b", ChangeType.UNCHANGED, True) + + def test_a_pair_across_addresses_must_say_moved(self) -> None: + with self.assertRaises(DomainValidationError): + self.make("aws_vpc.a", "aws_vpc.b", ChangeType.MODIFIED, False) + with self.assertRaises(DomainValidationError): + self.make("aws_vpc.a", "aws_vpc.b", ChangeType.UNCHANGED, False) + + def test_a_pair_at_one_address_is_not_moved(self) -> None: + with self.assertRaises(DomainValidationError): + self.make("aws_vpc.a", "aws_vpc.a", ChangeType.MODIFIED, True) + + def test_one_sided_matches_are_not_moved(self) -> None: + with self.assertRaises(DomainValidationError): + self.make("aws_vpc.a", None, ChangeType.DELETED, True) + with self.assertRaises(DomainValidationError): + self.make(None, "aws_vpc.b", ChangeType.CREATED, True) + + def test_moved_round_trips_and_is_required(self) -> None: + match = self.make("aws_vpc.a", "aws_vpc.b", ChangeType.MODIFIED, True) + data = match.to_dict() + self.assertEqual(IdentityMatch.from_dict(data), match) + del data["moved"] + with self.assertRaises(DomainValidationError): + IdentityMatch.from_dict(data) + with self.assertRaises(DomainValidationError): + IdentityMatch.from_dict({**match.to_dict(), "moved": "yes"}) + + def test_an_uncertain_pair_across_addresses_is_moved(self) -> None: + match = self.make("aws_vpc.a", "aws_vpc.b", ChangeType.UNCERTAIN, True) + self.assertTrue(match.moved) + + +# --- impact ----------------------------------------------------------------------------------- + +LONE = 'resource "aws_security_group" "lone" {\n name = "lone"\n vpc_id = aws_vpc.main.id\n}\n' +SOLO = 'resource "aws_security_group" "solo" {\n name = "lone"\n vpc_id = aws_vpc.main.id\n}\n' +MOVE = "moved {\n from = aws_security_group.lone\n to = aws_security_group.solo\n}\n" +SEC1, SEC2, SEC3, FUNC = "INV-SEC-001", "INV-SEC-002", "INV-SEC-003", "INV-FUNC-001" + + +def proof(invariant_id: str) -> PriorProof: + return PriorProof( + invariant_id=invariant_id, + invariant_version=1, + evidence_ids=(f"e-{invariant_id.lower()}",), + verifier_id={ + SEC1: "dail.verify.public_ingress", + SEC2: "dail.verify.public_ingress", + SEC3: "dail.verify.rds_public_flag", + FUNC: "dail.verify.reachability_cfg", + }[invariant_id], + verifier_version="1", + ) + + +class TestImpact(unittest.TestCase): + def source_of(self, report, address: str) -> ChangedResource: # type: ignore[no-untyped-def] + (found,) = (c for c in report.changed_resources if c.address == address) + return found + + def test_a_pure_rename_is_a_change_source_flagged_moved(self) -> None: + report = impact_between(NET + LONE, NET + SOLO + MOVE) + changed = self.source_of(report, "aws_security_group.solo") + self.assertEqual( + (changed.trusted_ref, changed.candidate_ref, changed.change_type), + ("aws_security_group.lone", "aws_security_group.solo", ChangeType.MODIFIED), + ) + self.assertIn(ChangeFlag.MOVED, changed.flags) + # every security group is in the SEC footprint (registry §3.5, C-64) + found = impacted(report) + for invariant in (SEC1, SEC2): + self.assertIs(found[invariant].status, ImpactStatus.AFFECTED) + self.assertIn("aws_security_group.solo", found[invariant].changed_resource_refs) + + def test_a_pure_rename_does_not_carry_the_sec_proofs(self) -> None: + prior = [proof(SEC1), proof(SEC2), proof(SEC3), proof(FUNC)] + report = impact_between(NET + LONE, NET + SOLO + MOVE, prior=prior) + for invariant in (SEC1, SEC2): + self.assertFalse( + report.carry_forward_ok( + invariant, + 1, + candidate_id=report.candidate_id, + parent_state_id=report.parent_state_id, + ) + ) + + def test_adding_count_is_a_change_source_flagged_moved(self) -> None: + counted = LONE.replace(' name = "lone"\n', ' count = 1\n name = "lone"\n') + report = impact_between(NET + LONE, NET + counted) + changed = self.source_of(report, "aws_security_group.lone[0]") + self.assertIn(ChangeFlag.MOVED, changed.flags) + self.assertIs(impacted(report)[SEC1].status, ImpactStatus.AFFECTED) + + def test_moved_and_replaced_carries_no_evidence(self) -> None: + renamed = SOLO.replace('name = "lone"', 'name = "other"') + prior = [proof(SEC1), proof(SEC2), proof(SEC3), proof(FUNC)] + report = impact_between(NET + LONE, NET + renamed + MOVE, prior=prior) + changed = self.source_of(report, "aws_security_group.solo") + self.assertIs(changed.change_type, ChangeType.REPLACED) + self.assertIn(ChangeFlag.MOVED, changed.flags) + for invariant in (SEC1, SEC2): + item = impacted(report)[invariant] + self.assertIs(item.status, ImpactStatus.AFFECTED) + self.assertIs(item.evidence_validity, EvidenceValidity.INVALID) + self.assertFalse( + report.carry_forward_ok( + invariant, + 1, + candidate_id=report.candidate_id, + parent_state_id=report.parent_state_id, + ) + ) + self.assertNotIn(invariant, {c.invariant_id for c in report.carry_forward_candidates}) + + def test_the_moved_flag_needs_both_refs(self) -> None: + with self.assertRaises(DomainValidationError): + ChangedResource( + address="aws_vpc.a", + trusted_ref="aws_vpc.a", + candidate_ref=None, + resource_type="aws_vpc", + change_type=ChangeType.DELETED, + flags=(ChangeFlag.MOVED,), + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_registry_v1_1.py b/tests/unit/test_registry_v1_1.py new file mode 100644 index 0000000..5ee41b7 --- /dev/null +++ b/tests/unit/test_registry_v1_1.py @@ -0,0 +1,326 @@ +"""Invariant registry v1.1 (P6d; C-150 closed by C-178; C-179 to C-181; C-85, C-62). + +Every expectation is typed from the P6d work package (sections 2, 3.2, 3.3) and the registry text: + +* ``docs/specs/INVARIANT_REGISTRY_v1.1.md`` exists; ``INVARIANT_REGISTRY_v1.md`` is byte-identical + to the file tagged ``registry-v1.0`` (C-85: after the tag a change is a new file). +* v1.1 changes exactly: §3.3 ``possible4``/``possible6`` (with a note), two §2.9 sentences, and the + versions (registry 1.1; INV-SEC-001 and INV-SEC-002 at version 2; INV-SEC-003 and INV-FUNC-001 + stay at version 1). Each change is marked ``[v1.1]`` and listed in a change log at the top. +* DAIL's definitions for v1.1: INV-SEC-001/002 version 2 citing ``registry-v1.1``; INV-SEC-003 and + INV-FUNC-001 the v1.0 definitions unchanged. DAIL stores registry 1.1 as the integer 2 (C-180, + the user's decision of 11 Nov 2026: ``invariant_registry_version`` stays an int, C-32). +* Evidence for SEC v1 does not satisfy v2 (C-62: supersession and reuse need equal + ``invariant_version``). +* The canonical scenario under v1.1: the unsafe candidate is REJECTED, the safe one PROMOTED. +""" + +from __future__ import annotations + +import dataclasses +import difflib +import hashlib +import unittest +from functools import cache +from pathlib import Path + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.impact import ReasonCode +from core.domain.invariant import Invariant +from core.domain.jsonvalue import thaw_json +from core.domain.promotion import ProofSource +from core.domain.registry_v1 import registry_v1_invariants +from core.domain.registry_v1_1 import ( + REGISTRY_TAG_V1_1, + REGISTRY_VERSION_V1_1, + registry_v1_1_invariants, +) +from core.verification.dispatch import DEFAULT_VERIFIERS, registry_of +from tests.domain_builders import at +from tests.pipeline_builders import inputs_for +from tests.promotion_pipeline import ROOT as FIXTURES_ROOT +from tests.promotion_pipeline import PipelineRun, fixtures_with_a_parent, pipeline, trusted_from + +SPECS = Path(__file__).resolve().parents[2] / "docs" / "specs" +V1_0 = SPECS / "INVARIANT_REGISTRY_v1.md" +V1_1 = SPECS / "INVARIANT_REGISTRY_v1.1.md" +# sha256 of INVARIANT_REGISTRY_v1.md at d7c0333 (the tagged text), line endings normalized to LF +V1_0_SHA256 = "031719cd8fe18544a82e863eb83cee45c4c495b07b2123a254a86bf58800ad5a" +NOW = at(0) +S, D = "aws_instance.app", "aws_db_instance.database" +SEC1, SEC2, SEC3, FUNC = "INV-SEC-001", "INV-SEC-002", "INV-SEC-003", "INV-FUNC-001" +SAFE = "canonical_safe_repair_promote_v1" +REGRESSION = "canonical_security_repair_breaks_function_reject_v1" + +NEW_POSSIBLE = """possible4(g) := exists indeterminate r in In(g) that could permit TCP/p + (its protocol or ports unresolved, or they permit p) and + (its IPv4 sources are unresolved or include a prefix list, + or its resolved IPv4 sources, together with the union of v4(r') + over r' in D(g), cover 0.0.0.0/0). +possible6(g) is the same for IPv6 sources and ::/0.""" +OLD_POSSIBLE = "IPv4 sources are unresolved or include a prefix list." +SENTENCE_1 = ( + "In the footprint comparison, an argument that neither configuration writes compares as " + "absent on both sides and is not changed. The predicates still treat such a value as §2.2 says." +) +SENTENCE_2 = ( + "The parent counterpart's inline-rule form (§3.5, §6.6) is compared through what it decides: " + "whether the group is RETAINED-INLINE in that direction (§2.6). A baseline has no parent, so " + "this is false for every group of a baseline." +) + + +def text(path: Path) -> str: + return path.read_bytes().decode("utf-8").replace("\r\n", "\n") + + +def squash(value: str) -> str: + """Whitespace-insensitive form, for text that a Markdown file may wrap or indent.""" + return " ".join(value.split()) + + +class TestRegistryFiles(unittest.TestCase): + def test_v1_0_is_byte_identical_to_the_tagged_text(self) -> None: + data = V1_0.read_bytes().replace(b"\r\n", b"\n") + self.assertEqual(hashlib.sha256(data).hexdigest(), V1_0_SHA256) + + def test_v1_1_exists_with_registry_version_1_1(self) -> None: + body = text(V1_1) + self.assertTrue(body.startswith("# Invariant Registry Specification v1.1\n")) + self.assertIn("`invariant_registry_version = 1.1`", body) + + def test_the_new_possible_clause_replaces_the_old_one(self) -> None: + body = squash(text(V1_1)) + self.assertIn(squash(NEW_POSSIBLE), body) + self.assertNotIn(squash(OLD_POSSIBLE), body) + self.assertIn(squash(OLD_POSSIBLE), squash(text(V1_0))) # the old text was there + + def test_the_two_section_2_9_sentences(self) -> None: + body = squash(text(V1_1)) + section = body[body.index("### 2.9") : body.index("### 2.10")] + self.assertIn(squash(SENTENCE_1), section) + self.assertIn(squash(SENTENCE_2), section) + + def test_invariant_versions(self) -> None: + body = text(V1_1) + self.assertIn("`INV-SEC-001`, version 2.", body) + self.assertIn("`INV-SEC-002`, version 2.", body) + self.assertIn("`INV-SEC-003`, version 1.", body) + self.assertIn("`INV-FUNC-001`, version 1.", body) + + def test_every_change_is_marked_and_in_the_change_log(self) -> None: + old, new = text(V1_0).splitlines(), text(V1_1).splitlines() + top = new[: new.index("---")] # the change log sits above the first rule of the file + self.assertIn("## Change log (v1.0 to v1.1)", top) + entries = [line for line in top if line.startswith("- [v1.1] ")] + self.assertEqual(len(entries), 3, entries) # §3.3, §2.9, §1 versioning + for wanted in ("**§3.3 `possible4` and `possible6`**", "**§2.9 clarification**", "**§1"): + self.assertEqual(sum(wanted in entry for entry in entries), 1, wanted) + matcher = difflib.SequenceMatcher(a=old, b=new, autojunk=False) + for tag, i1, i2, j1, j2 in matcher.get_opcodes(): + if tag == "equal": + continue + if (i1, i2, j1, j2) == (0, 1, 0, 1): + self.assertEqual(new[0], "# Invariant Registry Specification v1.1") + continue # the title names the file; it is not a change of the text + if tag == "delete": + self.fail(f"lines of v1.0 removed without a marked replacement: {old[i1:i2]}") + # the marker is in the change or right beside it (a code block cannot hold one) + window = "\n".join(new[max(0, j1 - 3) : j2 + 3]) + with self.subTest(lines=f"{j1 + 1}-{j2}"): + self.assertIn("[v1.1]", window) + + +class TestDefinitions(unittest.TestCase): + def setUp(self) -> None: + self.v10 = {d.invariant_id: d for d in registry_v1_invariants(NOW, source=S, destination=D)} + self.v11 = { + d.invariant_id: d for d in registry_v1_1_invariants(NOW, source=S, destination=D) + } + + def test_registry_version_and_tag(self) -> None: + self.assertEqual(REGISTRY_TAG_V1_1, "registry-v1.1") + self.assertEqual(REGISTRY_VERSION_V1_1, 2) + + def test_sec_001_and_002_are_version_2_and_cite_v1_1(self) -> None: + for invariant_id, section, port in ((SEC1, "§3", 22), (SEC2, "§4", 5432)): + definition = self.v11[invariant_id] + with self.subTest(invariant=invariant_id): + self.assertEqual(definition.version, 2) + self.assertEqual( + dict(definition.predicate), + {"registry": "registry-v1.1", "section": section, "parameters": {"p": port}}, + ) + self.assertIn("registry-v1.1", definition.description) + old = self.v10[invariant_id] + self.assertEqual( + (definition.verifier_id, definition.verifier_version), + (old.verifier_id, old.verifier_version), + ) + self.assertEqual(definition.scope, old.scope) + self.assertNotEqual(definition.definition_hash(), old.definition_hash()) + + def test_sec_003_and_func_001_are_the_v1_0_definitions(self) -> None: + for invariant_id in (SEC3, FUNC): + with self.subTest(invariant=invariant_id): + self.assertEqual(self.v11[invariant_id].version, 1) + self.assertEqual( + self.v11[invariant_id].definition_hash(), + self.v10[invariant_id].definition_hash(), + ) + + def test_the_definition_chooses_the_section_3_3_text(self) -> None: + self.assertEqual(registry_of(self.v10[SEC1]), "registry-v1.0") + self.assertEqual(registry_of(self.v11[SEC1]), "registry-v1.1") + self.assertEqual(registry_of(self.v11[SEC2]), "registry-v1.1") + for bad in ("registry-v9", None, 1): + predicate = {**thaw_json(self.v11[SEC1].predicate), "registry": bad} + with self.subTest(tag=bad), self.assertRaises(ValueError): + registry_of(dataclasses.replace(self.v11[SEC1], predicate=predicate)) + + def test_the_verifier_evaluates_each_definition_under_its_own_registry(self) -> None: + # registry v1.0 §3.3 gives PASS for this rule (C-150); v1.1 §3.3 gives UNKNOWN (C-178) + gap = ( + 'variable "u" {}\n' + 'resource "aws_security_group" "app" {\n}\n' + 'resource "aws_security_group_rule" "r" {\n type = "ingress"\n' + ' security_group_id = aws_security_group.app.id\n protocol = "tcp"\n' + ' from_port = var.u\n to_port = 22\n cidr_blocks = ["0.0.0.0/0"]\n}\n' + ) + inputs = inputs_for(gap, with_graphs=False) + cases = ( + (self.v10[SEC1], VerificationResult.PASS), + (self.v11[SEC1], VerificationResult.UNKNOWN), + (self.v10[SEC2], VerificationResult.PASS), + # §3.3: "could permit TCP/p (its protocol or ports unresolved, ...)": an unresolved + # from_port could permit 5432 whatever to_port says + (self.v11[SEC2], VerificationResult.UNKNOWN), + ) + for definition, expected in cases: + with self.subTest(invariant=definition.invariant_id, version=definition.version): + verifier = DEFAULT_VERIFIERS[(definition.verifier_id, definition.verifier_version)] + self.assertIs(verifier(definition, inputs).result, expected) + + def test_sorted_by_id(self) -> None: + ids = [d.invariant_id for d in registry_v1_1_invariants(NOW, source=S, destination=D)] + self.assertEqual(ids, sorted([SEC1, SEC2, SEC3, FUNC])) + + +# --- the pipeline under v1.1 ---------------------------------------------------------------------- + + +def v11_definitions(fixture_id: str) -> list[Invariant]: + binding = fixtures_with_a_parent()[fixture_id].data["bindings"]["INV-FUNC-001"] + return list(registry_v1_1_invariants(NOW, source=binding["S"], destination=binding["D"])) + + +def v10_definitions(fixture_id: str) -> list[Invariant]: + binding = fixtures_with_a_parent()[fixture_id].data["bindings"]["INV-FUNC-001"] + return list(registry_v1_invariants(NOW, source=binding["S"], destination=binding["D"])) + + +@cache +def under_v11(fixture_id: str) -> PipelineRun: + """Parent and candidate both under v1.1 (the parent's proofs are of the v1.1 versions).""" + return pipeline( + fixtures_with_a_parent()[fixture_id], + definitions=v11_definitions(fixture_id), + registry_version=REGISTRY_VERSION_V1_1, + ) + + +@cache +def v10_parent_v11_candidate(fixture_id: str) -> PipelineRun: + """The parent was proven under v1.0 (SEC proofs of version 1); the candidate is checked under + v1.1 (SEC version 2).""" + fixture = fixtures_with_a_parent()[fixture_id] + from core.terraform_model.normalization import normalize_directory + from tests.identity_builders import NOW as PIPE_NOW + + parent = fixture.data["parent"] + before = normalize_directory(FIXTURES_ROOT / parent, None, now=PIPE_NOW) + trusted = trusted_from(parent, before.resources, v10_definitions(fixture_id)) + return pipeline( + fixture, + definitions=v11_definitions(fixture_id), + registry_version=REGISTRY_VERSION_V1_1, + parent_trusted=trusted, + ) + + +def decide_v11(run: PipelineRun): # type: ignore[no-untyped-def] + return run.decide(policy=run.policy(invariant_registry_version=REGISTRY_VERSION_V1_1)) + + +class TestCanonicalScenarioUnderV11(unittest.TestCase): + def test_the_safe_repair_is_promoted(self) -> None: + outcome = decide_v11(under_v11(SAFE)) + self.assertIs(outcome.decision.decision, DecisionType.PROMOTE) + + def test_the_repair_that_breaks_the_database_path_is_rejected(self) -> None: + outcome = decide_v11(under_v11(REGRESSION)) + self.assertIs(outcome.decision.decision, DecisionType.REJECT) + + def test_sec_evidence_cites_version_2_and_registry_1_1(self) -> None: + run = under_v11(SAFE) + records = {r.target_id: r for r in run.verification.results} + record = records["INVARIANT:INV-SEC-001:2"] + self.assertEqual((record.invariant_id, record.invariant_version), (SEC1, 2)) + self.assertEqual(record.evidence["invariant_version"], 2) + self.assertTrue(str(record.evidence["predicate"]).startswith("registry-v1.1 §3 ")) + self.assertEqual( + (record.verifier_id, record.verifier_version), ("dail.verify.public_ingress", "1") + ) + + +class TestVersion1EvidenceDoesNotSatisfyVersion2(unittest.TestCase): + def test_the_sec_proofs_of_version_1_are_not_carried_forward(self) -> None: + run = v10_parent_v11_candidate(SAFE) + refs = {r.invariant_id: r.invariant_version for r in run.trusted.invariant_refs} + self.assertEqual(refs, {SEC1: 1, SEC2: 1, SEC3: 1, FUNC: 1}) + for invariant_id in (SEC1, SEC2): + with self.subTest(invariant=invariant_id): + self.assertFalse( + run.impact.carry_forward_ok( + invariant_id, + 2, + candidate_id=run.candidate.candidate_id, + parent_state_id=run.trusted.state_id, + ) + ) + self.assertFalse( + run.impact.carry_forward_ok( + invariant_id, + 1, + candidate_id=run.candidate.candidate_id, + parent_state_id=run.trusted.state_id, + ) + ) + unaffected = {u.key(): u for u in run.impact.unaffected} + if (invariant_id, 2) in unaffected: + self.assertIs( + unaffected[(invariant_id, 2)].reason, ReasonCode.INVARIANT_VERSION_CHANGED + ) + self.assertIn("INVARIANT:INV-SEC-002:2", run.work) # verified again, never carried + + def test_the_decision_verifies_sec_version_2_and_never_reuses_version_1(self) -> None: + run = v10_parent_v11_candidate(SAFE) + outcome = decide_v11(run) + plan = {(e.invariant_id, e.invariant_version): e.source for e in outcome.proof_plan} + self.assertEqual(plan.get((SEC2, 2)), ProofSource.VERIFIED) + self.assertNotIn((SEC2, 1), plan) + self.assertIs(outcome.decision.decision, DecisionType.PROMOTE) + + def test_the_default_verifier_table_is_unchanged(self) -> None: + self.assertEqual( + sorted(DEFAULT_VERIFIERS), + [ + ("dail.verify.public_ingress", "1"), + ("dail.verify.rds_public_flag", "1"), + ("dail.verify.reachability_cfg", "1"), + ], + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_verification_public_ingress.py b/tests/unit/test_verification_public_ingress.py index fd747a7..6d70d04 100644 --- a/tests/unit/test_verification_public_ingress.py +++ b/tests/unit/test_verification_public_ingress.py @@ -386,27 +386,74 @@ def test_an_unresolved_ipv6_list_is_unknown_for_ipv6_only(self) -> None: self.check(run(text), U, P, U, R.RULE_INDETERMINATE) +def port_rule(name: str, low: str, v4: str | None = None, v6: str | None = None) -> str: + """An ingress rule resource of the app group whose ``from_port`` is ``low`` (HCL text).""" + sources = "" if v4 is None else f" cidr_blocks = {v4}\n" + sources += "" if v6 is None else f" ipv6_cidr_blocks = {v6}\n" + return ( + f'resource "aws_security_group_rule" "{name}" {{\n type = "ingress"\n' + ' security_group_id = aws_security_group.app.id\n protocol = "tcp"\n' + f" from_port = {low}\n to_port = 22\n{sources}}}\n" + ) + + class TestRegistryGap(Expect): - """Registry §3.3 makes ``possible4`` depend on the IPv4 sources being unresolved or including a - prefix list. A rule whose *port* is unresolved but whose IPv4 source is the whole internet is - therefore not a possibility, and the registry text gives PASS. That is implemented verbatim - (prompt, C-146) and recorded as an Open row (C-150) for the authors: the next test pins the - behaviour so that it cannot change unnoticed.""" + """Registry v1.1 §3.3 (P6d; C-150 closed by C-178): ``possible4(g)`` also holds when an + indeterminate rule that could permit TCP/p has resolved IPv4 sources that, together with the + union of ``v4`` over ``D(g)``, cover 0.0.0.0/0 (``possible6`` likewise with ::/0). Registry + v1.0 gave PASS for ``from_port = var.u`` with ``cidr_blocks = ["0.0.0.0/0"]``; v1.1 gives + UNKNOWN. The expected values below are derived from that sentence.""" + + def test_unresolved_port_with_a_public_source_is_unknown(self) -> None: + outcome = run(VARS + sg() + port_rule("r", "var.u", v4='["0.0.0.0/0"]')) + self.check(outcome, U, U, P, R.RULE_INDETERMINATE) + self.assertEqual(len(outcome.observations["indeterminate_rules"]), 1) + + def test_unresolved_port_with_a_private_source_alone_is_still_pass(self) -> None: + outcome = run(VARS + sg() + port_rule("r", "var.u", v4='["10.0.0.0/8"]')) + self.check(outcome, P, P, P, None) + self.assertEqual(len(outcome.observations["indeterminate_rules"]), 1) + + def test_unresolved_port_with_the_whole_ipv6_internet_is_unknown_for_ipv6(self) -> None: + outcome = run(VARS + sg() + port_rule("r", "var.u", v6='["::/0"]')) + self.check(outcome, U, P, U, R.RULE_INDETERMINATE) - def test_unresolved_port_with_a_public_source_is_pass_by_the_registry_text(self) -> None: + def test_together_with_the_determinate_rules_it_covers(self) -> None: + # D(g) holds tcp 22 from 0.0.0.0/1; the indeterminate rule adds 128.0.0.0/1: covered text = ( VARS + sg() - + ( - 'resource "aws_security_group_rule" "r" {\n type = "ingress"\n' - ' security_group_id = aws_security_group.app.id\n protocol = "tcp"\n' - ' from_port = var.u\n to_port = 22\n cidr_blocks = ["0.0.0.0/0"]\n}\n' - ) + + rule("half", "ingress", "tcp", 22, 22, ["0.0.0.0/1"]) + + port_rule("r", "var.u", v4='["128.0.0.0/1"]') ) - outcome = run(text) - self.check(outcome, P, P, P, None) - # not hidden: the rule is reported as indeterminate in the observations - self.assertEqual(len(outcome.observations["indeterminate_rules"]), 1) + self.check(run(text), U, U, P, R.RULE_INDETERMINATE) + + def test_half_the_internet_alone_is_not_possible(self) -> None: + self.check(run(VARS + sg() + port_rule("r", "var.u", v4='["128.0.0.0/1"]')), P, P, P, None) + + def test_a_determinate_rule_on_another_port_does_not_count_for_d_of_g(self) -> None: + # D(g) holds only rules that permit TCP/p; a tcp 80 rule from 0.0.0.0/1 is not in it + text = ( + VARS + + sg() + + rule("web", "ingress", "tcp", 80, 80, ["0.0.0.0/1"]) + + port_rule("r", "var.u", v4='["128.0.0.0/1"]') + ) + self.check(run(text), P, P, P, None) + + def test_a_rule_that_cannot_permit_the_port_is_not_possible_whatever_its_source(self) -> None: + text = VARS + sg() + rule("r", "ingress", "udp", 22, 22, ANY4) + self.check(run(text), P, P, P, None) + + def test_the_registry_v1_0_reading_is_kept_for_v1_definitions(self) -> None: + # INV-SEC-001/002 version 1 are the registry-v1.0 predicate (TerraPreserve v1.0 labels) + resources = resources_of(VARS + sg() + port_rule("r", "var.u", v4='["0.0.0.0/0"]')) + old = evaluate_public_ingress(22, resources, registry="registry-v1.0") + self.check(old, P, P, P, None) + new = evaluate_public_ingress(22, resources, registry="registry-v1.1") + self.check(new, U, U, P, R.RULE_INDETERMINATE) + with self.assertRaises(ValueError): + evaluate_public_ingress(22, resources, registry="registry-v9") class TestIdentityAndRetention(Expect):