Skip to content

Commit 2a7fcb1

Browse files
hyperpolymathclaudegithub-advanced-security[bot]
authored
feat(cartridges): add google-drive-mcp (18 tools, supersedes hosted connector) (#267)
## What Adds **google-drive-mcp** — a fuller, safer Google Drive cartridge than the 8-tool hosted claude.ai connector: **18 tools** over Drive API v3 (full query search incl. shared drives, export-aware reading, format export, metadata, folder/recents, permissions + sharing, copy, create-with-content, update, move, rename, reversible trash/restore, revisions, storage quota, shared-drive enumeration). ## Why it's "better than the one we have" | | hosted connector | this cartridge | |---|---|---| | Tools | ~8, read-mostly | 18 | | Search | basic | full `files.list` query language + shared drives + pagination | | Read | text | export-aware (Docs→Markdown, Sheets→CSV), size-capped | | Write | copy/create | + update, move, rename, sharing | | Delete | — | **reversible trash/restore only — permanent delete deliberately absent** | ## Safety by design No permanent delete. The most destructive operation is a reversible `Trash`. This is a **type-level guarantee** in the Idris2 ABI — `actionIsDestructive` is total with no `True` case — plus a `safety` block in `cartridge.json`. ## Verification (Zig 0.15.2 / Idris2 0.8) - **ffi**: builds + 16 unit tests pass - **adapter**: builds + tests pass — modernised the three-protocol adapter and its `build.zig` to Zig 0.15 (fixed a dangling `ffi` init call and pre-0.15 net/format APIs; the sibling `google-sheets` adapter still fails to build) - **abi**: `idris2 --check` passes, incl. a new **18-constructor round-trip proof** - `integration_test.sh` green (also fixed its ABI check to validate by file path rather than silently no-op) - `cartridge.json` / panels JSON valid; `mod.js` passes `node --check` ## Honest status `available: false` / `catalogued` — implemented, not yet wired to a live backend. Ports 9301–9303 (REST/gRPC/GraphQL), unique in the estate. Cartridge counts in README/package.json left untouched (owner-managed). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-authored-by: Copilot Autofix powered by AI <62310815+github-advanced-security[bot]@users.noreply.github.com>
1 parent 8490e68 commit 2a7fcb1

16 files changed

Lines changed: 2196 additions & 0 deletions

File tree

‎cartridges/google-drive-mcp/README.adoc‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
= google-drive-mcp
3+
:toc: preamble
4+
5+
Google Drive cartridge for BoJ — Drive API v3 over the ADR-0006 five-symbol
6+
cartridge ABI.
7+
8+
== Why this cartridge
9+
10+
Designed to *supersede the hosted claude.ai Google Drive connector* (8
11+
read-mostly tools) with a fuller, safer surface — 18 tools:
12+
13+
|===
14+
| Capability | Hosted connector | this cartridge
15+
16+
| Search | basic | full `files.list` query language, shared drives, `orderBy`, pagination
17+
| Read content | text | export-aware (Docs→Markdown/plain, Sheets→CSV), size-capped
18+
| Export formats | — | any export MIME (pdf, docx, md, csv…), base64 for binary
19+
| Metadata / recents / permissions | ✓ | ✓ (richer fields)
20+
| Folder listing | — | ✓
21+
| Copy / create | ✓ | ✓ (+ inline content upload, folders, native Google types)
22+
| Update content | — | ✓
23+
| Move / rename | — | ✓
24+
| Delete | — | *reversible* trash/restore ONLY — permanent delete deliberately absent
25+
| Sharing (grant) | — | ✓ (reader/commenter/writer; no owner transfer)
26+
| Revisions | — | ✓
27+
| Storage quota | — | ✓
28+
| Shared-drive enumeration | — | ✓
29+
|===
30+
31+
== Safety posture
32+
33+
* *No permanent delete.* `files.delete` is not implemented; `gdrive_trash` is
34+
always recoverable via `gdrive_restore` or the Drive bin. Fail-safe by design.
35+
* *No owner transfer.* `gdrive_share` grants reader/commenter/writer only.
36+
* Notification emails are opt-in (`send_notification`, default false).
37+
* Size caps on content reads (default 1 MiB, caller-adjustable).
38+
39+
== Auth
40+
41+
OAuth2 Bearer token in `GOOGLE_DRIVE_ACCESS_TOKEN` (vault-mcp provides
42+
zero-knowledge credential proxying in production). Scopes:
43+
`drive.readonly` for the read tools, `drive` for write/share.
44+
45+
== Layout
46+
47+
* `cartridge.json` — contract (18 tool schemas)
48+
* `mod.js` — implementation (Deno/Node; `handleTool`)
49+
* `abi/GoogleDriveMcp/SafeRegistry.idr` — Idris2 session state machine
50+
* `ffi/` — Zig five-symbol ABI (`boj_cartridge_*`)
51+
* `adapter/` — Zig three-protocol adapter (REST :9301, gRPC :9302, GraphQL :9303)
52+
* `panels/manifest.json` — PanLL panel manifest
53+
* `tests/integration_test.sh`, `benchmarks/quick-bench.sh`
54+
55+
== Status
56+
57+
`catalogued` / `available: false` — implementation complete, not yet wired to a
58+
live backend deployment. The registry stays honest until it is.

‎cartridges/google-drive-mcp/abi/GoogleDriveMcp/SafeRegistry.idr‎

Lines changed: 248 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,248 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- GoogleDriveMcp.SafeRegistry — Type-safe ABI for google-drive-mcp cartridge.
5+
--
6+
-- Dependent-type state machine governing Google Drive API v3 access.
7+
-- Encodes mandatory OAuth2 auth and the 18 Drive operations (search,
8+
-- export-aware read, metadata, folder/recents listing, permissions, sharing,
9+
-- copy, create, update, move, rename, REVERSIBLE trash/restore, revisions,
10+
-- storage quota, shared-drive enumeration) as compile-time invariants.
11+
--
12+
-- Safety invariant encoded here: there is NO permanent-delete action. The most
13+
-- destructive operation is `Trash`, which is reversible via `Restore`. This is
14+
-- a type-level guarantee, not a convention — `actionIsDestructive` is total and
15+
-- has no `True` case.
16+
-- REST API: https://www.googleapis.com/drive/v3
17+
-- No unsafe escape hatches.
18+
19+
module GoogleDriveMcp.SafeRegistry
20+
21+
%default total
22+
23+
-- ---------------------------------------------------------------------------
24+
-- Authentication state machine
25+
-- ---------------------------------------------------------------------------
26+
27+
||| Session state for Google Drive MCP operations.
28+
||| Disconnected: no OAuth2 token configured.
29+
||| Connected: authenticated and ready for API calls.
30+
||| RateLimited: rate limit hit; must wait before retrying.
31+
||| Error: unrecoverable error (expired token, permission denied).
32+
public export
33+
data SessionState
34+
= Disconnected
35+
| Connected
36+
| RateLimited
37+
| Error
38+
39+
||| Proof that a state transition is valid.
40+
||| Google Drive requires OAuth2 auth — no anonymous access.
41+
public export
42+
data ValidTransition : SessionState -> SessionState -> Type where
43+
Connect : ValidTransition Disconnected Connected
44+
Disconnect : ValidTransition Connected Disconnected
45+
Throttle : ValidTransition Connected RateLimited
46+
Unthrottle : ValidTransition RateLimited Connected
47+
ConnectError : ValidTransition Connected Error
48+
DisconnError : ValidTransition Disconnected Error
49+
RecoverConnect : ValidTransition Error Connected
50+
RecoverDisconn : ValidTransition Error Disconnected
51+
52+
-- ---------------------------------------------------------------------------
53+
-- C-ABI integer encoding
54+
-- ---------------------------------------------------------------------------
55+
56+
||| Encode session state as C-compatible integer for FFI boundary.
57+
export
58+
sessionStateToInt : SessionState -> Int
59+
sessionStateToInt Disconnected = 0
60+
sessionStateToInt Connected = 1
61+
sessionStateToInt RateLimited = 2
62+
sessionStateToInt Error = 3
63+
64+
||| Decode integer back to session state. Returns Nothing for out-of-range.
65+
export
66+
intToSessionState : Int -> Maybe SessionState
67+
intToSessionState 0 = Just Disconnected
68+
intToSessionState 1 = Just Connected
69+
intToSessionState 2 = Just RateLimited
70+
intToSessionState 3 = Just Error
71+
intToSessionState _ = Nothing
72+
73+
||| Check if a state transition is valid (C-ABI export).
74+
export
75+
google_drive_mcp_can_transition : Int -> Int -> Int
76+
google_drive_mcp_can_transition from to =
77+
case (intToSessionState from, intToSessionState to) of
78+
(Just Disconnected, Just Connected) => 1
79+
(Just Connected, Just Disconnected) => 1
80+
(Just Connected, Just RateLimited) => 1
81+
(Just RateLimited, Just Connected) => 1
82+
(Just Connected, Just Error) => 1
83+
(Just Disconnected, Just Error) => 1
84+
(Just Error, Just Connected) => 1
85+
(Just Error, Just Disconnected) => 1
86+
_ => 0
87+
88+
-- ---------------------------------------------------------------------------
89+
-- Google Drive actions (integer codes match google_drive_mcp_ffi.zig exactly)
90+
-- ---------------------------------------------------------------------------
91+
92+
||| Actions available through the Google Drive MCP cartridge.
93+
public export
94+
data GoogleDriveAction
95+
= Search
96+
| ReadContent
97+
| ExportFile
98+
| GetMetadata
99+
| ListRecent
100+
| ListFolder
101+
| GetPermissions
102+
| Share
103+
| Copy
104+
| CreateFile
105+
| UpdateContent
106+
| Move
107+
| Rename
108+
| Trash
109+
| Restore
110+
| ListRevisions
111+
| StorageQuota
112+
| ListSharedDrives
113+
114+
||| Every Drive action requires an authenticated (Connected) session.
115+
export
116+
actionRequiresAuth : GoogleDriveAction -> Bool
117+
actionRequiresAuth _ = True
118+
119+
||| Whether an action mutates Drive state (create/modify/move/share/trash).
120+
||| Read/list/export/metadata/quota/revisions are non-mutating.
121+
export
122+
actionIsMutating : GoogleDriveAction -> Bool
123+
actionIsMutating Share = True
124+
actionIsMutating Copy = True
125+
actionIsMutating CreateFile = True
126+
actionIsMutating UpdateContent = True
127+
actionIsMutating Move = True
128+
actionIsMutating Rename = True
129+
actionIsMutating Trash = True
130+
actionIsMutating Restore = True
131+
actionIsMutating _ = False
132+
133+
||| SAFETY INVARIANT: no action is permanently destructive. `Trash` is
134+
||| reversible via `Restore`; permanent `files.delete` is deliberately not part
135+
||| of this ABI. Total function with no `True` clause == compile-time proof that
136+
||| the cartridge cannot irreversibly destroy data.
137+
export
138+
actionIsDestructive : GoogleDriveAction -> Bool
139+
actionIsDestructive _ = False
140+
141+
||| Encode action as C-compatible integer for FFI.
142+
export
143+
actionToInt : GoogleDriveAction -> Int
144+
actionToInt Search = 0
145+
actionToInt ReadContent = 1
146+
actionToInt ExportFile = 2
147+
actionToInt GetMetadata = 3
148+
actionToInt ListRecent = 4
149+
actionToInt ListFolder = 5
150+
actionToInt GetPermissions = 6
151+
actionToInt Share = 7
152+
actionToInt Copy = 8
153+
actionToInt CreateFile = 9
154+
actionToInt UpdateContent = 10
155+
actionToInt Move = 11
156+
actionToInt Rename = 12
157+
actionToInt Trash = 13
158+
actionToInt Restore = 14
159+
actionToInt ListRevisions = 15
160+
actionToInt StorageQuota = 16
161+
actionToInt ListSharedDrives = 17
162+
163+
||| Decode integer to Google Drive action.
164+
export
165+
intToAction : Int -> Maybe GoogleDriveAction
166+
intToAction 0 = Just Search
167+
intToAction 1 = Just ReadContent
168+
intToAction 2 = Just ExportFile
169+
intToAction 3 = Just GetMetadata
170+
intToAction 4 = Just ListRecent
171+
intToAction 5 = Just ListFolder
172+
intToAction 6 = Just GetPermissions
173+
intToAction 7 = Just Share
174+
intToAction 8 = Just Copy
175+
intToAction 9 = Just CreateFile
176+
intToAction 10 = Just UpdateContent
177+
intToAction 11 = Just Move
178+
intToAction 12 = Just Rename
179+
intToAction 13 = Just Trash
180+
intToAction 14 = Just Restore
181+
intToAction 15 = Just ListRevisions
182+
intToAction 16 = Just StorageQuota
183+
intToAction 17 = Just ListSharedDrives
184+
intToAction _ = Nothing
185+
186+
||| Round-trip proof: decoding an encoded action recovers it. Machine-checked
187+
||| for all 18 constructors, guaranteeing the FFI integer map is injective.
188+
export
189+
actionRoundTrip : (a : GoogleDriveAction) -> intToAction (actionToInt a) = Just a
190+
actionRoundTrip Search = Refl
191+
actionRoundTrip ReadContent = Refl
192+
actionRoundTrip ExportFile = Refl
193+
actionRoundTrip GetMetadata = Refl
194+
actionRoundTrip ListRecent = Refl
195+
actionRoundTrip ListFolder = Refl
196+
actionRoundTrip GetPermissions = Refl
197+
actionRoundTrip Share = Refl
198+
actionRoundTrip Copy = Refl
199+
actionRoundTrip CreateFile = Refl
200+
actionRoundTrip UpdateContent = Refl
201+
actionRoundTrip Move = Refl
202+
actionRoundTrip Rename = Refl
203+
actionRoundTrip Trash = Refl
204+
actionRoundTrip Restore = Refl
205+
actionRoundTrip ListRevisions = Refl
206+
actionRoundTrip StorageQuota = Refl
207+
actionRoundTrip ListSharedDrives = Refl
208+
209+
-- ---------------------------------------------------------------------------
210+
-- MCP tool declarations
211+
-- ---------------------------------------------------------------------------
212+
213+
||| Tools exposed via MCP protocol for this cartridge (one per action).
214+
public export
215+
data McpTool
216+
= ToolSearch
217+
| ToolReadContent
218+
| ToolExport
219+
| ToolGetMetadata
220+
| ToolListRecent
221+
| ToolListFolder
222+
| ToolGetPermissions
223+
| ToolShare
224+
| ToolCopy
225+
| ToolCreateFile
226+
| ToolUpdateContent
227+
| ToolMove
228+
| ToolRename
229+
| ToolTrash
230+
| ToolRestore
231+
| ToolListRevisions
232+
| ToolStorageQuota
233+
| ToolListSharedDrives
234+
235+
||| Every tool requires a connected session (OAuth2-gated).
236+
export
237+
toolRequiresSession : McpTool -> Bool
238+
toolRequiresSession _ = True
239+
240+
||| Total tool count for this cartridge.
241+
export
242+
toolCount : Nat
243+
toolCount = 18
244+
245+
||| Total action count for this cartridge.
246+
export
247+
actionCount : Nat
248+
actionCount = 18

‎cartridges/google-drive-mcp/abi/README.adoc‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= google-drive-mcp / abi — Idris2 ABI layer
4+
:orientation: shallow
5+
6+
== Purpose
7+
8+
Cartridge-local protocol types for `google-drive-mcp`. Defines the data, tool, and
9+
transition vocabulary this cartridge speaks. Inherits safety lemmas and the
10+
matrix-cell identifier scheme from the trunk ABI at `src/abi/`.
11+
12+
== Files
13+
14+
1 Idris2 module(s), ~174 lines total. Lead module:
15+
`SafeRegistry.idr`.
16+
17+
No `.ipkg` — consumed directly by wider BoJ callers; type-checks inside the
18+
trunk `boj.ipkg`.
19+
20+
== Invariants
21+
22+
* `%default total` at every module top.
23+
* Zero `believe_me`, `assert_total`, `postulate`, `Admitted`, or
24+
`sorry` (the trunk holds the four declared `believe_me` sites; leaf
25+
cartridges carry none).
26+
27+
== Test/proof surface
28+
29+
Thin module(s), no inline tests. Proof surface = type-check success under the
30+
trunk `idris2 --check`.
31+
32+
== Read-first
33+
34+
. `SafeRegistry.idr` — cartridge-local data records and enums.
35+
. Trunk `src/abi/Boj/Catalogue.idr` for how this cell participates in the
36+
2D matrix.

‎cartridges/google-drive-mcp/adapter/README.adoc‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= google-sheets-mcp / adapter — protocol bridge
4+
:orientation: shallow
5+
6+
== Purpose
7+
8+
Exposes this cartridge's FFI over the wire protocols declared in
9+
`cartridge.json`. Dispatches tool invocations to the C-ABI exports at
10+
`../ffi/` and formats responses per protocol.
11+
12+
== Files
13+
14+
[cols="1,4"]
15+
|===
16+
| File | Role
17+
18+
| `build.zig` | Zig build graph — depends on the sibling `ffi` target.
19+
| `google_sheets_adapter.zig` | Protocol dispatch (204 lines). Tool catalogue matches `cartridge.json`.
20+
| `SIDELINED-*.v.adoc` | zig predecessor(s). Not built — zig banned 2026-04-10.
21+
|===
22+
23+
== Invariants
24+
25+
* **Stateless** — all state lives behind the FFI, never in the adapter.
26+
* **Response passthrough** — whatever the FFI returns goes back to the wire
27+
unmodified (no embellishment, no silent recovery).
28+
* **Cartridge.json is source of truth** for the tool catalogue; drift between
29+
adapter and manifest is a CI failure.
30+
31+
== Test/proof surface
32+
33+
No inline tests at the adapter layer — protocol routing is exercised by the
34+
trunk seam tests at `ffi/zig/src/seams.zig`.
35+
36+
== Read-first
37+
38+
. `google_sheets_adapter.zig` — dispatch function and per-protocol routers.
39+
. `../cartridge.json` — the tool manifest the dispatcher mirrors.

0 commit comments

Comments
 (0)