RuDS/specs/git.allium

-- allium: 1
-- bDS Git Integration
-- Scope: extension (Bucket A — Git + Validation)
-- Distilled from: src/main/engine/GitEngine.ts

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

value GitProvider {
    kind: github | gitlab | gitea_forgejo
    -- Detected from remote URL patterns
}

value GitSyncStatus {
    -- Per-commit: local_only | remote_only | both
    kind: local_only | remote_only | both
}

value GitFileStatus {
    path: String
    old_path: String?
    kind: added | modified | deleted | renamed | untracked
}

value GitCommit {
    hash: String
    subject: String?
    author: String?
    date: String?
    sync_status: GitSyncStatus
}

value GitRemoteState {
    local_branch: String?
    upstream_branch: String?
    has_upstream: Boolean
    ahead: Integer
    behind: Integer
}

config {
    local_timeout: Duration = 15.seconds
    network_timeout: Duration = 120.seconds
    file_history_limit: Integer = 50
}

surface GitSyncStatusSurface {
    context status: GitSyncStatus

    exposes:
        status.kind
}

entity GitRepository {
    is_initialized: Boolean
    remote_url: String?
    provider: GitProvider?
    current_branch: String?
    has_lfs: Boolean
}

surface GitRepositorySurface {
    context repo: GitRepository

    exposes:
        repo.is_initialized
        repo.remote_url when repo.remote_url != null
        repo.provider when repo.provider != null
        repo.current_branch when repo.current_branch != null
        repo.has_lfs
}

surface GitControlSurface {
    facing _: GitOperator

    exposes:
        GitFileStatus
        GitCommit
        GitRemoteState

    provides:
        InitializeRepoRequested(project)
        GitStatusRequested(project)
        GitDiffRequested(project)
        GitFileDiffRequested(project, file_path)
        GitHistoryRequested(project, branch)
        GitFileHistoryRequested(project, file_path)
        GitRemoteStateRequested(project)
        GitFetchRequested(project)
        GitPullRequested(project)
        GitPushRequested(project)
        GitNetworkRunCancelled(project)
        GitCommitAllRequested(project, message)
        GitReconcileRequested(project, old_commit, new_commit)
        PruneLfsCacheRequested(project, retain_recent)
}

rule InitializeRepo {
    when: InitializeRepoRequested(project)
    ensures: GitRepository.created(
        is_initialized: true,
        remote_url: null,
        provider: null,
        current_branch: "master",
        has_lfs: true
    )
    ensures: GitignoreCreated(project)
        -- .gitignore manages generated artifacts, cached assets, dependency directories, etc.
    ensures: LfsTrackingConfigured(project)
        -- Git LFS auto-tracks image patterns (*.jpg, *.png, *.gif, etc.)
}

rule GetStatus {
    when: GitStatusRequested(project)
    -- Returns file-level status: added, modified, deleted, renamed, untracked
    ensures: GitStatusReport(files)
}

rule GetDiff {
    when: GitDiffRequested(project)
    ensures: GitDiffReport(staged_diff, unstaged_diff)
}

rule GetFileDiff {
    when: GitFileDiffRequested(project, file_path)
    -- Returns the file at HEAD and in the working tree. A missing side is
    -- represented by empty content so added and deleted files remain viewable.
    ensures: GitFileDiffReport(file_path, original_content, modified_content)
}

rule GetHistory {
    when: GitHistoryRequested(project, branch)
    -- Returns commit history with sync status per commit
    ensures: GitHistoryReport(commits)
    @guidance
        -- Each commit annotated with: local_only, remote_only, or both
        -- This drives the "push needed" / "pull needed" indicators
}


rule GetFileHistory {
    when: GitFileHistoryRequested(project, file_path)
    -- Follows renames and returns the newest config.file_history_limit commits.
    -- A file with no history produces an empty report rather than an error.
    ensures: GitFileHistoryReport(file_path, commits)
}

rule GetRemoteState {
    when: GitRemoteStateRequested(project)
    -- A repository without an upstream reports zero ahead/behind counts.
    ensures: GitRemoteStateReport(project, local_branch, upstream_branch, ahead, behind)
}

rule Fetch {
    when: GitFetchRequested(project)
    ensures: RemoteRefsUpdated(project)

    @guidance
        -- Network output is streamed live and the run can be cancelled.
}

rule Pull {
    when: GitPullRequested(project)
    ensures: LocalBranchUpdated(project)
    ensures: GitReconcileRequested(project, previous_head(project), current_head(project))
        -- After pull, detect changed files and reconcile DB

    @guidance
        -- Pull is fast-forward-only. Network output is streamed live and the
        -- run can be cancelled.
}

rule Push {
    when: GitPushRequested(project)
    ensures: RemoteBranchUpdated(project)

    @guidance
        -- Network output is streamed live and the run can be cancelled.
}

rule CancelNetworkRun {
    when: GitNetworkRunCancelled(project)
    ensures: RunningGitProcessTerminated(project)
    ensures: GitNetworkRunFinished(project, cancelled)
}

rule CommitAll {
    when: GitCommitAllRequested(project, message)
    requires: message != ""
    ensures: AllChangesStaged(project)
    ensures: CommitCreated(project, message)
}

-- Git reconciliation: sync DB from filesystem changes

rule ReconcileFromGit {
    when: GitReconcileRequested(project, old_commit, new_commit)
    -- Detect changed files between commits for posts, scripts, templates
    let post_changes = changed_post_files(old_commit, new_commit)
    let script_changes = changed_script_files(old_commit, new_commit)
    let template_changes = changed_template_files(old_commit, new_commit)

    for added in post_changes.added:
        ensures: post/Post.created(parse_post_file(added))
    for modified in post_changes.modified:
        ensures: PostUpdatedFromFile(modified)
    for deleted in post_changes.deleted:
        ensures: PostDeletedByPath(deleted)
    for renamed in post_changes.renamed:
        ensures: PostFileRenamed(renamed.old, renamed.new)

    -- Same pattern for scripts and templates
    for added in script_changes.added:
        ensures: script/Script.created(parse_script_file(added))
    for added in template_changes.added:
        ensures: template/Template.created(parse_template_file(added))

    ensures: EntityChangedEventsEmitted(project)
}

invariant NonInteractiveGit {
    -- All git operations run non-interactively:
    --   GIT_TERMINAL_PROMPT=0
    --   GCM_INTERACTIVE=never
    --   ssh -oBatchMode=yes
    -- No password prompts ever surface to the user
}

invariant StructuredAuthErrors {
    -- Auth failures produce structured guidance:
    --   per platform (macOS/Windows/Linux)
    --   per provider (GitHub/GitLab/Gitea)
    -- Instead of raw git error messages
}

invariant BoundedGitExecution {
    -- Local operations stop after config.local_timeout and network operations
    -- stop after config.network_timeout. Timeout errors identify the operation
    -- and preserve captured output; the spawned process is terminated.
}

invariant OfflineNetworkGate {
    -- Fetch, pull, and push are refused by their UI/automation caller while
    -- airplane mode is active. Repository inspection and local commits remain
    -- available.
}

rule PruneLfsCache {
    when: PruneLfsCacheRequested(project, retain_recent)
    -- Prunes LFS cache with configurable recent commit retention
    ensures: LfsCachePruned(project)
}