feat(abi): L16 K-CUT-LOSS, parametric in the grade kernel (PWL-01, PR C)

CHANGELOG.adoc

@@ -9,6 +9,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== L16 K-CUT-LOSS, parametric in the grade kernel (PWL-01 step 4, 2026-10-14)
+
+* New `KCut.idr` ports and re-proves choreographic-types `KCut.kcut-loss` @
+  `edb784a` over the kernel's `ResourceAlgebra` interface: graded global and
+  local types, cuts, projection with plain merge, consistency, and
+  `projCut` / `gradeProj` / `cutProjectable` / `kcutLoss` (K-1, K-2, K-3, K-5).
+  It is discharged at Loss, MaxPlus and HWM (K-6), and the upstream worked
+  broker protocol is evaluated in all three.
+* `Choreography.idr`: `GradedChoreography g` with `PartiesDeclared`, the
+  obligation `L16KCutLoss`, and its discharge `l16KCutLoss = kcutLoss`. Tying
+  the graded protocol to `messages` / `LegalTrace` is DESIGNED.
+* Rejects `UnprojectableChoice` and `InconsistentCut` (K-7), each refused on
+  the equality itself. `tools/check-kernel-proofs.sh` also checks upstream
+  `KCut.agda` and its two rejects at the pin.
+* `KCut` re-exports `Decidable.Equality` and the kernel interface, so
+  consumers can compute a concrete protocol's grades by evaluation.
+
 ==== L11 / L12 / L13 read through the grade kernel (PWL-01 steps 2–3, 2026-10-14)
 
 * *L11.* `CostBounded c n` is proved equal to the kernel's Loss order

LEVEL-STATUS.adoc

@@ -206,11 +206,21 @@ parser/Checker tests |*v1.4 — Idris2 proof + surface checker (L15-A +
 L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering
 DONE (task #9)*
 
-|16 |Agent choreography |Choreography.idr |(future) |12 parser/Checker
+|16 |Agent choreography |Choreography.idr + KCut.idr |(future) |12 parser/Checker
 tests |*v1.5 — composition proof over L13+L14+L15 live; surface checker
 enforces L16-A (role targets exist), L16-B (message endpoints declared),
 L16-C (payload primitive/declared region ref), L16-D (exact
-`+L13 + L14 + L15+` composition spec).*
+`+L13 + L14 + L15+` composition spec). PWL-01 step 4: grades drawn from
+the kernel — `+GradedChoreography g+` for any `+ResourceAlgebra g+`, with
+the K-CUT-LOSS obligation `+L16KCutLoss+` discharged by `+l16KCutLoss+` =
+`+KCut.kcutLoss+`, a port and re-proof of choreographic-types
+`+KCut.kcut-loss+` @ `+edb784a+` (K-1/K-2/K-3/K-5, and K-6 at Loss,
+MaxPlus, HWM: PROVEN in Idris2; correspondence ASSUMED; K-7 TESTED by
+`+tests/reject/{UnprojectableChoice,InconsistentCut}.idr+`; K-4 not
+re-checked here). Fragment: finite, binary choice, plain merge,
+synchronous. That the graded protocol IS the choreography's
+`+messages+` / `+LegalTrace+` is DESIGNED (only `+PartiesDeclared+` is
+checked); asynchrony OPEN upstream.*
 |===
 
 *[sfap]* = "`so far as possible`" — proofs are machine-checked in Idris2
@@ -315,7 +325,16 @@ envelope (via `+subsumeCompose+`) AND the combined L15 module envelope
 (via `+containedConcat+` + `+l15bSoundness+`). Closes post-A10 audit
 item 3.
 
-|Choreography.idr |0 |0 |0 |In package (v1.5 / L16)
+|Choreography.idr |0 |0 |0 |In package (v1.5 / L16). PWL-01 step 4:
+`+GradedChoreography+`, `+PartiesDeclared+`, `+L16KCutLoss+` /
+`+l16KCutLoss+`.
+
+|KCut.idr |0 |0 |0 |In package (PWL-01 step 4, 2026-10-14). K-CUT-LOSS
+parametric in the grade kernel: graded `+Global+` / `+Local+` types,
+`+Cut+` / `+LCut+`, projection with plain merge, `+Consistent+`;
+`+projCut+`, `+gradeProj+`, `+cutProjectable+`, `+kcutLoss+`, the three
+instance discharges and the worked broker protocol (computed readings
+TESTED). Port of choreographic-types @ `+edb784a+`.
 
 |Proofs.idr |0 |0 |0 |In package. Attestation API hardened A7
 (2026-04-18): every L1-L10 attestation now requires a witness from its

scripts/fetch-siblings.sh

@@ -11,15 +11,19 @@
 #                       checks the operation tables against this tree in Agda.
 #   occupancy-types   — the reclamation law (R-1..R-6) that
 #                       src/abi/TypedWasm/ABI/Occupancy.idr ports for L13.
+#   choreographic-types — K-CUT-LOSS, which src/abi/TypedWasm/ABI/KCut.idr
+#                       ports for L16.
 #
 # Re-pin deliberately, one commit per pin, and update the module headers that
 # cite the pin in the same commit.  Override for a local experiment with
-#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_TYPES_COMMIT=<sha> scripts/fetch-siblings.sh
+#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_TYPES_COMMIT=<sha> \
+#   CHOREOGRAPHIC_TYPES_COMMIT=<sha> scripts/fetch-siblings.sh
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
 OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}"
+CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}"
 
 fetch() { # fetch <name> <commit>
   local name="$1" commit="$2" dir="_build/dependencies/$1"
@@ -41,3 +45,4 @@ fetch() { # fetch <name> <commit>
 
 fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
 fetch occupancy-types "$OCCUPANCY_TYPES_COMMIT"
+fetch choreographic-types "$CHOREOGRAPHIC_TYPES_COMMIT"

src/abi/TypedWasm/ABI/Choreography.idr

@@ -19,10 +19,13 @@ module TypedWasm.ABI.Choreography
 
 import Data.List
 import Data.List.Elem
+import Data.Nat
 
 import TypedWasm.ABI.ModuleIsolation
 import TypedWasm.ABI.SessionProtocol
 import TypedWasm.ABI.ResourceCapabilities
+import TypedWasm.ABI.ResourceAlgebra
+import public TypedWasm.ABI.KCut
 
 %default total
 
@@ -239,3 +242,58 @@ traceSoundness c tr legal =
     (collectIsolation c.realisations c.compositionWitness)
     (collectSessionLinearity c.realisations c.compositionWitness)
     (collectCapabilityContainment c.realisations c.compositionWitness)
+
+-- ============================================================================
+-- Graded choreographies and K-CUT-LOSS (PWL-01 step 4, 2026-10-14)
+-- ============================================================================
+--
+-- The composition theorem above says nothing about grades.  This section
+-- adds them: a choreography's protocol graded in ANY algebra of the grade
+-- kernel (TypedWasm.ABI.ResourceAlgebra), with the K-CUT-LOSS obligation
+-- stated for it and discharged by TypedWasm.ABI.KCut.kcutLoss — a port and
+-- re-proof of choreographic-types `KCut.kcut-loss` @ edb784a (correspondence
+-- ASSUMED; see KCut.idr).  Fragment: finite messages and binary choice,
+-- plain merge, synchronous.
+--
+-- DESIGNED, not proved: that the graded protocol is the choreography's own
+-- (its messages are the declared `messages`, its runs the `LegalTrace`s).
+-- `PartiesDeclared` only checks that every party index names a declared
+-- role.  Asynchrony (queues) is OPEN upstream.
+
+||| Every party index in a protocol is below `n` (here: names a declared role).
+public export
+data PartiesDeclared : (n : Nat) -> Global g -> Type where
+  DEnd    : PartiesDeclared n End
+  DMsg    : {s, r : Party} -> {x : g} -> {gl : Global g} ->
+            LT s n -> LT r n -> PartiesDeclared n gl ->
+            PartiesDeclared n (Msg s r x gl)
+  DChoice : {s, r : Party} -> {x : g} -> {l, k : Global g} ->
+            LT s n -> LT r n -> PartiesDeclared n l -> PartiesDeclared n k ->
+            PartiesDeclared n (Choice s r x l k)
+
+||| An L16 choreography with a graded protocol over its roles: party i is
+||| the i-th declared role.
+public export
+record GradedChoreography (g : Type) where
+  constructor MkGradedChoreography
+  ||| The L16 choreography (roles, messages, realisations, L13–L15 witness).
+  choreography : Choreography
+  ||| Its protocol, graded in the kernel algebra `g`.
+  protocol     : Global g
+  ||| Every party in the protocol is a declared role.
+  declared     : PartiesDeclared (length choreography.roles) protocol
+
+||| The L16 K-CUT-LOSS obligation: at every consistent cut, every party reads
+||| on its own timeline exactly its share of the global grade.
+public export
+L16KCutLoss : {g : Type} -> ResourceAlgebra g => GradedChoreography g -> Type
+L16KCutLoss gc =
+  (p : Party) -> (c : Cut gc.protocol) -> Consistent p c ->
+  gradeAt p (cutGlobal gc.protocol c) = lgrade (cutLocal (proj p gc.protocol) (cutproj p c))
+
+||| Discharged for every graded choreography, parametrically in the grade
+||| algebra: KCut.kcutLoss.  At Loss this is the echo-loss reading, at MaxPlus
+||| worst-case cost, at HWM occupancy (KCut.kcutLossLoss / MaxPlus / HWM).
+public export
+l16KCutLoss : {g : Type} -> ResourceAlgebra g => (gc : GradedChoreography g) -> L16KCutLoss gc
+l16KCutLoss gc p c k = kcutLoss p gc.protocol c k