fix: restore the Idris2 0.8 package build

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)))

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

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

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

src/Proven/FFI/SafeLRU.idr

@@ -88,33 +88,32 @@ 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
 --------------------------------------------------------------------------------
 
 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

src/Proven/FFI/SafeMCP.idr

@@ -81,16 +81,17 @@ 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
 --------------------------------------------------------------------------------
 
 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"

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)

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

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

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")

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