IMPL-005: Lean 4 mechanisation of R5 protocol + shape verification (SPEC-005 v0.1.0) #7

Merged

hugooconnor merged 0 commits from refs/pull/7/head into main 2026-05-04 06:50:46 +00:00

Conversation 0 Commits - Files changed -

hugooconnor commented 2026-05-03 06:03:06 +00:00 (Migrated from codeberg.org)

Copy link

Mechanises SPEC-005: Lean 4 proofs of R5 (causal protocol + shape) verification, raising SPEC-002/003 contracts to the rigour level of the existing SPEC-001 R1–R3 proofs. Coordinated via plans/IMPL-005-r5-mechanisation.spl.

What landed

Lattice foundations

• lean-cbcl/LeanCbcl/Lattice/Result.lean — three-valued VerificationResult with bounded-lattice instance (REQ-510 / CON-510).
• lean-cbcl/LeanCbcl/Lattice/Store.lean — MessageStore G-Set lattice + lookup_monotone (REQ-511 / CON-511).

verify model + headline theorems (lean-cbcl/LeanCbcl/Verify.lean)

• verify_monotone — REQ-512 / CON-512 (the v1 retry that this PR's plan-edit unblocked).
• verify_all_is_meet — REQ-513 / CON-513.
• verify_eventually_consistent — REQ-514 / CON-514 (the SPEC-005 headline).

R5 sub-checks (lean-cbcl/LeanCbcl/R5.lean)

• check_acyclicity_iff_no_cycle — REQ-515 part 1 (soundness).
• check_reachability_iff_all_reachable — REQ-515 part 2 (soundness).
• check_performative_definedness_iff_all_defined — REQ-515 part 3 (full iff).
• check_step_uniqueness_iff_no_duplicates — REQ-515 part 4 (full iff).

DCFL preservation (lean-cbcl/LeanCbcl/DCFLPreservation.lean)

• dcfl_preserved_under_protocol — REQ-516 / REQ-209.
• dcfl_preserved_under_shape — REQ-516 / REQ-225.

Audit + parity + CI

• lean-cbcl/AxiomAudit.lean + scripts/check-axioms.sh — NFR-511 / TEST-551 (only propext / Classical.choice / Quot.sound permitted).
• crates/cbcl-core/tests/lean_parity.rs — TEST-518 / ADR-513 (one proptest per Lean theorem, 30 tests).
• .github/workflows/lean.yml extended with parity tests + cbcl-core triggers (TEST-518 / NFR-510).
• SPEC-002 / SPEC-003 verified-by: annotations reconciled with as-built state (REQ-517).

Test plan

Verified locally on a worktree of this branch:

• cd lean-cbcl && lake build — 40 jobs green
• cargo test -p cbcl-core --test lean_parity — 30/30 passed
• bash scripts/check-axioms.sh — 16 theorems audited, all axioms allowlisted
• CI green on Codeberg

Notes

• Theorems do not import Mathlib — the lattice typeclasses are rolled by hand. The plan's mathlib-setup task is recorded as completed but did not land a Mathlib dependency; the description in plans/IMPL-005-r5-mechanisation.spl and any verified-by notes referencing Mathlib structures are slightly aspirational vs. as-built. Worth reconciling in a follow-up if Mathlib dependencies are wanted later.
• The plan file itself includes an operator-asserted retry rule (defeater + prefer) added when v1 of verify-monotone produced an empty diff and wedged the supervisor; v2 then landed 547027e with the actual proof.

Mechanises SPEC-005: Lean 4 proofs of R5 (causal protocol + shape) verification, raising SPEC-002/003 contracts to the rigour level of the existing SPEC-001 R1–R3 proofs. Coordinated via `plans/IMPL-005-r5-mechanisation.spl`. ## What landed **Lattice foundations** - `lean-cbcl/LeanCbcl/Lattice/Result.lean` — three-valued `VerificationResult` with bounded-lattice instance (REQ-510 / CON-510). - `lean-cbcl/LeanCbcl/Lattice/Store.lean` — `MessageStore` G-Set lattice + `lookup_monotone` (REQ-511 / CON-511). **verify model + headline theorems** (`lean-cbcl/LeanCbcl/Verify.lean`) - `verify_monotone` — REQ-512 / CON-512 (the v1 retry that this PR's plan-edit unblocked). - `verify_all_is_meet` — REQ-513 / CON-513. - `verify_eventually_consistent` — REQ-514 / CON-514 (the SPEC-005 headline). **R5 sub-checks** (`lean-cbcl/LeanCbcl/R5.lean`) - `check_acyclicity_iff_no_cycle` — REQ-515 part 1 (soundness). - `check_reachability_iff_all_reachable` — REQ-515 part 2 (soundness). - `check_performative_definedness_iff_all_defined` — REQ-515 part 3 (full iff). - `check_step_uniqueness_iff_no_duplicates` — REQ-515 part 4 (full iff). **DCFL preservation** (`lean-cbcl/LeanCbcl/DCFLPreservation.lean`) - `dcfl_preserved_under_protocol` — REQ-516 / REQ-209. - `dcfl_preserved_under_shape` — REQ-516 / REQ-225. **Audit + parity + CI** - `lean-cbcl/AxiomAudit.lean` + `scripts/check-axioms.sh` — NFR-511 / TEST-551 (only `propext` / `Classical.choice` / `Quot.sound` permitted). - `crates/cbcl-core/tests/lean_parity.rs` — TEST-518 / ADR-513 (one proptest per Lean theorem, 30 tests). - `.github/workflows/lean.yml` extended with parity tests + cbcl-core triggers (TEST-518 / NFR-510). - SPEC-002 / SPEC-003 `verified-by:` annotations reconciled with as-built state (REQ-517). ## Test plan Verified locally on a worktree of this branch: - [x] `cd lean-cbcl && lake build` — 40 jobs green - [x] `cargo test -p cbcl-core --test lean_parity` — 30/30 passed - [x] `bash scripts/check-axioms.sh` — 16 theorems audited, all axioms allowlisted - [ ] CI green on Codeberg ## Notes - Theorems do not import Mathlib — the lattice typeclasses are rolled by hand. The plan's `mathlib-setup` task is recorded as completed but did not land a Mathlib dependency; the description in `plans/IMPL-005-r5-mechanisation.spl` and any `verified-by` notes referencing Mathlib structures are slightly aspirational vs. as-built. Worth reconciling in a follow-up if Mathlib dependencies are wanted later. - The plan file itself includes an operator-asserted retry rule (defeater + prefer) added when v1 of `verify-monotone` produced an empty diff and wedged the supervisor; v2 then landed `547027e` with the actual proof.

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

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

No description provided.