diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 5aa9403..88cf4c2 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -145,5 +145,22 @@ title = "State K-CUT-LOSS as the first Agda signature, against [ResourceAlgebra status = "open" priority = "high" +# ---- Application proof targets (added after pre-registration) ---- + +[[application-targets]] +id = "app-rapidnj-002" +name = "two-thread RapidNJ K-CUT-LOSS square" +status = "OPEN TARGET (not a proof; application note only)" +frontier = "two selected events e1/e2 with Independent₂ witness" +minimum-lemma = "localGrade p (localStep p e2 (localStep p e1 (project p s))) ≡ transportLoss p (globalGrade (step e2 (step e1 s)))" +prerequisite = "canonical state diamond for disjoint read/write footprints" +non-claim = "Does not assert upstream RapidNJ exposes this batch interface; does not address K-CUT-WARRANT" + +[[application-targets]] +id = "app-rapidnj-001" +name = "two-thread RapidNJ canonical state diamond" +status = "OPEN TARGET (algorithmic prerequisite, not K-CUT)" +statement = "step e2 (step e1 s) ~= step e1 (step e2 s) under Independent₂" + [blockers] note = "K-CUT cannot be typed until the repo is git-init'd + licensed by the owner. Everything below na-001 waits on that." diff --git a/EXPLAINME-new.adoc b/EXPLAINME-new.adoc index 6be3b25..764fb4c 100644 --- a/EXPLAINME-new.adoc +++ b/EXPLAINME-new.adoc @@ -16,11 +16,16 @@ ____ A global choreographic type G is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by an echo loss-grade and an epistemic standpoint-warrant. ____ -How this is implemented:: -`link:src/ChoreographicTypes/[]` defines `GlobalType`, the partial causal order structure, the grading by `EchoGrade` (imported from `echo-types`) and `EpiGrade` (imported from `epistemic-types`), and the `EndpointProjection` mapping. +How this is intended to be implemented:: +The planned `link:src/ChoreographicTypes/[]` tree will define `GlobalType`, the +partial causal order structure, the grading by `EchoGrade` (imported from +`echo-types`) and `EpiGrade` (imported from `epistemic-types`), and the +`EndpointProjection` mapping. Caveat:: -The definitions are present. The deep integration — proving that the grading laws hold under the projection mapping in the general case — is the content of K-CUT, which is open. +The current checkout does not contain the planned `src/` tree. The deep +integration — proving that the grading laws hold under the projection mapping +in the general case — remains the open K-CUT problem. === K-CUT-LOSS holds as equality @@ -29,8 +34,10 @@ ____ K-CUT-LOSS: Grading commutes with projection as an equality. Loss is type-determined. ____ -How this is implemented:: -The statement of K-CUT-LOSS is formalised in this repo. The *only* existing proof is the degenerate single-static-edge base case in `echo-types` (`RoleGraded.choreo-grade-commute`). No proof for general cuts exists here. +How this is intended to be implemented:: +The K-CUT-LOSS statement is a planned Agda target for this repo. The *only* +existing proof is the degenerate single-static-edge base case in `echo-types` +(`RoleGraded.choreo-grade-commute`). No proof for general cuts exists here. Caveat:: **This is an open conjecture, not a theorem.** The base case suggests it is likely true, but compositionality across arbitrary antichains is unproved. This is the hardest open problem in the repo. @@ -42,12 +49,26 @@ ____ K-CUT-WARRANT: Warrant transport commutes with projection only as a bound, and only under a SoundWarrant side-condition. The type upper-bounds discoverability but cannot determine it. ____ -How this is implemented:: -The statement of K-CUT-WARRANT is formalised here, importing `SoundWarrant` from `epistemic-types`. No proof exists, not even a base case. +How this is intended to be implemented:: +The K-CUT-WARRANT statement is a planned Agda target, importing +`SoundWarrant` from `epistemic-types`. No proof exists, not even a base case. Caveat:: **This is an open conjecture.** The directionality (bound, not equality) reflects the epistemic reality: an agent's local knowledge may exceed the type's requirements, so projection can only upper-bound the warrant, not determine it. This is the formal reflection of the `BeliefModality` / non-factive design in `epistemic-types`. +=== The RapidNJ application isolates the first non-degenerate target + +[quote, applications/rapidnj-two-thread.adoc] +____ +The smallest non-degenerate K-CUT lemma is a two-event loss-grade commuting square for a disjoint antichain frontier. +____ + +How this is implemented:: +`link:applications/rapidnj-two-thread.adoc[]` defines the application boundary and records the target in `link:applications/rapidnj-two-thread.agda[]`. The target names global and local reduction steps, projection, loss grading, transport, and an `Independent₂` witness. `Independent₂` is deliberately stronger than antichain membership: it must cover read/write disjointness, phase safety, and deterministic tie handling. + +Caveat:: +The accompanying Agda file contains open interfaces and postulated target signatures so that the proof obligation has a stable shape. It is not imported into the build and proves nothing. The RapidNJ state diamond (serialising two independent updates in either order) is an algorithmic prerequisite, separate from K-CUT-LOSS. No claim is made about the upstream implementation exposing this exact batch interface. + === The tropical resource-dioid is re-proved in-site [quote, README.adoc] @@ -94,7 +115,12 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4 [CAUTION] ==== -**No non-degenerate compositionality.** The repo currently defines the objects (global types, projections, grades, cuts) but does not compose them. All composition theorems are deferred pending K-CUT. +**No non-degenerate compositionality.** The repository's planned interfaces name the objects (global types, projections, grades, cuts) but the current checkout does not yet contain the canonical `src/` definitions or compose them. All composition theorems are deferred pending K-CUT. +==== + +[CAUTION] +==== +**The RapidNJ target is not a proof.** `applications/rapidnj-two-thread.agda` is a standalone typed target with open interfaces and postulates. It is not imported into `All.agda`; the two-thread state diamond, projection square, and K-CUT-LOSS equality remain to be proved. ==== [CAUTION] @@ -109,7 +135,13 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4 | Path | Proves | `src/ChoreographicTypes/` -| Definitions of global types, projection, grades, cuts, K-CUT statements +| Planned definitions of global types, projection, grades, cuts, K-CUT statements + +| `applications/rapidnj-two-thread.adoc` +| RapidNJ application boundary and the two-event proof decomposition + +| `applications/rapidnj-two-thread.agda` +| Open Agda signatures for the state diamond and two-thread K-CUT-LOSS target | `echo-types` (sibling) | `RoleGraded.choreo-grade-commute` (K-CUT-LOSS base case) diff --git a/GLOSSARY.adoc b/GLOSSARY.adoc index c05a67f..1c05b2d 100644 --- a/GLOSSARY.adoc +++ b/GLOSSARY.adoc @@ -64,6 +64,48 @@ K-CUT-WARRANT:: *Classification:* **project-specific** (conjecture). *Status:* **OPEN**. +== Applications + +[[rapidnj-reduction]] +RapidNJ reduction:: + In this repository's application note, one already-selected + RapidNJ-style neighbour-joining update over a global state. The note does + not claim that upstream RapidNJ has the same two-thread batch interface. + *Classification:* **application-specific**. + *See also:* <>, <> + +[[independent-frontier]] +Independent frontier (`Independent₂`):: + A two-event frontier that is an antichain and additionally satisfies the + implementation's read/write disjointness, phase-safety, and deterministic + tie-policy conditions. Antichain membership alone is not enough to justify + concurrent mutation of a RapidNJ state. + *Classification:* **project-specific application predicate**. + *Status:* **OPEN** until instantiated and proved for a concrete reduction + representation. + *See also:* <>, <> + +[[two-thread-diamond]] +Two-thread state diamond:: + The algorithmic equality, up to canonical state equivalence, that applying + two independent reductions in either serialisation gives the same observed + RapidNJ state: `step e2 (step e1 s) ~= step e1 (step e2 s)`. It is a + prerequisite for the K-CUT application, not K-CUT itself. + *Classification:* **application-specific proof target**. + *Status:* **OPEN**. + *See also:* <> + +[[two-thread-k-cut-loss]] +Two-thread K-CUT-LOSS:: + The first non-degenerate K-CUT-LOSS target in the RapidNJ application. For + every endpoint `p` and witnessed independent two-event frontier, the local + grade after the two projected steps equals the transported global loss grade + after the two global steps. The conclusion is an equality of loss grades; + it is not the warrant bound. + *Classification:* **project-specific application conjecture**. + *Status:* **OPEN**. + *See also:* <>, <> + == Patterns [[port-and-reprove]] diff --git a/README.adoc b/README.adoc index 63cec18..4d5b813 100644 --- a/README.adoc +++ b/README.adoc @@ -7,36 +7,74 @@ image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"] -Agda formalisation of a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. The central artefact is the open keystone K-CUT: the conjecture that grading and transport commute with projection across a consistent frontier. +Agda formalisation target for a graded multiparty-session and choreographic +type theory, combining echo loss-grades and epistemic standpoint-warrants. +The central artefact is the open keystone K-CUT: the conjecture that grading +and transport commute with projection across a consistent frontier. == Overview -A global choreographic type `G` is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by: +A global choreographic type `G` is read as a partial causal order. It is +projected to local types (endpoint projection), where each edge is graded by: -* An **echo loss-grade** (from `echo-types`): the structured information loss at that interaction. -* An **epistemic standpoint-warrant** (from `epistemic-types`): the evidence required to authorise that interaction. +* An **echo loss-grade** (from `echo-types`): the structured information loss + at that interaction. +* An **epistemic standpoint-warrant** (from `epistemic-types`): the evidence + required to authorise that interaction. -A **cut** is a consistent frontier (antichain) across the causal order. Loss is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is impossible), indexed by an ordinal loss value. +A **cut** is a consistent frontier (antichain) across the causal order. Loss +is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is +impossible), indexed by an ordinal loss value. -The sole purpose of this repository is to prove or falsify the keystone conjecture **K-CUT**: that grading and transport commute with projection across a cut. +The sole purpose of this repository is to prove or falsify the keystone +conjecture **K-CUT**: that grading and transport commute with projection across +a cut. == The keystone (K-CUT) — OPEN -K-CUT states: grading and transport commute with endpoint projection across a consistent frontier. It splits into two fragments: +K-CUT states: grading and transport commute with endpoint projection across a +consistent frontier. It splits into two fragments: K-CUT-LOSS:: - Grading commutes with projection as an *equality*. Loss is type-determined: the grade of the global cut equals the grade computed locally at the endpoint. - *Status:* **OPEN** (only degenerate single-static-edge base cases exist, proved in sibling repos). + Grading commutes with projection as an *equality*. Loss is type-determined: + the grade of the global cut equals the grade computed locally at the + endpoint. + *Status:* **OPEN** (only degenerate single-static-edge base cases exist, + proved in sibling repos). K-CUT-WARRANT:: - Warrant transport commutes with projection only as a *bound*, and only under a `SoundWarrant` side-condition. The type upper-bounds discoverability but cannot determine it (an agent may know more than the type requires, but never less). + Warrant transport commutes with projection only as a *bound*, and only under + a `SoundWarrant` side-condition. The type upper-bounds discoverability but + cannot determine it (an agent may know more than the type requires, but + never less). *Status:* **OPEN** (no proof exists). [CAUTION] ==== -**Nothing in this repo is proven yet.** Only degenerate single-static-edge base cases exist, located in sibling repositories (`echo-types` `RoleGraded.choreo-grade-commute`, `ChoreoInjective`). This repo exists to hold the formalisation of the general case. +**Nothing in this repo is proven yet.** Only degenerate single-static-edge +base cases exist, located in sibling repositories (`echo-types` +`RoleGraded.choreo-grade-commute`, `ChoreoInjective`). This repo currently +holds the specification, provenance, and application proof targets for the +formalisation of the general case. ==== +== Applications + +Applications are kept in a separate, explicitly non-normative section so that +an algorithm or UI does not get mistaken for a proof of K-CUT. The first case +study is a two-thread RapidNJ-style reduction: + +* link:applications/README.adoc[Applications index] +* link:applications/rapidnj-two-thread.adoc[Two-thread RapidNJ reduction] +* link:applications/rapidnj-two-thread.agda[Agda proof target] + +The smallest target in that case study is the two-event K-CUT-LOSS commuting +square under an `Independent₂` witness. The witness must strengthen +antichain membership with disjoint read/write footprints, phase safety, and a +deterministic tie policy. The application note separates this algorithmic +state diamond from the K-CUT equality and records the warrant component as +deferred. + == What is standard and what is ours [cols="1,2,2", options="header"] @@ -45,15 +83,15 @@ K-CUT-WARRANT:: | Multiparty session / choreographic types | Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) -| Core definitions +| Core definitions (planned) | Endpoint projection from global to local types | Standard -| Projection module +| Projection module (planned) | Dioid/tropical grading of sessions | Standard (various timed/costed session works) -| Re-proved in-site (tropical resource-dioid) +| Re-proved in-site (planned) | Echo loss-grades on choreographic edges | Imported from `echo-types` @@ -65,7 +103,7 @@ K-CUT-WARRANT:: | Assembly of echo + epistemic grades on partial causal orders | **Ours** (assembly) -| Core definitions +| Core definitions (planned) | K-CUT (grading/transport commutes with projection across a cut) | **Ours** (conjecture) @@ -74,20 +112,32 @@ K-CUT-WARRANT:: == Dependencies and the port-and-reprove pattern -This repository imports from the estate's Agda kernel: +The intended repository imports from the estate's Agda kernel: -* `echo-types` — the `ℕ ∪ {∞}` loss-dioid and the `choreo-grade-commute` base case. -* `epistemic-types` — the non-factive `Warrant` / `SoundWarrant` interface (the proof home for the warrant gap in K-CUT-WARRANT). +* `echo-types` — the `ℕ ∪ {∞}` loss-dioid and the `choreo-grade-commute` + base case. +* `epistemic-types` — the non-factive `Warrant` / `SoundWarrant` interface + (the proof home for the warrant gap in K-CUT-WARRANT). -The tropical resource-dioid is **re-proved in-site** rather than imported across kernels. This follows the estate's port-and-reprove pattern (precedent: `typed-wasm/…/Tropical.idr`), ensuring this repo is self-contained at the resource-algebra layer while maintaining logical consistency with `tropical-resource-typing`. +The tropical resource-dioid is **re-proved in-site** rather than imported +across kernels. This follows the estate's port-and-reprove pattern (precedent: +`typed-wasm/…/Tropical.idr`), ensuring that the resource-algebra layer can be +self-contained while maintaining logical consistency with +`tropical-resource-typing`. -Full cited statement of borrowed vs. ours: `dev-notes/2026-06-16-choreographic-types-what-it-is.adoc`. +The full cited borrowed-vs-ours statement is planned for +`dev-notes/2026-06-16-choreographic-types-what-it-is.adoc`. == What this is not -* **NOT Gentzen cut-elimination.** A cut here is a consistent frontier (antichain) of a causal order, not a proof-theoretic cut. +* **NOT Gentzen cut-elimination.** A cut here is a consistent frontier + (antichain) of a causal order, not a proof-theoretic cut. * **NOT a kernel or engine.** Implementation belongs to `typell`. -* **NOT a subdirectory of `echo-types` or `epistemic-types`.** It is a standalone repository registered in `nextgen-typing`. +* **NOT a subdirectory of `echo-types` or `epistemic-types`.** It is a + standalone repository registered in `nextgen-typing`. +* **NOT a claim about an upstream RapidNJ parallel implementation.** The + RapidNJ note is an application-shaped proof target and states its own + refinement boundary. == Repository Layout @@ -96,10 +146,13 @@ Full cited statement of borrowed vs. ours: `dev-notes/2026-06-16-choreographic-t | Path | Purpose | `src/ChoreographicTypes/` -| Agda formalisation (definitions, projection, K-CUT statement) +| Planned Agda formalisation (definitions, projection, K-CUT statement) + +| `applications/` +| Application notes and explicitly open Agda targets | `dev-notes/` -| Design notes, borrowed-vs-ours statement +| Planned design notes and borrowed-vs-ours statement | `.machine_readable/6a2/STATE.a2ml` | Pre-registration state (keystone, provenance, decisions) @@ -107,85 +160,29 @@ Full cited statement of borrowed vs. ours: `dev-notes/2026-06-16-choreographic-t == Build +The current checkout is a documentation and proof-target scaffold; the +planned `src/` tree is not present yet. Once it is added, the intended +standalone build is: + [source,bash] ---- agda --no-libraries -i src src/ChoreographicTypes/All.agda ---- +The application target under `applications/` is intentionally not part of +that command until its interfaces are connected to the canonical definitions. + == Documentation -* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps -* link:Glossary.adoc[Glossary] — terminology reference -* `dev-notes/2026-06-16-choreographic-types-what-it-is.adoc` — full cited statement of foundations +* link:EXPLAINME-new.adoc[EXPLAINME] — current claim-to-implementation map + and known gaps +* link:applications/README.adoc[Applications] — application index +* link:applications/rapidnj-two-thread.adoc[RapidNJ case study] — the + two-thread base-case proof target +* link:GLOSSARY.adoc[Glossary] — terminology reference +* link:EXPLAINME.adoc[Legacy resource-typing EXPLAINME] — retained historical + document == License -SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE].= Choreographic Types — Graded Multiparty Session Fusion -:toc: preamble -:toc-title: Contents -:icons: font -:doctype: article - -image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"] - -Agda formalisation of a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. The central artefact is the open keystone K-CUT: the conjecture that grading and transport commute with projection across a consistent frontier. - -== Overview - -A global choreographic type `G` is read as a partial causal order. It is projected to local types (endpoint projection), where each edge is graded by: - -* An **echo loss-grade** (from `echo-types`): the structured information loss at that interaction. -* An **epistemic standpoint-warrant** (from `epistemic-types`): the evidence required to authorise that interaction. - -A **cut** is a consistent frontier (antichain) across the causal order. Loss is read modally: ∇ contingent (loss may occur) / △ non-contingent (loss is impossible), indexed by an ordinal loss value. - -The sole purpose of this repository is to prove or falsify the keystone conjecture **K-CUT**: that grading and transport commute with projection across a cut. - -== The keystone (K-CUT) — OPEN - -K-CUT states: grading and transport commute with endpoint projection across a consistent frontier. It splits into two fragments: - -K-CUT-LOSS:: - Grading commutes with projection as an *equality*. Loss is type-determined: the grade of the global cut equals the grade computed locally at the endpoint. - *Status:* **OPEN** (only degenerate single-static-edge base cases exist, proved in sibling repos). - -K-CUT-WARRANT:: - Warrant transport commutes with projection only as a *bound*, and only under a `SoundWarrant` side-condition. The type upper-bounds discoverability but cannot determine it (an agent may know more than the type requires, but never less). - *Status:* **OPEN** (no proof exists). - -[CAUTION] -==== -**Nothing in this repo is proven yet.** Only degenerate single-static-edge base cases exist, located in sibling repositories (`echo-types` `RoleGraded.choreo-grade-commute`, `ChoreoInjective`). This repo exists to hold the formalisation of the general case. -==== - -== What is standard and what is ours - -[cols="1,2,2", options="header"] -|=== -| Concept | Status | Home - -| Multiparty session / choreographic types -| Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) -| Core definitions - -| Endpoint projection from global to local types -| Standard -| Projection module - -| Dioid/tropical grading of sessions -| Standard (various timed/costed session works) -| Re-proved in-site (tropical resource-dioid) - -| Echo loss-grades on choreographic edges -| Imported from `echo-types` -| `RoleGraded.choreo-grade-commute` (base case) - -| Epistemic warrants on choreographic edges -| Imported from `epistemic-types` -| `SoundWarrant` side-condition - -| Assembly of echo + epistemic grades on partial causal orders -| **Ours** (assembly) -| Core definitions - -| K-CUT (grading/transport commutes with projection across a cut) +SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE]. diff --git a/applications/README.adoc b/applications/README.adoc new file mode 100644 index 0000000..3a44eef --- /dev/null +++ b/applications/README.adoc @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Choreographic Types — Applications +:toc: preamble +:toc-title: Contents +:icons: font +:doctype: article + +This directory is an application notebook for the K-CUT programme. It is a +place to test the interfaces and proof obligations against a concrete +parallel algorithm without silently turning an application assumption into a +new theorem. + +[CAUTION] +==== +Application notes are **not proofs** and are not part of the Agda build yet. +They may identify a useful target, a missing side-condition, or a +counterexample. The K-CUT status in the repository root remains **OPEN**. +==== + +== Case studies + +[cols="1,2,2", options="header"] +|=== +| Application | Smallest target | Status + +| link:rapidnj-two-thread.adoc[Two-thread RapidNJ reduction] +| The two-event K-CUT-LOSS commuting square for a disjoint antichain frontier, + together with the underlying canonical-state diamond. +| **Open proof target**; no RapidNJ theorem is claimed here. +|=== + +The RapidNJ note is deliberately phrased as a proof boundary: it distinguishes +an algorithmic fact (two disjoint updates commute) from the K-CUT fact (local +grading equals transported global grading). That separation is the part a +consumer such as `metamanifold-webui` can safely use when it displays a proof +status or a frontier certificate. + +== Application discipline + +Every application note should state: + +. which global state and local projection it uses; +. which frontier is an antichain, and which stronger independence condition is + required by the implementation; +. the smallest Agda statement being attempted; +. whether the statement is a proof, an assumption, or an open target; and +. which runtime or UI claims remain outside the formalisation. + +An application must not be used as evidence that K-CUT, RapidNJ correctness, +or a downstream UI integration has been proved. diff --git a/applications/rapidnj-two-thread.adoc b/applications/rapidnj-two-thread.adoc new file mode 100644 index 0000000..49936c0 --- /dev/null +++ b/applications/rapidnj-two-thread.adoc @@ -0,0 +1,187 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += K-CUT application: a two-thread RapidNJ reduction +:toc: preamble +:toc-title: Contents +:icons: font +:doctype: article + +This is the first application note for link:README.adoc[Choreographic +Types]. It uses a RapidNJ-style neighbour-joining reduction as a concrete +shape for the open K-CUT question. It is a proof plan, not a result: the +Agda target is recorded in link:rapidnj-two-thread.agda[the accompanying +file], but it is intentionally not imported into `All.agda` and is not +proved. + +[CAUTION] +==== +This note does **not** claim that upstream RapidNJ has the exact two-thread +batch interface below. It models a possible two-thread schedule around +RapidNJ-style candidate selection and state updates. Establishing that an +implementation exposes this schedule is a separate refinement obligation. +==== + +== Short answer + +The smallest non-degenerate K-CUT lemma is a **two-event loss-grade +commuting square**. Let `s` be a RapidNJ state, `e1` and `e2` the two selected +reductions, and `p` an endpoint. If the two events form a consistent frontier +and are implementation-independent, prove: + +[source,text] +---- +localGrade p + (localStep p e2 (localStep p e1 (project p s))) + == +transportLoss p (globalGrade (step e2 (step e1 s))) +---- + +where `==` is Agda propositional equality (`_≡_`), not an observational +claim made by the UI. The same proof obligation must be invariant under the +other serialisation of the frontier: + +[source,text] +---- +step e2 (step e1 s) ~= step e1 (step e2 s) +---- + +Here `~=` is *canonical RapidNJ-state equivalence*, not necessarily raw record +equality: map iteration order, row-cache layout, and other representation +details must not affect the state observed by the grade or by projection. + +In words: execute the two independent reductions in either order, project to +`p`, and compute the local loss grade; it must equal transporting the global +loss grade across the same two-event cut. This is the smallest frontier larger +than the already-known single-edge case. It is the right gate before an +induction over arbitrary antichains. + +== What is being modelled + +RapidNJ accelerates the search for neighbour-joining pairs while retaining the +neighbour-joining optimisation criterion. The application boundary here is +narrower: + +* `State` contains the active clusters, distance data, row sums, and any + search/index state whose mutation is relevant to the reduction; +* `step e s` applies one already-selected join or reduction event to the + global state; +* `project p s` is the endpoint/local view used by the choreography; +* `localStep p e` is the corresponding local event, or the identity when `p` + does not observe `e`; +* `globalGrade` accumulates the echo loss grade at the frontier; +* `localGrade` computes the grade from the projected state; and +* `transportLoss` transports the global loss grade to endpoint `p`. + +This is intentionally below the search heuristic. Proving that two candidate +pairs are selected, tie-broken, and safe to batch belongs to the RapidNJ +refinement layer. K-CUT should not be used to hide that algorithmic proof. + +== The frontier and the missing side-condition + +An antichain is necessary but is not by itself sufficient for a parallel +RapidNJ update. Two events can be incomparable in the causal order and still +race on a shared distance-matrix entry or on a cached row bound. Define an +`Independent2 s e1 e2` witness that contains at least: + +. `e1` and `e2` are incomparable, so `{e1, e2}` is a consistent frontier; +. the selected cluster pairs are distinct and share no cluster; +. the read/write footprints of the two updates are disjoint, or a proved + commutation rule covers their shared reads; +. both events observe the same reduction phase and pre-state; and +. the candidate/tie-breaking policy is deterministic, or its permitted + equivalence is included in canonical state equivalence. + +The first item is the choreographic condition. The remaining items are the +algorithm-specific strengthening needed to justify treating the frontier as a +parallel reduction. In the accompanying Agda target, `Independent2` implies +`Antichain2`; it is not defined as mere antichain membership. + +== Separate the two diamonds + +There are two equalities here, and conflating them would make the application +look proved when it is not. + +=== 1. RapidNJ state diamond + +First establish the implementation/refinement lemma: + +[source,text] +---- +rapidnj-two-thread-diamond : + Independent2 s e1 e2 -> + step e2 (step e1 s) ~= step e1 (step e2 s) +---- + +This is an algorithmic statement. It should be proved using the disjoint +footprints and then lifted through canonicalisation. It is not K-CUT. + +=== 2. K-CUT-LOSS at the two-event cut + +Then establish, for every endpoint `p`, the equality in the short answer: + +[source,text] +---- +two-thread-K-CUT-LOSS : + Independent2 s e1 e2 -> + localGrade p + (localStep p e2 (localStep p e1 (project p s))) + == + transportLoss p (globalGrade (step e2 (step e1 s))) +---- + +The state diamond supplies schedule independence. Projection naturality for +each selected event and the grade composition law supply the two legs of the +square. The target is still an equality of **loss** grades; it does not assert +the warrant component. + +A useful proof trace is therefore: + +[source,text] +---- +local serialisation 1 + == transported global serialisation 1 + == transported global serialisation 2 -- state diamond + grade congruence + == local serialisation 2 +---- + +The first and last steps are the K-CUT-LOSS work. The middle step is the +RapidNJ diamond. Keeping those obligations separate makes failures +informative: a counterexample can be an unsafe batch, a projection mismatch, +or a grading mismatch. + +== Why this is the smallest useful target + +* A one-event frontier is the degenerate single-static-edge shape already + represented by `RoleGraded.choreo-grade-commute` in `echo-types`. +* Two events are the first frontier on which antichain independence and + serialisation order can differ. +* An arbitrary `k`-event frontier can be reached only after showing that a + permitted adjacent swap preserves the state, projection, and grade. The + two-event square is exactly that local swap. +* Proving the full NJ tree, the RapidNJ search heuristic, or a UI result first + would introduce unrelated algorithmic and representation obligations. + +Thus the recommended first theorem is not “parallel RapidNJ is correct”. It +is the loss-only, two-event square under an explicit `Independent2` witness. + +== What is deliberately deferred + +`K-CUT-WARRANT` remains a separate target. Its conclusion is a bound under +`SoundWarrant`, not the equality above, and this application note does not +invent a warrant proof. Likewise deferred are: + +* the proof that a concrete RapidNJ implementation exposes the selected + disjoint events; +* preservation of metric assumptions and the final unrooted tree; +* performance, scheduling, and memory claims; and +* any trust claim made by `metamanifold-webui` from a displayed trace. + +A downstream UI may display the frontier, the two serialisations, and the +status **open / proved / refuted** once a checked certificate exists. Until +then, it must treat this note and the Agda target as research metadata, not as +a certificate. + +== References + +* Martin Simonsen, Thomas Mailund, and Christian N. S. Pedersen, link:https://users-birc.au.dk/cstorm/software/rapidnj/papers/SimonsenOthers2008_WABI.pdf[Rapid Neighbour-Joining (WABI 2008)]. +* link:https://github.com/johnlees/rapidnj[RapidNJ source repository] (implementation reference; not a proof dependency). +* link:../README.adoc[Choreographic Types README] for the K-CUT-LOSS / K-CUT-WARRANT split. diff --git a/applications/rapidnj-two-thread.agda b/applications/rapidnj-two-thread.agda new file mode 100644 index 0000000..1b39dd4 --- /dev/null +++ b/applications/rapidnj-two-thread.agda @@ -0,0 +1,62 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- +-- Typed target for the first RapidNJ application. This file is deliberately +-- standalone and is not imported by the repository build: every declaration +-- below is an open interface or an open conjecture, not a proof. +module Applications.RapidNJ.TwoThread where + +open import Agda.Builtin.Equality using (_≡_) + +postulate + Role : Set + State : Set + LocalState : Set + Event : Set + Grade : Set + + -- Canonical equivalence hides representation-only differences such as + -- finite-map iteration order. It is not assumed to be raw equality. + StateEq : State → State → Set + + -- The two events are a consistent frontier when they are incomparable. + Antichain2 : Event → Event → Set + + project : Role → State → LocalState + step : Event → State → State + localStep : Role → Event → LocalState → LocalState + + globalGrade : State → Grade + localGrade : Role → LocalState → Grade + transportLoss : Role → Grade → Grade + + -- This is intentionally stronger than Antichain2. It must encode the + -- implementation's read/write and phase-safety conditions as well as + -- frontier membership. + Independent2 : Event → Event → State → Set + + independentToAntichain : + ∀ {e1 e2 s} → Independent2 e1 e2 s → Antichain2 e1 e2 + + -- Algorithmic prerequisite: the two selected reductions form a canonical + -- state diamond. This is not itself K-CUT. + twoThreadDiamond : + ∀ {e1 e2 s} → + Independent2 e1 e2 s → + StateEq (step e2 (step e1 s)) + (step e1 (step e2 s)) + + globalGradeRespectsStateEq : + ∀ {s t} → StateEq s t → globalGrade s ≡ globalGrade t + + -- Smallest non-degenerate K-CUT-LOSS target. The proof must be supplied + -- for every endpoint and every witnessed independent two-event frontier. + twoThreadKCutLoss : + ∀ {p e1 e2 s} → + Independent2 e1 e2 s → + localGrade p + (localStep p e2 (localStep p e1 (project p s))) + ≡ + transportLoss p (globalGrade (step e2 (step e1 s))) + +-- K-CUT-WARRANT is intentionally absent: its first application theorem has a +-- different conclusion (a bound under SoundWarrant), not this equality.