-- allium: 1
-- bDS Post Lifecycle
-- Scope: core (Wave 1)
-- Distilled from: src/main/engine/PostEngine.ts, postFileUtils.ts, schema.ts

use "./project.allium" as project

enum PostStatus {
    draft
    published
    archived
}

value Slug {
    value: String

    -- Generated by: transliterate unicode to ASCII, lowercase,
    -- replace [^a-z0-9]+ with hyphens, strip leading/trailing hyphens
    -- Transliteration scope: only German (ä/ö/ü/ß/ÄÖÜ) and English letters used.
    -- Verify transliteration matches the established bDS behaviour for this set.
    -- Uniqueness: tries base, then {slug}-2 .. {slug}-999, then {slug}-{timestamp}
}

value PostFilePath {
    -- posts/YYYY/MM/{slug}.md
    -- YYYY and MM derived from created_at
    base_dir: String
    year: String
    month: String
    slug: Slug
}

value PostCanonicalUrl {
    -- /{YYYY}/{MM}/{DD}/{slug}
    -- YYYY/MM/DD from created_at (zero-padded)
    year: String
    month: String
    day: String
    slug: Slug
}

value Frontmatter {
    -- YAML between --- delimiters at start of .md file
    -- Always present: id, title, slug, status, createdAt, updatedAt, tags, categories
    -- Optional (written only when truthy): excerpt, author, language,
    --   doNotTranslate (only when true), templateSlug, publishedAt
}

surface PostControlSurface {
    facing _: PostOperator

    provides:
        CreatePostRequested(project, title, content, tags, categories, author, language, template_slug)
        UpdatePostRequested(post, changes)
        PublishPostRequested(post)
        DeletePostRequested(post)
        ArchivePostRequested(post)
}

surface PostFilePathSurface {
    context path: PostFilePath

    exposes:
        path.base_dir
        path.year
        path.month
        path.slug
}

surface PostCanonicalUrlSurface {
    context url: PostCanonicalUrl

    exposes:
        url.year
        url.month
        url.day
        url.slug
}

surface FrontmatterSurface {
    context _: Frontmatter
}

entity Post {
    project: project/Project
    title: String
    slug: Slug
    excerpt: String?
    content: String?
    status: PostStatus
    author: String?
    language: String?
    do_not_translate: Boolean
    template_slug: String?
    file_path: String
    checksum: String?
    tags: List<String>
    categories: List<String>
    created_at: Timestamp
    updated_at: Timestamp
    published_at: Timestamp?

    -- Relationships
    translations: PostTranslation with canonical_post = this
    linked_media: PostMediaLink with post = this
    outgoing_links: PostLink with source = this
    incoming_links: PostLink with target = this

    -- Derived
    available_languages: translations -> language
    is_slug_frozen: published_at != null
        -- Slug changes only allowed before first publish
    content_location: if status = published: file_path else: content
        -- Published: body in filesystem. Draft: body in DB field.

    transitions status {
        draft -> published
        draft -> archived
        published -> draft
        published -> archived
        archived -> draft
        archived -> published
    }
}

entity PostLink {
    source: Post
    target: Post
    link_text: String?
}

entity PostMediaLink {
    post: Post
    media_id: String
    sort_order: Integer
}

invariant UniqueSlugPerProject {
    for a in Posts:
        for b in Posts:
            (a != b and a.project = b.project) implies a.slug != b.slug
}

rule CreatePost {
    when: CreatePostRequested(project, title, content, tags, categories, author, language, template_slug)
    let slug = Slug.generate(title ?? "untitled")
    let unique_slug = Slug.ensure_unique(slug, project)
    ensures:
        let new_post = Post.created(
            project: project,
            title: title ?? "",
            slug: unique_slug,
            content: content,
            status: draft,
            author: author,
            language: language,
            tags: tags ?? {},
            categories: categories ?? {},
            template_slug: template_slug,
            do_not_translate: false,
            file_path: ""
        )
        new_post.status = draft
        SearchIndexUpdated(new_post)
}

rule UpdatePost {
    when: UpdatePostRequested(post, changes)
    requires: not post.is_slug_frozen or changes.slug = null
        -- Cannot change slug after first publish
    ensures: post.updated_at = now
    ensures: PostFieldsUpdated(post, changes)
    ensures: SearchIndexUpdated(post)
    @guidance
        -- If post is published and content/metadata changed,
        -- status auto-transitions back to draft
}

rule ReopenPublishedPost {
    when: UpdatePostRequested(post, changes)
    requires: post.status = published
    requires: changes_affect_published_content(changes)
    ensures: post.status = draft
}

rule PublishPost {
    when: PublishPostRequested(post)
    requires: post.status = draft or post.status = archived
    ensures: post.status = published
    ensures: post.published_at = post.published_at ?? now
        -- Preserve original publish date on re-publish
    ensures: PostFileWritten(post)
        -- Writes frontmatter + markdown to posts/YYYY/MM/{slug}.md
    ensures: post.content = null
        -- Content cleared from DB; now lives in filesystem only
    ensures: SearchIndexUpdated(post)
    ensures: PostLinksUpdated(post)
        -- Parse inter-post links, update link graph
    ensures:
        for t in post.translations:
            TranslationFileWritten(t)
}

rule DeletePost {
    when: DeletePostRequested(post)
    ensures: not exists post
    ensures: PostFileDeleted(post)
        -- Remove .md file if it exists
    ensures:
        for t in post.translations:
            not exists t
    ensures: SearchIndexUpdated(post)
}

rule ArchivePost {
    when: ArchivePostRequested(post)
    requires: post.status = draft or post.status = published
    ensures: post.status = archived
}

-- File format axioms

invariant FrontmatterRoundtrip {
    -- Reading a post file written by the system produces identical
    -- field values to the database record at time of writing
    for post in Posts where status = published:
        parse_frontmatter(read_file(post.file_path)) = frontmatter_fields(post)
}

invariant DateBasedFileLayout {
    for post in Posts where file_path != "":
        post.file_path = format("posts/{yyyy}/{mm}/{slug}.md",
            yyyy: post.created_at.year,
            mm: post.created_at.month_padded,
            slug: post.slug)
}

-- Slug freeze: once published_at is set, the slug is permanently frozen.
-- This follows the established bDS rule: is_slug_frozen = published_at != null
-- Even if the post reverts to draft, the slug cannot be changed.