Repair by disagreement

This chapter computes a diff between two candidate Dogwood policies produced from the same natural-language requirement. The diff ignores known language equivalences, locates the remaining variation points, and presents the alternatives at each point. These localized alternatives drive clarification of the original intent.

Dogwood and temporal policies

Dogwood is a Cedar-derived policy language for authorization over event histories. Its temporal sublanguage is a bounded, past-only fragment of Metric First-Order Temporal Logic (MFOTL). It provides event predicates, formerly, previous, since, and the count and sum aggregations. Every temporal operator has a bounded look-back window.

A when temporal { phi } clause evaluates phi at the current decision timepoint against the recorded event history. The event schema determines the fields carried by each action and event kind. Request events carry inputs. Response events can additionally carry outputs such as an HTTP status code.

The original requirement is:

The agent may POST to /deploy, but only if a health check has already come back 200 in the last 15 minutes.

There is no reference policy against which to compare a generated answer. We instead compare two independently produced candidates and use their localized differences to formulate review questions.

The two candidates

Candidate A retains both current-request guards. Its temporal predicate, however, reads output.status_code from a request event:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { context.input.method == "POST" && context.input.path == "/deploy" }
when temporal {
    (count for (t: Timepoint). where (
        formerly within 15m (
            Strands::Action::"http:request"::request{
                callerPrincipal: principal,
                output.status_code: 200
            }
            && tp(t)
        )
    )) >= 1
};

Candidate B uses the response event kind but omits the /deploy guard:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { "POST" == context.input.method }
when temporal {
    1 <= (count for (t: Timepoint). where (
        formerly within 900s (
            tp(t)
            && Strands::Action::"http:request"::response{
                 output.status_code: 200,
                 callerPrincipal:    principal
               }
        )
    ))
};

The missing guard is a fail-open behavior. After a matching 200 response, candidate B permits a POST to /admin/purge-all as well as a POST to /deploy.

The candidates also contain six presentational differences:

difference	representation in Semper
Cedar condition order	`eAnd :assoc-comm-idem`
temporal conjunction order	`tAnd :assoc-comm-idem`
predicate field order	`args :assoc-comm-idem`
`method == "POST"` versus `"POST" == method`	`eEq :comm`
`15m` versus `900s`	rewrite `mins` through `secsTimes`, then constant-fold its product
`count >= 1` versus `1 <= count`	`(birewrite (tLte a b) (tGte b a))`

Encoding Dogwood in Semper

Semper does not evaluate Dogwood policies. It represents their abstract syntax as sorted first-order terms so that policies can be compared modulo the declared algebraic properties of the language operators and rewrite rules encoding known identities in the language. Dogwood remains responsible for validating and replaying completed policies.

The model retains the policy head, Cedar conditions, temporal conditions, aggregation binders, field paths, and request and response event kinds. The main correspondences are:

Dogwood construct	Semper representation
`permit (...) when ...`	`rule`, `permit`, and `head`
Cedar conditions and multiple `when` clauses	`Expr` terms under `eAnd`
`when temporal { phi }`	`(temporal phi)`
`formerly within 15m phi`	`(formerly (mins 15) phi)`
`formerly within 900s phi`	`(formerly (secs 900) phi)`
`Action::"..."::response{...}`	`(pred action response args)`
predicate field assignments	`arg` terms collected by `args`
`count for (t: Timepoint)`	`count`, `bcons`, and `(bvar 0)`
`count(...) >= 1`	`(tGte (agg ...) (tInt 1))`

Here is the complete executable model:

;; EXPECT: ok
;; EVAL: both

;; ANCHOR: dogwood-signature
(sort PolicySet)
(sort Effect)
(sort Scope)
(sort PScope)
(sort AScope)
(sort RScope)
(sort Action)
(sort Expr)
(sort SVal)
(sort TCond)
(sort TTerm)
(sort TAgg)
(sort ArgSet)
(sort Path)
(sort FSeg)
(sort Win)
(sort Ty)
(sort Binders)
(sort Kind)

(function noPolicies () PolicySet)
(function rule (Effect Scope Expr) PolicySet)
(function policies (PolicySet) PolicySet :assoc-comm-idem :identity (noPolicies))
(function permit () Effect)
(function forbid () Effect)

(function head (PScope AScope RScope) Scope)
(function anyPrincipal () PScope)
(function anyResource () RScope)
(function actionEq (Action) AScope)

(function eTrue () Expr)
(function eFalse () Expr)
(function eAnd (Expr) Expr :assoc-comm-idem :identity (eTrue))
(function eOr (Expr) Expr :assoc-comm-idem :identity (eFalse))
(function eEq (Expr Expr) Expr :comm)
(function eCtx (Path) Expr)
(function eStr (SVal) Expr)
(function temporal (TCond) Expr)

(function tTrue () TCond)
(function tAnd (TCond) TCond :assoc-comm-idem :identity (tTrue))
(function formerly (Win TCond) TCond)
(function tp (TTerm) TCond)
(function pred (Action Kind ArgSet) TCond)
(function tGte (TTerm TTerm) TCond)
(function tLte (TTerm TTerm) TCond)

(function bvar (IBig) TTerm)
(function scopePrincipal () TTerm)
(function tInt (IBig) TTerm)
(function agg (TAgg) TTerm)
(function count (Binders TCond) TAgg)
(function bnil () Binders)
(function bcons (Ty Binders) Binders)
(function tyTimepoint () Ty)

(function noArgs () ArgSet)
(function arg (Path TTerm) ArgSet)
(function args (ArgSet) ArgSet :assoc-comm-idem :identity (noArgs))
(function fnil () Path)
(function fld (FSeg Path) Path)
(function secs (IBig) Win)
(function mins (IBig) Win)
(function secsTimes (IBig IBig) Win)

(function request () Kind)
(function response () Kind)
(function aHttpRequest () Action)
(function fInput () FSeg)
(function fOutput () FSeg)
(function fMethod () FSeg)
(function fPath () FSeg)
(function fCallerPrincipal () FSeg)
(function fStatusCode () FSeg)
(function vPOST () SVal)
(function vDeploy () SVal)
;; ANCHOR_END: dogwood-signature

(let methodIsPost
  (eEq (eCtx (fld (fInput) (fld (fMethod) (fnil)))) (eStr (vPOST))))

(let methodIsPostFlipped
  (eEq (eStr (vPOST)) (eCtx (fld (fInput) (fld (fMethod) (fnil))))))

(let pathIsDeploy
  (eEq (eCtx (fld (fInput) (fld (fPath) (fnil)))) (eStr (vDeploy))))

(let healthArgs
  (args
    (arg (fld (fCallerPrincipal) (fnil)) (scopePrincipal))
    (arg (fld (fOutput) (fld (fStatusCode) (fnil))) (tInt 200))))

(let healthArgsFlipped
  (args
    (arg (fld (fOutput) (fld (fStatusCode) (fnil))) (tInt 200))
    (arg (fld (fCallerPrincipal) (fnil)) (scopePrincipal))))

;; ANCHOR: dogwood-candidates
(let candA
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      methodIsPost
      pathIsDeploy
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (mins 15)
                   (tAnd
                     (pred (aHttpRequest) (request) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1))))))

(let candB
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tLte
          (tInt 1)
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (tp (bvar 0))
                     (pred (aHttpRequest) (response) healthArgsFlipped)))))))
      methodIsPostFlipped)))
;; ANCHOR_END: dogwood-candidates

(let pickWorst
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (pred (aHttpRequest) (request) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1)))
      methodIsPost)))

(let repaired
  (rule (permit)
    (head (anyPrincipal) (actionEq (aHttpRequest)) (anyResource))
    (eAnd
      (temporal
        (tGte
          (agg (count (bcons (tyTimepoint) (bnil))
                 (formerly (secs 900)
                   (tAnd
                     (pred (aHttpRequest) (response) healthArgs)
                     (tp (bvar 0))))))
          (tInt 1)))
      methodIsPost
      pathIsDeploy)))

;; ANCHOR: dogwood-identity
(rewrite (mins x) (secsTimes x 60))
(rewrite (secsTimes x y) (secs (IBig::* x y)))
(birewrite (tLte a b) (tGte b a))
(run 4)
(check-eq (mins 15) (secs 900))
;; ANCHOR_END: dogwood-identity

(check-neq candA candB)
(check-neq repaired candA)
(check-neq repaired candB)
(check-neq pickWorst candA)
(check-neq pickWorst candB)
(check-neq repaired pickWorst)

;; ANCHOR: dogwood-main-query
(antiunify candA candB :algorithm exact)
(checkau candA candB :max_size 61 :algorithm exact)
;; ANCHOR_END: dogwood-main-query

(antiunify repaired candA :algorithm exact)
(checkau repaired candA :max_size 60 :algorithm exact)
(antiunify repaired candB :algorithm exact)
(checkau repaired candB :max_size 60 :algorithm exact)
(antiunify pickWorst candA :algorithm exact)
(checkau pickWorst candA :max_size 60 :algorithm exact)
(antiunify pickWorst candB :algorithm exact)
(checkau pickWorst candB :max_size 51 :algorithm exact)

The encoding retains each candidate’s original time unit. The rewrite from mins to secs states the conversion inside the comparison theory:

(rewrite (mins x) (secsTimes x 60))
(rewrite (secsTimes x y) (secs (IBig::* x y)))
(birewrite (tLte a b) (tGte b a))
(run 4)
(check-eq (mins 15) (secs 900))

The first rule builds (secsTimes 15 60). The second rule binds both operands as IBig literal values and evaluates the eager IBig::* primitive, reducing the intermediate term to (secs 900). The equality is therefore derived by visible rewrite rules rather than imposed while translating the policies.

The identity of eAnd represents an omitted condition. It lets the anti-unifier align candidate A’s path guard with eTrue instead of replacing the complete condition with one large variation. Treating Cedar conjunction as commutative assumes its operands have passed validation and cannot produce order-dependent errors. Temporal conjunction is set intersection and does not have that short-circuiting qualification.

The policy diff

The model runs the exact anti-unifier after applying the comparison identity:

(antiunify candA candB :algorithm exact)
(checkau candA candB :max_size 61 :algorithm exact)

The measured result has size 61, compression ratio 0.1864, and two variation points:

(anti-unify :size 61 :cr 0.1864 :completion exact
  (rule
    permit
    (head anyPrincipal (actionEq aHttpRequest) anyResource)
    (eAnd
      (eEq (eCtx (fld fInput (fld fMethod fnil))) (eStr vPOST))
      (temporal
        (tGte
          (agg
            (count
              (bcons tyTimepoint bnil)
              (formerly
                (mins 15)
                (tAnd
                  (tp (bvar 0))
                  (pred
                    aHttpRequest
                    (Variants request response)
                    (args
                      (arg (fld fCallerPrincipal fnil) scopePrincipal)
                      (arg (fld fOutput (fld fStatusCode fnil)) (tInt 200))))))))
          (tInt 1)))
      (Variants (eEq (eCtx (fld fInput (fld fPath fnil))) (eStr vDeploy)) eTrue))))

The first variation asks whether the historical event is a request or a response. The second asks whether the current request must target /deploy or whether the corresponding conjunction slot is eTrue.

All six presentational differences have disappeared. No rewrite equates either of the two reported alternatives.

Checking the four completions

Two binary variation points produce four complete policies:

event kind	path guard	source	validation	off-target replay
`request`	retained	candidate A	fails	not run
`request`	omitted	neither candidate	fails	not run
`response`	omitted	candidate B	passes	allows
`response`	retained	repaired policy	passes	denies

Dogwood validation rejects both request completions:

predicate `Strands::Action::"http:request"::request` mentions field
`output.status_code`, which is not declared on that event

The event schema therefore settles the first variation without a policy reviewer. Request events contain inputs but do not contain response outputs.

Both response completions validate. A replay contains a 200 response, POST /deploy, and then POST /admin/purge-all:

--- candB ---
@60 (time point 0): ALLOW
@120 (time point 1): ALLOW
--- repaired ---
@60 (time point 0): ALLOW
@120 (time point 1): DENY

The validator cannot infer whether /deploy was intended. The requirement settles that variation: retain the path guard. Combining candidate B’s event kind with candidate A’s guard produces a policy written by neither candidate:

@id("deploy_after_health_check")
permit (
    principal,
    action == Strands::Action::"http:request",
    resource
)
when { context.input.method == "POST" && context.input.path == "/deploy" }
when temporal {
    1 <= (count for (t: Timepoint). where (
        formerly within 900s (
            tp(t)
            && Strands::Action::"http:request"::response{
                 output.status_code: 200,
                 callerPrincipal:    principal
               }
        )
    ))
};

Anti-unification localizes the decisions but does not adjudicate them. Dogwood’s schema settles one decision mechanically; the original statement and replay settle the other. A mistake shared by both candidates would remain in their common skeleton, so the correlated-error limitation from Chapter 17 still applies.