diff --git a/docs/IDRIS2-BUILD-WORK-PACKAGE.adoc b/docs/IDRIS2-BUILD-WORK-PACKAGE.adoc new file mode 100644 index 00000000..1a34e29f --- /dev/null +++ b/docs/IDRIS2-BUILD-WORK-PACKAGE.adoc @@ -0,0 +1,501 @@ += Idris2 Build Work Package +:toc: macro +:toclevels: 3 +:source-highlighter: rouge + +Handover document for continuing the `proven` Idris2 build-repair campaign. + +Written 2026-08-27 at the point where the build frontier reached **211/305**. +Its purpose is that the next person does not re-derive any of this. + +Every claim below was produced by running the Idris2 compiler and reading its exit +code. Where something is an inference rather than a measurement, it says so. + +toc::[] + +== 0. Read this first — the three framing facts + +=== 0.1 VOID is not RED, and RED is not a regression + +The exit-code convention this campaign uses throughout: + +[cols="1,4"] +|=== +| `0` | correct — the check ran and passed +| `1` | wrong outcome — the check ran and failed +| `2` | **VOID** — no check was performed +|=== + +Before this campaign, `idris2 --build proven.ipkg` was **cancelled at CI's 45-minute +timeout** with zero modules built. That is VOID, not red: nothing was measured, so +nothing was learned. The campaign's first achievement was not fixing an error — it was +moving the build from *unmeasurable* to *measurably wrong*. + +=== 0.2 The error count is not a progress metric; the frontier is + +`SafeRegex/Parser.idr` reported **39 errors**. Classified by hand, that was +**6 real roots + 33 transitive totality propagations**. Curing the 6 roots took the +standalone check to **0 errors**. + +A *rising* error count after a fix is almost always **successive unmasking** — the +compiler getting further and finding more. Judge progress by the frontier +(`N/305: Building `), never by the error count. + +=== 0.3 Every frontier figure must name the tree it was measured on, and the compiler version + +* All figures here are **Idris2 0.7.0**, while the source and CI target **0.8.0**. +* Frontier **211/305** was measured on the **dirty working tree**, which carries an + uncommitted cure that `origin/main` does not have (see <>). A build of + `origin/main`, or of the PR #206 branch, **cannot** reach 211. + +== 1. Where the build actually is + +.Frontier progression, Idris2 0.7.0 +[cols="1,3,4,2"] +|=== +| Step | Frontier | Blocker | Status + +| — | `1/300` | build never completed | VOID +| 36 | `165/305` `SafeOTP` | class 13 + class 30 | cured +| 37 | `167/305` `SafeRedirect` | class 31 ×2 | cured +| 38 | `168/305` `SafeCSP` | class 32 | cured — **+30 modules** +| 39 | `198/305` `SafeCrypto.Proofs` | class 33 ×2 | cured, real proofs +| 40 | `203/305` `SafeUrl.Proofs` | class 35 | cured +| 41 | `210/305` `SafeRegex.Parser` | class 36 ×25, eta bug, 3 totality roots, class 37 | cured — rc=0 +| 42 | **`211/305` `SafeRegex.Matcher`** | see <> | **diagnosed, NOT fixed — this is the next job** +|=== + +Seven modules cured. **Zero new trusted-base markers** across the whole campaign. +Five proof obligations genuinely discharged (two in strictly stronger, generalised form): +`modernIsSecure`, `standardIsSecure`, `errorMakesInvalid`, `warningKeepsValid`, +`lteFrom65535Check`. + +Published as **PR #206**, seven files, based on `origin/main`. + +[[sweep]] +== 2. ⚠ The working tree is load-bearing — do not clean it + +This is the single most important operational fact in this document. + +`proven`'s working tree carries **245 uncommitted modified files**. They look like the +residue of an interrupted estate sweep. **They are not merely residue.** A large part of +them is the only thing making the repository parse. + +Measured on a pristine `origin/main` tree: + +[cols="4,1,1"] +|=== +| Detector over `src/**/*.idr`, pristine `origin/main` | Files | Occurrences + +| Raw grep `(^\|[[:space:]])postulate[[:space:]]` | 46 | 369 +| **Declaration position only** (comment lines excluded) | **42** | **360** +| Comment-only mentions (`--` / `\|\|\|`) | 4 | 9 +| Local working tree, declaration position | **0** | **0** +|=== + +IMPORTANT: The raw grep over-counts by 4 files. `SafeCrypto/Hash.idr`, +`SafeCrypto/Random.idr`, `SafeHTTP.idr` and `SafeJWT/Validate.idr` mention +`postulate` only inside comments and parse fine on `origin/main`. Quote **42**, +never 46 — the same over-generalisation this document faults elsewhere. +A detector that matches comments is not a detector for a *keyword* defect. + +`postulate` is **not an Idris2 keyword** (v0.7.0 answers `Couldn't parse declaration`; +absent from the changelog for v0.2.0–v0.8.0). In declaration position it makes the entire +file unparseable. So **42 tracked `.idr` files do not parse on `origin/main` today**, and +the cure for every one of them exists *only* in the uncommitted working tree. + +Controlled pair, same file, same compiler, same flags — `src/Proven/SafeRegex/Proofs.idr`: + +[cols="2,3"] +|=== +| pristine `origin/main` | `Error: Couldn't parse declaration` at 25:1 → **rc=1** +| cured working tree | **rc=0, 0 errors** +|=== + +[WARNING] +==== +**The reported error location lies.** Idris2 reports the span of the *docstring* (line 25), +not the `postulate` line that actually fails, because a `|||` block attaches to the +declaration that follows it. Anyone who greps the reported line finds well-formed prose and +concludes the report is spurious. +==== + +**Therefore:** never `git checkout -- .`, `git stash`, or `git clean` in this repo. The +disposition of those 245 files is an owner decision (ruling R-13, triage report first), and +until it is made they must be left exactly as found. + +=== 2.1 Five files are on disk but not in git + +Commit `f2833c2c` — titled *"feat: add ECHIDNA validation modules"*, author string `Test` — +**deleted 149 files, 22 of them `.idr` sources**. Seventeen were later restored *and +re-tracked*. Five were restored to the working tree but **never re-added to git**: + +* `src/Proven/SafeRegex/Matcher.idr` +* `src/Proven/SafeRegex/Parser.idr` — re-tracked by PR #206 +* `src/Proven/SafeSQL/Builder.idr` +* `src/Proven/SafeXML/Parser.idr` +* `src/Proven/SafeYAML/Parser.idr` + +All five are confirmed **absent** from a pristine `origin/main` tree. + +`Proven.FFI.SafeRegex` *is* listed at `proven.ipkg:309` and imports +`Proven.SafeRegex.Parser` at line 22 — so the local build reaches these files transitively +and compiles them, while a clean checkout does not contain them at all. +**The local build and the CI build have been building different source trees, and nothing +reported that.** + +This also explains a second defect: the `Char` → `SingleChar` constructor rename reached +`Types.idr`, `Safety.idr`, `Proofs.idr` and `SafeArgs/Proofs.idr` — and **missed +`Parser.idr`, the one file outside git's view**. A sweep that walks tracked files cannot +reach an untracked one, so untracked files silently accumulate rename debt. + +[TIP] +==== +**Detector worth building:** for every module named in an `.ipkg`, and every module +transitively imported by one, assert the source file is present in `HEAD`. +*Untracked-but-built* is a distinct failure class from *missing-from-ipkg*, and no existing +check sees it. +==== + +[[matcher]] +== 3. The next blocker, fully diagnosed + +`src/Proven/SafeRegex/Matcher.idr` at frontier `211/305`. It reports 16 errors; six are +roots. It is also one of the five untracked files above, so **re-add it to git as part of +the fix**. + +.... +BUILD_RC=1 +frontier: 211/305: Building Proven.SafeRegex.Matcher +errors: 16 shadow: 0 +Error: While processing right hand side of matchCharClass. Undefined name matchesClassWithFlags. +Error: While processing right hand side of matchesClassWithFlags. When unifying: ... +Error: ... Undefined name Proven.SafeRegex.Matcher.5468:5311:matchQuantified. +Error: findAll is not total, possibly not terminating due to call to ...findFrom +Error: findFirst is not total, possibly not terminating due to call to ...findFrom +Error: match is not total, possibly not terminating due to call to ...findFirst +.... + +[cols="1,2,4"] +|=== +| Line | Class | What to do + +| 133 | <> | `Char x =>` where the constructor is `SingleChar`. Reports `When unifying: Type and ?argTy -> CharClass`, **never** `Undefined name`. +| 127 | <> | `Undefined name matchesClassWithFlags` — it is defined at 130–131, *below* the use. Hoist the **signature only**, then delete the late signature. +| ~237 | <> | `where`-block scope around `matchQuantified` (mangled `Proven.SafeRegex.Matcher.5468:5311:matchQuantified`). Hoist to top level. +| — | <> | Three totality failures: `findAll` → `findFrom`, `findFirst` → `findFrom`, `match` → `findFirst`. Derive a `Nat` bound and recurse structurally on it. +|=== + +The relevant source, as it stands: + +[source,idris] +---- + 123 | case currentChar st of + 124 | Nothing => False + 125 | Just c => + 126 | let c' = if st.flags.caseInsensitive then toLower c else c + 127 | in matchesClassWithFlags c' cls st.flags -- forward reference + 129 | ||| Match character class with flags + 130 | matchesClassWithFlags : Char -> CharClass -> RegexFlags -> Bool + 131 | matchesClassWithFlags c cls flags = + 132 | case cls of + 133 | Char x => -- should be SingleChar +---- + +And the constructor it should be using, from `src/Proven/SafeRegex/Types.idr`: + +[source,idris] +---- +data CharClass : Type where + SingleChar : Char -> CharClass -- line 24 — NOT `Char` + Range : (from : Char) -> (to : Char) -> CharClass + Digit | Word | Space | Any : CharClass + Negate : CharClass -> CharClass + Union : CharClass -> CharClass -> CharClass +---- + +== 4. Blocker classes encountered + +Numbering is continuous with the estate-wide register. Only the classes met in `proven` +are reproduced here. + +[[c13]] +=== Class 13 — `where`-block ordering +A `where`-bound name must be defined before it is used within the block. + +[[c27]] +=== Class 27 — `Int` vs `Nat` in string primitives +`strSubstr : Int -> ...` against `String.length : ... -> Nat`. Convert explicitly. + +[[c28]] +=== Class 28 — top-level forward reference +Idris2 elaborates a module top-to-bottom. **Cure:** hoist the *signature only* above the +first use, then **delete the later signature** — leaving both is a duplicate-definition +error. + +[[c29]] +=== Class 29 — a `|||` docstring cannot attach to a `mutual` block +Move the docstring inside, onto a member. + +[[c30]] +=== Class 30 — recursion on a non-inductive numeric type +Idris2's termination checker needs a structurally decreasing argument. `Int`, `Integer` and +`Double` have none. **Cure:** derive a `Nat` bound (typically `length` of the input) and +recurse structurally on that. **Never** reach for a totality escape hatch. + +[[c31]] +=== Class 31 — a `where`-local wrapper that shadows the Prelude name it calls +A local `toLower` that calls `toLower` recurses into itself. **Cure:** rename the local. + +[WARNING] +==== +`grep -c 'is shadowing'` returns **0** on the very build reporting these. The shadow +counter does not see `where`-local bindings that shadow imported names — see <>. +==== + +[[c32]] +=== Class 32 — a `where` block attaches to ONE clause, not the whole function +In a multi-clause definition, a `where` block is visible only to the clause it follows. +Other clauses report `Undefined name`, and the name is *mangled* with source offsets +(`Module.5468:5311:name`), which is the diagnostic tell. **Cure: hoist to top level.** + +[[c33]] +=== Class 33 — a body written in a FOREIGN proof assistant's tactic language +Lean 4 syntax inside an Idris2 file: comma-list `unfold`, `simp [prf]`, `;`-sequenced +tactics, lowercase `rfl`. **Diagnostic:** the error points at a keyword *mid-line* in a +proof body. Frequently carries an arity bug as well. **Cure:** write the proof properly. + +[[c34]] +=== Class 34 — a top-level constant of a RECORD type is opaque to the unifier +Idris2 0.7.0 will not reduce a top-level constant whose type is a record. +**Control that compiles**, proving the problem is record-specific: + +[source,idris] +---- +n : Nat +n = 5 +tn : n = 5 +tn = Refl -- compiles +---- + +**Cure:** generalise over the record *value* and case-split on its constructor. + +[[c35]] +=== Class 35 — `Ord Nat`'s `<=` is NOT `Data.Nat.lte` +`p <= 65535` elaborates to `not (compare p 65535 == GT)`, whereas `lteReflectsLTE` consumes +`lte p 65535`. The two are **propositionally equal but not convertible**, so the stdlib +lemma will not apply. **Cure:** restate the hypothesis over the relation the lemma actually +consumes. + +[[c36]] +=== Class 36 — a rename that silently retargets to a Prelude name of a DIFFERENT KIND +The constructor is `SingleChar : Char -> CharClass`, but the file still writes `Char '\n'`. +`Char` *is* in scope — as the **builtin type** — so it resolves, and the error is +`Mismatch between: Type and Char -> CharClass`. It is **never** `Undefined name Char`. + +**Every existing detector misses this**: the identifier is spelled correctly and is in +scope; only its *kind* is wrong. + +Safe rewrite patterns: + +[source,bash] +---- +sed -i "s/(Char '/(SingleChar '/g; s/(Char c/(SingleChar c/g" "$F" +---- + +[CAUTION] +`(Char ` alone is **unsafe** — it also matches type positions such as +`satisfy : (Char -> Bool) -> Parser Char`. Always verify both the presence of the new form +and the absence of the old. + +[[c37]] +=== Class 37 — a `let`-bound record update cannot infer its type + +[source,idris] +---- +let st' = { input := rest, pos := S st.pos } st -- Can't infer type for this record update +let st' : ParserState = { input := rest, pos := S st.pos } st -- compiles +---- + +**Mechanism:** Idris2 resolves record-update field names from the **expected type, working +downward** — not from the type of the subject expression. Field names are ambiguous across +records, so it cannot work upward. Every *other* record update in the file compiled because +it sat inside `Right (x, { ... } st)`, where the tuple's second component is pinned by the +return type. **A bare `let` with no annotation is the one syntactic position that supplies +no expected type.** Exactly 1 of ~20 record updates in the file failed. + +Generalises to ambiguous record *projection* and to interface-method resolution. + +== 5. The cure discipline + +[IMPORTANT] +==== +**Defunctionalise, restructure, or prove properly. Never assert.** + +Census the file's trusted-base marker tokens *before* choosing a cure, and again after. +The whole campaign added **zero**. `SafeRegex/Parser.idr` was and remains 0/0/0/0. +==== + +=== 5.1 Fuel: keep it internal where the recursion is local + +When a function's recursion is confined to its own body, derive the fuel *inside* the body +from `length st.input` — the **public signature does not change** and the blast radius is +zero. Only a `mutual` block whose recursion crosses function boundaries needs an explicit +`Nat` parameter threaded through every member. + +In `SafeRegex/Parser.idr`: `many` and `parseClassContents` took internal fuel; the six-member +mutual block took an explicit `Nat`, and the entry points seed it with +`16 * length (unpack pattern) + 16`. The whole mutual block is private, so no public +signature moved. + +Totality then holds by construction: every intra-group call passes `k` where the clause +matched `S k`, so all members decrease strictly on argument 1. + +=== 5.2 `DISCHARGED` in a docstring is an unverified assertion + +There are **67** `DISCHARGED` docstring lines across **23** files in `src/`. Five were +written during this campaign and each was verified rc=0. **Sixty-two are pre-existing and +have never been verified.** Twenty of the 23 files carry **both** `DISCHARGED` and `OWED`. + +Four of the 62 were confirmed **false** — and all four were found by *compiling*, not by +reading. + +**The compiler is the only witness. The build is the audit instrument.** + +== 6. Harness traps + +These cost real time. Each is stated with the limit of what it was observed to do. + +[[t1]] +=== Trap 1 — a backgrounded launcher reports the LAUNCHER's exit code +A task notification saying *"completed (exit code 0)"* refers to the wrapper script, not to +`idris2`. This has falsely reported success **seven times** in this campaign. + +**Always** `grep '^BUILD_RC=' `. Never read the notification's exit code. + +=== Trap 2 — inside perl's `\Q...\E`, `\n` is quoted as a literal backslash-n +Prefer file reconstruction over in-place regex for multi-line edits: + +[source,bash] +---- +{ sed -n '1,Np' f; new-block; sed -n 'M,$p' f; } > tmp && mv tmp f +---- + +Then verify **both** the presence of the new text and the absence of the old. + +=== Trap 3 — standalone checks need `-p contrib` +[source,bash] +---- +idris2 -p contrib --source-dir src --check src/Proven/.idr # correct +---- +Never `--find-ipkg`. Without `-p contrib`, `Module Data.List.Equalities not found` +**masks the real error** and you debug the wrong thing. + +=== Trap 4 — idris2 progress output is block-buffered without a PTY +Polling the log mid-run returns nothing. **This is not a hang.** + +=== Trap 5 — `pgrep -f ` self-matches +The `pgrep` process's own command line contains the pattern, so it always finds itself. +Use **`pgrep -x idris2`**. + +This is the bounded-observation fallacy *inverted*: a non-null result mistaken for presence. +An empty-result control cannot catch it. + +[[shadow]] +=== Trap 6 — the shadow counter's reach is narrower than it looks +`grep -c 'is shadowing'` fires on implicitly-bound lowercase names in bodyless erased +`0 name : Type` declarations. It does **not** fire on `where`-local bindings that shadow +imported names (class 31). Quote both limits whenever quoting `shadow: N`. + +Readings this campaign: `5` @198, `3` @203, `55` @210, `0` @211. + +== 7. Git traps and techniques + +=== 7.1 `git branch -f` refuses on a branch checked out in a worktree +It fails *quietly enough* that later commands in the same compound shell line silently +describe the **old** branch. Verify against the **commit SHA**, never the branch name. + +=== 7.2 Rebase without touching a dirty worktree, via a temporary index +Needed here because the worktree holds 245 dirty files that must not move. This constructs +the commit entirely in git's object database: + +[source,bash] +---- +export GIT_INDEX_FILE="$T/tmpidx" +rm -f "$GIT_INDEX_FILE" +git read-tree origin/main +for f in ; do + sha=$(git rev-parse "$SRC:$f") + mode=$(git ls-tree "$SRC" -- "$f" | awk '{print $1}') + git update-index --add --cacheinfo "$mode,$sha,$f" +done +TREE=$(git write-tree) +NEW=$(git commit-tree "$TREE" -p origin/main -F "$T/commitmsg.txt") +unset GIT_INDEX_FILE +---- + +The dirty count stayed at 245 throughout. + +=== 7.3 Check your PR base before opening it +[source,bash] +---- +git rev-list --left-right --count origin/main...HEAD +---- +The local branch `fix/idris2-totality-and-elaboration-cures` sits on top of nine unrelated +CI commits, one of which bumps reusable-workflow pins to **`5b1d0022`** — a SHA already +recorded estate-wide as **phantom** and fixed across 15 repos. PR-ing that branch against +`main` would have re-introduced a known-bad pin under a new author. + +=== 7.4 A pristine tree without a clone +[source,bash] +---- +git archive origin/main | tar -x -C "$TMP/clean" +---- +No network, no `.git`, seconds rather than minutes. This is how the <> measurement +was taken. + +== 8. Reproducing the measurements + +Full build: + +[source,bash] +---- +#!/bin/bash +cd /path/to/proven +RAW=$T/build.raw +timeout 2700 idris2 --build-dir bd --build proven.ipkg > "$RAW" 2>&1 +RC=$? +{ + echo "BUILD_RC=$RC" + echo "frontier: $(grep -oE '^[0-9]+/[0-9]+: Building [A-Za-z0-9._]+' "$RAW" | tail -1)" + echo "errors: $(grep -c '^Error:' "$RAW") shadow: $(grep -c 'is shadowing' "$RAW")" + grep -n '^Error:' "$RAW" | head -6 +} > $T/build.log +---- + +Single module: + +[source,bash] +---- +timeout 900 idris2 -p contrib --source-dir src --check src/Proven/.idr +---- + +[NOTE] +`--build-dir bd` creates `bd/` inside the repo. It has not appeared in `git status`, but +check before staging — and **never** `git add -A` in this repo while the 245 files are +undisposed. + +== 9. Known-defective gates in this repo + +`.github/workflows/e2e.yml` — the marker gate is **well built**: it excludes lines whose +first non-whitespace is `|||` or `--` before failing, so doc-comment mentions do not +false-positive. Keep it. + +`.github/workflows/trustfile.yml` — *"Check believe_me audit trail"* **cannot fail**. It +computes `UNJUSTIFIED` from a pipeline that re-greps its own `-B1` context for the pattern +itself, discarding the justification check; the variable is then never read; and the only +branch prints `WARNING` above a threshold of 300 without ever calling `exit 1`. +**A gate that cannot fail is as defective as one that cannot pass.** + +Neither gate covers `assert_smaller`, top-level `partial`, or bodyless erased +`0 name : Type` declarations — which is where the repository's actual proof debt lives. diff --git a/src/Proven/SafeCSP.idr b/src/Proven/SafeCSP.idr index ab8b54af..2e53a3c3 100644 --- a/src/Proven/SafeCSP.idr +++ b/src/Proven/SafeCSP.idr @@ -88,6 +88,16 @@ data Directive = | ReportUri String | ReportTo String +||| Render a list of CSP sources as a space-separated header fragment. +||| +||| Hoisted to top level 2026-08-27. It was previously a `where` block written +||| after the LAST clause of `renderDirective`, so it was in scope for that one +||| clause only and the other 15 clauses could not see it -- a `where` attaches +||| to a single clause, never to a whole multi-clause function. +public export +renderSources : List Source -> String +renderSources srcs = fastConcat (intersperse " " (map show srcs)) + ||| Render a directive to its header string fragment public export renderDirective : Directive -> String @@ -110,9 +120,6 @@ renderDirective UpgradeInsecureRequests = "upgrade-insecure-requests" renderDirective BlockAllMixedContent = "block-all-mixed-content" renderDirective (ReportUri uri) = "report-uri " ++ uri renderDirective (ReportTo group) = "report-to " ++ group - where - renderSources : List Source -> String - renderSources srcs = fastConcat (intersperse " " (map show srcs)) -- ============================================================================ -- CSP POLICY diff --git a/src/Proven/SafeCrypto/Proofs.idr b/src/Proven/SafeCrypto/Proofs.idr index 3d9e46f8..0fbad4ee 100644 --- a/src/Proven/SafeCrypto/Proofs.idr +++ b/src/Proven/SafeCrypto/Proofs.idr @@ -55,7 +55,7 @@ import Data.Vect ||| (FFI-opaque Bits primitives). Discharge once a `Data.Bits` ||| reflective tactic / Prelude lemma is available. public export -postulate 0 constantTimeRefl : (d : ByteVector n) -> digestEq d d = True +0 constantTimeRefl : (d : ByteVector n) -> digestEq d d = True ||| OWED: constant-time `digestEq` is symmetric — ||| `digestEq d1 d2 = digestEq d2 d1`. Reduces to showing that @@ -66,7 +66,7 @@ postulate 0 constantTimeRefl : (d : ByteVector n) -> digestEq d d = True ||| stdlib). Same blocker family as `constantTimeRefl`. Discharge ||| once `Data.Bits` exposes `xorCommutative : (x, y : Bits8) -> x \`xor\` y = y \`xor\` x`. public export -postulate 0 constantTimeSym : (d1, d2 : ByteVector n) -> +0 constantTimeSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1 -------------------------------------------------------------------------------- @@ -122,31 +122,53 @@ public export sha1NotSecure : isSecure SHA1_ALG = False sha1NotSecure = Refl -||| OWED: any algorithm whose `securityLevel` is `Modern` is `isSecure`. -||| `isSecure` is defined as a `case securityLevel alg of` with a -||| wildcard `_ => True` arm covering `Modern` (and `Standard`). With -||| the hypothesis `securityLevel alg = Modern` in scope we need to -||| rewrite the scrutinee under the `case`, but Idris2 0.8.0 will not -||| reduce `isSecure alg` for an abstract `alg : HashAlg` even after -||| `rewrite` substitutes `securityLevel alg`, because the `case` was -||| not eta-expanded to a generalised motive at elaboration time. -||| Discharge by either (a) refactoring `isSecure` to a top-level -||| pattern-match dispatch on `securityLevel`, or (b) hand-proving via -||| `with (securityLevel alg) proof prf` once the 0.8.0 `with`/`rewrite` -||| interaction is improved. +||| Any algorithm whose `securityLevel` is `Modern` is `isSecure`. +||| +||| DISCHARGED 2026-08-27 by case-split on the finite `HashAlg` enum. +||| `securityLevel` is a top-level pattern match over 11 constructors, so +||| for every CONCRETE `alg` both it and `isSecure` reduce and `Refl` +||| closes the goal. The six non-`Modern` constructors are refuted by the +||| hypothesis itself, not assumed away. +||| +||| Supersedes an earlier note claiming `isSecure alg` could not be +||| reduced. That is true only while `alg` is ABSTRACT -- and `alg` does +||| not have to stay abstract. No change to the public API was needed. public export modernIsSecure : (alg : HashAlg) -> securityLevel alg = Modern -> isSecure alg = True -modernIsSecure prf = unfold isSecure; rewrite prf; rfl - -||| OWED: any algorithm whose `securityLevel` is `Standard` is -||| `isSecure`. Same shape as `modernIsSecure`. +modernIsSecure MD5_ALG Refl impossible +modernIsSecure SHA1_ALG Refl impossible +modernIsSecure SHA224_ALG Refl impossible +modernIsSecure SHA256_ALG Refl impossible +modernIsSecure SHA384_ALG Refl impossible +modernIsSecure SHA512_ALG Refl impossible +modernIsSecure SHA3_256_ALG _ = Refl +modernIsSecure SHA3_512_ALG _ = Refl +modernIsSecure BLAKE2b_ALG _ = Refl +modernIsSecure BLAKE2s_ALG _ = Refl +modernIsSecure BLAKE3_ALG _ = Refl + +||| Any algorithm whose `securityLevel` is `Standard` is `isSecure`. +||| +||| DISCHARGED 2026-08-27. Same shape as `modernIsSecure`: the four SHA-2 +||| constructors reduce to `True`; the other seven are refuted by the +||| hypothesis. public export standardIsSecure : (alg : HashAlg) -> securityLevel alg = Standard -> isSecure alg = True -standardIsSecure prf = unfold isSecure; rewrite prf; rfl +standardIsSecure MD5_ALG Refl impossible +standardIsSecure SHA1_ALG Refl impossible +standardIsSecure SHA3_256_ALG Refl impossible +standardIsSecure SHA3_512_ALG Refl impossible +standardIsSecure BLAKE2b_ALG Refl impossible +standardIsSecure BLAKE2s_ALG Refl impossible +standardIsSecure BLAKE3_ALG Refl impossible +standardIsSecure SHA224_ALG _ = Refl +standardIsSecure SHA256_ALG _ = Refl +standardIsSecure SHA384_ALG _ = Refl +standardIsSecure SHA512_ALG _ = Refl -------------------------------------------------------------------------------- -- Digest Comparison Properties @@ -158,13 +180,13 @@ standardIsSecure prf = unfold isSecure; rewrite prf; rfl ||| and inherits the same `Data.Bits` `xor x x = 0` reductive blocker. ||| Discharge together with `constantTimeRefl`. public export -postulate 0 digestEqRefl : (d : ByteVector n) -> digestEq d d = True +0 digestEqRefl : (d : ByteVector n) -> digestEq d d = True ||| OWED: digest equality is symmetric — `digestEq d1 d2 = digestEq d2 d1`. ||| Same claim as `constantTimeSym` above; same `Data.Bits` `xor` ||| commutativity blocker. Discharge together with `constantTimeSym`. public export -postulate 0 digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1 +0 digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1 ||| OWED: distinct `ByteVector`s compare unequal under `digestEq`. ||| Stated with `Not (d1 = d2)` (propositional inequality) because @@ -176,7 +198,7 @@ postulate 0 digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d ||| Discharge once `Data.Bits` exposes the cancellation lemma OR once ||| `digestEq` is refactored to recurse via `decEq` element-wise. public export -postulate 0 differentDigestsUnequal : (d1, d2 : ByteVector n) -> +0 differentDigestsUnequal : (d1, d2 : ByteVector n) -> Not (d1 = d2) -> digestEq d1 d2 = False @@ -198,7 +220,7 @@ postulate 0 differentDigestsUnequal : (d1, d2 : ByteVector n) -> ||| index, or (b) refactoring the return type so the length witness ||| is exposed without case-pattern reduction. public export -postulate 0 randomBytesLength : (n : Nat) -> +0 randomBytesLength : (n : Nat) -> case randomBytes n of Right (MkByteVec v) => length v = n Left _ => () @@ -213,7 +235,7 @@ postulate 0 randomBytesLength : (n : Nat) -> ||| modelled propositionally and `modLT : (a, b : Nat) -> IsSucc b -> LT (a \`mod\` b) b` ||| is available in `Data.Nat`. public export -postulate 0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} -> +0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} -> case randomNat max of Right n => LT n max Left _ => () @@ -225,7 +247,7 @@ postulate 0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} -> ||| reasoning. Same FFI + `Data.Nat` blocker family. Discharge ||| together with `randomNatBounded`. public export -postulate 0 randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} -> +0 randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} -> case randomNatRange mn mx of Right n => (LTE mn n, LTE n mx) Left _ => () @@ -245,7 +267,7 @@ postulate 0 randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} -> ||| `Not (c1 = c2)` for 0.8.0 (`/=` returns `Bool`). Discharge once ||| `Data.Bits` exposes the requisite cast/shift round-trip lemmas. public export -postulate 0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) -> +0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) -> Not (c1 = c2) -> Not (counterNonce pfx c1 = counterNonce pfx c2) @@ -254,7 +276,7 @@ postulate 0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) -> ||| `randomBytesLength` lifted through the rename. Same FFI entropy ||| opacity blocker; discharge together with `randomBytesLength`. public export -postulate 0 freshNonceSize : (n : Nat) -> +0 freshNonceSize : (n : Nat) -> case freshNonce n of Right (MkByteVec v) => length v = n Left _ => () @@ -275,7 +297,7 @@ postulate 0 freshNonceSize : (n : Nat) -> ||| once a `String`-FFI reflective tactic or pack/unpack length ||| lemma is available. public export -postulate 0 tokenLengthApprox : (bytes : Nat) -> +0 tokenLengthApprox : (bytes : Nat) -> case randomToken bytes of Right s => LTE (length s) ((bytes * 4 `div` 3) + 3) Left _ => () @@ -289,7 +311,7 @@ postulate 0 tokenLengthApprox : (bytes : Nat) -> ||| opacity blocker as `tokenLengthApprox`. Discharge together with ||| `tokenLengthApprox` once the pack/unpack length lemma lands. public export -postulate 0 uuidLength : case randomUUID of +0 uuidLength : case randomUUID of Right s => length s = 36 Left _ => () @@ -331,5 +353,5 @@ hexEncodeDeterministic _ _ = Refl ||| concrete `bytesToHex`, AND (b) the `String`-FFI reflective ||| tactic / pack-length lemma. public export -postulate 0 hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) -> +0 hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) -> mod (length (bytesToHex bs)) 2 = 0 diff --git a/src/Proven/SafeEmail/Proofs.idr b/src/Proven/SafeEmail/Proofs.idr index 4a2f747a..31a27335 100644 --- a/src/Proven/SafeEmail/Proofs.idr +++ b/src/Proven/SafeEmail/Proofs.idr @@ -58,7 +58,7 @@ parseDeterministic s = Refl ||| Discharge once a `Data.String` reflective tactic is available, ||| or once `splitOnLast` is reformulated on `List Char` so its ||| reduction does not pass through `unpack`. -postulate 0 parseNoAtFails : parseEmail "noatsign" = Nothing +0 parseNoAtFails : parseEmail "noatsign" = Nothing -------------------------------------------------------------------------------- -- Validation Properties @@ -78,34 +78,54 @@ postulate 0 parseNoAtFails : parseEmail "noatsign" = Nothing ||| record-projection reduction" comment was incorrect — it did not ||| type-check under Idris2 0.8.0.) public export -postulate 0 validResultIsValid : validResult.isValid = True - -||| OWED: adding an Error-severity issue makes the result invalid. -||| `addIssue` (Validation.idr L71-74) computes the new validity as -||| `result.isValid && issue.severity /= Error`; given -||| `issue.severity = Error` we have `Error /= Error = False`, so the -||| conjunction collapses to `False` for any starting `result`. Held -||| back by Idris2 0.8.0's user-defined `Eq ValidationSeverity` -||| instance (Validation.idr L28-32): equality on the three-arm -||| `data ValidationSeverity = Error | Warning | Info` does not -||| reduce under `(/=)` by Refl alone because `(/=)` is implemented -||| as `not . (==)` and `not (Error == Error)` requires unfolding -||| both the user-written `Eq` instance and `not`. Same family as -||| boj-server SafetyLemmas' enum-equality reflection gap. Discharge -||| with a `Bool`-vs-`Prop` reflective lemma `(==) Error Error = True` -||| DISCHARGED: Error severity → False via Not (Error = Error) → False. +0 validResultIsValid : validResult.isValid = True + +||| Adding an `Error`-severity issue makes ANY result invalid. +||| +||| DISCHARGED 2026-08-27, and GENERALISED. The lemma previously spoke +||| only about `validResult`; it now holds for every starting +||| `ValidationResult`, which is strictly stronger and -- unlike the +||| `validResult` form -- actually provable. See WHY NOT below. +||| +||| Proof: case-split the starting result to expose its `isValid` field. +||| When that field is `False`, `addIssue`'s conjunction is `False` +||| outright. When it is `True`, the conjunction collapses to +||| `issue.severity /= Error`, and rewriting by the hypothesis lets the +||| user-written `Eq ValidationSeverity` instance and `not` unfold. +||| +||| WHY NOT `validResult`: a top-level constant of a RECORD type is +||| opaque to the Idris2 0.7.0 unifier. Minimal reproduction -- for +||| `r : Rec; r = MkRec True []`, neither `r.isValid = True` nor +||| `r = MkRec True []` is provable by `Refl`; neither `%inline` nor the +||| `isValid r` projection form changes it; only a direct constructor +||| application such as `(MkRec True []).isValid` reduces. The same +||| constant at type `Nat` reduces normally, so the opacity is specific +||| to record-typed constants. +||| +||| That reproduced fact supersedes an earlier note attributing the +||| blockage to the enum-equality reflection gap. The `rewrite` above +||| clears that gap; the record constant was always the real obstacle. public export errorMakesInvalid : (issue : ValidationIssue) -> + (result : ValidationResult) -> issue.severity = Error -> - (addIssue issue validResult).isValid = False -errorMakesInvalid _ prf = unfold addIssue, validResult; simp [prf]; rfl + (addIssue issue result).isValid = False +errorMakesInvalid issue (MkValidationResult True _) prf = rewrite prf in Refl +errorMakesInvalid issue (MkValidationResult False _) _ = Refl -||| DISCHARGED: Warning severity ≠ Error, so True && True = True. +||| Adding a `Warning`-severity issue leaves ANY result's validity alone. +||| +||| DISCHARGED 2026-08-27, generalised the same way as +||| `errorMakesInvalid`. `Warning == Error` takes the `Eq` instance's +||| catch-all arm to `False`, so `not False = True` and the starting +||| result's own validity is returned unchanged. public export warningKeepsValid : (issue : ValidationIssue) -> + (result : ValidationResult) -> issue.severity = Warning -> - (addIssue issue validResult).isValid = True -warningKeepsValid _ prf = unfold addIssue, validResult; simp [prf]; rfl + (addIssue issue result).isValid = result.isValid +warningKeepsValid issue (MkValidationResult True _) prf = rewrite prf in Refl +warningKeepsValid issue (MkValidationResult False _) _ = Refl ||| DISCHARGED: combining two valid results yields a valid result. ||| The OWED comment suggested the discharge pattern: case-split on @@ -126,7 +146,7 @@ combineValidValid (MkValidationResult True _) (MkValidationResult True _) Refl R ||| Parsed email always contains @ public export data ContainsAt : String -> Type where - postulate MkContainsAt : (s : String) -> (prf : '@' `elem` unpack s = True) -> ContainsAt s + MkContainsAt : (s : String) -> (prf : '@' `elem` unpack s = True) -> ContainsAt s ||| OWED: if `parseEmail s` succeeds (`isJust (parseEmail s) = True`), ||| the input string contains `'@'` (`'@' `elem` unpack s = True`). @@ -140,22 +160,22 @@ data ContainsAt : String -> Type where ||| String FFI is reflectively modelled, or once `splitOnLast` is ||| factored through `List Char` with a structural lemma ||| `splitOnLastJust : splitOnLast c s = Just _ -> c `elem` unpack s = True`. -postulate 0 parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s +0 parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s ||| Local part length bound public export data ValidLocalLength : String -> Type where - postulate MkValidLocalLength : (local : String) -> LTE (length local) 64 -> ValidLocalLength local + MkValidLocalLength : (local : String) -> LTE (length local) 64 -> ValidLocalLength local ||| Domain length bound public export data ValidDomainLength : String -> Type where - postulate MkValidDomainLength : (domain : String) -> LTE (length domain) 253 -> ValidDomainLength domain + MkValidDomainLength : (domain : String) -> LTE (length domain) 253 -> ValidDomainLength domain ||| Total email length bound public export data ValidTotalLength : String -> Type where - postulate MkValidTotalLength : (email : String) -> LTE (length email) 254 -> ValidTotalLength email + MkValidTotalLength : (email : String) -> LTE (length email) 254 -> ValidTotalLength email -------------------------------------------------------------------------------- -- Normalization Properties @@ -173,7 +193,7 @@ data ValidTotalLength : String -> Type where ||| character-level lemma `Data.Char.toLowerIdempotent` lifted ||| through `pack . map toLower . unpack` (which still requires ||| reducing through `unpack` / `pack`). -postulate 0 normalizeIdempotent : (email : ParsedEmail) -> +0 normalizeIdempotent : (email : ParsedEmail) -> toLower email.domain = toLower (toLower email.domain) ||| Normalized emails with same local and domain are equal (trivial @@ -193,7 +213,7 @@ normalizedEquality e1 e2 _ prf = prf ||| Sanitized string contains no newlines public export data NoNewlines : String -> Type where - postulate MkNoNewlines : (s : String) -> + MkNoNewlines : (s : String) -> all (\c => c /= '\n' && c /= '\r') (unpack s) = True -> NoNewlines s @@ -217,7 +237,7 @@ sanitizeForHeader str = pack (filter isHeaderSafe (unpack str)) ||| `Bool` reduction. Same family as SafeHtml's filter-correctness ||| OWED. Discharge with a hand-written `filterAll` lemma or with a ||| reflective `Bool` tactic. -postulate 0 sanitizeRemovesNewlinesLemma : (s : String) -> +0 sanitizeRemovesNewlinesLemma : (s : String) -> all (\c => c /= '\n' && c /= '\r') (filter (\c => c /= '\n' && c /= '\r' && c /= '\0') (unpack s)) = True @@ -234,7 +254,7 @@ postulate 0 sanitizeRemovesNewlinesLemma : (s : String) -> ||| (2) the upstream `sanitizeRemovesNewlinesLemma` is itself OWED. ||| Discharge once both are discharged. public export -postulate 0 sanitizeRemovesNewlines : (s : String) -> +0 sanitizeRemovesNewlines : (s : String) -> NoNewlines (sanitizeForHeader s) -------------------------------------------------------------------------------- @@ -253,7 +273,7 @@ postulate 0 sanitizeRemovesNewlines : (s : String) -> ||| with `(::)`). Discharge with a hand-written ||| `filterAllSelf : (xs : List a) -> all p (filter p xs) = True` ||| lemma in `Data.List`, or via the reflective `Bool` tactic. -postulate 0 filterValidCorrect : (emails : List String) -> +0 filterValidCorrect : (emails : List String) -> all (\e => (validateEmailFull e).isValid) (filterValid emails) = True uniqueEmails : List ParsedEmail -> List ParsedEmail @@ -271,7 +291,7 @@ uniqueEmails = nubBy (\e1, e2 => toLower (e1.localPart ++ "@" ++ e1.domain) == ||| boj-server `Data.List` length-monotonicity OWED set. Discharge ||| by adding the missing lemma to `Data.List`, or by extending ||| `Data.List.Lemmas` (contrib) with it. -postulate 0 uniqueNoDuplicates : (emails : List ParsedEmail) -> +0 uniqueNoDuplicates : (emails : List ParsedEmail) -> LTE (length (uniqueEmails emails)) (length emails) -------------------------------------------------------------------------------- @@ -290,7 +310,7 @@ postulate 0 uniqueNoDuplicates : (emails : List ParsedEmail) -> ||| as SafeTOML's `isScalarCorrect` Bool-LEM gap. Discharge with a ||| one-line case-split on `isFreeEmail domain`. public export -postulate 0 freeEmailExhaustive : (domain : String) -> +0 freeEmailExhaustive : (domain : String) -> Either (isFreeEmail domain = True) (isFreeEmail domain = False) ||| OWED: `checkCommonTypos "gmial.com"` returns the @@ -305,7 +325,7 @@ postulate 0 freeEmailExhaustive : (domain : String) -> ||| `normalizeIdempotent` and `parseNoAtFails`. Discharge once the ||| String FFI is reflectively modelled, or by refactoring ||| `checkCommonTypos` to operate on `List Char`. -postulate 0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue +0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue (MkValidationIssue Warning "W010" "Possible typo - did you mean gmail.com?") validResult @@ -325,7 +345,7 @@ postulate 0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue ||| by the `addIssue` Bool-reduction gap shared with ||| `errorMakesInvalid`. Same family as `parseNoAtFails`. Discharge ||| once the String FFI is reflectively modelled. -postulate 0 validLocalNoStartDot : (local : String) -> +0 validLocalNoStartDot : (local : String) -> (validateLocalPart local).isValid = True -> isPrefixOf "." local = False @@ -335,7 +355,7 @@ postulate 0 validLocalNoStartDot : (local : String) -> ||| when `isSuffixOf "." local = True`. Held back by the same ||| String-FFI / Bool-reduction blockers; discharged in the same ||| stroke. -postulate 0 validLocalNoEndDot : (local : String) -> +0 validLocalNoEndDot : (local : String) -> (validateLocalPart local).isValid = True -> isSuffixOf "." local = False @@ -348,7 +368,7 @@ postulate 0 validLocalNoEndDot : (local : String) -> ||| `LTE 1 (length (forget xs))` as a Refl. Discharge with a ||| one-line case-split on the `List1` constructor (`x ::: xs` ||| gives length `S (length xs) >= S Z`). -postulate 0 validDomainHasLabel : (domain : String) -> +0 validDomainHasLabel : (domain : String) -> (validateDomain domain).isValid = True -> LTE 1 (length (forget (split (== '.') domain))) @@ -368,7 +388,7 @@ postulate 0 validDomainHasLabel : (domain : String) -> ||| `combineValidValid` plus the `foldl combineResults` invariant ||| (which `Data.List` does not expose as a Refl in Idris2 0.8.0). ||| Discharge alongside `combineValidValid`. -postulate 0 comprehensiveCatchesRFC : (s : String) -> +0 comprehensiveCatchesRFC : (s : String) -> (validateEmailFull s).isValid = False -> (validateComprehensive s).isValid = False @@ -387,6 +407,6 @@ postulate 0 comprehensiveCatchesRFC : (s : String) -> ||| `errorMakesInvalid`. Discharge alongside `errorMakesInvalid` + ||| `combineValidValid`, with one extra step-lemma per extra check ||| (each: "this check only emits non-Error issues"). -postulate 0 validPassesComprehensive : (s : String) -> +0 validPassesComprehensive : (s : String) -> (validateEmailFull s).isValid = True -> hasErrors (validateComprehensive s) = False diff --git a/src/Proven/SafeOTP.idr b/src/Proven/SafeOTP.idr index f8df409e..50b6ee14 100644 --- a/src/Proven/SafeOTP.idr +++ b/src/Proven/SafeOTP.idr @@ -166,12 +166,20 @@ public export validCounters : (unixTime : Integer) -> TOTPConfig -> List Integer validCounters unixTime config = let current = timeCounter unixTime config.period - skewInt = cast config.skew - in map (\offset => current + offset) - (rangeFrom (negate skewInt) skewInt) + in map (\offset => current + offset) (symRange config.skew) where - rangeFrom : Integer -> Integer -> List Integer - rangeFrom lo hi = if lo > hi then [] else lo :: rangeFrom (lo + 1) hi + -- Restructured 2026-08-27: the previous `rangeFrom : Integer -> Integer -> + -- List Integer` recursed on `lo + 1`, which the size-change principle cannot + -- see decreasing -- Integer carries no inductive structure. `config.skew` is + -- a Nat, and [-s .. s] has exactly 2s+1 elements, so counting down a Nat + -- fuel makes the descent structural. Totality is PROVED, not asserted. + countUp : Nat -> Integer -> List Integer + countUp Z _ = [] + countUp (S k) lo = lo :: countUp k (lo + 1) + + -- [-n .. n] as Integers: 2n+1 elements, the same list the old code produced. + symRange : Nat -> List Integer + symRange n = countUp (n + n + 1) (negate (cast n)) -- ============================================================================ -- VALIDATION (constant-time) @@ -224,15 +232,18 @@ totpProvisioningUri issuer account config = urlEncode : String -> String urlEncode = pack . concatMap encodeChar . unpack where + -- Idris2 requires definition-before-use inside `where` blocks exactly as + -- at top level, so these are ordered leaves-first: hexDigit, then toHex + -- (which calls it), then encodeChar (which calls toHex). + hexDigit : Int -> Char + hexDigit d = if d < 10 then chr (ord '0' + d) else chr (ord 'a' + d - 10) + toHex : Int -> String + toHex n = pack [hexDigit (n `div` 16), hexDigit (n `mod` 16)] encodeChar : Char -> List Char encodeChar ' ' = ['+'] encodeChar c = if isAlphaNum c || c == '-' || c == '_' || c == '.' then [c] else unpack ("%" ++ toHex (ord c)) - toHex : Int -> String - toHex n = pack [hexDigit (n `div` 16), hexDigit (n `mod` 16)] - hexDigit : Int -> Char - hexDigit d = if d < 10 then chr (ord '0' + d) else chr (ord 'a' + d - 10) ||| Generate an HOTP provisioning URI public export diff --git a/src/Proven/SafeRedirect.idr b/src/Proven/SafeRedirect.idr index 0421af22..bb56a8ce 100644 --- a/src/Proven/SafeRedirect.idr +++ b/src/Proven/SafeRedirect.idr @@ -43,12 +43,12 @@ isRelativeUrl : String -> Bool isRelativeUrl url = not (isInfixOf "://" url) && not (isPrefixOf "//" url) && - not (isPrefixOf "javascript:" (toLower url)) && - not (isPrefixOf "data:" (toLower url)) && - not (isPrefixOf "vbscript:" (toLower url)) + not (isPrefixOf "javascript:" (lowerStr url)) && + not (isPrefixOf "data:" (lowerStr url)) && + not (isPrefixOf "vbscript:" (lowerStr url)) where - toLower : String -> String - toLower = pack . map toLower . unpack + lowerStr : String -> String + lowerStr = pack . map toLower . unpack ||| Check if a URL starts with a safe path prefix public export @@ -78,10 +78,10 @@ isAllowedDomain allowedDomains url = Just host => any (\d => d == host || isSuffixOf ("." ++ d) host) allowedDomains where isSuffixOf : String -> String -> Bool - isSuffixOf suffix str = isPrefixOf (reverse suffix) (reverse str) + isSuffixOf suffix str = isPrefixOf (reverseStr suffix) (reverseStr str) where - reverse : String -> String - reverse = pack . reverse . unpack + reverseStr : String -> String + reverseStr = pack . reverse . unpack -- ============================================================================ -- REDIRECT VALIDATION diff --git a/src/Proven/SafeRegex/Parser.idr b/src/Proven/SafeRegex/Parser.idr new file mode 100644 index 00000000..60c363fb --- /dev/null +++ b/src/Proven/SafeRegex/Parser.idr @@ -0,0 +1,480 @@ +-- SPDX-License-Identifier: Palimpsest-MPL-1.0 +||| SafeRegex.Parser - Parse regex patterns from strings +||| +||| This module provides a safe regex parser that: +||| - Parses standard regex syntax (PCRE-like) +||| - Validates patterns during parsing +||| - Rejects patterns that would cause ReDoS +||| - Returns structured errors on invalid input +module Proven.SafeRegex.Parser + +import Proven.Core +import Proven.SafeRegex.Types +import Proven.SafeRegex.Safety +import Data.List +import Data.String +import Data.Maybe + +%default total + +-------------------------------------------------------------------------------- +-- Parser State +-------------------------------------------------------------------------------- + +||| Parser state +record ParserState where + constructor MkParserState + ||| Remaining input + input : List Char + ||| Current position (for error reporting) + pos : Nat + ||| Number of open groups + openGroups : Nat + ||| Next group ID to assign + nextGroupId : Nat + ||| Parsing flags + flags : RegexFlags + +||| Initial parser state +initState : String -> RegexFlags -> ParserState +initState s flags = MkParserState (unpack s) 0 0 1 flags + +||| Parser result +Parser : Type -> Type +Parser a = ParserState -> Either RegexError (a, ParserState) + +-------------------------------------------------------------------------------- +-- Parser Combinators +-------------------------------------------------------------------------------- + +||| Run a parser +runParser : Parser a -> ParserState -> Either RegexError (a, ParserState) +runParser p st = p st + +||| Pure value +pure : a -> Parser a +pure x st = Right (x, st) + +||| Map over parser result +map : (a -> b) -> Parser a -> Parser b +map f p st = case p st of + Left err => Left err + Right (x, st') => Right (f x, st') + +||| Sequence parsers +bind : Parser a -> (a -> Parser b) -> Parser b +bind p f st = case p st of + Left err => Left err + Right (x, st') => f x st' + +||| Fail with error +fail : RegexError -> Parser a +fail err _ = Left err + +||| Try a parser, return Nothing on failure +optional : Parser a -> Parser (Maybe a) +optional p st = case p st of + Left _ => Right (Nothing, st) + Right (x, st') => Right (Just x, st') + +||| Parse zero or more +many : Parser a -> Parser (List a) +many p st = go (length st.input) [] st + where + -- The budget is the number of input characters remaining. Every accepted + -- item must consume at least one character, so the budget is a strict + -- over-approximation of the iteration count and can never cut a + -- well-behaved parse short. A parser that succeeds WITHOUT consuming + -- input terminates the loop instead of spinning, which is the only + -- behavioural difference from the previous non-total definition -- and in + -- that case the previous definition did not terminate at all. + go : Nat -> List a -> Parser (List a) + go Z acc st' = Right (reverse acc, st') + go (S k) acc st' = case p st' of + Left _ => Right (reverse acc, st') + Right (x, st'') => + if length st''.input < length st'.input + then go k (x :: acc) st'' + else Right (reverse (x :: acc), st'') + +||| Parse one or more +some : Parser a -> Parser (List a) +some p st = case p st of + Left err => Left err + Right (x, st') => case many p st' of + Left err => Left err + Right (xs, st'') => Right (x :: xs, st'') + +||| Alternative +alt : Parser a -> Parser a -> Parser a +alt p1 p2 st = case p1 st of + Right res => Right res + Left _ => p2 st + +-------------------------------------------------------------------------------- +-- Character Parsers +-------------------------------------------------------------------------------- + +||| Peek at current character +peek : Parser (Maybe Char) +peek st = case st.input of + [] => Right (Nothing, st) + (c :: _) => Right (Just c, st) + +||| Consume any character +anyChar : Parser Char +anyChar st = case st.input of + [] => Left $ ParseError st.pos "Unexpected end of input" + (c :: rest) => Right (c, { input := rest, pos := S st.pos } st) + +||| Consume specific character +char : Char -> Parser Char +char expected st = case st.input of + [] => Left $ ParseError st.pos ("Expected '" ++ singleton expected ++ "'") + (c :: rest) => + if c == expected + then Right (c, { input := rest, pos := S st.pos } st) + else Left $ ParseError st.pos ("Expected '" ++ singleton expected ++ "', got '" ++ singleton c ++ "'") + +||| Consume character if predicate holds +satisfy : (Char -> Bool) -> Parser Char +satisfy pred st = case st.input of + [] => Left $ ParseError st.pos "Unexpected end of input" + (c :: rest) => + if pred c + then Right (c, { input := rest, pos := S st.pos } st) + else Left $ ParseError st.pos ("Unexpected character '" ++ singleton c ++ "'") + +||| Check if at end of input +atEnd : Parser Bool +atEnd st = Right (isNil st.input, st) + +||| Parse a digit +digit : Parser Char +digit = satisfy isDigit + +||| Parse a natural number +natural : Parser Nat +natural = map stringToNat (map pack (some digit)) + where + stringToNat : String -> Nat + stringToNat s = cast (cast {to=Integer} s) + +-------------------------------------------------------------------------------- +-- Escape Sequence Parsing +-------------------------------------------------------------------------------- + +||| Parse escape sequence +parseEscape : Parser CharClass +parseEscape st = case st.input of + [] => Left $ ParseError st.pos "Unexpected end after backslash" + (c :: rest) => + let st' : ParserState = { input := rest, pos := S st.pos } st + in case c of + 'd' => Right (Digit, st') + 'D' => Right (Negate Digit, st') + 'w' => Right (Word, st') + 'W' => Right (Negate Word, st') + 's' => Right (Space, st') + 'S' => Right (Negate Space, st') + 'n' => Right (SingleChar '\n', st') + 'r' => Right (SingleChar '\r', st') + 't' => Right (SingleChar '\t', st') + 'f' => Right (SingleChar '\x0C', st') -- Form feed + 'v' => Right (SingleChar '\x0B', st') -- Vertical tab + '0' => Right (SingleChar '\0', st') + '\\' => Right (SingleChar '\\', st') + '.' => Right (SingleChar '.', st') + '*' => Right (SingleChar '*', st') + '+' => Right (SingleChar '+', st') + '?' => Right (SingleChar '?', st') + '^' => Right (SingleChar '^', st') + '$' => Right (SingleChar '$', st') + '|' => Right (SingleChar '|', st') + '[' => Right (SingleChar '[', st') + ']' => Right (SingleChar ']', st') + '(' => Right (SingleChar '(', st') + ')' => Right (SingleChar ')', st') + '{' => Right (SingleChar '{', st') + '}' => Right (SingleChar '}', st') + _ => Left $ InvalidEscape st.pos c + +-------------------------------------------------------------------------------- +-- Character Class Parsing +-------------------------------------------------------------------------------- + +||| Parse character class item (inside [...]) +parseClassItem : Parser CharClass +parseClassItem st = case st.input of + [] => Left $ UnclosedCharClass st.pos + ('\\' :: rest) => parseEscape ({ input := rest, pos := S st.pos } st) + (']' :: _) => Left $ ParseError st.pos "Empty character class" + (c :: '-' :: ']' :: rest) => + -- Trailing dash: treat as literal + Right (Union (SingleChar c) (SingleChar '-'), { input := '-' :: ']' :: rest, pos := S st.pos } st) + (c1 :: '-' :: c2 :: rest) => + if c2 == ']' + then Right (SingleChar c1, { input := '-' :: ']' :: rest, pos := S st.pos } st) + else Right (Range c1 c2, { input := rest, pos := st.pos + 3 } st) + (c :: rest) => + Right (SingleChar c, { input := rest, pos := S st.pos } st) + +||| Parse character class contents +parseClassContents : Parser CharClass +parseClassContents st = go (length st.input) Nothing st + where + -- Budget is the remaining input length; each iteration consumes at least + -- one character via parseClassItem, so exhaustion is unreachable for + -- well-formed input. Exhaustion is reported as an unclosed class, which + -- is what running off the end of the input means here anyway. + go : Nat -> Maybe CharClass -> Parser CharClass + go Z _ st' = Left $ UnclosedCharClass st'.pos + go (S k) acc st' = case st'.input of + [] => Left $ UnclosedCharClass st'.pos + (']' :: rest) => + case acc of + Nothing => Left $ ParseError st'.pos "Empty character class" + Just cls => Right (cls, { input := rest, pos := S st'.pos } st') + _ => case parseClassItem st' of + Left err => Left err + Right (item, st'') => + go k (Just $ maybe item (\a => Union a item) acc) st'' + +||| Parse a character class [...] or [^...] +parseCharClass : Parser CharClass +parseCharClass st = + case bind (char '[') (\_ => peek) st of + Left err => Left err + Right (mc, st') => + case mc of + Just '^' => case bind anyChar (\_ => parseClassContents) st' of + Left err => Left err + Right (cls, st'') => Right (Negate cls, st'') + _ => parseClassContents st' + +-------------------------------------------------------------------------------- +-- Quantifier Parsing +-------------------------------------------------------------------------------- + +||| Parse quantifier suffix +parseQuantifier : Parser (Maybe Quantifier) +parseQuantifier st = case st.input of + ('*' :: '?' :: rest) => + Right (Just (lazy zeroOrMore), { input := rest, pos := st.pos + 2 } st) + ('*' :: rest) => + Right (Just zeroOrMore, { input := rest, pos := S st.pos } st) + ('+' :: '?' :: rest) => + Right (Just (lazy oneOrMore), { input := rest, pos := st.pos + 2 } st) + ('+' :: rest) => + Right (Just oneOrMore, { input := rest, pos := S st.pos } st) + ('?' :: '?' :: rest) => + Right (Just (lazy zeroOrOne), { input := rest, pos := st.pos + 2 } st) + ('?' :: rest) => + Right (Just zeroOrOne, { input := rest, pos := S st.pos } st) + ('{' :: rest) => + parseBraceQuantifier ({ input := rest, pos := S st.pos } st) + _ => Right (Nothing, st) + where + parseBraceQuantifier : Parser (Maybe Quantifier) + parseBraceQuantifier st = case natural st of + Left _ => Left $ InvalidQuantifier st.pos "Expected number in quantifier" + Right (n, st') => case st'.input of + ('}' :: rest) => + Right (Just (exactly n), { input := rest, pos := S st'.pos } st') + (',' :: '}' :: rest) => + Right (Just (atLeast n), { input := rest, pos := st'.pos + 2 } st') + (',' :: rest) => + case natural ({ input := rest, pos := S st'.pos } st') of + Left _ => Left $ InvalidQuantifier st.pos "Expected number after comma" + Right (m, st'') => case st''.input of + ('}' :: rest') => + if m < n + then Left $ InvalidQuantifier st.pos "Max less than min" + else Right (Just (between n m), { input := rest', pos := S st''.pos } st'') + _ => Left $ InvalidQuantifier st.pos "Expected '}'" + _ => Left $ InvalidQuantifier st.pos "Invalid quantifier syntax" + +-------------------------------------------------------------------------------- +-- Main Regex Parser +-------------------------------------------------------------------------------- + +mutual + ||| Parse a single regex atom (character, group, class, etc.) + ||| + ||| The leading `Nat` is a structural recursion budget. This group recurses + ||| through a `ParserState` record, which Idris2 cannot measure, so the + ||| budget supplies the decreasing argument instead. `parseRegex` seeds it + ||| with `16 * length (unpack pattern) + 16`: one cycle through the group is + ||| at most eight hops and consumes at least one input character, so the seed + ||| is a strict over-approximation and no valid pattern can exhaust it. + ||| Exhaustion is therefore unreachable for well-formed input, and is + ||| reported as an explicit complexity error rather than silently truncating + ||| the parse. + parseAtom : Nat -> Parser Regex + parseAtom Z st = Left $ ParseError st.pos "Regex complexity budget exhausted" + parseAtom (S k) st = case st.input of + [] => Right (Empty, st) + ('(' :: rest) => parseGroup k ({ input := rest, pos := S st.pos } st) + ('[' :: _) => map Match parseCharClass st + ('.' :: rest) => Right (Match Any, { input := rest, pos := S st.pos } st) + ('^' :: rest) => Right (StartAnchor, { input := rest, pos := S st.pos } st) + ('$' :: rest) => Right (EndAnchor, { input := rest, pos := S st.pos } st) + ('\\' :: 'b' :: rest) => Right (WordBoundary, { input := rest, pos := st.pos + 2 } st) + ('\\' :: c :: rest) => + if isDigit c && c /= '0' + then Right (BackRef (cast (ord c - ord '0')), { input := rest, pos := st.pos + 2 } st) + else case parseEscape ({ input := c :: rest, pos := S st.pos } st) of + Left err => Left err + Right (cls, st') => Right (Match cls, st') + (c :: rest) => + if c `elem` [')', '|', '*', '+', '?', '{', '}'] + then Right (Empty, st) -- Let caller handle these + else Right (Match (SingleChar c), { input := rest, pos := S st.pos } st) + + ||| Parse a group (...) or (?:...) etc. + parseGroup : Nat -> Parser Regex + parseGroup Z st = Left $ ParseError st.pos "Regex complexity budget exhausted" + parseGroup (S k) st = case st.input of + ('?' :: ':' :: rest) => + -- Non-capturing group + case parseAlternation k ({ input := rest, pos := st.pos + 2, openGroups := S st.openGroups } st) of + Left err => Left err + Right (r, st') => case st'.input of + (')' :: rest') => Right (NCGroup r, { input := rest', pos := S st'.pos, openGroups := pred st'.openGroups } st') + _ => Left $ UnclosedGroup st.pos + ('?' :: '=' :: rest) => + -- Positive lookahead + case parseAlternation k ({ input := rest, pos := st.pos + 2, openGroups := S st.openGroups } st) of + Left err => Left err + Right (r, st') => case st'.input of + (')' :: rest') => Right (Lookahead True r, { input := rest', pos := S st'.pos, openGroups := pred st'.openGroups } st') + _ => Left $ UnclosedGroup st.pos + ('?' :: '!' :: rest) => + -- Negative lookahead + case parseAlternation k ({ input := rest, pos := st.pos + 2, openGroups := S st.openGroups } st) of + Left err => Left err + Right (r, st') => case st'.input of + (')' :: rest') => Right (Lookahead False r, { input := rest', pos := S st'.pos, openGroups := pred st'.openGroups } st') + _ => Left $ UnclosedGroup st.pos + _ => + -- Capturing group + let gid = st.nextGroupId + st' = { openGroups := S st.openGroups, nextGroupId := S st.nextGroupId } st + in case parseAlternation k st' of + Left err => Left err + Right (r, st'') => case st''.input of + (')' :: rest) => Right (Group gid r, { input := rest, pos := S st''.pos, openGroups := pred st''.openGroups } st'') + _ => Left $ UnclosedGroup st.pos + + ||| Parse an atom with optional quantifier + parseQuantified : Nat -> Parser Regex + parseQuantified Z st = Left $ ParseError st.pos "Regex complexity budget exhausted" + parseQuantified (S k) st = case parseAtom k st of + Left err => Left err + Right (Empty, st') => Right (Empty, st') + Right (r, st') => case parseQuantifier st' of + Left err => Left err + Right (Nothing, st'') => Right (r, st'') + Right (Just q, st'') => Right (Quant r q, st'') + + ||| Parse a sequence of quantified atoms + parseSequence : Nat -> Parser Regex + parseSequence Z st = Left $ ParseError st.pos "Regex complexity budget exhausted" + parseSequence (S k) st = parseSequenceGo k Empty st + + ||| Accumulator loop for `parseSequence`. + ||| + ||| Hoisted out of a `where` block: `parseSequence` now has two clauses, and + ||| an Idris2 `where` attaches to a single clause only, so the helper has to + ||| live in the mutual group alongside its caller. + parseSequenceGo : Nat -> Regex -> Parser Regex + parseSequenceGo Z acc st = Right (acc, st) + parseSequenceGo (S k) acc st = case st.input of + [] => Right (acc, st) + ('|' :: _) => Right (acc, st) + (')' :: _) => Right (acc, st) + _ => case parseQuantified k st of + Left err => Left err + Right (Empty, st') => Right (acc, st') + Right (r, st') => + let combined = case acc of + Empty => r + _ => Seq acc r + in parseSequenceGo k combined st' + + ||| Parse alternation (a|b|c) + parseAlternation : Nat -> Parser Regex + parseAlternation Z st = Left $ ParseError st.pos "Regex complexity budget exhausted" + parseAlternation (S k) st = case parseSequence k st of + Left err => Left err + Right (r1, st') => case st'.input of + ('|' :: rest) => + case parseAlternation k ({ input := rest, pos := S st'.pos } st') of + Left err => Left err + Right (r2, st'') => Right (Alt r1 r2, st'') + _ => Right (r1, st') + +-------------------------------------------------------------------------------- +-- Public API +-------------------------------------------------------------------------------- + +||| Parse a regex pattern string +public export +parseRegex : String -> Either RegexError Regex +parseRegex pattern = + case parseAlternation (16 * length (unpack pattern) + 16) (initState pattern defaultFlags) of + Left err => Left err + Right (r, st) => + if isNil st.input + then Right r + else Left $ ParseError st.pos ("Unexpected character: " ++ pack st.input) + +||| Parse a regex pattern with flags +public export +parseRegexWithFlags : String -> RegexFlags -> Either RegexError Regex +parseRegexWithFlags pattern flags = + case parseAlternation (16 * length (unpack pattern) + 16) (initState pattern flags) of + Left err => Left err + Right (r, st) => + if isNil st.input + then Right r + else Left $ ParseError st.pos ("Unexpected character: " ++ pack st.input) + +||| Parse and create a safe regex +public export +parseSafe : String -> Either RegexError SafeRegex +parseSafe pattern = do + r <- parseRegex pattern + safe r + +||| Parse and create a strictly safe regex +public export +parseSafeStrict : String -> Either RegexError SafeRegex +parseSafeStrict pattern = do + r <- parseRegex pattern + safeStrict r + +||| Common pre-built safe patterns +public export +emailPattern : SafeRegex +emailPattern = case parseSafe "^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}$" of + Right sr => sr + Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 + +public export +urlPattern : SafeRegex +urlPattern = case parseSafe "^https?://[a-zA-Z0-9.-]+(/[a-zA-Z0-9._~:/?#@!$&'()*+,;=-]*)?$" of + Right sr => sr + Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 + +public export +ipv4Pattern : SafeRegex +ipv4Pattern = case parseSafe "^([0-9]{1,3}\\.){3}[0-9]{1,3}$" of + Right sr => sr + Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 + +public export +uuidPattern : SafeRegex +uuidPattern = case parseSafe "^[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}$" of + Right sr => sr + Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 diff --git a/src/Proven/SafeUrl/Proofs.idr b/src/Proven/SafeUrl/Proofs.idr index 6d60490f..af05a414 100644 --- a/src/Proven/SafeUrl/Proofs.idr +++ b/src/Proven/SafeUrl/Proofs.idr @@ -46,7 +46,7 @@ parseDeterministic s = Refl ||| Discharge once a `Data.Char` reflective tactic is available, or ||| `isUnreserved` is refactored to a non-FFI predicate. export -postulate 0 unreservedNotEncoded : (c : Char) -> +0 unreservedNotEncoded : (c : Char) -> isAlphaNum c = True -> percentEncode c = singleton c @@ -65,7 +65,7 @@ encodeEmptyEmpty = Refl ||| `unreservedNotEncoded` above). Discharge once both String FFI ||| reduction and a `Data.Char` reflective tactic are available. export -postulate 0 encodePreservesAlphaNum : (s : String) -> +0 encodePreservesAlphaNum : (s : String) -> all isAlphaNum (unpack s) = True -> urlEncode s = s @@ -88,7 +88,7 @@ decodeEmptySucceeds = Refl ||| make the case analysis on `go` definitional. Discharge once String ||| FFI reduction and a `Data.Char` reflective tactic are available. export -postulate 0 decodeUnreservedIdentity : (s : String) -> +0 decodeUnreservedIdentity : (s : String) -> all isAlphaNum (unpack s) = True -> urlDecode s = Just s @@ -105,7 +105,7 @@ postulate 0 decodeUnreservedIdentity : (s : String) -> ||| reduction is available, or via a property-test + trusted-extraction ||| validation campaign (see boj-server backend-assurance harness). export -postulate 0 encodeDecodeIdentity : (s : String) -> +0 encodeDecodeIdentity : (s : String) -> urlDecode (urlEncode s) = Just s -------------------------------------------------------------------------------- @@ -127,7 +127,7 @@ parseEmptyQuery = Refl ||| or refactor `buildQueryString` to expose the empty-list base case ||| at the top. export -postulate 0 emptyBuilderEmpty : buildQueryString Query.emptyQuery = "" +0 emptyBuilderEmpty : buildQueryString Query.emptyQuery = "" ||| DISCHARGED: Adding a parameter increases the parameter count by one. ||| `addParam key val qb` is defined as `MkQueryBuilder (qb.params ++ @@ -157,7 +157,7 @@ addParamIncreasesCount key val qb = lengthSnoc (key, val) qb.params ||| SafeChecksum Luhn/ISBN (String FFI opacity). Discharge once String ||| equality is type-level reducible, or via a property-test campaign. export -postulate 0 setGetIdentity : (key, val : String) -> (qs : QueryString) -> +0 setGetIdentity : (key, val : String) -> (qs : QueryString) -> getParam key (setParam key val qs) = Just val ||| OWED: After removing all instances of a key, `hasParam` returns @@ -170,7 +170,7 @@ postulate 0 setGetIdentity : (key, val : String) -> (qs : QueryString) -> ||| induction over `qs`. Discharge once String equality is type-level ||| reducible. Same blocker family as `setGetIdentity`. export -postulate 0 removeHasNot : (key : String) -> (qs : QueryString) -> +0 removeHasNot : (key : String) -> (qs : QueryString) -> hasParam key (removeAllParams key qs) = False ||| OWED: `filterParams` keeps only entries whose keys are in the given @@ -184,7 +184,7 @@ postulate 0 removeHasNot : (key : String) -> (qs : QueryString) -> ||| / proving the `filterAll` lemma and rewriting, once String equality ||| is type-level reducible. export -postulate 0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) -> +0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) -> all (\(k, _) => k `elem` keys) (filterParams keys qs) = True -------------------------------------------------------------------------------- @@ -202,7 +202,7 @@ postulate 0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) -> ||| "42" = Just 42` is operationally true but opaque). Discharge via ||| property-test + trusted-extraction validation. export -postulate 0 parseIntValid : (key : String) -> +0 parseIntValid : (key : String) -> getIntParam key [(key, "42")] = Just 42 ||| OWED: Parsing bool `"true"` from a matching key yields `Just True`. @@ -216,7 +216,7 @@ postulate 0 parseIntValid : (key : String) -> ||| Discharge once String equality is type-level reducible, or via ||| property-test campaign. export -postulate 0 parseBoolTrue : (key : String) -> +0 parseBoolTrue : (key : String) -> getBoolParam key [(key, "true")] = Just True ||| OWED: Parsing bool `"false"` from a matching key yields `Just @@ -225,7 +225,7 @@ postulate 0 parseBoolTrue : (key : String) -> ||| Held back by the same Idris2 0.8.0 String-literal-match ||| (`prim__eqString` FFI) opacity. Discharge with `parseBoolTrue`. export -postulate 0 parseBoolFalse : (key : String) -> +0 parseBoolFalse : (key : String) -> getBoolParam key [(key, "false")] = Just False -------------------------------------------------------------------------------- @@ -251,7 +251,7 @@ mergeEmptyRight qs = Refl ||| once String equality is type-level reducible and the snoc-length ||| lemma is `%reducible`. export -postulate 0 mergeEmptyLeft : (qs : QueryString) -> +0 mergeEmptyLeft : (qs : QueryString) -> mergeQueryStrings [] qs = qs ||| OWED: Query string append is associative — inherited from @@ -284,7 +284,7 @@ appendAssociative qs1 qs2 qs3 = sym (Data.List.appendAssociative qs1 qs2 qs3) ||| because `isSafeSchemeNotJavascript` is OWED — see below. public export data SafeURL : ParsedURL -> Type where - postulate MkSafeURL : (url : ParsedURL) -> + MkSafeURL : (url : ParsedURL) -> (0 _ : Not (url.scheme = Just (Custom "javascript"))) -> SafeURL url @@ -309,7 +309,7 @@ isSafeScheme url = case url.scheme of ||| `setGetIdentity`. Discharge once String equality is type-level ||| reducible. Used by `validateSafe` to construct `MkSafeURL`. export -postulate 0 isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True -> +0 isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True -> Not (url.scheme = Just (Custom "javascript")) ||| Validate URL is safe @@ -327,26 +327,34 @@ validateSafe url = ||| IPv4 address components are bounded public export data ValidIPv4 : Host -> Type where - postulate MkValidIPv4 : (a, b, c, d : Nat) -> + MkValidIPv4 : (a, b, c, d : Nat) -> LTE a 255 -> LTE b 255 -> LTE c 255 -> LTE d 255 -> ValidIPv4 (IPv4 a b c d) ||| Port number is bounded. -||| The `LTE p 65535` proof is stored at erased multiplicity (`0`) -||| because `lteFrom65535Check` is OWED — see below. +||| The `LTE p 65535` witness is stored at erased multiplicity (`0`) +||| because it is needed only for the type, never at runtime. public export data ValidPort : Nat -> Type where - postulate MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p + MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p -||| DISCHARGED via `Data.Nat.lteReflectsLTE` stdlib lemma. +||| DISCHARGED 2026-08-27 via `Data.Nat.lteReflectsLTE`. +||| +||| The hypothesis is stated over `Data.Nat.lte`, NOT over `Ord Nat`'s +||| `(<=)`. They are different functions: `p <= 65535` on `Nat` +||| elaborates to `not (compare p 65535 == GT)`, which is NOT convertible +||| with `lte p 65535` for an abstract `p`, and `lteReflectsLTE` consumes +||| the latter. Stating the lemma over `(<=)` is the whole reason it sat +||| undischarged -- the stdlib lemma was always the right one, applied to +||| the wrong relation. export -lteFrom65535Check : (p : Nat) -> (p <= 65535 = True) -> LTE p 65535 +lteFrom65535Check : (p : Nat) -> (Nat.lte p 65535 = True) -> LTE p 65535 lteFrom65535Check p prf = Data.Nat.lteReflectsLTE p 65535 prf ||| Validate port is in range public export validatePort : (p : Nat) -> Maybe (ValidPort p) validatePort p = - case decEq (p <= 65535) True of + case decEq (Nat.lte p 65535) True of Yes prf => Just (MkValidPort p (lteFrom65535Check p prf)) No _ => Nothing