Skip to content

Commit 1213bf2

Browse files
hyperpolymathhyperpolymath
authored
proof(SafeJson): annotate 13 bodyless decls as OWED (Refs standards#158) (#56)
## Summary Converts the 13 bare `export <sig>` postulates in `src/Proven/SafeJson/Proofs.idr` to the estate's OWED-with-justification convention established 2026-05-20 across the SafeChecksum / SafeBuffer / SafeCryptoAccel / SafeHKDF / SafeBloom / SafeFPGA / SafeAPIKey / SafeCORS / SafeCSV / SafeSemVer / SafeHtml / SafeArgs / SafeHTTP / SafeFile / SafeHeader / SafeMath / SafeTOML / SafeCSRF / SafeEnv siblings: - Triple-pipe `|||` docstring stating the claim. - Leading `0 ` erased-multiplicity (runtime-stripped). - Bare type signature; **no** `postulate` keyword. - Explicit Idris2 0.8.0 blocker + discharge condition per decl. Refs hyperpolymath/standards#158. ## The 13 OWED items, grouped by blocker family ### Family A — String FFI opacity (4 decls) `set` / `get` / `remove` / `hasKey` thread through `prim__eq_String` (or its `(/=)` lift via `filter`). Idris2 0.8.0 has no reflective `prim__eq_String`-to-`Dec`-eq lemma. Same class-(J) family as `boj-server` `Boj.SafetyLemmas.charEqSym` (`prim__eqChar` reflection gap) and `gossamer` `stringNotEqCommut` (`Panels.Distinct`, landed in gossamer PR #41). 1. `setGetIdentity` — `get k (set k v (JsonObject obj)) = Just v`. 2. `setPreservesOther` — `Not (k1 = k2) -> get k2 (set k1 v obj) = get k2 obj`. 3. `setHasKey` — `isObject obj = True -> hasKey k (set k v obj) = True`. 4. `removeNotHasKey` — `hasKey k (remove k obj) = False`. Joint discharge: ship a class-(J) `String` reflection axiom (mirror of `gossamer` `stringNotEqCommut`) or refactor `update` / `lookup` / `filter` onto a `DecEq` carrier. ### Family B — List length-append composition (1 decl) `Data.List.lengthAppend` in Idris2 0.8.0 is stated `length (xs ++ ys) = length xs + length ys`. Closing `length (arr ++ [v]) = length arr + 1` requires composing `lengthAppend` + `length [v] = 1` + `plusZeroRightNeutral` + `S` congruence — doable but multi-step, deferred to batch-discharge. 5. `appendLengthInc` — `arrayLength (append v (JsonArray arr)) = Just (length arr + 1)`. Discharge: write the 4-step composed proof, or add a one-step `lengthAppendSingleton` lemma to base. ### Family C — Covering-vs-total reduction (2 decls) `getPath` (in `Proven.SafeJson.Access`) and `matchesType` are `covering` (mutual recursion through `getSegment` / `all`). Idris2 0.8.0 will not reduce a `covering` function on abstract variables — same shape as the `deletePath` unreachable-clause warning already in this build. 6. `singleKeyPath` — `getPath [Key k] (JsonObject obj) = lookup k obj`. 7. `anyMatchesTAny` — `matchesType v TAny = True` for all `v`. Discharge: restate the callee as `total` via a structurally decreasing metric (path length / `JsonValue` size), or hand-write per-arm splits that elaborate `Refl` constructor-by-constructor. ### Family D — Parser FFI opacity (6 decls) `parseJson` dispatches into `Proven.SafeJson.Parser` and threads through `unpack` / `pack` / `strHead` / `strSubstr` plus fuel-driven recursion. No `parseJson "<literal>"` reduces to its result by `Refl` under Idris2 0.8.0. Same blocker family as `SafeChecksum` Luhn/ISBN (FFI-bound String) and `SafeHtml.escapePreservesNoLT`. 8. `parseNullCorrect` — `parseJson "null" = Just JsonNull`. 9. `parseTrueCorrect` — `parseJson "true" = Just (JsonBool True)`. 10. `parseFalseCorrect` — `parseJson "false" = Just (JsonBool False)`. 11. `parseEmptyFails` — `parseJson "" = Nothing`. 12. `parseEmptyArray` — `parseJson "[]" = Just (JsonArray [])`. 13. `parseEmptyObject` — `parseJson "{}" = Just (JsonObject [])`. Joint discharge: ship a reflective `String`-to-`List Char` axiom (or refactor the parser onto `List Char` end-to-end so the literal `unpack` can be supplied as a trusted constant at the call site). ## Verification ``` cd src && idris2 -p base --source-dir . --check --total \ Proven/SafeJson/Proofs.idr # -> exit 0 (5/5 modules build, no errors, --total accepted) ``` - All 13 OWED sigs carry erased multiplicity (`0 …`), so they are runtime-stripped — no executable axiom escapes into the built artifact. - Module-level shared comment for Family D avoids 6× near-duplicate docstrings while keeping each decl individually annotated per the convention. - Pre-existing `Proven.SafeJson.Access:282 deletePath _ _ = Nothing` unreachable-clause warning is unrelated to this PR and stays as the upstream baseline (it is the very `covering` family-C blocker cited for `singleKeyPath`). ## Why DRAFT Filed DRAFT per the convention (estate proven-CI queue settles asynchronously, sibling OWED PRs are landed by the owner in batches). ## Test plan - [x] `idris2 --check --total` green on the touched module against `origin/main` (rebased to `df6b0a1`, current SafeEnv tip). - [x] No other files touched (`git diff --stat` = 1 file). - [x] No callers depend on these sigs in a way that requires bodies (they were already bodyless `export` postulates on main). - [ ] Owner: merge after the estate proven-CI queue catches up. Refs hyperpolymath/standards#158.
1 parent c375b7b commit 1213bf2

1 file changed

Lines changed: 174 additions & 54 deletions

File tree

‎src/Proven/SafeJson/Proofs.idr‎

Lines changed: 174 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -87,29 +87,74 @@ asObjectFromObject obj = Refl
8787
-- Object Access Properties
8888
--------------------------------------------------------------------------------
8989

90-
||| Getting a key that was just set returns that value.
91-
||| Depends on Idris2 SafeJson set/get implementation correctness.
92-
export
93-
setGetIdentity : (k : String) -> (v : JsonValue) -> (obj : List (String, JsonValue)) ->
90+
||| OWED: getting a key that was just set returns that value:
91+
||| `get k (set k v (JsonObject obj)) = Just v`.
92+
||| `set` calls `update key val pairs` (`SafeJson.idr` L179) and `get`
93+
||| calls `lookup key pairs` (L156). Both thread through `(==)` on
94+
||| `String`, whose comparison is the opaque FFI primitive
95+
||| `prim__eq_String`. Idris2 0.8.0 does not reduce `k == k = True`
96+
||| by `Refl` — same blocker family as `SafeChecksum` Luhn/ISBN
97+
||| (FFI-bound String) and `boj-server` `Boj.SafetyLemmas.charEqSym`
98+
||| (the class-(J) `prim__eqChar` reflection gap, generalised to
99+
||| `String`). Held back by the absence of a reflective
100+
||| `prim__eq_String`-to-`Dec`-eq lemma in Idris2 0.8.0 base.
101+
||| Discharge once a class-(J) `String` reflection axiom is added
102+
||| or `update`/`lookup` are refactored onto a decidable-equality
103+
||| key type.
104+
public export
105+
0 setGetIdentity : (k : String) -> (v : JsonValue) -> (obj : List (String, JsonValue)) ->
94106
get k (set k v (JsonObject obj)) = Just v
95107

96-
||| Setting a key preserves other keys.
97-
||| Depends on Idris2 SafeJson set/get implementation correctness.
98-
export
99-
setPreservesOther : (k1, k2 : String) -> Not (k1 = k2) ->
108+
||| OWED: setting a different key preserves the other key's value:
109+
||| `Not (k1 = k2) -> get k2 (set k1 v obj) = get k2 obj`.
110+
||| `set k1 v` calls `update k1 v pairs`, which compares `k1 == k`
111+
||| for every pair `(k, _)` in the list. The proof requires that
112+
||| `k1 == k2 = False` (negative direction) whenever `Not (k1 = k2)`
113+
||| — the converse of `setGetIdentity`'s blocker, in the same
114+
||| `prim__eq_String` reflection-gap family. Idris2 0.8.0 has no
115+
||| primitive lemma `Not (a = b) -> prim__eq_String a b = False` and
116+
||| the elaborator cannot derive it by `Refl`. Same shape as the
117+
||| `gossamer` `stringNotEqCommut` class-(J) axiom landed in
118+
||| `Panels.Distinct` (`PR #41`). Held back by absence of a
119+
||| reflective `String`-disequality lemma. Discharge once the
120+
||| class-(J) `stringNotEq` axiom is shared via base, or `update`
121+
||| is rewritten on a `DecEq` carrier.
122+
public export
123+
0 setPreservesOther : (k1, k2 : String) -> Not (k1 = k2) ->
100124
(v : JsonValue) -> (obj : JsonValue) ->
101125
get k2 (set k1 v obj) = get k2 obj
102126

103-
||| A key that was set exists in the object.
104-
||| Depends on Idris2 SafeJson set/hasKey implementation correctness.
105-
export
106-
setHasKey : (k : String) -> (v : JsonValue) -> (obj : JsonValue) ->
127+
||| OWED: after `set k v obj`, `hasKey k` returns `True` whenever
128+
||| `obj` is an object.
129+
||| `hasKey key json = isJust (get key json)` (`SafeJson.idr` L162),
130+
||| so this reduces to `get k (set k v obj) = Just _`, which is the
131+
||| same `prim__eq_String` reflection gap as `setGetIdentity`. The
132+
||| extra hypothesis `isObject obj = True` only excludes the
133+
||| non-`JsonObject` arms of `set` (which return `obj` unchanged) —
134+
||| the residual obligation still threads through opaque String FFI
135+
||| equality. Held back by the same Idris2 0.8.0 blocker. Discharge
136+
||| together with `setGetIdentity` once a class-(J) `String`
137+
||| reflection lemma is in base.
138+
public export
139+
0 setHasKey : (k : String) -> (v : JsonValue) -> (obj : JsonValue) ->
107140
isObject obj = True -> hasKey k (set k v obj) = True
108141

109-
||| Removing a key means it no longer exists.
110-
||| Depends on Idris2 SafeJson remove/hasKey implementation correctness.
111-
export
112-
removeNotHasKey : (k : String) -> (obj : JsonValue) ->
142+
||| OWED: after `remove k obj`, `hasKey k` returns `False`.
143+
||| `remove k (JsonObject pairs) = JsonObject (filter (\(k', _) => k' /= k) pairs)`
144+
||| (`SafeJson.idr` L191). The proof needs `filter` to drop every
145+
||| pair with key `k`, which requires `k' /= k = False` whenever
146+
||| `k' = k` — i.e. `prim__eq_String k k = True` and its lifting
147+
||| through `/=`. Same FFI-opaque-String blocker family as
148+
||| `setGetIdentity` / `setPreservesOther`. Also requires the
149+
||| non-`JsonObject` arms (which return `obj` unchanged) not to
150+
||| contain `k`, but for arbitrary `obj : JsonValue` the statement
151+
||| is unconditionally false on `JsonObject [(k, _)]` reduced
152+
||| through any non-pattern-matching FFI path. Held back jointly
153+
||| by the `prim__eq_String` reflection gap and the absence of a
154+
||| reduction lemma for `filter` on FFI-keyed pairs. Discharge once
155+
||| both are addressed.
156+
public export
157+
0 removeNotHasKey : (k : String) -> (obj : JsonValue) ->
113158
hasKey k (remove k obj) = False
114159

115160
--------------------------------------------------------------------------------
@@ -129,10 +174,27 @@ prependLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
129174
Just (S (length arr))
130175
prependLengthInc v arr = Refl
131176

132-
||| Appending increases array length by 1.
133-
||| Depends on Idris2 SafeJson append/arrayLength implementation correctness.
134-
export
135-
appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
177+
||| OWED: appending an element increments the array length:
178+
||| `arrayLength (append v (JsonArray arr)) = Just (length arr + 1)`.
179+
||| `append v (JsonArray arr) = JsonArray (arr ++ [v])` (`SafeJson.idr`
180+
||| L234), so the proof reduces to
181+
||| `length (arr ++ [v]) = length arr + 1`, the standard list lemma.
182+
||| Idris2 0.8.0 does NOT reduce `length (arr ++ [v])` to
183+
||| `length arr + 1` by `Refl` alone — `(++)` is recursive on its
184+
||| first argument and stuck on the abstract `arr`. The proof
185+
||| obligation is `lengthAppend` (with `[v]` on the right), but
186+
||| `Data.List.lengthAppend` in Idris2 0.8.0 is stated as
187+
||| `length (xs ++ ys) = length xs + length ys` and applying it
188+
||| leaves a residual `length arr + length [v] = length arr + 1`
189+
||| that further requires `length [v] = 1` by `Refl` and the
190+
||| asymmetry of `+` on Nat (`plusZeroRightNeutral` shape). Doable
191+
||| with a multi-step proof; deferred for batch-discharge alongside
192+
||| the rest of this module. Held back by absence of a one-step
193+
||| `Data.List.lengthAppendSingleton` lemma. Discharge by composing
194+
||| `lengthAppend` + `plusZeroRightNeutral` + `S` congruence, or by
195+
||| adding a direct singleton-append lemma to base.
196+
public export
197+
0 appendLengthInc : (v : JsonValue) -> (arr : List JsonValue) ->
136198
arrayLength (append v (JsonArray arr)) =
137199
Just (length arr + 1)
138200

@@ -145,10 +207,25 @@ public export
145207
emptyPathIdentity : (v : JsonValue) -> getPath [] v = Just v
146208
emptyPathIdentity v = Refl
147209

148-
||| Single key path is equivalent to direct key access.
149-
||| Depends on getPath/getSegment reduction through Access module internals.
150-
export
151-
singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
210+
||| OWED: a single-segment `Key k` path equals direct `lookup`:
211+
||| `getPath [Key k] (JsonObject obj) = lookup k obj`.
212+
||| `getPath` is defined in `Proven.SafeJson.Access` and dispatches
213+
||| through `getSegment` (mutually recursive across `PathSegment`
214+
||| constructors). Idris2 0.8.0 marks the family `covering` (not
215+
||| `total`) because the recursion is on `List PathSegment` paired
216+
||| with a `JsonValue` whose `JsonArray`/`JsonObject` arms recurse
217+
||| with new path-tails — same termination-witness shape as the
218+
||| `Proven.SafeJson.Access.deletePath` unreachable-clause warning
219+
||| already in this build. Covering functions do NOT reduce by
220+
||| `Refl` outside their pattern arms in Idris2 0.8.0, so this
221+
||| statement cannot be discharged without an external
222+
||| `assert_total`-style reduction lemma. Held back by the same
223+
||| Access-module covering/total gap that motivated removing
224+
||| `singleIndexPath` (L154 comment). Discharge once `getPath`
225+
||| can be re-stated as `total` via a structurally decreasing
226+
||| metric (path length is the obvious candidate).
227+
public export
228+
0 singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
152229
getPath [Key k] (JsonObject obj) = lookup k obj
153230

154231
-- singleIndexPath: removed — where-clause in type signature is invalid
@@ -158,35 +235,63 @@ singleKeyPath : (k : String) -> (obj : List (String, JsonValue)) ->
158235
-- Parsing Properties
159236
--------------------------------------------------------------------------------
160237

161-
||| Parsing "null" gives JsonNull.
162-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
163-
export
164-
parseNullCorrect : parseJson "null" = Just JsonNull
165-
166-
||| Parsing "true" gives JsonBool True.
167-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
168-
export
169-
parseTrueCorrect : parseJson "true" = Just (JsonBool True)
238+
-- The six `parse*Correct` / `parseEmpty*` declarations below all
239+
-- share the same blocker family: `parseJson` (defined in
240+
-- `Proven.SafeJson` and dispatching to `Proven.SafeJson.Parser`)
241+
-- threads through `unpack`, `pack`, `strHead`, `strSubstr` and
242+
-- explicit fuel-driven recursion. Every one of those operates on
243+
-- `String` via Idris2 0.8.0's opaque FFI primitives, so no
244+
-- `parseJson "<literal>"` reduces to its result by `Refl`. Same
245+
-- blocker family as `SafeChecksum` Luhn/ISBN (FFI-bound String)
246+
-- and `SafeHtml.escapePreservesNoLT`. They all discharge together
247+
-- once Idris2 gains a reflective `String`-to-`List Char` axiom (or
248+
-- the parser is rewritten to operate on `List Char` end-to-end so
249+
-- the literal `unpack` can be supplied at the call site as a
250+
-- trusted constant).
251+
252+
||| OWED: `parseJson "null" = Just JsonNull`.
253+
||| Held back by Idris2 0.8.0's String-FFI opacity on the parser's
254+
||| `unpack`/`strHead` driver (see module-level comment above).
255+
||| Discharge once a reflective `String`-to-`List Char` axiom is
256+
||| available, or the parser is refactored onto `List Char`.
257+
public export
258+
0 parseNullCorrect : parseJson "null" = Just JsonNull
170259

171-
||| Parsing "false" gives JsonBool False.
172-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
173-
export
174-
parseFalseCorrect : parseJson "false" = Just (JsonBool False)
260+
||| OWED: `parseJson "true" = Just (JsonBool True)`.
261+
||| Held back by the same String-FFI parser opacity as
262+
||| `parseNullCorrect`. Discharge together.
263+
public export
264+
0 parseTrueCorrect : parseJson "true" = Just (JsonBool True)
175265

176-
||| Parsing an empty string fails.
177-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
178-
export
179-
parseEmptyFails : parseJson "" = Nothing
266+
||| OWED: `parseJson "false" = Just (JsonBool False)`.
267+
||| Held back by the same String-FFI parser opacity as
268+
||| `parseNullCorrect`. Discharge together.
269+
public export
270+
0 parseFalseCorrect : parseJson "false" = Just (JsonBool False)
271+
272+
||| OWED: `parseJson "" = Nothing`.
273+
||| Held back by the same String-FFI parser opacity as
274+
||| `parseNullCorrect` — `parseJson` cannot reduce the empty-string
275+
||| early-return arm to `Nothing` by `Refl` because the dispatch
276+
||| goes through `strHead`/`strLength` (FFI primitives). Discharge
277+
||| together with the rest of the parse-* family.
278+
public export
279+
0 parseEmptyFails : parseJson "" = Nothing
180280

181-
||| Parsing empty array succeeds.
182-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
183-
export
184-
parseEmptyArray : parseJson "[]" = Just (JsonArray [])
281+
||| OWED: `parseJson "[]" = Just (JsonArray [])`.
282+
||| Held back by the same String-FFI parser opacity as
283+
||| `parseNullCorrect`, plus the parser's two-character lookahead
284+
||| (`'['` then `']'`) which threads through `strSubstr`. Discharge
285+
||| together.
286+
public export
287+
0 parseEmptyArray : parseJson "[]" = Just (JsonArray [])
185288

186-
||| Parsing empty object succeeds.
187-
||| Depends on Idris2 SafeJson parseJson implementation correctness.
188-
export
189-
parseEmptyObject : parseJson "{}" = Just (JsonObject [])
289+
||| OWED: `parseJson "{}" = Just (JsonObject [])`.
290+
||| Held back by the same String-FFI parser opacity as
291+
||| `parseEmptyArray` (object-literal lookahead on `'{'` / `'}'`).
292+
||| Discharge together.
293+
public export
294+
0 parseEmptyObject : parseJson "{}" = Just (JsonObject [])
190295

191296
--------------------------------------------------------------------------------
192297
-- Validation Properties
@@ -212,11 +317,26 @@ public export
212317
stringMatchesTString : (s : String) -> matchesType (JsonString s) TString = True
213318
stringMatchesTString s = Refl
214319

215-
||| Any value matches TAny type.
216-
||| Depends on matchesType (covering due to mutual recursion) reducing
217-
||| for the TAny case.
218-
export
219-
anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True
320+
||| OWED: every `JsonValue` matches `TAny`:
321+
||| `matchesType v TAny = True` for all `v`.
322+
||| Definitionally `matchesType _ TAny = True` (`SafeJson.idr` L353).
323+
||| The clause is a catch-all on the second argument and reduces by
324+
||| `Refl` for any concrete `v` constructor — but Idris2 0.8.0 will
325+
||| not reduce it for an abstract `v : JsonValue` because the
326+
||| preceding clauses (`JsonArray arr` / `JsonObject pairs` with
327+
||| `TArray`/`TObject`/`TOneOf` on the right) are *covering* (not
328+
||| total): `matchesType` mutually recurses through `all` over the
329+
||| array/object children. Covering definitions do not reduce on
330+
||| open variables in Idris2 0.8.0 — same blocker family as
331+
||| `singleKeyPath` above. The proof would normally close by a
332+
||| six-arm case-split on `v` (`JsonNull`/`JsonBool b`/`JsonNumber n`
333+
||| /`JsonString s`/`JsonArray arr`/`JsonObject pairs`), each with
334+
||| `Refl`. Held back by the covering-vs-total reduction policy.
335+
||| Discharge once `matchesType` is restated as `total` (e.g. by
336+
||| an explicit size metric over `JsonValue` + children), or with
337+
||| a manual six-arm split that elaborates per-arm `Refl`s.
338+
public export
339+
0 anyMatchesTAny : (v : JsonValue) -> matchesType v TAny = True
220340

221341
--------------------------------------------------------------------------------
222342
-- Totality Proofs

0 commit comments

Comments
 (0)