From 2deab088ecbe5f5a9348fc5e2cf48827e5094909 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 25 Jul 2026 09:16:46 +0100 Subject: [PATCH] chore: explicit postulate sweep for bodyless declarations (standards#158) --- src/Proven/SafeAPIKey/Proofs.idr | 2 +- src/Proven/SafeArchive/Proofs.idr | 8 +-- src/Proven/SafeArgs/Proofs.idr | 14 ++--- src/Proven/SafeBase64/Proofs.idr | 52 ++++++++--------- src/Proven/SafeBloom/Proofs.idr | 2 +- src/Proven/SafeCSRF/Proofs.idr | 12 ++-- src/Proven/SafeCSV/Proofs.idr | 6 +- src/Proven/SafeCalculator/Proofs.idr | 2 +- src/Proven/SafeChecksum/Proofs.idr | 10 ++-- src/Proven/SafeCommand/Proofs.idr | 2 +- src/Proven/SafeContentType/Proofs.idr | 4 +- src/Proven/SafeCookie/Proofs.idr | 4 +- src/Proven/SafeCrypto/Proofs.idr | 26 ++++----- src/Proven/SafeDSP/Proofs.idr | 2 +- src/Proven/SafeEmail/Proofs.idr | 40 ++++++------- src/Proven/SafeEnv/Proofs.idr | 20 +++---- src/Proven/SafeFile/Proofs.idr | 12 ++-- src/Proven/SafeGPU/Proofs.idr | 2 +- src/Proven/SafeGit/Proofs.idr | 2 +- src/Proven/SafeHKDF/Proofs.idr | 4 +- src/Proven/SafeHTTP/Proofs.idr | 6 +- src/Proven/SafeHeader/Proofs.idr | 14 ++--- src/Proven/SafeHtml/Proofs.idr | 32 +++++------ src/Proven/SafeInput/Proofs.idr | 2 +- src/Proven/SafeJWT/Proofs.idr | 70 +++++++++++------------ src/Proven/SafeJson/Proofs.idr | 10 ++-- src/Proven/SafeML/Proofs.idr | 2 +- src/Proven/SafeMath/Proofs.idr | 4 +- src/Proven/SafeNPU/Proofs.idr | 2 +- src/Proven/SafeNetwork/Proofs.idr | 16 +++--- src/Proven/SafeOTP/Proofs.idr | 10 ++-- src/Proven/SafePassword/Proofs.idr | 42 +++++++------- src/Proven/SafePath/Proofs.idr | 50 ++++++++-------- src/Proven/SafePromptInjection/Proofs.idr | 2 +- src/Proven/SafeRegex/Proofs.idr | 46 +++++++-------- src/Proven/SafeSQL/Proofs.idr | 50 ++++++++-------- src/Proven/SafeSemVer/Proofs.idr | 4 +- src/Proven/SafeString/Proofs.idr | 18 +++--- src/Proven/SafeTOML/Proofs.idr | 28 ++++----- src/Proven/SafeUrl/Proofs.idr | 32 +++++------ src/Proven/SafeXML/Proofs.idr | 28 ++++----- src/Proven/SafeYAML/Proofs.idr | 26 ++++----- 42 files changed, 360 insertions(+), 360 deletions(-) diff --git a/src/Proven/SafeAPIKey/Proofs.idr b/src/Proven/SafeAPIKey/Proofs.idr index ed471a45..4674cc62 100644 --- a/src/Proven/SafeAPIKey/Proofs.idr +++ b/src/Proven/SafeAPIKey/Proofs.idr @@ -105,7 +105,7 @@ fullMaskStructure _ = Refl ||| Discharge once a `DecEq KeyFormat` instance is exposed alongside a ||| Bool-Prop reflection lemma for `==`, or once `mkAPIKeyWithFormat` ||| is refactored to case-split on `decEq key.format expected`. -0 formatMismatchRejected : (expected : KeyFormat) -> (s : String) -> +postulate 0 formatMismatchRejected : (expected : KeyFormat) -> (s : String) -> (key : APIKey) -> mkAPIKey s = Just key -> Not (key.format = expected) -> diff --git a/src/Proven/SafeArchive/Proofs.idr b/src/Proven/SafeArchive/Proofs.idr index 0ef7d1c5..b2092c4e 100644 --- a/src/Proven/SafeArchive/Proofs.idr +++ b/src/Proven/SafeArchive/Proofs.idr @@ -147,13 +147,13 @@ zeroCompressedNonZeroUncompressedIsZipBomb = Refl ||| OWED: A reasonably-compressed entry (ratio 100, well under 1000) ||| is NOT a zip bomb. Blocked on Nat-literal opacity (standards#128). public export -0 modestRatioNotZipBomb : +postulate 0 modestRatioNotZipBomb : isZipBomb (MkArchiveEntry "x" RegularFile 1 100 Nothing) = False ||| OWED: An entry with compression ratio > 1000 IS a zip bomb. Same ||| blocker. public export -0 extremeRatioIsZipBomb : +postulate 0 extremeRatioIsZipBomb : isZipBomb (MkArchiveEntry "x" RegularFile 1 1001 Nothing) = True -------------------------------------------------------------------------------- @@ -201,10 +201,10 @@ symlinkNoTargetNotDangerous = Refl ||| OWED: A path with no special characters has no traversal. Blocked ||| on the String FFI family (`isInfixOf` / `isPrefixOf`). public export -0 plainPathHasNoTraversal : +postulate 0 plainPathHasNoTraversal : hasPathTraversal "normal.txt" = False ||| OWED: A path with ".." has traversal. Same blocker. public export -0 dotDotPathHasTraversal : +postulate 0 dotDotPathHasTraversal : hasPathTraversal "../etc/passwd" = True diff --git a/src/Proven/SafeArgs/Proofs.idr b/src/Proven/SafeArgs/Proofs.idr index 55e55c46..fa901aaf 100644 --- a/src/Proven/SafeArgs/Proofs.idr +++ b/src/Proven/SafeArgs/Proofs.idr @@ -29,14 +29,14 @@ import Data.String ||| Predicate: Argument length is bounded public export data BoundedArg : Nat -> String -> Type where - MkBoundedArg : (maxLen : Nat) -> (arg : String) -> + postulate MkBoundedArg : (maxLen : Nat) -> (arg : String) -> {auto prf : length (unpack arg) <= maxLen = True} -> BoundedArg maxLen arg ||| Predicate: Argument count is bounded public export data BoundedArgCount : Nat -> List String -> Type where - MkBoundedArgCount : (maxCount : Nat) -> (args : List String) -> + postulate MkBoundedArgCount : (maxCount : Nat) -> (args : List String) -> {auto prf : length args <= maxCount = True} -> BoundedArgCount maxCount args @@ -65,7 +65,7 @@ argCountPreventsExhaustion opts count tooMany = () ||| Predicate: Option value is in allowed list public export data AllowedValue : List String -> String -> Type where - MkAllowedValue : (allowed : List String) -> (value : String) -> + postulate MkAllowedValue : (allowed : List String) -> (value : String) -> {auto prf : value `elem` allowed = True} -> AllowedValue allowed value @@ -98,7 +98,7 @@ nonEmptyAllowedRestricts allowed value notEmpty notIn = () ||| Predicate: All required arguments are present public export data RequiredPresent : List ArgSpec -> ParsedArgs -> Type where - MkRequiredPresent : (specs : List ArgSpec) -> (parsed : ParsedArgs) -> + postulate MkRequiredPresent : (specs : List ArgSpec) -> (parsed : ParsedArgs) -> RequiredPresent specs parsed ||| Theorem: Required check prevents missing arguments @@ -150,7 +150,7 @@ parseBool' str = ||| `Eq`-instance reduction lemma for `toLower` are available — or ||| once the parser is refactored to case-split via `DecEq` on a ||| `Recognised` ADT. -0 boolParsingComplete : (s : String) -> +postulate 0 boolParsingComplete : (s : String) -> toLower s `elem` ["true", "yes", "1", "on", "false", "no", "0", "off"] = True -> isJust (parseBool' s) = True @@ -168,7 +168,7 @@ parseBool' str = ||| String FFI primitives are exposed with reflective lemmas, or ||| once the parser is rewritten to fold over a typed `List Digit` ||| with explicit sign handling. -0 intParsingHandlesNegative : (s : String) -> +postulate 0 intParsingHandlesNegative : (s : String) -> isPrefixOf "-" s = True -> all Prelude.Types.isDigit (Data.List.drop 1 (unpack s)) = True -> isJust (parseInteger s) = True @@ -191,7 +191,7 @@ parseNat' str = do ||| a sign-tracking spec lemma, or once `parseNat'` is rewritten ||| without going through `Integer` (e.g. directly folding `Digit` ||| values into `Nat`). -0 natRejectsNegative : (s : String) -> +postulate 0 natRejectsNegative : (s : String) -> isPrefixOf "-" s = True -> parseNat' s = Nothing diff --git a/src/Proven/SafeBase64/Proofs.idr b/src/Proven/SafeBase64/Proofs.idr index 052c3b42..4b30b6a0 100644 --- a/src/Proven/SafeBase64/Proofs.idr +++ b/src/Proven/SafeBase64/Proofs.idr @@ -31,14 +31,14 @@ isValidOutputChar v c = isValidBase64Char v c || isPaddingChar c || ||| Predicate: Output contains only valid Base64 characters public export data ValidBase64Output : Base64Variant -> String -> Type where - MkValidBase64Output : (variant : Base64Variant) -> (s : String) -> + postulate MkValidBase64Output : (variant : Base64Variant) -> (s : String) -> {auto prf : all (isValidOutputChar variant) (unpack s) = True} -> ValidBase64Output variant s ||| Predicate: Encoded length is correct public export data CorrectEncodedLength : Base64Variant -> Nat -> Nat -> Type where - MkCorrectEncodedLength : (variant : Base64Variant) -> + postulate MkCorrectEncodedLength : (variant : Base64Variant) -> (inputLen : Nat) -> (outputLen : Nat) -> {auto prf : outputLen = encodedLength variant inputLen} -> CorrectEncodedLength variant inputLen outputLen @@ -46,7 +46,7 @@ data CorrectEncodedLength : Base64Variant -> Nat -> Nat -> Type where ||| Predicate: Decoded length is correct public export data CorrectDecodedLength : Nat -> Nat -> Nat -> Type where - MkCorrectDecodedLength : (encodedLen : Nat) -> (padding : Nat) -> (outputLen : Nat) -> + postulate MkCorrectDecodedLength : (encodedLen : Nat) -> (padding : Nat) -> (outputLen : Nat) -> {auto prf : outputLen = exactDecodedLength encodedLen padding} -> CorrectDecodedLength encodedLen padding outputLen @@ -57,7 +57,7 @@ data CorrectDecodedLength : Nat -> Nat -> Nat -> Type where ||| Predicate: Encoding is reversible public export data RoundtripSuccess : Base64Variant -> List Bits8 -> Type where - MkRoundtripSuccess : (variant : Base64Variant) -> (bytes : List Bits8) -> + postulate MkRoundtripSuccess : (variant : Base64Variant) -> (bytes : List Bits8) -> {auto prf : decode variant (encodeBytesToString variant bytes) = Ok bytes} -> RoundtripSuccess variant bytes @@ -83,7 +83,7 @@ data RoundtripSuccess : Base64Variant -> List Bits8 -> Type where ||| reflective tactic for `unpack` is available, or by hand-rolling a ||| 64-arm exhaustive case-split over the alphabet (one `Refl` per ||| character). -0 standardAlphabetValid : (c : Char) -> c `elem` unpack standardAlphabet = True -> +postulate 0 standardAlphabetValid : (c : Char) -> c `elem` unpack standardAlphabet = True -> isValidBase64Char Standard c = True ||| OWED: every character in the URL-safe Base64 alphabet @@ -95,7 +95,7 @@ data RoundtripSuccess : Base64Variant -> List Bits8 -> Type where ||| `String` at the type level — same FFI-primitive blocker as ||| `standardAlphabetValid` above. Discharge by the same mechanism ||| (`Data.String` reflective tactic or 64-arm exhaustive case-split). -0 urlSafeAlphabetValid : (c : Char) -> c `elem` unpack urlSafeAlphabet = True -> +postulate 0 urlSafeAlphabetValid : (c : Char) -> c `elem` unpack urlSafeAlphabet = True -> isValidBase64Char URLSafe c = True ||| OWED: the encoder `encodeBytesToString variant bytes` emits only @@ -115,7 +115,7 @@ data RoundtripSuccess : Base64Variant -> List Bits8 -> Type where ||| a `Data.String` `pack`/`unpack` reflective tactic is available, or ||| by lifting the proof to the underlying `List Char` produced before ||| `pack` (which IS reducible by induction on the 6-bit chunking). -0 encodeOutputValid : (variant : Base64Variant) -> (bytes : List Bits8) -> +postulate 0 encodeOutputValid : (variant : Base64Variant) -> (bytes : List Bits8) -> ValidBase64Output variant (encodeBytesToString variant bytes) -------------------------------------------------------------------------------- @@ -142,7 +142,7 @@ paddedLengthCorrect n = Refl ||| product-by-divisor is available, or by direct induction on ||| `(n + 2) `div` 3` using the `divides`/`Mod 0` lemmas from ||| `Data.Nat.Division`. -0 paddedLengthMultipleOf4 : (variant : Base64Variant) -> usesPadding variant = True -> +postulate 0 paddedLengthMultipleOf4 : (variant : Base64Variant) -> usesPadding variant = True -> (n : Nat) -> (encodedLength variant n) `mod` 4 = 0 ||| OWED: `decodedLength encodedLen <= (encodedLen * 3) `div` 4 + 1` @@ -159,7 +159,7 @@ paddedLengthCorrect n = Refl ||| `Bool`-reflective `lteSucc` is wired up, or by hand-writing ||| `decideEq` over the underlying `Nat` to convert the `LTE` proof ||| to its `Bool` form. -0 decodedLengthBound : (encodedLen : Nat) -> +postulate 0 decodedLengthBound : (encodedLen : Nat) -> decodedLength encodedLen <= (encodedLen * 3) `div` 4 + 1 = True ||| OWED: for non-empty input (`n > 0 = True`), `encodedLength variant @@ -179,7 +179,7 @@ paddedLengthCorrect n = Refl ||| available, or by chained applications of `lteMultRight`/ ||| `divLteRight` after refactoring `encodedLength` to expose a ||| `total` divisor. -0 encodingIncreasesLength : (variant : Base64Variant) -> (n : Nat) -> n > 0 = True -> +postulate 0 encodingIncreasesLength : (variant : Base64Variant) -> (n : Nat) -> n > 0 = True -> encodedLength variant n >= n = True -------------------------------------------------------------------------------- @@ -206,7 +206,7 @@ paddedLengthCorrect n = Refl ||| `List Bits8 -> List (Fin 64) -> List Char -> List (Fin 64) -> ||| List Bits8` decomposition where each leg IS reducible by ||| structural induction. -0 roundtripCorrect : (variant : Base64Variant) -> (bytes : List Bits8) -> +postulate 0 roundtripCorrect : (variant : Base64Variant) -> (bytes : List Bits8) -> decode variant (encodeBytesToString variant bytes) = Ok bytes ||| OWED: round-trip on the empty input, `decode variant @@ -224,7 +224,7 @@ paddedLengthCorrect n = Refl ||| the same mechanism, or as a one-off `Refl` once the encoder's ||| `pack`/`unpack` wrappers are reduced manually via a `Data.String` ||| reflective tactic. -0 roundtripEmpty : (variant : Base64Variant) -> +postulate 0 roundtripEmpty : (variant : Base64Variant) -> decode variant (encodeBytesToString variant []) = Ok [] ||| OWED: round-trip on a single byte, `decode variant @@ -242,7 +242,7 @@ paddedLengthCorrect n = Refl ||| as `roundtripCorrect`. Discharge once a `Data.Bits` reflective ||| tactic for `shiftL`/`shiftR`/`.&.` is available alongside the ||| `Data.String` `pack`/`unpack` tactic. -0 roundtripSingleByte : (variant : Base64Variant) -> (b : Bits8) -> +postulate 0 roundtripSingleByte : (variant : Base64Variant) -> (b : Bits8) -> decode variant (encodeBytesToString variant [b]) = Ok [b] ||| OWED: string-level round-trip, `decodeToString variant @@ -258,7 +258,7 @@ paddedLengthCorrect n = Refl ||| and `SafeHtml.escapePreservesNoLT`. Discharge once a ||| `Data.String` reflective tactic exposes `pack (unpack s) = s` and ||| `roundtripCorrect` is itself discharged. -0 roundtripString : (variant : Base64Variant) -> (s : String) -> +postulate 0 roundtripString : (variant : Base64Variant) -> (s : String) -> decodeToString variant (encodeStringToString variant s) = Ok s -------------------------------------------------------------------------------- @@ -281,7 +281,7 @@ paddedLengthCorrect n = Refl ||| `Data.String` reflective tactic exposes `length (unpack (pack ||| xs)) = length xs` (i.e. `pack`/`unpack` preserve length), then ||| `Refl` closes against the shared chunking step. -0 variantsEqualLength : (bytes : List Bits8) -> +postulate 0 variantsEqualLength : (bytes : List Bits8) -> length (unpack (encodeBytesToString Standard bytes)) = length (unpack (encodeBytesToString URLSafe bytes)) @@ -298,7 +298,7 @@ paddedLengthCorrect n = Refl ||| True`. Same blocker family as `decodedLengthBound`. Discharge by ||| the same mechanism (`Data.String` `unpack` + `Data.Nat`/`Bool` ||| `lte` reflective tactics). -0 noPadShorter : (bytes : List Bits8) -> +postulate 0 noPadShorter : (bytes : List Bits8) -> let standardLen = length (unpack (encodeBytesToString Standard bytes)) noPadLen = length (unpack (encodeBytesToString URLSafeNoPad bytes)) in noPadLen <= standardLen = True @@ -326,7 +326,7 @@ paddedLengthCorrect n = Refl ||| canonical Idris2 enhancement #2400-series), or by routing the ||| scrutinee through a `decideEq`-style helper that returns the ||| equation explicitly. -0 decodeNeverCrashes : (variant : Base64Variant) -> (input : String) -> +postulate 0 decodeNeverCrashes : (variant : Base64Variant) -> (input : String) -> Either (err : Base64Error ** decode variant input = Err err) (bytes : List Bits8 ** decode variant input = Ok bytes) @@ -346,7 +346,7 @@ paddedLengthCorrect n = Refl ||| reflective tactic for `unpack`/`elem` is available, or by ||| refactoring the decoder to return a `Dec`-style witness alongside ||| each rejection. -0 invalidCharDetected : (variant : Base64Variant) -> (input : String) -> +postulate 0 invalidCharDetected : (variant : Base64Variant) -> (input : String) -> (c : Char) -> (pos : Nat) -> c `elem` unpack input = True -> not (isValidBase64Char variant c) = True -> @@ -374,7 +374,7 @@ index' (S k) (_ :: xs) = index' k xs ||| `invalidCharDetected`. Discharge once a `Data.String` reflective ||| tactic for `unpack` / `index'` is available, or by refactoring ||| `decode` to thread an explicit position-validation `Dec` witness. -0 invalidPaddingDetected : (input : String) -> +postulate 0 invalidPaddingDetected : (input : String) -> -- Padding not at end (pos : Nat) -> pos < (length (unpack input) `minus` 2) = True -> index' pos (unpack input) = Just '=' -> @@ -399,7 +399,7 @@ index' (S k) (_ :: xs) = index' k xs ||| `length . unpack . pack = length` and a `Data.List1` `split` ||| reflective tactic is available, or by inductive proof over the ||| encoder's line-wrap loop counter. -0 mimeLineBreaksCorrect : (bytes : List Bits8) -> +postulate 0 mimeLineBreaksCorrect : (bytes : List Bits8) -> let encoded = encodeBytesToString MIME bytes lines = forget (split (== '\n') encoded) in all (\l => length (unpack l) <= mimeLineLength + 1) lines = True @@ -423,7 +423,7 @@ stripWhitespace s = pack (filter (not . isBase64Whitespace) (unpack s)) ||| tactic exposes `pack (filter p (unpack s))` as a `Refl`-able ||| operation, or by refactoring `decode MIME` to take the already- ||| stripped `String` as an explicit pre-condition. -0 mimeIgnoresWhitespace : (encoded : String) -> (withWs : String) -> +postulate 0 mimeIgnoresWhitespace : (encoded : String) -> (withWs : String) -> stripWhitespace withWs = encoded -> decode MIME withWs = decode MIME encoded @@ -446,7 +446,7 @@ stripWhitespace s = pack (filter (not . isBase64Whitespace) (unpack s)) ||| tactic for `pack`/`unpack` is available, or by lifting the proof ||| to the underlying pre-`pack` `List Char` where the alphabet table ||| lookup IS reducible (one `Refl` per Fin 64 index). -0 urlSafeContainsNoUnsafe : (bytes : List Bits8) -> +postulate 0 urlSafeContainsNoUnsafe : (bytes : List Bits8) -> let encoded = encodeBytesToString URLSafe bytes in all (\c => c /= '+' && c /= '/') (unpack encoded) = True @@ -467,7 +467,7 @@ stripWhitespace s = pack (filter (not . isBase64Whitespace) (unpack s)) ||| or by lifting to the pre-`pack` `List (Fin 64)` representation ||| and case-splitting on whether `62 \`elem\` indices` or ||| `63 \`elem\` indices`. -0 standardMayContainUnsafe : (bytes : List Bits8) -> +postulate 0 standardMayContainUnsafe : (bytes : List Bits8) -> Either ('+' `elem` unpack (encodeBytesToString Standard bytes) = True) (Either ('/' `elem` unpack (encodeBytesToString Standard bytes) = True) (all (\c => c /= '+' && c /= '/') (unpack (encodeBytesToString Standard bytes)) = True)) @@ -494,7 +494,7 @@ stripWhitespace s = pack (filter (not . isBase64Whitespace) (unpack s)) ||| `Data.Nat.Division` `divides`-elimination lemmas after ||| introducing `(k : Nat) ** n = 3 * k` from the `n `mod` 3 = 0` ||| hypothesis. -0 threeToFourRatio : (n : Nat) -> (n `mod` 3 = 0) = True -> +postulate 0 threeToFourRatio : (n : Nat) -> (n `mod` 3 = 0) = True -> encodedLength Standard n = (n `div` 3) * 4 ||| Count padding characters in a string @@ -520,7 +520,7 @@ countPadding s = length (filter (== '=') (unpack s)) ||| is available alongside a `Data.Nat` `mod`-elimination tactic, or ||| by case-splitting on `n `mod` 3 ∈ {0,1,2}` and lifting to the ||| pre-`pack` `List Char` where padding emission IS reducible. -0 paddingMatchesRemainder : (variant : Base64Variant) -> usesPadding variant = True -> +postulate 0 paddingMatchesRemainder : (variant : Base64Variant) -> usesPadding variant = True -> (n : Nat) -> let remainder = n `mod` 3 encoded = encodeBytesToString variant (replicate n 0) @@ -544,7 +544,7 @@ countPadding s = length (filter (== '=') (unpack s)) ||| `roundtripCorrect` is discharged: the proof body is then a pair ||| of `roundtripCorrect variant bytes1` and `roundtripCorrect ||| variant bytes2`. -0 segmentedRoundtrip : (variant : Base64Variant) -> (bytes1 : List Bits8) -> (bytes2 : List Bits8) -> +postulate 0 segmentedRoundtrip : (variant : Base64Variant) -> (bytes1 : List Bits8) -> (bytes2 : List Bits8) -> let enc1 = encodeBytesToString variant bytes1 enc2 = encodeBytesToString variant bytes2 in (decode variant enc1 = Ok bytes1, diff --git a/src/Proven/SafeBloom/Proofs.idr b/src/Proven/SafeBloom/Proofs.idr index e8622abc..bfc820be 100644 --- a/src/Proven/SafeBloom/Proofs.idr +++ b/src/Proven/SafeBloom/Proofs.idr @@ -169,6 +169,6 @@ intersectionPreservesHashes a b c prf with (a.size /= b.size || a.numHashes /= b ||| (`ord`, `unpack`) that Idris2 0.8.0 cannot type-level reduce; the ||| claim therefore lives as an explicit, named assumption. public export -0 noFalseNegatives : +postulate 0 noFalseNegatives : (v : String) -> (bf : BloomFilter) -> LT 0 bf.size -> LT 0 bf.numHashes -> isInfixOf v (insert v bf) = True diff --git a/src/Proven/SafeCSRF/Proofs.idr b/src/Proven/SafeCSRF/Proofs.idr index f2535203..aed4c158 100644 --- a/src/Proven/SafeCSRF/Proofs.idr +++ b/src/Proven/SafeCSRF/Proofs.idr @@ -53,7 +53,7 @@ import Data.List ||| directly so the length-equality and per-character comparison are ||| both type-level structural. public export -0 constantTimeEqRefl : (s : String) -> constantTimeEqual s s = True +postulate 0 constantTimeEqRefl : (s : String) -> constantTimeEqual s s = True ||| OWED: `constantTimeEqual a b = constantTimeEqual b a` for every ||| `a, b : String`. Operationally true because the length-inequality @@ -78,7 +78,7 @@ public export ||| awaits a `Data.Char.eqCharSym` reflective lemma symmetric to ||| `Boj.SafetyLemmas.charEqSym`. public export -0 constantTimeEqSym : (a, b : String) -> constantTimeEqual a b = constantTimeEqual b a +postulate 0 constantTimeEqSym : (a, b : String) -> constantTimeEqual a b = constantTimeEqual b a ||| OWED: if `Not (length a = length b)` then ||| `constantTimeEqual a b = False`. Operationally true because the @@ -103,7 +103,7 @@ public export ||| is refactored to take a `LengthEq`-tagged input (push the ||| length equality into the type and remove the runtime guard). public export -0 differentLengthUnequal : (a, b : String) -> +postulate 0 differentLengthUnequal : (a, b : String) -> Not (length a = length b) -> constantTimeEqual a b = False @@ -130,7 +130,7 @@ public export ||| `constantTimeEqRefl → tokenValidatesSelf`); the proof body is ||| then `constantTimeEqRefl (tokenString tok)`. public export -0 tokenValidatesSelf : (tok : CSRFToken) -> validateToken tok (tokenString tok) = True +postulate 0 tokenValidatesSelf : (tok : CSRFToken) -> validateToken tok (tokenString tok) = True ||| OWED: `validateDoubleSubmit (MkDoubleSubmit val val) = True` for ||| every `val : String`. By unfolding, @@ -147,7 +147,7 @@ public export ||| Discharge once `constantTimeEqRefl` is discharged; the proof ||| body is then `constantTimeEqRefl val`. public export -0 identicalDoubleSubmitValid : (val : String) -> +postulate 0 identicalDoubleSubmitValid : (val : String) -> validateDoubleSubmit (MkDoubleSubmit val val) = True ||| OWED: if `validateToken tok submitted = False` then @@ -178,7 +178,7 @@ public export ||| or (b) a Bool-Prop reflective tactic exposes `validateToken`'s ||| reduction. Recorded as OWED until one of those lands. public export -0 fullValidationRequiresToken : (tok : CSRFToken) -> (submitted : String) -> +postulate 0 fullValidationRequiresToken : (tok : CSRFToken) -> (submitted : String) -> (origins : List String) -> (origin : String) -> validateToken tok submitted = False -> fullValidation tok submitted origins origin = False diff --git a/src/Proven/SafeCSV/Proofs.idr b/src/Proven/SafeCSV/Proofs.idr index 42608968..6e05367e 100644 --- a/src/Proven/SafeCSV/Proofs.idr +++ b/src/Proven/SafeCSV/Proofs.idr @@ -164,15 +164,15 @@ columnByNameFromEmpty _ = Refl ||| OWED: Default delimiter is comma. public export -0 defaultDelimiterIsComma : defaultOptions.delimiter = ',' +postulate 0 defaultDelimiterIsComma : defaultOptions.delimiter = ',' ||| OWED: Default quote character is double-quote. public export -0 defaultQuoteIsDoubleQuote : defaultOptions.quote = '"' +postulate 0 defaultQuoteIsDoubleQuote : defaultOptions.quote = '"' ||| OWED: Default escape character matches quote character (RFC 4180). public export -0 defaultEscapeMatchesQuote : defaultOptions.escape = defaultOptions.quote +postulate 0 defaultEscapeMatchesQuote : defaultOptions.escape = defaultOptions.quote -------------------------------------------------------------------------------- -- Constructor-form witnesses of the same facts diff --git a/src/Proven/SafeCalculator/Proofs.idr b/src/Proven/SafeCalculator/Proofs.idr index ce7c83d5..43cb3677 100644 --- a/src/Proven/SafeCalculator/Proofs.idr +++ b/src/Proven/SafeCalculator/Proofs.idr @@ -36,4 +36,4 @@ module Proven.SafeCalculator.Proofs ||| `Proven.SafeMath.Proofs` baseline is repaired this file should be ||| rewritten with concrete proofs of the items above. public export -0 safeCalculatorProofsAwaitBaselineRepair : () +postulate 0 safeCalculatorProofsAwaitBaselineRepair : () diff --git a/src/Proven/SafeChecksum/Proofs.idr b/src/Proven/SafeChecksum/Proofs.idr index 2f36cfe5..6017be6c 100644 --- a/src/Proven/SafeChecksum/Proofs.idr +++ b/src/Proven/SafeChecksum/Proofs.idr @@ -119,24 +119,24 @@ xorChecksumEmpty = Refl ||| OWED: `sumChecksum []` = 0. Held back by `Integral Nat`'s `mod` ||| not reducing `0 \`mod\` 256 = 0` by Refl under Idris2 0.8.0. public export -0 sumChecksumEmpty : sumChecksum [] = 0 +postulate 0 sumChecksumEmpty : sumChecksum [] = 0 ||| OWED: `twosComplement []` = 0. Same blocker as `sumChecksumEmpty`. public export -0 twosComplementEmpty : twosComplement [] = 0 +postulate 0 twosComplementEmpty : twosComplement [] = 0 ||| OWED: at least one known-valid card-number passes Luhn. Discharge ||| requires reasoning through `unpack`/`ord` String FFI primitives. public export -0 luhnValidatesKnownGood : +postulate 0 luhnValidatesKnownGood : validateLuhn "4111111111111111" = True ||| OWED: at least one known-valid ISBN-10 passes its validator. public export -0 isbn10ValidatesKnownGood : +postulate 0 isbn10ValidatesKnownGood : validateISBN10 "0306406152" = True ||| OWED: at least one known-valid ISBN-13 passes its validator. public export -0 isbn13ValidatesKnownGood : +postulate 0 isbn13ValidatesKnownGood : validateISBN13 "9780306406157" = True diff --git a/src/Proven/SafeCommand/Proofs.idr b/src/Proven/SafeCommand/Proofs.idr index 371abc18..5d415158 100644 --- a/src/Proven/SafeCommand/Proofs.idr +++ b/src/Proven/SafeCommand/Proofs.idr @@ -156,6 +156,6 @@ redirectInjectionRejected = Refl ||| erased, named, and justified rather than hidden. Discharging it ||| needs an `unpack`/`all` bridge lemma (tracked in PROOF-NEEDS.md). public export -0 validNameCharsBridge : (s : String) +postulate 0 validNameCharsBridge : (s : String) -> isValidCommandName s = True -> all isValidCommandChar (unpack s) = True \ No newline at end of file diff --git a/src/Proven/SafeContentType/Proofs.idr b/src/Proven/SafeContentType/Proofs.idr index b22ef930..785557fa 100644 --- a/src/Proven/SafeContentType/Proofs.idr +++ b/src/Proven/SafeContentType/Proofs.idr @@ -24,7 +24,7 @@ import Data.Maybe ||| Predicate: String is valid token public export data ValidMediaToken : String -> Type where - MkValidMediaToken : (token : String) -> + postulate MkValidMediaToken : (token : String) -> {auto prf : isValidToken token = True} -> ValidMediaToken token @@ -58,7 +58,7 @@ spaceNotTokenChar = Refl ||| Predicate: Type is bounded public export data BoundedType : Nat -> String -> Type where - MkBoundedType : (maxLen : Nat) -> (t : String) -> + postulate MkBoundedType : (maxLen : Nat) -> (t : String) -> {auto prf : length (unpack t) <= maxLen = True} -> BoundedType maxLen t diff --git a/src/Proven/SafeCookie/Proofs.idr b/src/Proven/SafeCookie/Proofs.idr index c717459e..58e39651 100644 --- a/src/Proven/SafeCookie/Proofs.idr +++ b/src/Proven/SafeCookie/Proofs.idr @@ -24,7 +24,7 @@ import Data.String ||| Predicate: Cookie value has no injection characters public export data NoInjection : String -> Type where - MkNoInjection : (value : String) -> + postulate MkNoInjection : (value : String) -> {auto prf : not (hasInjectionChar value) = True} -> NoInjection value @@ -118,7 +118,7 @@ strictSameSiteStrict = Refl ||| Predicate: Cookie name is bounded public export data BoundedName : Nat -> String -> Type where - MkBoundedName : (maxLen : Nat) -> (name : String) -> + postulate MkBoundedName : (maxLen : Nat) -> (name : String) -> {auto prf : length (unpack name) <= maxLen = True} -> BoundedName maxLen name diff --git a/src/Proven/SafeCrypto/Proofs.idr b/src/Proven/SafeCrypto/Proofs.idr index a1ab1bbe..3d9e46f8 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 -0 constantTimeRefl : (d : ByteVector n) -> digestEq d d = True +postulate 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 @@ public export ||| stdlib). Same blocker family as `constantTimeRefl`. Discharge ||| once `Data.Bits` exposes `xorCommutative : (x, y : Bits8) -> x \`xor\` y = y \`xor\` x`. public export -0 constantTimeSym : (d1, d2 : ByteVector n) -> +postulate 0 constantTimeSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1 -------------------------------------------------------------------------------- @@ -158,13 +158,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 -0 digestEqRefl : (d : ByteVector n) -> digestEq d d = True +postulate 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 -0 digestEqSym : (d1, d2 : ByteVector n) -> digestEq d1 d2 = digestEq d2 d1 +postulate 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 +176,7 @@ public export ||| Discharge once `Data.Bits` exposes the cancellation lemma OR once ||| `digestEq` is refactored to recurse via `decEq` element-wise. public export -0 differentDigestsUnequal : (d1, d2 : ByteVector n) -> +postulate 0 differentDigestsUnequal : (d1, d2 : ByteVector n) -> Not (d1 = d2) -> digestEq d1 d2 = False @@ -198,7 +198,7 @@ public export ||| index, or (b) refactoring the return type so the length witness ||| is exposed without case-pattern reduction. public export -0 randomBytesLength : (n : Nat) -> +postulate 0 randomBytesLength : (n : Nat) -> case randomBytes n of Right (MkByteVec v) => length v = n Left _ => () @@ -213,7 +213,7 @@ public export ||| modelled propositionally and `modLT : (a, b : Nat) -> IsSucc b -> LT (a \`mod\` b) b` ||| is available in `Data.Nat`. public export -0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} -> +postulate 0 randomNatBounded : (max : Nat) -> {auto ok : IsSucc max} -> case randomNat max of Right n => LT n max Left _ => () @@ -225,7 +225,7 @@ public export ||| reasoning. Same FFI + `Data.Nat` blocker family. Discharge ||| together with `randomNatBounded`. public export -0 randomRangeBounded : (mn, mx : Nat) -> {auto ok : LTE mn mx} -> +postulate 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 +245,7 @@ public export ||| `Not (c1 = c2)` for 0.8.0 (`/=` returns `Bool`). Discharge once ||| `Data.Bits` exposes the requisite cast/shift round-trip lemmas. public export -0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) -> +postulate 0 counterNonceUnique : (pfx : ByteVec 8) -> (c1, c2 : Bits64) -> Not (c1 = c2) -> Not (counterNonce pfx c1 = counterNonce pfx c2) @@ -254,7 +254,7 @@ public export ||| `randomBytesLength` lifted through the rename. Same FFI entropy ||| opacity blocker; discharge together with `randomBytesLength`. public export -0 freshNonceSize : (n : Nat) -> +postulate 0 freshNonceSize : (n : Nat) -> case freshNonce n of Right (MkByteVec v) => length v = n Left _ => () @@ -275,7 +275,7 @@ public export ||| once a `String`-FFI reflective tactic or pack/unpack length ||| lemma is available. public export -0 tokenLengthApprox : (bytes : Nat) -> +postulate 0 tokenLengthApprox : (bytes : Nat) -> case randomToken bytes of Right s => LTE (length s) ((bytes * 4 `div` 3) + 3) Left _ => () @@ -289,7 +289,7 @@ public export ||| opacity blocker as `tokenLengthApprox`. Discharge together with ||| `tokenLengthApprox` once the pack/unpack length lemma lands. public export -0 uuidLength : case randomUUID of +postulate 0 uuidLength : case randomUUID of Right s => length s = 36 Left _ => () @@ -331,5 +331,5 @@ hexEncodeDeterministic _ _ = Refl ||| concrete `bytesToHex`, AND (b) the `String`-FFI reflective ||| tactic / pack-length lemma. public export -0 hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) -> +postulate 0 hexEncodeEvenLength : (bytesToHex : List Bits8 -> String) -> (bs : List Bits8) -> mod (length (bytesToHex bs)) 2 = 0 diff --git a/src/Proven/SafeDSP/Proofs.idr b/src/Proven/SafeDSP/Proofs.idr index 4e28db28..8d4ced7a 100644 --- a/src/Proven/SafeDSP/Proofs.idr +++ b/src/Proven/SafeDSP/Proofs.idr @@ -23,4 +23,4 @@ module Proven.SafeDSP.Proofs ||| Sentinel for the upstream `Data.Nat.Division` baseline-rot blocker. public export -0 safeDSPProofsAwaitBaselineRepair : () +postulate 0 safeDSPProofsAwaitBaselineRepair : () diff --git a/src/Proven/SafeEmail/Proofs.idr b/src/Proven/SafeEmail/Proofs.idr index b49d9984..4a2f747a 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`. -0 parseNoAtFails : parseEmail "noatsign" = Nothing +postulate 0 parseNoAtFails : parseEmail "noatsign" = Nothing -------------------------------------------------------------------------------- -- Validation Properties @@ -78,7 +78,7 @@ parseDeterministic s = Refl ||| record-projection reduction" comment was incorrect — it did not ||| type-check under Idris2 0.8.0.) public export -0 validResultIsValid : validResult.isValid = True +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 @@ -126,7 +126,7 @@ combineValidValid (MkValidationResult True _) (MkValidationResult True _) Refl R ||| Parsed email always contains @ public export data ContainsAt : String -> Type where - MkContainsAt : (s : String) -> (prf : '@' `elem` unpack s = True) -> ContainsAt s + postulate 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 +140,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`. -0 parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s +postulate 0 parsedContainsAt : (s : String) -> isJust (parseEmail s) = True -> ContainsAt s ||| Local part length bound public export data ValidLocalLength : String -> Type where - MkValidLocalLength : (local : String) -> LTE (length local) 64 -> ValidLocalLength local + postulate MkValidLocalLength : (local : String) -> LTE (length local) 64 -> ValidLocalLength local ||| Domain length bound public export data ValidDomainLength : String -> Type where - MkValidDomainLength : (domain : String) -> LTE (length domain) 253 -> ValidDomainLength domain + postulate MkValidDomainLength : (domain : String) -> LTE (length domain) 253 -> ValidDomainLength domain ||| Total email length bound public export data ValidTotalLength : String -> Type where - MkValidTotalLength : (email : String) -> LTE (length email) 254 -> ValidTotalLength email + postulate MkValidTotalLength : (email : String) -> LTE (length email) 254 -> ValidTotalLength email -------------------------------------------------------------------------------- -- Normalization Properties @@ -173,7 +173,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`). -0 normalizeIdempotent : (email : ParsedEmail) -> +postulate 0 normalizeIdempotent : (email : ParsedEmail) -> toLower email.domain = toLower (toLower email.domain) ||| Normalized emails with same local and domain are equal (trivial @@ -193,7 +193,7 @@ normalizedEquality e1 e2 _ prf = prf ||| Sanitized string contains no newlines public export data NoNewlines : String -> Type where - MkNoNewlines : (s : String) -> + postulate MkNoNewlines : (s : String) -> all (\c => c /= '\n' && c /= '\r') (unpack s) = True -> NoNewlines s @@ -217,7 +217,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. -0 sanitizeRemovesNewlinesLemma : (s : String) -> +postulate 0 sanitizeRemovesNewlinesLemma : (s : String) -> all (\c => c /= '\n' && c /= '\r') (filter (\c => c /= '\n' && c /= '\r' && c /= '\0') (unpack s)) = True @@ -234,7 +234,7 @@ sanitizeForHeader str = pack (filter isHeaderSafe (unpack str)) ||| (2) the upstream `sanitizeRemovesNewlinesLemma` is itself OWED. ||| Discharge once both are discharged. public export -0 sanitizeRemovesNewlines : (s : String) -> +postulate 0 sanitizeRemovesNewlines : (s : String) -> NoNewlines (sanitizeForHeader s) -------------------------------------------------------------------------------- @@ -253,7 +253,7 @@ public export ||| 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. -0 filterValidCorrect : (emails : List String) -> +postulate 0 filterValidCorrect : (emails : List String) -> all (\e => (validateEmailFull e).isValid) (filterValid emails) = True uniqueEmails : List ParsedEmail -> List ParsedEmail @@ -271,7 +271,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. -0 uniqueNoDuplicates : (emails : List ParsedEmail) -> +postulate 0 uniqueNoDuplicates : (emails : List ParsedEmail) -> LTE (length (uniqueEmails emails)) (length emails) -------------------------------------------------------------------------------- @@ -290,7 +290,7 @@ uniqueEmails = nubBy (\e1, e2 => toLower (e1.localPart ++ "@" ++ e1.domain) == ||| as SafeTOML's `isScalarCorrect` Bool-LEM gap. Discharge with a ||| one-line case-split on `isFreeEmail domain`. public export -0 freeEmailExhaustive : (domain : String) -> +postulate 0 freeEmailExhaustive : (domain : String) -> Either (isFreeEmail domain = True) (isFreeEmail domain = False) ||| OWED: `checkCommonTypos "gmial.com"` returns the @@ -305,7 +305,7 @@ public export ||| `normalizeIdempotent` and `parseNoAtFails`. Discharge once the ||| String FFI is reflectively modelled, or by refactoring ||| `checkCommonTypos` to operate on `List Char`. -0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue +postulate 0 typoCheckFindsKnown : checkCommonTypos "gmial.com" = addIssue (MkValidationIssue Warning "W010" "Possible typo - did you mean gmail.com?") validResult @@ -325,7 +325,7 @@ public export ||| by the `addIssue` Bool-reduction gap shared with ||| `errorMakesInvalid`. Same family as `parseNoAtFails`. Discharge ||| once the String FFI is reflectively modelled. -0 validLocalNoStartDot : (local : String) -> +postulate 0 validLocalNoStartDot : (local : String) -> (validateLocalPart local).isValid = True -> isPrefixOf "." local = False @@ -335,7 +335,7 @@ public export ||| when `isSuffixOf "." local = True`. Held back by the same ||| String-FFI / Bool-reduction blockers; discharged in the same ||| stroke. -0 validLocalNoEndDot : (local : String) -> +postulate 0 validLocalNoEndDot : (local : String) -> (validateLocalPart local).isValid = True -> isSuffixOf "." local = False @@ -348,7 +348,7 @@ public export ||| `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`). -0 validDomainHasLabel : (domain : String) -> +postulate 0 validDomainHasLabel : (domain : String) -> (validateDomain domain).isValid = True -> LTE 1 (length (forget (split (== '.') domain))) @@ -368,7 +368,7 @@ public export ||| `combineValidValid` plus the `foldl combineResults` invariant ||| (which `Data.List` does not expose as a Refl in Idris2 0.8.0). ||| Discharge alongside `combineValidValid`. -0 comprehensiveCatchesRFC : (s : String) -> +postulate 0 comprehensiveCatchesRFC : (s : String) -> (validateEmailFull s).isValid = False -> (validateComprehensive s).isValid = False @@ -387,6 +387,6 @@ public export ||| `errorMakesInvalid`. Discharge alongside `errorMakesInvalid` + ||| `combineValidValid`, with one extra step-lemma per extra check ||| (each: "this check only emits non-Error issues"). -0 validPassesComprehensive : (s : String) -> +postulate 0 validPassesComprehensive : (s : String) -> (validateEmailFull s).isValid = True -> hasErrors (validateComprehensive s) = False diff --git a/src/Proven/SafeEnv/Proofs.idr b/src/Proven/SafeEnv/Proofs.idr index 52264176..2c7d312c 100644 --- a/src/Proven/SafeEnv/Proofs.idr +++ b/src/Proven/SafeEnv/Proofs.idr @@ -25,7 +25,7 @@ import Data.String ||| Predicate: Name is valid public export data ValidName : String -> Type where - MkValidName : (name : String) -> + postulate MkValidName : (name : String) -> {auto prf : isValidEnvName name = True} -> ValidName name @@ -44,7 +44,7 @@ emptyNameInvalid = Refl ||| once a `Data.String` reflective tactic (or a `packUnpackInverse` ||| equation lemma) is available. export -0 digitStartInvalid : (s : String) -> +postulate 0 digitStartInvalid : (s : String) -> (c : Char) -> isDigit c = True -> isValidEnvName (pack (c :: unpack s)) = False @@ -60,7 +60,7 @@ export ||| commutativity is axiomatised in `gossamer` as `stringNotEqCommut`), ||| or refactor `wellKnownVars` to a sum-of-`DecEq`-checked names list. export -0 wellKnownValid : (name : String) -> +postulate 0 wellKnownValid : (name : String) -> Prelude.elem name Types.wellKnownVars = True -> isValidEnvName name = True @@ -86,7 +86,7 @@ userValid = Refl ||| Predicate: Value is within bounds public export data BoundedValue : Nat -> String -> Type where - MkBoundedValue : (maxLen : Nat) -> (value : String) -> + postulate MkBoundedValue : (maxLen : Nat) -> (value : String) -> {auto prf : length (unpack value) <= maxLen = True} -> BoundedValue maxLen value @@ -101,7 +101,7 @@ data BoundedValue : Nat -> String -> Type where ||| `Data.String`, or refactor `BoundedValue` to take `length value` ||| (a primitive String length) instead of `length (unpack value)`. export -0 emptyBounded : (maxLen : Nat) -> BoundedValue maxLen "" +postulate 0 emptyBounded : (maxLen : Nat) -> BoundedValue maxLen "" ||| Theorem: Bounded value check prevents overflow export @@ -123,7 +123,7 @@ defaultMaxLengthReasonable = Refl ||| Predicate: Name contains sensitive pattern public export data SensitivePatterned : String -> Type where - MkSensitivePatterned : (name : String) -> + postulate MkSensitivePatterned : (name : String) -> {auto prf : isSensitiveName name = True} -> SensitivePatterned name @@ -159,7 +159,7 @@ keySensitive = Refl ||| `if`-on-`Bool`-hypotheses, or refactor `classifyByName` to ||| `case isSensitiveName name of False => Public; True => Sensitive`. export -0 publicClassification : (name : String) -> +postulate 0 publicClassification : (name : String) -> isSensitiveName name = False -> classifyByName name = Public @@ -174,7 +174,7 @@ export ||| `keySensitive` already cover specific witnesses; this is the ||| universally-quantified form. export -0 sensitiveClassification : (name : String) -> +postulate 0 sensitiveClassification : (name : String) -> isSensitiveName name = True -> classifyByName name = Sensitive @@ -228,7 +228,7 @@ blockedPatternsPreventsAccess opts name blocked = () ||| refactor `parseBool` to compare against a pre-lower-cased list ||| without invoking `toLower`. export -0 validBoolParses : (s : String) -> +postulate 0 validBoolParses : (s : String) -> s `elem` ["true", "false", "yes", "no", "1", "0", "on", "off"] = True -> isJust (parseBool s) = True @@ -244,7 +244,7 @@ export ||| or refactor `validIntParses` to call a hand-rolled digit-folder ||| whose proof is straightforward induction over `unpack s`. export -0 validIntParses : (s : String) -> +postulate 0 validIntParses : (s : String) -> all Prelude.Types.isDigit (unpack s) = True -> isJust (parseInteger {a=Integer} s) = True diff --git a/src/Proven/SafeFile/Proofs.idr b/src/Proven/SafeFile/Proofs.idr index 6352e136..fe2b43d2 100644 --- a/src/Proven/SafeFile/Proofs.idr +++ b/src/Proven/SafeFile/Proofs.idr @@ -25,14 +25,14 @@ import Data.String ||| Predicate: Path is bounded public export data BoundedPath : Nat -> String -> Type where - MkBoundedPath : (maxLen : Nat) -> (path : String) -> + postulate MkBoundedPath : (maxLen : Nat) -> (path : String) -> {auto prf : length (unpack path) <= maxLen = True} -> BoundedPath maxLen path ||| Predicate: Path has no traversal public export data NoTraversal : String -> Type where - MkNoTraversal : (path : String) -> + postulate MkNoTraversal : (path : String) -> {auto prf : not (isInfixOf ".." path) = True} -> NoTraversal path @@ -63,7 +63,7 @@ traversalCheckPrevents path hasTraversal = () ||| Predicate: Read size is bounded public export data BoundedRead : Nat -> Nat -> Type where - MkBoundedRead : (limit : Nat) -> (size : Nat) -> + postulate MkBoundedRead : (limit : Nat) -> (size : Nat) -> {auto prf : size <= limit = True} -> BoundedRead limit size @@ -98,7 +98,7 @@ totalReadPrevents opts handle additional tooMuch = () ||| `length (unpack (pack xs)) = length xs`, plus the `List.take` length ||| lemma from `Data.List`. export -0 boundedReadAtMostLimit : (limit : Nat) -> (content : String) -> +postulate 0 boundedReadAtMostLimit : (limit : Nat) -> (content : String) -> length (unpack (pack (take limit (unpack content)))) <= limit = True -------------------------------------------------------------------------------- @@ -108,7 +108,7 @@ export ||| Predicate: Write size is bounded public export data BoundedWrite : Nat -> Nat -> Type where - MkBoundedWrite : (limit : Nat) -> (size : Nat) -> + postulate MkBoundedWrite : (limit : Nat) -> (size : Nat) -> {auto prf : size <= limit = True} -> BoundedWrite limit size @@ -262,7 +262,7 @@ writeTrackingMonotonic h bytes = plusGteOriginal h.bytesWritten bytes ||| reflective tactic gives `isInfixOf "\0" (pack xs) = elem '\0' xs` ||| plus the `filter` exclusion lemma. export -0 sanitizedNoNull : (s : String) -> +postulate 0 sanitizedNoNull : (s : String) -> not (isInfixOf "\0" (Operations.sanitizeContent s)) = True -------------------------------------------------------------------------------- diff --git a/src/Proven/SafeGPU/Proofs.idr b/src/Proven/SafeGPU/Proofs.idr index 961fa3d4..af8ad4fa 100644 --- a/src/Proven/SafeGPU/Proofs.idr +++ b/src/Proven/SafeGPU/Proofs.idr @@ -15,4 +15,4 @@ module Proven.SafeGPU.Proofs %default total public export -0 safeGPUProofsAwaitBaselineRepair : () +postulate 0 safeGPUProofsAwaitBaselineRepair : () diff --git a/src/Proven/SafeGit/Proofs.idr b/src/Proven/SafeGit/Proofs.idr index 640d78dd..740f4434 100644 --- a/src/Proven/SafeGit/Proofs.idr +++ b/src/Proven/SafeGit/Proofs.idr @@ -29,7 +29,7 @@ forbiddenRefCharsAnchor = Refl ||| OWED: `isValidRefName ""` = False (empty refs invalid). Blocked ||| on String FFI (`unpack`, `length` opacity for variable inputs). public export -0 emptyRefNameInvalid : isValidRefName "" = False +postulate 0 emptyRefNameInvalid : isValidRefName "" = False ||| DISCHARGED: `refName (MkGitRef s) = s` (record extraction ||| pass-through). `refName` is a direct pattern match diff --git a/src/Proven/SafeHKDF/Proofs.idr b/src/Proven/SafeHKDF/Proofs.idr index 0f93c9bb..681ce748 100644 --- a/src/Proven/SafeHKDF/Proofs.idr +++ b/src/Proven/SafeHKDF/Proofs.idr @@ -107,7 +107,7 @@ sha512MaxOutput = Refl ||| OWED: `mkHKDFParams` cannot return a `Just` that fails `isValid`. public export -0 mkHKDFParamsSound : +postulate 0 mkHKDFParamsSound : (h : HKDFHash) -> (ikm, salt, info, outLen : Nat) -> (p : HKDFParams) -> mkHKDFParams h ikm salt info outLen = Just p -> isValid p = True @@ -115,7 +115,7 @@ public export ||| OWED: `mkHKDFParams` returns `Nothing` iff the would-be params fail ||| validation. public export -0 mkHKDFParamsRejectsInvalid : +postulate 0 mkHKDFParamsRejectsInvalid : (h : HKDFHash) -> (ikm, salt, info, outLen : Nat) -> mkHKDFParams h ikm salt info outLen = Nothing -> isValid (MkHKDFParams h ikm salt info outLen) = False diff --git a/src/Proven/SafeHTTP/Proofs.idr b/src/Proven/SafeHTTP/Proofs.idr index 37d9e2fd..60e9f1d9 100644 --- a/src/Proven/SafeHTTP/Proofs.idr +++ b/src/Proven/SafeHTTP/Proofs.idr @@ -102,7 +102,7 @@ parseEmptyMethodFails = Refl ||| is available, or by deriving via `boolAnd`/`boolNot` case-split on ||| the `So` witness plus `lteTransitive` (200 <= sc.code < 300 < 400). export -0 successNotError : (sc : StatusCode) -> isSuccess sc = True -> isError sc = False +postulate 0 successNotError : (sc : StatusCode) -> isSuccess sc = True -> isError sc = False ||| OWED: error status codes are not successes. If `isError sc = True` ||| (i.e. `sc.code >= 400`), then `isSuccess sc = False` (i.e. @@ -113,7 +113,7 @@ export ||| Discharge once a `Data.Nat` linear-arithmetic reflective tactic ||| is available, or by case-split on `>=`/`<` with `lteTransitive`. export -0 errorNotSuccess : (sc : StatusCode) -> isError sc = True -> isSuccess sc = False +postulate 0 errorNotSuccess : (sc : StatusCode) -> isError sc = True -> isSuccess sc = False ||| OWED: retryable status codes are errors. 429, 502, 503, 504 are ||| each `>= 400`, so `isRetryable sc = True` implies `isError sc = @@ -126,7 +126,7 @@ export ||| analysis on the `||` chain with literal `lteSucc`-derived proofs ||| `429 >= 400`, `502 >= 400`, `503 >= 400`, `504 >= 400`. export -0 retryableIsError : (sc : StatusCode) -> isRetryable sc = True -> isError sc = True +postulate 0 retryableIsError : (sc : StatusCode) -> isRetryable sc = True -> isError sc = True -------------------------------------------------------------------------------- -- Header Injection Prevention Properties diff --git a/src/Proven/SafeHeader/Proofs.idr b/src/Proven/SafeHeader/Proofs.idr index 20c33299..24baaf67 100644 --- a/src/Proven/SafeHeader/Proofs.idr +++ b/src/Proven/SafeHeader/Proofs.idr @@ -23,7 +23,7 @@ import Data.String ||| Predicate: Header value has no CRLF public export data NoCRLF : String -> Type where - MkNoCRLF : (value : String) -> + postulate MkNoCRLF : (value : String) -> {auto prf : not (hasCRLF value) = True} -> NoCRLF value @@ -46,7 +46,7 @@ crlfCheckPreventsInjection value hasCrlf = () ||| once `HeaderValue` carries an erased `NoCRLF` proof field that this ||| lemma can simply project. export -0 headerValueNoCRLF : (v : HeaderValue) -> not (hasCRLF v.value) = True +postulate 0 headerValueNoCRLF : (v : HeaderValue) -> not (hasCRLF v.value) = True ||| Helper: render a header to its wire format public export @@ -64,7 +64,7 @@ renderHeader h = h.name.originalCase ++ ": " ++ h.value.value ||| tactic supplies `isInfixOf_append : isInfixOf p (a ++ b) = isInfixOf p a || isInfixOf p b`, ||| or via per-character induction on `unpack (renderHeader h)`. export -0 renderedHeaderSafe : (h : Header) -> +postulate 0 renderedHeaderSafe : (h : Header) -> not (hasCRLF (renderHeader h)) = True -------------------------------------------------------------------------------- @@ -74,7 +74,7 @@ export ||| Predicate: Header name is valid token public export data ValidToken : String -> Type where - MkValidToken : (name : String) -> + postulate MkValidToken : (name : String) -> {auto prf : isValidToken name = True} -> ValidToken name @@ -105,7 +105,7 @@ tokenValidationPrevents name invalid = () ||| Predicate: Header value is bounded public export data BoundedValue : Nat -> String -> Type where - MkBoundedValue : (maxLen : Nat) -> (value : String) -> + postulate MkBoundedValue : (maxLen : Nat) -> (value : String) -> {auto prf : length (unpack value) <= maxLen = True} -> BoundedValue maxLen value @@ -152,7 +152,7 @@ totalSizePrevents opts size tooLarge = () ||| hand-rewriting via `plusLteMonotone` over the two `.bounded` ||| projections. export -0 singleHeaderBounded : (h : Header) -> +postulate 0 singleHeaderBounded : (h : Header) -> length (unpack h.name.originalCase) + 2 + length (unpack h.value.value) <= maxNameLength + 2 + maxValueLength = True @@ -248,7 +248,7 @@ strictBlocksDangerous = Refl ||| pre-validated `HeaderName` (so the proof becomes a projection of ||| the constructor invariant). export -0 wellKnownNamesValid : (h : WellKnownHeader) -> +postulate 0 wellKnownNamesValid : (h : WellKnownHeader) -> isValidToken (show h) = True ||| Theorem: Security headers are categorized correctly diff --git a/src/Proven/SafeHtml/Proofs.idr b/src/Proven/SafeHtml/Proofs.idr index eaef6920..90382111 100644 --- a/src/Proven/SafeHtml/Proofs.idr +++ b/src/Proven/SafeHtml/Proofs.idr @@ -17,44 +17,44 @@ import Data.Nat ||| A string that has been HTML-escaped public export data EscapedHtml : Type where - MkEscapedHtml : (content : String) -> EscapedHtml + postulate MkEscapedHtml : (content : String) -> EscapedHtml ||| A string that has been sanitized public export data SanitizedHtml : Type where - MkSanitizedHtml : (content : String) -> SanitizedHtml + postulate MkSanitizedHtml : (content : String) -> SanitizedHtml ||| Proof that escaped HTML does not contain raw '<' public export data NoRawLT : String -> Type where - MkNoRawLT : not (elem '<' (unpack s)) = True -> NoRawLT s + postulate MkNoRawLT : not (elem '<' (unpack s)) = True -> NoRawLT s ||| Proof that escaped HTML does not contain raw '>' public export data NoRawGT : String -> Type where - MkNoRawGT : not (elem '>' (unpack s)) = True -> NoRawGT s + postulate MkNoRawGT : not (elem '>' (unpack s)) = True -> NoRawGT s ||| Proof that escaped HTML does not contain raw '&' (unescaped) public export data NoRawAmpersand : String -> Type where - MkNoRawAmpersand : not (isInfixOf "&" s && not (isInfixOf "&" s || isInfixOf "<" s || isInfixOf ">" s || isInfixOf """ s || isInfixOf "&#" s)) = True -> NoRawAmpersand s + postulate MkNoRawAmpersand : not (isInfixOf "&" s && not (isInfixOf "&" s || isInfixOf "<" s || isInfixOf ">" s || isInfixOf """ s || isInfixOf "&#" s)) = True -> NoRawAmpersand s ||| Proof that content contains no script tags public export data NoScriptTags : String -> Type where - MkNoScriptTags : not (isInfixOf " NoScriptTags s + postulate MkNoScriptTags : not (isInfixOf " NoScriptTags s ||| Proof that a URL has a safe scheme (no javascript:, data:, vbscript:) public export data SafeScheme : String -> Type where - MkSafeScheme : not (isPrefixOf "javascript:" (toLower s) || + postulate MkSafeScheme : not (isPrefixOf "javascript:" (toLower s) || isPrefixOf "vbscript:" (toLower s) || isPrefixOf "data:" (toLower s)) = True -> SafeScheme s ||| Combined XSS-safety proof public export data XSSSafe : String -> Type where - MkXSSSafe : NoRawLT s -> NoRawGT s -> NoScriptTags s -> XSSSafe s + postulate MkXSSSafe : NoRawLT s -> NoRawGT s -> NoScriptTags s -> XSSSafe s ||| Helper: escape a single HTML character public export @@ -81,7 +81,7 @@ escapeChar c = singleton c ||| Discharge once a `Data.String` reflective tactic or per-character ||| induction lemma over `unpack . concat . map` is available. public export -0 escapePreservesNoLT : (s : String) -> (escaped : String) -> +postulate 0 escapePreservesNoLT : (s : String) -> (escaped : String) -> escaped = concat (map escapeChar (unpack s)) -> NoRawLT escaped @@ -89,7 +89,7 @@ public export ||| If a string has no dangerous characters, escaping is a no-op public export data EscapeIdempotent : String -> Type where - MkEscapeIdempotent : NoRawLT s -> NoRawGT s -> NoRawAmpersand s -> + postulate MkEscapeIdempotent : NoRawLT s -> NoRawGT s -> NoRawAmpersand s -> EscapeIdempotent s ||| OWED: for every `input`, the corresponding sanitised `output` @@ -107,13 +107,13 @@ data EscapeIdempotent : String -> Type where ||| `isInfixOf` / `toLower` is available, or a per-character ||| induction lemma over the sanitiser's output construction. public export -0 sanitizeRemovesScripts : (input : String) -> (output : String) -> +postulate 0 sanitizeRemovesScripts : (input : String) -> (output : String) -> NoScriptTags output ||| Proof that attribute escaping prevents quote breakout public export data SafeAttribute : String -> Type where - MkSafeAttribute : not (elem '"' (unpack s)) = True -> + postulate MkSafeAttribute : not (elem '"' (unpack s)) = True -> not (elem '\'' (unpack s)) = True -> SafeAttribute s @@ -121,11 +121,11 @@ data SafeAttribute : String -> Type where public export data WellFormedHtml : Type where ||| Empty document is well-formed - EmptyDoc : WellFormedHtml + postulate EmptyDoc : WellFormedHtml ||| Text content (leaf node) is well-formed - TextNode : EscapedHtml -> WellFormedHtml + postulate TextNode : EscapedHtml -> WellFormedHtml ||| Element with children is well-formed if children are - ValidElement : (tag : String) -> + postulate ValidElement : (tag : String) -> (attrs : List (String, String)) -> (children : List WellFormedHtml) -> WellFormedHtml @@ -133,6 +133,6 @@ data WellFormedHtml : Type where ||| Proof that self-closing tags have no children public export data SelfClosing : String -> Type where - MkSelfClosing : elem tag ["br", "hr", "img", "input", "meta", "link", + postulate MkSelfClosing : elem tag ["br", "hr", "img", "input", "meta", "link", "area", "base", "col", "embed", "source", "track", "wbr"] = True -> SelfClosing tag diff --git a/src/Proven/SafeInput/Proofs.idr b/src/Proven/SafeInput/Proofs.idr index 1be53e11..258e81b6 100644 --- a/src/Proven/SafeInput/Proofs.idr +++ b/src/Proven/SafeInput/Proofs.idr @@ -15,4 +15,4 @@ import Proven.SafeInput ||| an `Eq CharClass` constrained to the nullary constructors is ||| provided. public export -0 safeInputProofsAwaitEqCharClass : () +postulate 0 safeInputProofsAwaitEqCharClass : () diff --git a/src/Proven/SafeJWT/Proofs.idr b/src/Proven/SafeJWT/Proofs.idr index 65f36b8e..64d7dfbc 100644 --- a/src/Proven/SafeJWT/Proofs.idr +++ b/src/Proven/SafeJWT/Proofs.idr @@ -24,30 +24,30 @@ import Data.String ||| Predicate: Algorithm is secure (not 'none') public export data IsSecureAlg : JWTAlgorithm -> Type where - HS256Secure : IsSecureAlg HS256 - HS384Secure : IsSecureAlg HS384 - HS512Secure : IsSecureAlg HS512 - RS256Secure : IsSecureAlg RS256 - RS384Secure : IsSecureAlg RS384 - RS512Secure : IsSecureAlg RS512 - ES256Secure : IsSecureAlg ES256 - ES384Secure : IsSecureAlg ES384 - ES512Secure : IsSecureAlg ES512 - PS256Secure : IsSecureAlg PS256 - PS384Secure : IsSecureAlg PS384 - PS512Secure : IsSecureAlg PS512 - EdDSASecure : IsSecureAlg EdDSA + postulate HS256Secure : IsSecureAlg HS256 + postulate HS384Secure : IsSecureAlg HS384 + postulate HS512Secure : IsSecureAlg HS512 + postulate RS256Secure : IsSecureAlg RS256 + postulate RS384Secure : IsSecureAlg RS384 + postulate RS512Secure : IsSecureAlg RS512 + postulate ES256Secure : IsSecureAlg ES256 + postulate ES384Secure : IsSecureAlg ES384 + postulate ES512Secure : IsSecureAlg ES512 + postulate PS256Secure : IsSecureAlg PS256 + postulate PS384Secure : IsSecureAlg PS384 + postulate PS512Secure : IsSecureAlg PS512 + postulate EdDSASecure : IsSecureAlg EdDSA ||| Predicate: Token has not expired public export data NotExpired : Integer -> Integer -> Type where - MkNotExpired : (exp : Integer) -> (current : Integer) -> + postulate MkNotExpired : (exp : Integer) -> (current : Integer) -> {auto prf : So (current <= exp)} -> NotExpired exp current ||| Predicate: Token is currently valid (nbf <= current <= exp) public export data IsCurrentlyValid : Integer -> Integer -> Integer -> Type where - MkCurrentlyValid : (nbf : Integer) -> (exp : Integer) -> (current : Integer) -> + postulate MkCurrentlyValid : (nbf : Integer) -> (exp : Integer) -> (current : Integer) -> {auto prf1 : So (nbf <= current)} -> {auto prf2 : So (current <= exp)} -> IsCurrentlyValid nbf exp current @@ -55,17 +55,17 @@ data IsCurrentlyValid : Integer -> Integer -> Integer -> Type where ||| Predicate: Signature has been verified public export data SignatureVerified : DecodedJWT -> SigningKey -> Type where - MkSignatureVerified : (jwt : DecodedJWT) -> (key : SigningKey) -> SignatureVerified jwt key + postulate MkSignatureVerified : (jwt : DecodedJWT) -> (key : SigningKey) -> SignatureVerified jwt key ||| Predicate: Claims have been validated public export data ClaimsValidated : JWTClaims -> ValidationOptions -> Type where - MkClaimsValidated : (claims : JWTClaims) -> (opts : ValidationOptions) -> ClaimsValidated claims opts + postulate MkClaimsValidated : (claims : JWTClaims) -> (opts : ValidationOptions) -> ClaimsValidated claims opts ||| Predicate: JWT is fully validated public export data FullyValidated : ValidatedJWT -> Type where - MkFullyValidated : (vjwt : ValidatedJWT) -> FullyValidated vjwt + postulate MkFullyValidated : (vjwt : ValidatedJWT) -> FullyValidated vjwt -------------------------------------------------------------------------------- -- Algorithm Security Proofs @@ -185,7 +185,7 @@ validatedMeansChecked vjwt = MkFullyValidated vjwt ||| or by introducing a generic `ifFalseElim : (if b then x else y) = ||| y -> b = False` and case-splitting on `claims.exp`. public export -0 expValidationSound : (currentTime : Integer) -> (skew : ClockSkew) -> (claims : JWTClaims) -> +postulate 0 expValidationSound : (currentTime : Integer) -> (skew : ClockSkew) -> (claims : JWTClaims) -> isOk (validateExp currentTime skew claims) = True -> (exp : Integer) -> claims.exp = Just exp -> currentTime <= exp + cast skew.expLeeway = True @@ -206,7 +206,7 @@ public export ||| reflective tactic or `ifFalseElim` lemma that closes ||| `expValidationSound`. public export -0 nbfValidationSound : (currentTime : Integer) -> (skew : ClockSkew) -> (claims : JWTClaims) -> +postulate 0 nbfValidationSound : (currentTime : Integer) -> (skew : ClockSkew) -> (claims : JWTClaims) -> isOk (validateNbf currentTime skew claims) = True -> (nbf : Integer) -> claims.nbf = Just nbf -> currentTime >= nbf - cast skew.nbfLeeway = True @@ -230,7 +230,7 @@ public export ||| ships a reflective `strEqSound : (s1 == s2 = True) -> s1 = s2` ||| with the same trust posture as boj-server `SafetyLemmas`. public export -0 issuerValidationSound : (expected : String) -> (claims : JWTClaims) -> +postulate 0 issuerValidationSound : (expected : String) -> (claims : JWTClaims) -> isOk (validateIssuer expected claims) = True -> claims.iss = Just expected @@ -252,7 +252,7 @@ public export ||| (x \`elem\` xs = True) -> ...` for instances whose `(==)` has a ||| Bool-Prop reflection lemma, parameterised by `strEqSound`. public export -0 audienceValidationSound : (expected : String) -> (claims : JWTClaims) -> +postulate 0 audienceValidationSound : (expected : String) -> (claims : JWTClaims) -> isOk (validateAudience expected claims) = True -> expected `elem` getAudienceList claims = True @@ -281,7 +281,7 @@ public export ||| `Dec (KeyValidForAlgorithm key alg)` witness so the ||| precondition is propositional rather than boolean. public export -0 keyMustMatchAlgorithm : (key : SigningKey) -> (jwt : DecodedJWT) -> +postulate 0 keyMustMatchAlgorithm : (key : SigningKey) -> (jwt : DecodedJWT) -> isOk (verifySignature key jwt) = True -> isKeyValidForAlgorithm key jwt.header.alg = True @@ -307,7 +307,7 @@ public export ||| one `Refl` per algorithm constructor — analogous to the ||| explicit enum case-split in `noneNotSecure` above). public export -0 noKeyOnlyForNone : (jwt : DecodedJWT) -> +postulate 0 noKeyOnlyForNone : (jwt : DecodedJWT) -> isOk (verifySignature NoKey jwt) = True -> jwt.header.alg = None @@ -333,7 +333,7 @@ public export ||| derive `False = True` from the guard premise and discharge ||| via `absurd Refl`). public export -0 secretKeyRequiresHMAC : (secret : List Bits8) -> (jwt : DecodedJWT) -> +postulate 0 secretKeyRequiresHMAC : (secret : List Bits8) -> (jwt : DecodedJWT) -> isOk (verifySignature (SecretKey secret) jwt) = True -> isSymmetric jwt.header.alg = True @@ -362,7 +362,7 @@ public export ||| available, plus a hand-rolled induction principle on the ||| `validateRequiredClaims` recursion. public export -0 requiredClaimsPresent : (claims : List String) -> (jwtClaims : JWTClaims) -> +postulate 0 requiredClaimsPresent : (claims : List String) -> (jwtClaims : JWTClaims) -> isOk (validateRequiredClaims claims jwtClaims) = True -> (name : String) -> name `elem` claims = True -> hasRequiredClaim name jwtClaims = True @@ -385,7 +385,7 @@ public export ||| tactic for `<=`/`>` is available, plus a `castNatToInteger` ||| reduction lemma. public export -0 maxAgeValidationSound : (currentTime : Integer) -> (maxAge : Nat) -> (claims : JWTClaims) -> +postulate 0 maxAgeValidationSound : (currentTime : Integer) -> (maxAge : Nat) -> (claims : JWTClaims) -> isOk (validateMaxAge currentTime maxAge claims) = True -> (iat : Integer) -> claims.iat = Just iat -> currentTime - iat <= cast maxAge = True @@ -418,7 +418,7 @@ public export ||| and the `when`/projection opacities are addressed (likely the ||| same `Data.Bool` reflective tactic as `expValidationSound`). public export -0 fullValidationImpliesAll : +postulate 0 fullValidationImpliesAll : (opts : ValidationOptions) -> (currentTime : Integer) -> (jwt : DecodedJWT) -> isOk (validateDecoded opts currentTime jwt) = True -> (opts.validateExp = True -> isOk (validateExp currentTime opts.clockSkew jwt.claims) = True, @@ -454,9 +454,9 @@ public export ||| the proof. Alternatively, hide `MkValidatedJWT` from the public ||| API and re-export only the `validate` smart constructor. public export -0 validatedJWTFromValidation : (vjwt : ValidatedJWT) -> +postulate 0 validatedJWTFromValidation : (vjwt : ValidatedJWT) -> (opts : ValidationOptions ** key : SigningKey ** currentTime : Integer ** - decoded : DecodedJWT ** + postulate decoded : DecodedJWT ** isOk (validate opts key currentTime decoded) = True) -------------------------------------------------------------------------------- @@ -483,7 +483,7 @@ public export ||| lemmas are in place — at that point `rejectNonePreventsNone` ||| closes by a 3-step `rewrite` + `Refl`. public export -0 rejectNonePreventsNone : (opts : ValidationOptions) -> opts.rejectNone = True -> +postulate 0 rejectNonePreventsNone : (opts : ValidationOptions) -> opts.rejectNone = True -> (jwt : DecodedJWT) -> jwt.header.alg = None -> isOk (validateDecoded opts 0 jwt) = False @@ -504,7 +504,7 @@ public export ||| AND `Result`-bind `Err`-propagation. Discharge with the same ||| three reflective lemmas. public export -0 allowedAlgorithmsRestrictive : (opts : ValidationOptions) -> +postulate 0 allowedAlgorithmsRestrictive : (opts : ValidationOptions) -> (alg : JWTAlgorithm) -> not (null opts.allowedAlgorithms) = True -> not (alg `elem` opts.allowedAlgorithms) = True -> (jwt : DecodedJWT) -> jwt.header.alg = alg -> @@ -601,7 +601,7 @@ SafeJWT Security Guarantees: ||| would be ~10 lines and structurally identical to ||| `noneNotSecure`. public export -0 algorithmConfusionPrevented : +postulate 0 algorithmConfusionPrevented : (jwt : DecodedJWT) -> jwt.header.alg = HS256 -> (rsaKey : SigningKey) -> isKeyValidForAlgorithm rsaKey RS256 = True -> isKeyValidForAlgorithm rsaKey HS256 = False @@ -629,7 +629,7 @@ public export ||| posture as gossamer's `stringNotEqCommut` (`%unsafe` + ||| `believe_me ()` over the FFI primitive). public export -0 tokenSubstitutionPrevented : +postulate 0 tokenSubstitutionPrevented : (opts : ValidationOptions) -> opts.requiredIssuer = Just "expected-issuer" -> (jwt : DecodedJWT) -> jwt.claims.iss = Just "malicious-issuer" -> isOk (validateDecoded opts 0 jwt) = False @@ -655,7 +655,7 @@ public export ||| dischargeable — at which point `replayMitigatedWithMaxAge` ||| follows by a 3-step `rewrite` + `Refl`. public export -0 replayMitigatedWithMaxAge : +postulate 0 replayMitigatedWithMaxAge : (opts : ValidationOptions) -> opts.maxAge = Just 300 -> (currentTime : Integer) -> (jwt : DecodedJWT) -> jwt.claims.iat = Just (currentTime - 600) -> -- Token is 10 minutes old diff --git a/src/Proven/SafeJson/Proofs.idr b/src/Proven/SafeJson/Proofs.idr index 7c83cf63..25c55523 100644 --- a/src/Proven/SafeJson/Proofs.idr +++ b/src/Proven/SafeJson/Proofs.idr @@ -393,7 +393,7 @@ anyMatchesTAny (JsonObject _) = Refl ||| This is guaranteed by the structure of the parser using fuel/depth limit public export data ParsingTerminates : String -> Type where - MkParsingTerminates : (s : String) -> (Either ParseError JsonValue) -> + postulate MkParsingTerminates : (s : String) -> (Either ParseError JsonValue) -> ParsingTerminates s ||| For any input string, parsing terminates @@ -408,10 +408,10 @@ parsingTotal s = MkParsingTerminates s (parse s) ||| Data type for well-formed JSON (syntactically valid) public export data WellFormedJson : JsonValue -> Type where - WFNull : WellFormedJson JsonNull - WFBool : (b : Bool) -> WellFormedJson (JsonBool b) - WFNumber : (n : Double) -> WellFormedJson (JsonNumber n) - WFString : (s : String) -> WellFormedJson (JsonString s) + postulate WFNull : WellFormedJson JsonNull + postulate WFBool : (b : Bool) -> WellFormedJson (JsonBool b) + postulate WFNumber : (n : Double) -> WellFormedJson (JsonNumber n) + postulate WFString : (s : String) -> WellFormedJson (JsonString s) WFArray : (arr : List JsonValue) -> Data.List.Quantifiers.All.All WellFormedJson arr -> WellFormedJson (JsonArray arr) diff --git a/src/Proven/SafeML/Proofs.idr b/src/Proven/SafeML/Proofs.idr index 574b99c2..cb49973d 100644 --- a/src/Proven/SafeML/Proofs.idr +++ b/src/Proven/SafeML/Proofs.idr @@ -12,4 +12,4 @@ import Proven.SafeML ||| Sentinel — surface depends on Double comparisons + So-proofs. public export -0 safeMLProofsAwaitDoubleEqDecide : () +postulate 0 safeMLProofsAwaitDoubleEqDecide : () diff --git a/src/Proven/SafeMath/Proofs.idr b/src/Proven/SafeMath/Proofs.idr index a11791c4..2309cb0d 100644 --- a/src/Proven/SafeMath/Proofs.idr +++ b/src/Proven/SafeMath/Proofs.idr @@ -182,7 +182,7 @@ modLtDivisor n (S d) = boundModNatNZ n (S d) ItIsSucc ||| `Data.Nat.Factor.gcdUnproven` (which IS total) and prove agreement ||| with `Data.Nat.gcd` on every input. public export -0 gcdZeroRight : (n : Nat) -> {auto 0 ok : NotBothZero n 0} -> gcd n 0 @{ok} = n +postulate 0 gcdZeroRight : (n : Nat) -> {auto 0 ok : NotBothZero n 0} -> gcd n 0 @{ok} = n ||| OWED: GCD is commutative — `gcd a b = gcd b a`. The base cases ||| (`gcd 0 (S b)` vs `gcd (S b) 0`) would be trivially `Refl` if @@ -200,4 +200,4 @@ public export ||| agreement with `Data.Nat.gcd` on every input — at which point ||| both `gcdZeroRight` and `gcdCommutative` discharge together. public export -0 gcdCommutative : (a, b : Nat) -> {auto 0 ok1 : NotBothZero a b} -> {auto 0 ok2 : NotBothZero b a} -> gcd a b @{ok1} = gcd b a @{ok2} +postulate 0 gcdCommutative : (a, b : Nat) -> {auto 0 ok1 : NotBothZero a b} -> {auto 0 ok2 : NotBothZero b a} -> gcd a b @{ok1} = gcd b a @{ok2} diff --git a/src/Proven/SafeNPU/Proofs.idr b/src/Proven/SafeNPU/Proofs.idr index 16987293..14dbabad 100644 --- a/src/Proven/SafeNPU/Proofs.idr +++ b/src/Proven/SafeNPU/Proofs.idr @@ -9,4 +9,4 @@ module Proven.SafeNPU.Proofs %default total public export -0 safeNPUProofsAwaitBaselineRepair : () +postulate 0 safeNPUProofsAwaitBaselineRepair : () diff --git a/src/Proven/SafeNetwork/Proofs.idr b/src/Proven/SafeNetwork/Proofs.idr index 844de198..7fdc0d0e 100644 --- a/src/Proven/SafeNetwork/Proofs.idr +++ b/src/Proven/SafeNetwork/Proofs.idr @@ -38,7 +38,7 @@ portAlwaysValid p = MkValidPort p ||| is exposed by `Data.Nat`, or `mkPort` is refactored to take the ||| `LTE` proof directly. public export -0 mkPortSucceeds : (n : Nat) -> LTE n 65535 -> IsJust (mkPort n) +postulate 0 mkPortSucceeds : (n : Nat) -> LTE n 65535 -> IsJust (mkPort n) ||| OWED: every CIDR block contains its own network address. Held back ||| by Idris2 0.8.0 not reducing `contains` on an abstract `CIDRBlock`: @@ -48,7 +48,7 @@ public export ||| Discharge once `ipToNat` monotonicity lemmas are proven and a ||| reflective bridge from primitive `>=` to `GTE` is available. public export -0 networkInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (networkAddress cidr) = True +postulate 0 networkInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (networkAddress cidr) = True ||| OWED: every CIDR block contains its own broadcast address. Same ||| blocker family as `networkInOwnCIDR` — `contains` does not reduce @@ -56,13 +56,13 @@ public export ||| Nat `>=`. Discharge once `ipToNat` monotonicity + a `>=`-to-`GTE` ||| reflective bridge are in place. public export -0 broadcastInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (broadcastAddress cidr) = True +postulate 0 broadcastInOwnCIDR : (cidr : CIDRBlock) -> contains cidr (broadcastAddress cidr) = True ||| CIDR subset transitivity: if A is a subset of B and B is a subset of C then A is a subset of C ||| This follows from the transitivity of the containment relation public export data SubsetTransitive : CIDRBlock -> CIDRBlock -> CIDRBlock -> Type where - MkSubsetTransitive : isSubsetOf a b = True -> + postulate MkSubsetTransitive : isSubsetOf a b = True -> isSubsetOf b c = True -> SubsetTransitive a b c @@ -75,7 +75,7 @@ data SubsetTransitive : CIDRBlock -> CIDRBlock -> CIDRBlock -> Type where ||| witness (e.g. `(c : Class ** ClassifiedAs p c)`) carrying the ||| `LTE` proof, or once a primitive-Nat reflective bridge lands. public export -0 systemPortBound : (p : Port) -> isSystemPort p = True -> LTE (portValue p) 1023 +postulate 0 systemPortBound : (p : Port) -> isSystemPort p = True -> LTE (portValue p) 1023 ||| OWED: every well-typed `Port` has `portValue p <= 65535`. Held ||| back by the move to runtime bounds checking: `mkPort` / `unsafeMkPort` @@ -87,14 +87,14 @@ public export ||| (i.e. `IsPort n := LTE n 65535`), or `Port` is rebuilt to store ||| the `LTE` proof directly. public export -0 portBounded : (p : Port) -> LTE (portValue p) 65535 +postulate 0 portBounded : (p : Port) -> LTE (portValue p) 65535 ||| Proof that host count is positive for prefix < 32 public export data PositiveHostCount : PrefixLength -> Type where - MkPositiveHostCount : LTE 1 (hostCount pfx) -> PositiveHostCount pfx + postulate MkPositiveHostCount : LTE 1 (hostCount pfx) -> PositiveHostCount pfx ||| Proof that private networks are not routable public export data PrivateNetwork : CIDRBlock -> Type where - MkPrivateNetwork : isPrivate cidr = True -> PrivateNetwork cidr + postulate MkPrivateNetwork : isPrivate cidr = True -> PrivateNetwork cidr diff --git a/src/Proven/SafeOTP/Proofs.idr b/src/Proven/SafeOTP/Proofs.idr index 9e7cfaa3..e370b71b 100644 --- a/src/Proven/SafeOTP/Proofs.idr +++ b/src/Proven/SafeOTP/Proofs.idr @@ -49,7 +49,7 @@ digits8Divisor = Refl ||| available, or by introducing a class-(J) `charEqRefl` axiom and a ||| per-list induction lemma over `go`. export -0 constantTimeCompareRefl : (s : String) -> constantTimeCompare s s = True +postulate 0 constantTimeCompareRefl : (s : String) -> constantTimeCompare s s = True ||| OWED: `constantTimeCompare` is symmetric — ||| `constantTimeCompare a b = constantTimeCompare b a` for all @@ -65,7 +65,7 @@ export ||| `Data.String` reflective tactic is available, or via a class-(J) ||| `charEqSym` axiom paired with a per-list induction over `go`. export -0 constantTimeCompareSym : (a, b : String) -> constantTimeCompare a b = constantTimeCompare b a +postulate 0 constantTimeCompareSym : (a, b : String) -> constantTimeCompare a b = constantTimeCompare b a ||| Empty strings compare equal. public export @@ -90,7 +90,7 @@ emptyStringsEqual = Refl ||| `constantTimeCompareRefl` is in scope, by `rewrite` on the head of ||| the `||`. export -0 codeValidatesAgainstSelf : (code : OTPCode) -> validateTOTPCode code [code] = True +postulate 0 codeValidatesAgainstSelf : (code : OTPCode) -> validateTOTPCode code [code] = True ||| OWED: TOTP validation accepts a code if it matches anywhere in ||| the candidate list. By definition `validateTOTPCode code codes = @@ -107,7 +107,7 @@ export ||| `rewrite` step for `_ :: _`), once a `Data.List.any` extensionality ||| lemma is in `contrib` — or inline the induction here. export -0 codeInListValidates : (code : OTPCode) -> (codes : List OTPCode) -> +postulate 0 codeInListValidates : (code : OTPCode) -> (codes : List OTPCode) -> any (\e => constantTimeCompare code.code e.code) codes = True -> validateTOTPCode code codes = True @@ -122,7 +122,7 @@ export ||| (String/Char primitive opacity in Idris2 0.8.0). Discharge ||| follows immediately once `constantTimeCompareRefl` is in scope. export -0 identicalHOTPValid : (code : OTPCode) -> validateHOTPCode code code = True +postulate 0 identicalHOTPValid : (code : OTPCode) -> validateHOTPCode code code = True ||| Validation against empty list always fails. public export diff --git a/src/Proven/SafePassword/Proofs.idr b/src/Proven/SafePassword/Proofs.idr index 2e526b10..02fa8f88 100644 --- a/src/Proven/SafePassword/Proofs.idr +++ b/src/Proven/SafePassword/Proofs.idr @@ -78,7 +78,7 @@ import Data.Maybe ||| `checkPolicy` to expose `checkLength` as a separately-callable ||| total function returning a `Dec` for the length predicate. public export -0 validPasswordLength : (policy : PasswordPolicy) -> +postulate 0 validPasswordLength : (policy : PasswordPolicy) -> (pwd : String) -> null (checkPolicy policy pwd) = True -> (length pwd >= policy.minLength = True, @@ -105,7 +105,7 @@ policyCheckDeterministic policy pwd = Refl ||| `unpack "" = []` definitionally, or refactor `checkPolicy` to ||| handle the empty case before threading through `unpack`. public export -0 emptyPasswordFails : (policy : PasswordPolicy) -> +postulate 0 emptyPasswordFails : (policy : PasswordPolicy) -> policy.minLength > 0 = True -> null (checkPolicy policy "") = False @@ -120,7 +120,7 @@ public export ||| dedicated lemma per checker. Discharge requires per-checker ||| monotonicity lemmas plus a `Data.String` reflective tactic. public export -0 longerPasswordBetter : (policy : PasswordPolicy) -> +postulate 0 longerPasswordBetter : (policy : PasswordPolicy) -> (short, long : String) -> length long > length short = True -> length (checkPolicy policy long) <= length (checkPolicy policy short) = True @@ -141,7 +141,7 @@ public export ||| `params.parallelism` and `Refl`-ing each leaf, or by a ||| `Decidable.Decidable.decide`-style reflective tactic over `<`. public export -0 argon2ParamsValid : (params : Argon2Params) -> +postulate 0 argon2ParamsValid : (params : Argon2Params) -> isRight (validateArgon2Params params) = True -> (params.timeCost >= 1 = True, params.memoryCost >= 8192 = True, @@ -155,7 +155,7 @@ public export ||| relation to `10` and `31` is case-analysed. Discharge by ||| case-splitting on `params.cost` and `Refl`-ing each leaf. public export -0 bcryptCostBounded : (params : BcryptParams) -> +postulate 0 bcryptCostBounded : (params : BcryptParams) -> isRight (validateBcryptParams params) = True -> (params.cost >= 10 = True, params.cost <= 31 = True) @@ -202,7 +202,7 @@ defaultScryptValid = Refl ||| Discharge once a `Data.Bits` reflective tactic for `xor`-self is ||| available, or by importing a per-bit-width self-xor lemma. public export -0 constantTimeRefl : (hash : List Bits8) -> +postulate 0 constantTimeRefl : (hash : List Bits8) -> constantTimeHashCompare hash hash = True ||| OWED: `constantTimeHashCompare` is symmetric in its two arguments. @@ -213,7 +213,7 @@ public export ||| requires either a `Data.Bits` reflective tactic for `xor`-symm or ||| a per-byte-width algebraic lemma. public export -0 constantTimeSym : (h1, h2 : List Bits8) -> +postulate 0 constantTimeSym : (h1, h2 : List Bits8) -> constantTimeHashCompare h1 h2 = constantTimeHashCompare h2 h1 ||| OWED: hashes of different length never compare equal under the @@ -229,7 +229,7 @@ public export ||| refactor `constantTimeHashCompare` to case-split on ||| `decEq (length xs) (length ys)` directly. public export -0 differentLengthNoMatch : (h1, h2 : List Bits8) -> +postulate 0 differentLengthNoMatch : (h1, h2 : List Bits8) -> length h1 /= length h2 = True -> constantTimeHashCompare h1 h2 = False @@ -250,7 +250,7 @@ public export ||| with a structurally-decreasing recursor (e.g., via `Vect` or ||| `Data.List.Quantifiers.AllInits`) making `analyzeStrength` total. public export -0 strengthScoreBounded : (pwd : String) -> +postulate 0 strengthScoreBounded : (pwd : String) -> score (analyzeStrength pwd) <= 100 = True ||| OWED: `entropy (analyzeStrength pwd) >= 0.0` for every password. @@ -266,7 +266,7 @@ public export ||| `Data.Double` non-negativity lemma for `*` and `log2` of ||| `>= 1.0` arguments. public export -0 entropyNonNegative : (pwd : String) -> +postulate 0 entropyNonNegative : (pwd : String) -> entropy (analyzeStrength pwd) >= 0.0 = True ||| OWED: a longer password has higher or equal entropy. By @@ -283,7 +283,7 @@ public export ||| is `covering`). Discharge requires all three blockers to be ||| lifted together. public export -0 longerHigherEntropy : (short, long : String) -> +postulate 0 longerHigherEntropy : (short, long : String) -> length long > length short = True -> entropy (analyzeStrength long) >= entropy (analyzeStrength short) = True @@ -298,7 +298,7 @@ public export ||| and `Refl`-ing each of the five leaves, or by refactoring the ||| `Ord` instance to derive from a `Cast StrengthLevel (Fin 5)`. public export -0 veryStrongMax : (level : StrengthLevel) -> level <= VeryStrong = True +postulate 0 veryStrongMax : (level : StrengthLevel) -> level <= VeryStrong = True ||| OWED: `StrengthLevel`'s ordering is transitive. The claim is the ||| standard transitivity of a total order, true by case-analysis on @@ -312,7 +312,7 @@ public export ||| derive from `Cast StrengthLevel (Fin 5)`, in which case ||| transitivity comes free from `Data.Fin`'s `Ord` transitivity. public export -0 strengthTransitive : (a, b, c : StrengthLevel) -> +postulate 0 strengthTransitive : (a, b, c : StrengthLevel) -> a <= b = True -> b <= c = True -> a <= c = True @@ -333,7 +333,7 @@ public export ||| helper). Discharge requires both a `Data.String` reflective ||| tactic for `toLower`/`elem` and `detectPatterns` becoming total. public export -0 commonPasswordDetected : (pwd : String) -> +postulate 0 commonPasswordDetected : (pwd : String) -> (toLower pwd `elem` ["password", "123456", "qwerty"]) = True -> any (\p => case p of CommonPassword _ => True; _ => False) (detectPatterns pwd) = True @@ -346,7 +346,7 @@ public export ||| `Refl`-ing each leaf, or by refactoring `patternPenalty` to ||| return a `Nat`-typed structure whose `>= 0` is by construction. public export -0 patternPenaltyNonNeg : (p : Pattern) -> patternPenalty p >= 0 = True +postulate 0 patternPenaltyNonNeg : (p : Pattern) -> patternPenalty p >= 0 = True -------------------------------------------------------------------------------- -- Rehash Decision Proofs @@ -364,7 +364,7 @@ public export ||| to derive `paramsAtLeast` from a per-algorithm `Decidable` ||| relation. public export -0 paramsAtLeastRefl : (params : HashParams) -> +postulate 0 paramsAtLeastRefl : (params : HashParams) -> paramsAtLeast params params = True ||| OWED: when current hash params are weaker than a target and the @@ -380,7 +380,7 @@ public export ||| antisymmetry exposed, or by rewriting the claim's codomain to ||| `decEq`-style witness. public export -0 strongerRequiresRehash : (weak, strong : HashParams) -> +postulate 0 strongerRequiresRehash : (weak, strong : HashParams) -> paramsAtLeast weak strong = False -> paramsAtLeast strong weak = True -> () @@ -400,7 +400,7 @@ public export ||| inlining `build (MkPolicyBuilder p)` to `p` via a definitional ||| equality lemma, or by marking `build` `%inline`. public export -0 builderProducesPolicy : build Policy.policyBuilder = Policy.defaultPolicy +postulate 0 builderProducesPolicy : build Policy.policyBuilder = Policy.defaultPolicy ||| DISCHARGED: `withMinLength n` followed by `build` yields a policy ||| whose `minLength` field equals `n`. The OWED comment suggested the @@ -428,7 +428,7 @@ withMinLengthCorrect n (MkPolicyBuilder (MkPolicy _ _ _ _ _ _ _ _ _ _)) = Refl ||| discharges, since this proof reduces to it after one record- ||| update normalisation step. public export -0 chainedBuildersCompose : (n : Nat) -> +postulate 0 chainedBuildersCompose : (n : Nat) -> minLength (build (withMinLength n (withUppercase Policy.policyBuilder))) = n -------------------------------------------------------------------------------- @@ -448,7 +448,7 @@ public export ||| derives from `Cast StrengthLevel (Fin 5)` (per ||| `strengthTransitive`'s discharge). public export -0 higherImpliesLower : (pwd : String) -> +postulate 0 higherImpliesLower : (pwd : String) -> (high, low : StrengthRequirement) -> requiredLevel high >= requiredLevel low = True -> meetsRequirement pwd high = True -> @@ -465,7 +465,7 @@ public export ||| `strengthScoreBounded` discharge — this proof reduces to their ||| composition. public export -0 veryStrongSatisfiesAll : (pwd : String) -> +postulate 0 veryStrongSatisfiesAll : (pwd : String) -> quickStrengthCheck pwd = VeryStrong -> (req : StrengthRequirement) -> meetsRequirement pwd req = True diff --git a/src/Proven/SafePath/Proofs.idr b/src/Proven/SafePath/Proofs.idr index 42e4806f..e9a1b330 100644 --- a/src/Proven/SafePath/Proofs.idr +++ b/src/Proven/SafePath/Proofs.idr @@ -103,7 +103,7 @@ import Data.Maybe ||| a `Data.String` reflective tactic (or a `splitPath . joinSegments ||| = id`-on-canonical-lists lemma) is available. export -0 normalizeIdempotent : (path : String) -> +postulate 0 normalizeIdempotent : (path : String) -> normalizePath (normalizePath path) = normalizePath path ||| OWED: normalisation removes empty segments. Witnessed by @@ -120,7 +120,7 @@ export ||| `splitPath` to a `List (Subset String NonEmpty)` where the ||| non-emptiness is propagated structurally. export -0 normalizeRemovesEmpty : (path : String) -> +postulate 0 normalizeRemovesEmpty : (path : String) -> not ("" `elem` splitPath (normalizePath path)) = True ||| OWED: normalisation removes `.` segments. Witnessed by @@ -133,7 +133,7 @@ export ||| available, or refactor `splitPath` to a `List PathSegment` where ||| `.` is excluded by construction. export -0 normalizeRemovesDot : (path : String) -> +postulate 0 normalizeRemovesDot : (path : String) -> not ("." `elem` splitPath (normalizePath path)) = True ||| OWED: a normalised absolute path has no leading `..` segment — @@ -151,7 +151,7 @@ export ||| tactic is available, or refactor to a `data IsAbsolute : String -> ||| Type` predicate carrying the witness structurally. export -0 normalizeAbsNoLeadingDotDot : (path : String) -> +postulate 0 normalizeAbsNoLeadingDotDot : (path : String) -> isPrefixOf "/" path = True -> case splitPath (normalizePath path) of (".." :: _) => Void @@ -164,7 +164,7 @@ export ||| Safe join prevents escape beyond base directory public export data NoEscape : (base : String) -> (combined : String) -> Type where - MkNoEscape : (base : String) -> (combined : String) -> + postulate MkNoEscape : (base : String) -> (combined : String) -> (prf : isPrefixOf (splitPath (normalizePath base)) (splitPath (normalizePath combined)) = True) -> NoEscape base combined @@ -186,7 +186,7 @@ data NoEscape : (base : String) -> (combined : String) -> Type where ||| `safeJoinPaths` to return a `Subset String (NoEscape base)` ||| carrying the proof in the type. export -0 safeJoinNoEscape : (base, rel : String) -> +postulate 0 safeJoinNoEscape : (base, rel : String) -> (result : String ** safeJoinPaths base rel = Just result) -> NoEscape base result @@ -206,7 +206,7 @@ export ||| or refactor `sanitizeSegment` to `List Char -> List Char` with ||| the safety predicate stated structurally. export -0 sanitizedIsSafe : (seg : String) -> +postulate 0 sanitizedIsSafe : (seg : String) -> isSafeSegment (sanitizeSegment seg) = True ||| OWED: every `ContainedPath base` value has a full path that is @@ -224,7 +224,7 @@ export ||| as `normalizeRemovesEmpty`. Discharge alongside ||| `safeJoinNoEscape`. export -0 containedInBase : (base : String) -> (cp : ContainedPath base) -> +postulate 0 containedInBase : (base : String) -> (cp : ContainedPath base) -> isAncestorOf base (getFullPath cp) = True -------------------------------------------------------------------------------- @@ -234,7 +234,7 @@ export ||| Data type for path without traversal public export data NoTraversal : String -> Type where - MkNoTraversal : (path : String) -> + postulate MkNoTraversal : (path : String) -> (prf : not (".." `elem` splitPath (normalizePath path)) = True) -> NoTraversal path @@ -252,7 +252,7 @@ data NoTraversal : String -> Type where ||| as `sanitizedIsSafe`. Discharge once a `Data.String` reflective ||| tactic for `unpack`/`pack` is available. export -0 sanitizedNoTraversal : (path : String) -> +postulate 0 sanitizedNoTraversal : (path : String) -> NoTraversal (normalizePath (joinSegments (map sanitizeSegment (splitPath path)))) ||| OWED: if `".." `elem` splitPath path = True` then `any (== "..") @@ -269,7 +269,7 @@ export ||| (or equivalent) is added to the Prelude, or once a ||| `Data.String` reflective tactic for `(==)` is available. export -0 traversalHasDotDot : (path : String) -> +postulate 0 traversalHasDotDot : (path : String) -> (".." `elem` splitPath path = True) -> any (== "..") (splitPath path) = True @@ -293,7 +293,7 @@ export ||| axiom (`%unsafe`, `believe_me ()` over `prim__eq_String`) in ||| the same trust posture as the boj-server / gossamer axioms. export -0 pathEqRefl : (path : String) -> pathEqSensitive path path = True +postulate 0 pathEqRefl : (path : String) -> pathEqSensitive path path = True ||| OWED: `pathEqSensitive` is symmetric, i.e. `pathEqSensitive p1 ||| p2 = pathEqSensitive p2 p1`. Witnessed by `pathEqSensitive` @@ -308,7 +308,7 @@ export ||| `Data.String` reflective tactic for `(==)` is available, or by ||| stating a `stringEqSym` class-J axiom in the same trust posture. export -0 pathEqSym : (p1, p2 : String) -> +postulate 0 pathEqSym : (p1, p2 : String) -> pathEqSensitive p1 p2 = pathEqSensitive p2 p1 ||| OWED: if `parent` is a parent of `child` then `parent` is an @@ -328,7 +328,7 @@ export ||| `splitPath . normalizePath` is reflective, or by a manual ||| `&&-projL` lemma followed by reflexivity on `isPrefixOf`. export -0 parentIsAncestor : (parent, child : String) -> +postulate 0 parentIsAncestor : (parent, child : String) -> isParentOf parent child = True -> isAncestorOf parent child = True @@ -346,7 +346,7 @@ export ||| structural induction over the prefix witness) and ||| `splitPath . normalizePath` is reflective. export -0 ancestorTransitive : (a, b, c : String) -> +postulate 0 ancestorTransitive : (a, b, c : String) -> isAncestorOf a b = True -> isAncestorOf b c = True -> isAncestorOf a c = True @@ -373,7 +373,7 @@ export ||| `record { stem : String, ext : Maybe String }` carrier where ||| the round-trip is structural. export -0 changeExtensionCorrect : (path, ext : String) -> +postulate 0 changeExtensionCorrect : (path, ext : String) -> not (ext == "") = True -> getExtension (changeExtension path ext) = Just ext @@ -387,7 +387,7 @@ export ||| `changeExtensionCorrect`. Discharge alongside ||| `changeExtensionCorrect`. export -0 stripExtensionRemoves : (path : String) -> +postulate 0 stripExtensionRemoves : (path : String) -> Data.Maybe.isJust (getExtension path) = True -> getExtension (stripExtension path) = Nothing @@ -407,7 +407,7 @@ export ||| `isSuffixOf` is available, or by stating a ||| `joinSegments_snoc_suffix` lemma over `List String`. export -0 addExtensionAdds : (path, ext : String) -> +postulate 0 addExtensionAdds : (path, ext : String) -> isSuffixOf ("." ++ ext) (addExtension path ext) = True -------------------------------------------------------------------------------- @@ -433,7 +433,7 @@ emptyMatchesEmpty = Refl ||| tactic for `unpack` is available, or by an induction on `s` via ||| `Strings.Strong.WithProof`. export -0 starMatchesAll : (s : String) -> matchGlob "*" s = True +postulate 0 starMatchesAll : (s : String) -> matchGlob "*" s = True ||| OWED: `matchGlob "?" (singleton c) = True` for every `c : Char` ||| — the question-mark wildcard matches any single character. @@ -450,7 +450,7 @@ export ||| tactic for `unpack . singleton = ::` (or equivalent) is ||| available. export -0 questionMatchesSingle : (c : Char) -> matchGlob "?" (singleton c) = True +postulate 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 @@ -468,7 +468,7 @@ export ||| `charEqRefl` class-J axiom in the same trust posture as ||| boj-server. export -0 literalMatchesSelf : (s : String) -> +postulate 0 literalMatchesSelf : (s : String) -> all (\c => c /= '*' && c /= '?') (unpack s) = True -> matchGlob s s = True @@ -492,7 +492,7 @@ export ||| structurally, or by a manual case-split on the guard chain ||| with `Strings.Substr.length`-reflective tactics. export -0 validPathBounded : (path : String) -> +postulate 0 validPathBounded : (path : String) -> (vp : ValidatedPath ** validatePath path = Right vp) -> Prelude.String.length path <= 4096 = True @@ -506,7 +506,7 @@ export ||| from `normalizeRemovesEmpty`. Same blocker family. Discharge ||| alongside `validPathBounded`. export -0 validSegmentsBounded : (path : String) -> +postulate 0 validSegmentsBounded : (path : String) -> (vp : ValidatedPath ** validatePath path = Right vp) -> all (\seg => Prelude.String.length seg <= 255) (splitPath path) = True @@ -522,7 +522,7 @@ export ||| Discharge alongside `validPathBounded`, or refactor to a ||| `dec*`-style decidable check. export -0 validPathNoNull : (path : String) -> +postulate 0 validPathNoNull : (path : String) -> (vp : ValidatedPath ** validatePath path = Right vp) -> not ('\0' `elem` unpack path) = True @@ -544,7 +544,7 @@ export ||| stuck on the FFI seam. Same blocker family. Discharge ||| alongside `safeJoinNoEscape`. export -0 containedStartsWithBase : (base : String) -> (cp : ContainedPath base) -> +postulate 0 containedStartsWithBase : (base : String) -> (cp : ContainedPath base) -> isPrefixOf (splitPath (normalizePath base)) (splitPath (normalizePath (getFullPath cp))) = True diff --git a/src/Proven/SafePromptInjection/Proofs.idr b/src/Proven/SafePromptInjection/Proofs.idr index 5b5fd4c5..f447c769 100644 --- a/src/Proven/SafePromptInjection/Proofs.idr +++ b/src/Proven/SafePromptInjection/Proofs.idr @@ -157,7 +157,7 @@ cleanIsSafe = Refl ||| than hidden. Discharging it needs an `unpack`/structural-recursion ||| bridge lemma (tracked in PROOF-NEEDS.md). public export -0 escapeNeutralisesAllDelimitersBridge : +postulate 0 escapeNeutralisesAllDelimitersBridge : (s : String) -> elem '<' (unpack (escapePromptDelimiters s)) = True -> elem '\\' (unpack (escapePromptDelimiters s)) = True diff --git a/src/Proven/SafeRegex/Proofs.idr b/src/Proven/SafeRegex/Proofs.idr index 9e2331bf..03703bd1 100644 --- a/src/Proven/SafeRegex/Proofs.idr +++ b/src/Proven/SafeRegex/Proofs.idr @@ -33,7 +33,7 @@ import Data.Nat ||| (same root cause as the `gcd` covering-callee reduction blocker in ||| PR #46). Discharge once the elaborator forces the field equation ||| through, or via a manual `rewrite` + `absurd Refl`. -0 boundedImpliesJustMax : (q : Quantifier) -> isBounded q = True -> +postulate 0 boundedImpliesJustMax : (q : Quantifier) -> isBounded q = True -> q.maxCount = Nothing -> Void ||| OWED: Bounded quantifiers expose a concrete `Nat` upper bound. @@ -44,7 +44,7 @@ import Data.Nat ||| equation across the `isBounded` unfolding (same blocker as ||| `boundedImpliesJustMax`). Discharge together with that lemma. public export -0 boundedQuantifierFinite : (q : Quantifier) -> (prf : isBounded q = True) -> (n : Nat ** q.maxCount = Just n) +postulate 0 boundedQuantifierFinite : (q : Quantifier) -> (prf : isBounded q = True) -> (n : Nat ** q.maxCount = Just n) ||| OWED: `steps < maxSteps = True` implies `S steps <= maxSteps = True`. ||| Operationally `<` is defined as `\a, b => S a <= b` on `Nat`, so the @@ -55,7 +55,7 @@ public export ||| through `compareNat` not through structural pattern match. Discharge ||| via `Data.Nat.lteSuccRight` after unfolding the instance, or once ||| the stdlib exposes `lt = lteS` as a definitional equality. -0 stepIncreases : (steps : Nat) -> (maxSteps : Nat) -> (steps < maxSteps = True) -> +postulate 0 stepIncreases : (steps : Nat) -> (maxSteps : Nat) -> (steps < maxSteps = True) -> (S steps <= maxSteps = True) ||| OWED: For any fuel-bounded match attempt there exists a step count @@ -77,7 +77,7 @@ public export ||| (defined `= matchingTerminatesLemma` below) is at default ||| multiplicity for the user-facing API; making the lemma `0` would ||| break that consumer. -matchingTerminatesLemma : (fuel : Nat) -> (r : Regex) -> +postulate matchingTerminatesLemma : (fuel : Nat) -> (r : Regex) -> Either (steps : Nat ** steps <= fuel = True) (steps : Nat ** steps > fuel = True) @@ -104,7 +104,7 @@ matchingTerminates = matchingTerminatesLemma ||| `Bool`-vs-`Prop` reflection gap. Discharge via a manual ||| `rewrite` of the `if`-head with the premise, or once a reflective ||| `Bool->Dec` bridge for arbitrary boolean scrutinees lands. -0 nestedQuantifiersExponential : (r : Regex) -> +postulate 0 nestedQuantifiersExponential : (r : Regex) -> hasNestedQuantifiers r = True -> determineComplexity r = Exponential @@ -119,7 +119,7 @@ matchingTerminates = matchingTerminatesLemma ||| countQuantifiers r > 0`. Discharge via the same reflective ||| `Bool->Dec` bridge plus an `andTrueSplit` lemma applied at the ||| premise. -0 overlappingAltsExponential : (r : Regex) -> +postulate 0 overlappingAltsExponential : (r : Regex) -> hasOverlappingAlternatives r = True -> countQuantifiers r > 0 = True -> (determineComplexity r = Exponential) `Either` @@ -132,7 +132,7 @@ matchingTerminates = matchingTerminatesLemma ||| Held back by the same Idris2 0.8.0 nested `if`-scrutinee blocker ||| as the other complexity-classification lemmas. Discharge via the ||| same reflective `Bool->Dec` bridge. -0 quantifiedEmptyQuadratic : (r : Regex) -> +postulate 0 quantifiedEmptyQuadratic : (r : Regex) -> hasQuantifiedEmpty r = True -> (determineComplexity r = Quadratic) `Either` (determineComplexity r = Exponential) @@ -149,7 +149,7 @@ matchingTerminates = matchingTerminatesLemma ||| four nested `case`-inversions on opaque function calls. Discharge ||| via a manual hand-written four-arm inversion, or once a tactic ||| for `if`-chain inversion lands. -0 linearNoExponentialPatterns : (r : Regex) -> +postulate 0 linearNoExponentialPatterns : (r : Regex) -> determineComplexity r = Linear -> (hasNestedQuantifiers r = False, Either (hasOverlappingAlternatives r = False) ((countQuantifiers r = 0) = True), @@ -203,7 +203,7 @@ unboundedNeverSafe RelaxedSafety = Refl ||| `Data.Nat.lteTransitive`. Discharge once a `Data.String` ||| reflective bridge for `length` is available, then apply ||| transitivity. -0 smallInputAlwaysSafe : (sr : SafeRegex) -> (input : String) -> +postulate 0 smallInputAlwaysSafe : (sr : SafeRegex) -> (input : String) -> length input <= 50 = True -> isInputSafe sr input = True @@ -217,7 +217,7 @@ unboundedNeverSafe RelaxedSafety = Refl ||| `boundedImpliesJustMax` (record-field equation not tracked by ||| case-split). Discharge via a manual `rewrite` of the scrutinee ||| with the premise. -0 linearAllowsLargeInput : (sr : SafeRegex) -> +postulate 0 linearAllowsLargeInput : (sr : SafeRegex) -> sr.complexity.level = Linear -> maxSafeInputLength sr = 10000000 @@ -226,7 +226,7 @@ unboundedNeverSafe RelaxedSafety = Refl ||| `maxSafeInputLength` (`Safety.idr` L375). ||| Held back by the same record-projection-through-`case` blocker as ||| `linearAllowsLargeInput`. Discharge identically. -0 exponentialRestrictsInput : (sr : SafeRegex) -> +postulate 0 exponentialRestrictsInput : (sr : SafeRegex) -> sr.complexity.level = Exponential -> maxSafeInputLength sr = 100 @@ -255,7 +255,7 @@ anyMatchesNonNewline _ prf = prf ||| primitives `prim__gte_Char` / `prim__lte_Char` — same blocker ||| family as `anyMatchesNonNewline`. Discharge once a `Data.Char` ||| reflective bridge is available. -0 digitOnlyDigits : (c : Char) -> +postulate 0 digitOnlyDigits : (c : Char) -> matchesClass c Digit = True -> (c >= '0' = True, c <= '9' = True) @@ -295,7 +295,7 @@ unionIsOr _ _ _ = Refl ||| marked `0` because the public `sameClassOverlaps` proof consumes ||| this lemma at default multiplicity. Discharge once a `Data.Char` ||| reflective bridge gives `eqCharRefl : (c : Char) -> (c == c) = True`. -charSelfOverlaps : (c : Char) -> classesOverlap (SingleChar c) (SingleChar c) = True +postulate charSelfOverlaps : (c : Char) -> classesOverlap (SingleChar c) (SingleChar c) = True ||| OWED: a `Range` overlaps itself. Operationally true by the ||| `(Range f1 t1) (Range f2 t2)` arm of `classesOverlap` @@ -309,7 +309,7 @@ charSelfOverlaps : (c : Char) -> classesOverlap (SingleChar c) (SingleChar c) = ||| public `sameClassOverlaps` proof consumes this lemma at default ||| multiplicity. Discharge once a `Data.Char` reflective bridge for ||| `(<)` is available. -rangeSelfOverlaps : (from, to : Char) -> classesOverlap (Range from to) (Range from to) = True +postulate rangeSelfOverlaps : (from, to : Char) -> classesOverlap (Range from to) (Range from to) = True ||| OWED: a `Union` overlaps itself. Operationally true by the ||| `(Union c1 c2) other` arm of `classesOverlap` (`Safety.idr` @@ -325,7 +325,7 @@ rangeSelfOverlaps : (from, to : Char) -> classesOverlap (Range from to) (Range f ||| public `sameClassOverlaps` proof consumes this lemma at default ||| multiplicity. Discharge via explicit induction on `(a, b)` plus ||| the discharged `charSelfOverlaps` / `rangeSelfOverlaps`. -unionSelfOverlaps : (a, b : CharClass) -> classesOverlap (Union a b) (Union a b) = True +postulate unionSelfOverlaps : (a, b : CharClass) -> classesOverlap (Union a b) (Union a b) = True ||| Proof that identical classes always overlap public export @@ -356,7 +356,7 @@ anyOverlapsAll _ = Refl ||| range/overlap lemmas. Discharge via a manual `rewrite` of `t1 < ||| f2` with the premise, plus the `Data.Bool` lemmas `orTrueLeft` ||| and `notTrue`. -0 disjointRangesNoOverlap : (f1, t1, f2, t2 : Char) -> +postulate 0 disjointRangesNoOverlap : (f1, t1, f2, t2 : Char) -> (t1 < f2 = True) -> classesOverlap (Range f1 t1) (Range f2 t2) = False @@ -415,7 +415,7 @@ backrefNotKnownSafe _ = Refl ||| the *linear-time* growth law underlying the matcher's safety ||| budget. Discharge via `Data.Nat.multStrictMonotone` plus a ||| manual `rewrite` of the case scrutinee. -0 linearStepLimitScales : (analysis : ComplexityAnalysis) -> +postulate 0 linearStepLimitScales : (analysis : ComplexityAnalysis) -> (analysis.level = Linear) -> (inputSize1, inputSize2 : Nat) -> (inputSize1 < inputSize2 = True) -> @@ -434,7 +434,7 @@ backrefNotKnownSafe _ = Refl ||| pattern into a hard-bounded ReDoS-resistant matcher. Discharge ||| via `Data.Nat.minLteRight` plus a manual `rewrite` of the ||| scrutinee. -0 exponentialStepLimitCapped : (analysis : ComplexityAnalysis) -> +postulate 0 exponentialStepLimitCapped : (analysis : ComplexityAnalysis) -> (analysis.level = Exponential) -> (inputSize : Nat) -> calculateStepLimit analysis inputSize <= 1000000 = True @@ -468,7 +468,7 @@ successIsMatched _ _ _ _ = Refl ||| `dateComponentsValid` / `timeComponentsValid`). Discharge once ||| `Capture` is refactored to carry the bound as an erased witness, ||| and the matcher is updated to produce it at every push site. -0 capturePositionsValid : (result : MatchResult) -> +postulate 0 capturePositionsValid : (result : MatchResult) -> (result.matched = True) -> All (\c => c.start <= c.end = True) result.captures @@ -486,7 +486,7 @@ successIsMatched _ _ _ _ = Refl ||| `andTrueSplit` applied twice plus `notFalseTrue`. Discharge via ||| a manual chain of `andTrueSplit` once the helper lands, or by ||| inlining the equation by hand. -0 seqPreservesSafety : (r1, r2 : Regex) -> +postulate 0 seqPreservesSafety : (r1, r2 : Regex) -> isKnownSafe r1 = True -> isKnownSafe r2 = True -> hasNestedQuantifiers (Seq r1 r2) = False -> @@ -498,7 +498,7 @@ successIsMatched _ _ _ _ = Refl ||| `isKnownSafe (Alt r1 r2) = isKnownSafe r1 && isKnownSafe r2 && not (regexesOverlap r1 r2)` ||| Held back by the same three-way `&&`-split blocker as ||| `seqPreservesSafety`. Discharge identically. -0 altPreservesSafety : (r1, r2 : Regex) -> +postulate 0 altPreservesSafety : (r1, r2 : Regex) -> isKnownSafe r1 = True -> isKnownSafe r2 = True -> regexesOverlap r1 r2 = False -> @@ -510,7 +510,7 @@ successIsMatched _ _ _ _ = Refl ||| `isKnownSafe (Quant r q) = isKnownSafe r && isBounded q && not (hasNestedQuantifiers (Quant r q))` ||| Held back by the same three-way `&&`-split blocker as ||| `seqPreservesSafety`. Discharge identically. -0 boundedQuantPreservesSafety : (r : Regex) -> (q : Quantifier) -> +postulate 0 boundedQuantPreservesSafety : (r : Regex) -> (q : Quantifier) -> isKnownSafe r = True -> isBounded q = True -> hasNestedQuantifiers (Quant r q) = False -> @@ -544,7 +544,7 @@ safetyAnalysisTotal r = (analyzeComplexity r ** Refl) ||| Discharge via the 60-arm case-split with `absurd Refl` on every ||| impossible arm, or by reformulating the lemma to take a single ||| `Ord ComplexityLevel`-derived strict-order proof. -complexityTransitiveFallback : (a, b, c : ComplexityLevel) -> +postulate complexityTransitiveFallback : (a, b, c : ComplexityLevel) -> a `compare` b = LT -> b `compare` c = LT -> a `compare` c = LT diff --git a/src/Proven/SafeSQL/Proofs.idr b/src/Proven/SafeSQL/Proofs.idr index 9b77fca0..f2564cdb 100644 --- a/src/Proven/SafeSQL/Proofs.idr +++ b/src/Proven/SafeSQL/Proofs.idr @@ -22,16 +22,16 @@ import Data.String public export data NoUnescapedQuotes : String -> Type where ||| Empty string has no unescaped quotes - EmptyNoQuotes : NoUnescapedQuotes "" + postulate EmptyNoQuotes : NoUnescapedQuotes "" ||| String with all quotes properly doubled - QuotesEscaped : (s : String) -> + postulate QuotesEscaped : (s : String) -> (prf : all (\c => c /= '\'') (unpack s) = True) -> NoUnescapedQuotes s ||| Predicate: A string contains no SQL comment markers public export data NoCommentMarkers : String -> Type where - MkNoCommentMarkers : (s : String) -> + postulate MkNoCommentMarkers : (s : String) -> (noDoubleDash : not (isInfixOf "--" s) = True) -> (noSlashStar : not (isInfixOf "/*" s) = True) -> NoCommentMarkers s @@ -39,14 +39,14 @@ data NoCommentMarkers : String -> Type where ||| Predicate: A string contains no statement terminators public export data NoStatementTerminators : String -> Type where - MkNoTerminators : (s : String) -> + postulate MkNoTerminators : (s : String) -> (noSemicolon : not (';' `elem` unpack s) = True) -> NoStatementTerminators s ||| Predicate: A string is a safe SQL identifier public export data IsSafeIdentifier : String -> Type where - MkSafeIdent : (s : String) -> + postulate MkSafeIdent : (s : String) -> (validChars : all isIdentifierChar (unpack s) = True) -> (notEmpty : length s > 0 = True) -> (notTooLong : length s <= 128 = True) -> @@ -63,7 +63,7 @@ isParamOrLiteral (Identifier _) = True ||| Predicate: A query uses only parameterized values (no string interpolation) public export data IsParameterized : ParameterizedQuery -> Type where - MkParameterized : (q : ParameterizedQuery) -> + postulate MkParameterized : (q : ParameterizedQuery) -> (noRawStrings : all isParamOrLiteral q.fragments = True) -> IsParameterized q @@ -71,27 +71,27 @@ data IsParameterized : ParameterizedQuery -> Type where public export data IsEscapedValue : SQLDialect -> SQLValue -> Type where ||| NULL is always safe - NullSafe : IsEscapedValue d SQLNull + postulate NullSafe : IsEscapedValue d SQLNull ||| Booleans are safe (rendered as TRUE/FALSE) - BoolSafe : IsEscapedValue d (SQLBool b) + postulate BoolSafe : IsEscapedValue d (SQLBool b) ||| Integers are safe (no string escaping needed) - IntSafe : IsEscapedValue d (SQLInt i) + postulate IntSafe : IsEscapedValue d (SQLInt i) ||| Naturals are safe - NatSafe : IsEscapedValue d (SQLNat n) + postulate NatSafe : IsEscapedValue d (SQLNat n) ||| Doubles are safe (numeric) - DoubleSafe : IsEscapedValue d (SQLDouble x) + postulate DoubleSafe : IsEscapedValue d (SQLDouble x) ||| Text is escaped by escapeString - TextEscaped : (d : SQLDialect) -> (s : String) -> IsEscapedValue d (SQLText s) + postulate TextEscaped : (d : SQLDialect) -> (s : String) -> IsEscapedValue d (SQLText s) ||| Blob is hex-encoded - BlobEncoded : (d : SQLDialect) -> (bs : List Bits8) -> IsEscapedValue d (SQLBlob bs) + postulate BlobEncoded : (d : SQLDialect) -> (bs : List Bits8) -> IsEscapedValue d (SQLBlob bs) ||| Date components are numeric - DateSafe : IsEscapedValue d (SQLDate y m day) + postulate DateSafe : IsEscapedValue d (SQLDate y m day) ||| Time components are numeric - TimeSafe : IsEscapedValue d (SQLTime h m s) + postulate TimeSafe : IsEscapedValue d (SQLTime h m s) ||| Timestamp components are numeric - TimestampSafe : IsEscapedValue d (SQLTimestamp y mo dy h mi s) + postulate TimestampSafe : IsEscapedValue d (SQLTimestamp y mo dy h mi s) ||| Raw SQL is trusted by construction (only from code, never user input) - RawTrusted : IsEscapedValue d (SQLRaw s) + postulate RawTrusted : IsEscapedValue d (SQLRaw s) -------------------------------------------------------------------------------- -- Core Safety Theorems @@ -116,7 +116,7 @@ data IsEscapedValue : SQLDialect -> SQLValue -> Type where ||| tactic or per-character induction lemma over ||| `unpack . concat . map` is available. export -0 escapeStringQuotesSafe : (d : SQLDialect) -> (s : String) -> +postulate 0 escapeStringQuotesSafe : (d : SQLDialect) -> (s : String) -> NoUnescapedQuotes (escapeString d s) ||| OWED: if `isValidIdentifier s = True` then `IsSafeIdentifier s`. @@ -138,7 +138,7 @@ export ||| `isValidIdentifier` is refactored to return a structural witness ||| (e.g. `Dec (IsSafeIdentifier s)`) instead of a `Bool`. export -0 identifierCharsSafe : (s : String) -> (prf : isValidIdentifier s = True) -> +postulate 0 identifierCharsSafe : (s : String) -> (prf : isValidIdentifier s = True) -> IsSafeIdentifier s ||| OWED: every `ParameterizedQuery` value `q` satisfies @@ -163,7 +163,7 @@ export ||| available, or (b) `ParameterizedQuery` is refactored to carry an ||| `IsParameterized` field at construction (intrinsic invariant). export -0 parameterizedQueriesSafe : (q : ParameterizedQuery) -> IsParameterized q +postulate 0 parameterizedQueriesSafe : (q : ParameterizedQuery) -> IsParameterized q ||| Theorem: All SQLValue types are safely escapable export @@ -188,7 +188,7 @@ allValuesSafe d (SQLRaw s) = RawTrusted public export data InjectionSafe : ParameterizedQuery -> Type where ||| Query is safe because it uses parameterization - SafeByParameterization : + postulate SafeByParameterization : (q : ParameterizedQuery) -> (isParam : IsParameterized q) -> (allEscaped : (v : SQLValue) -> v `elem` q.params = True -> IsEscapedValue q.dialect v) -> @@ -209,7 +209,7 @@ data InjectionSafe : ParameterizedQuery -> Type where ||| `Data.List.all` reflection lands, or `ParameterizedQuery` carries the ||| invariant intrinsically). Held back by the same blocker as its premise. export -0 builderQueriesSafe : (q : ParameterizedQuery) -> +postulate 0 builderQueriesSafe : (q : ParameterizedQuery) -> (builtWithBuilder : ()) -> InjectionSafe q @@ -221,7 +221,7 @@ export ||| `0`-multiplicity, opaque-String-FFI blocker), so this theorem inherits the ||| same debt and cannot be relevantly discharged until it is. export -0 cannotEscapeStringLiteral : (d : SQLDialect) -> (userInput : String) -> +postulate 0 cannotEscapeStringLiteral : (d : SQLDialect) -> (userInput : String) -> let escaped = escapeString d userInput in NoUnescapedQuotes escaped @@ -245,7 +245,7 @@ numericValuesCannotInject d i = IntSafe ||| which is OWED (erased) — so, like `builderQueriesSafe`, this cannot be ||| relevantly discharged until `parameterizedQueriesSafe` is. export -0 combinePreservesSafety : (q1 : ParameterizedQuery) -> (q2 : ParameterizedQuery) -> +postulate 0 combinePreservesSafety : (q1 : ParameterizedQuery) -> (q2 : ParameterizedQuery) -> InjectionSafe q1 -> InjectionSafe q2 -> InjectionSafe (combineQueries q1 q2) @@ -256,7 +256,7 @@ export ||| as `combinePreservesSafety`; discharge together once ||| `parameterizedQueriesSafe` is. export -0 addParamPreservesSafety : (q : ParameterizedQuery) -> (v : SQLValue) -> +postulate 0 addParamPreservesSafety : (q : ParameterizedQuery) -> (v : SQLValue) -> InjectionSafe q -> InjectionSafe (addParam v q) diff --git a/src/Proven/SafeSemVer/Proofs.idr b/src/Proven/SafeSemVer/Proofs.idr index 52be9356..f9cd30df 100644 --- a/src/Proven/SafeSemVer/Proofs.idr +++ b/src/Proven/SafeSemVer/Proofs.idr @@ -139,7 +139,7 @@ alphaAfterNumeric _ _ = Refl ||| lemma is available in `Data.Nat`, or refactor `isCompatible` to use ||| `decEq` or `compare ... = EQ` form. public export -0 compatibleWithSelf : (v : SemVer) -> isStable v = True -> isCompatible v v = True +postulate 0 compatibleWithSelf : (v : SemVer) -> isStable v = True -> isCompatible v v = True ||| OWED: `satisfiesGTE` is reflexive — every version satisfies `>=` ||| itself. By definition `satisfiesGTE v v = compare v v /= LT`, so @@ -153,4 +153,4 @@ public export ||| an `Ord`-reflexivity lemma is available for `Nat` and `List` is ||| chained through `comparePre`. public export -0 satisfiesGTERefl : (v : SemVer) -> satisfiesGTE v v = True +postulate 0 satisfiesGTERefl : (v : SemVer) -> satisfiesGTE v v = True diff --git a/src/Proven/SafeString/Proofs.idr b/src/Proven/SafeString/Proofs.idr index 57251699..b3b05e60 100644 --- a/src/Proven/SafeString/Proofs.idr +++ b/src/Proven/SafeString/Proofs.idr @@ -39,7 +39,7 @@ emptyStringLength = Refl ||| tactic for `length` / `++` is available, or `String` is refactored ||| to expose its packed-character list as a definitional equality. export -0 concatLength : (s1, s2 : String) -> +postulate 0 concatLength : (s1, s2 : String) -> Prelude.String.length (s1 ++ s2) = Prelude.String.length s1 + Prelude.String.length s2 -------------------------------------------------------------------------------- @@ -67,7 +67,7 @@ trimEmpty = Refl ||| tactic for `pack . unpack` is available, or `String` is refactored ||| to expose its packed-character list. export -0 trimNoWhitespace : (s : String) -> all (Prelude.Basics.not . isSpace) (unpack s) = True -> +postulate 0 trimNoWhitespace : (s : String) -> all (Prelude.Basics.not . isSpace) (unpack s) = True -> Proven.SafeString.trim s = s -------------------------------------------------------------------------------- @@ -101,7 +101,7 @@ escapeSQLEmpty = Refl ||| `pack . singletonList = singleton` (or the `singleton`/`unpack` ||| pair becomes a definitional inverse). export -0 escapeHTMLSafe : (c : Char) -> +postulate 0 escapeHTMLSafe : (c : Char) -> Prelude.Basics.not (c == '&' || c == '<' || c == '>' || c == '"' || c == '\'') = True -> escapeHTML (singleton c) = singleton c @@ -118,7 +118,7 @@ export ||| Refs standards#158). public export data NoUnescapedQuotes : String -> Type where - MkNoUnescapedQuotes : (s : String) -> + postulate MkNoUnescapedQuotes : (s : String) -> (0 prf : all (\c => c /= '\'') (unpack s) = True) -> NoUnescapedQuotes s @@ -145,7 +145,7 @@ data NoUnescapedQuotes : String -> Type where ||| tactic for `unpack . pack . map f` (or an induction principle on ||| the unpacked list) is available. export -0 escapeSQLSafeProperty : (s : String) -> +postulate 0 escapeSQLSafeProperty : (s : String) -> all (\c => c /= '\'') (unpack (escapeSQL s)) = True ||| After SQL escaping, there are no single quotes that aren't doubled @@ -161,7 +161,7 @@ escapeSQLSafe s = MkNoUnescapedQuotes (escapeSQL s) (escapeSQLSafeProperty s) ||| Refs standards#158). public export data NoRawBrackets : String -> Type where - MkNoRawBrackets : (s : String) -> + postulate MkNoRawBrackets : (s : String) -> (0 prf : all (\c => c /= '<' && c /= '>') (unpack s) = True) -> NoRawBrackets s @@ -181,7 +181,7 @@ data NoRawBrackets : String -> Type where ||| tactic for `unpack . pack . map f` (or an induction principle on ||| the unpacked list) is available. export -0 escapeHTMLSafeProperty : (s : String) -> +postulate 0 escapeHTMLSafeProperty : (s : String) -> all (\c => c /= '<' && c /= '>') (unpack (escapeHTML s)) = True ||| After HTML escaping, there are no raw angle brackets @@ -209,7 +209,7 @@ escapeHTMLSafe' s = MkNoRawBrackets (escapeHTML s) (escapeHTMLSafeProperty s) ||| and SafeHtml's `escapePreservesNoLT`. Discharge once a ||| `Data.String` reflective tactic for `pack . unpack` is available. export -0 splitJoinIdentity : (delim : Char) -> (s : String) -> +postulate 0 splitJoinIdentity : (delim : Char) -> (s : String) -> Prelude.Basics.not (delim `elem` unpack s) = True -> Proven.SafeString.join (singleton delim) (Proven.SafeString.split delim s) = s @@ -233,4 +233,4 @@ export ||| `join` are refactored to a list-based intermediate that admits ||| structural induction. export -0 linesUnlinesApprox : (s : String) -> Proven.SafeString.unlines (Proven.SafeString.lines s) = s ++ "" +postulate 0 linesUnlinesApprox : (s : String) -> Proven.SafeString.unlines (Proven.SafeString.lines s) = s ++ "" diff --git a/src/Proven/SafeTOML/Proofs.idr b/src/Proven/SafeTOML/Proofs.idr index e157071e..71770ed4 100644 --- a/src/Proven/SafeTOML/Proofs.idr +++ b/src/Proven/SafeTOML/Proofs.idr @@ -40,30 +40,30 @@ valueDepth (TTable kvs) = S (foldl max 0 (map (valueDepth . snd) kvs)) ||| Predicate: TOML has bounded nesting depth public export data BoundedDepth : Nat -> TOMLValue -> Type where - MkBoundedDepth : (maxDepth : Nat) -> (val : TOMLValue) -> + postulate MkBoundedDepth : (maxDepth : Nat) -> (val : TOMLValue) -> {auto prf : valueDepth val <= maxDepth = True} -> BoundedDepth maxDepth val ||| Predicate: TOML arrays are homogeneous public export data HomogeneousArray : TOMLValue -> Type where - MkHomogeneousArray : (arr : TOMLValue) -> HomogeneousArray arr + postulate MkHomogeneousArray : (arr : TOMLValue) -> HomogeneousArray arr ||| Predicate: Value is scalar (no nested structure) public export data IsScalar : TOMLValue -> Type where - StringScalar : IsScalar (TString s) - IntScalar : IsScalar (TInt i) - FloatScalar : IsScalar (TFloat f) - BoolScalar : IsScalar (TBool b) - DateTimeScalar : IsScalar (TDateTime dt) - DateScalar : IsScalar (TDate d) - TimeScalar : IsScalar (TTime t) + postulate StringScalar : IsScalar (TString s) + postulate IntScalar : IsScalar (TInt i) + postulate FloatScalar : IsScalar (TFloat f) + postulate BoolScalar : IsScalar (TBool b) + postulate DateTimeScalar : IsScalar (TDateTime dt) + postulate DateScalar : IsScalar (TDate d) + postulate TimeScalar : IsScalar (TTime t) ||| Predicate: Key is valid public export data ValidKey : String -> Type where - MkValidKey : (key : String) -> {auto prf : not (null (unpack key)) = True} -> ValidKey key + postulate MkValidKey : (key : String) -> {auto prf : not (null (unpack key)) = True} -> ValidKey key -------------------------------------------------------------------------------- -- Resource Limit Proofs @@ -183,7 +183,7 @@ scalarNotNested _ _ = () ||| tactic for `unpack` is available, or by introducing a generic ||| `andTrueSplit : (x && y = True) -> (x = True, y = True)` and ||| applying it under the opaque `unpack key`. -0 bareKeyCharsValid : (key : String) -> +postulate 0 bareKeyCharsValid : (key : String) -> isValidBareKey key = True -> all isValidBareKeyChar (unpack key) = True @@ -211,7 +211,7 @@ emptyKeyInvalid = Refl ||| reflective tactic for `unpack` is available, or by composing a ||| hand-written `anyNotAll : any (not . p) xs = True -> all p xs = ||| False` with `notTrueIsFalse` on the chained `Bool` equations. -0 specialCharsNeedQuoting : (key : String) -> +postulate 0 specialCharsNeedQuoting : (key : String) -> any (\c => not (isValidBareKeyChar c)) (unpack key) = True -> needsQuoting key = True @@ -298,7 +298,7 @@ inlineTableImmutable tab isTab = () ||| ...`) and `Parser.parseDate` is updated to produce the refined ||| record, or once a `Trusted.Parser` ghost-oracle predicate is ||| threaded through every `TOMLDate` consumer. -0 dateComponentsValid : (d : TOMLDate) -> +postulate 0 dateComponentsValid : (d : TOMLDate) -> (d.month >= 1 && d.month <= 12 && d.day >= 1 && d.day <= 31) = True @@ -323,7 +323,7 @@ inlineTableImmutable tab isTab = () ||| and `Parser.parseTime` is updated to produce the refined record, ||| or once a `Trusted.Parser` ghost-oracle predicate is threaded ||| through every `TOMLTime` consumer. -0 timeComponentsValid : (t : TOMLTime) -> +postulate 0 timeComponentsValid : (t : TOMLTime) -> (t.hour <= 23 && t.minute <= 59 && t.second <= 60) = True -- 60 for leap second diff --git a/src/Proven/SafeUrl/Proofs.idr b/src/Proven/SafeUrl/Proofs.idr index 188e8d0a..6d60490f 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 -0 unreservedNotEncoded : (c : Char) -> +postulate 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 -0 encodePreservesAlphaNum : (s : String) -> +postulate 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 -0 decodeUnreservedIdentity : (s : String) -> +postulate 0 decodeUnreservedIdentity : (s : String) -> all isAlphaNum (unpack s) = True -> urlDecode s = Just s @@ -105,7 +105,7 @@ export ||| reduction is available, or via a property-test + trusted-extraction ||| validation campaign (see boj-server backend-assurance harness). export -0 encodeDecodeIdentity : (s : String) -> +postulate 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 -0 emptyBuilderEmpty : buildQueryString Query.emptyQuery = "" +postulate 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 -0 setGetIdentity : (key, val : String) -> (qs : QueryString) -> +postulate 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 @@ export ||| induction over `qs`. Discharge once String equality is type-level ||| reducible. Same blocker family as `setGetIdentity`. export -0 removeHasNot : (key : String) -> (qs : QueryString) -> +postulate 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 @@ export ||| / proving the `filterAll` lemma and rewriting, once String equality ||| is type-level reducible. export -0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) -> +postulate 0 filterPreservesOnly : (keys : List String) -> (qs : QueryString) -> all (\(k, _) => k `elem` keys) (filterParams keys qs) = True -------------------------------------------------------------------------------- @@ -202,7 +202,7 @@ export ||| "42" = Just 42` is operationally true but opaque). Discharge via ||| property-test + trusted-extraction validation. export -0 parseIntValid : (key : String) -> +postulate 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 @@ export ||| Discharge once String equality is type-level reducible, or via ||| property-test campaign. export -0 parseBoolTrue : (key : String) -> +postulate 0 parseBoolTrue : (key : String) -> getBoolParam key [(key, "true")] = Just True ||| OWED: Parsing bool `"false"` from a matching key yields `Just @@ -225,7 +225,7 @@ export ||| Held back by the same Idris2 0.8.0 String-literal-match ||| (`prim__eqString` FFI) opacity. Discharge with `parseBoolTrue`. export -0 parseBoolFalse : (key : String) -> +postulate 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 -0 mergeEmptyLeft : (qs : QueryString) -> +postulate 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 - MkSafeURL : (url : ParsedURL) -> + postulate 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 -0 isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True -> +postulate 0 isSafeSchemeNotJavascript : (url : ParsedURL) -> isSafeScheme url = True -> Not (url.scheme = Just (Custom "javascript")) ||| Validate URL is safe @@ -327,7 +327,7 @@ validateSafe url = ||| IPv4 address components are bounded public export data ValidIPv4 : Host -> Type where - MkValidIPv4 : (a, b, c, d : Nat) -> + postulate MkValidIPv4 : (a, b, c, d : Nat) -> LTE a 255 -> LTE b 255 -> LTE c 255 -> LTE d 255 -> ValidIPv4 (IPv4 a b c d) @@ -336,7 +336,7 @@ data ValidIPv4 : Host -> Type where ||| because `lteFrom65535Check` is OWED — see below. public export data ValidPort : Nat -> Type where - MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p + postulate MkValidPort : (p : Nat) -> (0 _ : LTE p 65535) -> ValidPort p ||| DISCHARGED via `Data.Nat.lteReflectsLTE` stdlib lemma. export diff --git a/src/Proven/SafeXML/Proofs.idr b/src/Proven/SafeXML/Proofs.idr index 0281e7ad..2325863a 100644 --- a/src/Proven/SafeXML/Proofs.idr +++ b/src/Proven/SafeXML/Proofs.idr @@ -24,14 +24,14 @@ import Data.String ||| Predicate: XML contains no external entities public export data NoExternalEntities : String -> Type where - MkNoExternalEntities : (xml : String) -> + postulate MkNoExternalEntities : (xml : String) -> {auto prf : not (isInfixOf " NoExternalEntities xml ||| Predicate: XML contains no DOCTYPE declarations public export data NoDTD : String -> Type where - MkNoDTD : (xml : String) -> + postulate MkNoDTD : (xml : String) -> {auto prf : not (isInfixOf " NoDTD xml @@ -48,19 +48,19 @@ nodeDepth (Element _ _ children) = S (foldl max 0 (map nodeDepth children)) ||| Predicate: Element nesting depth is bounded public export data BoundedDepth : Nat -> XMLNode -> Type where - MkBoundedDepth : (maxDepth : Nat) -> (node : XMLNode) -> + postulate MkBoundedDepth : (maxDepth : Nat) -> (node : XMLNode) -> {auto prf : Proofs.nodeDepth node <= maxDepth = True} -> BoundedDepth maxDepth node ||| Predicate: All text is properly escaped public export data ProperlyEscaped : XMLNode -> Type where - MkProperlyEscaped : (node : XMLNode) -> ProperlyEscaped node + postulate MkProperlyEscaped : (node : XMLNode) -> ProperlyEscaped node ||| Predicate: Document is well-formed public export data WellFormed : XMLDocument -> Type where - MkWellFormed : (doc : XMLDocument) -> WellFormed doc + postulate MkWellFormed : (doc : XMLDocument) -> WellFormed doc -------------------------------------------------------------------------------- -- XXE Prevention Proofs @@ -97,7 +97,7 @@ secureDefaultsZeroExpansions = Refl ||| `Data.String` representation supplanting the FFI-opaque one) is ||| available. export -0 builderNoXXE : (builder : ElementBuilder) -> +postulate 0 builderNoXXE : (builder : ElementBuilder) -> NoExternalEntities (renderNode (build builder)) ||| OWED: The builder API never emits `` in rendered output, @@ -108,7 +108,7 @@ export ||| once `isInfixOf` is reflective, or once `renderNode` is refactored to ||| return a structural type that excludes `!DOCTYPE` by construction. export -0 builderNoDTD : (builder : ElementBuilder) -> +postulate 0 builderNoDTD : (builder : ElementBuilder) -> NoDTD (renderNode (build builder)) -------------------------------------------------------------------------------- @@ -134,7 +134,7 @@ entityExpansionBounded opts count tooMany = () ||| `xmlAttrValue` return a structural escaped-string type that ||| character-class excludes raw `&` by construction. export -0 builderNoEntities : (builder : ElementBuilder) -> +postulate 0 builderNoEntities : (builder : ElementBuilder) -> -- Builder escapes & to &, preventing entity references not (isInfixOf "&" (renderNode (build builder)) && not (isInfixOf "&" (renderNode (build builder)) || @@ -156,7 +156,7 @@ export ||| returns a structural `EscapedString` whose constructor character-class ||| excludes raw `<`. export -0 textEscapingSound : (s : String) -> +postulate 0 textEscapingSound : (s : String) -> let escaped = (xmlText s).escaped in not (isInfixOf "<" escaped && not (isInfixOf "<" escaped)) = True @@ -168,7 +168,7 @@ export ||| `unpack` is reflective, or once `xmlAttrValue` returns a structural ||| `EscapedAttrValue` whose constructor character-class excludes raw `"`. export -0 attrEscapingSound : (s : String) -> +postulate 0 attrEscapingSound : (s : String) -> let escaped = (xmlAttrValue s).escaped in not (isInfixOf "\"" escaped && not (isInfixOf """ escaped)) = True @@ -209,7 +209,7 @@ builderElementWellFormed builder = MkWellFormed (MkXMLDocument Nothing Nothing ( ||| to call `isValidXMLName` directly (so the two paths share a single ||| reduction). export -0 elementNameValidation : (name : String) -> +postulate 0 elementNameValidation : (name : String) -> isOk (xmlName name) = True -> isValidXMLName name = True @@ -222,7 +222,7 @@ export ||| once `xmlQName` is rewritten to compose `xmlName pfx` and ||| `xmlName local` so the two arms expose their underlying checks. export -0 qnameComponentsValid : (pfx : String) -> (local : String) -> +postulate 0 qnameComponentsValid : (pfx : String) -> (local : String) -> isOk (xmlQName pfx local) = True -> (isValidXMLName pfx = True, isValidXMLName local = True) @@ -259,7 +259,7 @@ builderDepthConstant builder = () ||| `xmlAttrValue` returns a structural `EscapedAttrValue` indexed by a ||| `List Char` whose constructor excludes `'"'` by construction. export -0 attrValueNoQuotes : (value : String) -> +postulate 0 attrValueNoQuotes : (value : String) -> let attrVal = xmlAttrValue value in all (\c => c /= '"' || False) (unpack attrVal.escaped) = True @@ -313,7 +313,7 @@ piNotXmlDecl target isXml = () ||| refactored to a structurally-recursive proof over the `XMLNode` ||| constructors. export -0 nestedElementsSafe : (parent : ElementBuilder) -> (child : XMLNode) -> +postulate 0 nestedElementsSafe : (parent : ElementBuilder) -> (child : XMLNode) -> ProperlyEscaped child -> ProperlyEscaped (build (withChild child parent)) diff --git a/src/Proven/SafeYAML/Proofs.idr b/src/Proven/SafeYAML/Proofs.idr index 090e1aac..93e828e9 100644 --- a/src/Proven/SafeYAML/Proofs.idr +++ b/src/Proven/SafeYAML/Proofs.idr @@ -23,7 +23,7 @@ import Data.String ||| Predicate: YAML has no dangerous tags public export data NoDangerousTags : YAMLValue -> Type where - MkNoDangerousTags : (val : YAMLValue) -> NoDangerousTags val + postulate MkNoDangerousTags : (val : YAMLValue) -> NoDangerousTags val ||| Compute YAML value nesting depth covering @@ -43,20 +43,20 @@ valueDepth (YObject kvs) = S (foldl max 0 (map (valueDepth . snd) kvs)) ||| Predicate: YAML has bounded depth public export data BoundedDepth : Nat -> YAMLValue -> Type where - MkBoundedDepth : (maxDepth : Nat) -> (val : YAMLValue) -> + postulate MkBoundedDepth : (maxDepth : Nat) -> (val : YAMLValue) -> {auto prf : valueDepth val <= maxDepth = True} -> BoundedDepth maxDepth val ||| Predicate: Value is scalar (no alias expansion possible) public export data IsScalar : YAMLValue -> Type where - NullScalar : IsScalar YNull - BoolScalar : IsScalar (YBool b) - IntScalar : IsScalar (YInt i) - FloatScalar : IsScalar (YFloat f) - StringScalar : IsScalar (YString s) - BinaryScalar : IsScalar (YBinary bs) - TimestampScalar : IsScalar (YTimestamp ts) + postulate NullScalar : IsScalar YNull + postulate BoolScalar : IsScalar (YBool b) + postulate IntScalar : IsScalar (YInt i) + postulate FloatScalar : IsScalar (YFloat f) + postulate StringScalar : IsScalar (YString s) + postulate BinaryScalar : IsScalar (YBinary bs) + postulate TimestampScalar : IsScalar (YTimestamp ts) -------------------------------------------------------------------------------- -- Tag Safety Proofs @@ -102,7 +102,7 @@ javaObjectIsDangerous = Refl ||| available, or refactor to a `YAMLTag` enum where decidable ||| equality reduces by Refl. export -0 standardTagsSafe : (tag : String) -> +postulate 0 standardTagsSafe : (tag : String) -> tag `elem` ["!!null", "!!bool", "!!int", "!!float", "!!str", "!!seq", "!!map"] = True -> isDangerousTag tag = False @@ -136,7 +136,7 @@ export ||| or refactor to a `YAMLTag` enum where decidable equality reduces ||| by Refl. export -0 secureDefaultsBlockDangerous : (tag : String) -> +postulate 0 secureDefaultsBlockDangerous : (tag : String) -> isDangerousTag tag = True -> isBlockedTag secureDefaults tag = True @@ -288,7 +288,7 @@ parseYAMLWith _ _ = Ok YNull ||| pattern is established, at which point this becomes a structural ||| `Right (val ** Refl)` over the parser's case-tree. export -0 parsingNeverCrashes : (input : String) -> (opts : YAMLSecurityOptions) -> +postulate 0 parsingNeverCrashes : (input : String) -> (opts : YAMLSecurityOptions) -> (err : YAMLError ** parseYAMLWith opts input = Err err) `Either` (val : YAMLValue ** parseYAMLWith opts input = Ok val) @@ -406,7 +406,7 @@ Attacks Prevented: Example blocked input: yaml !!python/object/apply:os.system - args: ['rm -rf /'] + postulate args: ['rm -rf /'] !!python/object/new:yaml.UnsafeLoader """