93 lines
4.3 KiB
Markdown
93 lines
4.3 KiB
Markdown
|
|
# ADR-0023: a policy is bound by what its seat can see
|
||
|
|
|
||
|
|
status: accepted
|
||
|
|
date: 2026-08-08
|
||
|
|
decided by: agent, under the standing loop authorization
|
||
|
|
tier: S (states a rule that already held in practice, and makes it
|
||
|
|
checkable; no interface moved)
|
||
|
|
references: [ADR-0013](ADR-0013-the-retrospective-search.md) (why the
|
||
|
|
retrospective search may see everything), [CB-RES-0009](../research/CB-RES-0009-extensive-form-is-the-lingua-franca.md)
|
||
|
|
(information sets), [specs/GameDesign.md](../specs/GameDesign.md) §1.4
|
||
|
|
(sensitivity), F27
|
||
|
|
|
||
|
|
## Context
|
||
|
|
|
||
|
|
`Policy::choose` takes `&GroundState`. `GroundState` carries every
|
||
|
|
face-down Problem's suit and value and every seat's hand.
|
||
|
|
`GroundState::project` exists precisely to withhold those:
|
||
|
|
`ProblemView::FaceDown` carries nothing but the fact that a Problem is
|
||
|
|
there.
|
||
|
|
|
||
|
|
**So the trait hands a bot exactly the information the projection was
|
||
|
|
written to hide.** No shipped policy reads it — `GreedyPolicy::rank`
|
||
|
|
touches only `stress`, `claimed_by` and the legal set — but nothing
|
||
|
|
prevents it, and nothing would notice.
|
||
|
|
|
||
|
|
This stops being latent immediately. CB-WP-0049 writes policies whose job
|
||
|
|
is to **value Problems** in order to test F27, and a Problem's value is
|
||
|
|
the field the projection hides. A seat that ranks a claim by the value of
|
||
|
|
a face-down card is playing a game nobody can play, and every number
|
||
|
|
measured with it would be about that game.
|
||
|
|
|
||
|
|
## D1 — a policy may not depend on what its seat cannot see
|
||
|
|
|
||
|
|
A measurement made with a peeking policy is not a measurement of GROUND.
|
||
|
|
|
||
|
|
**This is the mirror of ADR-0013 D1**, and the pairing is the point. The
|
||
|
|
retrospective search is *allowed* to see everything, because after the
|
||
|
|
game there is one world and a line found in it was executable in the only
|
||
|
|
world there was. A policy plays **during** the game, from inside an
|
||
|
|
information set, so the same permission would be a different claim
|
||
|
|
entirely — the classic strategy-fusion error.
|
||
|
|
|
||
|
|
Same repository, two searches over the same kernel, opposite permissions,
|
||
|
|
and the discriminator is **when the question is asked**.
|
||
|
|
|
||
|
|
## D2 — checked behaviourally, not by the type system
|
||
|
|
|
||
|
|
The obvious enforcement is to change `choose` to take `&GroundView`. We do
|
||
|
|
not do that first, because a **behavioural control catches more**:
|
||
|
|
|
||
|
|
> Vary only what the seat cannot see, and assert the policy's choice does
|
||
|
|
> not move.
|
||
|
|
|
||
|
|
- It binds **every** policy, including ones written later and ones written
|
||
|
|
outside this crate, without their cooperation.
|
||
|
|
- It survives a policy that gets the view and reconstructs hidden state by
|
||
|
|
other means.
|
||
|
|
- It is the sensitivity discipline the project already runs on
|
||
|
|
(GameDesign §1.4): name the variable, vary it, watch the number.
|
||
|
|
|
||
|
|
A type change makes one route unavailable; the control makes the property
|
||
|
|
false-if-violated. **The type change is still worth doing** and is not
|
||
|
|
refused here — it is simply not the thing that establishes the property.
|
||
|
|
|
||
|
|
## D3 — the control must be shown to fail
|
||
|
|
|
||
|
|
A peek control that no policy can fail is decoration (ADR-0006 D3). The
|
||
|
|
test carries a deliberately peeking policy — one that ranks by the value
|
||
|
|
of face-down Problems — and asserts **that** policy is caught. A control
|
||
|
|
proven only against compliant policies has not been proven at all.
|
||
|
|
|
||
|
|
## Consequences
|
||
|
|
|
||
|
|
- Every policy is covered by the peek control, and a new one that peeks
|
||
|
|
goes red on arrival rather than on review.
|
||
|
|
- Hidden-information variation becomes a fixture: the same helper that
|
||
|
|
proves policies blind can measure how much a line depended on what was
|
||
|
|
hidden.
|
||
|
|
- Policies that must reason about unseen Problems have to do it as
|
||
|
|
*inference from what is visible* (a face-down Problem exists, and the
|
||
|
|
scenario states the deal), which is the honest form of the same
|
||
|
|
reasoning.
|
||
|
|
- Bots remain unable to test claims about mechanisms they do not attend to
|
||
|
|
— an orthogonal limit, recorded as F27, and **not** addressed by this.
|
||
|
|
|
||
|
|
## What was rejected
|
||
|
|
|
||
|
|
| rejected | why |
|
||
|
|
|---|---|
|
||
|
|
| changing `choose` to `&GroundView` first | closes one route; the property still would not be checked, and outside policies could still peek |
|
||
|
|
| trusting review | four reviews on this repo found five, three, four and two FATAL items; peeking is invisible in a diff that looks like ranking |
|
||
|
|
| allowing peeking for "stronger" bots | a stronger bot at a game nobody can play measures that game; ADR-0013 D1's permission is retrospective and does not transfer |
|