A pre-registration and research notebook for a graded multiparty-session and
choreographic type theory, combining echo loss-grades and epistemic
standpoint-warrants. Agda is the prover: the finite, binary-choice, plain-merge,
synchronous fragment is checked under a pinned --safe --without-K gate (see
Validation), and PROOF-STATUS ledgers what is and is
not proved. The central artefact is the keystone K-CUT — proved for that
fragment and open beyond it — the statement that grading and transport
commute with projection across a consistent frontier.
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.
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, restricted to the endpoint, equals the grade read locally at the endpoint up to the projected cut. Status: PROVEN for the finite binary-choice, plain-merge fragment, 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 byscripts/minimal-laws.sh). Recursion, full merge and asynchrony remain OPEN. See PROOF-STATUS.adoc. - K-CUT-WARRANT
-
Warrant transport commutes with projection only as a bound, and only under a
SoundWarrantside-condition. Status: PROVEN in bound form for the same fragment (src/Choreographic/Bound.agda): in a Kripke frame whose worlds are consistent cuts and whose accessibility is sameness of local view, every party knows its restricted grade (aSoundWarrantin epistemic-types' own interface, imported) and knows a one-sided bound on the global grade, whose direction depends on where the sequence unit sits in the algebra’s order. The transport component is in too: the local frontier is known at every world (receiving is knowing it was received), party access "q sees at least what p sees" is epistemic-types'Preorderinstantiated, and knowledge is monotone along it — a lawful world-indexedAccessibleModality. OPEN beyond the fragment: recursion, full merge, asynchrony, data-dependent warrants. See PROOF-STATUS.adoc.
|
Note
|
The single-static-edge base case in echo-types
( |
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:
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.
| Concept | Status | Home |
|---|---|---|
Multiparty session / choreographic types |
Standard (Honda–Yoshida–Carbone, Montesi, Hirsch–Garg, Bocchi–Yoshida) |
|
Endpoint projection from global to local types |
Standard |
|
Dioid/tropical grading of sessions |
Standard (various timed/costed session works) |
Imported from |
Echo loss-grades on choreographic edges |
Imported from |
|
Epistemic warrants on choreographic edges |
Imported from |
|
Assembly of echo + epistemic grades on partial causal orders |
Ours (assembly) |
|
K-CUT (grading/transport commutes with projection across a cut) |
Ours (conjecture) |
|
The development imports three siblings of the estate’s Agda kernel, each at
one pinned commit fetched by scripts/fetch-siblings.sh (a full SHA,
verified after checkout; the gate fails on a mismatch):
-
resource-algebra— the parametricResourceAlgebra(alternatives ⊕, sequence ⊗, the induced order ≼; dioid, ordered and annihilating layers) and theLoss(min-plus, ℕ ∪ {∞}),MaxPlus(ℕ ∪ {−∞}) andHWMinstances. Same kernel: imported, not re-proved. -
epistemic-types—Warrant/SoundWarrantandAccess.Preorder, imported, not imitated (the proof home for the warrant side of K-CUT-WARRANT). -
echo-types—experimental/echo-additive/Grade.agda, the echo-additive ℕ ∪ {∞} grade.src/Choreographic/Base/EchoAdditive.agdapackages it as aResourceAlgebrafrom echo-types' own lemmas and proves it agrees withLossoperation for operation, so "min-plus" and "echo-additive" are one checked algebra, not two transcriptions. That module is the only one that needs the Agda standard library (through echo-types) and is checked as its own root, so the keystone stays builtins-only.
The tropical algebra was re-proved in-site, in resource-algebra
(Instances/MaxPlus.agda), rather than imported across kernels, following
the estate’s port-and-reprove pattern (precedent: typed-wasm/…/Tropical.idr).
The named cross-prover bridge obligation — that MaxPlus agrees with
tropical-types' Lean 4 instance : CommSemiring Tropical — is
resource-algebra’s ledger row M-2 and is OPEN there. This repository inherits
it: every MaxPlus discharge (kcut-loss-MaxPlus, kcut-warrant-MaxPlus)
carries the Lean theorem as provenance, never as an import. See
docs/pre-registration-addendum-2026-10-13.adoc.
The research intent, borrowed-vs-ours ledger and outstanding obligations are preserved in the pre-registration record.
-
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-typesorepistemic-types. It is a standalone repository registered innextgen-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.
| Path | Purpose |
|---|---|
|
The checked development ( |
|
Expected rejections: each must fail at its |
|
A deliberately impoverished |
|
The proof gate, as run by |
|
The ledger: every claim with PROVEN / TESTED / ASSUMED / DESIGNED / OPEN and the module that discharges it; every cited name is bound to its definition, and the definition’s comment back to the row, by the integrity check |
|
Application notes and explicitly postulated Agda targets (not proofs) |
|
Research state, provenance and outstanding proof obligations |
|
Owner-only Actions policy repair and verification |
|
Documentation integrity and regression checks (not proof checking) |
The proof gate is .github/workflows/proofs.yml: a digest-pinned Debian 13
container with agda-bin=2.6.4.3-1+b2 and agda-stdlib=2.1-4 from the
distribution, siblings fetched at pinned commits, and every module checked
with --safe --without-K --no-libraries --ignore-interfaces --double-check
-W error. To run it locally with that Agda (any other version is refused;
set AGDA_VERSION to check deliberately with another):
bash scripts/fetch-siblings.sh # resource-algebra, epistemic-types, echo-types at their pins
bash scripts/check.sh # core proofs, echo-additive instance, expected rejections
bash scripts/minimal-laws.sh # which laws K-CUT-LOSS usesapplications/rapidnj-two-thread.agda is not part of the gate: it is a
postulated target, not a proof (see PROOF-STATUS.adoc).
The documentation integrity checks are structural only and never evidence that anything is proved. With Node.js 22 or newer:
node scripts/check-repository.mjs
node --test tests/*.test.mjsSee src/Choreographic/ and PROOF-STATUS.adoc: K-CUT-LOSS and both components of K-CUT-WARRANT are proved for the finite, binary-choice, plain-merge, synchronous fragment, parametric in resource-algebra, and checked by the gate above on every pull request and every push to main since 2026-10-13. The plan below is kept as the record of what was planned.
-
EXPLAINME — claim-to-implementation map and known gaps
-
Applications — application index
-
RapidNJ case study — the two-thread base-case proof target
-
Glossary — terminology reference
SPDX-License-Identifier: MPL-2.0 — see LICENSE.