proof(SafeJson): fix appendLengthInc so the module compiles (completes #138)

[hyperpolymath]

Summary

Completes the work of #138, verified end-to-end against a clean Idris2 0.8.0 + contrib toolchain. Discharges the two SafeJson.Proofs OWEDs #138 targeted, and fixes the pre-existing bug that was actually preventing the module from compiling.

idris2 --check src/Proven/SafeJson/Proofs.idr builds all 5 modules (Core → Parser → Access → SafeJson → Proofs) with 0 errors (one pre-existing unreachable-clause warning in Access, also present on main).

What it discharges

• anyMatchesTAny — 6-arm case-split on JsonValue; for each concrete head every earlier clause demands a non-TAny second argument, so each arm reduces to the catch-all matchesType _ TAny = True by Refl. No totality change needed.
• singleKeyPath — with-pattern on lookup k obj, both arms by Refl (Maybe-identity).

The actual blocker: appendLengthInc (from #127)

Data.List.Equalities.lengthSnoc is element-first (lengthSnoc x xs), so the existing lengthSnoc arr v does not type-check under Idris2 0.8.0 contrib (Mismatch: JsonValue vs List ?a). Because it fails to elaborate, it blocks the entire SafeJson.Proofs module — so none of its proofs (including #138's two new ones) were checkable. Fixed to lengthSnoc v arr.

This is the failure #138's description attributed to "a local contrib quirk [that] does NOT reproduce in CI." It is not local — it reproduces on a clean v0.8.0 install, which also means main's own idris2 --build proven.ipkg currently fails at this module. This PR fixes that.

Correction to an earlier version of this PR

An earlier push on this branch also marked getPath/getSegment total and claimed that annotation was required for singleKeyPath to discharge. That claim was wrong and has been reverted. Verified: with appendLengthInc fixed, SafeJson.Proofs checks cleanly while those accessors stay covering (the %default in Access.idr). The covering annotation does not block the clause-level reduction the proof relies on, so no totality change is needed and Access.idr is left untouched. The change set is now Proofs.idr only.

Verification (clean idris2 0.8.0, contrib + network)

• ✅ idris2 --check src/Proven/SafeJson/Proofs.idr — all 5 modules, 0 errors, Access left covering
• ✅ Reverting the lengthSnoc fix reproduces the appendLengthInc Mismatch
• ✅ Confirmed the total annotation is not needed (covering + fix compiles clean) — hence dropped
• ✅ No believe_me / postulate / idris_crash / assert_total

Relationship to #138

#138 is closed; its branch already carries this same minimal fix. This PR (on the development branch) is the canonical, CI-running version.

Refs #138, #127, proven#90 #107 #119.

---

Generated by Claude Code

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

[hyperpolymath]

📌 Systemic finding (filing here — repo Issues are disabled). This PR fixes a one-line proof bug, but that bug reaching main points at a CI-gating gap worth tracking separately.

1. main currently fails idris2 --build proven.ipkg

appendLengthInc (introduced by #127) calls lengthSnoc arr v, but Data.List.Equalities.lengthSnoc is element-first (lengthSnoc : (x : a) -> (xs : List a) -> length (xs ++ [x]) = S (length xs)). So lengthSnoc arr v does not type-check:

Error: While processing right hand side of appendLengthInc. When unifying:
    JsonValue   and   List ?a
Mismatch between: JsonValue and List ?a.
Proven.SafeJson.Proofs:208:36--208:37

Since the module fails to elaborate, every proof in SafeJson.Proofs is currently unchecked on main. Reproduced on a clean Idris2 v0.8.0 + contrib install (the exact toolchain idris2-ci.yml provisions). The fix here (lengthSnoc v arr) makes all five SafeJson modules build with 0 errors.

2. The Idris build did not gate the merge (root cause)

The more important problem: a non-compiling change reached main because the Idris build check didn't block it. From #127:

• created 18:50:58Z, merged 18:53:32Z — ~2.5 min later
• a cold build (0.8.0) takes ~20 min (per the workflow's own comments)
• proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommutative (proven#90 #107 #119) #127's build (0.8.0) / verify-idris-build checks are recorded as queued — not completed at merge time
• only SonarCloud had reported (success)

So green SonarCloud + a fast manual merge let broken Idris through. The same queued-for-hours pattern is visible across recent proof PRs.

Suggested remediation

1. Land this fix so main compiles again.
2. Make build (0.8.0) (ideally also verify-idris-build) a required status check on main via branch protection. Until then, "merged green" ≠ "type-checks."
3. Reduce Idris CI latency so requiring it is practical — confirm the actions/cache step is hitting; consider a fast cone-check gate (idris2 --check of just the changed module's closure, sub-minute) as the required job, with the full matrix non-blocking.

cc @hyperpolymath — flagging since Issues are disabled and this is broader than this PR.

---

Generated by Claude Code

[hyperpolymath]

Correction to my comment just above: repo Issues are not disabled — I've filed the systemic finding as #145. Please track the CI-gating discussion there; the comment above is superseded by that issue.

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 321 issues detected

Severity	Count
🔴 Critical	130
🟠 High	31
🟡 Medium	160

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence