(module examples.authority_ir
  (capsule "0.25.0")
  (profile agentic external.http ui.a2ui persistence.ledger)

  (type RefundRequest (record
    (refund_id U64)
    (amount_usd U32)))

  (event SubmitRefund
    (refund_id U64)
    (amount_usd U32))
  (event HumanApproved)
  (event HumanDenied)

  (port RefundAPI
    (protocol http)
    (endpoint "https://refunds.example.test")
    (tool issue_refund)
    (summary "Mediated refund API endpoint."))

  (store RefundLedger
    (backend surrealdb)
    (authority operational-refund-records))

  (principal ClaimsLead
    (kind human)
    (identity sso-passkey)
    (credential phishing-resistant)
    (attestation workforce-device)
    (summary "Human owner of refund review mandates."))

  (principal RefundReviewer
    (kind agent)
    (identity cryptographic)
    (credential short-lived)
    (attestation required)
    (owner ClaimsLead)
    (summary "Agent principal bound to one refund review task."))

  (mandate RefundReviewMandate
    (issued-by ClaimsLead)
    (issued-to RefundReviewer)
    (purpose "Review and optionally issue one refund.")
    (subject refund_id)
    (scope tenant.current refund.current)
    (valid-for 30m)
    (revocable true))

  (delegation RefundReviewDelegation
    (from ClaimsLead)
    (to RefundReviewer)
    (under RefundReviewMandate)
    (may-use RefundAPI.issue_refund RefundLedger)
    (may-delegate false)
    (expires-after 30m)
    (requires traceable-chain human-approval-for-high-risk))

  (gate RefundApprovalGate
    (summary "Refunds above the low-risk threshold require explicit human approval.")
    (requires approval ClaimsLead granted)
    (on-fail reject)
    (on-pass manual))

  (capability IssueSmallRefund
    (principal RefundReviewer)
    (effect (http.call RefundAPI.issue_refund))
    (resource refund_id)
    (scope tenant.current refund.current)
    (valid-for 5m)
    (requires-mandate RefundReviewMandate)
    (requires-delegation RefundReviewDelegation)
    (revocation immediate)
    (risk medium)
    (approval RefundApprovalGate)
    (limit max-amount-usd 100))

  (authority-policy RefundPolicy
    (input principal mandate delegation capability effect context risk)
    (outcome allow deny defer escalate)
    (default deny)
    (on allow
      (if (<= amount_usd 50)))
    (on escalate
      (if (> amount_usd 50))
      (effect (approval.request RefundApprovalGate))))

  (trust-boundary RefundAgentBoundary
    (sandbox required)
    (network deny-by-default)
    (filesystem read-only)
    (egress RefundAPI)
    (secrets ambient-false)
    (attestation required)
    (capability IssueSmallRefund))

  (telemetry-obligation RefundTelemetry
    (must-emit invocation.start invocation.end policy.evaluated capability.issued effect.intent effect.approved effect.executed effect.denied)
    (include trace_id span_id principal_id mandate_id delegation_id capability_id contract_hash effect_intent_id)
    (export otel siem ledger)
    (tamper-evident true))

  (memory-policy RefundMemory
    (isolation per-tenant per-session)
    (ttl untrusted-context 24h)
    (source-attribution required)
    (hash-validation on-read)
    (quarantine-on-integrity-fail true)
    (promotion requires-accepted-claim))

  (machine RefundReview
    (version "0.1")
    (context
      (refund_id U64)
      (amount_usd U32))
    (event SubmitRefund
      (refund_id U64)
      (amount_usd U32))
    (event HumanApproved)
    (event HumanDenied)
    (initial idle)
    (persistence
      (store RefundLedger)
      (event-log refund_events)
      (snapshot refund_snapshots)
      (replay true))
    (state idle
      (on SubmitRefund
        (target reviewing)
        (effects
          (db.write RefundLedger.review_started))))
    (state reviewing
      (on HumanApproved
        (guard (<= amount_usd 100))
        (target issued)
        (effects
          (http.call RefundAPI.issue_refund)
          (db.write RefundLedger.review_issued)))
      (on HumanDenied
        (target rejected)
        (effects
          (db.write RefundLedger.review_rejected))))
    (state issued (type final))
    (state rejected (type final))))