Implement runtime causal verification, shape constraints, and policy handling (REQ-200/220/231/305) #3

Merged

hugooconnor merged 0 commits from refs/pull/3/head into main

2026-04-28 07:17:51 +00:00

hugooconnor commented

2026-04-28 03:59:45 +00:00

(Migrated from codeberg.org)

Summary

End-to-end implementation of the runtime side of CBCL's verification model. Before this branch, dialects could declare causal protocols and shape constraints, but those declarations weren't enforced when messages arrived. This branch closes the gap: parse → causal verify → expand → shape check → apply effects, with policy-driven handling of Unknown predecessors, blame attribution on every rejection, and signature binding for the new fields.

What this implements

Module	What landed
`cbcl-core/src/protocol.rs`	Three-valued lattice (`Valid`/`Unknown`/`Violation`) with `meet`/`join`. `CausalProtocol`, `StepDecl`, `NodeRef::{Single, Any, All}`. `verify_causal` reads `:caused-by`, looks up predecessors in the store, returns the result.
`cbcl-core/src/store.rs`	`ThreadedMessageStore` (per-thread G-Set CRDT, ADR-008 thread isolation). `HashIndex` for O(1) lookup. `CausalClosureBundle` for thread-history transfer.
`cbcl-core/src/policy.rs`	`UnknownPredecessorPolicy::{Reject, Buffer { max_pending, ttl }}`. `apply_policy` is a pure mapping. `PendingQueue` is the per-thread bounded buffer with TTL and re-evaluation.
`cbcl-core/src/blame.rs`	`ViolationError` attribution on every rejection (causal and shape).
`cbcl-core/src/r5.rs`	Shape + protocol well-formedness. `r5_violations_with_ancestors` resolves inherited performatives.
`cbcl-core/src/clock.rs`	`Clock` trait, `NoClock` (default), `SystemClock` (std-gated).
`cbcl-core/src/agent.rs`	`Agent` owns the store, policy, pending queue, merge policy, and clock. `evaluate_and_apply` enforces the full pipeline before applying effects. Returns `AgentOutcome::{Applied, CausalReject, Pending, Buffered, EvalError}`. `MergePolicy::{Conjunction, Disjunction}` for multi-protocol composition.
`cbcl-core/src/canonical.rs`	Canonical signing form (RFC 9804 §6.2) extended to v2: covers `causal_protocol` and `shapes` when present, byte-identical to v1 when absent. `CANONICAL_FORM_VERSION` constant tracks bumps.
`cbcl-parser/src/pipeline.rs`	`run_pipeline_full` orchestrates the fail-closed receive path with policy-driven `Pending`/`Buffered` outcomes. Wrapped/dialect-scoped messages traverse to the innermost Simple before verification.

Review history

This branch went through four rounds of review feedback. Each round's findings are addressed in their own commits, listed here so reviewers can audit incremental fixes in isolation:

Round 1 — initial review (4 findings)

ed060e8 R5 protocol definedness honors inherited performatives
9f3a3ae Pipeline reorders causal verify before evaluate (no shape masking)
eb4195e Pipeline applies UnknownPredecessorPolicy (was treating Unknown as Valid)
2e3b56a Agent::evaluate_and_apply enforces causal verification (was bypassing entirely)

Round 2 — five findings on round-1 fixes

e8350fb Reject signed dialects with causal_protocol/shapes (stopgap, later replaced)
c687434 Alias cbcl → cbcl-base in install-time ancestor resolution
d608b10 Pipeline iterates all protocols mentioning a performative (child protocols on inherited perfs)
4a58a27 Meta-validation passes registry ancestors
72356e9 Pipeline traverses wrappers to innermost Simple

Round 3 — three findings, ported to agent

362ee77 Agent traverses wrappers
fcfd681 Agent iterates all installed protocols
8feb746 Agent re-evaluation filters to matching protocols

Round 4 — three low-severity polish items

5752b43 Extracted innermost_simple to Message method
e07e8fe Explicit (Pending, Pending) arm in merge_policy_outcomes
5cd9c7b Clock-aware buffer (evaluate_and_apply_at / step_at / expire(now))

Self-review / follow-ups (post round-4 sign-off)

1d25319 Bind causal_protocol/shapes via canonical signing form (replaces the round-2 stopgap)
d762a14 Add MergePolicy::{Conjunction, Disjunction} to Agent
d54d062 Inject Clock trait into Agent
96c3085 Fix MergePolicy::Disjunction (Unknown, Violation) inconsistency — surfaced by my own re-review; the live and re-evaluation paths disagreed under disjunction, allowing buffered messages to be flushed as Reject by an unrelated protocol's verdict
fc49712 Pin canonical form via version constant + golden-bytes snapshots
6651d6e Polish Clock: SystemClock falls back to u64::MAX on failure, clone test, eviction-is-pull-based doc

Testing

877 workspace tests passing across 16 binaries. Each finding ships with a regression test that demonstrates the bug on the unfixed code, so a future regression in any specific area surfaces immediately.

Migration / API notes

Public API additions:

PipelineResult::{Pending, Buffered} variants; PipelineContext::{new, with_policy} constructors
Agent::{with_policy, with_clock, with_merge_policy, evaluate_and_apply_at, step_at, expire, reevaluate_pending}
AgentOutcome enum (replaces Result<EvalResult, EvalError> from evaluate_and_apply)
MergePolicy::{Conjunction, Disjunction}
Clock trait, NoClock, SystemClock (std-gated)
CANONICAL_FORM_VERSION (currently 2); legacy dialects produce v1-identical bytes
Message::innermost_simple()

Behavioural changes:

Agent::evaluate_and_apply return type changed to AgentOutcome — call sites that pattern-matched Result need updating.
run_pipeline_full now requires a policy field on PipelineContext (use ::new() for the default Reject).

Test plan

Workspace tests pass (cargo test --workspace)
No new clippy warnings introduced
Branch up to date with main (merged via 0be60d9)
CI green on Codeberg
Independent reviewer pass on the 7 self-review-driven follow-up commits

## Summary End-to-end implementation of the runtime side of CBCL's verification model. Before this branch, dialects could *declare* causal protocols and shape constraints, but those declarations weren't enforced when messages arrived. This branch closes the gap: parse → causal verify → expand → shape check → apply effects, with policy-driven handling of `Unknown` predecessors, blame attribution on every rejection, and signature binding for the new fields. ## What this implements | Module | What landed | |---|---| | `cbcl-core/src/protocol.rs` | Three-valued lattice (`Valid`/`Unknown`/`Violation`) with `meet`/`join`. `CausalProtocol`, `StepDecl`, `NodeRef::{Single, Any, All}`. `verify_causal` reads `:caused-by`, looks up predecessors in the store, returns the result. | | `cbcl-core/src/store.rs` | `ThreadedMessageStore` (per-thread G-Set CRDT, ADR-008 thread isolation). `HashIndex` for O(1) lookup. `CausalClosureBundle` for thread-history transfer. | | `cbcl-core/src/policy.rs` | `UnknownPredecessorPolicy::{Reject, Buffer { max_pending, ttl }}`. `apply_policy` is a pure mapping. `PendingQueue` is the per-thread bounded buffer with TTL and re-evaluation. | | `cbcl-core/src/blame.rs` | `ViolationError` attribution on every rejection (causal and shape). | | `cbcl-core/src/r5.rs` | Shape + protocol well-formedness. `r5_violations_with_ancestors` resolves inherited performatives. | | `cbcl-core/src/clock.rs` | `Clock` trait, `NoClock` (default), `SystemClock` (std-gated). | | `cbcl-core/src/agent.rs` | `Agent` owns the store, policy, pending queue, merge policy, and clock. `evaluate_and_apply` enforces the full pipeline before applying effects. Returns `AgentOutcome::{Applied, CausalReject, Pending, Buffered, EvalError}`. `MergePolicy::{Conjunction, Disjunction}` for multi-protocol composition. | | `cbcl-core/src/canonical.rs` | Canonical signing form (RFC 9804 §6.2) extended to v2: covers `causal_protocol` and `shapes` when present, byte-identical to v1 when absent. `CANONICAL_FORM_VERSION` constant tracks bumps. | | `cbcl-parser/src/pipeline.rs` | `run_pipeline_full` orchestrates the fail-closed receive path with policy-driven `Pending`/`Buffered` outcomes. Wrapped/dialect-scoped messages traverse to the innermost Simple before verification. | ## Review history This branch went through four rounds of review feedback. Each round's findings are addressed in their own commits, listed here so reviewers can audit incremental fixes in isolation: **Round 1 — initial review (4 findings)** - `ed060e8` R5 protocol definedness honors inherited performatives - `9f3a3ae` Pipeline reorders causal verify before evaluate (no shape masking) - `eb4195e` Pipeline applies `UnknownPredecessorPolicy` (was treating `Unknown` as `Valid`) - `2e3b56a` `Agent::evaluate_and_apply` enforces causal verification (was bypassing entirely) **Round 2 — five findings on round-1 fixes** - `e8350fb` Reject signed dialects with `causal_protocol`/`shapes` (stopgap, later replaced) - `c687434` Alias `cbcl` → `cbcl-base` in install-time ancestor resolution - `d608b10` Pipeline iterates all protocols mentioning a performative (child protocols on inherited perfs) - `4a58a27` Meta-validation passes registry ancestors - `72356e9` Pipeline traverses wrappers to innermost Simple **Round 3 — three findings, ported to agent** - `362ee77` Agent traverses wrappers - `fcfd681` Agent iterates all installed protocols - `8feb746` Agent re-evaluation filters to matching protocols **Round 4 — three low-severity polish items** - `5752b43` Extracted `innermost_simple` to `Message` method - `e07e8fe` Explicit `(Pending, Pending)` arm in `merge_policy_outcomes` - `5cd9c7b` Clock-aware buffer (`evaluate_and_apply_at` / `step_at` / `expire(now)`) **Self-review / follow-ups (post round-4 sign-off)** - `1d25319` Bind `causal_protocol`/`shapes` via canonical signing form (replaces the round-2 stopgap) - `d762a14` Add `MergePolicy::{Conjunction, Disjunction}` to Agent - `d54d062` Inject `Clock` trait into Agent - `96c3085` **Fix `MergePolicy::Disjunction` (Unknown, Violation) inconsistency** — surfaced by my own re-review; the live and re-evaluation paths disagreed under disjunction, allowing buffered messages to be flushed as `Reject` by an unrelated protocol's verdict - `fc49712` Pin canonical form via version constant + golden-bytes snapshots - `6651d6e` Polish `Clock`: `SystemClock` falls back to `u64::MAX` on failure, clone test, eviction-is-pull-based doc ## Testing 877 workspace tests passing across 16 binaries. Each finding ships with a regression test that demonstrates the bug on the unfixed code, so a future regression in any specific area surfaces immediately. ## Migration / API notes Public API additions: - `PipelineResult::{Pending, Buffered}` variants; `PipelineContext::{new, with_policy}` constructors - `Agent::{with_policy, with_clock, with_merge_policy, evaluate_and_apply_at, step_at, expire, reevaluate_pending}` - `AgentOutcome` enum (replaces `Result<EvalResult, EvalError>` from `evaluate_and_apply`) - `MergePolicy::{Conjunction, Disjunction}` - `Clock` trait, `NoClock`, `SystemClock` (std-gated) - `CANONICAL_FORM_VERSION` (currently `2`); legacy dialects produce v1-identical bytes - `Message::innermost_simple()` Behavioural changes: - `Agent::evaluate_and_apply` return type changed to `AgentOutcome` — call sites that pattern-matched `Result` need updating. - `run_pipeline_full` now requires a `policy` field on `PipelineContext` (use `::new()` for the default `Reject`). ## Test plan - [x] Workspace tests pass (`cargo test --workspace`) - [x] No new clippy warnings introduced - [x] Branch up to date with `main` (merged via `0be60d9`) - [ ] CI green on Codeberg - [ ] Independent reviewer pass on the 7 self-review-driven follow-up commits

No reviewers

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

anuna-research/cbcl-rs!3

No description provided.

Rows
Columns