proof(SafeJson): DISCHARGE 4 object-key OWEDs via DecEq carrier refactor

[hyperpolymath]

Summary

Refactor set/get/hasKey/remove in Proven.SafeJson to use a DecEq String key carrier (new lookupObj/updateObj/removeObj) instead of the prior (==)/(/=)/lookup/filter chain. Runtime semantics identical; the win is that decEq's Yes/No arms expose structural proofs the discharge lemmas pattern-match on.

OWEDs cleared (4/12 SafeJson remaining → 8 left)

OWED	Discharge
setGetIdentity	Induction + lookupObjConsRefl / lookupObjConsSkip + IH
setPreservesOther	Induction + 4-way case-split on decEq k1 k' × decEq k2 k', new lookupObjConsCong lifts IH through cons in No-No branch
setHasKey	cong isJust (setGetIdentity ...)
removeNotHasKey	cong isJust (removeLookupNothing ...) with new top-level removeLookupNothing lemma

Type strengthening

setPreservesOther / setHasKey / removeNotHasKey had obj : JsonValue with isObject obj = True hypothesis. The old form was vacuously trivial for non-JsonObject values; the strengthened form takes obj : List (String, JsonValue) (the object body directly), so the proof carries the actual key-preservation invariant.

New reusable helpers

• lookupObjConsRefl : reflexive head match returns head
• lookupObjConsSkip : non-matching head skips
• lookupObjConsCong : equation lifting through cons
• removeLookupNothing : remove-then-lookup misses

API impact

set : String -> JsonValue -> JsonValue -> JsonValue and friends keep their signatures. Internal update/lookup/filter replaced by updateObj/lookupObj/removeObj. merge also updated to use updateObj for consistency.

Verification

• idris2 --check src/Proven/SafeJson.idr → Exit 0
• idris2 --check src/Proven/SafeJson/Proofs.idr → only pre-existing appendLengthInc local-vs-CI quirk (same as PR proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommutative (proven#90 #107 #119) #127/proof(SafeJson): DISCHARGE anyMatchesTAny (6-arm split) + singleKeyPath (with-pattern) #138, doesn't repro in CI)
• /tmp/charrefl/src/TestDecEq.idr prototype: all 4 OWED shapes proven
• Zero believe_me / postulate / idris_crash

Remaining SafeJson OWEDs (8 left)

All 6 parser OWEDs (parseNullCorrect / parseTrueCorrect / parseFalseCorrect / parseEmptyFails / parseEmptyArray / parseEmptyObject) — to be addressed by Family B (parseJsonChars : List Char -> Maybe JsonValue + bridge). Plus 2 already discharged in #138 (anyMatchesTAny, singleKeyPath).

Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious OWED meta), proven#119 (paths-forward — this is Family A implementing the DecEq-carrier path).

Test plan

• Local SafeJson.idr type-check clean
• Local SafeJson/Proofs.idr type-check (only pre-existing quirk)
• /tmp/charrefl prototype of all 4 discharge proofs
• CI `idris2 --check proven.ipkg` green
• CI test suite green

🤖 Generated with 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

[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