temporal_count_formerly_login

An aggregation-flavoured temporal macro. count_formerly(?w, ?s) counts the timepoints within a window ?w at which predicate ?s held. It desugars to

count for ($t: Timepoint). where (formerly within ?w (?s && tp($t)))

where $t is a fresh binder the macro introduces itself — hygienically renamed per call site, so the macro is safe to reuse across policies. The macro is spliced into a comparison inside exists, never called on its own: the login_count_positive rule permits an Alert only when the same user has had at least one Login on the same server within the last hour (count == n and n > 0).

The trace shows both outcomes:

• @0 — alice logs in on s1 (a history-only event; no Alert permit applies, so the decision is a deny).
• @100 — alice raises an Alert on s1, 100s after her login → allow (a matching login is within the 1h window and the count is positive).
• @200 — bob raises an Alert on s2 with no prior login → deny.

Referenced by guide/06-macros.md.

Policy

// An aggregation-flavoured temporal macro: `count_formerly(?w, ?s)` counts
// the timepoints in a window at which a predicate held. It is spliced into a
// comparison inside `exists`, never called on its own. Note `$t` is a fresh
// binder the macro introduces itself, hygienically renamed per call site.
def temporal count_formerly(?w, ?s) {
    count for ($t: Timepoint). where (formerly within ?w (?s && tp($t)))
};

@id("login_count_positive")
permit (
    principal,
    action == Drupe::Action::"Alert",
    resource
)
when temporal {
    exists (n: Long). (
        (count_formerly(1h, Drupe::Action::"Login"::request{
            input.user: _, input.server: context.input.server
        })) == n
        && n > 0
    )
};

Schema

namespace Drupe {
  type AlertInput = {
    level: Long,
    server: String
  };

  type AlertOutput = {  };

  type ContentFilterFinding = {
    severityScore: decimal
  };

  type LoginInput = {
    server: String,
    user: String
  };

  type LoginOutput = {  };

  type PromptAttackFinding = {
    severityScore: decimal
  };

  type SensitiveInfoFinding = {
    confidenceScore: decimal
  };

  type SystemContext = {
    now: datetime
  };

  entity Gateway;

  entity IamEntity = {
    id: String
  };

  entity OAuthUser = {
    id: String
  } tags String;

  entity UnauthenticatedUser;

  action "Alert" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: AlertInput,
      output?: AlertOutput,
      system: SystemContext
    }
  };

  action "CallTool" in [Action::"Mcp"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "Http" appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "InvokeAgent" in [Action::"Http"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input?: {      },
      system: SystemContext
    }
  };

  action "InvokeLLM" in [Action::"Http"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input?: {      },
      system: SystemContext
    }
  };

  action "Login" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: LoginInput,
      output?: LoginOutput,
      system: SystemContext
    }
  };

  action "Mcp" appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "UnknownTool" in [Action::"CallTool"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };
}

Trace

@0 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { server: "s1", user: "alice" }) Drupe::Action::"Login"::request(input: { server: "s1", user: "alice" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@100 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { level: 1, server: "s1" }) Drupe::Action::"Alert"::request(input: { level: 1, server: "s1" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u2")
@200 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { level: 1, server: "s2" }) Drupe::Action::"Alert"::request(input: { level: 1, server: "s2" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u3")

Expected Output

@0 (time point 0): DENY
@100 (time point 1): ALLOW  [rules: 0]
@200 (time point 2): DENY