proof(SafeFile): DISCHARGE readTrackingMonotonic + writeTrackingMonotonic (#136)

## Summary

Discharge the last two OWED handle-tracking theorems in
`Proven.SafeFile.Proofs`:

- `readTrackingMonotonic : (Operations.updateAfterRead h
bytes).bytesRead >= h.bytesRead = True`
- `writeTrackingMonotonic : (Operations.updateAfterWrite h
bytes).bytesWritten >= h.bytesWritten = True`

The blocker per the OWED comment was "Idris2 0.8.0 doesn't reduce
record-update field projection through a function call". Verified that's
accurate (test harness at `/tmp/charrefl/src/TestNatGte.idr`), but the
fix is two-part:

1. **`Operations.idr`** — Flip both `updateAfterRead` /
`updateAfterWrite` from `export` to `public export` AND inline the
explicit `MkSafeHandle` constructor instead of the record-update sugar
(`{ bytesRead := ... } h`). Runtime semantics identical, but the
explicit constructor reduces definitionally under field projection at
type-check time.

2. **`Proofs.idr`** — Add helper `plusGteOriginal : (n, m : Nat) -> (n +
m) >= n = True` (induction on `n`, case-split on `m` only in the `Z`
branch). Discharge both theorems trivially.

## Verification

- `idris2 --check src/Proven/SafeFile/Operations.idr` → Exit 0
- `idris2 --check src/Proven/SafeFile/Proofs.idr` → Exit 0
- Empirical confirmation: `/tmp/charrefl/src/TestNatGte.idr` shows
record-update DOES NOT reduce; explicit-constructor DOES.

Zero `believe_me` / `postulate` / `idris_crash`. No external-caller
breakage (no uses outside `SafeFile/Proofs.idr` per estate grep).

Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious OWED
meta), proven#119 (paths-forward).

## Test plan

- [x] Local type-check `Operations.idr` clean
- [x] Local type-check `Proofs.idr` clean
- [ ] CI `idris2 --check proven.ipkg` green
- [ ] CI test suite green

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeFile/Operations.idr

@@ -156,14 +156,25 @@ checkWritable h =
     else Err (InvalidOperation "write" h.mode)
 
 ||| Update handle after read
-export
+|||
+||| Inlined as explicit `MkSafeHandle` constructor (rather than
+||| record-update syntax) so that the field projection
+||| `(updateAfterRead h bytes).bytesRead` reduces definitionally to
+||| `h.bytesRead + bytes` at type-check time. Record-update sugar does
+||| not unfold under projection in Idris2 0.8.0; explicit constructor
+||| does. Runtime behaviour is identical.
+public export
 updateAfterRead : SafeHandle -> Nat -> SafeHandle
-updateAfterRead h bytes = { bytesRead := h.bytesRead + bytes } h
+updateAfterRead h bytes =
+  MkSafeHandle h.handleId h.mode h.path (h.bytesRead + bytes) h.bytesWritten
 
 ||| Update handle after write
-export
+|||
+||| See `updateAfterRead` for why this uses explicit-constructor form.
+public export
 updateAfterWrite : SafeHandle -> Nat -> SafeHandle
-updateAfterWrite h bytes = { bytesWritten := h.bytesWritten + bytes } h
+updateAfterWrite h bytes =
+  MkSafeHandle h.handleId h.mode h.path h.bytesRead (h.bytesWritten + bytes)
 
 ||| Create new handle (for simulation/testing)
 export

src/Proven/SafeFile/Proofs.idr

@@ -13,6 +13,7 @@ import Proven.Core
 import Proven.SafeFile.Types
 import Proven.SafeFile.Operations
 import Data.List
+import Data.Nat
 import Data.String
 
 %default total
@@ -210,35 +211,33 @@ fileSizeCheckPrevents path size limit tooLarge = ()
 -- Handle Tracking Proofs
 --------------------------------------------------------------------------------
 
-||| OWED: `updateAfterRead h bytes` produces a handle whose `bytesRead`
-||| field equals `h.bytesRead + bytes`, hence is `>=` the prior value.
-||| Operationally true by direct unfolding of
-|||   `updateAfterRead h bytes = { bytesRead := h.bytesRead + bytes } h`
-||| in `Proven.SafeFile.Operations`.
-||| Held back by Idris2 0.8.0 not reducing record-update field projection
-||| through a function call during type-checking — `(updateAfterRead h
-||| bytes).bytesRead` does not normalise to `h.bytesRead + bytes` by Refl
-||| (same blocker as the deleted `newHandleZeroCounters` documented at
-||| L218-220). Discharge once Idris2 fixes the record-update reduction
-||| (tracked upstream) or via a manual rewrite + `lteAddRight` proof on
-||| `Nat` once both sides are forced into normal form.
-export
-0 readTrackingMonotonic : (h : SafeHandle) -> (bytes : Nat) ->
-                          (Operations.updateAfterRead h bytes).bytesRead >= h.bytesRead = True
-
-||| OWED: `updateAfterWrite h bytes` produces a handle whose
-||| `bytesWritten` field equals `h.bytesWritten + bytes`, hence is `>=`
-||| the prior value. Operationally true by direct unfolding of
-|||   `updateAfterWrite h bytes = { bytesWritten := h.bytesWritten + bytes } h`
-||| in `Proven.SafeFile.Operations`.
-||| Held back by Idris2 0.8.0 not reducing record-update field projection
-||| through a function call during type-checking (same blocker family as
-||| `readTrackingMonotonic` above). Discharge once Idris2 fixes the
-||| record-update reduction, or via a manual rewrite + `lteAddRight`
-||| proof on `Nat` once both sides are forced into normal form.
-export
-0 writeTrackingMonotonic : (h : SafeHandle) -> (bytes : Nat) ->
-                           (Operations.updateAfterWrite h bytes).bytesWritten >= h.bytesWritten = True
+||| Helper: `n + m >= n = True` for all `Nat`. Used to discharge the
+||| tracking-monotonic theorems below. Induction on `n` (case-split on
+||| `m` is only needed in the `Z` branch because `m >= 0` reduces only
+||| after pattern-matching on whether `m` is `Z` or `S _`).
+plusGteOriginal : (n, m : Nat) -> (n + m) >= n = True
+plusGteOriginal Z Z = Refl
+plusGteOriginal Z (S _) = Refl
+plusGteOriginal (S k) m = plusGteOriginal k m
+
+||| DISCHARGED: `updateAfterRead h bytes` produces a handle whose
+||| `bytesRead` is `>=` the prior value. By inlined-constructor
+||| definition in `Operations.updateAfterRead`, the field projection
+||| reduces definitionally to `h.bytesRead + bytes`; the remaining
+||| Nat inequality `(n + m) >= n = True` is closed by induction
+||| (`plusGteOriginal`).
+public export
+readTrackingMonotonic : (h : SafeHandle) -> (bytes : Nat) ->
+                        (Operations.updateAfterRead h bytes).bytesRead >= h.bytesRead = True
+readTrackingMonotonic h bytes = plusGteOriginal h.bytesRead bytes
+
+||| DISCHARGED: `updateAfterWrite h bytes` produces a handle whose
+||| `bytesWritten` is `>=` the prior value. Same shape of proof as
+||| `readTrackingMonotonic` above.
+public export
+writeTrackingMonotonic : (h : SafeHandle) -> (bytes : Nat) ->
+                         (Operations.updateAfterWrite h bytes).bytesWritten >= h.bytesWritten = True
+writeTrackingMonotonic h bytes = plusGteOriginal h.bytesWritten bytes
 
 ||| Theorem: New handle has zero counters
 -- newHandleZeroCounters removed: newHandle constructs a record but