From 07db0782c701a604e9723bea73d52253a18b7516 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 20 May 2026 18:33:10 +0100
Subject: [PATCH] proof(SafeHTTP): annotate 3 bodyless decls as
 OWED-with-justification

Converts `successNotError`, `errorNotSuccess` and `retryableIsError` in
`src/Proven/SafeHTTP/Proofs.idr` from bodyless `export` signatures to
the estate's OWED-with-justification convention established 2026-05-20
across SafeChecksum / Buffer / CryptoAccel / HKDF / Bloom / FPGA /
SafeAPIKey / SafeCORS / SafeCSV / SafeSemVer / SafeHtml:

- Triple-pipe `|||` doc-comment stating the claim
- `0 ` (erased multiplicity) so the postulate is not runtime-callable
- Bare signature, no `postulate` keyword
- Explicit Idris2 0.8.0 blocker + discharge condition

All three claims sit in the same blocker family: `Nat` order /
equality comparisons on the abstract record-projected `sc.code`
field (existentially bound by `MkStatusCode`, only carries the
`So (code >= 100 && code <= 599)` range witness) do not reduce by
`Refl` alone under Idris2 0.8.0. Same posture as SafeChecksum's
`Nat`-mod identities.

Discharge route: `Data.Nat` linear-arithmetic reflective tactic
or hand-written case-split with `lteTransitive`.

Refs hyperpolymath/standards#158.
---
 src/Proven/SafeHTTP/Proofs.idr | 45 +++++++++++++++++++++++++---------
 1 file changed, 34 insertions(+), 11 deletions(-)

diff --git a/src/Proven/SafeHTTP/Proofs.idr b/src/Proven/SafeHTTP/Proofs.idr
index 3cd88929..5de0a1b2 100644
--- a/src/Proven/SafeHTTP/Proofs.idr
+++ b/src/Proven/SafeHTTP/Proofs.idr
@@ -90,20 +90,43 @@ parseEmptyMethodFails = Refl
 -- HTTP Status Code Properties
 --------------------------------------------------------------------------------
 
-||| Success status codes are not errors.
-||| If isSuccess returns True, isError must return False.
-||| Proved by contradiction: if code >= 200 && code < 300, then code < 400.
+||| OWED: success status codes are not errors. If `isSuccess sc = True`
+||| (i.e. `sc.code >= 200 && sc.code < 300`), then `isError sc = False`
+||| (i.e. `sc.code >= 400` is false). Held back by Idris2 0.8.0 not
+||| reducing the comparison-chain `>=`/`<` on the abstract `Nat`
+||| `sc.code` to literal `True`/`False` by `Refl` alone — `sc.code` is
+||| existentially bound by `MkStatusCode` and only carries the range
+||| witness `So (code >= 100 && code <= 599)`, not a concrete value.
+||| Same blocker family as SafeChecksum's `Nat`-mod reductions.
+||| Discharge once a `Data.Nat` linear-arithmetic reflective tactic
+||| is available, or by deriving via `boolAnd`/`boolNot` case-split on
+||| the `So` witness plus `lteTransitive` (200 <= sc.code < 300 < 400).
 export
-successNotError : (sc : StatusCode) -> isSuccess sc = True -> isError sc = False
-
-||| Error status codes are not successes.
+0 successNotError : (sc : StatusCode) -> isSuccess sc = True -> isError sc = False
+
+||| OWED: error status codes are not successes. If `isError sc = True`
+||| (i.e. `sc.code >= 400`), then `isSuccess sc = False` (i.e.
+||| `sc.code >= 200 && sc.code < 300` is false because `sc.code < 300`
+||| contradicts `sc.code >= 400`). Held back by Idris2 0.8.0 not
+||| reducing `Nat` order comparisons on the abstract record-projected
+||| `sc.code` by `Refl`. Same blocker family as `successNotError`.
+||| Discharge once a `Data.Nat` linear-arithmetic reflective tactic
+||| is available, or by case-split on `>=`/`<` with `lteTransitive`.
 export
-errorNotSuccess : (sc : StatusCode) -> isError sc = True -> isSuccess sc = False
-
-||| Retryable status codes are errors.
-||| 429, 502, 503, 504 are all >= 400.
+0 errorNotSuccess : (sc : StatusCode) -> isError sc = True -> isSuccess sc = False
+
+||| OWED: retryable status codes are errors. 429, 502, 503, 504 are
+||| each `>= 400`, so `isRetryable sc = True` implies `isError sc =
+||| True`. Held back by Idris2 0.8.0 not reducing the four-way `||`
+||| equality-disjunction (`sc.code == 429 || ... || sc.code == 504`)
+||| into a definite value of `sc.code >= 400` by `Refl` — the `Nat`
+||| equality primitives on the abstract record field do not unfold.
+||| Same blocker family as `successNotError`. Discharge once a
+||| `Data.Nat` reflective tactic is available, or by four-arm case
+||| analysis on the `||` chain with literal `lteSucc`-derived proofs
+||| `429 >= 400`, `502 >= 400`, `503 >= 400`, `504 >= 400`.
 export
-retryableIsError : (sc : StatusCode) -> isRetryable sc = True -> isError sc = True
+0 retryableIsError : (sc : StatusCode) -> isRetryable sc = True -> isError sc = True
 
 --------------------------------------------------------------------------------
 -- Header Injection Prevention Properties