|
| 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 | +-- RokurMcp.SafeGate — Type-safe ABI for the rokur-mcp cartridge. |
| 5 | +-- |
| 6 | +-- Container pre-start secrets gate. Validates that all required secrets |
| 7 | +-- are present before allowing a container to start. Delegates to the |
| 8 | +-- Rokur sidecar service (Deno, port 9090) for policy evaluation. |
| 9 | +-- Never exposes secret values — only presence/absence verdicts. |
| 10 | + |
| 11 | +module RokurMcp.SafeGate |
| 12 | + |
| 13 | +%default total |
| 14 | + |
| 15 | +-- --------------------------------------------------------------------------- |
| 16 | +-- Gate state machine |
| 17 | +-- --------------------------------------------------------------------------- |
| 18 | + |
| 19 | +||| Gate lifecycle states for container pre-start authorization. |
| 20 | +||| |
| 21 | +||| - Idle: no authorization request pending. |
| 22 | +||| - Checking: secrets presence check in progress. |
| 23 | +||| - Allowed: all required secrets present, container may start. |
| 24 | +||| - Denied: one or more required secrets missing, container blocked. |
| 25 | +||| - Error: policy engine failure (fail-closed = deny). |
| 26 | +public export |
| 27 | +data GateState = Idle | Checking | Allowed | Denied | Error |
| 28 | + |
| 29 | +||| Proof that a gate state transition is valid. |
| 30 | +||| |
| 31 | +||| Transition graph: |
| 32 | +||| Idle -> Checking (begin authorization) |
| 33 | +||| Checking -> Allowed (all secrets present) |
| 34 | +||| Checking -> Denied (missing secrets) |
| 35 | +||| Checking -> Error (policy engine failure) |
| 36 | +||| Allowed -> Idle (reset after container started) |
| 37 | +||| Denied -> Idle (reset after denial logged) |
| 38 | +||| Error -> Idle (reset after error handled) |
| 39 | +public export |
| 40 | +data ValidGateTransition : GateState -> GateState -> Type where |
| 41 | + BeginCheck : ValidGateTransition Idle Checking |
| 42 | + Approve : ValidGateTransition Checking Allowed |
| 43 | + Reject : ValidGateTransition Checking Denied |
| 44 | + Fault : ValidGateTransition Checking Error |
| 45 | + ResetAllowed : ValidGateTransition Allowed Idle |
| 46 | + ResetDenied : ValidGateTransition Denied Idle |
| 47 | + ResetError : ValidGateTransition Error Idle |
| 48 | + |
| 49 | +-- --------------------------------------------------------------------------- |
| 50 | +-- Gate actions |
| 51 | +-- --------------------------------------------------------------------------- |
| 52 | + |
| 53 | +||| Actions that can be performed through the MCP rokur interface. |
| 54 | +public export |
| 55 | +data GateAction |
| 56 | + = AuthorizeStart -- ^ Request pre-start authorization for a container |
| 57 | + | CheckStatus -- ^ Query current secrets presence status |
| 58 | + | ReloadSecrets -- ^ Hot-reload required secrets from environment |
| 59 | + | QueryHealth -- ^ Liveness check on the Rokur sidecar |
| 60 | + |
| 61 | +||| Whether an action requires the gate to be in a specific state. |
| 62 | +||| Health is always available. AuthorizeStart requires Idle. |
| 63 | +||| CheckStatus and ReloadSecrets available in Idle or Allowed. |
| 64 | +export |
| 65 | +actionRequiresIdle : GateAction -> Bool |
| 66 | +actionRequiresIdle AuthorizeStart = True |
| 67 | +actionRequiresIdle CheckStatus = False |
| 68 | +actionRequiresIdle ReloadSecrets = False |
| 69 | +actionRequiresIdle QueryHealth = False |
| 70 | + |
| 71 | +-- --------------------------------------------------------------------------- |
| 72 | +-- Policy verdict |
| 73 | +-- --------------------------------------------------------------------------- |
| 74 | + |
| 75 | +||| Authorization verdict from the policy engine. |
| 76 | +||| Secret names are intentionally NEVER exposed — only counts. |
| 77 | +public export |
| 78 | +record AuthVerdict where |
| 79 | + constructor MkVerdict |
| 80 | + allowed : Bool |
| 81 | + policy : String -- "allow" or "deny" |
| 82 | + code : String -- decision reason code |
| 83 | + requiredCount : Nat |
| 84 | + missingCount : Nat |
| 85 | + policyEngine : String -- "builtin" or "external" |
| 86 | + |
| 87 | +-- --------------------------------------------------------------------------- |
| 88 | +-- C-ABI integer encoding — gate state |
| 89 | +-- --------------------------------------------------------------------------- |
| 90 | + |
| 91 | +export |
| 92 | +gateStateToInt : GateState -> Int |
| 93 | +gateStateToInt Idle = 0 |
| 94 | +gateStateToInt Checking = 1 |
| 95 | +gateStateToInt Allowed = 2 |
| 96 | +gateStateToInt Denied = 3 |
| 97 | +gateStateToInt Error = 4 |
| 98 | + |
| 99 | +export |
| 100 | +intToGateState : Int -> Maybe GateState |
| 101 | +intToGateState 0 = Just Idle |
| 102 | +intToGateState 1 = Just Checking |
| 103 | +intToGateState 2 = Just Allowed |
| 104 | +intToGateState 3 = Just Denied |
| 105 | +intToGateState 4 = Just Error |
| 106 | +intToGateState _ = Nothing |
| 107 | + |
| 108 | +-- --------------------------------------------------------------------------- |
| 109 | +-- C-ABI integer encoding — gate action |
| 110 | +-- --------------------------------------------------------------------------- |
| 111 | + |
| 112 | +export |
| 113 | +gateActionToInt : GateAction -> Int |
| 114 | +gateActionToInt AuthorizeStart = 0 |
| 115 | +gateActionToInt CheckStatus = 1 |
| 116 | +gateActionToInt ReloadSecrets = 2 |
| 117 | +gateActionToInt QueryHealth = 3 |
| 118 | + |
| 119 | +export |
| 120 | +intToGateAction : Int -> Maybe GateAction |
| 121 | +intToGateAction 0 = Just AuthorizeStart |
| 122 | +intToGateAction 1 = Just CheckStatus |
| 123 | +intToGateAction 2 = Just ReloadSecrets |
| 124 | +intToGateAction 3 = Just QueryHealth |
| 125 | +intToGateAction _ = Nothing |
| 126 | + |
| 127 | +-- --------------------------------------------------------------------------- |
| 128 | +-- C-ABI transition validator |
| 129 | +-- --------------------------------------------------------------------------- |
| 130 | + |
| 131 | +export |
| 132 | +rokur_mcp_can_transition : Int -> Int -> Int |
| 133 | +rokur_mcp_can_transition from to = |
| 134 | + case (intToGateState from, intToGateState to) of |
| 135 | + (Just Idle, Just Checking) => 1 -- BeginCheck |
| 136 | + (Just Checking, Just Allowed) => 1 -- Approve |
| 137 | + (Just Checking, Just Denied) => 1 -- Reject |
| 138 | + (Just Checking, Just Error) => 1 -- Fault |
| 139 | + (Just Allowed, Just Idle) => 1 -- ResetAllowed |
| 140 | + (Just Denied, Just Idle) => 1 -- ResetDenied |
| 141 | + (Just Error, Just Idle) => 1 -- ResetError |
| 142 | + _ => 0 |
| 143 | + |
| 144 | +-- --------------------------------------------------------------------------- |
| 145 | +-- MCP tool declarations |
| 146 | +-- --------------------------------------------------------------------------- |
| 147 | + |
| 148 | +public export |
| 149 | +data McpTool |
| 150 | + = ToolAuthorizeStart -- ^ rokur/authorize-start |
| 151 | + | ToolCheckStatus -- ^ rokur/status |
| 152 | + | ToolReloadSecrets -- ^ rokur/reload |
| 153 | + | ToolHealth -- ^ rokur/health |
| 154 | + |
| 155 | +export |
| 156 | +toolCount : Nat |
| 157 | +toolCount = 4 |
0 commit comments