-- 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
    executing
    accepted
    rejected
    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_translation | propose_media_metadata | propose_post_metadata
    status: ProposalStatus
    entity_id: String
    data: String
    created_at: Timestamp
    expires_at: Timestamp
    resolved_at: Timestamp?
    result: String?
    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 -> executing
        pending -> expired
        executing -> accepted
        executing -> rejected
    }
}

surface ProposalSurface {
    context proposal: Proposal

    exposes:
        proposal.kind
        proposal.status
        proposal.entity_id
        proposal.data
        proposal.created_at
        proposal.expires_at
        proposal.resolved_at when proposal.resolved_at != null
        proposal.result when proposal.result != null
        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: Duration = 30.minutes
}

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("get_post_translations", post_id)
        McpToolInvoked("get_media_translations", media_id)
        McpToolInvoked("upsert_media_translation", params)
        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)
}

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

invariant StatelessHttpHandling {
    -- Each HTTP request opens a fresh shared database connection through a
    -- path-only application context. No MCP session id or client state is kept.
}

invariant InertProposalPayloads {
    -- Write tools validate their request and persist only a serialized proposal.
    -- They do not create or update posts, media translations, scripts, templates,
    -- sidecars, or other content before explicit desktop approval.
}

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

surface ProjectResource {
    facing viewer: McpClient
    context project: Project
    exposes:
        project.id
        project.name
        project.slug
        project.description
        project.public_url
        project.main_language
        project.blog_languages
    @guidance
        -- bds://project. Local filesystem paths are not exposed.
}

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
}

surface StatsResource {
    facing viewer: McpClient
    context blog: Blog
    exposes:
        blog.post_count
        blog.media_count
        blog.tag_count
        blog.category_count
    @guidance
        -- bds://stats
}

surface PostMediaResource {
    facing viewer: McpClient
    context post: post/Post
    exposes:
        for m in post.media:
            m.id
            m.filename
            m.title
            m.alt
            m.caption
            m.tags
    @guidance
        -- bds://posts/{id}/media
        -- Unknown post ids return not_found.
}

surface MediaImageResource {
    facing viewer: McpClient
    context media_item: media/Media
    exposes:
        media_item.mime_type
        media_item.file_bytes
    @guidance
        -- bds://media/{id}/image
        -- Returns blob content using the media MIME type.
        -- Unknown media ids or missing files return not_found.
}

-- 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)
}

rule GetPostTranslations {
    when: McpToolInvoked("get_post_translations", post_id)
    -- Lists all available translations for a post.
    ensures: PostTranslations(post_id)
}

rule GetMediaTranslations {
    when: McpToolInvoked("get_media_translations", media_id)
    -- Lists all available translated metadata for a media item.
    ensures: MediaTranslations(media_id)
}

rule UpsertMediaTranslation {
    when: McpToolInvoked("upsert_media_translation", params)
    -- Persists an inert translated-metadata proposal for desktop review.
    ensures: Proposal.created(
        kind: propose_media_translation,
        entity_id: params.media_id,
        data: serialize(params),
        created_at: now,
        expires_at: now + config.proposal_ttl,
        draft_post: null,
        proposed_script: null,
        proposed_template: null,
        target_media: params.media,
        target_post: null,
        status: pending
    )
}

-- Write tools (proposal-based)

rule DraftPost {
    when: McpToolInvoked("draft_post", params)
    -- Validates and stores an inert post payload; returns proposalId.
    ensures:
        let proposal = Proposal.created(
            kind: draft_post,
            entity_id: params.proposal_entity_id,
            data: serialize(params),
            created_at: now,
            expires_at: now + config.proposal_ttl,
            draft_post: null,
            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 proposal = Proposal.created(
            kind: propose_script,
            entity_id: params.proposal_entity_id,
            data: serialize(params),
            created_at: now,
            expires_at: now + config.proposal_ttl,
            draft_post: null,
            proposed_script: null,
            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 proposal = Proposal.created(
            kind: propose_template,
            entity_id: params.proposal_entity_id,
            data: serialize(params),
            created_at: now,
            expires_at: now + config.proposal_ttl,
            draft_post: null,
            proposed_script: null,
            proposed_template: null,
            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,
            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,
            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(deserialize_post(proposal.data))
        if proposal.kind = propose_script:
            script/PublishScriptRequested(deserialize_script(proposal.data))
        if proposal.kind = propose_template:
            template/PublishTemplateRequested(deserialize_template(proposal.data))
        if proposal.kind = propose_media_translation:
            media/UpsertMediaTranslationRequested(deserialize_media_translation(proposal.data))
        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))
        proposal.status = accepted
        proposal.result = serialize(result)
        proposal.resolved_at = now
}

rule DiscardProposal {
    when: DiscardProposalRequested(proposal)
    -- There are no temporary content entities to clean up.
    ensures: proposal.status = rejected
    ensures: proposal.result = serialize(rejected)
    ensures: proposal.resolved_at = now
}

rule ExpireProposal {
    when: proposal: Proposal.is_expired becomes true
    -- Expiry marks the inert proposal terminal; no content cleanup is needed.
    ensures: proposal.status = expired
    ensures: proposal.result = serialize(expired)
    ensures: proposal.resolved_at = now
}

-- Agent configuration

value McpAgentKind {
    -- Currently supported and shown: claude_code, github_copilot.
    kind: String
}

surface McpAgentKindSurface {
    context agent_kind: McpAgentKind

    exposes:
        agent_kind.kind
}

surface McpSettingsSurface {
    provides:
        SettingsMCPAgentToggled(agent_kind)

    @guidance
        -- Agent configuration install/remove is exposed by the settings UI,
        -- not by the MCP automation surface.
}

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

rule UninstallAgentConfig {
    when: SettingsMCPAgentToggled(agent_kind)
    requires: AgentConfigInstalled(agent_kind)
    ensures: AgentConfigRemoved(agent_kind)
}

invariant ProposalPayloadEncoding {
    -- Proposal.data stores the validated serialized payload for every write.
    -- Terminal status/result rows remain available for result reporting.
}
