proof(ocapn): mechanize op:flush per-reference FIFO in Lean 4 + Veil#3249
Draft
kumavis wants to merge 6 commits into
Draft
proof(ocapn): mechanize op:flush per-reference FIFO in Lean 4 + Veil#3249kumavis wants to merge 6 commits into
kumavis wants to merge 6 commits into
Conversation
|
Implement the receiver-initiated flush handshake that preserves per-reference FIFO order when a peer is about to shorten a promise (typically as part of a third-party handoff). When the receiver sends op:flush for an exported promise position, the exporter mints a fresh local promise, swaps it in at the same export position (keeping the slot's refcount), and replies with op:flush-done. Further deliveries the receiver had already sent for that position arrive before the ack and dispatch on the original promise; deliveries sent after ack are serialized through the new promise and naturally buffer until the shortened reference resolves it. Also exposes _debug.flushExport on Ocapn for tests, and adds replaceExportValue on the pairwise table to support in-place value replacement at a slot.
Move op:flush / op:flush-done into the existing OcapnMessageUnionCodec snapshot table so the wire form is captured by the same convention as the other operations, and update the snapshots. Drop the now-redundant manual round-trip tests. The flush behavior tests previously had B return an unresolved promise directly, which blocks the deliver-fulfill until the promise settles and prevented the export from being registered. Wrap the promise in an array so the array (a copyArray) is the immediate fulfillment value and the embedded promise is serialized as desc:import-promise on the wire. Also satisfy lint: thread the void/Promise<void> conversion of quietReject through unknown, and silence no-use-before-define on captures of send, didUnplug, and quietReject inside the new handler / flushExport.
kumavis
force-pushed
the
claude/implement-ocapn-flush-iisn9
branch
from
f8ea0e2 to
40aee83
Compare
Add packages/ocapn/proofs/veil — a Lake project that mechanizes the central
safety claim of the op:flush proposal in the Veil framework on top of Lean
4.24.
The model is a 3-party Alice/Bob/Carol abstraction:
- Bob is the sole sender of reference messages targeting Alice's exported
promise p1, partitioned into two phases: pre-flush messages (B->A) and
post-handoff messages (B->C->C->A after the handoff completes).
- The flush handshake (op:flush, op:flush-done), the deposit-gift / handoff-
give / withdraw-gift sequence, and Alice's pairwise-FIFO processing order
are encoded as 14 Veil actions whose preconditions capture A1 (pairwise
FIFO) and A3 (gift availability) of the informal proof.
The verified safety property:
phase1 m1 ∧ phase2 m2 ∧ processed m2 → processed m1
i.e. once Alice has dispatched any phase-2 reference message, every phase-1
reference message has likewise been dispatched - the cross-phase end-to-end
FIFO claim. The two-fence chain from the informal proof is captured by 8
inductive-invariant clauses; #check_invariants emits 144 SMT obligations and
discharges them all (Z3/CVC5).
A 15-step BMC trace witnesses that the protocol admits a non-trivial happy-
path execution.
See packages/ocapn/proofs/veil/README.md for build instructions and a
mapping back to the informal proof's "Sandwich Lemma".
Add .github/workflows/ocapn-flush-proof.yml. The job runs on PRs (and on master pushes) that touch packages/ocapn/proofs/, sets up Lean 4 via leanprover/lean-action, fetches Veil + transitive deps with `lake update`, and runs `lake build OcapnFlush.Flush` while capturing the build log. After the build completes the workflow asserts the verification shape: - no clause in the inductive-invariant table reports ❌, - at least one ✅ marker is present (guards against the `#check_invariants` step silently disappearing), - Veil's "Trusting the SMT solver for N theorems" line is emitted, and - exactly two `sorry`-admitted declarations remain in the proof file (`prove_inv_inductive` and `sat trace [happyPath]`, both documented in the README and corresponding to claims the SMT solver has already validated). Veil's downloadDependencies step also pulls `uv` from astral.sh; the job pre-installs `uv` via pip and stages it into the expected build path so the toolchain bootstrap is robust against astral outages. The build log is uploaded as an artifact for postmortem.
kumavis
force-pushed
the
claude/ocapn-flush-veil-proof
branch
from
49bbf40 to
c6d5619
Compare
The repo's GitHub Actions runtime policy forbids any non-pinned action, including transitively-referenced ones inside composite actions. The leanprover/lean-action@v1.5.0 composite calls `actions/cache/restore@v5` (no SHA), so the workflow failed to start even though lean-action's own SHA was pinned. Replace the lean-action step with a self-contained installer that parses `lean-toolchain`, downloads the matching Lean release tarball from GitHub (which is allowed), extracts it, and adds the bin dir to PATH. Reorder the uv pre-stage to run after `lake update`, since the .lake/packages/veil tree only exists after dependency resolution.
…trivial interleavings Add OcapnFlush/FourParty.lean: a Veil model of two sequential flush + handoff cycles in a chain Alice / Bob / Carol / Dave. Bob hands the reference to Carol via the existing flush handshake, then Carol in turn hands it to Dave via a second flush handshake. Reference messages are partitioned into three phases (phase1 = Bob's pre-flush messages, phase2 = Carol's between-handoffs messages, phase3 = Dave's post-handoff messages). The key new fact the model exercises is that phase-2 traffic may flow freely while Carol is preparing and running her own flush — the action preconditions deliberately do *not* require phase-2 to be drained before Carol initiates her flush. The fence chain doubles up: one B↔A chain transitions phase1→phase2, one C↔A chain transitions phase2→phase3. The linking invariant `cdFlushSentByC → cHoldsRef` is what forces Carol's flush to be causally downstream of Bob's handoff, letting the two chains compose. Verification: - `#check_invariants` emits 580 SMT obligations (init + actions × 21 invariant clauses + 3 safety clauses), all `✅`. - `sat trace [twoShortenings]` runs a 30-step trace where Carol's flush initiation is interleaved between the first phase-2 send and its Alice-side processing. Same `sorry` footprint as Flush.lean: `prove_inv_inductive` and the `sat trace` BMC are admitted to the SMT solver via Veil's `reconstructProofs := false`. Update the CI workflow to build the entire library (not just Flush.lean) and to count admitted-declaration sorrys per module (currently 2 per file). Update the README accordingly, including a discussion of which interleavings the new module covers and which (fully-symmetric concurrent flushes at adjacent intermediaries) it does not.
kumavis
force-pushed
the
claude/implement-ocapn-flush-iisn9
branch
3 times, most recently
from
ee674ad to
19c0bbf
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Stacks on top of #3248 with a mechanized proof, in Lean 4 + Veil, of the central per-reference FIFO claim that motivates the
op:flushwork in #3248.packages/ocapn/proofs/veil/is a self-contained Lake project that models a 3-party Alice / Bob / Carol abstraction of OCapN's flush-based promise-shortening protocol and discharges the cross-phase FIFO safety claim by SMT (Z3 / CVC5) via Veil's#check_invariantsmechanism.What is verified
For Bob's reference messages targeted at Alice's exported promise
p1, partitioned into:op:flush, traveling B→A.The safety property is the cross-phase end-to-end FIFO claim:
i.e. once Alice has dispatched any phase-2 reference message to the entity, every phase-1 message has also been dispatched. This is the formal counterpart of the informal "Sandwich Lemma" in the proof reports already discussed on #3248.
How
OcapnFlush/Flush.leandeclares a Veil transition system with:processed, and protocol-event flags;op:flushsend, Alice's swap, Bob's deposit-gift / handoff-give, Carol's withdraw-gift, etc.); each action's preconditions encode pairwise FIFO (A1) and the gift-availability gate (A3);flushProcessedAtA → flushSentByBflushProcessedAtA → (phase1 M → processed M)— flush fencedepositGiftProcessedAtA → flushProcessedAtA— B→A FIFOwithdrawGiftProcessedAtA → depositGiftProcessedAtA— gift availabilitycHoldsRef → withdrawGiftProcessedAtAphase2 M ∧ processed M → withdrawGiftProcessedAtA— C→A FIFOprocessed M → (phase1 M ∨ phase2 M)¬ (phase1 M ∧ phase2 M)#check_invariantsproduces 144 SMT obligations (init + every clause × every action + safety) and reports✅for every one. Asat trace [happyPath]BMC obligation also confirms the protocol admits a 15-step non-trivial execution that ends with both a phase-1 and a phase-2 message processed.The
prove_inv_inductiveandsat traceblocks are admitted withsorry(Veil'sreconstructProofs := false), since the SMT verification — not Lean proof-term reconstruction — is Veil's verification of record. The README explains.What is not in this model
Build / install
The README documents the install process. On a vanilla machine:
uv(used by Veil for SMT-model wrappers) needs to be reachable; ifastral.shis blocked you can install it viapip install uvand copy the binary into.lake/packages/veil/.lake/build/uv. Output ends with:Test plan
lake build OcapnFlush.Flushsucceeds; all 144 SMT clauses reported✅.sat trace [happyPath]BMC trace produces a satisfying 15-step execution.https://claude.ai/code/session_013hZeUaQrKVRoZQjpd1vcs4
Generated by Claude Code