-- allium: 1
-- bDS MCP Server (Model Context Protocol)
-- Scope: extension (Bucket G — MCP + Automation)
-- Distilled from: src/main/engine/MCPServer.ts, ProposalStore, MCPAgentConfigEngine.ts

use "./post.allium" as post
use "./media.allium" as media
use "./script.allium" as script
use "./template.allium" as template

enum ProposalStatus {
    pending
    expired
}

entity McpServer {
    transport: http | stdio
    host: String                        -- 127.0.0.1 for HTTP
    port: Integer                       -- 4124 for HTTP
    is_running: Boolean
}

surface McpServerSurface {
    context server: McpServer

    exposes:
        server.transport
        server.host
        server.port
        server.is_running
}

entity Proposal {
    kind: draft_post | propose_script | propose_template | propose_media_metadata | propose_post_metadata
    status: ProposalStatus
    entity_id: String
    data: String
    created_at: Timestamp
    expires_at: Timestamp
    draft_post: post/Post?
    proposed_script: script/Script?
    proposed_template: template/Template?
    target_media: media/Media?
    target_post: post/Post?

    -- Derived
    is_expired: expires_at <= now

    transitions status {
        pending -> expired
    }
}

surface ProposalSurface {
    context proposal: Proposal

    exposes:
        proposal.kind
        proposal.status
        proposal.entity_id
        proposal.data
        proposal.created_at
        proposal.expires_at
        proposal.draft_post when proposal.draft_post != null
        proposal.proposed_script when proposal.proposed_script != null
        proposal.proposed_template when proposal.proposed_template != null
        proposal.target_media when proposal.target_media != null
        proposal.target_post when proposal.target_post != null
        proposal.is_expired
}

config {
    http_port: Integer = 4124
    proposal_ttl_app: Duration = 30.minutes
    proposal_ttl_cli: Duration = 8.hours
}

surface McpAutomationSurface {
    facing _: McpClient

    provides:
        McpToolInvoked("check_term", term)
        McpToolInvoked("search_posts", params)
        McpToolInvoked("count_posts", params)
        McpToolInvoked("read_post_by_slug", slug, language)
        McpToolInvoked("draft_post", params)
        McpToolInvoked("propose_script", params)
        McpToolInvoked("propose_template", params)
        McpToolInvoked("propose_media_metadata", params)
        McpToolInvoked("propose_post_metadata", params)
        AcceptProposalRequested(proposal)
        DiscardProposalRequested(proposal)
        InstallAgentConfigRequested(agent_kind)
        UninstallAgentConfigRequested(agent_kind)
}

invariant LocalhostOnlyHttp {
    -- HTTP transport binds to 127.0.0.1 only
    -- Origin validation: localhost only
    -- CORS headers present
}

invariant StatelessHttpHandling {
    -- Each HTTP request creates a fresh McpServer instance
    -- No session state between requests
}

-- Read-only resources (bds:// scheme)

surface PostsResource {
    facing viewer: McpClient
    context posts: Posts
    exposes:
        for p in posts:
            p.id
            p.title
            p.slug
            p.status
            p.tags
            p.categories
            p.created_at
            p.backlinks
            p.outlinks
    @guidance
        -- Paginated: 50 per page, base64url cursor
        -- bds://posts, bds://posts?cursor={cursor}
}

surface MediaResource {
    facing viewer: McpClient
    context media_items: Media
    exposes:
        for m in media_items:
            m.id
            m.filename
            m.title
            m.alt
            m.caption
            m.tags
    @guidance
        -- bds://media, bds://media?cursor={cursor}
}

surface TagsResource {
    facing viewer: McpClient
    context tags: Tags
    exposes:
        for t in tags:
            t.name
            t.color
            t.post_count
    @guidance
        -- bds://tags
}

surface CategoriesResource {
    facing viewer: McpClient
    context categories: Categories
    exposes:
        for c in categories:
            c.name
            c.post_count
    @guidance
        -- bds://categories
}

-- Read-only tools

rule CheckTerm {
    when: McpToolInvoked("check_term", term)
    -- Disambiguates a term as category, tag, or both
    -- Returns post counts for each
    let is_category = is_category_term(term)
    let is_tag = is_tag_term(term)
    ensures: TermCheckResult(
        is_category: is_category,
        category_post_count: if is_category: category_post_count(term) else: 0,
        is_tag: is_tag,
        tag_post_count: if is_tag: tag_post_count(term) else: 0
    )
}

rule SearchPosts {
    when: McpToolInvoked("search_posts", params)
    -- Full-text + filtered search with pagination envelope
    -- Params: query, category, tags[], language, missingTranslationLanguage,
    --   year, month, status, offset, limit
    -- Returns: { total, offset, limit, hasMore, posts[] }
    -- Each post includes backlinks[] and linksTo[]
    ensures: SearchEnvelope(results)
}

rule CountPosts {
    when: McpToolInvoked("count_posts", params)
    -- Grouped counts by: year, month, tag, category, status
    -- Params: groupBy[], optional filters
    ensures: GroupedCounts(results)
}

rule ReadPostBySlug {
    when: McpToolInvoked("read_post_by_slug", slug, language)
    -- Full post content by slug
    -- Optional language parameter for translation view
    ensures: FullPostContent(post)
}

-- Write tools (proposal-based)

rule DraftPost {
    when: McpToolInvoked("draft_post", params)
    -- Creates a draft post in DB
    -- Returns proposalId for accept/discard lifecycle
    ensures:
        let new_post = post/Post.created(
            title: params.title,
            content: params.content,
            status: draft
        )
        let proposal = Proposal.created(
            kind: draft_post,
            entity_id: new_post.id,
            data: "",
            created_at: now,
            expires_at: now + config.proposal_ttl_app,
            draft_post: new_post,
            proposed_script: null,
            proposed_template: null,
            target_media: null,
            target_post: null,
            status: pending
        )
        proposal.status = pending
}

rule ProposeScript {
    when: McpToolInvoked("propose_script", params)
    requires: ValidateScript(params.content) = valid
    ensures:
        let new_script = script/Script.created(
            title: params.title,
            kind: params.kind,
            content: params.content,
            status: draft
        )
        let proposal = Proposal.created(
            kind: propose_script,
            entity_id: new_script.id,
            data: "",
            created_at: now,
            expires_at: now + config.proposal_ttl_app,
            draft_post: null,
            proposed_script: new_script,
            proposed_template: null,
            target_media: null,
            target_post: null,
            status: pending
        )
        proposal.status = pending
}

rule ProposeTemplate {
    when: McpToolInvoked("propose_template", params)
    requires: ValidateLiquid(params.content) = valid
    ensures:
        let new_template = template/Template.created(
            title: params.title,
            kind: params.kind,
            content: params.content,
            status: draft
        )
        let proposal = Proposal.created(
            kind: propose_template,
            entity_id: new_template.id,
            data: "",
            created_at: now,
            expires_at: now + config.proposal_ttl_app,
            draft_post: null,
            proposed_script: null,
            proposed_template: new_template,
            target_media: null,
            target_post: null,
            status: pending
        )
        proposal.status = pending
}

rule ProposeMediaMetadata {
    when: McpToolInvoked("propose_media_metadata", params)
    ensures:
        let proposal = Proposal.created(
            kind: propose_media_metadata,
            entity_id: params.media_id,
            data: serialize(params),
            created_at: now,
            expires_at: now + config.proposal_ttl_app,
            draft_post: null,
            proposed_script: null,
            proposed_template: null,
            target_media: params.media,
            target_post: null,
            status: pending
        )
        proposal.status = pending
}

rule ProposePostMetadata {
    when: McpToolInvoked("propose_post_metadata", params)
    ensures:
        let proposal = Proposal.created(
            kind: propose_post_metadata,
            entity_id: params.post_id,
            data: serialize(params),
            created_at: now,
            expires_at: now + config.proposal_ttl_app,
            draft_post: null,
            proposed_script: null,
            proposed_template: null,
            target_media: null,
            target_post: params.post,
            status: pending
        )
        proposal.status = pending
}

-- Proposal lifecycle

rule AcceptProposal {
    when: AcceptProposalRequested(proposal)
    requires: not proposal.is_expired
    ensures:
        if proposal.kind = draft_post:
            post/PublishPostRequested(proposal.draft_post)
        if proposal.kind = propose_script:
            script/PublishScriptRequested(proposal.proposed_script)
        if proposal.kind = propose_template:
            template/PublishTemplateRequested(proposal.proposed_template)
        if proposal.kind = propose_media_metadata:
            media/UpdateMediaRequested(proposal.target_media, deserialize_media_changes(proposal.data))
        if proposal.kind = propose_post_metadata:
            post/UpdatePostRequested(proposal.target_post, deserialize_post_changes(proposal.data))
        not exists proposal
}

rule DiscardProposal {
    when: DiscardProposalRequested(proposal)
    ensures:
        if proposal.kind = draft_post:
            post/DeletePostRequested(proposal.draft_post)
        if proposal.kind = propose_script:
            script/DeleteScriptRequested(proposal.proposed_script)
        if proposal.kind = propose_template:
            template/DeleteTemplateRequested(proposal.proposed_template)
        not exists proposal
}

rule ExpireProposal {
    when: proposal: Proposal.is_expired becomes true
    -- On expiry: clean up draft DB rows
    ensures: proposal.status = expired
    ensures: DiscardProposalRequested(proposal)
}

-- Agent configuration

value McpAgentKind {
    -- Supported: claude_code, claude_desktop, github_copilot,
    --   gemini_cli, opencode, mistral_vibe, openai_codex
    kind: String
}

surface McpAgentKindSurface {
    context agent_kind: McpAgentKind

    exposes:
        agent_kind.kind
}

rule InstallAgentConfig {
    when: InstallAgentConfigRequested(agent_kind)
    -- Writes stdio MCP server config into the agent's config file
    ensures: AgentConfigInstalled(agent_kind)
}

rule UninstallAgentConfig {
    when: UninstallAgentConfigRequested(agent_kind)
    ensures: AgentConfigRemoved(agent_kind)
}

invariant ProposalPayloadEncoding {
    -- Proposal.data stores a serialized payload for metadata proposals.
    -- draft_post / propose_script / propose_template proposals keep the
    -- created entity reference directly on the proposal record.
}