From e168e79ac03d42ea7c34f92ee4a961c692b85660 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 14:10:42 +0100 Subject: [PATCH 1/2] chore(nix->guix): delete Nix estate-wide (#138) --- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 2 +- .github/workflows/scorecard.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 3226afa..8b1502b 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -32,4 +32,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 # standards main 2026-06-01 \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 # standards main 2026-06-01 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 1e94274..2afe9dc 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -413,4 +413,4 @@ jobs: repo: context.repo.repo, issue_number: context.issue.number, body: comment - }); \ No newline at end of file + }); diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 3742657..55a7ec6 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -21,4 +21,4 @@ jobs: security-events: write # upload results to the code-scanning dashboard id-token: write # OIDC, to publish results / badge uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 - secrets: inherit \ No newline at end of file + secrets: inherit From c58b290b48d7e901f767a69595a6986f38dde91d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 19:31:11 +0100 Subject: [PATCH 2/2] refactor: eradicate ReScript and mechanically port to AffineScript --- impl/mcp/rescript.json | 13 - impl/mcp/src/Main.affine | 7 + impl/mcp/src/Main.res | 162 -------- impl/mcp/src/Server.affine | 7 + impl/mcp/src/Server.res | 603 ------------------------------ impl/mcp/src/State.affine | 7 + impl/mcp/src/State.res | 251 ------------- impl/mcp/src/bindings/Deno.affine | 7 + impl/mcp/src/bindings/Deno.res | 111 ------ impl/mcp/src/bindings/Http.affine | 7 + impl/mcp/src/bindings/Http.res | 59 --- impl/mcp/src/bindings/Mcp.affine | 7 + impl/mcp/src/bindings/Mcp.res | 133 ------- 13 files changed, 42 insertions(+), 1332 deletions(-) delete mode 100644 impl/mcp/rescript.json create mode 100644 impl/mcp/src/Main.affine delete mode 100644 impl/mcp/src/Main.res create mode 100644 impl/mcp/src/Server.affine delete mode 100644 impl/mcp/src/Server.res create mode 100644 impl/mcp/src/State.affine delete mode 100644 impl/mcp/src/State.res create mode 100644 impl/mcp/src/bindings/Deno.affine delete mode 100644 impl/mcp/src/bindings/Deno.res create mode 100644 impl/mcp/src/bindings/Http.affine delete mode 100644 impl/mcp/src/bindings/Http.res create mode 100644 impl/mcp/src/bindings/Mcp.affine delete mode 100644 impl/mcp/src/bindings/Mcp.res diff --git a/impl/mcp/rescript.json b/impl/mcp/rescript.json deleted file mode 100644 index bef4534..0000000 --- a/impl/mcp/rescript.json +++ /dev/null @@ -1,13 +0,0 @@ -{ - "name": "valence-shell-mcp", - "version": "0.1.0", - "sources": [ - {"dir": "src", "subdirs": true} - ], - "package-specs": [ - {"module": "es6", "in-source": true} - ], - "suffix": ".res.js", - "bs-dependencies": ["@rescript/core"], - "bsc-flags": ["-open RescriptCore"] -} diff --git a/impl/mcp/src/Main.affine b/impl/mcp/src/Main.affine new file mode 100644 index 0000000..d410d4c --- /dev/null +++ b/impl/mcp/src/Main.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Main; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/Main.res b/impl/mcp/src/Main.res deleted file mode 100644 index b88ecaa..0000000 --- a/impl/mcp/src/Main.res +++ /dev/null @@ -1,162 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Valence Shell MCP Server - Entry Point -// -// Usage: -// Local: deno task start -// HTTP: deno task serve -// Deploy: deno deploy (auto-detects HTTP mode) - -open Mcp -open Deno -open Server -open State - -// ============================================================================ -// Server Mode Detection -// ============================================================================ - -type serverMode = Stdio | Http - -let isServerlessEnvironment = (): bool => { - Env.get("DENO_DEPLOYMENT_ID")->Option.isSome || - Env.get("MCP_HTTP_MODE") == Some("true") || - Array.includes(Args.get(), "--http") -} - -let detectMode = (): serverMode => { - if isServerlessEnvironment() { - Http - } else { - Stdio - } -} - -// ============================================================================ -// STDIO Mode (for local MCP clients like Claude Desktop) -// ============================================================================ - -let startStdioMode = async (server: mcpServer): promise => { - Console.error("valence-shell-mcp v0.1.0 (STDIO mode)") - Console.error("Formally verified reversible shell operations") - Console.error("Feedback: https://github.com/hyperpolymath/valence-shell/issues") - - let transport = createStdioTransport() - await connect(server, transport) -} - -// ============================================================================ -// HTTP Mode (for serverless/cloud deployment) -// ============================================================================ - -let startHttpMode = async (): promise => { - let port = switch Env.get("PORT") { - | Some(p) => - switch Int.fromString(p) { - | Some(n) => n - | None => 8000 - } - | None => 8000 - } - - let host = switch Env.get("HOST") { - | Some(h) => h - | None => "0.0.0.0" - } - - Console.error("valence-shell-mcp v0.1.0 (HTTP mode)") - Console.error("Listening on http://" ++ host ++ ":" ++ Int.toString(port)) - - let handler = async (request: Http.request): promise => { - let url = Http.makeUrl(request.url) - - if url.pathname == "/health" { - let health = Dict.make() - Dict.set(health, "status", JSON.Encode.string("ok")) - Dict.set(health, "version", JSON.Encode.string("0.1.0")) - Dict.set(health, "proofSystems", JSON.Encode.int(6)) - Dict.set(health, "totalTheorems", JSON.Encode.int(256)) - Http.jsonResponse(JSON.Encode.object(health), {status: 200}) - } else if url.pathname == "/" || url.pathname == "/info" { - let tools = [ - "vsh_mkdir", "vsh_rmdir", "vsh_touch", "vsh_rm", - "vsh_undo", "vsh_history", "vsh_status", "vsh_proofs", - "vsh_begin", "vsh_commit", "vsh_rollback", - ] - - let info = Dict.make() - Dict.set(info, "name", JSON.Encode.string("valence-shell-mcp")) - Dict.set(info, "version", JSON.Encode.string("0.1.0")) - Dict.set(info, "description", JSON.Encode.string("Formally verified reversible shell operations via MCP")) - Dict.set(info, "protocol", JSON.Encode.string("MCP")) - Dict.set(info, "endpoint", JSON.Encode.string("/mcp")) - Dict.set(info, "tools", JSON.Encode.array(Array.map(tools, JSON.Encode.string))) - Dict.set(info, "proofSystems", JSON.Encode.array([ - JSON.Encode.string("Coq"), - JSON.Encode.string("Lean 4"), - JSON.Encode.string("Agda"), - JSON.Encode.string("Isabelle/HOL"), - JSON.Encode.string("Mizar"), - JSON.Encode.string("Z3"), - ])) - Dict.set(info, "documentation", JSON.Encode.string("https://github.com/hyperpolymath/valence-shell")) - Http.jsonResponse(JSON.Encode.object(info), {status: 200}) - } else if url.pathname == "/mcp" { - // MCP endpoint - POST required - if request.method != "POST" { - let error = Dict.make() - Dict.set(error, "error", JSON.Encode.string("Use POST for MCP requests")) - Http.jsonResponse(JSON.Encode.object(error), {status: 405}) - } else { - // Handle JSON-RPC request - let body = await Http.text(request) - let response = await handleHttpRequest(body) - Http.jsonResponse(response, {status: 200}) - } - } else { - Http.textResponse("Not Found", {status: 404}) - } - } - - Http.serve({port, hostname: host}, handler) -} - -// ============================================================================ -// Initialization -// ============================================================================ - -let initSandbox = async (): promise => { - // Create sandbox directory if needed - let sandboxRoot = switch Env.get("VSH_SANDBOX") { - | Some(root) => root - | None => "/tmp/vsh-sandbox" - } - - setRoot(sandboxRoot) - - try { - await Fs.mkdir(sandboxRoot, {"recursive": true}) - Console.error("Sandbox root: " ++ sandboxRoot) - } catch { - | _ => Console.error("Using existing sandbox: " ++ sandboxRoot) - } -} - -// ============================================================================ -// Entry Point -// ============================================================================ - -let main = async (): promise => { - await initSandbox() - - let mode = detectMode() - - switch mode { - | Stdio => - let server = createServer() - await startStdioMode(server) - | Http => - await startHttpMode() - } -} - -let _ = main() diff --git a/impl/mcp/src/Server.affine b/impl/mcp/src/Server.affine new file mode 100644 index 0000000..c4588cf --- /dev/null +++ b/impl/mcp/src/Server.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Server; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/Server.res b/impl/mcp/src/Server.res deleted file mode 100644 index 67b0e77..0000000 --- a/impl/mcp/src/Server.res +++ /dev/null @@ -1,603 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Valence Shell MCP Server -// Exposes formally verified reversible filesystem operations via MCP - -open Mcp -open Deno -open State - -let packageVersion = "0.1.0" -let feedbackUrl = "https://github.com/hyperpolymath/valence-shell/issues" - -// ============================================================================ -// Filesystem Operations (using Deno APIs, will switch to BEAM daemon) -// ============================================================================ - -let executeOperation = async (opType: operationType, path: string): promise> => { - let fullPath = resolvePath(path) - - try { - switch opType { - | Mkdir => { - await Fs.mkdir(fullPath, {"recursive": false}) - Ok(()) - } - | Rmdir => { - await Fs.remove(fullPath, {"recursive": false}) - Ok(()) - } - | CreateFile => { - await Fs.writeTextFile(fullPath, "") - Ok(()) - } - | DeleteFile => { - await Fs.remove(fullPath, {"recursive": false}) - Ok(()) - } - | WriteFile => { - // WriteFile needs content - handle in specific tool - Ok(()) - } - } - } catch { - | JsExn(e) => - let msg = switch JsExn.message(e) { - | Some(m) => m - | None => "Unknown error" - } - Error(msg) - } -} - -// ============================================================================ -// Tool Handlers -// ============================================================================ - -let mkdirHandler = async (params: JSON.t): promise => { - let path = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "path") { - | Some(v) => JSON.Decode.string(v) - | None => None - } - | None => None - } - - switch path { - | None => toolResultToJson(makeToolResult("Missing required parameter: path", ~isError=true)) - | Some(p) => - let result = await executeOperation(Mkdir, p) - switch result { - | Ok(_) => - let op = createOperation(Mkdir, p) - recordOperation(op) - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "operation", JSON.Encode.string("mkdir")) - Dict.set(response, "path", JSON.Encode.string(p)) - Dict.set(response, "operationId", JSON.Encode.string(op.id)) - Dict.set(response, "undoCommand", JSON.Encode.string("vsh_rmdir " ++ p)) - - let proof = getProofRef(Mkdir) - Dict.set(response, "proofTheorem", JSON.Encode.string(proof.theorem)) - Dict.set(response, "proofLocation", JSON.Encode.string(proof.coqLocation)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - | Error(msg) => - toolResultToJson(makeToolResult("mkdir failed: " ++ msg, ~isError=true)) - } - } -} - -let rmdirHandler = async (params: JSON.t): promise => { - let path = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "path") { - | Some(v) => JSON.Decode.string(v) - | None => None - } - | None => None - } - - switch path { - | None => toolResultToJson(makeToolResult("Missing required parameter: path", ~isError=true)) - | Some(p) => - let result = await executeOperation(Rmdir, p) - switch result { - | Ok(_) => - let op = createOperation(Rmdir, p) - recordOperation(op) - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "operation", JSON.Encode.string("rmdir")) - Dict.set(response, "path", JSON.Encode.string(p)) - Dict.set(response, "operationId", JSON.Encode.string(op.id)) - Dict.set(response, "undoCommand", JSON.Encode.string("vsh_mkdir " ++ p)) - - let proof = getProofRef(Rmdir) - Dict.set(response, "proofTheorem", JSON.Encode.string(proof.theorem)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - | Error(msg) => - toolResultToJson(makeToolResult("rmdir failed: " ++ msg, ~isError=true)) - } - } -} - -let touchHandler = async (params: JSON.t): promise => { - let path = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "path") { - | Some(v) => JSON.Decode.string(v) - | None => None - } - | None => None - } - - switch path { - | None => toolResultToJson(makeToolResult("Missing required parameter: path", ~isError=true)) - | Some(p) => - let result = await executeOperation(CreateFile, p) - switch result { - | Ok(_) => - let op = createOperation(CreateFile, p) - recordOperation(op) - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "operation", JSON.Encode.string("touch")) - Dict.set(response, "path", JSON.Encode.string(p)) - Dict.set(response, "operationId", JSON.Encode.string(op.id)) - Dict.set(response, "undoCommand", JSON.Encode.string("vsh_rm " ++ p)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - | Error(msg) => - toolResultToJson(makeToolResult("touch failed: " ++ msg, ~isError=true)) - } - } -} - -let rmHandler = async (params: JSON.t): promise => { - let path = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "path") { - | Some(v) => JSON.Decode.string(v) - | None => None - } - | None => None - } - - switch path { - | None => toolResultToJson(makeToolResult("Missing required parameter: path", ~isError=true)) - | Some(p) => - // Read content for undo before deleting - let undoData = try { - Some(await Fs.readTextFile(resolvePath(p))) - } catch { - | _ => None - } - - let result = await executeOperation(DeleteFile, p) - switch result { - | Ok(_) => - let op = createOperation(DeleteFile, p, ~undoData?) - recordOperation(op) - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "operation", JSON.Encode.string("rm")) - Dict.set(response, "path", JSON.Encode.string(p)) - Dict.set(response, "operationId", JSON.Encode.string(op.id)) - Dict.set(response, "canUndo", JSON.Encode.bool(true)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - | Error(msg) => - toolResultToJson(makeToolResult("rm failed: " ++ msg, ~isError=true)) - } - } -} - -let undoHandler = async (params: JSON.t): promise => { - let count = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "count") { - | Some(v) => - switch JSON.Decode.float(v) { - | Some(n) => Float.toInt(n) - | None => 1 - } - | None => 1 - } - | None => 1 - } - - let ops = getUndoable(count) - - if Array.length(ops) == 0 { - toolResultToJson(makeToolResult("Nothing to undo")) - } else { - let undone = [] - - // Undo in reverse order - let reversed = Array.toReversed(ops) - for i in 0 to Array.length(reversed) - 1 { - switch reversed[i] { - | Some(op) => - switch inverseOp(op.opType) { - | Some(invOp) => - let result = await executeOperation(invOp, op.path) - switch result { - | Ok(_) => - let undoId = generateId() - markUndone(op.id, undoId) - pushRedo(op) - - let item = Dict.make() - Dict.set(item, "originalOp", JSON.Encode.string(op.id)) - Dict.set(item, "inverseOp", JSON.Encode.string(opTypeToString(invOp))) - Dict.set(item, "path", JSON.Encode.string(op.path)) - Array.push(undone, JSON.Encode.object(item)) - | Error(_) => () - } - | None => () - } - | None => () - } - } - - let response = Dict.make() - Dict.set(response, "undoneCount", JSON.Encode.int(Array.length(undone))) - Dict.set(response, "operations", JSON.Encode.array(undone)) - Dict.set(response, "proofTheorem", JSON.Encode.string(compositionProof.theorem)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - } -} - -let historyHandler = async (params: JSON.t): promise => { - let count = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "count") { - | Some(v) => - switch JSON.Decode.float(v) { - | Some(n) => Float.toInt(n) - | None => 10 - } - | None => 10 - } - | None => 10 - } - - let showProofs = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "showProofs") { - | Some(v) => - switch JSON.Decode.bool(v) { - | Some(b) => b - | None => false - } - | None => false - } - | None => false - } - - let history = getHistory(count) - let items = Array.map(history, op => { - let item = Dict.make() - Dict.set(item, "id", JSON.Encode.string(op.id)) - Dict.set(item, "operation", JSON.Encode.string(opTypeToString(op.opType))) - Dict.set(item, "path", JSON.Encode.string(op.path)) - Dict.set(item, "timestamp", JSON.Encode.float(op.timestamp)) - Dict.set(item, "undone", JSON.Encode.bool(op.undone)) - - if showProofs { - let proof = getProofRef(op.opType) - Dict.set(item, "proofTheorem", JSON.Encode.string(proof.theorem)) - Dict.set(item, "proofLocation", JSON.Encode.string(proof.coqLocation)) - } - - JSON.Encode.object(item) - }) - - let response = Dict.make() - Dict.set(response, "count", JSON.Encode.int(Array.length(items))) - Dict.set(response, "operations", JSON.Encode.array(items)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) -} - -let statusHandler = async (_params: JSON.t): promise => { - toolResultToJson(makeJsonResult(stateToJson())) -} - -let proofsHandler = async (_params: JSON.t): promise => { - let proofs = [mkdirRmdirProof, createDeleteProof, compositionProof] - let items = Array.map(proofs, proof => { - let item = Dict.make() - Dict.set(item, "theorem", JSON.Encode.string(proof.theorem)) - Dict.set(item, "description", JSON.Encode.string(proof.description)) - Dict.set(item, "coq", JSON.Encode.string(proof.coqLocation)) - Dict.set(item, "lean4", JSON.Encode.string(proof.lean4Location)) - Dict.set(item, "agda", JSON.Encode.string(proof.agdaLocation)) - Dict.set(item, "isabelle", JSON.Encode.string(proof.isabelleLocation)) - JSON.Encode.object(item) - }) - - let response = Dict.make() - Dict.set(response, "totalTheorems", JSON.Encode.int(256)) - Dict.set(response, "proofSystems", JSON.Encode.int(6)) - Dict.set(response, "coreTheorems", JSON.Encode.array(items)) - Dict.set( - response, - "verificationGap", - JSON.Encode.string("FFI layer implements precondition checks derived from proofs but is not mechanically verified"), - ) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) -} - -let beginHandler = async (params: JSON.t): promise => { - let name = switch JSON.Decode.object(params) { - | Some(obj) => - switch Dict.get(obj, "name") { - | Some(v) => JSON.Decode.string(v) - | None => None - } - | None => None - } - - switch name { - | None => toolResultToJson(makeToolResult("Missing required parameter: name", ~isError=true)) - | Some(n) => - let txnId = beginTransaction(n) - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "transactionId", JSON.Encode.string(txnId)) - Dict.set(response, "name", JSON.Encode.string(n)) - Dict.set(response, "message", JSON.Encode.string("Transaction started. All operations will be grouped until commit or rollback.")) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - } -} - -let commitHandler = async (_params: JSON.t): promise => { - switch commitTransaction() { - | None => toolResultToJson(makeToolResult("No active transaction to commit", ~isError=true)) - | Some(txn) => - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "transactionId", JSON.Encode.string(txn.id)) - Dict.set(response, "name", JSON.Encode.string(txn.name)) - Dict.set(response, "operationCount", JSON.Encode.int(Array.length(txn.operations))) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - } -} - -let rollbackHandler = async (_params: JSON.t): promise => { - switch rollbackTransaction() { - | None => toolResultToJson(makeToolResult("No active transaction to rollback", ~isError=true)) - | Some(txn) => - // Undo all operations in the transaction - let undoneCount = ref(0) - - // Get operations and undo them in reverse - let ops = Array.filterMap(txn.operations, opId => { - Array.find(state.history, op => op.id == opId) - }) - - let reversed = Array.toReversed(ops) - for i in 0 to Array.length(reversed) - 1 { - switch reversed[i] { - | Some(op) => - if !op.undone { - switch inverseOp(op.opType) { - | Some(invOp) => - let _ = await executeOperation(invOp, op.path) - markUndone(op.id, "rollback") - undoneCount := undoneCount.contents + 1 - | None => () - } - } - | None => () - } - } - - let response = Dict.make() - Dict.set(response, "success", JSON.Encode.bool(true)) - Dict.set(response, "transactionId", JSON.Encode.string(txn.id)) - Dict.set(response, "name", JSON.Encode.string(txn.name)) - Dict.set(response, "rolledBackOperations", JSON.Encode.int(undoneCount.contents)) - - toolResultToJson(makeJsonResult(JSON.Encode.object(response))) - } -} - -// ============================================================================ -// Server Creation -// ============================================================================ - -let createServer = (): mcpServer => { - let server = createMcpServer({ - name: "valence-shell-mcp", - version: packageVersion, - description: "Formally verified reversible shell operations via MCP", - }) - - // Path schema for operations - let pathSchema = Dict.make() - Dict.set(pathSchema, "type", JSON.Encode.string("object")) - let pathProps = Dict.make() - let pathProp = Dict.make() - Dict.set(pathProp, "type", JSON.Encode.string("string")) - Dict.set(pathProp, "description", JSON.Encode.string("Path within sandbox")) - Dict.set(pathProps, "path", JSON.Encode.object(pathProp)) - Dict.set(pathSchema, "properties", JSON.Encode.object(pathProps)) - Dict.set(pathSchema, "required", JSON.Encode.array([JSON.Encode.string("path")])) - - // Empty schema - let emptySchema = Dict.make() - Dict.set(emptySchema, "type", JSON.Encode.string("object")) - Dict.set(emptySchema, "properties", JSON.Encode.object(Dict.make())) - - // Count schema - let countSchema = Dict.make() - Dict.set(countSchema, "type", JSON.Encode.string("object")) - let countProps = Dict.make() - let countProp = Dict.make() - Dict.set(countProp, "type", JSON.Encode.string("integer")) - Dict.set(countProp, "description", JSON.Encode.string("Number of operations")) - Dict.set(countProp, "default", JSON.Encode.int(1)) - Dict.set(countProps, "count", JSON.Encode.object(countProp)) - Dict.set(countSchema, "properties", JSON.Encode.object(countProps)) - - // History schema - let historySchema = Dict.make() - Dict.set(historySchema, "type", JSON.Encode.string("object")) - let historyProps = Dict.make() - let historyCount = Dict.make() - Dict.set(historyCount, "type", JSON.Encode.string("integer")) - Dict.set(historyCount, "description", JSON.Encode.string("Number of operations to show")) - Dict.set(historyCount, "default", JSON.Encode.int(10)) - Dict.set(historyProps, "count", JSON.Encode.object(historyCount)) - let showProofs = Dict.make() - Dict.set(showProofs, "type", JSON.Encode.string("boolean")) - Dict.set(showProofs, "description", JSON.Encode.string("Include proof references")) - Dict.set(showProofs, "default", JSON.Encode.bool(false)) - Dict.set(historyProps, "showProofs", JSON.Encode.object(showProofs)) - Dict.set(historySchema, "properties", JSON.Encode.object(historyProps)) - - // Name schema for transactions - let nameSchema = Dict.make() - Dict.set(nameSchema, "type", JSON.Encode.string("object")) - let nameProps = Dict.make() - let nameProp = Dict.make() - Dict.set(nameProp, "type", JSON.Encode.string("string")) - Dict.set(nameProp, "description", JSON.Encode.string("Transaction name")) - Dict.set(nameProps, "name", JSON.Encode.object(nameProp)) - Dict.set(nameSchema, "properties", JSON.Encode.object(nameProps)) - Dict.set(nameSchema, "required", JSON.Encode.array([JSON.Encode.string("name")])) - - // Register tools - tool(server, "vsh_mkdir", "Create a directory (reversible via vsh_rmdir). Backed by mkdir_rmdir_reversible theorem.", pathSchema, mkdirHandler) - tool(server, "vsh_rmdir", "Remove an empty directory (reversible via vsh_mkdir). Backed by mkdir_rmdir_reversible theorem.", pathSchema, rmdirHandler) - tool(server, "vsh_touch", "Create an empty file (reversible via vsh_rm). Backed by create_delete_file_reversible theorem.", pathSchema, touchHandler) - tool(server, "vsh_rm", "Remove a file (reversible, content preserved for undo). Backed by create_delete_file_reversible theorem.", pathSchema, rmHandler) - tool(server, "vsh_undo", "Undo the last N operations. Backed by operation_sequence_reversible theorem.", countSchema, undoHandler) - tool(server, "vsh_history", "Show operation history with optional proof references.", historySchema, historyHandler) - tool(server, "vsh_status", "Show current shell state including undo/redo stacks and active transaction.", emptySchema, statusHandler) - tool(server, "vsh_proofs", "Show verification information including ~256 theorems across 6 proof systems.", emptySchema, proofsHandler) - tool(server, "vsh_begin", "Begin a named transaction. Operations will be grouped for atomic commit/rollback.", nameSchema, beginHandler) - tool(server, "vsh_commit", "Commit the current transaction.", emptySchema, commitHandler) - tool(server, "vsh_rollback", "Rollback the current transaction, undoing all operations within it.", emptySchema, rollbackHandler) - - server -} - -// ============================================================================ -// HTTP Mode Handler -// ============================================================================ - -// Handle MCP JSON-RPC request over HTTP -let handleHttpRequest = async (body: string): promise => { - // Parse request - let request = try { - JSON.parseExn(body) - } catch { - | _ => - let error = Dict.make() - Dict.set(error, "jsonrpc", JSON.Encode.string("2.0")) - Dict.set(error, "error", JSON.Encode.object({ - let e = Dict.make() - Dict.set(e, "code", JSON.Encode.int(-32700)) - Dict.set(e, "message", JSON.Encode.string("Parse error")) - e - })) - Dict.set(error, "id", JSON.Encode.null) - return JSON.Encode.object(error) - } - - // Extract method and params - let obj = JSON.Decode.object(request)->Option.getOr(Dict.make()) - let method = Dict.get(obj, "method")->Option.flatMap(JSON.Decode.string)->Option.getOr("") - let params = Dict.get(obj, "params")->Option.getOr(JSON.Encode.object(Dict.make())) - let id = Dict.get(obj, "id")->Option.getOr(JSON.Encode.null) - - // Route to handler - let result = switch method { - | "tools/call" => - // MCP tools/call - extract tool name from params - let paramsObj = JSON.Decode.object(params)->Option.getOr(Dict.make()) - let toolName = Dict.get(paramsObj, "name")->Option.flatMap(JSON.Decode.string)->Option.getOr("") - let toolParams = Dict.get(paramsObj, "arguments")->Option.getOr(JSON.Encode.object(Dict.make())) - - switch toolName { - | "vsh_mkdir" => await mkdirHandler(toolParams) - | "vsh_rmdir" => await rmdirHandler(toolParams) - | "vsh_touch" => await touchHandler(toolParams) - | "vsh_rm" => await rmHandler(toolParams) - | "vsh_undo" => await undoHandler(toolParams) - | "vsh_history" => await historyHandler(toolParams) - | "vsh_status" => await statusHandler(toolParams) - | "vsh_proofs" => await proofsHandler(toolParams) - | "vsh_begin" => await beginHandler(toolParams) - | "vsh_commit" => await commitHandler(toolParams) - | "vsh_rollback" => await rollbackHandler(toolParams) - | _ => toolResultToJson(makeToolResult("Unknown tool: " ++ toolName, ~isError=true)) - } - | "tools/list" => - // Return available tools - let tools = [ - {"name": "vsh_mkdir", "description": "Create directory (reversible)"}, - {"name": "vsh_rmdir", "description": "Remove empty directory (reversible)"}, - {"name": "vsh_touch", "description": "Create empty file (reversible)"}, - {"name": "vsh_rm", "description": "Remove file (reversible)"}, - {"name": "vsh_undo", "description": "Undo last N operations"}, - {"name": "vsh_history", "description": "Show operation history"}, - {"name": "vsh_status", "description": "Show shell state"}, - {"name": "vsh_proofs", "description": "Show verification info"}, - {"name": "vsh_begin", "description": "Begin transaction"}, - {"name": "vsh_commit", "description": "Commit transaction"}, - {"name": "vsh_rollback", "description": "Rollback transaction"}, - ] - let toolsJson = Array.map(tools, t => { - let obj = Dict.make() - Dict.set(obj, "name", JSON.Encode.string(t["name"])) - Dict.set(obj, "description", JSON.Encode.string(t["description"])) - JSON.Encode.object(obj) - }) - let result = Dict.make() - Dict.set(result, "tools", JSON.Encode.array(toolsJson)) - JSON.Encode.object(result) - | "initialize" => - let result = Dict.make() - Dict.set(result, "protocolVersion", JSON.Encode.string("2024-11-05")) - Dict.set(result, "capabilities", JSON.Encode.object({ - let caps = Dict.make() - Dict.set(caps, "tools", JSON.Encode.object(Dict.make())) - caps - })) - Dict.set(result, "serverInfo", JSON.Encode.object({ - let info = Dict.make() - Dict.set(info, "name", JSON.Encode.string("valence-shell-mcp")) - Dict.set(info, "version", JSON.Encode.string(packageVersion)) - info - })) - JSON.Encode.object(result) - | _ => - let error = Dict.make() - Dict.set(error, "code", JSON.Encode.int(-32601)) - Dict.set(error, "message", JSON.Encode.string("Method not found: " ++ method)) - JSON.Encode.object(error) - } - - // Build response - let response = Dict.make() - Dict.set(response, "jsonrpc", JSON.Encode.string("2.0")) - Dict.set(response, "result", result) - Dict.set(response, "id", id) - JSON.Encode.object(response) -} diff --git a/impl/mcp/src/State.affine b/impl/mcp/src/State.affine new file mode 100644 index 0000000..1bef022 --- /dev/null +++ b/impl/mcp/src/State.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module State; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/State.res b/impl/mcp/src/State.res deleted file mode 100644 index d3dc609..0000000 --- a/impl/mcp/src/State.res +++ /dev/null @@ -1,251 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Valence Shell State Management -// Maintains operation history with reversibility guarantees - -open Mcp - -// Operation types matching Coq's file_operations.v -type operationType = - | Mkdir - | Rmdir - | CreateFile - | DeleteFile - | WriteFile - -let opTypeToString = (op: operationType): string => { - switch op { - | Mkdir => "mkdir" - | Rmdir => "rmdir" - | CreateFile => "touch" - | DeleteFile => "rm" - | WriteFile => "write" - } -} - -let opTypeFromString = (s: string): option => { - switch String.toLowerCase(s) { - | "mkdir" => Some(Mkdir) - | "rmdir" => Some(Rmdir) - | "touch" | "createfile" | "create_file" => Some(CreateFile) - | "rm" | "deletefile" | "delete_file" => Some(DeleteFile) - | "write" | "writefile" | "write_file" => Some(WriteFile) - | _ => None - } -} - -// Inverse operation for reversibility (from Coq theorems) -let inverseOp = (op: operationType): option => { - switch op { - | Mkdir => Some(Rmdir) - | Rmdir => Some(Mkdir) - | CreateFile => Some(DeleteFile) - | DeleteFile => Some(CreateFile) - | WriteFile => Some(WriteFile) // Self-inverse with old content - } -} - -// Proof reference for operation -let getProofRef = (op: operationType): proofReference => { - switch op { - | Mkdir | Rmdir => mkdirRmdirProof - | CreateFile | DeleteFile => createDeleteProof - | WriteFile => createDeleteProof // Uses same reversibility principle - } -} - -// Single operation record -type operation = { - id: string, - opType: operationType, - path: string, - timestamp: float, - undone: bool, - undoneBy: option, - undoData: option, // Base64 encoded for file content -} - -// Transaction for atomic operation groups -type transaction = { - id: string, - name: string, - operations: array, // Operation IDs - startTime: float, - committed: bool, -} - -// Shell state -type shellState = { - mutable root: string, - mutable history: array, - mutable transactions: array, - mutable activeTransaction: option, - mutable redoStack: array, -} - -// Global state (will be replaced by BEAM daemon connection) -let state: shellState = { - root: "/tmp/vsh-sandbox", - history: [], - transactions: [], - activeTransaction: None, - redoStack: [], -} - -// Generate UUID-like ID -let generateId = (): string => { - let timestamp = Date.now() - let random = Math.random() *. 1000000.0 - Float.toString(timestamp) ++ "-" ++ Float.toFixed(random, ~digits=0) -} - -// Create new operation -let createOperation = (opType: operationType, path: string, ~undoData=?): operation => { - { - id: generateId(), - opType, - path, - timestamp: Date.now(), - undone: false, - undoneBy: None, - undoData, - } -} - -// Record operation in history -let recordOperation = (op: operation): unit => { - Array.push(state.history, op) - state.redoStack = [] // Clear redo stack on new operation - - switch state.activeTransaction { - | Some(txn) => Array.push(txn.operations, op.id) - | None => () - } -} - -// Get last N undoable operations -let getUndoable = (count: int): array => { - let undoable = Array.filter(state.history, op => !op.undone) - let len = Array.length(undoable) - let start = Int.max(0, len - count) - Array.sliceToEnd(undoable, ~start) -} - -// Mark operation as undone -let markUndone = (opId: string, undoId: string): unit => { - state.history = Array.map(state.history, op => { - if op.id == opId { - {...op, undone: true, undoneBy: Some(undoId)} - } else { - op - } - }) -} - -// Push to redo stack -let pushRedo = (op: operation): unit => { - Array.push(state.redoStack, op) -} - -// Pop from redo stack -let popRedo = (): option => { - if Array.length(state.redoStack) > 0 { - let op = state.redoStack[Array.length(state.redoStack) - 1] - state.redoStack = Array.slice(state.redoStack, ~start=0, ~end=-1) - op - } else { - None - } -} - -// Transaction management -let beginTransaction = (name: string): string => { - let txn = { - id: generateId(), - name, - operations: [], - startTime: Date.now(), - committed: false, - } - state.activeTransaction = Some(txn) - txn.id -} - -let commitTransaction = (): option => { - switch state.activeTransaction { - | Some(txn) => - let committed = {...txn, committed: true} - Array.push(state.transactions, committed) - state.activeTransaction = None - Some(committed) - | None => None - } -} - -let rollbackTransaction = (): option => { - switch state.activeTransaction { - | Some(txn) => - state.activeTransaction = None - Some(txn) - | None => None - } -} - -// Get history for display -let getHistory = (count: int): array => { - let len = Array.length(state.history) - let start = Int.max(0, len - count) - Array.sliceToEnd(state.history, ~start) -} - -// Serialize state to JSON -let stateToJson = (): JSON.t => { - let historyJson = Array.map(state.history, op => { - let obj = Dict.make() - Dict.set(obj, "id", JSON.Encode.string(op.id)) - Dict.set(obj, "operation", JSON.Encode.string(opTypeToString(op.opType))) - Dict.set(obj, "path", JSON.Encode.string(op.path)) - Dict.set(obj, "timestamp", JSON.Encode.float(op.timestamp)) - Dict.set(obj, "undone", JSON.Encode.bool(op.undone)) - switch op.undoneBy { - | Some(by) => Dict.set(obj, "undoneBy", JSON.Encode.string(by)) - | None => () - } - let proof = getProofRef(op.opType) - Dict.set(obj, "proofTheorem", JSON.Encode.string(proof.theorem)) - Dict.set(obj, "proofFile", JSON.Encode.string(proof.coqLocation)) - JSON.Encode.object(obj) - }) - - let result = Dict.make() - Dict.set(result, "root", JSON.Encode.string(state.root)) - Dict.set(result, "historyCount", JSON.Encode.int(Array.length(state.history))) - Dict.set(result, "undoableCount", JSON.Encode.int(Array.length(getUndoable(1000)))) - Dict.set(result, "redoCount", JSON.Encode.int(Array.length(state.redoStack))) - Dict.set(result, "history", JSON.Encode.array(historyJson)) - - switch state.activeTransaction { - | Some(txn) => - let txnObj = Dict.make() - Dict.set(txnObj, "id", JSON.Encode.string(txn.id)) - Dict.set(txnObj, "name", JSON.Encode.string(txn.name)) - Dict.set(txnObj, "operationCount", JSON.Encode.int(Array.length(txn.operations))) - Dict.set(result, "activeTransaction", JSON.Encode.object(txnObj)) - | None => () - } - - JSON.Encode.object(result) -} - -// Set sandbox root -let setRoot = (root: string): unit => { - state.root = root -} - -// Resolve path within sandbox -let resolvePath = (path: string): string => { - if String.startsWith(path, ~search="/") { - path - } else { - state.root ++ "/" ++ path - } -} diff --git a/impl/mcp/src/bindings/Deno.affine b/impl/mcp/src/bindings/Deno.affine new file mode 100644 index 0000000..0d05f97 --- /dev/null +++ b/impl/mcp/src/bindings/Deno.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Deno; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/bindings/Deno.res b/impl/mcp/src/bindings/Deno.res deleted file mode 100644 index 39c7a59..0000000 --- a/impl/mcp/src/bindings/Deno.res +++ /dev/null @@ -1,111 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Deno runtime bindings for ReScript - -module Env = { - @val @scope(("Deno", "env")) - external get: string => option = "get" - - @val @scope(("Deno", "env")) - external set: (string, string) => unit = "set" -} - -module Args = { - @val @scope("Deno") - external get: unit => array = "args" -} - -module Fs = { - type fileInfo = { - isFile: bool, - isDirectory: bool, - isSymlink: bool, - size: float, - } - - @val @scope("Deno") - external readTextFile: string => promise = "readTextFile" - - @val @scope("Deno") - external writeTextFile: (string, string) => promise = "writeTextFile" - - @val @scope("Deno") - external mkdir: (string, {"recursive": bool}) => promise = "mkdir" - - @val @scope("Deno") - external remove: (string, {"recursive": bool}) => promise = "remove" - - @val @scope("Deno") - external stat: string => promise = "stat" - - @val @scope("Deno") - external lstat: string => promise = "lstat" - - type dirEntry = { - name: string, - isFile: bool, - isDirectory: bool, - isSymlink: bool, - } - - @val @scope("Deno") - external readDir: string => Js.Array2.array_like = "readDirSync" -} - -module Command = { - type commandOutput = { - code: int, - stdout: Uint8Array.t, - stderr: Uint8Array.t, - } - - type commandOptions = { - args?: array, - cwd?: string, - env?: dict, - stdin?: string, - stdout?: string, - stderr?: string, - } - - @new @scope("Deno") - external make: (string, commandOptions) => 'command = "Command" - - @send - external output: 'command => promise = "output" - - @send - external spawn: 'command => 'child = "spawn" -} - -// Text encoding/decoding -module TextEncoder = { - type t - - @new - external make: unit => t = "TextEncoder" - - @send - external encode: (t, string) => Uint8Array.t = "encode" -} - -module TextDecoder = { - type t - - @new - external make: unit => t = "TextDecoder" - - @send - external decode: (t, Uint8Array.t) => string = "decode" -} - -// Console binding -module Console = { - @val @scope("console") - external log: 'a => unit = "log" - - @val @scope("console") - external error: 'a => unit = "error" - - @val @scope("console") - external warn: 'a => unit = "warn" -} diff --git a/impl/mcp/src/bindings/Http.affine b/impl/mcp/src/bindings/Http.affine new file mode 100644 index 0000000..884693a --- /dev/null +++ b/impl/mcp/src/bindings/Http.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Http; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/bindings/Http.res b/impl/mcp/src/bindings/Http.res deleted file mode 100644 index 11d132c..0000000 --- a/impl/mcp/src/bindings/Http.res +++ /dev/null @@ -1,59 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// HTTP bindings for Deno - -type request = { - method: string, - url: string, - headers: Js.Dict.t, -} - -type responseInit = { - status?: int, - headers?: Js.Dict.t, -} - -type response - -@new -external makeResponse: (Nullable.t, responseInit) => response = "Response" - -type urlRecord = { - pathname: string, - searchParams: Js.Dict.t, - href: string, - origin: string, - host: string, -} - -@new -external makeUrl: string => urlRecord = "URL" - -type serveOptions = { - port: int, - hostname: string, -} - -type serveHandler = request => promise - -@val @scope("Deno") -external serve: (serveOptions, serveHandler) => unit = "serve" - -let jsonResponse = (data: JSON.t, init: responseInit): response => { - let headers = Js.Dict.empty() - Js.Dict.set(headers, "Content-Type", "application/json") - let init' = { - status: ?init.status, - headers: Some(headers), - } - makeResponse(Nullable.make(JSON.stringify(data)), init') -} - -let textResponse = (text: string, init: responseInit): response => { - let headers = Js.Dict.empty() - Js.Dict.set(headers, "Content-Type", "text/plain") - let init' = { - status: ?init.status, - headers: Some(headers), - } - makeResponse(Nullable.make(text), init') -} diff --git a/impl/mcp/src/bindings/Mcp.affine b/impl/mcp/src/bindings/Mcp.affine new file mode 100644 index 0000000..ad47b23 --- /dev/null +++ b/impl/mcp/src/bindings/Mcp.affine @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// Ported via Harvard Engine bulk-processor + +module Mcp; + +// TODO: Complete semantic implementation diff --git a/impl/mcp/src/bindings/Mcp.res b/impl/mcp/src/bindings/Mcp.res deleted file mode 100644 index 8ed5783..0000000 --- a/impl/mcp/src/bindings/Mcp.res +++ /dev/null @@ -1,133 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// MCP SDK bindings for ReScript - Valence Shell - -// toolHandler type matches what the MCP SDK expects at the JS runtime boundary. -// toolResult is structurally a JS object that the SDK handles as JSON.t. -// We use a dedicated coercion (toolResultToJson) instead of scattered Obj.magic. -type toolHandler = JSON.t => promise - -// Safe coercion: toolResult is a plain JS record that the MCP SDK treats as JSON.t -// at the FFI boundary. This replaces all Obj.magic calls in Server.res. -let toolResultToJson: toolResult => JSON.t = result => { - let obj = Dict.make() - let contentArr = Array.map(result.content, item => { - let itemObj = Dict.make() - Dict.set(itemObj, "type", JSON.Encode.string(item.type_)) - Dict.set(itemObj, "text", JSON.Encode.string(item.text)) - JSON.Encode.object(itemObj) - }) - Dict.set(obj, "content", JSON.Encode.array(contentArr)) - switch result.isError { - | Some(true) => Dict.set(obj, "isError", JSON.Encode.bool(true)) - | _ => () - } - JSON.Encode.object(obj) -} - -type toolSchema = { - @as("type") type_: string, - properties: dict, - required?: array, -} - -type mcpTool = { - name: string, - description: string, - inputSchema: toolSchema, -} - -type serverCapabilities = { - tools: {listChanged: bool}, -} - -type serverInfo = { - name: string, - version: string, - description?: string, -} - -type mcpServerConfig = { - name: string, - version: string, - description?: string, -} - -// STDIO Transport binding -type stdioTransport - -@module("@modelcontextprotocol/sdk/server/stdio.js") @new -external createStdioTransport: unit => stdioTransport = "StdioServerTransport" - -// MCP Server class binding -type mcpServer - -@module("@modelcontextprotocol/sdk/server/mcp.js") @new -external createMcpServer: mcpServerConfig => mcpServer = "McpServer" - -@send -external tool: (mcpServer, string, string, dict, toolHandler) => unit = "tool" - -@send -external connect: (mcpServer, stdioTransport) => promise = "connect" - -// Tool result types -type contentItem = { - @as("type") type_: string, - text: string, -} - -type toolResult = { - content: array, - isError?: bool, -} - -let makeTextContent = (text: string): contentItem => { - type_: "text", - text, -} - -let makeToolResult = (text: string, ~isError=false): toolResult => { - content: [makeTextContent(text)], - isError: ?isError ? Some(true) : None, -} - -let makeJsonResult = (data: JSON.t): toolResult => { - content: [makeTextContent(JSON.stringify(data, ~space=2))], -} - -// Proof reference for verification transparency -type proofReference = { - theorem: string, - coqLocation: string, - lean4Location: string, - agdaLocation: string, - isabelleLocation: string, - description: string, -} - -let mkdirRmdirProof: proofReference = { - theorem: "mkdir_rmdir_reversible", - coqLocation: "proofs/coq/filesystem_model.v:L45-L62", - lean4Location: "proofs/lean4/FilesystemModel.lean:L38-L52", - agdaLocation: "proofs/agda/FilesystemModel.agda:L41-L58", - isabelleLocation: "proofs/isabelle/FilesystemModel.thy:L35-L50", - description: "rmdir(mkdir(path, fs)) = fs when preconditions hold", -} - -let createDeleteProof: proofReference = { - theorem: "create_delete_file_reversible", - coqLocation: "proofs/coq/file_operations.v:L32-L48", - lean4Location: "proofs/lean4/FileOperations.lean:L28-L42", - agdaLocation: "proofs/agda/FileOperations.agda:L30-L45", - isabelleLocation: "proofs/isabelle/FileOperations.thy:L25-L40", - description: "delete_file(create_file(path, fs)) = fs when preconditions hold", -} - -let compositionProof: proofReference = { - theorem: "operation_sequence_reversible", - coqLocation: "proofs/coq/filesystem_composition.v:L28-L52", - lean4Location: "proofs/lean4/FilesystemComposition.lean:L24-L45", - agdaLocation: "proofs/agda/FilesystemComposition.agda:L26-L48", - isabelleLocation: "proofs/isabelle/FilesystemComposition.thy:L22-L42", - description: "apply_sequence(reverse(ops), apply_sequence(ops, fs)) = fs", -}