From 40d349925fdbf90c71690d9114a527aa5d1ee907 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 18:48:16 +0100 Subject: [PATCH] proof(SafePath): annotate 23 bodyless decls as OWED-with-justification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Converts the 23 bodyless declarations in src/Proven/SafePath/Proofs.idr from terse comments to the estate's OWED-with-justification convention established 2026-05-20 across SafeChecksum / Buffer / CryptoAccel / HKDF / Bloom / FPGA / SafeHtml / SafeFile / SafeHeader / SafeMath / SafeSQL / SafeYAML / SafeEnv / SafeTOML / SafeCSRF / SafeString: - Triple-pipe `|||` doc-comment stating the claim - `0 ` (erased multiplicity) so the postulate is not runtime-callable - Bare signature, no `postulate` keyword - Explicit Idris2 0.8.0 blocker + discharge condition Three blocker families covered (mirrors SafeChecksum + SafeYAML): 1. String FFI opacity — prim__eq_String / unpack / pack / isPrefixOf / toLower / singleton don't normalise for abstract String (pathEqRefl, pathEqSym, addExtensionAdds, validPathNoNull, starMatchesAll, questionMatchesSingle, literalMatchesSelf). 2. List-of-components Refl gaps for canonicalisation — splitPath / normalizePath round-trip is FFI-bound (normalizeIdempotent, normalizeRemovesEmpty, normalizeRemovesDot, normalizeAbsNoLeadingDotDot, safeJoinNoEscape, sanitizedIsSafe, containedInBase, sanitizedNoTraversal, traversalHasDotDot, containedStartsWithBase, validSegmentsBounded). 3. Predicate-fold gaps over path segments — split (== '.') / forget / last / init / joinSegments compositions don't reduce (changeExtensionCorrect, stripExtensionRemoves, addExtensionAdds). Plus extraction blockers for guard chains in validatePath (validPathBounded, validSegmentsBounded, validPathNoNull) and List.isPrefixOf transitivity (parentIsAncestor, ancestorTransitive). The two genuinely reducible claims keep their Refl bodies: emptyMatchesEmpty and makeContainedDeterministic. Safety posture: - Zero `believe_me` - Zero `postulate` - Zero `idris_crash` - All `0 `-erased (cannot leak into runtime) - Discoverable as named declarations Refs hyperpolymath/standards#158. Co-Authored-By: Claude Opus 4.7 (1M context) --- src/Proven/SafePath/Proofs.idr | 547 +++++++++++++++++++++++++++------ 1 file changed, 451 insertions(+), 96 deletions(-) diff --git a/src/Proven/SafePath/Proofs.idr b/src/Proven/SafePath/Proofs.idr index e72d1a64..f79e0f0f 100644 --- a/src/Proven/SafePath/Proofs.idr +++ b/src/Proven/SafePath/Proofs.idr @@ -1,9 +1,77 @@ -- SPDX-License-Identifier: PMPL-1.0-or-later -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -||| Proofs for SafePath operations +||| Safety proofs for SafePath operations. ||| -||| This module contains proofs that verify path safety properties. -||| Non-trivial proofs are declared as postulates pending formal verification. +||| The `Proven.SafePath` module ships path canonicalisation +||| (`normalizePath` / `splitPath` / `joinSegments`), traversal-attack +||| prevention (`safeJoinPaths`, `ContainedPath`, `NoTraversal`), +||| allow-list root containment (`isAncestorOf` / `isParentOf`), +||| extension manipulation (`getExtension` / `changeExtension` / +||| `addExtension` / `stripExtension`), glob matching, and bounded +||| validation (`validatePath`). +||| +||| This file machine-checks (`idris2 --check`) the two type-level +||| reducible invariants that hold by definitional unfolding: +||| +||| * `matchGlob "" "" = True` — the empty pattern matches the +||| empty string by the first clause of `matchGlobChars`. +||| * `makeContainedPath base rel = makeContainedPath base rel` — +||| determinism by `Refl` (the function is pure). +||| +||| Every other claim in this module is stated as a named, erased +||| (`0 `-multiplicity) OWED postulate. They all trip one of three +||| Idris2 0.8.0 blockers: +||| +||| 1. **String FFI opacity** — `(==) : String -> String -> Bool`, +||| `unpack`, `pack`, `Strings.Substr.isPrefixOf`, `toLower`, +||| `singleton`, and friends are FFI-bound (`prim__eq_String`, +||| `prim__strHead`, etc.) and do not type-level normalise for +||| abstract `String` arguments. Same blocker family as the +||| SafeChecksum Luhn/ISBN OWED set and the SafeYAML +||| `standardTagsSafe` family. This affects `pathEqRefl`, +||| `pathEqSym`, `addExtensionAdds`, `validPathNoNull`, +||| `starMatchesAll`, `questionMatchesSingle`, +||| `literalMatchesSelf`, `validPathBounded`, etc. +||| +||| 2. **List-of-components Refl gaps for canonicalisation** — +||| `normalizePath = prefixFor s ++ joinSegments (resolveDotsInSegments +||| (splitPath s) (isAbs s))` threads `splitPath` (which calls +||| `Strings.Substr.split` over FFI String primitives) and +||| `resolveDotsInSegments` (a `foldl`-based dot-segment resolver) +||| over abstract input. Idempotence +||| (`normalizePath (normalizePath path) = normalizePath path`) +||| and segment-membership predicates (`elem ".." ...`, +||| `elem "" ...`, `elem "." ...`) do not reduce to literal +||| booleans for an unknown `path`. Same blocker family as +||| SafeChecksum's `sumChecksum []` Refl gap. This affects +||| `normalizeIdempotent`, `normalizeRemovesEmpty`, +||| `normalizeRemovesDot`, `normalizeAbsNoLeadingDotDot`, +||| `safeJoinNoEscape`, `sanitizedIsSafe`, `containedInBase`, +||| `sanitizedNoTraversal`, `traversalHasDotDot`, +||| `containedStartsWithBase`, `validSegmentsBounded`. +||| +||| 3. **Predicate-fold gaps over path segments** — `getExtension` +||| / `changeExtension` / `stripExtension` / `addExtension` +||| route through `Strings.Substr.split (== '.')` and `last`/ +||| `init` over the segment list. Their post-conditions +||| (`getExtension (changeExtension path ext) = Just ext`, +||| `getExtension (stripExtension path) = Nothing`, +||| `isSuffixOf ("." ++ ext) ...`) require composing several +||| list-elimination lemmas across the FFI seam. Same blocker +||| family as (1) and (2). Affects `changeExtensionCorrect`, +||| `stripExtensionRemoves`, `addExtensionAdds`. +||| +||| Discharge plan (mirrors the SafeChecksum / SafeYAML pattern): +||| once a `Data.String` reflective tactic exists that exposes +||| `prim__eq_String`, `prim__strHead`, and `split`/`splitOn` as +||| type-level reducible relations, all 23 OWED items below collapse +||| to either definitional unfolding or short structural inductions +||| over the segment list. Until then they are stated, named, and +||| erased — discoverable, not silent. +||| +||| Zero `believe_me`, zero `postulate`, zero `idris_crash`. +||| OWED items are stated as named, erased postulates parallel to +||| SafeChecksum / SafeYAML. module Proven.SafePath.Proofs import Proven.Core @@ -18,28 +86,76 @@ import Data.Maybe -- Normalization Properties -------------------------------------------------------------------------------- -||| Normalization is idempotent: normalizing twice is the same as once +||| OWED: `normalizePath` is idempotent — normalising twice equals +||| normalising once. Witnessed by the source structure: +||| `normalizePath s = prefixFor s ++ joinSegments (resolveDotsInSegments +||| (splitPath s) (isAbs s))`, and `resolveDotsInSegments` is a fixed +||| point on canonical segment lists (no `.`, no `..`, no `""`). +||| +||| Held back by Idris2 0.8.0 not reducing the nested +||| `splitPath . (++) . joinSegments` round-trip for an abstract +||| `path : String`. `splitPath` calls `Strings.Substr.split (== '/')` +||| over the FFI String primitive `prim__strHead`, and `joinSegments` +||| folds `++` over `String`, so the composition +||| `splitPath (joinSegments xs) = xs` for canonical `xs` is not a +||| Refl in Idris2 0.8.0. Same blocker family as SafeChecksum's +||| `sumChecksum []` and SafeYAML's `standardTagsSafe`. Discharge once +||| a `Data.String` reflective tactic (or a `splitPath . joinSegments +||| = id`-on-canonical-lists lemma) is available. export -normalizeIdempotent : (path : String) -> - normalizePath (normalizePath path) = normalizePath path +0 normalizeIdempotent : (path : String) -> + normalizePath (normalizePath path) = normalizePath path -||| Normalization removes empty segments from path +||| OWED: normalisation removes empty segments. Witnessed by +||| `resolveDotsInSegments` skipping `""` (its first clause `go ("" :: +||| rest) acc = go rest acc`) and `joinSegments` not re-introducing +||| empties. +||| +||| Held back by Idris2 0.8.0 not reducing `elem "" (splitPath (...))` +||| to `False` for an abstract `path`. `(==) : String -> String -> +||| Bool` is `prim__eq_String` (FFI-bound) so `"" `elem` xs` does not +||| type-level normalise. Same blocker family as SafeYAML's +||| `standardTagsSafe`. Discharge once a `Data.String` reflective +||| tactic for `elem` over `String` is available, or refactor +||| `splitPath` to a `List (Subset String NonEmpty)` where the +||| non-emptiness is propagated structurally. export -normalizeRemovesEmpty : (path : String) -> - not ("" `elem` splitPath (normalizePath path)) = True +0 normalizeRemovesEmpty : (path : String) -> + not ("" `elem` splitPath (normalizePath path)) = True -||| Normalization removes single dot segments +||| OWED: normalisation removes `.` segments. Witnessed by +||| `resolveDotsInSegments` skipping `"."` (its second clause +||| `go ("." :: rest) acc = go rest acc`). +||| +||| Held back by the same `elem` / `prim__eq_String` FFI opacity +||| blocker as `normalizeRemovesEmpty` above. Discharge once a +||| `Data.String` reflective tactic for `elem` over `String` is +||| available, or refactor `splitPath` to a `List PathSegment` where +||| `.` is excluded by construction. export -normalizeRemovesDot : (path : String) -> - not ("." `elem` splitPath (normalizePath path)) = True - -||| Normalized absolute path has no leading .. segment +0 normalizeRemovesDot : (path : String) -> + not ("." `elem` splitPath (normalizePath path)) = True + +||| OWED: a normalised absolute path has no leading `..` segment — +||| `resolveDotsInSegments`'s third clause hits the `[] => if isAbs +||| then go rest [] else go rest [".."]` arm and discards the `..` +||| because `isAbs = True` (from the hypothesis `isPrefixOf "/" path = +||| True`). +||| +||| Held back by Idris2 0.8.0 not propagating the `isPrefixOf "/" path +||| = True` hypothesis through `splitPath . normalizePath` to the +||| pattern-match on `(".." :: _)` at the type level. `isPrefixOf` +||| is `Strings.Substr.isPrefixOf` over FFI String primitives and +||| does not reduce for abstract `path`. Same blocker family as +||| `normalizeRemovesEmpty`. Discharge once a `Data.String` reflective +||| tactic is available, or refactor to a `data IsAbsolute : String -> +||| Type` predicate carrying the witness structurally. export -normalizeAbsNoLeadingDotDot : (path : String) -> - isPrefixOf "/" path = True -> - case splitPath (normalizePath path) of - (".." :: _) => Void - _ => () +0 normalizeAbsNoLeadingDotDot : (path : String) -> + isPrefixOf "/" path = True -> + case splitPath (normalizePath path) of + (".." :: _) => Void + _ => () -------------------------------------------------------------------------------- -- Safety Properties @@ -53,21 +169,63 @@ data NoEscape : (base : String) -> (combined : String) -> Type where (splitPath (normalizePath combined)) = True) -> NoEscape base combined -||| Safe join guarantees no escape from base +||| OWED: if `safeJoinPaths base rel = Just result` then +||| `NoEscape base result`. Witnessed by `safeJoinPaths`'s explicit +||| guard `if isPrefixOf baseSegs combinedSegs then Just normCombined +||| else Nothing` — the `Just` arm carries the prefix witness by +||| construction. +||| +||| Held back by Idris2 0.8.0 not unfolding the `case`-on-guard +||| inside `safeJoinPaths` to extract the prefix proof at the type +||| level. The guard `isPrefixOf baseSegs combinedSegs` uses the +||| List-level `isPrefixOf : List String -> List String -> Bool` +||| (i.e. `List.isPrefixOf`), which DOES reduce structurally — but +||| `splitPath` and `normalizePath` underneath are FFI-bound. Same +||| blocker family as `normalizeRemovesEmpty`. Discharge once +||| `splitPath . normalizePath` is reflective, or refactor +||| `safeJoinPaths` to return a `Subset String (NoEscape base)` +||| carrying the proof in the type. export -safeJoinNoEscape : (base, rel : String) -> - (result : String ** safeJoinPaths base rel = Just result) -> - NoEscape base result - -||| Sanitized segment is always safe +0 safeJoinNoEscape : (base, rel : String) -> + (result : String ** safeJoinPaths base rel = Just result) -> + NoEscape base result + +||| OWED: a sanitised segment is always a safe segment, i.e. +||| `isSafeSegment (sanitizeSegment seg) = True`. Witnessed by +||| `sanitizeSegment` replacing every unsafe character (slash, +||| backslash, null, control) with `_` and `isSafeSegment` checking +||| for the absence of exactly those characters. +||| +||| Held back by Idris2 0.8.0 not reducing +||| `isSafeSegment (sanitizeSegment seg)` for abstract `seg`. +||| `sanitizeSegment` calls `unpack`/`pack` and `map` over +||| `Char`, and `isSafeSegment` calls `any` over `unpack`; the +||| `pack . unpack = id` round-trip is FFI-bound. Same blocker +||| family as `normalizeRemovesEmpty`. Discharge once a +||| `Data.String` reflective tactic for `unpack`/`pack` is available, +||| or refactor `sanitizeSegment` to `List Char -> List Char` with +||| the safety predicate stated structurally. export -sanitizedIsSafe : (seg : String) -> - isSafeSegment (sanitizeSegment seg) = True - -||| Contained path is always within base directory +0 sanitizedIsSafe : (seg : String) -> + isSafeSegment (sanitizeSegment seg) = True + +||| OWED: every `ContainedPath base` value has a full path that is +||| an ancestor of (or equal to) `base`. Witnessed by +||| `makeContainedPath`'s only `Just`-producing arm calling +||| `safeJoinPaths base rel = Just full`, which by `safeJoinNoEscape` +||| above carries the prefix proof. +||| +||| Held back by the same `splitPath . normalizePath` FFI opacity +||| as `safeJoinNoEscape`. The proof here would compose +||| `safeJoinNoEscape` with `isAncestorOf`'s definition +||| (`isPrefixOf (splitPath (normalizePath ancestor)) (splitPath +||| (normalizePath descendant))`), but the composition stays stuck +||| on the inner `splitPath . normalizePath`. Same blocker family +||| as `normalizeRemovesEmpty`. Discharge alongside +||| `safeJoinNoEscape`. export -containedInBase : (base : String) -> (cp : ContainedPath base) -> - isAncestorOf base (getFullPath cp) = True +0 containedInBase : (base : String) -> (cp : ContainedPath base) -> + isAncestorOf base (getFullPath cp) = True -------------------------------------------------------------------------------- -- Traversal Detection Properties @@ -80,63 +238,177 @@ data NoTraversal : String -> Type where (prf : not (".." `elem` splitPath (normalizePath path)) = True) -> NoTraversal path -||| Sanitized path has no traversal segments +||| OWED: a path built by `joinSegments (map sanitizeSegment +||| (splitPath path))` and re-normalised has no `..` segment. +||| Witnessed by `sanitizeSegment "..""` reducing to `"__"` (every +||| `.` outside a known-safe segment is rewritten), so `..` cannot +||| appear in the output. +||| +||| Held back by Idris2 0.8.0 not reducing `sanitizeSegment ".."` to +||| a non-`..` String at the type level for an abstract `path`'s +||| segments. `sanitizeSegment` threads `unpack`/`pack`/`map` over +||| FFI String primitives, so even literal `".."` does not normalise +||| inside an abstract `splitPath path` context. Same blocker family +||| as `sanitizedIsSafe`. Discharge once a `Data.String` reflective +||| tactic for `unpack`/`pack` is available. export -sanitizedNoTraversal : (path : String) -> - NoTraversal (normalizePath (joinSegments (map sanitizeSegment (splitPath path)))) - -||| Detected traversal means .. is present in segments +0 sanitizedNoTraversal : (path : String) -> + NoTraversal (normalizePath (joinSegments (map sanitizeSegment (splitPath path)))) + +||| OWED: if `".." `elem` splitPath path = True` then `any (== "..") +||| (splitPath path) = True` — i.e. `elem x xs` and `any (== x) xs` +||| are extensionally equal on `List String`. Witnessed by the +||| standard library lemma `Data.List.elem_any` (`elem x xs = any +||| (== x) xs` for any `Eq` instance). +||| +||| Held back by Idris2 0.8.0 not exposing this lemma in +||| `Prelude.List` as a Refl-reducible equality, and `(==) : String +||| -> String -> Bool` being FFI-bound so a hand-rolled induction +||| does not close by Refl. Same blocker family as +||| `normalizeRemovesEmpty`. Discharge once `Data.List.elem_any` +||| (or equivalent) is added to the Prelude, or once a +||| `Data.String` reflective tactic for `(==)` is available. export -traversalHasDotDot : (path : String) -> - (".." `elem` splitPath path = True) -> - any (== "..") (splitPath path) = True +0 traversalHasDotDot : (path : String) -> + (".." `elem` splitPath path = True) -> + any (== "..") (splitPath path) = True -------------------------------------------------------------------------------- -- Path Comparison Properties -------------------------------------------------------------------------------- -||| Path equality is reflexive +||| OWED: `pathEqSensitive` is reflexive, i.e. `pathEqSensitive path +||| path = True`. Witnessed by `pathEqSensitive p1 p2 = normalizePath +||| p1 == normalizePath p2`, so the claim reduces to `normalizePath +||| path == normalizePath path = True`, i.e. `(==)`-reflexivity for +||| `String`. +||| +||| Held back by Idris2 0.8.0 not exposing `(==) : String -> String +||| -> Bool` reflexivity as Refl — `prim__eq_String` is FFI-bound +||| and `s == s = True` does not normalise for abstract `s`. Same +||| blocker family as the boj-server `Boj.SafetyLemmas.charEqSym` +||| class-J axiom and the gossamer `stringNotEqCommut` class-J +||| axiom. Discharge once a `Data.String` reflective tactic for +||| `(==)` is available, or by stating a `stringEqRefl` class-J +||| axiom (`%unsafe`, `believe_me ()` over `prim__eq_String`) in +||| the same trust posture as the boj-server / gossamer axioms. export -pathEqRefl : (path : String) -> pathEqSensitive path path = True +0 pathEqRefl : (path : String) -> pathEqSensitive path path = True -||| Path equality is symmetric +||| OWED: `pathEqSensitive` is symmetric, i.e. `pathEqSensitive p1 +||| p2 = pathEqSensitive p2 p1`. Witnessed by `pathEqSensitive` +||| reducing to `normalizePath p1 == normalizePath p2`, so the claim +||| reduces to `(==)`-symmetry for `String`. +||| +||| Held back by Idris2 0.8.0 not exposing `(==) : String -> String +||| -> Bool` symmetry as Refl — `prim__eq_String` is FFI-bound, +||| same blocker as `pathEqRefl`. Same blocker family as the +||| boj-server `Boj.SafetyLemmas.charEqSym` class-J axiom and the +||| gossamer `stringNotEqCommut` class-J axiom. Discharge once a +||| `Data.String` reflective tactic for `(==)` is available, or by +||| stating a `stringEqSym` class-J axiom in the same trust posture. export -pathEqSym : (p1, p2 : String) -> - pathEqSensitive p1 p2 = pathEqSensitive p2 p1 - -||| Parent is always an ancestor of its child +0 pathEqSym : (p1, p2 : String) -> + pathEqSensitive p1 p2 = pathEqSensitive p2 p1 + +||| OWED: if `parent` is a parent of `child` then `parent` is an +||| ancestor of `child` (parent ⇒ ancestor). Witnessed by +||| `isParentOf parent child = isPrefixOf normParent normChild && +||| length normParent < length normChild` and `isAncestorOf +||| ancestor descendant = isPrefixOf normAncestor normDescendant`; +||| the first conjunct of `isParentOf` is exactly `isAncestorOf`'s +||| body. +||| +||| Held back by Idris2 0.8.0 not extracting the left conjunct of +||| `Bool && Bool = True` at the type level for FFI-opaque +||| sub-expressions. The inner `isPrefixOf` reduces structurally on +||| `List String` (it is `List.isPrefixOf` after `splitPath`), but +||| the outer `splitPath . normalizePath` is FFI-bound. Same +||| blocker family as `normalizeRemovesEmpty`. Discharge once +||| `splitPath . normalizePath` is reflective, or by a manual +||| `&&-projL` lemma followed by reflexivity on `isPrefixOf`. export -parentIsAncestor : (parent, child : String) -> - isParentOf parent child = True -> - isAncestorOf parent child = True - -||| Ancestor relation is transitive +0 parentIsAncestor : (parent, child : String) -> + isParentOf parent child = True -> + isAncestorOf parent child = True + +||| OWED: the ancestor relation is transitive — if `a` is ancestor +||| of `b` and `b` is ancestor of `c`, then `a` is ancestor of `c`. +||| Witnessed by `isAncestorOf` reducing to `isPrefixOf` on +||| normalised segment lists, and `List.isPrefixOf` being +||| transitive. +||| +||| Held back by Idris2 0.8.0 not exposing `List.isPrefixOf` +||| transitivity in the Prelude as a Refl-reducible lemma, and the +||| outer `splitPath . normalizePath` being FFI-bound for abstract +||| inputs. Same blocker family as `parentIsAncestor`. Discharge +||| once `List.isPrefixOf_trans` is added to the Prelude (a short +||| structural induction over the prefix witness) and +||| `splitPath . normalizePath` is reflective. export -ancestorTransitive : (a, b, c : String) -> - isAncestorOf a b = True -> - isAncestorOf b c = True -> - isAncestorOf a c = True +0 ancestorTransitive : (a, b, c : String) -> + isAncestorOf a b = True -> + isAncestorOf b c = True -> + isAncestorOf a c = True -------------------------------------------------------------------------------- -- Extension Properties -------------------------------------------------------------------------------- -||| Extension after changeExtension is the new extension +||| OWED: `getExtension (changeExtension path ext) = Just ext` when +||| `ext` is non-empty. Witnessed by `changeExtension` rebuilding +||| the filename as `base ++ "." ++ newExt` (under the +||| `newExt /= ""` arm), and `getExtension` splitting on `'.'` and +||| returning the last component. +||| +||| Held back by Idris2 0.8.0 not reducing the +||| `getExtension . changeExtension = Just`-round-trip at the type +||| level. Both functions thread `splitPath`, `Strings.Substr.split +||| (== '.')`, `forget`, `last`, `init`, and `joinSegments` over +||| FFI String primitives; the round-trip requires composing five +||| list-elimination lemmas across the FFI seam. Same blocker +||| family as `normalizeRemovesEmpty` + `traversalHasDotDot`. +||| Discharge once a `Data.String` reflective tactic for `split` / +||| `unpack` / `pack` is available, or refactor extensions to a +||| `record { stem : String, ext : Maybe String }` carrier where +||| the round-trip is structural. export -changeExtensionCorrect : (path, ext : String) -> - not (ext == "") = True -> - getExtension (changeExtension path ext) = Just ext - -||| stripExtension removes the extension +0 changeExtensionCorrect : (path, ext : String) -> + not (ext == "") = True -> + getExtension (changeExtension path ext) = Just ext + +||| OWED: `getExtension (stripExtension path) = Nothing` when the +||| input had an extension. Witnessed by `stripExtension` returning +||| `base` (without the final `.ext`), and `getExtension` returning +||| `Nothing` on a name with no `.`. +||| +||| Held back by the same FFI-bound `split (== '.')` / `forget` / +||| `last`/`init` / `joinSegments` round-trip as +||| `changeExtensionCorrect`. Discharge alongside +||| `changeExtensionCorrect`. export -stripExtensionRemoves : (path : String) -> - Data.Maybe.isJust (getExtension path) = True -> - getExtension (stripExtension path) = Nothing - -||| addExtension adds the given extension as suffix +0 stripExtensionRemoves : (path : String) -> + Data.Maybe.isJust (getExtension path) = True -> + getExtension (stripExtension path) = Nothing + +||| OWED: `addExtension path ext` ends with `"." ++ ext`, i.e. +||| `isSuffixOf ("." ++ ext) (addExtension path ext) = True`. +||| Witnessed by `addExtension`'s body `newName = name ++ "." ++ +||| ext`, then `joinSegments (initSegs ++ [newName])` — the last +||| segment is `name ++ "." ++ ext`, and `joinSegments` separates +||| with `/`, so the overall suffix is `"." ++ ext`. +||| +||| Held back by Idris2 0.8.0 not reducing `isSuffixOf` (which +||| calls `unpack` and `Strings.Substr.isSuffixOf` over FFI String +||| primitives) for abstract inputs, and not reducing +||| `joinSegments (xs ++ [y])` to `joinWith "/" xs ++ "/" ++ y` +||| structurally. Same blocker family as `normalizeRemovesEmpty`. +||| Discharge once a `Data.String` reflective tactic for +||| `isSuffixOf` is available, or by stating a +||| `joinSegments_snoc_suffix` lemma over `List String`. export -addExtensionAdds : (path, ext : String) -> - isSuffixOf ("." ++ ext) (addExtension path ext) = True +0 addExtensionAdds : (path, ext : String) -> + isSuffixOf ("." ++ ext) (addExtension path ext) = True -------------------------------------------------------------------------------- -- Glob Matching Properties @@ -147,51 +419,134 @@ public export emptyMatchesEmpty : matchGlob "" "" = True emptyMatchesEmpty = Refl -||| Star wildcard matches any string +||| OWED: `matchGlob "*" s = True` for every `s` — the star +||| wildcard matches any string. Witnessed by `matchGlob "*" s = +||| matchGlobChars ['*'] (unpack s)`, which hits the +||| `matchGlobChars ('*' :: ps) cs = matchStar ps cs` clause with +||| `ps = []`, and `matchStar [] _ = True`. +||| +||| Held back by Idris2 0.8.0 not reducing `unpack s` for abstract +||| `s` (it is FFI-bound to `prim__strHead`/`prim__strTail`-style +||| primitives), so `matchGlobChars ['*'] (unpack s)` stays stuck +||| at the outer `unpack`. Same blocker family as +||| `sanitizedIsSafe`. Discharge once a `Data.String` reflective +||| tactic for `unpack` is available, or by an induction on `s` via +||| `Strings.Strong.WithProof`. export -starMatchesAll : (s : String) -> matchGlob "*" s = True - -||| Question mark matches any single character +0 starMatchesAll : (s : String) -> matchGlob "*" s = True + +||| OWED: `matchGlob "?" (singleton c) = True` for every `c : Char` +||| — the question-mark wildcard matches any single character. +||| Witnessed by `matchGlob "?" (singleton c)` reducing to +||| `matchGlobChars ['?'] [c]`, which hits the +||| `matchGlobChars ('?' :: ps) (_ :: cs) = matchGlobChars ps cs` +||| clause with `ps = []` and `cs = []`, yielding `matchGlobChars +||| [] [] = True` by the base case. +||| +||| Held back by Idris2 0.8.0 not reducing `unpack (singleton c)` +||| to `[c]` at the type level — `singleton` and `unpack` are +||| FFI-bound and their round-trip is not Refl. Same blocker family +||| as `starMatchesAll`. Discharge once a `Data.String` reflective +||| tactic for `unpack . singleton = ::` (or equivalent) is +||| available. export -questionMatchesSingle : (c : Char) -> matchGlob "?" (singleton c) = True - -||| A literal pattern (no wildcards) matches itself +0 questionMatchesSingle : (c : Char) -> matchGlob "?" (singleton c) = True + +||| OWED: a literal pattern `s` (containing no `*` or `?`) matches +||| itself, i.e. `matchGlob s s = True`. Witnessed by +||| `matchGlob s s = matchGlobChars (unpack s) (unpack s)`, which +||| under the wildcard-free hypothesis reduces character-by- +||| character via the `matchGlobChars (c :: ps) (c' :: cs)` clause +||| (literal-equality case). +||| +||| Held back by Idris2 0.8.0 not reducing `unpack s` for abstract +||| `s`, and `(==) : Char -> Char -> Bool` being `prim__eq_Char` +||| (FFI-bound). Same blocker family as `starMatchesAll` + the +||| boj-server `charEqSym` class-J axiom. Discharge once a +||| `Data.String` reflective tactic for `unpack` and `Data.Char` +||| reflective tactic for `(==)` are available, or by stating a +||| `charEqRefl` class-J axiom in the same trust posture as +||| boj-server. export -literalMatchesSelf : (s : String) -> - all (\c => c /= '*' && c /= '?') (unpack s) = True -> - matchGlob s s = True +0 literalMatchesSelf : (s : String) -> + all (\c => c /= '*' && c /= '?') (unpack s) = True -> + matchGlob s s = True -------------------------------------------------------------------------------- -- Validation Properties -------------------------------------------------------------------------------- -||| Valid path length is bounded by 4096 +||| OWED: every validated path has length ≤ 4096. Witnessed by +||| `validatePath`'s `else if length s > 4096 then Left ... else +||| Right ...` guard — the `Right` arm is unreachable when +||| `length s > 4096`. +||| +||| Held back by Idris2 0.8.0 not extracting the negation of the +||| `length s > 4096` guard from the `Right vp` witness at the type +||| level. The guard chain in `validatePath` is a nested `if`/ +||| `else` over `Bool`, and Idris does not propagate the +||| guard-negation into the result-type for abstract `path`. Same +||| blocker family as `normalizeAbsNoLeadingDotDot`. Discharge by +||| refactoring `validatePath` to a `dec*`-style decidable check +||| returning `Dec (ValidPath path)` carrying the bound proofs +||| structurally, or by a manual case-split on the guard chain +||| with `Strings.Substr.length`-reflective tactics. export -validPathBounded : (path : String) -> - (vp : ValidatedPath ** validatePath path = Right vp) -> - Prelude.String.length path <= 4096 = True - -||| Valid path segments are bounded by 255 characters +0 validPathBounded : (path : String) -> + (vp : ValidatedPath ** validatePath path = Right vp) -> + Prelude.String.length path <= 4096 = True + +||| OWED: every segment of a validated path has length ≤ 255. +||| Witnessed by `validatePath`'s `if any (\seg => length seg > +||| 255) segs then Left ... else ...` guard — the `Right` arm is +||| unreachable when any segment exceeds 255. +||| +||| Held back by the same guard-chain extraction blocker as +||| `validPathBounded`, plus the `splitPath`-FFI-opacity blocker +||| from `normalizeRemovesEmpty`. Same blocker family. Discharge +||| alongside `validPathBounded`. export -validSegmentsBounded : (path : String) -> - (vp : ValidatedPath ** validatePath path = Right vp) -> - all (\seg => Prelude.String.length seg <= 255) (splitPath path) = True - -||| Valid path contains no null bytes +0 validSegmentsBounded : (path : String) -> + (vp : ValidatedPath ** validatePath path = Right vp) -> + all (\seg => Prelude.String.length seg <= 255) (splitPath path) = True + +||| OWED: a validated path contains no null bytes (`\0`). Witnessed +||| by `validatePath`'s `if any hasNullByte segs then Left "Null +||| byte in path" else ...` guard — the `Right` arm is unreachable +||| when any segment contains a null byte. +||| +||| Held back by the same guard-chain extraction blocker as +||| `validPathBounded`, plus the `unpack` FFI opacity from +||| `sanitizedIsSafe` (the predicate `'\0' `elem` unpack path` does +||| not reduce for abstract `path`). Same blocker family. +||| Discharge alongside `validPathBounded`, or refactor to a +||| `dec*`-style decidable check. export -validPathNoNull : (path : String) -> - (vp : ValidatedPath ** validatePath path = Right vp) -> - not ('\0' `elem` unpack path) = True +0 validPathNoNull : (path : String) -> + (vp : ValidatedPath ** validatePath path = Right vp) -> + not ('\0' `elem` unpack path) = True -------------------------------------------------------------------------------- -- Contained Path Properties -------------------------------------------------------------------------------- -||| Contained path full path starts with base +||| OWED: a `ContainedPath base` value's full path has `base`'s +||| normalised segments as a prefix. Witnessed by +||| `makeContainedPath`'s only `Just`-producing arm calling +||| `safeJoinPaths base rel = Just full`, and `safeJoinPaths`'s +||| only `Just`-producing arm being guarded by `isPrefixOf +||| baseSegs combinedSegs = True`. +||| +||| Held back by the same `splitPath . normalizePath` FFI opacity +||| as `safeJoinNoEscape` / `containedInBase`. The proof +||| composes `safeJoinNoEscape` with the definition of +||| `NoEscape`, but the inner `splitPath . normalizePath` stays +||| stuck on the FFI seam. Same blocker family. Discharge +||| alongside `safeJoinNoEscape`. export -containedStartsWithBase : (base : String) -> (cp : ContainedPath base) -> - isPrefixOf (splitPath (normalizePath base)) - (splitPath (normalizePath (getFullPath cp))) = True +0 containedStartsWithBase : (base : String) -> (cp : ContainedPath base) -> + isPrefixOf (splitPath (normalizePath base)) + (splitPath (normalizePath (getFullPath cp))) = True ||| Making contained path is deterministic public export