Repository navigation
formal: compare Lean protocol with fenced store decisions - #336
Conversation
🚀 Deploying Preview to Cloudflare 🚀Preview URL: https://feat-protocol-differential-76.spec.contextful.work (commit 13d3f7b)This URL reflects your latest Preview deploymentPreview Deployments by commit
|
contextful formal protocol-differential replays saved regressions, then compares seeded lease and stale-write sequences across three nodes and four lease generations against the executable Lean model. Each step compares the holder, fence, guarded-object ETags and commit outcome; a drift is reduced, replayed and reported with both states. Closes #76.
9f5f892 to
13d3f7b
Compare
![flaredispatch-fractalboxdev[bot]](https://avatars.githubusercontent.com/in/4273665?s=60&v=4){kind=small}
There was a problem hiding this comment.
AI code review — 🛑 Request changes
Risk tier: full · 1 critical · 3 warnings · 0 suggestions
Reviewers: security
1. ⚠️ Warning — Spawns a separate reference process for every test case
📍 crates/contextful-cli/src/protocol_differential.rs:400-425
'compare' starts and tears down the protocol executable for each sequence. A normal run executes 64 generated cases plus every regression, so this incurs dozens of process startups and repeated model initialization; the integration test invokes the command twice. Keep one reference process alive and stream multiple cases through it, or otherwise batch cases, to avoid making this formal check unnecessarily slow.
2. ⚠️ Warning — Rebuilds the Lean package on every CLI invocation
📍 crates/contextful-cli/src/protocol_differential.rs:466-486
When '--reference' is omitted, every invocation runs 'lake build', even when the binary is already available and unchanged. The integration test deliberately invokes this command twice, causing repeated build checks and process overhead. Resolve/build the reference once per test run (or cache the resolved executable/build result) instead of unconditionally invoking Lake from each CLI invocation.
3. 🛑 Critical — Gated protocol assurance test can pass without executing
📍 crates/contextful-cli/tests/integration/protocol_differential.rs:26-34
The test returns successfully whenever 'lake --version' is unavailable, unless an opt-in environment variable is set. This allows the ledger-marked 'stale-fence-differential' gate to pass in environments without Lean while performing none of the protocol differential checks. Make Lean availability a required CI prerequisite for this pinned gate, or mark the test as skipped/non-gating rather than recording it as gated.
4. ⚠️ Warning — Assurance additions are attributed to the wrong milestone
The change increases Milestone 1 — 'authority core' performed count from 187 to 190, while all three newly pinned clauses are under 'assurance.differential-test'. This makes the compliance status ledger internally misleading; update the appropriate assurance milestone/count instead of changing the authority milestone.
1 participant
The protocol differential command compares seeded lease and stale-write sequences across three nodes and four lease generations. Each step compares the executable Lean model with Rust lease, pointer, and commit-log decisions, including the holder, fence, guarded-object ETags, and commit outcome.
Saved cases replay before generated cases. A drift is reduced, replayed, and reported with the reduced sequence's own step index and model/store states. The fixed-seed integration test records zero drift in the target ledger. Weekly random-seed exploration is defined by the counterpart FlareDispatch recipe in fractalboxdev/flare-dispatch#182, alongside the repository's existing dispatcher schedules.
The three protocol integration tests pass with Lean required. The pinned protocol model builds, corpus lint reports zero violations, and the CLI's no-default-feature Clippy check passes with existing warnings in unchanged core and CLI code. Strict warning promotion flags those existing warnings. The regression for minimized drift reports fails before its repair.
The harness calls existing core store decisions. Its Lean model and node projection are explicit under
assurance.model.protocol-model; the three differential-test clauses pin the integration tests.Closes #76.