From c63abf87648658da66924b9d9cb3f6142930d4af Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 30 May 2026 23:10:30 +0000 Subject: [PATCH 1/2] proof(SafeJson): DISCHARGE anyMatchesTAny + singleKeyPath; fix appendLengthInc; make path accessors total MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the work of PR #138, verified end-to-end against a clean Idris2 0.8.0 + contrib toolchain (idris2 --check builds all 5 SafeJson modules with 0 errors). Discharges two SafeJson.Proofs OWEDs: - anyMatchesTAny: 6-arm case-split on JsonValue; each concrete head reduces through the catch-all `matchesType _ TAny = True` by Refl (matchesType stays `covering` — a concrete head per arm is enough). - singleKeyPath: with-pattern on `lookup k obj`, both arms by Refl (Maybe-identity). Two corrections PR #138 as-authored required but missed: 1. getPath / getSegment are made `total` in SafeJson.Access. They were `covering` via the module `%default covering` (contrary to the PR's claim that they were already total). Idris2 0.8.0 does not reduce `covering` definitions during proof conversion, so singleKeyPath cannot discharge while they remain covering — reverting the annotation reproduces the `singleKeyPath` Mismatch failure. Both are structurally total: getSegment is non-recursive, getPath decreases on the path list. 2. appendLengthInc (from PR #127) had its `lengthSnoc` arguments swapped. `Data.List.Equalities.lengthSnoc` takes the element first (`lengthSnoc x xs`), so `lengthSnoc arr v` does not type-check under Idris2 0.8.0 contrib. This pre-existing error blocks the entire SafeJson.Proofs module from compiling on main, so it had to be fixed for any of these proofs to be checkable. Corrected to `lengthSnoc v arr`. No believe_me / postulate / idris_crash / assert_total introduced. Refs #138, #127, proven#90 #107 #119. https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy --- src/Proven/SafeJson/Access.idr | 18 ++++++-- src/Proven/SafeJson/Proofs.idr | 83 ++++++++++++++++++---------------- 2 files changed, 60 insertions(+), 41 deletions(-) diff --git a/src/Proven/SafeJson/Access.idr b/src/Proven/SafeJson/Access.idr index 707e0b996..e8d75b8f2 100644 --- a/src/Proven/SafeJson/Access.idr +++ b/src/Proven/SafeJson/Access.idr @@ -93,8 +93,15 @@ field _ _ = Left NotAnObject -- Safe Path Access -------------------------------------------------------------------------------- -||| Access JSON value at a path segment -public export +||| Access JSON value at a path segment. +||| Marked `total` (overriding the module-default `covering`): the top-level +||| dispatch is non-recursive and the `index'` helper recurses structurally +||| on `Nat`/`List`. Totality — not merely coverage — is what lets the +||| equational lemmas in `Proven.SafeJson.Proofs` reduce `getSegment` on +||| abstract arguments, since Idris2 0.8.0 does not unfold `covering` +||| definitions during conversion checking. +public export +total getSegment : PathSegment -> JsonValue -> Maybe JsonValue getSegment (Key k) (JsonObject pairs) = lookup k pairs getSegment (Index i) (JsonArray arr) = index' i arr @@ -105,8 +112,13 @@ getSegment (Index i) (JsonArray arr) = index' i arr index' (S n) (_ :: xs) = index' n xs getSegment _ _ = Nothing -||| Access JSON value at a path +||| Access JSON value at a path. +||| Marked `total` (overriding the module-default `covering`): structurally +||| decreasing on the path list and dispatching through the now-`total` +||| `getSegment`. Required so `singleKeyPath` (and future path lemmas) in +||| `Proven.SafeJson.Proofs` can reduce `getPath` on abstract arguments. public export +total getPath : JsonPath -> JsonValue -> Maybe JsonValue getPath [] val = Just val getPath (seg :: rest) val = case getSegment seg val of diff --git a/src/Proven/SafeJson/Proofs.idr b/src/Proven/SafeJson/Proofs.idr index 5f50109f9..9a870a45a 100644 --- a/src/Proven/SafeJson/Proofs.idr +++ b/src/Proven/SafeJson/Proofs.idr @@ -198,14 +198,17 @@ prependLengthInc v arr = Refl ||| DISCHARGED: `append v (JsonArray arr) = JsonArray (arr ++ [v])` ||| (SafeJson.idr L233-234), so the goal reduces to ||| `Just (length (arr ++ [v])) = Just (length arr + 1)`. Apply -||| `lengthSnoc arr v : length (arr ++ [v]) = S (length arr)`, then +||| `lengthSnoc v arr : length (arr ++ [v]) = S (length arr)`, then ||| close the `S n` vs `n + 1` gap with `plusCommutative 1 n`. +||| (`Data.List.Equalities.lengthSnoc` takes the element first, then the +||| list — `lengthSnoc x xs`; the previous `lengthSnoc arr v` argument +||| order did not type-check under Idris2 0.8.0 contrib.) public export appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) -> arrayLength (append v (JsonArray arr)) = Just (length arr + 1) appendLengthInc v arr = - cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr))) + cong Just (trans (lengthSnoc v arr) (plusCommutative 1 (length arr))) -------------------------------------------------------------------------------- -- Path Access Properties @@ -216,26 +219,32 @@ public export emptyPathIdentity : (v : JsonValue) -> getPath [] v = Just v emptyPathIdentity v = Refl -||| OWED: a single-segment `Key k` path equals direct `lookup`: +||| DISCHARGED: a single-segment `Key k` path equals direct `lookup`: ||| `getPath [Key k] (JsonObject obj) = lookup k obj`. -||| `getPath` is defined in `Proven.SafeJson.Access` and dispatches -||| through `getSegment` (mutually recursive across `PathSegment` -||| constructors). Idris2 0.8.0 marks the family `covering` (not -||| `total`) because the recursion is on `List PathSegment` paired -||| with a `JsonValue` whose `JsonArray`/`JsonObject` arms recurse -||| with new path-tails — same termination-witness shape as the -||| `Proven.SafeJson.Access.deletePath` unreachable-clause warning -||| already in this build. Covering functions do NOT reduce by -||| `Refl` outside their pattern arms in Idris2 0.8.0, so this -||| statement cannot be discharged without an external -||| `assert_total`-style reduction lemma. Held back by the same -||| Access-module covering/total gap that motivated removing -||| `singleIndexPath` (L154 comment). Discharge once `getPath` -||| can be re-stated as `total` via a structurally decreasing -||| metric (path length is the obvious candidate). -public export -0 singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) -> +||| +||| The original OWED comment correctly identified the blocker: while +||| `getPath`/`getSegment` were `covering` (via the `%default covering` +||| in `Proven.SafeJson.Access`), Idris2 0.8.0 does not reduce `covering` +||| definitions during proof conversion, so neither side of the equation +||| meets — verified: even the one-step +||| `getSegment (Key k) (JsonObject obj) = lookup k obj` fails by `Refl` +||| while the module default holds. The fix lives in +||| `Proven.SafeJson.Access`: both functions are now explicitly `total` +||| (they always were structurally — `getSegment` is non-recursive, +||| `getPath` decreases on the path list). With totality `getPath` +||| reduces: +||| getPath [Key k] (JsonObject obj) +||| = case getSegment (Key k) (JsonObject obj) of +||| { Nothing => Nothing; Just v => getPath [] v } +||| = case lookup k obj of { Nothing => Nothing; Just v => Just v } +||| and the `with`-pattern on `lookup k obj` closes both arms by `Refl` +||| (Maybe-identity). +public export +singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) -> getPath [Key k] (JsonObject obj) = lookup k obj +singleKeyPath k obj with (lookup k obj) + singleKeyPath k obj | Nothing = Refl + singleKeyPath k obj | Just _ = Refl -- singleIndexPath: removed — where-clause in type signature is invalid -- in Idris2 0.8.0 and the index' helper conflicts with stdlib names. @@ -326,26 +335,24 @@ public export stringMatchesTString : (s : String) -> matchesType (JsonString s) TString = True stringMatchesTString s = Refl -||| OWED: every `JsonValue` matches `TAny`: +||| DISCHARGED: every `JsonValue` matches `TAny`: ||| `matchesType v TAny = True` for all `v`. ||| Definitionally `matchesType _ TAny = True` (`SafeJson.idr` L353). -||| The clause is a catch-all on the second argument and reduces by -||| `Refl` for any concrete `v` constructor — but Idris2 0.8.0 will -||| not reduce it for an abstract `v : JsonValue` because the -||| preceding clauses (`JsonArray arr` / `JsonObject pairs` with -||| `TArray`/`TObject`/`TOneOf` on the right) are *covering* (not -||| total): `matchesType` mutually recurses through `all` over the -||| array/object children. Covering definitions do not reduce on -||| open variables in Idris2 0.8.0 — same blocker family as -||| `singleKeyPath` above. The proof would normally close by a -||| six-arm case-split on `v` (`JsonNull`/`JsonBool b`/`JsonNumber n` -||| /`JsonString s`/`JsonArray arr`/`JsonObject pairs`), each with -||| `Refl`. Held back by the covering-vs-total reduction policy. -||| Discharge once `matchesType` is restated as `total` (e.g. by -||| an explicit size metric over `JsonValue` + children), or with -||| a manual six-arm split that elaborates per-arm `Refl`s. -public export -0 anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True +||| Unlike `singleKeyPath`, this needs no totality change: although +||| `matchesType` is `covering`, supplying a concrete head constructor +||| in each arm of a manual six-arm case-split +||| (`JsonNull` / `JsonBool b` / `JsonNumber n` / `JsonString s` / +||| `JsonArray arr` / `JsonObject pairs`) is enough — every earlier +||| clause demands a non-`TAny` second argument, so each arm reduces +||| through the catch-all `matchesType _ TAny = True` clause by `Refl`. +public export +anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True +anyMatchesTAny JsonNull = Refl +anyMatchesTAny (JsonBool _) = Refl +anyMatchesTAny (JsonNumber _) = Refl +anyMatchesTAny (JsonString _) = Refl +anyMatchesTAny (JsonArray _) = Refl +anyMatchesTAny (JsonObject _) = Refl -------------------------------------------------------------------------------- -- Totality Proofs From ecda96ecfbccfa74a13ea21cc5341675f82cba6e Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 31 May 2026 05:56:02 +0000 Subject: [PATCH 2/2] proof(SafeJson): drop unnecessary `total` change; keep minimal appendLengthInc fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Aligns this branch with the verified-minimal change set (matching the fix on #138's branch). Supersedes the previous commit, which marked getPath/getSegment `total` and claimed that annotation was required for singleKeyPath to discharge. That claim was wrong. Verified against a clean Idris2 0.8.0 + contrib toolchain: with appendLengthInc fixed, SafeJson.Proofs type-checks with getPath/getSegment left `covering` (the module default) — 0 errors across all five SafeJson modules. The covering annotation does not block the clause-level reduction singleKeyPath relies on, so no totality change is needed. Access.idr is therefore reverted to its main state (untouched). The only substantive fix is the one this branch actually needs: appendLengthInc used `lengthSnoc arr v`, but Data.List.Equalities.lengthSnoc is element-first (`lengthSnoc x xs`); `lengthSnoc arr v` fails to type-check under Idris2 0.8.0 contrib and blocks the whole module. Corrected to `lengthSnoc v arr`. Proof comments for singleKeyPath and anyMatchesTAny corrected to match (no false "they are total" claim), and stale /tmp/ scratch-path references removed. No believe_me / postulate / idris_crash / assert_total introduced. Refs #138, #127, proven#90 #107 #119. https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy --- src/Proven/SafeJson/Access.idr | 18 +++----------- src/Proven/SafeJson/Proofs.idr | 44 ++++++++++++++-------------------- 2 files changed, 21 insertions(+), 41 deletions(-) diff --git a/src/Proven/SafeJson/Access.idr b/src/Proven/SafeJson/Access.idr index e8d75b8f2..707e0b996 100644 --- a/src/Proven/SafeJson/Access.idr +++ b/src/Proven/SafeJson/Access.idr @@ -93,15 +93,8 @@ field _ _ = Left NotAnObject -- Safe Path Access -------------------------------------------------------------------------------- -||| Access JSON value at a path segment. -||| Marked `total` (overriding the module-default `covering`): the top-level -||| dispatch is non-recursive and the `index'` helper recurses structurally -||| on `Nat`/`List`. Totality — not merely coverage — is what lets the -||| equational lemmas in `Proven.SafeJson.Proofs` reduce `getSegment` on -||| abstract arguments, since Idris2 0.8.0 does not unfold `covering` -||| definitions during conversion checking. -public export -total +||| Access JSON value at a path segment +public export getSegment : PathSegment -> JsonValue -> Maybe JsonValue getSegment (Key k) (JsonObject pairs) = lookup k pairs getSegment (Index i) (JsonArray arr) = index' i arr @@ -112,13 +105,8 @@ getSegment (Index i) (JsonArray arr) = index' i arr index' (S n) (_ :: xs) = index' n xs getSegment _ _ = Nothing -||| Access JSON value at a path. -||| Marked `total` (overriding the module-default `covering`): structurally -||| decreasing on the path list and dispatching through the now-`total` -||| `getSegment`. Required so `singleKeyPath` (and future path lemmas) in -||| `Proven.SafeJson.Proofs` can reduce `getPath` on abstract arguments. +||| Access JSON value at a path public export -total getPath : JsonPath -> JsonValue -> Maybe JsonValue getPath [] val = Just val getPath (seg :: rest) val = case getSegment seg val of diff --git a/src/Proven/SafeJson/Proofs.idr b/src/Proven/SafeJson/Proofs.idr index 9a870a45a..42a7d34f1 100644 --- a/src/Proven/SafeJson/Proofs.idr +++ b/src/Proven/SafeJson/Proofs.idr @@ -202,7 +202,8 @@ prependLengthInc v arr = Refl ||| close the `S n` vs `n + 1` gap with `plusCommutative 1 n`. ||| (`Data.List.Equalities.lengthSnoc` takes the element first, then the ||| list — `lengthSnoc x xs`; the previous `lengthSnoc arr v` argument -||| order did not type-check under Idris2 0.8.0 contrib.) +||| order did not type-check under Idris2 0.8.0 contrib and blocked the +||| whole module from compiling.) public export appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) -> arrayLength (append v (JsonArray arr)) = @@ -221,24 +222,15 @@ emptyPathIdentity v = Refl ||| DISCHARGED: a single-segment `Key k` path equals direct `lookup`: ||| `getPath [Key k] (JsonObject obj) = lookup k obj`. -||| -||| The original OWED comment correctly identified the blocker: while -||| `getPath`/`getSegment` were `covering` (via the `%default covering` -||| in `Proven.SafeJson.Access`), Idris2 0.8.0 does not reduce `covering` -||| definitions during proof conversion, so neither side of the equation -||| meets — verified: even the one-step -||| `getSegment (Key k) (JsonObject obj) = lookup k obj` fails by `Refl` -||| while the module default holds. The fix lives in -||| `Proven.SafeJson.Access`: both functions are now explicitly `total` -||| (they always were structurally — `getSegment` is non-recursive, -||| `getPath` decreases on the path list). With totality `getPath` -||| reduces: -||| getPath [Key k] (JsonObject obj) -||| = case getSegment (Key k) (JsonObject obj) of -||| { Nothing => Nothing; Just v => getPath [] v } -||| = case lookup k obj of { Nothing => Nothing; Just v => Just v } -||| and the `with`-pattern on `lookup k obj` closes both arms by `Refl` -||| (Maybe-identity). +||| On the concrete spine `[Key k]` / `JsonObject obj`, `getPath` and +||| `getSegment` reduce by clause-matching to +||| case lookup k obj of { Nothing => Nothing; Just v => Just v } +||| Abstracting `lookup k obj` with a `with`-pattern then closes both +||| arms by `Refl` (Maybe-identity). +||| (`getPath`/`getSegment` are `covering` via the `%default covering` +||| in `Proven.SafeJson.Access`; that annotation does not block this +||| clause-level reduction, so they are left covering and the proof +||| still goes through.) public export singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) -> getPath [Key k] (JsonObject obj) = lookup k obj @@ -338,13 +330,13 @@ stringMatchesTString s = Refl ||| DISCHARGED: every `JsonValue` matches `TAny`: ||| `matchesType v TAny = True` for all `v`. ||| Definitionally `matchesType _ TAny = True` (`SafeJson.idr` L353). -||| Unlike `singleKeyPath`, this needs no totality change: although -||| `matchesType` is `covering`, supplying a concrete head constructor -||| in each arm of a manual six-arm case-split -||| (`JsonNull` / `JsonBool b` / `JsonNumber n` / `JsonString s` / -||| `JsonArray arr` / `JsonObject pairs`) is enough — every earlier -||| clause demands a non-`TAny` second argument, so each arm reduces -||| through the catch-all `matchesType _ TAny = True` clause by `Refl`. +||| Discharged by a six-arm case-split on `v` (`JsonNull` / `JsonBool b` +||| / `JsonNumber n` / `JsonString s` / `JsonArray arr` / +||| `JsonObject pairs`): `matchesType _ TAny = True` is a catch-all, and +||| for each concrete head every earlier clause demands a non-`TAny` +||| second argument, so each arm reduces to the catch-all and closes by +||| `Refl`. No totality change is needed — a concrete head per arm is +||| sufficient even though `matchesType` is `covering`. public export anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True anyMatchesTAny JsonNull = Refl