(module edl.github_coding_agent
  (capsule "0.1.0")
  (profile agentic external.mcp persistence.ledger telemetry.otel)

  (store EnclosureLedger
    (backend file)
    (authority enclosure-receipts))

  (principal HumanRepoOwner
    (kind human)
    (identity passkey-or-oidc)
    (summary "EDL principal human:repo-owner"))

  (principal AgentCodingAgent
    (kind agent)
    (identity cryptographic)
    (credential short-lived)
    (attestation required)
    (summary "EDL principal agent:coding-agent"))

  (mandate MandateRepoMaintenance
    (issued-by HumanRepoOwner)
    (issued-to AgentCodingAgent)
    (purpose "Prepare pull requests and request approved merges.")
    (valid-for 8h)
    (revocable true)
  )

  (delegation DelegationRepoMaintenance
    (from HumanRepoOwner)
    (to AgentCodingAgent)
    (under MandateRepoMaintenance)
    (may-delegate false)
    (expires-after 8h)
  )

  (port GateGithub
    (protocol mcp)
    (endpoint "https://doorkeeper.internal/mcp")
    (tool github_force_push github_merge_pr github_propose_pr)
    (summary "EDL gate gate:github"))

  (gate HumanApprovalGate
    (summary "Human approval required for high-risk enclosed actions.")
    (requires approval HumanRepoOwner granted)
    (on-fail reject)
    (on-pass manual))

  (capability CapGithubProposePr
    (principal AgentCodingAgent)
    (effect (mcp.call GateGithub.github_propose_pr))
    (resource repo:acme/app)
    (valid-for 10m)
    (requires-mandate MandateRepoMaintenance)
    (requires-delegation DelegationRepoMaintenance)
  )

  (capability CapGithubMergePr
    (principal AgentCodingAgent)
    (effect (mcp.call GateGithub.github_merge_pr))
    (resource repo:acme/app:branch:main)
    (valid-for 2m)
    (requires-mandate MandateRepoMaintenance)
    (requires-delegation DelegationRepoMaintenance)
    (approval HumanRepoOwner)
    (limit single-use true)
  )

  (trust-boundary EncGithubCodingAgent
    (mode enforce)
    (fail-closed true)
    (sandbox required)
    (network deny-by-default)
    (filesystem root-read-only)
    (egress-only GateGithub)
    (secrets ambient-deny)
    (requires-attestation true)
    (requires-profile-digest true)
    (capability CapGithubMergePr CapGithubProposePr)
    (summary "EDL enclosure enc:github-coding-agent"))

  (telemetry-obligation EnclosureTelemetry
    (must-emit invocation.start invocation.end enclosure.attested policy.evaluated capability.issued effect.intent effect.denied effect.escalated effect.executed receipt.emitted)
    (include trace_id agent_id principal_id mandate_id delegation_id capability_jti enclosure_id enclosure_profile_digest action_hash policy_id gate_id effect_intent_id)
    (export ledger siem)
    (tamper-evident true))

  (memory-policy MemSession
    (isolation per-session)
    (ttl default 24h)
    (source-attribution required)
    (hash-validation on-read)
  )

  (memory-policy MemRepoSummary
    (isolation per-repo)
    (ttl default 7d)
    (promotion requires-review)
  )

  (authority-policy PolicyGithub
    (input principal mandate delegation capability effect context risk)
    (outcome allow deny defer escalate)
    (default deny)
    (on allow (if "effect == \"github.propose_pr\" and resource.repo == \"acme/app\""))
    (on escalate (if "effect == \"github.merge_pr\" and resource.branch == \"main\""))
    (on deny (if "effect in [\"github.force_push\", \"github.disable_branch_protection\"]"))
  )

  (machine EnclosedAgent
    (version "0.1.0")
    (context
      (repo Text)
      (branch Text)
      (request_id U64))
    (event ProposeChange
      (repo Text)
      (branch Text)
      (summary Text))
    (event RequestPrivilegedAction
      (repo Text)
      (branch Text)
      (request_id U64))
    (event HumanApproved
      (approval_id Text))
    (event HumanDenied
      (approval_id Text))
    (event Complete)
    (initial ready)
    (persistence
      (store EnclosureLedger)
      (event-log enclosure_events)
      (snapshot enclosure_snapshots)
      (replay true))
    (state ready
      (on ProposeChange
        (target ready)
        (effects
          (policy.evaluate PolicyGithub)
          (mcp.call GateGithub.github_propose_pr)
          (receipt.emit proposal_receipt)))
      (on RequestPrivilegedAction
        (target waiting_for_approval)
        (effects
          (policy.evaluate PolicyGithub)
          (approval.request HumanApprovalGate)))
      (on Complete
        (target completed)
        (effects
          (receipt.emit enclosure_completed))))
    (state waiting_for_approval
      (on HumanApproved
        (target ready)
        (effects
          (capability.issue CapGithubMergePr)
          (mcp.call GateGithub.github_merge_pr)
          (receipt.emit privileged_action_executed)))
      (on HumanDenied
        (target ready)
        (effects
          (receipt.emit privileged_action_denied))))
    (state completed (type final))))