diff --git a/src/Proven/FFI/SafeArgs.idr b/src/Proven/FFI/SafeArgs.idr index 9b08ef21..5da29a94 100644 --- a/src/Proven/FFI/SafeArgs.idr +++ b/src/Proven/FFI/SafeArgs.idr @@ -315,4 +315,4 @@ proven_idris_args_extract_equals_value arg = (_, val) => if null (unpack val) then (1, "no equals sign found") - else (0, drop 1 val) + else (0, pack (drop 1 (unpack val))) diff --git a/src/Proven/FFI/SafeCron.idr b/src/Proven/FFI/SafeCron.idr index cc1f60d1..ba668f50 100644 --- a/src/Proven/FFI/SafeCron.idr +++ b/src/Proven/FFI/SafeCron.idr @@ -20,6 +20,7 @@ module Proven.FFI.SafeCron import Proven.SafeCron import Proven.Core import Data.String +import Data.List1 %default total @@ -32,6 +33,12 @@ encodeBool : Bool -> Int encodeBool False = 0 encodeBool True = 1 +||| Check an FFI integer before converting it to a natural-number cron field. +||| In particular, negative inputs must not be accepted through a saturating cast. +inIntBounds : FieldBounds -> Int -> Bool +inIntBounds bounds value = + value >= cast bounds.minVal && value <= cast bounds.maxVal + ||| Encode field type encodeCronFieldType : CronField -> Int encodeCronFieldType Any = 0 @@ -91,27 +98,27 @@ proven_idris_cron_day_of_week_max = cast dayOfWeekBounds.maxVal export proven_idris_cron_is_valid_minute : Int -> Int proven_idris_cron_is_valid_minute val = - encodeBool (inBounds minuteBounds (cast val)) + encodeBool (inIntBounds minuteBounds val) export proven_idris_cron_is_valid_hour : Int -> Int proven_idris_cron_is_valid_hour val = - encodeBool (inBounds hourBounds (cast val)) + encodeBool (inIntBounds hourBounds val) export proven_idris_cron_is_valid_day_of_month : Int -> Int proven_idris_cron_is_valid_day_of_month val = - encodeBool (inBounds dayOfMonthBounds (cast val)) + encodeBool (inIntBounds dayOfMonthBounds val) export proven_idris_cron_is_valid_month : Int -> Int proven_idris_cron_is_valid_month val = - encodeBool (inBounds monthBounds (cast val)) + encodeBool (inIntBounds monthBounds val) export proven_idris_cron_is_valid_day_of_week : Int -> Int proven_idris_cron_is_valid_day_of_week val = - encodeBool (inBounds dayOfWeekBounds (cast val)) + encodeBool (inIntBounds dayOfWeekBounds val) export proven_idris_cron_validate_single : Int -> Int -> Int -> Int @@ -136,11 +143,11 @@ export proven_idris_cron_is_valid_time : Int -> Int -> Int -> Int -> Int -> Int proven_idris_cron_is_valid_time minute hour dayOfMonth month dayOfWeek = encodeBool ( - inBounds minuteBounds (cast minute) && - inBounds hourBounds (cast hour) && - inBounds dayOfMonthBounds (cast dayOfMonth) && - inBounds monthBounds (cast month) && - inBounds dayOfWeekBounds (cast dayOfWeek) + inIntBounds minuteBounds minute && + inIntBounds hourBounds hour && + inIntBounds dayOfMonthBounds dayOfMonth && + inIntBounds monthBounds month && + inIntBounds dayOfWeekBounds dayOfWeek ) export @@ -165,7 +172,7 @@ proven_idris_cron_is_too_frequent cronStr = export proven_idris_cron_estimate_interval_minutes : String -> Int proven_idris_cron_estimate_interval_minutes cronStr = - let parts = split (== ' ') cronStr + let parts = filter (/= "") (forget (split (== ' ') cronStr)) in case parts of [minute, _, _, _, _] => if minute == "*" then 1 -- Every minute @@ -179,13 +186,10 @@ proven_idris_cron_estimate_interval_minutes cronStr = where parseStep : String -> Maybe Nat parseStep s = - case split (== '/') s of - [_, stepStr] => parsePositive stepStr + case forget (split (== '/') s) of + [_, stepStr] => parsePositive {a = Nat} stepStr _ => Nothing - parsePositive : String -> Maybe Nat - parsePositive s = parsePositive (cast {to = Integer} s) - export proven_idris_cron_is_at_least_hourly : String -> Int proven_idris_cron_is_at_least_hourly cronStr = @@ -310,7 +314,7 @@ proven_idris_cron_is_monthly cronStr = export proven_idris_cron_field_count : String -> Int proven_idris_cron_field_count cronStr = - cast (length (split (== ' ') cronStr)) + cast (length (filter (/= "") (forget (split (== ' ') cronStr)))) export proven_idris_cron_has_five_fields : String -> Int diff --git a/src/Proven/FFI/SafeFile.idr b/src/Proven/FFI/SafeFile.idr index ad588072..23b8b462 100644 --- a/src/Proven/FFI/SafeFile.idr +++ b/src/Proven/FFI/SafeFile.idr @@ -26,6 +26,7 @@ import Proven.SafeFile.Types import Proven.SafeFile.Operations import Proven.Core import Data.String +import Data.List1 %default total @@ -88,13 +89,13 @@ proven_idris_file_has_dangerous_pattern path = export proven_idris_file_is_in_allowed_dir : String -> String -> Int proven_idris_file_is_in_allowed_dir allowedDirs path = - let dirs = split (== ',') allowedDirs + let dirs = forget (split (== ',') allowedDirs) in encodeBool (isInAllowedDir dirs path) export proven_idris_file_is_blocked_path : String -> String -> Int proven_idris_file_is_blocked_path blockedPaths path = - let paths = split (== ',') blockedPaths + let paths = forget (split (== ',') blockedPaths) in encodeBool (isBlockedPath paths path) -------------------------------------------------------------------------------- @@ -120,7 +121,7 @@ proven_idris_file_extension path = encodeMaybeString (extension path) export proven_idris_file_join_path : String -> String proven_idris_file_join_path componentsStr = - let components = split (== ',') componentsStr + let components = forget (split (== ',') componentsStr) in joinPath components export diff --git a/src/Proven/FFI/SafeHeader.idr b/src/Proven/FFI/SafeHeader.idr index c147edb3..cac1e2d0 100644 --- a/src/Proven/FFI/SafeHeader.idr +++ b/src/Proven/FFI/SafeHeader.idr @@ -141,12 +141,12 @@ proven_idris_header_is_size_error errorMsg = export proven_idris_header_max_name_length : Int -proven_idris_header_max_name_length = cast maxHeaderNameLength +proven_idris_header_max_name_length = cast maxNameLength export proven_idris_header_max_value_length : Int -proven_idris_header_max_value_length = cast maxHeaderValueLength +proven_idris_header_max_value_length = cast maxValueLength export proven_idris_header_max_total_size : Int -proven_idris_header_max_total_size = cast maxTotalHeaderSize +proven_idris_header_max_total_size = cast maxTotalSize diff --git a/src/Proven/FFI/SafeLRU.idr b/src/Proven/FFI/SafeLRU.idr index 2c6d0ec2..b9edd03c 100644 --- a/src/Proven/FFI/SafeLRU.idr +++ b/src/Proven/FFI/SafeLRU.idr @@ -88,8 +88,7 @@ proven_idris_lru_fill_ratio_percent currentSize capacity = export proven_idris_lru_is_nearly_full : Int -> Int -> Int -> Int proven_idris_lru_is_nearly_full currentSize capacity threshold = - let percent = cast (currentSize * 100) / cast capacity - in encodeBool (percent >= cast threshold) + encodeBool (capacity > 0 && currentSize * 100 >= threshold * capacity) -------------------------------------------------------------------------------- -- Hit Rate Calculation @@ -97,24 +96,24 @@ proven_idris_lru_is_nearly_full currentSize capacity threshold = export proven_idris_lru_hit_rate : Int -> Int -> Double -proven_idris_lru_hit_rate hits total = - if total == 0 then 0.0 - else cast hits / cast total +proven_idris_lru_hit_rate hits totalCount = + if totalCount == 0 then 0.0 + else cast hits / cast totalCount export proven_idris_lru_hit_rate_percent : Int -> Int -> Double -proven_idris_lru_hit_rate_percent hits total = - proven_idris_lru_hit_rate hits total * 100.0 +proven_idris_lru_hit_rate_percent hits totalCount = + proven_idris_lru_hit_rate hits totalCount * 100.0 export proven_idris_lru_miss_rate : Int -> Int -> Double -proven_idris_lru_miss_rate hits total = - 1.0 - proven_idris_lru_hit_rate hits total +proven_idris_lru_miss_rate hits totalCount = + 1.0 - proven_idris_lru_hit_rate hits totalCount export proven_idris_lru_miss_rate_percent : Int -> Int -> Double -proven_idris_lru_miss_rate_percent hits total = - proven_idris_lru_miss_rate hits total * 100.0 +proven_idris_lru_miss_rate_percent hits totalCount = + proven_idris_lru_miss_rate hits totalCount * 100.0 -------------------------------------------------------------------------------- -- Eviction Statistics @@ -180,11 +179,11 @@ proven_idris_lru_optimal_capacity_for_hit_rate avgAccesses targetHitRate = export proven_idris_lru_recommend_resize : Int -> Int -> Int -> Int -> Int -proven_idris_lru_recommend_resize currentSize capacity hits total = - let hitRate = proven_idris_lru_hit_rate hits total +proven_idris_lru_recommend_resize currentSize capacity hits totalCount = + let hitRate = proven_idris_lru_hit_rate hits totalCount targetHitRate = 0.85 -- Target 85% hit rate in if hitRate < targetHitRate - then cast (cast capacity * 1.5) -- Increase capacity by 50% + then cast (the Double (cast capacity) * 1.5) -- Increase capacity by 50% else capacity -------------------------------------------------------------------------------- @@ -193,8 +192,8 @@ proven_idris_lru_recommend_resize currentSize capacity hits total = export proven_idris_lru_is_efficient : Int -> Int -> Double -> Int -proven_idris_lru_is_efficient hits total minHitRate = - let rate = proven_idris_lru_hit_rate hits total +proven_idris_lru_is_efficient hits totalCount minHitRate = + let rate = proven_idris_lru_hit_rate hits totalCount in encodeBool (rate >= minHitRate) export diff --git a/src/Proven/FFI/SafeMCP.idr b/src/Proven/FFI/SafeMCP.idr index 5326a2f4..b241d977 100644 --- a/src/Proven/FFI/SafeMCP.idr +++ b/src/Proven/FFI/SafeMCP.idr @@ -81,7 +81,8 @@ proven_idris_mcp_max_result_size = cast maxResultSize export proven_idris_mcp_is_result_size_ok : Int -> Int -proven_idris_mcp_is_result_size_ok size = encodeBool (cast size <= maxResultSize) +proven_idris_mcp_is_result_size_ok size = + encodeBool (size >= 0 && size <= cast maxResultSize) -------------------------------------------------------------------------------- -- MCP Role Info @@ -89,8 +90,8 @@ proven_idris_mcp_is_result_size_ok size = encodeBool (cast size <= maxResultSize export proven_idris_mcp_role_name : Int -> String -proven_idris_mcp_role_name 0 = show User -proven_idris_mcp_role_name 1 = show Assistant -proven_idris_mcp_role_name 2 = show System -proven_idris_mcp_role_name 3 = show Tool +proven_idris_mcp_role_name 0 = show Proven.SafeMCP.User +proven_idris_mcp_role_name 1 = show Proven.SafeMCP.Assistant +proven_idris_mcp_role_name 2 = show Proven.SafeMCP.System +proven_idris_mcp_role_name 3 = show Proven.SafeMCP.Tool proven_idris_mcp_role_name _ = "unknown" diff --git a/src/Proven/FFI/SafeMath.idr b/src/Proven/FFI/SafeMath.idr index 0dd06eda..eab7451e 100644 --- a/src/Proven/FFI/SafeMath.idr +++ b/src/Proven/FFI/SafeMath.idr @@ -34,7 +34,7 @@ encodeResult (Just x) = (0, x) export proven_idris_math_div : Integer -> Integer -> (Int, Integer) proven_idris_math_div numerator denominator = - encodeResult (div numerator denominator) + encodeResult (safeDiv numerator denominator) export proven_idris_math_div_or : Integer -> Integer -> Integer -> Integer @@ -44,7 +44,7 @@ proven_idris_math_div_or def numerator denominator = export proven_idris_math_mod : Integer -> Integer -> (Int, Integer) proven_idris_math_mod numerator denominator = - encodeResult (mod numerator denominator) + encodeResult (safeMod numerator denominator) -------------------------------------------------------------------------------- -- Checked Arithmetic (Overflow Detection) @@ -145,8 +145,8 @@ proven_idris_math_max a b = export proven_idris_math_percent_of : Integer -> Integer -> (Int, Integer) -proven_idris_math_percent_of percent total = - encodeResult (percentOf percent total) +proven_idris_math_percent_of percent totalValue = + encodeResult (percentOf percent totalValue) export proven_idris_math_as_percent : Integer -> Integer -> (Int, Integer) diff --git a/src/Proven/FFI/SafeMonotonic.idr b/src/Proven/FFI/SafeMonotonic.idr index 7dcde6b3..2f7d89b6 100644 --- a/src/Proven/FFI/SafeMonotonic.idr +++ b/src/Proven/FFI/SafeMonotonic.idr @@ -285,8 +285,8 @@ proven_idris_monotonic_delta current previous = export proven_idris_monotonic_average : Int -> Int -> Int -proven_idris_monotonic_average total count = - if count == 0 then 0 else total `div` count +proven_idris_monotonic_average sum count = + if count == 0 then 0 else sum `div` count export proven_idris_lamport_clock_drift : Int -> Int -> Int diff --git a/src/Proven/FFI/SafeNetwork.idr b/src/Proven/FFI/SafeNetwork.idr index 7481a106..205eb09a 100644 --- a/src/Proven/FFI/SafeNetwork.idr +++ b/src/Proven/FFI/SafeNetwork.idr @@ -46,7 +46,7 @@ encodeMaybeIPv6 (Just ip) = (0, show ip) ||| Encode Maybe Port as (status, error) encodeMaybePort : Maybe Port -> (Int, String) encodeMaybePort Nothing = (1, "Invalid port number") -encodeMaybePort (Just port) = (0, show (portToNat port)) +encodeMaybePort (Just port) = (0, show (portValue port)) ||| Encode Maybe MACAddress as (status, address) encodeMaybeMAC : Maybe MACAddress -> (Int, String) @@ -99,7 +99,7 @@ proven_idris_ipv4_is_broadcast : String -> Int proven_idris_ipv4_is_broadcast s = case parseIPv4 s of Nothing => 0 - Just ip => ip == broadcast + Just ip => encodeBool (isBroadcastIPv4 ip) export proven_idris_ipv4_is_global : String -> Int @@ -156,7 +156,7 @@ proven_idris_ipv6_is_global : String -> Int proven_idris_ipv6_is_global s = case parseIPv6 s of Nothing => 0 - Just ip => encodeBool (isGlobalIPv6 ip) + Just ip => encodeBool (isGlobalUnicastIPv6 ip) export proven_idris_ipv6_is_multicast : String -> Int @@ -213,7 +213,7 @@ proven_idris_port_is_well_known : Int -> Int proven_idris_port_is_well_known n = case mkPort (cast n) of Nothing => 0 - Just port => encodeBool (isWellKnownPort port) + Just port => encodeBool (isSystemPort port) export proven_idris_port_is_registered : Int -> Int @@ -227,14 +227,14 @@ proven_idris_port_is_ephemeral : Int -> Int proven_idris_port_is_ephemeral n = case mkPort (cast n) of Nothing => 0 - Just port => encodeBool (isEphemeralPort port) + Just port => encodeBool (isDynamicPort port) export proven_idris_port_is_privileged : Int -> Int proven_idris_port_is_privileged n = case mkPort (cast n) of Nothing => 0 - Just port => encodeBool (isPrivilegedPort port) + Just port => encodeBool (isSystemPort port) -------------------------------------------------------------------------------- -- MAC Address Operations diff --git a/src/Proven/FFI/SafeOAuth.idr b/src/Proven/FFI/SafeOAuth.idr index 403b68a7..0b86152e 100644 --- a/src/Proven/FFI/SafeOAuth.idr +++ b/src/Proven/FFI/SafeOAuth.idr @@ -11,6 +11,8 @@ module Proven.FFI.SafeOAuth import Proven.SafeOAuth +import Data.String +import Data.List1 %default total @@ -63,7 +65,7 @@ proven_idris_oauth_is_secure_redirect_uri = encodeBool . isSecureRedirectUri export proven_idris_oauth_is_valid_redirect_uri : String -> String -> Int proven_idris_oauth_is_valid_redirect_uri uri allowedCsv = - let allowed = split (== ',') allowedCsv + let allowed = forget (split (== ',') allowedCsv) in encodeBool (isValidRedirectUri uri allowed) -------------------------------------------------------------------------------- @@ -96,7 +98,7 @@ proven_idris_oauth_validate_code_exchange : String -> String -> String -> String proven_idris_oauth_validate_code_exchange sentState receivedState redirectUri allowedCsv = case (mkOAuthState sentState, mkOAuthState receivedState) of (Just s, Just r) => - let allowed = split (== ',') allowedCsv + let allowed = forget (split (== ',') allowedCsv) in case validateCodeExchange s r redirectUri allowed of Left StateMismatch => (1, "State mismatch (CSRF)") Left InsecureRedirect => (1, "Insecure redirect URI") diff --git a/src/Proven/FFI/SafeProbability.idr b/src/Proven/FFI/SafeProbability.idr index a219ac14..4ecc642d 100644 --- a/src/Proven/FFI/SafeProbability.idr +++ b/src/Proven/FFI/SafeProbability.idr @@ -49,7 +49,7 @@ proven_idris_prob_certain = certain.value export proven_idris_prob_impossible : Double -proven_idris_prob_impossible = impossible.value +proven_idris_prob_impossible = impossibleEvent.value export proven_idris_prob_fair : Double diff --git a/src/Proven/FFI/SafeRateLimiter.idr b/src/Proven/FFI/SafeRateLimiter.idr index f2687681..61d13448 100644 --- a/src/Proven/FFI/SafeRateLimiter.idr +++ b/src/Proven/FFI/SafeRateLimiter.idr @@ -65,8 +65,8 @@ export proven_idris_ratelimit_tokens_after_refill : Int -> Int -> Int -> Int -> Int proven_idris_ratelimit_tokens_after_refill currentTokens refillRate elapsedTime capacity = let newTokens = proven_idris_ratelimit_tokens_to_add refillRate elapsedTime capacity - total = currentTokens + newTokens - in if total > capacity then capacity else total + tokenTotal = currentTokens + newTokens + in if tokenTotal > capacity then capacity else tokenTotal export proven_idris_ratelimit_can_acquire : Int -> Int -> Int @@ -179,10 +179,10 @@ proven_idris_ratelimit_recommend_refill_rate targetRequestsPerSec intervalSize = targetRequestsPerSec * intervalSize export -proven_idris_ratelimit_recommend_window_size : Int -> Int +proven_idris_ratelimit_recommend_window_size : Int -> Int -> Int proven_idris_ratelimit_recommend_window_size targetRequestsPerSec maxBurst = - -- Window size should be large enough to smooth out bursts - if targetRequestsPerSec == 0 then maxBurst + -- Window size should be large enough to smooth out bursts. + if targetRequestsPerSec <= 0 then max 0 maxBurst else max maxBurst (maxBurst `div` targetRequestsPerSec) -------------------------------------------------------------------------------- @@ -204,8 +204,7 @@ proven_idris_ratelimit_request_utilization currentCount maxRequests = export proven_idris_ratelimit_is_throttled : Int -> Int -> Int -> Int proven_idris_ratelimit_is_throttled currentCount maxRequests threshold = - let percent = cast (currentCount * 100) / cast maxRequests - in encodeBool (percent >= cast threshold) + encodeBool (maxRequests > 0 && currentCount * 100 >= threshold * maxRequests) -------------------------------------------------------------------------------- -- Time Calculations diff --git a/src/Proven/FFI/SafeRegex.idr b/src/Proven/FFI/SafeRegex.idr index 7be16acd..125249bc 100644 --- a/src/Proven/FFI/SafeRegex.idr +++ b/src/Proven/FFI/SafeRegex.idr @@ -134,43 +134,43 @@ proven_idris_regex_quick_replace_all pattern input replacement = export proven_idris_regex_email_pattern : String -proven_idris_regex_email_pattern = emailPattern +proven_idris_regex_email_pattern = emailPatternSource export proven_idris_regex_url_pattern : String -proven_idris_regex_url_pattern = urlPattern +proven_idris_regex_url_pattern = urlPatternSource export proven_idris_regex_ipv4_pattern : String -proven_idris_regex_ipv4_pattern = ipv4Pattern +proven_idris_regex_ipv4_pattern = ipv4PatternSource export proven_idris_regex_uuid_pattern : String -proven_idris_regex_uuid_pattern = uuidPattern +proven_idris_regex_uuid_pattern = uuidPatternSource export proven_idris_regex_integer_pattern : String -proven_idris_regex_integer_pattern = integerPattern +proven_idris_regex_integer_pattern = integerPatternSource export proven_idris_regex_decimal_pattern : String -proven_idris_regex_decimal_pattern = decimalPattern +proven_idris_regex_decimal_pattern = decimalPatternSource export proven_idris_regex_identifier_pattern : String -proven_idris_regex_identifier_pattern = identifierPattern +proven_idris_regex_identifier_pattern = identifierPatternSource export proven_idris_regex_hex_color_pattern : String -proven_idris_regex_hex_color_pattern = hexColorPattern +proven_idris_regex_hex_color_pattern = hexColorPatternSource export proven_idris_regex_date_pattern : String -proven_idris_regex_date_pattern = datePattern +proven_idris_regex_date_pattern = datePatternSource export proven_idris_regex_time_pattern : String -proven_idris_regex_time_pattern = timePattern +proven_idris_regex_time_pattern = timePatternSource -------------------------------------------------------------------------------- -- Complexity Level Constants diff --git a/src/Proven/FFI/SafeResource.idr b/src/Proven/FFI/SafeResource.idr index 4901e3ae..56981528 100644 --- a/src/Proven/FFI/SafeResource.idr +++ b/src/Proven/FFI/SafeResource.idr @@ -377,18 +377,18 @@ export proven_idris_pool_should_expand : Int -> Int -> Int -> Int proven_idris_pool_should_expand inUse available maxSize = -- Should expand if utilization > 80% and not at max - let total = inUse + available - utilization = if total == 0 then 0.0 - else cast inUse / cast total - in encodeBool (utilization > 0.8 && total < maxSize) + let poolSize = inUse + available + utilization = if poolSize == 0 then 0.0 + else cast inUse / cast poolSize + in encodeBool (utilization > 0.8 && poolSize < maxSize) export proven_idris_pool_should_shrink : Int -> Int -> Int proven_idris_pool_should_shrink inUse available = -- Should shrink if many resources idle - let total = inUse + available - utilization = if total == 0 then 0.0 - else cast inUse / cast total + let poolSize = inUse + available + utilization = if poolSize == 0 then 0.0 + else cast inUse / cast poolSize in encodeBool (utilization < 0.2 && available > 5) -------------------------------------------------------------------------------- diff --git a/src/Proven/FFI/SafeRetry.idr b/src/Proven/FFI/SafeRetry.idr index f9c0368b..98b7418a 100644 --- a/src/Proven/FFI/SafeRetry.idr +++ b/src/Proven/FFI/SafeRetry.idr @@ -46,6 +46,25 @@ encodeBool : Bool -> Int encodeBool False = 0 encodeBool True = 1 +||| Convert an FFI retry count to bounded structural fuel. Public validation +||| caps retry policies at 100 attempts; calculations apply the same cap so an +||| unchecked foreign caller cannot trigger unbounded recursion. +boundedRetryFuel : Int -> Nat +boundedRetryFuel count = + if count <= 0 then 0 + else if count > 100 then 100 + else cast count + +intPower : Int -> Nat -> Int +intPower _ Z = 1 +intPower base (S exponent) = base * intPower base exponent + +sumExponentialDelays : Nat -> Int -> Int -> Int -> Int +sumExponentialDelays Z _ _ accumulator = accumulator +sumExponentialDelays (S remaining) delay multiplier accumulator = + sumExponentialDelays remaining (delay * multiplier) multiplier + (accumulator + delay) + -------------------------------------------------------------------------------- -- Backoff Strategy Encoding -------------------------------------------------------------------------------- @@ -87,11 +106,7 @@ proven_idris_retry_linear_delay initial increment attempt = export proven_idris_retry_exponential_delay : Int -> Int -> Int -> Int proven_idris_retry_exponential_delay initial multiplier attempt = - initial * power multiplier attempt - where - power : Int -> Int -> Int - power _ 0 = 1 - power b n = if n > 0 then b * power b (n - 1) else 1 + initial * intPower multiplier (boundedRetryFuel attempt) export proven_idris_retry_delay_with_cap : Int -> Int -> Int @@ -224,13 +239,8 @@ proven_idris_retry_average_delay totalDelay totalOps = export proven_idris_retry_max_total_delay : Int -> Int -> Int -> Int proven_idris_retry_max_total_delay maxAttempts initialDelay multiplier = - -- Calculate max delay for exponential backoff - let helper : Int -> Int -> Int -> Int - helper 0 _ acc = acc - helper n delay acc = - let nextDelay = delay * multiplier - in helper (n - 1) nextDelay (acc + delay) - in helper maxAttempts initialDelay 0 + -- Calculate the delay with the same 100-attempt limit as policy validation. + sumExponentialDelays (boundedRetryFuel maxAttempts) initialDelay multiplier 0 export proven_idris_retry_recommend_max_attempts : Int -> Int diff --git a/src/Proven/FFI/SafeSQL.idr b/src/Proven/FFI/SafeSQL.idr index b258e4a9..585ad842 100644 --- a/src/Proven/FFI/SafeSQL.idr +++ b/src/Proven/FFI/SafeSQL.idr @@ -51,13 +51,13 @@ decodeSQLDialect _ = Nothing ||| Encode Result ParameterizedQuery as (status, sql, paramCount) encodeQueryResult : Result SQLError ParameterizedQuery -> (Int, String, Int) -encodeQueryResult (Err err) = (1, friendlyError err, 0) +encodeQueryResult (Err err) = (1, show err, 0) encodeQueryResult (Ok query) = (0, toSQL query, cast (length (getParams query))) ||| Encode Result () as (status, error) encodeValidationResult : Result SQLError () -> (Int, String) -encodeValidationResult (Err err) = (1, friendlyError err) +encodeValidationResult (Err err) = (1, show err) encodeValidationResult (Ok ()) = (0, "") -------------------------------------------------------------------------------- @@ -95,10 +95,10 @@ proven_idris_sql_select_from dialectInt tableName = Nothing => (1, "Invalid SQL dialect", 0) Just dialect => case selectFrom dialect tableName of - Err err => (1, friendlyError err, 0) + Err err => (1, show err, 0) Ok builder => case build builder of - Err err => (1, friendlyError err, 0) + Err err => (1, show err, 0) Ok query => encodeQueryResult (Ok query) export @@ -122,14 +122,14 @@ proven_idris_sql_is_valid_identifier name = export proven_idris_sql_validate_table_name : String -> (Int, String) proven_idris_sql_validate_table_name name = - case mkTableName name of + case mkIdentifier name of Nothing => (1, "Invalid table name: " ++ name) Just _ => (0, name) export proven_idris_sql_validate_column_name : String -> (Int, String) proven_idris_sql_validate_column_name name = - case mkColumnName name of + case mkIdentifier name of Nothing => (1, "Invalid column name: " ++ name) Just _ => (0, name) @@ -143,22 +143,23 @@ proven_idris_sql_analyze_for_injection text = case analyzeForInjection text of Safe => 0 -- Safe Warning _ => 1 -- Warning (suspicious but might be OK) - Critical _ => 2 -- Critical (definitely injection) + Dangerous _ => 2 -- Likely injection + Critical _ => 2 -- Definite injection export proven_idris_sql_has_sql_keywords : String -> Int proven_idris_sql_has_sql_keywords text = - encodeBool (hasSQLKeywords text) + encodeBool (any (\kw => isInfixOf kw (toUpper text)) dangerousKeywords) export proven_idris_sql_has_comment_syntax : String -> Int proven_idris_sql_has_comment_syntax text = - encodeBool (hasCommentSyntax text) + encodeBool (isInfixOf "--" text || isInfixOf "/*" text || isInfixOf "*/" text) export proven_idris_sql_has_string_escape : String -> Int proven_idris_sql_has_string_escape text = - encodeBool (hasStringEscape text) + encodeBool (isInfixOf "\\" text || isInfixOf "'" text || isInfixOf "\"" text) -------------------------------------------------------------------------------- -- Error Classification diff --git a/src/Proven/FFI/SafeString.idr b/src/Proven/FFI/SafeString.idr index cbde1f34..044e5761 100644 --- a/src/Proven/FFI/SafeString.idr +++ b/src/Proven/FFI/SafeString.idr @@ -98,12 +98,12 @@ proven_idris_string_is_blank s = export proven_idris_string_contains : String -> String -> Int proven_idris_string_contains needle haystack = - encodeBool (contains needle haystack) + encodeBool (containsSubstr needle haystack) export proven_idris_string_starts_with : String -> String -> Int -proven_idris_string_starts_with prefix s = - encodeBool (startsWith prefix s) +proven_idris_string_starts_with prefixText s = + encodeBool (startsWith prefixText s) export proven_idris_string_ends_with : String -> String -> Int @@ -116,7 +116,7 @@ proven_idris_string_ends_with suffix s = export proven_idris_string_trim : String -> String -proven_idris_string_trim s = trim s +proven_idris_string_trim s = Proven.SafeString.trim s export proven_idris_string_trim_left : String -> String @@ -129,12 +129,12 @@ proven_idris_string_trim_right s = trimRight s export proven_idris_string_pad_left : Int -> Int -> String -> String proven_idris_string_pad_left targetLen padCharCode s = - padLeft (decodeNat targetLen) (decodeChar padCharCode) s + Proven.SafeString.padLeft (decodeNat targetLen) (decodeChar padCharCode) s export proven_idris_string_pad_right : Int -> Int -> String -> String proven_idris_string_pad_right targetLen padCharCode s = - padRight (decodeNat targetLen) (decodeChar padCharCode) s + Proven.SafeString.padRight (decodeNat targetLen) (decodeChar padCharCode) s export proven_idris_string_truncate : Int -> String -> String diff --git a/src/Proven/FFI/SafeTransaction.idr b/src/Proven/FFI/SafeTransaction.idr index ffec1d00..0627e5b4 100644 --- a/src/Proven/FFI/SafeTransaction.idr +++ b/src/Proven/FFI/SafeTransaction.idr @@ -231,36 +231,36 @@ proven_idris_tx_can_rollback_to_savepoint status savepointOpCount = export proven_idris_tx_success_rate : Int -> Int -> Double -proven_idris_tx_success_rate committed total = - if total == 0 then 0.0 - else cast committed / cast total +proven_idris_tx_success_rate committed totalCount = + if totalCount == 0 then 0.0 + else cast committed / cast totalCount export proven_idris_tx_success_rate_percent : Int -> Int -> Double -proven_idris_tx_success_rate_percent committed total = - proven_idris_tx_success_rate committed total * 100.0 +proven_idris_tx_success_rate_percent committed totalCount = + proven_idris_tx_success_rate committed totalCount * 100.0 export proven_idris_tx_rollback_rate : Int -> Int -> Double -proven_idris_tx_rollback_rate rolledBack total = - if total == 0 then 0.0 - else cast rolledBack / cast total +proven_idris_tx_rollback_rate rolledBack totalCount = + if totalCount == 0 then 0.0 + else cast rolledBack / cast totalCount export proven_idris_tx_rollback_rate_percent : Int -> Int -> Double -proven_idris_tx_rollback_rate_percent rolledBack total = - proven_idris_tx_rollback_rate rolledBack total * 100.0 +proven_idris_tx_rollback_rate_percent rolledBack totalCount = + proven_idris_tx_rollback_rate rolledBack totalCount * 100.0 export proven_idris_tx_failure_rate : Int -> Int -> Double -proven_idris_tx_failure_rate failed total = - if total == 0 then 0.0 - else cast failed / cast total +proven_idris_tx_failure_rate failed totalCount = + if totalCount == 0 then 0.0 + else cast failed / cast totalCount export proven_idris_tx_failure_rate_percent : Int -> Int -> Double -proven_idris_tx_failure_rate_percent failed total = - proven_idris_tx_failure_rate failed total * 100.0 +proven_idris_tx_failure_rate_percent failed totalCount = + proven_idris_tx_failure_rate failed totalCount * 100.0 export proven_idris_tx_average_operations : Int -> Int -> Double @@ -282,9 +282,9 @@ proven_idris_tx_conflict_count count = count export proven_idris_tx_conflict_rate : Int -> Int -> Double -proven_idris_tx_conflict_rate conflicts total = - if total == 0 then 0.0 - else cast conflicts / cast total +proven_idris_tx_conflict_rate conflicts totalCount = + if totalCount == 0 then 0.0 + else cast conflicts / cast totalCount export proven_idris_tx_should_retry : Int -> Int -> Int diff --git a/src/Proven/FFI/SafeUUID.idr b/src/Proven/FFI/SafeUUID.idr index dd7c5f15..3ae8bf74 100644 --- a/src/Proven/FFI/SafeUUID.idr +++ b/src/Proven/FFI/SafeUUID.idr @@ -12,13 +12,15 @@ encodeBool : Bool -> Int encodeBool False = 0 encodeBool True = 1 --- UUID version encoding: V1=1, V2=2, V3=3, V4=4, V5=5 +-- UUID version encoding: known versions preserve their number; other nibbles +-- preserve the version value discovered by the parser. encodeVersion : UUIDVersion -> Int encodeVersion V1 = 1 encodeVersion V2 = 2 encodeVersion V3 = 3 encodeVersion V4 = 4 encodeVersion V5 = 5 +encodeVersion (Unknown n) = cast n -- UUID variant encoding: NCS=0, RFC4122=1, Microsoft=2, Future=3 encodeVariant : UUIDVariant -> Int diff --git a/src/Proven/FFI/SafeUnit.idr b/src/Proven/FFI/SafeUnit.idr index f21f4517..26277b56 100644 --- a/src/Proven/FFI/SafeUnit.idr +++ b/src/Proven/FFI/SafeUnit.idr @@ -45,15 +45,9 @@ encodeBool True = 1 ||| Encode dimension as 7-tuple encodeDimension : Dimension -> (Int, Int, Int, Int, Int, Int, Int) -encodeDimension d = ( - cast d.length, - cast d.mass, - cast d.time, - cast d.current, - cast d.temperature, - cast d.amount, - cast d.luminosity -) +encodeDimension d = + (cast d.length, cast d.mass, cast d.time, cast d.current, + cast d.temperature, cast d.amount, cast d.luminosity) ||| Decode 7-tuple to dimension decodeDimension : Int -> Int -> Int -> Int -> Int -> Int -> Int -> Dimension diff --git a/src/Proven/FFI/SafeVersion.idr b/src/Proven/FFI/SafeVersion.idr index ee09b8ff..65ba7a29 100644 --- a/src/Proven/FFI/SafeVersion.idr +++ b/src/Proven/FFI/SafeVersion.idr @@ -24,6 +24,7 @@ module Proven.FFI.SafeVersion import Proven.SafeVersion import Proven.Core import Data.String +import Data.List1 %default total @@ -67,12 +68,16 @@ proven_idris_version_is_valid s = encodeBool (isValid s) export proven_idris_version_has_prerelease : String -> Int proven_idris_version_has_prerelease s = - encodeBool (isInfixOf "-" s && not (isInfixOf "+" (takeWhile (/= '+') s))) + case parse s of + Nothing => 0 + Just v => encodeBool (not (isNil v.prerelease)) export proven_idris_version_has_build : String -> Int proven_idris_version_has_build s = - encodeBool (isInfixOf "+" s) + case parse s of + Nothing => 0 + Just v => encodeBool (not (isNil v.build)) -------------------------------------------------------------------------------- -- Formatting @@ -81,8 +86,8 @@ proven_idris_version_has_build s = export proven_idris_version_format : Int -> Int -> Int -> String -> String -> String proven_idris_version_format major minor patch prerelease build = - let pre = if prerelease == "" then [] else split (== '.') prerelease - bld = if build == "" then [] else split (== '.') build + let pre = if prerelease == "" then [] else forget (split (== '.') prerelease) + bld = if build == "" then [] else forget (split (== '.') build) v = MkSemVer (cast major) (cast minor) (cast patch) pre bld in format v @@ -164,7 +169,7 @@ proven_idris_version_with_prerelease versionStr prerelease = case parse versionStr of Nothing => versionStr Just v => - let pre = if prerelease == "" then [] else split (== '.') prerelease + let pre = if prerelease == "" then [] else forget (split (== '.') prerelease) in format (withPrerelease pre v) export @@ -173,7 +178,7 @@ proven_idris_version_with_build versionStr build = case parse versionStr of Nothing => versionStr Just v => - let bld = if build == "" then [] else split (== '.') build + let bld = if build == "" then [] else forget (split (== '.') build) in format (withBuild bld v) export diff --git a/src/Proven/SafeArchive/Proofs.idr b/src/Proven/SafeArchive/Proofs.idr index 0ef7d1c5..26944c86 100644 --- a/src/Proven/SafeArchive/Proofs.idr +++ b/src/Proven/SafeArchive/Proofs.idr @@ -28,6 +28,7 @@ module Proven.SafeArchive.Proofs import Proven.SafeArchive %default total +%unbound_implicits off -------------------------------------------------------------------------------- -- EntryType enum self-equality diff --git a/src/Proven/SafeChecksum/Proofs.idr b/src/Proven/SafeChecksum/Proofs.idr index 2f36cfe5..bd1b814e 100644 --- a/src/Proven/SafeChecksum/Proofs.idr +++ b/src/Proven/SafeChecksum/Proofs.idr @@ -46,6 +46,7 @@ import Data.List import Data.Bits %default total +%unbound_implicits off -------------------------------------------------------------------------------- -- Spec-anchor constants (CRC32 IEEE 802.3, Adler-32 modulus) diff --git a/src/Proven/SafeCron.idr b/src/Proven/SafeCron.idr index 6c7425a5..913ee4ef 100644 --- a/src/Proven/SafeCron.idr +++ b/src/Proven/SafeCron.idr @@ -64,18 +64,23 @@ record FieldBounds where minVal : Nat maxVal : Nat +public export minuteBounds : FieldBounds minuteBounds = MkBounds 0 59 +public export hourBounds : FieldBounds hourBounds = MkBounds 0 23 +public export dayOfMonthBounds : FieldBounds dayOfMonthBounds = MkBounds 1 31 +public export monthBounds : FieldBounds monthBounds = MkBounds 1 12 +public export dayOfWeekBounds : FieldBounds dayOfWeekBounds = MkBounds 0 6 diff --git a/src/Proven/SafeCron/Proofs.idr b/src/Proven/SafeCron/Proofs.idr index 01adb55b..d26f51cf 100644 --- a/src/Proven/SafeCron/Proofs.idr +++ b/src/Proven/SafeCron/Proofs.idr @@ -11,6 +11,7 @@ module Proven.SafeCron.Proofs import Proven.SafeCron %default total +%unbound_implicits off -------------------------------------------------------------------------------- -- CronField Show anchors diff --git a/src/Proven/SafeGit/Proofs.idr b/src/Proven/SafeGit/Proofs.idr index 640d78dd..5354cdec 100644 --- a/src/Proven/SafeGit/Proofs.idr +++ b/src/Proven/SafeGit/Proofs.idr @@ -11,6 +11,7 @@ module Proven.SafeGit.Proofs import Proven.SafeGit %default total +%unbound_implicits off ||| DISCHARGED: spec anchor — the 9 ref characters forbidden by ||| git-check-ref-format. `forbiddenRefChars` is `public export` with diff --git a/src/Proven/SafeNetwork/IPv4.idr b/src/Proven/SafeNetwork/IPv4.idr index c6e932d2..193eff00 100644 --- a/src/Proven/SafeNetwork/IPv4.idr +++ b/src/Proven/SafeNetwork/IPv4.idr @@ -174,6 +174,12 @@ isDocumentationIPv4 (MkIPv4 198 51 100 _) = True isDocumentationIPv4 (MkIPv4 203 0 113 _) = True isDocumentationIPv4 _ = False +||| Check if IPv4 is in the RFC 2544 benchmarking range (198.18.0.0/15). +public export +isBenchmarkingIPv4 : IPv4 -> Bool +isBenchmarkingIPv4 (MkIPv4 198 second _ _) = second == 18 || second == 19 +isBenchmarkingIPv4 _ = False + ||| Check if IPv4 is globally routable public export isGlobalIPv4 : IPv4 -> Bool @@ -184,7 +190,8 @@ isGlobalIPv4 ip = not (isMulticastIPv4 ip) && not (isBroadcastIPv4 ip) && not (isReservedIPv4 ip) && - not (isDocumentationIPv4 ip) + not (isDocumentationIPv4 ip) && + not (isBenchmarkingIPv4 ip) -------------------------------------------------------------------------------- -- Network Classes (Historical) diff --git a/src/Proven/SafeProbability.idr b/src/Proven/SafeProbability.idr index a58bc20b..e115e1b5 100644 --- a/src/Proven/SafeProbability.idr +++ b/src/Proven/SafeProbability.idr @@ -55,8 +55,8 @@ certain = MkProb 1.0 ||| Impossible event (probability = 0) public export -impossible : Probability -impossible = MkProb 0.0 +impossibleEvent : Probability +impossibleEvent = MkProb 0.0 ||| Fair coin flip (probability = 0.5) public export @@ -112,8 +112,8 @@ toOdds (MkProb p) = public export fromOdds : Odds -> Probability fromOdds (MkOdds f a) = - let total = f + a - in MkProb (if total == 0.0 then 0.0 else f / total) + let sumOdds = f + a + in MkProb (if sumOdds == 0.0 then 0.0 else f / sumOdds) ||| Express odds as ratio (e.g., "3 to 2") public export @@ -150,10 +150,10 @@ bernoulli _ _ = 0.0 ||| Binomial coefficient (n choose k) binomial : Nat -> Nat -> Nat -binomial n k = - if k > n then 0 - else if k == 0 || k == n then 1 - else binomial (minus n 1) (minus k 1) + binomial (minus n 1) k +binomial Z Z = 1 +binomial Z (S _) = 0 +binomial (S _) Z = 1 +binomial (S n) (S k) = binomial n k + binomial n (S k) ||| Binomial distribution: P(X = k) for n trials with probability p public export diff --git a/src/Proven/SafePromptInjection/Proofs.idr b/src/Proven/SafePromptInjection/Proofs.idr index 5b5fd4c5..fe128877 100644 --- a/src/Proven/SafePromptInjection/Proofs.idr +++ b/src/Proven/SafePromptInjection/Proofs.idr @@ -35,6 +35,7 @@ import Data.List import Data.String %default total +%unbound_implicits off -------------------------------------------------------------------------------- -- Per-character escape soundness (one Refl each — no quantifier gap) diff --git a/src/Proven/SafeRational.idr b/src/Proven/SafeRational.idr index 69601ff2..a91a8fe2 100644 --- a/src/Proven/SafeRational.idr +++ b/src/Proven/SafeRational.idr @@ -41,10 +41,24 @@ Show RationalError where -- Helper Functions -------------------------------------------------------------------------------- -||| Greatest common divisor +||| Greatest common divisor. The subtraction algorithm carries an explicit +||| `a + b + 1` budget, so totality does not depend on the covering Integer +||| remainder operation. gcd : Integer -> Integer -> Integer -gcd a 0 = abs a -gcd a b = gcd b (a `mod` b) +gcd a b = + let left : Nat = cast (abs a) + right : Nat = cast (abs b) + in cast (gcdNatFuel (S (left + right)) left right) + where + gcdNatFuel : (fuel : Nat) -> Nat -> Nat -> Nat + gcdNatFuel Z left right = if left == 0 then right else left + gcdNatFuel (S fuel) Z right = right + gcdNatFuel (S fuel) left Z = left + gcdNatFuel (S fuel) left right = + if left == right then left + else if left > right + then gcdNatFuel fuel (minus left right) right + else gcdNatFuel fuel left (minus right left) ||| Normalize a rational to lowest terms with positive denominator normalize : Integer -> Integer -> Rational @@ -226,20 +240,32 @@ public export fromDouble : (maxDenom : Integer) -> Double -> Rational fromDouble maxDenom x = if x == 0 then zero - else if x < 0 then negate (fromDouble maxDenom (-x)) - else findBest 0 1 1 0 + else + let target = if x < 0 then -x else x + budget : Nat = S (cast (abs maxDenom)) + result = findBest budget target 0 1 1 0 + in if x < 0 then negate result else result where - findBest : Integer -> Integer -> Integer -> Integer -> Rational - findBest a b c d = - let mediant_n = a + c - mediant_d = b + d - in if mediant_d > maxDenom - then if abs (toDouble (MkRational a b) - x) < abs (toDouble (MkRational c d) - x) - then MkRational a b - else MkRational c d - else if toDouble (MkRational mediant_n mediant_d) < x - then findBest mediant_n mediant_d c d - else findBest a b mediant_n mediant_d + closer : Double -> Integer -> Integer -> Integer -> Integer -> Rational + closer target a b c d = + if b == 0 then MkRational c d + else if d == 0 then MkRational a b + else if abs (toDouble (MkRational a b) - target) < + abs (toDouble (MkRational c d) - target) + then MkRational a b + else MkRational c d + + findBest : (fuel : Nat) -> Double -> + Integer -> Integer -> Integer -> Integer -> Rational + findBest Z target a b c d = closer target a b c d + findBest (S fuel) target a b c d = + let mediantN = a + c + mediantD = b + d + in if mediantD > maxDenom + then closer target a b c d + else if toDouble (MkRational mediantN mediantD) < target + then findBest fuel target mediantN mediantD c d + else findBest fuel target a b mediantN mediantD ||| Floor division (towards negative infinity) public export diff --git a/src/Proven/SafeRegex.idr b/src/Proven/SafeRegex.idr index 82081a36..6d304220 100644 --- a/src/Proven/SafeRegex.idr +++ b/src/Proven/SafeRegex.idr @@ -182,52 +182,52 @@ hasRedosRisk pattern = ||| Pre-built safe email pattern public export safeEmailPattern : Either RegexError SafeRegex -safeEmailPattern = parseSafe emailPattern +safeEmailPattern = Right emailPattern ||| Pre-built safe URL pattern public export safeUrlPattern : Either RegexError SafeRegex -safeUrlPattern = parseSafe urlPattern +safeUrlPattern = Right urlPattern ||| Pre-built safe IPv4 pattern public export safeIpv4Pattern : Either RegexError SafeRegex -safeIpv4Pattern = parseSafe ipv4Pattern +safeIpv4Pattern = Right ipv4Pattern ||| Pre-built safe UUID pattern public export safeUuidPattern : Either RegexError SafeRegex -safeUuidPattern = parseSafe uuidPattern +safeUuidPattern = Right uuidPattern ||| Pre-built safe integer pattern public export safeIntegerPattern : Either RegexError SafeRegex -safeIntegerPattern = parseSafe integerPattern +safeIntegerPattern = parseSafe integerPatternSource ||| Pre-built safe decimal pattern public export safeDecimalPattern : Either RegexError SafeRegex -safeDecimalPattern = parseSafe decimalPattern +safeDecimalPattern = parseSafe decimalPatternSource ||| Pre-built safe identifier pattern (programming language identifiers) public export safeIdentifierPattern : Either RegexError SafeRegex -safeIdentifierPattern = parseSafe identifierPattern +safeIdentifierPattern = parseSafe identifierPatternSource ||| Pre-built safe hex color pattern public export safeHexColorPattern : Either RegexError SafeRegex -safeHexColorPattern = parseSafe hexColorPattern +safeHexColorPattern = parseSafe hexColorPatternSource ||| Pre-built safe date pattern (YYYY-MM-DD) public export safeDatePattern : Either RegexError SafeRegex -safeDatePattern = parseSafe datePattern +safeDatePattern = parseSafe datePatternSource ||| Pre-built safe time pattern (HH:MM:SS) public export safeTimePattern : Either RegexError SafeRegex -safeTimePattern = parseSafe timePattern +safeTimePattern = parseSafe timePatternSource -------------------------------------------------------------------------------- -- Monad-like Operations for Pattern Composition diff --git a/src/Proven/SafeRegex/Matcher.idr b/src/Proven/SafeRegex/Matcher.idr index 988f3f35..d6e67cdf 100644 --- a/src/Proven/SafeRegex/Matcher.idr +++ b/src/Proven/SafeRegex/Matcher.idr @@ -116,6 +116,11 @@ getCapture st groupId = -- Character Matching -------------------------------------------------------------------------------- +||| Match a character class with the supplied regex flags. +||| The signature precedes `matchCharClass` deliberately: Idris2 resolves +||| top-level names in declaration order. +matchesClassWithFlags : Char -> CharClass -> RegexFlags -> Bool + ||| Match a character class at current position public export matchCharClass : MatchState -> CharClass -> Bool @@ -126,11 +131,10 @@ matchCharClass st cls = let c' = if st.flags.caseInsensitive then toLower c else c in matchesClassWithFlags c' cls st.flags -||| Match character class with flags -matchesClassWithFlags : Char -> CharClass -> RegexFlags -> Bool +-- Definition for the forward declaration above. matchesClassWithFlags c cls flags = case cls of - Char x => + SingleChar x => let x' = if flags.caseInsensitive then toLower x else x in c == x' Range from to => @@ -194,188 +198,140 @@ data MatchAttempt : Type where ||| Step limit exceeded - abort StepLimitExceeded : Nat -> MatchAttempt -||| Match a regex against input starting at current position -||| Uses fuel for totality -public export -matchRegex : (fuel : Nat) -> Regex -> MatchState -> MatchAttempt -matchRegex Z _ st = StepLimitExceeded st.steps -matchRegex (S fuel) r st = - case step st of - Nothing => StepLimitExceeded st.steps - Just st' => matchRegex' fuel r st' - where - matchRegex' : Nat -> Regex -> MatchState -> MatchAttempt - - -- Empty matches empty string - matchRegex' _ Empty st = Success st - - -- Never fails - matchRegex' _ Never st = Failure st - - -- Match character class - matchRegex' _ (Match cls) st = - if matchCharClass st cls - then Success (advance st 1) - else Failure st - - -- Sequence: match r1 then r2 - matchRegex' fuel (Seq r1 r2) st = - case matchRegex fuel r1 st of - Success st' => matchRegex fuel r2 st' - Failure st' => Failure st' - StepLimitExceeded n => StepLimitExceeded n - - -- Alternative: try r1, if fails try r2 - matchRegex' fuel (Alt r1 r2) st = - case matchRegex fuel r1 st of - Success st' => Success st' - Failure _ => matchRegex fuel r2 st - StepLimitExceeded n => StepLimitExceeded n - - -- Quantifier: match r multiple times - matchRegex' fuel (Quant r q) st = - matchQuantified fuel r q 0 st - - -- Capturing group - matchRegex' fuel (Group gid r) st = - let startPos = st.position - in case matchRegex fuel r st of - Success st' => Success (saveCapture st' gid startPos st'.position) - other => other - - -- Non-capturing group - matchRegex' fuel (NCGroup r) st = matchRegex fuel r st - - -- Start anchor - matchRegex' _ StartAnchor st = - if st.flags.multiline - then if atLineStart st then Success st else Failure st - else if atStart st then Success st else Failure st - - -- End anchor - matchRegex' _ EndAnchor st = - if st.flags.multiline - then if atLineEnd st then Success st else Failure st - else if atEnd st then Success st else Failure st - - -- Word boundary - matchRegex' _ WordBoundary st = - if atWordBoundary st then Success st else Failure st - - -- Backreference - matchRegex' fuel (BackRef gid) st = - case getCapture st gid of - Nothing => Failure st -- Group not captured yet - Just (_, _, text) => - let textLen = length text - in if st.position + textLen <= st.inputLen && - substring st st.position (st.position + textLen) == text - then Success (advance st textLen) - else Failure st - - -- Positive lookahead (?=...) - matchRegex' fuel (Lookahead True r) st = - case matchRegex fuel r st of - Success _ => Success st -- Match but don't consume - Failure st' => Failure st' - StepLimitExceeded n => StepLimitExceeded n - - -- Negative lookahead (?!...) - matchRegex' fuel (Lookahead False r) st = - case matchRegex fuel r st of - Success _ => Failure st -- Lookahead should NOT match - Failure _ => Success st - StepLimitExceeded n => StepLimitExceeded n - - -- Positive lookbehind (?<=...) - matchRegex' fuel (Lookbehind True r) st = - -- Simplified: try matching from various positions behind - matchLookbehind fuel r st True - - -- Negative lookbehind (? Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt - matchQuantified Z _ _ _ st = StepLimitExceeded st.steps - matchQuantified (S fuel) r q count st = - case step st of - Nothing => StepLimitExceeded st.steps - Just st' => - -- Check if we've reached max count - let atMax = case q.maxCount of - Nothing => False - Just m => count >= m - in if atMax - then Success st' - else if q.greedy - then matchQuantifiedGreedy fuel r q count st' - else matchQuantifiedLazy fuel r q count st' - - -- Greedy quantifier matching - matchQuantifiedGreedy : Nat -> Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt - matchQuantifiedGreedy Z _ _ _ st = StepLimitExceeded st.steps - matchQuantifiedGreedy (S fuel) r q count st = - -- Try to match one more - case matchRegex fuel r st of - Success st' => - -- Successfully matched, try for more (greedy) - case matchQuantified fuel r q (S count) st' of - Success st'' => Success st'' - Failure _ => - -- Backtrack: if we have enough, succeed here - if count >= q.minCount - then Success st' - else Failure st - StepLimitExceeded n => StepLimitExceeded n - Failure _ => - -- Can't match more, check if we have enough - if count >= q.minCount - then Success st - else Failure st - StepLimitExceeded n => StepLimitExceeded n - - -- Lazy quantifier matching - matchQuantifiedLazy : Nat -> Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt - matchQuantifiedLazy Z _ _ _ st = StepLimitExceeded st.steps - matchQuantifiedLazy (S fuel) r q count st = - -- First check if we have minimum - if count >= q.minCount - then Success st -- Lazy: stop as soon as minimum is satisfied - else case matchRegex fuel r st of - Success st' => matchQuantified fuel r q (S count) st' - other => other - - -- Lookbehind matching (simplified) - matchLookbehind : Nat -> Regex -> MatchState -> Bool -> MatchAttempt - matchLookbehind Z _ st _ = StepLimitExceeded st.steps - matchLookbehind (S fuel) r st positive = - -- Try matching from positions behind current - let tryFrom = tryLookbehindFrom fuel r st st.position positive - in tryFrom - - tryLookbehindFrom : Nat -> Regex -> MatchState -> Nat -> Bool -> MatchAttempt - tryLookbehindFrom Z _ st _ _ = StepLimitExceeded st.steps - tryLookbehindFrom (S fuel) r st 0 positive = - -- Try from position 0 - let testSt = { position := 0 } st - in case matchRegex fuel r testSt of - Success st' => - if st'.position == st.position - then if positive then Success st else Failure st - else if positive then Failure st else Success st - Failure _ => if positive then Failure st else Success st - StepLimitExceeded n => StepLimitExceeded n - tryLookbehindFrom (S fuel) r st pos positive = - let testSt = { position := minus pos 1 } st - in case matchRegex fuel r testSt of - Success st' => - if st'.position == st.position - then if positive then Success st else Failure st - else tryLookbehindFrom fuel r st (minus pos 1) positive - Failure _ => tryLookbehindFrom fuel r st (minus pos 1) positive - StepLimitExceeded n => StepLimitExceeded n +-- Keeping the mutually recursive helpers at top level makes every fuel +-- decrease visible to Idris2's totality checker; a `where` block would attach +-- only to one equation. +mutual + ||| Match a regex against input starting at current position. + ||| Every recursive path consumes fuel. + public export + matchRegex : (fuel : Nat) -> Regex -> MatchState -> MatchAttempt + matchRegex Z _ st = StepLimitExceeded st.steps + matchRegex (S fuel) r st = + case step st of + Nothing => StepLimitExceeded st.steps + Just st' => matchRegexStep fuel r st' + + matchRegexStep : Nat -> Regex -> MatchState -> MatchAttempt + matchRegexStep _ Empty st = Success st + matchRegexStep _ Never st = Failure st + matchRegexStep _ (Match cls) st = + if matchCharClass st cls + then Success (advance st 1) + else Failure st + matchRegexStep fuel (Seq r1 r2) st = + case matchRegex fuel r1 st of + Success st' => matchRegex fuel r2 st' + Failure st' => Failure st' + StepLimitExceeded n => StepLimitExceeded n + matchRegexStep fuel (Alt r1 r2) st = + case matchRegex fuel r1 st of + Success st' => Success st' + Failure _ => matchRegex fuel r2 st + StepLimitExceeded n => StepLimitExceeded n + matchRegexStep fuel (Quant r q) st = + matchQuantified fuel r q 0 st + matchRegexStep fuel (Group gid r) st = + let startPos = st.position + in case matchRegex fuel r st of + Success st' => Success (saveCapture st' gid startPos st'.position) + other => other + matchRegexStep fuel (NCGroup r) st = matchRegex fuel r st + matchRegexStep _ StartAnchor st = + if st.flags.multiline + then if atLineStart st then Success st else Failure st + else if atStart st then Success st else Failure st + matchRegexStep _ EndAnchor st = + if st.flags.multiline + then if atLineEnd st then Success st else Failure st + else if atEnd st then Success st else Failure st + matchRegexStep _ WordBoundary st = + if atWordBoundary st then Success st else Failure st + matchRegexStep _ (BackRef gid) st = + case getCapture st gid of + Nothing => Failure st + Just (_, _, text) => + let textLen = length text + in if st.position + textLen <= st.inputLen && + substring st st.position (st.position + textLen) == text + then Success (advance st textLen) + else Failure st + matchRegexStep fuel (Lookahead True r) st = + case matchRegex fuel r st of + Success _ => Success st + Failure st' => Failure st' + StepLimitExceeded n => StepLimitExceeded n + matchRegexStep fuel (Lookahead False r) st = + case matchRegex fuel r st of + Success _ => Failure st + Failure _ => Success st + StepLimitExceeded n => StepLimitExceeded n + matchRegexStep fuel (Lookbehind positive r) st = + matchLookbehind fuel r st positive + + matchQuantified : Nat -> Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt + matchQuantified Z _ _ _ st = StepLimitExceeded st.steps + matchQuantified (S fuel) r q count st = + case step st of + Nothing => StepLimitExceeded st.steps + Just st' => + let atMax = case q.maxCount of + Nothing => False + Just m => count >= m + in if atMax + then Success st' + else if q.greedy + then matchQuantifiedGreedy fuel r q count st' + else matchQuantifiedLazy fuel r q count st' + + matchQuantifiedGreedy : Nat -> Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt + matchQuantifiedGreedy Z _ _ _ st = StepLimitExceeded st.steps + matchQuantifiedGreedy (S fuel) r q count st = + case matchRegex fuel r st of + Success st' => + case matchQuantified fuel r q (S count) st' of + Success st'' => Success st'' + Failure _ => + if count >= q.minCount then Success st' else Failure st + StepLimitExceeded n => StepLimitExceeded n + Failure _ => + if count >= q.minCount then Success st else Failure st + StepLimitExceeded n => StepLimitExceeded n + + matchQuantifiedLazy : Nat -> Regex -> Quantifier -> Nat -> MatchState -> MatchAttempt + matchQuantifiedLazy Z _ _ _ st = StepLimitExceeded st.steps + matchQuantifiedLazy (S fuel) r q count st = + if count >= q.minCount + then Success st + else case matchRegex fuel r st of + Success st' => matchQuantified fuel r q (S count) st' + other => other + + matchLookbehind : Nat -> Regex -> MatchState -> Bool -> MatchAttempt + matchLookbehind Z _ st _ = StepLimitExceeded st.steps + matchLookbehind (S fuel) r st positive = + tryLookbehindFrom fuel r st st.position positive + + tryLookbehindFrom : Nat -> Regex -> MatchState -> Nat -> Bool -> MatchAttempt + tryLookbehindFrom Z _ st _ _ = StepLimitExceeded st.steps + tryLookbehindFrom (S fuel) r st 0 positive = + let testSt = { position := 0 } st + in case matchRegex fuel r testSt of + Success st' => + if st'.position == st.position + then if positive then Success st else Failure st + else if positive then Failure st else Success st + Failure _ => if positive then Failure st else Success st + StepLimitExceeded n => StepLimitExceeded n + tryLookbehindFrom (S fuel) r st pos positive = + let testSt = { position := minus pos 1 } st + in case matchRegex fuel r testSt of + Success st' => + if st'.position == st.position + then if positive then Success st else Failure st + else tryLookbehindFrom fuel r st (minus pos 1) positive + Failure _ => tryLookbehindFrom fuel r st (minus pos 1) positive + StepLimitExceeded n => StepLimitExceeded n -------------------------------------------------------------------------------- -- High-Level Matching API @@ -404,42 +360,44 @@ matchAt sr input pos flags = ||| Find first match in input string public export findFirst : SafeRegex -> String -> RegexFlags -> MatchResult -findFirst sr input flags = findFrom 0 +findFirst sr input flags = findFrom (S inputLen) 0 where inputLen : Nat inputLen = length input - findFrom : Nat -> MatchResult - findFrom pos = + findFrom : (fuel : Nat) -> Nat -> MatchResult + findFrom Z _ = noMatch 0 + findFrom (S fuel) pos = if pos > inputLen then noMatch 0 else case matchAt sr input pos flags of result@(MkMatchResult True _ _ _) => result MkMatchResult False _ _ steps => if pos < inputLen - then findFrom (S pos) + then findFrom fuel (S pos) else noMatch steps ||| Find all matches in input string public export findAll : SafeRegex -> String -> RegexFlags -> List MatchResult -findAll sr input flags = findFrom 0 +findAll sr input flags = findFrom (S inputLen) 0 where inputLen : Nat inputLen = length input - findFrom : Nat -> List MatchResult - findFrom pos = + findFrom : (fuel : Nat) -> Nat -> List MatchResult + findFrom Z _ = [] + findFrom (S fuel) pos = if pos > inputLen then [] else case matchAt sr input pos flags of result@(MkMatchResult True (Just (_, end)) _ _) => - result :: findFrom (max (S pos) end) + result :: findFrom fuel (max (S pos) end) MkMatchResult False _ _ _ => if pos < inputLen - then findFrom (S pos) + then findFrom fuel (S pos) else [] - _ => findFrom (S pos) + _ => findFrom fuel (S pos) ||| Test if regex matches anywhere in input public export @@ -468,42 +426,44 @@ replaceFirst sr input replacement = ||| Replace all matches public export replaceAll : SafeRegex -> String -> String -> String -replaceAll sr input replacement = go 0 "" +replaceAll sr input replacement = go (S inputLen) 0 "" where inputLen : Nat inputLen = length input - go : Nat -> String -> String - go pos acc = + go : (fuel : Nat) -> Nat -> String -> String + go Z pos acc = acc ++ substr pos (minus inputLen pos) input + go (S fuel) pos acc = if pos >= inputLen then acc ++ substr pos (minus inputLen pos) input else case matchAt sr input pos defaultFlags of MkMatchResult True (Just (start, end)) _ _ => let before = substr pos (minus start pos) input newPos = max (S pos) end - in go newPos (acc ++ before ++ replacement) + in go fuel newPos (acc ++ before ++ replacement) _ => if pos < inputLen - then go (S pos) (acc ++ singleton (assert_total $ strIndex input (cast pos))) + then go fuel (S pos) (acc ++ singleton (assert_total $ strIndex input (cast pos))) else acc ||| Split string by regex public export split : SafeRegex -> String -> List String -split sr input = go 0 [] +split sr input = go (S inputLen) 0 [] where inputLen : Nat inputLen = length input - go : Nat -> List String -> List String - go pos acc = + go : (fuel : Nat) -> Nat -> List String -> List String + go Z pos acc = reverse (substr pos (minus inputLen pos) input :: acc) + go (S fuel) pos acc = if pos >= inputLen then reverse (substr pos (minus inputLen pos) input :: acc) else case matchAt sr input pos defaultFlags of MkMatchResult True (Just (start, end)) _ _ => let part = substr pos (minus start pos) input newPos = max (S pos) end - in go newPos (part :: acc) + in go fuel newPos (part :: acc) _ => reverse (substr pos (minus inputLen pos) input :: acc) diff --git a/src/Proven/SafeRegex/Parser.idr b/src/Proven/SafeRegex/Parser.idr index 60c363fb..024f5fce 100644 --- a/src/Proven/SafeRegex/Parser.idr +++ b/src/Proven/SafeRegex/Parser.idr @@ -454,27 +454,70 @@ parseSafeStrict pattern = do r <- parseRegex pattern safeStrict r +||| Canonical source strings for the common pre-built patterns. Keeping these +||| beside the compiled values prevents the FFI and convenience APIs from +||| drifting onto different expressions. +public export +emailPatternSource : String +emailPatternSource = "^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}$" + +public export +urlPatternSource : String +urlPatternSource = "^https?://[a-zA-Z0-9.-]+(/[a-zA-Z0-9._~:/?#@!$&'()*+,;=-]*)?$" + +public export +ipv4PatternSource : String +ipv4PatternSource = "^([0-9]{1,3}\\.){3}[0-9]{1,3}$" + +public export +uuidPatternSource : String +uuidPatternSource = "^[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}$" + +public export +integerPatternSource : String +integerPatternSource = "^-?[0-9]+$" + +public export +decimalPatternSource : String +decimalPatternSource = "^-?[0-9]+(\\.[0-9]+)?$" + +public export +identifierPatternSource : String +identifierPatternSource = "^[a-zA-Z_][a-zA-Z0-9_]*$" + +public export +hexColorPatternSource : String +hexColorPatternSource = "^#[0-9a-fA-F]{6}$" + +public export +datePatternSource : String +datePatternSource = "^[0-9]{4}-[0-9]{2}-[0-9]{2}$" + +public export +timePatternSource : String +timePatternSource = "^[0-9]{2}:[0-9]{2}:[0-9]{2}$" + ||| Common pre-built safe patterns public export emailPattern : SafeRegex -emailPattern = case parseSafe "^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}$" of +emailPattern = case parseSafe emailPatternSource of Right sr => sr Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 public export urlPattern : SafeRegex -urlPattern = case parseSafe "^https?://[a-zA-Z0-9.-]+(/[a-zA-Z0-9._~:/?#@!$&'()*+,;=-]*)?$" of +urlPattern = case parseSafe urlPatternSource of Right sr => sr Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 public export ipv4Pattern : SafeRegex -ipv4Pattern = case parseSafe "^([0-9]{1,3}\\.){3}[0-9]{1,3}$" of +ipv4Pattern = case parseSafe ipv4PatternSource of Right sr => sr Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 public export uuidPattern : SafeRegex -uuidPattern = case parseSafe "^[0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{4}-[0-9a-fA-F]{12}$" of +uuidPattern = case parseSafe uuidPatternSource of Right sr => sr Left _ => MkSafeRegex Empty (MkComplexityAnalysis Linear 0 0 0 False False []) 1000 diff --git a/src/Proven/SafeSQL.idr b/src/Proven/SafeSQL.idr index f8703306..78e8b63d 100644 --- a/src/Proven/SafeSQL.idr +++ b/src/Proven/SafeSQL.idr @@ -163,18 +163,28 @@ getNamedParams q = q.namedParams ||| Validate a query before execution public export validate : ParameterizedQuery -> Result SQLError ParameterizedQuery -validate q = do - _ <- validateParams q - _ <- validateQuerySafety q - Ok q +validate q = + if length (unpack (toSQL q)) > maxQueryLength + then Err (InvalidQuery "Query exceeds maximum length") + else if length q.params > maxParamCount + then Err (InvalidQuery "Query exceeds maximum parameter count") + else do + _ <- validateParams q + _ <- validateQuerySafety q + Ok q ||| Validate strictly (rejects SQLRaw) public export validateStrict : ParameterizedQuery -> Result SQLError ParameterizedQuery -validateStrict q = do - _ <- validateParams q - _ <- validateQueryStrict q - Ok q +validateStrict q = + if length (unpack (toSQL q)) > maxQueryLength + then Err (InvalidQuery "Query exceeds maximum length") + else if length q.params > maxParamCount + then Err (InvalidQuery "Query exceeds maximum parameter count") + else do + _ <- validateParams q + _ <- validateQueryStrict q + Ok q -------------------------------------------------------------------------------- -- Convenience Value Constructors diff --git a/src/Proven/SafeSQL/Types.idr b/src/Proven/SafeSQL/Types.idr index 78267040..40d7d686 100644 --- a/src/Proven/SafeSQL/Types.idr +++ b/src/Proven/SafeSQL/Types.idr @@ -99,6 +99,22 @@ Eq SQLValue where -- Safe Identifier -------------------------------------------------------------------------------- +||| Maximum supported identifier length. This is enforced by +||| `isValidIdentifier` and exposed through the FFI. +public export +maxIdentifierLength : Nat +maxIdentifierLength = 128 + +||| Maximum rendered query length accepted by `validate`. +public export +maxQueryLength : Nat +maxQueryLength = 1048576 + +||| Maximum positional parameter count accepted by `validate`. +public export +maxParamCount : Nat +maxParamCount = 65535 + ||| A validated SQL identifier (table name, column name, etc.) ||| Only allows alphanumeric characters and underscores public export @@ -134,7 +150,7 @@ isValidIdentifier s = StrCons c rest => (isAlpha c || c == '_') && all isIdentifierChar (unpack rest) && - length s <= 128 -- Reasonable max length + length s <= maxIdentifierLength ||| SQL reserved words that cannot be used as identifiers without quoting public export diff --git a/src/Proven/SafeSSRF/Proofs.idr b/src/Proven/SafeSSRF/Proofs.idr index 6ddd2e66..f6ab766c 100644 --- a/src/Proven/SafeSSRF/Proofs.idr +++ b/src/Proven/SafeSSRF/Proofs.idr @@ -11,6 +11,7 @@ import Data.Nat import Data.List %default total +%unbound_implicits off -------------------------------------------------------------------------------- -- Address Classification Properties diff --git a/src/Proven/SafeTOML/Types.idr b/src/Proven/SafeTOML/Types.idr index 1c489711..6623d05e 100644 --- a/src/Proven/SafeTOML/Types.idr +++ b/src/Proven/SafeTOML/Types.idr @@ -134,62 +134,69 @@ data TOMLValue : Type where ||| Table (standard or array of tables) TTable : List (String, TOMLValue) -> TOMLValue -public export covering -Show TOMLValue where - show (TString s) = show s - show (TInt i) = show i - show (TFloat f) = show f - show (TBool True) = "true" - show (TBool False) = "false" - show (TDateTime dt) = show dt - show (TDate d) = show d - show (TTime t) = show t - show (TArray xs) = "[" ++ join ", " (map show xs) ++ "]" - where - join : String -> List String -> String - join _ [] = "" - join _ [x] = x - join sep (x :: xs) = x ++ sep ++ join sep xs - show (TInlineTable kvs) = "{" ++ join ", " (map showKV kvs) ++ "}" - where - join : String -> List String -> String - join _ [] = "" - join _ [x] = x - join sep (x :: xs) = x ++ sep ++ join sep xs - showKV : (String, TOMLValue) -> String - showKV (k, v) = k ++ " = " ++ show v - show (TTable kvs) = "[table: " ++ show (length kvs) ++ " keys]" - -||| Equality helper for lists of TOML values (structurally recursive) -covering -tomlListEq : List TOMLValue -> List TOMLValue -> Bool - -||| Equality helper for TOML key-value pairs (structurally recursive) -covering -tomlPairsEq : List (String, TOMLValue) -> List (String, TOMLValue) -> Bool - -public export covering -Eq TOMLValue where - TString a == TString b = a == b - TInt a == TInt b = a == b - TFloat a == TFloat b = a == b - TBool a == TBool b = a == b - TDateTime a == TDateTime b = a == b - TDate a == TDate b = a == b - TTime a == TTime b = a == b - TArray a == TArray b = tomlListEq a b - TInlineTable a == TInlineTable b = tomlPairsEq a b - TTable a == TTable b = tomlPairsEq a b - _ == _ = False +tomlJoinStrings : String -> List String -> String +tomlJoinStrings _ [] = "" +tomlJoinStrings _ [x] = x +tomlJoinStrings sep (x :: xs) = x ++ sep ++ tomlJoinStrings sep xs + +-- Expose recursion through array and inline-table spines explicitly. This is +-- total over the TOML tree and avoids an opaque `map show` recursion. +mutual + tomlToString : TOMLValue -> String + tomlToString (TString s) = show s + tomlToString (TInt i) = show i + tomlToString (TFloat f) = show f + tomlToString (TBool True) = "true" + tomlToString (TBool False) = "false" + tomlToString (TDateTime dt) = show dt + tomlToString (TDate d) = show d + tomlToString (TTime t) = show t + tomlToString (TArray xs) = "[" ++ tomlJoinStrings ", " (tomlValuesToStrings xs) ++ "]" + tomlToString (TInlineTable kvs) = + "{" ++ tomlJoinStrings ", " (tomlPairsToStrings kvs) ++ "}" + tomlToString (TTable kvs) = "[table: " ++ show (length kvs) ++ " keys]" + + tomlValuesToStrings : List TOMLValue -> List String + tomlValuesToStrings [] = [] + tomlValuesToStrings (x :: xs) = tomlToString x :: tomlValuesToStrings xs + + tomlPairsToStrings : List (String, TOMLValue) -> List String + tomlPairsToStrings [] = [] + tomlPairsToStrings ((key, value) :: rest) = + (key ++ " = " ++ tomlToString value) :: tomlPairsToStrings rest -tomlListEq [] [] = True -tomlListEq (x :: xs) (y :: ys) = x == y && tomlListEq xs ys -tomlListEq _ _ = False +public export +Show TOMLValue where + show = tomlToString + +mutual + tomlEq : TOMLValue -> TOMLValue -> Bool + tomlEq (TString a) (TString b) = a == b + tomlEq (TInt a) (TInt b) = a == b + tomlEq (TFloat a) (TFloat b) = a == b + tomlEq (TBool a) (TBool b) = a == b + tomlEq (TDateTime a) (TDateTime b) = a == b + tomlEq (TDate a) (TDate b) = a == b + tomlEq (TTime a) (TTime b) = a == b + tomlEq (TArray a) (TArray b) = tomlListEq a b + tomlEq (TInlineTable a) (TInlineTable b) = tomlPairsEq a b + tomlEq (TTable a) (TTable b) = tomlPairsEq a b + tomlEq _ _ = False + + tomlListEq : List TOMLValue -> List TOMLValue -> Bool + tomlListEq [] [] = True + tomlListEq (x :: xs) (y :: ys) = tomlEq x y && tomlListEq xs ys + tomlListEq _ _ = False + + tomlPairsEq : List (String, TOMLValue) -> List (String, TOMLValue) -> Bool + tomlPairsEq [] [] = True + tomlPairsEq ((k1, v1) :: ps1) ((k2, v2) :: ps2) = + k1 == k2 && tomlEq v1 v2 && tomlPairsEq ps1 ps2 + tomlPairsEq _ _ = False -tomlPairsEq [] [] = True -tomlPairsEq ((k1, v1) :: ps1) ((k2, v2) :: ps2) = - k1 == k2 && v1 == v2 && tomlPairsEq ps1 ps2 -tomlPairsEq _ _ = False +public export +Eq TOMLValue where + (==) = tomlEq -------------------------------------------------------------------------------- -- TOML Document diff --git a/src/Proven/SafeUUID.idr b/src/Proven/SafeUUID.idr index 94acbd57..efc838d1 100644 --- a/src/Proven/SafeUUID.idr +++ b/src/Proven/SafeUUID.idr @@ -88,24 +88,28 @@ parse s = extractVersion : String -> UUIDVersion extractVersion hex = - case strIndex hex 12 of - Just '1' => V1 - Just '2' => V2 - Just '3' => V3 - Just '4' => V4 - Just '5' => V5 - Just c => Unknown (cast (ord c - ord '0')) - Nothing => Unknown 0 + case drop 12 (unpack hex) of + '1' :: _ => V1 + '2' :: _ => V2 + '3' :: _ => V3 + '4' :: _ => V4 + '5' :: _ => V5 + c :: _ => Unknown (cast (ord c - ord '0')) + [] => Unknown 0 extractVariant : String -> UUIDVariant extractVariant hex = - case strIndex hex 16 >>= hexToNibble of - Just n => + case drop 16 (unpack hex) of + c :: _ => variantFromNibble (hexToNibble c) + [] => RFC4122 + where + variantFromNibble : Maybe Nat -> UUIDVariant + variantFromNibble (Just n) = if n < 8 then NCS else if n < 12 then RFC4122 else if n < 14 then Microsoft else Future - Nothing => RFC4122 + variantFromNibble Nothing = RFC4122 ||| Validate a UUID string public export diff --git a/src/Proven/SafeVersion.idr b/src/Proven/SafeVersion.idr index bf771712..5c78de34 100644 --- a/src/Proven/SafeVersion.idr +++ b/src/Proven/SafeVersion.idr @@ -9,6 +9,7 @@ module Proven.SafeVersion import public Proven.Core import Data.String import Data.List +import Data.List1 import Data.Maybe %default total @@ -52,7 +53,7 @@ comparePrerelease (a :: as) (b :: bs) = where parseNum : String -> Maybe Nat parseNum s = if all isDigit (unpack s) && s /= "" - then Just (cast (parseInteger s)) + then map cast (parseInteger s) else Nothing public export @@ -92,11 +93,17 @@ parse s = parseDotted : String -> List String parseDotted "" = [] - parseDotted str = split (== '.') str + parseDotted str = forget (split (== '.') str) + + parseN : String -> Maybe Nat + parseN str = + if all isDigit (unpack str) && str /= "" + then map cast (parseInteger str) + else Nothing parseCore : String -> Maybe (Nat, Nat, Nat) parseCore str = - case split (== '.') str of + case forget (split (== '.') str) of [maj, min, pat] => do major <- parseN maj minor <- parseN min @@ -104,12 +111,6 @@ parse s = Just (major, minor, patch) _ => Nothing - parseN : String -> Maybe Nat - parseN str = - if all isDigit (unpack str) && str /= "" - then Just (cast (parseInteger str)) - else Nothing - ||| Check if a string is a valid semantic version public export isValid : String -> Bool diff --git a/src/Proven/SafeYAML/Types.idr b/src/Proven/SafeYAML/Types.idr index 5a74ff77..47c25a19 100644 --- a/src/Proven/SafeYAML/Types.idr +++ b/src/Proven/SafeYAML/Types.idr @@ -48,60 +48,67 @@ data YAMLValue : Type where ||| Timestamp value YTimestamp : String -> YAMLValue -public export covering -Show YAMLValue where - show YNull = "null" - show (YBool True) = "true" - show (YBool False) = "false" - show (YInt i) = show i - show (YFloat f) = show f - show (YString s) = show s - show (YArray xs) = "[" ++ join ", " (map show xs) ++ "]" - where - join : String -> List String -> String - join _ [] = "" - join _ [x] = x - join sep (x :: xs) = x ++ sep ++ join sep xs - show (YObject kvs) = "{" ++ join ", " (map showKV kvs) ++ "}" - where - join : String -> List String -> String - join _ [] = "" - join _ [x] = x - join sep (x :: xs) = x ++ sep ++ join sep xs - showKV : (String, YAMLValue) -> String - showKV (k, v) = k ++ ": " ++ show v - show (YBinary bs) = "!!binary " ++ show (length bs) ++ " bytes" - show (YTimestamp ts) = "!!timestamp " ++ ts - -||| Equality helper for lists of YAML values (structurally recursive) -covering -yamlListEq : List YAMLValue -> List YAMLValue -> Bool - -||| Equality helper for YAML object pairs (structurally recursive) -covering -yamlPairsEq : List (String, YAMLValue) -> List (String, YAMLValue) -> Bool - -public export covering -Eq YAMLValue where - YNull == YNull = True - YBool a == YBool b = a == b - YInt a == YInt b = a == b - YFloat a == YFloat b = a == b - YString a == YString b = a == b - YArray a == YArray b = yamlListEq a b - YObject a == YObject b = yamlPairsEq a b - YBinary a == YBinary b = a == b - YTimestamp a == YTimestamp b = a == b - _ == _ = False +joinStrings : String -> List String -> String +joinStrings _ [] = "" +joinStrings _ [x] = x +joinStrings sep (x :: xs) = x ++ sep ++ joinStrings sep xs + +-- These helpers are mutually recursive over the YAML tree and the lists held +-- by its collection constructors. Making that structure explicit avoids the +-- opaque `map show` call that previously forced the Show instance to covering. +mutual + yamlToString : YAMLValue -> String + yamlToString YNull = "null" + yamlToString (YBool True) = "true" + yamlToString (YBool False) = "false" + yamlToString (YInt i) = show i + yamlToString (YFloat f) = show f + yamlToString (YString s) = show s + yamlToString (YArray xs) = "[" ++ joinStrings ", " (yamlValuesToStrings xs) ++ "]" + yamlToString (YObject kvs) = "{" ++ joinStrings ", " (yamlPairsToStrings kvs) ++ "}" + yamlToString (YBinary bs) = "!!binary " ++ show (length bs) ++ " bytes" + yamlToString (YTimestamp ts) = "!!timestamp " ++ ts + + yamlValuesToStrings : List YAMLValue -> List String + yamlValuesToStrings [] = [] + yamlValuesToStrings (x :: xs) = yamlToString x :: yamlValuesToStrings xs + + yamlPairsToStrings : List (String, YAMLValue) -> List String + yamlPairsToStrings [] = [] + yamlPairsToStrings ((key, value) :: rest) = + (key ++ ": " ++ yamlToString value) :: yamlPairsToStrings rest -yamlListEq [] [] = True -yamlListEq (x :: xs) (y :: ys) = x == y && yamlListEq xs ys -yamlListEq _ _ = False +public export +Show YAMLValue where + show = yamlToString + +mutual + yamlEq : YAMLValue -> YAMLValue -> Bool + yamlEq YNull YNull = True + yamlEq (YBool a) (YBool b) = a == b + yamlEq (YInt a) (YInt b) = a == b + yamlEq (YFloat a) (YFloat b) = a == b + yamlEq (YString a) (YString b) = a == b + yamlEq (YArray a) (YArray b) = yamlListEq a b + yamlEq (YObject a) (YObject b) = yamlPairsEq a b + yamlEq (YBinary a) (YBinary b) = a == b + yamlEq (YTimestamp a) (YTimestamp b) = a == b + yamlEq _ _ = False + + yamlListEq : List YAMLValue -> List YAMLValue -> Bool + yamlListEq [] [] = True + yamlListEq (x :: xs) (y :: ys) = yamlEq x y && yamlListEq xs ys + yamlListEq _ _ = False + + yamlPairsEq : List (String, YAMLValue) -> List (String, YAMLValue) -> Bool + yamlPairsEq [] [] = True + yamlPairsEq ((k1, v1) :: ps1) ((k2, v2) :: ps2) = + k1 == k2 && yamlEq v1 v2 && yamlPairsEq ps1 ps2 + yamlPairsEq _ _ = False -yamlPairsEq [] [] = True -yamlPairsEq ((k1, v1) :: ps1) ((k2, v2) :: ps2) = - k1 == k2 && v1 == v2 && yamlPairsEq ps1 ps2 -yamlPairsEq _ _ = False +public export +Eq YAMLValue where + (==) = yamlEq -------------------------------------------------------------------------------- -- YAML Document @@ -115,7 +122,7 @@ record YAMLDocument where tags : List (String, String) -- Tag handles value : YAMLValue -public export covering +public export Show YAMLDocument where show doc = case doc.version of Just v => "%YAML " ++ v ++ "\n---\n" ++ show doc.value