From ce9c2ac20afc10f81de44d643fbce7a4fa2073ec Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 12:04:15 +0000 Subject: [PATCH 1/3] Pre-register ladder increment I3a: asynchrony 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 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- .../pre-registration-addendum-2026-10-19.adoc | 110 ++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 docs/pre-registration-addendum-2026-10-19.adoc diff --git a/docs/pre-registration-addendum-2026-10-19.adoc b/docs/pre-registration-addendum-2026-10-19.adoc new file mode 100644 index 0000000..7be8111 --- /dev/null +++ b/docs/pre-registration-addendum-2026-10-19.adoc @@ -0,0 +1,110 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Pre-registration addendum — 2026-10-19 (ladder increment I3a: asynchrony) +:revdate: 2026-10-19 + +This addendum fixes the model, the accounting and the claims of the first +I3 increment before any of it is proved. It is committed ahead of the +proofs. Whatever the proofs then show, including any claim that fails, is +recorded against these statements in PROOF-STATUS.adoc, section +"Asynchrony". + +== The model, fixed before proving + +* *Asynchronous cut.* As before, a cut is a prefix of the global type's + tree. Now each message, and each choice's selection, inside the prefix is + either *delivered* or *in flight*: sent, not yet received. +* *Causality.* The receiver of a message in flight does nothing later in + the prefix. Its own timeline is blocked at the pending receive, and it + cannot send what it has not yet been told. Nothing else is constrained: + the sender, and every other party, carries on. +* *Projection.* The sender's local cut includes the send. The receiver's + local cut stops before the receive. An outsider's is unchanged. Plain + merge at choices a party is outside of is stated on the parties' views, + as `Consistent` is for synchronous cuts. +* *Worlds* are causal asynchronous cuts that are consistent for every + party. As before, two worlds are indistinguishable to a party when its + view is the same. + +== The accounting, fixed before proving + +With messages in flight, "the global grade up to the cut" splits into a +sent-so-far grade and a received-so-far grade, and the bound theorems (W-4, +W-5) have to say which they mean. Fixed here: + +* *A party's restricted grade.* The sender pays an interaction's grade + when it sends, and the receiver when it receives. A message in flight has + been paid for by its sender only. +* *The global grade in the bounds* is the *sent-so-far* grade: the grade of + the synchronous cut obtained by delivering everything in flight (the + *completion*). A received-so-far grade would have to drop messages from + the middle of the prefix, and a dropped middle message leaves no prefix of + the global type. It is not defined in this increment. + +== The falsifier's reading, fixed before proving + +The 2026-10-12 addendum said asynchrony should break `sender-knows` and keep +`receiver-knows`. Both T-2 fixtures are instances of "a party knows its own +frontier", and that cannot break: a party's view is its own frontier. The +symmetric statement synchronous K-CUT actually makes is about the *other* +end of a message, and it is read as follows: + +* *receiver-knows:* the receiver of a message knows it was sent. Predicted + to hold asynchronously. +* *sender-knows:* the sender of a message knows it was received. This holds + synchronously, where a message is one event for both ends. Predicted to + fail asynchronously at every world where the receiver has done nothing + since the message, because no reply has come back. + +== Claims, each with its falsifier + +Y-1:: *Conservativity.* Synchronous cuts are exactly the asynchronous cuts +with nothing in flight. Projection, consistency and the restricted grade +agree with their synchronous counterparts there, and they are causal. +_Falsifier:_ an embedded synchronous cut whose asynchronous projection, +consistency or grade differs. +Y-2:: *Asynchronous K-CUT-LOSS.* For every causal cut consistent for p, +p's restricted grade under the split accounting equals the grade of p's +local view. It is parametric in the resource algebra and uses the same two +laws as K-1 (⊗ left unit, ⊕ idempotence). _Falsifier:_ such a cut where the +two differ, or a proof that needs a third law. +Y-3:: *In-flight invisibility.* Delivering a message in flight changes no +party's view except its receiver's. _Falsifier:_ any other party whose view +changes. +Y-4:: *The asynchronous frame.* "Loss implies warrant" survives (p knows +its own restricted grade), and so does knowledge of the own frontier +(T-2). _Falsifier:_ a world where p's own grade or frontier differs between +two worlds p cannot tell apart. +Y-5:: *Receiver knows sent.* At every world where the first message of a +protocol has been delivered, its receiver knows it was delivered, and so +that it was sent. _Falsifier:_ a receiver-indistinguishable world where it +was not sent. +Y-6:: *Sender does not know receipt.* At every world where the first +message has been delivered but its receiver has done nothing since, the +sender does not know it was received. The same proposition is a theorem in +the synchronous frame. _Falsifier:_ asynchronous knowledge of receipt +without a reply. If that were provable, asynchrony would not separate the +two ends of a message, and the prediction would be refuted. +Y-7:: *Bounds survive with sent-so-far accounting, in both directions.* +If every grade is ≽ 𝟙, p's restricted grade is a known lower bound on the +sent-so-far grade. If every grade is ≼ 𝟙, it is a known upper bound. These +are the W-4 and W-5 analogues; a receiver that lags behind its messages is +the case to watch. _Falsifier:_ a lagging receiver for which the bound +fails. +Y-8:: *A reply restores the knowledge.* In a protocol where the receiver +answers, the sender knows its message was received once the answer has +arrived. _Falsifier:_ a world consistent with the sender's view in which the +answer arrived but the first message was not delivered. + +== Scope + +* Asynchronous cuts cover the whole fragment, choices included: a + selection can be in flight. Y-1 to Y-4 and Y-7 are stated for all of it. +* Y-5 and Y-6 are stated for the first message of an arbitrary protocol. + Deeper messages reduce to that case through delivered prefixes, but the + general position-indexed statement is not attempted here. +* Y-8 is a single protocol, checked exhaustively over its worlds. The + general statement, that knowledge of receipt needs a chain of messages + back, is not attempted here. +* Unchanged: no recursion, no full merge, no delegation. Queues are not + data: an asynchronous cut records what is in flight, not how it is + buffered. From 4ace0af985d4a5038fc8e7b1406906ab2ef2dba7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 12:20:57 +0000 Subject: [PATCH 2/3] Asynchrony: K-CUT-LOSS survives, transport becomes directional (I3a) 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 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- ARCHITECTURE.adoc | 5 + EXPLAINME.adoc | 29 ++- PROOF-STATUS.adoc | 65 +++++- README.adoc | 14 +- docs/CHANGELOG-entry.adoc | 25 +++ docs/README-keystone-section.adoc | 14 +- scripts/minimal-laws.sh | 9 +- src/Choreographic/All.agda | 3 + src/Choreographic/Async.agda | 308 ++++++++++++++++++++++++++ src/Choreographic/AsyncBound.agda | 91 ++++++++ src/Choreographic/AsyncKnowledge.agda | 167 ++++++++++++++ src/Choreographic/Instances.agda | 110 ++++++++- src/Choreographic/Transport.agda | 3 +- tests/reject/SenderKnowsReceipt.agda | 24 ++ 14 files changed, 834 insertions(+), 33 deletions(-) create mode 100644 src/Choreographic/Async.agda create mode 100644 src/Choreographic/AsyncBound.agda create mode 100644 src/Choreographic/AsyncKnowledge.agda create mode 100644 tests/reject/SenderKnowsReceipt.agda diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index eb56635..8ae4f18 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -69,6 +69,11 @@ the siblings it imports, and the gate that checks it. `Bound` and `Transport` prove K-CUT-WARRANT in bound form and its transport component, instantiating `epistemic-types`' `Warrant`, `SoundWarrant` and `Access.Preorder` rather than imitating them. +. *Asynchrony* — `Async` adds cuts whose messages and selections are + delivered or in flight, and proves K-CUT-LOSS for them; `AsyncKnowledge` + is the Kripke frame over them (the receiver of a message knows it was + sent, its sender does not know it was received); `AsyncBound` is the + bound against the sent-so-far grade. . *Instances and applications* — `Instances` discharges the keystone at the three estate algebras and computes a worked protocol; `Swap` and `Operational` read the RapidNJ two-thread diamond at the type level; diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 040c427..c0849b1 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -28,9 +28,10 @@ is the local side, `src/Choreographic/Projection.agda` endpoint projection with plain merge, cut projection and `Consistent`. Caveat:: -The fragment is finite, binary-choice, plain-merge and synchronous. There is -no recursion, no full merge, no delegation, no asynchrony. Warrants are what -the type determines (`src/Choreographic/Kripke.agda`); data-dependent +The fragment is finite, binary-choice and plain-merge. There is no +recursion, no full merge, no delegation. Asynchrony is a layer over the same +fragment (`src/Choreographic/Async.agda`): messages and selections in +flight, not queues as data. Warrants are what the type determines (`src/Choreographic/Kripke.agda`); data-dependent warrants are outside the model. === K-CUT-LOSS holds as equality @@ -47,9 +48,11 @@ How this is implemented:: proof uses only ⊕-idempotence and ⊗-left-unit. Caveat:: -**Proved for the fragment only.** Beyond it (recursion, full merge, -asynchrony) K-CUT-LOSS is open and pre-registered with its falsifiers -(`docs/pre-registration-addendum-2026-10-12.adoc`). +**Proved for the fragment only**, synchronously and, with the sender paying +at send and the receiver at receipt, asynchronously (`akcut-loss` in +`src/Choreographic/Async.agda`, from the same two laws). Beyond it +(recursion, full merge) K-CUT-LOSS is open and pre-registered with its +falsifiers (`docs/pre-registration-addendum-2026-10-12.adoc`). === K-CUT-WARRANT holds as a bound, with its transport component @@ -68,8 +71,12 @@ access as epistemic-types' `Preorder`; a world-indexed `AccessibleModality`). Caveat:: **Same fragment.** `SoundWarrant` is discharged only for warrants the choreography determines; for anything about payloads it stays an -assumption. Asynchrony is expected to break the sender half of the transport -result and is the pre-registered falsifier. +assumption. Asynchronously the transport result is directional, as +pre-registered (`docs/pre-registration-addendum-2026-10-19.adoc`): the +receiver of a message knows it was sent, its sender does not know it was +received until a reply arrives (`src/Choreographic/AsyncKnowledge.agda`), +and the bound survives against the sent-so-far grade +(`src/Choreographic/AsyncBound.agda`). === The resource algebra is imported, the tropical bridge is named @@ -123,8 +130,10 @@ structural and is never evidence that anything is proved. [CAUTION] ==== -**K-CUT is open beyond the fragment.** Recursion, full merge, asynchrony and -data-dependent warrants are pre-registered, not proved. +**K-CUT is open beyond the fragment.** Recursion, full merge and +data-dependent warrants are pre-registered, not proved. Asynchrony is in +for messages in flight; its knowledge results are stated for a protocol's +first message (PROOF-STATUS, "Asynchrony"). ==== [CAUTION] diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index c8bca5d..e281a18 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= choreographic-types — Proof Status (K-CUT development, 2026-10-13) -:revdate: 2026-10-13 += choreographic-types — Proof Status (K-CUT development, 2026-10-19) +:revdate: 2026-10-19 Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line names the module that discharges it under @@ -25,10 +25,11 @@ projection with *plain merge* (a non-participant's two branches must project identically); cuts as frontiers (`stop` / `cont-*`); consistent cuts = plain merge still holds on the truncated branches. Grades are drawn from any `ResourceAlgebra`. *Not* in the fragment: recursion (μ-types), -full merge, delegation, asynchrony/queues, n-ary choice (a fold of binary), -delegation, and data-dependent warrants (the frame carries only what the -type determines). Both components of K-CUT-WARRANT — bound and transport -— are in, for this fragment. +full merge, delegation, n-ary choice (a fold of binary), queues as data, +and data-dependent warrants (the frame carries only what the type +determines). Both components of K-CUT-WARRANT — bound and transport — are +in, for this fragment. Asynchrony, with messages and selections in flight, +is a layer over the same fragment (section "Asynchrony" below). == Keystone @@ -74,6 +75,37 @@ epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit | T-6 | epistemic-types' `AccessibleModality` cannot be instantiated as stated: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the mismatch is a finding for epistemic-types |=== +== Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda) + +Ladder increment I3a, pre-registered before any proof in +link:docs/pre-registration-addendum-2026-10-19.adoc[]. A cut is still a +prefix of the global type's tree, but each message and each selection in it +is delivered or in flight, and the receiver of anything in flight does +nothing later in the prefix (`Causal`). The sender pays an interaction's +grade at send, the receiver at receipt (`grade↾ₐ`). Worlds are causal cuts +consistent for every party; accessibility is sameness of view, as in W-1. +All eight claims came out as pre-registered. + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| Y-1 | Conservativity: synchronous cuts are exactly the asynchronous cuts with nothing in flight (`Settled`). Embedding lands in them, and on them completion (deliver everything in flight) is its inverse. Embedding preserves projection, consistency, causality and the restricted grade | PROVEN (`Async.embed-settled`, `complete-embed`, `embed-complete`, `acutproj-embed`, `embed-consistent`, `embed-causal`, `grade↾ₐ-embed`) +| Y-2 | *Asynchronous K-CUT-LOSS*: for every causal cut κ consistent for p, `grade↾ₐ p G κ ≡ lgrade (aview p G κ)`, parametric in the resource algebra and discharged at the three instances. It uses the same two laws as K-1: a receiver still waiting is quiet, so its continuation contributes 𝟙 | PROVEN (`Async.akcut-loss`; `Instances.akcut-loss-Loss`, `akcut-loss-MaxPlus`, `akcut-loss-HWM`); TESTED (`scripts/minimal-laws.sh` checks Async.agda against the two-law Core) +| Y-3 | In-flight invisibility: delivering a message or selection in flight changes no party's local cut but its receiver's | PROVEN (`Async.flight-invisible`, `flight-invisible-choice`) +| Y-4 | The asynchronous frame. LOSS ⇒ WARRANT survives: p knows its own restricted grade and holds a sound warrant for it in epistemic-types' interface. p also knows its own frontier (T-2) | PROVEN (`AsyncKnowledge.AFrame`, `aknows-own-grade`, `asound-warrant`, `aknows-local-cut`) +| Y-5 | *Receiver knows sent*: at every world where a protocol's first message s → r (s ≢ r) is delivered, its receiver knows it was delivered, and so that it was sent | PROVEN (`AsyncKnowledge.receiver-knows-delivered`, `receiver-knows-sent`) +| Y-6 | *Sender does not know receipt*, the pre-registered falsifier, confirmed. At every world where the first message is delivered and its receiver has done nothing since, the world where it is still in flight looks the same to every party but the receiver, so the sender does not know it was received. In the synchronous frame the same proposition is a theorem | PROVEN (`AsyncKnowledge.only-receiver-sees`, `sender-cannot-know-receipt`, `sync-sender-knows-receipt`); TESTED (`Instances.sender-blind`, `receiver-sees`, `sender-cannot-know`; `tests/reject/SenderKnowsReceipt`) +| Y-7 | Both bounds survive against the sent-so-far grade `gradeₛ` (the completion's): if every grade is ≽ 𝟙, p's restricted grade is a known lower bound; if every grade is ≼ 𝟙, a known upper bound. A receiver that lags has paid 𝟙 where the completion pays g, which is on the side each bound needs. Discharged as W-6 | PROVEN (`AsyncBound.grade↾ₐ-≼`, `≼-grade↾ₐ`, `grade↾ₐ-≼ₛ`, `gradeₛ-≼↾ₐ`, `aknows-lower-bound`, `aknows-upper-bound`; `Instances.async-warrant-HWM`, `async-warrant-Loss`, `async-warrant-MaxPlus`) +| Y-8 | *A reply restores the knowledge.* In `0 → 1 : a . 1 → 0 : b`, for every resource algebra and grades a, b: once the reply has been received, 0 knows its message was delivered, because a reply can only come from a receiver that has acted. A reply still in flight is not enough | PROVEN (`Instances.reply-gives-knowledge`, `reply-in-flight-is-not-enough`) +|=== + +Not claimed: a statement for messages other than a protocol's first (they +reduce to it through delivered prefixes, but the position-indexed theorem is +not written), the general form of Y-8 (knowledge of receipt exactly when a +chain of messages leads back from it), and a received-so-far global grade, +which would drop messages from the middle of the prefix and so is not a +prefix of the global type. + == Applications: the two-thread diamond (Swap.agda) `applications/rapidnj-two-thread.agda` states the first application target @@ -148,10 +180,11 @@ Client 0, broker 1, server 2: `0→1:a . 1→2:b . 0→2 chooses {2→1:c | 2→ * *Data-dependent warrants.* The frame carries only what the type determines; warrants about payloads are outside it, and there `SoundWarrant` stays an assumption — with a precise scope (W-2, T-2). -* *Asynchrony.* With queues, T-2's sender half (`sender-knows`) is expected - to fail: a send without receipt is a world the sender cannot distinguish - from one with receipt. Pre-registered as the falsifier that separates - synchronous from asynchronous K-CUT. +* *Asynchrony beyond I3a.* Messages in flight are in (Y-1 to Y-8), and the + pre-registered falsifier came out as predicted (Y-6). Still open: the + position-indexed form of Y-5 and Y-6, the general form of Y-8 (knowledge + of receipt needs a chain of messages back), queues as data, and + asynchrony combined with recursion. * *Recursion.* μ-types change `Cut` (a frontier through an unfolding) and need a coinductive or fuel-indexed grade. Not attempted. * *Full merge.* Only plain merge. Full merge (branches may differ in labels @@ -183,6 +216,18 @@ and MaxPlus p's view is a *lower* bound on the global grade; in Loss it is an *upper* bound in ≼, i.e. numerically p's view accounts for no more loss than the global total. Any K-CUT-WARRANT statement must say which. +== What Y-6 says about the keystone + +Synchronously, a message is one event for both of its ends, and T-2's two +halves (receiving is knowing it was received; sending is knowing it was +sent) say the same thing twice. Asynchronously they come apart. The +receiver's knowledge that the message was sent survives (Y-5), because a +receive is causally after its send. The sender's knowledge that it was +received does not (Y-6), and comes back only when something the receiver +did after the receipt reaches the sender (Y-8). The transport component of +K-CUT-WARRANT is therefore directional, and synchrony was what hid the +direction. The loss component is not: Y-2 needs no new law. + == What K-4 says about the keystone That K-CUT-LOSS survives with only idempotence and a left unit means the diff --git a/README.adoc b/README.adoc index 1ccbe40..bc5e08d 100644 --- a/README.adoc +++ b/README.adoc @@ -45,8 +45,10 @@ K-CUT-LOSS:: parametric in any `ResourceAlgebra` (`src/Choreographic/KCut.agda`, `kcut-loss`), discharged at the Loss, MaxPlus and HWM instances. Uses only ⊕-idempotence and ⊗-left-unit - (certified by `scripts/minimal-laws.sh`). Recursion, full merge and - asynchrony remain OPEN. See link:PROOF-STATUS.adoc[]. + (certified by `scripts/minimal-laws.sh`). It holds asynchronously too, + with messages in flight, the sender paying at send and the receiver at + receipt, from the same two laws (`src/Choreographic/Async.agda`, + `akcut-loss`). Recursion and full merge remain OPEN. See link:PROOF-STATUS.adoc[]. K-CUT-WARRANT:: Warrant transport commutes with projection only as a *bound*, and only under a `SoundWarrant` side-condition. @@ -60,8 +62,12 @@ K-CUT-WARRANT:: at every world (receiving is knowing it was received), party access "q sees at least what p sees" is epistemic-types' `Preorder` instantiated, and knowledge is monotone along it — a lawful world-indexed - `AccessibleModality`. OPEN beyond the fragment: recursion, full merge, - asynchrony, data-dependent warrants. See link:PROOF-STATUS.adoc[]. + `AccessibleModality`. Asynchronously (`src/Choreographic/AsyncKnowledge.agda`, + `src/Choreographic/AsyncBound.agda`) the bound survives against the + sent-so-far grade and the receiver of a message knows it was sent, but its + sender does not know it was received until a reply arrives: the + pre-registered falsifier, confirmed. OPEN beyond the fragment: recursion, + full merge, data-dependent warrants. See link:PROOF-STATUS.adoc[]. [NOTE] ==== diff --git a/docs/CHANGELOG-entry.adoc b/docs/CHANGELOG-entry.adoc index 3f7b7d5..b1324e2 100644 --- a/docs/CHANGELOG-entry.adoc +++ b/docs/CHANGELOG-entry.adoc @@ -1,3 +1,28 @@ +== 2026-10-19 — asynchrony (ladder increment I3a) + +* `docs/pre-registration-addendum-2026-10-19.adoc`, committed before the + proofs: the asynchronous model, the accounting (the sender pays at send, + the receiver at receipt; bounds use the sent-so-far grade), the reading of + the 2026-10-12 falsifier, and claims Y-1 to Y-8 with their falsifiers. +* `src/Choreographic/Async.agda`: cuts whose messages and selections are + delivered or in flight, with causality; conservativity over synchronous + cuts; asynchronous K-CUT-LOSS from the same two laws, which + `scripts/minimal-laws.sh` now also certifies; in-flight invisibility. +* `src/Choreographic/AsyncKnowledge.agda`: the frame over asynchronous + worlds. The receiver of a delivered message knows it was sent; its sender + does not know it was received while the receiver has done nothing since, + although the same proposition is a theorem synchronously. This is the + pre-registered falsifier, confirmed. +* `src/Choreographic/AsyncBound.agda`: both bounds against the sent-so-far + grade. +* `src/Choreographic/Instances.agda`: discharges at Loss, MaxPlus and HWM; a + concrete witness; a reply restores the sender's knowledge, and a reply + still in flight does not. +* `tests/reject/SenderKnowsReceipt.agda`: the sender's knowledge of receipt + is refused. +* PROOF-STATUS: section "Asynchrony", rows Y-1 to Y-8, and "What Y-6 says + about the keystone". + == 2026-10-14 — the ledger is bound to the code * `scripts/check-repository.mjs`: every name a PROVEN or TESTED row of diff --git a/docs/README-keystone-section.adoc b/docs/README-keystone-section.adoc index 9407140..acf6b35 100644 --- a/docs/README-keystone-section.adoc +++ b/docs/README-keystone-section.adoc @@ -12,8 +12,10 @@ K-CUT-LOSS:: parametric in any `ResourceAlgebra` (`src/Choreographic/KCut.agda`, `kcut-loss`), discharged at the Loss, MaxPlus and HWM instances. Uses only ⊕-idempotence and ⊗-left-unit - (certified by `scripts/minimal-laws.sh`). Recursion, full merge and - asynchrony remain OPEN. See link:../PROOF-STATUS.adoc[]. + (certified by `scripts/minimal-laws.sh`). It holds asynchronously too, + with messages in flight, the sender paying at send and the receiver at + receipt, from the same two laws (`src/Choreographic/Async.agda`, + `akcut-loss`). Recursion and full merge remain OPEN. See link:../PROOF-STATUS.adoc[]. K-CUT-WARRANT:: Warrant transport commutes with projection only as a *bound*, and only under a `SoundWarrant` side-condition. @@ -27,8 +29,12 @@ K-CUT-WARRANT:: at every world (receiving is knowing it was received), party access "q sees at least what p sees" is epistemic-types' `Preorder` instantiated, and knowledge is monotone along it — a lawful world-indexed - `AccessibleModality`. OPEN beyond the fragment: recursion, full merge, - asynchrony, data-dependent warrants. See link:../PROOF-STATUS.adoc[]. + `AccessibleModality`. Asynchronously (`src/Choreographic/AsyncKnowledge.agda`, + `src/Choreographic/AsyncBound.agda`) the bound survives against the + sent-so-far grade and the receiver of a message knows it was sent, but its + sender does not know it was received until a reply arrives: the + pre-registered falsifier, confirmed. OPEN beyond the fragment: recursion, + full merge, data-dependent warrants. See link:../PROOF-STATUS.adoc[]. [NOTE] ==== diff --git a/scripts/minimal-laws.sh b/scripts/minimal-laws.sh index b3c4d8d..1ceb5ed 100755 --- a/scripts/minimal-laws.sh +++ b/scripts/minimal-laws.sh @@ -1,8 +1,9 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 -# Certifies which algebra laws K-CUT-LOSS depends on: KCut.agda is checked -# against tests/minimal-laws, a Core whose record has ONLY ⊕-idempotence and -# ⊗-left-unit. If this passes, no other law is used (PROOF-STATUS K-4). +# Certifies which algebra laws K-CUT-LOSS depends on: KCut.agda, and its +# asynchronous counterpart Async.agda, are checked against tests/minimal-laws, +# a Core whose record has ONLY ⊕-idempotence and ⊗-left-unit. If this +# passes, no other law is used (PROOF-STATUS K-4, Y-2). set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." export LC_ALL="${LC_ALL:-C.UTF-8}" @@ -14,3 +15,5 @@ cp "$ra/ResourceAlgebra/Prelude.agda" "$tmp/ResourceAlgebra/" cp tests/minimal-laws/ResourceAlgebra/Core.agda "$tmp/ResourceAlgebra/" "$prover" --safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/KCut.agda echo "PASS: K-CUT-LOSS typechecks with only ⊕-idempotence and ⊗-left-unit" +"$prover" --safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/Async.agda +echo "PASS: asynchronous K-CUT-LOSS typechecks with only ⊕-idempotence and ⊗-left-unit" diff --git a/src/Choreographic/All.agda b/src/Choreographic/All.agda index 95bb262..a0f9c16 100644 --- a/src/Choreographic/All.agda +++ b/src/Choreographic/All.agda @@ -9,4 +9,7 @@ import Choreographic.Party import Choreographic.Instances -- instantiates Global/Local/Projection/KCut/Kripke/Bound/Transport import Choreographic.Swap -- (parametric; instantiated in Instances.Diamond) import Choreographic.Operational -- (parametric; instantiated in Instances.GradeNotStateInvariant) +import Choreographic.Async -- (parametric; instantiated in Instances, with AsyncKnowledge +import Choreographic.AsyncKnowledge -- and AsyncBound) +import Choreographic.AsyncBound import Choreographic.Base.RoleGraded diff --git a/src/Choreographic/Async.agda b/src/Choreographic/Async.agda new file mode 100644 index 0000000..b1df7e4 --- /dev/null +++ b/src/Choreographic/Async.agda @@ -0,0 +1,308 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Asynchronous cuts (ladder increment I3a; pre-registered in +-- docs/pre-registration-addendum-2026-10-19.adoc). +-- +-- A cut is still a prefix of the global type's tree, but each message and +-- each selection in it is either delivered or in flight: sent, not yet +-- received. The receiver of a message in flight does nothing later in the +-- prefix (`Causal`): its timeline is blocked at the pending receive. The +-- sender pays an interaction's grade when it sends and the receiver when it +-- receives (`grade↾ₐ`). +-- +-- embed, complete synchronous cuts are the cuts with nothing in flight; +-- completion delivers everything in flight +-- akcut-loss K-CUT-LOSS for asynchronous cuts, from the same two +-- laws as K-1: ⊗ left unit and ⊕ idempotence +-- flight-invisible delivering a message changes only its receiver's +-- local cut +-- +-- Like KCut.agda, this module is also checked against a Core with only those +-- two laws (scripts/minimal-laws.sh). +open import ResourceAlgebra.Core + +module Choreographic.Async (R : ResourceAlgebra) where + +open import ResourceAlgebra.Prelude +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Local R +open import Choreographic.Projection R +open import Choreographic.KCut R using (proj-cut; grade-proj-msg; proj-cut-msg) +open ResourceAlgebra R + +⊥-elim : {A : Set} → ⊥ → A +⊥-elim () + +---------------------------------------------------------------------- +-- Asynchronous cuts. `dlv-*` delivered, `flt-*` in flight. +data ACut : Global → Set where + stop : ∀ {G} → ACut G + dlv-msg : ∀ {s r g G} → ACut G → ACut (msg s r g G) + flt-msg : ∀ {s r g G} → ACut G → ACut (msg s r g G) + dlv-choice : ∀ {s r g G₁ G₂} → ACut G₁ → ACut G₂ → ACut (choice s r g G₁ G₂) + flt-choice : ∀ {s r g G₁ G₂} → ACut G₁ → ACut G₂ → ACut (choice s r g G₁ G₂) + +-- An interaction in flight, projected: the sender has acted, the receiver's +-- local cut stops before its receive, an outsider's passes through. +fltproj-msg : ∀ {p s r g L} (ρ : Role p s r) → LCut L → LCut (proj-msg ρ g L) +fltproj-msg (sender _) k = cont-send k +fltproj-msg (receiver _ _) k = stop +fltproj-msg (outside _ _) k = k + +fltproj-choice : ∀ {p s r g L₁ L₂} (ρ : Role p s r) + → LCut L₁ → LCut L₂ → LCut (proj-choice ρ g L₁ L₂) +fltproj-choice (sender _) k₁ k₂ = cont-select k₁ k₂ +fltproj-choice (receiver _ _) k₁ k₂ = stop +fltproj-choice (outside _ _) k₁ k₂ = k₁ + +-- p's local cut at an asynchronous cut; a delivered interaction projects +-- as in the synchronous case. +acutproj : ∀ {G} (p : Party) → ACut G → LCut (proj p G) +acutproj p stop = stop +acutproj p (dlv-msg {s} {r} {g} c) = cutproj-msg {g = g} (role p s r) (acutproj p c) +acutproj p (flt-msg {s} {r} {g} c) = fltproj-msg {g = g} (role p s r) (acutproj p c) +acutproj p (dlv-choice {s} {r} {g} c₁ c₂) = cutproj-choice {g = g} (role p s r) (acutproj p c₁) (acutproj p c₂) +acutproj p (flt-choice {s} {r} {g} c₁ c₂) = fltproj-choice {g = g} (role p s r) (acutproj p c₁) (acutproj p c₂) + +-- p's standpoint at an asynchronous cut. +aview : (p : Party) (G : Global) → ACut G → Local +aview p G κ = proj p G ↾ₗ acutproj p κ + +-- p has done nothing in κ. Read off p's local cut, which at a choice p is +-- outside of shows the left branch only; in a world, plain merge for p +-- (AConsistent) makes the two branches agree, so nothing is missed there. +Quiet : ∀ {G} → Party → ACut G → Set +Quiet p κ = acutproj p κ ≡ stop + +-- Causality: the receiver of an interaction in flight does nothing later. +data Causal : ∀ {G} → ACut G → Set where + stop : ∀ {G} → Causal (stop {G}) + dlv-msg : ∀ {s r g G} {c : ACut G} → Causal c → Causal (dlv-msg {s} {r} {g} c) + flt-msg : ∀ {s r g G} {c : ACut G} → Causal c → Quiet r c → Causal (flt-msg {s} {r} {g} c) + dlv-choice : ∀ {s r g G₁ G₂} {c₁ : ACut G₁} {c₂ : ACut G₂} + → Causal c₁ → Causal c₂ → Causal (dlv-choice {s} {r} {g} c₁ c₂) + flt-choice : ∀ {s r g G₁ G₂} {c₁ : ACut G₁} {c₂ : ACut G₂} + → Causal c₁ → Causal c₂ → Quiet r c₁ → Quiet r c₂ + → Causal (flt-choice {s} {r} {g} c₁ c₂) + +-- Plain merge on views, at a choice p is outside of. +AMerge : ∀ (p : Party) {s r} → Role p s r → ∀ {G₁ G₂} → ACut G₁ → ACut G₂ → Set +AMerge p (sender _) c₁ c₂ = ⊤ +AMerge p (receiver _ _) c₁ c₂ = ⊤ +AMerge p (outside _ _) {G₁} {G₂} c₁ c₂ = aview p G₁ c₁ ≡ aview p G₂ c₂ + +data AConsistent (p : Party) : ∀ {G} → ACut G → Set where + stop : ∀ {G} → AConsistent p (stop {G}) + dlv-msg : ∀ {s r g G} {c : ACut G} → AConsistent p c → AConsistent p (dlv-msg {s} {r} {g} c) + flt-msg : ∀ {s r g G} {c : ACut G} → AConsistent p c → AConsistent p (flt-msg {s} {r} {g} c) + dlv-choice : ∀ {s r g G₁ G₂} {c₁ : ACut G₁} {c₂ : ACut G₂} + → AConsistent p c₁ → AConsistent p c₂ → AMerge p (role p s r) c₁ c₂ + → AConsistent p (dlv-choice {s} {r} {g} c₁ c₂) + flt-choice : ∀ {s r g G₁ G₂} {c₁ : ACut G₁} {c₂ : ACut G₂} + → AConsistent p c₁ → AConsistent p c₂ → AMerge p (role p s r) c₁ c₂ + → AConsistent p (flt-choice {s} {r} {g} c₁ c₂) + +---------------------------------------------------------------------- +-- Synchronous cuts inside asynchronous ones, and back. +-- A synchronous cut is an asynchronous one with nothing in flight. +embed : ∀ {G} → Cut G → ACut G +embed stop = stop +embed (cont-msg c) = dlv-msg (embed c) +embed (cont-choice c₁ c₂) = dlv-choice (embed c₁) (embed c₂) + +-- Nothing in flight. +data Settled : ∀ {G} → ACut G → Set where + stop : ∀ {G} → Settled (stop {G}) + dlv-msg : ∀ {s r g G} {c : ACut G} → Settled c → Settled (dlv-msg {s} {r} {g} c) + dlv-choice : ∀ {s r g G₁ G₂} {c₁ : ACut G₁} {c₂ : ACut G₂} + → Settled c₁ → Settled c₂ → Settled (dlv-choice {s} {r} {g} c₁ c₂) + +-- Deliver everything in flight. +complete : ∀ {G} → ACut G → Cut G +complete stop = stop +complete (dlv-msg c) = cont-msg (complete c) +complete (flt-msg c) = cont-msg (complete c) +complete (dlv-choice c₁ c₂) = cont-choice (complete c₁) (complete c₂) +complete (flt-choice c₁ c₂) = cont-choice (complete c₁) (complete c₂) + +---------------------------------------------------------------------- +-- Grades. What p has paid for an interaction in flight: the sender its +-- grade, everyone else nothing yet. +atₐ : ∀ {p s r} → Role p s r → Grade → Grade +atₐ (sender _) g = g +atₐ (receiver _ _) _ = 𝟙 +atₐ (outside _ _) _ = 𝟙 + +-- p's restricted grade at an asynchronous cut: the sender pays at send, +-- the receiver at receipt. +grade↾ₐ : Party → (G : Global) → ACut G → Grade +grade↾ₐ p G stop = 𝟙 +grade↾ₐ p (msg s r g G) (dlv-msg c) = at (role p s r) g ⊗ grade↾ₐ p G c +grade↾ₐ p (msg s r g G) (flt-msg c) = atₐ (role p s r) g ⊗ grade↾ₐ p G c +grade↾ₐ p (choice s r g G₁ G₂) (dlv-choice c₁ c₂) = at (role p s r) g ⊗ (grade↾ₐ p G₁ c₁ ⊕ grade↾ₐ p G₂ c₂) +grade↾ₐ p (choice s r g G₁ G₂) (flt-choice c₁ c₂) = atₐ (role p s r) g ⊗ (grade↾ₐ p G₁ c₁ ⊕ grade↾ₐ p G₂ c₂) + +-- The global grade of everything sent so far: the completion's. A +-- received-so-far grade would drop messages from the middle of the prefix, +-- which leaves no prefix of the global type; it is not defined. +gradeₛ : (G : Global) → ACut G → Grade +gradeₛ G κ = grade (G ↾ complete κ) + +---------------------------------------------------------------------- +-- (Y-1) Conservativity. + +-- Ledger Y-1. +complete-embed : ∀ {G} (c : Cut G) → complete (embed c) ≡ c +complete-embed stop = refl +complete-embed (cont-msg {s} {r} {g} c) = cong (cont-msg {s} {r} {g}) (complete-embed c) +complete-embed (cont-choice {s} {r} {g} c₁ c₂) = + cong₂ (cont-choice {s} {r} {g}) (complete-embed c₁) (complete-embed c₂) + +-- And back: a cut with nothing in flight is an embedded synchronous cut, so +-- embed is a bijection onto the settled cuts. +-- Ledger Y-1. +embed-complete : ∀ {G} {κ : ACut G} → Settled κ → embed (complete κ) ≡ κ +embed-complete stop = refl +embed-complete (dlv-msg {s} {r} {g} c) = cong (dlv-msg {s} {r} {g}) (embed-complete c) +embed-complete (dlv-choice {s} {r} {g} c₁ c₂) = + cong₂ (dlv-choice {s} {r} {g}) (embed-complete c₁) (embed-complete c₂) + +-- Ledger Y-1. +embed-settled : ∀ {G} (c : Cut G) → Settled (embed c) +embed-settled stop = stop +embed-settled (cont-msg c) = dlv-msg (embed-settled c) +embed-settled (cont-choice c₁ c₂) = dlv-choice (embed-settled c₁) (embed-settled c₂) + +-- Ledger Y-1. +embed-causal : ∀ {G} (c : Cut G) → Causal (embed c) +embed-causal stop = stop +embed-causal (cont-msg c) = dlv-msg (embed-causal c) +embed-causal (cont-choice c₁ c₂) = dlv-choice (embed-causal c₁) (embed-causal c₂) + +-- Ledger Y-1. +acutproj-embed : ∀ {G} p (c : Cut G) → acutproj p (embed c) ≡ cutproj p c +acutproj-embed p stop = refl +acutproj-embed p (cont-msg {s} {r} {g} c) = + cong (cutproj-msg {g = g} (role p s r)) (acutproj-embed p c) +acutproj-embed p (cont-choice {s} {r} {g} c₁ c₂) = + cong₂ (cutproj-choice {g = g} (role p s r)) (acutproj-embed p c₁) (acutproj-embed p c₂) + +-- An embedded cut's view is the projection of the truncated type. +aview-embed : ∀ p G (c : Cut G) → aview p G (embed c) ≡ proj p (G ↾ c) +aview-embed p G c = trans (cong (proj p G ↾ₗ_) (acutproj-embed p c)) (sym (proj-cut p G c)) + +amerge-embed : ∀ {p s r} (ρ : Role p s r) {G₁ G₂} (c₁ : Cut G₁) (c₂ : Cut G₂) + → Merge p ρ (G₁ ↾ c₁) (G₂ ↾ c₂) → AMerge p ρ (embed c₁) (embed c₂) +amerge-embed (sender _) c₁ c₂ m = tt +amerge-embed (receiver _ _) c₁ c₂ m = tt +amerge-embed {p = p} (outside _ _) {G₁} {G₂} c₁ c₂ m = + trans (aview-embed p G₁ c₁) (trans m (sym (aview-embed p G₂ c₂))) + +-- Ledger Y-1. +embed-consistent : ∀ {p G} (c : Cut G) → Consistent p c → AConsistent p (embed c) +embed-consistent stop stop = stop +embed-consistent (cont-msg c) (cont-msg k) = dlv-msg (embed-consistent c k) +embed-consistent {p = p} (cont-choice {s} {r} c₁ c₂) (cont-choice k₁ k₂ m) = + dlv-choice (embed-consistent c₁ k₁) (embed-consistent c₂ k₂) (amerge-embed (role p s r) c₁ c₂ m) + +-- Ledger Y-1. +grade↾ₐ-embed : ∀ p G (c : Cut G) → grade↾ₐ p G (embed c) ≡ grade↾ p (G ↾ c) +grade↾ₐ-embed p G stop = refl +grade↾ₐ-embed p (msg s r g G) (cont-msg c) = + cong (at (role p s r) g ⊗_) (grade↾ₐ-embed p G c) +grade↾ₐ-embed p (choice s r g G₁ G₂) (cont-choice c₁ c₂) = + cong (at (role p s r) g ⊗_) (cong₂ _⊕_ (grade↾ₐ-embed p G₁ c₁) (grade↾ₐ-embed p G₂ c₂)) + +---------------------------------------------------------------------- +-- (Y-2) Asynchronous K-CUT-LOSS. One helper per node shape, each taking the +-- continuation's equation; the receiver of an interaction in flight is +-- quiet, so its continuation contributes 𝟙. + +aloss-dlv-msg : ∀ {p s r} (ρ : Role p s r) g {L} (k : LCut L) {x} + → x ≡ lgrade (L ↾ₗ k) + → at ρ g ⊗ x ≡ lgrade (proj-msg ρ g L ↾ₗ cutproj-msg ρ k) +aloss-dlv-msg ρ g {L} k e = trans (grade-proj-msg ρ g e) (cong lgrade (proj-cut-msg ρ g L k)) + +aloss-flt-msg : ∀ {p s r} (ρ : Role p s r) g {L} (k : LCut L) {x} + → x ≡ lgrade (L ↾ₗ k) → (p ≡ r → k ≡ stop) + → atₐ ρ g ⊗ x ≡ lgrade (proj-msg ρ g L ↾ₗ fltproj-msg ρ k) +aloss-flt-msg (sender _) g k e q = cong (g ⊗_) e +aloss-flt-msg (receiver _ pr) g {L} k e q = + trans (cong (𝟙 ⊗_) (trans e (cong (λ k' → lgrade (L ↾ₗ k')) (q pr)))) (IsSeqMonoid.unitˡ seq 𝟙) +aloss-flt-msg (outside _ _) g k {x} e q = trans (IsSeqMonoid.unitˡ seq x) e + +-- Plain merge on views collapses the two branches of an outsider. +merge-views : ∀ {L₁ L₂ x₁ x₂} → x₁ ≡ lgrade L₁ → x₂ ≡ lgrade L₂ → L₁ ≡ L₂ → x₁ ⊕ x₂ ≡ lgrade L₁ +merge-views {L₁} e₁ e₂ m = + trans (cong₂ _⊕_ e₁ (trans e₂ (cong lgrade (sym m)))) (IsAltMonoid.idem alt (lgrade L₁)) + +aloss-dlv-choice : ∀ {p s r} (ρ : Role p s r) g {G₁ G₂} (c₁ : ACut G₁) (c₂ : ACut G₂) {x₁ x₂} + → x₁ ≡ lgrade (aview p G₁ c₁) → x₂ ≡ lgrade (aview p G₂ c₂) → AMerge p ρ c₁ c₂ + → at ρ g ⊗ (x₁ ⊕ x₂) + ≡ lgrade (proj-choice ρ g (proj p G₁) (proj p G₂) ↾ₗ cutproj-choice ρ (acutproj p c₁) (acutproj p c₂)) +aloss-dlv-choice (sender _) g c₁ c₂ e₁ e₂ _ = cong (g ⊗_) (cong₂ _⊕_ e₁ e₂) +aloss-dlv-choice (receiver _ _) g c₁ c₂ e₁ e₂ _ = cong (g ⊗_) (cong₂ _⊕_ e₁ e₂) +aloss-dlv-choice (outside _ _) g c₁ c₂ {x₁} {x₂} e₁ e₂ m = + trans (IsSeqMonoid.unitˡ seq (x₁ ⊕ x₂)) (merge-views e₁ e₂ m) + +aloss-flt-choice : ∀ {p s r} (ρ : Role p s r) g {G₁ G₂} (c₁ : ACut G₁) (c₂ : ACut G₂) {x₁ x₂} + → x₁ ≡ lgrade (aview p G₁ c₁) → x₂ ≡ lgrade (aview p G₂ c₂) → AMerge p ρ c₁ c₂ + → (p ≡ r → acutproj p c₁ ≡ stop) → (p ≡ r → acutproj p c₂ ≡ stop) + → atₐ ρ g ⊗ (x₁ ⊕ x₂) + ≡ lgrade (proj-choice ρ g (proj p G₁) (proj p G₂) ↾ₗ fltproj-choice ρ (acutproj p c₁) (acutproj p c₂)) +aloss-flt-choice (sender _) g c₁ c₂ e₁ e₂ _ q₁ q₂ = cong (g ⊗_) (cong₂ _⊕_ e₁ e₂) +aloss-flt-choice {p = p} (receiver _ pr) g {G₁} {G₂} c₁ c₂ e₁ e₂ _ q₁ q₂ = + trans (cong (𝟙 ⊗_) (cong₂ _⊕_ (quiet-𝟙 G₁ c₁ e₁ (q₁ pr)) (quiet-𝟙 G₂ c₂ e₂ (q₂ pr)))) + (trans (IsSeqMonoid.unitˡ seq (𝟙 ⊕ 𝟙)) (IsAltMonoid.idem alt 𝟙)) + where + quiet-𝟙 : ∀ G (c : ACut G) {x} → x ≡ lgrade (aview p G c) → acutproj p c ≡ stop → x ≡ 𝟙 + quiet-𝟙 G c e q = trans e (cong (λ k → lgrade (proj p G ↾ₗ k)) q) +aloss-flt-choice (outside _ _) g c₁ c₂ {x₁} {x₂} e₁ e₂ m q₁ q₂ = + trans (IsSeqMonoid.unitˡ seq (x₁ ⊕ x₂)) (merge-views e₁ e₂ m) + +-- The receiver of an interaction in flight is quiet in what follows. +quiet-at : ∀ {p r G} (c : ACut G) → Quiet r c → p ≡ r → acutproj p c ≡ stop +quiet-at c q e = subst (λ t → acutproj t c ≡ stop) (sym e) q + +-- Ledger Y-2. +akcut-loss : ∀ p G (κ : ACut G) → Causal κ → AConsistent p κ + → grade↾ₐ p G κ ≡ lgrade (aview p G κ) +akcut-loss p G stop _ _ = refl +akcut-loss p (msg s r g G) (dlv-msg c) (dlv-msg a) (dlv-msg k) = + aloss-dlv-msg (role p s r) g (acutproj p c) (akcut-loss p G c a k) +akcut-loss p (msg s r g G) (flt-msg c) (flt-msg a q) (flt-msg k) = + aloss-flt-msg (role p s r) g (acutproj p c) (akcut-loss p G c a k) (quiet-at c q) +akcut-loss p (choice s r g G₁ G₂) (dlv-choice c₁ c₂) (dlv-choice a₁ a₂) (dlv-choice k₁ k₂ m) = + aloss-dlv-choice (role p s r) g c₁ c₂ (akcut-loss p G₁ c₁ a₁ k₁) (akcut-loss p G₂ c₂ a₂ k₂) m +akcut-loss p (choice s r g G₁ G₂) (flt-choice c₁ c₂) (flt-choice a₁ a₂ q₁ q₂) (flt-choice k₁ k₂ m) = + aloss-flt-choice (role p s r) g c₁ c₂ (akcut-loss p G₁ c₁ a₁ k₁) (akcut-loss p G₂ c₂ a₂ k₂) m + (quiet-at c₁ q₁) (quiet-at c₂ q₂) + +---------------------------------------------------------------------- +-- (Y-3) Delivering an interaction in flight changes only its receiver's +-- local cut. + +invisible-msg : ∀ {p s r g L} (ρ : Role p s r) (k : LCut L) → p ≢ r + → fltproj-msg {g = g} ρ k ≡ cutproj-msg ρ k +invisible-msg (sender _) k _ = refl +invisible-msg (receiver _ e) k ne = ⊥-elim (ne e) +invisible-msg (outside _ _) k _ = refl + +invisible-choice : ∀ {p s r g L₁ L₂} (ρ : Role p s r) (k₁ : LCut L₁) (k₂ : LCut L₂) → p ≢ r + → fltproj-choice {g = g} ρ k₁ k₂ ≡ cutproj-choice ρ k₁ k₂ +invisible-choice (sender _) k₁ k₂ _ = refl +invisible-choice (receiver _ e) k₁ k₂ ne = ⊥-elim (ne e) +invisible-choice (outside _ _) k₁ k₂ _ = refl + +-- Ledger Y-3. +flight-invisible : ∀ p {s r g G} (c : ACut G) → p ≢ r + → acutproj p (flt-msg {s} {r} {g} c) ≡ acutproj p (dlv-msg c) +flight-invisible p {s} {r} c ne = invisible-msg (role p s r) (acutproj p c) ne + +-- Ledger Y-3. +flight-invisible-choice : ∀ p {s r g G₁ G₂} (c₁ : ACut G₁) (c₂ : ACut G₂) → p ≢ r + → acutproj p (flt-choice {s} {r} {g} c₁ c₂) ≡ acutproj p (dlv-choice c₁ c₂) +flight-invisible-choice p {s} {r} c₁ c₂ ne = invisible-choice (role p s r) (acutproj p c₁) (acutproj p c₂) ne diff --git a/src/Choreographic/AsyncBound.agda b/src/Choreographic/AsyncBound.agda new file mode 100644 index 0000000..da9d287 --- /dev/null +++ b/src/Choreographic/AsyncBound.agda @@ -0,0 +1,91 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- K-CUT-WARRANT's bound over asynchronous cuts (ladder increment I3a). +-- +-- The global grade is the sent-so-far grade `gradeₛ`: the grade of the +-- completion, where everything in flight is delivered. Both directions of +-- Bound.agda survive. +-- +-- every grade ≽ 𝟙 ⇒ grade↾ₐ p G κ ≼ gradeₛ G κ (HWM; MaxPlus on vals) +-- every grade ≼ 𝟙 ⇒ gradeₛ G κ ≼ grade↾ₐ p G κ (Loss) +-- +-- The case to watch is a receiver that lags behind its messages. It has +-- paid 𝟙 where the completion pays g, and 𝟙 sits on the same side of every +-- grade as the bound needs: below them in the first case, above them in the +-- second. +open import ResourceAlgebra.Core + +module Choreographic.AsyncBound (R : ResourceAlgebra) (ord : IsOrdered R) where + +open import ResourceAlgebra.Prelude +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Async R +open import Choreographic.AsyncKnowledge R using (module AFrame) +open import Choreographic.Bound R ord using (Each; msg; choice; each-cut; grade↾-≼; grade-≼↾; ≡-≼) +open ResourceAlgebra R +open IsOrdered ord + +---------------------------------------------------------------------- +-- What p has paid by κ, against what it pays once κ is completed. +atₐ-≼ : ∀ {p s r} (ρ : Role p s r) {g} → 𝟙 ≼ g → atₐ ρ g ≼ at ρ g +atₐ-≼ (sender _) {g} _ = ≼-refl g +atₐ-≼ (receiver _ _) u = u +atₐ-≼ (outside _ _) _ = ≼-refl 𝟙 + +≼-atₐ : ∀ {p s r} (ρ : Role p s r) {g} → g ≼ 𝟙 → at ρ g ≼ atₐ ρ g +≼-atₐ (sender _) {g} _ = ≼-refl g +≼-atₐ (receiver _ _) u = u +≼-atₐ (outside _ _) _ = ≼-refl 𝟙 + +-- Ledger Y-7. +grade↾ₐ-≼ : ∀ p {G} → Each (𝟙 ≼_) G → (κ : ACut G) → grade↾ₐ p G κ ≼ grade↾ p (G ↾ complete κ) +grade↾ₐ-≼ p _ stop = ≼-refl 𝟙 +grade↾ₐ-≼ p {msg s r g G} (msg u e) (dlv-msg c) = + ⊗-mono (≼-refl (at (role p s r) g)) (grade↾ₐ-≼ p e c) +grade↾ₐ-≼ p {msg s r g G} (msg u e) (flt-msg c) = + ⊗-mono (atₐ-≼ (role p s r) u) (grade↾ₐ-≼ p e c) +grade↾ₐ-≼ p {choice s r g G₁ G₂} (choice u e₁ e₂) (dlv-choice c₁ c₂) = + ⊗-mono (≼-refl (at (role p s r) g)) (⊕-mono (grade↾ₐ-≼ p e₁ c₁) (grade↾ₐ-≼ p e₂ c₂)) +grade↾ₐ-≼ p {choice s r g G₁ G₂} (choice u e₁ e₂) (flt-choice c₁ c₂) = + ⊗-mono (atₐ-≼ (role p s r) u) (⊕-mono (grade↾ₐ-≼ p e₁ c₁) (grade↾ₐ-≼ p e₂ c₂)) + +-- Ledger Y-7. +≼-grade↾ₐ : ∀ p {G} → Each (_≼ 𝟙) G → (κ : ACut G) → grade↾ p (G ↾ complete κ) ≼ grade↾ₐ p G κ +≼-grade↾ₐ p _ stop = ≼-refl 𝟙 +≼-grade↾ₐ p {msg s r g G} (msg u e) (dlv-msg c) = + ⊗-mono (≼-refl (at (role p s r) g)) (≼-grade↾ₐ p e c) +≼-grade↾ₐ p {msg s r g G} (msg u e) (flt-msg c) = + ⊗-mono (≼-atₐ (role p s r) u) (≼-grade↾ₐ p e c) +≼-grade↾ₐ p {choice s r g G₁ G₂} (choice u e₁ e₂) (dlv-choice c₁ c₂) = + ⊗-mono (≼-refl (at (role p s r) g)) (⊕-mono (≼-grade↾ₐ p e₁ c₁) (≼-grade↾ₐ p e₂ c₂)) +≼-grade↾ₐ p {choice s r g G₁ G₂} (choice u e₁ e₂) (flt-choice c₁ c₂) = + ⊗-mono (≼-atₐ (role p s r) u) (⊕-mono (≼-grade↾ₐ p e₁ c₁) (≼-grade↾ₐ p e₂ c₂)) + +---------------------------------------------------------------------- +-- The bound against the sent-so-far grade, then known. + +-- Ledger Y-7. +grade↾ₐ-≼ₛ : ∀ p {G} → Each (𝟙 ≼_) G → (κ : ACut G) → grade↾ₐ p G κ ≼ gradeₛ G κ +grade↾ₐ-≼ₛ p e κ = ≼-trans (grade↾ₐ-≼ p e κ) (grade↾-≼ p (each-cut e (complete κ))) + +-- Ledger Y-7. +gradeₛ-≼↾ₐ : ∀ p {G} → Each (_≼ 𝟙) G → (κ : ACut G) → gradeₛ G κ ≼ grade↾ₐ p G κ +gradeₛ-≼↾ₐ p e κ = ≼-trans (grade-≼↾ p (each-cut e (complete κ))) (≼-grade↾ₐ p e κ) + +module _ (G : Global) (p : Party) where + open AFrame G + + -- Ledger Y-7. + aknows-lower-bound : Each (𝟙 ≼_) G → ∀ w + → AKnows p w (λ w' → grade↾ₐ p G (acut w) ≼ gradeₛ G (acut w')) + aknows-lower-bound e w w' s = + ≡-≼ (sym (aknows-own-grade p w w' s)) (grade↾ₐ-≼ₛ p e (acut w')) + + -- Ledger Y-7. + aknows-upper-bound : Each (_≼ 𝟙) G → ∀ w + → AKnows p w (λ w' → gradeₛ G (acut w') ≼ grade↾ₐ p G (acut w)) + aknows-upper-bound e w w' s = + ≼-trans (gradeₛ-≼↾ₐ p e (acut w')) (≡-≼ (aknows-own-grade p w w' s) (≼-refl _)) diff --git a/src/Choreographic/AsyncKnowledge.agda b/src/Choreographic/AsyncKnowledge.agda new file mode 100644 index 0000000..81bf243 --- /dev/null +++ b/src/Choreographic/AsyncKnowledge.agda @@ -0,0 +1,167 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Knowledge over asynchronous cuts (ladder increment I3a). +-- +-- The frame is Kripke.agda's, with asynchronous worlds: causal cuts that +-- are consistent for every party. Two worlds are p-indistinguishable when +-- p's view is the same. +-- +-- (Y-4) What survives: p knows its own restricted grade, so holds a sound +-- warrant for it, and p knows its own frontier. +-- (Y-5) The receiver of a delivered message knows it was delivered, and +-- so that it was sent. +-- (Y-6) Its sender does not know it was received, at every world where +-- the receiver has done nothing since. In the synchronous frame +-- the same proposition is a theorem: asynchrony is what separates +-- the two ends of a message. +open import ResourceAlgebra.Core + +module Choreographic.AsyncKnowledge (R : ResourceAlgebra) where + +open import ResourceAlgebra.Prelude +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Local R +open import Choreographic.Projection R +open import Choreographic.Async R +open import Choreographic.Kripke R using (module Frame; view) +open import Choreographic.Transport R using (↾ₗ-injective) +open import EpistemicTypes.Warrant using (mkWarrant; SoundWarrant; soundWarrant) +open ResourceAlgebra R + +-- Ledger Y-4. +module AFrame (G : Global) where + + -- An asynchronous world: a causal cut, consistent for every party. + record AWorld : Set where + constructor world + field + acut : ACut G + causal : Causal acut + consistent : ∀ p → AConsistent p acut + open AWorld public + + infix 4 _~[_]_ + _~[_]_ : AWorld → Party → AWorld → Set + w ~[ p ] w' = aview p G (acut w) ≡ aview p G (acut w') + + -- φ holds at every world with the same view for p, including w. + AKnows : Party → AWorld → (AWorld → Set) → Set + AKnows p w φ = ∀ w' → w ~[ p ] w' → φ w' + + aknows-factive : ∀ p w φ → AKnows p w φ → φ w + aknows-factive p w φ k = k w refl + + -- epistemic-types' interface, as in Kripke.agda: the evidence is + -- knowledge, and soundness is the reflexivity of the frame. + -- Ledger Y-4. + asound-warrant : (p : Party) (w : AWorld) (φ : AWorld → Set) → SoundWarrant Party p (φ w) + asound-warrant p w φ = soundWarrant (mkWarrant (AKnows p w φ)) (aknows-factive p w φ) + + -- LOSS ⇒ WARRANT survives asynchrony: by akcut-loss, p's restricted grade + -- is a function of p's view. + -- Ledger Y-4. + aknows-own-grade : ∀ p w → AKnows p w (λ w' → grade↾ₐ p G (acut w') ≡ grade↾ₐ p G (acut w)) + aknows-own-grade p w w' e = + trans (akcut-loss p G (acut w') (causal w') (consistent w' p)) + (trans (cong lgrade (sym e)) + (sym (akcut-loss p G (acut w) (causal w) (consistent w p)))) + + -- p knows exactly how far its own timeline has run. + -- Ledger Y-4. + aknows-local-cut : ∀ p w → AKnows p w (λ w' → acutproj p (acut w') ≡ acutproj p (acut w)) + aknows-local-cut p w w' e = ↾ₗ-injective (proj p G) (acutproj p (acut w')) (acutproj p (acut w)) (sym e) + +---------------------------------------------------------------------- +-- The first message of a protocol msg s r g G: delivered, or sent. +Delivered : ∀ {s r g G} → ACut (msg s r g G) → Set +Delivered stop = ⊥ +Delivered (dlv-msg _) = ⊤ +Delivered (flt-msg _) = ⊥ + +Sent : ∀ {s r g G} → ACut (msg s r g G) → Set +Sent stop = ⊥ +Sent (dlv-msg _) = ⊤ +Sent (flt-msg _) = ⊤ + +delivered→sent : ∀ {s r g G} (κ : ACut (msg s r g G)) → Delivered κ → Sent κ +delivered→sent stop () +delivered→sent (dlv-msg _) _ = tt +delivered→sent (flt-msg _) () + +-- The same, for a synchronous cut, where the message is one event. +SDelivered : ∀ {s r g G} → Cut (msg s r g G) → Set +SDelivered stop = ⊥ +SDelivered (cont-msg _) = ⊤ + +-- The first message, s → r, of an arbitrary protocol. +module Head (s r : Party) (g : Grade) (G : Global) (s≢r : s ≢ r) where + open AFrame (msg s r g G) + + private + -- The receiver's view tells a delivered message from one not delivered. + r-dlv≢stop : ∀ {L} (ρ : Role r s r) (k : LCut L) → proj-msg ρ g L ↾ₗ cutproj-msg ρ k ≢ end + r-dlv≢stop (sender e) k _ = s≢r (sym e) + r-dlv≢stop (receiver _ _) k () + r-dlv≢stop (outside _ ne) k _ = ne refl + + r-dlv≢flt : ∀ {L} (ρ : Role r s r) (k k' : LCut L) + → proj-msg ρ g L ↾ₗ cutproj-msg ρ k ≢ proj-msg ρ g L ↾ₗ fltproj-msg ρ k' + r-dlv≢flt (sender e) k k' _ = s≢r (sym e) + r-dlv≢flt (receiver _ _) k k' () + r-dlv≢flt (outside _ ne) k k' _ = ne refl + + r-delivered : (κ κ' : ACut (msg s r g G)) → Delivered κ + → aview r (msg s r g G) κ ≡ aview r (msg s r g G) κ' → Delivered κ' + r-delivered (dlv-msg c) (dlv-msg c') _ _ = tt + r-delivered (dlv-msg c) stop _ e = ⊥-elim (r-dlv≢stop (role r s r) (acutproj r c) e) + r-delivered (dlv-msg c) (flt-msg c') _ e = ⊥-elim (r-dlv≢flt (role r s r) (acutproj r c) (acutproj r c') e) + r-delivered stop _ () _ + r-delivered (flt-msg c) _ () _ + + -- Ledger Y-5. + receiver-knows-delivered : ∀ w → Delivered (acut w) → AKnows r w (λ w' → Delivered (acut w')) + receiver-knows-delivered w d w' e = r-delivered (acut w) (acut w') d e + + -- Ledger Y-5. + receiver-knows-sent : ∀ w → Delivered (acut w) → AKnows r w (λ w' → Sent (acut w')) + receiver-knows-sent w d w' e = delivered→sent (acut w') (receiver-knows-delivered w d w' e) + + -------------------------------------------------------------------- + -- The world where the first message is delivered and its receiver has + -- done nothing since, and the world where it is still in flight. + delivered-world in-flight-world : (c : ACut G) → Causal c → Quiet r c → (∀ p → AConsistent p c) → AWorld + delivered-world c a q k = world (dlv-msg c) (dlv-msg a) (λ p → dlv-msg (k p)) + in-flight-world c a q k = world (flt-msg c) (flt-msg a q) (λ p → flt-msg (k p)) + + -- Every party but the receiver sees the two alike. + -- Ledger Y-6. + only-receiver-sees : ∀ p c a q k → p ≢ r → delivered-world c a q k ~[ p ] in-flight-world c a q k + only-receiver-sees p c a q k ne = cong (proj p (msg s r g G) ↾ₗ_) (sym (flight-invisible p c ne)) + + -- So the sender does not know its message was received. + -- Ledger Y-6. + sender-cannot-know-receipt : ∀ c a q k → ¬ AKnows s (delivered-world c a q k) (λ w' → Delivered (acut w')) + sender-cannot-know-receipt c a q k K = K (in-flight-world c a q k) (only-receiver-sees s c a q k s≢r) + + -------------------------------------------------------------------- + -- The synchronous contrast: there the sender does know. + private + module S = Frame (msg s r g G) + + s-dlv≢stop : ∀ {L} (ρ : Role s s r) (k : LCut L) → proj-msg ρ g L ↾ₗ cutproj-msg ρ k ≢ end + s-dlv≢stop (sender _) k () + s-dlv≢stop (receiver ne _) k _ = ne refl + s-dlv≢stop (outside ne _) k _ = ne refl + + s-delivered : (c c' : Cut (msg s r g G)) → SDelivered c + → view s (msg s r g G) c ≡ view s (msg s r g G) c' → SDelivered c' + s-delivered (cont-msg c) (cont-msg c') _ _ = tt + s-delivered (cont-msg c) stop _ e = ⊥-elim (s-dlv≢stop (role s s r) (cutproj s c) e) + s-delivered stop _ () _ + + -- Ledger Y-6. + sync-sender-knows-receipt : ∀ w → SDelivered (S.cut w) → S.Knows s w (λ w' → SDelivered (S.cut w')) + sync-sender-knows-receipt w d w' e = s-delivered (S.cut w) (S.cut w') d e diff --git a/src/Choreographic/Instances.agda b/src/Choreographic/Instances.agda index cb73c29..89969b7 100644 --- a/src/Choreographic/Instances.agda +++ b/src/Choreographic/Instances.agda @@ -190,7 +190,8 @@ module TransportWitness where receiver-knows = knows-local-cut 1 w₂ -- ... and, synchronously, the sender knows both were sent. Asynchrony - -- (send without receipt) is exactly where this symmetry would break. + -- (send without receipt) is where this symmetry breaks: AsyncWitness + -- below, Y-6. -- Ledger T-2. sender-knows : Knows 0 w₂ (λ w' → cutproj 0 (cut w') ≡ cont-send (cont-send stop)) sender-knows = knows-local-cut 0 w₂ @@ -278,3 +279,110 @@ module GradeNotStateInvariant where equivalent p = swap-proj (disjoint (λ ()) (λ ()) (λ ()) (λ ())) p a b end grades-differ : peak (grade s) ≢ peak (grade t) grades-differ () + +---------------------------------------------------------------------- +-- Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda). +import Choreographic.Async +import Choreographic.AsyncBound +module AL = Choreographic.Async Loss +module AM = Choreographic.Async MaxPlus +module AH = Choreographic.Async HWM + +-- Ledger Y-2. +akcut-loss-Loss = AL.akcut-loss +-- Ledger Y-2. +akcut-loss-MaxPlus = AM.akcut-loss +-- Ledger Y-2. +akcut-loss-HWM = AH.akcut-loss + +module YH = Choreographic.AsyncBound HWM HWM-ordered +module YL = Choreographic.AsyncBound Loss Loss-ordered +module YM = Choreographic.AsyncBound MaxPlus MaxPlus-ordered + +-- The bound against the sent-so-far grade, discharged as W-6 is: HWM and +-- MaxPlus (bot-free) from below, Loss from above. +-- Ledger Y-7. +async-warrant-HWM = λ G p w → YH.aknows-lower-bound G p (BH.each-of (ResourceAlgebra.𝟘-least HWM) G) w + +-- Ledger Y-7. +async-warrant-Loss = λ G p w → YL.aknows-upper-bound G p (BL.each-of loss-unit-greatest G) w + +-- Ledger Y-7. +async-warrant-MaxPlus = λ G p (botfree : BM.Each (ResourceAlgebra._≼_ MaxPlus (val 0)) G) w → + YM.aknows-lower-bound G p botfree w + +-- The first message of the witness protocol (0 → 1 twice), delivered and +-- still in flight. (TESTED by evaluation.) +module AsyncWitness where + open import Choreographic.Global MaxPlus + open import Choreographic.Async MaxPlus + open import Choreographic.AsyncKnowledge MaxPlus + open Witness using (G) + open AFrame G + + delivered in-flight : AWorld + delivered = world (dlv-msg stop) (dlv-msg stop) (λ _ → dlv-msg stop) + in-flight = world (flt-msg stop) (flt-msg stop refl) (λ _ → flt-msg stop) + + -- The sender sees no difference ... + -- Ledger Y-6. + sender-blind : delivered ~[ 0 ] in-flight + sender-blind = refl + + -- ... the receiver does. + -- Ledger Y-6. + receiver-sees : ¬ (delivered ~[ 1 ] in-flight) + receiver-sees () + + -- So the sender does not know its first message arrived. + -- Ledger Y-6. + sender-cannot-know : ¬ AKnows 0 delivered (λ w' → Delivered (acut w')) + sender-cannot-know = + Head.sender-cannot-know-receipt 0 1 (val 1) (msg 0 1 (val 1) end) (λ ()) stop stop refl (λ _ → stop) + +-- A reply restores the knowledge: 0 → 1 : a, then 1 → 0 : b. Once the +-- reply has been received, 0 knows its message was delivered: a reply could +-- only have been sent by a receiver that had acted. A reply still in flight +-- is not enough. +-- Ledger Y-8. +module Acknowledgement (R : ResourceAlgebra) (a b : ResourceAlgebra.Grade R) where + open import Choreographic.Global R + open import Choreographic.Local R + open import Choreographic.Async R + open import Choreographic.AsyncKnowledge R + open import Choreographic.Transport R using (send-inj) + + G : Global + G = msg 0 1 a (msg 1 0 b end) + + open AFrame G + + acknowledged replied unreceived : AWorld + -- Both messages delivered. + acknowledged = world (dlv-msg (dlv-msg stop)) (dlv-msg (dlv-msg stop)) (λ _ → dlv-msg (dlv-msg stop)) + -- The first delivered, the reply in flight. + replied = world (dlv-msg (flt-msg stop)) (dlv-msg (flt-msg stop refl)) (λ _ → dlv-msg (flt-msg stop)) + -- The first still in flight. + unreceived = world (flt-msg stop) (flt-msg stop refl) (λ _ → flt-msg stop) + + private + recv≢end : ∀ {q g L} → recv q g L ≢ end + recv≢end () + + -- Every world 0 cannot tell from `acknowledged` has the first message + -- delivered. A world where it is in flight but the reply was sent + -- breaks causality: the reply's sender, 1, is not quiet. + ack : (κ : ACut G) → Causal κ → aview 0 G (acut acknowledged) ≡ aview 0 G κ → Delivered κ + ack (dlv-msg _) _ _ = tt + ack stop _ () + ack (flt-msg stop) _ e = recv≢end (send-inj e) + ack (flt-msg (flt-msg _)) _ e = recv≢end (send-inj e) + ack (flt-msg (dlv-msg _)) (flt-msg _ ()) _ + + -- Ledger Y-8. + reply-gives-knowledge : AKnows 0 acknowledged (λ w' → Delivered (acut w')) + reply-gives-knowledge w' e = ack (acut w') (causal w') e + + -- Ledger Y-8. + reply-in-flight-is-not-enough : ¬ AKnows 0 replied (λ w' → Delivered (acut w')) + reply-in-flight-is-not-enough K = K unreceived refl diff --git a/src/Choreographic/Transport.agda b/src/Choreographic/Transport.agda index 4777542..324eed6 100644 --- a/src/Choreographic/Transport.agda +++ b/src/Choreographic/Transport.agda @@ -13,7 +13,8 @@ -- every world p knows exactly how far its own timeline has run, and -- therefore every fact about its own frontier — receiving is knowing -- it was received. In this synchronous fragment the sender knows the --- same of its sends; asynchrony is where that symmetry breaks. +-- same of its sends; asynchrony is where that symmetry breaks +-- (AsyncKnowledge.agda, Y-5 and Y-6). -- (T3) Why AccessibleModality itself cannot be instantiated: its carrier is -- E : K → Set → Set, but Kripke knowledge is indexed by worlds, -- E : K → (World → Set) → (World → Set). IndexedAccessible below is diff --git a/tests/reject/SenderKnowsReceipt.agda b/tests/reject/SenderKnowsReceipt.agda new file mode 100644 index 0000000..8197cad --- /dev/null +++ b/tests/reject/SenderKnowsReceipt.agda @@ -0,0 +1,24 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Ledger Y-6. +module SenderKnowsReceipt where +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.MaxPlus +open import Choreographic.Global MaxPlus +open import Choreographic.Async MaxPlus +open import Choreographic.AsyncKnowledge MaxPlus + +-- Must fail: asynchronously, the sender of a message does not know it was +-- received until something comes back. Synchronously the same claim is a +-- theorem (Head.sync-sender-knows-receipt in AsyncKnowledge.agda). +G : Global +G = msg 0 1 (val 1) (msg 0 1 (val 1) end) + +open AFrame G + +delivered : AWorld +delivered = world (dlv-msg stop) (dlv-msg stop) (λ _ → dlv-msg stop) + +invalid : AKnows 0 delivered (λ w' → Delivered (acut w')) +invalid w' _ = tt From b35c46c815fe462c0c90c7946f13806182017660 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 16:32:21 +0000 Subject: [PATCH 3/3] Docs: restrict the reply claim to the proved first-message cases 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 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- ARCHITECTURE.adoc | 5 +++-- EXPLAINME.adoc | 8 +++++--- README.adoc | 11 +++++++---- docs/CHANGELOG-entry.adoc | 10 ++++++---- docs/README-keystone-section.adoc | 11 +++++++---- 5 files changed, 28 insertions(+), 17 deletions(-) diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index 8ae4f18..0e96509 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -71,8 +71,9 @@ the siblings it imports, and the gate that checks it. `SoundWarrant` and `Access.Preorder` rather than imitating them. . *Asynchrony* — `Async` adds cuts whose messages and selections are delivered or in flight, and proves K-CUT-LOSS for them; `AsyncKnowledge` - is the Kripke frame over them (the receiver of a message knows it was - sent, its sender does not know it was received); `AsyncBound` is the + is the Kripke frame over them (the receiver of a protocol's first message + knows it was sent, its sender does not know it was received while the + receiver has done nothing since); `AsyncBound` is the bound against the sent-so-far grade. . *Instances and applications* — `Instances` discharges the keystone at the three estate algebras and computes a worked protocol; `Swap` and diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c0849b1..8be12e2 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -73,9 +73,11 @@ Caveat:: choreography determines; for anything about payloads it stays an assumption. Asynchronously the transport result is directional, as pre-registered (`docs/pre-registration-addendum-2026-10-19.adoc`): the -receiver of a message knows it was sent, its sender does not know it was -received until a reply arrives (`src/Choreographic/AsyncKnowledge.agda`), -and the bound survives against the sent-so-far grade +receiver of a protocol's first message knows it was sent, and its sender +does not know it was received while the receiver has done nothing since +(`src/Choreographic/AsyncKnowledge.agda`); a reply restores that knowledge +in the two-message protocol only (`Instances.Acknowledgement`), the +position-indexed and general-chain forms being open. The bound survives against the sent-so-far grade (`src/Choreographic/AsyncBound.agda`). === The resource algebra is imported, the tropical bridge is named diff --git a/README.adoc b/README.adoc index bc5e08d..4443a26 100644 --- a/README.adoc +++ b/README.adoc @@ -64,10 +64,13 @@ K-CUT-WARRANT:: and knowledge is monotone along it — a lawful world-indexed `AccessibleModality`. Asynchronously (`src/Choreographic/AsyncKnowledge.agda`, `src/Choreographic/AsyncBound.agda`) the bound survives against the - sent-so-far grade and the receiver of a message knows it was sent, but its - sender does not know it was received until a reply arrives: the - pre-registered falsifier, confirmed. OPEN beyond the fragment: recursion, - full merge, data-dependent warrants. See link:PROOF-STATUS.adoc[]. + sent-so-far grade and the receiver of a protocol's first message knows it + was sent, but its sender does not know it was received while the receiver + has done nothing since: the pre-registered falsifier, confirmed. A reply + restores that knowledge, proved only for the two-message protocol + `0 → 1 : a . 1 → 0 : b`. OPEN beyond the fragment: the position-indexed + form of these two, the general reply chain, recursion, full merge, + data-dependent warrants. See link:PROOF-STATUS.adoc[]. [NOTE] ==== diff --git a/docs/CHANGELOG-entry.adoc b/docs/CHANGELOG-entry.adoc index b1324e2..d1874cb 100644 --- a/docs/CHANGELOG-entry.adoc +++ b/docs/CHANGELOG-entry.adoc @@ -9,15 +9,17 @@ cuts; asynchronous K-CUT-LOSS from the same two laws, which `scripts/minimal-laws.sh` now also certifies; in-flight invisibility. * `src/Choreographic/AsyncKnowledge.agda`: the frame over asynchronous - worlds. The receiver of a delivered message knows it was sent; its sender - does not know it was received while the receiver has done nothing since, + worlds. The receiver of a protocol's first message knows it was sent; its + sender does not know it was received while the receiver has done nothing + since, although the same proposition is a theorem synchronously. This is the pre-registered falsifier, confirmed. * `src/Choreographic/AsyncBound.agda`: both bounds against the sent-so-far grade. * `src/Choreographic/Instances.agda`: discharges at Loss, MaxPlus and HWM; a - concrete witness; a reply restores the sender's knowledge, and a reply - still in flight does not. + concrete witness; in the two-message protocol a reply restores the + sender's knowledge and a reply still in flight does not (the general chain + is open). * `tests/reject/SenderKnowsReceipt.agda`: the sender's knowledge of receipt is refused. * PROOF-STATUS: section "Asynchrony", rows Y-1 to Y-8, and "What Y-6 says diff --git a/docs/README-keystone-section.adoc b/docs/README-keystone-section.adoc index acf6b35..c12d929 100644 --- a/docs/README-keystone-section.adoc +++ b/docs/README-keystone-section.adoc @@ -31,10 +31,13 @@ K-CUT-WARRANT:: and knowledge is monotone along it — a lawful world-indexed `AccessibleModality`. Asynchronously (`src/Choreographic/AsyncKnowledge.agda`, `src/Choreographic/AsyncBound.agda`) the bound survives against the - sent-so-far grade and the receiver of a message knows it was sent, but its - sender does not know it was received until a reply arrives: the - pre-registered falsifier, confirmed. OPEN beyond the fragment: recursion, - full merge, data-dependent warrants. See link:../PROOF-STATUS.adoc[]. + sent-so-far grade and the receiver of a protocol's first message knows it + was sent, but its sender does not know it was received while the receiver + has done nothing since: the pre-registered falsifier, confirmed. A reply + restores that knowledge, proved only for the two-message protocol + `0 → 1 : a . 1 → 0 : b`. OPEN beyond the fragment: the position-indexed + form of these two, the general reply chain, recursion, full merge, + data-dependent warrants. See link:../PROOF-STATUS.adoc[]. [NOTE] ====