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