feat(abi): L11/L12 read through the grade kernel; L13 occupancy and R-2 at a boundary (PWL-01, PR B)

.github/workflows/push-email-notify.yml

@@ -40,7 +40,7 @@ jobs:
     timeout-minutes: 5
     steps:
       - name: Send push notification email
-        uses: hyperpolymath/smtp-notify-action@v0.5.0
+        uses: hyperpolymath/smtp-notify-action@v0.3.0
         with:
           server_address: ${{ secrets.SMTP_HOST }}
           server_port: ${{ secrets.SMTP_PORT }}

CHANGELOG.adoc

@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
 == Changelog
 
 All notable changes to this project will be documented in this file.
@@ -8,6 +9,28 @@
 
 === [Unreleased]
 
+==== L11 / L12 / L13 read through the grade kernel (PWL-01 steps 2–3, 2026-10-14)
+
+* *L11.* `CostBounded c n` is proved equal to the kernel's Loss order
+  `Finite n ≼ c`, and path bounds compose by the kernel's `otimesMono`
+  (`costBoundedSeq`). New `Level11WorstCaseProof` grades a branching access
+  plan in MaxPlus (`worstCaseThen`, `worstCaseOneOf`). It is DESIGNED: no
+  surface syntax or attestation uses it. The bottleneck stays MinMax.
+* *L12.* `stalenessGrade` is the reader's lag as a Loss grade: fresh = 𝟙,
+  stale ≠ 𝟙, never synced = 𝟘, and relayed lag = ⊗ (`stalenessRelay`).
+  `syncGrade` now carries a note that its number is a version, not a loss.
+* *L13.* New `Occupancy.idr` ports occupancy-types @ `af95728` R-1..R-5
+  (reclamation law, occupancy ≤ cost, strict reclamation, the 4-vs-7 witness)
+  over the kernel's HWM. It binds them to `private_memory` (an HWM grade within
+  the declared maximum) and to `boundary` (the cut that frees peak − drift).
+  The binding is DESIGNED.
+* Kernel additions: each instance's order read in ℕ (`lossLeOfLTE`,
+  `maxPlusLeOfLTE` and inverses); `ResourceAlgebra/Nat.idr` gains `maxLub`
+  and min/max-vs-`LTE` lemmas. These are typed-wasm's own, labelled as such.
+* New rejects: `CostIsOccupancy`, `DriftIsPeak` (occupancy-types R-6) and
+  `WorstCaseIsCheapest`. `tools/check-kernel-proofs.sh` also runs
+  occupancy-types' own Agda check at its pin.
+
 ==== Grade kernel: resource-algebra ported as the ABI's one source of grades (PWL-01, 2026-10-14)
 
 `src/abi/TypedWasm/ABI/ResourceAlgebra.idr` and `ResourceAlgebra/{Nat,Loss,

LEVEL-STATUS.adoc

@@ -154,7 +154,16 @@ monotonicity, mirrors `+tropical-resource-typing+`
 `+Bridge.hub_ceiling_le+`), `+ResidueMeasure+` (E→R, mirrors
 `+Resource.EchoBridge+`), and `+Level11BottleneckProof+` +
 `+bottleneckCeilsEdges+` wired into
-`+Proofs.attestL11_Bottleneck+`/`+_Sound+`.*
+`+Proofs.attestL11_Bottleneck+`/`+_Sound+`. PWL-01 step 2: the
+obligations read through the kernel — `+CostBounded c n+` IS the Loss
+order `+Finite n ≼ c+` (`+costBoundedIsLossOrder+` /
+`+lossOrderIsCostBounded+`, PROVEN) and path bounds compose by the
+kernel's `+otimesMono+` (`+costBoundedSeq+`, PROVEN);
+`+Level11WorstCaseProof+` grades a branching plan in MaxPlus with
+`+worstCaseThen+` / `+worstCaseOneOf+` from `+otimesMono+` /
+`+oplusMono+` (PROVEN; the obligation itself DESIGNED — no surface or
+attestation uses it). `+Level11BottleneckProof+` is MinMax, not MaxPlus,
+and stays as it is (`+tests/reject/TropicalIsNotMaxPlus.idr+`).*
 
 |12 |Epistemic safety |Epistemic.idr |Not yet |None |*In package (A1,
 2026-04-18); A10 (2026-05-26) closes the "`freshness propagation under
@@ -165,11 +174,28 @@ sibling `+Tropical.TropCost+` (∞ = never-synced) +
 `+neverSyncedInfeasible+`/`+observedFeasible+`/`+observedNotInfeasible+`
 — extant Nat-indexed proofs untouched. Header IS-NOT note: this
 read-consistency model is a DIFFERENT problem from canonical
-`+epistemic-types+`’ standpoint-indexed modality.*
-
-|13 |Module isolation |ModuleIsolation.idr |(per-module handles, future)
+`+epistemic-types+`’ standpoint-indexed modality. PWL-01 step 2:
+staleness graded in the kernel's Loss — `+stalenessGrade+` is the lag;
+fresh is 𝟙 (`+freshHasNoStaleness+`), stale is not (`+staleHasStaleness+`),
+never-synced is 𝟘 (`+neverSyncedIsCollapse+`), and a relayed lag is the
+kernel's ⊗ (`+stalenessRelay+`), all PROVEN. `+syncGrade+` is kept but
+holds a version, not a loss: ordering it with the kernel order would rank
+older versions higher.*
+
+|13 |Module isolation |ModuleIsolation.idr + Occupancy.idr |(per-module handles, future)
 |12 parser/Checker tests |*v1.2 — Idris2 proof + surface checker live;
-007 lowering DONE (task #5)*
+007 lowering DONE (task #5). PWL-01 step 3: occupancy graded in the
+kernel's HWM — R-1..R-5 of occupancy-types @ `+af95728+` re-proved in
+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
+that frees peak − drift (`+BoundaryCut+`, `+boundaryOccupancy+`,
+`+fitsAcrossBoundary+`) — is DESIGNED: nothing links the grade to
+`+memory.grow+` and no checker emits it. `+striated+` occupancy OPEN
+(surface-only construct).*
 
 |14 |Session protocols |SessionProtocol.idr |(typed-state handles,
 future) |13 parser/Checker tests |*v1.3 — Idris2 proof + surface checker
@@ -372,6 +398,12 @@ pinned sources and by Idris2 `+Refl+` against the port, with a
 LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused
 for the intended reason.
 
+|Occupancy.idr |0 |0 |0 |In package (PWL-01 step 3, 2026-10-14). L13
+occupancy over the kernel's HWM grade: occupancy-types
+(`+Reclaim.agda+` / `+Timeline.agda+` / `+Witness.agda+` @ `+af95728+`)
+R-1..R-5 ported and re-proved; L13 binding (`+OccupancyGradedMemory+`,
+`+BoundaryCut+`, `+boundaryFrees+`, `+fitsAcrossBoundary+`) DESIGNED.
+
 |VerifierSpec.idr |0 |0 |0 |Introduced A13 (2026-05-26, PR #72) as
 statement-level spec-of-record for post-A10 items 7+8. *Promoted to
 total bodies 2026-05-27 (PR #79)*: same `+ModuleSummary+` /

scripts/fetch-siblings.sh

@@ -9,14 +9,17 @@
 #   resource-algebra  — the grade kernel; src/abi/TypedWasm/ABI/ResourceAlgebra*
 #                       is its Idris2 transcription, and tests/transcription
 #                       checks the operation tables against this tree in Agda.
+#   occupancy-types   — the reclamation law (R-1..R-6) that
+#                       src/abi/TypedWasm/ABI/Occupancy.idr ports for L13.
 #
 # Re-pin deliberately, one commit per pin, and update the module headers that
 # cite the pin in the same commit.  Override for a local experiment with
-#   RESOURCE_ALGEBRA_COMMIT=<sha> scripts/fetch-siblings.sh
+#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_TYPES_COMMIT=<sha> scripts/fetch-siblings.sh
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
+OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}"
 
 fetch() { # fetch <name> <commit>
   local name="$1" commit="$2" dir="_build/dependencies/$1"
@@ -37,3 +40,4 @@ fetch() { # fetch <name> <commit>
 }
 
 fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
+fetch occupancy-types "$OCCUPANCY_TYPES_COMMIT"

src/abi/TypedWasm/ABI/Epistemic.idr

@@ -397,6 +397,10 @@ observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync)
 -- indexed modality.  Adopting the shared grade is vocabulary alignment, NOT a
 -- claim that this layer instantiates the canonical AccessibleModality.
 
+||| NOTE (PWL-01): the number in `syncGrade` is a VERSION, not a loss.  Under the
+||| kernel's Loss order (`LeG`, smaller is higher) comparing two syncGrades
+||| ranks the OLDER version higher, so do not order them with `LeG`.  The
+||| Loss reading of staleness is `stalenessGrade` below (the lag).
 ||| The tropical sync-grade of a knowledge state, read as irrecoverability:
 ||| never-observed (`Unknown`) relegates to `Infinity` (infeasible / unreachable
 ||| knowledge); knowledge observed at version `v` has finite grade `Finite v`.
@@ -422,3 +426,86 @@ public export
 observedNotInfeasible : (s : Sync mod field old ver) ->
                         Not (syncGrade (Observed {oldVer = old} s) = Infinity)
 observedNotInfeasible _ Refl impossible
+
+-- ============================================================================
+-- Staleness as a Loss grade (PWL-01 step 2, 2026-10-14 — ADDITIVE)
+-- ============================================================================
+--
+-- L12 staleness, graded in the kernel's Loss instance
+-- (TypedWasm.ABI.ResourceAlgebra.Loss): a reader's loss is its LAG, the
+-- number of versions it is behind.  Fresh knowledge loses nothing (𝟙 =
+-- Finite 0, the top of the Loss order); never-synced knowledge is total
+-- collapse (𝟘 = Infinity, the bottom).  Lag accumulates along a relay of
+-- readers by the kernel's sequence (⊗ = +), `stalenessRelay`.  Nothing
+-- above is re-indexed; the A10–A14 proofs are untouched.
+
+||| Staleness of knowing version `known` when the field is at `current`:
+||| the lag, as a Loss grade.
+public export
+stalenessGrade : (known, current : Nat) -> LossGrade
+stalenessGrade known current = Finite (minus current known)
+
+||| Staleness of a knowledge state against the field's current version.
+||| Never observed is total collapse.
+public export
+knowledgeStaleness : {0 m : ModuleId} -> {0 f : String} -> {ver : Nat} ->
+                     Knowledge m f ver -> (current : Nat) -> LossGrade
+knowledgeStaleness {ver} (Observed _) current = stalenessGrade ver current
+knowledgeStaleness Unknown            _       = Infinity
+
+||| Fresh knowledge loses nothing: its staleness is the kernel's 𝟙.
+public export
+freshHasNoStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} ->
+                      Fresh m f known current ->
+                      stalenessGrade known current = oneG {g = LossGrade}
+freshHasNoStaleness (MkFresh _ _ _ eq) =
+  rewrite eq in cong Finite (sym (minusZeroN current))
+
+||| Stale knowledge loses something: its staleness is not 𝟙.
+public export
+staleHasStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} ->
+                    Stale m f known current ->
+                    Not (stalenessGrade known current = oneG {g = LossGrade})
+staleHasStaleness (MkStale lt) prf =
+  succNotLTEzero (replace {p = \x => LT 0 x} (finiteInjective prf) (minusPos lt))
+
+||| Never-synced knowledge is the kernel's 𝟘 (total collapse).
+public export
+neverSyncedIsCollapse : {0 m : ModuleId} -> {0 f : String} -> (current : Nat) ->
+                        knowledgeStaleness {m} {f} Unknown current = zeroG {g = LossGrade}
+neverSyncedIsCollapse _ = Refl
+
+||| Every staleness is at or below fresh in the Loss order: 𝟙 is the top.
+public export
+freshIsTop : (known, current : Nat) -> LeG (stalenessGrade known current) (oneG {g = LossGrade})
+freshIsTop known current = lossLeOne (stalenessGrade known current)
+
+||| A Level-12 proof is a proof of zero staleness.
+public export
+level12NoStaleness : (p : Level12Proof) ->
+                     stalenessGrade p.knownVersion p.currentVersion = oneG {g = LossGrade}
+level12NoStaleness p = freshHasNoStaleness p.freshness
+
+private
+minusPlusCancel : (x, r : Nat) -> minus (x + r) r = x
+minusPlusCancel x r = rewrite plusCommutative x r in minusPlus r
+
+private
+lagSplits : {r, i, t : Nat} -> LTE r i -> LTE i t ->
+            minus t r = minus t i + minus i r
+lagSplits {r} {i} {t} ri it =
+  -- t = ((t − i) + (i − r)) + r, by (t − i) + i = t and (i − r) + r = i;
+  -- subtract r from both sides.
+  trans (cong (\z => minus z r)
+          (trans (sym (plusMinusLte i t it))
+          (trans (cong (\z => minus t i + z) (sym (plusMinusLte r i ri)))
+                 (plusAssociative (minus t i) (minus i r) r))))
+        (minusPlusCancel (minus t i + minus i r) r)
+
+||| Relayed knowledge: a reader at version r who learned from a reader at i,
+||| itself behind the truth t, lags t by the SEQUENCE of the two lags — the
+||| kernel's ⊗ in Loss.  (r ≤ i ≤ t: knowledge only flows forward.)
+public export
+stalenessRelay : {r, i, t : Nat} -> LTE r i -> LTE i t ->
+                 stalenessGrade r t = otimes (stalenessGrade i t) (stalenessGrade r i)
+stalenessRelay ri it = cong Finite (lagSplits ri it)