From fecd66d940c715039428bfb34241fef002e7dcb8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:49:27 +0000 Subject: [PATCH 1/3] fix(tools): check-kernel-proofs.sh exits if cd fails shellcheck SC2164. The gate runs without `set -e` (it collects failures), so a failed cd would have carried on from the caller's directory: `rm -rf _build/kernel-proofs` and every relative path would resolve there. Same guard as panll's check-abi.sh (hyperpolymath/panll#145). The other PWL-01 scripts (check-grade-kernel.sh, scripts/fetch-siblings.sh, tests/transcription/gen.sh) are shellcheck-clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tools/check-kernel-proofs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 9ce6e1b..41dc633 100755 --- a/tools/check-kernel-proofs.sh +++ b/tools/check-kernel-proofs.sh @@ -25,7 +25,7 @@ # tools/check-kernel-proofs.sh --regen # rewrite ops.tsv from the port, # # then check (commit the diff) set -uo pipefail -cd "$(dirname "$0")/.." +cd "$(dirname "$0")/.." || exit 1 ROOT="$(pwd)" REGEN=0; [ "${1:-}" = "--regen" ] && REGEN=1 From d9879573c8c0eeee00f592341c1ac326f94cb6cc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:55:12 +0000 Subject: [PATCH 2/3] fix(abi): WithinMaximum bounds a private memory's initial allocation CodeRabbit on #273 (Occupancy.idr:185). UnderMaximum asked only that the run's peak fit the declared maximum. An empty run has peak 0, so `\pm, m, prf => UnderMaximum prf LTEZero` certified every private memory with a maximum, including MkPrivateMemory o n 2 (Just 1), whose initial allocation already exceeds it. The memory is live from its initial allocation on, so UnderMaximum now takes `LTE pm.initial m` as well; `peak g` stays the run's absolute live-state peak. Reproduced first: against main 117bbf8 that declaration typechecks. New reject tests/reject/InitialOverMaximum.idr states it with the new constructor and is refused at the initial bound ("Can't solve constraint between: 0 and pm .initial"). The binding stays DESIGNED; LEVEL-STATUS row 13 and the reject README name the fixture. check-kernel-proofs: build, 10 rejection(s), table, 3 negative control rows; regression 202 passed; e2e passed; warnings unchanged (24). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- CHANGELOG.adoc | 8 ++++++++ LEVEL-STATUS.adoc | 6 ++++-- src/abi/TypedWasm/ABI/Occupancy.idr | 11 +++++++++-- tests/reject/InitialOverMaximum.idr | 24 ++++++++++++++++++++++++ tests/reject/README.adoc | 1 + 5 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 tests/reject/InitialOverMaximum.idr diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index cf8cc17..6543e0f 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,14 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Fixed (2026-10-14) + +* `Occupancy.WithinMaximum`: `UnderMaximum` now bounds a private memory's + initial allocation as well as its run's peak. With only the peak bounded, + an empty run (peak 0) certified a memory declared with `initial` above + `maximum`. New reject `InitialOverMaximum`. Found by CodeRabbit on #273. +* `tools/check-kernel-proofs.sh` exits if its `cd` fails (shellcheck SC2164). + ==== 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` @ diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc index e0c839e..99f61a9 100644 --- a/LEVEL-STATUS.adoc +++ b/LEVEL-STATUS.adoc @@ -190,8 +190,10 @@ Idris2 (`+cutFactor+`, `+reclaimLaw+`, `+occupancyAtCut+`, `+occupancyLeCost+`, `+noReclaim+`, `+reclaimed+`, `+witness*+`: PROVEN; statement correspondence ASSUMED, port-and-reprove), R-6 as `+tests/reject/{CostIsOccupancy,DriftIsPeak}.idr+` (TESTED). The L13 -binding — an HWM grade per `+private_memory+` within its declared -maximum (`+OccupancyGradedMemory+`), a declared `+boundary+` as the cut +binding — an HWM grade per `+private_memory+` whose initial allocation +and peak both fit its declared maximum (`+OccupancyGradedMemory+`; +`+tests/reject/InitialOverMaximum.idr+` refuses the peak-only bound), a +declared `+boundary+` as the cut that frees peak − drift (`+BoundaryCut+`, `+boundaryOccupancy+`, `+fitsAcrossBoundary+`) — is DESIGNED: nothing links the grade to `+memory.grow+` and no checker emits it. `+striated+` occupancy OPEN diff --git a/src/abi/TypedWasm/ABI/Occupancy.idr b/src/abi/TypedWasm/ABI/Occupancy.idr index e47e53c..32fc1d1 100644 --- a/src/abi/TypedWasm/ABI/Occupancy.idr +++ b/src/abi/TypedWasm/ABI/Occupancy.idr @@ -175,14 +175,21 @@ reclaimedPlusDrift : (g : HWMGrade) -> reclaimedAt g + drift g = peak g reclaimedPlusDrift (MkHWM p n b) = plusMinusLte n p b ||| A private memory's run stays within its declared maximum (in pages). +||| `peak g` is the run's absolute live-state peak. The memory is live from +||| its initial allocation on, before any phase runs, so the initial +||| allocation must fit as well: without that bound an empty run (peak 0) +||| would certify a memory declared with `initial` above `maximum` +||| (tests/reject/InitialOverMaximum.idr). public export data WithinMaximum : PrivateMemory -> HWMGrade -> Type where ||| No maximum declared. NoMaximum : {pm : PrivateMemory} -> {g : HWMGrade} -> pm.maximum = Nothing -> WithinMaximum pm g - ||| The peak does not exceed the declared maximum. + ||| Neither the initial allocation nor the peak exceeds the declared + ||| maximum. UnderMaximum : {pm : PrivateMemory} -> {g : HWMGrade} -> {m : Nat} -> - pm.maximum = Just m -> LTE (peak g) m -> WithinMaximum pm g + pm.maximum = Just m -> LTE pm.initial m -> LTE (peak g) m -> + WithinMaximum pm g ||| A private memory graded by occupancy: its run, phase by phase, and the ||| proof that the run's high-water mark fits the declaration. diff --git a/tests/reject/InitialOverMaximum.idr b/tests/reject/InitialOverMaximum.idr new file mode 100644 index 0000000..59fd8f1 --- /dev/null +++ b/tests/reject/InitialOverMaximum.idr @@ -0,0 +1,24 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- MUST FAIL (tools/check-kernel-proofs.sh). L13 occupancy binding. +-- +-- An empty run has peak 0, so if only the peak had to fit, every private +-- memory with a declared maximum would be certified, including one declared +-- with `initial` above `maximum` (MkPrivateMemory o n 2 (Just 1)). The +-- initial allocation is live before any phase runs; WithinMaximum bounds it +-- too. Before that bound this declaration typechecked (with the first +-- LTEZero dropped). +-- EXPECT: Can't solve constraint between: 0 and pm \.initial +module InitialOverMaximum + +import TypedWasm.ABI.ResourceAlgebra +import TypedWasm.ABI.ResourceAlgebra.HWM +import TypedWasm.ABI.ModuleIsolation +import TypedWasm.ABI.Occupancy + +%default total + +invalid : (pm : PrivateMemory) -> (m : Nat) -> pm.maximum = Just m -> + WithinMaximum pm (timelineGrade []) +invalid pm m prf = UnderMaximum prf LTEZero LTEZero diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc index d441962..c1c5426 100644 --- a/tests/reject/README.adoc +++ b/tests/reject/README.adoc @@ -18,6 +18,7 @@ because then the control proves nothing. | `CostIsOccupancy` | an L13 run charged the sum of its peaks, as if the boundary reclaimed nothing (occupancy-types R-6) | `DriftIsPeak` | drift identified with peak: "a boundary never reclaims" (occupancy-types R-6) | `WorstCaseIsCheapest` | L11's MaxPlus worst case charging the cheaper branch +| `InitialOverMaximum` | an L13 private memory certified by an empty run although its initial allocation is unbounded by its maximum | `UnprojectableChoice` | K-CUT-LOSS without the Projectable side-condition (choreographic-types K-7) | `InconsistentCut` | K-CUT-LOSS without the Consistent side-condition (choreographic-types K-7) |=== From 292f109a330d474f33bd93557d5ba5557497e789 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:59:20 +0000 Subject: [PATCH 3/3] fix(ci): kernel-proofs fetches Idris2 by commit, not by its v0.8.0 tag Same defect CodeRabbit found in panll's copy of this job (hyperpolymath/panll#145, CWE-494): a tag can move. The job now fetches 15a3e4e70843f7a34100f6470c04b791330788df (what v0.8.0 names), checks HEAD against it, and tags it v0.8.0 locally so the Makefile reports the release version rather than 0.8.0-. actions.lock is unaffected (no action reference changed). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index ffe2029..93ef94e 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -51,11 +51,15 @@ jobs: # PINNED Agda kernel (resource-algebra @ cf9235c, Agda --safe --without-K) # on tests/transcription/ops.tsv; both provers refuse the wrong rows. # Idris2 publishes no binaries and its release-tarball URL 404s (see - # e2e.yml build-e2e), so 0.8.0 is built from its tag with Chez Scheme. + # e2e.yml build-e2e), so 0.8.0 is built from source with Chez Scheme, + # fetched by the commit its v0.8.0 tag names (a tag can move; the SHA + # cannot). kernel-proofs: name: Grade kernel proofs (Idris2 0.8.0 + Agda) runs-on: ubuntu-latest timeout-minutes: 40 + env: + IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df # v0.8.0 steps: - name: Checkout uses: actions/checkout@v7.0.1 @@ -66,7 +70,13 @@ jobs: agda --version - name: Build Idris2 0.8.0 from source run: | - git clone --quiet --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$RUNNER_TEMP/idris2-src" + git init --quiet "$RUNNER_TEMP/idris2-src" + git -C "$RUNNER_TEMP/idris2-src" fetch --quiet --depth 1 https://github.com/idris-lang/Idris2 "$IDRIS2_COMMIT" + git -C "$RUNNER_TEMP/idris2-src" checkout --quiet --detach FETCH_HEAD + test "$(git -C "$RUNNER_TEMP/idris2-src" rev-parse HEAD)" = "$IDRIS2_COMMIT" + # Local tag on the verified commit, so the Makefile reports the + # release version (0.8.0) rather than 0.8.0-. + git -C "$RUNNER_TEMP/idris2-src" tag v0.8.0 make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \ || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; } make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \