Repository navigation
Asynchrony: K-CUT-LOSS survives, transport becomes directional (I3a) - #35
Merged
Merged
Conversation
Fixes, before any proof, the asynchronous model (cuts whose messages and selections are delivered or in flight; the receiver of a message in flight does nothing later), the accounting (the sender pays at send, the receiver at receipt; bounds use the sent-so-far grade of the completion), and the reading of the 2026-10-12 falsifier: the sender of a message knows it was received synchronously, and is predicted not to know it asynchronously until a reply arrives. Eight claims, Y-1 to Y-8, each with its falsifier. The proofs follow in a later commit and are recorded against these statements in PROOF-STATUS. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Ladder increment I3a, against the claims pre-registered in the previous commit (docs/pre-registration-addendum-2026-10-19.adoc). All eight came out as pre-registered. Async.agda: cuts whose messages and selections are delivered or in flight; the receiver of anything in flight does nothing later (Causal). Synchronous cuts are exactly the cuts with nothing in flight, and every notion agrees on them (Y-1). K-CUT-LOSS holds with the sender paying at send and the receiver at receipt, from the same two laws as K-1; scripts/minimal-laws.sh now certifies that too (Y-2). Delivering a message in flight changes only its receiver's local cut (Y-3). AsyncKnowledge.agda: the Kripke frame over asynchronous worlds. LOSS => WARRANT and knowledge of the own frontier survive (Y-4). The receiver of a protocol's first message knows it was sent (Y-5). Its sender does not know it was received at any world where the receiver has done nothing since, although the same proposition is a theorem in the synchronous frame (Y-6): the pre-registered falsifier, confirmed. AsyncBound.agda: both bounds survive against the sent-so-far grade, the completion's (Y-7). Instances.agda: discharges at Loss, MaxPlus and HWM; a concrete witness; in 0 -> 1 . 1 -> 0, a received reply gives the sender knowledge of receipt, and a reply still in flight does not (Y-8). tests/reject/SenderKnowsReceipt.agda: the claim is refused. PROOF-STATUS gains the "Asynchrony" section and "What Y-6 says about the keystone"; README, EXPLAINME, ARCHITECTURE and the changelog no longer list asynchrony as open, and say what remains. scripts/check.sh passes (core, echo-additive instance, 5 expected rejections), scripts/minimal-laws.sh passes for KCut and Async, the documentation guard and 27 tests pass, and the 25 locally runnable estate gates pass. --safe --without-K, no postulates. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Contributor
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 15
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
hyperpolymath
marked this pull request as ready for review
October 19, 2026 16:27
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4ace0af985
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Codex review on #35: README, keystone section, EXPLAINME, ARCHITECTURE and the changelog stated 'receipt is unknown until a reply arrives' as a general result. The proofs cover the protocol's first message while its receiver has done nothing since (Y-6) and the two-message protocol (Y-8). The wording now says so and names the open forms. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
|
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
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
Ladder increment I3a: asynchrony. The first commit is the pre-registration (
docs/pre-registration-addendum-2026-10-19.adoc). It fixes the model, the accounting, the reading of the 2026-10-12 falsifier, and claims Y-1 to Y-8 with their falsifiers, before any proof. The second commit is the proofs. All eight claims came out as pre-registered.The headline: K-CUT-LOSS survives asynchrony unchanged, and the transport half of K-CUT-WARRANT becomes directional.
That is the falsifier pre-registered on 2026-10-12, confirmed.
Type of change
What is proved
Async.agdagrade↾ₐ p G κ ≡ lgrade (aview p G κ)for every causal cut consistent for p. The sender pays at send, the receiver at receipt. Parametric, discharged at Loss/MaxPlus/HWM, from the same two laws as K-1Async.agda,Instances.agda;scripts/minimal-laws.shnow also checksAsync.agdaAsync.agdaSoundWarrantin epistemic-types' interface) and knowledge of the own frontier surviveAsyncKnowledge.agdaAsyncKnowledge.agdaAsyncKnowledge.agda,Instances.agda,tests/reject/SenderKnowsReceipt.agdaAsyncBound.agda,Instances.agda0 → 1 : a . 1 → 0 : b, a received reply gives the sender knowledge of receipt; a reply in flight does not (any algebra, any grades)Instances.agdaPROOF-STATUS gains the "Asynchrony" section and a short "What Y-6 says about the keystone". README, EXPLAINME, ARCHITECTURE and the changelog no longer list asynchrony as open. Each now says what remains: the position-indexed form of Y-5/Y-6, the general form of Y-8 (message chains), queues as data, and asynchrony with recursion.
How has this been verified?
All of the following were re-run on this branch after it was rebuilt on
mainat08f8f00.scripts/check.sh, locally in Agda 2.6.4.3 with agda-stdlib 2.1-4 (the gate's pins): it passes for the core, the echo-additive instance and 5 expected rejections. The new rejection fails at itsinvalidline with⊤ !=< Delivered (AWorld.acut w').scripts/minimal-laws.shpasses forKCut.agdaand now forAsync.agda.--safe --without-K; no postulates undersrc/ortests/; no matching on equalities of abstract grades.node scripts/check-repository.mjspasses. The ledger binding was checked to catch a broken Y-row citation.Checklist
--safe --without-K, no postulates, every cited definition carries its-- Ledger Y-n.lineNotes for reviewers
sender-knowsas the falsifier. Read literally, the T-2 fixtures are "a party knows its own frontier", and that cannot break. The pre-registration fixes the reading before any proof: the sender knows the message was received.Quietreads the receiver's local cut, which at a choice it is outside of shows only the left branch. Worlds also require plain merge for every party, which makes the branches agree. The module comment says so.mainafter CI: the lock is accepted at job setup again (required checks, Scorecard) #34 merged. Two commits, pre-registration first; please keep them separate (rebase or merge commit) so the order stays on record.Generated by Claude Code
Summary by CodeRabbit