|
| 1 | +-- SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +-- CratesMcp.SafeRegistry — Type-safe ABI for crates-mcp cartridge. |
| 5 | +-- |
| 6 | +-- Dependent-type state machine governing crates.io API access. |
| 7 | +-- Encodes optional Bearer token auth, crate search, metadata retrieval, |
| 8 | +-- version listing, download stats, dependency analysis, reverse deps, |
| 9 | +-- owner listing, and category/keyword browsing as compile-time invariants. |
| 10 | +-- REST API: https://crates.io/api/v1 |
| 11 | +-- No unsafe escape hatches. |
| 12 | + |
| 13 | +module CratesMcp.SafeRegistry |
| 14 | + |
| 15 | +%default total |
| 16 | + |
| 17 | +-- --------------------------------------------------------------------------- |
| 18 | +-- Authentication state machine |
| 19 | +-- --------------------------------------------------------------------------- |
| 20 | + |
| 21 | +||| Session state for crates.io MCP operations. |
| 22 | +||| Unauthenticated: no API token; read-only operations available. |
| 23 | +||| Authenticated: crates.io API token active, full access. |
| 24 | +||| RateLimited: crates.io rate limit hit (429); must wait. |
| 25 | +||| Error: unrecoverable error (invalid token, network failure). |
| 26 | +public export |
| 27 | +data SessionState |
| 28 | + = Unauthenticated |
| 29 | + | Authenticated |
| 30 | + | RateLimited |
| 31 | + | Error |
| 32 | + |
| 33 | +||| Proof that a state transition is valid. |
| 34 | +||| crates.io allows both authenticated and unauthenticated sessions. |
| 35 | +public export |
| 36 | +data ValidTransition : SessionState -> SessionState -> Type where |
| 37 | + Authenticate : ValidTransition Unauthenticated Authenticated |
| 38 | + Deauthenticate : ValidTransition Authenticated Unauthenticated |
| 39 | + Throttle : ValidTransition Authenticated RateLimited |
| 40 | + ThrottleAnon : ValidTransition Unauthenticated RateLimited |
| 41 | + Unthrottle : ValidTransition RateLimited Authenticated |
| 42 | + UnthrottleAnon : ValidTransition RateLimited Unauthenticated |
| 43 | + AuthError : ValidTransition Authenticated Error |
| 44 | + AnonError : ValidTransition Unauthenticated Error |
| 45 | + RecoverToAuth : ValidTransition Error Authenticated |
| 46 | + RecoverToAnon : ValidTransition Error Unauthenticated |
| 47 | + |
| 48 | +-- --------------------------------------------------------------------------- |
| 49 | +-- C-ABI integer encoding |
| 50 | +-- --------------------------------------------------------------------------- |
| 51 | + |
| 52 | +||| Encode session state as C-compatible integer for FFI boundary. |
| 53 | +export |
| 54 | +sessionStateToInt : SessionState -> Int |
| 55 | +sessionStateToInt Unauthenticated = 0 |
| 56 | +sessionStateToInt Authenticated = 1 |
| 57 | +sessionStateToInt RateLimited = 2 |
| 58 | +sessionStateToInt Error = 3 |
| 59 | + |
| 60 | +||| Decode integer back to session state. Returns Nothing for out-of-range. |
| 61 | +export |
| 62 | +intToSessionState : Int -> Maybe SessionState |
| 63 | +intToSessionState 0 = Just Unauthenticated |
| 64 | +intToSessionState 1 = Just Authenticated |
| 65 | +intToSessionState 2 = Just RateLimited |
| 66 | +intToSessionState 3 = Just Error |
| 67 | +intToSessionState _ = Nothing |
| 68 | + |
| 69 | +||| Check if a state transition is valid (C-ABI export). |
| 70 | +export |
| 71 | +crates_mcp_can_transition : Int -> Int -> Int |
| 72 | +crates_mcp_can_transition from to = |
| 73 | + case (intToSessionState from, intToSessionState to) of |
| 74 | + (Just Unauthenticated, Just Authenticated) => 1 |
| 75 | + (Just Authenticated, Just Unauthenticated) => 1 |
| 76 | + (Just Authenticated, Just RateLimited) => 1 |
| 77 | + (Just Unauthenticated, Just RateLimited) => 1 |
| 78 | + (Just RateLimited, Just Authenticated) => 1 |
| 79 | + (Just RateLimited, Just Unauthenticated) => 1 |
| 80 | + (Just Authenticated, Just Error) => 1 |
| 81 | + (Just Unauthenticated, Just Error) => 1 |
| 82 | + (Just Error, Just Authenticated) => 1 |
| 83 | + (Just Error, Just Unauthenticated) => 1 |
| 84 | + _ => 0 |
| 85 | + |
| 86 | +-- --------------------------------------------------------------------------- |
| 87 | +-- crates.io actions |
| 88 | +-- --------------------------------------------------------------------------- |
| 89 | + |
| 90 | +||| Actions available through the crates.io MCP cartridge. |
| 91 | +||| Grouped: Search, Metadata, Versions, Downloads, Dependencies, |
| 92 | +||| Reverse Dependencies, Owners, Categories, Keywords, Users, Features. |
| 93 | +public export |
| 94 | +data CratesAction |
| 95 | + = SearchCrates |
| 96 | + | GetCrate |
| 97 | + | GetVersion |
| 98 | + | ListVersions |
| 99 | + | GetDownloads |
| 100 | + | GetDependencies |
| 101 | + | GetReverseDependencies |
| 102 | + | GetOwners |
| 103 | + | ListCategories |
| 104 | + | GetCategory |
| 105 | + | ListKeywords |
| 106 | + | GetUser |
| 107 | + | GetFeatures |
| 108 | + |
| 109 | +||| Whether an action requires Authenticated state. |
| 110 | +||| crates.io allows unauthenticated read access for all query operations. |
| 111 | +export |
| 112 | +actionRequiresAuth : CratesAction -> Bool |
| 113 | +actionRequiresAuth _ = False |
| 114 | + |
| 115 | +||| Whether an action is a write/mutating operation. |
| 116 | +||| All crates-mcp actions are read-only queries. |
| 117 | +export |
| 118 | +actionIsMutating : CratesAction -> Bool |
| 119 | +actionIsMutating _ = False |
| 120 | + |
| 121 | +||| Encode action as C-compatible integer for FFI. |
| 122 | +export |
| 123 | +actionToInt : CratesAction -> Int |
| 124 | +actionToInt SearchCrates = 0 |
| 125 | +actionToInt GetCrate = 1 |
| 126 | +actionToInt GetVersion = 2 |
| 127 | +actionToInt ListVersions = 3 |
| 128 | +actionToInt GetDownloads = 4 |
| 129 | +actionToInt GetDependencies = 5 |
| 130 | +actionToInt GetReverseDependencies = 6 |
| 131 | +actionToInt GetOwners = 7 |
| 132 | +actionToInt ListCategories = 8 |
| 133 | +actionToInt GetCategory = 9 |
| 134 | +actionToInt ListKeywords = 10 |
| 135 | +actionToInt GetUser = 11 |
| 136 | +actionToInt GetFeatures = 12 |
| 137 | + |
| 138 | +||| Decode integer to crates action. |
| 139 | +export |
| 140 | +intToAction : Int -> Maybe CratesAction |
| 141 | +intToAction 0 = Just SearchCrates |
| 142 | +intToAction 1 = Just GetCrate |
| 143 | +intToAction 2 = Just GetVersion |
| 144 | +intToAction 3 = Just ListVersions |
| 145 | +intToAction 4 = Just GetDownloads |
| 146 | +intToAction 5 = Just GetDependencies |
| 147 | +intToAction 6 = Just GetReverseDependencies |
| 148 | +intToAction 7 = Just GetOwners |
| 149 | +intToAction 8 = Just ListCategories |
| 150 | +intToAction 9 = Just GetCategory |
| 151 | +intToAction 10 = Just ListKeywords |
| 152 | +intToAction 11 = Just GetUser |
| 153 | +intToAction 12 = Just GetFeatures |
| 154 | +intToAction _ = Nothing |
| 155 | + |
| 156 | +-- --------------------------------------------------------------------------- |
| 157 | +-- MCP tool declarations |
| 158 | +-- --------------------------------------------------------------------------- |
| 159 | + |
| 160 | +||| Tools exposed via MCP protocol for this cartridge. |
| 161 | +public export |
| 162 | +data McpTool |
| 163 | + = ToolSearchCrates |
| 164 | + | ToolGetCrate |
| 165 | + | ToolGetVersion |
| 166 | + | ToolListVersions |
| 167 | + | ToolGetDownloads |
| 168 | + | ToolGetDependencies |
| 169 | + | ToolGetReverseDependencies |
| 170 | + | ToolGetOwners |
| 171 | + | ToolListCategories |
| 172 | + | ToolGetCategory |
| 173 | + | ToolListKeywords |
| 174 | + | ToolGetUser |
| 175 | + | ToolGetFeatures |
| 176 | + |
| 177 | +||| Check if a tool requires an authenticated session. |
| 178 | +||| All crates.io read operations work without auth. |
| 179 | +export |
| 180 | +toolRequiresSession : McpTool -> Bool |
| 181 | +toolRequiresSession _ = False |
| 182 | + |
| 183 | +||| Total tool count for this cartridge. |
| 184 | +export |
| 185 | +toolCount : Nat |
| 186 | +toolCount = 13 |
| 187 | + |
| 188 | +||| Total action count for this cartridge. |
| 189 | +export |
| 190 | +actionCount : Nat |
| 191 | +actionCount = 13 |
0 commit comments