diff --git a/demos/proof_carrying_promotion/.gitignore b/demos/proof_carrying_promotion/.gitignore new file mode 100644 index 00000000..89f9ac04 --- /dev/null +++ b/demos/proof_carrying_promotion/.gitignore @@ -0,0 +1 @@ +out/ diff --git a/demos/proof_carrying_promotion/README.md b/demos/proof_carrying_promotion/README.md new file mode 100644 index 00000000..b7c1cf3f --- /dev/null +++ b/demos/proof_carrying_promotion/README.md @@ -0,0 +1,108 @@ +# Proof-Carrying Coherence Promotion Demo (ADR-0218) + +This demo proves one narrow boundary: + +```text +A model-style proposer submits a claim, a proof candidate, and +status/confidence garbage. +CORE ignores proposer authority entirely. +CORE fresh-reads curator-certified store state. +CORE recomputes the proof under the pinned deductive engine. +CORE promotes or refuses only through vault-owned certified promotion. +The trace proves the decision. +``` + +## Public proof spine + +```text +proposer proposes +store state grounds +engine recomputes +vault owns the flip +trace proves +``` + +## What this proves + +* A `SPECULATIVE` claim becomes `COHERENT` **iff** it is deductively entailed + by an already-`COHERENT`, curator-certified premise set — decided by the + REAL ratified promoter ([`teaching/proof_promotion.py`](../../teaching/proof_promotion.py)), + not a demo-local reimplementation. +* The only mutation site is + [`VaultStore.apply_certified_promotion`](../../vault/store.py), which + independently replay-verifies the certificate under the pinned engine + (`generate/proof_chain/engine_pin.py`) and fresh-reads live store state + before flipping anything. This demo adds **no** vault writer and **no** + status-transition site: the local arena is reconstructed via the + persistence path (`VaultStore.from_dict`), and INV-21 / INV-29 scan this + directory. +* Proposer-attached `proof` / `status` / `confidence` / `certificate` / + `trace_hash` are data, never authority: the whole proposer block is handed + to `certify_promotion` as `proposer_payload`, which deletes it unread + (ADR-0218 §D3.5). The artifact records the ignored field names; the tests + prove the decision and the certificate digest are byte-identical with and + without the garbage. +* A tampered certificate fails byte-for-byte replay re-verification and + mutates nothing. A certificate built from a stale store state (a premise + re-stated `contested` after certification) is refused by the vault's + live fresh-read — the same honest certificate, the same digest, a + different live world, no flip. +* Invalid payloads (attempts to smuggle `promoted`, `final_status`, + `authority_path`, `certificate_digest`, `trace_hash`, `evidence_ledger`, + …) are rejected by the closed schema *before* any evaluation runs: + `authority_evaluated: false`, `certificate_digest: null`, no arena is even + built. +* Every output embeds the certificate's SHA-256 digest and the engine pin, + and the response `trace_hash` is computed over the whole body — the + certificate digest therefore folds into the trace hash. + +## Honesty ledger — what this does NOT prove + +* This demo proves **local deterministic proof-carrying promotion in the + demo envelope** — fixed fixtures, a throwaway local store arena, a small + propositional regime. Nothing more. +* Promotion is from `SPECULATIVE` to `COHERENT` **only**. No other + transition is performed or claimed. +* Promotion requires, jointly: live store state, curator-certified readings + (`reading_certified: true` + the certified form), all-`COHERENT` premises, + pinned replay verification, and vault-owned mutation. Remove any one and + the demo refuses. +* Proposer confidence / status / proof is **not** authority — and saying so + here is backed by tests, not by trust. +* This does **not** prove autonomous open-world learning. The premises and + readings are curator-declared fixture data; the reading (NL→proposition) + step remains the human-certified hazard surface (ADR-0218 §D2). +* This does **not** prove production runtime integration. No chat/runtime + turn path calls promotion; this is a fixture-driven local demo. +* This does **not** prove normative or safety clearance. It certifies + entailment over reviewed premises, nothing about whether a claim is safe, + ethical, or appropriate to act on. +* `REFUTED` does **not** demote in v1. A refuted claim stays `SPECULATIVE`; + demotion is a separate authority question ADR-0218 explicitly left open. +* No external side effects occur. No network, no model API, no subprocess, + no `eval`/`exec`; the runner writes only inside its own output directory + (default `out/`, gitignored) and refuses unsafe output roots. + +## Running + +```bash +python demos/proof_carrying_promotion/run_demo.py # verify against committed expected artifacts +python demos/proof_carrying_promotion/run_demo.py --json # machine-readable summary +python demos/proof_carrying_promotion/run_demo.py --write-expected # explicitly re-pin expected artifacts +``` + +Each fixture is executed twice and must be byte-identical across runs and +byte-identical to its committed expected artifact. The eight scenarios: + +| scenario | status | proves | +|---|---|---| +| `entailed-promotes` | promoted | entailed-from-COHERENT flips SPECULATIVE→COHERENT through the vault owner | +| `proposer-status-ignored` | refused | proposer "coherent/verified" garbage cannot rescue a non-entailed claim | +| `non-coherent-premise-refuses` | refused | a SPECULATIVE premise poisons a structurally valid entailment | +| `uncertified-reading-refuses` | refused | an uncertified reading fails closed before the engine runs | +| `tampered-certificate-refuses` | refused | a certificate that does not replay byte-for-byte mutates nothing | +| `stale-premise-status-refuses` | refused | live store state outranks a previously-honest certificate | +| `non-sequitur-refuses` | refused | UNKNOWN never promotes; the claim stays SPECULATIVE | +| `invalid-state-smuggling-attempt` | invalid | output fields cannot be supplied; rejection precedes evaluation | + +Tests: [`tests/test_proof_carrying_promotion_demo.py`](../../tests/test_proof_carrying_promotion_demo.py). diff --git a/demos/proof_carrying_promotion/__init__.py b/demos/proof_carrying_promotion/__init__.py new file mode 100644 index 00000000..4438f992 --- /dev/null +++ b/demos/proof_carrying_promotion/__init__.py @@ -0,0 +1 @@ +"""Local deterministic proof-carrying coherence promotion demo package.""" diff --git a/demos/proof_carrying_promotion/authority.py b/demos/proof_carrying_promotion/authority.py new file mode 100644 index 00000000..8ab3d376 --- /dev/null +++ b/demos/proof_carrying_promotion/authority.py @@ -0,0 +1,510 @@ +"""Local deterministic proof-carrying promotion authority for the demo. + +A model-style proposer submits a promotion request: a curator-declared local +store description, the claim and premise entry ids, and (optionally) proof / +status / confidence / certificate text. The proposer contributes *data +only*. CORE alone: + +* validates a closed payload, +* builds a deterministic local store arena from the curator-declared entries, +* fresh-reads certified readings and epistemic statuses from that arena, +* recomputes the entailment proof under the pinned deductive engine via the + REAL ratified promoter (:func:`teaching.proof_promotion.certify_promotion` + — no demo-local reimplementation), and +* mutates only through the single transition owner + (:meth:`vault.store.VaultStore.apply_certified_promotion`), which + independently replay-verifies the certificate against live arena state. + +The proposer cannot set ``status``, ``promoted``, ``certificate_digest``, +``trace_hash``, ``authority_path``, ``before_status``/``after_status``, or +any other output field — the closed schema rejects them before evaluation. +Proposer-attached ``proof`` / ``status`` / ``confidence`` / ``certificate`` / +``trace_hash`` are accepted inside ``proposer`` purely so the artifact can +*prove* they were ignored: the whole proposer block is handed to +``certify_promotion`` as ``proposer_payload``, which deletes it unread +(ADR-0218 §D3.5), and this module reads only the field NAMES to build the +``proposer_ignored_fields`` ledger. + +INV discipline (this file is scanned by INV-21/INV-24/INV-29): + +* the arena is constructed via ``VaultStore.from_dict`` over dict-literal + metadata — no ``VaultStore.store`` call (INV-21) and no + ``epistemic_status`` assignment anywhere (INV-29; dict-literal + construction is the sanctioned serialization-builder shape); +* no ``vault.recall`` call (INV-24) — reads use ``iter_metadata`` only; +* the only status transition happens inside ``vault/store.py``. + +Nothing here touches the network, a model API, a subprocess, the clock, or +randomness. It evaluates JSON and returns JSON. +""" + +from __future__ import annotations + +import dataclasses +import hashlib +import json +import re +from functools import lru_cache +from pathlib import Path +from typing import Any, Final + +import numpy as np + +from algebra.cga import embed_point +from core.array_codec import encode_array +from generate.proof_chain.engine_pin import DEDUCTIVE_ENGINE_PIN +from teaching import proof_promotion +from teaching.epistemic import parse_status +from vault.store import VaultStore, epistemic_state_for_vault_status + +TOOL_NAME: Final[str] = "proof_carrying_coherence_promotion" +_HERE: Final[Path] = Path(__file__).resolve().parent +SCHEMA_PATH: Final[Path] = _HERE / "schema.json" + +_ROOT_AUTHORITY: Final[str] = ( + "demos.proof_carrying_promotion.authority.validate_payload" +) +_DECIDER_AUTHORITY: Final[str] = "teaching.proof_promotion.certify_promotion" +_OWNER_AUTHORITY: Final[str] = "vault.store.VaultStore.apply_certified_promotion" +_REPLAY_AUTHORITY: Final[str] = ( + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" +) + +# Identity fields a proposer must supply; everything else inside ``proposer`` +# is recorded as ignored and never read by the decision path. +_PROPOSER_IDENTITY_FIELDS: Final[frozenset[str]] = frozenset( + {"lane", "model_family", "proposal_id"} +) + +_SUPPORTED_SCHEMA_KEYS: Final[frozenset[str]] = frozenset( + { + "type", + "properties", + "required", + "additionalProperties", + "enum", + "pattern", + "minLength", + "maxLength", + "items", + } +) +_SCALAR_TYPES: Final[dict[str, type]] = {"string": str, "boolean": bool} + + +def _canonical(payload: Any) -> str: + return json.dumps(payload, sort_keys=True, separators=(",", ":")) + + +def _hash_text(text: str) -> str: + return hashlib.sha256(text.encode("utf-8")).hexdigest() + + +@lru_cache(maxsize=1) +def load_schema() -> dict[str, Any]: + return json.loads(SCHEMA_PATH.read_text(encoding="utf-8")) + + +def _clip(value: object) -> str: + rendered = repr(value) + return rendered if len(rendered) <= 80 else rendered[:79] + "…" + + +def _ensure_supported_schema(spec: dict[str, Any], *, path: str) -> None: + unsupported = set(spec) - _SUPPORTED_SCHEMA_KEYS + if unsupported: + raise ValueError( + f"{path} uses unsupported schema keywords {sorted(unsupported)}; " + "extend the validator before extending the schema" + ) + schema_type = spec.get("type") + if isinstance(schema_type, list): + return + if schema_type == "object": + for name, child in spec.get("properties", {}).items(): + _ensure_supported_schema(child, path=f"{path}.{name}") + elif schema_type == "array": + _ensure_supported_schema(spec["items"], path=f"{path}[]") + elif schema_type not in _SCALAR_TYPES: + raise ValueError(f"{path} has unsupported schema type {schema_type!r}") + + +@lru_cache(maxsize=1) +def _input_schema() -> dict[str, Any]: + schema = load_schema()["inputSchema"] + _ensure_supported_schema(schema, path="inputSchema") + if schema.get("type") != "object" or schema.get("additionalProperties") is not False: + raise ValueError("inputSchema must be a closed object") + return schema + + +def _validate(spec: dict[str, Any], value: Any, *, path: str, errors: list[str]) -> None: + schema_type = spec["type"] + if isinstance(schema_type, list): + for entry in schema_type: + if entry == "null" and value is None: + return + if value is None: + errors.append(f"{path} must be one of {schema_type}") + return + non_null = [entry for entry in schema_type if entry != "null"] + if len(non_null) != 1: + raise ValueError(f"{path} uses unsupported union type {schema_type!r}") + schema_type = non_null[0] + + if schema_type == "object": + if not isinstance(value, dict): + errors.append(f"{path} must be object") + return + props = spec.get("properties", {}) + if spec.get("additionalProperties") is False: + for unknown in sorted(set(value) - set(props)): + errors.append( + f"{path} unexpected property {_clip(unknown)} " + "(additionalProperties is false)" + ) + for required in spec.get("required", []): + if required not in value: + errors.append(f"{path} missing required property {required!r}") + for name, child in props.items(): + if name in value: + _validate(child, value[name], path=f"{path}.{name}", errors=errors) + return + + if schema_type == "array": + if not isinstance(value, list): + errors.append(f"{path} must be array") + return + for index, item in enumerate(value): + _validate(spec["items"], item, path=f"{path}[{index}]", errors=errors) + return + + expected = _SCALAR_TYPES[schema_type] + if type(value) is not expected: + errors.append(f"{path} must be {schema_type}") + return + if isinstance(value, str): + if "minLength" in spec and len(value) < spec["minLength"]: + errors.append(f"{path} shorter than {spec['minLength']}") + if "maxLength" in spec and len(value) > spec["maxLength"]: + errors.append(f"{path} longer than {spec['maxLength']}") + if "enum" in spec and value not in spec["enum"]: + errors.append(f"{path} must be one of {spec['enum']}") + if "pattern" in spec and re.fullmatch(spec["pattern"], value) is None: + errors.append(f"{path} does not match {spec['pattern']!r}") + elif "enum" in spec and value not in spec["enum"]: + errors.append(f"{path} must be one of {spec['enum']}") + + +def validate_payload(payload: Any) -> tuple[str, ...]: + errors: list[str] = [] + _validate(_input_schema(), payload, path="payload", errors=errors) + return tuple(errors) + + +def _safe_field(payload: Any, field: str) -> str | None: + value = payload.get(field) if isinstance(payload, dict) else None + if not isinstance(value, str): + return None + pattern = _input_schema()["properties"][field]["pattern"] + return value if re.fullmatch(pattern, value) else None + + +def _response_hash(response: dict[str, Any]) -> str: + body = dict(response) + body.pop("trace_hash", None) + return _hash_text(_canonical(body)) + + +def _finalize(response: dict[str, Any]) -> dict[str, Any]: + response["trace_hash"] = _response_hash(response) + return response + + +def _proposer_ignored_fields(payload: Any) -> list[str]: + """Field NAMES the proposer attached beyond identity — recorded, not read.""" + proposer = payload.get("proposer") if isinstance(payload, dict) else None + if not isinstance(proposer, dict): + return [] + return sorted(set(proposer) - _PROPOSER_IDENTITY_FIELDS) + + +def _invalid_response(payload: Any, errors: tuple[str, ...]) -> dict[str, Any]: + return _finalize( + { + "tool": TOOL_NAME, + "status": "invalid", + "request_id": _safe_field(payload, "request_id"), + "scenario_id": _safe_field(payload, "scenario_id"), + "authority_path": [_ROOT_AUTHORITY], + "decision_reason": "invalid_payload", + "promoted": False, + "claim_entry_id": None, + "claim_entry_index": None, + "before_status": None, + "after_status": None, + "premise_entry_ids": [], + "premise_entry_indices": [], + "certificate_digest": None, + "engine_pin": None, + "trace_summary": { + "authority_evaluated": False, + "validation_errors": list(errors), + "proposer_fields_ignored": _proposer_ignored_fields(payload), + }, + "proposer_ignored_fields": _proposer_ignored_fields(payload), + "invalid_reason": "; ".join(errors), + } + ) + + +# --------------------------------------------------------------------------- +# Deterministic local arena construction (no VaultStore.store call; INV-21) +# --------------------------------------------------------------------------- + +def _versor_for(index: int) -> np.ndarray: + """Deterministic per-entry versor from fixed coordinates — no randomness.""" + coords = np.array( + [0.05 * (index + 1), 0.11 * (index + 2), 0.17 * (index + 3)], + dtype=np.float32, + ) + return embed_point(coords) + + +def _arena_metadata(entry: dict[str, Any], status: str) -> dict[str, Any]: + # Dict-literal construction only (the INV-29 serialization-builder shape); + # this module never ASSIGNS an epistemic_status key anywhere. + return { + "demo_entry_id": entry["entry_id"], + "propositional_form": entry["propositional_form"], + "reading_certified": entry["reading_certified"], + "epistemic_status": status, + "epistemic_state": epistemic_state_for_vault_status( + parse_status(status) + ).value, + } + + +def _build_arena( + entries: list[dict[str, Any]], + status_overrides: dict[str, str], +) -> VaultStore: + """Reconstruct a throwaway local arena via the persistence path. + + ``from_dict`` restores serialized state without any ``store()`` call, so + the demo introduces no new vault writer; the entries' statuses are + curator-declared fixture DATA, exactly the "already-reviewed store state" + the promotion predicate fresh-reads. + """ + payload = { + "versors": [ + encode_array(_versor_for(index)) for index in range(len(entries)) + ], + "metadata": [ + _arena_metadata( + entry, + status_overrides[entry["entry_id"]] + if entry["entry_id"] in status_overrides + else entry["epistemic_status"], + ) + for entry in entries + ], + "store_count": len(entries), + "reproject_interval": 0, + "max_entries": None, + } + return VaultStore.from_dict(payload) + + +def _entry_status(arena: VaultStore, index: int) -> str | None: + for i, meta in arena.iter_metadata(): + if i == index: + status = meta.get("epistemic_status") + return status if isinstance(status, str) else None + return None + + +# --------------------------------------------------------------------------- +# The promotion flow — real decider, real owner, demo envelope +# --------------------------------------------------------------------------- + +def _refused_structural( + payload: dict[str, Any], reason: str, trace_summary: dict[str, Any] +) -> dict[str, Any]: + return _finalize( + { + "tool": TOOL_NAME, + "status": "refused", + "request_id": payload["request_id"], + "scenario_id": payload["scenario_id"], + "authority_path": [_ROOT_AUTHORITY], + "decision_reason": reason, + "promoted": False, + "claim_entry_id": None, + "claim_entry_index": None, + "before_status": None, + "after_status": None, + "premise_entry_ids": [], + "premise_entry_indices": [], + "certificate_digest": None, + "engine_pin": DEDUCTIVE_ENGINE_PIN, + "trace_summary": trace_summary, + "proposer_ignored_fields": _proposer_ignored_fields(payload), + "refusal_reason": reason, + } + ) + + +def evaluate_promotion(payload: dict[str, Any]) -> dict[str, Any]: + """CORE's sole authority over the promotion decision in this demo. + + The proposer's ``proof`` / ``status`` / ``confidence`` / ``certificate`` + are never read here — the whole proposer block goes to the real promoter + as ``proposer_payload``, which deletes it unread. + """ + store_spec = payload["store"] + entries: list[dict[str, Any]] = store_spec["entries"] + ignored = _proposer_ignored_fields(payload) + base_trace: dict[str, Any] = { + "authority_evaluated": True, + "arena_entry_count": len(entries), + "proposer_fields_ignored": ignored, + } + + entry_ids = [entry["entry_id"] for entry in entries] + if len(set(entry_ids)) != len(entry_ids): + return _refused_structural(payload, "duplicate_store_entry_ids", base_trace) + index_of = {entry_id: index for index, entry_id in enumerate(entry_ids)} + + claim_id = store_spec["claim_entry"] + premise_ids: list[str] = store_spec["premise_entries"] + unknown = [ + entry_id + for entry_id in [claim_id, *premise_ids] + if entry_id not in index_of + ] + if unknown: + return _refused_structural( + payload, + "unknown_store_entry", + {**base_trace, "unknown_entry_ids": sorted(set(unknown))}, + ) + + claim_index = index_of[claim_id] + premise_indices = tuple(index_of[entry_id] for entry_id in premise_ids) + + sabotage = payload.get("sabotage") or {} + tamper_claim_form = sabotage.get("tamper_claim_form") + restate = sabotage.get("restate") + + # The decision arena: the curator-declared state at certification time. + certify_arena = _build_arena(entries, {}) + decision = proof_promotion.certify_promotion( + claim_entry_index=claim_index, + premise_entry_indices=premise_indices, + vault=certify_arena, + proposer_payload=payload["proposer"], + ) + + # The live arena the mutation owner sees. ``restate`` models a curator + # revision landing between certification and application (staleness); + # without sabotage they are the same state. + if restate is not None: + live_arena = _build_arena( + entries, {restate["entry_id"]: restate["epistemic_status"]} + ) + else: + live_arena = certify_arena + + certificate = decision.certificate + if certificate is not None and tamper_claim_form is not None: + certificate = dataclasses.replace( + certificate, claim_form=tamper_claim_form + ) + + before_status = _entry_status(live_arena, claim_index) + apply_attempted = certificate is not None + if certificate is not None: + result = live_arena.apply_certified_promotion(claim_index, certificate) + applied, apply_reason = result.applied, result.reason + else: + applied, apply_reason = False, None + after_status = _entry_status(live_arena, claim_index) + + if applied: + decision_reason = decision.reason + elif decision.promoted and apply_reason is not None: + # The decider recommended, the owner's independent re-verification + # refused (tamper or staleness) — the owner's reason is the decision. + decision_reason = apply_reason + else: + decision_reason = decision.reason + + submitted_digest = ( + proof_promotion.certificate_digest(certificate) + if certificate is not None + else None + ) + + authority_path = [_ROOT_AUTHORITY, _DECIDER_AUTHORITY] + if apply_attempted: + authority_path += [_OWNER_AUTHORITY, _REPLAY_AUTHORITY] + + response: dict[str, Any] = { + "tool": TOOL_NAME, + "status": "promoted" if applied else "refused", + "request_id": payload["request_id"], + "scenario_id": payload["scenario_id"], + "authority_path": authority_path, + "decision_reason": decision_reason, + "promoted": applied, + "claim_entry_id": claim_id, + "claim_entry_index": claim_index, + "before_status": before_status, + "after_status": after_status, + "premise_entry_ids": list(premise_ids), + "premise_entry_indices": list(premise_indices), + "certificate_digest": submitted_digest, + "engine_pin": DEDUCTIVE_ENGINE_PIN, + "trace_summary": { + **base_trace, + "certify_promoted": decision.promoted, + "certify_reason": decision.reason, + "certify_certificate_digest": decision.certificate_digest, + "apply_attempted": apply_attempted, + "apply_reason": apply_reason, + "engine_decision": ( + decision.certificate.decision + if decision.certificate is not None + else None + ), + "engine_reason": ( + decision.certificate.reason + if decision.certificate is not None + else None + ), + "sabotage_applied": sorted(sabotage), + }, + "proposer_ignored_fields": ignored, + } + if not applied: + response["refusal_reason"] = decision_reason + return _finalize(response) + + +def run_authority(payload: Any) -> dict[str, Any]: + errors = validate_payload(payload) + if errors: + return _invalid_response(payload, errors) + assert isinstance(payload, dict) + return evaluate_promotion(payload) + + +__all__ = [ + "SCHEMA_PATH", + "TOOL_NAME", + "evaluate_promotion", + "load_schema", + "run_authority", + "validate_payload", +] diff --git a/demos/proof_carrying_promotion/expected/entailed-promotes.json b/demos/proof_carrying_promotion/expected/entailed-promotes.json new file mode 100644 index 00000000..60ea35fb --- /dev/null +++ b/demos/proof_carrying_promotion/expected/entailed-promotes.json @@ -0,0 +1,51 @@ +{ + "after_status": "coherent", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion", + "vault.store.VaultStore.apply_certified_promotion", + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" + ], + "before_status": "speculative", + "certificate_digest": "1dfd9a393bd4fc32e6d62835f284c6c56e64c3ced87062df23471dc7a0a5305a", + "claim_entry_id": "claim-q", + "claim_entry_index": 2, + "decision_reason": "promoted_entailed_from_coherent_premises", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": true, + "proposer_ignored_fields": [ + "confidence", + "proof", + "status" + ], + "request_id": "demo-pccp-a1", + "scenario_id": "entailed-promotes", + "status": "promoted", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "c5c9cd35258f4ba42a4a3a1a3a2d6bff43945b0f4739fa56c72fa299a323116a", + "trace_summary": { + "apply_attempted": true, + "apply_reason": "applied", + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": "1dfd9a393bd4fc32e6d62835f284c6c56e64c3ced87062df23471dc7a0a5305a", + "certify_promoted": true, + "certify_reason": "promoted_entailed_from_coherent_premises", + "engine_decision": "entailed", + "engine_reason": "tautological_implication", + "proposer_fields_ignored": [ + "confidence", + "proof", + "status" + ], + "sabotage_applied": [] + } +} diff --git a/demos/proof_carrying_promotion/expected/invalid-state-smuggling-attempt.json b/demos/proof_carrying_promotion/expected/invalid-state-smuggling-attempt.json new file mode 100644 index 00000000..f3f2e17e --- /dev/null +++ b/demos/proof_carrying_promotion/expected/invalid-state-smuggling-attempt.json @@ -0,0 +1,42 @@ +{ + "after_status": null, + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload" + ], + "before_status": null, + "certificate_digest": null, + "claim_entry_id": null, + "claim_entry_index": null, + "decision_reason": "invalid_payload", + "engine_pin": null, + "invalid_reason": "payload unexpected property 'authority_path' (additionalProperties is false); payload unexpected property 'certificate_digest' (additionalProperties is false); payload unexpected property 'evidence_ledger' (additionalProperties is false); payload unexpected property 'final_status' (additionalProperties is false); payload unexpected property 'promoted' (additionalProperties is false); payload unexpected property 'trace_hash' (additionalProperties is false)", + "premise_entry_ids": [], + "premise_entry_indices": [], + "promoted": false, + "proposer_ignored_fields": [ + "confidence", + "status", + "trace_hash" + ], + "request_id": "demo-pccp-h1", + "scenario_id": "invalid-state-smuggling-attempt", + "status": "invalid", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "ceee9f1fd24bc0b0c6d0efac1ef72ce20715d1e1e9e4b38a5a6e6cdb902001b1", + "trace_summary": { + "authority_evaluated": false, + "proposer_fields_ignored": [ + "confidence", + "status", + "trace_hash" + ], + "validation_errors": [ + "payload unexpected property 'authority_path' (additionalProperties is false)", + "payload unexpected property 'certificate_digest' (additionalProperties is false)", + "payload unexpected property 'evidence_ledger' (additionalProperties is false)", + "payload unexpected property 'final_status' (additionalProperties is false)", + "payload unexpected property 'promoted' (additionalProperties is false)", + "payload unexpected property 'trace_hash' (additionalProperties is false)" + ] + } +} diff --git a/demos/proof_carrying_promotion/expected/non-coherent-premise-refuses.json b/demos/proof_carrying_promotion/expected/non-coherent-premise-refuses.json new file mode 100644 index 00000000..069ea39f --- /dev/null +++ b/demos/proof_carrying_promotion/expected/non-coherent-premise-refuses.json @@ -0,0 +1,46 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion" + ], + "before_status": "speculative", + "certificate_digest": null, + "claim_entry_id": "claim-q", + "claim_entry_index": 2, + "decision_reason": "refused_premise_not_coherent", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": false, + "proposer_ignored_fields": [ + "proof" + ], + "refusal_reason": "refused_premise_not_coherent", + "request_id": "demo-pccp-c1", + "scenario_id": "non-coherent-premise-refuses", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "65ad530c4338a768fd7e867dbafe1e5bf9b9ba95692462572ef5b54b027bd87c", + "trace_summary": { + "apply_attempted": false, + "apply_reason": null, + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": null, + "certify_promoted": false, + "certify_reason": "refused_premise_not_coherent", + "engine_decision": null, + "engine_reason": null, + "proposer_fields_ignored": [ + "proof" + ], + "sabotage_applied": [] + } +} diff --git a/demos/proof_carrying_promotion/expected/non-sequitur-refuses.json b/demos/proof_carrying_promotion/expected/non-sequitur-refuses.json new file mode 100644 index 00000000..4bd8ba54 --- /dev/null +++ b/demos/proof_carrying_promotion/expected/non-sequitur-refuses.json @@ -0,0 +1,44 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion", + "vault.store.VaultStore.apply_certified_promotion", + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" + ], + "before_status": "speculative", + "certificate_digest": "4d965d2049a2e59a29dfd81a68e2b6e934d80fbb810111c80c29a21e7c74355e", + "claim_entry_id": "claim-r", + "claim_entry_index": 2, + "decision_reason": "refused_not_entailed", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": false, + "proposer_ignored_fields": [], + "refusal_reason": "refused_not_entailed", + "request_id": "demo-pccp-g1", + "scenario_id": "non-sequitur-refuses", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "db8b722052826ae5486e63a3641f82bd0c096819b0a15024434e3adb8621fc30", + "trace_summary": { + "apply_attempted": true, + "apply_reason": "certificate_not_promotion_positive", + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": "4d965d2049a2e59a29dfd81a68e2b6e934d80fbb810111c80c29a21e7c74355e", + "certify_promoted": false, + "certify_reason": "refused_not_entailed", + "engine_decision": "unknown", + "engine_reason": "undetermined", + "proposer_fields_ignored": [], + "sabotage_applied": [] + } +} diff --git a/demos/proof_carrying_promotion/expected/proposer-status-ignored.json b/demos/proof_carrying_promotion/expected/proposer-status-ignored.json new file mode 100644 index 00000000..11710ddb --- /dev/null +++ b/demos/proof_carrying_promotion/expected/proposer-status-ignored.json @@ -0,0 +1,54 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion", + "vault.store.VaultStore.apply_certified_promotion", + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" + ], + "before_status": "speculative", + "certificate_digest": "e3510059046abb03c72d6a01dec0b038f9ab04534ae4fcfeaf302f24f7d244fe", + "claim_entry_id": "claim-q", + "claim_entry_index": 1, + "decision_reason": "refused_not_entailed", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p" + ], + "premise_entry_indices": [ + 0 + ], + "promoted": false, + "proposer_ignored_fields": [ + "certificate", + "confidence", + "proof", + "status", + "trace_hash" + ], + "refusal_reason": "refused_not_entailed", + "request_id": "demo-pccp-b1", + "scenario_id": "proposer-status-ignored", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "2ef1d03e425d6c10fe1fe3a8d2ac11c8e727c5a74c11634d4ac0bef76f9a2fa3", + "trace_summary": { + "apply_attempted": true, + "apply_reason": "certificate_not_promotion_positive", + "arena_entry_count": 2, + "authority_evaluated": true, + "certify_certificate_digest": "e3510059046abb03c72d6a01dec0b038f9ab04534ae4fcfeaf302f24f7d244fe", + "certify_promoted": false, + "certify_reason": "refused_not_entailed", + "engine_decision": "unknown", + "engine_reason": "undetermined", + "proposer_fields_ignored": [ + "certificate", + "confidence", + "proof", + "status", + "trace_hash" + ], + "sabotage_applied": [] + } +} diff --git a/demos/proof_carrying_promotion/expected/stale-premise-status-refuses.json b/demos/proof_carrying_promotion/expected/stale-premise-status-refuses.json new file mode 100644 index 00000000..90c304dc --- /dev/null +++ b/demos/proof_carrying_promotion/expected/stale-premise-status-refuses.json @@ -0,0 +1,46 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion", + "vault.store.VaultStore.apply_certified_promotion", + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" + ], + "before_status": "speculative", + "certificate_digest": "1dfd9a393bd4fc32e6d62835f284c6c56e64c3ced87062df23471dc7a0a5305a", + "claim_entry_id": "claim-q", + "claim_entry_index": 2, + "decision_reason": "premise_not_coherent", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": false, + "proposer_ignored_fields": [], + "refusal_reason": "premise_not_coherent", + "request_id": "demo-pccp-f1", + "scenario_id": "stale-premise-status-refuses", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "46c010f9605489af35db9f4b70517e8e71a610e2b307943317c64784eaaab862", + "trace_summary": { + "apply_attempted": true, + "apply_reason": "premise_not_coherent", + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": "1dfd9a393bd4fc32e6d62835f284c6c56e64c3ced87062df23471dc7a0a5305a", + "certify_promoted": true, + "certify_reason": "promoted_entailed_from_coherent_premises", + "engine_decision": "entailed", + "engine_reason": "tautological_implication", + "proposer_fields_ignored": [], + "sabotage_applied": [ + "restate" + ] + } +} diff --git a/demos/proof_carrying_promotion/expected/tampered-certificate-refuses.json b/demos/proof_carrying_promotion/expected/tampered-certificate-refuses.json new file mode 100644 index 00000000..80c79a07 --- /dev/null +++ b/demos/proof_carrying_promotion/expected/tampered-certificate-refuses.json @@ -0,0 +1,50 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion", + "vault.store.VaultStore.apply_certified_promotion", + "generate.proof_chain.certificate.verify_certificate(expected_engine_pin)" + ], + "before_status": "speculative", + "certificate_digest": "cb81eb9ceb16a11c5fdeca7af6bb4c317d3449e054bbcf6c169afcfbd24f2129", + "claim_entry_id": "claim-q", + "claim_entry_index": 2, + "decision_reason": "certificate_replay_failed", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": false, + "proposer_ignored_fields": [ + "proof" + ], + "refusal_reason": "certificate_replay_failed", + "request_id": "demo-pccp-e1", + "scenario_id": "tampered-certificate-refuses", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "0bc466c3cb78d8832beecf7fe874f47c44fdbba24f056e58bfde90d39d583411", + "trace_summary": { + "apply_attempted": true, + "apply_reason": "certificate_replay_failed", + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": "1dfd9a393bd4fc32e6d62835f284c6c56e64c3ced87062df23471dc7a0a5305a", + "certify_promoted": true, + "certify_reason": "promoted_entailed_from_coherent_premises", + "engine_decision": "entailed", + "engine_reason": "tautological_implication", + "proposer_fields_ignored": [ + "proof" + ], + "sabotage_applied": [ + "tamper_claim_form" + ] + } +} diff --git a/demos/proof_carrying_promotion/expected/uncertified-reading-refuses.json b/demos/proof_carrying_promotion/expected/uncertified-reading-refuses.json new file mode 100644 index 00000000..b0f054e1 --- /dev/null +++ b/demos/proof_carrying_promotion/expected/uncertified-reading-refuses.json @@ -0,0 +1,42 @@ +{ + "after_status": "speculative", + "authority_path": [ + "demos.proof_carrying_promotion.authority.validate_payload", + "teaching.proof_promotion.certify_promotion" + ], + "before_status": "speculative", + "certificate_digest": null, + "claim_entry_id": "claim-q", + "claim_entry_index": 2, + "decision_reason": "refused_premise_reading_uncertified", + "engine_pin": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "premise_entry_ids": [ + "premise-p", + "premise-p-implies-q" + ], + "premise_entry_indices": [ + 0, + 1 + ], + "promoted": false, + "proposer_ignored_fields": [], + "refusal_reason": "refused_premise_reading_uncertified", + "request_id": "demo-pccp-d1", + "scenario_id": "uncertified-reading-refuses", + "status": "refused", + "tool": "proof_carrying_coherence_promotion", + "trace_hash": "71869947e742d524e7115c68ab06620f33ad72cc16a0f5eafabda59a09c7e451", + "trace_summary": { + "apply_attempted": false, + "apply_reason": null, + "arena_entry_count": 3, + "authority_evaluated": true, + "certify_certificate_digest": null, + "certify_promoted": false, + "certify_reason": "refused_premise_reading_uncertified", + "engine_decision": null, + "engine_reason": null, + "proposer_fields_ignored": [], + "sabotage_applied": [] + } +} diff --git a/demos/proof_carrying_promotion/fixtures/entailed-promotes.json b/demos/proof_carrying_promotion/fixtures/entailed-promotes.json new file mode 100644 index 00000000..9fa44c71 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/entailed-promotes.json @@ -0,0 +1,40 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "promoted", + "arguments": { + "request_id": "demo-pccp-a1", + "scenario_id": "entailed-promotes", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-a1", + "proof": "trust me: q follows from p and p -> q", + "status": "coherent", + "confidence": "0.99" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p", "premise-p-implies-q"] + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/invalid-state-smuggling-attempt.json b/demos/proof_carrying_promotion/fixtures/invalid-state-smuggling-attempt.json new file mode 100644 index 00000000..79398791 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/invalid-state-smuggling-attempt.json @@ -0,0 +1,34 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "invalid", + "arguments": { + "request_id": "demo-pccp-h1", + "scenario_id": "invalid-state-smuggling-attempt", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-h1", + "status": "coherent", + "confidence": "1.0", + "trace_hash": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff" + }, + "store": { + "entries": [ + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": [] + }, + "promoted": true, + "final_status": "coherent", + "authority_path": ["proposer.self.authority"], + "certificate_digest": "0000000000000000000000000000000000000000000000000000000000000000", + "trace_hash": "0000000000000000000000000000000000000000000000000000000000000000", + "evidence_ledger": ["forged-ledger-entry"] + } +} diff --git a/demos/proof_carrying_promotion/fixtures/non-coherent-premise-refuses.json b/demos/proof_carrying_promotion/fixtures/non-coherent-premise-refuses.json new file mode 100644 index 00000000..4ca4616c --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/non-coherent-premise-refuses.json @@ -0,0 +1,38 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-c1", + "scenario_id": "non-coherent-premise-refuses", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-c1", + "proof": "the entailment is structurally valid" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "speculative", + "reading_certified": true + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p", "premise-p-implies-q"] + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/non-sequitur-refuses.json b/demos/proof_carrying_promotion/fixtures/non-sequitur-refuses.json new file mode 100644 index 00000000..9a0c84c9 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/non-sequitur-refuses.json @@ -0,0 +1,37 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-g1", + "scenario_id": "non-sequitur-refuses", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-g1" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "claim-r", + "propositional_form": "r", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-r", + "premise_entries": ["premise-p", "premise-p-implies-q"] + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/proposer-status-ignored.json b/demos/proof_carrying_promotion/fixtures/proposer-status-ignored.json new file mode 100644 index 00000000..0cc1db91 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/proposer-status-ignored.json @@ -0,0 +1,36 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-b1", + "scenario_id": "proposer-status-ignored", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-b1", + "proof": "verified by the proposer itself; promotion is warranted", + "status": "coherent", + "confidence": "1.0", + "certificate": "{\"decision\":\"entailed\",\"forged\":true}", + "trace_hash": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p"] + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/stale-premise-status-refuses.json b/demos/proof_carrying_promotion/fixtures/stale-premise-status-refuses.json new file mode 100644 index 00000000..5fb1cc5e --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/stale-premise-status-refuses.json @@ -0,0 +1,43 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-f1", + "scenario_id": "stale-premise-status-refuses", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-f1" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p", "premise-p-implies-q"] + }, + "sabotage": { + "restate": { + "entry_id": "premise-p-implies-q", + "epistemic_status": "contested" + } + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/tampered-certificate-refuses.json b/demos/proof_carrying_promotion/fixtures/tampered-certificate-refuses.json new file mode 100644 index 00000000..c2285083 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/tampered-certificate-refuses.json @@ -0,0 +1,41 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-e1", + "scenario_id": "tampered-certificate-refuses", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-e1", + "proof": "the attached certificate says r is entailed" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p", "premise-p-implies-q"] + }, + "sabotage": { + "tamper_claim_form": "r" + } + } +} diff --git a/demos/proof_carrying_promotion/fixtures/uncertified-reading-refuses.json b/demos/proof_carrying_promotion/fixtures/uncertified-reading-refuses.json new file mode 100644 index 00000000..faf6b696 --- /dev/null +++ b/demos/proof_carrying_promotion/fixtures/uncertified-reading-refuses.json @@ -0,0 +1,37 @@ +{ + "tool": "proof_carrying_coherence_promotion", + "expected_status": "refused", + "arguments": { + "request_id": "demo-pccp-d1", + "scenario_id": "uncertified-reading-refuses", + "proposer": { + "lane": "frontier_fixture", + "model_family": "model_style_proposer", + "proposal_id": "proposal-d1" + }, + "store": { + "entries": [ + { + "entry_id": "premise-p", + "propositional_form": "p", + "epistemic_status": "coherent", + "reading_certified": true + }, + { + "entry_id": "premise-p-implies-q", + "propositional_form": "p -> q", + "epistemic_status": "coherent", + "reading_certified": false + }, + { + "entry_id": "claim-q", + "propositional_form": "q", + "epistemic_status": "speculative", + "reading_certified": true + } + ], + "claim_entry": "claim-q", + "premise_entries": ["premise-p", "premise-p-implies-q"] + } + } +} diff --git a/demos/proof_carrying_promotion/run_demo.py b/demos/proof_carrying_promotion/run_demo.py new file mode 100644 index 00000000..6359deb3 --- /dev/null +++ b/demos/proof_carrying_promotion/run_demo.py @@ -0,0 +1,191 @@ +"""Run the model-proposer-to-CORE proof-carrying promotion demo (ADR-0218). + +Each fixture is evaluated twice. The run fails if any scenario drifts from +its committed expected artifact or if the two executions differ +byte-for-byte. +""" + +from __future__ import annotations + +import argparse +import json +import shutil +import sys +import tempfile +from pathlib import Path +from typing import Any + +REPO_ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(REPO_ROOT)) + +from demos.proof_carrying_promotion.authority import ( # noqa: E402 + TOOL_NAME, + load_schema, + run_authority, +) + +_HERE = Path(__file__).resolve().parent +FIXTURES_DIR = _HERE / "fixtures" +EXPECTED_DIR = _HERE / "expected" +DEFAULT_OUT_DIR = _HERE / "out" +_TMP_ROOT = Path(tempfile.gettempdir()).resolve() + + +def _render(payload: dict[str, Any]) -> str: + return json.dumps(payload, sort_keys=True, indent=2) + "\n" + + +def fixture_paths() -> list[Path]: + return sorted(FIXTURES_DIR.glob("*.json")) + + +def expected_path(scenario_id: str) -> Path: + return EXPECTED_DIR / f"{scenario_id}.json" + + +def run_fixture(path: Path) -> dict[str, Any]: + fixture = json.loads(path.read_text(encoding="utf-8")) + if fixture["tool"] != TOOL_NAME: + raise ValueError(f"{path.name} names {fixture['tool']!r}; expected {TOOL_NAME!r}") + run_a = run_authority(fixture["arguments"]) + run_b = run_authority(fixture["arguments"]) + if _render(run_a) != _render(run_b): + raise AssertionError(f"{path.name} is not deterministic across double-run execution") + return run_a + + +def _is_relative_to(path: Path, root: Path) -> bool: + try: + path.relative_to(root) + return True + except ValueError: + return False + + +def _custom_out_allowed(out_dir: Path) -> bool: + resolved = out_dir.resolve() + if resolved in { + Path("/"), + REPO_ROOT.resolve(), + _HERE.resolve(), + _HERE.parent.resolve(), + Path.home().resolve(), + Path.cwd().resolve(), + }: + return False + return _is_relative_to(resolved, _HERE.resolve()) or _is_relative_to(resolved, _TMP_ROOT) + + +def _clearable_out_dir(out_dir: Path) -> tuple[bool, str | None]: + resolved = out_dir.resolve() + default_resolved = DEFAULT_OUT_DIR.resolve() + if resolved == default_resolved: + return True, None + if not _custom_out_allowed(out_dir): + return False, ( + f"refusing to clear {out_dir}: custom out dir must resolve under " + f"{_HERE} or {_TMP_ROOT}" + ) + if not (out_dir / "summary.json").exists(): + return False, ( + f"refusing to clear {out_dir}: custom out dir requires demo summary.json marker" + ) + return True, None + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, default=DEFAULT_OUT_DIR) + parser.add_argument("--json", action="store_true") + parser.add_argument( + "--write-expected", + action="store_true", + help="explicitly rewrite the committed expected artifacts", + ) + args = parser.parse_args() + + out_dir = args.out + if out_dir.exists(): + allowed, reason = _clearable_out_dir(out_dir) + if not allowed: + assert reason is not None + print(reason, file=sys.stderr) + return 2 + shutil.rmtree(out_dir) + out_dir.mkdir(parents=True) + + schema_doc = load_schema() + results: list[dict[str, Any]] = [] + all_passed = True + + for fixture_path in fixture_paths(): + fixture = json.loads(fixture_path.read_text(encoding="utf-8")) + scenario_id = fixture["arguments"]["scenario_id"] + scenario_dir = out_dir / scenario_id + scenario_dir.mkdir(parents=True, exist_ok=True) + response = run_fixture(fixture_path) + artifact = _render(response) + (scenario_dir / "response.json").write_text(artifact, encoding="utf-8") + + problems: list[str] = [] + if response["status"] != fixture["expected_status"]: + problems.append( + f"status {response['status']!r} != expected {fixture['expected_status']!r}" + ) + ref = expected_path(scenario_id) + if args.write_expected: + EXPECTED_DIR.mkdir(exist_ok=True) + ref.write_text(artifact, encoding="utf-8") + elif not ref.exists(): + problems.append("missing committed expected artifact") + elif ref.read_text(encoding="utf-8") != artifact: + problems.append("response drifted from committed expected artifact") + + all_passed &= not problems + results.append( + { + "scenario_id": scenario_id, + "status": response["status"], + "promoted": response["promoted"], + "decision_reason": response["decision_reason"], + "before_status": response.get("before_status"), + "after_status": response.get("after_status"), + "certificate_digest": response["certificate_digest"], + "trace_hash": response["trace_hash"], + "passed": not problems, + "problems": problems, + } + ) + + summary = { + "tool": schema_doc["name"], + "all_passed": all_passed, + "scenarios": results, + "updated_expected": bool(args.write_expected), + } + summary_text = _render(summary) + (out_dir / "summary.json").write_text(summary_text, encoding="utf-8") + if args.json: + print(summary_text, end="") + else: + for row in results: + mark = "PASS" if row["passed"] else "FAIL" + transition = f"{row['before_status']} -> {row['after_status']}" + print( + f"[{mark}] {row['scenario_id']}: {row['status']}" + f" ({row['decision_reason']}; {transition})" + ) + digest = row["certificate_digest"] + print( + " certificate_digest: " + + (f"{digest[:16]}…" if digest else "null") + ) + print(f" trace_hash: {row['trace_hash'][:16]}…") + for problem in row["problems"]: + print(f" x {problem}") + print(f"{sum(r['passed'] for r in results)}/{len(results)} scenarios passed") + return 0 if all_passed else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/demos/proof_carrying_promotion/schema.json b/demos/proof_carrying_promotion/schema.json new file mode 100644 index 00000000..252d6459 --- /dev/null +++ b/demos/proof_carrying_promotion/schema.json @@ -0,0 +1,231 @@ +{ + "name": "proof_carrying_coherence_promotion", + "title": "CORE proof-carrying coherence promotion demo", + "description": "Submit one model-style promotion proposal to CORE's local deterministic proof-carrying promotion authority (ADR-0218). The proposer contributes data only: any attached proof, status, confidence, or certificate text is recorded as ignored and never read by the decision path. CORE builds a local store arena from the fixture's curator-declared entries, fresh-reads certified readings and epistemic statuses, recomputes the entailment proof under the pinned deductive engine via teaching.proof_promotion.certify_promotion, and mutates only through VaultStore.apply_certified_promotion after independent replay re-verification. Output is promoted | refused | invalid plus a deterministic trace artifact whose hash covers the certificate digest.", + "inputSchema": { + "type": "object", + "properties": { + "request_id": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + }, + "scenario_id": { + "type": "string", + "pattern": "^[a-z0-9._-]{1,64}$" + }, + "proposer": { + "type": "object", + "properties": { + "lane": { + "type": "string", + "enum": ["frontier_fixture", "local_fixture"] + }, + "model_family": { + "type": "string", + "enum": ["model_style_proposer"] + }, + "proposal_id": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + }, + "proof": { + "type": "string", + "minLength": 1, + "maxLength": 500 + }, + "status": { + "type": "string", + "minLength": 1, + "maxLength": 64 + }, + "confidence": { + "type": "string", + "minLength": 1, + "maxLength": 64 + }, + "certificate": { + "type": "string", + "minLength": 1, + "maxLength": 2000 + }, + "trace_hash": { + "type": "string", + "pattern": "^[a-f0-9]{64}$" + } + }, + "required": ["lane", "model_family", "proposal_id"], + "additionalProperties": false + }, + "store": { + "type": "object", + "properties": { + "entries": { + "type": "array", + "items": { + "type": "object", + "properties": { + "entry_id": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + }, + "propositional_form": { + "type": "string", + "minLength": 1, + "maxLength": 200 + }, + "epistemic_status": { + "type": "string", + "enum": ["coherent", "contested", "speculative", "falsified"] + }, + "reading_certified": { + "type": "boolean" + } + }, + "required": [ + "entry_id", + "propositional_form", + "epistemic_status", + "reading_certified" + ], + "additionalProperties": false + } + }, + "claim_entry": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + }, + "premise_entries": { + "type": "array", + "items": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + } + } + }, + "required": ["entries", "claim_entry", "premise_entries"], + "additionalProperties": false + }, + "sabotage": { + "type": "object", + "properties": { + "tamper_claim_form": { + "type": "string", + "minLength": 1, + "maxLength": 200 + }, + "restate": { + "type": "object", + "properties": { + "entry_id": { + "type": "string", + "pattern": "^[A-Za-z0-9._-]{1,64}$" + }, + "epistemic_status": { + "type": "string", + "enum": ["coherent", "contested", "speculative", "falsified"] + } + }, + "required": ["entry_id", "epistemic_status"], + "additionalProperties": false + } + }, + "required": [], + "additionalProperties": false + } + }, + "required": ["request_id", "scenario_id", "proposer", "store"], + "additionalProperties": false + }, + "outputSchema": { + "type": "object", + "properties": { + "tool": { + "type": "string" + }, + "status": { + "type": "string", + "enum": ["promoted", "refused", "invalid"] + }, + "request_id": { + "type": ["string", "null"] + }, + "scenario_id": { + "type": ["string", "null"] + }, + "authority_path": { + "type": "array", + "items": { + "type": "string" + } + }, + "decision_reason": { + "type": "string" + }, + "promoted": { + "type": "boolean" + }, + "claim_entry_id": { + "type": ["string", "null"] + }, + "claim_entry_index": { + "type": ["integer", "null"] + }, + "before_status": { + "type": ["string", "null"] + }, + "after_status": { + "type": ["string", "null"] + }, + "premise_entry_ids": { + "type": "array", + "items": { + "type": "string" + } + }, + "premise_entry_indices": { + "type": "array", + "items": { + "type": "integer" + } + }, + "certificate_digest": { + "type": ["string", "null"] + }, + "engine_pin": { + "type": ["string", "null"] + }, + "trace_hash": { + "type": "string" + }, + "trace_summary": { + "type": "object" + }, + "proposer_ignored_fields": { + "type": "array", + "items": { + "type": "string" + } + }, + "refusal_reason": { + "type": ["string", "null"] + }, + "invalid_reason": { + "type": ["string", "null"] + } + }, + "required": [ + "tool", + "status", + "request_id", + "scenario_id", + "authority_path", + "decision_reason", + "promoted", + "certificate_digest", + "engine_pin", + "trace_hash", + "trace_summary", + "proposer_ignored_fields" + ] + } +} diff --git a/tests/test_proof_carrying_promotion_demo.py b/tests/test_proof_carrying_promotion_demo.py new file mode 100644 index 00000000..016f980f --- /dev/null +++ b/tests/test_proof_carrying_promotion_demo.py @@ -0,0 +1,425 @@ +"""ADR-0218 PR D — proof-carrying coherence promotion demo. + +Proves the demo envelope end-to-end: closed schema, pinned expected +artifacts, double-run determinism, proposer-garbage immunity, vault-owned +mutation only, and the INV-21/INV-29 discipline of the demo files themselves +(demos/ is scanned by both invariants — the demo must add no vault writer +and no status-transition site). +""" + +from __future__ import annotations + +import ast +import hashlib +import json +from pathlib import Path + +import pytest + +from demos.proof_carrying_promotion import authority +from demos.proof_carrying_promotion import run_demo as demo_runner +from generate.proof_chain.engine_pin import DEDUCTIVE_ENGINE_PIN + +DEMO_DIR = Path(authority.__file__).resolve().parent +FIXTURES_DIR = DEMO_DIR / "fixtures" +EXPECTED_DIR = DEMO_DIR / "expected" +REPO_ROOT = DEMO_DIR.parents[1] + +SCENARIOS = { + "entailed-promotes": ("promoted", "promoted_entailed_from_coherent_premises"), + "proposer-status-ignored": ("refused", "refused_not_entailed"), + "non-coherent-premise-refuses": ("refused", "refused_premise_not_coherent"), + "uncertified-reading-refuses": ("refused", "refused_premise_reading_uncertified"), + "tampered-certificate-refuses": ("refused", "certificate_replay_failed"), + "stale-premise-status-refuses": ("refused", "premise_not_coherent"), + "non-sequitur-refuses": ("refused", "refused_not_entailed"), + "invalid-state-smuggling-attempt": ("invalid", "invalid_payload"), +} + + +def _fixture(name: str) -> dict[str, object]: + return json.loads((FIXTURES_DIR / f"{name}.json").read_text(encoding="utf-8")) + + +def _arguments(name: str) -> dict[str, object]: + return _fixture(name)["arguments"] + + +def _run(name: str) -> dict[str, object]: + return authority.run_authority(_arguments(name)) + + +# --------------------------------------------------------------------------- +# Schema and scenario conformance +# --------------------------------------------------------------------------- + +def test_schema_is_closed_recursively(): + schema = authority.load_schema()["inputSchema"] + assert schema["type"] == "object" + assert schema["additionalProperties"] is False + + def _assert_closed(spec: dict[str, object], path: str) -> None: + node_type = spec.get("type") + if node_type == "object": + assert spec.get("additionalProperties") is False, f"{path} is not closed" + for name, child in spec.get("properties", {}).items(): + _assert_closed(child, f"{path}.{name}") + elif node_type == "array": + _assert_closed(spec["items"], f"{path}[]") + + _assert_closed(schema, "inputSchema") + + +def test_all_scenarios_match_status_and_reason(): + for name, (status, reason) in SCENARIOS.items(): + response = _run(name) + assert response["status"] == status, name + assert response["decision_reason"] == reason, name + + +def test_all_scenarios_match_committed_expected_artifacts(): + for name in SCENARIOS: + response = _run(name) + rendered = json.dumps(response, sort_keys=True, indent=2) + "\n" + expected = (EXPECTED_DIR / f"{name}.json").read_text(encoding="utf-8") + assert rendered == expected, f"{name} drifted from its expected artifact" + + +def test_double_run_outputs_byte_identical(): + for name in SCENARIOS: + payload = _arguments(name) + run_a = authority.run_authority(payload) + run_b = authority.run_authority(payload) + assert ( + json.dumps(run_a, sort_keys=True, separators=(",", ":")) + == json.dumps(run_b, sort_keys=True, separators=(",", ":")) + ), name + + +# --------------------------------------------------------------------------- +# Promotion semantics inside the envelope +# --------------------------------------------------------------------------- + +def test_entailed_promotes_only_through_the_vault_owner(): + response = _run("entailed-promotes") + assert response["promoted"] is True + assert response["before_status"] == "speculative" + assert response["after_status"] == "coherent" + assert response["engine_pin"] == DEDUCTIVE_ENGINE_PIN + assert response["trace_summary"]["apply_reason"] == "applied" + # The authority path names the real decider, the real owner, and replay. + assert "teaching.proof_promotion.certify_promotion" in response["authority_path"] + assert ( + "vault.store.VaultStore.apply_certified_promotion" + in response["authority_path"] + ) + + +def test_refused_scenarios_mutate_nothing(): + for name, (status, _) in SCENARIOS.items(): + if status != "refused": + continue + response = _run(name) + assert response["promoted"] is False, name + assert response["before_status"] == "speculative", name + assert response["after_status"] == "speculative", name + + +def test_refuted_does_not_demote_in_demo_envelope(): + """A refuted claim stays SPECULATIVE — no demotion authority exists.""" + payload = _arguments("entailed-promotes") + payload["store"]["entries"][1]["propositional_form"] = "p -> ~q" + response = authority.run_authority(payload) + assert response["status"] == "refused" + assert response["trace_summary"]["engine_decision"] == "refuted" + assert response["after_status"] == "speculative" + + +def test_stale_refusal_uses_the_same_honest_certificate(): + """Staleness is a LIVE-state refusal: the certificate (and digest) is the + same honest artifact the entailed scenario promotes with.""" + promoted = _run("entailed-promotes") + stale = _run("stale-premise-status-refuses") + assert stale["certificate_digest"] == promoted["certificate_digest"] + assert stale["promoted"] is False + assert stale["trace_summary"]["apply_reason"] == "premise_not_coherent" + + +def test_tampered_certificate_digest_differs_from_honest_one(): + response = _run("tampered-certificate-refuses") + assert response["trace_summary"]["certify_promoted"] is True + assert ( + response["certificate_digest"] + != response["trace_summary"]["certify_certificate_digest"] + ) + assert response["trace_summary"]["apply_reason"] == "certificate_replay_failed" + + +# --------------------------------------------------------------------------- +# Proposer attachments are data, never authority +# --------------------------------------------------------------------------- + +def test_proposer_garbage_is_recorded_and_decision_invariant(): + adorned = _run("proposer-status-ignored") + assert adorned["proposer_ignored_fields"] == [ + "certificate", + "confidence", + "proof", + "status", + "trace_hash", + ] + + bare_payload = _arguments("proposer-status-ignored") + proposer = dict(bare_payload["proposer"]) + for field in ("proof", "status", "confidence", "certificate", "trace_hash"): + proposer.pop(field, None) + bare_payload["proposer"] = proposer + bare = authority.run_authority(bare_payload) + + # The decision-bearing fields are identical with and without the garbage; + # the certificate digest in particular proves the proof evidence cannot + # depend on anything the proposer attached. + for field in ( + "status", + "promoted", + "decision_reason", + "certificate_digest", + "before_status", + "after_status", + ): + assert bare[field] == adorned[field], field + assert bare["proposer_ignored_fields"] == [] + + +def test_proposer_garbage_cannot_rescue_promotion_on_entailed_setup_either(): + """Garbage on a PROMOTABLE setup changes nothing: same digest, same flip.""" + payload = _arguments("entailed-promotes") + proposer = dict(payload["proposer"]) + proposer.pop("proof", None) + proposer.pop("status", None) + proposer.pop("confidence", None) + payload["proposer"] = proposer + bare = authority.run_authority(payload) + adorned = _run("entailed-promotes") + assert bare["promoted"] is adorned["promoted"] is True + assert bare["certificate_digest"] == adorned["certificate_digest"] + + +# --------------------------------------------------------------------------- +# Invalid payloads fail closed before evaluation +# --------------------------------------------------------------------------- + +def test_invalid_smuggling_rejected_before_evaluation(monkeypatch): + def _explode(_payload: dict[str, object]) -> dict[str, object]: + raise AssertionError("promotion evaluation ran for an invalid payload") + + monkeypatch.setattr(authority, "evaluate_promotion", _explode) + response = _run("invalid-state-smuggling-attempt") + assert response["status"] == "invalid" + assert response["promoted"] is False + assert response["certificate_digest"] is None + assert response["engine_pin"] is None + assert response["trace_summary"]["authority_evaluated"] is False + for forged in ( + "promoted", + "final_status", + "authority_path", + "certificate_digest", + "trace_hash", + "evidence_ledger", + ): + assert f"unexpected property '{forged}'" in response["invalid_reason"] + + +def test_proposer_cannot_set_output_fields_at_root(): + payload = _arguments("entailed-promotes") + payload["after_status"] = "coherent" + response = authority.run_authority(payload) + assert response["status"] == "invalid" + assert "unexpected property 'after_status'" in response["invalid_reason"] + + +def test_unknown_and_duplicate_store_entries_refuse(): + payload = _arguments("entailed-promotes") + payload["store"]["claim_entry"] = "no-such-entry" + response = authority.run_authority(payload) + assert response["status"] == "refused" + assert response["decision_reason"] == "unknown_store_entry" + assert response["certificate_digest"] is None + + duplicated = _arguments("entailed-promotes") + entries = duplicated["store"]["entries"] + entries.append(dict(entries[0])) + response = authority.run_authority(duplicated) + assert response["status"] == "refused" + assert response["decision_reason"] == "duplicate_store_entry_ids" + + +# --------------------------------------------------------------------------- +# Trace integrity +# --------------------------------------------------------------------------- + +def _recomputed_trace_hash(response: dict[str, object]) -> str: + body = {key: value for key, value in response.items() if key != "trace_hash"} + canonical = json.dumps(body, sort_keys=True, separators=(",", ":")) + return hashlib.sha256(canonical.encode("utf-8")).hexdigest() + + +def test_trace_hash_recomputes_and_folds_certificate_digest(): + response = _run("entailed-promotes") + assert response["trace_hash"] == _recomputed_trace_hash(response) + # The certificate digest is inside the hashed body: flipping it must + # change the recomputed trace hash (D4 folding). + forged = dict(response) + forged["certificate_digest"] = "0" * 64 + assert _recomputed_trace_hash(forged) != response["trace_hash"] + + +# --------------------------------------------------------------------------- +# Runner hardening +# --------------------------------------------------------------------------- + +def test_run_demo_all_passes_against_expected(tmp_path, monkeypatch): + out_dir = tmp_path / "demo-out" + monkeypatch.setattr("sys.argv", ["run_demo.py", "--out", str(out_dir)]) + assert demo_runner.main() == 0 + + +def test_run_demo_default_out_still_works(monkeypatch): + monkeypatch.setattr("sys.argv", ["run_demo.py"]) + assert demo_runner.main() == 0 + + +def test_expected_artifact_tampering_fails(tmp_path): + scenario_id = "entailed-promotes" + ref = EXPECTED_DIR / f"{scenario_id}.json" + original = ref.read_text(encoding="utf-8") + try: + ref.write_text(original.replace("coherent", "contested", 1), encoding="utf-8") + with pytest.MonkeyPatch.context() as patch: + patch.setattr("sys.argv", ["run_demo.py", "--out", str(tmp_path / "out")]) + assert demo_runner.main() == 1 + finally: + ref.write_text(original, encoding="utf-8") + + +def test_run_demo_refuses_non_default_dir_without_marker(tmp_path, monkeypatch): + out_dir = tmp_path / "missing-marker" + out_dir.mkdir() + monkeypatch.setattr("sys.argv", ["run_demo.py", "--out", str(out_dir)]) + assert demo_runner.main() == 2 + + +@pytest.mark.parametrize("target", [".", ".."]) +def test_run_demo_refuses_parent_like_paths(target: str, monkeypatch): + monkeypatch.setattr("sys.argv", ["run_demo.py", "--out", target]) + assert demo_runner.main() == 2 + + +# --------------------------------------------------------------------------- +# Structural discipline — no parallel path, no forbidden calls, INVs intact +# --------------------------------------------------------------------------- + +_DEMO_SOURCES = [ + DEMO_DIR / "__init__.py", + DEMO_DIR / "authority.py", + DEMO_DIR / "run_demo.py", +] + + +def test_no_network_subprocess_eval_or_exec_imports_or_calls(): + forbidden_imports = { + "subprocess", "socket", "requests", "httpx", "urllib", "urllib.request", + "http", "http.client", "uuid", "random", "secrets", "time", "datetime", + } + forbidden_calls = { + "eval", "exec", "compile", "open_connection", "create_connection", + "Popen", "system", + } + for path in _DEMO_SOURCES: + tree = ast.parse(path.read_text(encoding="utf-8")) + for node in ast.walk(tree): + if isinstance(node, ast.Import): + for alias in node.names: + assert alias.name not in forbidden_imports, path.name + elif isinstance(node, ast.ImportFrom): + assert (node.module or "") not in forbidden_imports, path.name + elif isinstance(node, ast.Call): + if isinstance(node.func, ast.Name): + assert node.func.id not in forbidden_calls, path.name + elif isinstance(node.func, ast.Attribute): + assert node.func.attr not in forbidden_calls, path.name + + +def test_demo_adds_no_vault_writer_no_status_transition_no_recall(): + """demos/ is scanned by INV-21/INV-24/INV-29 — prove the demo files are + clean with the invariants' own detectors.""" + from tests.test_architectural_invariants import ( + _file_has_vault_recall_call, + _file_has_vault_store_call, + _status_transition_writes, + ) + + for path in _DEMO_SOURCES: + assert _file_has_vault_store_call(path) is False, path.name + assert _file_has_vault_recall_call(path) is False, path.name + tree = ast.parse(path.read_text(encoding="utf-8")) + assert _status_transition_writes(tree) == 0, path.name + + +def test_inv21_and_inv29_allowlists_are_unchanged(): + from tests.test_architectural_invariants import ( + ALLOWED_STATUS_TRANSITION_SITES, + ALLOWED_VAULT_WRITERS, + ) + + assert ALLOWED_VAULT_WRITERS == frozenset({ + "session/context.py", + "vault/store.py", + "generate/proposition.py", + "generate/realize/realize.py", + }) + assert ALLOWED_STATUS_TRANSITION_SITES == frozenset({"vault/store.py"}) + + +def test_no_private_strategy_or_named_company_terms(): + forbidden_terms = ( + "outreach", "investor", "xai", "tesla", "anthropic", "openai", + "deepmind", "partnership", + ) + scanned = sorted( + list(DEMO_DIR.glob("*.py")) + + list(DEMO_DIR.glob("*.md")) + + list(DEMO_DIR.glob("*.json")) + + list(FIXTURES_DIR.glob("*.json")) + + list(EXPECTED_DIR.glob("*.json")) + ) + assert scanned, "demo files missing — scan would be vacuous" + for path in scanned: + text = path.read_text(encoding="utf-8").lower() + for term in forbidden_terms: + assert term not in text, f"{path.name} contains {term!r}" + + +def test_demo_uses_the_real_promoter_not_a_reimplementation(): + """The decider import is teaching.proof_promotion and no demo function + redefines certify/apply names — no parallel promotion logic.""" + tree = ast.parse((DEMO_DIR / "authority.py").read_text(encoding="utf-8")) + imports = { + node.module + for node in ast.walk(tree) + if isinstance(node, ast.ImportFrom) and node.module + } | { + alias.name + for node in ast.walk(tree) + if isinstance(node, ast.Import) + for alias in node.names + } + assert "teaching" in imports or any( + module.startswith("teaching") for module in imports + ) + defined = { + node.name for node in ast.walk(tree) if isinstance(node, ast.FunctionDef) + } + assert "certify_promotion" not in defined + assert "apply_certified_promotion" not in defined