write_after_read

The canonical history-dependent policy: permit SellShares only if the same user had an ApproveSale for the same stock within the last hour (formerly within 1h, with the stock pinned via input.stock: context.input.stock).

The trace shows all three cases:

• @0 — ApproveSale for AMZN by alice (a history-only event here; no SellShares permit applies, so the decision is a deny).
• @100 — alice sells AMZN, 100s after the approval → allow (a matching approval is within the window).
• @5000 — bob sells MSFT with no prior approval → deny.

Referenced by guide/04-temporal-expressions.md.

Policy

// Permit selling shares of a stock only if the same user had that sale
// approved within the last hour. The `when temporal { … }` block is the
// temporal marker; its body reads the accumulated event history.
//
// `input.stock: context.input.stock` PINS the approval to the same stock as
// the current request — without the pin this would match an approval for any
// stock.
@id("sell_after_approval")
permit (
    principal,
    action == Drupe::Action::"SellShares",
    resource
)
when temporal {
    formerly within 1h Drupe::Action::"ApproveSale"::response{
        input.stock: context.input.stock
    }
};

Schema

namespace Drupe {
  type ApproveSaleInput = {
    shares: Long,
    stock: String
  };

  type ApproveSaleOutput = {
    approved: Bool
  };

  type ContentFilterFinding = {
    severityScore: decimal
  };

  type GetStockInfoInput = {
    stock: String
  };

  type GetStockInfoOutput = {
    info: String
  };

  type PromptAttackFinding = {
    severityScore: decimal
  };

  type SellSharesInput = {
    shares: Long,
    stock: String
  };

  type SellSharesOutput = {
    proceeds: decimal
  };

  type SensitiveInfoFinding = {
    confidenceScore: decimal
  };

  type SystemContext = {
    now: datetime
  };

  entity Gateway;

  entity IamEntity = {
    id: String
  };

  entity OAuthUser = {
    id: String
  } tags String;

  entity UnauthenticatedUser;

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

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

  action "GetStockInfo" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: GetStockInfoInput,
      output?: GetStockInfoOutput,
      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 "Mcp" appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "SellShares" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: SellSharesInput,
      output?: SellSharesOutput,
      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: { shares: 5, stock: "AMZN" }) Drupe::Action::"ApproveSale"::request(input: { shares: 5, stock: "AMZN" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@50 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { shares: 5, stock: "AMZN" }) Drupe::Action::"ApproveSale"::response(input: { shares: 5, stock: "AMZN" }, output: { approved: true }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@100 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { shares: 5, stock: "AMZN" }) Drupe::Action::"SellShares"::request(input: { shares: 5, stock: "AMZN" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u2")
@5000 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { shares: 5, stock: "MSFT" }) Drupe::Action::"SellShares"::request(input: { shares: 5, stock: "MSFT" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u3")

Expected Output

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