diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md
index 0b438a1..2fee8d5 100644
--- a/.kiro/specs/access-control-prover/design.md
+++ b/.kiro/specs/access-control-prover/design.md
@@ -226,9 +226,10 @@ the tree-sitter syntax tree of one function (blocks, if/else, switch arms, loops
 finally, return, throw, break, continue, exit) and computes dominators (`dominates(a_line, b_line)`) and the
 control context of a line (`context(line) -> ControlContext(conditions, in_loop, in_try, catches, on_exception_path)`).
 `src/openultrasast/semantic/obligations/cfg_dominance.py::CfgDominance` implements the `Dominance` protocol:
-a statement witness dominates when its block dominates the operation's block and its failure effect is
-`throws`, `returns` or `exits` (the guard's condition leads to an exit on the failing arm; a bare boolean
-whose value no branch or exit consumes before the operation is `value_only`); router and decorator scopes
+a statement witness dominates when its block dominates the operation's block and the operation is unreachable
+from the guard's failing arm: either that arm exits (`throws`, `returns`, `exits`), or the operation lies only
+inside the passing branch (`if (can(x)) { op(); }`, effect `branches`); a bare boolean whose value no branch or
+exit consumes before the operation is `value_only` and never discharges; router and decorator scopes
 dominate as before; along a path record, a witness on an earlier hop dominates as before. Without a graph for
 a function, `CfgDominance` falls back to `OrderDominance` and records `cfg_unavailable`.
 The trace's `Guard` gains `relation` (`all_paths`, `some_paths`, `none`, `after`) and `effect`
diff --git a/.kiro/specs/access-control-prover/requirements.md b/.kiro/specs/access-control-prover/requirements.md
index 551ebc1..15f01a8 100644
--- a/.kiro/specs/access-control-prover/requirements.md
+++ b/.kiro/specs/access-control-prover/requirements.md
@@ -217,8 +217,8 @@ without it, so that a check in a branch the attacker can avoid, or one whose res
    guard's statement (dominators over the graph); the trace shall record each guard's relation to the operation
    as `all_paths`, `some_paths`, `none` or `after`.
 3. The trace shall record each guard's failure effect: `throws`, `returns`, `exits` (break, continue, exit call),
-   or `value_only` when the guard's result is not consumed by a branch or an exit before the operation; a
-   `value_only` guard shall not discharge.
+   `branches` (the operation lies only inside the guard's passing branch), or `value_only` when the guard's
+   result is not consumed by a branch or an exit before the operation; a `value_only` guard shall not discharge.
 4. The trace shall record the operation's control context: the branch conditions it sits under in order (the
    guard's own condition when it is one), whether it is inside a loop, inside a try whose catch swallows the
    guard's exception type, or on an exception path.