core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

Merge pull request #696 from AssetOverflow/feat/pccp-demo

Browse source 
ADR-0218 PR D: local deterministic proof-carrying promotion demo
This commit is contained in:
Shay 2026-06-11 22:51:05 -07:00 committed by GitHub
commit 015b97803b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
23 changed files with 2148 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
demos/proof_carrying_promotion/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
out/

108
demos/proof_carrying_promotion/README.md Normal file
View file

@ -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).

1
demos/proof_carrying_promotion/__init__.py Normal file
View file

@ -0,0 +1 @@
"""Local deterministic proof-carrying coherence promotion demo package."""

510
demos/proof_carrying_promotion/authority.py Normal file
View file

@ -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",
]

51
demos/proof_carrying_promotion/expected/entailed-promotes.json Normal file
View file

@ -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": []
}
}

42
demos/proof_carrying_promotion/expected/invalid-state-smuggling-attempt.json Normal file
View file

@ -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)"
]
}
}

46
demos/proof_carrying_promotion/expected/non-coherent-premise-refuses.json Normal file
View file

@ -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": []
}
}

44
demos/proof_carrying_promotion/expected/non-sequitur-refuses.json Normal file
View file

@ -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": []
}
}

54
demos/proof_carrying_promotion/expected/proposer-status-ignored.json Normal file
View file

@ -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": []
}
}

46
demos/proof_carrying_promotion/expected/stale-premise-status-refuses.json Normal file
View file

@ -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"
]
}
}

50
demos/proof_carrying_promotion/expected/tampered-certificate-refuses.json Normal file
View file

@ -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"
]
}
}

42
demos/proof_carrying_promotion/expected/uncertified-reading-refuses.json Normal file
View file

@ -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": []
}
}

40
demos/proof_carrying_promotion/fixtures/entailed-promotes.json Normal file
View file

@ -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"]
}
}
}

34
demos/proof_carrying_promotion/fixtures/invalid-state-smuggling-attempt.json Normal file
View file

@ -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"]
}
}

38
demos/proof_carrying_promotion/fixtures/non-coherent-premise-refuses.json Normal file
View file

@ -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"]
}
}
}

37
demos/proof_carrying_promotion/fixtures/non-sequitur-refuses.json Normal file
View file

@ -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"]
}
}
}

36
demos/proof_carrying_promotion/fixtures/proposer-status-ignored.json Normal file
View file

@ -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"]
}
}
}

43
demos/proof_carrying_promotion/fixtures/stale-premise-status-refuses.json Normal file
View file

@ -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"
}
}
}
}

41
demos/proof_carrying_promotion/fixtures/tampered-certificate-refuses.json Normal file
View file

@ -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"
}
}
}

37
demos/proof_carrying_promotion/fixtures/uncertified-reading-refuses.json Normal file
View file

@ -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"]
}
}
}

191
demos/proof_carrying_promotion/run_demo.py Normal file
View file

@ -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())

231
demos/proof_carrying_promotion/schema.json Normal file
View file

@ -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"
]
}
}

425
tests/test_proof_carrying_promotion_demo.py Normal file
View file

@ -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