# ceco proof gate

Runtime policy enforcement extracted from [`ceco-offline`](../ceco-offline)
(`development` @ `484bb16`, 2026-07-04).

This package is the **proof gate** only: an MCP server that evaluates agent
actions against a Policy State Machine, emits a tamper-evident audit trail, and
optionally dispatches approved transitions to internal / federated handlers.

It does **not** include the ceco compile / synthesis pipeline (`ceco derive`,
SMT/Lean generation, `ceco-mcp` analysis server, or supplier-onboarding demo).

## What is included

| Area | Modules |
|---|---|
| Gate MCP + SSE daemon | `gate_mcp_server`, `gate_daemon`, `gate_config` |
| Transition evaluation | `runtime`, `dsl`, `sexp`, `simulate` (concrete), `validator` |
| Federation / handlers | `mcp_client`, `mcp_federation`, `internal_mcp_server`, `internal_handlers` |
| Context & anchors | `context_resolvers`, `policy_anchor`, `code_guards`, `proof_cache` |
| Audit / attestation | `audit/` (hash chain, CPAR/CCPB, optional ZK backends) |

## Docs

- [Proof Gate API](docs/whitepapers/ceco-proof-gate-api.html) — MCP tool reference
- [MCP Architecture](docs/whitepapers/ceco-mcp-architecture.html) — tiered gate / internal / domain
- [Gate Runtime Performance](docs/whitepapers/ceco-gate-runtime-performance.html) — SSE daemon, machine cache, transition index
- [Gate Security Findings](docs/whitepapers/ceco-gate-security-findings.html)
- [Audit Trail](docs/whitepapers/ceco-audit-trail.html)
- [Proof Gate State Machine](docs/whitepapers/rb_proof_gate_state_machine.html)
- [Full specification](docs/spec/ceco-specification.pdf) — Part II is the runtime gate; Parts I/III describe the offline compile pipeline (not shipped here)
- [Operating notes](GATE.md)

## Install

```bash
cd /home/martyn/repos/ceco
poetry install
# or: pip install -e ".[dev]"
```

## Quick start (payment example)

```bash
export CECO_GATE_CONFIG=examples/gate_config.payment.yaml
export CECO_GATE_INTERNAL_MODE=inprocess

# stdio MCP (Cursor / Claude Desktop spawn this)
poetry run ceco-gate-mcp

# or persistent SSE daemon for multi-turn agents
poetry run ceco-gate-daemon
curl http://127.0.0.1:14780/health
```

Point an MCP client at stdio `ceco-gate-mcp`, or at
`http://127.0.0.1:14780/sse` for the daemon.

## Entry points

| Script | Module |
|---|---|
| `ceco-gate-mcp` | `ceco.gate_mcp_server:main` |
| `ceco-gate-daemon` | `ceco.gate_daemon:main` |
| `ceco-internal-mcp` | `ceco.internal_mcp_server:main` |

## Tests

```bash
poetry run pytest tests/ -q
```

## Provenance

Source: `/home/martyn/repos/ceco-offline` branch `development` commit `484bb16`.
Feature branches `feat/gate-daemon`, `feat/machine-cache`, and `feat/transition-index`
are already merged into that tip. Local uncommitted edits in `ceco-offline` that
removed the machine cache / transition index were **not** carried over.