Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

cap_open_agent_prs_windowed

EXPERIMENTAL. This bundle uses arithmetic in temporal comparison operands, gated behind the off-by-default Cargo feature experimental-arithmetic. A default build rejects this policy; the test harnesses check this bundle only when built with that feature.

This bundle exercises - between two aggregates (a cap on open PRs).

A cap on concurrently open pull requests. A coding agent may hold at most 3 open PRs at once, so a new open is allowed only while fewer than 3 are open, measured as opens minus completed reviews in the 24h window. The guard runs before the new PR lands, which is why “at most 3 open” reads as < 3 at decision time.

permit (principal, action == Repo::Action::"OpenPullRequest", resource)
when temporal {
    (count for (t: Timepoint). where (
        formerly within 24h (Repo::Action::"OpenPullRequest"::response{} && tp(t))
    ))
    - (count for (t: Timepoint). where (
        formerly within 24h (Repo::Action::"CompleteReview"::response{} && tp(t))
    )) < 3
};

Without arithmetic only the exact comparison reviewed < opened is writable; the cap constant has nowhere to go. Both aggregates are parenthesized (the fencing rule: an aggregate anywhere but the final position of the final operand fences its greedy where body). The counts match response events, so a denied open attempt does not consume the cap.

Replay

opened − reviewed is the number of PRs open at the moment of decision; the request being decided is not yet among them.

Decision pointEventOpen PRs (opened − reviewed)Verdict
@0open r10 − 0 = 0allow (r1 is the 1st open PR)
@10open r21 − 0 = 1allow (2nd)
@20open r32 − 0 = 2allow (3rd)
@30open r43 − 0 = 3deny (r4 would be the 4th)
@40review v1not OpenPullRequestdeny
@50open r53 − 1 = 2allow (back up to 3 open)

The denied @30 attempt has no response, so it does not count at @50; the completed review at @41 is what reopens capacity.

Files

  • policy.dw: the permit with the count difference.
  • schema.cedarschema: Repo action schema (OpenPullRequest, CompleteReview).
  • trace.log: four open attempts, one completed review, one more open, all by the agent principal devin.
  • expected.out: the per-decision-point verdict stream.

Reproduce (run from this directory):

dogwood validate policy.dw --policy-schema schema.cedarschema
dogwood replay   policy.dw --policy-schema schema.cedarschema --trace trace.log

World: repo. Default event schema; no providers.

Referenced by guide/04-temporal-expressions.md (arithmetic in comparison operands).

Policy

// A cap on concurrently open PRs: a coding agent may hold at most 3 open
// pull requests at once. A new open is allowed only while fewer than 3
// are open, measured as opens minus completed reviews in the 24h window;
// the guard runs before the new PR lands, so `< 3` now means at most 3
// open afterwards.
//
// The `-` between the two counts is the arithmetic this bundle exists to
// exercise. Without it only the exact comparison `reviewed < opened` is
// writable, and the cap constant has nowhere to go.
//
// Both counts match `response` events (successful opens and completed
// reviews), not requests. A denied open attempt stays in the trace, so
// counting requests would let denials consume the cap.

@id("cap_open_agent_prs_windowed")
permit (
    principal,
    action == Repo::Action::"OpenPullRequest",
    resource
)
when temporal {
    (count for (t: Timepoint). where (
        formerly within 24h (Repo::Action::"OpenPullRequest"::response{} && tp(t))
    ))
    - (count for (t: Timepoint). where (
        formerly within 24h (Repo::Action::"CompleteReview"::response{} && tp(t))
    )) < 3
};

Schema

namespace Repo {
  type OpenPullRequestInput = {
    repo: String
  };

  type OpenPullRequestOutput = {  };

  type CompleteReviewInput = {
    repo: String
  };

  type CompleteReviewOutput = {  };

  type SystemContext = {
    now: datetime
  };

  entity Gateway;

  entity OAuthUser = {
    id: String
  } tags String;

  action "OpenPullRequest" appliesTo {
    principal: [OAuthUser],
    resource: [Gateway],
    context: {
      input: OpenPullRequestInput,
      output?: OpenPullRequestOutput,
      system: SystemContext
    }
  };

  action "CompleteReview" appliesTo {
    principal: [OAuthUser],
    resource: [Gateway],
    context: {
      input: CompleteReviewInput,
      output?: CompleteReviewOutput,
      system: SystemContext
    }
  };
}

Trace

@0 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"OpenPullRequest"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r1")
@1 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") Repo::Action::"OpenPullRequest"::response(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r1")
@10 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"OpenPullRequest"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r2")
@11 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") Repo::Action::"OpenPullRequest"::response(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r2")
@20 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"OpenPullRequest"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r3")
@21 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") Repo::Action::"OpenPullRequest"::response(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r3")
@30 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"OpenPullRequest"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r4")
@40 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"CompleteReview"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "v1")
@41 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") Repo::Action::"CompleteReview"::response(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "v1")
@50 scope(principal: Repo::OAuthUser::"devin", resource: Repo::Gateway::"gw1") request_context(input: { repo: "web" }) Repo::Action::"OpenPullRequest"::request(input: { repo: "web" }, callerPrincipal: Repo::OAuthUser::"devin", callerResource: Repo::Gateway::"gw1", requestId: "r5")

Expected Output

@0 (time point 0): ALLOW  [rules: 0]
@10 (time point 1): ALLOW  [rules: 0]
@20 (time point 2): ALLOW  [rules: 0]
@30 (time point 3): DENY
@40 (time point 4): DENY
@50 (time point 5): ALLOW  [rules: 0]