Repository navigation
feat(abi): L16 K-CUT-LOSS, parametric in the grade kernel (PWL-01, PR C) - #274
Merged
Merged
Conversation
… again E2E Validation and Static Analysis Gate have been `startup_failure` on main since 554345c (#268): Dependabot bumped setup-node 7.0.0 -> 7.1.0, upload-artifact 7.0.1 -> 7.0.2, download-artifact 8.0.1 -> 8.0.2 and setup-ocaml 3.8.0 -> 3.9.0 without a lock refresh, the same failure #266 fixed two commits earlier. A ref absent from .github/workflows/actions.lock is a ref the organisation does not allow, so the workflow is rejected before any job runs. This reverses exactly #268's four workflow edits, back to the refs the lock declares. It does not prevent recurrence: the next grouped actions bump will drift again unless the lock is regenerated with it (owner decision). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
With E2E Validation able to start again, its structural and smoke jobs
fail on paths that moved without the tests following (pre-existing on
main, masked by the startup_failure):
tests/e2e.sh LEVEL-STATUS.md -> LEVEL-STATUS.adoc, and the
row pattern "| N |" (Markdown) -> "^|N |"
(AsciiDoc), so all 12 rows are really checked
tests/aspect/claim-envelope LEVEL-STATUS / PROOF-NEEDS / TEST-NEEDS .md
-> .adoc in the RSR list and the L11/L12
cross-check
tests/aspect/security-envelope .well-known/security.txt
-> www/.well-known/security.txt
README.adoc, ROADMAP.adoc docs/WHITEPAPER.md -> docs/WHITEPAPER.adoc
Locally: tests/e2e.sh (E2E_BUILD=0) 47 passed / 0 failed (was 35 / 1),
claim-envelope 57 / 0 (was 51 / 5), security-envelope 10 / 0 (was 9 / 1).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
src/abi/TypedWasm/ABI/ResourceAlgebra.idr transcribes
hyperpolymath/resource-algebra Core.agda @ cf9235c: the ResourceAlgebra
interface (alternatives an idempotent commutative monoid, sequence a
monoid), the induced order and its lemmas, and IsOrdered / IsDioid /
IsAnnihilating as separate interfaces, as in Agda, with "every dioid is
ordered" as dioidMonoL/R and the named implementation dioidOrdered.
ResourceAlgebra/{Loss,MaxPlus,HWM}.idr transcribe Instances/*.agda clause
for clause (constructors renamed fin/inf -> Finite/Infinity, val/bot ->
Val/Bot, hwm -> MkHWM; clause order kept, so both sides reduce alike).
Separation.idr carries the S-1..S-3 witnesses. ResourceAlgebra/Nat.idr
holds only the Nat lemmas Idris2's base lacks: base's Data.Nat.minimum /
maximum / LTE are the Agda Prelude's min / max / ≤ clause for clause, so
they are used rather than declared again.
scripts/fetch-siblings.sh fetches resource-algebra at the pin into
_build/dependencies (the residual-evidence-types pattern).
All laws re-proved under %default total with no believe_me /
assert_total; the package builds clean under Idris2 0.8.0 (30 modules).
Correspondence to the Agda source: ASSUMED (transcription).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Tropical.TropCost is now the kernel's Loss carrier (TropCost = LossGrade; tropAdd = lossAlt, tropMul = lossSeq). The twelve semiring axioms and the dioid-order layer are derived from the kernel's instance proofs instead of re-proved over a private copy; the local tropMin and natMax are deleted (base's minimum / maximum serve the bottleneck layer). Every public name and direction is kept, so Epistemic.idr and Proofs.idr compile unchanged. The header no longer says max-plus tracks the bottleneck: TropCost is min-plus and tropMax is min-max (choice min, sequence max, +inf absorbing), which is neither min-plus nor max-plus. tropMax stays local because the kernel has no MinMax instance. Echo.idr names its loss grade from the same kernel instance (EchoGrade, echoKeep = oneG, echoCollapse = zeroG) and defines no grade operation. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
tools/check-grade-kernel.sh is the grep gate for "one definition of
min-plus and one of max-plus": no tracked .idr file may define a Nat
min/max (base's are the one definition), no file outside the kernel may
define a grade operation (op (C x) (C y) = C (min/max/+ ...)), and the
kernel must hold exactly the two in Loss.idr and the two in MaxPlus.idr.
--self-test is its negative control (8 seeded duplicates caught, kernel
shapes and near-misses not). Run against main's Tropical.idr it fails on
tropMin / natMax / tropAdd / tropMul, as it should. tools/grade-kernel.allow
lists the one exception, Tropical.tropMax (MinMax bottleneck), with why it
is neither algebra.
tools/check-kernel-proofs.sh runs, failing (never skipping) without
idris2 0.8.0 and agda:
- resource-algebra's own check at the pin (Agda --safe --without-K
--no-libraries --double-check, 3 rejects);
- a clean idris2 --build of the ABI, exit 0 AND no Error line;
- tests/reject/*.idr: each refused at its invalid declaration with its
EXPECT message, not for a scope/parse/path reason;
- tests/transcription: the port, evaluated by Explore.idr, reproduces
ops.tsv (172 rows); Agda accepts every row by refl against the PINNED
instances and Idris2 by Refl against the port (244 equalities each);
every row of wrong-rows.tsv is refused by both.
Both run in contract-gate.yml (new jobs grade-kernel and kernel-proofs):
actions.lock is keyed by workflow path, so a new workflow file would be
rejected at startup; this one already holds the only action used.
Idris2 0.8.0 is built from its tag (no binaries are published).
tests/proof/regression.mjs pins 31 kernel names.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…ELOG LEVEL-STATUS row 11 and the proof inventory say what the code now does (TropCost = LossGrade; tropMin / natMax deleted); a new inventory row and a "Grade kernel (PWL-01)" section give the kernel's statuses with their artefacts: laws PROVEN in Idris2; correspondence to the Agda source ASSUMED, TESTED on the 172-row table; separation TESTED. It records the correction that Tropical.idr was never max-plus. No level changes status. CONTRACT.adoc: the grade gates under Enforcement, and why contract.abi.sha256 does not change (the I3 anchors cover section.rs's wire format, not src/abi). spec: the L11 sentence no longer claims max-plus for throughput. Also replaces one stray NBSP in LEVEL-STATUS. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
CHANGELOG.adoc never carried one; this branch is the first to touch it since the licence-consistency check started looking at changed docs, so add the CC-BY-SA-4.0 identifier the other .adoc files use. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…uash merges) #270 and #271 were squash-merged into main, so their commits on this branch are not ancestors of main. Merging main back in (rather than force-pushing a rebased branch) keeps the branch's published history; the trees agree except for the SPDX header commit, which is not yet on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
L11 (Tropical.idr). The numeric bound CostBounded c n is proved to BE the kernel's Loss order, Finite n ≼ c (costBoundedIsLossOrder / lossOrderIsCostBounded), so path bounds compose by the kernel's otimesMono (costBoundedSeq) rather than by a new argument. A new Level11WorstCaseProof grades a branching access plan in MaxPlus (worst case: + along Then, max at OneOf) with worstCaseThen / worstCaseOneOf from otimesMono / oplusMono and worstCaseFinite / worstCaseWithin reading the bound in ℕ. The obligation is DESIGNED (no surface syntax or attestation uses it). Level11BottleneckProof is MinMax and is left as it is; it is not MaxPlus (tests/reject/TropicalIsNotMaxPlus.idr), and tests/reject/WorstCaseIsCheapest.idr refuses reading MaxPlus's choice as the cheaper branch. L12 (Epistemic.idr, additive). stalenessGrade is a reader's lag as a Loss grade: fresh is the kernel's 𝟙 (freshHasNoStaleness), stale is not (staleHasStaleness), never synced is 𝟘 (neverSyncedIsCollapse), 𝟙 is the top (freshIsTop), and a relayed lag is the kernel's ⊗ (stalenessRelay). syncGrade gains a note: its number is a version, not a loss. Kernel additions (typed-wasm's own, labelled; not transcription): each instance's order read in ℕ (Loss: Finite n ≼ Finite k iff k ≤ n; MaxPlus: Val m ≼ Val n iff m ≤ n), and min/max-vs-LTE lemmas plus maxLub in ResourceAlgebra/Nat.idr. No operation changes, so the transcription table is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
…ndary
src/abi/TypedWasm/ABI/Occupancy.idr ports and re-proves occupancy-types
@ af95728 (Order / Timeline / Reclaim / Witness .agda) over the kernel's
HWM instance: R-1 cutFactor (the grade factors at every cut, in any
resource algebra), R-2 reclaimLaw / occupancyAtCut (the suffix starts from
the prefix's drift), R-3 occupancyLeCost / protocolOccupancyLeCost, R-4
noReclaim / reclaimed, R-5 the occupancy-4 / cost-7 witness. R-6 is
tests/reject/{CostIsOccupancy,DriftIsPeak}.idr. Statement correspondence:
ASSUMED (port-and-reprove).
L13 binding, DESIGNED (no operational semantics or checker behind it):
OccupancyGradedMemory carries a private memory's run and proof that its
peak fits the declared maximum; BoundaryCut is a run cut at a declared
boundary, boundaryFrees = peak − drift of the prefix, boundaryOccupancy is
R-2 there, and fitsAcrossBoundary is the budget rule (the run after the
boundary fits in what the boundary left). striated regions are surface
syntax only, so their occupancy is OPEN.
scripts/fetch-siblings.sh pins occupancy-types at af95728;
tools/check-kernel-proofs.sh runs its own Agda check (core + 2 rejects)
against our resource-algebra pin (its own, b2c9f1f, differs from cf9235c
only by a workflow file).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Rows 11, 12 and 13 now say which kernel artefact each obligation draws on and with what status: PROVEN for the Idris2 theorems, ASSUMED for the port's correspondence to occupancy-types, DESIGNED for the worst-case obligation and the L13 binding, OPEN for striated occupancy. No row moves to achieved; L11 and L12 stay draft. New inventory row for Occupancy.idr, CHANGELOG entry, reject README rows, and 18 names pinned in tests/proof/regression.mjs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
cargo-verify (E2E Validation) fails before compiling anything:
error: failed to parse lock file ... package `wasmparser` is
specified twice in the lockfile
Three Dependabot PRs (#231 wasm-encoder, #232 wasmprinter, #233
wasmparser), each moving to 0.256.0, merged on top of each other and left
two `wasmparser 0.256.0` entries plus a stale 0.255.0 one that a crate
still pointed at. It went unseen because E2E Validation was
startup_failure until #270.
The lock was rewritten by cargo itself (`cargo metadata` after dropping
the duplicated entry), not by hand: one dependency edge 0.255.0 -> 0.256.0,
the 0.255.0 entry and the duplicate removed, nothing upgraded.
`cargo build --workspace --locked` and `cargo test --workspace --locked`
pass (all test binaries ok).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
The four staleness lemmas auto-bound `mod` and `field`, adding four
"implicitly bind ... shadowing Prelude.Num.mod / FieldVersion.field"
warnings to the build (28 against main's 24). Binding them explicitly as
`{0 m : ModuleId} -> {0 f : String}` returns the build to main's 24
warnings, none from this PR. No statement changes.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
src/abi/TypedWasm/ABI/KCut.idr ports and re-proves choreographic-types
KCut.kcut-loss @ edb784a over the kernel's ResourceAlgebra interface:
graded Global / Local types, Cut / LCut and their truncations, projection
with plain merge, Projectable, Consistent, and the three lemmas K-CUT-LOSS
is assembled from — projCut (K-2, no algebra laws), gradeProj (K-3,
seqUnitL and altIdem only), cutProjectable (K-5) — giving kcutLoss (K-1).
Discharged at Loss, MaxPlus and HWM (K-6); the upstream worked broker
protocol is evaluated in all three (Loss 8 / 3 at the cut, MaxPlus 8,
HWM peak 5 / 2 at the cut). K-4 is not re-checked here. Statement
correspondence: ASSUMED (port-and-reprove).
Choreography.idr: GradedChoreography g (any kernel algebra) with
PartiesDeclared, the obligation L16KCutLoss and its discharge
l16KCutLoss = kcutLoss. That the graded protocol is the choreography's
own messages / LegalTrace is DESIGNED; asynchrony is OPEN upstream.
tests/reject/{UnprojectableChoice,InconsistentCut}.idr (K-7): each is
refused on the equality itself (1 vs 2), so both side-conditions are
load-bearing. Getting them there showed that a consumer could not reduce
a concrete protocol's grades: role unfolds to base's decEq, which a module
only evaluates if it imports Decidable.Equality. KCut now re-exports it
and the kernel interface.
scripts/fetch-siblings.sh pins choreographic-types at edb784a;
tools/check-kernel-proofs.sh checks upstream KCut.agda (it needs only
resource-algebra) and its two rejects, each refused with "1 != 2".
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Row 16 now states the graded L16 fragment with its statuses — K-1/2/3/5/6 PROVEN in Idris2, correspondence ASSUMED, K-7 TESTED, K-4 not re-checked, the protocol-to-choreography tie DESIGNED, asynchrony OPEN. No row moves to achieved. Inventory row for KCut.idr, CHANGELOG entry, reject README rows, 12 names pinned in tests/proof/regression.mjs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 34 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
governance / Actions lockfile verify fails on main and on every PR:
workflow uses ref "v0.5.0" but lockfile pins "v0.3.0"
(.github/workflows/push-email-notify.yml)
Dependabot #265 bumped hyperpolymath/smtp-notify-action v0.3.0 -> v0.5.0
without a lock refresh, the same drift #266 and #270 reverted elsewhere
(#270 left this one alone because #268 did not cause it). Back to the
locked v0.3.0; recurrence needs the lock refreshed with the bump (owner
decision, as in #270).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
hyperpolymath
marked this pull request as ready for review
October 14, 2026 01:31
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
|
hyperpolymath
added a commit
to hyperpolymath/panll
that referenced
this pull request
Oct 14, 2026
…rnel (PWL-01) (#145) ## Summary PWL-01 step 5, on the panll side. A clade's resource contract is now graded in typed-wasm's Idris2 grade kernel, which is imported at a pin and not re-declared: - **panel state** is graded by occupancy (HWM); - the **Panel-N → Panel-W crossing** is graded by loss (Loss). Also in this PR: one graded contract (`neurosym-bridge`), the `{grade, algebra}` wire schema for TypeLL, and a CI job that actually typechecks the module. Kernel pin: typed-wasm main `117bbf8`. That is hyperpolymath/typed-wasm#274; the kernel itself landed in #271, and #273 added its Nat lemmas. **Finding:** `panel-clades/src/abi/{Types,Layout,Foreign}.idr` have never typechecked: - their module names don't match their paths; - laid out correctly, `Types.idr` still has 11 errors; - yet their README claimed "Verified by Idris2 0.8.0", with every proof CLOSED. So the acceptance line "panel-clades ABI typechecks against the ported kernel" holds for the **new** module only. The three existing files are reported here, not fixed; details below. ## Changes - `panel-clades/src/abi/PanelClades/ABI/Grades.idr`: - `StateWithin` and `phasesWithin`: the reclamation law at the panel (a second phase fits in what the first left). Uses the kernel's `maxLub`. - `LossWithin`: total collapse is never within tolerance. - `crossTwice`: losses add (the kernel's `lossSeq`). - `betterOfTwo`: keep the less lossy translation (`lossAlt`). - `CladeResourceContract`, with its `TaggedGrade` `{grade, algebra}` pairs. - The **`neurosym-bridge` contract**: state peak 48 / drift 16 within a budget of 64; crossing loss 2 within a tolerance of 3. These are declared values for you to confirm, not measurements, so the contract is **DESIGNED**. - A computed witness: two panel phases occupy 64 but cost 96 under max-plus. - `panel-clades/scripts/fetch-siblings.sh` (the pin) and `panel-clades/scripts/check-abi.sh` (the gate). The gate: - builds the kernel at the pin; - builds `panel-clades-grades.ipkg` against it; - runs `tests/reject/{OverBudget,CollapseWithinTolerance}.idr`. A missing toolchain fails the gate; it never skips. - CI: job `panel-clades-abi` in `build-validation.yml`, with Idris2 0.8.0 built from its tag. - `schema/typell-grade.schema.json`: the `{grade, algebra}` payload, with algebra ∈ loss / maxplus / hwm. **DESIGNED**: the Panel-L ↔ TypeLL JSON-RPC wiring doesn't exist yet (`TypeLLService`/`TypeLLCmd` are stubs). - Docs: the check status in the panel-clades ABI README (with SPDX header), a pointer from the TypeLL clade README, `CHANGELOG`. ## Status (artefact for each) | Claim | Status | Artefact | |---|---|---| | Grades lemmas (`phasesWithin`, `crossTwice`, `betterOfTwo`) | PROVEN | `idris2 --build panel-clades-grades.ipkg` against the pinned kernel | | Occupancy ≠ cost at the panel (64 vs 96) | TESTED (computed) | `panelPhasesOccupancy`, `panelPhasesCost` | | Over-budget state / collapsed crossing refused | TESTED | `tests/reject/*.idr` | | `neurosym-bridge` contract values | DESIGNED | declared values in `Grades.idr` | | `{grade, algebra}` on the TypeLL wire | DESIGNED | `schema/typell-grade.schema.json` | | `Types/Layout/Foreign.idr` typecheck | **does not hold** | `src/abi/README.adoc`, "Check status" | ## The pre-existing ABI errors (not fixed here) 1. Module `PanelClades.ABI.Types` lives at `src/abi/Types.idr`, so Idris2 refuses all three files outright (`Module name … does not match file name`). 2. Moved to matching paths, `Types.idr` still has 11 errors: - `%runElab` without `%language ElabReflection`; - `DecEq` without `import Decidable.Equality` (×2); - `So` auto-proofs for runtime values (`createHandle`, `mkCladeId`); - `Bits (ptrSize p)` used as a type (`CPtr`); - pattern matching on types (`cSizeOf`, `cAlignOf`); - `allCladeKinds` / `cladeKindExhaustive`, where `cladeKindCount` is auto-bound as a variable. Some of these need redesign rather than a one-line fix. Whether to fix them in a follow-up is your call. ## CI on this PR The new job is `Build Validation / panel-clades-abi`. Every other red check is red on `main` (`787ac2e`) too, for reasons outside this diff: | Check | Cause (from the log) | On main | |---|---|---| | Build Validation / validate | `deno task couldn't find deno.json(c) or package.json` (ReScript build gate) | red, same step | | Rust CI / Cargo check | `no matching package named gossamer-rs` (path dependency on a sibling checkout that CI doesn't make) | red | | Governance / Actions lockfile verify | no `.github/workflows/actions.lock`; the grace window closed on 2026-10-01 | red | | Governance / Workflow security linter | `main-estate-audit.yml` lacks an SPDX header and a top-level `permissions:` | red | | Dogfood Gate / K9 contracts | 117 `config.k9.ncl` files lack the `K9!` magic line | red | | Central Estate Audit / Code Hygiene | unlinked `TODO` markers in `src/update/*.affine` (none in this diff; its proof-circumvention scan found none) | red | CodeFactor reported one issue. Running shellcheck locally on this PR's scripts found SC2164 (unguarded `cd` in a script without `set -e`) and SC2181. Both are fixed in `a188675`, and shellcheck is now clean on both scripts. Each of the gate's failure branches was re-checked with an idris2 shim. ## Testing ``` bash panel-clades/scripts/check-abi.sh Idris 2, version 0.8.0 typed-wasm at 117bbf895b513673ba06eb6c4ebb0e26e276e295 PASS: typed-wasm grade kernel built at 117bbf8 PASS: panel-clades-grades.ipkg builds against the kernel (1 module(s), 0 errors) PASS: rejected CollapseWithinTolerance at line 17 (Mismatch between: Finite .* and Infinity) PASS: rejected OverBudget at line 17 (Mismatch between: 0 and 16) OK: panel-clades grades ABI — builds against the kernel, 2 rejection(s) ``` Mutation checks: - lowering the contract's budget from 64 to 40 makes the gate exit 1 (build refused; the rejections flagged as failing for the wrong reason); - an idris2 shim that refuses the kernel build, or prints `Error:` but exits 0, makes the gate exit 1. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
PWL-01 step 4. This states K-CUT-LOSS for the L16 fragment and ports and re-proves it in Idris2, rather than recording it ASSUMED. The source is choreographic-types
KCut.kcut-loss@edb784a7d26c276c2abfa8399b773d346dbb101e, parametric in the grade kernel'sResourceAlgebrainterface. Choreography grades are now drawn from the kernel.Stacked on #273 (PR B); the base is that PR's branch. No row moves to achieved.
Changes
src/abi/TypedWasm/ABI/KCut.idr:Global/Localtypes,Cut/LCutand their truncations, projection with plain merge,Projectable,Consistent;projCut(K-2, uses no algebra laws),gradeProj(K-3, uses onlyseqUnitLandaltIdem),cutProjectable(K-5), and from themkcutLoss(K-1);kcutLossLoss/kcutLossMaxPlus/kcutLossHWM(K-6);Choreography.idr:GradedChoreography gfor any kernel algebra, withPartiesDeclared, the obligationL16KCutLoss, and its dischargel16KCutLoss = kcutLoss.tests/reject/{UnprojectableChoice,InconsistentCut}.idr. Each is refused on the K-CUT equality itself (1 vs 2), so both side-conditions are load-bearing.KCutcould not reduce a concrete protocol's grades:roleunfolds to base'sdecEq, which a module only evaluates if it importsDecidable.Equality.KCutnow re-exports it and the kernel interface. The first version of each control was refused for that elaboration reason, not the intended one; the gate's wrong-reason filter is what caught it.scripts/fetch-siblings.shpins choreographic-types atedb784a.tools/check-kernel-proofs.shchecks upstreamKCut.agda(which needs only resource-algebra) and its two Agda rejects, each refused with1 != 2.LEVEL-STATUSrow 16 + inventory,CHANGELOG, reject README, 12 names pinned inregression.mjs.Status rows (artefact for each)
KCut.kcutLoss,Choreography.l16KCutLossprojCut/gradeProj/cutProjectableKCut.idrminimal-laws.sh)kcutLossLoss/MaxPlus/HWMmessages/LegalTracePartiesDeclaredchecked)RSR Quality Checklist
Required
main, none from this PRunsafeblocks without// SAFETY:comments.envfiles includedAs Applicable
.machine_readable/descriptiles/STATE.a2mlnot updated (stale since 2026-05-27; owner's call)CHANGELOGupdatedcontract.abi.sha256unchanged (I3 anchors are the wire format only)Testing
🤖 Generated with Claude Code
https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
Generated by Claude Code