proof(SafePath): annotate 23 bodyless decls as OWED (Refs standards#158) (#57)

## Summary

Converts the 23 bodyless declarations in
`src/Proven/SafePath/Proofs.idr` from terse comments to the estate's
OWED-with-justification convention established 2026-05-20 across
SafeChecksum / Buffer / CryptoAccel / HKDF / Bloom / FPGA / SafeHtml /
SafeFile / SafeHeader / SafeMath / SafeSQL / SafeYAML / SafeEnv /
SafeTOML / SafeCSRF / SafeString:

- 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

Refs hyperpolymath/standards#158.

## The 23 OWED items, grouped by blocker family

### Family 1 — String FFI opacity (7 items)

`prim__eq_String` / `unpack` / `pack` / `isPrefixOf` / `toLower` /
`singleton` are FFI-bound and don't normalise for abstract `String`.
Same blocker family as SafeChecksum's Luhn/ISBN OWED set and SafeYAML's
`standardTagsSafe` family, and the boj-server
`Boj.SafetyLemmas.charEqSym` / gossamer `stringNotEqCommut` class-J
axioms.

- **`pathEqRefl`** — `pathEqSensitive path path = True`. Reflexivity of
`(==)` over `String`.
- **`pathEqSym`** — `pathEqSensitive p1 p2 = pathEqSensitive p2 p1`.
Symmetry of `(==)` over `String`.
- **`addExtensionAdds`** — `isSuffixOf ("." ++ ext) (addExtension path
ext) = True`. `isSuffixOf` is FFI-bound.
- **`validPathNoNull`** — `not ('\0' \`elem\` unpack path) = True` for
validated `path`. `unpack` is FFI-bound.
- **`starMatchesAll`** — `matchGlob "*" s = True`. `unpack s` doesn't
reduce for abstract `s`.
- **`questionMatchesSingle`** — `matchGlob "?" (singleton c) = True`.
`unpack . singleton` round-trip is FFI-bound.
- **`literalMatchesSelf`** — wildcard-free `s` matches itself. `unpack`
+ `prim__eq_Char` both FFI-bound.

### Family 2 — List-of-components Refl gaps for canonicalisation (11
items)

`splitPath` / `normalizePath` / `joinSegments` route through FFI String
primitives (`prim__strHead`, `Strings.Substr.split`). The composition
`splitPath (joinSegments xs) = xs` for canonical `xs` is not a Refl in
Idris2 0.8.0. Same blocker family as SafeChecksum's `sumChecksum []`.

- **`normalizeIdempotent`** — `normalizePath` is a fixed point on
canonical segment lists.
- **`normalizeRemovesEmpty`** — no `""` segment survives. `elem` over
FFI-bound `(==)`.
- **`normalizeRemovesDot`** — no `"."` segment survives. Same `elem`/FFI
blocker.
- **`normalizeAbsNoLeadingDotDot`** — absolute paths can't start with
`..`. `isPrefixOf "/" path` hypothesis doesn't propagate through
`splitPath . normalizePath`.
- **`safeJoinNoEscape`** — `safeJoinPaths`'s `Just`-arm carries the
prefix witness by construction; extraction blocked by inner FFI.
- **`sanitizedIsSafe`** — `isSafeSegment (sanitizeSegment seg) = True`.
`unpack`/`pack` round-trip is FFI-bound.
- **`containedInBase`** — composes `safeJoinNoEscape` with
`isAncestorOf`'s definition; same inner blocker.
- **`sanitizedNoTraversal`** — sanitised path has no `..` segment.
`sanitizeSegment ".."` doesn't reduce for abstract segments.
- **`traversalHasDotDot`** — `elem ".." xs` ⇒ `any (== "..") xs`. Awaits
`Data.List.elem_any` in Prelude or `(==)` reflective tactic.
- **`containedStartsWithBase`** — `ContainedPath base`'s full path has
`base`'s normalised segments as a prefix; composes `safeJoinNoEscape`.
- **`validSegmentsBounded`** — every segment of a validated path has
length ≤ 255. Guard-chain extraction + `splitPath` FFI opacity.

### Family 3 — Predicate-fold gaps over path segments (3 items)

`getExtension` / `changeExtension` / `stripExtension` / `addExtension`
thread through `Strings.Substr.split (== '.')` / `forget` / `last` /
`init` / `joinSegments` — the round-trip requires composing five
list-elimination lemmas across the FFI seam.

- **`changeExtensionCorrect`** — `getExtension (changeExtension path
ext) = Just ext` for non-empty `ext`.
- **`stripExtensionRemoves`** — `getExtension (stripExtension path) =
Nothing` when the input had an extension.
- (`addExtensionAdds` is also a Family-3 claim but the dominant blocker
is Family-1 `isSuffixOf` — listed there.)

### Family 4 — `validatePath` guard-chain extraction + List.isPrefixOf
transitivity (2 items)

The nested `if`/`else` over `Bool` in `validatePath` doesn't propagate
guard-negation into the result type; `List.isPrefixOf` transitivity
isn't exposed in the Prelude as a Refl-reducible lemma.

- **`validPathBounded`** — `length path <= 4096` for validated paths.
- **`parentIsAncestor`** — `isParentOf` ⇒ `isAncestorOf` (left-conjunct
extraction).
- **`ancestorTransitive`** — `isAncestorOf` is transitive
(`List.isPrefixOf` transitivity).

## The two genuinely reducible claims (kept with bodies)

- **`emptyMatchesEmpty : matchGlob "" "" = True`** — `= Refl`.
- **`makeContainedDeterministic`** — `= Refl` (pure function).

## Safety posture

- Zero `believe_me`
- Zero `postulate`
- Zero `idris_crash`
- All `0 `-erased — postulates cannot leak into runtime
- Discoverable as named declarations (vs silent / commented-out)

## Test plan

- [ ] Idris2 0.8.0 `--check` on `src/Proven/SafePath/Proofs.idr` once
estate base-package dependency resolution is unjammed (CI is currently
jammed — DRAFT until then; mirrors the precedent set by PRs
#41/#46/#47/#48/#51/#52/#53/#54)
- [ ] Verify no downstream module shadows the names (grep was clean at
edit time)
- [ ] Owner review of OWED reasons against SafeChecksum / SafeYAML
precedent

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

Author: hyperpolymath