Skip to content

Commit c63abf8

Browse files
claudeclaude
committed
proof(SafeJson): DISCHARGE anyMatchesTAny + singleKeyPath; fix appendLengthInc; make path accessors total
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
1 parent 40b127f commit c63abf8

2 files changed

Lines changed: 60 additions & 41 deletions

File tree

‎src/Proven/SafeJson/Access.idr‎

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,8 +93,15 @@ field _ _ = Left NotAnObject
9393
-- Safe Path Access
9494
--------------------------------------------------------------------------------
9595

96-
||| Access JSON value at a path segment
97-
public export
96+
||| Access JSON value at a path segment.
97+
||| Marked `total` (overriding the module-default `covering`): the top-level
98+
||| dispatch is non-recursive and the `index'` helper recurses structurally
99+
||| on `Nat`/`List`. Totality — not merely coverage — is what lets the
100+
||| equational lemmas in `Proven.SafeJson.Proofs` reduce `getSegment` on
101+
||| abstract arguments, since Idris2 0.8.0 does not unfold `covering`
102+
||| definitions during conversion checking.
103+
public export
104+
total
98105
getSegment : PathSegment -> JsonValue -> Maybe JsonValue
99106
getSegment (Key k) (JsonObject pairs) = lookup k pairs
100107
getSegment (Index i) (JsonArray arr) = index' i arr
@@ -105,8 +112,13 @@ getSegment (Index i) (JsonArray arr) = index' i arr
105112
index' (S n) (_ :: xs) = index' n xs
106113
getSegment _ _ = Nothing
107114

108-
||| Access JSON value at a path
115+
||| Access JSON value at a path.
116+
||| Marked `total` (overriding the module-default `covering`): structurally
117+
||| decreasing on the path list and dispatching through the now-`total`
118+
||| `getSegment`. Required so `singleKeyPath` (and future path lemmas) in
119+
||| `Proven.SafeJson.Proofs` can reduce `getPath` on abstract arguments.
109120
public export
121+
total
110122
getPath : JsonPath -> JsonValue -> Maybe JsonValue
111123
getPath [] val = Just val
112124
getPath (seg :: rest) val = case getSegment seg val of

‎src/Proven/SafeJson/Proofs.idr‎

Lines changed: 45 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -198,14 +198,17 @@ prependLengthInc v arr = Refl
198198
||| DISCHARGED: `append v (JsonArray arr) = JsonArray (arr ++ [v])`
199199
||| (SafeJson.idr L233-234), so the goal reduces to
200200
||| `Just (length (arr ++ [v])) = Just (length arr + 1)`. Apply
201-
||| `lengthSnoc arr v : length (arr ++ [v]) = S (length arr)`, then
201+
||| `lengthSnoc v arr : length (arr ++ [v]) = S (length arr)`, then
202202
||| close the `S n` vs `n + 1` gap with `plusCommutative 1 n`.
203+
||| (`Data.List.Equalities.lengthSnoc` takes the element first, then the
204+
||| list — `lengthSnoc x xs`; the previous `lengthSnoc arr v` argument
205+
||| order did not type-check under Idris2 0.8.0 contrib.)
203206
public export
204207
appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
205208
arrayLength (append v (JsonArray arr)) =
206209
Just (length arr + 1)
207210
appendLengthInc v arr =
208-
cong Just (trans (lengthSnoc arr v) (plusCommutative 1 (length arr)))
211+
cong Just (trans (lengthSnoc v arr) (plusCommutative 1 (length arr)))
209212

210213
--------------------------------------------------------------------------------
211214
-- Path Access Properties
@@ -216,26 +219,32 @@ public export
216219
emptyPathIdentity : (v : JsonValue) -> getPath [] v = Just v
217220
emptyPathIdentity v = Refl
218221

219-
||| OWED: a single-segment `Key k` path equals direct `lookup`:
222+
||| DISCHARGED: a single-segment `Key k` path equals direct `lookup`:
220223
||| `getPath [Key k] (JsonObject obj) = lookup k obj`.
221-
||| `getPath` is defined in `Proven.SafeJson.Access` and dispatches
222-
||| through `getSegment` (mutually recursive across `PathSegment`
223-
||| constructors). Idris2 0.8.0 marks the family `covering` (not
224-
||| `total`) because the recursion is on `List PathSegment` paired
225-
||| with a `JsonValue` whose `JsonArray`/`JsonObject` arms recurse
226-
||| with new path-tails — same termination-witness shape as the
227-
||| `Proven.SafeJson.Access.deletePath` unreachable-clause warning
228-
||| already in this build. Covering functions do NOT reduce by
229-
||| `Refl` outside their pattern arms in Idris2 0.8.0, so this
230-
||| statement cannot be discharged without an external
231-
||| `assert_total`-style reduction lemma. Held back by the same
232-
||| Access-module covering/total gap that motivated removing
233-
||| `singleIndexPath` (L154 comment). Discharge once `getPath`
234-
||| can be re-stated as `total` via a structurally decreasing
235-
||| metric (path length is the obvious candidate).
236-
public export
237-
0 singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
224+
|||
225+
||| The original OWED comment correctly identified the blocker: while
226+
||| `getPath`/`getSegment` were `covering` (via the `%default covering`
227+
||| in `Proven.SafeJson.Access`), Idris2 0.8.0 does not reduce `covering`
228+
||| definitions during proof conversion, so neither side of the equation
229+
||| meets — verified: even the one-step
230+
||| `getSegment (Key k) (JsonObject obj) = lookup k obj` fails by `Refl`
231+
||| while the module default holds. The fix lives in
232+
||| `Proven.SafeJson.Access`: both functions are now explicitly `total`
233+
||| (they always were structurally — `getSegment` is non-recursive,
234+
||| `getPath` decreases on the path list). With totality `getPath`
235+
||| reduces:
236+
||| getPath [Key k] (JsonObject obj)
237+
||| = case getSegment (Key k) (JsonObject obj) of
238+
||| { Nothing => Nothing; Just v => getPath [] v }
239+
||| = case lookup k obj of { Nothing => Nothing; Just v => Just v }
240+
||| and the `with`-pattern on `lookup k obj` closes both arms by `Refl`
241+
||| (Maybe-identity).
242+
public export
243+
singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
238244
getPath [Key k] (JsonObject obj) = lookup k obj
245+
singleKeyPath k obj with (lookup k obj)
246+
singleKeyPath k obj | Nothing = Refl
247+
singleKeyPath k obj | Just _ = Refl
239248

240249
-- singleIndexPath: removed — where-clause in type signature is invalid
241250
-- in Idris2 0.8.0 and the index' helper conflicts with stdlib names.
@@ -326,26 +335,24 @@ public export
326335
stringMatchesTString : (s : String) -> matchesType (JsonString s) TString = True
327336
stringMatchesTString s = Refl
328337

329-
||| OWED: every `JsonValue` matches `TAny`:
338+
||| DISCHARGED: every `JsonValue` matches `TAny`:
330339
||| `matchesType v TAny = True` for all `v`.
331340
||| Definitionally `matchesType _ TAny = True` (`SafeJson.idr` L353).
332-
||| The clause is a catch-all on the second argument and reduces by
333-
||| `Refl` for any concrete `v` constructor — but Idris2 0.8.0 will
334-
||| not reduce it for an abstract `v : JsonValue` because the
335-
||| preceding clauses (`JsonArray arr` / `JsonObject pairs` with
336-
||| `TArray`/`TObject`/`TOneOf` on the right) are *covering* (not
337-
||| total): `matchesType` mutually recurses through `all` over the
338-
||| array/object children. Covering definitions do not reduce on
339-
||| open variables in Idris2 0.8.0 — same blocker family as
340-
||| `singleKeyPath` above. The proof would normally close by a
341-
||| six-arm case-split on `v` (`JsonNull`/`JsonBool b`/`JsonNumber n`
342-
||| /`JsonString s`/`JsonArray arr`/`JsonObject pairs`), each with
343-
||| `Refl`. Held back by the covering-vs-total reduction policy.
344-
||| Discharge once `matchesType` is restated as `total` (e.g. by
345-
||| an explicit size metric over `JsonValue` + children), or with
346-
||| a manual six-arm split that elaborates per-arm `Refl`s.
347-
public export
348-
0 anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True
341+
||| Unlike `singleKeyPath`, this needs no totality change: although
342+
||| `matchesType` is `covering`, supplying a concrete head constructor
343+
||| in each arm of a manual six-arm case-split
344+
||| (`JsonNull` / `JsonBool b` / `JsonNumber n` / `JsonString s` /
345+
||| `JsonArray arr` / `JsonObject pairs`) is enough — every earlier
346+
||| clause demands a non-`TAny` second argument, so each arm reduces
347+
||| through the catch-all `matchesType _ TAny = True` clause by `Refl`.
348+
public export
349+
anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True
350+
anyMatchesTAny JsonNull = Refl
351+
anyMatchesTAny (JsonBool _) = Refl
352+
anyMatchesTAny (JsonNumber _) = Refl
353+
anyMatchesTAny (JsonString _) = Refl
354+
anyMatchesTAny (JsonArray _) = Refl
355+
anyMatchesTAny (JsonObject _) = Refl
349356

350357
--------------------------------------------------------------------------------
351358
-- Totality Proofs

0 commit comments

Comments
 (0)