For agents

#Failure semantics

Every rejection is atomic and fail-closed: nothing partial is ever applied, and the response tells you which gate fired.

Agent rule of thumb: 409 means the state forbids it (back off, or it will keep failing until the window moves); 403 means you may not do it (fix the caller or the payload, not the timing).

#Worked example: the spend cap

With rollingSum(amount) ≤ 100 over 3600s declared on agents/$agentId/spend (see the quickstart policy), a sequence of individually plausible writes behaves like this:

$ USER_ID="$(bounded whoami --json | jq -r .id)"
$ bounded data set --path "agents/$USER_ID/spend/s1" --data '{"amount": 60}'
✓ committed                                  # window sum: 60 / 100

$ bounded data set --path "agents/$USER_ID/spend/s2" --data '{"amount": 60}'
✗ 409 postcondition failed: invariant "spend_cap" requires
  rolling sum(agents/$agentId/spend/$spendId.amount) <= 100
  # 60 + 60 = 120
  nothing committed

$ bounded data set --path "agents/$USER_ID/spend/s3" --data '{"amount": 40}'
✓ committed                                  # window sum: 100 / 100

$ bounded data set --path "agents/$USER_ID/spend/s4" --data '{"amount": 1}'
✗ 409 postcondition failed: invariant "spend_cap" requires
  rolling sum(agents/$agentId/spend/$spendId.amount) <= 100
  # 100 + 1 = 101

The second 60 is rejected even though it is identical to the first, the cap is about the window sum, not the write. The 40 lands exactly on the cap; the 1 after it fails. There is no payload an agent can construct that lands the window above 100: that is the property the prover discharged at deploy.

#Atomic set-many & in-batch composition

bounded data set-many submits multiple writes as one transaction: every rule, every invariant, every hook either passes for the whole batch or the whole batch is rejected. This is what makes conserve usable, a transfer is a debit and a credit that only exist together:

# balanced: -50 here, +50 there, one atomic batch → accepted
$ cat transfer.json
[
  { "path": "accounts/alice", "document": { "balance": 50 } },
  { "path": "accounts/bob", "document": { "balance": 150 } }
]
$ bounded data set-many --from-json transfer.json
✓ committed 2 document(s)                    # 100+100 → 50+150, total preserved

# unbalanced: -50 / +40 → the whole batch is rejected
$ bounded data set-many --from-json bad-transfer.json
✗ 409 postcondition failed: invariant "no_minting" requires
  sum(accounts/$id.balance) to be conserved
  conserve(balance): write-set sum 190 != 200
  nothing committed, neither document changed

In-batch composition

Rules evaluate against staged state: the rule for entry N sees the results of entries 0..N-1 via getAfter(). That turns set-many into a composition primitive, guard documents and the writes they gate travel in one atomic unit, with no TOCTOU window between check and act:

# gated/$docId create rule:
#   "getAfter(/allowlist/@user.id).approved == true"
# Replace <your-user-id> below with: bounded whoami --json | jq -r .id
#
# One batch creates the allowlist entry AND the gated write.
# The rule on entry N sees entries 0..N-1, staged, atomic.
[
  { "path": "allowlist/<your-user-id>", "document": { "approved": true } },
  { "path": "gated/g1", "document": { "value": 7 } }
]
$ bounded data set-many --from-json compose.json
✓ committed 2 document(s)

# Reverse the order and the gate sees no staged entry → whole batch 403s.

• Order matters: stage the guard before the write that reads it.
• get() reads pre-batch state; getAfter() reads staged state. Use getAfter for any post-condition (“balance still ≥ floor after the transfer”).
• Distinct paths per entry, in-batch path collisions reject.

#Append-only caps

Collections under a rollingSum are append-only event logs: update and delete are rejected, so the history a cap is computed from cannot be rewritten, not by a compromised agent, not by your own buggy retry loop. Write each spend as a new document with a fresh id; idempotency comes from your ids, not from overwrites.

#Machine-readable docs

• /llms.txt, entry point: setup flow, runtime semantics, SDK pointers.
• /llms-full.txt, the condensed policy reference: every key, every invariant type, failure semantics, and the worked examples above, in one plain-text file.
• /llms.txt provides the short public setup and execution loop for coding agents.