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

[hyperpolymath]

Summary

Two small fixes to the merged PWL-01 work.

1. Occupancy.WithinMaximum didn't bound a private memory's initial allocation. CodeRabbit reported it on feat(abi): L11/L12 read through the grade kernel; L13 occupancy and R-2 at a boundary (PWL-01, PR B) #273 (Occupancy.idr:185) and nobody answered before the merge.
   • 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.
   • That includes MkPrivateMemory o n 2 (Just 1), which already exceeds its maximum when it is allocated.
   • Reproduced first: that declaration typechecks against main 117bbf8.
2. tools/check-kernel-proofs.sh could carry on after a failed cd (shellcheck SC2164). The gate runs without set -e, because it collects failures instead of stopping. A failed cd would have left rm -rf "$OUT", rm -rf src/abi/build and every relative path resolving from the caller's directory. CodeFactor found the same defect in panll's copy of the pattern (feat(panel-clades): graded clade contracts over typed-wasm's grade kernel (PWL-01) panll#145).

Changes

• src/abi/TypedWasm/ABI/Occupancy.idr: UnderMaximum now also takes LTE pm.initial m. peak g stays the run's absolute live-state peak, and the doc comment says so.
• New reject tests/reject/InitialOverMaximum.idr, which states the old general claim with the new constructor. It is refused at the initial bound (Can't solve constraint between: 0 and pm .initial).
• LEVEL-STATUS row 13 and tests/reject/README.adoc name the fixture. The binding stays DESIGNED; no status moves.
• tools/check-kernel-proofs.sh: cd "$(dirname "$0")/.." || exit 1.
• CHANGELOG: a Fixed entry for both.

The other PWL-01 scripts are already shellcheck-clean: check-grade-kernel.sh, scripts/fetch-siblings.sh and tests/transcription/gen.sh. tools/check-contract.sh has the same SC2164; it predates PWL-01 and is left alone here.

RSR Quality Checklist

Required

• Tests pass (see Testing)
• Code is formatted
• Linter is clean: Idris2 build warnings unchanged (24); shellcheck clean on the PWL-01 scripts
• No banned language patterns
• No unsafe blocks without // SAFETY: comments
• No banned functions
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• Documentation updated (LEVEL-STATUS row 13, reject README)
• CHANGELOG updated
• ABI changes validated: contract.abi.sha256 unchanged (its anchors cover only the wire format)

Testing

tools/check-kernel-proofs.sh   OK: kernel proofs — build, 10 rejection(s), table, and 3 negative control row(s)
  PASS: idris2 --build typed-wasm.ipkg: 32 module(s) built, 0 errors
  PASS: rejected InitialOverMaximum at line 24 (Can't solve constraint between: 0 and pm \.initial)
tools/check-grade-kernel.sh    OK: one definition of min-plus (ResourceAlgebra/Loss.idr) and one of max-plus (ResourceAlgebra/MaxPlus.idr); no Nat min/max outside base
tools/check-contract.sh        OK: contract gate — I1 + I3 hold
node tests/proof/regression.mjs --strict   202 passed, 0 failed, 0 skipped
E2E_BUILD=0 bash tests/e2e.sh              E2E validation PASSED

Negative control: the same declaration with the old two-argument UnderMaximum typechecks against main 117bbf8 (exit 0, no Error:).

🤖 Generated with Claude Code

https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t

[coderabbitai]

Warning

Review limit reached

You'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 17 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: af39295c-9835-4890-8314-3cd1d1f3233b

📥 Commits

Reviewing files that changed from the base of the PR and between 117bbf8 and 292f109.

📒 Files selected for processing: 7

• .github/workflows/contract-gate.yml
• CHANGELOG.adoc
• LEVEL-STATUS.adoc
• src/abi/TypedWasm/ABI/Occupancy.idr
• tests/reject/InitialOverMaximum.idr
• tests/reject/README.adoc
• tools/check-kernel-proofs.sh

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud