|
| 1 | +-- SPDX-License-Identifier: MPL-2.0 |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +||| BugFilingMcp.SafeBugFiling: Formally verified bug-filing pipeline states. |
| 4 | +||| |
| 5 | +||| Cartridge: bug-filing-mcp (wraps the feedback-o-tron engine) |
| 6 | +||| Matrix cell: Development domain x {MCP, REST} protocols |
| 7 | +||| |
| 8 | +||| This module defines the interactive filing pipeline as a state machine |
| 9 | +||| that prevents: |
| 10 | +||| - Submitting a report that was rejected by the usefulness gate |
| 11 | +||| - Submitting template answers that were never validated |
| 12 | +||| - Skipping research when a duplicate check is required |
| 13 | +||| |
| 14 | +||| Doctrine encoded (feedback-o-tron design intent): |
| 15 | +||| - the gate is usefulness, not tone: Salvaged is a live state, not an end |
| 16 | +||| - zero-signal hostility dead-ends in Rejected (no path to Submitted) |
| 17 | +||| - open questions loop Synthesized -> Synthesized until validation |
| 18 | +||| |
| 19 | +||| State machine: |
| 20 | +||| Draft -> Researched -> Synthesized -> Validated -> Submitted |
| 21 | +||| (Synthesized may be Salvaged first; Rejected is terminal) |
| 22 | +module BugFilingMcp.SafeBugFiling |
| 23 | + |
| 24 | +import Data.List |
| 25 | + |
| 26 | +%default total |
| 27 | + |
| 28 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 29 | +-- Filing Pipeline State Machine |
| 30 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 31 | + |
| 32 | +||| Pipeline lifecycle states for one piece of feedback. |
| 33 | +public export |
| 34 | +data FilingState |
| 35 | + = Draft -- raw feedback exists, nothing checked |
| 36 | + | Researched -- duplicates + template questions fetched |
| 37 | + | Salvaged -- hostile wrapping stripped; actionable core kept |
| 38 | + | Synthesized -- template hydrated; open questions may remain |
| 39 | + | Validated -- answers passed the form-schema boundary |
| 40 | + | Submitted -- dispatched to the forge(s) |
| 41 | + | Rejected -- zero-signal hostility: terminal, never filed |
| 42 | + |
| 43 | +||| Equality for filing states. |
| 44 | +public export |
| 45 | +Eq FilingState where |
| 46 | + Draft == Draft = True |
| 47 | + Researched == Researched = True |
| 48 | + Salvaged == Salvaged = True |
| 49 | + Synthesized == Synthesized = True |
| 50 | + Validated == Validated = True |
| 51 | + Submitted == Submitted = True |
| 52 | + Rejected == Rejected = True |
| 53 | + _ == _ = False |
| 54 | + |
| 55 | +||| Valid state transitions (enforced at the type level). |
| 56 | +||| Critically there is NO constructor targeting Submitted except from |
| 57 | +||| Validated, and NO constructor leaving Rejected. |
| 58 | +public export |
| 59 | +data ValidTransition : FilingState -> FilingState -> Type where |
| 60 | + Research : ValidTransition Draft Researched |
| 61 | + SalvageCore : ValidTransition Researched Salvaged |
| 62 | + Synthesize : ValidTransition Researched Synthesized |
| 63 | + Resynth : ValidTransition Synthesized Synthesized -- open-questions loop |
| 64 | + FromSalvage : ValidTransition Salvaged Synthesized |
| 65 | + Validate : ValidTransition Synthesized Validated |
| 66 | + Submit : ValidTransition Validated Submitted |
| 67 | + RejectR : ValidTransition Researched Rejected |
| 68 | + RejectD : ValidTransition Draft Rejected |
| 69 | + |
| 70 | +||| Runtime transition validator (mirrors ValidTransition). |
| 71 | +public export |
| 72 | +canTransition : FilingState -> FilingState -> Bool |
| 73 | +canTransition Draft Researched = True |
| 74 | +canTransition Researched Salvaged = True |
| 75 | +canTransition Researched Synthesized = True |
| 76 | +canTransition Synthesized Synthesized = True |
| 77 | +canTransition Salvaged Synthesized = True |
| 78 | +canTransition Synthesized Validated = True |
| 79 | +canTransition Validated Submitted = True |
| 80 | +canTransition Researched Rejected = True |
| 81 | +canTransition Draft Rejected = True |
| 82 | +canTransition _ _ = False |
| 83 | + |
| 84 | +||| Rejected is terminal: no transition out of it is ever valid. |
| 85 | +export |
| 86 | +rejectedIsTerminal : (s : FilingState) -> ValidTransition Rejected s -> Void |
| 87 | +rejectedIsTerminal _ Research impossible |
| 88 | +rejectedIsTerminal _ SalvageCore impossible |
| 89 | +rejectedIsTerminal _ Synthesize impossible |
| 90 | +rejectedIsTerminal _ Resynth impossible |
| 91 | +rejectedIsTerminal _ FromSalvage impossible |
| 92 | +rejectedIsTerminal _ Validate impossible |
| 93 | +rejectedIsTerminal _ Submit impossible |
| 94 | +rejectedIsTerminal _ RejectR impossible |
| 95 | +rejectedIsTerminal _ RejectD impossible |
| 96 | + |
| 97 | +||| Submission only ever follows validation: the sole transition into |
| 98 | +||| Submitted starts at Validated. |
| 99 | +export |
| 100 | +submitRequiresValidation : (s : FilingState) -> ValidTransition s Submitted -> s = Validated |
| 101 | +submitRequiresValidation Validated Submit = Refl |
| 102 | + |
| 103 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 104 | +-- MCP Tool Definitions |
| 105 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 106 | + |
| 107 | +||| MCP tools exposed by this cartridge. |
| 108 | +public export |
| 109 | +data McpTool |
| 110 | + = ToolResearch -- research_feedback |
| 111 | + | ToolSynthesize -- synthesize_feedback |
| 112 | + | ToolSubmit -- submit_feedback |
| 113 | + |
| 114 | +||| MCP tool name (must match cartridge.json). |
| 115 | +public export |
| 116 | +toolName : McpTool -> String |
| 117 | +toolName ToolResearch = "research_feedback" |
| 118 | +toolName ToolSynthesize = "synthesize_feedback" |
| 119 | +toolName ToolSubmit = "submit_feedback" |
| 120 | + |
| 121 | +||| The pipeline state each tool drives toward. |
| 122 | +public export |
| 123 | +toolTarget : McpTool -> FilingState |
| 124 | +toolTarget ToolResearch = Researched |
| 125 | +toolTarget ToolSynthesize = Synthesized |
| 126 | +toolTarget ToolSubmit = Submitted |
| 127 | + |
| 128 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 129 | +-- C-ABI Exports |
| 130 | +-- ═══════════════════════════════════════════════════════════════════════════ |
| 131 | + |
| 132 | +||| Filing state to integer for the C ABI. |
| 133 | +public export |
| 134 | +filingStateToInt : FilingState -> Int |
| 135 | +filingStateToInt Draft = 0 |
| 136 | +filingStateToInt Researched = 1 |
| 137 | +filingStateToInt Salvaged = 2 |
| 138 | +filingStateToInt Synthesized = 3 |
| 139 | +filingStateToInt Validated = 4 |
| 140 | +filingStateToInt Submitted = 5 |
| 141 | +filingStateToInt Rejected = 6 |
| 142 | + |
| 143 | +||| Integer to filing state (unknown collapses to Rejected: fail closed). |
| 144 | +public export |
| 145 | +intToFilingState : Int -> FilingState |
| 146 | +intToFilingState 0 = Draft |
| 147 | +intToFilingState 1 = Researched |
| 148 | +intToFilingState 2 = Salvaged |
| 149 | +intToFilingState 3 = Synthesized |
| 150 | +intToFilingState 4 = Validated |
| 151 | +intToFilingState 5 = Submitted |
| 152 | +intToFilingState _ = Rejected |
| 153 | + |
| 154 | +||| FFI: Validate a state transition. |
| 155 | +export |
| 156 | +bf_can_transition : Int -> Int -> Int |
| 157 | +bf_can_transition from to = |
| 158 | + if canTransition (intToFilingState from) (intToFilingState to) then 1 else 0 |
0 commit comments