proof(SafeFile): DISCHARGE readTrackingMonotonic + writeTrackingMonotonic via inlined-constructor + Nat induction (proven#90 #107 #119)

The two OWED tracking-monotonic theorems were blocked by Idris2 0.8.0
not reducing record-update field projection through a function call.
The fix is two-part:

1. **Operations.idr**: Flip `updateAfterRead`/`updateAfterWrite` from
   `export` to `public export`, AND replace the record-update sugar
   (`{ bytesRead := ... } h`) with the explicit `MkSafeHandle`
   constructor. Runtime behaviour is identical, but the explicit
   constructor allows `(updateAfterRead h bytes).bytesRead` to reduce
   definitionally to `h.bytesRead + bytes` at type-check time —
   confirmed by /tmp/charrefl test harness.

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

Empirical reduction map confirms `(n + m) >= n = True` reduces via
the `compare`-based Bool `>=` for Nat after pattern-matching on `n`
and `m` in the `Z` cases (`reference_idris2_0_8_0_reduction_map.md`).

Zero `believe_me`/`postulate`/`idris_crash`. No external API change
— `updateAfterRead`/`updateAfterWrite` already had no non-test
callers (grep'd whole tree). Visibility flip is monotonic
(`export` → `public export`).

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

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