From 8bd30a1ed225beb988831327adf19fc5390cf01c Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:17:36 +0530 Subject: [PATCH 1/8] P6a step 0: record the P5 gate verdict (PHASE_GATES) Co-Authored-By: Claude Sonnet 5.5 --- docs/PHASE_GATES.md | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/docs/PHASE_GATES.md b/docs/PHASE_GATES.md index a81bf40..83351b0 100644 --- a/docs/PHASE_GATES.md +++ b/docs/PHASE_GATES.md @@ -153,7 +153,23 @@ Carry-forward: C-150 and C-155 for registry v1.1 before D4; index_rules placehol C-143 option B before D4; C-148 NOT_APPLICABLE question goes to the authors. ``` -## P5b–P10 — NOT STARTED +## P5 — Verification + +```text +P5 gate: PASSED (external review, 29 Oct 2026; PR #23 at c3524ef, merged before the verdict, C-28 +process lapse recorded a sixth time). Milestone M2 reached. Suite passes on Python 3.12 and 3.13 +(skipped=1); black, ruff and mypy clean. The P5b defect (an unresolved vpc_security_group_ids +entry gave PASS) is fixed (C-156); reviewer reproductions, about 100 FUNC probes and 3 mutations +of the fix all as the registry says. CIDR boundary mutants of covers() killed. Limits: the +20-fixture FUNC table and F4/F8 were not independently re-run by the reviewer. +Carry-forward: registry v1.1 amendment before D4 for C-150 and C-155 (including item 13 and engine +casing); index_rules placeholder hazard with C-143 option B before D4; C-148 NOT_APPLICABLE +question to the authors; the unused row 7 branch of sg_s.unresolved in _possible is dead code, +clean up later. C-45 enforcement in P6 (blocker). C-144 to C-148, C-151 to C-156 Proposed; +C-149, C-150, C-155 Open. +``` + +## P6a–P10 — NOT STARTED ## Temporary exceptions From 54f9c7d3d1123232daa969e261b4a20ac2af5857 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:24:13 +0530 Subject: [PATCH 2/8] =?UTF-8?q?P6a=20step=201:=20register=20rows=20C-157?= =?UTF-8?q?=20to=20C-161=20(Proposed),=20decide=20C-37=20and=20C-41,=20bou?= =?UTF-8?q?ndary=20rule=20R18=20(Doc=2009=20=C2=A717-=C2=A729;=20C-37,=20C?= =?UTF-8?q?-41,=20C-157=20to=20C-161)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit R18 was written test-first: its self-tests failed until the rule existed in check_module (core.promotion imports only the standard library and core.domain.*). Co-Authored-By: Claude Sonnet 5.5 --- docs/DECISIONS_REGISTER.md | 9 +++- .../contract/test_architecture_boundaries.py | 52 +++++++++++++++++++ 2 files changed, 59 insertions(+), 2 deletions(-) diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index f62079a..436cc18 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -47,11 +47,11 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-34 | Provenance union (implements C-07) | source_kind (= Doc 11 source_type; Doc 05 enum), source_component, source_reference, observed_at (= Doc 05 timestamp), tool_name, tool_version, parser_version, normalization_version, algorithm_version, transformation_steps. The first four are required. The rest use explicit null, except transformation_steps, which defaults to an empty tuple. | Accepted 1 Oct 2026 (P1a) | | C-35 | Interim storage in P1a | `core/domain/storage.py` is adapted to the new shapes: schema version 3, the same four table names, every immutability trigger kept, older schema versions refused. It is replaced behind repository ports with the Doc 05 §20 tables in P1b. | Accepted 1 Oct 2026 (P1a) | | C-36 | Enum scope | `ObligationCategory` (not in Doc 05 §4.1) is removed; obligation kinds come from Docs 08/09 in P4 if needed. `EvidenceKind` is not defined in the domain; P2-fix defines the single evidence taxonomy (C-06). | Accepted 1 Oct 2026 (P1a) | -| C-37 | When `InvariantRef` invalidation fields are set (Doc 06 §14) | P1a keeps both fields, validated both-set-or-both-null, and `can_satisfy_proof()` is False when they are set. Under C-23, a rejection never touches vN's refs, so it is undefined which event sets them. Decide before P6a, against Doc 09. | **Open** | +| C-37 | When `InvariantRef` invalidation fields are set (Doc 06 §14) | P1a keeps both fields, validated both-set-or-both-null, and `can_satisfy_proof()` is False when they are set. Under C-23, a rejection never touches vN's refs, so it is undefined which event sets them. Decide before P6a, against Doc 09. **Decided 29 Oct 2026 (P6a prompt).** *The invalidation fields of an `InvariantRef` are never set by any P6 event.* Trusted states are immutable (DATA-INT-006) and a rejection never touches vN's references (C-23), so no event can write them to a stored reference; the references of vN+1 are created fresh from VERIFIED or CARRIED_FORWARD proofs, so there is nothing to invalidate at creation. "Invalidation" is represented by (a) the candidate-scoped AFFECTED records of the impact report and (b) evidence-validity transitions (C-52). The two fields stay in the model, always null on references written by baseline, promotion or carry-forward; a reference that has them set can never satisfy proof (`can_satisfy_proof()` unchanged). Tests: promotion-side code never sets them; `carry_forward` refuses a PROTECTED reference with them set (already true; pinned). | Decided 29 Oct 2026 (P6a prompt); implemented in P6a | | C-38 | A PROMOTABLE candidate whose promotion commit fails for a reason other than a stale parent | Doc 06 §27 requires "no new current Trusted State" but gives no candidate status. P1a allows no exit other than PROMOTED or stale rejection. Decide before P6b. | **Open** | | C-39 | Evidence record identifiers | Record IDs in evidence/ (evidence, operation, attempt, request, transition, event) become canonical UUIDs per Doc 05 §3. Implemented in P2-fix, which also restores the P2 gate test's link to real evidence IDs. | Accepted 1 Oct 2026 (review). Implemented in P2-fix | | C-40 | Proof binding and coverage | `InvariantProof` carries `origin` (`ProofOrigin`: BASELINE, VERIFIED, CARRIED_FORWARD) and is created only by `InvariantProof.for_baseline` (origin BASELINE), `InvariantEvaluation.to_proof` (origin VERIFIED, bound to the evaluation's `candidate_id`) and `InvariantProof.carry_forward(parent_ref, candidate)` (origin CARRIED_FORWARD; `parent_ref.state_id` must equal `candidate.parent_state_id`; status and evidence copied unchanged; a PROTECTED ref must pass `can_satisfy_proof()`). `establish_baseline` accepts only BASELINE proofs. `promote` accepts only VERIFIED proofs bound to this candidate and CARRIED_FORWARD proofs from the current state. Every `invariant_id` on the current state must have a proof, with an `invariant_version` not lower than its current one. A trusted state holds at most one reference per `invariant_id`. `InvariantRef` records `origin`; `origin` is not part of `state_hash` (C-33 unchanged). Whether carry-forward is permitted for a given invariant (impact, C-22) remains P6 policy. | Accepted 1 Oct 2026 (review) | -| C-41 | Retiring an invariant from a lineage, and whether `invariant_registry_version` must be monotonic across promotions | P1a forbids dropping an invariant at promotion (C-40). Decide before P6a. | **Open** | +| C-41 | Retiring an invariant from a lineage, and whether `invariant_registry_version` must be monotonic across promotions | P1a forbids dropping an invariant at promotion (C-40). Decide before P6a. **Decided 29 Oct 2026 (P6a prompt).** *In this prototype an invariant is never retired from a lineage.* (1) Dropping an invariant at promotion stays forbidden (C-40). A registry change that removes an invariant requires a **new lineage** with its own baseline. (2) `invariant_registry_version` is **non-decreasing across promotions** within a lineage: a policy whose registry version is lower than the current state's is not a PROMOTE (decision ESCALATE, reason `POLICY_REGISTRY_REGRESSION`). (3) Invariant versions per id are non-decreasing (already enforced). (4) An invariant that is **new** in the registry (not on the current state) is required by the policy's extra-required list and, having no parent reference, can only be proven by a fresh VERIFIED PASS. (5) An invariant whose version rose cannot be carried forward (Doc 09 §28); it needs a fresh VERIFIED PASS at the new version. | Decided 29 Oct 2026 (P6a prompt); implemented in P6a | | C-42 | P1 table subset | P1b creates `patches`, `trusted_states`, `candidates`, `resources`, `invariants` and `invariant_refs` (Doc 05 §20), plus three tables not named in §20: `state_resources` and `candidate_resources` (a resource record is shared by a candidate and the state promoted from it, so ownership is a link), and `lineage_heads` (the Doc 06 §6 current pointer). The other §20 tables arrive with their owning packages: evidence_events P2-fix; identity/dependency/impact/verification reports P3–P5; promotion_decisions P6; llm_* P7; experiments/runs/attempts/oracle_results P8. | Accepted 2 Oct 2026 (P1b) | | C-43 | Repository ports and adapter | Protocols in `core/domain/repositories.py`. The SQLite adapter lives in `core/persistence/`. The Doc 05 §26 set is extended with a `PatchRepository` (Doc 05 §9, §33) and a `UnitOfWork` that implements the §32 transaction. EvidenceRepository comes in P2-fix; AnalysisRepository in P3–P6. `sqlite3` may be imported only in `core/persistence/`, `evidence/` and `core/application/health.py` (rule R11). | Accepted 2 Oct 2026 (P1b) | | C-44 | Schema migrations | No migration tooling until the first persistent research data exists. Any database with a schema version other than 5 is refused (P2-fix, C-59) with instructions to delete the local development database. The tooling decision is made before P8a. | Accepted 2 Oct 2026 (P1b) | @@ -168,3 +168,8 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-154 | P5b: assumptions, observations and the baseline list | The result's `assumptions`, sorted: `IPv4 only`, `M1: RDS security groups and subnet group share one VPC (C-15, C-77, uncited)`, `M4: default network ACL assumed (no NACL type present)`, and `tolerated type: aws_db_subnet_group (C-15)` when that type is present. Closed observation keys (present on every path): `row`, `reason`, `detail`, `endpoints`, `port`, `unresolved` (why row 4 applies), `path` (`S`, `subnet`, `vpc_s`, `sg_s`, `egress_rule`, `sg_d`, `ingress_rule`, `vpc_d`; a part that is not reached is null), `row2_causes`, `failing_conditions`, `indeterminate_rules`, `partial_coverage`, `relevant_unsupported`. `baseline.py`: the relevant-unsupported list of a created resource becomes the 26 types of registry §2.7 for INV-FUNC-001 (`core.domain.registry_v1.FUNC_RELEVANT_UNSUPPORTED`, which contains the three of the security list), so a created resource of any of them is UNSUPPORTED `type.relevant_unsupported`, not PASS with `applicable = false`; the predicate lists for INV-SEC-001/002 do not change. | Proposed (P5b) | | C-155 | P5b: cases that registry §6 does not decide, settled conservatively here, for registry v1.1 | Implementing INV-FUNC-001 exactly as §6.3 and §6.4 left these open; each was settled by the work package's rule R5 (UNSUPPORTED, or the cautious reading) and is listed in C-152 and C-153. The authors should confirm or amend them together with C-150 in registry v1.1 (a new file under C-85, with the version bump of the invariants whose results change). **(1) Row 4 and E2.** Row 4 names E3 and E4 but not E2; an unresolved `D.port`, or an unresolved `D.engine` when there is no port, is UNKNOWN here (row 4), because an unresolved E2 cannot be a PASS and no other row fits. **(2) Row 7, "it".** When both E5 and E6 fail and an indeterminate rule could satisfy only one of them, row 7 is UNKNOWN here (the more cautious reading; the precise reading would be FAIL, since both are needed). **(3) "Could satisfy".** An indeterminate rule with a resolved satisfying side beside an unresolved port or protocol counts as one that could satisfy (UNKNOWN), unlike the SEC `possible` text of C-150, which drops it. **(4) Row 2 and an UNSUPPORTED endpoint resource.** The work package says UNKNOWN (C-152); §2.4 would call it UNSUPPORTED. **(5) Rules of unknown direction.** A rule resource whose `type` is unresolved counts as a rule of every direction: it can satisfy E5 or E6 (row 7) and makes a group that declares an explicit empty list MIXED (row 2). **(6) A pseudo-group with an unresolved target.** Its rules are determinate but may belong to a group of `SG(S)` or `SG(D)`; they count for row 7. **(7) Literal ids.** A literal AWS id as a `vpc_id`, as an entry of `vpc_security_group_ids` or as a `subnet_id` is UNSUPPORTED (the VPC CIDR or the rules of that group are not known). **(8) M1.** Groups of `D` in two VPCs, and `D` with neither `port` nor `engine`, are UNSUPPORTED. **(9) M3.** A route table whose `vpc_id` cannot be fixed, a placeholder route table, a route whose destination or target cannot be fixed, a prefix-list destination and a dynamic route expansion that cannot be fixed make the result UNSUPPORTED when they could belong to `VPC(D)`; an IPv6-only route is not read (M5); a route with no target is treated as non-local. **(10) E5 and E6 per rule.** `v4(r)` is the CIDR list of one rule, so two rules with half of the range each do not cover it; the registry text does not say that explicitly. **(11) `src_sg` of an egress rule** is read as the group named in `security_groups` or `source_security_group_id` of that egress rule (a destination group), as AWS does. **(12) `ADDR(S)`** with an unresolved `private_ip` falls back to the subnet CIDR, and an unresolved subnet CIDR leaves E6 undecidable by a CIDR (row 7). **(13) An unresolved entry of `SG(S)`** (`S.vpc_security_group_ids`) is UNKNOWN (row 4) here (C-156); an extra allow-only group cannot remove permission, so the authors may relax it to PASS in registry v1.1 when the known groups are enough, once MIXED and RETAINED-INLINE can be checked for it. | Open (found 29 Oct 2026; P5b) | | C-156 | P5b-fix: an unresolved entry of `vpc_security_group_ids` is row 4; the engine is compared exactly | Registry §6.3 E3: each entry of `D.vpc_security_group_ids` references a configured aws_security_group with a resolved `vpc_id`; §6.4 row 4: when E3 or E4 needs an unresolved value the result is UNKNOWN. P5b let an unresolved entry (a variable, a `concat` with a variable, a group of unknown `count`) reach row 6 and give PASS when the known groups established the path (found by the external review of PR #22). **(1)** An entry of `D.vpc_security_group_ids` that is unresolved, or that references a placeholder group, is added to the row 4 reasons when the side is read, so row 4 (UNKNOWN, `attribute.unresolved`) applies after rows 1 to 3 and any row 2 cause, and before rows 5 to 9; the path is neither a PASS nor a FAIL then. **(2)** The same for `S.vpc_security_group_ids`; the registry is silent, see C-155 item 13. **(3)** The row 7 use of the unresolved entries of the side is unchanged; row 4 now returns first, so it is not reached for them. **(4)** A literal id stays UNSUPPORTED (C-155 item 7). **(5)** E2 compares `engine` with the exact string `postgres`, as the registry writes it; `Postgres` or `POSTGRES` without a port is row 3 (FAIL) (before, the comparison ignored case). Open question for the authors: the provider may accept other spellings of the engine name; no behaviour beyond the exact comparison. **(6)** Two P5b tests asserted the superseded results (an unresolved entry of `S` with the path established: PASS, row 6; with no path: row 7); they now assert UNKNOWN, row 4, and were changed in the commit that changes the code. | Proposed (P5b-fix) | +| C-157 | P6a: boundary, types and entry point of the decision half of the Promotion Controller | New rule **R18**: `core.promotion` imports only the standard library and `core.domain.*` (never `core.verification`, `core.identity`, `core.dependency`, `core.impact`, `core.terraform_model`, `core.persistence`, `core.application`, `evidence`), with a self-test like R14 to R17; nothing is loosened; R8 is unchanged and P6a does not use it (P6b is the first caller of `promote`). Types in `core/domain/promotion.py`: `PromotionDecision` (Doc 05 §15), `PromotionEvidence` (Doc 11 §26), `PromotionPolicy`, the closed vocabularies `DecisionReason` and `ProofSource` (VERIFIED, CARRIED_FORWARD), `OracleVerdict`, `ProofPlanEntry`, `DecisionOutcome` and `PromotionInputError` (a `DomainValidationError`). Logic in `core/promotion/` (`decide.py`, `policy.py`, `lifecycle.py`). Entry point `decide(candidate, trusted, impact, verification, policy, *, decision_id, now, attempt_number=1, oracle_verdicts=()) -> DecisionOutcome`, where `DecisionOutcome` holds the `PromotionDecision`, the `ProofPlan` (which source proves each required invariant, for P6b) and the `PromotionEvidence`. `decide` is pure: no clock, no randomness (`decision_id` and `now` are injected), no I/O, no mutation of any argument. Malformed arguments (wrong types, another lineage, a candidate that is neither ANALYZING nor PROMOTABLE, a bad attempt number, duplicate oracle verdicts) raise `PromotionInputError`; everything the decision itself finds is a REJECT, RETRY or ESCALATE, never an exception. **Implementation notes (P6a):** `PromotionDecision` adds `reason`, `attempt_number` and `content_hash` to the fields of Doc 05 §15 (the spec lists no reason field, but says non-promotion decisions must preserve their blocking reasons; `blocking_conditions` keeps all of them, `reason` is the highest-severity one); `PromotionPolicy` carries the invariant definitions of its registry version (`invariants`), because `core.promotion` may not import a registry; it also carries the verifier ids that the two gate items are expected to name (`gate_verifiers`; the baseline items of created resources name the verifier that the verification engine chose for the resource type, so the result's own verifier is accepted for RESOURCE items: an assumption and a spec gap, see the P6a report); the gate verifier ids are copied from `core.verification.engine` and a test (which may import both) pins that they are equal; `decide` takes the current trusted state of the lineage as `trusted`. | Proposed (P6a) | +| C-158 | P6a: `decide()` order, severity and the retry/escalate table | Order (Doc 09 Appendix A, extended): (1) emergency switch and policy sanity; (2) stale parent; (3) construction and the STRUCTURAL and CONSISTENCY gate items; (4) required invariants (C-159); (5) oracle conflicts (C-160); (6) evidence sufficiency and decision completeness (C-161); (7) PROMOTE. A stale parent is checked first and wins over everything (`candidate.parent_state_id != trusted.state_id`: REJECT, `STALE_PARENT`). **Order independence, a deliberate deviation from Appendix A's early return:** the loop of Appendix A returns at the first non-PASS item, so a later FAIL could hide behind an earlier UNKNOWN. `decide` examines **all** required items and then folds by severity: any FAIL, STRUCTURAL or CONSISTENCY FAIL, or REJECT-class non-success gives **REJECT**; otherwise any ESCALATE-class gives **ESCALATE**; otherwise any RETRY-class gives **RETRY**; otherwise PROMOTE. The decision never depends on the order of results, work items or invariants (property test). **Non-success table** (`PromotionPolicy.non_success`, closed, versioned): UNKNOWN gives RETRY (a new patch or more context could resolve it); UNSUPPORTED on a required invariant gives REJECT (a retry cannot make the model larger, Doc 09 §29); VERIFIER_ERROR gives RETRY if the error `type` is in `policy.transient_errors` (default empty), else ESCALATE. A construction failure and a STRUCTURAL FAIL give REJECT, a CONSISTENCY FAIL gives REJECT (`INCONSISTENT_REPORTS`, Doc 09 §31), a missing result for a required item gives REJECT `INSUFFICIENT_EVIDENCE` (Appendix A). **Retry budget:** `policy.max_attempts` (default 3, validated 1 to 10) and the input `attempt_number`: a RETRY at `attempt_number >= max_attempts` becomes **ESCALATE** with reason `RETRY_BUDGET_EXHAUSTED` (never REJECT, never PASS; Doc 09 §23, repeated UNKNOWN is not an eventual PASS). Backoff and scheduling stay outside the core. Flagged as a decision for the authors (Doc 09 §23 puts retry limits outside the core semantic decision; only the exhaustion rule is here). **Severity order:** REJECT above ESCALATE above RETRY is a choice; the spec does not order them. Flagged for the authors. Every blocking condition found is recorded in `blocking_conditions` (sorted, closed codes), not only the first; `reason` is the highest-severity one, ties broken by a fixed list. The impact report or verification report of another candidate or parent is a REJECT `INCONSISTENT_REPORTS`. | Proposed (P6a) | +| C-159 | P6a: required set and proof source (this closes C-45) | **Required set** = every invariant on the current state (its id, at the version in the policy's registry) together with `policy.extra_required` (C-41(4)), plus the gate items STRUCTURAL and CONSISTENCY and the RESOURCE baseline items of the impact work set. A required invariant missing from the policy's registry, or at a lower version than the current reference, is an `ESCALATE` (`POLICY_REGISTRY_REGRESSION`). Each required invariant is proven by exactly one of: **VERIFIED**, a fresh (`fresh(...)`), sufficient (`sufficient(...)`) PASS in the verification report for target `INVARIANT::` with the definition's verifier id and version, and `evidence_level` not below `policy.min_evidence_level` ("L1"); or **CARRIED_FORWARD**, only if **all** hold: `policy.carry_forward_enabled`; `impact.carry_forward_ok(id, version, candidate_id=..., parent_state_id=...)` is True (the C-45 query); the parent reference exists with the **same** invariant version, status **PROTECTED** and `can_satisfy_proof()`; the invariant is **not** in the impact report's affected set and no uncertainty record names it; the definition names the same verifier as the parent's evidence (definitions are immutable, so equal versions imply it: verifier configuration changes are not modelled, an assumption and a spec gap against Doc 06 §17). **Never carried forward:** an affected invariant (C-45); a non-PROTECTED parent reference (VIOLATED or UNCERTAIN; a violated invariant must be re-verified to PASS, which is what the canonical SSH repair does); a version change; any invariant when `carry_forward_enabled` is False (the Stateful-Full condition, C-22). If a fresh result exists for the target it decides: FAIL rejects, a non-success follows the table, a sufficient PASS is VERIFIED; carry-forward is tried only when no fresh result exists. If neither source exists the decision is REJECT `INSUFFICIENT_EVIDENCE` listing the invariants without proof. A PASS that is not `sufficient` or not `fresh` is not proof (`EVIDENCE_NOT_SUFFICIENT`, `EVIDENCE_STALE`, both under INSUFFICIENT_EVIDENCE). `decide` never runs verification; the orchestrator of P6b applies the `VerificationScopePolicy` before it. A PASS marked not applicable (C-148, open) is a PASS here, as in `aggregate`. | Proposed (P6a) | +| C-160 | P6a: oracle evidence (Doc 09 §16, §17) | `OracleVerdict(invariant_id, invariant_version, result, oracle_version)` is optional input. Oracle evidence is never proof (ADR-010, C-54): `PromotionPolicy` refuses to be constructed with `accept_oracle_for_unknown=True`; the field exists so that the refusal is explicit and testable. Primary PASS (or a carried-forward proof) with oracle FAIL: a conflict is recorded, the check is not treated as proven, and the decision is `policy.conflict_decision` (REJECT or ESCALATE, default ESCALATE, never PROMOTE) with reason `EVIDENCE_CONFLICT`. Primary FAIL with oracle PASS: the FAIL stays blocking (REJECT). Primary UNKNOWN with oracle PASS: the UNKNOWN stays non-success; no oracle acceptance. Agreement changes nothing. The conflict is listed in `blocking_conditions`. An oracle FAIL for a carried-forward invariant is treated as a conflict too (the oracle sees a violation that nobody re-verified). | Proposed (P6a) | +| C-161 | P6a: emergency switch and decision completeness | `policy.automatic_enabled` False turns any would-be PROMOTE into **ESCALATE** with reason `AUTOMATIC_PROMOTION_DISABLED`; non-PROMOTE decisions are unchanged (Doc 14 §37). The audit record keeps what the decision would have been (`would_have_been` in `blocking_conditions`). Before a decision is returned, **decision completeness** (Doc 11 §43) is evaluated on the finished decision: candidate binding valid; parent binding valid (`parent_state_id` equals `candidate.parent_state_id`, DATA-INT-003); every `supporting_results` id exists in the verification report; the report's `candidate_hash` equals the candidate's `state_hash` and its content hash recomputes; the impact report's content hash recomputes; `policy_version` recorded. A PROMOTE that fails completeness becomes ESCALATE `DECISION_INCOMPLETE`; a non-PROMOTE keeps its decision and records the incompleteness. A PROMOTE lists in `supporting_results` **every** verification result id used, and in `PromotionEvidence.verification_refs` the same ids (Doc 11 §26). | Proposed (P6a) | diff --git a/tests/contract/test_architecture_boundaries.py b/tests/contract/test_architecture_boundaries.py index 276d590..3300d18 100644 --- a/tests/contract/test_architecture_boundaries.py +++ b/tests/contract/test_architecture_boundaries.py @@ -43,6 +43,9 @@ R17 core.verification imports only the standard library, core.domain.* and itself: not core.terraform_model, core.dependency, core.identity, core.impact, core.persistence, core.application, core.promotion or any other core.* package, and not evidence (C-144). +R18 core.promotion imports only the standard library, core.domain.* and itself: not + core.verification, core.identity, core.dependency, core.impact, core.terraform_model, + core.persistence, core.application or any other core.* package, and not evidence (C-157). ORACLE nothing in this repository imports the TerraPreserve oracle (ADR-010). A self-test feeds in-memory sources that break each rule, so a checker that @@ -213,6 +216,15 @@ def check_module(module: str, imports: set[str]) -> list[Violation]: or top in ("evidence", "sqlite3") ): violations.append(Violation("R17", module, name)) + if _within(module, "core.promotion") and ( + ( + top == "core" + and not _within(name, "core.promotion") + and not _within(name, "core.domain") + ) + or top in ("evidence", "sqlite3") + ): + violations.append(Violation("R18", module, name)) if (in_core or in_evidence) and not is_stdlib and top not in ("core", "evidence"): package = ".".join(module.split(".")[:2]) if top not in THIRD_PARTY_ALLOWLIST.get(package, frozenset()): @@ -617,6 +629,46 @@ def test_r17_applies_only_to_the_verification_engine(self) -> None: "R17", self.rules_for("core.verificationx.bad", "from core.persistence import sqlite\n") ) + def test_r18_forbids_everything_but_the_standard_library_and_core_domain(self) -> None: + # C-157: the decision half of the Promotion Controller consumes domain objects only + for module in ("core.promotion", "core.promotion.decide", "core.promotion.lifecycle"): + for source in ( + "from core.verification import engine\n", + "import core.verification.structural\n", + "from core.identity import engine\n", + "from core.dependency import build\n", + "from core.impact import engine\n", + "from core.terraform_model import security_rules\n", + "from core.persistence import sqlite\n", + "from core.application import config\n", + "import evidence.store\n", + "import sqlite3\n", + "from ..verification import engine\n", + ): + with self.subTest(module=module, source=source.strip()): + is_package = module == "core.promotion" + self.assertIn("R18", self.rules_for(module, source, is_package)) + + def test_r18_allows_core_domain_itself_and_the_standard_library(self) -> None: + for module in ("core.promotion.decide", "core.promotion.policy"): + for source in ( + "from core.domain.promotion import PromotionDecision\n", + "from core.domain import hashing\n", + "import core.domain.verification\n", + "from core.promotion.policy import dail_policy\n", + "from .policy import dail_policy\n", + "import dataclasses\nfrom collections.abc import Mapping\n", + ): + with self.subTest(module=module, source=source.splitlines()[0]): + self.assertNotIn("R18", self.rules_for(module, source)) + + def test_r18_applies_only_to_the_promotion_package(self) -> None: + for module in ("core.verification.ok", "core.impact.ok", "core.application.ok"): + self.assertNotIn("R18", self.rules_for(module, "from core.domain import hashing\n")) + self.assertNotIn( + "R18", self.rules_for("core.promotionx.bad", "from core.persistence import sqlite\n") + ) + def test_the_verification_engine_cannot_import_the_application_layer_or_promotion(self) -> None: self.assertIn( "R2", self.rules_for("core.verification.engine", "from core.application import x\n") From ce1a0b8025418f50361fb2568624b7e2963cfb95 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:29:12 +0530 Subject: [PATCH 3/8] =?UTF-8?q?P6a=20step=202:=20promotion=20types,=20the?= =?UTF-8?q?=20policy=20and=20its=20two=20constructors=20(Doc=2005=20=C2=A7?= =?UTF-8?q?15,=20Doc=2011=20=C2=A726;=20C-157,=20C-158,=20C-160,=20C-161)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PromotionDecision and PromotionEvidence (guards, hash recomputed by the constructor, round trip), the closed DecisionReason and ProofSource vocabularies, OracleVerdict, ProofPlanEntry, DecisionOutcome and PromotionPolicy (non-success table, retry budget 1 to 10, the oracle cannot be accepted). dail_policy and stateful_full_policy differ in carry-forward only (C-22). The 48 tests were written first and failed with ImportError until the types existed. Co-Authored-By: Claude Sonnet 5.5 --- core/domain/__init__.py | 4 + core/domain/promotion.py | 786 ++++++++++++++++++++++++++++ core/promotion/__init__.py | 16 +- core/promotion/policy.py | 120 +++++ tests/unit/test_promotion_domain.py | 365 +++++++++++++ tests/unit/test_promotion_policy.py | 224 ++++++++ 6 files changed, 1509 insertions(+), 6 deletions(-) create mode 100644 core/domain/promotion.py create mode 100644 core/promotion/policy.py create mode 100644 tests/unit/test_promotion_domain.py create mode 100644 tests/unit/test_promotion_policy.py diff --git a/core/domain/__init__.py b/core/domain/__init__.py index ef008d7..dd32206 100644 --- a/core/domain/__init__.py +++ b/core/domain/__init__.py @@ -22,6 +22,10 @@ reasons, and the three pure functions P6 needs (``sufficient``, ``fresh``, ``aggregate``), which never count anything doubtful as proof. +Promotion (P6a; Doc 09 §17-§29, C-157 to C-161): ``promotion`` holds ``PromotionDecision``, +``PromotionEvidence``, ``PromotionPolicy`` and the closed vocabularies of decision reasons and +proof sources. The decision itself is ``core.promotion.decide``. + Lifecycles: explicit transition tables and functions (``lifecycle``, ``state``) that reject every transition the specification forbids, including SM-001 to SM-010. Lifecycle-bearing objects can be created only through those functions, so ``dataclasses.replace`` and direct constructor calls diff --git a/core/domain/promotion.py b/core/domain/promotion.py new file mode 100644 index 0000000..77024af --- /dev/null +++ b/core/domain/promotion.py @@ -0,0 +1,786 @@ +"""Promotion types: the decision, its evidence and the policy (P6a; Doc 05 §15, Doc 06 §16-§21, +Doc 09 §17-§29, Doc 11 §26, §43; C-157 to C-161). + +The decision half of the Promotion Controller (``core.promotion.decide``) turns the full evaluation +context into one ``PromotionDecision``: PROMOTE, REJECT, RETRY or ESCALATE. A decision preserves +every blocking reason (Doc 05 §15), and a PROMOTE names every verification result that established +eligibility (Doc 11 §26). ``committed_state_id`` and ``new_state_id`` stay null here; the commit of +P6b is the only thing that sets them (DATA-INT-004). + +``PromotionPolicy`` is data: the registry version, the invariant definitions, the non-success table, +the retry budget and the emergency switch are all passed in, so neither this module nor +``core.promotion`` reads configuration (Doc 14 §37). The policy refuses to accept oracle evidence as +proof (ADR-010, C-54). +""" + +from __future__ import annotations + +from collections.abc import Iterable, Mapping +from dataclasses import dataclass, field +from datetime import datetime +from enum import StrEnum +from typing import Any, Final + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.errors import DomainValidationError, HashMismatchError +from core.domain.hashing import content_hash +from core.domain.ids import require_uuid +from core.domain.invariant import Invariant +from core.domain.jsonvalue import ( + iso_utc, + parse_enum, + parse_utc, + require_enum, + require_int, + require_keys, + require_text, + utc, +) +from core.domain.verification import EVIDENCE_LEVELS + +GATE_STRUCTURAL: Final = "STRUCTURAL" +GATE_CONSISTENCY: Final = "CONSISTENCY" +GATE_TARGETS: Final = (GATE_CONSISTENCY, GATE_STRUCTURAL) +CHECK_KINDS: Final = ("BASELINE", "GATE", "INVARIANT") +SUFFICIENCY_VALUES: Final = ("INSUFFICIENT", "SUFFICIENT") +NON_SUCCESS_RESULTS: Final = ( + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, + VerificationResult.VERIFIER_ERROR, +) +NON_PROMOTE: Final = (DecisionType.ESCALATE, DecisionType.REJECT, DecisionType.RETRY) +MAX_ATTEMPTS_LIMIT: Final = 10 + + +class PromotionInputError(DomainValidationError): + """The arguments of ``decide`` are malformed (wrong types, another lineage, ...). A finding of + the decision itself is never an error: it is a REJECT, RETRY or ESCALATE (C-157).""" + + +class DecisionReason(StrEnum): + """Why a decision was taken: one closed code per reason (C-157, C-158).""" + + STALE_PARENT = "STALE_PARENT" + STRUCTURAL_FAILURE = "STRUCTURAL_FAILURE" + INCONSISTENT_REPORTS = "INCONSISTENT_REPORTS" + REQUIRED_CHECK_FAILED = "REQUIRED_CHECK_FAILED" + REQUIRED_UNKNOWN = "REQUIRED_UNKNOWN" + REQUIRED_UNSUPPORTED = "REQUIRED_UNSUPPORTED" + VERIFIER_ERROR = "VERIFIER_ERROR" + INSUFFICIENT_EVIDENCE = "INSUFFICIENT_EVIDENCE" + EVIDENCE_NOT_SUFFICIENT = "EVIDENCE_NOT_SUFFICIENT" + EVIDENCE_STALE = "EVIDENCE_STALE" + EVIDENCE_CONFLICT = "EVIDENCE_CONFLICT" + RETRY_BUDGET_EXHAUSTED = "RETRY_BUDGET_EXHAUSTED" + POLICY_REGISTRY_REGRESSION = "POLICY_REGISTRY_REGRESSION" + AUTOMATIC_PROMOTION_DISABLED = "AUTOMATIC_PROMOTION_DISABLED" + DECISION_INCOMPLETE = "DECISION_INCOMPLETE" + ALL_REQUIRED_PROVEN = "ALL_REQUIRED_PROVEN" + + +class ProofSource(StrEnum): + """What proves a required invariant (C-159): a fresh verification, or the parent's reference.""" + + VERIFIED = "VERIFIED" + CARRIED_FORWARD = "CARRIED_FORWARD" + + +def _bool(value: object, name: str) -> bool: + if not isinstance(value, bool): + raise DomainValidationError(f"{name}: must be a boolean") + return value + + +def _texts(value: object, name: str, *, allowed: frozenset[str] | None = None) -> tuple[str, ...]: + if isinstance(value, str) or not isinstance(value, Iterable): + raise DomainValidationError(f"{name}: must be a list of texts") + items = tuple(require_text(item, f"{name}[]") for item in value) + if len(set(items)) != len(items): + raise DomainValidationError(f"{name}: duplicate entry") + if allowed is not None and not set(items) <= allowed: + raise DomainValidationError(f"{name}: names something that is not defined") + return tuple(sorted(items)) + + +def _uuids(value: object, name: str) -> tuple[str, ...]: + """A strictly sorted tuple of canonical UUIDs.""" + if isinstance(value, str) or not isinstance(value, Iterable): + raise DomainValidationError(f"{name}: must be a list of UUIDs") + items = tuple(require_uuid(item, f"{name}[]") for item in value) + if list(items) != sorted(set(items)): + raise DomainValidationError(f"{name}: must be sorted and without duplicates") + return items + + +def _objects[T](value: object, kind: type[T], name: str) -> tuple[T, ...]: + if isinstance(value, str) or not isinstance(value, Iterable): + raise DomainValidationError(f"{name}: must be a list") + items = tuple(value) + if not all(isinstance(item, kind) for item in items): + raise DomainValidationError(f"{name}: must hold {kind.__name__} objects") + return items + + +def _list_of(value: object, name: str) -> list[Any]: + if not isinstance(value, list | tuple): + raise DomainValidationError(f"{name}: must be a list") + return list(value) + + +# --- required checks and blocking conditions ------------------------------------------------------ + + +@dataclass(frozen=True) +class RequiredCheck: + """One thing the decision required, and what proved it (C-159). + + ``source`` is None when nothing proved it. A VERIFIED check names the verification result that + did (``verification_id``); a CARRIED_FORWARD one (invariants only) names none: its evidence is + the parent reference's, listed in the ``ProofPlanEntry``. + """ + + target_id: str + kind: str + source: ProofSource | None + verification_id: str | None + + def __post_init__(self) -> None: + require_text(self.target_id, "RequiredCheck.target_id") + if self.kind not in CHECK_KINDS: + raise DomainValidationError(f"RequiredCheck.kind: must be one of {CHECK_KINDS}") + if self.source is not None: + require_enum(self.source, ProofSource, "RequiredCheck.source") + if (self.source is ProofSource.VERIFIED) != (self.verification_id is not None): + raise DomainValidationError( + "RequiredCheck: a VERIFIED check names its result, and only a VERIFIED one does" + ) + if self.verification_id is not None: + require_uuid(self.verification_id, "RequiredCheck.verification_id") + if self.source is ProofSource.CARRIED_FORWARD and self.kind != "INVARIANT": + raise DomainValidationError("RequiredCheck: only an invariant can be carried forward") + + def to_dict(self) -> dict[str, Any]: + return { + "target_id": self.target_id, + "kind": self.kind, + "source": None if self.source is None else self.source.value, + "verification_id": self.verification_id, + } + + @classmethod + def from_dict(cls, data: Mapping[str, Any]) -> RequiredCheck: + fields = require_keys(data, ("target_id", "kind", "source", "verification_id"), "check") + source = fields["source"] + return cls( + target_id=fields["target_id"], + kind=fields["kind"], + source=None if source is None else parse_enum(source, ProofSource, "check.source"), + verification_id=fields["verification_id"], + ) + + +@dataclass(frozen=True) +class BlockingCondition: + """One reason a decision is not a PROMOTE. ``decision`` is the class of the condition: what + this condition alone would give (REJECT, RETRY or ESCALATE, never PROMOTE).""" + + code: DecisionReason + decision: DecisionType + target: str + detail: str + + def __post_init__(self) -> None: + require_enum(self.code, DecisionReason, "BlockingCondition.code") + require_enum(self.decision, DecisionType, "BlockingCondition.decision") + if self.decision not in NON_PROMOTE: + raise DomainValidationError("BlockingCondition: a blocking condition is not a PROMOTE") + if self.code is DecisionReason.ALL_REQUIRED_PROVEN: + raise DomainValidationError("BlockingCondition: ALL_REQUIRED_PROVEN blocks nothing") + require_text(self.target, "BlockingCondition.target") + require_text(self.detail, "BlockingCondition.detail") + + def sort_key(self) -> tuple[str, str, str, str]: + return (self.code.value, self.target, self.detail, self.decision.value) + + def to_dict(self) -> dict[str, Any]: + return { + "code": self.code.value, + "decision": self.decision.value, + "target": self.target, + "detail": self.detail, + } + + @classmethod + def from_dict(cls, data: Mapping[str, Any]) -> BlockingCondition: + fields = require_keys(data, ("code", "decision", "target", "detail"), "blocking condition") + return cls( + code=parse_enum(fields["code"], DecisionReason, "condition.code"), + decision=parse_enum(fields["decision"], DecisionType, "condition.decision"), + target=fields["target"], + detail=fields["detail"], + ) + + +def _checks(value: object) -> tuple[RequiredCheck, ...]: + checks = _objects(value, RequiredCheck, "required_checks") + keys = [check.target_id for check in checks] + if keys != sorted(set(keys)): + raise DomainValidationError( + "required_checks: must be sorted by target, one check per target" + ) + return checks + + +# --- the decision --------------------------------------------------------------------------------- + + +_DECISION_KEYS = ( + "decision_id", + "candidate_id", + "parent_state_id", + "decision", + "reason", + "policy_version", + "attempt_number", + "required_checks", + "blocking_conditions", + "supporting_results", + "created_at", + "committed_state_id", + "content_hash", +) + + +@dataclass(frozen=True) +class PromotionDecision: + """The decision of the Promotion Controller about one candidate (Doc 05 §15). + + Beyond the fields of Doc 05 §15 it records the ``reason`` (the highest-severity blocking + condition, or ALL_REQUIRED_PROVEN) and the ``attempt_number`` (C-157). Create it with + ``create``; the constructor recomputes ``content_hash``, which excludes the id and the clock. + """ + + decision_id: str + candidate_id: str + parent_state_id: str + decision: DecisionType + reason: DecisionReason + policy_version: str + attempt_number: int + required_checks: tuple[RequiredCheck, ...] + blocking_conditions: tuple[BlockingCondition, ...] + supporting_results: tuple[str, ...] + created_at: datetime + committed_state_id: str | None + content_hash: str + + def __post_init__(self) -> None: + name = "PromotionDecision" + require_uuid(self.decision_id, f"{name}.decision_id") + require_uuid(self.candidate_id, f"{name}.candidate_id") + require_uuid(self.parent_state_id, f"{name}.parent_state_id") + require_enum(self.decision, DecisionType, f"{name}.decision") + require_enum(self.reason, DecisionReason, f"{name}.reason") + require_text(self.policy_version, f"{name}.policy_version") + require_int(self.attempt_number, f"{name}.attempt_number", 1) + if self.committed_state_id is not None: + raise DomainValidationError( + f"{name}.committed_state_id: null until the commit of P6b (DATA-INT-004)" + ) + object.__setattr__(self, "created_at", utc(self.created_at, f"{name}.created_at")) + checks = _checks(self.required_checks) + conditions = _objects(self.blocking_conditions, BlockingCondition, "blocking_conditions") + if [c.sort_key() for c in conditions] != sorted({c.sort_key() for c in conditions}): + raise DomainValidationError( + f"{name}.blocking_conditions: must be sorted and without duplicates" + ) + results = _uuids(self.supporting_results, f"{name}.supporting_results") + self._check_decision(conditions, results) + object.__setattr__(self, "required_checks", checks) + object.__setattr__(self, "blocking_conditions", conditions) + object.__setattr__(self, "supporting_results", results) + if self.content_hash != self.compute_hash(): + raise HashMismatchError( + f"DATA-INT-010: PromotionDecision {self.decision_id} content_hash does not " + "match its content" + ) + + def _check_decision( + self, conditions: tuple[BlockingCondition, ...], results: tuple[str, ...] + ) -> None: + name = "PromotionDecision" + if self.decision is DecisionType.PROMOTE: + if self.reason is not DecisionReason.ALL_REQUIRED_PROVEN or conditions: + raise DomainValidationError( + f"{name}: a PROMOTE is ALL_REQUIRED_PROVEN and has no blocking condition" + ) + if not results: + raise DomainValidationError( + f"{name}: a PROMOTE must reference the evidence that satisfied the policy " + "(Doc 05 §15)" + ) + return + if self.reason is DecisionReason.ALL_REQUIRED_PROVEN: + raise DomainValidationError(f"{name}: only a PROMOTE has everything proven") + if not conditions: + raise DomainValidationError( + f"{name}: a {self.decision.value} must preserve its blocking reasons (Doc 05 §15)" + ) + if self.reason not in {c.code for c in conditions}: + raise DomainValidationError(f"{name}: the reason is not among the blocking conditions") + + def _payload(self) -> dict[str, Any]: + data = self.to_dict() + for key in ("decision_id", "created_at", "content_hash"): + del data[key] + return data + + def compute_hash(self) -> str: + return content_hash(self._payload()) + + @classmethod + def create( + cls, + *, + decision_id: str, + candidate_id: str, + parent_state_id: str, + decision: DecisionType, + reason: DecisionReason, + policy_version: str, + attempt_number: int, + required_checks: Iterable[RequiredCheck], + blocking_conditions: Iterable[BlockingCondition], + supporting_results: Iterable[str], + created_at: datetime, + ) -> PromotionDecision: + """Build the decision and its hash (the constructor then checks both).""" + probe = { + "candidate_id": candidate_id, + "parent_state_id": parent_state_id, + "decision": getattr(decision, "value", decision), + "reason": getattr(reason, "value", reason), + "policy_version": policy_version, + "attempt_number": attempt_number, + "required_checks": [c.to_dict() for c in required_checks], + "blocking_conditions": [c.to_dict() for c in blocking_conditions], + "supporting_results": list(supporting_results), + "committed_state_id": None, + } + return cls( + decision_id=decision_id, + candidate_id=candidate_id, + parent_state_id=parent_state_id, + decision=decision, + reason=reason, + policy_version=policy_version, + attempt_number=attempt_number, + required_checks=tuple(required_checks), + blocking_conditions=tuple(blocking_conditions), + supporting_results=tuple(supporting_results), + created_at=created_at, + committed_state_id=None, + content_hash=content_hash(probe), + ) + + def to_dict(self) -> dict[str, Any]: + return { + "decision_id": self.decision_id, + "candidate_id": self.candidate_id, + "parent_state_id": self.parent_state_id, + "decision": self.decision.value, + "reason": self.reason.value, + "policy_version": self.policy_version, + "attempt_number": self.attempt_number, + "required_checks": [c.to_dict() for c in self.required_checks], + "blocking_conditions": [c.to_dict() for c in self.blocking_conditions], + "supporting_results": list(self.supporting_results), + "created_at": iso_utc(self.created_at), + "committed_state_id": self.committed_state_id, + "content_hash": self.content_hash, + } + + @classmethod + def from_dict(cls, data: Mapping[str, Any]) -> PromotionDecision: + fields = require_keys(data, _DECISION_KEYS, "PromotionDecision") + return cls( + decision_id=fields["decision_id"], + candidate_id=fields["candidate_id"], + parent_state_id=fields["parent_state_id"], + decision=parse_enum(fields["decision"], DecisionType, "decision"), + reason=parse_enum(fields["reason"], DecisionReason, "reason"), + policy_version=fields["policy_version"], + attempt_number=fields["attempt_number"], + required_checks=tuple( + RequiredCheck.from_dict(item) + for item in _list_of(fields["required_checks"], "required_checks") + ), + blocking_conditions=tuple( + BlockingCondition.from_dict(item) + for item in _list_of(fields["blocking_conditions"], "blocking_conditions") + ), + supporting_results=tuple(_list_of(fields["supporting_results"], "supporting_results")), + created_at=parse_utc(fields["created_at"], "PromotionDecision.created_at"), + committed_state_id=fields["committed_state_id"], + content_hash=fields["content_hash"], + ) + + +# --- the evidence of a decision ------------------------------------------------------------------- + + +_EVIDENCE_KEYS = ( + "decision_id", + "candidate_id", + "parent_state_id", + "required_checks", + "verification_refs", + "evidence_sufficiency", + "policy_version", + "decision", + "reason", + "new_state_id", + "content_hash", +) + + +@dataclass(frozen=True) +class PromotionEvidence: + """What a decision rests on (Doc 11 §26). A PROMOTE references every mandatory verification + result used; ``new_state_id`` stays null until P6b creates the state.""" + + decision_id: str + candidate_id: str + parent_state_id: str + required_checks: tuple[RequiredCheck, ...] + verification_refs: tuple[str, ...] + evidence_sufficiency: str + policy_version: str + decision: DecisionType + reason: DecisionReason + new_state_id: str | None + content_hash: str + + def __post_init__(self) -> None: + name = "PromotionEvidence" + require_uuid(self.decision_id, f"{name}.decision_id") + require_uuid(self.candidate_id, f"{name}.candidate_id") + require_uuid(self.parent_state_id, f"{name}.parent_state_id") + require_text(self.policy_version, f"{name}.policy_version") + require_enum(self.decision, DecisionType, f"{name}.decision") + require_enum(self.reason, DecisionReason, f"{name}.reason") + if self.evidence_sufficiency not in SUFFICIENCY_VALUES: + raise DomainValidationError( + f"{name}.evidence_sufficiency: must be one of {SUFFICIENCY_VALUES}" + ) + if self.new_state_id is not None: + raise DomainValidationError(f"{name}.new_state_id: null until the commit of P6b") + checks = _checks(self.required_checks) + refs = _uuids(self.verification_refs, f"{name}.verification_refs") + if self.decision is DecisionType.PROMOTE and ( + not refs or self.evidence_sufficiency != "SUFFICIENT" + ): + raise DomainValidationError( + f"{name}: a PROMOTE references every result it used and its evidence is " + "SUFFICIENT (Doc 11 §26)" + ) + object.__setattr__(self, "required_checks", checks) + object.__setattr__(self, "verification_refs", refs) + if self.content_hash != self.compute_hash(): + raise HashMismatchError( + f"DATA-INT-010: PromotionEvidence of decision {self.decision_id} content_hash " + "does not match its content" + ) + + def _payload(self) -> dict[str, Any]: + data = self.to_dict() + del data["decision_id"] + del data["content_hash"] + return data + + def compute_hash(self) -> str: + return content_hash(self._payload()) + + @classmethod + def create( + cls, + *, + decision_id: str, + candidate_id: str, + parent_state_id: str, + required_checks: Iterable[RequiredCheck], + verification_refs: Iterable[str], + evidence_sufficiency: str, + policy_version: str, + decision: DecisionType, + reason: DecisionReason, + ) -> PromotionEvidence: + probe = { + "candidate_id": candidate_id, + "parent_state_id": parent_state_id, + "required_checks": [c.to_dict() for c in required_checks], + "verification_refs": list(verification_refs), + "evidence_sufficiency": evidence_sufficiency, + "policy_version": policy_version, + "decision": getattr(decision, "value", decision), + "reason": getattr(reason, "value", reason), + "new_state_id": None, + } + return cls( + decision_id=decision_id, + candidate_id=candidate_id, + parent_state_id=parent_state_id, + required_checks=tuple(required_checks), + verification_refs=tuple(verification_refs), + evidence_sufficiency=evidence_sufficiency, + policy_version=policy_version, + decision=decision, + reason=reason, + new_state_id=None, + content_hash=content_hash(probe), + ) + + def to_dict(self) -> dict[str, Any]: + return { + "decision_id": self.decision_id, + "candidate_id": self.candidate_id, + "parent_state_id": self.parent_state_id, + "required_checks": [c.to_dict() for c in self.required_checks], + "verification_refs": list(self.verification_refs), + "evidence_sufficiency": self.evidence_sufficiency, + "policy_version": self.policy_version, + "decision": self.decision.value, + "reason": self.reason.value, + "new_state_id": self.new_state_id, + "content_hash": self.content_hash, + } + + @classmethod + def from_dict(cls, data: Mapping[str, Any]) -> PromotionEvidence: + fields = require_keys(data, _EVIDENCE_KEYS, "PromotionEvidence") + return cls( + decision_id=fields["decision_id"], + candidate_id=fields["candidate_id"], + parent_state_id=fields["parent_state_id"], + required_checks=tuple( + RequiredCheck.from_dict(item) + for item in _list_of(fields["required_checks"], "required_checks") + ), + verification_refs=tuple(_list_of(fields["verification_refs"], "verification_refs")), + evidence_sufficiency=fields["evidence_sufficiency"], + policy_version=fields["policy_version"], + decision=parse_enum(fields["decision"], DecisionType, "decision"), + reason=parse_enum(fields["reason"], DecisionReason, "reason"), + new_state_id=fields["new_state_id"], + content_hash=fields["content_hash"], + ) + + +# --- the plan, the outcome and the oracle's verdict ----------------------------------------------- + + +@dataclass(frozen=True) +class ProofPlanEntry: + """Which source proves one required invariant (C-159), for the commit of P6b. + + VERIFIED: ``verification_id`` is the result that proves it. CARRIED_FORWARD: ``source_state_id`` + is the state whose reference is copied and ``evidence_ids`` are that reference's evidence.""" + + invariant_id: str + invariant_version: int + source: ProofSource + verification_id: str | None + source_state_id: str | None + evidence_ids: tuple[str, ...] + + def __post_init__(self) -> None: + require_text(self.invariant_id, "ProofPlanEntry.invariant_id") + require_int(self.invariant_version, "ProofPlanEntry.invariant_version", 1) + require_enum(self.source, ProofSource, "ProofPlanEntry.source") + verified = self.source is ProofSource.VERIFIED + if (self.verification_id is not None) != verified: + raise DomainValidationError( + "ProofPlanEntry: a VERIFIED entry names its result, a carried one does not" + ) + if (self.source_state_id is not None) == verified: + raise DomainValidationError( + "ProofPlanEntry: a carried entry names its source state, a verified one does not" + ) + if self.verification_id is not None: + require_uuid(self.verification_id, "ProofPlanEntry.verification_id") + if self.source_state_id is not None: + require_uuid(self.source_state_id, "ProofPlanEntry.source_state_id") + object.__setattr__( + self, + "evidence_ids", + tuple(require_uuid(e, "ProofPlanEntry.evidence_ids[]") for e in self.evidence_ids), + ) + + @property + def target_id(self) -> str: + return f"INVARIANT:{self.invariant_id}:{self.invariant_version}" + + +@dataclass(frozen=True) +class DecisionOutcome: + """What ``decide`` returns: the decision, the proof plan and the evidence (C-157).""" + + decision: PromotionDecision + proof_plan: tuple[ProofPlanEntry, ...] + evidence: PromotionEvidence + + def __post_init__(self) -> None: + if not isinstance(self.decision, PromotionDecision): + raise DomainValidationError("DecisionOutcome.decision: expected a PromotionDecision") + if not isinstance(self.evidence, PromotionEvidence): + raise DomainValidationError("DecisionOutcome.evidence: expected a PromotionEvidence") + plan = _objects(self.proof_plan, ProofPlanEntry, "DecisionOutcome.proof_plan") + if self.evidence.decision_id != self.decision.decision_id: + raise DomainValidationError("DecisionOutcome: the evidence belongs to another decision") + object.__setattr__(self, "proof_plan", plan) + + +@dataclass(frozen=True) +class OracleVerdict: + """What the independent oracle said about one invariant (Doc 09 §16). Evidence, not proof.""" + + invariant_id: str + invariant_version: int + result: VerificationResult + oracle_version: str + + def __post_init__(self) -> None: + if not isinstance(self.invariant_id, str) or not self.invariant_id.startswith("INV-"): + raise DomainValidationError("OracleVerdict.invariant_id: must be an INV-... id") + require_int(self.invariant_version, "OracleVerdict.invariant_version", 1) + require_enum(self.result, VerificationResult, "OracleVerdict.result") + require_text(self.oracle_version, "OracleVerdict.oracle_version") + + +# --- the policy ----------------------------------------------------------------------------------- + + +@dataclass(frozen=True) +class PromotionPolicy: + """The promotion policy (C-158 to C-161). Frozen data: nothing here reads configuration. + + ``non_success`` is the closed table of Doc 09 §20 (UNKNOWN, UNSUPPORTED, VERIFIER_ERROR to + REJECT, RETRY or ESCALATE); it never maps to PROMOTE. ``accept_oracle_for_unknown`` exists only + so that the refusal is explicit: oracle evidence is never proof (C-160). ``gate_verifiers`` + names the verifier each mandatory gate item must come from. + """ + + policy_version: str + invariant_registry_version: int + invariants: tuple[Invariant, ...] + extra_required: tuple[str, ...] + min_evidence_level: str + carry_forward_enabled: bool + non_success: tuple[tuple[VerificationResult, DecisionType], ...] + transient_errors: tuple[str, ...] + max_attempts: int + conflict_decision: DecisionType + automatic_enabled: bool + accept_oracle_for_unknown: bool + gate_verifiers: tuple[tuple[str, str, str], ...] + _by_id: dict[str, Invariant] = field( + init=False, repr=False, compare=False, default_factory=dict + ) + + def __post_init__(self) -> None: + name = "PromotionPolicy" + require_text(self.policy_version, f"{name}.policy_version") + require_int(self.invariant_registry_version, f"{name}.invariant_registry_version", 1) + definitions = _objects(self.invariants, Invariant, f"{name}.invariants") + by_id = {d.invariant_id: d for d in definitions} + if not definitions or len(by_id) != len(definitions): + raise DomainValidationError( + f"{name}.invariants: one definition per invariant id, at least one (C-41)" + ) + object.__setattr__( + self, "invariants", tuple(sorted(definitions, key=lambda d: d.invariant_id)) + ) + object.__setattr__(self, "_by_id", by_id) + object.__setattr__( + self, + "extra_required", + _texts(self.extra_required, f"{name}.extra_required", allowed=frozenset(by_id)), + ) + if self.min_evidence_level not in EVIDENCE_LEVELS: + raise DomainValidationError( + f"{name}.min_evidence_level: must be one of {EVIDENCE_LEVELS}" + ) + _bool(self.carry_forward_enabled, f"{name}.carry_forward_enabled") + _bool(self.automatic_enabled, f"{name}.automatic_enabled") + if _bool(self.accept_oracle_for_unknown, f"{name}.accept_oracle_for_unknown"): + raise DomainValidationError( + f"{name}: oracle evidence is never proof, so accept_oracle_for_unknown must be " + "False (ADR-010, C-54, C-160)" + ) + object.__setattr__(self, "non_success", self._table(self.non_success)) + object.__setattr__( + self, "transient_errors", _texts(self.transient_errors, f"{name}.transient_errors") + ) + if require_int(self.max_attempts, f"{name}.max_attempts", 1) > MAX_ATTEMPTS_LIMIT: + raise DomainValidationError(f"{name}.max_attempts: at most {MAX_ATTEMPTS_LIMIT}") + require_enum(self.conflict_decision, DecisionType, f"{name}.conflict_decision") + if self.conflict_decision not in (DecisionType.REJECT, DecisionType.ESCALATE): + raise DomainValidationError(f"{name}.conflict_decision: REJECT or ESCALATE, never else") + object.__setattr__(self, "gate_verifiers", self._gates(self.gate_verifiers)) + + @staticmethod + def _table( + value: object, + ) -> tuple[tuple[VerificationResult, DecisionType], ...]: + name = "PromotionPolicy.non_success" + if isinstance(value, str) or not isinstance(value, Iterable): + raise DomainValidationError(f"{name}: must be a list of pairs") + pairs = [] + for item in value: + if not isinstance(item, tuple) or len(item) != 2: + raise DomainValidationError(f"{name}: must be a list of pairs") + result = require_enum(item[0], VerificationResult, f"{name} key") + decision = require_enum(item[1], DecisionType, f"{name} value") + if decision not in NON_PROMOTE: + raise DomainValidationError(f"{name}: a non-success never maps to PROMOTE") + pairs.append((result, decision)) + if sorted(r.value for r, _ in pairs) != sorted(r.value for r in NON_SUCCESS_RESULTS): + raise DomainValidationError( + f"{name}: exactly one entry for each of UNKNOWN, UNSUPPORTED, VERIFIER_ERROR" + ) + return tuple(sorted(pairs, key=lambda pair: pair[0].value)) + + @staticmethod + def _gates(value: object) -> tuple[tuple[str, str, str], ...]: + name = "PromotionPolicy.gate_verifiers" + if isinstance(value, str) or not isinstance(value, Iterable): + raise DomainValidationError(f"{name}: must be a list of triples") + triples = [] + for item in value: + if not isinstance(item, tuple) or len(item) != 3: + raise DomainValidationError(f"{name}: must be a list of triples") + triples.append(tuple(require_text(part, f"{name}[]") for part in item)) + if sorted(t[0] for t in triples) != sorted(GATE_TARGETS): + raise DomainValidationError(f"{name}: exactly one verifier for each gate item") + return tuple(sorted((t[0], t[1], t[2]) for t in triples)) + + def definition(self, invariant_id: str) -> Invariant | None: + """The definition of ``invariant_id`` at the policy's registry version, if it has one.""" + return self._by_id.get(invariant_id) + + def gate_verifier(self, target_id: str) -> tuple[str, str]: + for target, verifier_id, verifier_version in self.gate_verifiers: + if target == target_id: + return verifier_id, verifier_version + raise DomainValidationError(f"PromotionPolicy: {target_id!r} is not a gate item") + + def non_success_decision( + self, result: VerificationResult, error_type: str | None = None + ) -> DecisionType: + """What a non-success result of a required item gives (C-158). A VERIFIER_ERROR of a + listed transient type is retried; an unlisted one follows the table.""" + if result not in NON_SUCCESS_RESULTS: + raise DomainValidationError(f"non_success_decision: {result} is not a non-success") + if result is VerificationResult.VERIFIER_ERROR and error_type in self.transient_errors: + return DecisionType.RETRY + return dict(self.non_success)[result] diff --git a/core/promotion/__init__.py b/core/promotion/__init__.py index ee629b7..e9c4f7c 100644 --- a/core/promotion/__init__.py +++ b/core/promotion/__init__.py @@ -2,11 +2,15 @@ Owning spec sections: Doc 09 §17-41 (conflicting evidence, preconditions, decision matrix, commit transaction, carry-forward, idempotency, concurrency). -Built in: P6a (policy, decide(), decision completeness) and P6b (commit -transaction, carry-forward, concurrency). +Built in: P6a (policy, decide(), decision completeness, applying a decision to the +candidate) and P6b (commit transaction, carry-forward, concurrency). -Import restrictions (tests/contract/test_architecture_boundaries.py): -must not import ``core.application`` (R2); must not import ``llm``, -``experiments``, ``scripts``, ``apps``, ``benchmark`` or ``oracle`` (R3). -Standard library only (R7). No code yet. +P6a is the decision half: ``decide`` is a pure function of its arguments that returns PROMOTE, +REJECT, RETRY or ESCALATE with every blocking reason; ``lifecycle.candidate_after`` applies the +decision to the candidate; ``policy`` builds the DAIL and Stateful-Full policies. Nothing here +commits anything or calls ``TrustedState.promote`` (P6b does). + +Import restrictions (tests/contract/test_architecture_boundaries.py): standard library and +``core.domain.*`` only (R18, C-157). In particular it never imports ``core.verification``: it +consumes the reports as domain objects, and it never runs or repairs verification (Doc 02 §15). """ diff --git a/core/promotion/policy.py b/core/promotion/policy.py new file mode 100644 index 0000000..9ef9b0a --- /dev/null +++ b/core/promotion/policy.py @@ -0,0 +1,120 @@ +"""The two promotion policies (P6a; Doc 09 §20, §28; C-22, C-157 to C-161). + +``dail_policy`` is the DAIL condition (carry-forward on). ``stateful_full_policy`` is the +Stateful-Full comparison condition of Doc 13: the same controller, the same table, the same budget, +with carry-forward disabled, so every required invariant has to be verified again (C-22). The two +differ in one field and a test pins that. + +Nothing here reads configuration. ``automatic_enabled`` has no default: the caller passes the +reviewed ``promotion.automatic_enabled`` value (Doc 14 §37), so a policy can never be built with the +emergency switch left to chance. + +Standard library and ``core.domain`` only (R18). +""" + +from __future__ import annotations + +from collections.abc import Iterable +from typing import Final + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.invariant import Invariant +from core.domain.promotion import PromotionPolicy + +# The verifier ids that the verification engine gives the two gate items (core.verification.engine). +# core.promotion may not import that package (R18), so they are copied here; a test pins them. +GATE_VERIFIERS: Final = ( + ("CONSISTENCY", "dail.verify.consistency", "1"), + ("STRUCTURAL", "dail.verify.structural", "1"), +) +DEFAULT_NON_SUCCESS: Final = ( + (VerificationResult.UNKNOWN, DecisionType.RETRY), + (VerificationResult.UNSUPPORTED, DecisionType.REJECT), + (VerificationResult.VERIFIER_ERROR, DecisionType.ESCALATE), +) +DEFAULT_MIN_EVIDENCE_LEVEL: Final = "L1" +DEFAULT_MAX_ATTEMPTS: Final = 3 + + +def _policy( + *, + carry_forward_enabled: bool, + policy_version: str, + invariants: Iterable[Invariant], + automatic_enabled: bool, + invariant_registry_version: int, + extra_required: Iterable[str], + transient_errors: Iterable[str], + max_attempts: int, + conflict_decision: DecisionType, + min_evidence_level: str, +) -> PromotionPolicy: + return PromotionPolicy( + policy_version=policy_version, + invariant_registry_version=invariant_registry_version, + invariants=tuple(invariants), + extra_required=tuple(extra_required), + min_evidence_level=min_evidence_level, + carry_forward_enabled=carry_forward_enabled, + non_success=DEFAULT_NON_SUCCESS, + transient_errors=tuple(transient_errors), + max_attempts=max_attempts, + conflict_decision=conflict_decision, + automatic_enabled=automatic_enabled, + accept_oracle_for_unknown=False, + gate_verifiers=GATE_VERIFIERS, + ) + + +def dail_policy( + *, + policy_version: str, + invariants: Iterable[Invariant], + automatic_enabled: bool, + invariant_registry_version: int = 1, + extra_required: Iterable[str] = (), + transient_errors: Iterable[str] = (), + max_attempts: int = DEFAULT_MAX_ATTEMPTS, + conflict_decision: DecisionType = DecisionType.ESCALATE, + min_evidence_level: str = DEFAULT_MIN_EVIDENCE_LEVEL, +) -> PromotionPolicy: + """The DAIL condition: an unaffected, protected invariant may be carried forward (C-159).""" + return _policy( + carry_forward_enabled=True, + policy_version=policy_version, + invariants=invariants, + automatic_enabled=automatic_enabled, + invariant_registry_version=invariant_registry_version, + extra_required=extra_required, + transient_errors=transient_errors, + max_attempts=max_attempts, + conflict_decision=conflict_decision, + min_evidence_level=min_evidence_level, + ) + + +def stateful_full_policy( + *, + policy_version: str, + invariants: Iterable[Invariant], + automatic_enabled: bool, + invariant_registry_version: int = 1, + extra_required: Iterable[str] = (), + transient_errors: Iterable[str] = (), + max_attempts: int = DEFAULT_MAX_ATTEMPTS, + conflict_decision: DecisionType = DecisionType.ESCALATE, + min_evidence_level: str = DEFAULT_MIN_EVIDENCE_LEVEL, +) -> PromotionPolicy: + """The Stateful-Full condition (Doc 13, C-22): nothing is carried forward.""" + return _policy( + carry_forward_enabled=False, + policy_version=policy_version, + invariants=invariants, + automatic_enabled=automatic_enabled, + invariant_registry_version=invariant_registry_version, + extra_required=extra_required, + transient_errors=transient_errors, + max_attempts=max_attempts, + conflict_decision=conflict_decision, + min_evidence_level=min_evidence_level, + ) diff --git a/tests/unit/test_promotion_domain.py b/tests/unit/test_promotion_domain.py new file mode 100644 index 0000000..3e139ca --- /dev/null +++ b/tests/unit/test_promotion_domain.py @@ -0,0 +1,365 @@ +"""The promotion types (P6a step 2; Doc 05 §15, Doc 11 §26; C-157 to C-161). + +Expected values come from the spec text: a PROMOTE "must reference the evidence that satisfied the +promotion policy"; "non-promotion decisions must preserve their blocking reasons for audit" +(Doc 05 §15); ``committed_state_id`` is null until the commit of P6b (DATA-INT-004); the five +decision reasons of C-157 are a closed vocabulary; ``PromotionEvidence`` has the fields of Doc 11 +§26 and a PROMOTE "must reference every mandatory verification result used". +""" + +from __future__ import annotations + +import dataclasses +import unittest +from typing import Any + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.errors import DomainValidationError, HashMismatchError +from core.domain.promotion import ( + BlockingCondition, + DecisionReason, + OracleVerdict, + PromotionDecision, + PromotionEvidence, + PromotionInputError, + ProofSource, + RequiredCheck, +) +from tests.domain_builders import at, uid + +CANDIDATE = uid(3001) +PARENT = uid(1) +RESULT_A, RESULT_B = uid(7001), uid(7002) + + +def checks() -> tuple[RequiredCheck, ...]: + return ( + RequiredCheck("CONSISTENCY", "GATE", ProofSource.VERIFIED, RESULT_A), + RequiredCheck("INVARIANT:INV-SEC-001:1", "INVARIANT", ProofSource.VERIFIED, RESULT_B), + ) + + +def blocking(code: DecisionReason = DecisionReason.REQUIRED_CHECK_FAILED) -> BlockingCondition: + return BlockingCondition(code, DecisionType.REJECT, "INVARIANT:INV-SEC-001:1", "result FAIL") + + +def decision(**changes: Any) -> PromotionDecision: + fields: dict[str, Any] = { + "decision_id": uid(9001), + "candidate_id": CANDIDATE, + "parent_state_id": PARENT, + "decision": DecisionType.PROMOTE, + "reason": DecisionReason.ALL_REQUIRED_PROVEN, + "policy_version": "policy-1", + "attempt_number": 1, + "required_checks": checks(), + "blocking_conditions": (), + "supporting_results": (RESULT_A, RESULT_B), + "created_at": at(5), + } + fields.update(changes) + return PromotionDecision.create(**fields) + + +def rejection(**changes: Any) -> PromotionDecision: + fields: dict[str, Any] = { + "decision": DecisionType.REJECT, + "reason": DecisionReason.REQUIRED_CHECK_FAILED, + "blocking_conditions": (blocking(),), + "supporting_results": (RESULT_A,), + } + fields.update(changes) + return decision(**fields) + + +class TestVocabularies(unittest.TestCase): + def test_the_reasons_are_the_closed_list_of_c157(self) -> None: + self.assertEqual( + {reason.value for reason in DecisionReason}, + { + "STALE_PARENT", + "STRUCTURAL_FAILURE", + "INCONSISTENT_REPORTS", + "REQUIRED_CHECK_FAILED", + "REQUIRED_UNKNOWN", + "REQUIRED_UNSUPPORTED", + "VERIFIER_ERROR", + "INSUFFICIENT_EVIDENCE", + "EVIDENCE_NOT_SUFFICIENT", + "EVIDENCE_STALE", + "EVIDENCE_CONFLICT", + "RETRY_BUDGET_EXHAUSTED", + "POLICY_REGISTRY_REGRESSION", + "AUTOMATIC_PROMOTION_DISABLED", + "DECISION_INCOMPLETE", + "ALL_REQUIRED_PROVEN", + }, + ) + + def test_a_proof_comes_from_verification_or_from_carrying_forward(self) -> None: + self.assertEqual({s.value for s in ProofSource}, {"VERIFIED", "CARRIED_FORWARD"}) + + def test_an_input_error_is_a_domain_validation_error(self) -> None: + self.assertTrue(issubclass(PromotionInputError, DomainValidationError)) + + +class TestRequiredCheckAndBlockingCondition(unittest.TestCase): + def test_a_verified_check_names_its_result_and_a_carried_one_names_none(self) -> None: + RequiredCheck("INVARIANT:INV-SEC-002:1", "INVARIANT", ProofSource.VERIFIED, RESULT_A) + RequiredCheck("INVARIANT:INV-SEC-002:1", "INVARIANT", ProofSource.CARRIED_FORWARD, None) + RequiredCheck("INVARIANT:INV-SEC-002:1", "INVARIANT", None, None) + for source, result in ( + (ProofSource.VERIFIED, None), + (ProofSource.CARRIED_FORWARD, RESULT_A), + (None, RESULT_A), + ): + with ( + self.subTest(source=source, result=result), + self.assertRaises(DomainValidationError), + ): + RequiredCheck("INVARIANT:INV-SEC-002:1", "INVARIANT", source, result) + + def test_a_check_has_a_known_kind_and_a_text_target(self) -> None: + for kind in ("GATE", "INVARIANT", "BASELINE"): + RequiredCheck("T", kind, None, None) + with self.assertRaises(DomainValidationError): + RequiredCheck("T", "OTHER", None, None) + with self.assertRaises(DomainValidationError): + RequiredCheck("", "GATE", None, None) + + def test_a_blocking_condition_is_never_a_promote(self) -> None: + BlockingCondition(DecisionReason.STALE_PARENT, DecisionType.REJECT, "STATE", "x") + with self.assertRaises(DomainValidationError): + BlockingCondition(DecisionReason.STALE_PARENT, DecisionType.PROMOTE, "STATE", "x") + with self.assertRaises(DomainValidationError): + BlockingCondition("STALE_PARENT", DecisionType.REJECT, "STATE", "x") # type: ignore[arg-type] + with self.assertRaises(DomainValidationError): + BlockingCondition(DecisionReason.STALE_PARENT, DecisionType.REJECT, "", "x") + + def test_round_trips(self) -> None: + condition = blocking() + self.assertEqual(BlockingCondition.from_dict(condition.to_dict()), condition) + check = checks()[1] + self.assertEqual(RequiredCheck.from_dict(check.to_dict()), check) + + +class TestPromotionDecision(unittest.TestCase): + def test_a_promote_references_the_results_that_satisfied_the_policy(self) -> None: + made = decision() + self.assertEqual(made.decision, DecisionType.PROMOTE) + self.assertEqual(made.supporting_results, (RESULT_A, RESULT_B)) + self.assertIsNone(made.committed_state_id) + with self.assertRaises(DomainValidationError): + decision(supporting_results=()) + + def test_a_promote_has_no_blocking_condition_and_the_proven_reason(self) -> None: + with self.assertRaises(DomainValidationError): + decision(blocking_conditions=(blocking(),)) + with self.assertRaises(DomainValidationError): + decision(reason=DecisionReason.REQUIRED_CHECK_FAILED) + + def test_a_non_promote_preserves_its_blocking_reasons(self) -> None: + for kind in (DecisionType.REJECT, DecisionType.RETRY, DecisionType.ESCALATE): + with self.subTest(decision=kind): + made = rejection(decision=kind) + self.assertEqual(made.blocking_conditions, (blocking(),)) + with self.assertRaises(DomainValidationError): + rejection(decision=kind, blocking_conditions=()) + + def test_a_non_promote_cannot_claim_everything_is_proven(self) -> None: + with self.assertRaises(DomainValidationError): + rejection(reason=DecisionReason.ALL_REQUIRED_PROVEN) + + def test_the_reason_is_one_of_the_blocking_conditions(self) -> None: + with self.assertRaises(DomainValidationError): + rejection(reason=DecisionReason.STRUCTURAL_FAILURE) + made = rejection( + reason=DecisionReason.STRUCTURAL_FAILURE, + blocking_conditions=( + blocking(), + BlockingCondition( + DecisionReason.STRUCTURAL_FAILURE, DecisionType.REJECT, "STRUCTURAL", "x" + ), + ), + ) + self.assertEqual(len(made.blocking_conditions), 2) + + def test_the_commit_is_not_part_of_p6a(self) -> None: + # DATA-INT-004: committed_state_id is set only by the commit of P6b + with self.assertRaises(DomainValidationError): + dataclasses.replace(decision(), committed_state_id=uid(55)) + + def test_ids_and_text_are_checked(self) -> None: + for field, value in ( + ("candidate_id", "not-a-uuid"), + ("parent_state_id", "x"), + ("decision_id", ""), + ("policy_version", ""), + ("attempt_number", 0), + ("attempt_number", True), + ("decision", "PROMOTE"), + ("reason", "ALL_REQUIRED_PROVEN"), + ): + with self.subTest(field=field, value=value), self.assertRaises(DomainValidationError): + decision(**{field: value}) + + def test_supporting_results_are_sorted_distinct_uuids(self) -> None: + with self.assertRaises(DomainValidationError): + decision(supporting_results=(RESULT_B, RESULT_A)) + with self.assertRaises(DomainValidationError): + decision(supporting_results=(RESULT_A, RESULT_A)) + with self.assertRaises(DomainValidationError): + decision(supporting_results=("not-a-uuid",)) + + def test_required_checks_are_sorted_and_one_per_target(self) -> None: + first, second = checks() + with self.assertRaises(DomainValidationError): + decision(required_checks=(second, first)) + with self.assertRaises(DomainValidationError): + decision(required_checks=(first, first)) + + def test_blocking_conditions_are_sorted_and_distinct(self) -> None: + low = BlockingCondition(DecisionReason.EVIDENCE_STALE, DecisionType.REJECT, "A", "x") + high = BlockingCondition( + DecisionReason.REQUIRED_CHECK_FAILED, DecisionType.REJECT, "B", "x" + ) + both = rejection(blocking_conditions=(low, high), reason=DecisionReason.EVIDENCE_STALE) + self.assertEqual( + both.blocking_conditions, tuple(sorted((low, high), key=lambda c: c.sort_key())) + ) + with self.assertRaises(DomainValidationError): + rejection(blocking_conditions=(high, high)) + + def test_the_hash_is_recomputed_by_the_constructor(self) -> None: + made = decision() + with self.assertRaises(HashMismatchError): + dataclasses.replace(made, policy_version="policy-2") + with self.assertRaises(HashMismatchError): + dataclasses.replace(made, content_hash="0" * 64) + + def test_the_hash_ignores_the_id_and_the_clock_and_follows_the_content(self) -> None: + a = decision() + b = decision(decision_id=uid(9002), created_at=at(99)) + self.assertEqual(a.content_hash, b.content_hash) + for change in ( + {"policy_version": "policy-2"}, + {"attempt_number": 2}, + {"supporting_results": (RESULT_A,)}, + {"parent_state_id": uid(2)}, + ): + with self.subTest(change=change): + self.assertNotEqual(decision(**change).content_hash, a.content_hash) + + def test_a_round_trip_keeps_everything(self) -> None: + for made in (decision(), rejection(), rejection(decision=DecisionType.ESCALATE)): + with self.subTest(decision=made.decision): + self.assertEqual(PromotionDecision.from_dict(made.to_dict()), made) + + def test_from_dict_refuses_missing_extra_and_unknown_values(self) -> None: + data = decision().to_dict() + for broken in ( + {k: v for k, v in data.items() if k != "reason"}, + {**data, "extra": 1}, + {**data, "reason": "MADE_UP"}, + {**data, "decision": "MAYBE"}, + ): + with self.subTest(keys=sorted(broken)), self.assertRaises(DomainValidationError): + PromotionDecision.from_dict(broken) + + def test_the_dict_is_plain_json(self) -> None: + import json + + text = json.dumps(rejection().to_dict(), sort_keys=True) + self.assertEqual(json.loads(text), rejection().to_dict()) + + +class TestPromotionEvidence(unittest.TestCase): + def evidence(self, **changes: Any) -> PromotionEvidence: + fields: dict[str, Any] = { + "decision_id": uid(9001), + "candidate_id": CANDIDATE, + "parent_state_id": PARENT, + "required_checks": checks(), + "verification_refs": (RESULT_A, RESULT_B), + "evidence_sufficiency": "SUFFICIENT", + "policy_version": "policy-1", + "decision": DecisionType.PROMOTE, + "reason": DecisionReason.ALL_REQUIRED_PROVEN, + } + fields.update(changes) + return PromotionEvidence.create(**fields) + + def test_the_fields_of_doc_11_section_26(self) -> None: + made = self.evidence() + self.assertEqual( + set(made.to_dict()), + { + "decision_id", + "candidate_id", + "parent_state_id", + "required_checks", + "verification_refs", + "evidence_sufficiency", + "policy_version", + "decision", + "reason", + "new_state_id", + "content_hash", + }, + ) + self.assertIsNone(made.new_state_id) + + def test_a_promote_references_every_mandatory_result_it_used(self) -> None: + with self.assertRaises(DomainValidationError): + self.evidence(verification_refs=()) + with self.assertRaises(DomainValidationError): + self.evidence(evidence_sufficiency="INSUFFICIENT") + + def test_a_non_promote_may_say_the_evidence_is_insufficient(self) -> None: + made = self.evidence( + decision=DecisionType.REJECT, + reason=DecisionReason.INSUFFICIENT_EVIDENCE, + evidence_sufficiency="INSUFFICIENT", + verification_refs=(RESULT_A,), + ) + self.assertEqual(made.evidence_sufficiency, "INSUFFICIENT") + + def test_the_sufficiency_is_a_closed_value(self) -> None: + with self.assertRaises(DomainValidationError): + self.evidence(evidence_sufficiency="MAYBE") + + def test_the_new_state_is_not_part_of_p6a(self) -> None: + with self.assertRaises(DomainValidationError): + dataclasses.replace(self.evidence(), new_state_id=uid(77)) + + def test_hash_and_round_trip(self) -> None: + made = self.evidence() + self.assertEqual(PromotionEvidence.from_dict(made.to_dict()), made) + with self.assertRaises(HashMismatchError): + dataclasses.replace(made, policy_version="policy-2") + + def test_the_references_are_sorted_distinct_uuids(self) -> None: + with self.assertRaises(DomainValidationError): + self.evidence(verification_refs=(RESULT_B, RESULT_A)) + with self.assertRaises(DomainValidationError): + self.evidence(verification_refs=("x",)) + + +class TestOracleVerdict(unittest.TestCase): + def test_a_verdict_names_an_invariant_a_result_and_an_oracle_version(self) -> None: + verdict = OracleVerdict("INV-SEC-001", 1, VerificationResult.FAIL, "oracle-1") + self.assertEqual(verdict.result, VerificationResult.FAIL) + + def test_malformed_verdicts_are_refused(self) -> None: + for args in ( + ("SEC-1", 1, VerificationResult.PASS, "o"), + ("INV-SEC-001", 0, VerificationResult.PASS, "o"), + ("INV-SEC-001", 1, "PASS", "o"), + ("INV-SEC-001", 1, VerificationResult.PASS, ""), + ): + with self.subTest(args=args), self.assertRaises(DomainValidationError): + OracleVerdict(*args) # type: ignore[arg-type] + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_promotion_policy.py b/tests/unit/test_promotion_policy.py new file mode 100644 index 0000000..c74fca4 --- /dev/null +++ b/tests/unit/test_promotion_policy.py @@ -0,0 +1,224 @@ +"""The promotion policy (P6a step 2; Doc 09 §17-§23, §28, Doc 14 §37; C-22, C-41, C-157 to C-161). + +Expected values come from the prompt's spec extracts: the non-success table (UNKNOWN retries, +UNSUPPORTED rejects, VERIFIER_ERROR escalates unless its type is listed as transient); the retry +budget is validated 1..10 with default 3; the evidence level is "L1"; ``accept_oracle_for_unknown`` +must be refused; the Stateful-Full policy differs from the DAIL policy in carry-forward only (C-22). +""" + +from __future__ import annotations + +import dataclasses +import unittest +from typing import Any + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.errors import DomainValidationError +from core.domain.promotion import PromotionPolicy +from core.promotion.policy import ( + DEFAULT_NON_SUCCESS, + GATE_VERIFIERS, + dail_policy, + stateful_full_policy, +) +from tests.domain_builders import FUNC, SEC, invariant + +U, S, E = ( + VerificationResult.UNKNOWN, + VerificationResult.UNSUPPORTED, + VerificationResult.VERIFIER_ERROR, +) + + +def invariants() -> tuple[Any, ...]: + return (invariant(FUNC), invariant(SEC)) + + +def dail(**changes: Any) -> PromotionPolicy: + fields: dict[str, Any] = { + "policy_version": "policy-1", + "invariants": invariants(), + "automatic_enabled": True, + } + fields.update(changes) + return dail_policy(**fields) + + +def raw(**changes: Any) -> PromotionPolicy: + """The class itself, for values the constructors would not offer.""" + fields: dict[str, Any] = { + "policy_version": "policy-1", + "invariant_registry_version": 1, + "invariants": invariants(), + "extra_required": (), + "min_evidence_level": "L1", + "carry_forward_enabled": True, + "non_success": DEFAULT_NON_SUCCESS, + "transient_errors": (), + "max_attempts": 3, + "conflict_decision": DecisionType.ESCALATE, + "automatic_enabled": True, + "accept_oracle_for_unknown": False, + "gate_verifiers": GATE_VERIFIERS, + } + fields.update(changes) + return PromotionPolicy(**fields) + + +class TestDefaults(unittest.TestCase): + def test_the_dail_policy_defaults(self) -> None: + policy = dail() + self.assertTrue(policy.carry_forward_enabled) + self.assertEqual(policy.min_evidence_level, "L1") + self.assertEqual(policy.max_attempts, 3) + self.assertEqual(policy.conflict_decision, DecisionType.ESCALATE) + self.assertEqual(policy.transient_errors, ()) + self.assertFalse(policy.accept_oracle_for_unknown) + self.assertEqual(policy.extra_required, ()) + + def test_the_default_non_success_table(self) -> None: + policy = dail() + self.assertEqual(policy.non_success_decision(U), DecisionType.RETRY) + self.assertEqual(policy.non_success_decision(S), DecisionType.REJECT) + self.assertEqual(policy.non_success_decision(E), DecisionType.ESCALATE) + + def test_a_listed_transient_error_type_is_retried(self) -> None: + policy = dail(transient_errors=("TimeoutError",)) + self.assertEqual(policy.non_success_decision(E, "TimeoutError"), DecisionType.RETRY) + self.assertEqual(policy.non_success_decision(E, "ValueError"), DecisionType.ESCALATE) + self.assertEqual(policy.non_success_decision(E, None), DecisionType.ESCALATE) + self.assertEqual(policy.non_success_decision(U, "TimeoutError"), DecisionType.RETRY) + + def test_only_a_non_success_has_a_decision(self) -> None: + policy = dail() + for result in (VerificationResult.PASS, VerificationResult.FAIL): + with self.subTest(result=result), self.assertRaises(DomainValidationError): + policy.non_success_decision(result) + + def test_the_gate_verifiers_are_those_of_the_verification_engine(self) -> None: + # tests may import both packages; the policy copies the ids because core.promotion may not + from core.verification.engine import ( + CONSISTENCY_ID, + CONSISTENCY_VERIFIER, + STRUCTURAL_ID, + STRUCTURAL_VERIFIER, + ) + + self.assertEqual( + dict((target, (vid, ver)) for target, vid, ver in GATE_VERIFIERS), + {STRUCTURAL_ID: STRUCTURAL_VERIFIER, CONSISTENCY_ID: CONSISTENCY_VERIFIER}, + ) + + +class TestStatefulFull(unittest.TestCase): + def test_it_differs_from_the_dail_policy_in_carry_forward_only(self) -> None: + # C-22: the same controller, carry-forward disabled + full = stateful_full_policy( + policy_version="policy-1", invariants=invariants(), automatic_enabled=True + ) + self.assertFalse(full.carry_forward_enabled) + self.assertEqual(dataclasses.replace(full, carry_forward_enabled=True), dail()) + + def test_the_switch_has_no_default(self) -> None: + with self.assertRaises(TypeError): + dail_policy(policy_version="p", invariants=invariants()) # type: ignore[call-arg] + with self.assertRaises(TypeError): + stateful_full_policy(policy_version="p", invariants=invariants()) # type: ignore[call-arg] + + +class TestValidation(unittest.TestCase): + def test_the_oracle_cannot_be_accepted(self) -> None: + with self.assertRaises(DomainValidationError): + raw(accept_oracle_for_unknown=True) + + def test_the_retry_budget_is_one_to_ten(self) -> None: + for good in (1, 3, 10): + self.assertEqual(raw(max_attempts=good).max_attempts, good) + for bad in (0, 11, -1, True, "3", 2.5): + with self.subTest(bad=bad), self.assertRaises(DomainValidationError): + raw(max_attempts=bad) + + def test_the_evidence_level_is_a_known_level(self) -> None: + self.assertEqual(raw(min_evidence_level="L0").min_evidence_level, "L0") + with self.assertRaises(DomainValidationError): + raw(min_evidence_level="L9") + + def test_the_conflict_decision_is_reject_or_escalate(self) -> None: + for good in (DecisionType.REJECT, DecisionType.ESCALATE): + self.assertEqual(raw(conflict_decision=good).conflict_decision, good) + for bad in (DecisionType.PROMOTE, DecisionType.RETRY, "REJECT"): + with self.subTest(bad=bad), self.assertRaises(DomainValidationError): + raw(conflict_decision=bad) + + def test_the_non_success_table_is_closed_and_never_promotes(self) -> None: + good = ((U, DecisionType.REJECT), (S, DecisionType.REJECT), (E, DecisionType.RETRY)) + self.assertEqual(raw(non_success=good).non_success_decision(U), DecisionType.REJECT) + for bad in ( + ((U, DecisionType.RETRY), (S, DecisionType.REJECT)), + ( + (U, DecisionType.RETRY), + (S, DecisionType.REJECT), + (E, DecisionType.ESCALATE), + (U, DecisionType.RETRY), + ), + ((U, DecisionType.PROMOTE), (S, DecisionType.REJECT), (E, DecisionType.ESCALATE)), + ( + (VerificationResult.PASS, DecisionType.REJECT), + (S, DecisionType.REJECT), + (E, DecisionType.ESCALATE), + ), + ((U, "RETRY"), (S, DecisionType.REJECT), (E, DecisionType.ESCALATE)), + ): + with self.subTest(bad=bad), self.assertRaises(DomainValidationError): + raw(non_success=bad) + + def test_the_registry_version_and_the_texts(self) -> None: + for field, value in ( + ("invariant_registry_version", 0), + ("invariant_registry_version", True), + ("policy_version", ""), + ("transient_errors", ("",)), + ("transient_errors", "TimeoutError"), + ("extra_required", "INV-SEC-001"), + ("carry_forward_enabled", 1), + ("automatic_enabled", "yes"), + ): + with self.subTest(field=field, value=value), self.assertRaises(DomainValidationError): + raw(**{field: value}) + + def test_the_registry_holds_one_definition_per_id_at_the_policy_version(self) -> None: + sec = invariant(SEC) + with self.assertRaises(DomainValidationError): + raw(invariants=(sec, sec)) + with self.assertRaises(DomainValidationError): + raw(invariants=()) + with self.assertRaises(DomainValidationError): + raw(invariants=("INV-SEC-001",)) + policy = raw(invariants=(invariant(SEC), invariant(FUNC))) + self.assertEqual([d.invariant_id for d in policy.invariants], [FUNC, SEC]) + self.assertEqual(policy.definition(SEC), invariant(SEC)) + self.assertIsNone(policy.definition("INV-SEC-009")) + + def test_an_extra_required_invariant_must_be_defined(self) -> None: + self.assertEqual(raw(extra_required=(FUNC,)).extra_required, (FUNC,)) + with self.assertRaises(DomainValidationError): + raw(extra_required=("INV-SEC-009",)) + with self.assertRaises(DomainValidationError): + raw(extra_required=(SEC, SEC)) + + def test_both_gate_items_name_a_verifier(self) -> None: + only = (GATE_VERIFIERS[0],) + with self.assertRaises(DomainValidationError): + raw(gate_verifiers=only) + with self.assertRaises(DomainValidationError): + raw(gate_verifiers=(("OTHER", "v", "1"), GATE_VERIFIERS[1])) + with self.assertRaises(DomainValidationError): + raw(gate_verifiers=(("STRUCTURAL", "", "1"), GATE_VERIFIERS[1])) + + def test_the_policy_is_frozen(self) -> None: + with self.assertRaises(dataclasses.FrozenInstanceError): + dail().carry_forward_enabled = False # type: ignore[misc] + + +if __name__ == "__main__": + unittest.main() From 94ea4f9d75eabb301d3f1aec835da229a7908c3c Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:32:43 +0530 Subject: [PATCH 4/8] =?UTF-8?q?P6a=20step=203:=20InvariantProof.carry=5Ffo?= =?UTF-8?q?rward=20needs=20the=20impact=20report=20(Doc=2006=20=C2=A714,?= =?UTF-8?q?=20Doc=2009=20=C2=A728;=20C-45,=20C-141,=20C-159)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit carry_forward(parent_ref, candidate, impact) now refuses unless the impact report of exactly this candidate and parent says the invariant is unaffected with eligible evidence (ImpactReport.carry_forward_ok): an affected, uncertain or unmentioned invariant, a report for another candidate, parent or version, and a report whose hash no longer recomputes all raise. The callers got the new argument only: tests/unit/test_proof.py (8 calls), tests/adversarial/test_state_machine_rules.py (1) and tests/domain_builders.carried_proof (which feeds tests/unit/test_promotion_coverage.py). The 33 changed or new tests were shown failing first (31 TypeErrors), and 5 scratch-copy mutants of the new check are killed. Co-Authored-By: Claude Sonnet 5.5 --- core/domain/invariant.py | 31 ++++- tests/adversarial/test_state_machine_rules.py | 10 +- tests/domain_builders.py | 8 +- tests/promotion_builders.py | 55 ++++++++ tests/unit/test_proof.py | 130 ++++++++++++++++-- 5 files changed, 220 insertions(+), 14 deletions(-) create mode 100644 tests/promotion_builders.py diff --git a/core/domain/invariant.py b/core/domain/invariant.py index 9b5fbca..b687533 100644 --- a/core/domain/invariant.py +++ b/core/domain/invariant.py @@ -383,12 +383,21 @@ def for_baseline( ) @classmethod - def carry_forward(cls, parent_ref: InvariantRef, candidate: object) -> InvariantProof: + def carry_forward( + cls, parent_ref: InvariantRef, candidate: object, impact: object + ) -> InvariantProof: """The proof of an invariant that the candidate leaves as the current state has it (origin CARRIED_FORWARD). Status, evidence and verification time are copied unchanged, so a VIOLATED or UNCERTAIN reference stays that way. A PROTECTED reference must still satisfy - proof, i.e. must not be invalidated (C-40). Whether carrying forward is permitted for an - invariant the candidate affects is P6 policy (C-22).""" + proof, i.e. must not be invalidated (C-40). + + C-45: the impact report of exactly this candidate and parent must say that the invariant is + unaffected and that its prior evidence is eligible (``carry_forward_ok``, C-141). An + affected, uncertain or unmentioned invariant, or a report that is for another candidate or + parent, is for another version, or no longer recomputes its hash, is refused: a regression + cannot hide behind the parent's old evidence. Whether the policy permits carrying forward at + all is decided by the Promotion Controller (C-22, C-159).""" + from core.domain.impact import ImpactReport from core.domain.state import CandidateState if not isinstance(parent_ref, InvariantRef): @@ -402,6 +411,22 @@ def carry_forward(cls, parent_ref: InvariantRef, candidate: object) -> Invariant "C-40: the reference belongs to state " f"{parent_ref.state_id}, not the candidate's parent {candidate.parent_state_id}" ) + if not isinstance(impact, ImpactReport): + raise DomainValidationError( + "C-45: carry_forward needs the ImpactReport of this candidate and parent" + ) + if not impact.carry_forward_ok( + parent_ref.invariant_id, + parent_ref.invariant_version, + candidate_id=candidate.candidate_id, + parent_state_id=candidate.parent_state_id, + ): + raise DomainValidationError( + f"C-45: the impact report does not allow carrying {parent_ref.invariant_id} " + f"(version {parent_ref.invariant_version}) forward: it is affected, uncertain, " + "unmentioned or without eligible evidence, or the report is not for this " + "candidate and parent, or its hash no longer recomputes" + ) if parent_ref.status is InvariantStatus.PROTECTED and not parent_ref.can_satisfy_proof(): raise DomainValidationError( f"C-40: the PROTECTED reference to {parent_ref.invariant_id} was invalidated " diff --git a/tests/adversarial/test_state_machine_rules.py b/tests/adversarial/test_state_machine_rules.py index 717031d..de181d6 100644 --- a/tests/adversarial/test_state_machine_rules.py +++ b/tests/adversarial/test_state_machine_rules.py @@ -64,6 +64,7 @@ uid, verified_proof, ) +from tests.promotion_builders import impact_for CS = CandidateStatus S = InvariantStatus @@ -463,7 +464,14 @@ def test_a_violated_invariant_cannot_be_recorded_protected_without_an_evaluation promote(candidate, v0, proofs=[sec, proof(FUNC, S.PROTECTED, evidence=12)]) # (c) Carrying the reference forward keeps it VIOLATED. carried = promote( - candidate, v0, proofs=[sec, InvariantProof.carry_forward(ref_of(v0, FUNC), candidate)] + candidate, + v0, + proofs=[ + sec, + InvariantProof.carry_forward( + ref_of(v0, FUNC), candidate, impact_for(v0, candidate, carry=(FUNC,)) + ), + ], ) self.assertEqual(ref_of(carried, FUNC).status, S.VIOLATED) self.assertFalse(ref_of(carried, FUNC).can_satisfy_proof()) diff --git a/tests/domain_builders.py b/tests/domain_builders.py index 6611278..a0f2163 100644 --- a/tests/domain_builders.py +++ b/tests/domain_builders.py @@ -205,8 +205,12 @@ def verified_proof( def carried_proof( parent: TrustedState, candidate: CandidateState, invariant_id: str = SEC ) -> InvariantProof: - """A CARRIED_FORWARD proof copied from the parent's reference (C-40).""" - return InvariantProof.carry_forward(parent_ref(parent, invariant_id), candidate) + """A CARRIED_FORWARD proof copied from the parent's reference (C-40), with an impact report + that says the candidate leaves the invariant alone and its evidence is eligible (C-45).""" + from tests.promotion_builders import impact_for + + impact = impact_for(parent, candidate, carry=(invariant_id,)) + return InvariantProof.carry_forward(parent_ref(parent, invariant_id), candidate, impact) def baseline( diff --git a/tests/promotion_builders.py b/tests/promotion_builders.py new file mode 100644 index 0000000..9aa775d --- /dev/null +++ b/tests/promotion_builders.py @@ -0,0 +1,55 @@ +"""Builders for the promotion tests (P6a). Not a test module. + +Tests may import every package; ``core.promotion`` may import only ``core.domain`` (R18). +Everything is deterministic: ids come from ``tests.domain_builders.uid`` and times from ``at``. +""" + +from __future__ import annotations + +from collections.abc import Iterable + +from core.domain.impact import ImpactReport +from core.domain.invariant import InvariantRef +from core.domain.state import CandidateState, TrustedState + + +def _ref(parent: TrustedState, invariant_id: str) -> InvariantRef: + return next(r for r in parent.invariant_refs if r.invariant_id == invariant_id) + + +def impact_for( + parent: TrustedState, + candidate: CandidateState, + *, + carry: Iterable[str] = (), + affected: Iterable[str] = (), + uncertain: Iterable[str] = (), + ineligible: Iterable[str] = (), + versions: dict[str, int] | None = None, +) -> ImpactReport: + """An impact report of ``candidate`` against ``parent``. + + ``carry`` are unaffected invariants whose prior evidence is eligible (the parent reference's + own evidence); ``ineligible`` are unaffected but not eligible; ``affected`` and ``uncertain`` + are the impacted ones, which owe a work item. ``versions`` overrides the invariant version the + report names (default: the version of the parent's reference).""" + from tests import impact_builders as ib + + def version(invariant_id: str) -> int: + if versions and invariant_id in versions: + return versions[invariant_id] + return _ref(parent, invariant_id).invariant_version + + impacted = [ib.affected_invariant(i, version(i)) for i in affected] + [ + ib.uncertain_invariant(i, version(i)) for i in uncertain + ] + kept = [ + ib.unaffected(i, version(i), eligible=True, evidence=_ref(parent, i).evidence_ids) + for i in carry + ] + [ib.unaffected(i, version(i)) for i in ineligible] + return ib.report( + affected=impacted, + unaffected_invariants=kept, + parent_state_id=parent.state_id, + candidate_id=candidate.candidate_id, + ) diff --git a/tests/unit/test_proof.py b/tests/unit/test_proof.py index 53a277c..d86fb94 100644 --- a/tests/unit/test_proof.py +++ b/tests/unit/test_proof.py @@ -18,6 +18,7 @@ IllegalTransitionError, UnauthorizedConstructionError, ) +from core.domain.impact import ImpactReport from core.domain.invariant import InvariantEvaluation, InvariantProof, InvariantRef from tests.domain_builders import ( FUNC, @@ -29,6 +30,7 @@ uid, verified_proof, ) +from tests.promotion_builders import impact_for EVIDENCE = uid(1500) @@ -64,7 +66,9 @@ def setUp(self) -> None: self.candidate = new_candidate(self.v0) self.baseline_proof = proof(FUNC, S.VIOLATED, evidence=2) self.carried = InvariantProof.carry_forward( - next(r for r in self.v0.invariant_refs if r.invariant_id == FUNC), self.candidate + next(r for r in self.v0.invariant_refs if r.invariant_id == FUNC), + self.candidate, + impact_for(self.v0, self.candidate, carry=(FUNC,)), ) def test_direct_construction_is_refused_for_every_origin(self) -> None: @@ -177,10 +181,14 @@ def setUp(self) -> None: def ref(self, invariant_id: str) -> InvariantRef: return next(r for r in self.v0.invariant_refs if r.invariant_id == invariant_id) + def impact(self, invariant_id: str) -> ImpactReport: + """An impact report that leaves ``invariant_id`` alone and offers its evidence (C-45).""" + return impact_for(self.v0, self.candidate, carry=(invariant_id,)) + def test_status_evidence_and_time_are_copied_unchanged(self) -> None: for invariant_id in (SEC, FUNC, "INV-SEC-002"): ref = self.ref(invariant_id) - p = InvariantProof.carry_forward(ref, self.candidate) + p = InvariantProof.carry_forward(ref, self.candidate, self.impact(invariant_id)) with self.subTest(invariant=invariant_id): self.assertIs(p.origin, ProofOrigin.CARRIED_FORWARD) self.assertEqual(p.status, ref.status) # VIOLATED and UNCERTAIN stay as they are @@ -190,7 +198,7 @@ def test_status_evidence_and_time_are_copied_unchanged(self) -> None: self.assertEqual(p.invariant_version, ref.invariant_version) def test_it_is_bound_to_the_candidate_and_to_the_state_it_came_from(self) -> None: - p = InvariantProof.carry_forward(self.ref(SEC), self.candidate) + p = InvariantProof.carry_forward(self.ref(SEC), self.candidate, self.impact(SEC)) self.assertEqual(p.candidate_id, self.candidate.candidate_id) self.assertEqual(p.source_state_id, self.v0.state_id) @@ -198,7 +206,7 @@ def test_a_reference_from_another_state_is_refused(self) -> None: other = baseline(state_id=uid(88)) foreign = next(r for r in other.invariant_refs if r.invariant_id == SEC) with self.assertRaises(DomainValidationError) as ctx: - InvariantProof.carry_forward(foreign, self.candidate) + InvariantProof.carry_forward(foreign, self.candidate, self.impact(SEC)) self.assertIn("C-40", str(ctx.exception)) def test_an_invalidated_protected_reference_is_refused(self) -> None: @@ -208,20 +216,126 @@ def test_an_invalidated_protected_reference_is_refused(self) -> None: invalidated = InvariantRef.from_dict(data) self.assertFalse(invalidated.can_satisfy_proof()) with self.assertRaises(DomainValidationError) as ctx: - InvariantProof.carry_forward(invalidated, self.candidate) + InvariantProof.carry_forward(invalidated, self.candidate, self.impact(SEC)) self.assertIn("C-40", str(ctx.exception)) def test_a_protected_status_is_never_manufactured_from_a_weaker_reference(self) -> None: for invariant_id in (FUNC, "INV-SEC-002"): with self.subTest(invariant=invariant_id): - p = InvariantProof.carry_forward(self.ref(invariant_id), self.candidate) + p = InvariantProof.carry_forward( + self.ref(invariant_id), self.candidate, self.impact(invariant_id) + ) self.assertNotEqual(p.status, S.PROTECTED) def test_arguments_are_type_checked(self) -> None: with self.assertRaises(DomainValidationError): - InvariantProof.carry_forward({"invariant_id": SEC}, self.candidate) # type: ignore[arg-type] + InvariantProof.carry_forward( + {"invariant_id": SEC}, # type: ignore[arg-type] + self.candidate, + self.impact(SEC), + ) with self.assertRaises(DomainValidationError): - InvariantProof.carry_forward(self.ref(SEC), self.v0) # type: ignore[arg-type] + InvariantProof.carry_forward( + self.ref(SEC), + self.v0, # type: ignore[arg-type] + self.impact(SEC), + ) + + +class TestCarryForwardNeedsTheImpactReport(unittest.TestCase): + """C-45, the canonical DAIL failure: a candidate that affects an invariant and then violates + it must not hide behind the parent's old evidence. ``carry_forward`` therefore asks the impact + report of exactly this candidate and parent (``carry_forward_ok``, C-141): anything but an + eligible, unaffected invariant is refused.""" + + def setUp(self) -> None: + self.v0 = baseline( + proofs=[ + proof(SEC, S.PROTECTED, evidence=1, minutes=3), + proof(FUNC, S.PROTECTED, evidence=2, minutes=4), + ] + ) + self.candidate = new_candidate(self.v0) + + def ref(self, invariant_id: str) -> InvariantRef: + return next(r for r in self.v0.invariant_refs if r.invariant_id == invariant_id) + + def carry(self, impact: object, invariant_id: str = SEC) -> InvariantProof: + return InvariantProof.carry_forward( + self.ref(invariant_id), + self.candidate, + impact, # type: ignore[arg-type] + ) + + def refused(self, impact: object, invariant_id: str = SEC) -> None: + with self.assertRaises(DomainValidationError) as ctx: + self.carry(impact, invariant_id) + self.assertIn("C-45", str(ctx.exception)) + + def test_an_unaffected_invariant_with_eligible_evidence_may_be_carried(self) -> None: + carried = self.carry(impact_for(self.v0, self.candidate, carry=(SEC, FUNC))) + self.assertIs(carried.origin, ProofOrigin.CARRIED_FORWARD) + self.assertEqual(carried.evidence_ids, self.ref(SEC).evidence_ids) + + def test_an_affected_invariant_is_refused(self) -> None: + self.refused(impact_for(self.v0, self.candidate, affected=(SEC,), carry=(FUNC,))) + + def test_an_uncertain_invariant_is_refused(self) -> None: + self.refused(impact_for(self.v0, self.candidate, uncertain=(SEC,), carry=(FUNC,))) + + def test_an_invariant_the_report_does_not_mention_is_refused(self) -> None: + self.refused(impact_for(self.v0, self.candidate, carry=(FUNC,)), SEC) + + def test_an_unaffected_invariant_without_eligible_evidence_is_refused(self) -> None: + self.refused(impact_for(self.v0, self.candidate, ineligible=(SEC,), carry=(FUNC,))) + + def test_a_report_for_another_candidate_is_refused(self) -> None: + other = new_candidate(self.v0, sequence=2, n=2) + self.refused(impact_for(self.v0, other, carry=(SEC,))) + + def test_a_report_for_another_parent_is_refused(self) -> None: + other_parent = baseline(state_id=uid(88)) + report = impact_for(other_parent, self.candidate, carry=(SEC,)) + self.assertNotEqual(report.parent_state_id, self.candidate.parent_state_id) + self.refused(report) + + def test_a_report_whose_hash_no_longer_recomputes_is_refused(self) -> None: + report = impact_for(self.v0, self.candidate, carry=(SEC,)) + object.__setattr__(report, "graph_version", "tampered") + self.assertNotEqual(report.content_hash, report.compute_hash()) + self.refused(report) + + def test_a_report_that_names_the_invariant_at_another_version_is_refused(self) -> None: + self.refused(impact_for(self.v0, self.candidate, carry=(SEC,), versions={SEC: 2})) + + def test_the_version_asked_is_the_version_of_the_reference(self) -> None: + # a reference to version 2: a report that only knows version 1 does not allow it, and + # one that names version 2 does + newer = InvariantProof.for_baseline( + invariant_id=SEC, + invariant_version=2, + status=S.PROTECTED, + evidence_ids=(uid(1001),), + verified_at=at(3), + ) + self.v0 = baseline(proofs=[newer, proof(FUNC, S.PROTECTED, evidence=2)]) + self.candidate = new_candidate(self.v0) + self.assertEqual(self.ref(SEC).invariant_version, 2) + self.refused(impact_for(self.v0, self.candidate, carry=(SEC,), versions={SEC: 1})) + carried = self.carry(impact_for(self.v0, self.candidate, carry=(SEC,))) + self.assertEqual(carried.invariant_version, 2) + + def test_the_report_is_required_and_must_be_one(self) -> None: + with self.assertRaises(TypeError): + InvariantProof.carry_forward(self.ref(SEC), self.candidate) # type: ignore[call-arg] + for bad in (None, {"carry_forward_candidates": [SEC]}, "ImpactReport"): + with self.subTest(bad=bad), self.assertRaises(DomainValidationError): + self.carry(bad) + + def test_a_refusal_changes_nothing(self) -> None: + before = self.v0.state_hash + self.refused(impact_for(self.v0, self.candidate, affected=(SEC,))) + self.assertEqual(self.v0.state_hash, before) if __name__ == "__main__": From d1d3418fd2ec77bcc4109fe84d7318f83217843f Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:40:32 +0530 Subject: [PATCH 5/8] =?UTF-8?q?P6a=20step=204:=20decide():=20Appendix=20A?= =?UTF-8?q?=20with=20the=20severity=20fold,=20the=20non-success=20table,?= =?UTF-8?q?=20proof=20sources,=20oracle=20conflicts,=20retry=20budget,=20e?= =?UTF-8?q?mergency=20switch,=20completeness=20(Doc=2009=20=C2=A717-=C2=A7?= =?UTF-8?q?29,=20Appendix=20A;=20C-41,=20C-45,=20C-157=20to=20C-161)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit decide(candidate, trusted, impact, verification, policy, ...) is a pure function that examines every required item (gates, invariants, baseline items), proves each by a fresh sufficient PASS or by carrying its reference forward (never for an affected, non-PROTECTED, version-changed or policy-disabled invariant), folds the blocking conditions by severity (REJECT above ESCALATE above RETRY), converts an exhausted RETRY to ESCALATE, treats an oracle FAIL against a proven check as a conflict, and downgrades an incomplete or switched-off PROMOTE to ESCALATE. A stale parent wins. 95 tests, written from the spec first: they failed with ImportError until decide existed; at the first run 88 passed and the 7 failures were mistakes in the tests (a duplicate result id, the wrong definition picked by index, a replace() the domain forbids, an expected list order, an expected proof plan, a text scan, a stale-parent that was not stale), not in the code. Co-Authored-By: Claude Sonnet 5.5 --- core/promotion/decide.py | 640 +++++++++++++++ tests/promotion_builders.py | 315 +++++++- tests/unit/test_promotion_decide.py | 1115 +++++++++++++++++++++++++++ 3 files changed, 2067 insertions(+), 3 deletions(-) create mode 100644 core/promotion/decide.py create mode 100644 tests/unit/test_promotion_decide.py diff --git a/core/promotion/decide.py b/core/promotion/decide.py new file mode 100644 index 0000000..9dbb77e --- /dev/null +++ b/core/promotion/decide.py @@ -0,0 +1,640 @@ +"""``decide``: the decision half of the Promotion Controller (P6a; Doc 09 §17-§29, Appendix A, +Doc 06 §16-§21, Doc 11 §26, §43; C-45, C-157 to C-161, C-37, C-41). + +A pure function of its arguments: no clock, no randomness, no I/O, no mutation. It consumes the +reports it is given and never runs, repeats or repairs verification (Doc 02 §15). Anything it finds +is a decision (REJECT, RETRY or ESCALATE, with every blocking reason); only a malformed argument +raises (``PromotionInputError``). Uncertainty never promotes: an UNKNOWN, UNSUPPORTED or +VERIFIER_ERROR result, a missing, stale or insufficient one, an oracle conflict and an incomplete +decision all stop short of PROMOTE. + +The order of Doc 09 Appendix A is kept (stale parent, structure, required items, sufficiency), but +the early return of its loop is not: every required item is examined and the conditions are folded +by severity (C-158), so a later FAIL cannot hide behind an earlier UNKNOWN and the decision does not +depend on the order of anything. + +Standard library and ``core.domain`` only (R18). +""" + +from __future__ import annotations + +from collections.abc import Iterable, Mapping, Sequence +from dataclasses import dataclass, field +from datetime import datetime +from typing import Final + +from core.domain.enums import ( + CandidateStatus, + DecisionType, + InvariantStatus, + VerificationResult, +) +from core.domain.errors import DomainValidationError +from core.domain.ids import require_uuid +from core.domain.impact import ImpactReport, WorkTargetType +from core.domain.invariant import Invariant, InvariantRef +from core.domain.jsonvalue import utc +from core.domain.promotion import ( + GATE_CONSISTENCY, + GATE_STRUCTURAL, + BlockingCondition, + DecisionOutcome, + DecisionReason, + OracleVerdict, + PromotionDecision, + PromotionEvidence, + PromotionInputError, + PromotionPolicy, + ProofPlanEntry, + ProofSource, + RequiredCheck, +) +from core.domain.state import CandidateState, TrustedState +from core.domain.verification import ( + EVIDENCE_LEVELS, + VerificationReport, + VerificationResultRecord, + fresh, + sufficient, +) + +D = DecisionType +R = DecisionReason + +_SEVERITY: Final = {D.REJECT: 3, D.ESCALATE: 2, D.RETRY: 1} +# Among the conditions of the winning class the reason is the first of this list (C-158). +_PRIORITY: Final = ( + R.STALE_PARENT, + R.STRUCTURAL_FAILURE, + R.INCONSISTENT_REPORTS, + R.REQUIRED_CHECK_FAILED, + R.REQUIRED_UNSUPPORTED, + R.INSUFFICIENT_EVIDENCE, + R.EVIDENCE_NOT_SUFFICIENT, + R.EVIDENCE_STALE, + R.POLICY_REGISTRY_REGRESSION, + R.VERIFIER_ERROR, + R.EVIDENCE_CONFLICT, + R.RETRY_BUDGET_EXHAUSTED, + R.REQUIRED_UNKNOWN, + R.DECISION_INCOMPLETE, + R.AUTOMATIC_PROMOTION_DISABLED, +) +_NON_SUCCESS_CODE: Final = { + VerificationResult.UNKNOWN: R.REQUIRED_UNKNOWN, + VerificationResult.UNSUPPORTED: R.REQUIRED_UNSUPPORTED, + VerificationResult.VERIFIER_ERROR: R.VERIFIER_ERROR, +} +_DECIDABLE: Final = (CandidateStatus.ANALYZING, CandidateStatus.PROMOTABLE) + + +def fold(conditions: Sequence[BlockingCondition]) -> tuple[DecisionType, DecisionReason]: + """The decision and the reason of a non-empty set of blocking conditions (C-158): the most + severe class wins (REJECT above ESCALATE above RETRY), and within it the reason is the first of + a fixed list. It does not depend on the order of ``conditions``.""" + if not conditions: + raise DomainValidationError("fold: there is no blocking condition to decide on") + top = max(_SEVERITY[c.decision] for c in conditions) + winners = [c for c in conditions if _SEVERITY[c.decision] == top] + decision = next(d for d, severity in _SEVERITY.items() if severity == top) + return decision, min((c.code for c in winners), key=_PRIORITY.index) + + +# --- arguments ------------------------------------------------------------------------------------ + + +def _check_arguments( + candidate: object, + trusted: object, + impact: object, + verification: object, + policy: object, + decision_id: object, + now: object, + attempt_number: object, + oracle_verdicts: object, +) -> tuple[datetime, tuple[OracleVerdict, ...]]: + for value, kind, name in ( + (candidate, CandidateState, "candidate"), + (trusted, TrustedState, "trusted"), + (impact, ImpactReport, "impact"), + (verification, VerificationReport, "verification"), + (policy, PromotionPolicy, "policy"), + ): + if not isinstance(value, kind): + raise PromotionInputError(f"decide: {name} must be a {kind.__name__}") + assert isinstance(candidate, CandidateState) and isinstance(trusted, TrustedState) + try: + require_uuid(decision_id, "decide.decision_id") + moment = utc(now, "decide.now") + except DomainValidationError as error: + raise PromotionInputError(str(error)) from None + if ( + not isinstance(attempt_number, int) + or isinstance(attempt_number, bool) + or attempt_number < 1 + ): + raise PromotionInputError("decide.attempt_number: must be an integer >= 1") + if candidate.lineage_id != trusted.lineage_id: + raise PromotionInputError( + "decide: the candidate and the trusted state are in different lineages" + ) + if candidate.status not in _DECIDABLE or candidate.state_hash is None: + raise PromotionInputError( + f"decide: a {candidate.status.value} candidate is not under analysis " + "(ANALYZING or PROMOTABLE)" + ) + if isinstance(oracle_verdicts, str) or not isinstance(oracle_verdicts, Iterable): + raise PromotionInputError("decide.oracle_verdicts: must be a list of OracleVerdict") + verdicts = tuple(oracle_verdicts) + if not all(isinstance(v, OracleVerdict) for v in verdicts): + raise PromotionInputError("decide.oracle_verdicts: must hold OracleVerdict objects") + keys = [(v.invariant_id, v.invariant_version) for v in verdicts] + if len(set(keys)) != len(keys): + raise PromotionInputError("decide.oracle_verdicts: two verdicts for one invariant version") + return moment, verdicts + + +# --- the pieces of the decision ------------------------------------------------------------------- + + +@dataclass(frozen=True) +class _Item: + """One required target, and what a result for it must be.""" + + target_id: str + kind: str # GATE, INVARIANT or BASELINE + invariant: Invariant | None # the definition at the policy's registry version + reference: InvariantRef | None # the current state's reference to it, if any + verifier: tuple[str, str] | None # id and version a result must carry; None: its own + + +@dataclass +class _Verdict: + check: RequiredCheck + conditions: list[BlockingCondition] = field(default_factory=list) + entry: ProofPlanEntry | None = None + result_id: str | None = None + + +def _condition( + code: DecisionReason, decision: DecisionType, target: str, detail: str +) -> BlockingCondition: + return BlockingCondition(code, decision, target, detail) + + +def _described(record: VerificationResultRecord) -> str: + reason = "" if record.reason is None else f" {record.reason.value}" + return f"result {record.verification_id}: {record.result.value}{reason}" + + +def _failure_code(item: _Item) -> DecisionReason: + if item.target_id == GATE_STRUCTURAL: + return R.STRUCTURAL_FAILURE + if item.target_id == GATE_CONSISTENCY: + return R.INCONSISTENT_REPORTS + return R.REQUIRED_CHECK_FAILED + + +def _level_ok(record: VerificationResultRecord, policy: PromotionPolicy) -> bool: + return EVIDENCE_LEVELS.index(record.evidence_level) >= EVIDENCE_LEVELS.index( + policy.min_evidence_level + ) + + +def _required_items( + trusted: TrustedState, impact: ImpactReport, policy: PromotionPolicy +) -> tuple[list[_Item], list[BlockingCondition]]: + """Every required target (C-159), and the policy conditions found on the way (C-41).""" + problems: list[BlockingCondition] = [] + if policy.invariant_registry_version < trusted.invariant_registry_version: + problems.append( + _condition( + R.POLICY_REGISTRY_REGRESSION, + D.ESCALATE, + "POLICY", + f"registry version {policy.invariant_registry_version} is lower than the " + f"current state's {trusted.invariant_registry_version}", + ) + ) + references = {ref.invariant_id: ref for ref in trusted.invariant_refs} + items = [ + _Item(target, "GATE", None, None, policy.gate_verifier(target)) + for target in (GATE_CONSISTENCY, GATE_STRUCTURAL) + ] + for invariant_id in sorted({*references, *policy.extra_required}): + reference = references.get(invariant_id) + definition = policy.definition(invariant_id) + if definition is None or ( + reference is not None and definition.version < reference.invariant_version + ): + version = 1 if reference is None else reference.invariant_version + problems.append( + _condition( + R.POLICY_REGISTRY_REGRESSION, + D.ESCALATE, + f"INVARIANT:{invariant_id}:{version}", + "the policy has no definition of it at or above the current version", + ) + ) + items.append( + _Item(f"INVARIANT:{invariant_id}:{version}", "UNDEFINED", None, reference, None) + ) + continue + items.append( + _Item( + f"INVARIANT:{invariant_id}:{definition.version}", + "INVARIANT", + definition, + reference, + (definition.verifier_id, definition.verifier_version), + ) + ) + items.extend( + _Item(work.target_id, "BASELINE", None, None, None) + for work in impact.verification_work + if work.target_type is WorkTargetType.RESOURCE + ) + return sorted(items, key=lambda item: item.target_id), problems + + +def _binding_conditions( + candidate: CandidateState, impact: ImpactReport, verification: VerificationReport +) -> list[BlockingCondition]: + """The reports must be those of this candidate and this parent (Doc 09 §19, §31).""" + found = [] + if impact.candidate_id != candidate.candidate_id: + found.append(("impact report", "is for another candidate")) + if impact.parent_state_id != candidate.parent_state_id: + found.append(("impact report", "is for another parent state")) + if verification.candidate_id != candidate.candidate_id: + found.append(("verification report", "is for another candidate")) + return [ + _condition(R.INCONSISTENT_REPORTS, D.REJECT, name.replace(" ", "-"), f"the {name} {what}") + for name, what in found + ] + + +def _carry_forward_refusals( + item: _Item, + candidate: CandidateState, + trusted: TrustedState, + impact: ImpactReport, + policy: PromotionPolicy, +) -> list[str]: + """Why ``item`` cannot be proven by carrying its reference forward (C-159); empty if it can.""" + assert item.invariant is not None + definition, reference = item.invariant, item.reference + refusals = [] + if not policy.carry_forward_enabled: + refusals.append("the policy does not permit carry-forward") + if reference is None: + refusals.append("the current state has no reference to it") + else: + if reference.invariant_version != definition.version: + refusals.append( + f"its version changed from {reference.invariant_version} to {definition.version}" + ) + if reference.status is not InvariantStatus.PROTECTED: + refusals.append(f"its reference is {reference.status.value}, not PROTECTED") + elif not reference.can_satisfy_proof(): + refusals.append("its reference was invalidated") + key = (definition.invariant_id, definition.version) + if impact.affected_for(*key) is not None: + refusals.append("the candidate affects it") + if any((r.invariant_id, r.invariant_version) == key for r in impact.uncertainty): + refusals.append("its impact is uncertain") + if not impact.carry_forward_ok( + *key, candidate_id=candidate.candidate_id, parent_state_id=candidate.parent_state_id + ): + refusals.append("the impact report does not offer its evidence") + if reference is not None and reference.state_id != trusted.state_id: + refusals.append("its reference is not the current state's") + return refusals + + +def _assess( + item: _Item, + records: Mapping[str, VerificationResultRecord], + candidate: CandidateState, + trusted: TrustedState, + impact: ImpactReport, + policy: PromotionPolicy, +) -> _Verdict: + """Is ``item`` proven, and if not, why not (C-158, C-159)?""" + candidate_hash = candidate.state_hash + assert candidate_hash is not None + verdict = _Verdict(RequiredCheck(item.target_id, _kind(item), None, None)) + if item.kind == "UNDEFINED": + return verdict # the policy condition already says what is wrong + record = records.get(item.target_id) + invariant = item.invariant + verifier_id, verifier_version = item.verifier or ( + (record.verifier_id, record.verifier_version) if record is not None else ("", "") + ) + is_fresh = record is not None and fresh( + record, + candidate_hash=candidate_hash, + invariant_version=None if invariant is None else invariant.version, + verifier_version=verifier_version, + ) + if record is not None and is_fresh: + _assess_result(verdict, item, record, verifier_id, verifier_version, candidate_hash, policy) + return verdict + if invariant is not None: + refusals = _carry_forward_refusals(item, candidate, trusted, impact, policy) + if not refusals: + assert item.reference is not None + verdict.check = RequiredCheck( + item.target_id, "INVARIANT", ProofSource.CARRIED_FORWARD, None + ) + verdict.entry = ProofPlanEntry( + invariant.invariant_id, + invariant.version, + ProofSource.CARRIED_FORWARD, + None, + trusted.state_id, + item.reference.evidence_ids, + ) + return verdict + why = f"no fresh result; carry-forward refused: {'; '.join(refusals)}" + else: + why = "no fresh result" + if record is None: + verdict.conditions.append( + _condition(R.INSUFFICIENT_EVIDENCE, D.REJECT, item.target_id, f"no result; {why}") + ) + else: + verdict.conditions.append( + _condition( + R.EVIDENCE_STALE, + D.REJECT, + item.target_id, + f"{_described(record)} is stale for this candidate and these versions; {why}", + ) + ) + return verdict + + +def _kind(item: _Item) -> str: + return "INVARIANT" if item.kind == "UNDEFINED" else item.kind + + +def _assess_result( + verdict: _Verdict, + item: _Item, + record: VerificationResultRecord, + verifier_id: str, + verifier_version: str, + candidate_hash: str, + policy: PromotionPolicy, +) -> None: + """A fresh result decides: FAIL rejects, a non-success follows the table, a sufficient PASS + proves (Doc 09 §11, §18).""" + target, described = item.target_id, _described(record) + if record.result is VerificationResult.FAIL: + verdict.conditions.append(_condition(_failure_code(item), D.REJECT, target, described)) + return + if record.result is VerificationResult.PASS: + invariant = item.invariant + if sufficient( + record, + target_id=target, + candidate_hash=candidate_hash, + invariant_id=None if invariant is None else invariant.invariant_id, + invariant_version=None if invariant is None else invariant.version, + verifier_id=verifier_id, + verifier_version=verifier_version, + ) and _level_ok(record, policy): + verdict.check = RequiredCheck( + target, _kind(item), ProofSource.VERIFIED, record.verification_id + ) + verdict.result_id = record.verification_id + if invariant is not None: + verdict.entry = ProofPlanEntry( + invariant.invariant_id, + invariant.version, + ProofSource.VERIFIED, + record.verification_id, + None, + (), + ) + return + verdict.conditions.append( + _condition( + R.EVIDENCE_NOT_SUFFICIENT, + D.REJECT, + target, + f"{described} is not sufficient proof: it must be from {verifier_id} " + f"{verifier_version} at level {policy.min_evidence_level} or above", + ) + ) + return + error_type = None if record.error is None else record.error["type"] + verdict.conditions.append( + _condition( + _NON_SUCCESS_CODE[record.result], + policy.non_success_decision(record.result, error_type), + target, + described, + ) + ) + + +def _oracle_conflicts( + verdicts: Iterable[OracleVerdict], + results: dict[str, _Verdict], + policy: PromotionPolicy, +) -> list[BlockingCondition]: + """Primary PASS (or a carried proof) and oracle FAIL: a conflict, and the check is not proven + (C-160). Every other pairing leaves the primary result as it is.""" + found = [] + for oracle in sorted(verdicts, key=lambda v: (v.invariant_id, v.invariant_version)): + if oracle.result is not VerificationResult.FAIL: + continue + target = f"INVARIANT:{oracle.invariant_id}:{oracle.invariant_version}" + verdict = results.get(target) + if verdict is None or verdict.check.source is None: + continue + found.append( + _condition( + R.EVIDENCE_CONFLICT, + policy.conflict_decision, + target, + f"the primary verifier proves it but oracle {oracle.oracle_version} reports FAIL", + ) + ) + verdict.check = RequiredCheck(target, "INVARIANT", None, None) + verdict.entry = None + verdict.result_id = None + return found + + +def completeness_problems( + candidate: CandidateState, + parent_state_id: str, + supporting: Iterable[str], + impact: ImpactReport, + verification: VerificationReport, + policy: PromotionPolicy, +) -> list[str]: + """What is missing for the decision to be complete (Doc 11 §43, C-161): candidate and parent + binding, every supporting result present, the report hashes, the policy version.""" + problems = [] + if parent_state_id != candidate.parent_state_id: + problems.append("the decision's parent is not the candidate's parent state") + if verification.candidate_id != candidate.candidate_id: + problems.append("the verification report is for another candidate") + if impact.candidate_id != candidate.candidate_id: + problems.append("the impact report is for another candidate") + held = {r.verification_id for r in verification.results} + for missing in sorted(set(supporting) - held): + problems.append(f"supporting result {missing} is not in the verification report") + if verification.candidate_hash != candidate.state_hash: + problems.append( + "the verification report's candidate_hash is not the candidate's state_hash" + ) + if verification.content_hash != verification.compute_hash(): + problems.append("the verification report's content hash does not recompute") + if impact.content_hash != impact.compute_hash(): + problems.append("the impact report's content hash does not recompute") + if not policy.policy_version: + problems.append("the policy version is not recorded") + return problems + + +# --- decide --------------------------------------------------------------------------------------- + + +def decide( + candidate: CandidateState, + trusted: TrustedState, + impact: ImpactReport, + verification: VerificationReport, + policy: PromotionPolicy, + *, + decision_id: str, + now: datetime, + attempt_number: int = 1, + oracle_verdicts: Iterable[OracleVerdict] = (), +) -> DecisionOutcome: + """PROMOTE, REJECT, RETRY or ESCALATE for ``candidate`` against the current state ``trusted``. + + ``attempt_number`` counts the attempts at this candidate's problem (1 for the first); it feeds + only the retry budget of the policy. PROMOTE needs every required item proven, nothing + conflicting, a complete decision and the emergency switch on (Doc 09 §19).""" + moment, verdicts = _check_arguments( + candidate, + trusted, + impact, + verification, + policy, + decision_id, + now, + attempt_number, + oracle_verdicts, + ) + if candidate.parent_state_id != trusted.state_id: + stale = _condition( + R.STALE_PARENT, + D.REJECT, + "STATE", + f"the candidate's parent {candidate.parent_state_id} is not the current state " + f"{trusted.state_id}", + ) + return _build(candidate, policy, decision_id, moment, attempt_number, [], [stale], (), ()) + items, conditions = _required_items(trusted, impact, policy) + conditions += _binding_conditions(candidate, impact, verification) + records = {r.target_id: r for r in verification.results} + assessed = { + item.target_id: _assess(item, records, candidate, trusted, impact, policy) for item in items + } + for verdict in assessed.values(): + conditions += verdict.conditions + conditions += _oracle_conflicts(verdicts, assessed, policy) + ordered = [assessed[item.target_id] for item in items] + checks = [v.check for v in ordered] + plan = sorted((v.entry for v in ordered if v.entry is not None), key=lambda e: e.invariant_id) + supporting = sorted({v.result_id for v in ordered if v.result_id is not None}) + problems = completeness_problems( + candidate, candidate.parent_state_id, supporting, impact, verification, policy + ) + if not conditions: + if problems: + conditions.append( + _condition(R.DECISION_INCOMPLETE, D.ESCALATE, "DECISION", "; ".join(problems)) + ) + if not policy.automatic_enabled: + conditions.append( + _condition( + R.AUTOMATIC_PROMOTION_DISABLED, + D.ESCALATE, + "POLICY", + "automatic promotion is disabled; the decision would have been PROMOTE", + ) + ) + else: + decision, _ = fold(conditions) + if decision is D.RETRY and attempt_number >= policy.max_attempts: + conditions.append( + _condition( + R.RETRY_BUDGET_EXHAUSTED, + D.ESCALATE, + "POLICY", + f"attempt {attempt_number} of {policy.max_attempts}: repeated UNKNOWN is " + "not an eventual PASS", + ) + ) + decision, _ = fold(conditions) + if problems: # recorded; the decision it keeps is the one found above + conditions.append( + _condition(R.DECISION_INCOMPLETE, decision, "DECISION", "; ".join(problems)) + ) + return _build( + candidate, policy, decision_id, moment, attempt_number, checks, conditions, plan, supporting + ) + + +def _build( + candidate: CandidateState, + policy: PromotionPolicy, + decision_id: str, + moment: datetime, + attempt_number: int, + checks: Sequence[RequiredCheck], + conditions: Sequence[BlockingCondition], + plan: Sequence[ProofPlanEntry], + supporting: Sequence[str], +) -> DecisionOutcome: + unique = sorted({c.sort_key(): c for c in conditions}.values(), key=BlockingCondition.sort_key) + if unique: + decision, reason = fold(unique) + else: + decision, reason = D.PROMOTE, R.ALL_REQUIRED_PROVEN + ordered_checks = sorted(checks, key=lambda c: c.target_id) + made = PromotionDecision.create( + decision_id=decision_id, + candidate_id=candidate.candidate_id, + parent_state_id=candidate.parent_state_id, + decision=decision, + reason=reason, + policy_version=policy.policy_version, + attempt_number=attempt_number, + required_checks=ordered_checks, + blocking_conditions=unique, + supporting_results=sorted(supporting), + created_at=moment, + ) + proven = bool(ordered_checks) and all(c.source is not None for c in ordered_checks) + evidence = PromotionEvidence.create( + decision_id=decision_id, + candidate_id=candidate.candidate_id, + parent_state_id=candidate.parent_state_id, + required_checks=ordered_checks, + verification_refs=sorted(supporting), + evidence_sufficiency="SUFFICIENT" if proven else "INSUFFICIENT", + policy_version=policy.policy_version, + decision=decision, + reason=reason, + ) + return DecisionOutcome(made, tuple(plan), evidence) diff --git a/tests/promotion_builders.py b/tests/promotion_builders.py index 9aa775d..9b5b882 100644 --- a/tests/promotion_builders.py +++ b/tests/promotion_builders.py @@ -2,15 +2,69 @@ Tests may import every package; ``core.promotion`` may import only ``core.domain`` (R18). Everything is deterministic: ids come from ``tests.domain_builders.uid`` and times from ``at``. + +``make_world`` builds the canonical scenario at the domain level: a trusted state ``v0`` in which +INV-SEC-001 is VIOLATED (public SSH is open) and the other three registry-v1.0 invariants are +PROTECTED; a candidate that fixes SSH; an impact report in which INV-SEC-001 and INV-FUNC-001 are +affected and INV-SEC-002 and INV-SEC-003 are eligible to carry forward; and a verification report +with a fresh L1 PASS for every required item. Each test then changes one thing. """ from __future__ import annotations -from collections.abc import Iterable +import dataclasses +from collections.abc import Iterable, Mapping +from dataclasses import dataclass, field +from typing import Any +from core.domain.enums import ( + CandidateStatus, + ChangeType, + InvariantCategory, + InvariantStatus, + VerificationResult, +) from core.domain.impact import ImpactReport -from core.domain.invariant import InvariantRef +from core.domain.invariant import Invariant, InvariantProof, InvariantRef +from core.domain.promotion import DecisionOutcome, OracleVerdict, PromotionPolicy +from core.domain.registry_v1 import registry_v1_invariants from core.domain.state import CandidateState, TrustedState +from core.domain.verification import ( + VerificationClass, + VerificationReason, + VerificationReport, + VerificationResultRecord, + VerificationTargetType, +) +from core.promotion.decide import decide +from core.promotion.policy import dail_policy +from tests.domain_builders import ( + LINEAGE, + NORMALIZATION, + analyzing_candidate, + at, + canonical_resources, + transition_candidate, + uid, +) + +SEC1, SEC2, SEC3, FUNC1 = "INV-SEC-001", "INV-SEC-002", "INV-SEC-003", "INV-FUNC-001" +ALL = (SEC1, SEC2, SEC3, FUNC1) +GATES = ("STRUCTURAL", "CONSISTENCY") +BASELINE_ITEM = "RESOURCE:aws_internet_gateway.new" +PASS, FAIL = VerificationResult.PASS, VerificationResult.FAIL +UNKNOWN = VerificationResult.UNKNOWN +UNSUPPORTED = VerificationResult.UNSUPPORTED +ERROR = VerificationResult.VERIFIER_ERROR +DECISION_ID = uid(9100) +NOW = at(20) + +_REASONS = { + FAIL: VerificationReason.PREDICATE_VIOLATED, + UNKNOWN: VerificationReason.RULE_INDETERMINATE, + UNSUPPORTED: VerificationReason.TYPE_RELEVANT_UNSUPPORTED, + ERROR: VerificationReason.VERIFIER_ERROR, +} def _ref(parent: TrustedState, invariant_id: str) -> InvariantRef: @@ -26,13 +80,15 @@ def impact_for( uncertain: Iterable[str] = (), ineligible: Iterable[str] = (), versions: dict[str, int] | None = None, + with_baseline_work: bool = True, ) -> ImpactReport: """An impact report of ``candidate`` against ``parent``. ``carry`` are unaffected invariants whose prior evidence is eligible (the parent reference's own evidence); ``ineligible`` are unaffected but not eligible; ``affected`` and ``uncertain`` are the impacted ones, which owe a work item. ``versions`` overrides the invariant version the - report names (default: the version of the parent's reference).""" + report names (default: the version of the parent's reference). With ``with_baseline_work`` the + report also owes the baseline item of the created resource ``BASELINE_ITEM``.""" from tests import impact_builders as ib def version(invariant_id: str) -> int: @@ -47,9 +103,262 @@ def version(invariant_id: str) -> int: ib.unaffected(i, version(i), eligible=True, evidence=_ref(parent, i).evidence_ids) for i in carry ] + [ib.unaffected(i, version(i)) for i in ineligible] + work = [ib.work_for(item) for item in impacted] + if with_baseline_work: + work.append(ib.baseline_work("aws_internet_gateway.new")) + changed = [ib.changed("aws_security_group.app")] + if with_baseline_work: + changed.append(ib.changed("aws_internet_gateway.new", ChangeType.CREATED)) return ib.report( + changed_resources=changed, affected=impacted, + work=work, unaffected_invariants=kept, parent_state_id=parent.state_id, candidate_id=candidate.candidate_id, ) + + +# --- verification results ------------------------------------------------------------------------- + + +def record( + candidate: CandidateState, + target_id: str, + result: VerificationResult = PASS, + *, + definition: Invariant | None = None, + level: str = "L1", + verifier: tuple[str, str] | None = None, + candidate_hash: str | None = None, + error_type: str = "RuntimeError", + reason: VerificationReason | None = None, + n: int = 0, +) -> VerificationResultRecord: + """One result for ``target_id`` (an invariant, a gate item or a resource), by default a fresh + L1 result of the verifier the definition names.""" + assert candidate.state_hash is not None + if target_id.startswith("INVARIANT:"): + assert definition is not None + target_type = VerificationTargetType.INVARIANT + klass = ( + VerificationClass.SECURITY + if definition.category is InvariantCategory.SECURITY + else VerificationClass.FUNCTIONAL + ) + invariant_id: str | None = definition.invariant_id + version: int | None = definition.version + chosen = verifier or (definition.verifier_id, definition.verifier_version) + elif target_id in GATES: + target_type = VerificationTargetType.STRUCTURAL + klass = getattr(VerificationClass, target_id) + invariant_id, version = None, None + chosen = verifier or (f"dail.verify.{target_id.lower()}", "1") + else: + target_type = VerificationTargetType.RESOURCE + klass = VerificationClass.BASELINE + invariant_id, version = None, None + chosen = verifier or ("dail.verify.baseline", "1") + chosen_reason = None if result is PASS else (reason or _REASONS[result]) + error = ( + {"type": error_type, "message": "boom", "class": "Exception"} if result is ERROR else None + ) + return VerificationResultRecord( + verification_id=uid(7000 + n), + request_id=uid(8000 + n), + target_type=target_type, + target_id=target_id, + candidate_id=candidate.candidate_id, + candidate_hash=candidate_hash or candidate.state_hash, + invariant_id=invariant_id, + invariant_version=version, + verifier_id=chosen[0], + verifier_version=chosen[1], + evidence_level=level, + verification_class=klass, + result=result, + reason=chosen_reason, + applicable=True, + clauses=None, + observations={}, + assumptions=(), + evidence={"predicate": "p", "inputs": {}, "observations": {}, "result": result.value}, + error=error, + started_at=at(10), + completed_at=at(11), + ) + + +def report_of( + candidate: CandidateState, records: Iterable[VerificationResultRecord] +) -> VerificationReport: + items = list(records) + return VerificationReport.create( + candidate_id=candidate.candidate_id, + candidate_hash=candidate.state_hash or "0" * 64, + results=items, + verifier_invocations=len(items), + verifier_set_version="dail-verify-1", + report_id=uid(6000), + ) + + +# --- the world ------------------------------------------------------------------------------------ + + +def invariant_definitions() -> dict[str, Invariant]: + return { + d.invariant_id: d + for d in registry_v1_invariants( + at(0), source="aws_instance.app", destination="aws_db_instance.database" + ) + } + + +def trusted_state( + statuses: Mapping[str, InvariantStatus] | None = None, + *, + registry_version: int = 1, + state_id: str | None = None, + versions: Mapping[str, int] | None = None, + ids: Iterable[str] = ALL, +) -> TrustedState: + """A baseline (version 0): INV-SEC-001 VIOLATED, the rest PROTECTED unless ``statuses`` says + otherwise.""" + wanted = {SEC1: InvariantStatus.VIOLATED} + wanted.update(statuses or {}) + proofs = [ + InvariantProof.for_baseline( + invariant_id=i, + invariant_version=(versions or {}).get(i, 1), + status=wanted.get(i, InvariantStatus.PROTECTED), + evidence_ids=(uid(1100 + n),), + verified_at=at(1), + ) + for n, i in enumerate(sorted(ids)) + ] + return TrustedState.establish_baseline( + lineage_id=LINEAGE, + resources=canonical_resources(ssh_open=True, db_path=True), + invariant_proofs=proofs, + evidence_refs=sorted({e for p in proofs for e in p.evidence_ids}), + normalization_version=NORMALIZATION, + invariant_registry_version=registry_version, + now=at(1), + state_id=state_id or uid(1), + ) + + +@dataclass(frozen=True) +class World: + trusted: TrustedState + candidate: CandidateState + impact: ImpactReport + verification: VerificationReport + policy: PromotionPolicy + records: Mapping[str, VerificationResultRecord] = field(default_factory=dict) + definitions: Mapping[str, Invariant] = field(default_factory=dict) + + def with_report(self, records: Iterable[VerificationResultRecord]) -> World: + items = list(records) + return dataclasses.replace( + self, + records={r.target_id: r for r in items}, + verification=report_of(self.candidate, items), + ) + + def with_policy(self, **changes: Any) -> World: + return dataclasses.replace(self, policy=dataclasses.replace(self.policy, **changes)) + + +def target(invariant_id: str, version: int = 1) -> str: + return f"INVARIANT:{invariant_id}:{version}" + + +def make_world( + *, + results: Mapping[str, VerificationResult | None | VerificationResultRecord] | None = None, + affected: Iterable[str] = (SEC1, FUNC1), + uncertain: Iterable[str] = (), + carry: Iterable[str] | None = None, + statuses: Mapping[str, InvariantStatus] | None = None, + registry_version: int = 1, + candidate_status: CandidateStatus = CandidateStatus.ANALYZING, + with_baseline_work: bool = True, + policy: PromotionPolicy | None = None, + automatic_enabled: bool = True, +) -> World: + """The canonical world, with ``results`` overriding single targets: a result value replaces the + PASS, ``None`` removes the item, a record is used as it is.""" + definitions = invariant_definitions() + trusted = trusted_state(statuses, registry_version=registry_version) + candidate = analyzing_candidate(trusted, canonical_resources(ssh_open=False, db_path=True)) + if candidate_status is CandidateStatus.PROMOTABLE: + candidate = transition_candidate(candidate, CandidateStatus.PROMOTABLE) + impacted = tuple(affected) + unsure = tuple(uncertain) + kept = ( + tuple(i for i in ALL if i not in impacted and i not in unsure) + if carry is None + else tuple(carry) + ) + impact = impact_for( + trusted, + candidate, + carry=kept, + affected=impacted, + uncertain=unsure, + with_baseline_work=with_baseline_work, + ) + wanted: dict[str, Any] = {g: PASS for g in GATES} + for i in (*impacted, *unsure): + wanted[target(i)] = PASS + if with_baseline_work: + wanted[BASELINE_ITEM] = PASS + wanted.update(results or {}) + items = [] + for n, (tid, value) in enumerate(sorted(wanted.items())): + if value is None: + continue + if isinstance(value, VerificationResultRecord): + items.append(value) + continue + definition = None + if tid.startswith("INVARIANT:"): + definition = definitions[tid.split(":")[1]] + items.append(record(candidate, tid, value, definition=definition, n=n)) + chosen = policy or dail_policy( + policy_version="policy-1", + invariants=definitions.values(), + automatic_enabled=automatic_enabled, + invariant_registry_version=registry_version, + ) + return World( + trusted=trusted, + candidate=candidate, + impact=impact, + verification=report_of(candidate, items), + policy=chosen, + records={r.target_id: r for r in items}, + definitions=definitions, + ) + + +def run( + world: World, + *, + attempt_number: int = 1, + oracle: Iterable[OracleVerdict] = (), + decision_id: str = DECISION_ID, +) -> DecisionOutcome: + return decide( + world.candidate, + world.trusted, + world.impact, + world.verification, + world.policy, + decision_id=decision_id, + now=NOW, + attempt_number=attempt_number, + oracle_verdicts=tuple(oracle), + ) diff --git a/tests/unit/test_promotion_decide.py b/tests/unit/test_promotion_decide.py new file mode 100644 index 0000000..4241c01 --- /dev/null +++ b/tests/unit/test_promotion_decide.py @@ -0,0 +1,1115 @@ +"""``decide()``: Doc 09 Appendix A, the decision matrix of §20 and §41, and C-157 to C-161 (P6a +step 4). + +HAND DERIVATION, written before ``decide`` existed. The canonical world (see +``tests/promotion_builders.py``): the trusted state ``v0`` has INV-SEC-001 VIOLATED (public SSH is +open) and INV-SEC-002, INV-SEC-003 and INV-FUNC-001 PROTECTED. The candidate fixes SSH. The impact +report has INV-SEC-001 and INV-FUNC-001 affected and INV-SEC-002 and INV-SEC-003 unaffected with +eligible evidence; it also owes the baseline item of one created resource. Required (C-159): the +gate items STRUCTURAL and CONSISTENCY, the four invariants and the baseline item. A fresh L1 PASS +exists for every item that owes verification: the two gates, the two affected invariants and the +baseline item (five results). So: + + INV-SEC-001 VERIFIED (affected; its reference is VIOLATED, so it could not be carried anyway) + INV-FUNC-001 VERIFIED (affected) + INV-SEC-002 CARRIED_FORWARD (unaffected, PROTECTED, eligible, same version, policy allows it) + INV-SEC-003 CARRIED_FORWARD (the same) + decision PROMOTE, reason ALL_REQUIRED_PROVEN, supporting results = the five verification ids. + +Each test below changes one thing and states what Appendix A, §20 or C-158 to C-161 then give. The +doc 09 §20 matrix: all PASS and parent current gives PROMOTE; any required FAIL gives REJECT; a +required UNKNOWN that a retry could resolve gives RETRY; UNSUPPORTED when mandatory gives REJECT +(§29); a verifier error that cannot be retried automatically gives ESCALATE; a stale parent gives +REJECT and never PROMOTE; a construction failure gives REJECT; an unresolved evidence conflict gives +ESCALATE or REJECT per policy, never PROMOTE. +""" + +from __future__ import annotations + +import ast +import dataclasses +import itertools +import random +import unittest +from pathlib import Path + +from core.domain.enums import ( + CandidateStatus, + DecisionType, + InvariantStatus, + VerificationResult, +) +from core.domain.errors import DomainValidationError +from core.domain.invariant import Invariant +from core.domain.promotion import ( + BlockingCondition, + DecisionOutcome, + DecisionReason, + OracleVerdict, + PromotionInputError, + ProofSource, +) +from core.domain.state import TrustedState +from core.domain.verification import VerificationReason, VerificationReport +from core.promotion.decide import completeness_problems, fold +from core.promotion.policy import dail_policy, stateful_full_policy +from tests.domain_builders import analyzing_candidate, baseline, canonical_resources, uid +from tests.promotion_builders import ( + ALL, + BASELINE_ITEM, + ERROR, + FAIL, + FUNC1, + PASS, + SEC1, + SEC2, + SEC3, + UNKNOWN, + UNSUPPORTED, + World, + impact_for, + make_world, + record, + report_of, + run, + target, + trusted_state, +) + +D, R = DecisionType, DecisionReason +ROOT = Path(__file__).resolve().parents[2] + + +def codes(outcome: DecisionOutcome) -> list[DecisionReason]: + return [c.code for c in outcome.decision.blocking_conditions] + + +def sources(outcome: DecisionOutcome) -> dict[str, ProofSource]: + return {e.invariant_id: e.source for e in outcome.proof_plan} + + +def decided(outcome: DecisionOutcome) -> tuple[DecisionType, DecisionReason]: + return outcome.decision.decision, outcome.decision.reason + + +def definitions_with(world: World, **bumped: int) -> list[Invariant]: + """The registry of the world with some invariants at a higher version.""" + out = [] + for invariant_id, definition in world.definitions.items(): + if invariant_id in bumped: + for _ in range(bumped[invariant_id] - definition.version): + definition = Invariant.new_version(definition, now=world.trusted.created_at) + out.append(definition) + return out + + +class TestAllRequiredProven(unittest.TestCase): + def setUp(self) -> None: + self.world = make_world() + self.outcome = run(self.world) + + def test_the_canonical_safe_repair_is_promoted(self) -> None: + self.assertEqual(decided(self.outcome), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(self.outcome.decision.blocking_conditions, ()) + self.assertEqual(self.outcome.decision.attempt_number, 1) + + def test_the_decision_is_bound_to_the_candidate_the_parent_and_the_policy(self) -> None: + decision = self.outcome.decision + self.assertEqual(decision.candidate_id, self.world.candidate.candidate_id) + self.assertEqual(decision.parent_state_id, self.world.candidate.parent_state_id) + self.assertEqual(decision.parent_state_id, self.world.trusted.state_id) + self.assertEqual(decision.policy_version, "policy-1") + self.assertIsNone(decision.committed_state_id) + + def test_the_proof_plan_says_which_source_proves_each_invariant(self) -> None: + self.assertEqual( + sources(self.outcome), + { + SEC1: ProofSource.VERIFIED, + FUNC1: ProofSource.VERIFIED, + SEC2: ProofSource.CARRIED_FORWARD, + SEC3: ProofSource.CARRIED_FORWARD, + }, + ) + by_id = {e.invariant_id: e for e in self.outcome.proof_plan} + self.assertEqual( + by_id[SEC1].verification_id, self.world.records[target(SEC1)].verification_id + ) + carried = by_id[SEC2] + reference = next(r for r in self.world.trusted.invariant_refs if r.invariant_id == SEC2) + self.assertIsNone(carried.verification_id) + self.assertEqual(carried.source_state_id, self.world.trusted.state_id) + self.assertEqual(carried.evidence_ids, reference.evidence_ids) + self.assertEqual( + [e.invariant_id for e in self.outcome.proof_plan], sorted(sources(self.outcome)) + ) + + def test_a_promote_lists_every_verification_result_it_used(self) -> None: + used = sorted( + self.world.records[t].verification_id + for t in ( + "STRUCTURAL", + "CONSISTENCY", + target(SEC1), + target(FUNC1), + BASELINE_ITEM, + ) + ) + self.assertEqual(list(self.outcome.decision.supporting_results), used) + self.assertEqual(list(self.outcome.evidence.verification_refs), used) + # a carried-forward invariant has no result of this candidate to reference + for carried in (SEC2, SEC3): + self.assertNotIn(target(carried), self.world.records) + + def test_the_required_checks_name_every_gate_invariant_and_baseline_item(self) -> None: + wanted = { + "CONSISTENCY": ("GATE", ProofSource.VERIFIED), + "STRUCTURAL": ("GATE", ProofSource.VERIFIED), + target(FUNC1): ("INVARIANT", ProofSource.VERIFIED), + target(SEC1): ("INVARIANT", ProofSource.VERIFIED), + target(SEC2): ("INVARIANT", ProofSource.CARRIED_FORWARD), + target(SEC3): ("INVARIANT", ProofSource.CARRIED_FORWARD), + BASELINE_ITEM: ("BASELINE", ProofSource.VERIFIED), + } + got = {c.target_id: (c.kind, c.source) for c in self.outcome.decision.required_checks} + self.assertEqual(got, wanted) + self.assertEqual( + [c.target_id for c in self.outcome.decision.required_checks], sorted(wanted) + ) + + def test_the_evidence_record_follows_doc_11_section_26(self) -> None: + evidence = self.outcome.evidence + self.assertEqual(evidence.decision_id, self.outcome.decision.decision_id) + self.assertEqual(evidence.evidence_sufficiency, "SUFFICIENT") + self.assertEqual((evidence.decision, evidence.reason), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(evidence.required_checks, self.outcome.decision.required_checks) + self.assertEqual(evidence.policy_version, "policy-1") + self.assertIsNone(evidence.new_state_id) + + def test_a_promotable_candidate_may_be_decided_again(self) -> None: + # P6b decides again at commit time, when the candidate is already PROMOTABLE + world = make_world(candidate_status=CandidateStatus.PROMOTABLE) + self.assertEqual(decided(run(world)), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + + +class TestStatefulFull(unittest.TestCase): + """C-22: the same controller with carry-forward disabled.""" + + def stateful(self, world: World) -> World: + policy = stateful_full_policy( + policy_version="policy-1", + invariants=world.definitions.values(), + automatic_enabled=True, + ) + return dataclasses.replace(world, policy=policy) + + def test_nothing_is_carried_forward_and_unverified_invariants_have_no_proof(self) -> None: + out = run(self.stateful(make_world())) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual( + sorted(c.target for c in out.decision.blocking_conditions), + [target(SEC2), target(SEC3)], + ) + self.assertNotIn(ProofSource.CARRIED_FORWARD, sources(out).values()) + + def test_when_everything_is_verified_again_it_promotes_with_no_carried_proof(self) -> None: + world = make_world(affected=ALL, carry=()) + out = run(self.stateful(world)) + self.assertEqual(decided(out), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(set(sources(out).values()), {ProofSource.VERIFIED}) + self.assertEqual(len(out.proof_plan), 4) + + +class TestAppendixAAndTheDecisionMatrix(unittest.TestCase): + """Doc 09 §20 and §41, one row each.""" + + def test_security_pass_and_functional_fail_is_rejected(self) -> None: + out = run(make_world(results={target(FUNC1): FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(FUNC1)]) + self.assertNotIn(FUNC1, sources(out)) + self.assertEqual(out.evidence.evidence_sufficiency, "INSUFFICIENT") + + def test_security_fail_and_functional_pass_is_rejected(self) -> None: + out = run(make_world(results={target(SEC1): FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(SEC1)]) + + def test_both_failing_preserves_both_reasons(self) -> None: + out = run(make_world(results={target(SEC1): FAIL, target(FUNC1): FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertEqual( + sorted(c.target for c in out.decision.blocking_conditions), + [target(FUNC1), target(SEC1)], + ) + + def test_a_required_unknown_is_a_retry_and_never_a_promotion(self) -> None: + out = run(make_world(results={target(FUNC1): UNKNOWN})) + self.assertEqual(decided(out), (D.RETRY, R.REQUIRED_UNKNOWN)) + self.assertNotIn(FUNC1, sources(out)) + + def test_a_mandatory_unsupported_is_rejected(self) -> None: + out = run(make_world(results={target(FUNC1): UNSUPPORTED})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_UNSUPPORTED)) + + def test_a_verifier_error_that_cannot_be_retried_is_escalated(self) -> None: + out = run(make_world(results={target(FUNC1): ERROR})) + self.assertEqual(decided(out), (D.ESCALATE, R.VERIFIER_ERROR)) + + def test_a_transient_verifier_error_is_retried(self) -> None: + world = make_world(results={}) + error = record( + world.candidate, + target(FUNC1), + ERROR, + definition=world.definitions[FUNC1], + error_type="TimeoutError", + n=40, + ) + base = make_world(results={target(FUNC1): error}) + out = run(base.with_policy(transient_errors=("TimeoutError",))) + self.assertEqual(decided(out), (D.RETRY, R.VERIFIER_ERROR)) + other = run(base.with_policy(transient_errors=("ValueError",))) + self.assertEqual(decided(other), (D.ESCALATE, R.VERIFIER_ERROR)) + + def test_a_missing_result_is_insufficient_evidence(self) -> None: + out = run(make_world(results={target(FUNC1): None})) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(FUNC1)]) + + def test_a_missing_gate_item_is_insufficient_evidence(self) -> None: + for gate in ("STRUCTURAL", "CONSISTENCY"): + with self.subTest(gate=gate): + out = run(make_world(results={gate: None})) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [gate]) + + def test_a_missing_baseline_item_is_insufficient_evidence(self) -> None: + out = run(make_world(results={BASELINE_ITEM: None})) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + + def test_a_failed_baseline_item_is_a_failed_required_check(self) -> None: + out = run(make_world(results={BASELINE_ITEM: FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + + def test_a_construction_failure_is_rejected(self) -> None: + world = make_world() + bad = record( + world.candidate, + "STRUCTURAL", + FAIL, + reason=VerificationReason.CONSTRUCTION_INVALID, + n=41, + ) + out = run(make_world(results={"STRUCTURAL": bad})) + self.assertEqual(decided(out), (D.REJECT, R.STRUCTURAL_FAILURE)) + + def test_a_structural_finding_is_rejected(self) -> None: + out = run(make_world(results={"STRUCTURAL": FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.STRUCTURAL_FAILURE)) + + def test_inconsistent_reports_are_rejected(self) -> None: + out = run(make_world(results={"CONSISTENCY": FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.INCONSISTENT_REPORTS)) + + def test_a_non_success_gate_follows_the_table(self) -> None: + self.assertEqual( + decided(run(make_world(results={"STRUCTURAL": UNKNOWN}))), + (D.RETRY, R.REQUIRED_UNKNOWN), + ) + self.assertEqual( + decided(run(make_world(results={"CONSISTENCY": ERROR}))), (D.ESCALATE, R.VERIFIER_ERROR) + ) + + +class TestStaleParent(unittest.TestCase): + def stale(self, world: World) -> World: + return dataclasses.replace(world, trusted=trusted_state(state_id=uid(2))) + + def test_a_candidate_of_an_old_parent_is_rejected(self) -> None: + out = run(self.stale(make_world())) + self.assertEqual(decided(out), (D.REJECT, R.STALE_PARENT)) + self.assertEqual(codes(out), [R.STALE_PARENT]) + self.assertEqual(out.decision.parent_state_id, out.decision.parent_state_id) + self.assertEqual(out.proof_plan, ()) + + def test_staleness_wins_over_a_fail_an_unknown_and_an_error(self) -> None: + for results in ( + {target(SEC1): FAIL}, + {target(FUNC1): UNKNOWN}, + {target(FUNC1): ERROR}, + {"STRUCTURAL": FAIL}, + ): + with self.subTest(results=results): + out = run(self.stale(make_world(results=results))) + self.assertEqual(decided(out), (D.REJECT, R.STALE_PARENT)) + self.assertEqual(codes(out), [R.STALE_PARENT]) + + def test_the_decision_names_the_parent_of_the_candidate(self) -> None: + world = self.stale(make_world()) + out = run(world) + self.assertEqual(out.decision.parent_state_id, world.candidate.parent_state_id) + self.assertNotEqual(out.decision.parent_state_id, world.trusted.state_id) + + +class TestEvidenceSufficiencyAndFreshness(unittest.TestCase): + def with_record(self, **options: object) -> DecisionOutcome: + world = make_world() + changed = record( + world.candidate, + target(FUNC1), + PASS, + definition=world.definitions[FUNC1], + n=42, + **options, # type: ignore[arg-type] + ) + return run(make_world(results={target(FUNC1): changed})) + + def test_a_result_below_the_minimum_evidence_level_is_not_proof(self) -> None: + out = self.with_record(level="L0") + self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_NOT_SUFFICIENT)) + + def test_the_minimum_level_is_the_policys(self) -> None: + world = make_world() + low = record( + world.candidate, + target(FUNC1), + PASS, + definition=world.definitions[FUNC1], + level="L0", + n=43, + ) + relaxed = make_world(results={target(FUNC1): low}).with_policy(min_evidence_level="L0") + self.assertEqual(decided(run(relaxed)), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + + def test_a_pass_of_another_verifier_is_not_proof(self) -> None: + # same version, other id: fresh but not sufficient (Doc 09 §11) + out = self.with_record(verifier=("other.verifier", "1")) + self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_NOT_SUFFICIENT)) + + def test_a_result_of_an_older_verifier_version_is_stale(self) -> None: + out = self.with_record(verifier=("dail.verify.reachability_cfg", "0")) + self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_STALE)) + + def test_a_report_of_another_candidate_hash_makes_every_result_stale(self) -> None: + world = make_world() + other_hash = "1" * 64 + records = [ + dataclasses.replace(r, candidate_hash=other_hash) for r in world.records.values() + ] + stale = VerificationReport.create( + candidate_id=world.candidate.candidate_id, + candidate_hash=other_hash, + results=records, + verifier_invocations=len(records), + verifier_set_version="dail-verify-1", + ) + out = run(dataclasses.replace(world, verification=stale)) + self.assertEqual(out.decision.decision, D.REJECT) + self.assertIn(R.EVIDENCE_STALE, codes(out)) + self.assertIn(R.DECISION_INCOMPLETE, codes(out)) # the report hash is not the candidate's + # only the carried-forward invariants have a proof: they do not rest on the report + self.assertEqual(sorted(sources(out)), [SEC2, SEC3]) + + def test_a_stale_result_is_not_used_instead_of_the_fresh_one_it_replaced(self) -> None: + # a FAIL of an older verifier version does not count as a FAIL (aggregate ignores it) and + # the invariant has no proof either + out = self.with_record(verifier=("dail.verify.reachability_cfg", "0")) + self.assertNotIn(R.REQUIRED_CHECK_FAILED, codes(out)) + + +class TestSeverityFold(unittest.TestCase): + """C-158: REJECT above ESCALATE above RETRY, over every pair of conditions.""" + + CASES = { + "REJECT": {target(SEC1): FAIL}, + "ESCALATE": {target(FUNC1): ERROR}, + "RETRY": {BASELINE_ITEM: UNKNOWN}, + } + WANT = { + frozenset({"REJECT"}): D.REJECT, + frozenset({"ESCALATE"}): D.ESCALATE, + frozenset({"RETRY"}): D.RETRY, + frozenset({"REJECT", "ESCALATE"}): D.REJECT, + frozenset({"REJECT", "RETRY"}): D.REJECT, + frozenset({"ESCALATE", "RETRY"}): D.ESCALATE, + frozenset({"REJECT", "ESCALATE", "RETRY"}): D.REJECT, + } + + def test_every_combination_gives_the_most_severe_class(self) -> None: + for names, want in self.WANT.items(): + results: dict[str, VerificationResult] = {} + for name in names: + results.update(self.CASES[name]) + with self.subTest(conditions=sorted(names)): + out = run(make_world(results=results)) # type: ignore[arg-type] + self.assertEqual(out.decision.decision, want) + self.assertEqual(len(out.decision.blocking_conditions), len(names)) + + def test_a_later_fail_is_not_hidden_behind_an_earlier_unknown(self) -> None: + # Appendix A returns at the first non-PASS item; INV-FUNC-001 is checked before INV-SEC-001 + out = run(make_world(results={target(FUNC1): UNKNOWN, target(SEC1): FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertEqual(sorted(codes(out)), [R.REQUIRED_CHECK_FAILED, R.REQUIRED_UNKNOWN]) + + def test_a_baseline_fail_is_not_hidden_behind_an_unknown_invariant(self) -> None: + out = run(make_world(results={target(SEC1): UNKNOWN, BASELINE_ITEM: FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + + def test_a_gate_fail_wins_over_an_error_and_an_unknown(self) -> None: + out = run( + make_world(results={"STRUCTURAL": FAIL, target(FUNC1): ERROR, target(SEC1): UNKNOWN}) + ) + self.assertEqual(decided(out), (D.REJECT, R.STRUCTURAL_FAILURE)) + + def test_the_reason_is_the_highest_priority_of_the_winning_class(self) -> None: + out = run(make_world(results={"STRUCTURAL": FAIL, target(FUNC1): FAIL})) + self.assertEqual(out.decision.reason, R.STRUCTURAL_FAILURE) + out = run(make_world(results={target(FUNC1): FAIL, target(SEC1): UNSUPPORTED})) + self.assertEqual(out.decision.reason, R.REQUIRED_CHECK_FAILED) + + def test_the_fold_does_not_depend_on_the_order_of_the_conditions(self) -> None: + conditions = [ + BlockingCondition(R.REQUIRED_CHECK_FAILED, D.REJECT, "A", "x"), + BlockingCondition(R.VERIFIER_ERROR, D.ESCALATE, "B", "x"), + BlockingCondition(R.REQUIRED_UNKNOWN, D.RETRY, "C", "x"), + BlockingCondition(R.EVIDENCE_STALE, D.REJECT, "D", "x"), + ] + rng = random.Random(20261029) + expected = fold(conditions) + self.assertEqual(expected, (D.REJECT, R.REQUIRED_CHECK_FAILED)) + for _ in range(50): + shuffled = conditions[:] + rng.shuffle(shuffled) + self.assertEqual(fold(shuffled), expected) + for size in (1, 2, 3): + for subset in itertools.combinations(conditions, size): + for ordering in itertools.permutations(subset): + self.assertEqual(fold(list(ordering)), fold(list(subset))) + + def test_nothing_to_fold_is_not_a_decision(self) -> None: + with self.assertRaises(DomainValidationError): + fold([]) + + +class TestRetryBudget(unittest.TestCase): + def unknown( + self, attempt: int, *, max_attempts: int = 3, extra: dict | None = None + ) -> DecisionOutcome: + results = {target(FUNC1): UNKNOWN} + results.update(extra or {}) + world = make_world(results=results).with_policy(max_attempts=max_attempts) + return run(world, attempt_number=attempt) + + def test_a_retry_below_the_budget_stays_a_retry(self) -> None: + for attempt in (1, 2): + with self.subTest(attempt=attempt): + out = self.unknown(attempt) + self.assertEqual(decided(out), (D.RETRY, R.REQUIRED_UNKNOWN)) + self.assertEqual(out.decision.attempt_number, attempt) + + def test_the_last_attempt_escalates_and_never_rejects_or_passes(self) -> None: + out = self.unknown(3) + self.assertEqual(decided(out), (D.ESCALATE, R.RETRY_BUDGET_EXHAUSTED)) + self.assertEqual(sorted(codes(out)), [R.REQUIRED_UNKNOWN, R.RETRY_BUDGET_EXHAUSTED]) + self.assertEqual(decided(self.unknown(7)), (D.ESCALATE, R.RETRY_BUDGET_EXHAUSTED)) + + def test_a_budget_of_one_escalates_the_first_unknown(self) -> None: + out = self.unknown(1, max_attempts=1) + self.assertEqual(decided(out), (D.ESCALATE, R.RETRY_BUDGET_EXHAUSTED)) + + def test_the_budget_changes_only_a_retry(self) -> None: + out = self.unknown(9, extra={target(SEC1): FAIL}) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + world = make_world(results={target(FUNC1): ERROR}).with_policy( + transient_errors=("RuntimeError",) + ) + self.assertEqual(decided(run(world, attempt_number=1)), (D.RETRY, R.VERIFIER_ERROR)) + self.assertEqual( + decided(run(world, attempt_number=3)), (D.ESCALATE, R.RETRY_BUDGET_EXHAUSTED) + ) + + +class TestEmergencySwitch(unittest.TestCase): + def test_a_would_be_promote_is_escalated(self) -> None: + out = run(make_world(automatic_enabled=False)) + self.assertEqual(decided(out), (D.ESCALATE, R.AUTOMATIC_PROMOTION_DISABLED)) + condition = out.decision.blocking_conditions[0] + self.assertIn("PROMOTE", condition.detail) # the audit keeps what it would have been + self.assertEqual(out.evidence.evidence_sufficiency, "SUFFICIENT") + self.assertEqual(len(out.proof_plan), 4) + + def test_other_decisions_are_unchanged(self) -> None: + cases = ( + ({target(SEC1): FAIL}, (D.REJECT, R.REQUIRED_CHECK_FAILED)), + ({target(FUNC1): UNKNOWN}, (D.RETRY, R.REQUIRED_UNKNOWN)), + ({target(FUNC1): ERROR}, (D.ESCALATE, R.VERIFIER_ERROR)), + ) + for results, want in cases: + with self.subTest(results=results): + out = run(make_world(results=results, automatic_enabled=False)) # type: ignore[arg-type] + self.assertEqual(decided(out), want) + self.assertNotIn(R.AUTOMATIC_PROMOTION_DISABLED, codes(out)) + + +class TestRegistryRegression(unittest.TestCase): + """C-41: the registry version is non-decreasing and nothing is retired.""" + + def test_a_policy_with_a_lower_registry_version_is_escalated(self) -> None: + world = make_world(registry_version=2).with_policy(invariant_registry_version=1) + out = run(world) + self.assertEqual(decided(out), (D.ESCALATE, R.POLICY_REGISTRY_REGRESSION)) + + def test_a_higher_or_equal_registry_version_is_fine(self) -> None: + self.assertEqual( + decided(run(make_world(registry_version=1).with_policy(invariant_registry_version=3))), + (D.PROMOTE, R.ALL_REQUIRED_PROVEN), + ) + + def test_an_invariant_of_the_current_state_missing_from_the_policy_is_escalated(self) -> None: + world = make_world() + smaller = dail_policy( + policy_version="policy-1", + invariants=[d for i, d in world.definitions.items() if i != SEC3], + automatic_enabled=True, + ) + out = run(dataclasses.replace(world, policy=smaller)) + self.assertEqual(decided(out), (D.ESCALATE, R.POLICY_REGISTRY_REGRESSION)) + self.assertIn(target(SEC3), [c.target for c in out.decision.blocking_conditions]) + + def test_a_policy_definition_older_than_the_reference_is_escalated(self) -> None: + trusted = trusted_state(versions={SEC2: 2}) + world = make_world() + candidate = analyzing_candidate(trusted, canonical_resources(ssh_open=False, db_path=True)) + impact = impact_for(trusted, candidate, carry=(SEC2, SEC3), affected=(SEC1, FUNC1)) + records = [ + record(candidate, "STRUCTURAL", n=1), + record(candidate, "CONSISTENCY", n=2), + record(candidate, target(SEC1), definition=world.definitions[SEC1], n=3), + record(candidate, target(FUNC1), definition=world.definitions[FUNC1], n=4), + record(candidate, BASELINE_ITEM, n=5), + ] + again = dataclasses.replace( + world, + trusted=trusted, + candidate=candidate, + impact=impact, + verification=report_of(candidate, records), + ) + out = run(again) + self.assertEqual(decided(out), (D.ESCALATE, R.POLICY_REGISTRY_REGRESSION)) + + def test_a_new_invariant_is_required_and_needs_a_fresh_verified_pass(self) -> None: + # the state has three invariants; the registry has four and the policy requires the new one + trusted = trusted_state(ids=(SEC1, SEC2, SEC3)) + world = make_world() + candidate = analyzing_candidate(trusted, canonical_resources(ssh_open=False, db_path=True)) + impact = impact_for(trusted, candidate, carry=(SEC2, SEC3), affected=(SEC1,)) + policy = dail_policy( + policy_version="policy-1", + invariants=world.definitions.values(), + automatic_enabled=True, + extra_required=(FUNC1,), + ) + base = [ + record(candidate, "STRUCTURAL", n=1), + record(candidate, "CONSISTENCY", n=2), + record(candidate, target(SEC1), definition=world.definitions[SEC1], n=3), + record(candidate, BASELINE_ITEM, n=5), + ] + without = dataclasses.replace( + world, + trusted=trusted, + candidate=candidate, + impact=impact, + policy=policy, + verification=report_of(candidate, base), + ) + out = run(without) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(FUNC1)]) + func = record(candidate, target(FUNC1), definition=world.definitions[FUNC1], n=4) + with_proof = dataclasses.replace(without, verification=report_of(candidate, [*base, func])) + out = run(with_proof) + self.assertEqual(decided(out), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(sources(out)[FUNC1], ProofSource.VERIFIED) + + def test_an_invariant_whose_version_rose_cannot_be_carried_forward(self) -> None: + world = make_world() + policy = dail_policy( + policy_version="policy-1", + invariants=definitions_with(world, **{SEC2: 2}), + automatic_enabled=True, + ) + bumped = dataclasses.replace(world, policy=policy) + out = run(bumped) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(SEC2, 2)]) + # a fresh VERIFIED PASS at the new version proves it + second = next(d for d in definitions_with(world, **{SEC2: 2}) if d.invariant_id == SEC2) + fresh_v2 = record(world.candidate, target(SEC2, 2), definition=second, n=50) + done = bumped.with_report([*bumped.records.values(), fresh_v2]) + out = run(done) + self.assertEqual(decided(out), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(sources(out)[SEC2], ProofSource.VERIFIED) + + +class TestCarryForwardRules(unittest.TestCase): + """C-159: every precondition of a carry-forward removed in turn, and the never-cases.""" + + def only(self, out: DecisionOutcome) -> list[str]: + return [c.target for c in out.decision.blocking_conditions] + + def test_an_affected_invariant_is_never_carried_forward(self) -> None: + # SEC-001 is affected; with its result missing nothing may stand in for it (C-45) + out = run(make_world(results={target(SEC1): None})) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual(self.only(out), [target(SEC1)]) + self.assertNotIn(SEC1, sources(out)) + + def test_an_affected_protected_invariant_is_never_carried_forward(self) -> None: + world = make_world(affected=(SEC1, SEC2, FUNC1), results={target(SEC2): None}) + out = run(world) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_an_uncertain_invariant_is_never_carried_forward(self) -> None: + world = make_world( + affected=(SEC1,), uncertain=(SEC2,), carry=(SEC3, FUNC1), results={target(SEC2): None} + ) + out = run(world) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_carry_forward_needs_the_policy_to_permit_it(self) -> None: + world = make_world().with_policy(carry_forward_enabled=False) + out = run(world) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual(self.only(out), [target(SEC2), target(SEC3)]) + + def test_carry_forward_needs_eligible_evidence_in_the_impact_report(self) -> None: + base = make_world() + impact = impact_for( + base.trusted, + base.candidate, + carry=(SEC3,), + ineligible=(SEC2,), + affected=(SEC1, FUNC1), + ) + out = run(dataclasses.replace(base, impact=impact)) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_carry_forward_needs_the_impact_report_to_recompute_its_hash(self) -> None: + world = make_world() + object.__setattr__(world.impact, "graph_version", "tampered") + out = run(world) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + unproven = [ + c.target for c in out.decision.blocking_conditions if c.code is R.INSUFFICIENT_EVIDENCE + ] + self.assertEqual(unproven, [target(SEC2), target(SEC3)]) + self.assertIn(R.DECISION_INCOMPLETE, codes(out)) + + def test_a_violated_reference_is_never_carried_forward(self) -> None: + # R1 of the prompt: an unrelated edit cannot promote from a violated baseline invariant + world = make_world(statuses={SEC2: InvariantStatus.VIOLATED}) + out = run(world) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_an_uncertain_reference_is_never_carried_forward(self) -> None: + world = make_world(statuses={SEC2: InvariantStatus.UNCERTAIN}) + out = run(world) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_an_invalidated_reference_is_never_carried_forward(self) -> None: + world = make_world() + data = world.trusted.to_dict() + for ref in data["invariant_refs"]: + if ref["invariant_id"] == SEC2: + ref["invalidated_by_candidate_id"] = world.candidate.candidate_id + ref["invalidation_reason"] = "affected by the candidate" + invalidated = TrustedState.from_dict(data) + out = run(dataclasses.replace(world, trusted=invalidated)) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_a_version_change_is_never_carried_forward(self) -> None: + world = make_world() + policy = dail_policy( + policy_version="policy-1", + invariants=definitions_with(world, **{SEC3: 2}), + automatic_enabled=True, + ) + out = run(dataclasses.replace(world, policy=policy)) + self.assertEqual(self.only(out), [target(SEC3, 2)]) + + def test_a_fresh_result_decides_even_for_an_unaffected_invariant(self) -> None: + out = run(make_world(results={target(SEC2): FAIL})) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertEqual(self.only(out), [target(SEC2)]) + + def test_a_fresh_pass_is_preferred_to_carrying_forward(self) -> None: + out = run(make_world(results={target(SEC2): PASS})) + self.assertEqual(decided(out), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + self.assertEqual(sources(out)[SEC2], ProofSource.VERIFIED) + self.assertEqual(sources(out)[SEC3], ProofSource.CARRIED_FORWARD) + + def test_no_condition_hides_the_others(self) -> None: + out = run(make_world().with_policy(carry_forward_enabled=False)) + self.assertEqual(len(out.decision.blocking_conditions), 2) + + def test_the_refusal_says_why(self) -> None: + out = run(make_world().with_policy(carry_forward_enabled=False)) + self.assertTrue(all("carry" in c.detail for c in out.decision.blocking_conditions)) + + def test_promotion_code_never_sets_the_invalidation_fields(self) -> None: + # C-37: no P6 event sets them + for path in sorted((ROOT / "core" / "promotion").glob("*.py")): + text = path.read_text(encoding="utf-8") + for name in ("invalidated_by_candidate_id", "invalidation_reason"): + with self.subTest(file=path.name, name=name): + self.assertNotIn(name, text) + + +class TestOracleEvidence(unittest.TestCase): + """C-160, Doc 09 §16 and §17.""" + + def oracle(self, invariant: str, result: VerificationResult) -> OracleVerdict: + return OracleVerdict(invariant, 1, result, "oracle-1") + + def test_agreement_changes_nothing(self) -> None: + verdicts = [self.oracle(i, PASS) for i in ALL] + self.assertEqual( + decided(run(make_world(), oracle=verdicts)), (D.PROMOTE, R.ALL_REQUIRED_PROVEN) + ) + + def test_primary_pass_and_oracle_fail_is_a_conflict_and_never_a_promotion(self) -> None: + out = run(make_world(), oracle=[self.oracle(FUNC1, FAIL)]) + self.assertEqual(decided(out), (D.ESCALATE, R.EVIDENCE_CONFLICT)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [target(FUNC1)]) + self.assertNotIn(FUNC1, sources(out)) # not treated as proven + self.assertEqual(out.evidence.evidence_sufficiency, "INSUFFICIENT") + + def test_the_policy_may_make_a_conflict_a_rejection(self) -> None: + world = make_world().with_policy(conflict_decision=D.REJECT) + out = run(world, oracle=[self.oracle(FUNC1, FAIL)]) + self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_CONFLICT)) + + def test_an_oracle_fail_on_a_carried_forward_invariant_is_a_conflict(self) -> None: + out = run(make_world(), oracle=[self.oracle(SEC2, FAIL)]) + self.assertEqual(decided(out), (D.ESCALATE, R.EVIDENCE_CONFLICT)) + self.assertNotIn(SEC2, sources(out)) + + def test_primary_fail_and_oracle_pass_stays_a_rejection(self) -> None: + out = run(make_world(results={target(FUNC1): FAIL}), oracle=[self.oracle(FUNC1, PASS)]) + self.assertEqual(decided(out), (D.REJECT, R.REQUIRED_CHECK_FAILED)) + self.assertNotIn(R.EVIDENCE_CONFLICT, codes(out)) + + def test_primary_unknown_and_oracle_pass_stays_unknown(self) -> None: + out = run(make_world(results={target(FUNC1): UNKNOWN}), oracle=[self.oracle(FUNC1, PASS)]) + self.assertEqual(decided(out), (D.RETRY, R.REQUIRED_UNKNOWN)) + + def test_an_oracle_pass_never_proves_a_missing_result(self) -> None: + out = run(make_world(results={target(FUNC1): None}), oracle=[self.oracle(FUNC1, PASS)]) + self.assertEqual(decided(out), (D.REJECT, R.INSUFFICIENT_EVIDENCE)) + + def test_a_verdict_for_another_version_or_an_unrequired_invariant_is_ignored(self) -> None: + verdicts = [OracleVerdict(FUNC1, 2, FAIL, "oracle-1"), self.oracle("INV-OTHER-001", FAIL)] + self.assertEqual( + decided(run(make_world(), oracle=verdicts)), (D.PROMOTE, R.ALL_REQUIRED_PROVEN) + ) + + def test_a_stale_parent_still_wins_over_a_conflict(self) -> None: + world = dataclasses.replace(make_world(), trusted=trusted_state(state_id=uid(2))) + self.assertEqual( + decided(run(world, oracle=[self.oracle(FUNC1, FAIL)])), (D.REJECT, R.STALE_PARENT) + ) + + def test_the_policy_cannot_accept_the_oracle(self) -> None: + with self.assertRaises(DomainValidationError): + make_world().with_policy(accept_oracle_for_unknown=True) + + +class TestDecisionCompleteness(unittest.TestCase): + """C-161, Doc 11 §43.""" + + def test_a_tampered_verification_report_downgrades_a_promote(self) -> None: + world = make_world() + object.__setattr__(world.verification, "content_hash", "0" * 64) + out = run(world) + self.assertEqual(decided(out), (D.ESCALATE, R.DECISION_INCOMPLETE)) + self.assertIn("verification", out.decision.blocking_conditions[0].detail) + + def test_a_tampered_impact_report_downgrades_a_promote(self) -> None: + # every invariant verified, so carry_forward_ok is not what is tested here + world = make_world(affected=ALL, carry=()) + object.__setattr__(world.impact, "graph_version", "tampered") + out = run(world) + self.assertEqual(decided(out), (D.ESCALATE, R.DECISION_INCOMPLETE)) + + def test_a_non_promote_keeps_its_decision_and_records_the_incompleteness(self) -> None: + world = make_world(results={target(FUNC1): UNKNOWN}) + object.__setattr__(world.verification, "content_hash", "0" * 64) + out = run(world) + self.assertEqual(decided(out), (D.RETRY, R.REQUIRED_UNKNOWN)) + self.assertIn(R.DECISION_INCOMPLETE, codes(out)) + + def test_a_complete_decision_has_no_problem(self) -> None: + world = make_world() + out = run(world) + self.assertEqual( + completeness_problems( + world.candidate, + out.decision.parent_state_id, + out.decision.supporting_results, + world.impact, + world.verification, + world.policy, + ), + [], + ) + + def test_each_clause_is_checked(self) -> None: + world = make_world() + out = run(world) + supporting = list(out.decision.supporting_results) + parent = out.decision.parent_state_id + + def problems(**changes: object) -> list[str]: + args: dict[str, object] = { + "candidate": world.candidate, + "parent_state_id": parent, + "supporting": supporting, + "impact": world.impact, + "verification": world.verification, + "policy": world.policy, + } + args.update(changes) + return completeness_problems( # type: ignore[arg-type] + args["candidate"], + args["parent_state_id"], + args["supporting"], + args["impact"], + args["verification"], + args["policy"], + ) + + self.assertTrue(problems(parent_state_id=uid(2))) # parent binding + self.assertTrue( + problems(supporting=[*supporting, uid(31337)]) + ) # a result that is not there + other = make_world(results={target(FUNC1): FAIL}) + self.assertEqual(problems(verification=other.verification), []) # hashes recompute + broken_report = make_world() + object.__setattr__(broken_report.verification, "content_hash", "0" * 64) + self.assertTrue(problems(verification=broken_report.verification)) + broken_impact = make_world() + object.__setattr__(broken_impact.impact, "graph_version", "tampered") + self.assertTrue(problems(impact=broken_impact.impact)) + + def test_the_candidate_hash_of_the_report_must_be_the_candidates(self) -> None: + world = make_world() + other_hash = "1" * 64 + records = [ + dataclasses.replace(r, candidate_hash=other_hash) for r in world.records.values() + ] + report = VerificationReport.create( + candidate_id=world.candidate.candidate_id, + candidate_hash=other_hash, + results=records, + verifier_invocations=len(records), + verifier_set_version="dail-verify-1", + ) + found = completeness_problems( + world.candidate, world.trusted.state_id, [], world.impact, report, world.policy + ) + self.assertEqual(len(found), 1) + self.assertIn("candidate_hash", found[0]) + + +class TestReportBindings(unittest.TestCase): + """The impact and verification reports must be those of this candidate and parent.""" + + def test_an_impact_report_of_another_candidate_is_rejected(self) -> None: + world = make_world() + elsewhere = analyzing_candidate( + world.trusted, canonical_resources(ssh_open=False, db_path=True), n=2 + ) + self.assertNotEqual(elsewhere.candidate_id, world.candidate.candidate_id) + other = dataclasses.replace( + world, + impact=impact_for(world.trusted, elsewhere, carry=(SEC2, SEC3), affected=(SEC1, FUNC1)), + ) + out = run(other) + self.assertEqual(decided(out), (D.REJECT, R.INCONSISTENT_REPORTS)) + self.assertNotIn(SEC2, sources(out)) + + def test_an_impact_report_of_another_parent_is_rejected(self) -> None: + world = make_world() + elsewhere = trusted_state(state_id=uid(2)) + report = impact_for(elsewhere, world.candidate, carry=(SEC2, SEC3), affected=(SEC1, FUNC1)) + out = run(dataclasses.replace(world, impact=report)) + self.assertEqual(decided(out), (D.REJECT, R.INCONSISTENT_REPORTS)) + + def test_a_verification_report_of_another_candidate_is_rejected(self) -> None: + world = make_world() + report = VerificationReport.create( + candidate_id=uid(99), + candidate_hash=world.candidate.state_hash or "", + results=[dataclasses.replace(r, candidate_id=uid(99)) for r in world.records.values()], + verifier_invocations=5, + verifier_set_version="dail-verify-1", + ) + out = run(dataclasses.replace(world, verification=report)) + self.assertEqual(decided(out), (D.REJECT, R.INCONSISTENT_REPORTS)) + + +class TestMalformedArguments(unittest.TestCase): + def test_wrong_types_raise_an_input_error(self) -> None: + w = make_world() + calls = { + "candidate": lambda: self.call(w, candidate=w.trusted), + "trusted": lambda: self.call(w, trusted=w.candidate), + "impact": lambda: self.call(w, impact=w.verification), + "verification": lambda: self.call(w, verification=w.impact), + "policy": lambda: self.call(w, policy="policy"), + } + for name, call in calls.items(): + with self.subTest(argument=name), self.assertRaises(PromotionInputError): + call() + + def call(self, world: World, **replace: object) -> DecisionOutcome: + from core.promotion.decide import decide + + args: dict[str, object] = { + "candidate": world.candidate, + "trusted": world.trusted, + "impact": world.impact, + "verification": world.verification, + "policy": world.policy, + } + args.update(replace) + return decide( + args["candidate"], # type: ignore[arg-type] + args["trusted"], # type: ignore[arg-type] + args["impact"], # type: ignore[arg-type] + args["verification"], # type: ignore[arg-type] + args["policy"], # type: ignore[arg-type] + decision_id=uid(9100), + now=world.trusted.created_at, + ) + + def test_the_other_arguments_are_checked_too(self) -> None: + from datetime import datetime + + from core.promotion.decide import decide + + w = make_world() + + def call(**kw: object) -> DecisionOutcome: + args: dict[str, object] = { + "decision_id": uid(9100), + "now": w.trusted.created_at, + "attempt_number": 1, + "oracle_verdicts": (), + } + args.update(kw) + return decide(w.candidate, w.trusted, w.impact, w.verification, w.policy, **args) # type: ignore[arg-type] + + for name, value in ( + ("decision_id", "not-a-uuid"), + ("now", datetime(2026, 10, 1)), # naive + ("now", "2026-10-01"), + ("attempt_number", 0), + ("attempt_number", True), + ("attempt_number", "1"), + ("oracle_verdicts", ("PASS",)), + ("oracle_verdicts", "oracle"), + ): + with self.subTest(argument=name, value=value), self.assertRaises(PromotionInputError): + call(**{name: value}) + duplicate = OracleVerdict(FUNC1, 1, PASS, "o") + with self.assertRaises(PromotionInputError): + call(oracle_verdicts=(duplicate, OracleVerdict(FUNC1, 1, FAIL, "o"))) + + def test_another_lineage_is_an_input_error_not_a_decision(self) -> None: + w = make_world() + other_lineage = baseline(lineage_id=uid(77)) + with self.assertRaises(PromotionInputError): + self.call(w, trusted=other_lineage) + + def test_a_candidate_that_is_not_under_analysis_is_an_input_error(self) -> None: + w = make_world() + for status in (CandidateStatus.REJECTED, CandidateStatus.RETRY_REQUIRED): + from core.domain.state import transition_candidate + + moved = transition_candidate(w.candidate, status) + with self.subTest(status=status), self.assertRaises(PromotionInputError): + self.call(w, candidate=moved) + + +class TestPurity(unittest.TestCase): + def test_the_same_inputs_give_the_same_outcome(self) -> None: + world = make_world() + self.assertEqual(run(world), run(world)) + self.assertEqual(run(world).decision.content_hash, run(world).decision.content_hash) + + def test_the_id_changes_the_id_and_nothing_else(self) -> None: + world = make_world() + a, b = run(world), run(world, decision_id=uid(9200)) + self.assertNotEqual(a.decision.decision_id, b.decision.decision_id) + self.assertEqual(a.decision.content_hash, b.decision.content_hash) + self.assertEqual(a.proof_plan, b.proof_plan) + + def test_no_argument_is_changed(self) -> None: + for world in ( + make_world(), + make_world(results={target(FUNC1): FAIL}), + make_world(results={target(FUNC1): UNKNOWN}), + dataclasses.replace(make_world(), trusted=trusted_state(state_id=uid(2))), + ): + before = ( + world.candidate.to_dict(), + world.trusted.to_dict(), + world.impact.to_dict(), + world.verification.to_dict(), + world.policy, + ) + run(world, oracle=[OracleVerdict(FUNC1, 1, FAIL, "o")]) + after = ( + world.candidate.to_dict(), + world.trusted.to_dict(), + world.impact.to_dict(), + world.verification.to_dict(), + world.policy, + ) + self.assertEqual(before, after) + + def test_the_decision_code_has_no_clock_randomness_or_io(self) -> None: + for path in sorted((ROOT / "core" / "promotion").glob("*.py")): + text = path.read_text(encoding="utf-8") + for forbidden in ( + "datetime.now", + "utcnow", + "time.time", + "import random", + "uuid4", + "open(", + "print(", + "import os", + "import logging", + ): + with self.subTest(file=path.name, forbidden=forbidden): + self.assertNotIn(forbidden, text) + + def test_the_decision_never_runs_or_repairs_verification(self) -> None: + for path in sorted((ROOT / "core" / "promotion").glob("*.py")): + tree = ast.parse(path.read_text(encoding="utf-8")) + for node in ast.walk(tree): + if isinstance(node, ast.ImportFrom): + self.assertFalse((node.module or "").startswith("core.verification"), path.name) + if isinstance(node, ast.Name): + self.assertNotEqual(node.id, "run_work_set", path.name) + + +if __name__ == "__main__": + unittest.main() From e9b1e0c8281c6f433808dc4dc2e191501126b56f Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:42:05 +0530 Subject: [PATCH 6/8] =?UTF-8?q?P6a=20step=205:=20candidate=5Fafter=20appli?= =?UTF-8?q?es=20a=20decision=20to=20the=20candidate=20lifecycle=20without?= =?UTF-8?q?=20touching=20Trusted=20State=20(Doc=2006=20=C2=A75,=20=C2=A720?= =?UTF-8?q?,=20=C2=A722=20SM-001=20to=20SM-004,=20SM-010;=20C-29,=20C-157)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROMOTE -> PROMOTABLE (never PROMOTED), REJECT -> REJECTED (a PROMOTABLE candidate only through the stale-parent exit), RETRY -> RETRY_REQUIRED, ESCALATE -> ESCALATED, with the existing transition functions only. The decision must be about this candidate and its parent; a PROMOTE against a state that is no longer the parent raises StaleParentError (SM-010). The trusted state is read and never changed. 17 tests, written first; at the first run 14 of 17 passed and the 3 failures were one test comparing resources of two separate worlds. Co-Authored-By: Claude Sonnet 5.5 --- core/promotion/lifecycle.py | 76 ++++++++ tests/unit/test_promotion_lifecycle.py | 232 +++++++++++++++++++++++++ 2 files changed, 308 insertions(+) create mode 100644 core/promotion/lifecycle.py create mode 100644 tests/unit/test_promotion_lifecycle.py diff --git a/core/promotion/lifecycle.py b/core/promotion/lifecycle.py new file mode 100644 index 0000000..cdef2fc --- /dev/null +++ b/core/promotion/lifecycle.py @@ -0,0 +1,76 @@ +"""Applying a decision to the candidate (P6a; Doc 06 §4-§5, §20, §22 SM-001 to SM-004 and SM-010, +Doc 09 §21-§25; C-29, C-157). + +``candidate_after`` moves a candidate under analysis along the legal exit of Doc 06 §5 that the +decision names, using only the existing lifecycle functions of ``core.domain.state``: + + PROMOTE -> PROMOTABLE (never PROMOTED: SM-002, the commit of P6b does that) + REJECT -> REJECTED (a PROMOTABLE candidate only through the stale-parent exit, C-29) + RETRY -> RETRY_REQUIRED + ESCALATE -> ESCALATED + +The trusted state is read (its id, its lineage) and never changed: a decision does not advance +Trusted State (SM-001), and a rejection or a retry preserves the current one (SM-003, SM-004). +Nothing here creates or advances a trusted state. + +Standard library and ``core.domain`` only (R18). +""" + +from __future__ import annotations + +from core.domain.enums import CandidateStatus, DecisionType +from core.domain.errors import StaleParentError +from core.domain.promotion import DecisionReason, PromotionDecision, PromotionInputError +from core.domain.state import ( + CandidateState, + TrustedState, + reject_stale_candidate, + transition_candidate, +) + +_EXIT = { + DecisionType.REJECT: CandidateStatus.REJECTED, + DecisionType.RETRY: CandidateStatus.RETRY_REQUIRED, + DecisionType.ESCALATE: CandidateStatus.ESCALATED, +} + + +def candidate_after( + decision: PromotionDecision, candidate: CandidateState, trusted: TrustedState +) -> CandidateState: + """The candidate once ``decision`` is applied; ``trusted`` is only read. + + The decision must be about this candidate and its parent (DATA-INT-003). A candidate that is + not in the status the exit needs, or whose exit the lifecycle forbids, raises the domain's + ``IllegalTransitionError``; a PROMOTE for a candidate whose parent is no longer the current + state raises ``StaleParentError`` (SM-010).""" + if not isinstance(decision, PromotionDecision): + raise PromotionInputError("candidate_after: decision must be a PromotionDecision") + if not isinstance(candidate, CandidateState): + raise PromotionInputError("candidate_after: candidate must be a CandidateState") + if not isinstance(trusted, TrustedState): + raise PromotionInputError("candidate_after: trusted must be a TrustedState") + if decision.candidate_id != candidate.candidate_id: + raise PromotionInputError("candidate_after: the decision is about another candidate") + if decision.parent_state_id != candidate.parent_state_id: + raise PromotionInputError( + "candidate_after: the decision's parent is not the candidate's parent (DATA-INT-003)" + ) + if candidate.lineage_id != trusted.lineage_id: + raise PromotionInputError("candidate_after: the trusted state is in another lineage") + if decision.decision is DecisionType.PROMOTE: + if candidate.parent_state_id != trusted.state_id: + raise StaleParentError( + candidate.status, + CandidateStatus.PROMOTABLE, + f"the candidate's parent {candidate.parent_state_id} is not the current state " + f"{trusted.state_id}", + ) + return transition_candidate(candidate, CandidateStatus.PROMOTABLE) + if ( + decision.decision is DecisionType.REJECT + and decision.reason is DecisionReason.STALE_PARENT + and candidate.status is CandidateStatus.PROMOTABLE + ): + return reject_stale_candidate(candidate, trusted) + return transition_candidate(candidate, _EXIT[decision.decision]) diff --git a/tests/unit/test_promotion_lifecycle.py b/tests/unit/test_promotion_lifecycle.py new file mode 100644 index 0000000..cb34a8b --- /dev/null +++ b/tests/unit/test_promotion_lifecycle.py @@ -0,0 +1,232 @@ +"""Applying a decision to the candidate (P6a step 5; Doc 06 §4-§5, §20, §22 SM-001 to SM-004 and +SM-010, §25-§26, Doc 09 §21-§25). + +Expected values come from the spec text: ANALYZING leaves to REJECTED, RETRY_REQUIRED, ESCALATED or +PROMOTABLE (Doc 06 §5); a PROMOTE makes the candidate PROMOTABLE and never PROMOTED (SM-002: only +the commit of P6b); a REJECT or a RETRY "preserves the current Trusted State" (SM-003, SM-004) and +"later attempts start from the unchanged baseline" (Doc 06 §25); a stale-parent candidate cannot +promote (SM-010) and a PROMOTABLE one is rejected only through the stale-parent exit (C-29). +""" + +from __future__ import annotations + +import ast +import dataclasses +import unittest +from pathlib import Path + +from core.domain.enums import CandidateStatus as CS +from core.domain.enums import DecisionType +from core.domain.errors import IllegalTransitionError, StaleParentError +from core.domain.promotion import DecisionOutcome, DecisionReason, PromotionInputError +from core.domain.state import ( + CandidateState, + TrustedState, + mark_promoted, + transition_candidate, +) +from core.promotion.lifecycle import candidate_after +from tests.domain_builders import analyzing_candidate, canonical_resources, patch_for, uid +from tests.promotion_builders import ( + ERROR, + FAIL, + FUNC1, + UNKNOWN, + World, + make_world, + run, + target, + trusted_state, +) + +D, R = DecisionType, DecisionReason +ROOT = Path(__file__).resolve().parents[2] +LIFECYCLE = ROOT / "core" / "promotion" / "lifecycle.py" + + +def apply(world: World, outcome: DecisionOutcome) -> CandidateState: + return candidate_after(outcome.decision, world.candidate, world.trusted) + + +class TestFromAnalyzing(unittest.TestCase): + def test_each_decision_takes_the_candidate_to_the_status_of_doc_06_section_5(self) -> None: + cases = ( + (make_world(), D.PROMOTE, CS.PROMOTABLE), + (make_world(results={target(FUNC1): FAIL}), D.REJECT, CS.REJECTED), + (make_world(results={target(FUNC1): UNKNOWN}), D.RETRY, CS.RETRY_REQUIRED), + (make_world(results={target(FUNC1): ERROR}), D.ESCALATE, CS.ESCALATED), + ) + for world, decision, status in cases: + outcome = run(world) + with self.subTest(decision=decision): + self.assertEqual(outcome.decision.decision, decision) + self.assertEqual(world.candidate.status, CS.ANALYZING) + self.assertEqual(apply(world, outcome).status, status) + + def test_a_promote_never_makes_the_candidate_promoted(self) -> None: + # SM-002: PROMOTED is reached only by mark_promoted after TrustedState.promote (P6b) + world = make_world() + moved = apply(world, run(world)) + self.assertNotEqual(moved.status, CS.PROMOTED) + with self.assertRaises(IllegalTransitionError) as caught: + transition_candidate(moved, CS.PROMOTED) + self.assertEqual(caught.exception.rule, "SM-002") + + def test_the_candidate_keeps_its_content(self) -> None: + for results in ({}, {target(FUNC1): FAIL}, {target(FUNC1): UNKNOWN}): + world = make_world(results=results) + moved = apply(world, run(world)) + with self.subTest(results=results): + self.assertEqual(moved.candidate_id, world.candidate.candidate_id) + self.assertEqual(moved.state_hash, world.candidate.state_hash) + self.assertEqual(moved.parent_state_id, world.candidate.parent_state_id) + self.assertEqual(moved.resources, world.candidate.resources) + + def test_the_applied_candidate_is_a_new_object(self) -> None: + world = make_world() + before = world.candidate.to_dict() + moved = apply(world, run(world)) + self.assertIsNot(moved, world.candidate) + self.assertEqual(world.candidate.to_dict(), before) + + +class TestTheTrustedStateIsNeverTouched(unittest.TestCase): + """SM-001, SM-003, SM-004: a decision never advances Trusted State, and a rejection or a retry + leaves the current one in place.""" + + def test_no_decision_changes_the_trusted_state(self) -> None: + for results in ( + {}, + {target(FUNC1): FAIL}, + {target(FUNC1): UNKNOWN}, + {target(FUNC1): ERROR}, + ): + world = make_world(results=results) + before = (world.trusted.state_hash, world.trusted.to_dict()) + apply(world, run(world)) + with self.subTest(results=results): + self.assertEqual((world.trusted.state_hash, world.trusted.to_dict()), before) + + def test_a_later_attempt_starts_again_from_the_unchanged_parent(self) -> None: + # SM-003 / Doc 06 §25: after a REJECT the next candidate is built from the same state + world = make_world(results={target(FUNC1): FAIL}) + rejected = apply(world, run(world)) + self.assertEqual(rejected.status, CS.REJECTED) + again = CandidateState.create( + parent=world.trusted, + patch=patch_for(world.trusted, n=9), + candidate_sequence=2, + now=world.trusted.created_at, + ) + self.assertEqual(again.parent_state_id, world.trusted.state_id) + self.assertEqual(again.parent_state_id, rejected.parent_state_id) + + def test_a_rejected_retried_or_escalated_candidate_cannot_become_promotable(self) -> None: + for results, final in ( + ({target(FUNC1): FAIL}, CS.REJECTED), + ({target(FUNC1): UNKNOWN}, CS.RETRY_REQUIRED), + ({target(FUNC1): ERROR}, CS.ESCALATED), + ): + world = make_world(results=results) + moved = apply(world, run(world)) + with self.subTest(status=final), self.assertRaises(IllegalTransitionError): + transition_candidate(moved, CS.PROMOTABLE) + self.assertEqual(moved.status, final) + + def test_nothing_here_can_create_or_advance_a_trusted_state(self) -> None: + source = ast.parse(LIFECYCLE.read_text(encoding="utf-8")) + names = {n.attr for n in ast.walk(source) if isinstance(n, ast.Attribute)} | { + n.id for n in ast.walk(source) if isinstance(n, ast.Name) + } + for forbidden in ("promote", "mark_promoted", "establish_baseline"): + self.assertNotIn(forbidden, names) + self.assertTrue(callable(mark_promoted) and callable(TrustedState.promote)) + + +class TestStaleParent(unittest.TestCase): + def newer(self, world: World) -> World: + return dataclasses.replace(world, trusted=trusted_state(state_id=uid(2))) + + def test_an_analyzing_candidate_of_an_old_parent_is_rejected(self) -> None: + world = self.newer(make_world()) + outcome = run(world) + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), (D.REJECT, R.STALE_PARENT) + ) + self.assertEqual(apply(world, outcome).status, CS.REJECTED) + + def test_a_promotable_candidate_is_rejected_through_the_stale_parent_exit(self) -> None: + # C-29: PROMOTABLE -> REJECTED only as a stale parent + world = self.newer(make_world(candidate_status=CS.PROMOTABLE)) + outcome = run(world) + moved = apply(world, outcome) + self.assertEqual(moved.status, CS.REJECTED) + self.assertEqual(moved.status_reason, "STALE_PARENT") + + def test_a_promotable_candidate_cannot_be_rejected_for_another_reason(self) -> None: + world = make_world(candidate_status=CS.PROMOTABLE, results={target(FUNC1): FAIL}) + outcome = run(world) + self.assertEqual(outcome.decision.decision, D.REJECT) + with self.assertRaises(IllegalTransitionError): + apply(world, outcome) + + def test_a_promote_cannot_be_applied_when_the_parent_is_no_longer_current(self) -> None: + # SM-010: build a PROMOTE for the old parent, then try to apply it against the new state + world = make_world() + outcome = run(world) + self.assertEqual(outcome.decision.decision, D.PROMOTE) + with self.assertRaises(StaleParentError) as caught: + candidate_after(outcome.decision, world.candidate, trusted_state(state_id=uid(2))) + self.assertEqual(caught.exception.rule, "SM-010") + + +class TestBindings(unittest.TestCase): + def test_a_decision_for_another_candidate_is_refused(self) -> None: + world = make_world() + other = analyzing_candidate( + world.trusted, canonical_resources(ssh_open=False, db_path=True), n=2 + ) + with self.assertRaises(PromotionInputError): + candidate_after(run(world).decision, other, world.trusted) + + def test_a_decision_for_another_parent_is_refused(self) -> None: + world = make_world() + decision = run(world).decision + elsewhere = trusted_state(state_id=uid(2)) + other_candidate = analyzing_candidate( + elsewhere, canonical_resources(ssh_open=False, db_path=True), n=1 + ) + with self.assertRaises(PromotionInputError): + candidate_after(decision, other_candidate, elsewhere) + + def test_the_arguments_are_type_checked(self) -> None: + world = make_world() + decision = run(world).decision + for args in ( + (None, world.candidate, world.trusted), + (decision, world.trusted, world.trusted), + (decision, world.candidate, world.candidate), + ): + with ( + self.subTest(args=[type(a).__name__ for a in args]), + self.assertRaises(PromotionInputError), + ): + candidate_after(*args) # type: ignore[arg-type] + + def test_a_candidate_that_was_already_decided_cannot_be_decided_again(self) -> None: + world = make_world() + outcome = run(world) + moved = apply(world, outcome) + with self.assertRaises(IllegalTransitionError): + candidate_after(outcome.decision, moved, world.trusted) + + def test_a_candidate_that_is_not_analyzing_cannot_receive_a_decision(self) -> None: + world = make_world(results={target(FUNC1): UNKNOWN}) + retried = apply(world, run(world)) + failing = make_world(results={target(FUNC1): FAIL}) + with self.assertRaises(IllegalTransitionError): + candidate_after(run(failing).decision, retried, failing.trusted) + + +if __name__ == "__main__": + unittest.main() From 689728af1111004a8ce690ffb94d7690cc3663c6 Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:46:23 +0530 Subject: [PATCH 7/8] =?UTF-8?q?P6a=20step=206a:=20the=20canonical=20transi?= =?UTF-8?q?tions=20and=20every=20fixture=20with=20a=20parent=20through=20t?= =?UTF-8?q?he=20real=20pipeline=20(Doc=2012=20=C2=A75-=C2=A77,=20Doc=2006?= =?UTF-8?q?=20=C2=A725-=C2=A726;=20C-22,=20C-45,=20C-159)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit tests/promotion_pipeline.py runs normalisation, identity, graphs, impact (with the prior proofs of the trusted state), the scope policy, the verification engine and decide. patch_safe promotes (INV-SEC-001 VERIFIED because its reference is VIOLATED; the others VERIFIED or CARRIED_FORWARD as the engine's own impact report says), patch_regression is rejected with the functional check as its blocking condition, Stateful-Full carries nothing, and 15 of the other 15 decisions are among the reviewer's decision.allowed. The real pipeline found a defect in decide: every gate item was EVIDENCE_NOT_SUFFICIENT, because the engine gives STRUCTURAL and CONSISTENCY level L0 and decide applied the L1 minimum to them; the test builder had used L1 for them too. The level rule now applies to invariants and baseline items only (C-159 updated), with tests for both. Co-Authored-By: Claude Sonnet 5.5 --- core/promotion/decide.py | 7 +- docs/DECISIONS_REGISTER.md | 2 +- tests/promotion_builders.py | 7 +- tests/promotion_pipeline.py | 266 +++++++++++++++++++++++ tests/unit/test_promotion_decide.py | 14 ++ tests/unit/test_promotion_fixtures.py | 299 ++++++++++++++++++++++++++ 6 files changed, 589 insertions(+), 6 deletions(-) create mode 100644 tests/promotion_pipeline.py create mode 100644 tests/unit/test_promotion_fixtures.py diff --git a/core/promotion/decide.py b/core/promotion/decide.py index 9dbb77e..09f4e13 100644 --- a/core/promotion/decide.py +++ b/core/promotion/decide.py @@ -405,7 +405,7 @@ def _assess_result( invariant_version=None if invariant is None else invariant.version, verifier_id=verifier_id, verifier_version=verifier_version, - ) and _level_ok(record, policy): + ) and (item.kind == "GATE" or _level_ok(record, policy)): verdict.check = RequiredCheck( target, _kind(item), ProofSource.VERIFIED, record.verification_id ) @@ -426,7 +426,10 @@ def _assess_result( D.REJECT, target, f"{described} is not sufficient proof: it must be from {verifier_id} " - f"{verifier_version} at level {policy.min_evidence_level} or above", + f"{verifier_version}" + + ( + "" if item.kind == "GATE" else f" at level {policy.min_evidence_level} or above" + ), ) ) return diff --git a/docs/DECISIONS_REGISTER.md b/docs/DECISIONS_REGISTER.md index 436cc18..d075283 100644 --- a/docs/DECISIONS_REGISTER.md +++ b/docs/DECISIONS_REGISTER.md @@ -170,6 +170,6 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec | C-156 | P5b-fix: an unresolved entry of `vpc_security_group_ids` is row 4; the engine is compared exactly | Registry §6.3 E3: each entry of `D.vpc_security_group_ids` references a configured aws_security_group with a resolved `vpc_id`; §6.4 row 4: when E3 or E4 needs an unresolved value the result is UNKNOWN. P5b let an unresolved entry (a variable, a `concat` with a variable, a group of unknown `count`) reach row 6 and give PASS when the known groups established the path (found by the external review of PR #22). **(1)** An entry of `D.vpc_security_group_ids` that is unresolved, or that references a placeholder group, is added to the row 4 reasons when the side is read, so row 4 (UNKNOWN, `attribute.unresolved`) applies after rows 1 to 3 and any row 2 cause, and before rows 5 to 9; the path is neither a PASS nor a FAIL then. **(2)** The same for `S.vpc_security_group_ids`; the registry is silent, see C-155 item 13. **(3)** The row 7 use of the unresolved entries of the side is unchanged; row 4 now returns first, so it is not reached for them. **(4)** A literal id stays UNSUPPORTED (C-155 item 7). **(5)** E2 compares `engine` with the exact string `postgres`, as the registry writes it; `Postgres` or `POSTGRES` without a port is row 3 (FAIL) (before, the comparison ignored case). Open question for the authors: the provider may accept other spellings of the engine name; no behaviour beyond the exact comparison. **(6)** Two P5b tests asserted the superseded results (an unresolved entry of `S` with the path established: PASS, row 6; with no path: row 7); they now assert UNKNOWN, row 4, and were changed in the commit that changes the code. | Proposed (P5b-fix) | | C-157 | P6a: boundary, types and entry point of the decision half of the Promotion Controller | New rule **R18**: `core.promotion` imports only the standard library and `core.domain.*` (never `core.verification`, `core.identity`, `core.dependency`, `core.impact`, `core.terraform_model`, `core.persistence`, `core.application`, `evidence`), with a self-test like R14 to R17; nothing is loosened; R8 is unchanged and P6a does not use it (P6b is the first caller of `promote`). Types in `core/domain/promotion.py`: `PromotionDecision` (Doc 05 §15), `PromotionEvidence` (Doc 11 §26), `PromotionPolicy`, the closed vocabularies `DecisionReason` and `ProofSource` (VERIFIED, CARRIED_FORWARD), `OracleVerdict`, `ProofPlanEntry`, `DecisionOutcome` and `PromotionInputError` (a `DomainValidationError`). Logic in `core/promotion/` (`decide.py`, `policy.py`, `lifecycle.py`). Entry point `decide(candidate, trusted, impact, verification, policy, *, decision_id, now, attempt_number=1, oracle_verdicts=()) -> DecisionOutcome`, where `DecisionOutcome` holds the `PromotionDecision`, the `ProofPlan` (which source proves each required invariant, for P6b) and the `PromotionEvidence`. `decide` is pure: no clock, no randomness (`decision_id` and `now` are injected), no I/O, no mutation of any argument. Malformed arguments (wrong types, another lineage, a candidate that is neither ANALYZING nor PROMOTABLE, a bad attempt number, duplicate oracle verdicts) raise `PromotionInputError`; everything the decision itself finds is a REJECT, RETRY or ESCALATE, never an exception. **Implementation notes (P6a):** `PromotionDecision` adds `reason`, `attempt_number` and `content_hash` to the fields of Doc 05 §15 (the spec lists no reason field, but says non-promotion decisions must preserve their blocking reasons; `blocking_conditions` keeps all of them, `reason` is the highest-severity one); `PromotionPolicy` carries the invariant definitions of its registry version (`invariants`), because `core.promotion` may not import a registry; it also carries the verifier ids that the two gate items are expected to name (`gate_verifiers`; the baseline items of created resources name the verifier that the verification engine chose for the resource type, so the result's own verifier is accepted for RESOURCE items: an assumption and a spec gap, see the P6a report); the gate verifier ids are copied from `core.verification.engine` and a test (which may import both) pins that they are equal; `decide` takes the current trusted state of the lineage as `trusted`. | Proposed (P6a) | | C-158 | P6a: `decide()` order, severity and the retry/escalate table | Order (Doc 09 Appendix A, extended): (1) emergency switch and policy sanity; (2) stale parent; (3) construction and the STRUCTURAL and CONSISTENCY gate items; (4) required invariants (C-159); (5) oracle conflicts (C-160); (6) evidence sufficiency and decision completeness (C-161); (7) PROMOTE. A stale parent is checked first and wins over everything (`candidate.parent_state_id != trusted.state_id`: REJECT, `STALE_PARENT`). **Order independence, a deliberate deviation from Appendix A's early return:** the loop of Appendix A returns at the first non-PASS item, so a later FAIL could hide behind an earlier UNKNOWN. `decide` examines **all** required items and then folds by severity: any FAIL, STRUCTURAL or CONSISTENCY FAIL, or REJECT-class non-success gives **REJECT**; otherwise any ESCALATE-class gives **ESCALATE**; otherwise any RETRY-class gives **RETRY**; otherwise PROMOTE. The decision never depends on the order of results, work items or invariants (property test). **Non-success table** (`PromotionPolicy.non_success`, closed, versioned): UNKNOWN gives RETRY (a new patch or more context could resolve it); UNSUPPORTED on a required invariant gives REJECT (a retry cannot make the model larger, Doc 09 §29); VERIFIER_ERROR gives RETRY if the error `type` is in `policy.transient_errors` (default empty), else ESCALATE. A construction failure and a STRUCTURAL FAIL give REJECT, a CONSISTENCY FAIL gives REJECT (`INCONSISTENT_REPORTS`, Doc 09 §31), a missing result for a required item gives REJECT `INSUFFICIENT_EVIDENCE` (Appendix A). **Retry budget:** `policy.max_attempts` (default 3, validated 1 to 10) and the input `attempt_number`: a RETRY at `attempt_number >= max_attempts` becomes **ESCALATE** with reason `RETRY_BUDGET_EXHAUSTED` (never REJECT, never PASS; Doc 09 §23, repeated UNKNOWN is not an eventual PASS). Backoff and scheduling stay outside the core. Flagged as a decision for the authors (Doc 09 §23 puts retry limits outside the core semantic decision; only the exhaustion rule is here). **Severity order:** REJECT above ESCALATE above RETRY is a choice; the spec does not order them. Flagged for the authors. Every blocking condition found is recorded in `blocking_conditions` (sorted, closed codes), not only the first; `reason` is the highest-severity one, ties broken by a fixed list. The impact report or verification report of another candidate or parent is a REJECT `INCONSISTENT_REPORTS`. | Proposed (P6a) | -| C-159 | P6a: required set and proof source (this closes C-45) | **Required set** = every invariant on the current state (its id, at the version in the policy's registry) together with `policy.extra_required` (C-41(4)), plus the gate items STRUCTURAL and CONSISTENCY and the RESOURCE baseline items of the impact work set. A required invariant missing from the policy's registry, or at a lower version than the current reference, is an `ESCALATE` (`POLICY_REGISTRY_REGRESSION`). Each required invariant is proven by exactly one of: **VERIFIED**, a fresh (`fresh(...)`), sufficient (`sufficient(...)`) PASS in the verification report for target `INVARIANT::` with the definition's verifier id and version, and `evidence_level` not below `policy.min_evidence_level` ("L1"); or **CARRIED_FORWARD**, only if **all** hold: `policy.carry_forward_enabled`; `impact.carry_forward_ok(id, version, candidate_id=..., parent_state_id=...)` is True (the C-45 query); the parent reference exists with the **same** invariant version, status **PROTECTED** and `can_satisfy_proof()`; the invariant is **not** in the impact report's affected set and no uncertainty record names it; the definition names the same verifier as the parent's evidence (definitions are immutable, so equal versions imply it: verifier configuration changes are not modelled, an assumption and a spec gap against Doc 06 §17). **Never carried forward:** an affected invariant (C-45); a non-PROTECTED parent reference (VIOLATED or UNCERTAIN; a violated invariant must be re-verified to PASS, which is what the canonical SSH repair does); a version change; any invariant when `carry_forward_enabled` is False (the Stateful-Full condition, C-22). If a fresh result exists for the target it decides: FAIL rejects, a non-success follows the table, a sufficient PASS is VERIFIED; carry-forward is tried only when no fresh result exists. If neither source exists the decision is REJECT `INSUFFICIENT_EVIDENCE` listing the invariants without proof. A PASS that is not `sufficient` or not `fresh` is not proof (`EVIDENCE_NOT_SUFFICIENT`, `EVIDENCE_STALE`, both under INSUFFICIENT_EVIDENCE). `decide` never runs verification; the orchestrator of P6b applies the `VerificationScopePolicy` before it. A PASS marked not applicable (C-148, open) is a PASS here, as in `aggregate`. | Proposed (P6a) | +| C-159 | P6a: required set and proof source (this closes C-45) | **Required set** = every invariant on the current state (its id, at the version in the policy's registry) together with `policy.extra_required` (C-41(4)), plus the gate items STRUCTURAL and CONSISTENCY and the RESOURCE baseline items of the impact work set. A required invariant missing from the policy's registry, or at a lower version than the current reference, is an `ESCALATE` (`POLICY_REGISTRY_REGRESSION`). Each required invariant is proven by exactly one of: **VERIFIED**, a fresh (`fresh(...)`), sufficient (`sufficient(...)`) PASS in the verification report for target `INVARIANT::` with the definition's verifier id and version, and `evidence_level` not below `policy.min_evidence_level` ("L1"; the same level rule holds for a baseline item, while the two gate items are L0 evidence by construction in the verification engine and need only a `sufficient` PASS: found by running the real pipeline, where a uniform L1 rule rejected every gate item); or **CARRIED_FORWARD**, only if **all** hold: `policy.carry_forward_enabled`; `impact.carry_forward_ok(id, version, candidate_id=..., parent_state_id=...)` is True (the C-45 query); the parent reference exists with the **same** invariant version, status **PROTECTED** and `can_satisfy_proof()`; the invariant is **not** in the impact report's affected set and no uncertainty record names it; the definition names the same verifier as the parent's evidence (definitions are immutable, so equal versions imply it: verifier configuration changes are not modelled, an assumption and a spec gap against Doc 06 §17). **Never carried forward:** an affected invariant (C-45); a non-PROTECTED parent reference (VIOLATED or UNCERTAIN; a violated invariant must be re-verified to PASS, which is what the canonical SSH repair does); a version change; any invariant when `carry_forward_enabled` is False (the Stateful-Full condition, C-22). If a fresh result exists for the target it decides: FAIL rejects, a non-success follows the table, a sufficient PASS is VERIFIED; carry-forward is tried only when no fresh result exists. If neither source exists the decision is REJECT `INSUFFICIENT_EVIDENCE` listing the invariants without proof. A PASS that is not `sufficient` or not `fresh` is not proof (`EVIDENCE_NOT_SUFFICIENT`, `EVIDENCE_STALE`, both under INSUFFICIENT_EVIDENCE). `decide` never runs verification; the orchestrator of P6b applies the `VerificationScopePolicy` before it. A PASS marked not applicable (C-148, open) is a PASS here, as in `aggregate`. | Proposed (P6a) | | C-160 | P6a: oracle evidence (Doc 09 §16, §17) | `OracleVerdict(invariant_id, invariant_version, result, oracle_version)` is optional input. Oracle evidence is never proof (ADR-010, C-54): `PromotionPolicy` refuses to be constructed with `accept_oracle_for_unknown=True`; the field exists so that the refusal is explicit and testable. Primary PASS (or a carried-forward proof) with oracle FAIL: a conflict is recorded, the check is not treated as proven, and the decision is `policy.conflict_decision` (REJECT or ESCALATE, default ESCALATE, never PROMOTE) with reason `EVIDENCE_CONFLICT`. Primary FAIL with oracle PASS: the FAIL stays blocking (REJECT). Primary UNKNOWN with oracle PASS: the UNKNOWN stays non-success; no oracle acceptance. Agreement changes nothing. The conflict is listed in `blocking_conditions`. An oracle FAIL for a carried-forward invariant is treated as a conflict too (the oracle sees a violation that nobody re-verified). | Proposed (P6a) | | C-161 | P6a: emergency switch and decision completeness | `policy.automatic_enabled` False turns any would-be PROMOTE into **ESCALATE** with reason `AUTOMATIC_PROMOTION_DISABLED`; non-PROMOTE decisions are unchanged (Doc 14 §37). The audit record keeps what the decision would have been (`would_have_been` in `blocking_conditions`). Before a decision is returned, **decision completeness** (Doc 11 §43) is evaluated on the finished decision: candidate binding valid; parent binding valid (`parent_state_id` equals `candidate.parent_state_id`, DATA-INT-003); every `supporting_results` id exists in the verification report; the report's `candidate_hash` equals the candidate's `state_hash` and its content hash recomputes; the impact report's content hash recomputes; `policy_version` recorded. A PROMOTE that fails completeness becomes ESCALATE `DECISION_INCOMPLETE`; a non-PROMOTE keeps its decision and records the incompleteness. A PROMOTE lists in `supporting_results` **every** verification result id used, and in `PromotionEvidence.verification_refs` the same ids (Doc 11 §26). | Proposed (P6a) | diff --git a/tests/promotion_builders.py b/tests/promotion_builders.py index 9b5b882..76dc8af 100644 --- a/tests/promotion_builders.py +++ b/tests/promotion_builders.py @@ -128,7 +128,7 @@ def record( result: VerificationResult = PASS, *, definition: Invariant | None = None, - level: str = "L1", + level: str | None = None, verifier: tuple[str, str] | None = None, candidate_hash: str | None = None, error_type: str = "RuntimeError", @@ -136,7 +136,8 @@ def record( n: int = 0, ) -> VerificationResultRecord: """One result for ``target_id`` (an invariant, a gate item or a resource), by default a fresh - L1 result of the verifier the definition names.""" + result of the verifier the definition names: L1, as the verification engine gives for an + invariant and a baseline item, and L0 for the two gate items, as it does.""" assert candidate.state_hash is not None if target_id.startswith("INVARIANT:"): assert definition is not None @@ -174,7 +175,7 @@ def record( invariant_version=version, verifier_id=chosen[0], verifier_version=chosen[1], - evidence_level=level, + evidence_level=level or ("L0" if target_id in GATES else "L1"), verification_class=klass, result=result, reason=chosen_reason, diff --git a/tests/promotion_pipeline.py b/tests/promotion_pipeline.py new file mode 100644 index 0000000..1c10594 --- /dev/null +++ b/tests/promotion_pipeline.py @@ -0,0 +1,266 @@ +"""The whole pipeline, from a fixture directory to a promotion decision (P6a step 6). Not a test +module. + +Normalise the parent and the candidate directory, identity, graphs, impact with the prior proofs +of the trusted state, the verification scope policy, the verification engine, then ``decide``. +Tests may import every package; the pipeline modules are P3 to P5, ``decide`` is P6a. + +The trusted state is built from the parent directory: its invariant statuses are those of the +parent's own ``expected.json`` (PASS is PROTECTED, FAIL is VIOLATED, anything else UNCERTAIN), which +is hand-written data (C-89). Nothing here computes an expected decision. +""" + +from __future__ import annotations + +import json +from collections.abc import Mapping +from dataclasses import dataclass +from typing import Any + +from core.application.scope_policy import DailScopePolicy +from core.dependency.build import build_graph +from core.dependency.invariants import SemanticBinding +from core.domain.enums import CandidateStatus, InvariantStatus +from core.domain.impact import ImpactReport, WorkTargetType +from core.domain.invariant import Invariant, InvariantProof +from core.domain.promotion import DecisionOutcome, PromotionPolicy +from core.domain.state import ( + CandidateState, + TrustedState, + finish_building, + start_building, + transition_candidate, +) +from core.domain.verification import ConstructionStatus, VerificationReport +from core.identity.engine import compare +from core.impact.engine import compute_impact +from core.impact.inputs import PriorProof +from core.promotion.decide import decide +from core.promotion.policy import dail_policy, stateful_full_policy +from core.terraform_model.normalization import normalize_directory +from core.terraform_model.normalize import NORMALIZATION_VERSION +from core.verification.dispatch import DEFAULT_VERIFIERS, REACHABILITY_CFG, VerifierTable +from core.verification.engine import run_work_set +from core.verification.inputs import VerificationInputs +from tests import fixture_catalog as fc +from tests.domain_builders import LINEAGE, patch_for, uid +from tests.identity_builders import NOW +from tests.impact_builders import registry +from tests.pipeline_builders import ( + CANDIDATE_STATE, + PARENT_STATE, + counting_ids, + fixed_clock, + invariant_item, +) + +ROOT = fc.REPO_ROOT +INVARIANTS = ("INV-FUNC-001", "INV-SEC-001", "INV-SEC-002", "INV-SEC-003") +_STATUS = {"PASS": InvariantStatus.PROTECTED, "FAIL": InvariantStatus.VIOLATED} + + +@dataclass(frozen=True) +class PipelineRun: + fixture_id: str + trusted: TrustedState + candidate: CandidateState + inputs: VerificationInputs + impact: ImpactReport + verification: VerificationReport + definitions: tuple[Invariant, ...] + work: tuple[str, ...] + parent: str + + def policy( + self, *, stateful_full: bool = False, automatic_enabled: bool = True, **options: Any + ) -> PromotionPolicy: + make = stateful_full_policy if stateful_full else dail_policy + return make( + policy_version="policy-p6a", + invariants=self.definitions, + automatic_enabled=automatic_enabled, + **options, + ) + + def newer_trusted(self) -> TrustedState: + """Another state of the same lineage with the same content, as if it had been promoted + after this candidate was made (Doc 09 §25): this candidate is then stale.""" + return trusted_from( + self.parent, self.trusted.resources, list(self.definitions), state_id=uid(403) + ) + + def decide( + self, + policy: PromotionPolicy | None = None, + *, + trusted: TrustedState | None = None, + attempt_number: int = 1, + ) -> DecisionOutcome: + return decide( + self.candidate, + trusted or self.trusted, + self.impact, + self.verification, + policy or self.policy(), + decision_id=uid(9300), + now=NOW, + attempt_number=attempt_number, + ) + + +def parent_statuses(parent: str) -> dict[str, InvariantStatus]: + """The invariant statuses of the parent directory's own ``expected.json``.""" + data = json.loads((ROOT / parent / "expected.json").read_text(encoding="utf-8")) + results: Mapping[str, Mapping[str, Any]] = data["results"] + return {i: _STATUS.get(results[i]["result"], InvariantStatus.UNCERTAIN) for i in results} + + +def trusted_from( + parent: str, resources: Any, definitions: list[Invariant], *, state_id: str = PARENT_STATE +) -> TrustedState: + statuses = parent_statuses(parent) + proofs = [ + InvariantProof.for_baseline( + invariant_id=d.invariant_id, + invariant_version=d.version, + status=statuses[d.invariant_id], + evidence_ids=(uid(2100 + n),), + verified_at=NOW, + ) + for n, d in enumerate(definitions) + ] + return TrustedState.establish_baseline( + lineage_id=LINEAGE, + resources=resources, + 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, + now=NOW, + state_id=state_id, + ) + + +def pipeline( + fixture: fc.Fixture, + *, + stateful_full: bool = False, + verifiers: VerifierTable = DEFAULT_VERIFIERS, +) -> PipelineRun: + """Everything up to the verification report for one fixture that has a parent.""" + data = fixture.data + parent = data["parent"] + assert parent is not None, data["fixture_id"] + binding = data["bindings"]["INV-FUNC-001"] + source, destination = binding["S"], binding["D"] + 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()) + semantic = [SemanticBinding("INV-FUNC-001", source, destination, "TCP", 5432)] + trusted = trusted_from(parent, before.resources, definitions) + identity = compare( + before.resources, + after.resources, + list(after.moves), + parent_state_id=PARENT_STATE, + candidate_id=CANDIDATE_STATE, + now=NOW, + ) + trusted_graph = build_graph( + before.resources, definitions, semantic, state_id=PARENT_STATE, now=NOW + ) + candidate_graph = build_graph( + after.resources, definitions, semantic, state_id=CANDIDATE_STATE, now=NOW + ) + priors = [ + PriorProof( + ref.invariant_id, + ref.invariant_version, + ref.evidence_ids, + next(d for d in definitions if d.invariant_id == ref.invariant_id).verifier_id, + next(d for d in definitions if d.invariant_id == ref.invariant_id).verifier_version, + ) + for ref in trusted.invariant_refs + ] + impact = compute_impact( + before.resources, + after.resources, + identity, + trusted_graph, + candidate_graph, + definitions, + priors, + parent_state_id=PARENT_STATE, + candidate_id=CANDIDATE_STATE, + now=NOW, + ) + inputs = VerificationInputs( + candidate_resources=after.resources, + parent_resources=before.resources, + candidate_state_hash=after.resource_set_hash, + normalization_version=NORMALIZATION_VERSION, + candidate_id=CANDIDATE_STATE, + parent_state_id=PARENT_STATE, + identity=identity, + impact=impact, + candidate_graph=candidate_graph, + trusted_graph=trusted_graph, + invariants=tuple(definitions), + construction=ConstructionStatus.OK, + ) + candidate = CandidateState.create( + parent=trusted, + patch=patch_for(trusted, n=7), + candidate_sequence=1, + now=NOW, + candidate_id=CANDIDATE_STATE, + ) + candidate = finish_building(start_building(candidate), after.resources) + candidate = transition_candidate(candidate, CandidateStatus.ANALYZING) + assert candidate.state_hash == after.resource_set_hash + if stateful_full: # Doc 13: every invariant is verified again, plus the created resources + work = [invariant_item(i) for i in INVARIANTS] + [ + w for w in impact.verification_work if w.target_type is WorkTargetType.RESOURCE + ] + else: + work = list(DailScopePolicy().select(impact, definitions)) + report = run_work_set( + work, inputs, clock=fixed_clock(), ids=counting_ids(), verifiers=verifiers + ) + return PipelineRun( + data["fixture_id"], + trusted, + candidate, + inputs, + impact, + report, + tuple(definitions), + tuple(sorted(w.target_id for w in work)), + parent, + ) + + +def failing_reachability(_definition: Invariant, _inputs: VerificationInputs) -> Any: + raise RuntimeError("the reachability verifier crashed") + + +def with_failing_reachability() -> VerifierTable: + """The default verifier table with a reachability verifier that raises (Doc 12 §19).""" + return {**DEFAULT_VERIFIERS, REACHABILITY_CFG: failing_reachability} + + +def fixtures_with_a_parent() -> dict[str, fc.Fixture]: + found = {fx.data["fixture_id"]: fx for fx in fc.load_all().values()} + return {k: v for k, v in sorted(found.items()) if v.data["parent"] is not None} + + +__all__ = [ + "PipelineRun", + "failing_reachability", + "fixtures_with_a_parent", + "parent_statuses", + "pipeline", + "trusted_from", + "with_failing_reachability", +] diff --git a/tests/unit/test_promotion_decide.py b/tests/unit/test_promotion_decide.py index 4241c01..4c47ae5 100644 --- a/tests/unit/test_promotion_decide.py +++ b/tests/unit/test_promotion_decide.py @@ -369,6 +369,20 @@ def test_a_result_below_the_minimum_evidence_level_is_not_proof(self) -> None: out = self.with_record(level="L0") self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_NOT_SUFFICIENT)) + def test_the_gate_items_are_l0_evidence_and_still_proof(self) -> None: + # the verification engine gives the structural and consistency items level L0 + world = make_world() + self.assertEqual(world.records["STRUCTURAL"].evidence_level, "L0") + self.assertEqual(world.records["CONSISTENCY"].evidence_level, "L0") + self.assertEqual(decided(run(world)), (D.PROMOTE, R.ALL_REQUIRED_PROVEN)) + + def test_a_baseline_item_below_the_minimum_level_is_not_proof(self) -> None: + world = make_world() + low = record(world.candidate, BASELINE_ITEM, PASS, level="L0", n=44) + out = run(make_world(results={BASELINE_ITEM: low})) + self.assertEqual(decided(out), (D.REJECT, R.EVIDENCE_NOT_SUFFICIENT)) + self.assertEqual([c.target for c in out.decision.blocking_conditions], [BASELINE_ITEM]) + def test_the_minimum_level_is_the_policys(self) -> None: world = make_world() low = record( diff --git a/tests/unit/test_promotion_fixtures.py b/tests/unit/test_promotion_fixtures.py new file mode 100644 index 0000000..b1fc91b --- /dev/null +++ b/tests/unit/test_promotion_fixtures.py @@ -0,0 +1,299 @@ +"""``decide`` on the real pipeline and the fixtures (P6a step 6; Doc 12 §5-§7, Doc 09 §33-§34, +Doc 06 §25-§26; C-22, C-45, C-159). + +The trusted state ``v0`` is built from the parent fixture directory with the statuses of the +parent's own hand-written ``expected.json`` (C-89). Then the real pipeline runs: normalisation, identity, +graphs, impact with the prior proofs, the DAIL scope policy, the verification engine, ``decide``. + +HAND EXPECTATIONS (written before the first run, from the canonical scenario of CLAUDE.md and the +``expected.json`` of the three canonical fixtures): + +* ``canonical_regression/baseline`` is v0: INV-SEC-001 FAIL (public SSH open), INV-SEC-002, + INV-SEC-003 and INV-FUNC-001 PASS, so v0 has SEC-001 VIOLATED and the other three PROTECTED. +* ``patch_safe`` (fixes SSH, keeps the path): all four invariants PASS, the declared remediation + target INV-SEC-001 is met, ``decision.allowed`` is PROMOTE. A VIOLATED invariant cannot be carried + forward, so INV-SEC-001 is VERIFIED; the proof source of each other invariant follows the engine's + own impact report: VERIFIED if the candidate affects it, CARRIED_FORWARD if it is unaffected and + its evidence eligible. +* ``patch_regression`` (fixes SSH, removes the path): INV-FUNC-001 FAIL, ``decision.allowed`` is + REJECT, and the blocking condition is the failed functional check. +* With the Stateful-Full policy (C-22) and every invariant verified again, ``patch_safe`` promotes + with nothing carried forward; the regression is still rejected. +* After a REJECT, v0 is still the current state and the next attempt starts from it (Doc 06 §25). + +For the other fixtures the reviewer's ``decision.allowed`` is the cross-check: the decision must be +one of them. Where a fixture does not fit, the test says so rather than bend. +""" + +from __future__ import annotations + +import json +import os +import subprocess +import sys +import unittest +from functools import cache + +from core.domain.enums import CandidateStatus, DecisionType, InvariantStatus +from core.domain.promotion import DecisionOutcome, DecisionReason, ProofSource +from core.promotion.decide import completeness_problems +from core.promotion.lifecycle import candidate_after +from tests import fixture_catalog as fc +from tests.promotion_pipeline import ( + PipelineRun, + fixtures_with_a_parent, + pipeline, + with_failing_reachability, +) + +D, R = DecisionType, DecisionReason +SAFE = "canonical_safe_repair_promote_v1" +REGRESSION = "canonical_security_repair_breaks_function_reject_v1" +FUNC, SEC1 = "INV-FUNC-001", "INV-SEC-001" + + +@cache +def run_of(fixture_id: str, *, stateful_full: bool = False, fault: bool = False) -> PipelineRun: + fixture = fixtures_with_a_parent()[fixture_id] + verifiers = with_failing_reachability() if fault else None + if verifiers is None: + return pipeline(fixture, stateful_full=stateful_full) + return pipeline(fixture, stateful_full=stateful_full, verifiers=verifiers) + + +def sources(outcome: DecisionOutcome) -> dict[str, ProofSource]: + return {e.invariant_id: e.source for e in outcome.proof_plan} + + +class TestCanonicalTransitions(unittest.TestCase): + def test_v0_has_public_ssh_open_and_the_database_path_protected(self) -> None: + statuses = {r.invariant_id: r.status for r in run_of(SAFE).trusted.invariant_refs} + self.assertEqual( + statuses, + { + "INV-FUNC-001": InvariantStatus.PROTECTED, + "INV-SEC-001": InvariantStatus.VIOLATED, + "INV-SEC-002": InvariantStatus.PROTECTED, + "INV-SEC-003": InvariantStatus.PROTECTED, + }, + ) + + def test_the_safe_repair_is_promoted(self) -> None: + run = run_of(SAFE) + outcome = run.decide() + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), (D.PROMOTE, R.ALL_REQUIRED_PROVEN) + ) + self.assertEqual(outcome.decision.blocking_conditions, ()) + + def test_the_ssh_repair_is_verified_and_the_rest_follow_the_engines_impact_report(self) -> None: + run = run_of(SAFE) + got = sources(run.decide()) + self.assertEqual(got[SEC1], ProofSource.VERIFIED) # its reference is VIOLATED + impact = run.impact + for ref in run.trusted.invariant_refs: + key = (ref.invariant_id, ref.invariant_version) + with self.subTest(invariant=ref.invariant_id): + if impact.affected_for(*key) is not None: + self.assertEqual(got[ref.invariant_id], ProofSource.VERIFIED) + else: + self.assertTrue( + impact.carry_forward_ok( + *key, + candidate_id=run.candidate.candidate_id, + parent_state_id=run.trusted.state_id, + ) + ) + self.assertEqual(ref.status, InvariantStatus.PROTECTED) + self.assertEqual(got[ref.invariant_id], ProofSource.CARRIED_FORWARD) + + def test_at_least_one_invariant_is_carried_and_at_least_one_is_verified(self) -> None: + # the point of DAIL: the canonical repair re-verifies less than everything + got = sources(run_of(SAFE).decide()) + self.assertIn(ProofSource.CARRIED_FORWARD, got.values()) + self.assertIn(ProofSource.VERIFIED, got.values()) + + def test_the_repair_that_breaks_the_database_path_is_rejected(self) -> None: + outcome = run_of(REGRESSION).decide() + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), + (D.REJECT, R.REQUIRED_CHECK_FAILED), + ) + self.assertEqual( + [c.target for c in outcome.decision.blocking_conditions], [f"INVARIANT:{FUNC}:1"] + ) + self.assertNotIn(FUNC, sources(outcome)) + self.assertEqual(sources(outcome)[SEC1], ProofSource.VERIFIED) # SSH is fixed all the same + + def test_with_stateful_full_nothing_is_carried_forward(self) -> None: + run = run_of(SAFE, stateful_full=True) + outcome = run.decide(run.policy(stateful_full=True)) + self.assertEqual(outcome.decision.decision, D.PROMOTE) + self.assertEqual(set(sources(outcome).values()), {ProofSource.VERIFIED}) + self.assertEqual(len(outcome.proof_plan), 4) + + def test_stateful_full_policy_without_the_extra_verification_has_no_proof(self) -> None: + run = run_of(SAFE) # DAIL scope: the unaffected invariant was not verified + outcome = run.decide(run.policy(stateful_full=True)) + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), + (D.REJECT, R.INSUFFICIENT_EVIDENCE), + ) + self.assertNotIn(ProofSource.CARRIED_FORWARD, sources(outcome).values()) + + def test_stateful_full_still_rejects_the_regression(self) -> None: + run = run_of(REGRESSION, stateful_full=True) + outcome = run.decide(run.policy(stateful_full=True)) + self.assertEqual(outcome.decision.decision, D.REJECT) + self.assertEqual(outcome.decision.reason, R.REQUIRED_CHECK_FAILED) + + def test_the_rejection_leaves_v0_current_and_the_next_attempt_starts_from_it(self) -> None: + bad, good = run_of(REGRESSION), run_of(SAFE) + before = (bad.trusted.state_hash, bad.trusted.to_dict()) + rejected = candidate_after(bad.decide().decision, bad.candidate, bad.trusted) + self.assertEqual(rejected.status, CandidateStatus.REJECTED) + self.assertEqual((bad.trusted.state_hash, bad.trusted.to_dict()), before) + # the second attempt has the same parent and is promotable against the unchanged state + self.assertEqual(good.candidate.parent_state_id, bad.candidate.parent_state_id) + self.assertEqual(good.candidate.parent_state_id, bad.trusted.state_id) + second = good.decide() + self.assertEqual(second.decision.decision, D.PROMOTE) + promotable = candidate_after(second.decision, good.candidate, bad.trusted) + self.assertEqual(promotable.status, CandidateStatus.PROMOTABLE) + + +class TestEveryFixtureWithAParent(unittest.TestCase): + """The cross-check against the reviewer's ``decision.allowed`` (hand-written data).""" + + def decision_for(self, fixture_id: str) -> DecisionOutcome: + fixture = fixtures_with_a_parent()[fixture_id] + kind = (fixture.data.get("process") or {}).get("kind") + if kind == "stale_parent": + run = run_of(fixture_id) + return run.decide(trusted=run.newer_trusted()) + if kind == "verifier_fault": + return run_of(fixture_id, fault=True).decide() + return run_of(fixture_id).decide() + + def test_the_decision_is_one_the_reviewer_allows(self) -> None: + for fixture_id, fixture in fixtures_with_a_parent().items(): + with self.subTest(fixture=fixture_id): + outcome = self.decision_for(fixture_id) + self.assertIn(outcome.decision.decision.value, fixture.data["decision"]["allowed"]) + + def test_nothing_is_promoted_unless_every_expected_result_is_pass(self) -> None: + for fixture_id, fixture in fixtures_with_a_parent().items(): + expected = [v["result"] for v in fixture.data["results"].values()] + outcome = self.decision_for(fixture_id) + if any(result != "PASS" for result in expected): + with self.subTest(fixture=fixture_id): + self.assertNotEqual(outcome.decision.decision, D.PROMOTE) + + def test_a_promote_needs_the_proof_of_every_invariant_of_the_state(self) -> None: + for fixture_id in fixtures_with_a_parent(): + outcome = self.decision_for(fixture_id) + if outcome.decision.decision is not D.PROMOTE: + continue + run = run_of(fixture_id) + with self.subTest(fixture=fixture_id): + self.assertEqual( + sorted(sources(outcome)), + sorted(r.invariant_id for r in run.trusted.invariant_refs), + ) + + def test_every_decision_is_complete_and_preserves_what_it_needs(self) -> None: + for fixture_id in fixtures_with_a_parent(): + outcome = self.decision_for(fixture_id) + run = run_of(fixture_id) + decision = outcome.decision + with self.subTest(fixture=fixture_id): + self.assertEqual(decision.candidate_id, run.candidate.candidate_id) + self.assertEqual(decision.parent_state_id, run.candidate.parent_state_id) + if decision.decision is D.PROMOTE: + self.assertTrue(decision.supporting_results) + else: + self.assertTrue(decision.blocking_conditions) + self.assertEqual( + completeness_problems( + run.candidate, + decision.parent_state_id, + decision.supporting_results, + run.impact, + run.verification, + run.policy(), + ), + [], + ) + + def test_the_stale_parent_process_fixture_is_rejected_as_stale(self) -> None: + outcome = self.decision_for("process_stale_parent_reject_v1") + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), (D.REJECT, R.STALE_PARENT) + ) + + def test_the_verifier_error_process_fixture_is_escalated(self) -> None: + outcome = self.decision_for("process_verifier_error_escalate_v1") + self.assertEqual( + (outcome.decision.decision, outcome.decision.reason), (D.ESCALATE, R.VERIFIER_ERROR) + ) + self.assertEqual( + [c.target for c in outcome.decision.blocking_conditions], [f"INVARIANT:{FUNC}:1"] + ) + + def test_each_decision_applies_to_the_candidate_without_touching_the_trusted_state( + self, + ) -> None: + wanted = { + D.PROMOTE: CandidateStatus.PROMOTABLE, + D.REJECT: CandidateStatus.REJECTED, + D.RETRY: CandidateStatus.RETRY_REQUIRED, + D.ESCALATE: CandidateStatus.ESCALATED, + } + for fixture_id in fixtures_with_a_parent(): + outcome = self.decision_for(fixture_id) + run = run_of(fixture_id) + before = run.trusted.state_hash + moved = candidate_after(outcome.decision, run.candidate, run.trusted) + with self.subTest(fixture=fixture_id): + self.assertEqual(moved.status, wanted[outcome.decision.decision]) + self.assertEqual(run.trusted.state_hash, before) + + +class TestDeterminism(unittest.TestCase): + SCRIPT = ( + "import sys, json\n" + "sys.path.insert(0, '.')\n" + "from tests.promotion_pipeline import fixtures_with_a_parent, pipeline\n" + "ids = ['canonical_safe_repair_promote_v1'," + " 'canonical_security_repair_breaks_function_reject_v1', 'sg_private_ssh_pass_v1']\n" + "out = {}\n" + "for fid in ids:\n" + " run = pipeline(fixtures_with_a_parent()[fid])\n" + " d = run.decide()\n" + " out[fid] = [d.decision.content_hash, d.evidence.content_hash," + " [e.source.value for e in d.proof_plan]]\n" + "print(json.dumps(out, sort_keys=True))\n" + ) + + def test_the_decision_does_not_depend_on_the_hash_seed(self) -> None: + answers = set() + for seed in ("0", "1", "424242"): + env = {**os.environ, "PYTHONHASHSEED": seed} + done = subprocess.run( + [sys.executable, "-I", "-c", self.SCRIPT], + capture_output=True, + text=True, + env=env, + cwd=str(fc.REPO_ROOT), + check=False, + ) + self.assertEqual(done.returncode, 0, done.stderr[-600:]) + answers.add(done.stdout.strip()) + self.assertEqual(len(answers), 1) + self.assertEqual( + set(json.loads(answers.pop())), {SAFE, REGRESSION, "sg_private_ssh_pass_v1"} + ) + + +if __name__ == "__main__": + unittest.main() From 2a4cdf91537b04f41e98a1ef60d8a4e2c26a54cb Mon Sep 17 00:00:00 2001 From: Ayushxsingh100 Date: Thu, 29 Oct 2026 13:49:42 +0530 Subject: [PATCH 8/8] =?UTF-8?q?P6a=20step=206b:=20seeded=20properties=20of?= =?UTF-8?q?=20decide=20and=20the=20fault=20cases=20(Doc=2012=20=C2=A717,?= =?UTF-8?q?=20=C2=A719;=20C-45,=20C-158=20to=20C-161)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five seeds, 60 generated worlds each: a required FAIL always rejects, a required non-success never promotes, a PROMOTE has a full proof plan and only supporting results that exist, a stale parent is rejected, nothing affected, uncertain, not PROTECTED or policy-disabled is carried forward (C-45), the emergency switch, the retry budget and an oracle FAIL each stop a PROMOTE, and nothing is mutated. The generator reaches all four decisions and 13 reasons. Every checker is also handed a decision that breaks its rule and must fail. The fault cases (verifier crash, hash mismatch, stale candidate, truncated report, missing STRUCTURAL) each give a known non-PROMOTE decision and leave the trusted state unchanged. Also fixes a line over 100 columns in the fixtures test. Co-Authored-By: Claude Sonnet 5.5 --- tests/promotion_builders.py | 3 + tests/unit/test_promotion_faults.py | 115 +++++++ tests/unit/test_promotion_fixtures.py | 5 +- tests/unit/test_promotion_properties.py | 395 ++++++++++++++++++++++++ 4 files changed, 516 insertions(+), 2 deletions(-) create mode 100644 tests/unit/test_promotion_faults.py create mode 100644 tests/unit/test_promotion_properties.py diff --git a/tests/promotion_builders.py b/tests/promotion_builders.py index 76dc8af..e924466 100644 --- a/tests/promotion_builders.py +++ b/tests/promotion_builders.py @@ -282,6 +282,7 @@ def make_world( affected: Iterable[str] = (SEC1, FUNC1), uncertain: Iterable[str] = (), carry: Iterable[str] | None = None, + ineligible: Iterable[str] = (), statuses: Mapping[str, InvariantStatus] | None = None, registry_version: int = 1, candidate_status: CandidateStatus = CandidateStatus.ANALYZING, @@ -303,12 +304,14 @@ def make_world( if carry is None else tuple(carry) ) + unmatched = tuple(ineligible) impact = impact_for( trusted, candidate, carry=kept, affected=impacted, uncertain=unsure, + ineligible=unmatched, with_baseline_work=with_baseline_work, ) wanted: dict[str, Any] = {g: PASS for g in GATES} diff --git a/tests/unit/test_promotion_faults.py b/tests/unit/test_promotion_faults.py new file mode 100644 index 0000000..1019b8e --- /dev/null +++ b/tests/unit/test_promotion_faults.py @@ -0,0 +1,115 @@ +"""Fault cases of the decision (P6a step 6; Doc 12 §19, Doc 09 §37, Doc 06 §20 and §27). + +Each fault yields a known non-PROMOTE decision and leaves the trusted state unchanged: a verifier +crash is a VERIFIER_ERROR that escalates, a report or an impact report that no longer matches its +hash cannot make a complete decision, a stale candidate is rejected, a truncated report has no proof +for what it lacks, and a missing STRUCTURAL item is missing evidence. +""" + +from __future__ import annotations + +import dataclasses +import unittest + +from core.domain.enums import DecisionType, VerificationResult +from core.domain.promotion import DecisionReason +from core.domain.verification import VerificationReport +from tests.domain_builders import uid +from tests.promotion_builders import ( + FUNC1, + SEC1, + World, + make_world, + report_of, + run, + target, + trusted_state, +) +from tests.promotion_pipeline import fixtures_with_a_parent, pipeline, with_failing_reachability + +D, R = DecisionType, DecisionReason +SAFE = "canonical_safe_repair_promote_v1" + + +def untouched(world: World) -> tuple[str, dict[str, object]]: + return world.trusted.state_hash, world.trusted.to_dict() + + +class TestFaults(unittest.TestCase): + def check(self, world: World, decision: DecisionType, reason: DecisionReason) -> None: + before = untouched(world) + out = run(world) + self.assertEqual((out.decision.decision, out.decision.reason), (decision, reason)) + self.assertEqual(untouched(world), before) + + def test_a_verifier_crash_is_a_verifier_error_that_escalates(self) -> None: + run_ = pipeline(fixtures_with_a_parent()[SAFE], verifiers=with_failing_reachability()) + func = next(r for r in run_.verification.results if r.invariant_id == "INV-FUNC-001") + self.assertEqual(func.result, VerificationResult.VERIFIER_ERROR) + before = run_.trusted.to_dict() + out = run_.decide() + self.assertEqual( + (out.decision.decision, out.decision.reason), (D.ESCALATE, R.VERIFIER_ERROR) + ) + self.assertEqual(run_.trusted.to_dict(), before) + + def test_a_report_that_no_longer_matches_its_hash_cannot_promote(self) -> None: + world = make_world() + object.__setattr__(world.verification, "content_hash", "0" * 64) + self.check(world, D.ESCALATE, R.DECISION_INCOMPLETE) + + def test_an_impact_report_that_no_longer_matches_its_hash_cannot_promote(self) -> None: + world = make_world(affected=(SEC1, FUNC1, "INV-SEC-002", "INV-SEC-003"), carry=()) + object.__setattr__(world.impact, "graph_version", "tampered") + self.check(world, D.ESCALATE, R.DECISION_INCOMPLETE) + + def test_a_candidate_whose_hash_is_not_the_reports_has_no_fresh_proof(self) -> None: + world = make_world() + object.__setattr__(world.candidate, "state_hash", "1" * 64) + out = run(world) + self.assertEqual(out.decision.decision, D.REJECT) + self.assertIn(R.EVIDENCE_STALE, [c.code for c in out.decision.blocking_conditions]) + + def test_a_stale_candidate_is_rejected(self) -> None: + world = dataclasses.replace(make_world(), trusted=trusted_state(state_id=uid(2))) + self.check(world, D.REJECT, R.STALE_PARENT) + + def test_a_truncated_report_has_no_proof_for_what_it_lacks(self) -> None: + world = make_world() + kept = list(world.verification.results)[:2] + truncated = dataclasses.replace(world, verification=report_of(world.candidate, kept)) + before = untouched(truncated) + out = run(truncated) + self.assertEqual( + (out.decision.decision, out.decision.reason), (D.REJECT, R.INSUFFICIENT_EVIDENCE) + ) + self.assertEqual(untouched(truncated), before) + missing = {c.target for c in out.decision.blocking_conditions} + held = {r.target_id for r in kept} + self.assertTrue(missing) + self.assertFalse(missing & held) + + def test_an_empty_report_proves_nothing_that_needs_a_result(self) -> None: + world = make_world() + empty = VerificationReport.create( + candidate_id=world.candidate.candidate_id, + candidate_hash=world.candidate.state_hash or "", + results=[], + verifier_invocations=0, + verifier_set_version="dail-verify-1", + ) + out = run(dataclasses.replace(world, verification=empty)) + self.assertEqual( + (out.decision.decision, out.decision.reason), (D.REJECT, R.INSUFFICIENT_EVIDENCE) + ) + targets = {c.target for c in out.decision.blocking_conditions} + self.assertIn("STRUCTURAL", targets) + self.assertIn("CONSISTENCY", targets) + self.assertIn(target(SEC1), targets) + + def test_a_missing_structural_item_is_missing_evidence(self) -> None: + self.check(make_world(results={"STRUCTURAL": None}), D.REJECT, R.INSUFFICIENT_EVIDENCE) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/unit/test_promotion_fixtures.py b/tests/unit/test_promotion_fixtures.py index b1fc91b..4d916eb 100644 --- a/tests/unit/test_promotion_fixtures.py +++ b/tests/unit/test_promotion_fixtures.py @@ -2,8 +2,9 @@ Doc 06 §25-§26; C-22, C-45, C-159). The trusted state ``v0`` is built from the parent fixture directory with the statuses of the -parent's own hand-written ``expected.json`` (C-89). Then the real pipeline runs: normalisation, identity, -graphs, impact with the prior proofs, the DAIL scope policy, the verification engine, ``decide``. +parent's own hand-written ``expected.json`` (C-89). Then the real pipeline runs: normalisation, +identity, graphs, impact with the prior proofs, the DAIL scope policy, the verification engine, +``decide``. HAND EXPECTATIONS (written before the first run, from the canonical scenario of CLAUDE.md and the ``expected.json`` of the three canonical fixtures): diff --git a/tests/unit/test_promotion_properties.py b/tests/unit/test_promotion_properties.py new file mode 100644 index 0000000..c1f5aa0 --- /dev/null +++ b/tests/unit/test_promotion_properties.py @@ -0,0 +1,395 @@ +"""Properties of ``decide`` over generated worlds (P6a step 6; Doc 12 §17; C-45, C-158 to C-161). + +Seeded ``random`` (standard library), five seeds, 60 worlds each. Every property is stated from the +spec, not from the code: + +* a required FAIL never gives PROMOTE (and gives REJECT); a required UNKNOWN, UNSUPPORTED or + VERIFIER_ERROR never gives PROMOTE; +* PROMOTE implies every required invariant has a proof-plan entry and every supporting result id is + in the verification report; +* a stale parent never gives PROMOTE; +* an affected, uncertain, non-PROTECTED, or policy-disabled invariant never appears with the source + CARRIED_FORWARD (the executable form of C-45); +* the decision does not depend on which item carries which non-success (order independence); +* ``decide`` does not mutate any argument and is deterministic; +* the emergency switch, the retry budget and the oracle conflict each stop a PROMOTE. + +Each property is run by a checker function, and the last class shows that every checker FAILS on a +decision that breaks its rule (a test that cannot fail proves nothing). +""" + +from __future__ import annotations + +import dataclasses +import itertools +import random +import unittest +from collections.abc import Callable +from typing import Any + +from core.domain.enums import DecisionType, InvariantStatus, VerificationResult +from core.domain.promotion import ( + DecisionOutcome, + DecisionReason, + OracleVerdict, + ProofSource, +) +from tests.domain_builders import uid +from tests.promotion_builders import ( + ALL, + BASELINE_ITEM, + ERROR, + FAIL, + GATES, + PASS, + SEC1, + UNKNOWN, + UNSUPPORTED, + World, + make_world, + run, + target, + trusted_state, +) + +D, R = DecisionType, DecisionReason +SEEDS = (20261029, 1, 7, 424242, 99991) +WORLDS = 60 +NON_SUCCESS = (UNKNOWN, UNSUPPORTED, ERROR) +RESULT_CHOICES: list[VerificationResult | None] = [PASS] * 8 + [ + FAIL, + UNKNOWN, + UNSUPPORTED, + ERROR, + None, +] +STATUS_CHOICES = ( + InvariantStatus.PROTECTED, + InvariantStatus.PROTECTED, + InvariantStatus.VIOLATED, + InvariantStatus.UNCERTAIN, +) +REQUIRED_TARGETS = (*GATES, *(target(i) for i in ALL), BASELINE_ITEM) + + +@dataclasses.dataclass +class Case: + world: World + results: dict[str, VerificationResult | None] + roles: dict[str, str] + statuses: dict[str, InvariantStatus] + attempt: int + oracle: list[OracleVerdict] + stale: bool + + +def random_case(rng: random.Random) -> Case: + friendly = rng.random() < 0.5 # half the worlds start from a promotable one and are spoiled + statuses = {i: rng.choice(STATUS_CHOICES) for i in ALL} + roles = { + i: rng.choice(["affected", "affected", "uncertain", "carry", "carry", "ineligible", "none"]) + for i in ALL + } + if friendly: + roles = {i: rng.choice(["affected", "carry"]) for i in ALL} + statuses = { + i: InvariantStatus.PROTECTED if roles[i] == "carry" else rng.choice(STATUS_CHOICES) + for i in ALL + } + + def pick(role: str) -> list[str]: + return [i for i in ALL if roles[i] == role] + + owed = [*GATES, BASELINE_ITEM, *(target(i) for i in pick("affected") + pick("uncertain"))] + results: dict[str, VerificationResult | None] = {} + for tid in (*owed, *(target(i) for i in ALL if rng.random() < 0.25)): + results[tid] = PASS if friendly and rng.random() < 0.93 else rng.choice(RESULT_CHOICES) + if friendly and rng.random() < 0.4: # exactly one thing is wrong + for tid in owed: + results[tid] = PASS + results[rng.choice(owed)] = rng.choice([FAIL, UNKNOWN, UNSUPPORTED, ERROR, None]) + world = make_world( + results=results, # type: ignore[arg-type] + affected=pick("affected"), + uncertain=pick("uncertain"), + carry=pick("carry"), + ineligible=pick("ineligible"), + statuses=statuses, + automatic_enabled=rng.random() < 0.9, + ).with_policy( + carry_forward_enabled=rng.random() < 0.9, + max_attempts=rng.randint(2, 6), + conflict_decision=rng.choice([D.REJECT, D.ESCALATE]), + ) + stale = rng.random() < 0.08 + if stale: + world = dataclasses.replace(world, trusted=trusted_state(statuses, state_id=uid(2))) + verdicts = [ + OracleVerdict(i, 1, rng.choice([PASS, FAIL]), "oracle-1") for i in ALL if rng.random() < 0.1 + ] + return Case(world, results, roles, statuses, rng.randint(1, 5), verdicts, stale) + + +def cases() -> list[tuple[int, Case]]: + return [ + (seed, random_case(random.Random(seed * 1000 + n))) for seed in SEEDS for n in range(WORLDS) + ] + + +def decide_case(case: Case) -> DecisionOutcome: + return run(case.world, attempt_number=case.attempt, oracle=case.oracle) + + +# --- the checkers: each returns the list of ways a decision breaks one rule ----------------------- + + +def check_fail_rejects(case: Case, out: DecisionOutcome) -> list[str]: + fails = [t for t in REQUIRED_TARGETS if case.results.get(t) is FAIL] + if fails and out.decision.decision is not D.REJECT: + return [f"a required FAIL on {fails[0]} gave {out.decision.decision.value}"] + return [] + + +def check_non_success_never_promotes(case: Case, out: DecisionOutcome) -> list[str]: + bad = [t for t in REQUIRED_TARGETS if case.results.get(t) in NON_SUCCESS] + if bad and out.decision.decision is D.PROMOTE: + return [f"a required non-success on {bad[0]} gave PROMOTE"] + return [] + + +def check_promote_has_full_proof(case: Case, out: DecisionOutcome) -> list[str]: + if out.decision.decision is not D.PROMOTE: + return [] + problems = [] + planned = {e.invariant_id for e in out.proof_plan} + required = {r.invariant_id for r in case.world.trusted.invariant_refs} + if planned != required: + problems.append(f"plan {sorted(planned)} is not the required set {sorted(required)}") + report_ids = {r.verification_id for r in case.world.verification.results} + if ( + not set(out.decision.supporting_results) <= report_ids + or not out.decision.supporting_results + ): + problems.append("a supporting result is not in the report, or there is none") + if out.decision.blocking_conditions: + problems.append("a PROMOTE with blocking conditions") + if any(c.source is None for c in out.decision.required_checks): + problems.append("a PROMOTE with an unproven required check") + return problems + + +def check_stale_never_promotes(case: Case, out: DecisionOutcome) -> list[str]: + if case.stale and (out.decision.decision, out.decision.reason) != (D.REJECT, R.STALE_PARENT): + return [f"a stale parent gave {out.decision.decision.value} {out.decision.reason.value}"] + return [] + + +def check_c45(case: Case, out: DecisionOutcome) -> list[str]: + problems = [] + for entry in out.proof_plan: + if entry.source is not ProofSource.CARRIED_FORWARD: + continue + role = case.roles[entry.invariant_id] + if role in ("affected", "uncertain"): + problems.append(f"{entry.invariant_id} was {role} but carried forward") + if case.statuses[entry.invariant_id] is not InvariantStatus.PROTECTED: + problems.append(f"{entry.invariant_id} was not PROTECTED but carried forward") + if role in ("ineligible", "none"): + problems.append(f"{entry.invariant_id} had no eligible evidence but was carried") + if not case.world.policy.carry_forward_enabled: + problems.append("the policy disables carry-forward but a proof was carried") + return problems + + +def check_switch_budget_conflict(case: Case, out: DecisionOutcome) -> list[str]: + problems = [] + if out.decision.decision is D.PROMOTE: + if not case.world.policy.automatic_enabled: + problems.append("PROMOTE with the emergency switch off") + proven = {(e.invariant_id, 1) for e in out.proof_plan} + for verdict in case.oracle: + if ( + verdict.result is FAIL + and (verdict.invariant_id, verdict.invariant_version) in proven + ): + problems.append(f"PROMOTE although the oracle failed {verdict.invariant_id}") + if out.decision.decision is D.RETRY and case.attempt >= case.world.policy.max_attempts: + problems.append("a RETRY at or beyond the retry budget") + return problems + + +CHECKERS: dict[str, Callable[[Case, DecisionOutcome], list[str]]] = { + "a required FAIL rejects": check_fail_rejects, + "a non-success never promotes": check_non_success_never_promotes, + "a PROMOTE has full proof": check_promote_has_full_proof, + "a stale parent is rejected": check_stale_never_promotes, + "C-45: nothing affected is carried": check_c45, + "switch, budget and oracle conflict stop a PROMOTE": check_switch_budget_conflict, +} + + +class TestProperties(unittest.TestCase): + def test_each_property_holds_over_the_generated_worlds(self) -> None: + sample = cases() + seen: set[tuple[DecisionType, DecisionReason]] = set() + for name, checker in CHECKERS.items(): + with self.subTest(property=name): + for seed, case in sample: + out = decide_case(case) + seen.add((out.decision.decision, out.decision.reason)) + self.assertEqual(checker(case, out), [], f"seed {seed}") + # the generator reaches every kind of decision, or the properties would be vacuous + decisions = {d for d, _ in seen} + self.assertEqual(decisions, set(DecisionType)) + self.assertGreaterEqual(len(seen), 8) + + def test_a_good_share_of_the_worlds_are_promoted_and_carry_something(self) -> None: + promoted = carried = 0 + for _, case in cases(): + out = decide_case(case) + if out.decision.decision is D.PROMOTE: + promoted += 1 + carried += any(e.source is ProofSource.CARRIED_FORWARD for e in out.proof_plan) + self.assertGreater(promoted, 10) + self.assertGreater(carried, 3) + + def test_the_decision_does_not_change_any_argument_and_is_deterministic(self) -> None: + for seed, case in cases()[::7]: + w = case.world + before = ( + w.candidate.to_dict(), + w.trusted.to_dict(), + w.impact.to_dict(), + w.verification.to_dict(), + w.policy, + list(case.oracle), + ) + first = decide_case(case) + second = decide_case(case) + after = ( + w.candidate.to_dict(), + w.trusted.to_dict(), + w.impact.to_dict(), + w.verification.to_dict(), + w.policy, + list(case.oracle), + ) + self.assertEqual(before, after, f"seed {seed}") + self.assertEqual(first, second, f"seed {seed}") + + def test_the_decision_does_not_depend_on_the_order_of_the_oracle_verdicts(self) -> None: + rng = random.Random(SEEDS[0]) + for _, case in cases()[::5]: + if len(case.oracle) < 2: + continue + want = decide_case(case) + shuffled = case.oracle[:] + rng.shuffle(shuffled) + got = run(case.world, attempt_number=case.attempt, oracle=shuffled) + self.assertEqual(got, want) + + +class TestOrderIndependence(unittest.TestCase): + """The decision depends on the classes of the conditions, not on which item carries which.""" + + def decision(self, assignment: dict[str, VerificationResult]) -> tuple[Any, Any]: + out = run(make_world(results=assignment)) # type: ignore[arg-type] + return out.decision.decision, out.decision.reason + + def test_swapping_two_results_between_two_items_changes_nothing(self) -> None: + items = ("STRUCTURAL", "CONSISTENCY", target("INV-FUNC-001"), target(SEC1), BASELINE_ITEM) + results = (FAIL, UNKNOWN, UNSUPPORTED, ERROR) + for first, second in itertools.combinations(items, 2): + for a, b in itertools.permutations(results, 2): + with self.subTest(first=first, second=second, a=a.value, b=b.value): + one = self.decision({first: a, second: b}) + other = self.decision({first: b, second: a}) + self.assertEqual(one[0], other[0]) + # the reason may differ only where an item is a gate (each gate FAIL has its + # own code); for two items that are not gates it is equal + if first not in GATES and second not in GATES: + self.assertEqual(one, other) + + def test_a_fail_is_never_hidden_by_any_other_non_success_at_any_position(self) -> None: + items = ("STRUCTURAL", "CONSISTENCY", target("INV-FUNC-001"), target(SEC1), BASELINE_ITEM) + for failing, other in itertools.permutations(items, 2): + for non_success in NON_SUCCESS: + with self.subTest(failing=failing, other=other, non_success=non_success.value): + got = self.decision({failing: FAIL, other: non_success}) + self.assertEqual(got[0], D.REJECT) + + +class TestTheCheckersCanFail(unittest.TestCase): + """A property that cannot fail proves nothing: hand each checker a decision that breaks it.""" + + def case_and_out(self, **kw: Any) -> tuple[Case, DecisionOutcome]: + world = make_world(**kw) + case = Case( + world, + {t: PASS for t in REQUIRED_TARGETS}, + {i: "affected" if i in (SEC1, "INV-FUNC-001") else "carry" for i in ALL}, + {i: InvariantStatus.PROTECTED for i in ALL}, + 1, + [], + False, + ) + return case, run(world) + + def test_a_promote_that_ignores_a_fail_is_caught(self) -> None: + case, out = self.case_and_out() + self.assertEqual(out.decision.decision, D.PROMOTE) + case.results[target(SEC1)] = ( + FAIL # pretend the report said FAIL while the decision promoted + ) + self.assertTrue(check_fail_rejects(case, out)) + + def test_a_promote_that_ignores_a_non_success_is_caught(self) -> None: + case, out = self.case_and_out() + case.results[BASELINE_ITEM] = UNKNOWN + self.assertTrue(check_non_success_never_promotes(case, out)) + + def test_a_promote_without_a_full_plan_is_caught(self) -> None: + case, out = self.case_and_out() + thin = dataclasses.replace(out, proof_plan=out.proof_plan[:-1]) + self.assertTrue(check_promote_has_full_proof(case, thin)) + + def test_a_promote_for_a_stale_parent_is_caught(self) -> None: + case, out = self.case_and_out() + case.stale = True + self.assertTrue(check_stale_never_promotes(case, out)) + + def test_a_carried_affected_invariant_is_caught(self) -> None: + case, out = self.case_and_out() + carried = next(e for e in out.proof_plan if e.source is ProofSource.CARRIED_FORWARD) + case.roles[carried.invariant_id] = "affected" + self.assertTrue(check_c45(case, out)) + case.roles[carried.invariant_id] = "carry" + case.statuses[carried.invariant_id] = InvariantStatus.VIOLATED + self.assertTrue(check_c45(case, out)) + case.statuses[carried.invariant_id] = InvariantStatus.PROTECTED + case.world = case.world.with_policy(carry_forward_enabled=False) + self.assertTrue(check_c45(case, out)) + + def test_a_promote_with_the_switch_off_is_caught(self) -> None: + case, out = self.case_and_out() + case.world = case.world.with_policy(automatic_enabled=False) + self.assertTrue(check_switch_budget_conflict(case, out)) + + def test_a_promote_against_an_oracle_fail_is_caught(self) -> None: + case, out = self.case_and_out() + case.oracle = [OracleVerdict("INV-FUNC-001", 1, FAIL, "oracle-1")] + self.assertTrue(check_switch_budget_conflict(case, out)) + + def test_a_retry_beyond_the_budget_is_caught(self) -> None: + case, _ = self.case_and_out() + case.world = case.world.with_policy(max_attempts=2) + retry = run( + make_world(results={target("INV-FUNC-001"): UNKNOWN}).with_policy(max_attempts=9) + ) + self.assertEqual(retry.decision.decision, D.RETRY) + case.attempt = 2 + self.assertTrue(check_switch_budget_conflict(case, retry)) + + +if __name__ == "__main__": + unittest.main()