From 9f28ca9186276b5c04d812fde95e98fa7c85d706 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 11 May 2026 09:23:19 +0200 Subject: [PATCH] refactor(provenbridge): collapse placeholder to proven re-exports Closes the idaptik side of hyperpolymath/proven#8 (transferred from hyperpolymath/affinescript#58). Removes the 1658-line placeholder that mirrored five proven Safe* modules locally, replacing it with direct re-exports + idaptik-domain extractors built on proven. Net: 1443 lines deleted, 206 added (file 1658 -> 625 lines). Gated on: hyperpolymath/proven#9, which adds the small surface gaps this PR consumes (Proven.SafeJson.Access.field, Proven.SafeMath. divChecked, and the move of Proven.SafeInput into the Proven namespace and ipkg manifests). Marked draft until proven#9 merges. What changed in ProvenBridge.idr: - Replace local `JValue` type + 1600-char fuel-based JSON parser placeholder with `import public Proven.SafeJson.{,Parser,Access}`. All extractor signatures rename `JValue` -> `JsonValue`, `jGet` -> `get`, `jAsString` -> `asString`, etc. `parseJsonString` -> `parse`. - Replace local Int64 overflow stubs + `gameMath{Add,Sub,Mul,Div}` + `clampGameValue` + `percentOfTotal` with `import public Proven. SafeMath` and rewrite the idaptik-specific combinators (`clampHP`, `clampAlertLevel`, `applyDamage`, `critDamage`, `alertThresholdReached`) on top of `clamp`, `subChecked`, `mulChecked`, `percentOf` directly. - Replace local `game{CharAt,Substring,Trim,Truncate,...}` with `import public Proven.SafeString` and rewrite `validateLevelName`, `formatDeviceLabel`, `sanitiseTerminalInput` on top of `trim`, `isAscii`, `truncateWithEllipsis`, `padRight`, `truncate`. - Replace local `GameByte`/`GameBytes`/`gameConstantTimeEq` and hex/hash placeholders with `import public Proven.SafeCrypto` and rewrite `verifyAuthToken` on top of `hexToBytes` + `constantTimeEq`. Drop `gameSyncTag` (was a `gameHmac _ _ _ = []` stub providing zero integrity); callers should reach for `Proven.SafeCrypto.hmac` directly once that has a real FFI backing. - Replace local `Game{InputResult,CharClass,InputBuffer,Keystroke}` + all `gameValidate*` / `gameHandleKey` with `import public Proven.SafeInput` and rewrite `terminalHackBuffer`, `numericEntryBuffer`, `hexEntryBuffer`, `handleAndValidateInt`, `handleAndValidateNat` on top of `filteredBuffer`, `handleKey`, `validateInt`, `validateNat`. Naming change inside ProvenBridge: - The local `Extracted` type's `Ok` constructor is renamed to `Got`. Why: `import public Proven.SafeJson` transitively re-exports `Proven.Core.Result.Ok`, which would clash. A `%hide Proven.Core. Result.Ok` directive is also added so the rename is sufficient even if a future Idris2 disambiguator gets pickier. Out of scope (intentional): - LessonsMD L1's `Validation[E,A]` stdlib-floor proposal: the `Extracted` type here is the same shape (accumulating-error applicative-flavour) and would naturally retire to a future `Proven.Validation` if/when that lands. Local module additions to idaptik-ums.ipkg: - Uncomment `depends = proven`. Co-authored-by: Claude Opus 4.7 --- idaptik-ums/idaptik-ums.ipkg | 6 +- idaptik-ums/src/abi/ProvenBridge.idr | 1443 ++++---------------------- 2 files changed, 206 insertions(+), 1243 deletions(-) diff --git a/idaptik-ums/idaptik-ums.ipkg b/idaptik-ums/idaptik-ums.ipkg index 3f722b33..9c576e63 100644 --- a/idaptik-ums/idaptik-ums.ipkg +++ b/idaptik-ums/idaptik-ums.ipkg @@ -7,11 +7,7 @@ authors = "Jonathan D.A. Jewell" sourcedir = "src/abi" --- depends = proven --- ^ Uncomment when the proven package is available as a local dependency. --- ProvenBridge currently uses local placeholder types that mirror --- Proven.SafeJson.Parser.JsonValue. Once this dependency is added, --- the local types in ProvenBridge.idr should be replaced with imports. +depends = proven modules = Primitives, Types, diff --git a/idaptik-ums/src/abi/ProvenBridge.idr b/idaptik-ums/src/abi/ProvenBridge.idr index 7cc8f19e..0496e3ba 100644 --- a/idaptik-ums/src/abi/ProvenBridge.idr +++ b/idaptik-ums/src/abi/ProvenBridge.idr @@ -1,26 +1,25 @@ -- SPDX-License-Identifier: AGPL-3.0-or-later -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -- --- ProvenBridge.idr — Bridge between the proven repo and UMS game systems +-- ProvenBridge.idr — idaptik's use of the proven library. -- --- This module provides total, formally-grounded operations for IDApTIK by --- bridging five proven modules: SafeJson, SafeMath, SafeString, SafeCrypto, --- and SafeInput. All functions are total: they return structured errors --- instead of crashing. +-- Re-exports the five Safe* modules idaptik depends on, plus the +-- idaptik-domain extractors (LevelData / DeviceSpec / Zone / Guard / +-- ZoneTransition) and game-specific combinators built on them. -- --- Integration status: --- - Types are defined locally to allow compilation without the proven --- package dependency. When the proven ipkg is added as a dependency, --- replace the local types with imports (see TODO markers below). --- --- Bridged modules: --- - SafeJson: JSON parsing/validation for level data (lines ~40-640) --- - SafeMath: Safe arithmetic for damage/HP/alert calculations (lines ~735+) --- - SafeString: Safe text ops for player input and terminal display (lines ~900+) --- - SafeCrypto: Constant-time comparison for multiplayer auth (lines ~1050+) --- - SafeInput: Keystroke handling for terminal hacking sequences (lines ~1150+) +-- Before the proven dependency landed, this file was a 1658-line +-- placeholder mirroring each proven module locally so idaptik could +-- compile in isolation. Closes idaptik-side of hyperpolymath/proven#8. module ProvenBridge +import public Proven.SafeJson -- JsonValue + get/asString/asNumber/asInt/asBool/asArray/asObject +import public Proven.SafeJson.Parser -- parse, ParseError, JsonValue constructors +import public Proven.SafeJson.Access -- field, AccessError, getAt, etc. +import public Proven.SafeMath -- addChecked, subChecked, mulChecked, divChecked, clamp, percentOf +import public Proven.SafeString -- charAt, substring, trim, truncate, split, isAscii, parseNat, parseInt +import public Proven.SafeCrypto -- Byte, Bytes, constantTimeEq, hexToBytes, bytesToHex +import public Proven.SafeInput -- InputBuffer, Keystroke, CharClass, InputResult, handleKey, validate* + import Primitives import Types import Devices @@ -35,268 +34,14 @@ import Data.String %default total ------------------------------------------------------------------------- --- JSON Value representation (mirrors Proven.SafeJson.Parser.JsonValue) ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace this block with: --- import Proven.SafeJson --- import Proven.SafeJson.Parser --- import Proven.SafeJson.Access --- once the proven package is declared as a dependency in idaptik-ums.ipkg. - -||| JSON value type, locally mirrored from Proven.SafeJson.Parser. -||| When proven is available as a dependency, remove this and import directly. -public export -data JValue : Type where - JNull : JValue - JBool : Bool -> JValue - JNumber : Double -> JValue - JString : String -> JValue - JArray : List JValue -> JValue - JObject : List (String, JValue) -> JValue - ------------------------------------------------------------------------- --- Minimal total JSON parser (placeholder for Proven.SafeJson.parse) ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace parseJsonString with: --- Proven.SafeJson.Parser.parse : String -> Either ParseError JsonValue --- The proven parser handles Unicode escapes, nesting limits, and provides --- position-annotated errors. This placeholder only returns a generic error. - -||| Attempt to parse a JSON string into a JValue. -||| This is a placeholder that delegates to a minimal recursive-descent -||| parser. The real implementation will call Proven.SafeJson.parse. -||| -||| @input Raw JSON text -||| @return Left with human-readable error, or Right with parsed value -export -parseJsonString : String -> Either String JValue -parseJsonString input = - let chars = unpack (trim input) - in case chars of - [] => Left "Empty input" - _ => mapFst showErr (parseTop chars 0) - where - ||| Convert position-tagged error to human-readable string. - showErr : (Nat, String) -> String - showErr (pos, msg) = "Parse error at position " ++ show pos ++ ": " ++ msg - - ||| Map over the Left branch of an Either. - mapFst : (a -> c) -> Either a b -> Either c b - mapFst f (Left x) = Left (f x) - mapFst _ (Right x) = Right x - - mutual - ||| Top-level parse: skip leading whitespace, parse one value, - ||| reject trailing non-whitespace. - parseTop : List Char -> Nat -> Either (Nat, String) JValue - parseTop cs pos = - let (cs1, pos1) = skipWS cs pos - in case parseValue cs1 pos1 0 of - Left err => Left err - Right (val, cs2, pos2) => - let (cs3, _) = skipWS cs2 pos2 - in if null cs3 - then Right val - else Left (pos2, "Trailing content after value") - - ||| Skip whitespace characters, advancing position. - skipWS : List Char -> Nat -> (List Char, Nat) - skipWS [] p = ([], p) - skipWS (c :: cs) p = - if c == ' ' || c == '\n' || c == '\r' || c == '\t' - then skipWS cs (S p) - else (c :: cs, p) - - ||| Parse a single JSON value with depth tracking. - ||| Depth is bounded to prevent stack overflow on malicious input. - parseValue : List Char -> Nat -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseValue [] pos _ = Left (pos, "Unexpected end of input") - parseValue cs pos depth = - if depth > 100 - then Left (pos, "Nesting too deep (max 100)") - else let (cs', pos') = skipWS cs pos - in case cs' of - [] => Left (pos', "Unexpected end of input") - ('n' :: rest) => parseNull rest pos' - ('t' :: rest) => parseTrue rest pos' - ('f' :: rest) => parseFalse rest pos' - ('"' :: rest) => parseStr rest (S pos') [] - ('[' :: rest) => parseArr rest (S pos') (S depth) - ('{' :: rest) => parseObj rest (S pos') (S depth) - (c :: _) => - if c == '-' || (c >= '0' && c <= '9') - then parseNum cs' pos' - else Left (pos', "Unexpected character: " ++ singleton c) - - ||| Parse the literal "null" (the 'n' has already been consumed). - parseNull : List Char -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseNull ('u' :: 'l' :: 'l' :: rest) pos = Right (JNull, rest, pos + 4) - parseNull _ pos = Left (pos, "Expected 'null'") - - ||| Parse the literal "true" (the 't' has already been consumed). - parseTrue : List Char -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseTrue ('r' :: 'u' :: 'e' :: rest) pos = Right (JBool True, rest, pos + 4) - parseTrue _ pos = Left (pos, "Expected 'true'") - - ||| Parse the literal "false" (the 'f' has already been consumed). - parseFalse : List Char -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseFalse ('a' :: 'l' :: 's' :: 'e' :: rest) pos = Right (JBool False, rest, pos + 5) - parseFalse _ pos = Left (pos, "Expected 'false'") - - ||| Parse a JSON string (opening '"' already consumed). - parseStr : List Char -> Nat -> List Char -> Either (Nat, String) (JValue, List Char, Nat) - parseStr [] pos _ = Left (pos, "Unterminated string") - parseStr ('"' :: rest) pos acc = Right (JString (pack (reverse acc)), rest, S pos) - parseStr ('\\' :: c :: rest) pos acc = - case c of - '"' => parseStr rest (pos + 2) ('"' :: acc) - '\\' => parseStr rest (pos + 2) ('\\' :: acc) - '/' => parseStr rest (pos + 2) ('/' :: acc) - 'n' => parseStr rest (pos + 2) ('\n' :: acc) - 'r' => parseStr rest (pos + 2) ('\r' :: acc) - 't' => parseStr rest (pos + 2) ('\t' :: acc) - _ => Left (pos, "Unknown escape: \\" ++ singleton c) - parseStr ('\\' :: []) pos _ = Left (pos, "Unterminated escape") - parseStr (c :: rest) pos acc = parseStr rest (S pos) (c :: acc) - - ||| Parse a JSON number. Collects digit/sign/dot/e characters, then - ||| delegates to cast for conversion. - parseNum : List Char -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseNum cs pos = - let (numChars, rest, pos') = collectNum cs pos - numStr = pack numChars - in case parseDouble numStr of - Just d => Right (JNumber d, rest, pos') - Nothing => Left (pos, "Invalid number: " ++ numStr) - where - isNumChar : Char -> Bool - isNumChar c = (c >= '0' && c <= '9') || c == '.' || c == '-' - || c == '+' || c == 'e' || c == 'E' - - collectNum : List Char -> Nat -> (List Char, List Char, Nat) - collectNum [] p = ([], [], p) - collectNum (c :: cs') p = - if isNumChar c - then let (more, rest, p') = collectNum cs' (S p) - in (c :: more, rest, p') - else ([], c :: cs', p) - - parseDouble : String -> Maybe Double - parseDouble s = Just (cast {to=Double} s) - - ||| Parse a JSON array (opening '[' already consumed). - parseArr : List Char -> Nat -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseArr cs pos depth = - let (cs1, pos1) = skipWS cs pos - in case cs1 of - (']' :: rest) => Right (JArray [], rest, S pos1) - _ => parseArrElems cs1 pos1 depth [] - - ||| Parse comma-separated array elements. - parseArrElems : List Char -> Nat -> Nat -> List JValue - -> Either (Nat, String) (JValue, List Char, Nat) - parseArrElems cs pos depth acc = - case parseValue cs pos depth of - Left err => Left err - Right (val, cs1, pos1) => - let (cs2, pos2) = skipWS cs1 pos1 - in case cs2 of - (']' :: rest) => Right (JArray (reverse (val :: acc)), rest, S pos2) - (',' :: rest) => - let (cs3, pos3) = skipWS rest (S pos2) - in parseArrElems cs3 pos3 depth (val :: acc) - _ => Left (pos2, "Expected ',' or ']' in array") - - ||| Parse a JSON object (opening '{' already consumed). - parseObj : List Char -> Nat -> Nat -> Either (Nat, String) (JValue, List Char, Nat) - parseObj cs pos depth = - let (cs1, pos1) = skipWS cs pos - in case cs1 of - ('}' :: rest) => Right (JObject [], rest, S pos1) - _ => parseObjMembers cs1 pos1 depth [] - - ||| Parse comma-separated object members ("key": value). - parseObjMembers : List Char -> Nat -> Nat -> List (String, JValue) - -> Either (Nat, String) (JValue, List Char, Nat) - parseObjMembers cs pos depth acc = - case cs of - ('"' :: rest) => - case parseStr rest (S pos) [] of - Left err => Left err - Right (JString key, cs1, pos1) => - let (cs2, pos2) = skipWS cs1 pos1 - in case cs2 of - (':' :: rest2) => - let (cs3, pos3) = skipWS rest2 (S pos2) - in case parseValue cs3 pos3 depth of - Left err => Left err - Right (val, cs4, pos4) => - let (cs5, pos5) = skipWS cs4 pos4 - in case cs5 of - ('}' :: rest3) => - Right (JObject (reverse ((key, val) :: acc)), rest3, S pos5) - (',' :: rest3) => - let (cs6, pos6) = skipWS rest3 (S pos5) - in parseObjMembers cs6 pos6 depth ((key, val) :: acc) - _ => Left (pos5, "Expected ',' or '}' in object") - _ => Left (pos2, "Expected ':' after object key") - -- parseStr returned a non-string (impossible by construction) - Right _ => Left (pos, "Internal error: key parse did not yield string") - _ => Left (pos, "Expected '\"' for object key") +-- Hide Result.Ok / Result.Err brought in transitively via Proven.Core +-- so the local Extracted type's Got/Errs constructors disambiguate +-- without explicit qualification. +%hide Proven.Core.Result.Ok +%hide Proven.Core.Result.Err ------------------------------------------------------------------------ --- Safe JSON accessors (mirrors Proven.SafeJson / Proven.SafeJson.Access) ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace with imports from Proven.SafeJson.Access - -||| Look up a key in a JObject. Returns Nothing for non-objects or missing keys. -export -jGet : String -> JValue -> Maybe JValue -jGet key (JObject pairs) = lookup key pairs -jGet _ _ = Nothing - -||| Extract a String from a JValue. -export -jAsString : JValue -> Maybe String -jAsString (JString s) = Just s -jAsString _ = Nothing - -||| Extract a Double from a JValue. -export -jAsNumber : JValue -> Maybe Double -jAsNumber (JNumber n) = Just n -jAsNumber _ = Nothing - -||| Extract an Integer from a JValue (truncates fractional part). -export -jAsInt : JValue -> Maybe Integer -jAsInt (JNumber n) = Just (cast n) -jAsInt _ = Nothing - -||| Extract a Nat from a JValue (returns Nothing for negatives). -export -jAsNat : JValue -> Maybe Nat -jAsNat (JNumber n) = if n >= 0.0 then Just (cast (cast {to=Integer} n)) else Nothing -jAsNat _ = Nothing - -||| Extract a Bool from a JValue. -export -jAsBool : JValue -> Maybe Bool -jAsBool (JBool b) = Just b -jAsBool _ = Nothing - -||| Extract a List from a JArray. -export -jAsArray : JValue -> Maybe (List JValue) -jAsArray (JArray xs) = Just xs -jAsArray _ = Nothing - ------------------------------------------------------------------------- --- Level data extraction from JSON +-- Level data extraction from JSON (idaptik-domain, built on Proven.SafeJson) ------------------------------------------------------------------------ ||| Errors collected during level data extraction. @@ -306,25 +51,29 @@ ExtractionErrors : Type ExtractionErrors = List String ||| Result of extracting a value: either the value or accumulated errors. -||| We use List String rather than a single error so that extraction can +||| We use `List String` rather than a single error so extraction can ||| report ALL problems in one pass, not just the first. +||| +||| The constructor is named `Got` (not `Ok`) to avoid ambiguity with +||| `Proven.Core.Result.Ok`, which is in scope via the `Proven.SafeJson` +||| re-export above. public export data Extracted : Type -> Type where ||| Extraction succeeded with a value. - Ok : a -> Extracted a + Got : a -> Extracted a ||| Extraction failed with one or more error descriptions. Errs : (errors : ExtractionErrors) -> Extracted a ||| Functor-like map for Extracted. export mapExtracted : (a -> b) -> Extracted a -> Extracted b -mapExtracted f (Ok x) = Ok (f x) +mapExtracted f (Got x) = Got (f x) mapExtracted _ (Errs es) = Errs es ||| Combine two Extracted values, accumulating errors from both sides. export combineExtracted : Extracted a -> Extracted b -> Extracted (a, b) -combineExtracted (Ok x) (Ok y) = Ok (x, y) +combineExtracted (Got x) (Got y) = Got (x, y) combineExtracted (Errs e1) (Errs e2) = Errs (e1 ++ e2) combineExtracted (Errs e1) _ = Errs e1 combineExtracted _ (Errs e2) = Errs e2 @@ -332,56 +81,64 @@ combineExtracted _ (Errs e2) = Errs e2 ||| Convert an Extracted to Either, joining errors with newlines. export extractedToEither : Extracted a -> Either String a -extractedToEither (Ok x) = Right x +extractedToEither (Got x) = Right x extractedToEither (Errs es) = Left (joinBy "\n" es) +||| Extract a Nat from a JSON value (returns Nothing for negatives). +||| Proven.SafeJson exposes `asInt` but not `asNat`; this is the +||| idaptik-side helper that adds the non-negativity check. +export +asNat : JsonValue -> Maybe Nat +asNat (JsonNumber n) = if n >= 0.0 then Just (cast (cast {to=Integer} n)) else Nothing +asNat _ = Nothing + ||| Require a field to exist and satisfy a predicate. export -requireField : String -> String -> (JValue -> Maybe a) -> JValue -> Extracted a +requireField : String -> String -> (JsonValue -> Maybe a) -> JsonValue -> Extracted a requireField context fieldName extract json = - case jGet fieldName json of + case get fieldName json of Nothing => Errs [context ++ ": missing required field '" ++ fieldName ++ "'"] Just val => case extract val of Nothing => Errs [context ++ ": field '" ++ fieldName ++ "' has wrong type"] - Just x => Ok x + Just x => Got x ||| Require an optional field: if present it must parse, if absent returns Nothing. export -optionalField : String -> String -> (JValue -> Maybe a) -> JValue -> Extracted (Maybe a) +optionalField : String -> String -> (JsonValue -> Maybe a) -> JsonValue -> Extracted (Maybe a) optionalField context fieldName extract json = - case jGet fieldName json of - Nothing => Ok Nothing + case get fieldName json of + Nothing => Got Nothing Just val => case extract val of Nothing => Errs [context ++ ": field '" ++ fieldName ++ "' has wrong type"] - Just x => Ok (Just x) + Just x => Got (Just x) ------------------------------------------------------------------------ -- Octet / IpAddress extraction ------------------------------------------------------------------------ -||| Parse an octet (0-255) from a JValue number. +||| Parse an octet (0-255) from a JsonValue number. export -extractOctet : String -> JValue -> Extracted (Fin 256) +extractOctet : String -> JsonValue -> Extracted (Fin 256) extractOctet context json = - case jAsInt json of + case asInt json of Nothing => Errs [context ++ ": expected integer for octet"] Just n => if n >= 0 && n <= 255 then case natToFin (cast n) 256 of - Just f => Ok f + Just f => Got f Nothing => Errs [context ++ ": octet out of range (internal)"] else Errs [context ++ ": octet " ++ show n ++ " out of range 0-255"] ||| Parse an IP address from a JSON string in "a.b.c.d" format. export -extractIpAddress : String -> JValue -> Extracted IpAddress +extractIpAddress : String -> JsonValue -> Extracted IpAddress extractIpAddress context json = - case jAsString json of + case asString json of Nothing => Errs [context ++ ": expected string for IP address"] Just s => - case split (== '.') s of + case Data.String.split (== '.') s of -- split returns a List1 (SnocList), so we convert and check length parts => let partsList = forget parts @@ -389,7 +146,7 @@ extractIpAddress context json = [a, b, c, d] => case (parseOctetStr a, parseOctetStr b, parseOctetStr c, parseOctetStr d) of (Just o1, Just o2, Just o3, Just o4) => - Ok (MkIpAddress o1 o2 o3 o4) + Got (MkIpAddress o1 o2 o3 o4) _ => Errs [context ++ ": invalid IP address octets in '" ++ s ++ "'"] _ => Errs [context ++ ": IP address must have exactly 4 octets, got '" ++ s ++ "'"] where @@ -408,50 +165,50 @@ extractIpAddress context json = ||| Parse a SecurityLevel from a JSON string. export -extractSecurityLevel : String -> JValue -> Extracted SecurityLevel +extractSecurityLevel : String -> JsonValue -> Extracted SecurityLevel extractSecurityLevel ctx json = - case jAsString json of + case asString json of Nothing => Errs [ctx ++ ": expected string for security level"] - Just "open" => Ok Open - Just "weak" => Ok Weak - Just "medium" => Ok Medium - Just "strong" => Ok Strong + Just "open" => Got Open + Just "weak" => Got Weak + Just "medium" => Got Medium + Just "strong" => Got Strong Just other => Errs [ctx ++ ": unknown security level '" ++ other ++ "'"] ||| Parse a DeviceKind from a JSON string. export -extractDeviceKind : String -> JValue -> Extracted DeviceKind +extractDeviceKind : String -> JsonValue -> Extracted DeviceKind extractDeviceKind ctx json = - case jAsString json of + case asString json of Nothing => Errs [ctx ++ ": expected string for device kind"] - Just "laptop" => Ok Laptop - Just "desktop" => Ok Desktop - Just "server" => Ok Server - Just "router" => Ok Router - Just "switch" => Ok Switch - Just "firewall" => Ok Firewall - Just "camera" => Ok Camera - Just "access_point" => Ok AccessPoint - Just "patch_panel" => Ok PatchPanel - Just "power_supply" => Ok PowerSupply - Just "phone_system" => Ok PhoneSystem - Just "fibre_hub" => Ok FibreHub + Just "laptop" => Got Laptop + Just "desktop" => Got Desktop + Just "server" => Got Server + Just "router" => Got Router + Just "switch" => Got Switch + Just "firewall" => Got Firewall + Just "camera" => Got Camera + Just "access_point" => Got AccessPoint + Just "patch_panel" => Got PatchPanel + Just "power_supply" => Got PowerSupply + Just "phone_system" => Got PhoneSystem + Just "fibre_hub" => Got FibreHub Just other => Errs [ctx ++ ": unknown device kind '" ++ other ++ "'"] ||| Parse a GuardRank from a JSON string. export -extractGuardRank : String -> JValue -> Extracted GuardRank +extractGuardRank : String -> JsonValue -> Extracted GuardRank extractGuardRank ctx json = - case jAsString json of + case asString json of Nothing => Errs [ctx ++ ": expected string for guard rank"] - Just "basic" => Ok BasicGuard - Just "enforcer" => Ok Enforcer - Just "anti_hacker" => Ok AntiHacker - Just "sentinel" => Ok Sentinel - Just "assassin" => Ok Assassin - Just "elite" => Ok EliteGuard - Just "security_chief" => Ok SecurityChief - Just "rival_hacker" => Ok RivalHacker + Just "basic" => Got BasicGuard + Just "enforcer" => Got Enforcer + Just "anti_hacker" => Got AntiHacker + Just "sentinel" => Got Sentinel + Just "assassin" => Got Assassin + Just "elite" => Got EliteGuard + Just "security_chief" => Got SecurityChief + Just "rival_hacker" => Got RivalHacker Just other => Errs [ctx ++ ": unknown guard rank '" ++ other ++ "'"] ------------------------------------------------------------------------ @@ -460,25 +217,25 @@ extractGuardRank ctx json = ||| Extract a DeviceSpec from a JSON object. export -extractDevice : String -> JValue -> Extracted DeviceSpec +extractDevice : String -> JsonValue -> Extracted DeviceSpec extractDevice ctx json = - case ( extractDeviceKind (ctx ++ ".kind") =<< maybeToExtracted (ctx ++ ".kind") (jGet "kind" json) - , extractIpAddress (ctx ++ ".ip") =<< maybeToExtracted (ctx ++ ".ip") (jGet "ip" json) - , requireField ctx "name" jAsString json - , extractSecurityLevel (ctx ++ ".security") =<< maybeToExtracted (ctx ++ ".security") (jGet "security" json) + case ( extractDeviceKind (ctx ++ ".kind") =<< maybeToExtracted (ctx ++ ".kind") (get "kind" json) + , extractIpAddress (ctx ++ ".ip") =<< maybeToExtracted (ctx ++ ".ip") (get "ip" json) + , requireField ctx "name" asString json + , extractSecurityLevel (ctx ++ ".security") =<< maybeToExtracted (ctx ++ ".security") (get "security" json) ) of - (Ok k, Ok i, Ok n, Ok s) => Ok (MkDeviceSpec k i n s) - (e1, e2, e3, e4) => Errs (collectErrs [e1, e2, e3, e4]) + (Got k, Got i, Got n, Got s) => Got (MkDeviceSpec k i n s) + (e1, e2, e3, e4) => Errs (collectErrs [e1, e2, e3, e4]) where ||| Bind-like operation for Extracted. Applies f to the inner value, ||| or propagates errors. (=<<) : (a -> Extracted b) -> Extracted a -> Extracted b - (=<<) f (Ok x) = f x + (=<<) f (Got x) = f x (=<<) _ (Errs es) = Errs es ||| Lift a Maybe into Extracted, using the given context for error messages. maybeToExtracted : String -> Maybe a -> Extracted a - maybeToExtracted _ (Just x) = Ok x + maybeToExtracted _ (Just x) = Got x maybeToExtracted msg Nothing = Errs [msg ++ ": field missing"] ||| Collect error messages from a list of Extracted values. @@ -489,33 +246,33 @@ extractDevice ctx json = ||| Extract a Zone from a JSON object. export -extractZone : String -> JValue -> Extracted Zone +extractZone : String -> JsonValue -> Extracted Zone extractZone ctx json = - case (requireField ctx "name" jAsString json, - requireField ctx "security_tier" jAsNat json) of - (Ok n, Ok t) => Ok (MkZone n t) + case (requireField ctx "name" asString json, + requireField ctx "security_tier" asNat json) of + (Got n, Got t) => Got (MkZone n t) (Errs e1, Errs e2) => Errs (e1 ++ e2) - (Errs e1, _) => Errs e1 - (_, Errs e2) => Errs e2 + (Errs e1, _) => Errs e1 + (_, Errs e2) => Errs e2 ||| Extract a GuardPlacement from a JSON object. export -extractGuard : String -> JValue -> Extracted GuardPlacement +extractGuard : String -> JsonValue -> Extracted GuardPlacement extractGuard ctx json = - case ( requireField ctx "world_x" jAsNumber json - , requireField ctx "zone" jAsString json - , extractGuardRank ctx =<< maybeToExtracted (ctx ++ ".rank") (jGet "rank" json) - , requireField ctx "patrol_radius" jAsNumber json + case ( requireField ctx "world_x" asNumber json + , requireField ctx "zone" asString json + , extractGuardRank ctx =<< maybeToExtracted (ctx ++ ".rank") (get "rank" json) + , requireField ctx "patrol_radius" asNumber json ) of - (Ok wx, Ok z, Ok r, Ok pr) => Ok (MkGuardPlacement (MkWorldX wx) z r pr) - (e1, e2, e3, e4) => Errs (collectErrs [e1, e2, e3, e4]) + (Got wx, Got z, Got r, Got pr) => Got (MkGuardPlacement (MkWorldX wx) z r pr) + (e1, e2, e3, e4) => Errs (collectErrs [e1, e2, e3, e4]) where (=<<) : (a -> Extracted b) -> Extracted a -> Extracted b - (=<<) f (Ok x) = f x + (=<<) f (Got x) = f x (=<<) _ (Errs es) = Errs es maybeToExtracted : String -> Maybe a -> Extracted a - maybeToExtracted _ (Just x) = Ok x + maybeToExtracted _ (Just x) = Got x maybeToExtracted msg Nothing = Errs [msg ++ ": field missing"] collectErrs : List (Extracted a) -> ExtractionErrors @@ -525,14 +282,14 @@ extractGuard ctx json = ||| Extract a ZoneTransition from a JSON object. export -extractZoneTransition : String -> JValue -> Extracted ZoneTransition +extractZoneTransition : String -> JsonValue -> Extracted ZoneTransition extractZoneTransition ctx json = - case ( requireField ctx "world_x" jAsNumber json - , requireField ctx "from_zone" jAsString json - , requireField ctx "to_zone" jAsString json + case ( requireField ctx "world_x" asNumber json + , requireField ctx "from_zone" asString json + , requireField ctx "to_zone" asString json ) of - (Ok wx, Ok fz, Ok tz) => Ok (MkZoneTransition (MkWorldX wx) fz tz) - (e1, e2, e3) => Errs (collectErrs [e1, e2, e3]) + (Got wx, Got fz, Got tz) => Got (MkZoneTransition (MkWorldX wx) fz tz) + (e1, e2, e3) => Errs (collectErrs [e1, e2, e3]) where collectErrs : List (Extracted a) -> ExtractionErrors collectErrs [] = [] @@ -546,19 +303,19 @@ extractZoneTransition ctx json = ||| Extract a list of items from a JSON array, accumulating all errors. ||| Each element is labelled with its index for error context. export -extractList : String -> (String -> JValue -> Extracted a) -> JValue -> Extracted (List a) +extractList : String -> (String -> JsonValue -> Extracted a) -> JsonValue -> Extracted (List a) extractList ctx extractor json = - case jAsArray json of + case asArray json of Nothing => Errs [ctx ++ ": expected JSON array"] Just xs => go xs 0 [] [] where - go : List JValue -> Nat -> List a -> ExtractionErrors -> Extracted (List a) - go [] _ acc [] = Ok (reverse acc) + go : List JsonValue -> Nat -> List a -> ExtractionErrors -> Extracted (List a) + go [] _ acc [] = Got (reverse acc) go [] _ _ errs = Errs (reverse errs) go (x :: xs) idx acc errs = let elemCtx = ctx ++ "[" ++ show idx ++ "]" in case extractor elemCtx x of - Ok val => go xs (S idx) (val :: acc) errs + Got val => go xs (S idx) (val :: acc) errs Errs es => go xs (S idx) acc (es ++ errs) ------------------------------------------------------------------------ @@ -579,50 +336,46 @@ extractList ctx extractor json = ||| Fields not yet extracted (dogs, drones, assassins, items, wiring, ||| mission, physical, device_defences) return empty defaults. These will ||| be filled in as their respective extractors are implemented. -||| -||| TODO(proven-integration): Replace parseJsonString call with -||| Proven.SafeJson.Parser.parse, then convert Proven.SafeJson.Parser.JsonValue -||| to JValue (or unify the types). export parseLevelJson : String -> Either String LevelData parseLevelJson input = - case parseJsonString input of - Left err => Left ("JSON parse failure: " ++ err) + case parse input of + Left err => Left ("JSON parse failure: " ++ show err) Right json => extractedToEither (extractLevelData json) where ||| Build a LevelData from the top-level JSON object. ||| Accumulates errors across all fields so the caller gets a complete ||| report rather than stopping at the first problem. - extractLevelData : JValue -> Extracted LevelData + extractLevelData : JsonValue -> Extracted LevelData extractLevelData json = - let devicesR = case jGet "devices" json of - Nothing => Ok [] + let devicesR = case get "devices" json of + Nothing => Got [] Just v => extractList "devices" extractDevice v - zonesR = case jGet "zones" json of - Nothing => Ok [] + zonesR = case get "zones" json of + Nothing => Got [] Just v => extractList "zones" extractZone v - guardsR = case jGet "guards" json of - Nothing => Ok [] + guardsR = case get "guards" json of + Nothing => Got [] Just v => extractList "guards" extractGuard v - ztR = case jGet "zone_transitions" json of - Nothing => Ok [] + ztR = case get "zone_transitions" json of + Nothing => Got [] Just v => extractList "zone_transitions" extractZoneTransition v - hasPbxR = case jGet "has_pbx" json of - Nothing => Ok False - Just v => case jAsBool v of - Just b => Ok b + hasPbxR = case get "has_pbx" json of + Nothing => Got False + Just v => case asBool v of + Just b => Got b Nothing => Errs ["has_pbx: expected boolean"] - pbxIpR = case jGet "pbx_ip" json of - Nothing => Ok (MkIpAddress 0 0 0 0) + pbxIpR = case get "pbx_ip" json of + Nothing => Got (MkIpAddress 0 0 0 0) Just v => extractIpAddress "pbx_ip" v - pbxWxR = case jGet "pbx_world_x" json of - Nothing => Ok (MkWorldX 0.0) - Just v => case jAsNumber v of - Just n => Ok (MkWorldX n) + pbxWxR = case get "pbx_world_x" json of + Nothing => Got (MkWorldX 0.0) + Just v => case asNumber v of + Just n => Got (MkWorldX n) Nothing => Errs ["pbx_world_x: expected number"] in case (devicesR, zonesR, guardsR, ztR, hasPbxR, pbxIpR, pbxWxR) of - (Ok devs, Ok zs, Ok gs, Ok zt, Ok hp, Ok pip, Ok pwx) => - Ok (MkLevelData + (Got devs, Got zs, Got gs, Got zt, Got hp, Got pip, Got pwx) => + Got (MkLevelData devs -- devices zs -- zones gs -- guards @@ -656,10 +409,10 @@ parseLevelJson input = ||| Run cross-domain validation checks on a LevelData and collect all ||| failures as human-readable strings. ||| -||| This function performs the decidable (Bool-returning) subset of the -||| checks that Validation.idr encodes as proofs. It cannot construct -||| the proof witnesses (those require compile-time evidence), but it -||| can report whether the data WOULD pass validation. +||| Performs the decidable (Bool-returning) subset of the checks that +||| Validation.idr encodes as proofs. It cannot construct the proof +||| witnesses (those require compile-time evidence) but it can report +||| whether the data WOULD pass validation. ||| ||| Checks performed: ||| 1. Every guard references a zone that exists in the zone list. @@ -667,9 +420,6 @@ parseLevelJson input = ||| 3. PBX IP (when enabled) exists in the device registry. ||| 4. No duplicate device IPs. ||| 5. No duplicate zone names. -||| -||| @level The level data to validate -||| @return A list of failure descriptions (empty means all checks pass) export validateAndReport : LevelData -> List String validateAndReport level = @@ -738,921 +488,138 @@ validateAndReport level = else findDupNames xs (x :: seen) ------------------------------------------------------------------------ +-- Game-specific arithmetic (built on Proven.SafeMath) ------------------------------------------------------------------------ --- --- SECTION 2: SafeMath Bridge --- --- Safe arithmetic for game mechanics: damage calculations, HP clamping, --- overflow-checked stat modifications, percentage-based alert thresholds. --- ------------------------------------------------------------------------- ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace this section with: --- import Proven.SafeMath --- once the proven package is declared as a dependency in idaptik-ums.ipkg. - ------------------------------------------------------------------------- --- 64-bit overflow bounds (mirrors Proven.SafeMath) ------------------------------------------------------------------------- - -||| Maximum signed 64-bit integer value. -||| Locally mirrored from Proven.SafeMath.maxInt64. -export -bridgeMaxInt64 : Integer -bridgeMaxInt64 = 9223372036854775807 - -||| Minimum signed 64-bit integer value. -||| Locally mirrored from Proven.SafeMath.minInt64. -export -bridgeMinInt64 : Integer -bridgeMinInt64 = -9223372036854775808 - -||| Check whether an integer fits in signed 64 bits. -||| Mirrors Proven.SafeMath.fitsInt64. -fitsInt64 : Integer -> Bool -fitsInt64 n = n >= bridgeMinInt64 && n <= bridgeMaxInt64 - ------------------------------------------------------------------------- --- Checked arithmetic (mirrors Proven.SafeMath.addChecked etc.) ------------------------------------------------------------------------- - -||| Safe addition with 64-bit overflow detection. -||| Used for stat accumulation (e.g. adding XP, stacking buffs). -||| -||| @a First operand -||| @b Second operand -||| @return Just result if no overflow, Nothing otherwise -export -gameMathAdd : Integer -> Integer -> Maybe Integer -gameMathAdd a b = - let result = a + b - in if fitsInt64 result then Just result else Nothing - -||| Safe subtraction with 64-bit underflow detection. -||| Used for damage application where HP must not wrap negative. -||| -||| @a Value to subtract from -||| @b Amount to subtract -||| @return Just result if no underflow, Nothing otherwise -export -gameMathSub : Integer -> Integer -> Maybe Integer -gameMathSub a b = - let result = a - b - in if fitsInt64 result then Just result else Nothing - -||| Safe multiplication with 64-bit overflow detection. -||| Used for critical-hit multipliers and combo damage scaling. -||| -||| @a First factor -||| @b Second factor -||| @return Just result if no overflow, Nothing otherwise -export -gameMathMul : Integer -> Integer -> Maybe Integer -gameMathMul a b = - let result = a * b - in if fitsInt64 result then Just result else Nothing - ------------------------------------------------------------------------- --- Safe division (mirrors Proven.SafeMath.div) ------------------------------------------------------------------------- - -||| Safe integer division for damage calculations. -||| Returns Nothing on division by zero instead of crashing. -||| -||| Example: splitting damage across multiple targets. -||| gameMathDiv 100 3 = Just 33 -||| gameMathDiv 100 0 = Nothing -||| -||| @numerator The dividend -||| @denominator The divisor -||| @return Just quotient, or Nothing for division by zero -export -gameMathDiv : (numerator : Integer) -> (denominator : Integer) -> Maybe Integer -gameMathDiv _ 0 = Nothing -gameMathDiv n d = Just (n `div` d) - -||| Safe division with fallback for game mechanics. -||| When the divisor is zero, returns the default instead of crashing. -||| Useful for averages where the count might be zero. -||| -||| @def Default value returned on division by zero -||| @n Dividend -||| @d Divisor -export -gameMathDivOr : (def : Integer) -> (n : Integer) -> (d : Integer) -> Integer -gameMathDivOr def _ 0 = def -gameMathDivOr _ n d = n `div` d - ------------------------------------------------------------------------- --- Clamping (mirrors Proven.SafeMath.clamp) ------------------------------------------------------------------------- - -||| Clamp a value to [lo, hi]. -||| Core operation for HP bars, energy gauges, alert levels. -||| -||| Example: -||| clampGameValue 0 100 (-5) = 0 -||| clampGameValue 0 100 150 = 100 -||| clampGameValue 0 100 42 = 42 -||| -||| @lo Minimum allowed value (inclusive) -||| @hi Maximum allowed value (inclusive) -||| @value The raw value to clamp -||| @return value clamped into [lo, hi] -export -clampGameValue : (lo : Integer) -> (hi : Integer) -> (value : Integer) -> Integer -clampGameValue lo hi value = - if value < lo then lo - else if value > hi then hi - else value -||| Clamp HP to [0, maxHP]. Specialisation of clampGameValue for hit points. -||| -||| @maxHP The character's maximum HP -||| @rawHP The raw HP value (may be negative after damage or >max after heal) -||| @return HP clamped to [0, maxHP] +||| Clamp HP to [0, maxHP]. Specialisation of Proven.SafeMath.clamp. export clampHP : (maxHP : Integer) -> (rawHP : Integer) -> Integer -clampHP maxHP rawHP = clampGameValue 0 maxHP rawHP +clampHP maxHP rawHP = clamp 0 maxHP rawHP -||| Clamp alert level to valid range [0, 5]. -||| IDApTIK uses 6 alert tiers: 0 (undetected) through 5 (lockdown). -||| -||| @raw Raw alert value -||| @return Clamped alert level +||| Clamp alert level to [0, 5]. IDApTIK uses 6 alert tiers: +||| 0 (undetected) through 5 (lockdown). export -clampAlertLevel : (raw : Integer) -> Integer -clampAlertLevel = clampGameValue 0 5 - ------------------------------------------------------------------------- --- Percentage operations (mirrors Proven.SafeMath.percentOf / asPercent) ------------------------------------------------------------------------- - -||| Calculate a percentage of a total, safely. -||| Used for alert thresholds (e.g. "trigger alarm at 75% detection"). -||| -||| percentOfTotal 75 200 = Just 150 -||| percentOfTotal 50 0 = Just 0 -||| -||| @percent Percentage (0-100 typical, but any integer allowed) -||| @total The base value -||| @return Just (percent * total / 100), or Nothing on overflow -export -percentOfTotal : (percent : Integer) -> (total : Integer) -> Maybe Integer -percentOfTotal percent total = do - product <- gameMathMul percent total - gameMathDiv product 100 - -||| What percentage is part of whole? -||| Used for progress bars and detection meter display. -||| -||| asGamePercent 50 200 = Just 25 -||| asGamePercent 3 0 = Nothing -||| -||| @part The partial value -||| @whole The total value -||| @return Just percentage, or Nothing on division by zero / overflow -export -asGamePercent : (part : Integer) -> (whole : Integer) -> Maybe Integer -asGamePercent part whole = do - scaled <- gameMathMul part 100 - gameMathDiv scaled whole - ------------------------------------------------------------------------- --- Game-specific arithmetic combinators ------------------------------------------------------------------------- +clampAlertLevel : Integer -> Integer +clampAlertLevel raw = clamp 0 5 raw ||| Apply damage to current HP, clamping to [0, maxHP]. ||| Total: cannot crash, always returns a valid HP value. -||| -||| @maxHP Character's maximum HP -||| @currentHP Current HP before damage -||| @damage Raw damage amount (positive = damage, negative = healing) -||| @return New HP, clamped to [0, maxHP] +||| Underflow (massive damage) floors HP to 0. export applyDamage : (maxHP : Integer) -> (currentHP : Integer) -> (damage : Integer) -> Integer applyDamage maxHP currentHP damage = - case gameMathSub currentHP damage of + case subChecked currentHP damage of Just newHP => clampHP maxHP newHP - Nothing => 0 -- Underflow means massive damage: HP floors to 0 + Nothing => 0 -||| Calculate critical hit damage with overflow protection. +||| Critical hit damage with overflow protection. ||| Multiplies base damage by a multiplier, clamping to maxDamage cap. -||| -||| @baseDamage Raw damage before crit -||| @multiplier Crit multiplier (e.g. 2 for double damage) -||| @maxDamage Damage cap to prevent absurd values -||| @return Crit damage, clamped to [0, maxDamage] +||| Overflow (huge multiplier) caps to maxDamage. export critDamage : (baseDamage : Integer) -> (multiplier : Integer) -> (maxDamage : Integer) -> Integer critDamage baseDamage multiplier maxDamage = - case gameMathMul baseDamage multiplier of - Just product => clampGameValue 0 maxDamage product - Nothing => maxDamage -- Overflow means huge: cap to maxDamage + case mulChecked baseDamage multiplier of + Just product => clamp 0 maxDamage product + Nothing => maxDamage ||| Check if an alert threshold has been reached. -||| Returns True when the current detection level meets or exceeds -||| the given percentage of the maximum detection capacity. -||| -||| @thresholdPercent Threshold percentage (0-100) -||| @currentDetection Current detection accumulator -||| @maxDetection Maximum detection capacity -||| @return True if threshold is met or exceeded +||| Returns True when current detection meets or exceeds +||| `thresholdPercent` of maxDetection. On overflow, conservatively +||| reports threshold as reached (worst-case for the player). export alertThresholdReached : (thresholdPercent : Integer) -> (currentDetection : Integer) -> (maxDetection : Integer) -> Bool alertThresholdReached thresholdPercent currentDetection maxDetection = - case percentOfTotal thresholdPercent maxDetection of + case percentOf thresholdPercent maxDetection of Just threshold => currentDetection >= threshold - Nothing => True -- On overflow, assume worst case (alert triggered) - + Nothing => True ------------------------------------------------------------------------ +-- Game-specific string operations (built on Proven.SafeString) ------------------------------------------------------------------------ --- --- SECTION 3: SafeString Bridge --- --- Safe text operations for player input handling, terminal text --- processing, level name validation, and display truncation. --- ------------------------------------------------------------------------- ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace this section with: --- import Proven.SafeString --- once the proven package is declared as a dependency in idaptik-ums.ipkg. - ------------------------------------------------------------------------- --- Safe character access (mirrors Proven.SafeString.charAt / substring) ------------------------------------------------------------------------- - -||| Get character at index, returning Nothing if out of bounds. -||| Mirrors Proven.SafeString.charAt. -||| Used for cursor-position display in the terminal hacking UI. -||| -||| @s Source string -||| @idx Zero-based character index -||| @return Just the character, or Nothing if out of bounds -export -gameCharAt : String -> Nat -> Maybe Char -gameCharAt s idx = index' idx (unpack s) - where - index' : Nat -> List Char -> Maybe Char - index' _ [] = Nothing - index' Z (x :: _) = Just x - index' (S n) (_ :: xs) = index' n xs - -||| Get substring safely, returning Nothing for invalid indices. -||| Mirrors Proven.SafeString.substring. -||| Used for extracting visible portions of scrolling terminal output. -||| -||| @start Start index (0-based) -||| @len Desired length -||| @s Source string -||| @return Just the substring, or Nothing if start is past end -export -gameSubstring : (start : Nat) -> (len : Nat) -> String -> Maybe String -gameSubstring start len s = - let chars = unpack s - totalLen = length chars - in if start > totalLen - then Nothing - else Just $ pack $ take len (drop start chars) ------------------------------------------------------------------------- --- String transformation (mirrors Proven.SafeString.trim / truncate) ------------------------------------------------------------------------- - -||| Trim whitespace from both ends. -||| Mirrors Proven.SafeString.trim. -||| Used for normalising player-typed commands in the terminal. -||| -||| @s Raw input string -||| @return Trimmed string -export -gameTrim : String -> String -gameTrim s = ltrim (rtrim s) - where - rtrim : String -> String - rtrim str = pack (reverse (dropWhile isSpace (reverse (unpack str)))) - - ltrim : String -> String - ltrim str = pack (dropWhile isSpace (unpack str)) - -||| Truncate string to maximum length. -||| Mirrors Proven.SafeString.truncate. -||| Used for fitting device names and zone labels into fixed-width UI panels. -||| -||| @maxLen Maximum allowed character count -||| @s Source string -||| @return String truncated to at most maxLen characters -export -gameTruncate : (maxLen : Nat) -> String -> String -gameTruncate maxLen s = - if length s <= maxLen - then s - else pack (take maxLen (unpack s)) - -||| Truncate with ellipsis for display contexts where the user should -||| know the text was cut. Reserves 3 characters for "...". -||| -||| @maxLen Maximum allowed length (including ellipsis) -||| @s Source string -||| @return Truncated string, with "..." appended if truncation occurred -export -gameTruncateEllipsis : (maxLen : Nat) -> String -> String -gameTruncateEllipsis maxLen s = - if length s <= maxLen - then s - else if maxLen <= 3 - then gameTruncate maxLen s - else gameTruncate (minus maxLen 3) s ++ "..." - ------------------------------------------------------------------------- --- String splitting (mirrors Proven.SafeString.split) ------------------------------------------------------------------------- - -||| Split string on a delimiter character. -||| Mirrors Proven.SafeString.split. -||| Used for parsing comma-separated command arguments in the terminal. -||| -||| @delim Delimiter character -||| @s Source string -||| @return List of substrings between delimiters -export -gameSplit : (delim : Char) -> String -> List String -gameSplit delim s = splitHelper delim (unpack s) [] [] - where - splitHelper : Char -> List Char -> List Char -> List String -> List String - splitHelper _ [] current acc = reverse (pack (reverse current) :: acc) - splitHelper d (c :: cs) current acc = - if c == d - then splitHelper d cs [] (pack (reverse current) :: acc) - else splitHelper d cs (c :: current) acc - ------------------------------------------------------------------------- --- String validation (mirrors Proven.SafeString.isAscii / parseNat / parseInt) ------------------------------------------------------------------------- - -||| Check if string contains only ASCII characters. -||| Mirrors Proven.SafeString.isAscii. -||| Used to validate player names and level identifiers (no Unicode exploits). -||| -||| @s String to check -||| @return True if all characters have ordinal < 128 -export -gameIsAscii : String -> Bool -gameIsAscii s = all (\c => ord c < 128) (unpack s) - -||| Check if string contains only digits. -||| Locally mirrored from Proven.SafeString.isDigits. -||| Used for validating numeric input in terminal hack sequences. -||| -||| @s String to check -||| @return True if non-empty and all chars are digits -gameIsDigits : String -> Bool -gameIsDigits s = length s > 0 && all isDigit (unpack s) - -||| Parse a string to a natural number, returning Nothing for invalid input. -||| Mirrors Proven.SafeString.parseNat. -||| Used for parsing port numbers and IP octets typed by the player. -||| -||| @s String to parse -||| @return Just the Nat value, or Nothing if not a valid non-negative integer -export -gameParseNat : String -> Maybe Nat -gameParseNat s = - if length s == 0 || not (gameIsDigits s) - then Nothing - else Just (parseNat' (unpack s) 0) - where - parseNat' : List Char -> Nat -> Nat - parseNat' [] acc = acc - parseNat' (c :: cs) acc = - let digit = cast (ord c - ord '0') - in parseNat' cs (acc * 10 + digit) - -||| Parse a string to an Integer, handling optional leading minus. -||| Mirrors Proven.SafeString.parseInt. -||| Used for parsing signed values in terminal expressions. -||| -||| @s String to parse -||| @return Just the Integer, or Nothing if not a valid integer -export -gameParseInt : String -> Maybe Integer -gameParseInt s = case strM s of - StrNil => Nothing - StrCons '-' rest => - map negate (gameParseNat rest >>= \n => Just (cast n)) - StrCons '+' rest => - gameParseNat rest >>= \n => Just (cast n) - StrCons _ _ => - gameParseNat s >>= \n => Just (cast n) - ------------------------------------------------------------------------- --- Game-specific string combinators ------------------------------------------------------------------------- - -||| Validate a level name: must be non-empty, ASCII-only, and within length limit. -||| Returns Left with error description, or Right with the validated name. -||| -||| @maxLen Maximum allowed length for level names -||| @name Candidate level name -||| @return Right name if valid, Left error otherwise +||| Validate a level name: must be non-empty, ASCII-only, within length limit. export validateLevelName : (maxLen : Nat) -> (name : String) -> Either String String -validateLevelName maxLen name = - let trimmed = gameTrim name +validateLevelName maxLen rawName = + let trimmed = trim rawName in if length trimmed == 0 then Left "Level name must not be empty" - else if not (gameIsAscii trimmed) + else if not (isAscii trimmed) then Left "Level name must contain only ASCII characters" else if length trimmed > maxLen then Left ("Level name exceeds maximum length of " ++ show maxLen) else Right trimmed ||| Format a device name for display in the network map panel. -||| Truncates to the panel width and pads with spaces for alignment. -||| -||| @panelWidth Available character width -||| @deviceName Raw device name from level data -||| @return Display-ready string, exactly panelWidth characters +||| Truncates to panel width with ellipsis, then right-pads with spaces. export formatDeviceLabel : (panelWidth : Nat) -> (deviceName : String) -> String formatDeviceLabel panelWidth deviceName = - let truncated = gameTruncateEllipsis panelWidth deviceName - currentLen = length truncated - in if currentLen >= panelWidth - then truncated - else truncated ++ pack (replicate (minus panelWidth currentLen) ' ') + let truncated = truncateWithEllipsis panelWidth deviceName + in padRight panelWidth ' ' truncated ||| Sanitise player-typed terminal command: trim, truncate, and reject ||| non-ASCII to prevent injection of control characters. -||| -||| @maxLen Maximum command length -||| @raw Raw player input -||| @return Right with sanitised command, or Left with rejection reason export sanitiseTerminalInput : (maxLen : Nat) -> (raw : String) -> Either String String sanitiseTerminalInput maxLen raw = - let trimmed = gameTrim raw + let trimmed = trim raw in if length trimmed == 0 then Left "Empty command" - else if not (gameIsAscii trimmed) + else if not (isAscii trimmed) then Left "Non-ASCII characters not permitted in terminal" - else Right (gameTruncate maxLen trimmed) + else Right (truncate maxLen trimmed) - ------------------------------------------------------------------------- ------------------------------------------------------------------------ --- --- SECTION 4: SafeCrypto Bridge --- --- Constant-time operations for multiplayer authentication tokens --- and game-sync integrity verification. --- ------------------------------------------------------------------------- ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace this section with: --- import Proven.SafeCrypto --- once the proven package is declared as a dependency in idaptik-ums.ipkg. - ------------------------------------------------------------------------- --- Byte types (mirrors Proven.SafeCrypto) ------------------------------------------------------------------------- - -||| A single byte. Mirrors Proven.SafeCrypto.Byte. -public export -GameByte : Type -GameByte = Bits8 - -||| A sequence of bytes. Mirrors Proven.SafeCrypto.Bytes. -public export -GameBytes : Type -GameBytes = List GameByte - ------------------------------------------------------------------------- --- Constant-time comparison (mirrors Proven.SafeCrypto.constantTimeEq) ------------------------------------------------------------------------- - -||| Constant-time byte sequence comparison. -||| Mirrors Proven.SafeCrypto.constantTimeEq. -||| -||| CRITICAL for multiplayer: timing side-channels in token comparison -||| would allow an attacker to brute-force auth tokens byte-by-byte. -||| This comparison always examines all bytes regardless of where -||| the first mismatch occurs. -||| -||| @xs First byte sequence -||| @ys Second byte sequence -||| @return True iff sequences are the same length and all bytes match -export -gameConstantTimeEq : GameBytes -> GameBytes -> Bool -gameConstantTimeEq xs ys = - if length xs /= length ys - then False - else ctGo xs ys 0 - where - ctGo : GameBytes -> GameBytes -> GameByte -> Bool - ctGo [] [] acc = acc == 0 - ctGo (x :: xs') (y :: ys') acc = ctGo xs' ys' (acc `or` (x `xor` y)) - ctGo _ _ _ = False -- Unreachable: lengths already checked - ------------------------------------------------------------------------- --- Hex conversion utilities (mirrors Proven.SafeCrypto) ------------------------------------------------------------------------- - -||| Convert a hex string to bytes. Returns Nothing for invalid hex. -||| Used for parsing auth tokens received as hex strings over the wire. -||| -||| @s Hex-encoded string (must have even length) -||| @return Just the byte sequence, or Nothing for invalid hex -export -gameHexToBytes : String -> Maybe GameBytes -gameHexToBytes s = go (unpack s) [] - where - hexVal : Char -> Maybe Nat - hexVal c = - if c >= '0' && c <= '9' then Just (cast (ord c - ord '0')) - else if c >= 'a' && c <= 'f' then Just (cast (ord c - ord 'a' + 10)) - else if c >= 'A' && c <= 'F' then Just (cast (ord c - ord 'A' + 10)) - else Nothing - - go : List Char -> GameBytes -> Maybe GameBytes - go [] acc = Just (reverse acc) - go [_] _ = Nothing -- Odd number of hex chars - go (h1 :: h2 :: rest) acc = do - v1 <- hexVal h1 - v2 <- hexVal h2 - go rest (cast (v1 * 16 + v2) :: acc) - -||| Convert bytes to hex string. -||| Used for encoding auth tokens for wire transmission. -||| -||| @bytes Byte sequence to encode -||| @return Lowercase hex string -export -gameBytesToHex : GameBytes -> String -gameBytesToHex bytes = concat (map byteToHex bytes) - where - hexDigit : Nat -> Char - hexDigit n = if n < 10 then chr (ord '0' + cast n) else chr (ord 'a' + cast n - 10) - - byteToHex : GameByte -> String - byteToHex b = - let n = cast {to=Nat} b - in pack [hexDigit (n `div` 16), hexDigit (n `mod` 16)] - ------------------------------------------------------------------------- --- Hash / HMAC stubs (mirrors Proven.SafeCrypto.hash / hmac) ------------------------------------------------------------------------- - --- NOTE: Proven.SafeCrypto.hash and Proven.SafeCrypto.hmac are themselves --- stubs awaiting Zig FFI implementation. We mirror the type signatures --- here so that call sites compile and can be wired up later. - -||| Supported hash algorithms for game sync integrity. -public export -data GameHashAlg = GameSHA256 | GameBLAKE2b - -||| Hash result: opaque byte list (length depends on algorithm). -||| Awaiting FFI: this is a stub that returns an empty byte list. -||| -||| @alg The hash algorithm to use -||| @input Bytes to hash -||| @return Hash digest (currently empty; real impl via Zig FFI) -export -gameHash : (alg : GameHashAlg) -> GameBytes -> GameBytes -gameHash _ _ = [] -- Stub: awaiting Zig FFI via Proven.SafeCrypto.hash - -||| HMAC result: keyed hash for message authentication. -||| Awaiting FFI: this is a stub that returns an empty byte list. -||| -||| @alg The hash algorithm to use -||| @key HMAC key bytes -||| @msg Message bytes -||| @return HMAC digest (currently empty; real impl via Zig FFI) -export -gameHmac : (alg : GameHashAlg) -> (key : GameBytes) -> (msg : GameBytes) -> GameBytes -gameHmac _ _ _ = [] -- Stub: awaiting Zig FFI via Proven.SafeCrypto.hmac - ------------------------------------------------------------------------- --- Game-specific crypto combinators +-- Game-specific crypto (built on Proven.SafeCrypto) ------------------------------------------------------------------------ ||| Verify a multiplayer auth token using constant-time comparison. -||| Compares a received hex-encoded token against the expected token bytes. -||| -||| @expectedBytes The expected token as raw bytes -||| @receivedHex The received token as a hex string -||| @return True if tokens match, False otherwise (including parse failure) +||| Compares a received hex-encoded token against expected token bytes. +||| Returns False (not an error) on invalid hex. export -verifyAuthToken : (expectedBytes : GameBytes) -> (receivedHex : String) -> Bool +verifyAuthToken : (expectedBytes : Bytes) -> (receivedHex : String) -> Bool verifyAuthToken expectedBytes receivedHex = - case gameHexToBytes receivedHex of - Nothing => False -- Invalid hex: reject - Just receivedBytes => gameConstantTimeEq expectedBytes receivedBytes + case hexToBytes receivedHex of + Nothing => False + Just receivedBytes => constantTimeEq expectedBytes receivedBytes -||| Compute integrity tag for a game-sync payload. -||| Uses HMAC with the session key to prevent tampering. -||| Currently a stub: returns empty bytes until Zig FFI is available. -||| -||| @sessionKey Session-specific HMAC key -||| @payload Serialised game state bytes -||| @return HMAC tag bytes (empty until FFI wired) -export -gameSyncTag : (sessionKey : GameBytes) -> (payload : GameBytes) -> GameBytes -gameSyncTag sessionKey payload = gameHmac GameSHA256 sessionKey payload - - ------------------------------------------------------------------------- ------------------------------------------------------------------------- --- --- SECTION 5: SafeInput Bridge --- --- Player keystroke handling for terminal hacking sequences. --- Provides input buffers, keystroke processing, and typed input --- validation for the in-game terminal UI. --- ------------------------------------------------------------------------- ------------------------------------------------------------------------- - --- TODO(proven-integration): Replace this section with: --- import SafeInput --- once the proven package is declared as a dependency in idaptik-ums.ipkg. - ------------------------------------------------------------------------- --- Input result type (mirrors SafeInput.InputResult) ------------------------------------------------------------------------- - -||| Result of validating player input in the terminal. -||| Mirrors SafeInput.InputResult. -||| -||| - GameInputValid: input is complete and valid -||| - GameInputInvalid: input is rejected (with reason) -||| - GameInputPartial: input is valid so far but incomplete (with hint) -public export -data GameInputResult : Type -> Type where - GameInputValid : a -> GameInputResult a - GameInputInvalid : (reason : String) -> GameInputResult a - GameInputPartial : (hint : String) -> GameInputResult a - -||| Map over a GameInputResult. -export -mapGameInput : (a -> b) -> GameInputResult a -> GameInputResult b -mapGameInput f (GameInputValid x) = GameInputValid (f x) -mapGameInput _ (GameInputInvalid r) = GameInputInvalid r -mapGameInput _ (GameInputPartial h) = GameInputPartial h - -||| Convert GameInputResult to Either (collapsing Partial to Left). -export -gameInputToEither : GameInputResult a -> Either String a -gameInputToEither (GameInputValid x) = Right x -gameInputToEither (GameInputInvalid r) = Left r -gameInputToEither (GameInputPartial h) = Left ("Incomplete: " ++ h) - ------------------------------------------------------------------------- --- Character classes (mirrors SafeInput.CharClass) ------------------------------------------------------------------------- - -||| Character class for input filtering. -||| Mirrors SafeInput.CharClass. -public export -data GameCharClass : Type where - GameAlphanumeric : GameCharClass - GameAlphabetic : GameCharClass - GameNumeric : GameCharClass - GamePrintable : GameCharClass - GameIdentifier : GameCharClass -- Letters, digits, underscore - GameHexDigit : GameCharClass - GameCustom : (Char -> Bool) -> GameCharClass - -||| Check if a character matches a class. -||| Mirrors SafeInput.matchesClass. -export -gameMatchesClass : Char -> GameCharClass -> Bool -gameMatchesClass c GameAlphanumeric = isAlphaNum c -gameMatchesClass c GameAlphabetic = isAlpha c -gameMatchesClass c GameNumeric = isDigit c -gameMatchesClass c GamePrintable = c >= ' ' && c <= '~' -gameMatchesClass c GameIdentifier = isAlphaNum c || c == '_' -gameMatchesClass c GameHexDigit = isHexDigit c -gameMatchesClass c (GameCustom f) = f c - ------------------------------------------------------------------------- --- Input buffer (mirrors SafeInput.InputBuffer) ------------------------------------------------------------------------- - -||| Input buffer with validation, for the in-game terminal. -||| Mirrors SafeInput.InputBuffer. -public export -record GameInputBuffer where - constructor MkGameBuffer - gibContent : String - gibMaxLength : Nat - gibCursorPos : Nat - gibCharFilter : Maybe GameCharClass - -||| Create an empty input buffer with a given maximum length. -||| Mirrors SafeInput.emptyBuffer. -||| -||| @maxLen Maximum number of characters the buffer can hold -export -gameEmptyBuffer : (maxLen : Nat) -> GameInputBuffer -gameEmptyBuffer maxLen = MkGameBuffer "" maxLen 0 Nothing - -||| Create a buffer with a character class filter. -||| Mirrors SafeInput.filteredBuffer. -||| -||| @maxLen Maximum number of characters -||| @cls Character class filter -export -gameFilteredBuffer : (maxLen : Nat) -> GameCharClass -> GameInputBuffer -gameFilteredBuffer maxLen cls = MkGameBuffer "" maxLen 0 (Just cls) - -||| Get buffer content. -export -gameBufferContent : GameInputBuffer -> String -gameBufferContent = gibContent - -||| Check if the buffer is empty. -export -gameBufferIsEmpty : GameInputBuffer -> Bool -gameBufferIsEmpty buf = buf.gibContent == "" - -||| Check if the buffer is full. -export -gameBufferIsFull : GameInputBuffer -> Bool -gameBufferIsFull buf = length buf.gibContent >= buf.gibMaxLength +-- gameSyncTag (previously a stub returning []) was dropped here: +-- callers should use Proven.SafeCrypto.hmac directly once it has a +-- real FFI backing. Re-introduce a wrapper if a stable idaptik-named +-- entry point is needed. ------------------------------------------------------------------------ --- Keystroke handling (mirrors SafeInput.Keystroke / handleKey) +-- Game-specific input (built on Proven.SafeInput) ------------------------------------------------------------------------ -||| Keystroke representation for the terminal hacking UI. -||| Mirrors SafeInput.Keystroke. -public export -data GameKeystroke : Type where - GKCharKey : Char -> GameKeystroke - GKBackspace : GameKeystroke - GKDelete : GameKeystroke - GKEnter : GameKeystroke - GKEscape : GameKeystroke - GKLeft : GameKeystroke - GKRight : GameKeystroke - GKHome : GameKeystroke - GKEnd : GameKeystroke - GKTab : GameKeystroke - -||| Handle a keystroke, updating the buffer. -||| Mirrors SafeInput.handleKey. -||| This is the core input processing function for the terminal hacking UI. -||| Character filtering and length limits are enforced automatically. -||| -||| @key Keystroke to process -||| @buf Current buffer state -||| @return Updated buffer after applying the keystroke +||| Terminal hacking input buffer: printable ASCII, 80 chars max. export -gameHandleKey : GameKeystroke -> GameInputBuffer -> GameInputBuffer -gameHandleKey key buf = case key of - GKCharKey c => insertChar c buf - GKBackspace => deleteBackward buf - GKDelete => deleteForward buf - GKLeft => { gibCursorPos := buf.gibCursorPos `minus` 1 } buf - GKRight => { gibCursorPos := min (buf.gibCursorPos + 1) (length buf.gibContent) } buf - GKHome => { gibCursorPos := 0 } buf - GKEnd => { gibCursorPos := length buf.gibContent } buf - _ => buf -- Enter, Escape, Tab handled at higher level - where - insertChar : Char -> GameInputBuffer -> GameInputBuffer - insertChar c b = - if length b.gibContent >= b.gibMaxLength then b - else case b.gibCharFilter of - Nothing => doInsert c b - Just cls => if gameMatchesClass c cls then doInsert c b else b - - doInsert : Char -> GameInputBuffer -> GameInputBuffer - doInsert c b = - let chars = unpack b.gibContent - (before, after) = splitAt b.gibCursorPos chars - newContent = pack (before ++ [c] ++ after) - in { gibContent := newContent, gibCursorPos := b.gibCursorPos + 1 } b - - deleteBackward : GameInputBuffer -> GameInputBuffer - deleteBackward b = - if b.gibCursorPos == 0 then b - else let chars = unpack b.gibContent - (before, after) = splitAt b.gibCursorPos chars - newBefore = take (length before `minus` 1) before - newContent = pack (newBefore ++ after) - in { gibContent := newContent, gibCursorPos := b.gibCursorPos `minus` 1 } b +terminalHackBuffer : InputBuffer +terminalHackBuffer = filteredBuffer 80 Printable - deleteForward : GameInputBuffer -> GameInputBuffer - deleteForward b = - let chars = unpack b.gibContent - (before, after) = splitAt b.gibCursorPos chars - newAfter = drop 1 after - newContent = pack (before ++ newAfter) - in { gibContent := newContent } b - -||| Clear the buffer, resetting content and cursor. +||| Numeric entry buffer: 5 digits max (enough for ports 0-65535). export -gameClearBuffer : GameInputBuffer -> GameInputBuffer -gameClearBuffer buf = { gibContent := "", gibCursorPos := 0 } buf - ------------------------------------------------------------------------- --- Input validation (mirrors SafeInput.validateInt / validateNat / etc.) ------------------------------------------------------------------------- +numericEntryBuffer : InputBuffer +numericEntryBuffer = filteredBuffer 5 Numeric -||| Validate buffer content as an integer. -||| Mirrors SafeInput.validateInt. -||| Used when the player types a numeric value in terminal hack prompts. -||| -||| @s The string to validate -||| @return GameInputValid with the integer, GameInputPartial if incomplete, -||| or GameInputInvalid if the string is not a valid integer -export -gameValidateInt : String -> GameInputResult Integer -gameValidateInt s = - if s == "" then GameInputPartial "Enter a number" - else if s == "-" then GameInputPartial "Enter digits after minus" - else case parseInteger s of - Nothing => GameInputInvalid "Not a valid integer" - Just n => GameInputValid n - -||| Validate buffer content as a natural number. -||| Mirrors SafeInput.validateNat. -||| Used for IP octet entry and port number input. -||| -||| @s The string to validate -||| @return GameInputValid with the Nat, or error/partial -export -gameValidateNat : String -> GameInputResult Nat -gameValidateNat s = - if s == "" then GameInputPartial "Enter a positive number" - else case parsePositive s of - Nothing => GameInputInvalid "Not a valid positive number" - Just n => GameInputValid n - -||| Validate non-empty string. -||| Mirrors SafeInput.validateNonEmpty. -||| Used for command entry where empty input should be rejected. -||| -||| @s The string to validate -||| @return GameInputValid with the string, or GameInputPartial -export -gameValidateNonEmpty : String -> GameInputResult String -gameValidateNonEmpty s = - if s == "" then GameInputPartial "Enter some text" - else GameInputValid s - ------------------------------------------------------------------------- --- Game-specific input combinators ------------------------------------------------------------------------- - -||| Create a terminal hacking input buffer. -||| Accepts only printable ASCII characters, capped at 80 chars -||| (standard terminal width). -export -terminalHackBuffer : GameInputBuffer -terminalHackBuffer = gameFilteredBuffer 80 GamePrintable - -||| Create a numeric-only input buffer for port/octet entry. -||| Capped at 5 digits (enough for port numbers 0-65535). +||| Hex entry buffer: 64 hex chars max (256-bit hash). export -numericEntryBuffer : GameInputBuffer -numericEntryBuffer = gameFilteredBuffer 5 GameNumeric +hexEntryBuffer : InputBuffer +hexEntryBuffer = filteredBuffer 64 HexDigit -||| Create a hex-only input buffer for token/hash entry. -||| Capped at 64 hex chars (256-bit hash). +||| Process a keystroke and validate the resulting buffer as an integer. export -hexEntryBuffer : GameInputBuffer -hexEntryBuffer = gameFilteredBuffer 64 GameHexDigit - -||| Process a keystroke and validate the result as an integer. -||| Combines input handling and validation in one step. -||| -||| @key Keystroke to process -||| @buf Current buffer -||| @return Updated buffer paired with validation result -export -handleAndValidateInt : GameKeystroke -> GameInputBuffer - -> (GameInputBuffer, GameInputResult Integer) +handleAndValidateInt : Keystroke -> InputBuffer -> (InputBuffer, InputResult Integer) handleAndValidateInt key buf = - let newBuf = gameHandleKey key buf - in (newBuf, gameValidateInt (gibContent newBuf)) + let newBuf = handleKey key buf + in (newBuf, validateInt (getContent newBuf)) -||| Process a keystroke and validate the result as a Nat. -||| -||| @key Keystroke to process -||| @buf Current buffer -||| @return Updated buffer paired with validation result +||| Process a keystroke and validate as a Nat. export -handleAndValidateNat : GameKeystroke -> GameInputBuffer - -> (GameInputBuffer, GameInputResult Nat) +handleAndValidateNat : Keystroke -> InputBuffer -> (InputBuffer, InputResult Nat) handleAndValidateNat key buf = - let newBuf = gameHandleKey key buf - in (newBuf, gameValidateNat (gibContent newBuf)) + let newBuf = handleKey key buf + in (newBuf, validateNat (getContent newBuf))