docs(nip-fi): make the global-control obligation oracle-detectable

The gate-satisfiability repair left the two global controls
(deny-everything, allow-everything) as normative prose no listed oracle
could detect: FI-CONF-MUTATION required mutants and survivor handling
only, FI-CONF-CLAIM-COMPLETE caught omitted mutant evidence only, and
the release gate names mutants and the denial-fixture control only. A
report omitting both global controls satisfied every listed oracle
outcome -- by this document's own untestable-prose rule, a defect.

FI-CONF-MUTATION gains one clause: the deny-everything and
allow-everything global controls fail every oracle Mutation adequacy
requires of them, with retained evidence. "Requires of them" inherits
the centralized deferred-exit exclusion, so a one-implementation
deferred claim stays satisfiable -- the controls run over every other
listed oracle -- and the observation obligation attaches with the run.

Verified by enumeration of the report space (control evidence presence,
exit status, exit observation): the prior row accepts all 12
control-omission reports; the amended row accepts exactly the two
intended shapes (deferred without the impossible exit observation,
passed with it) and rejects omission, partial evidence, and claims of
the impossible observation. Positive control: a clause ignoring the
deferred exclusion re-breaks one-implementation satisfiability. Oracle
census unchanged at 58.

Co-authored-by: Eva <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: Eva <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
This commit is contained in:
Eva
2026-08-20 10:46:52 -04:00
parent 0863c736d6
commit f76231be52

View File

@@ -462,7 +462,7 @@ They close no item in this gate.
|---|---|
| `FI-CONF-CLAIM-COMPLETE` | A report missing an applicable oracle, duplicating one, carrying a result from another claim tuple, claiming a status other than `pass`/`not-applicable` — or `deferred` on any oracle other than `FI-CONF-INTEROP-EXIT` — or omitting mutant evidence for any oracle other than a deferred `FI-CONF-INTEROP-EXIT`, is rejected. |
| `FI-CONF-DENIAL-FIXTURES` | Every enumerated private condition has a fixture; core and each claimed profile pass exact identifier/class/owner enumeration agreement; anonymity-set responses compare byte-identical; the distinguishing negative control fails. |
| `FI-CONF-MUTATION` | Every listed oracle — except `FI-CONF-INTEROP-EXIT` while validly deferred, per **Mutation adequacy** — has a singly-applied, attributed, reachability-witnessed mutant killed by that entry's own oracle; survivors are recorded, not waived. |
| `FI-CONF-MUTATION` | Every listed oracle — except `FI-CONF-INTEROP-EXIT` while validly deferred, per **Mutation adequacy** — has a singly-applied, attributed, reachability-witnessed mutant killed by that entry's own oracle; the deny-everything and allow-everything global controls fail every oracle **Mutation adequacy** requires of them, with retained evidence; survivors are recorded, not waived. |
| `FI-CONF-INTEROP-EXIT` | Two independent implementations produce, from the documents alone, valid requests equal over the request compared object and per-class denials equal over the denial compared object, and accept each other's output. |
## Security considerations