fix: PWL-01 follow-ups — WithinMaximum bounds the initial allocation; gate exits if cd fails

.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-<sha>.
+          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 \

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` @

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

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.

tests/reject/InitialOverMaximum.idr

@@ -0,0 +1,24 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- 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

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)
 |===

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