Totality refactor: SafeJson.Access (%default covering → per-function total)

[hyperpolymath]

Summary

src/Proven/SafeJson/Access.idr line 17 declares:

```idris
-- JSON tree traversal functions are structurally recursive over nested
-- JsonValue but the totality checker cannot verify through where clauses.
%default covering
```

This makes every function in the file covering by default — including parsePathSegments/parsePathIndex (mutually recursive over List Char), getPath, matchesType, and the Show JsonValue instance.

Additionally src/Proven/SafeJson/Parser.idr:38 carries an explicit covering declaration.

The mutual recursion is genuinely structural — parsePathSegments and parsePathIndex decrement the List Char input on every call, and getPath/matchesType recurse on JSON children — but the totality checker cannot see the structural decrease through the where-clause sub-functions.

Refactor needed

For each covering function, do one of:

• Hoist the recursion out of where to top level so the structural-decrease argument is visible at the file level. This is the cleanest fix for parsePathSegments/parsePathIndex.
• Add an explicit fuel parameter for the JSON-tree traversals (getPath, matchesType) — the JSON value is the recursion subject, and an assert_smaller jval (extractChild jval) pattern works for the immediate cases. Fuel may be cleaner if multiple children recurse.
• Replace %default covering with %default total and let the compiler tell you which specific functions still need fixing. (Recommended starting point — surfaces the actual gap.)

OWED sites that discharge once this lands

Per docs/proof-debt-triage-tier-a.md:

• src/Proven/SafeJson/Proofs.idr:228 — singleKeyPath (~50 min after totality)
• src/Proven/SafeJson/Proofs.idr:339 — anyMatchesTAny (~50 min after totality)

Total downstream proof work: ~1.5h once totality lands. The refactor itself is estimated 3-5h (multiple mutually recursive functions, possibly some genuine non-trivial decreases).

Caveat

If the parsePath* functions genuinely cannot be proven total without a fuel parameter (e.g., the List Char is consumed but the JsonPath accumulator grows), the right answer may be to expose a fuel-bounded API and keep the unbounded version as a thin total wrapper that calls the fuel version with length input. Worth a feasibility check before committing to a refactor approach.

Acceptance criteria

• src/Proven/SafeJson/Access.idr builds with %default total and no per-function covering.
• src/Proven/SafeJson/Parser.idr builds without covering on line 38.
• Existing tests pass.
• The 2 OWED sites above land as discharged theorems in a follow-up PR.

Related

• Phase 2 triage plan: docs/proof-debt-triage.md §8 Days 11-14.
• Per-site disposition: docs/proof-debt-triage-tier-a.md § SafeJson.

🤖 Filed by Claude during Phase 2 Days 11-14 of the proof-debt triage.