Skip to content

Commit bb51407

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(SafeUrl): annotate 16 bodyless decls as OWED (Refs standards#158) (#61)
## Summary Apply the OWED-with-justification convention (set 2026-05-20 by SafeChecksum / SafeBuffer / SafeCryptoAccel / SafeHKDF / SafeBloom / SafeFPGA, lives in PRs #37-#46) to the 16 bodyless declarations in `src/Proven/SafeUrl/Proofs.idr`. Refs hyperpolymath/standards#158. Three parts per decl: ```idris ||| OWED: <one-sentence statement> ||| Held back by <specific Idris2 0.8.0 blocker>. Discharge once ||| <what would unblock it>. 0 declarationName : Type ``` No `postulate` keyword (consistent with every other `Proofs.idr` in the estate). No `believe_me`, no `idris_crash`. Erased multiplicity (`0 `) — these are stated assumptions, not runtime code, parallel to the I6/I7 stated-assumption pattern in `proof-of-work`'s ABI seam. ## Note on two runtime-consumed lemmas Two of the 16 OWED decls (`isSafeSchemeNotJavascript`, `lteFrom65535Check`) have in-file runtime call sites in `validateSafe` and `validatePort`. To keep the convention strictly uniform across all 16 decls, the corresponding data-constructor proof arguments are switched to erased multiplicity: - `MkSafeURL`'s second arg → `(0 _ : Not (url.scheme = Just (Custom "javascript")))` - `MkValidPort`'s second arg → `(0 _ : LTE p 65535)` This is a same-file change. Verified scope: - `SafeUrl.idr` does **not** import `SafeUrl.Proofs` (the dependency edge runs the other way), so external API is unchanged. - The similarly-named `MkValidPort` in `SafeNetwork/Port.idr` is a separate single-arg local constructor, unrelated to this one. ## The 16 decls ### Encoding / decoding (String/Char FFI opacity) 1. **`unreservedNotEncoded`** — `isAlphaNum c = True ⇒ percentEncode c = singleton c`. Blocked by `Data.Char.isAlphaNum` / `isUnreserved` routing through `prim__charPred` FFI; `Refl` cannot reduce the `if`-branch. 2. **`encodePreservesAlphaNum`** — fully-alphanumeric string is fixed by `urlEncode`. Blocked by `unpack`/`pack`/`concat` String FFI opacity (SafeFile `boundedReadAtMostLimit` family) + per-element `isAlphaNum`. 3. **`decodeUnreservedIdentity`** — fully-alphanumeric string round-trips through `urlDecode`. Same blocker family as #1 + #2. 4. **`encodeDecodeIdentity`** — full `urlDecode ∘ urlEncode = Just`. Blocked by String FFI + Char FFI + the percent-hex arithmetic identity. Same family as proof-of-work I7 (FFI-correctness assumption). ### Query builder / accessor (String equality, list folding) 5. **`emptyBuilderEmpty`** — `buildQueryString emptyQuery = ""`. Blocked by `Data.String.joinWith` not reducing through its inner `where`-block; `++` on String is FFI-opaque (same family as SafeHeader `renderedHeaderSafe`). 6. **`addParamIncreasesCount`** — `paramCount (addParam k v qb).params = S (paramCount qb.params)`. Reduces to the standard `length (xs ++ [x]) = S (length xs)` list-folding identity; needs induction on `xs`, `Refl` cannot close it. Stdlib-plumbing OWED (discharge in-Idris2). 7. **`setGetIdentity`** — `getParam k (setParam k v qs) = Just v`. Blocked by String `==` routing through `prim__eqString` FFI in the `if k == key` branches. 8. **`removeHasNot`** — `hasParam k (removeAllParams k qs) = False`. Same String-equality FFI blocker as #7. 9. **`filterPreservesOnly`** — `filterParams` keeps only entries with permitted keys. The standard `filterAll : all p (filter p xs) = True` lemma instantiated at our predicate; blocked by `Data.List` stdlib not exposing it `%reducible` + `elem` on String FFI opacity. ### Query parameter parsing (FFI-correctness assumptions) 10. **`parseIntValid`** — parsing `"42"` from a matching key yields `Just 42`. Blocked by `parseInteger`'s `strM`/`unpack`/`all isDigit`/`foldl` String+Char FFI chain (same family as SafeArgs `intParsingHandlesNegative`). 11. **`parseBoolTrue`** — parsing `"true"` yields `Just True`. Blocked by `case toLower s of "true" => …` String-literal match via `prim__eqString`. 12. **`parseBoolFalse`** — symmetric to `parseBoolTrue`. ### Query string merge (stdlib-plumbing + String equality) 13. **`mergeEmptyLeft`** — `mergeQueryStrings [] qs = qs`. Blocked by per-step `hasParam k acc` String-equality FFI opacity + `lengthSnoc`-style induction on `qs`. Same family as `setGetIdentity` + `addParamIncreasesCount`. 14. **`appendAssociative`** — inherited from `Data.List.appendAssociative`. Stdlib-plumbing OWED — proof exists in Prelude but not exposed `%reducible`; discharge by import + rewrite. Not a fundamental gap. ### URL security / port validation (String equality, LTE-from-Bool) 15. **`isSafeSchemeNotJavascript`** — `isSafeScheme url = True ⇒ Not (scheme = Just (Custom "javascript"))`. Blocked by `Custom "javascript" = Custom "javascript"` routing through `prim__eqString` for the payload — case-equality opaque to `Refl`. **Runtime-consumed** (see "Note" above); `MkSafeURL` arg moved to `(0 _ : ...)`. 16. **`lteFrom65535Check`** — `p <= 65535 = True ⇒ LTE p 65535`. The well-known `lteReflectsLTE` reflective lemma. Stdlib proof exists (`Decidable.Order.fromLte`-family) but the chain through `Ord Nat`'s `<=` does not reduce by `Refl`. **Runtime-consumed** (see "Note" above); `MkValidPort` arg moved to `(0 _ : ...)`. ## Out of scope - Discharging any OWED. Each annotation pins a stated path (reflective tactic / property-test / stdlib-plumbing); discharge is a separate per-decl PR per the standards#158 campaign rhythm. - Any file other than `src/Proven/SafeUrl/Proofs.idr`. The two `(0 _ : ...)` data-constructor argument changes are in the same file and have no out-of-file consumers (verified by grep). ## Test plan - [ ] Idris2 0.8.0 `--check` on `Proven.SafeUrl.Proofs` (build was not green pre-PR — file had 16 bodyless decls; this PR's job is to make the OWED state *discoverable* and convention-conformant, not to fix the build, per the standards#158 campaign rhythm.) - [ ] Grep audit: `^||| OWED:` count = `^0 [a-zA-Z]` count = 16. - [ ] No `postulate`, `believe_me`, or `idris_crash` introduced. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 6a6c484 commit bb51407

1 file changed

Lines changed: 227 additions & 68 deletions

File tree

‎src/Proven/SafeUrl/Proofs.idr‎

Lines changed: 227 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -32,20 +32,41 @@ parseDeterministic s = Refl
3232
-- URL Encoding Properties
3333
--------------------------------------------------------------------------------
3434

35-
||| Percent-encoding leaves unreserved (alphanumeric) characters unchanged
36-
unreservedNotEncoded : (c : Char) ->
37-
isAlphaNum c = True ->
38-
percentEncode c = singleton c
35+
||| OWED: Percent-encoding leaves unreserved (alphanumeric) characters
36+
||| unchanged. Operationally true by direct unfolding of `percentEncode`:
37+
||| `if isUnreserved c then singleton c else "%" ++ toHex (ord c)` —
38+
||| and `isUnreserved c = isAlphaNum c || c == '-' || c == '.' || ...`,
39+
||| so `isAlphaNum c = True` collapses `isUnreserved c` to `True` and the
40+
||| branch reduces to `singleton c`. Held back by Idris2 0.8.0 not
41+
||| type-level reducing `Data.Char.isAlphaNum` / `isUnreserved` — both
42+
||| route through the `Char` FFI primitive `prim__charPred` whose result
43+
||| is opaque to `Refl`. Same blocker family as SafeChecksum's
44+
||| `extractDigits` and SafeHeader's `hasCRLF` (Char/String FFI opacity).
45+
||| Discharge once a `Data.Char` reflective tactic is available, or
46+
||| `isUnreserved` is refactored to a non-FFI predicate.
47+
export
48+
0 unreservedNotEncoded : (c : Char) ->
49+
isAlphaNum c = True ->
50+
percentEncode c = singleton c
3951

4052
||| Empty string encodes to empty string
4153
public export
4254
encodeEmptyEmpty : urlEncode "" = ""
4355
encodeEmptyEmpty = Refl
4456

45-
||| URL-encoding a fully alphanumeric string is the identity
46-
encodePreservesAlphaNum : (s : String) ->
47-
all isAlphaNum (unpack s) = True ->
48-
urlEncode s = s
57+
||| OWED: URL-encoding a fully alphanumeric string is the identity.
58+
||| Operationally follows from `unreservedNotEncoded` lifted across
59+
||| `unpack`/`map percentEncode`/`concat`, plus the `concat . map
60+
||| singleton . unpack = id` String round-trip. Held back by Idris2
61+
||| 0.8.0 not type-level reducing `unpack`/`pack`/`concat` (String FFI
62+
||| opacity, same family as SafeFile `boundedReadAtMostLimit`) and not
63+
||| reducing `Data.Char.isAlphaNum` per-element (see
64+
||| `unreservedNotEncoded` above). Discharge once both String FFI
65+
||| reduction and a `Data.Char` reflective tactic are available.
66+
export
67+
0 encodePreservesAlphaNum : (s : String) ->
68+
all isAlphaNum (unpack s) = True ->
69+
urlEncode s = s
4970

5071
--------------------------------------------------------------------------------
5172
-- URL Decoding Properties
@@ -56,14 +77,35 @@ public export
5677
decodeEmptySucceeds : urlDecode "" = Just ""
5778
decodeEmptySucceeds = Refl
5879

59-
||| Decoding a string of unreserved characters is the identity
60-
decodeUnreservedIdentity : (s : String) ->
61-
all isAlphaNum (unpack s) = True ->
62-
urlDecode s = Just s
63-
64-
||| URL-encode then decode round-trips to the original string
65-
encodeDecodeIdentity : (s : String) ->
66-
urlDecode (urlEncode s) = Just s
80+
||| OWED: Decoding a string of unreserved characters is the identity.
81+
||| Operationally true because `urlDecode`'s inner `go` recurses on the
82+
||| char list, and every non-`%`-non-`+` char hits the wildcard branch
83+
||| `go (c :: rest) = Just (c :: ...)`. Combined with the
84+
||| `pack . unpack = id` round-trip this gives `urlDecode s = Just s`.
85+
||| Held back by Idris2 0.8.0 not reducing `unpack`/`pack` (String FFI
86+
||| opacity) and not reducing the per-element `isAlphaNum` premise to
87+
||| make the case analysis on `go` definitional. Discharge once String
88+
||| FFI reduction and a `Data.Char` reflective tactic are available.
89+
export
90+
0 decodeUnreservedIdentity : (s : String) ->
91+
all isAlphaNum (unpack s) = True ->
92+
urlDecode s = Just s
93+
94+
||| OWED: URL-encode then URL-decode round-trips to the original
95+
||| string. Operationally true by case-analysis on each character of
96+
||| `unpack s`: unreserved chars round-trip via `singleton`/wildcard
97+
||| branch; reserved chars round-trip via `"%" ++ toHex (ord c)` →
98+
||| `decodePercent`. Held back by Idris2 0.8.0 not reducing `unpack` /
99+
||| `pack` / `concat` (String FFI opacity), `Data.Char.chr`/`ord`
100+
||| (Char FFI), and the arithmetic identity
101+
||| `chr (hi * 16 + lo) = c` given `hi = ord c \`div\` 16`,
102+
||| `lo = ord c \`mod\` 16`. Same blocker family as proof-of-work I7
103+
||| (FFI-correctness assumption). Discharge once String/Char FFI
104+
||| reduction is available, or via a property-test + trusted-extraction
105+
||| validation campaign (see boj-server backend-assurance harness).
106+
export
107+
0 encodeDecodeIdentity : (s : String) ->
108+
urlDecode (urlEncode s) = Just s
67109

68110
--------------------------------------------------------------------------------
69111
-- Query String Properties
@@ -74,47 +116,117 @@ public export
74116
parseEmptyQuery : parseQueryString "" = []
75117
parseEmptyQuery = Refl
76118

77-
||| Empty query builder builds empty string.
78-
||| Depends on joinWith/map/formatPair where-clause reduction which is
79-
||| opaque to the type checker.
119+
||| OWED: Empty query builder builds the empty string.
120+
||| `buildQueryString emptyQuery` reduces to `joinWith "&" (map
121+
||| formatPair [])` = `joinWith "&" []` = `""`. Held back by Idris2
122+
||| 0.8.0 not reducing `Data.String.joinWith` past its inner
123+
||| `where`-block `go`, which threads through `++` on `String` (String
124+
||| FFI opacity). Same blocker family as SafeHeader `renderedHeaderSafe`.
125+
||| Discharge once `joinWith`/`++` on `String` are type-level reducible,
126+
||| or refactor `buildQueryString` to expose the empty-list base case
127+
||| at the top.
80128
export
81-
emptyBuilderEmpty : buildQueryString Query.emptyQuery = ""
82-
83-
||| Adding a parameter increases count.
84-
||| Depends on length (xs ++ [x]) = S (length xs) which requires
85-
||| induction on xs; Refl cannot close this for an abstract qb.
129+
0 emptyBuilderEmpty : buildQueryString Query.emptyQuery = ""
130+
131+
||| OWED: Adding a parameter increases the parameter count by one.
132+
||| `addParam key val qb` is defined as `MkQueryBuilder (qb.params ++
133+
||| [(key, val)])`, so the claim reduces to
134+
||| `length (qb.params ++ [(key, val)]) = S (length qb.params)`. This
135+
||| is a standard list-folding identity (`length (xs ++ [x]) = S (length
136+
||| xs)`) but requires induction on `xs` — `Refl` cannot close it for an
137+
||| abstract `qb.params`. Held back by Idris2 0.8.0's stdlib not
138+
||| exposing this lemma as a `%reducible` rewrite. Same family as
139+
||| SafeFile read/write tracking proofs. Discharge by importing /
140+
||| proving `lengthSnoc : (xs : List a) -> (x : a) -> length (xs ++ [x])
141+
||| = S (length xs)` and rewriting.
86142
export
87-
addParamIncreasesCount : (key, val : String) -> (qb : QueryBuilder) ->
88-
paramCount (addParam key val qb).params =
89-
S (paramCount qb.params)
90-
91-
||| Getting a parameter just set by key returns that value
92-
setGetIdentity : (key, val : String) -> (qs : QueryString) ->
93-
getParam key (setParam key val qs) = Just val
94-
95-
||| After removing all instances of a key, hasParam returns False
96-
removeHasNot : (key : String) -> (qs : QueryString) ->
97-
hasParam key (removeAllParams key qs) = False
98-
99-
||| filterParams keeps only entries whose keys are in the given list
100-
filterPreservesOnly : (keys : List String) -> (qs : QueryString) ->
101-
all (\(k, _) => k `elem` keys) (filterParams keys qs) = True
143+
0 addParamIncreasesCount : (key, val : String) -> (qb : QueryBuilder) ->
144+
paramCount (addParam key val qb).params =
145+
S (paramCount qb.params)
146+
147+
||| OWED: Getting a parameter just set by key returns that value.
148+
||| Operationally true by case analysis on `hasParam key qs`: in the
149+
||| `True` branch, `setParam` `map`-replaces every key-matching entry
150+
||| with `val`, and `getParam = lookup` returns the first match; in the
151+
||| `False` branch, `setParam` appends `(key, val)` to the end, and
152+
||| `lookup` falls through to that appended pair (since no earlier
153+
||| entry matches). Held back by Idris2 0.8.0 not type-level reducing
154+
||| `String` equality `==` (routes through `prim__eqString` FFI), so the
155+
||| `if k == key` branches in `setParam` and the `if k == key` branches
156+
||| in `lookup` cannot be evaluated by `Refl`. Same blocker family as
157+
||| SafeChecksum Luhn/ISBN (String FFI opacity). Discharge once String
158+
||| equality is type-level reducible, or via a property-test campaign.
159+
export
160+
0 setGetIdentity : (key, val : String) -> (qs : QueryString) ->
161+
getParam key (setParam key val qs) = Just val
162+
163+
||| OWED: After removing all instances of a key, `hasParam` returns
164+
||| False. `removeAllParams key = filter (\(k, _) => k /= key)`, so the
165+
||| filtered list contains no entry with key `k = key`; therefore
166+
||| `lookup key (removeAllParams key qs) = Nothing`, hence `isJust …
167+
||| = False`. Held back by Idris2 0.8.0 not type-level reducing
168+
||| `String` `/=` / `==` (`prim__eqString` FFI), so the per-element
169+
||| `filter` predicate's truth value is opaque to `Refl`, blocking
170+
||| induction over `qs`. Discharge once String equality is type-level
171+
||| reducible. Same blocker family as `setGetIdentity`.
172+
export
173+
0 removeHasNot : (key : String) -> (qs : QueryString) ->
174+
hasParam key (removeAllParams key qs) = False
175+
176+
||| OWED: `filterParams` keeps only entries whose keys are in the given
177+
||| list — equivalently, every entry surviving `filter (\(k, _) => k
178+
||| \`elem\` keys)` satisfies that predicate. This is the standard
179+
||| `Data.List` lemma `filterAll : (p : a -> Bool) -> (xs : List a) ->
180+
||| all p (filter p xs) = True` instantiated at our predicate. Held
181+
||| back by Idris2 0.8.0's `Data.List` not exposing `filterAll` as a
182+
||| `%reducible` rewrite, AND by `elem` on `String` routing through
183+
||| `prim__eqString` FFI (per-element opacity). Discharge by importing
184+
||| / proving the `filterAll` lemma and rewriting, once String equality
185+
||| is type-level reducible.
186+
export
187+
0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) ->
188+
all (\(k, _) => k `elem` keys) (filterParams keys qs) = True
102189

103190
--------------------------------------------------------------------------------
104191
-- Query Parameter Parsing Properties
105192
--------------------------------------------------------------------------------
106193

107-
||| Parsing integer "42" from a matching key yields Just 42
108-
parseIntValid : (key : String) ->
109-
getIntParam key [(key, "42")] = Just 42
110-
111-
||| Parsing bool "true" from a matching key yields Just True
112-
parseBoolTrue : (key : String) ->
113-
getBoolParam key [(key, "true")] = Just True
114-
115-
||| Parsing bool "false" from a matching key yields Just False
116-
parseBoolFalse : (key : String) ->
117-
getBoolParam key [(key, "false")] = Just False
194+
||| OWED: Parsing integer `"42"` from a matching key yields `Just 42`.
195+
||| `getIntParam key [(key, "42")] = getParam key [(key, "42")] >>=
196+
||| parseInteger`, which should reduce to `Just "42" >>= parseInteger
197+
||| = parseInteger "42" = Just 42`. Held back by Idris2 0.8.0 not
198+
||| type-level reducing `String` equality in `lookup`'s inner `if k ==
199+
||| key`, and not reducing `parseInteger`'s `strM`/`unpack`/`all
200+
||| isDigit`/`foldl` String+Char FFI chain. Same blocker family as
201+
||| SafeChecksum Luhn (FFI-correctness assumption — `parseInteger
202+
||| "42" = Just 42` is operationally true but opaque). Discharge via
203+
||| property-test + trusted-extraction validation.
204+
export
205+
0 parseIntValid : (key : String) ->
206+
getIntParam key [(key, "42")] = Just 42
207+
208+
||| OWED: Parsing bool `"true"` from a matching key yields `Just True`.
209+
||| `getBoolParam key [(key, "true")] = lookup key [(key, "true")] >>=
210+
||| parseBool`, and the inner `parseBool "true"` matches the literal
211+
||| `"true" => Just True` arm of its `case toLower s of …` after
212+
||| `toLower "true" = "true"`. Held back by Idris2 0.8.0 not type-level
213+
||| reducing `String` equality in `lookup` (`prim__eqString`) and the
214+
||| `case toLower s of "true" => …` String-literal match (also
215+
||| `prim__eqString`-routed). Same blocker family as `parseIntValid`.
216+
||| Discharge once String equality is type-level reducible, or via
217+
||| property-test campaign.
218+
export
219+
0 parseBoolTrue : (key : String) ->
220+
getBoolParam key [(key, "true")] = Just True
221+
222+
||| OWED: Parsing bool `"false"` from a matching key yields `Just
223+
||| False`. Symmetric to `parseBoolTrue` — operationally the
224+
||| `"false" => Just False` arm of `parseBool`'s `case toLower s of …`.
225+
||| Held back by the same Idris2 0.8.0 String-literal-match
226+
||| (`prim__eqString` FFI) opacity. Discharge with `parseBoolTrue`.
227+
export
228+
0 parseBoolFalse : (key : String) ->
229+
getBoolParam key [(key, "false")] = Just False
118230

119231
--------------------------------------------------------------------------------
120232
-- Query String Merge Properties
@@ -126,24 +238,47 @@ mergeEmptyRight : (qs : QueryString) ->
126238
mergeQueryStrings qs [] = qs
127239
mergeEmptyRight qs = Refl
128240

129-
||| Merging empty into a query string yields that query string
130-
mergeEmptyLeft : (qs : QueryString) ->
131-
mergeQueryStrings [] qs = qs
132-
133-
||| Query string append is associative (by list append associativity)
134-
appendAssociative : (qs1, qs2, qs3 : QueryString) ->
135-
appendQueryStrings (appendQueryStrings qs1 qs2) qs3 =
136-
appendQueryStrings qs1 (appendQueryStrings qs2 qs3)
241+
||| OWED: Merging empty (left) into a query string yields that query
242+
||| string. `mergeQueryStrings [] qs = foldl (\q, (k, v) => setParam k v
243+
||| q) [] qs`, i.e. fold starting from `[]` over all pairs in `qs`,
244+
||| each step calling `setParam k v` which (since the accumulator never
245+
||| already contains `k`) appends `[(k, v)]`. The final accumulator
246+
||| equals `qs`. Held back by Idris2 0.8.0 not reducing the per-step
247+
||| `hasParam k acc` check (`String` `==` via `prim__eqString` FFI),
248+
||| which would let us see the accumulator collapse to a snoc chain;
249+
||| also requires `lengthSnoc`-style induction on `qs`. Same blocker
250+
||| family as `setGetIdentity` and `addParamIncreasesCount`. Discharge
251+
||| once String equality is type-level reducible and the snoc-length
252+
||| lemma is `%reducible`.
253+
export
254+
0 mergeEmptyLeft : (qs : QueryString) ->
255+
mergeQueryStrings [] qs = qs
256+
257+
||| OWED: Query string append is associative — inherited from
258+
||| `Data.List.appendAssociative` since `appendQueryStrings = (++)` on
259+
||| `QueryString = List (String, String)`. Held back by Idris2 0.8.0's
260+
||| `Data.List` not exposing `appendAssociative` as a `%reducible`
261+
||| rewrite (the proof exists in Prelude but requires induction on
262+
||| `qs1`, and `Refl` cannot close it for abstract `qs1`). Discharge
263+
||| by importing `Data.List.appendAssociative` and rewriting (the
264+
||| proof is in-Idris2 — this is a stdlib-plumbing OWED, not a
265+
||| fundamental gap).
266+
export
267+
0 appendAssociative : (qs1, qs2, qs3 : QueryString) ->
268+
appendQueryStrings (appendQueryStrings qs1 qs2) qs3 =
269+
appendQueryStrings qs1 (appendQueryStrings qs2 qs3)
137270

138271
--------------------------------------------------------------------------------
139272
-- URL Security Properties
140273
--------------------------------------------------------------------------------
141274

142-
||| Data type for safe URLs (no javascript: scheme)
275+
||| Data type for safe URLs (no javascript: scheme).
276+
||| The non-javascript proof is stored at erased multiplicity (`0`)
277+
||| because `isSafeSchemeNotJavascript` is OWED — see below.
143278
public export
144279
data SafeURL : ParsedURL -> Type where
145280
MkSafeURL : (url : ParsedURL) ->
146-
Not (url.scheme = Just (Custom "javascript")) ->
281+
(0 _ : Not (url.scheme = Just (Custom "javascript"))) ->
147282
SafeURL url
148283

149284
||| Check if URL has safe scheme
@@ -155,9 +290,20 @@ isSafeScheme url = case url.scheme of
155290
Just (Custom "vbscript") => False
156291
_ => True
157292

158-
||| If isSafeScheme holds, the scheme is not javascript (for MkSafeURL)
159-
isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True ->
160-
Not (url.scheme = Just (Custom "javascript"))
293+
||| OWED: If `isSafeScheme url = True`, then `url.scheme` is not
294+
||| `Just (Custom "javascript")`. By contraposition on `isSafeScheme`'s
295+
||| case-analysis: if the scheme were `Just (Custom "javascript")`, the
296+
||| first arm would fire and return `False`, contradicting the
297+
||| hypothesis `isSafeScheme url = True`. Held back by Idris2 0.8.0
298+
||| not type-level reducing `String` equality (`Custom "javascript" =
299+
||| Custom "javascript"` routes through `prim__eqString` for the
300+
||| payload) — without that, the case-equality required to derive the
301+
||| contradiction is opaque to `Refl`. Same blocker family as
302+
||| `setGetIdentity`. Discharge once String equality is type-level
303+
||| reducible. Used by `validateSafe` to construct `MkSafeURL`.
304+
export
305+
0 isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True ->
306+
Not (url.scheme = Just (Custom "javascript"))
161307

162308
||| Validate URL is safe
163309
public export
@@ -178,13 +324,26 @@ data ValidIPv4 : Host -> Type where
178324
LTE a 255 -> LTE b 255 -> LTE c 255 -> LTE d 255 ->
179325
ValidIPv4 (IPv4 a b c d)
180326

181-
||| Port number is bounded
327+
||| Port number is bounded.
328+
||| The `LTE p 65535` proof is stored at erased multiplicity (`0`)
329+
||| because `lteFrom65535Check` is OWED — see below.
182330
public export
183331
data ValidPort : Nat -> Type where
184-
MkValidPort : (p : Nat) -> LTE p 65535 -> ValidPort p
185-
186-
||| Runtime comparison p <= 65535 implies the LTE proof witness
187-
lteFrom65535Check : (p : Nat) -> (p <= 65535 = True) -> LTE p 65535
332+
MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p
333+
334+
||| OWED: Runtime comparison `p <= 65535 = True` implies the `LTE p
335+
||| 65535` proof witness. Operationally this is the well-known
336+
||| reflective lemma `Data.Nat.lteReflectsLTE : (n, m : Nat) -> n <= m
337+
||| = True -> LTE n m`. Held back by Idris2 0.8.0's `Data.Nat` not
338+
||| exposing this as a definitional/`%reducible` rewrite — the stdlib
339+
||| proof exists (`Decidable.Order.fromLte`-family) but the chain
340+
||| through `Ord Nat`'s `<=` implementation does not reduce via `Refl`
341+
||| for an abstract `p`. Discharge by importing the existing stdlib
342+
||| lemma and rewriting (this is a stdlib-plumbing OWED, not a
343+
||| fundamental gap). Consumed by `validatePort` to construct
344+
||| `MkValidPort`'s erased proof argument.
345+
export
346+
0 lteFrom65535Check : (p : Nat) -> (p <= 65535 = True) -> LTE p 65535
188347

189348
||| Validate port is in range
190349
public export

0 commit comments

Comments
 (0)